Fix/disprove script exceeds 4 m with constraints (BitVM#297)

* feat: add tmul for fp2 with 4 window stack len

* feat: add fp2_w4 in ss_mul to reduce script size

* feat: add w4 version of lc4_keep_elements

* chore: specify vec capactiy

* doc: add docs to new functions

Author: manishbista28

bitvm/src/bn254/fp254impl.rs

@@ -686,6 +686,49 @@ pub trait Fp254Impl {
         (script, hints)
     }
 
+    // Assumes tmul hint (1 BigInteger) at the top of stack
+    // and operands (a, b, c, d) at stack depths (a_depth, b_depth, c_depth, d_depth)
+    // Computes r = a * c + b * d (mod p)
+    #[allow(clippy::too_many_arguments)]
+    fn hinted_mul_lc2_w4(
+        a_depth: u32,
+        a: ark_bn254::Fq,
+        b_depth: u32,
+        b: ark_bn254::Fq,
+        c_depth: u32,
+        c: ark_bn254::Fq,
+        d_depth: u32,
+        d: ark_bn254::Fq,
+    ) -> (Script, Vec<Hint>) {
+        assert!(a_depth > b_depth && b_depth > c_depth && c_depth > d_depth);
+
+        let mut hints = Vec::with_capacity(1);
+
+        let modulus = &Fq::modulus_as_bigint();
+
+        let x = BigInt::from_str(&a.to_string()).unwrap();
+        let y = BigInt::from_str(&b.to_string()).unwrap();
+        let z = BigInt::from_str(&c.to_string()).unwrap();
+        let w = BigInt::from_str(&d.to_string()).unwrap();
+
+        let q = (x * z + y * w) / modulus;
+
+        let script = script! {
+            for _ in 0..Self::N_LIMBS {
+                OP_DEPTH OP_1SUB OP_ROLL // hints
+            }
+            // { Fq::push(ark_bn254::Fq::from_str(&q.to_string()).unwrap()) }
+            { Fq::roll(a_depth + 1) }
+            { Fq::roll(b_depth + 2) }
+            { Fq::roll(c_depth + 3) }
+            { Fq::roll(d_depth + 4) }
+            { Fq::tmul_lc2_w4() }
+        };
+        hints.push(Hint::BigIntegerTmulLC2(q));
+
+        (script, hints)
+    }
+
     #[allow(clippy::too_many_arguments)]
     fn hinted_mul_lc4(
         a_depth: u32,
@@ -792,6 +835,47 @@ pub trait Fp254Impl {
         (script, hints)
     }
 
+    // Same as hinted_mul_lc2_keep_elements(), except retains operands (a, b, c, d) on stack
+    #[allow(clippy::too_many_arguments)]
+    fn hinted_mul_lc2_keep_elements_w4(
+        a_depth: u32,
+        a: ark_bn254::Fq,
+        b_depth: u32,
+        b: ark_bn254::Fq,
+        c_depth: u32,
+        c: ark_bn254::Fq,
+        d_depth: u32,
+        d: ark_bn254::Fq,
+    ) -> (Script, Vec<Hint>) {
+        assert!(a_depth > b_depth && b_depth > c_depth && c_depth > d_depth);
+
+        let mut hints = Vec::with_capacity(1);
+
+        let modulus = &Fq::modulus_as_bigint();
+
+        let x = BigInt::from_str(&a.to_string()).unwrap();
+        let y = BigInt::from_str(&b.to_string()).unwrap();
+        let z = BigInt::from_str(&c.to_string()).unwrap();
+        let w = BigInt::from_str(&d.to_string()).unwrap();
+
+        let q = (x * z + y * w) / modulus;
+
+        let script = script! {
+            for _ in 0..Self::N_LIMBS {
+                OP_DEPTH OP_1SUB OP_ROLL // hints
+            }
+            // { Fq::push(ark_bn254::Fq::from_str(&q.to_string()).unwrap()) }
+            { Fq::copy(a_depth + 1) }
+            { Fq::copy(b_depth + 2) }
+            { Fq::copy(c_depth + 3) }
+            { Fq::copy(d_depth + 4) }
+            { Fq::tmul_lc2_w4() }
+        };
+        hints.push(Hint::BigIntegerTmulLC2(q));
+
+        (script, hints)
+    }
+
     // TODO: Optimize using the sqaure feature
     fn hinted_square(a: ark_bn254::Fq) -> (Script, Vec<Hint>) {
         let mut hints = Vec::new();

bitvm/src/bn254/fq.rs

@@ -47,6 +47,16 @@ impl Fq {
         }
     }
 
+    // Wrapper over 4-bit windowed tmul that computes a linear combination of two terms
+    // Computes r = a * c + b * d (mod p)
+    // Input Stack: [hint, a, b, c, d]
+    // Output Stack: [r]
+    pub fn tmul_lc2_w4() -> Script {
+        script! {
+            { <Fq as Fp254Mul2LCW4>::tmul() }
+        }
+    }
+
     pub fn tmul_lc4() -> Script {
         script! {
             { <Fq as Fp254Mul4LC>::tmul() }
@@ -408,6 +418,7 @@ macro_rules! fp_lc_mul {
 
 fp_lc_mul!(Mul, 4, 4, [true]);
 fp_lc_mul!(Mul2LC, 3, 3, [true, true]);
+fp_lc_mul!(Mul2LCW4, 4, 4, [true, true]);
 fp_lc_mul!(Mul4LC, 3, 3, [true, true, true, true]);
 
 #[cfg(test)]

bitvm/src/bn254/fq2.rs

@@ -192,6 +192,46 @@ impl Fq2 {
         (script, hints)
     }
 
+    // Given Fq2 elements a and b, compute their product
+    // A = a0 + a1 u, B = b0 + b1 u, where $u^2$ is quadratic non-residue, for bn-254 $u^2$ = -1
+    // A.B = (a0.b0 + a1.b1 $u^2$) + u (a0.b1 + a1b0) = (a0.b0 - a1.b1) + u (a0.b1 + a1.b0)
+    // This specific version uses tmul of 4-bit window to compute each of the two terms above.
+    pub fn hinted_mul_w4(
+        mut a_depth: u32,
+        mut a: ark_bn254::Fq2,
+        mut b_depth: u32,
+        mut b: ark_bn254::Fq2,
+    ) -> (Script, Vec<Hint>) {
+        if a_depth < b_depth {
+            (a_depth, b_depth) = (b_depth, a_depth);
+            (a, b) = (b, a);
+        }
+        assert_ne!(a_depth, b_depth);
+
+        let mut hints = Vec::with_capacity(2);
+
+        let (hinted_script1, hint1) =
+            Fq::hinted_mul_lc2_keep_elements_w4(3, a.c0, 2, a.c1, 1, b.c1, 0, b.c0);
+        let (hinted_script2, hint2) = Fq::hinted_mul_lc2_w4(3, a.c0, 2, a.c1, 1, b.c0, 0, -b.c1);
+
+        let script = script! {
+            { Fq2::roll(a_depth) }
+            { Fq2::roll(b_depth + 2) }                       // a.c0 a.c1 b.c0 b.c1
+            { Fq::roll(1) }                                  // a.c0 a.c1 b.c1 b.c0
+            { hinted_script1 }                               // a.c0 a.c1 b.c1 b.c0 a.c0*b.c1+a.c1*b.c0
+            { Fq::toaltstack() }                             // a.c0 a.c1 b.c1 b.c0 | a.c0*b.c1+a.c1*b.c0
+            { Fq::roll(1) }                                  // a.c0 a.c1 b.c0 b.c1 | a.c0*b.c1+a.c1*b.c0
+            { Fq::neg(0) }                                   // a.c0 a.c1 b.c0 -b.c1 | a.c0*b.c1+a.c1*b.c0
+            { hinted_script2 }                               // a.c0*b.c0-a.c1*b.c1 | a.c0*b.c1+a.c1*b.c0
+            { Fq::fromaltstack() }                           // a.c0*b.c0-a.c1*b.c1 a.c0*b.c1+a.c1*b.c0
+        };
+
+        hints.extend(hint1);
+        hints.extend(hint2);
+
+        (script, hints)
+    }
+
     pub fn hinted_mul_by_constant(
         a: ark_bn254::Fq2,
         constant: &ark_bn254::Fq2,
@@ -496,6 +536,33 @@ mod test {
         }
     }
 
+    #[test]
+    fn test_bn254_fq2_hinted_mul_w4() {
+        let mut prng: ChaCha20Rng = ChaCha20Rng::seed_from_u64(0);
+
+        for _ in 0..100 {
+            let a = ark_bn254::Fq2::rand(&mut prng);
+            let b = ark_bn254::Fq2::rand(&mut prng);
+            let c = a.mul(&b);
+
+            let (hinted_mul, hints) = Fq2::hinted_mul_w4(2, a, 0, b);
+            println!("Fq2::hinted_mul_w4: {} bytes", hinted_mul.len());
+
+            let script = script! {
+                for hint in hints {
+                    { hint.push() }
+                }
+                { Fq2::push(a) }
+                { Fq2::push(b) }
+                { hinted_mul.clone() }
+                { Fq2::push(c) }
+                { Fq2::equalverify() }
+                OP_TRUE
+            };
+            run(script);
+        }
+    }
+
     #[test]
     fn test_bn254_fq2_hinted_mul_by_constant() {
         let mut prng: ChaCha20Rng = ChaCha20Rng::seed_from_u64(0);

bitvm/src/bn254/g2.rs

@@ -472,7 +472,7 @@ pub fn hinted_affine_add_line(
 ) -> (Script, Vec<Hint>) {
     let mut hints = Vec::new();
     let (hinted_script0, hint0) = Fq2::hinted_square(c3);
-    let (hinted_script1, hint1) = Fq2::hinted_mul(4, c3, 0, c3.square() - tx - qx);
+    let (hinted_script1, hint1) = Fq2::hinted_mul_w4(4, c3, 0, c3.square() - tx - qx);
 
     let script = script! {
         // [c3, c4, T.x, Q.x]

bitvm/src/chunk/api.rs

@@ -1302,6 +1302,7 @@ mod test {
         }
 
         let _total = NUM_PUBS + NUM_U256 + NUM_HASH;
+        const RESERVED_SPACE: usize = 16000; // blockreservedweight=8000 + extra (8000)
         for i in 0.._total {
             println!("ITERATION {:?}", i);
             let mut proof_asserts = read_asserts_from_file("bridge_data/chunker_data/assert.json");
@@ -1317,6 +1318,7 @@ mod test {
                 let scr = hint_script
                     .clone()
                     .push_script(verifier_scripts[index].clone());
+                assert!(scr.len() < 4_000_000 - RESERVED_SPACE);
                 let res = execute_script(scr);
                 for i in 0..res.final_stack.len() {
                     println!("{i:} {:?}", res.final_stack.get(i));

bitvm/src/chunk/taps_mul.rs

@@ -27,10 +27,10 @@ pub(crate) fn utils_fq6_ss_mul(
     let i = b * e;
     let result = ark_bn254::Fq6::new(g, h, i);
 
-    let (g_scr, g_hints) = Fq2::hinted_mul(2, d, 0, a);
+    let (g_scr, g_hints) = Fq2::hinted_mul_w4(2, d, 0, a);
     // We use lc4 to compute h as it requires lesser number of tmul hints compared to doing the same thing with two LC2s
     let (h_scr, h_hints) = Fq2::hinted_mul_lc4_keep_elements(b, d, e, a);
-    let (i_scr, i_hints) = Fq2::hinted_mul(2, e, 0, b);
+    let (i_scr, i_hints) = Fq2::hinted_mul_w4(2, e, 0, b);
 
     let mut hints = vec![];
     for hint in [i_hints, g_hints, h_hints] {