sp1_core_machine/operations/
msb.rs

1use serde::{Deserialize, Serialize};
2use sp1_core_executor::{
3    events::{ByteLookupEvent, ByteRecord},
4    ByteOpcode,
5};
6use sp1_hypercube::air::SP1AirBuilder;
7use struct_reflection::{StructReflection, StructReflectionHelper};
8
9use slop_algebra::{AbstractField, Field};
10use sp1_derive::{AlignedBorrow, InputExpr, InputParams, IntoShape, SP1OperationBuilder};
11
12use crate::air::SP1Operation;
13
14/// Operation columns for computing the most significant bit of a u16.
15#[derive(
16    AlignedBorrow,
17    Default,
18    Debug,
19    Clone,
20    Copy,
21    Serialize,
22    Deserialize,
23    IntoShape,
24    SP1OperationBuilder,
25    StructReflection,
26)]
27#[repr(C)]
28pub struct U16MSBOperation<T> {
29    /// The result of the msb operation.
30    pub msb: T,
31}
32
33impl<F: Field> U16MSBOperation<F> {
34    pub fn populate_msb(&mut self, record: &mut impl ByteRecord, a_u16: u16) -> u32 {
35        let msb = (a_u16 >> 15) & 1;
36        self.msb = F::from_canonical_u16(msb);
37        let diff = a_u16.wrapping_mul(2u16);
38        record.add_byte_lookup_event(ByteLookupEvent {
39            opcode: ByteOpcode::Range,
40            a: diff,
41            b: 16,
42            c: 0,
43        });
44        msb as u32
45    }
46
47    /// Evaluate the `U16MSBOperation` on the given inputs.
48    /// Assumes that `a` is a valid u16.
49    /// Constrains that `is_real` is boolean.
50    /// If `is_real` is true, it constrains that the result is the msb of `a`.
51    pub fn eval_msb<AB: SP1AirBuilder>(
52        builder: &mut AB,
53        a: AB::Expr,
54        cols: U16MSBOperation<AB::Var>,
55        is_real: AB::Expr,
56    ) {
57        // Constrain that `is_real` is boolean.
58        builder.assert_bool(is_real.clone());
59        // Constrain that `msb` is boolean.
60        builder.assert_bool(cols.msb);
61        let two = AB::Expr::from_canonical_u32(2);
62        let base = AB::Expr::from_canonical_u32(1 << 16);
63        let diff = two * a - cols.msb * base;
64        // Constrains that `2 * a - msb * 2^16` is in u16 range, while `msb` is boolean.
65        // If `0 <= a < 2^15`, then `msb` must be 0.
66        // If `2^15 <= a < 2^16`, then `msb` must be 1.
67        builder.send_byte(
68            AB::Expr::from_canonical_u8(ByteOpcode::Range as u8),
69            diff,
70            AB::Expr::from_canonical_u32(16),
71            AB::Expr::zero(),
72            is_real,
73        );
74    }
75}
76
77#[derive(Clone, Debug, InputExpr, InputParams)]
78pub struct U16MSBOperationInput<AB: SP1AirBuilder> {
79    pub a: AB::Expr,
80    pub cols: U16MSBOperation<AB::Var>,
81    pub is_real: AB::Expr,
82}
83
84impl<AB: SP1AirBuilder> SP1Operation<AB> for U16MSBOperation<AB::F> {
85    type Input = U16MSBOperationInput<AB>;
86    type Output = ();
87
88    fn lower(builder: &mut AB, input: Self::Input) -> Self::Output {
89        Self::eval_msb(builder, input.a, input.cols, input.is_real);
90    }
91}
sp1_core_machine/operations/msb.rs

sp1_core_machine/operations/
msb.rs
