[feat] BN254 AssertFinalExponentiationIsOne

ecc/execution/Cargo.toml

@@ -8,8 +8,10 @@ edition.workspace = true
 halo2curves-axiom = { git = "https://github.com/axiom-crypto/halo2curves.git", branch = "test/visibility" }
 itertools.workspace = true
 rand_core = "0.6.4"
+num = "0.4.3"
+rand.workspace = true
 
 [dev-dependencies]
-rand.workspace = true
+lazy_static.workspace = true
 rng = "0.1.0"
 subtle = "2.6.1"

ecc/execution/src/common/field.rs

@@ -1,4 +1,5 @@
 use halo2curves_axiom::ff::Field;
+use num::BigInt;
 
 pub trait FieldExtension: Field {
     type BaseField: Field;
@@ -27,6 +28,15 @@ pub trait Fp12Constructor<Fp2: FieldExtension> {
     fn new(c00: Fp2, c01: Fp2, c02: Fp2, c10: Fp2, c11: Fp2, c12: Fp2) -> Self;
 }
 
+pub trait ExpBigInt<Fp: Field> {
+    /// Exponentiates a field element by a BigInt
+    fn exp(&self, k: BigInt) -> Fp;
+}
+
+pub trait FeltPrint<Fp: Field> {
+    fn felt_print(&self, label: &str);
+}
+
 pub fn fp12_square<Fp12: Field>(x: Fp12) -> Fp12 {
     fp12_multiply(x, x)
 }

ecc/execution/src/common/final_exp.rs

@@ -0,0 +1,20 @@
+use halo2curves_axiom::ff::Field;
+
+use super::{EcPoint, ExpBigInt, FieldExtension};
+
+#[allow(non_snake_case)]
+pub trait FinalExp<Fp, Fp2, Fp12>
+where
+    Fp: Field,
+    Fp2: FieldExtension<BaseField = Fp>,
+    Fp12: FieldExtension<BaseField = Fp2> + ExpBigInt<Fp12>,
+{
+    /// Assert in circuit that the final exponentiation is equal to one. The actual final
+    /// exponentiaton is calculated out of circuit via final_exp_hint.
+    fn assert_final_exp_is_one(&self, f: Fp12, P: &[EcPoint<Fp>], Q: &[EcPoint<Fp2>]);
+
+    /// Generates a hint for the final exponentiation to be calculated out of circuit
+    /// Input is the result of the Miller loop
+    /// Output is c (residue witness inverse) and u (cubic nonresidue power)
+    fn final_exp_hint(&self, f: Fp12) -> (Fp12, Fp12);
+}

ecc/execution/src/common/miller_loop.rs

@@ -13,10 +13,19 @@ where
     Fp2: FieldExtension<BaseField = Fp>,
     Fp12: FieldExtension<BaseField = Fp2>,
 {
+    /// Xi value for the curve
     fn xi() -> Fp2;
+
+    /// Seed value for the curve
     fn seed() -> u64;
+
+    /// Pseudo-binary used for the loop counter of the curve
     fn pseudo_binary_encoding() -> [i8; BITS];
+
+    /// Function to evaluate the line functions of the Miller loop
     fn evaluate_lines_vec(&self, f: Fp12, lines: Vec<EvaluatedLine<Fp, Fp2>>) -> Fp12;
+
+    /// Runs before the main loop in the Miller loop function
     fn pre_loop(
         &self,
         f: Fp12,
@@ -25,6 +34,8 @@ where
         x_over_ys: Vec<Fp>,
         y_invs: Vec<Fp>,
     ) -> (Fp12, Vec<EcPoint<Fp2>>);
+
+    /// Runs after the main loop in the Miller loop function
     fn post_loop(
         &self,
         f: Fp12,
@@ -34,11 +45,14 @@ where
         y_invs: Vec<Fp>,
     ) -> (Fp12, Vec<EcPoint<Fp2>>);
 
+    /// Runs the multi-Miller loop with no embedded exponent
     #[allow(non_snake_case)]
     fn multi_miller_loop(&self, P: &[EcPoint<Fp>], Q: &[EcPoint<Fp2>]) -> Fp12 {
         self.multi_miller_loop_embedded_exp(P, Q, None)
     }
 
+    /// Runs the multi-Miller loop with an embedded exponent, removing the need to calculate the residue witness
+    /// in the final exponentiation step
     #[allow(non_snake_case)]
     fn multi_miller_loop_embedded_exp(
         &self,
@@ -70,11 +84,6 @@ where
 
         let pseudo_binary_encoding = Self::pseudo_binary_encoding();
         for i in (0..pseudo_binary_encoding.len() - 2).rev() {
-            println!(
-                "miller i: {} = {}; Q_acc.x: {:?}",
-                i, pseudo_binary_encoding[i], Q_acc[0].x
-            );
-
             f = fp12_square::<Fp12>(f);
 
             let mut lines = Vec::<EvaluatedLine<Fp, Fp2>>::new();

ecc/execution/src/common/mod.rs

@@ -1,11 +1,17 @@
 mod field;
+mod final_exp;
 mod line;
 mod miller_loop;
 mod miller_step;
+mod pairing;
 mod point;
+mod utils;
 
 pub use field::*;
+pub use final_exp::*;
 pub use line::*;
 pub use miller_loop::*;
 pub use miller_step::*;
+pub use pairing::*;
 pub use point::*;
+pub use utils::*;

ecc/execution/src/common/pairing.rs

@@ -0,0 +1,12 @@
+use halo2curves_axiom::ff::Field;
+
+use super::FieldExtension;
+
+#[allow(non_snake_case)]
+pub trait PairingCheck<Fp, Fp2>
+where
+    Fp: Field,
+    Fp2: FieldExtension<BaseField = Fp>,
+{
+    fn pairing_check(&self, P: Fp, Q: Fp2);
+}