Feat : MSM black box implementation

provekit/common/src/witness/scheduling/dependency.rs

@@ -78,7 +78,9 @@ impl DependencyInfo {
             WitnessBuilder::Sum(_, ops) => ops.iter().map(|SumTerm(_, idx)| *idx).collect(),
             WitnessBuilder::Product(_, a, b) => vec![*a, *b],
             WitnessBuilder::MultiplicitiesForRange(_, _, values) => values.clone(),
-            WitnessBuilder::Inverse(_, x) => vec![*x],
+            WitnessBuilder::Inverse(_, x)
+            | WitnessBuilder::ModularInverse(_, x, _)
+            | WitnessBuilder::IntegerQuotient(_, x, _) => vec![*x],
             WitnessBuilder::IndexedLogUpDenominator(
                 _,
                 sz,
@@ -152,6 +154,28 @@ impl DependencyInfo {
                 }
                 v
             }
+            WitnessBuilder::MulModHint {
+                a_lo,
+                a_hi,
+                b_lo,
+                b_hi,
+                ..
+            } => vec![*a_lo, *a_hi, *b_lo, *b_hi],
+            WitnessBuilder::WideModularInverse { a_lo, a_hi, .. } => vec![*a_lo, *a_hi],
+            WitnessBuilder::WideAddQuotient {
+                a_lo,
+                a_hi,
+                b_lo,
+                b_hi,
+                ..
+            } => vec![*a_lo, *a_hi, *b_lo, *b_hi],
+            WitnessBuilder::WideSubBorrow {
+                a_lo,
+                a_hi,
+                b_lo,
+                b_hi,
+                ..
+            } => vec![*a_lo, *a_hi, *b_lo, *b_hi],
             WitnessBuilder::BytePartition { x, .. } => vec![*x],
 
             WitnessBuilder::U32AdditionMulti(_, _, inputs) => inputs
@@ -240,6 +264,8 @@ impl DependencyInfo {
             | WitnessBuilder::Challenge(idx)
             | WitnessBuilder::IndexedLogUpDenominator(idx, ..)
             | WitnessBuilder::Inverse(idx, _)
+            | WitnessBuilder::ModularInverse(idx, ..)
+            | WitnessBuilder::IntegerQuotient(idx, ..)
             | WitnessBuilder::ProductLinearOperation(idx, ..)
             | WitnessBuilder::LogUpDenominator(idx, ..)
             | WitnessBuilder::LogUpInverse(idx, ..)
@@ -282,6 +308,14 @@ impl DependencyInfo {
                 let n = 1usize << *num_bits;
                 (*start..*start + n).collect()
             }
+            WitnessBuilder::MulModHint { output_start, .. } => {
+                (*output_start..*output_start + 20).collect()
+            }
+            WitnessBuilder::WideModularInverse { output_start, .. } => {
+                (*output_start..*output_start + 2).collect()
+            }
+            WitnessBuilder::WideAddQuotient { output, .. } => vec![*output],
+            WitnessBuilder::WideSubBorrow { output, .. } => vec![*output],
             WitnessBuilder::U32Addition(result_idx, carry_idx, ..) => {
                 vec![*result_idx, *carry_idx]
             }

provekit/common/src/witness/scheduling/remapper.rs

@@ -115,6 +115,12 @@ impl WitnessIndexRemapper {
             WitnessBuilder::Inverse(idx, operand) => {
                 WitnessBuilder::Inverse(self.remap(*idx), self.remap(*operand))
             }
+            WitnessBuilder::ModularInverse(idx, operand, modulus) => {
+                WitnessBuilder::ModularInverse(self.remap(*idx), self.remap(*operand), *modulus)
+            }
+            WitnessBuilder::IntegerQuotient(idx, dividend, divisor) => {
+                WitnessBuilder::IntegerQuotient(self.remap(*idx), self.remap(*dividend), *divisor)
+            }
             WitnessBuilder::ProductLinearOperation(
                 idx,
                 ProductLinearTerm(x, a, b),
@@ -215,6 +221,60 @@ impl WitnessIndexRemapper {
                         .collect(),
                 )
             }
+            WitnessBuilder::MulModHint {
+                output_start,
+                a_lo,
+                a_hi,
+                b_lo,
+                b_hi,
+                modulus,
+            } => WitnessBuilder::MulModHint {
+                output_start: self.remap(*output_start),
+                a_lo:         self.remap(*a_lo),
+                a_hi:         self.remap(*a_hi),
+                b_lo:         self.remap(*b_lo),
+                b_hi:         self.remap(*b_hi),
+                modulus:      *modulus,
+            },
+            WitnessBuilder::WideModularInverse {
+                output_start,
+                a_lo,
+                a_hi,
+                modulus,
+            } => WitnessBuilder::WideModularInverse {
+                output_start: self.remap(*output_start),
+                a_lo:         self.remap(*a_lo),
+                a_hi:         self.remap(*a_hi),
+                modulus:      *modulus,
+            },
+            WitnessBuilder::WideAddQuotient {
+                output,
+                a_lo,
+                a_hi,
+                b_lo,
+                b_hi,
+                modulus,
+            } => WitnessBuilder::WideAddQuotient {
+                output:  self.remap(*output),
+                a_lo:    self.remap(*a_lo),
+                a_hi:    self.remap(*a_hi),
+                b_lo:    self.remap(*b_lo),
+                b_hi:    self.remap(*b_hi),
+                modulus: *modulus,
+            },
+            WitnessBuilder::WideSubBorrow {
+                output,
+                a_lo,
+                a_hi,
+                b_lo,
+                b_hi,
+            } => WitnessBuilder::WideSubBorrow {
+                output: self.remap(*output),
+                a_lo:   self.remap(*a_lo),
+                a_hi:   self.remap(*a_hi),
+                b_lo:   self.remap(*b_lo),
+                b_hi:   self.remap(*b_hi),
+            },
             WitnessBuilder::BytePartition { lo, hi, x, k } => WitnessBuilder::BytePartition {
                 lo: self.remap(*lo),
                 hi: self.remap(*hi),

provekit/common/src/witness/witness_builder.rs

@@ -88,6 +88,18 @@ pub enum WitnessBuilder {
     /// The inverse of the value at a specified witness index
     /// (witness index, operand witness index)
     Inverse(usize, usize),
+    /// The modular inverse of the value at a specified witness index, modulo
+    /// a given prime modulus. Computes a^{-1} mod m using Fermat's little
+    /// theorem (a^{m-2} mod m). Unlike Inverse (BN254 field inverse), this
+    /// operates as integer modular arithmetic.
+    /// (witness index, operand witness index, modulus)
+    ModularInverse(usize, usize, #[serde(with = "serde_ark")] FieldElement),
+    /// The integer quotient floor(dividend / divisor). Used by reduce_mod to
+    /// compute k = floor(v / m) so that v = k*m + result with 0 <= result < m.
+    /// Unlike field multiplication by the inverse, this performs true integer
+    /// division on the BigInteger representation.
+    /// (witness index, dividend witness index, divisor constant)
+    IntegerQuotient(usize, usize, #[serde(with = "serde_ark")] FieldElement),
     /// Products with linear operations on the witness indices.
     /// Fields are ProductLinearOperation(witness_idx, (index, a, b), (index, c,
     /// d)) such that we wish to compute (ax + b) * (cx + d).
@@ -189,6 +201,63 @@ pub enum WitnessBuilder {
     /// Inverse of combined lookup table entry denominator (constant operands).
     /// Computes: 1 / (sz - lhs - rs*rhs - rs²*and_out - rs³*xor_out)
     CombinedTableEntryInverse(CombinedTableEntryInverseData),
+    /// Prover hint for multi-limb modular multiplication: (a * b) mod p.
+    /// Given inputs a = (a_lo, a_hi) and b = (b_lo, b_hi) as 128-bit limbs,
+    /// and a constant 256-bit modulus p, computes quotient q, remainder r,
+    /// their 86-bit decompositions, and carry witnesses.
+    ///
+    /// Outputs 20 witnesses starting at output_start:
+    ///   [0..2)   q_lo, q_hi (quotient in 128-bit limbs)
+    ///   [2..4)   r_lo, r_hi (remainder in 128-bit limbs)
+    ///   [4..7)   a_86_0, a_86_1, a_86_2 (a in 86-bit limbs)
+    ///   [7..10)  b_86_0, b_86_1, b_86_2 (b in 86-bit limbs)
+    ///   [10..13) q_86_0, q_86_1, q_86_2 (q in 86-bit limbs)
+    ///   [13..16) r_86_0, r_86_1, r_86_2 (r in 86-bit limbs)
+    ///   [16..20) c0, c1, c2, c3 (carry witnesses, unsigned-offset)
+    MulModHint {
+        output_start: usize,
+        a_lo:         usize,
+        a_hi:         usize,
+        b_lo:         usize,
+        b_hi:         usize,
+        modulus:      [u64; 4],
+    },
+    /// Prover hint for wide modular inverse: a^{-1} mod p.
+    /// Given input a = (a_lo, a_hi) as 128-bit limbs and constant modulus p,
+    /// computes the inverse via Fermat's little theorem (a^{p-2} mod p).
+    ///
+    /// Outputs 2 witnesses at output_start: inv_lo, inv_hi (128-bit limbs).
+    WideModularInverse {
+        output_start: usize,
+        a_lo:         usize,
+        a_hi:         usize,
+        modulus:      [u64; 4],
+    },
+    /// Prover hint for wide addition quotient: q = floor((a + b) / p).
+    /// Given inputs a = (a_lo, a_hi) and b = (b_lo, b_hi) as 128-bit limbs,
+    /// and a constant 256-bit modulus p, computes q ∈ {0, 1}.
+    ///
+    /// Outputs 1 witness at output: q.
+    WideAddQuotient {
+        output:  usize,
+        a_lo:    usize,
+        a_hi:    usize,
+        b_lo:    usize,
+        b_hi:    usize,
+        modulus: [u64; 4],
+    },
+    /// Prover hint for wide subtraction borrow: q = (a < b) ? 1 : 0.
+    /// Given inputs a = (a_lo, a_hi) and b = (b_lo, b_hi) as 128-bit limbs,
+    /// computes q ∈ {0, 1} indicating whether a borrow (adding p) is needed.
+    ///
+    /// Outputs 1 witness at output: q.
+    WideSubBorrow {
+        output: usize,
+        a_lo:   usize,
+        a_hi:   usize,
+        b_lo:   usize,
+        b_hi:   usize,
+    },
     /// Decomposes a packed value into chunks of specified bit-widths.
     /// Given packed value and chunk_bits = [b0, b1, ..., bn]:
     ///   packed = c0 + c1 * 2^b0 + c2 * 2^(b0+b1) + ...
@@ -260,6 +329,8 @@ impl WitnessBuilder {
             WitnessBuilder::ChunkDecompose { chunk_bits, .. } => chunk_bits.len(),
             WitnessBuilder::SpreadBitExtract { chunk_bits, .. } => chunk_bits.len(),
             WitnessBuilder::MultiplicitiesForSpread(_, num_bits, _) => 1usize << *num_bits,
+            WitnessBuilder::MulModHint { .. } => 20,
+            WitnessBuilder::WideModularInverse { .. } => 2,
 
             _ => 1,
         }