sp1_recursion_core/air/
is_ext_zero.rs

1//! An operation to check if the input is 0.
2//!
3//! This is guaranteed to return 1 if and only if the input is 0.
4//!
5//! The idea is that 1 - input * inverse is exactly the boolean value indicating whether the input
6//! is 0.
7use crate::air::Block;
8use p3_air::AirBuilder;
9use p3_field::{
10    extension::{BinomialExtensionField, BinomiallyExtendable},
11    AbstractField, Field,
12};
13use sp1_derive::AlignedBorrow;
14use sp1_stark::air::{BinomialExtension, SP1AirBuilder};
15
16use crate::air::extension::BinomialExtensionUtils;
17
18use crate::runtime::D;
19
20/// A set of columns needed to compute whether the given word is 0.
21#[derive(AlignedBorrow, Default, Debug, Clone, Copy)]
22#[repr(C)]
23pub struct IsExtZeroOperation<T> {
24    /// The inverse of the input.
25    pub inverse: Block<T>,
26
27    /// Result indicating whether the input is 0. This equals `inverse * input == 0`.
28    pub result: T,
29}
30
31impl<F: Field + BinomiallyExtendable<D>> IsExtZeroOperation<F> {
32    pub fn populate(&mut self, a: Block<F>) -> F {
33        let a = BinomialExtensionField::<F, D>::from_block(a);
34
35        let (inverse, result) = if a.is_zero() {
36            (BinomialExtensionField::zero(), F::one())
37        } else {
38            (a.inverse(), F::zero())
39        };
40
41        self.inverse = inverse.as_block();
42        self.result = result;
43
44        let prod = inverse * a;
45        debug_assert!(prod == BinomialExtensionField::<F, D>::one() || prod.is_zero());
46
47        result
48    }
49}
50
51impl<F: Field> IsExtZeroOperation<F> {
52    pub fn eval<AB: SP1AirBuilder>(
53        builder: &mut AB,
54        a: BinomialExtension<AB::Expr>,
55        cols: IsExtZeroOperation<AB::Var>,
56        is_real: AB::Expr,
57    ) {
58        // Assert that the `is_real` is a boolean.
59        builder.assert_bool(is_real.clone());
60        // Assert that the result is boolean.
61        builder.when(is_real.clone()).assert_bool(cols.result);
62
63        // 1. Input == 0 => is_zero = 1 regardless of the inverse.
64        // 2. Input != 0
65        //   2.1. inverse is correctly set => is_zero = 0.
66        //   2.2. inverse is incorrect
67        //     2.2.1 inverse is nonzero => is_zero isn't bool, it fails.
68        //     2.2.2 inverse is 0 => is_zero is 1. But then we would assert that a = 0. And that
69        //                           assert fails.
70
71        // If the input is 0, then any product involving it is 0. If it is nonzero and its inverse
72        // is correctly set, then the product is 1.
73        let one_ext = BinomialExtension::<AB::Expr>::from_base(AB::Expr::one());
74
75        let inverse = cols.inverse.as_extension::<AB>();
76
77        let is_zero = one_ext.clone() - inverse * a.clone();
78        let result_ext = BinomialExtension::<AB::Expr>::from_base(cols.result.into());
79
80        for (eq_z, res) in is_zero.into_iter().zip(result_ext.0) {
81            builder.when(is_real.clone()).assert_eq(eq_z, res);
82        }
83
84        builder.when(is_real.clone()).assert_bool(cols.result);
85
86        // If the result is 1, then the input is 0.
87        for x in a {
88            builder.when(is_real.clone()).when(cols.result).assert_zero(x.clone());
89        }
90    }
91}
sp1_recursion_core/air/is_ext_zero.rs

sp1_recursion_core/air/
is_ext_zero.rs
