Saturated experiment revived

[andres-erbsen]

Perhaps there is a way forward here after all.

• Instead of #1761, a less ambitious alternative would be to add a special if to the pipeline IR for cases where a specific branch is expected to be taken, and the other branch is only there for proof purposes. Only the expected-dead branch should be thunked. Thus there wouldn't be a need to do bounds analysis inside a thunk.
• #1778 perf impact could be avoided (or at least reduced) by uncurrying list_rect in templates
• #1777 issue is probably a rewrite-rule conflict and it looks like perhaps it could be debugged to satisfaction. EDIT: I posted a hypothesis/proposal there.
• #2121 would need to be finished up to actually get appropriately efficient Bedrock2 code out after template instantiation

@JasonGross did I get this right?

[JasonGross]

@JasonGross did I get this right?

Yes, that sounds right to me

[andres-erbsen]

The first step listed above seems like the most uncertain still, so if we want to move forward here, that would be the one to try first. Following

• 31c76f820862e902f19f043fb428ab4521fe92f8 is a commit that adds new operations to rewrite
• https://github.com/mit-plv/fiat-crypto/blame/master/src/Util/Bool.v#L135 has full thunked bool operators; we want one that is only thunked in one argument
• This new operation would be used to replace all if in synthesizable definitions in src/Arithmetic/SaturatedPseudoMersenne.v