Using word_by_word_montgomery with one-word prime modulus

[divergentdave]

I have a use case where I'd like to try using fiat-crypto with smaller prime moduli, such that the modulus can fit in one machine word. (see divviup/libprio-rs#757) Currently, this doesn't work. Running ./src/ExtractionOCaml/word_by_word_montgomery --lang Rust --inline field64 64 18446744069414584321 opp returns an error and dumps some IR. The issue is that Z.zselect appears deep inside an expression, when it can only be synthesized if it's the top-level node of a let binding.

Comparing the IR to successful output from a similar invocation with a two-word prime, ./src/ExtractionOCaml/word_by_word_montgomery --lang Rust --inline --debug on-success field128 64 340282366920938462946865773367900766209 opp, I noticed that the bad substitution happened following the line After rewriting subst01 for RewriteArith_0. It appears this is a particular case of #1477. I made the following patch, and it fixed the issue with synthesizing opp() (though this sort of workaround would be a game of whack-a-mole).

diff --git a/src/PushButtonSynthesis/WordByWordMontgomery.v b/src/PushButtonSynthesis/WordByWordMontgomery.v
index 74888dc11..01149e3c1 100644
--- a/src/PushButtonSynthesis/WordByWordMontgomery.v
+++ b/src/PushButtonSynthesis/WordByWordMontgomery.v
@@ -356,7 +356,7 @@ Section __.
 
   Definition opp
     := Pipeline.BoundsPipeline
-         true (* subst01 *)
+         false (* subst01 *)
          possible_values
          (reified_opp_gen
             @ GallinaReify.Reify (machine_wordsize:Z) @ GallinaReify.Reify n @ GallinaReify.Reify m)

[JasonGross]

It appears this is a particular case of #1477.
Indeed

I made the following patch, and it fixed the issue with synthesizing opp() (though this sort of workaround would be a game of whack-a-mole).

Let me know if you're interested in trying the more ambitious fix, of writing the pass that fixes #1477. I'm happy to advise on how to implement this if you want to give it a shot. (Note that SubstVarLike already exists, so the only pass to write is the one that let-binds applications of selected idents, and then piping the machinery that invokes the pass and records the idents to be bound for each backend)