SAW/MIR: idiomatic way to prove Barrett reduction over x < 2^46 without bit-blasting?

[amarshat]

I’m trying to verify a Barrett reduction in RustCrypto’s module_lattice field core, shared by ml-dsa / ml-kem, using mir_verify.

The relevant function is:

fn barrett_reduce(x: Self::Long) -> Self::Int {   // Long = u64, Int = u32
    let x: Self::LongLong = x.into();              // LongLong = u128
    let product  = x * Self::BARRETT_MULTIPLIER;   // MULTIPLIER = (1<<46)/q = 8396807
    let quotient = product >> Self::BARRETT_SHIFT; // SHIFT = 46
    let remainder = x - quotient * Self::QLL;      // q = 8380417
    Self::small_reduce(Truncate::truncate(remainder))
}

The intended theorem is:

let barrett_spec = do {
    x <- mir_fresh_var "x" mir_u64;
    mir_precond {{ x < (1 << 46) }};           // a*b domain: a,b < q < 2^23
    mir_execute_func [mir_term x];
    mir_return (mir_term {{ drop`{32} (x % 8380417) : [32] }});
};

mir_verify m ".../barrett_reduce" [] false barrett_spec z3;

What I see:

x < 2^28  -> z3 proves in about 4s
x < 2^36  -> no result
x < 2^44  -> no result
x < 2^46  -> no result

I tried z3, abc, cvc5, yices, do { goal_eval_unint []; z3; }, and a carry-folded/reformulated spec. The wider domains time out after several minutes.

My current hypothesis is that the proof is going through bit-vector reasoning over:

((x * 8396807) >> 46)

where x is symbolic over a 2^46-wide domain. That gives a roughly 70-bit intermediate (x < 2^46 times M ≈ 2^23) and the solver ends up bit-blasting the multiply/shift shape rather than using the arithmetic structure of Barrett reduction.

My question:

What is the idiomatic SAW way to discharge this kind of Barrett-style reduction proof?

Specifically, is the usual approach one of these?

1. Keep the proof in BV land, but abstract the quotient:
   quotient = (x * M) >> k, then prove/use a side condition about quotient*q <= x < (quotient+1)*q + small_error, avoiding direct bit-blasting of the wide multiply/shift.

2. Use uninterpreted functions or rewrite lemmas for the shift/multiply quotient shape, then discharge only the small Euclidean/modular obligation.

3. Move to unbounded integer reasoning, prove the Barrett arithmetic there, and bridge BV ↔ Integer inside SAW.

4. Something else entirely, such as proving/extracting a reusable lemma for the reducer and using that as an override everywhere else.

For context, we proved an analogous Montgomery reduction in a C/Cryptol pipeline by lifting the arithmetic into Isabelle. I’m trying to understand whether there is a SAW-native idiom that avoids adding a second prover for this Rust/MIR proof.

Minimal repro:

https://github.com/amarshat/pqc-assay/blob/main/implementations/rustcrypto-ml-dsa/proof/ntt/repro_barrett_2p46.saw

It is a single mir_verify over the reducer. It needs build/mldsa_harness.linked-mir.json, produced by:

scripts/setup_rust.sh
cd implementations/rustcrypto-ml-dsa/harness
cargo +nightly-2025-09-14 saw-build

I can also attach the .linked-mir.json directly if that is easier.

Related scaling issue:

I see a similar shape when verifying one NTT layer, ntt_layer<128,1>, against the FIPS 204 Alg 41 spec. I currently assume the field operations with mir_unsafe_assume_spec; the overrides apply and symbolic simulation finishes, but the final proof obligation times out. The spec computes % q independently per output coefficient, while the implementation reduces after each operation, so the final goal contains many independent modular-reduction obligations.

For that case, is the preferred SAW style to make the spec compositionally use the same override terms, so the proof discharges mostly by rewriting? Or is there a standard tactic/lemma pattern for many independent modular-reduction obligations?

Layer experiment:

https://github.com/amarshat/pqc-assay/blob/main/implementations/rustcrypto-ml-dsa/proof/ntt/layer_assumed_barrett.saw

Toolchain: SAW 1.5.1, solvers bundled with that release.

Context: open formal-verification project on RustCrypto ML-DSA; scalar layer, including Barrett over u32, ct_div, zetas, and hint logic, is already SAW-verified. This wider Barrett proof gates the NTT-layer proofs for FIPS 204 Alg 41/42.

[RyanGlScott]

Hi @amarshat.

Unfortunately, proving the implementation of Barrett reduction is one of those things that SMT-based tools like SAW fundamentally struggle with. I wish I had a deep, technical explanation for why that is, but that gets into details of SMT solvers that are well above my pay grade.

In the past, when we've proven implementations of Montgomery reduction (not quite Barrett reduction, but similar in many ways), we did so by using {llvm,mir}_unsafe_assume_spec to express the low-level operations in terms of Integer operations. I think that this is the "Move to unbounded integer reasoning, prove the Barrett arithmetic there, and bridge BV ↔ Integer inside SAW" operation you propose above. This is not to say that the proof will necessarily fall out for free if you do this (SMT solvers' support for solving Integer queries efficiently also tends to be somewhat limited), but it is usually possible if you are careful to get the proof goals into the right shape.

For that case, is the preferred SAW style to make the spec compositionally use the same override terms, so the proof discharges mostly by rewriting? Or is there a standard tactic/lemma pattern for many independent modular-reduction obligations?

When we did the aforementioned Montgomery reduction proofs, this is more or less the approach that we used. Generally, we applied one or more rewrites on the proof goal to simplify things into a form where the SMT solver could figure out what is going on.

[amarshat]

Thanks @RyanGlScott for the steer 💯

Quick update from my side: I've now mechanized the integer core in SAW - prove_print z3 discharges barrettInt x == x mod q over the full x < 2^46 domain in ~0.7s (where the bit-vector form of the identical goal times out), with a q+1 mutation giving an in-domain counterexample to confirm it's non-vacuous. So the arithmetic side is settled; what's left is precisely the BV↔Integer bridge you describe.
I'll take the mir_unsafe_assume_spec route - expressing the low-level u128 multiply/shift in terms of Integer operations, then rewriting the goal into shape - following the Montgomery precedent. Will report back whether it falls out for barrett_reduce.

And thanks for the confirmation that this class of goal is a fundamental SMT-tooling limitation rather than something I was holding wrong - that's a useful data point; I'm writing up exactly where this tractability boundary falls for ML-DSA's modular arithmetic.

[sauclovian-g]

We ought to have some kind of solver or tactic that specifically lifts bitvectors to bounded integers. Transporting proofs across domains like that is in general a theoretical headache, but this particular case is really not that difficult...

[amarshat]

Thanks both, this helped.

@RyanGlScott the Integer route worked for the arithmetic. I lifted the Barrett identity to unbounded Integer and z3 proves it over the whole domain in about 0.7s:

barrettInt x == x % q    for all x in [0, 2^46)     -- z3, ~0.7s

(non-vacuity: swapping q for q+1 gives an in-domain counterexample). I also wrote the exact bit-vector mirror of the impl and checked it equals x % q for x < 2^24, where the BV form still solves, so I'm confident the model is faithful.

So the arithmetic and the model are both settled. What's left is the BV to Integer bridge itself, and that's where I'm stuck, for two concrete reasons:

1. There's no callable op to assume_spec. In this crate the u128 multiply is an inline MIR BinaryOp(Mul) (the reducer is 2 Mul + 1 Shr + 1 Sub inline, no __multi3/mul callee), so unlike the Montgomery case there's nothing to express in Integer via mir_unsafe_assume_spec. The bridge has to come from rewriting the goal.

2. The bridge rules cliff at the same width. If I try to prove even the atomic shift rule by z3:

toInteger (x >> 46) == toInteger x / 2^46

it proves at width <= 56 and times out at width >= 64. So I can't hand-prove the BV to Integer rules at the width Barrett needs (product < 2^70) and addsimp them; the rule proofs hit the same wall.

@sauclovian-g this looks like exactly the "lift bitvectors to bounded integers" tactic you mentioned, and I agree the case is easy on paper. What I want is to push toInteger through the operations with the standard homomorphisms:

toInteger (zext x)       == toInteger x
toInteger (a * b : [n])  == toInteger a * toInteger b     (needs a*b < 2^n)
toInteger (x >> k)       == toInteger x / 2^k
toInteger (a - b : [n])  == toInteger a - toInteger b     (needs a >= b)
toInteger (drop`{j} r)   == toInteger r                   (needs r < 2^(n-j))

The two side conditions (multiply doesn't wrap, subtract doesn't borrow) both follow from x < 2^46: product < 2^70 < 2^128, quotient < 2^24, quotient*q < 2^47, remainder in [0, 2q) < 2^24. Once toInteger is pushed all the way in, the goal is the pure-Integer identity above, which already discharges.

Two questions:

1. Does SAWCore already expose these bvToInt/bvToNat homomorphism identities as rewrite rules (a Simpset I can addsimp and drive with simplify), or would they need adding to the Prelude and proving width-parametrically (once for all n, not per width)?

2. What's the idiomatic way to discharge the no-wrap and no-borrow side conditions from the input-range precondition inside the rewriter? When I tried, addsimp rejected the guarded (implication) forms ("not an equation") and goal_insert rejected the universally-quantified version.

If a bv_lift-style tactic doesn't exist yet and it would be useful upstream, I'm happy to prototype it against this case. It seems like the right general primitive to have.

Repro is the same file, repro_barrett_2p46.saw; the proven Integer core is escape2_core.saw in the same directory.