sp1_core_machine/operations/
u16_compare.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#[derive(
15    AlignedBorrow,
16    Default,
17    Debug,
18    Clone,
19    Copy,
20    Serialize,
21    Deserialize,
22    IntoShape,
23    SP1OperationBuilder,
24    StructReflection,
25)]
26#[repr(C)]
27pub struct U16CompareOperation<T> {
28    /// The result of the compare operation (1 if a < b, 0 if a >= b)
29    pub bit: T,
30}
31
32impl<F: Field> U16CompareOperation<F> {
33    pub fn populate(&mut self, record: &mut impl ByteRecord, a_u16: u16, b_u16: u16, c_u16: u16) {
34        self.bit = F::from_canonical_u16(a_u16);
35        let diff = b_u16.wrapping_sub(c_u16);
36        record.add_byte_lookup_event(ByteLookupEvent {
37            opcode: ByteOpcode::Range,
38            a: diff as u16,
39            b: 16,
40            c: 0,
41        });
42    }
43
44    /// Evaluate the compare operation.
45    /// Assumes that `a`, `b` are both u16.
46    /// Constrains that `is_real` is boolean.
47    /// If `is_real` is true, constrains that the result is correctly computed.
48    pub fn eval_compare_u16<AB: SP1AirBuilder>(
49        builder: &mut AB,
50        a: AB::Expr,
51        b: AB::Expr,
52        cols: U16CompareOperation<AB::Var>,
53        is_real: AB::Expr,
54    ) {
55        // Constrain that `is_real` is boolean.
56        builder.assert_bool(is_real.clone());
57        // Constrain that `cols.bit` is boolean.
58        builder.assert_bool(cols.bit);
59        let base = AB::Expr::from_canonical_u32(1 << 16);
60        let diff = a - b + cols.bit * base;
61        // Since `a, b` are both u16, `a - b` will be in `(-2^16, 2^16)`.
62        // If `a < b`, then `bit` must be one for `diff` to be in `[0, 2^16)`.
63        // If `a >= b`, then `bit` must be zero for `diff` to be in `[0, 2^16)`.
64        // With correct `bit`, the `diff` value will be in u16 range.
65        builder.send_byte(
66            AB::Expr::from_canonical_u8(ByteOpcode::Range as u8),
67            diff,
68            AB::Expr::from_canonical_u32(16),
69            AB::Expr::zero(),
70            is_real.clone(),
71        );
72    }
73}
74
75#[derive(Clone, InputParams, InputExpr)]
76pub struct U16CompareOperationInput<AB: SP1AirBuilder> {
77    pub a: AB::Expr,
78    pub b: AB::Expr,
79    pub cols: U16CompareOperation<AB::Var>,
80    pub is_real: AB::Expr,
81}
82
83impl<AB: SP1AirBuilder> SP1Operation<AB> for U16CompareOperation<AB::F> {
84    type Input = U16CompareOperationInput<AB>;
85    type Output = ();
86
87    fn lower(builder: &mut AB, input: Self::Input) -> Self::Output {
88        Self::eval_compare_u16(builder, input.a, input.b, input.cols, input.is_real);
89    }
90}
sp1_core_machine/operations/u16_compare.rs

sp1_core_machine/operations/
u16_compare.rs
