verify_last_layer

src/common/horner_eval.cairo

@@ -3,7 +3,7 @@
 // `point` is the value at which the polynomial will be evaluated.
 // The function returns the polynomial evaluation as `felt252`.
 
-fn horner_eval(coefs: Array<felt252>, point: felt252) -> felt252 {
+fn horner_eval(coefs: Span<felt252>, point: felt252) -> felt252 {
     let mut res = 0;
     let mut i = coefs.len();
     loop {

src/common/math.cairo

@@ -17,6 +17,11 @@ fn pow(base: felt252, exp: felt252) -> felt252 {
             exp = exp / 2; // Divide exponent by 2
         }
     };
-
     res
 }
+
+fn mul_inverse(x: felt252) -> felt252 {
+    // From Fermat's little theorem, a ^ (p - 1) = 1 when p is prime and a != 0. Since a ^ (p - 1) = a · a ^ (p - 2) we have that 
+    // a ^ (p - 2) is the multiplicative inverse of a modulo p.
+    pow(x, 3618502788666131213697322783095070105623107215331596699973092056135872020479)
+}

src/common/tests/test_horner_eval.cairo

@@ -1,10 +1,11 @@
+use core::array::ArrayTrait;
 use cairo_verifier::common::horner_eval::horner_eval;
 
 #[test]
 #[available_gas(9999999999)]
 fn test_horner_eval_0() {
     let mut coefs = ArrayTrait::<felt252>::new();
-    let eval = horner_eval(coefs, 1);
+    let eval = horner_eval(coefs.span(), 1);
     assert(eval == 0, 'invalid evaluation result');
 }
 
@@ -13,7 +14,7 @@ fn test_horner_eval_0() {
 fn test_horner_eval_1() {
     let mut coefs = ArrayTrait::<felt252>::new();
     coefs.append(1);
-    let eval = horner_eval(coefs, 7);
+    let eval = horner_eval(coefs.span(), 7);
     assert(eval == 1, 'invalid evaluation result');
 }
 
@@ -26,7 +27,7 @@ fn test_horner_eval_2() {
     coefs.append(19);
     coefs.append(1);
     coefs.append(9);
-    let eval = horner_eval(coefs, 13);
+    let eval = horner_eval(coefs.span(), 13);
     assert(eval == 262591, 'invalid evaluation result');
 }
 
@@ -48,6 +49,6 @@ fn test_horner_eval_3() {
     coefs.append(7);
     coefs.append(111);
     coefs.append(1);
-    let eval = horner_eval(coefs, 19);
+    let eval = horner_eval(coefs.span(), 19);
     assert(eval == 288577899334361215, 'invalid evaluation result');
 }

src/common/tests/test_math.cairo

@@ -1,4 +1,4 @@
-use cairo_verifier::common::math::pow;
+use cairo_verifier::common::math::{pow, mul_inverse};
 
 #[test]
 #[available_gas(9999999999)]
@@ -25,3 +25,43 @@ fn test_pow_2() {
         'Invalid value'
     );
 }
+
+#[test]
+#[available_gas(9999999999)]
+fn test_mul_inverse_1() {
+    let x = 9751091999414713;
+    let inv_x = mul_inverse(x);
+    assert(x * inv_x == 1, 'Invalid value');
+}
+
+#[test]
+#[available_gas(9999999999)]
+fn test_mul_inverse_2() {
+    let x = 97199414713;
+    let inv_x = mul_inverse(x);
+    assert(x * inv_x == 1, 'Invalid value');
+}
+
+#[test]
+#[available_gas(9999999999)]
+fn test_mul_inverse_3() {
+    let x = 92011457780;
+    let inv_x = mul_inverse(x);
+    assert(x * inv_x == 1, 'Invalid value');
+}
+
+#[test]
+#[available_gas(9999999999)]
+fn test_mul_inverse_4() {
+    let x = 193456804421077096570009938751278224656090409051406060084;
+    let inv_inv_x = mul_inverse(mul_inverse(x));
+    assert(x == inv_inv_x, 'Invalid value');
+}
+
+#[test]
+#[available_gas(9999999999)]
+fn test_mul_inverse_5() {
+    let x = 19345680409051406060084;
+    let inv_inv_x = mul_inverse(mul_inverse(x));
+    assert(x == inv_inv_x, 'Invalid value');
+}

src/fri.cairo

@@ -2,6 +2,8 @@ mod fri_formula;
 mod fri_group;
 mod fri_layer;
 mod fri_config;
+mod fri_last_layer;
+mod fri;
 
 #[cfg(test)]
 mod tests;

src/fri/fri_last_layer.cairo

@@ -0,0 +1,26 @@
+use core::option::OptionTrait;
+use core::traits::TryInto;
+
+use cairo_verifier::common::horner_eval;
+use cairo_verifier::common::math;
+use cairo_verifier::fri::fri_layer::FriLayerQuery;
+// Verifies FRI last layer by evaluating the given polynomial on the given points (=inverses of
+// x_inv_values), and comparing the results to the given values.
+fn verify_last_layer(
+    n_queries: felt252,
+    queries: Span<FriLayerQuery>,
+    coefficients: Span<felt252>
+) {
+    let mut i: u32 = 0;
+    let len: u32 = n_queries.try_into().unwrap();
+    loop {
+        if i == len {
+            break;
+        }
+        let value = horner_eval::horner_eval(
+            coefficients, math::mul_inverse(*(queries.at(i)).x_inv_value)
+        );
+        assert(value == *(queries.at(i)).y_value, '');
+        i += 1;
+    }
+}