sp1_core_machine/operations/
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;
10
11use sp1_stark::air::SP1AirBuilder;
12
13/// A set of columns needed to compute whether the given word is 0.
14#[derive(AlignedBorrow, Default, Debug, Clone, Copy)]
15#[repr(C)]
16pub struct IsZeroOperation<T> {
17    /// The inverse of the input.
18    pub inverse: T,
19
20    /// Result indicating whether the input is 0. This equals `inverse * input == 0`.
21    pub result: T,
22}
23
24impl<F: Field> IsZeroOperation<F> {
25    pub fn populate(&mut self, a: u32) -> u32 {
26        self.populate_from_field_element(F::from_canonical_u32(a))
27    }
28
29    pub fn populate_from_field_element(&mut self, a: F) -> u32 {
30        if a == F::zero() {
31            self.inverse = F::zero();
32            self.result = F::one();
33        } else {
34            self.inverse = a.inverse();
35            self.result = F::zero();
36        }
37        let prod = self.inverse * a;
38        debug_assert!(prod == F::one() || prod == F::zero());
39        (a == F::zero()) as u32
40    }
41
42    pub fn eval<AB: SP1AirBuilder>(
43        builder: &mut AB,
44        a: AB::Expr,
45        cols: IsZeroOperation<AB::Var>,
46        is_real: AB::Expr,
47    ) {
48        let one: AB::Expr = AB::F::one().into();
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        let is_zero = one.clone() - cols.inverse * a.clone();
61        builder.when(is_real.clone()).assert_eq(is_zero, cols.result);
62        builder.when(is_real.clone()).assert_bool(cols.result);
63
64        // If the result is 1, then the input is 0.
65        builder.when(is_real.clone()).when(cols.result).assert_zero(a.clone());
66    }
67}
sp1_core_machine/operations/is_zero.rs

sp1_core_machine/operations/
is_zero.rs
