sp1_core_machine/operations/
global_interaction.rs

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

sp1_core_machine/operations/
global_interaction.rs
