BN254 multi-precision support for WASM backend

[VanshSahay]

The WASM backend (PR #415) supports single-word field arithmetic for primes < 2^63. BN254 (254-bit prime) needs 4-word arithmetic.

What's already in place

• compileModule accepts numWords parameter (default 1)
• snarkjs ABI handles n32 = numWords * 2 and signalBytes = n32 * 4
• fieldHelpers has a multi-word path (currently stubbed)

Work needed

1. Multi-word field arithmetic in WAT for 4-word elements

• fadd_4: word-by-word add with carry + conditional sub of prime
• fsub_4: word-by-word sub with borrow + conditional add of prime
• fmul_4: double-and-add (requires only fadd, about 254 iterations per mul)
• finv_4: Fermat little theorem via fpow_4

2. Expression compilers parameterized by numWords

Each FExpr operation pushes/pops numWords i64 values instead of 1. NExpr and BExpr unchanged.

3. Witness function signature

For numWords > 1, the direct witness function takes numWords * numInputs params and returns numWords * tw results.

Approach

Write the multi-word arithmetic as a standalone .wat file, test with wat2wasm + Node.js against known BN254 test vectors, then integrate into the Lean WAT generator in Compile.lean.

[VanshSahay]

Quick update from the WASM/R1CS work in #415

the WASM backend only does single-word i64 arithmetic, but BN254 needs 4-word (256-bit). The witness generator has to compute (a * b) mod p correctly for 254-bit numbers inside a WASM module, which has no big-int primitives, you have to implement schoolbook multiplication and Barrett reduction by hand in WAT.

I wrote a Lean generator that emits multi-word WAT for any prime. For BN254 it produces $fmul (4×4 schoolbook multiply + Barrett reduction), $fadd, $fsub. 3×5=15, p×1=0, and critically 2^128² = 2^256 mod p passes. The compilers push/pop 4 values per field element instead of 1. The full SHA256 compression function (81K signals, 80K constraints) compiles and loads in snarkjs. Single-word circuits still work unchanged

two things are left
(1) finv for multi-word : currently stubbed. Fermat exponentiation would be ~300K WAT instructions; extended Euclidean seems like the right approach but I haven't written the generator yet
(2) The BN254 Fact (Nat.Prime …) instance uses sorry because native_decide takes 8+ minutes for a 254-bit number, which means you can't #eval a circuit targeting BN254 from Lean. The generated WAT is verified correct, but the Lean-side compilation path is blocked on the primality proof.

Currently stuck on figuring out a fast way to prove a 254-bit number is prime in Lean, or ideas for the finv WAT generator, would appreciate pointers

[mitschabaude]

finv for multi-word : currently stubbed. Fermat exponentiation would be ~300K WAT instructions;

no it shouldn't, and if it does, we're doing something wrong in our approach to write wasm. wasm supports function calls. fermat exponentiation is on the order of 250 double-and-add steps, which is on the order of 500 WAT instructions if you call your mul/square routines.

[mitschabaude]

The BN254 Fact (Nat.Prime …) instance uses sorry because native_decide takes 8+ minutes for a 254-bit number, which means you can't #eval a circuit targeting BN254 from Lean. The generated WAT is verified correct, but the Lean-side compilation path is blocked on the primality proof.

after switching to Lean 4.30 we will be able to import CompPoly, which has proper proofs for primality for large primes.

until then just use #eval!