openvm_pairing_guest/halo2curves_shims/bls12_381/
line.rs

1extern crate std;
2
3use std::ops::{Add, Mul, Neg, Sub};
4
5use halo2curves_axiom::bls12_381::{Fq12, Fq2};
6use openvm_ecc_guest::{
7    algebra::{field::FieldExtension, Field},
8    AffinePoint,
9};
10
11use super::{Bls12_381, BLS12_381_XI};
12use crate::pairing::{EvaluatedLine, LineMulMType};
13
14impl LineMulMType<Fq2, Fq12> for Bls12_381 {
15    fn mul_023_by_023(l0: &EvaluatedLine<Fq2>, l1: &EvaluatedLine<Fq2>) -> [Fq2; 5] {
16        let b0 = &l0.b;
17        let c0 = &l0.c;
18        let b1 = &l1.b;
19        let c1 = &l1.c;
20
21        // where w⁶ = xi
22        // l0 * l1 = c0c1 + (c0b1 + c1b0)w² + (c0 + c1)w³ + (b0b1)w⁴ + (b0 +b1)w⁵ + w⁶
23        //         = (c0c1 + xi) + (c0b1 + c1b0)w² + (c0 + c1)w³ + (b0b1)w⁴ + (b0 + b1)w⁵
24        let x0 = c0 * c1 + *BLS12_381_XI;
25        let x2 = c0 * b1 + c1 * b0;
26        let x3 = c0 + c1;
27        let x4 = b0 * b1;
28        let x5 = b0 + b1;
29
30        [x0, x2, x3, x4, x5]
31    }
32
33    /// Multiplies a line in 023-form with a Fp12 element to get an Fp12 element
34    fn mul_by_023(f: &Fq12, l: &EvaluatedLine<Fq2>) -> Fq12 {
35        Self::mul_by_02345(f, &[l.c, l.b, Fq2::ONE, Fq2::ZERO, Fq2::ZERO])
36    }
37
38    /// Multiplies a line in 02345-form with a Fp12 element to get an Fp12 element
39    fn mul_by_02345(f: &Fq12, x: &[Fq2; 5]) -> Fq12 {
40        let fx = Fq12::from_coeffs([x[0], Fq2::ZERO, x[1], x[2], x[3], x[4]]);
41        f * fx
42    }
43}
44
45/// Returns a line function for a tangent line at the point P
46#[allow(non_snake_case)]
47pub fn tangent_line_023<Fp, Fp2>(P: AffinePoint<Fp>) -> EvaluatedLine<Fp2>
48where
49    Fp: Field,
50    Fp2: FieldExtension<Fp> + Field,
51    for<'a> &'a Fp: Add<&'a Fp, Output = Fp>,
52    for<'a> &'a Fp: Sub<&'a Fp, Output = Fp>,
53    for<'a> &'a Fp: Mul<&'a Fp, Output = Fp>,
54    for<'a> &'a Fp2: Add<&'a Fp2, Output = Fp2>,
55    for<'a> &'a Fp2: Sub<&'a Fp2, Output = Fp2>,
56    for<'a> &'a Fp2: Mul<&'a Fp2, Output = Fp2>,
57    for<'a> &'a Fp2: Neg<Output = Fp2>,
58{
59    let one = &Fp2::ONE;
60    let two = &(one + one);
61    let three = &(one + two);
62    let x = &Fp2::embed(P.x);
63    let y = &Fp2::embed(P.y);
64
65    // λ = (3x^2) / (2y)
66    // 1 - λ(x/y)w^-1 + (λx - y)(1/y)w^-3
67    // = (λx - y)(1/y) - λ(x/y)w^2 + w^3
68    //
69    // b = -(λ * x / y)
70    //   = -3x^3 / 2y^2
71    // c = (λ * x - y) / y
72    //   = 3x^3/2y^2 - 1
73    let x_squared = &(x * x);
74    let x_cubed = &(x_squared * x);
75    let y_squared = &(y * y);
76    let three_x_cubed = three * x_cubed;
77    let two_y_squared = two * y_squared;
78
79    let b = three_x_cubed.clone().neg().div_unsafe(&two_y_squared);
80    let c = three_x_cubed.div_unsafe(&two_y_squared) - &Fp2::ONE;
81
82    EvaluatedLine { b, c }
83}