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 serde::{Deserialize, Serialize};
8use slop_air::AirBuilder;
9use slop_algebra::{AbstractField, Field};
10use sp1_derive::{AlignedBorrow, InputExpr, InputParams, IntoShape, SP1OperationBuilder};
11
12use sp1_hypercube::air::SP1AirBuilder;
13use struct_reflection::{StructReflection, StructReflectionHelper};
14
15use crate::air::SP1Operation;
16
17/// A set of columns needed to compute whether the given input is 0.
18#[derive(
19    AlignedBorrow,
20    Default,
21    Debug,
22    Clone,
23    Copy,
24    Serialize,
25    Deserialize,
26    IntoShape,
27    SP1OperationBuilder,
28    StructReflection,
29)]
30#[repr(C)]
31pub struct IsZeroOperation<T> {
32    /// The inverse of the input.
33    pub inverse: T,
34
35    /// Result indicating whether the input is 0. This equals `inverse * input == 0`.
36    pub result: T,
37}
38
39impl<F: Field> IsZeroOperation<F> {
40    pub fn populate(&mut self, a: u64) -> u64 {
41        self.populate_from_field_element(F::from_canonical_u64(a))
42    }
43
44    pub fn populate_from_field_element(&mut self, a: F) -> u64 {
45        if a == F::zero() {
46            self.inverse = F::zero();
47            self.result = F::one();
48        } else {
49            self.inverse = a.inverse();
50            self.result = F::zero();
51        }
52        let prod = self.inverse * a;
53        debug_assert!(prod == F::one() || prod == F::zero());
54        (a == F::zero()) as u64
55    }
56
57    /// Evaluate the `IsZeroOperation` on the given inputs.
58    /// If `is_real` is non-zero, it constrains that the result is `a == 0`.
59    fn eval_is_zero<AB: SP1AirBuilder>(
60        builder: &mut AB,
61        a: AB::Expr,
62        cols: IsZeroOperation<AB::Var>,
63        is_real: AB::Expr,
64    ) {
65        let one: AB::Expr = AB::Expr::one();
66
67        // 1. Input == 0 => is_zero = 1 regardless of the inverse.
68        // 2. Input != 0
69        //   2.1. inverse is correctly set => is_zero = 0.
70        //   2.2. inverse is incorrect
71        //     2.2.1 inverse is nonzero => is_zero isn't bool, it fails.
72        //     2.2.2 inverse is 0 => is_zero is 1. But then we would assert that a = 0. And that
73        //                           assert fails.
74
75        // If the input is 0, then any product involving it is 0. If it is nonzero and its inverse
76        // is correctly set, then the product is 1.
77        let is_zero = one.clone() - cols.inverse * a.clone();
78        builder.when(is_real.clone()).assert_eq(is_zero, cols.result);
79        builder.when(is_real.clone()).assert_bool(cols.result);
80
81        // If the result is 1, then the input is 0.
82        builder.when(is_real.clone()).when(cols.result).assert_zero(a.clone());
83    }
84}
85
86#[derive(Clone, InputParams, InputExpr)]
87pub struct IsZeroOperationInput<AB: SP1AirBuilder> {
88    pub a: AB::Expr,
89    pub cols: IsZeroOperation<AB::Var>,
90    pub is_real: AB::Expr,
91}
92
93impl<AB: SP1AirBuilder> SP1Operation<AB> for IsZeroOperation<AB::F> {
94    type Input = IsZeroOperationInput<AB>;
95    type Output = ();
96
97    fn lower(builder: &mut AB, input: Self::Input) {
98        Self::eval_is_zero(builder, input.a, input.cols, input.is_real);
99    }
100}
sp1_core_machine/operations/is_zero.rs

sp1_core_machine/operations/
is_zero.rs
