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

sp1_core_machine/operations/
is_zero.rs
