halo2_ecc/fields/
fp12.rs

Help
1use std::marker::PhantomData;
2
3use crate::ff::PrimeField as _;
4use crate::impl_field_ext_chip_common;
5
6use super::{
7    vector::{FieldVector, FieldVectorChip},
8    FieldChip, FieldExtConstructor, PrimeFieldChip,
9};
10
11use halo2_base::{
12    utils::{modulus, BigPrimeField},
13    AssignedValue, Context,
14};
15use num_bigint::BigUint;
16
17/// Represent Fp12 point as FqPoint with degree = 12
18/// `Fp12 = Fp2[w] / (w^6 - u - xi)`
19/// This implementation assumes p = 3 (mod 4) in order for the polynomial u^2 + 1 to
20/// be irreducible over Fp; i.e., in order for -1 to not be a square (quadratic residue) in Fp
21/// This means we store an Fp12 point as `\sum_{i = 0}^6 (a_{i0} + a_{i1} * u) * w^i`
22/// This is encoded in an FqPoint of degree 12 as `(a_{00}, ..., a_{50}, a_{01}, ..., a_{51})`
23#[derive(Clone, Copy, Debug)]
24pub struct Fp12Chip<'a, F: BigPrimeField, FpChip: FieldChip<F>, Fp12, const XI_0: i64>(
25    pub FieldVectorChip<'a, F, FpChip>,
26    PhantomData<Fp12>,
27);
28
29impl<'a, F, FpChip, Fp12, const XI_0: i64> Fp12Chip<'a, F, FpChip, Fp12, XI_0>
30where
31    F: BigPrimeField,
32    FpChip: PrimeFieldChip<F>,
33    FpChip::FieldType: BigPrimeField,
34    Fp12: crate::ff::Field,
35{
36    /// User must construct an `FpChip` first using a config. This is intended so everything shares a single `FlexGateChip`, which is needed for the column allocation to work.
37    pub fn new(fp_chip: &'a FpChip) -> Self {
38        assert_eq!(
39            modulus::<FpChip::FieldType>() % 4usize,
40            BigUint::from(3u64),
41            "p must be 3 (mod 4) for the polynomial u^2 + 1 to be irreducible"
42        );
43        Self(FieldVectorChip::new(fp_chip), PhantomData)
44    }
45
46    pub fn fp_chip(&self) -> &FpChip {
47        self.0.fp_chip
48    }
49
50    pub fn fp2_mul_no_carry(
51        &self,
52        ctx: &mut Context<F>,
53        fp12_pt: FieldVector<FpChip::UnsafeFieldPoint>,
54        fp2_pt: FieldVector<FpChip::UnsafeFieldPoint>,
55    ) -> FieldVector<FpChip::UnsafeFieldPoint> {
56        let fp12_pt = fp12_pt.0;
57        let fp2_pt = fp2_pt.0;
58        assert_eq!(fp12_pt.len(), 12);
59        assert_eq!(fp2_pt.len(), 2);
60
61        let fp_chip = self.fp_chip();
62        let mut out_coeffs = Vec::with_capacity(12);
63        for i in 0..6 {
64            let coeff1 = fp_chip.mul_no_carry(ctx, fp12_pt[i].clone(), fp2_pt[0].clone());
65            let coeff2 = fp_chip.mul_no_carry(ctx, fp12_pt[i + 6].clone(), fp2_pt[1].clone());
66            let coeff = fp_chip.sub_no_carry(ctx, coeff1, coeff2);
67            out_coeffs.push(coeff);
68        }
69        for i in 0..6 {
70            let coeff1 = fp_chip.mul_no_carry(ctx, fp12_pt[i + 6].clone(), fp2_pt[0].clone());
71            let coeff2 = fp_chip.mul_no_carry(ctx, fp12_pt[i].clone(), fp2_pt[1].clone());
72            let coeff = fp_chip.add_no_carry(ctx, coeff1, coeff2);
73            out_coeffs.push(coeff);
74        }
75        FieldVector(out_coeffs)
76    }
77
78    // for \sum_i (a_i + b_i u) w^i, returns \sum_i (-1)^i (a_i + b_i u) w^i
79    pub fn conjugate(
80        &self,
81        ctx: &mut Context<F>,
82        a: FieldVector<FpChip::FieldPoint>,
83    ) -> FieldVector<FpChip::FieldPoint> {
84        let a = a.0;
85        assert_eq!(a.len(), 12);
86
87        let coeffs = a
88            .into_iter()
89            .enumerate()
90            .map(|(i, c)| if i % 2 == 0 { c } else { self.fp_chip().negate(ctx, c) })
91            .collect();
92        FieldVector(coeffs)
93    }
94}
95
96/// multiply Fp2 elts: (a0 + a1 * u) * (XI0 + u) without carry
97///
98/// # Assumptions
99/// * `a` is `Fp2` point represented as `FieldVector` with degree = 2
100pub fn mul_no_carry_w6<F: BigPrimeField, FC: FieldChip<F>, const XI_0: i64>(
101    fp_chip: &FC,
102    ctx: &mut Context<F>,
103    a: FieldVector<FC::UnsafeFieldPoint>,
104) -> FieldVector<FC::UnsafeFieldPoint> {
105    let [a0, a1]: [_; 2] = a.0.try_into().unwrap();
106    // (a0 + a1 u) * (XI_0 + u) = (a0 * XI_0 - a1) + (a1 * XI_0 + a0) u     with u^2 = -1
107    // This should fit in the overflow representation if limb_bits is large enough
108    let a0_xi0 = fp_chip.scalar_mul_no_carry(ctx, a0.clone(), XI_0);
109    let out0_0_nocarry = fp_chip.sub_no_carry(ctx, a0_xi0, a1.clone());
110    let out0_1_nocarry = fp_chip.scalar_mul_and_add_no_carry(ctx, a1, a0, XI_0);
111    FieldVector(vec![out0_0_nocarry, out0_1_nocarry])
112}
113
114// a lot of this is common to any field extension (lots of for loops), but due to the way rust traits work, it is hard to create a common generic trait that does this. The main problem is that if you had a `FieldExtCommon` trait and wanted to implement `FieldChip` for anything with `FieldExtCommon`, rust will stop you because someone could implement `FieldExtCommon` and `FieldChip` for the same type, causing a conflict.
115// partially solved using macro
116
117impl<F, FpChip, Fp12, const XI_0: i64> FieldChip<F> for Fp12Chip<'_, F, FpChip, Fp12, XI_0>
118where
119    F: BigPrimeField,
120    FpChip: PrimeFieldChip<F>,
121    FpChip::FieldType: BigPrimeField,
122    Fp12: crate::ff::Field + FieldExtConstructor<FpChip::FieldType, 12>,
123    FieldVector<FpChip::UnsafeFieldPoint>: From<FieldVector<FpChip::FieldPoint>>,
124    FieldVector<FpChip::FieldPoint>: From<FieldVector<FpChip::ReducedFieldPoint>>,
125{
126    const PRIME_FIELD_NUM_BITS: u32 = FpChip::FieldType::NUM_BITS;
127    type UnsafeFieldPoint = FieldVector<FpChip::UnsafeFieldPoint>;
128    type FieldPoint = FieldVector<FpChip::FieldPoint>;
129    type ReducedFieldPoint = FieldVector<FpChip::ReducedFieldPoint>;
130    type FieldType = Fp12;
131    type RangeChip = FpChip::RangeChip;
132
133    fn get_assigned_value(&self, x: &Self::UnsafeFieldPoint) -> Fp12 {
134        assert_eq!(x.0.len(), 12);
135        let values = x.0.iter().map(|v| self.fp_chip().get_assigned_value(v)).collect::<Vec<_>>();
136        Fp12::new(values.try_into().unwrap())
137    }
138
139    // w^6 = u + xi for xi = 9
140    fn mul_no_carry(
141        &self,
142        ctx: &mut Context<F>,
143        a: impl Into<Self::UnsafeFieldPoint>,
144        b: impl Into<Self::UnsafeFieldPoint>,
145    ) -> Self::UnsafeFieldPoint {
146        let a = a.into().0;
147        let b = b.into().0;
148        assert_eq!(a.len(), 12);
149        assert_eq!(b.len(), 12);
150
151        let fp_chip = self.fp_chip();
152        // a = \sum_{i = 0}^5 (a_i * w^i + a_{i + 6} * w^i * u)
153        // b = \sum_{i = 0}^5 (b_i * w^i + b_{i + 6} * w^i * u)
154        let mut a0b0_coeffs: Vec<FpChip::UnsafeFieldPoint> = Vec::with_capacity(11);
155        let mut a0b1_coeffs: Vec<FpChip::UnsafeFieldPoint> = Vec::with_capacity(11);
156        let mut a1b0_coeffs: Vec<FpChip::UnsafeFieldPoint> = Vec::with_capacity(11);
157        let mut a1b1_coeffs: Vec<FpChip::UnsafeFieldPoint> = Vec::with_capacity(11);
158        for i in 0..6 {
159            for j in 0..6 {
160                let coeff00 = fp_chip.mul_no_carry(ctx, &a[i], &b[j]);
161                let coeff01 = fp_chip.mul_no_carry(ctx, &a[i], &b[j + 6]);
162                let coeff10 = fp_chip.mul_no_carry(ctx, &a[i + 6], &b[j]);
163                let coeff11 = fp_chip.mul_no_carry(ctx, &a[i + 6], &b[j + 6]);
164                if i + j < a0b0_coeffs.len() {
165                    a0b0_coeffs[i + j] = fp_chip.add_no_carry(ctx, &a0b0_coeffs[i + j], coeff00);
166                    a0b1_coeffs[i + j] = fp_chip.add_no_carry(ctx, &a0b1_coeffs[i + j], coeff01);
167                    a1b0_coeffs[i + j] = fp_chip.add_no_carry(ctx, &a1b0_coeffs[i + j], coeff10);
168                    a1b1_coeffs[i + j] = fp_chip.add_no_carry(ctx, &a1b1_coeffs[i + j], coeff11);
169                } else {
170                    a0b0_coeffs.push(coeff00);
171                    a0b1_coeffs.push(coeff01);
172                    a1b0_coeffs.push(coeff10);
173                    a1b1_coeffs.push(coeff11);
174                }
175            }
176        }
177
178        let mut a0b0_minus_a1b1 = Vec::with_capacity(11);
179        let mut a0b1_plus_a1b0 = Vec::with_capacity(11);
180        for i in 0..11 {
181            let a0b0_minus_a1b1_entry = fp_chip.sub_no_carry(ctx, &a0b0_coeffs[i], &a1b1_coeffs[i]);
182            let a0b1_plus_a1b0_entry = fp_chip.add_no_carry(ctx, &a0b1_coeffs[i], &a1b0_coeffs[i]);
183
184            a0b0_minus_a1b1.push(a0b0_minus_a1b1_entry);
185            a0b1_plus_a1b0.push(a0b1_plus_a1b0_entry);
186        }
187
188        // out_i       = a0b0_minus_a1b1_i + XI_0 * a0b0_minus_a1b1_{i + 6} - a0b1_plus_a1b0_{i + 6}
189        // out_{i + 6} = a0b1_plus_a1b0_{i} + a0b0_minus_a1b1_{i + 6} + XI_0 * a0b1_plus_a1b0_{i + 6}
190        let mut out_coeffs = Vec::with_capacity(12);
191        for i in 0..6 {
192            if i < 5 {
193                let mut coeff = fp_chip.scalar_mul_and_add_no_carry(
194                    ctx,
195                    &a0b0_minus_a1b1[i + 6],
196                    &a0b0_minus_a1b1[i],
197                    XI_0,
198                );
199                coeff = fp_chip.sub_no_carry(ctx, coeff, &a0b1_plus_a1b0[i + 6]);
200                out_coeffs.push(coeff);
201            } else {
202                out_coeffs.push(a0b0_minus_a1b1[i].clone());
203            }
204        }
205        for i in 0..6 {
206            if i < 5 {
207                let mut coeff =
208                    fp_chip.add_no_carry(ctx, &a0b1_plus_a1b0[i], &a0b0_minus_a1b1[i + 6]);
209                coeff =
210                    fp_chip.scalar_mul_and_add_no_carry(ctx, &a0b1_plus_a1b0[i + 6], coeff, XI_0);
211                out_coeffs.push(coeff);
212            } else {
213                out_coeffs.push(a0b1_plus_a1b0[i].clone());
214            }
215        }
216        FieldVector(out_coeffs)
217    }
218
219    impl_field_ext_chip_common!();
220}
221
222mod bn254 {
223    use crate::fields::FieldExtConstructor;
224    use crate::halo2_proofs::halo2curves::bn256::{Fq, Fq12, Fq2, Fq6};
225    // This means we store an Fp12 point as `\sum_{i = 0}^6 (a_{i0} + a_{i1} * u) * w^i`
226    // This is encoded in an FqPoint of degree 12 as `(a_{00}, ..., a_{50}, a_{01}, ..., a_{51})`
227    impl FieldExtConstructor<Fq, 12> for Fq12 {
228        fn new(c: [Fq; 12]) -> Self {
229            Fq12 {
230                c0: Fq6 {
231                    c0: Fq2 { c0: c[0], c1: c[6] },
232                    c1: Fq2 { c0: c[2], c1: c[8] },
233                    c2: Fq2 { c0: c[4], c1: c[10] },
234                },
235                c1: Fq6 {
236                    c0: Fq2 { c0: c[1], c1: c[7] },
237                    c1: Fq2 { c0: c[3], c1: c[9] },
238                    c2: Fq2 { c0: c[5], c1: c[11] },
239                },
240            }
241        }
242
243        fn coeffs(&self) -> Vec<Fq> {
244            let x = self;
245            vec![
246                x.c0.c0.c0, x.c1.c0.c0, x.c0.c1.c0, x.c1.c1.c0, x.c0.c2.c0, x.c1.c2.c0, x.c0.c0.c1,
247                x.c1.c0.c1, x.c0.c1.c1, x.c1.c1.c1, x.c0.c2.c1, x.c1.c2.c1,
248            ]
249        }
250    }
251}
halo2_ecc/fields/fp12.rs

halo2_ecc/fields/
fp12.rs
