sp1_core_machine/operations/
global_interaction.rs

1use crate::air::WordAirBuilder;
2use slop_air::AirBuilder;
3use slop_algebra::{AbstractExtensionField, AbstractField, Field, PrimeField32};
4use sp1_core_executor::{
5    events::{ByteLookupEvent, ByteRecord},
6    ByteOpcode,
7};
8use sp1_derive::AlignedBorrow;
9use sp1_hypercube::{
10    air::SP1AirBuilder,
11    operations::poseidon2::{
12        air::{eval_external_round, eval_internal_rounds},
13        permutation::Poseidon2Cols,
14        trace::populate_perm_deg3,
15        Poseidon2Operation, NUM_EXTERNAL_ROUNDS,
16    },
17    septic_curve::{SepticCurve, CURVE_WITNESS_DUMMY_POINT_X, CURVE_WITNESS_DUMMY_POINT_Y},
18    septic_extension::{SepticBlock, SepticExtension},
19};
20
21/// A set of columns needed to compute the global interaction elliptic curve digest.
22#[derive(AlignedBorrow, Clone, Copy)]
23#[repr(C)]
24pub struct GlobalInteractionOperation<T: Copy> {
25    pub x_coordinate: SepticBlock<T>,
26    pub y_coordinate: SepticBlock<T>,
27    pub permutation: Poseidon2Operation<T>,
28    pub offset: T,
29    pub y6_byte_decomp: [T; 4],
30}
31
32impl<F: PrimeField32> GlobalInteractionOperation<F> {
33    pub fn get_digest(
34        values: [u32; 8],
35        is_receive: bool,
36        kind: u8,
37    ) -> (SepticCurve<F>, u8, [F; 16], [F; 16]) {
38        let mut new_values = values.map(|x| F::from_canonical_u32(x));
39        new_values[0] = new_values[0] + F::from_canonical_u32((kind as u32) << 24);
40        let (point, offset, m_trial, m_hash) = SepticCurve::<F>::lift_x(new_values);
41        if !is_receive {
42            return (point.neg(), offset, m_trial, m_hash);
43        }
44        (point, offset, m_trial, m_hash)
45    }
46
47    pub fn populate(
48        &mut self,
49        blu: &mut impl ByteRecord,
50        values: [u32; 8],
51        is_receive: bool,
52        is_real: bool,
53        kind: u8,
54    ) {
55        if is_real {
56            let (point, offset, m_trial, m_hash) = Self::get_digest(values, is_receive, kind);
57            blu.add_byte_lookup_event(ByteLookupEvent {
58                opcode: ByteOpcode::U8Range,
59                a: 0,
60                b: 0,
61                c: offset,
62            });
63            self.offset = F::from_canonical_u8(offset);
64            self.x_coordinate = SepticBlock::<F>::from(point.x.0);
65            self.y_coordinate = SepticBlock::<F>::from(point.y.0);
66            let range_check_value = if is_receive {
67                point.y.0[6].as_canonical_u32() - 1
68            } else {
69                F::ORDER_U32 - point.y.0[6].as_canonical_u32() - 1
70            };
71            assert!(range_check_value < 63 * (1 << 24));
72            for i in 0..3 {
73                let byte = ((range_check_value >> (8 * i)) & 0xFF) as u8;
74                self.y6_byte_decomp[i] = F::from_canonical_u8(byte);
75                blu.add_byte_lookup_event(ByteLookupEvent {
76                    opcode: ByteOpcode::U8Range,
77                    a: 0,
78                    b: 0,
79                    c: byte,
80                });
81            }
82            let last_byte = (range_check_value >> 24) as u8;
83            self.y6_byte_decomp[3] = F::from_canonical_u8(last_byte);
84            blu.add_byte_lookup_event(ByteLookupEvent {
85                opcode: ByteOpcode::LTU,
86                a: 1,
87                b: last_byte,
88                c: 63,
89            });
90            self.permutation = populate_perm_deg3(m_trial, Some(m_hash));
91
92            assert_eq!(self.x_coordinate.0[0], self.permutation.permutation.perm_output()[0]);
93        } else {
94            self.populate_dummy();
95            assert_eq!(self.x_coordinate.0[0], self.permutation.permutation.perm_output()[0]);
96        }
97    }
98
99    pub fn populate_dummy(&mut self) {
100        self.x_coordinate = SepticBlock::<F>::from_base_fn(|i| {
101            F::from_canonical_u32(CURVE_WITNESS_DUMMY_POINT_X[i])
102        });
103        self.y_coordinate = SepticBlock::<F>::from_base_fn(|i| {
104            F::from_canonical_u32(CURVE_WITNESS_DUMMY_POINT_Y[i])
105        });
106        self.offset = F::zero();
107        for i in 0..4 {
108            self.y6_byte_decomp[i] = F::zero();
109        }
110        self.permutation = populate_perm_deg3([F::zero(); 16], None);
111    }
112}
113
114impl<F: Field> GlobalInteractionOperation<F> {
115    /// Constrain that the elliptic curve point for the global interaction is correctly derived.
116    #[allow(clippy::too_many_arguments)]
117    pub fn eval_single_digest<AB: SP1AirBuilder + slop_air::PairBuilder>(
118        builder: &mut AB,
119        values: [AB::Expr; 8],
120        cols: GlobalInteractionOperation<AB::Var>,
121        is_receive: AB::Expr,
122        is_send: AB::Expr,
123        is_real: AB::Var,
124        kind: AB::Var,
125        message_0_limbs: [AB::Var; 2],
126    ) {
127        // Constrain that the `is_real` is boolean.
128        builder.assert_bool(is_real);
129        builder.when(is_real).assert_eq(is_receive.clone() + is_send.clone(), AB::Expr::one());
130        builder.assert_bool(is_receive.clone());
131        builder.assert_bool(is_send.clone());
132
133        // Ensure that the offset is a byte.
134        builder.send_byte(
135            AB::Expr::from_canonical_u32(ByteOpcode::U8Range as u32),
136            AB::Expr::zero(),
137            AB::Expr::zero(),
138            cols.offset.into(),
139            is_real.into(),
140        );
141
142        // Range check the first element in the message to be 24 bits so that we can encode the
143        // interaction kind in the upper bits.
144        builder.when(is_real).assert_eq(
145            values[0].clone(),
146            message_0_limbs[0] + message_0_limbs[1] * AB::F::from_canonical_u32(1 << 16),
147        );
148        builder.slice_range_check_u16(&[message_0_limbs[0].into(), values[7].clone()], is_real);
149        builder.slice_range_check_u8(&[message_0_limbs[1]], is_real);
150        // Range check that the `kind` is at most 6 bits.
151        builder.send_byte(
152            AB::Expr::from_canonical_u32(ByteOpcode::Range as u32),
153            kind.into(),
154            AB::Expr::from_canonical_u32(6),
155            AB::Expr::zero(),
156            is_real.into(),
157        );
158
159        // Turn the message into a hash input. Only the first 8 elements are non-zero, as the rate
160        // of the Poseidon2 hash is 8. Combining `values[0]` with `kind` is safe, as
161        // `values[0]` is range checked to be 24 bits, and `kind` is known to be 6 bits.
162        // Combining `values[7]` with `offset` is also safe, since `values[7]` is range checked
163        // to be 16 bits, while `offset` is known to be 8 bits.
164        let m_trial = [
165            values[0].clone() + AB::Expr::from_canonical_u32(1 << 24) * kind,
166            values[1].clone(),
167            values[2].clone(),
168            values[3].clone(),
169            values[4].clone(),
170            values[5].clone(),
171            values[6].clone(),
172            values[7].clone() + AB::Expr::from_canonical_u32(1 << 16) * cols.offset,
173            AB::Expr::zero(),
174            AB::Expr::zero(),
175            AB::Expr::zero(),
176            AB::Expr::zero(),
177            AB::Expr::zero(),
178            AB::Expr::zero(),
179            AB::Expr::zero(),
180            AB::Expr::zero(),
181        ];
182
183        // Constrain the input of the permutation to be the message.
184        for i in 0..16 {
185            builder.when(is_real).assert_eq(
186                cols.permutation.permutation.external_rounds_state()[0][i].into(),
187                m_trial[i].clone(),
188            );
189        }
190
191        // Constrain the permutation.
192        for r in 0..NUM_EXTERNAL_ROUNDS {
193            eval_external_round(builder, &cols.permutation.permutation, r);
194        }
195        eval_internal_rounds(builder, &cols.permutation.permutation);
196
197        // Constrain that when `is_real` is true, the x-coordinate is the hash of the message.
198        let m_hash = cols.permutation.permutation.perm_output();
199        for i in 0..7 {
200            builder.when(is_real).assert_eq(cols.x_coordinate[i].into(), m_hash[i]);
201        }
202        let x = SepticExtension::<AB::Expr>::from_base_fn(|i| cols.x_coordinate[i].into());
203        let y = SepticExtension::<AB::Expr>::from_base_fn(|i| cols.y_coordinate[i].into());
204
205        // Constrain that `(x, y)` is a valid point on the curve.
206        let y2 = y.square();
207        let x3_2x_26z5 = SepticCurve::<AB::Expr>::curve_formula(x);
208        builder.assert_septic_ext_eq(y2, x3_2x_26z5);
209
210        // Constrain that `0 <= y6_value < 63 * 2^24 < (p - 1) / 2`.
211        let mut y6_value = AB::Expr::zero();
212        for i in 0..3 {
213            y6_value =
214                y6_value + cols.y6_byte_decomp[i] * AB::Expr::from_canonical_u32(1 << (8 * i));
215            builder.send_byte(
216                AB::Expr::from_canonical_u32(ByteOpcode::U8Range as u32),
217                AB::Expr::zero(),
218                AB::Expr::zero(),
219                cols.y6_byte_decomp[i].into(),
220                is_real.into(),
221            );
222        }
223        y6_value = y6_value + cols.y6_byte_decomp[3] * AB::Expr::from_canonical_u32(1 << 24);
224        builder.send_byte(
225            AB::Expr::from_canonical_u32(ByteOpcode::LTU as u32),
226            AB::Expr::one(),
227            cols.y6_byte_decomp[3].into(),
228            AB::Expr::from_canonical_u8(63),
229            is_real.into(),
230        );
231
232        // Constrain that y has correct sign.
233        // If it's a receive: `1 <= y_6 <= 63 * 2^24`, and `y_6 == y6_value + 1`.
234        // If it's a send: `p - 63 * 2^24 <= y_6 <= p - 1`, and `y_6 = p - 1 - y6_value`.
235        builder.when(is_receive).assert_eq(y.0[6].clone(), AB::Expr::one() + y6_value.clone());
236        builder.when(is_send).assert_zero(y.0[6].clone() + AB::Expr::one() + y6_value.clone());
237    }
238}
sp1_core_machine/operations/global_interaction.rs

sp1_core_machine/operations/
global_interaction.rs
