sp1_recursion_compiler/circuit/
builder.rs

1//! An implementation of Poseidon2 over BN254.
2
3use std::borrow::Cow;
4
5use crate::prelude::*;
6use itertools::Itertools;
7use slop_algebra::{AbstractExtensionField, AbstractField};
8use sp1_hypercube::{
9    septic_curve::SepticCurve, septic_digest::SepticDigest, septic_extension::SepticExtension,
10};
11use sp1_primitives::{SP1ExtensionField, SP1Field};
12use sp1_recursion_executor::{RecursionPublicValues, D, PERMUTATION_WIDTH};
13
14pub trait CircuitV2Builder<C: Config> {
15    fn bits2num_v2_f(&mut self, bits: impl IntoIterator<Item = Felt<SP1Field>>) -> Felt<SP1Field>;
16    fn num2bits_v2_f(&mut self, num: Felt<SP1Field>, num_bits: usize) -> Vec<Felt<SP1Field>>;
17    fn prefix_sum_checks_v2(
18        &mut self,
19        point_1: Vec<Felt<SP1Field>>,
20        point_2: Vec<Ext<SP1Field, SP1ExtensionField>>,
21    ) -> (Ext<SP1Field, SP1ExtensionField>, Felt<SP1Field>);
22    fn poseidon2_permute_v2(
23        &mut self,
24        state: [Felt<SP1Field>; PERMUTATION_WIDTH],
25    ) -> [Felt<SP1Field>; PERMUTATION_WIDTH];
26    fn ext2felt_v2(&mut self, ext: Ext<SP1Field, SP1ExtensionField>) -> [Felt<SP1Field>; D];
27    fn add_curve_v2(
28        &mut self,
29        point1: SepticCurve<Felt<SP1Field>>,
30        point2: SepticCurve<Felt<SP1Field>>,
31    ) -> SepticCurve<Felt<SP1Field>>;
32    fn assert_digest_zero_v2(
33        &mut self,
34        is_real: Felt<SP1Field>,
35        digest: SepticDigest<Felt<SP1Field>>,
36    );
37    fn sum_digest_v2(
38        &mut self,
39        digests: Vec<SepticDigest<Felt<SP1Field>>>,
40    ) -> SepticDigest<Felt<SP1Field>>;
41    fn select_global_cumulative_sum(
42        &mut self,
43        is_first_execution_shard: Felt<SP1Field>,
44        vk_digest: SepticDigest<Felt<SP1Field>>,
45    ) -> SepticDigest<Felt<SP1Field>>;
46    fn commit_public_values_v2(&mut self, public_values: RecursionPublicValues<Felt<SP1Field>>);
47    fn cycle_tracker_v2_enter(&mut self, name: impl Into<Cow<'static, str>>);
48    fn cycle_tracker_v2_exit(&mut self);
49    fn hint_ext_v2(&mut self) -> Ext<SP1Field, SP1ExtensionField>;
50    fn hint_felt_v2(&mut self) -> Felt<SP1Field>;
51    fn hint_exts_v2(&mut self, len: usize) -> Vec<Ext<SP1Field, SP1ExtensionField>>;
52    fn hint_felts_v2(&mut self, len: usize) -> Vec<Felt<SP1Field>>;
53}
54
55impl<C: Config> CircuitV2Builder<C> for Builder<C> {
56    fn bits2num_v2_f(&mut self, bits: impl IntoIterator<Item = Felt<SP1Field>>) -> Felt<SP1Field> {
57        let mut num: Felt<_> = self.eval(SP1Field::zero());
58        for (i, bit) in bits.into_iter().enumerate() {
59            // Add `bit * 2^i` to the sum.
60            num = self.eval(num + bit * SP1Field::from_wrapped_u32(1 << i));
61        }
62        num
63    }
64
65    /// Converts a felt to bits inside a circuit.
66    fn num2bits_v2_f(&mut self, num: Felt<SP1Field>, num_bits: usize) -> Vec<Felt<SP1Field>> {
67        let output = std::iter::from_fn(|| Some(self.uninit())).take(num_bits).collect::<Vec<_>>();
68        self.push_op(DslIr::CircuitV2HintBitsF(output.clone(), num));
69
70        let x: SymbolicFelt<_> = output
71            .iter()
72            .enumerate()
73            .map(|(i, &bit)| {
74                self.assert_felt_eq(bit * (bit - SP1Field::one()), SP1Field::zero());
75                bit * SP1Field::from_wrapped_u32(1 << i)
76            })
77            .sum();
78
79        // Range check the bits to be less than the SP1Field modulus.
80
81        assert!(num_bits <= 31, "num_bits must be less than or equal to 31");
82
83        // If there are less than 31 bits, there is nothing to check.
84        if num_bits > 30 {
85            // Since SP1Field modulus is 2^31 - 2^24 + 1, if any of the top `7` bits are zero, the
86            // number is less than 2^24, and we can stop the iteration. Othwriwse, if all the top
87            // `7` bits are '1`, we need to check that all the bottom `24` are '0`
88
89            // Get a flag that is zero if any of the top `7` bits are zero, and one otherwise. We
90            // can do this by simply taking their product (which is bitwise AND).
91            let are_all_top_bits_one: Felt<_> = self.eval(
92                output
93                    .iter()
94                    .rev()
95                    .take(7)
96                    .copied()
97                    .map(SymbolicFelt::from)
98                    .product::<SymbolicFelt<_>>(),
99            );
100
101            // Assert that if all the top `7` bits are one, then all the bottom `24` bits are zero.
102            for bit in output.iter().take(24).copied() {
103                self.assert_felt_eq(bit * are_all_top_bits_one, SP1Field::zero());
104            }
105        }
106
107        // Check that the original number matches the bit decomposition.
108        self.assert_felt_eq(x, num);
109
110        output
111    }
112
113    /// A version of the `prefix_sum_checks` that uses the LagrangeEval precompile.
114    fn prefix_sum_checks_v2(
115        &mut self,
116        point_1: Vec<Felt<SP1Field>>,
117        point_2: Vec<Ext<SP1Field, SP1ExtensionField>>,
118    ) -> (Ext<SP1Field, SP1ExtensionField>, Felt<SP1Field>) {
119        let len = point_1.len();
120        assert_eq!(point_1.len(), point_2.len());
121        // point_1 is current and next prefix sum merged
122        assert_eq!(len % 2, 0);
123        let output: Vec<Ext<_, _>> = std::iter::from_fn(|| Some(self.uninit())).take(len).collect();
124        let field_accs: Vec<Felt<_>> =
125            std::iter::from_fn(|| Some(self.uninit())).take(len).collect();
126        let one: Ext<_, _> = self.uninit();
127        let zero: Felt<_> = self.uninit();
128        self.push_op(DslIr::ImmE(one, SP1ExtensionField::one()));
129        self.push_op(DslIr::ImmF(zero, SP1Field::zero()));
130        self.push_op(DslIr::CircuitV2PrefixSumChecks(Box::new((
131            zero,
132            one,
133            output.clone(),
134            field_accs.clone(),
135            point_1,
136            point_2,
137        ))));
138        (output[len - 1], field_accs[len / 2 - 1])
139    }
140
141    /// Applies the Poseidon2 permutation to the given array.
142    fn poseidon2_permute_v2(
143        &mut self,
144        array: [Felt<SP1Field>; PERMUTATION_WIDTH],
145    ) -> [Felt<SP1Field>; PERMUTATION_WIDTH] {
146        let output: [Felt<SP1Field>; PERMUTATION_WIDTH] = core::array::from_fn(|_| self.uninit());
147        self.push_op(DslIr::CircuitV2Poseidon2PermuteKoalaBear(Box::new((output, array))));
148        output
149    }
150
151    /// Decomposes an ext into its felt coordinates.
152    fn ext2felt_v2(&mut self, ext: Ext<SP1Field, SP1ExtensionField>) -> [Felt<SP1Field>; D] {
153        let felts = core::array::from_fn(|_| self.uninit());
154        self.push_op(DslIr::CircuitExt2Felt(felts, ext));
155        // Verify that the decomposed extension element is correct.
156        let mut reconstructed_ext: Ext<SP1Field, SP1ExtensionField> =
157            self.constant(SP1ExtensionField::zero());
158        for i in 0..4 {
159            let felt = felts[i];
160            let monomial: Ext<SP1Field, SP1ExtensionField> =
161                self.constant(<SP1ExtensionField as AbstractExtensionField<SP1Field>>::monomial(i));
162            reconstructed_ext = self.eval(reconstructed_ext + monomial * felt);
163        }
164
165        self.assert_ext_eq(reconstructed_ext, ext);
166
167        felts
168    }
169
170    /// Adds two septic elliptic curve points.
171    fn add_curve_v2(
172        &mut self,
173        point1: SepticCurve<Felt<SP1Field>>,
174        point2: SepticCurve<Felt<SP1Field>>,
175    ) -> SepticCurve<Felt<SP1Field>> {
176        // Hint the curve addition result.
177        let point_sum_x: [Felt<SP1Field>; 7] = core::array::from_fn(|_| self.uninit());
178        let point_sum_y: [Felt<SP1Field>; 7] = core::array::from_fn(|_| self.uninit());
179        let point =
180            SepticCurve { x: SepticExtension(point_sum_x), y: SepticExtension(point_sum_y) };
181        self.push_op(DslIr::CircuitV2HintAddCurve(Box::new((point, point1, point2))));
182
183        // Convert each point into a point over SymbolicFelt.
184        let point1_symbolic = SepticCurve::convert(point1, |x| x.into());
185        let point2_symbolic = SepticCurve::convert(point2, |x| x.into());
186        let point_symbolic = SepticCurve::convert(point, |x| x.into());
187
188        // Evaluate `sum_checker_x` and `sum_checker_y`.
189        let sum_checker_x = SepticCurve::<SymbolicFelt<SP1Field>>::sum_checker_x(
190            point1_symbolic,
191            point2_symbolic,
192            point_symbolic,
193        );
194
195        let sum_checker_y = SepticCurve::<SymbolicFelt<SP1Field>>::sum_checker_y(
196            point1_symbolic,
197            point2_symbolic,
198            point_symbolic,
199        );
200
201        // Constrain `sum_checker_x` and `sum_checker_y` to be all zero.
202        for limb in sum_checker_x.0 {
203            self.assert_felt_eq(limb, SP1Field::zero());
204        }
205
206        for limb in sum_checker_y.0 {
207            self.assert_felt_eq(limb, SP1Field::zero());
208        }
209
210        point
211    }
212
213    /// Asserts that the `digest` is the zero digest when `is_real` is non-zero.
214    fn assert_digest_zero_v2(
215        &mut self,
216        is_real: Felt<SP1Field>,
217        digest: SepticDigest<Felt<SP1Field>>,
218    ) {
219        let zero = SepticDigest::<SymbolicFelt<SP1Field>>::zero();
220        for (digest_limb_x, zero_limb_x) in digest.0.x.0.into_iter().zip_eq(zero.0.x.0.into_iter())
221        {
222            self.assert_felt_eq(is_real * digest_limb_x, is_real * zero_limb_x);
223        }
224        for (digest_limb_y, zero_limb_y) in digest.0.y.0.into_iter().zip_eq(zero.0.y.0.into_iter())
225        {
226            self.assert_felt_eq(is_real * digest_limb_y, is_real * zero_limb_y);
227        }
228    }
229
230    /// Returns the zero digest when `is_first_execution_shard` is zero, and returns the `vk_digest`
231    /// when `is_first_execution_shard` is one. It is assumed that `is_first_execution_shard` is
232    /// already checked to be a boolean.
233    fn select_global_cumulative_sum(
234        &mut self,
235        is_first_execution_shard: Felt<SP1Field>,
236        vk_digest: SepticDigest<Felt<SP1Field>>,
237    ) -> SepticDigest<Felt<SP1Field>> {
238        let zero = SepticDigest::<SymbolicFelt<SP1Field>>::zero();
239        let one: Felt<SP1Field> = self.constant(SP1Field::one());
240        let x = SepticExtension(core::array::from_fn(|i| {
241            self.eval(
242                is_first_execution_shard * vk_digest.0.x.0[i]
243                    + (one - is_first_execution_shard) * zero.0.x.0[i],
244            )
245        }));
246        let y = SepticExtension(core::array::from_fn(|i| {
247            self.eval(
248                is_first_execution_shard * vk_digest.0.y.0[i]
249                    + (one - is_first_execution_shard) * zero.0.y.0[i],
250            )
251        }));
252        SepticDigest(SepticCurve { x, y })
253    }
254
255    // Sums the digests into one.
256    fn sum_digest_v2(
257        &mut self,
258        digests: Vec<SepticDigest<Felt<SP1Field>>>,
259    ) -> SepticDigest<Felt<SP1Field>> {
260        let mut convert_to_felt =
261            |point: SepticCurve<SP1Field>| SepticCurve::convert(point, |value| self.eval(value));
262
263        let start = convert_to_felt(SepticDigest::starting_digest().0);
264        let zero_digest = convert_to_felt(SepticDigest::zero().0);
265
266        if digests.is_empty() {
267            return SepticDigest(zero_digest);
268        }
269
270        let neg_start = convert_to_felt(SepticDigest::starting_digest().0.neg());
271        let neg_zero_digest = convert_to_felt(SepticDigest::zero().0.neg());
272
273        let mut ret = start;
274        for (i, digest) in digests.clone().into_iter().enumerate() {
275            ret = self.add_curve_v2(ret, digest.0);
276            if i != digests.len() - 1 {
277                ret = self.add_curve_v2(ret, neg_zero_digest)
278            }
279        }
280        SepticDigest(self.add_curve_v2(ret, neg_start))
281    }
282
283    // Commits public values.
284    fn commit_public_values_v2(&mut self, public_values: RecursionPublicValues<Felt<SP1Field>>) {
285        self.push_op(DslIr::CircuitV2CommitPublicValues(Box::new(public_values)));
286    }
287
288    fn cycle_tracker_v2_enter(&mut self, name: impl Into<Cow<'static, str>>) {
289        self.push_op(DslIr::CycleTrackerV2Enter(name.into()));
290    }
291
292    fn cycle_tracker_v2_exit(&mut self) {
293        self.push_op(DslIr::CycleTrackerV2Exit);
294    }
295
296    /// Hint a single felt.
297    fn hint_felt_v2(&mut self) -> Felt<SP1Field> {
298        self.hint_felts_v2(1)[0]
299    }
300
301    /// Hint a single ext.
302    fn hint_ext_v2(&mut self) -> Ext<SP1Field, SP1ExtensionField> {
303        self.hint_exts_v2(1)[0]
304    }
305
306    /// Hint a vector of felts.
307    fn hint_felts_v2(&mut self, len: usize) -> Vec<Felt<SP1Field>> {
308        let arr = std::iter::from_fn(|| Some(self.uninit())).take(len).collect::<Vec<_>>();
309        self.push_op(DslIr::CircuitV2HintFelts(arr[0], len));
310        arr
311    }
312
313    /// Hint a vector of exts.
314    fn hint_exts_v2(&mut self, len: usize) -> Vec<Ext<SP1Field, SP1ExtensionField>> {
315        let arr = std::iter::from_fn(|| Some(self.uninit())).take(len).collect::<Vec<_>>();
316        self.push_op(DslIr::CircuitV2HintExts(arr[0], len));
317        arr
318    }
319}
sp1_recursion_compiler/circuit/builder.rs

sp1_recursion_compiler/circuit/
builder.rs
