Fix and prove the Bernstein-Yang word-by-word Montgomery specs (scrutineer #2522, #2523, #2524)

[JasonGross]

Fixes scrutineer findings #2522, #2523 and #2524 (one shared root cause).

The bug

The three Bernstein-Yang operations of the word-by-word Montgomery synthesis (msat, divstep_precomp, divstep) were the only word-by-word Montgomery operations whose Definition <op>_correct in src/COperationSpecifications.v had no discharged Lemma <op>_correct in src/PushButtonSynthesis/WordByWordMontgomery.v. Those Props are pretty-printed verbatim into the Postconditions: doc-comment of every generated C/Rust/Go/Zig/Java file, so the generated files shipped contracts that nothing ever checked, and all three were false:

• #2524 msat_correct asserted twos_complement_eval msat = m /\ valid msat; valid includes eval msat < m, so this is unconditionally false (the output is exactly m). The generated comment claimed 0 ≤ eval out1 < m, which is verbatim the precondition of every Montgomery-domain function in the same file.
• #2523 divstep_precomp_correct equated a field element with the unreduced power ((m - 1) / 2) ^ i (no mod m) and used the wrong base: the emitted constant is ((m + 1) / 2) ^ i mod m (i.e. 2^-i mod m, the inverse of 2 to the iteration count), which is what divstep_precompmod computes. I confirmed this numerically against the shipped constants of p256_64, p256_32 and secp256k1_montgomery_64.
• #2522 divstep_correct wrote the fifth output of the odd branch as (eval (from_montgomery v) - eval (from_montgomery v)) mod m (identically 0) instead of r - v, and its bounds line read valid r1 /\ valid r1 /\ valid f1 /\ valid g1.

Verifying the report against the definitions turned up more defects in the same specs that the report did not mention:

• twos_complement_eval was eval_twos_complement bitwidth n (over the n Montgomery limbs) while msat, f and g carry sat_limbs = n + 1 limbs. For p256 (m ≥ 2^255) that reads m as a negative 256-bit integer, so even twos_complement_eval msat = m was false, and the Computed values header defining twos_complement_eval z in every generated file described a 4-limb evaluation applied to 5-limb arrays.
• valid f1 /\ valid g1 can never hold (f1, g1 have sat_limbs limbs and f may equal m); the true statement is the saturated limb bound established by the bounds pipeline.
• d1 = 1 - d ignores that d is a two's-complement machine word; BYInv.divstep_correct_full is stated with Z.twos_complement bitwidth d.
• The Bernstein-Yang preconditions on divstep (f odd; |f|, |g|, |d| bounded away from overflow) were missing, so the spec was unprovable as stated.

The fix

• src/COperationSpecifications.v: the three specs are restated so that they are true and provable from the existing Arithmetic development. msat_correct and divstep_correct take sat_limbs; twos_complement_eval is over sat_limbs limbs; d is interpreted with Z.twos_complement; msat gets the saturated limb bounds instead of valid; divstep_precomp gets mod m on both sides and the base (m + 1) / 2; divstep gets r - v, valid v1, the bounds on d1/f1/g1 and the required preconditions.
• src/Arithmetic/BYInv.v: new lemmas divstep_valid (the Montgomery-domain outputs v1, r1 are valid), select_valid, length_valid, eval_twos_complement_partition.
• src/PushButtonSynthesis/WordByWordMontgomery.v: discharged Lemma msat_correct, Lemma divstep_precomp_correct, Lemma divstep_correct plus Wf_msat/Wf_divstep_precomp/Wf_divstep (added to the wf_op_cache hints), following the pattern of the other 16 operations, so that the printed contracts are theorems from now on. The doc-comment context maps twos_complement_eval to the sat_limbs evaluation and adds twos_complement for the single word d; the Computed values header defines both at the right width. use_curve_good additionally exports 1 < machine_wordsize (already enforced by check_args; appended after the existing conjuncts so positional destructs elsewhere are unaffected).
• src/PushButtonSynthesis/Primitives.v: the correctness-stringification printer strips leading list_Z_bounded_by / word-bound conjuncts (previously only a single trailing one was supported) and prints Z.odd x = true as x is odd. Existing outputs are unaffected (no other generated file changes).
• Generated files: regenerated with the rebuilt word_by_word_montgomery and bedrock2_word_by_word_montgomery binaries. Only the Postconditions:/Preconditions: doc-comments of msat, divstep, divstep_precomp and the Computed values header change; the generated code is byte-for-byte unchanged.

Example (p256_64, C)

  * Preconditions:
  *   0 ≤ eval arg4 < m
  *   0 ≤ eval arg5 < m
  *   -2^(64 - 1) + 1 < twos_complement arg1 < 2^(64 - 1) - 1
  *   (twos_complement_eval arg2) is odd
  *   -2^(64 * 5 - 2) < twos_complement_eval arg2 < 2^(64 * 5 - 2)
  *   -2^(64 * 5 - 2) < twos_complement_eval arg3 < 2^(64 * 5 - 2)
  * Postconditions:
  *   twos_complement out1 = (if 0 < twos_complement arg1 ∧ (twos_complement_eval arg3) is odd then 1 - twos_complement arg1 else 1 + twos_complement arg1)
  *   ...
  *   eval (from_montgomery out5) mod m = (if 0 < twos_complement arg1 ∧ (twos_complement_eval arg3) is odd then (eval (from_montgomery arg5) - eval (from_montgomery arg4)) mod m else ...)
  *   0 ≤ eval out4 < m
  *   0 ≤ eval out5 < m

Alternatives considered

• Keeping n-limb twos_complement_eval and only fixing the three reported lines: the resulting specs would still be false (see above) and unprovable.
• Stating the precomp value as (2^i * eval (from_montgomery out1)) mod m = 1: equivalent, but the chosen form mirrors divstep_precompmod exactly and matches the existing style.
• Not changing the printer: the new bounds conjuncts and the f odd precondition could not be rendered otherwise.

Verification

All verification was done with the overlay build described in the team notes (local coqc -q -R src Crypto ... against the installed coq-fiat-crypto-with-bedrock, Rocq 9.4+alpha), not a full make.

Numeric check of the report's claims (Python, against the shipped constants in fiat-c/src/{p256_64,p256_32,secp256k1_montgomery_64}.c): eval(msat) == m in all three; ((m+1)/2)^i mod m equals the emitted precomp constant in all three and ((m-1)/2)^i mod m does not (i = 741 for the 256-bit moduli).

Coq (all compiled successfully, in dependency order):

• src/Arithmetic/BYInv.v, src/COperationSpecifications.v, src/PushButtonSynthesis/Primitives.v, src/PushButtonSynthesis/BYInversionReificationCache.v
• all six src/PushButtonSynthesis/{BaseConversion,DettmanMultiplication,SaturatedSolinas,SolinasReduction,UnsaturatedSolinas,WordByWordMontgomery}.v (the last one carries the three new _correct lemmas and the doc-comment generation)
• src/CLI.v, src/StandaloneOCamlMain.v, src/ExtractionOCaml/word_by_word_montgomery.v
• the 11-file bedrock2 cone (src/Bedrock/Field/Common/{Util,Tactics}.v, Translation/Proofs/{UsedVarnames,EquivalenceProperties,Flatten,LoadStoreList}.v, Common/Arrays/MakeAccessSizes.v, Common/Names/MakeNames.v, Translation/Parameters/Defaults.v, Stringification/Stringification.v, src/Bedrock/Standalone/StandaloneOCamlMain.v) and src/ExtractionOCaml/bedrock2_word_by_word_montgomery.v
• the 32-file cone up to src/Bedrock/Field/Synthesis/New/{WordByWordMontgomery,UnsaturatedSolinas}.v (these consume use_curve_good and the specs), compiled with the HEAD src/Bedrock/Field/Common/Types.v

Binaries and generated files: both src/ExtractionOCaml/word_by_word_montgomery and src/ExtractionOCaml/bedrock2_word_by_word_montgomery were rebuilt from the extracted OCaml with the Makefile's ocamlfind ocamlopt invocation, and all 136 generated files that request msat/divstep/divstep_precomp were regenerated via make -f Makefile.examples <targets> WORD_BY_WORD_MONTGOMERY=... BEDROCK2_WORD_BY_WORD_MONTGOMERY=.... The 21 fiat-json files came out byte-identical (JSON carries no doc-comments); the other 115 changed. A check over git diff confirms every added/removed line in the generated files is a comment line (/* */, //, ///, //!).

Compile checks of the regenerated files:

• C: cc -Wall -Wno-unused-function -Wpedantic -Werror -c on all 21 touched fiat-c/src/*.c (the test-c-files flags) and cc -Wall -Wno-unused-function -Werror -Wno-error=unused-but-set-variable -c on all 21 touched fiat-bedrock2/src/*.c: all pass.
• Go: go build ./... in fiat-go: passes.
• Zig: zig build test in fiat-zig: passes (its test driver only exercises a subset of functions).

Not verified (please rely on CI):

• Rust: no cargo/rustc on this machine, so fiat-rust was not built. The Rust changes are //!//// comment lines only.
• Java: no javac, so fiat-java was not compiled (comment lines only).
• A full make of the repository, including src/Bedrock/End2End/**, the Haskell/JS extractions and CI's regeneration check.

🤖 Generated with Claude Code

https://claude.ai/code/session_016Rbn2gww3MGhvrh52fNjpD