Skip to main content

sp1_recursion_circuit/
lib.rs

1use challenger::{
2    CanCopyChallenger, CanObserveVariable, DuplexChallengerVariable, FieldChallengerVariable,
3    MultiField32ChallengerVariable,
4};
5use hash::{FieldHasherVariable, Poseidon2SP1FieldHasherVariable};
6use itertools::izip;
7use slop_algebra::{AbstractExtensionField, AbstractField, PrimeField32};
8use slop_bn254::Bn254Fr;
9use slop_challenger::IopCtx;
10use slop_koala_bear::{
11    KoalaBear_BEGIN_EXT_CONSTS, KoalaBear_END_EXT_CONSTS, KoalaBear_PARTIAL_CONSTS,
12};
13use sp1_hypercube::operations::poseidon2::{NUM_EXTERNAL_ROUNDS, NUM_INTERNAL_ROUNDS};
14use sp1_recursion_compiler::{
15    circuit::CircuitV2Builder,
16    config::{InnerConfig, OuterConfig},
17    ir::{Builder, Config, DslIr, Ext, Felt, SymbolicExt, SymbolicFelt, Var, Variable},
18};
19use sp1_recursion_executor::{RecursionPublicValues, DIGEST_SIZE, NUM_BITS, PERMUTATION_WIDTH};
20use std::iter::{repeat, zip};
21use utils::{felt_bytes_to_bn254_var, felts_to_bn254_var, words_to_bytes};
22
23use sp1_hypercube::SP1InnerPcs;
24pub mod basefold;
25pub mod challenger;
26pub mod dummy;
27pub mod hash;
28pub mod jagged;
29pub mod logup_gkr;
30pub mod machine;
31pub mod shard;
32pub mod sumcheck;
33mod symbolic;
34pub mod utils;
35pub mod witness;
36pub mod zerocheck;
37pub const D: usize = 4;
38use sp1_primitives::{SP1ExtensionField, SP1Field, SP1GlobalContext, SP1OuterGlobalContext};
39
40use crate::utils::felt_proof_nonce_to_bn254_var;
41
42pub type Digest<C, SC> = <SC as FieldHasherVariable<C>>::DigestVariable;
43
44pub type InnerSC = SP1InnerPcs;
45pub trait SP1FieldConfigVariable<C: CircuitConfig>:
46    IopCtx + FieldHasherVariable<C> + Poseidon2SP1FieldHasherVariable<C> + Send + Sync
47{
48    type FriChallengerVariable: FieldChallengerVariable<C, <C as CircuitConfig>::Bit>
49        + CanObserveVariable<C, <Self as FieldHasherVariable<C>>::DigestVariable>
50        + CanCopyChallenger<C>;
51
52    /// Get a new challenger corresponding to the given config.
53    fn challenger_variable(builder: &mut Builder<C>) -> Self::FriChallengerVariable;
54
55    fn commit_recursion_public_values(
56        builder: &mut Builder<C>,
57        public_values: RecursionPublicValues<Felt<SP1Field>>,
58    );
59}
60
61pub trait CircuitConfig: Config {
62    type Bit: Copy + Variable<Self>;
63
64    fn read_bit(builder: &mut Builder<Self>) -> Self::Bit;
65
66    fn read_felt(builder: &mut Builder<Self>) -> Felt<SP1Field>;
67
68    fn read_ext(builder: &mut Builder<Self>) -> Ext<SP1Field, SP1ExtensionField>;
69
70    fn assert_bit_zero(builder: &mut Builder<Self>, bit: Self::Bit);
71
72    fn assert_bit_one(builder: &mut Builder<Self>, bit: Self::Bit);
73
74    fn ext2felt(
75        builder: &mut Builder<Self>,
76        ext: Ext<SP1Field, SP1ExtensionField>,
77    ) -> [Felt<SP1Field>; D];
78
79    fn felt2ext(
80        builder: &mut Builder<Self>,
81        felt: [Felt<SP1Field>; D],
82    ) -> Ext<SP1Field, SP1ExtensionField>;
83
84    fn exp_reverse_bits(
85        builder: &mut Builder<Self>,
86        input: Felt<SP1Field>,
87        power_bits: Vec<Self::Bit>,
88    ) -> Felt<SP1Field>;
89
90    #[allow(clippy::type_complexity)]
91    fn prefix_sum_checks(
92        builder: &mut Builder<Self>,
93        x1: Vec<Felt<SP1Field>>,
94        x2: Vec<Ext<SP1Field, SP1ExtensionField>>,
95    ) -> (Ext<SP1Field, SP1ExtensionField>, Felt<SP1Field>);
96
97    fn num2bits(
98        builder: &mut Builder<Self>,
99        num: Felt<SP1Field>,
100        num_bits: usize,
101    ) -> Vec<Self::Bit>;
102
103    fn bits2num(
104        builder: &mut Builder<Self>,
105        bits: impl IntoIterator<Item = Self::Bit>,
106    ) -> Felt<SP1Field>;
107
108    #[allow(clippy::type_complexity)]
109    fn select_chain_f(
110        builder: &mut Builder<Self>,
111        should_swap: Self::Bit,
112        first: impl IntoIterator<Item = Felt<SP1Field>> + Clone,
113        second: impl IntoIterator<Item = Felt<SP1Field>> + Clone,
114    ) -> Vec<Felt<SP1Field>>;
115
116    #[allow(clippy::type_complexity)]
117    fn select_chain_ef(
118        builder: &mut Builder<Self>,
119        should_swap: Self::Bit,
120        first: impl IntoIterator<Item = Ext<SP1Field, SP1ExtensionField>> + Clone,
121        second: impl IntoIterator<Item = Ext<SP1Field, SP1ExtensionField>> + Clone,
122    ) -> Vec<Ext<SP1Field, SP1ExtensionField>>;
123
124    fn range_check_felt(builder: &mut Builder<Self>, value: Felt<SP1Field>, num_bits: usize) {
125        let bits = Self::num2bits(builder, value, NUM_BITS);
126        for bit in bits.into_iter().skip(num_bits) {
127            Self::assert_bit_zero(builder, bit);
128        }
129    }
130
131    fn poseidon2_permute_v2(
132        builder: &mut Builder<Self>,
133        input: [Felt<SP1Field>; PERMUTATION_WIDTH],
134    ) -> [Felt<SP1Field>; PERMUTATION_WIDTH];
135
136    fn poseidon2_compress_v2(
137        builder: &mut Builder<Self>,
138        input: impl IntoIterator<Item = Felt<SP1Field>>,
139    ) -> [Felt<SP1Field>; DIGEST_SIZE] {
140        let mut pre_iter = input.into_iter().chain(repeat(builder.eval(SP1Field::zero())));
141        let pre = core::array::from_fn(move |_| pre_iter.next().unwrap());
142        let post = Self::poseidon2_permute_v2(builder, pre);
143        let post: [Felt<SP1Field>; DIGEST_SIZE] = post[..DIGEST_SIZE].try_into().unwrap();
144        post
145    }
146}
147
148impl CircuitConfig for InnerConfig {
149    type Bit = Felt<SP1Field>;
150
151    fn assert_bit_zero(builder: &mut Builder<Self>, bit: Self::Bit) {
152        builder.assert_felt_eq(bit, SP1Field::zero());
153    }
154
155    fn assert_bit_one(builder: &mut Builder<Self>, bit: Self::Bit) {
156        builder.assert_felt_eq(bit, SP1Field::one());
157    }
158
159    fn read_bit(builder: &mut Builder<Self>) -> Self::Bit {
160        builder.hint_felt_v2()
161    }
162
163    fn read_felt(builder: &mut Builder<Self>) -> Felt<SP1Field> {
164        builder.hint_felt_v2()
165    }
166
167    fn read_ext(builder: &mut Builder<Self>) -> Ext<SP1Field, SP1ExtensionField> {
168        builder.hint_ext_v2()
169    }
170
171    fn ext2felt(
172        builder: &mut Builder<Self>,
173        ext: Ext<SP1Field, SP1ExtensionField>,
174    ) -> [Felt<SP1Field>; D] {
175        builder.ext2felt_v2(ext)
176    }
177
178    fn felt2ext(
179        builder: &mut Builder<Self>,
180        felt: [Felt<SP1Field>; D],
181    ) -> Ext<SP1Field, SP1ExtensionField> {
182        let mut reconstructed_ext: Ext<SP1Field, SP1ExtensionField> =
183            builder.constant(SP1ExtensionField::zero());
184        for i in 0..D {
185            let mut monomial_slice = [SP1Field::zero(); D];
186            monomial_slice[i] = SP1Field::one();
187            let monomial: Ext<SP1Field, SP1ExtensionField> =
188                builder.constant(SP1ExtensionField::from_base_slice(&monomial_slice));
189            reconstructed_ext = builder.eval(reconstructed_ext + monomial * felt[i]);
190        }
191        reconstructed_ext
192    }
193
194    fn exp_reverse_bits(
195        builder: &mut Builder<Self>,
196        input: Felt<SP1Field>,
197        power_bits: Vec<Felt<SP1Field>>,
198    ) -> Felt<SP1Field> {
199        let mut result = builder.constant(SP1Field::one());
200        let mut power_f = input;
201        let bit_len = power_bits.len();
202
203        for i in 1..=bit_len {
204            let index = bit_len - i;
205            let bit = power_bits[index];
206            let prod: Felt<_> = builder.eval(result * power_f);
207            result = builder.eval(bit * prod + (SymbolicFelt::one() - bit) * result);
208            power_f = builder.eval(power_f * power_f);
209        }
210        result
211    }
212
213    fn prefix_sum_checks(
214        builder: &mut Builder<Self>,
215        x1: Vec<Felt<SP1Field>>,
216        x2: Vec<Ext<SP1Field, SP1ExtensionField>>,
217    ) -> (Ext<SP1Field, SP1ExtensionField>, Felt<SP1Field>) {
218        builder.prefix_sum_checks_v2(x1, x2)
219    }
220
221    fn num2bits(
222        builder: &mut Builder<Self>,
223        num: Felt<SP1Field>,
224        num_bits: usize,
225    ) -> Vec<Felt<SP1Field>> {
226        builder.num2bits_v2_f(num, num_bits)
227    }
228
229    fn bits2num(
230        builder: &mut Builder<Self>,
231        bits: impl IntoIterator<Item = Felt<SP1Field>>,
232    ) -> Felt<SP1Field> {
233        builder.bits2num_v2_f(bits)
234    }
235
236    fn select_chain_f(
237        builder: &mut Builder<Self>,
238        should_swap: Self::Bit,
239        first: impl IntoIterator<Item = Felt<SP1Field>> + Clone,
240        second: impl IntoIterator<Item = Felt<SP1Field>> + Clone,
241    ) -> Vec<Felt<SP1Field>> {
242        let one: Felt<_> = builder.constant(SP1Field::one());
243        let shouldnt_swap: Felt<_> = builder.eval(one - should_swap);
244
245        let id_branch = first.clone().into_iter().chain(second.clone());
246        let swap_branch = second.into_iter().chain(first);
247        zip(zip(id_branch, swap_branch), zip(repeat(shouldnt_swap), repeat(should_swap)))
248            .map(|((id_v, sw_v), (id_c, sw_c))| builder.eval(id_v * id_c + sw_v * sw_c))
249            .collect()
250    }
251
252    fn select_chain_ef(
253        builder: &mut Builder<Self>,
254        should_swap: Self::Bit,
255        first: impl IntoIterator<Item = Ext<SP1Field, SP1ExtensionField>> + Clone,
256        second: impl IntoIterator<Item = Ext<SP1Field, SP1ExtensionField>> + Clone,
257    ) -> Vec<Ext<SP1Field, SP1ExtensionField>> {
258        let one: Felt<_> = builder.constant(SP1Field::one());
259        let shouldnt_swap: Felt<_> = builder.eval(one - should_swap);
260
261        let id_branch = first.clone().into_iter().chain(second.clone());
262        let swap_branch = second.into_iter().chain(first);
263        zip(zip(id_branch, swap_branch), zip(repeat(shouldnt_swap), repeat(should_swap)))
264            .map(|((id_v, sw_v), (id_c, sw_c))| builder.eval(id_v * id_c + sw_v * sw_c))
265            .collect()
266    }
267
268    fn poseidon2_permute_v2(
269        builder: &mut Builder<Self>,
270        input: [Felt<SP1Field>; PERMUTATION_WIDTH],
271    ) -> [Felt<SP1Field>; PERMUTATION_WIDTH] {
272        builder.poseidon2_permute_v2(input)
273    }
274}
275
276#[derive(Debug, Default, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
277pub struct WrapConfig;
278
279impl Config for WrapConfig {
280    type N = <InnerConfig as Config>::N;
281    fn initialize(builder: &mut Builder<Self>) {
282        for round in 0..NUM_EXTERNAL_ROUNDS + NUM_INTERNAL_ROUNDS {
283            for i in 0..PERMUTATION_WIDTH / D {
284                let add_rc = if (NUM_EXTERNAL_ROUNDS / 2
285                    ..NUM_EXTERNAL_ROUNDS / 2 + NUM_INTERNAL_ROUNDS)
286                    .contains(&round)
287                {
288                    builder.constant(SP1ExtensionField::from_base({
289                        let result = KoalaBear_PARTIAL_CONSTS[round - NUM_EXTERNAL_ROUNDS / 2]
290                            .as_canonical_u32();
291
292                        SP1Field::from_wrapped_u32(result)
293                    }))
294                } else {
295                    builder.constant(SP1ExtensionField::from_base_fn(|idx| {
296                        let result = if round < NUM_EXTERNAL_ROUNDS / 2 {
297                            KoalaBear_BEGIN_EXT_CONSTS[round][i * D + idx].as_canonical_u32()
298                        } else {
299                            KoalaBear_END_EXT_CONSTS
300                                [round - NUM_INTERNAL_ROUNDS - NUM_EXTERNAL_ROUNDS / 2][i * D + idx]
301                                .as_canonical_u32()
302                        };
303                        SP1Field::from_wrapped_u32(result)
304                    }))
305                };
306
307                builder.poseidon2_constants.push(add_rc);
308            }
309        }
310    }
311}
312
313impl CircuitConfig for WrapConfig {
314    type Bit = <InnerConfig as CircuitConfig>::Bit;
315
316    fn assert_bit_zero(builder: &mut Builder<Self>, bit: Self::Bit) {
317        builder.assert_felt_eq(bit, SP1Field::zero());
318    }
319
320    fn assert_bit_one(builder: &mut Builder<Self>, bit: Self::Bit) {
321        builder.assert_felt_eq(bit, SP1Field::one());
322    }
323
324    fn read_bit(builder: &mut Builder<Self>) -> Self::Bit {
325        builder.hint_felt_v2()
326    }
327
328    fn read_felt(builder: &mut Builder<Self>) -> Felt<SP1Field> {
329        builder.hint_felt_v2()
330    }
331
332    fn read_ext(builder: &mut Builder<Self>) -> Ext<SP1Field, SP1ExtensionField> {
333        builder.hint_ext_v2()
334    }
335
336    fn ext2felt(
337        builder: &mut Builder<Self>,
338        ext: Ext<SP1Field, SP1ExtensionField>,
339    ) -> [Felt<SP1Field>; D] {
340        let felts = core::array::from_fn(|_| builder.uninit());
341        builder.push_op(DslIr::CircuitChipExt2Felt(felts, ext));
342        felts
343    }
344
345    fn felt2ext(
346        builder: &mut Builder<Self>,
347        felt: [Felt<SP1Field>; D],
348    ) -> Ext<SP1Field, SP1ExtensionField> {
349        let ext = builder.uninit();
350        builder.push_op(DslIr::CircuitChipFelt2Ext(ext, felt));
351        ext
352    }
353
354    fn exp_reverse_bits(
355        builder: &mut Builder<Self>,
356        input: Felt<SP1Field>,
357        power_bits: Vec<Felt<SP1Field>>,
358    ) -> Felt<SP1Field> {
359        let mut result = builder.constant(SP1Field::one());
360        let mut power_f = input;
361        let bit_len = power_bits.len();
362
363        for i in 1..=bit_len {
364            let index = bit_len - i;
365            let bit = power_bits[index];
366            let prod: Felt<_> = builder.eval(result * power_f);
367            result = builder.eval(bit * prod + (SymbolicFelt::one() - bit) * result);
368            power_f = builder.eval(power_f * power_f);
369        }
370        result
371    }
372
373    fn prefix_sum_checks(
374        builder: &mut Builder<Self>,
375        point_1: Vec<Felt<SP1Field>>,
376        point_2: Vec<Ext<SP1Field, SP1ExtensionField>>,
377    ) -> (Ext<SP1Field, SP1ExtensionField>, Felt<SP1Field>) {
378        let mut acc: Ext<_, _> = builder.uninit();
379        builder.push_op(DslIr::ImmE(acc, SP1ExtensionField::one()));
380        let mut acc_felt: Felt<_> = builder.uninit();
381        builder.push_op(DslIr::ImmF(acc_felt, SP1Field::zero()));
382        let one: Felt<_> = builder.constant(SP1Field::one());
383        for (i, (x1, x2)) in izip!(point_1.clone(), point_2).enumerate() {
384            let prod = builder.uninit();
385            builder.push_op(DslIr::MulEF(prod, x2, x1));
386            let lagrange_term: Ext<_, _> = builder.eval(SymbolicExt::one() - x1 - x2 + prod + prod);
387            // Check that x1 is boolean.
388            builder.assert_felt_eq(x1 * (x1 - one), SymbolicFelt::zero());
389            acc = builder.eval(acc * lagrange_term);
390            // Only need felt of first half of point_1 (current prefix sum).
391            if i < point_1.len() / 2 {
392                acc_felt = builder.eval(x1 + acc_felt * SymbolicFelt::from_canonical_u32(2));
393            }
394        }
395        (acc, acc_felt)
396    }
397
398    fn num2bits(
399        builder: &mut Builder<Self>,
400        num: Felt<SP1Field>,
401        num_bits: usize,
402    ) -> Vec<Felt<SP1Field>> {
403        builder.num2bits_v2_f(num, num_bits)
404    }
405
406    fn bits2num(
407        builder: &mut Builder<Self>,
408        bits: impl IntoIterator<Item = Felt<SP1Field>>,
409    ) -> Felt<SP1Field> {
410        builder.bits2num_v2_f(bits)
411    }
412
413    fn select_chain_f(
414        builder: &mut Builder<Self>,
415        should_swap: Self::Bit,
416        first: impl IntoIterator<Item = Felt<SP1Field>> + Clone,
417        second: impl IntoIterator<Item = Felt<SP1Field>> + Clone,
418    ) -> Vec<Felt<SP1Field>> {
419        let one: Felt<_> = builder.constant(SP1Field::one());
420        let shouldnt_swap: Felt<_> = builder.eval(one - should_swap);
421
422        let id_branch = first.clone().into_iter().chain(second.clone());
423        let swap_branch = second.into_iter().chain(first);
424        zip(zip(id_branch, swap_branch), zip(repeat(shouldnt_swap), repeat(should_swap)))
425            .map(|((id_v, sw_v), (id_c, sw_c))| builder.eval(id_v * id_c + sw_v * sw_c))
426            .collect()
427    }
428
429    fn select_chain_ef(
430        builder: &mut Builder<Self>,
431        should_swap: Self::Bit,
432        first: impl IntoIterator<Item = Ext<SP1Field, SP1ExtensionField>> + Clone,
433        second: impl IntoIterator<Item = Ext<SP1Field, SP1ExtensionField>> + Clone,
434    ) -> Vec<Ext<SP1Field, SP1ExtensionField>> {
435        let one: Felt<_> = builder.constant(SP1Field::one());
436        let shouldnt_swap: Felt<_> = builder.eval(one - should_swap);
437
438        let id_branch = first.clone().into_iter().chain(second.clone());
439        let swap_branch = second.into_iter().chain(first);
440        zip(zip(id_branch, swap_branch), zip(repeat(shouldnt_swap), repeat(should_swap)))
441            .map(|((id_v, sw_v), (id_c, sw_c))| builder.eval(id_v * id_c + sw_v * sw_c))
442            .collect()
443    }
444
445    fn poseidon2_permute_v2(
446        builder: &mut Builder<Self>,
447        input: [Felt<SP1Field>; PERMUTATION_WIDTH],
448    ) -> [Felt<SP1Field>; PERMUTATION_WIDTH] {
449        let mut state = Self::blockify(builder, input);
450        for i in 0..NUM_EXTERNAL_ROUNDS / 2 {
451            state = Self::external_round(builder, state, i);
452        }
453        for i in 0..NUM_INTERNAL_ROUNDS {
454            state[0] = Self::internal_constant_addition(builder, state[0], i);
455            state[0] = Self::pow7_internal(builder, state[0]);
456            state = Self::internal_linear_layer(builder, state);
457        }
458        for i in NUM_EXTERNAL_ROUNDS / 2..NUM_EXTERNAL_ROUNDS {
459            state = Self::external_round(builder, state, i);
460        }
461        Self::unblockify(builder, state)
462    }
463}
464
465impl WrapConfig {
466    fn blockify(
467        builder: &mut Builder<Self>,
468        input: [Felt<SP1Field>; PERMUTATION_WIDTH],
469    ) -> [Ext<SP1Field, SP1ExtensionField>; PERMUTATION_WIDTH / D] {
470        let mut ret: [Ext<SP1Field, SP1ExtensionField>; PERMUTATION_WIDTH / D] =
471            core::array::from_fn(|_| builder.uninit());
472        for i in 0..PERMUTATION_WIDTH / D {
473            ret[i] = Self::felt2ext(builder, input[i * D..i * D + D].try_into().unwrap());
474        }
475        ret
476    }
477
478    fn unblockify(
479        builder: &mut Builder<Self>,
480        input: [Ext<SP1Field, SP1ExtensionField>; PERMUTATION_WIDTH / D],
481    ) -> [Felt<SP1Field>; PERMUTATION_WIDTH] {
482        let mut ret = core::array::from_fn(|_| builder.uninit());
483        for i in 0..PERMUTATION_WIDTH / D {
484            let felts = Self::ext2felt(builder, input[i]);
485            for j in 0..D {
486                ret[i * D + j] = felts[j];
487            }
488        }
489        ret
490    }
491
492    fn external_round(
493        builder: &mut Builder<Self>,
494        input: [Ext<SP1Field, SP1ExtensionField>; PERMUTATION_WIDTH / D],
495        round_index: usize,
496    ) -> [Ext<SP1Field, SP1ExtensionField>; PERMUTATION_WIDTH / D] {
497        let mut state = input;
498        if round_index == 0 {
499            state = Self::external_linear_layer(builder, state);
500        }
501        state = Self::external_constant_addition(builder, state, round_index);
502        #[allow(clippy::needless_range_loop)]
503        for i in 0..PERMUTATION_WIDTH / D {
504            state[i] = Self::pow7(builder, state[i]);
505        }
506        state = Self::external_linear_layer(builder, state);
507        state
508    }
509
510    fn external_linear_layer(
511        builder: &mut Builder<Self>,
512        input: [Ext<SP1Field, SP1ExtensionField>; PERMUTATION_WIDTH / D],
513    ) -> [Ext<SP1Field, SP1ExtensionField>; PERMUTATION_WIDTH / D] {
514        let output = core::array::from_fn(|_| builder.uninit());
515        builder.push_op(DslIr::Poseidon2ExternalLinearLayer(Box::new((output, input))));
516        output
517    }
518
519    fn internal_linear_layer(
520        builder: &mut Builder<Self>,
521        input: [Ext<SP1Field, SP1ExtensionField>; PERMUTATION_WIDTH / D],
522    ) -> [Ext<SP1Field, SP1ExtensionField>; PERMUTATION_WIDTH / D] {
523        let output = core::array::from_fn(|_| builder.uninit());
524        builder.push_op(DslIr::Poseidon2InternalLinearLayer(Box::new((output, input))));
525        output
526    }
527
528    fn pow7(
529        builder: &mut Builder<Self>,
530        input: Ext<SP1Field, SP1ExtensionField>,
531    ) -> Ext<SP1Field, SP1ExtensionField> {
532        let output = builder.uninit();
533        builder.push_op(DslIr::Poseidon2ExternalSBOX(output, input));
534        output
535    }
536
537    fn pow7_internal(
538        builder: &mut Builder<Self>,
539        input: Ext<SP1Field, SP1ExtensionField>,
540    ) -> Ext<SP1Field, SP1ExtensionField> {
541        let output = builder.uninit();
542        builder.push_op(DslIr::Poseidon2InternalSBOX(output, input));
543        output
544    }
545
546    fn external_constant_addition(
547        builder: &mut Builder<Self>,
548        input: [Ext<SP1Field, SP1ExtensionField>; PERMUTATION_WIDTH / D],
549        round_index: usize,
550    ) -> [Ext<SP1Field, SP1ExtensionField>; PERMUTATION_WIDTH / D] {
551        let output = core::array::from_fn(|_| builder.uninit());
552        let round = if round_index < NUM_EXTERNAL_ROUNDS / 2 {
553            round_index
554        } else {
555            round_index + NUM_INTERNAL_ROUNDS
556        };
557        for i in 0..PERMUTATION_WIDTH / D {
558            let add_rc = builder.poseidon2_constants[(PERMUTATION_WIDTH / D) * round + i];
559            builder.push_op(DslIr::AddE(output[i], input[i], add_rc));
560        }
561
562        output
563    }
564
565    fn internal_constant_addition(
566        builder: &mut Builder<Self>,
567        input: Ext<SP1Field, SP1ExtensionField>,
568        round_index: usize,
569    ) -> Ext<SP1Field, SP1ExtensionField> {
570        let round = round_index + NUM_EXTERNAL_ROUNDS / 2;
571        let add_rc = builder.poseidon2_constants[(PERMUTATION_WIDTH / D) * round];
572        let output = builder.uninit();
573        builder.push_op(DslIr::AddE(output, input, add_rc));
574        output
575    }
576}
577
578impl CircuitConfig for OuterConfig {
579    type Bit = Var<<Self as Config>::N>;
580
581    fn assert_bit_zero(builder: &mut Builder<Self>, bit: Self::Bit) {
582        builder.assert_var_eq(bit, Self::N::zero());
583    }
584
585    fn assert_bit_one(builder: &mut Builder<Self>, bit: Self::Bit) {
586        builder.assert_var_eq(bit, Self::N::one());
587    }
588
589    fn read_bit(builder: &mut Builder<Self>) -> Self::Bit {
590        builder.witness_var()
591    }
592
593    fn read_felt(builder: &mut Builder<Self>) -> Felt<SP1Field> {
594        builder.witness_felt()
595    }
596
597    fn read_ext(builder: &mut Builder<Self>) -> Ext<SP1Field, SP1ExtensionField> {
598        builder.witness_ext()
599    }
600
601    fn ext2felt(
602        builder: &mut Builder<Self>,
603        ext: Ext<SP1Field, SP1ExtensionField>,
604    ) -> [Felt<SP1Field>; D] {
605        let felts = core::array::from_fn(|_| builder.uninit());
606        builder.push_op(DslIr::CircuitExt2Felt(felts, ext));
607        felts
608    }
609
610    fn felt2ext(
611        builder: &mut Builder<Self>,
612        felt: [Felt<SP1Field>; D],
613    ) -> Ext<SP1Field, SP1ExtensionField> {
614        let ext = builder.uninit();
615        builder.push_op(DslIr::CircuitFelts2Ext(felt, ext));
616        ext
617    }
618
619    fn exp_reverse_bits(
620        builder: &mut Builder<Self>,
621        input: Felt<SP1Field>,
622        power_bits: Vec<Var<<Self as Config>::N>>,
623    ) -> Felt<SP1Field> {
624        let mut result = builder.constant(SP1Field::one());
625        let power_f = input;
626        let bit_len = power_bits.len();
627
628        for i in 1..=bit_len {
629            let index = bit_len - i;
630            let bit = power_bits[index];
631            let prod = builder.eval(result * power_f);
632            result = builder.select_f(bit, prod, result);
633            builder.assign(power_f, power_f * power_f);
634        }
635        result
636    }
637
638    fn prefix_sum_checks(
639        builder: &mut Builder<Self>,
640        point_1: Vec<Felt<SP1Field>>,
641        point_2: Vec<Ext<SP1Field, SP1ExtensionField>>,
642    ) -> (Ext<SP1Field, SP1ExtensionField>, Felt<SP1Field>) {
643        let acc: Ext<_, _> = builder.uninit();
644        builder.push_op(DslIr::ImmE(acc, SP1ExtensionField::one()));
645        let mut acc_felt: Felt<_> = builder.uninit();
646        builder.push_op(DslIr::ImmF(acc_felt, SP1Field::zero()));
647        for (i, (x1, x2)) in izip!(point_1.clone(), point_2).enumerate() {
648            builder.push_op(DslIr::EqEval(x1, x2, acc));
649            // Only need felt of first half of point_1 (current prefix sum).
650            if i < point_1.len() / 2 {
651                acc_felt = builder.eval(x1 + acc_felt * SymbolicFelt::from_canonical_u32(2));
652            }
653        }
654        (acc, acc_felt)
655    }
656
657    fn num2bits(
658        builder: &mut Builder<Self>,
659        num: Felt<SP1Field>,
660        num_bits: usize,
661    ) -> Vec<Var<<Self as Config>::N>> {
662        builder.num2bits_f_circuit(num)[..num_bits].to_vec()
663    }
664
665    fn bits2num(
666        builder: &mut Builder<Self>,
667        bits: impl IntoIterator<Item = Var<<Self as Config>::N>>,
668    ) -> Felt<SP1Field> {
669        let result = builder.eval(SP1Field::zero());
670        for (i, bit) in bits.into_iter().enumerate() {
671            let to_add: Felt<_> = builder.uninit();
672            let pow2 = builder.constant(SP1Field::from_canonical_u32(1 << i));
673            let zero = builder.constant(SP1Field::zero());
674            builder.push_op(DslIr::CircuitSelectF(bit, pow2, zero, to_add));
675            builder.assign(result, result + to_add);
676        }
677        result
678    }
679
680    fn select_chain_f(
681        builder: &mut Builder<Self>,
682        should_swap: Self::Bit,
683        first: impl IntoIterator<Item = Felt<SP1Field>> + Clone,
684        second: impl IntoIterator<Item = Felt<SP1Field>> + Clone,
685    ) -> Vec<Felt<SP1Field>> {
686        let id_branch = first.clone().into_iter().chain(second.clone());
687        let swap_branch = second.into_iter().chain(first);
688        zip(id_branch, swap_branch)
689            .map(|(id_v, sw_v): (Felt<_>, Felt<_>)| -> Felt<_> {
690                let result: Felt<_> = builder.uninit();
691                builder.push_op(DslIr::CircuitSelectF(should_swap, sw_v, id_v, result));
692                result
693            })
694            .collect()
695    }
696
697    fn select_chain_ef(
698        builder: &mut Builder<Self>,
699        should_swap: Self::Bit,
700        first: impl IntoIterator<Item = Ext<SP1Field, SP1ExtensionField>> + Clone,
701        second: impl IntoIterator<Item = Ext<SP1Field, SP1ExtensionField>> + Clone,
702    ) -> Vec<Ext<SP1Field, SP1ExtensionField>> {
703        let id_branch = first.clone().into_iter().chain(second.clone());
704        let swap_branch = second.into_iter().chain(first);
705        zip(id_branch, swap_branch)
706            .map(|(id_v, sw_v): (Ext<_, _>, Ext<_, _>)| -> Ext<_, _> {
707                let result: Ext<_, _> = builder.uninit();
708                builder.push_op(DslIr::CircuitSelectE(should_swap, sw_v, id_v, result));
709                result
710            })
711            .collect()
712    }
713
714    fn poseidon2_permute_v2(
715        _: &mut Builder<Self>,
716        _: [Felt<SP1Field>; PERMUTATION_WIDTH],
717    ) -> [Felt<SP1Field>; PERMUTATION_WIDTH] {
718        unimplemented!();
719    }
720}
721
722impl<C: CircuitConfig<Bit = Felt<SP1Field>>> SP1FieldConfigVariable<C> for SP1GlobalContext {
723    type FriChallengerVariable = DuplexChallengerVariable<C>;
724
725    fn challenger_variable(builder: &mut Builder<C>) -> Self::FriChallengerVariable {
726        DuplexChallengerVariable::new(builder)
727    }
728
729    fn commit_recursion_public_values(
730        builder: &mut Builder<C>,
731        public_values: RecursionPublicValues<Felt<SP1Field>>,
732    ) {
733        builder.commit_public_values_v2(public_values);
734    }
735}
736
737impl<C: CircuitConfig<N = Bn254Fr, Bit = Var<Bn254Fr>>> SP1FieldConfigVariable<C>
738    for SP1OuterGlobalContext
739{
740    type FriChallengerVariable = MultiField32ChallengerVariable<C>;
741
742    fn challenger_variable(builder: &mut Builder<C>) -> Self::FriChallengerVariable {
743        MultiField32ChallengerVariable::new(builder)
744    }
745
746    fn commit_recursion_public_values(
747        builder: &mut Builder<C>,
748        public_values: RecursionPublicValues<Felt<SP1Field>>,
749    ) {
750        let committed_values_digest_bytes_felts: [Felt<_>; 32] =
751            words_to_bytes(&public_values.committed_value_digest).try_into().unwrap();
752        let committed_values_digest_bytes: Var<_> =
753            felt_bytes_to_bn254_var(builder, &committed_values_digest_bytes_felts);
754        builder.commit_committed_values_digest_circuit(committed_values_digest_bytes);
755
756        let vkey_hash = felts_to_bn254_var(builder, &public_values.sp1_vk_digest);
757        builder.commit_vkey_hash_circuit(vkey_hash);
758
759        let exit_code = public_values.exit_code;
760        let var_exit_code: Var<C::N> = builder.felt2var_circuit(exit_code);
761        builder.commit_exit_code_circuit(var_exit_code);
762
763        let vk_root: Var<_> = felts_to_bn254_var(builder, &public_values.vk_root);
764        builder.commit_vk_root_circuit(vk_root);
765
766        let proof_nonce: Var<_> =
767            felt_proof_nonce_to_bn254_var(builder, &public_values.proof_nonce);
768        builder.commit_proof_nonce_circuit(proof_nonce);
769    }
770}