[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
+lazy_static.workspace = true
 
 [dev-dependencies]
-rand.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;
@@ -20,13 +21,25 @@ pub trait FieldExtension: Field {
 }
 
 pub trait Fp2Constructor<Fp: Field> {
+    /// Constructs a new Fp2 element from 2 Fp coefficients.
     fn new(c0: Fp, c1: Fp) -> Self;
 }
 
 pub trait Fp12Constructor<Fp2: FieldExtension> {
+    /// Constructs a new Fp12 element from 6 Fp2 coefficients.
     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_bigint(&self, k: BigInt) -> Fp;
+}
+
+#[cfg(test)]
+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,21 @@
+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. Scalar coefficients
+    /// to the curve points must equal to zero, which is checked in a debug_assert.
+    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);
+}