mit-plv/fiat-crypto

Remove `subst01` knob

JasonGross opened this issue · 0 comments

Controlling subst01 on a per-field-operation is a kludge to work around the fact that some operations cannot occur in arithmetic expressions in some language backends like C, because they are emitted in the style where we pass in pointers to the return values rather than returning the values.

We should instead have a final pass that let-binds the return-passing-style operations---which should be specified per-backend not per-operation---and then inlines only let-bound variables (not things that are used only once). Then we can hopefully hardcode subst01 to true.