Saturated experiment revived

[andres-erbsen]

Perhaps there is a way forward here after all.

• Instead of Don't replace abstract state of higher order functions with bottom when we can avoid it (now guarded by --fancy-and-powerful-but-exponentially-slow-bounds-analysis) #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.
• Add remaining rewrite rules for saturated arithmetic #1778 perf impact could be avoided (or at least reduced) by uncurrying list_rect in templates
• Unobjectionable rewrite rules for saturated arithmetic #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.
• Preserve two-output operations from Rewriter Pipeline to Bedrock2 #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]

Another alternative to #1761 would be to remove this kind of checks from the templates, avoiding the need to do range analysis on thunks by doing that range analysis in proofs instead. This might involve using list (word 64) instead of list Z. Going in this direction would be shifting work from the rewriter and associated pipeline into tactic-based proofs. However, there's a good chance the resulting code would work with the current rewriter, or perhaps even with eval-cbv (if first transformed to continuation-passing style).

[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

• 31c76f8 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