sp1_recursion_core/air/
is_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 p3_air::AirBuilder;
8use p3_field::{AbstractField, Field};
9use sp1_derive::AlignedBorrow;
10use sp1_stark::air::SP1AirBuilder;
11
12/// A set of columns needed to compute whether the given word is 0.
13#[derive(AlignedBorrow, Default, Debug, Clone, Copy)]
14#[repr(C)]
15pub struct IsZeroOperation<T> {
16    /// The inverse of the input.
17    pub inverse: T,
18
19    /// Result indicating whether the input is 0. This equals `inverse * input == 0`.
20    pub result: T,
21}
22
23impl<F: Field> IsZeroOperation<F> {
24    pub fn populate(&mut self, a: F) -> F {
25        let (inverse, result) =
26            if a.is_zero() { (F::zero(), F::one()) } else { (a.inverse(), F::zero()) };
27
28        self.inverse = inverse;
29        self.result = result;
30
31        let prod = inverse * a;
32        debug_assert!(prod == F::one() || prod.is_zero());
33
34        result
35    }
36}
37
38impl<F: Field> IsZeroOperation<F> {
39    pub fn eval<AB: SP1AirBuilder>(
40        builder: &mut AB,
41        a: AB::Expr,
42        cols: IsZeroOperation<AB::Var>,
43        is_real: AB::Expr,
44    ) {
45        // Assert that the `is_real` is a boolean.
46        builder.assert_bool(is_real.clone());
47        // Assert that the result is boolean.
48        builder.when(is_real.clone()).assert_bool(cols.result);
49
50        // 1. Input == 0 => is_zero = 1 regardless of the inverse.
51        // 2. Input != 0
52        //   2.1. inverse is correctly set => is_zero = 0.
53        //   2.2. inverse is incorrect
54        //     2.2.1 inverse is nonzero => is_zero isn't bool, it fails.
55        //     2.2.2 inverse is 0 => is_zero is 1. But then we would assert that a = 0. And that
56        //                           assert fails.
57
58        // If the input is 0, then any product involving it is 0. If it is nonzero and its inverse
59        // is correctly set, then the product is 1.
60
61        let one = AB::Expr::one();
62        let inverse = cols.inverse;
63
64        let is_zero = one.clone() - inverse * a.clone();
65
66        builder.when(is_real.clone()).assert_eq(is_zero, cols.result);
67
68        builder.when(is_real.clone()).assert_bool(cols.result);
69
70        // If the result is 1, then the input is 0.
71        builder.when(is_real.clone()).when(cols.result).assert_zero(a.clone());
72    }
73}
sp1_recursion_core/air/is_zero.rs

sp1_recursion_core/air/
is_zero.rs
