sp1_core_machine/operations/
baby_bear_range.rs

1use std::array;
2
3use p3_air::AirBuilder;
4use p3_field::{AbstractField, Field};
5use sp1_derive::AlignedBorrow;
6use sp1_stark::air::SP1AirBuilder;
7
8#[derive(AlignedBorrow, Default, Debug, Clone, Copy)]
9#[repr(C)]
10pub struct BabyBearBitDecomposition<T> {
11    /// The bit decoposition of the`value`.
12    pub bits: [T; 32],
13
14    /// The product of the the bits 3 to 5 in `most_sig_byte_decomp`.
15    pub and_most_sig_byte_decomp_3_to_5: T,
16
17    /// The product of the the bits 3 to 6 in `most_sig_byte_decomp`.
18    pub and_most_sig_byte_decomp_3_to_6: T,
19
20    /// The product of the the bits 3 to 7 in `most_sig_byte_decomp`.
21    pub and_most_sig_byte_decomp_3_to_7: T,
22}
23
24impl<F: Field> BabyBearBitDecomposition<F> {
25    pub fn populate(&mut self, value: u32) {
26        self.bits = array::from_fn(|i| F::from_canonical_u32((value >> i) & 1));
27        let most_sig_byte_decomp = &self.bits[24..32];
28        self.and_most_sig_byte_decomp_3_to_5 = most_sig_byte_decomp[3] * most_sig_byte_decomp[4];
29        self.and_most_sig_byte_decomp_3_to_6 =
30            self.and_most_sig_byte_decomp_3_to_5 * most_sig_byte_decomp[5];
31        self.and_most_sig_byte_decomp_3_to_7 =
32            self.and_most_sig_byte_decomp_3_to_6 * most_sig_byte_decomp[6];
33    }
34
35    pub fn range_check<AB: SP1AirBuilder>(
36        builder: &mut AB,
37        value: AB::Var,
38        cols: BabyBearBitDecomposition<AB::Var>,
39        is_real: AB::Expr,
40    ) {
41        let mut reconstructed_value = AB::Expr::zero();
42        for (i, bit) in cols.bits.iter().enumerate() {
43            builder.when(is_real.clone()).assert_bool(*bit);
44            reconstructed_value =
45                reconstructed_value.clone() + AB::Expr::from_wrapped_u32(1 << i) * *bit;
46        }
47
48        // Assert that bits2num(bits) == value.
49        builder.when(is_real.clone()).assert_eq(reconstructed_value, value);
50
51        // Range check that value is less than baby bear modulus.  To do this, it is sufficient
52        // to just do comparisons for the most significant byte. BabyBear's modulus is (in big
53        // endian binary) 01111000_00000000_00000000_00000001.  So we need to check the
54        // following conditions:
55        // 1) if most_sig_byte > 01111000, then fail.
56        // 2) if most_sig_byte == 01111000, then value's lower sig bytes must all be 0.
57        // 3) if most_sig_byte < 01111000, then pass.
58        let most_sig_byte_decomp = &cols.bits[24..32];
59        builder.when(is_real.clone()).assert_zero(most_sig_byte_decomp[7]);
60
61        // Compute the product of the "top bits".
62        builder.when(is_real.clone()).assert_eq(
63            cols.and_most_sig_byte_decomp_3_to_5,
64            most_sig_byte_decomp[3] * most_sig_byte_decomp[4],
65        );
66        builder.when(is_real.clone()).assert_eq(
67            cols.and_most_sig_byte_decomp_3_to_6,
68            cols.and_most_sig_byte_decomp_3_to_5 * most_sig_byte_decomp[5],
69        );
70        builder.when(is_real.clone()).assert_eq(
71            cols.and_most_sig_byte_decomp_3_to_7,
72            cols.and_most_sig_byte_decomp_3_to_6 * most_sig_byte_decomp[6],
73        );
74
75        // If the top bits are all 0, then the lower bits must all be 0.
76        let mut lower_bits_sum: AB::Expr = AB::Expr::zero();
77        for bit in cols.bits[0..27].iter() {
78            lower_bits_sum = lower_bits_sum + *bit;
79        }
80        builder
81            .when(is_real)
82            .when(cols.and_most_sig_byte_decomp_3_to_7)
83            .assert_zero(lower_bits_sum);
84    }
85}
sp1_core_machine/operations/baby_bear_range.rs

sp1_core_machine/operations/
baby_bear_range.rs
