[Zellic Audit] 3.12 Incomplete handling of G1 point addition (BitVM#379)

Hakkush-07 · web-flow · commit a977a217ac0b · 2025-11-11T12:35:41.000+03:00
* create a version of G1Affine::hinted_check_add that the caller must use with points that are not t==q nor t==-q

* optimize G1Affine::hinted_check_add and add TODO comments for later

* rearrange wrong if checks in G1Affine::hinted_check_add

* add validity checks to hints of new G1Affine::hinted_check_add

* fix hint validity check and roll in G1Affine::hinted_check_add
diff --git a/bitvm/src/bigint/cmp.rs b/bitvm/src/bigint/cmp.rs
@@ -27,6 +27,22 @@ impl<const N_BITS: u32, const LIMB_SIZE: u32> BigIntImpl<N_BITS, LIMB_SIZE> {
         }
     }
 
+    pub fn equal_keep_elements(a: u32, b: u32) -> Script {
+        script! {
+            { Self::copy_zip(a, b) }
+            for _ in 0..Self::N_LIMBS {
+                OP_EQUAL
+                OP_TOALTSTACK
+            }
+            for _ in 0..Self::N_LIMBS {
+                OP_FROMALTSTACK
+            }
+            for _ in 0..Self::N_LIMBS - 1 {
+                OP_BOOLAND
+            }
+        }
+    }
+
     pub fn notequal(a: u32, b: u32) -> Script {
         script! {
             { Self::equal(a, b) }
diff --git a/bitvm/src/bn254/fp254impl.rs b/bitvm/src/bn254/fp254impl.rs
@@ -107,6 +107,11 @@ pub trait Fp254Impl {
         U254::equal(a, b)
     }
 
+    #[inline]
+    fn equal_keep_elements(a: u32, b: u32) -> Script {
+        U254::equal_keep_elements(a, b)
+    }
+
     #[inline]
     fn equalverify(a: u32, b: u32) -> Script {
         U254::equalverify(a, b)
diff --git a/bitvm/src/bn254/g1.rs b/bitvm/src/bn254/g1.rs
@@ -169,8 +169,13 @@ impl G1Affine {
         }
     }
 
-    pub fn hinted_check_add(t: ark_bn254::G1Affine, q: ark_bn254::G1Affine) -> (Script, Vec<Hint>) {
+    pub fn hinted_check_add_prevent_degenerate(
+        t: ark_bn254::G1Affine,
+        q: ark_bn254::G1Affine,
+    ) -> (Script, Vec<Hint>) {
         let mut hints = vec![];
+        assert_ne!(t, q);
+        assert_ne!(t, -q);
 
         let (alpha, bias) = if !t.is_zero() && !q.is_zero() {
             let alpha = (t.y - q.y) / (t.x - q.x);
@@ -226,6 +231,106 @@ impl G1Affine {
         (script, hints)
     }
 
+    pub fn hinted_check_add(t: ark_bn254::G1Affine, q: ark_bn254::G1Affine) -> (Script, Vec<Hint>) {
+        let mut hints = vec![];
+
+        let (alpha, bias) = if t.is_zero() || q.is_zero() {
+            // no hint, dummy zero
+            (ark_bn254::Fq::ZERO, ark_bn254::Fq::ZERO)
+        } else if t == -q {
+            // no hint, dummy zero
+            (ark_bn254::Fq::ZERO, ark_bn254::Fq::ZERO)
+        } else if t == q {
+            // doubling hints
+            let alpha = (t.x.square() + t.x.square() + t.x.square()) / (t.y + t.y);
+            let bias = t.y - alpha * t.x;
+            (alpha, bias)
+        } else {
+            // adding hints
+            let alpha = (t.y - q.y) / (t.x - q.x);
+            let bias = t.y - alpha * t.x;
+            (alpha, bias)
+        };
+
+        let (hinted_script1, hint1) = Self::hinted_check_chord_line(t, q, alpha);
+        let (hinted_script2, hint2) = Self::hinted_add(t.x, q.x, alpha);
+        let (hinted_script3, hint3) = Self::hinted_check_tangent_line(t, alpha);
+
+        let script = script! {           // tx ty qx qy
+            { G1Affine::is_zero_keep_element() }
+            OP_IF
+                { G1Affine::drop() }
+            OP_ELSE
+                { G1Affine::roll(2) }
+                { G1Affine::is_zero_keep_element() }
+                OP_IF
+                    { G1Affine::drop() }
+                OP_ELSE                                    // qx qy tx ty
+                    { Fq::equal_keep_elements(3, 1) }      // t == q or t == -q
+                    OP_DUP
+                    OP_TOALTSTACK
+                    OP_TOALTSTACK
+                    { Fq::equal_keep_elements(2, 0) }
+                    OP_NOT
+                    OP_FROMALTSTACK
+                    OP_BOOLAND
+                    OP_IF                                  // case: t == -q
+                        OP_FROMALTSTACK OP_DROP
+                        { G1Affine::drop() }
+                        { G1Affine::drop() }
+                        { G1Affine::identity() }
+                    OP_ELSE                                // case: t != -q
+                        for _ in 0..Fq::N_LIMBS {
+                            OP_DEPTH OP_1SUB OP_ROLL
+                        }
+                        { Fq::check_validity_and_keep_element() }
+                        for _ in 0..Fq::N_LIMBS {
+                            OP_DEPTH OP_1SUB OP_ROLL
+                        }                                  // qx qy tx ty c3 c4
+                        { Fq::check_validity_and_keep_element() }
+                        { Fq::copy(1) }                    // qx qy tx ty c3 c4 c3
+                        { Fq::copy(1) }                    // qx qy tx ty c3 c4 c3 c4
+                        { Fq::copy(5) }                    // qx qy tx ty c3 c4 c3 c4 tx
+                        { Fq::roll(5) }                    // qx qy tx c3 c4 c3 c4 tx ty
+                        OP_FROMALTSTACK
+                        OP_IF                              // case: t == q
+                            { hinted_script3 }             // qx qy tx c3 c4 is_tangent_line_correct
+                            OP_VERIFY                      // qx qy tx c3 c4
+                            { Fq::roll(3) }                // qx tx c3 c4 qy
+                            { Fq::drop() }                 // qx tx c3 c4
+                        OP_ELSE                            // case: general case
+                            { Fq::copy(8) }                // qx qy tx c3 c4 c3 c4 tx ty qx
+                            { Fq::roll(8) }                // qx tx c3 c4 c3 c4 tx ty qx qy
+                            { hinted_script1 }             // qx tx c3 c4 0/1
+                            OP_VERIFY                      // qx tx c3 c4
+                        OP_ENDIF
+                        { Fq::roll(2) }                    // qx c3 c4 tx
+                        { Fq::roll(3) }                    // c3 c4 tx qx
+                        { hinted_script2 }                 // x' y'
+                    OP_ENDIF
+                OP_ENDIF
+            OP_ENDIF
+        };
+
+        if t.is_zero() || q.is_zero() {
+            // no hint
+        } else if t == -q {
+            // no hint
+        } else if t == q {
+            hints.push(Hint::Fq(alpha));
+            hints.push(Hint::Fq(-bias));
+            hints.extend(hint3);
+            hints.extend(hint2);
+        } else {
+            hints.push(Hint::Fq(alpha));
+            hints.push(Hint::Fq(-bias));
+            hints.extend(hint1);
+            hints.extend(hint2);
+        };
+
+        (script, hints)
+    }
+
     /// add two points T and Q
     ///     x' = alpha^2 - T.x - Q.x
     ///     y' = -bias - alpha * x'
@@ -673,50 +778,68 @@ mod test {
     }
 
     #[test]
-    fn test_g1_affine_hinted_check_add() {
-        //println!("G1.hinted_add: {} bytes", G1Affine::check_add().len());
+    fn test_g1_affine_hinted_check_add_prevent_degenerate() {
         let mut prng = ChaCha20Rng::seed_from_u64(0);
         let t = ark_bn254::G1Affine::rand(&mut prng);
         let q = ark_bn254::G1Affine::rand(&mut prng);
-        let alpha = (t.y - q.y) / (t.x - q.x);
-        // -bias
-        let bias_minus = alpha * t.x - t.y;
-
-        let x = alpha.square() - t.x - q.x;
-        let y = bias_minus - alpha * x;
+        let r = (t + q).into_affine();
 
-        let (hinted_check_add, hints) = G1Affine::hinted_check_add(t, q);
+        let (hinted_check_add, hints) = G1Affine::hinted_check_add_prevent_degenerate(t, q);
 
         let script = script! {
             for hint in hints {
                 { hint.push() }
             }
-            { Fq::push(t.x) }
-            { Fq::push(t.y) }
-            { Fq::push(q.x) }
-            { Fq::push(q.y) }
+            { G1Affine::push(t) }
+            { G1Affine::push(q) }
             { hinted_check_add.clone() }
-            // [x']
-            { Fq::push(y) }
-            // [x', y', y]
-            { Fq::equalverify(1,0) }
-            // [x']
-            { Fq::push(x) }
-            // [x', x]
-            { Fq::equalverify(1,0) }
-            // []
+            { G1Affine::push(r) }
+            { G1Affine::equalverify() }
             OP_TRUE
-            // [OP_TRUE]
         };
         let exec_result = execute_script(script);
         assert!(exec_result.success);
         println!(
-            "hinted_check_add: {} @ {} stack",
+            "hinted_check_add_prevent_degenerate: {} @ {} stack",
             hinted_check_add.len(),
             exec_result.stats.max_nb_stack_items
         );
     }
 
+    #[test]
+    fn test_g1_affine_hinted_check_add() {
+        let mut prng = ChaCha20Rng::seed_from_u64(0);
+        let t = ark_bn254::G1Affine::rand(&mut prng);
+        let q = ark_bn254::G1Affine::rand(&mut prng);
+        let r = (t + q).into_affine();
+        let tt = (t + t).into_affine();
+        let negt = -t;
+        let z = ark_bn254::G1Affine::zero();
+
+        for (t, q, r) in [(t, q, r), (t, t, tt), (t, negt, z), (t, z, t)] {
+            let (hinted_check_add, hints) = G1Affine::hinted_check_add(t, q);
+
+            let script = script! {
+                for hint in hints {
+                    { hint.push() }
+                }
+                { G1Affine::push(t) }
+                { G1Affine::push(q) }
+                { hinted_check_add.clone() }
+                { G1Affine::push(r) }
+                { G1Affine::equalverify() }
+                OP_TRUE
+            };
+            let exec_result = execute_script(script);
+            assert!(exec_result.success);
+            println!(
+                "hinted_check_add: {} @ {} stack",
+                hinted_check_add.len(),
+                exec_result.stats.max_nb_stack_items
+            );
+        }
+    }
+
     #[test]
     fn test_g1_affine_hinted_check_double() {
         //println!("G1.hinted_add: {} bytes", G1Affine::check_add().len());
diff --git a/bitvm/src/bn254/msm.rs b/bitvm/src/bn254/msm.rs
@@ -230,7 +230,7 @@ fn accumulate_addition_chain_for_a_scalar_mul(
             );
 
             // accumulate value using hinted_check_add
-            let (add_scr, add_hints) = G1Affine::hinted_check_add(prev, row_g1);
+            let (add_scr, add_hints) = G1Affine::hinted_check_add_prevent_degenerate(prev, row_g1);
 
             prev = (prev + row_g1).into_affine(); // output of this chunk: t + q
             vec_row_g1_scr.push(row_g1_scr);
diff --git a/bitvm/src/chunk/taps_msm.rs b/bitvm/src/chunk/taps_msm.rs
@@ -137,7 +137,7 @@ pub(crate) fn chunk_hash_p(
     let (tx, qx, ty, qy) = (hint_in_t.x, hint_in_q.x, hint_in_t.y, hint_in_q.y);
     let t = ark_bn254::G1Affine::new_unchecked(tx, ty);
     let q = ark_bn254::G1Affine::new_unchecked(qx, qy);
-    let (add_scr, add_hints) = G1Affine::hinted_check_add(t, q);
+    let (add_scr, add_hints) = G1Affine::hinted_check_add_prevent_degenerate(t, q);
     let r = (t + q).into_affine();
     let ops_script = script! {
         // [t] [hash_r, hash_t]
