sp1_recursion_compiler/ir/
types.rs

1use alloc::format;
2
3use serde::{Deserialize, Serialize};
4use slop_algebra::{AbstractExtensionField, AbstractField, Field};
5use sp1_primitives::{SP1ExtensionField, SP1Field};
6
7use super::{
8    Builder, Config, DslIr, ExtConst, ExtHandle, FeltHandle, FromConstant, SymbolicExt,
9    SymbolicFelt, SymbolicVar, VarHandle, Variable,
10};
11
12/// A variable that represents a native field element.
13///
14/// Used for counters, simple loops, etc.
15#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
16pub struct Var<N> {
17    pub(crate) idx: u32,
18    pub(crate) handle: *mut VarHandle<N>,
19}
20
21/// A variable that represents an emulated field element.
22///
23/// Used to do field arithmetic for recursive verification.
24#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
25pub struct Felt<F> {
26    pub(crate) idx: u32,
27    pub(crate) handle: *mut FeltHandle<F>,
28}
29
30/// A variable that represents an emulated extension field element.
31///
32/// Used to do extension field arithmetic for recursive verification.
33#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
34pub struct Ext<F, EF> {
35    pub(crate) idx: u32,
36    pub(crate) handle: *mut ExtHandle<F, EF>,
37}
38
39unsafe impl<N> Send for Var<N> {}
40unsafe impl<F, EF> Send for Ext<F, EF> {}
41unsafe impl<F> Send for Felt<F> {}
42
43unsafe impl<N> Sync for Var<N> {}
44unsafe impl<F, EF> Sync for Ext<F, EF> {}
45unsafe impl<F> Sync for Felt<F> {}
46
47#[derive(Debug, Clone, Default, Serialize, Deserialize)]
48pub struct Witness<C: Config> {
49    pub vars: Vec<C::N>,
50    pub felts: Vec<SP1Field>,
51    pub exts: Vec<SP1ExtensionField>,
52    pub vkey_hash: C::N,
53    pub committed_values_digest: C::N,
54    pub exit_code: C::N,
55    pub proof_nonce: C::N,
56    pub vk_root: C::N,
57}
58
59impl<C: Config> Witness<C> {
60    pub fn write_vkey_hash(&mut self, vkey_hash: C::N) {
61        self.vars.push(vkey_hash);
62        self.vkey_hash = vkey_hash;
63    }
64
65    pub fn write_committed_values_digest(&mut self, committed_values_digest: C::N) {
66        self.vars.push(committed_values_digest);
67        self.committed_values_digest = committed_values_digest
68    }
69
70    pub fn write_exit_code(&mut self, exit_code: C::N) {
71        self.vars.push(exit_code);
72        self.exit_code = exit_code;
73    }
74
75    pub fn write_vk_root(&mut self, vk_root: C::N) {
76        self.vars.push(vk_root);
77        self.vk_root = vk_root;
78    }
79
80    pub fn write_proof_nonce(&mut self, proof_nonce: C::N) {
81        self.vars.push(proof_nonce);
82        self.proof_nonce = proof_nonce;
83    }
84}
85
86impl<N> Var<N> {
87    pub(crate) const fn new(idx: u32, handle: *mut VarHandle<N>) -> Self {
88        Self { idx, handle }
89    }
90
91    pub(crate) fn id(&self) -> String {
92        format!("var{}", self.idx)
93    }
94}
95
96impl<F> Felt<F> {
97    pub(crate) const fn new(id: u32, handle: *mut FeltHandle<F>) -> Self {
98        Self { idx: id, handle }
99    }
100
101    pub(crate) fn id(&self) -> String {
102        format!("felt{}", self.idx)
103    }
104
105    pub(crate) fn inverse(&self) -> SymbolicFelt<F>
106    where
107        F: Field,
108    {
109        SymbolicFelt::<F>::one() / *self
110    }
111}
112
113impl<F, EF> Ext<F, EF> {
114    pub(crate) const fn new(id: u32, handle: *mut ExtHandle<F, EF>) -> Self {
115        Self { idx: id, handle }
116    }
117
118    pub(crate) fn id(&self) -> String {
119        format!("ext{}", self.idx)
120    }
121}
122
123impl<C: Config> Variable<C> for Var<C::N> {
124    type Expression = SymbolicVar<C::N>;
125
126    fn uninit(builder: &mut Builder<C>) -> Self {
127        let id = builder.variable_count();
128        let var = Var::new(id, builder.var_handle.as_mut());
129        builder.inner.get_mut().variable_count += 1;
130        var
131    }
132
133    fn assign(&self, src: Self::Expression, builder: &mut Builder<C>) {
134        match src {
135            SymbolicVar::Const(src) => {
136                builder.push_op(DslIr::ImmV(*self, src));
137            }
138            SymbolicVar::Val(src) => {
139                builder.push_op(DslIr::AddVI(*self, src, C::N::zero()));
140            }
141        }
142    }
143
144    fn assert_eq(
145        lhs: impl Into<Self::Expression>,
146        rhs: impl Into<Self::Expression>,
147        builder: &mut Builder<C>,
148    ) {
149        let lhs = lhs.into();
150        let rhs = rhs.into();
151
152        match (lhs, rhs) {
153            (SymbolicVar::Const(lhs), SymbolicVar::Const(rhs)) => {
154                assert_eq!(lhs, rhs, "Assertion failed at compile time");
155            }
156            (SymbolicVar::Const(lhs), SymbolicVar::Val(rhs)) => {
157                builder.push_traced_op(DslIr::AssertEqVI(rhs, lhs));
158            }
159            (SymbolicVar::Val(lhs), SymbolicVar::Const(rhs)) => {
160                builder.push_traced_op(DslIr::AssertEqVI(lhs, rhs));
161            }
162            (SymbolicVar::Val(lhs), SymbolicVar::Val(rhs)) => {
163                builder.push_traced_op(DslIr::AssertEqV(lhs, rhs));
164            }
165        }
166    }
167
168    fn assert_ne(
169        lhs: impl Into<Self::Expression>,
170        rhs: impl Into<Self::Expression>,
171        builder: &mut Builder<C>,
172    ) {
173        let lhs = lhs.into();
174        let rhs = rhs.into();
175
176        match (lhs, rhs) {
177            (SymbolicVar::Const(lhs), SymbolicVar::Const(rhs)) => {
178                assert_ne!(lhs, rhs, "Assertion failed at compile time");
179            }
180            (SymbolicVar::Const(lhs), SymbolicVar::Val(rhs)) => {
181                builder.push_traced_op(DslIr::AssertNeVI(rhs, lhs));
182            }
183            (SymbolicVar::Val(lhs), SymbolicVar::Const(rhs)) => {
184                builder.push_traced_op(DslIr::AssertNeVI(lhs, rhs));
185            }
186            (SymbolicVar::Val(lhs), SymbolicVar::Val(rhs)) => {
187                builder.push_traced_op(DslIr::AssertNeV(lhs, rhs));
188            }
189        }
190    }
191}
192
193impl<C: Config> Variable<C> for Felt<SP1Field> {
194    type Expression = SymbolicFelt<SP1Field>;
195
196    fn uninit(builder: &mut Builder<C>) -> Self {
197        let idx = builder.variable_count();
198        let felt = Felt::<SP1Field>::new(idx, builder.felt_handle.as_mut());
199        builder.inner.get_mut().variable_count += 1;
200        felt
201    }
202
203    fn assign(&self, src: Self::Expression, builder: &mut Builder<C>) {
204        match src {
205            SymbolicFelt::Const(src) => {
206                builder.push_op(DslIr::ImmF(*self, src));
207            }
208            SymbolicFelt::Val(src) => {
209                builder.push_op(DslIr::AddFI(*self, src, SP1Field::zero()));
210            }
211        }
212    }
213
214    fn assert_eq(
215        lhs: impl Into<Self::Expression>,
216        rhs: impl Into<Self::Expression>,
217        builder: &mut Builder<C>,
218    ) {
219        let lhs = lhs.into();
220        let rhs = rhs.into();
221
222        match (lhs, rhs) {
223            (SymbolicFelt::Const(lhs), SymbolicFelt::Const(rhs)) => {
224                assert_eq!(lhs, rhs, "Assertion failed at compile time");
225            }
226            (SymbolicFelt::Const(lhs), SymbolicFelt::Val(rhs)) => {
227                builder.push_traced_op(DslIr::AssertEqFI(rhs, lhs));
228            }
229            (SymbolicFelt::Val(lhs), SymbolicFelt::Const(rhs)) => {
230                builder.push_traced_op(DslIr::AssertEqFI(lhs, rhs));
231            }
232            (SymbolicFelt::Val(lhs), SymbolicFelt::Val(rhs)) => {
233                builder.push_traced_op(DslIr::AssertEqF(lhs, rhs));
234            }
235        }
236    }
237
238    fn assert_ne(
239        lhs: impl Into<Self::Expression>,
240        rhs: impl Into<Self::Expression>,
241        builder: &mut Builder<C>,
242    ) {
243        let lhs = lhs.into();
244        let rhs = rhs.into();
245
246        match (lhs, rhs) {
247            (SymbolicFelt::Const(lhs), SymbolicFelt::Const(rhs)) => {
248                assert_ne!(lhs, rhs, "Assertion failed at compile time");
249            }
250            (SymbolicFelt::Const(lhs), SymbolicFelt::Val(rhs)) => {
251                builder.push_traced_op(DslIr::AssertNeFI(rhs, lhs));
252            }
253            (SymbolicFelt::Val(lhs), SymbolicFelt::Const(rhs)) => {
254                builder.push_traced_op(DslIr::AssertNeFI(lhs, rhs));
255            }
256            (SymbolicFelt::Val(lhs), SymbolicFelt::Val(rhs)) => {
257                builder.push_traced_op(DslIr::AssertNeF(lhs, rhs));
258            }
259        }
260    }
261}
262
263impl<C: Config> Variable<C> for Ext<SP1Field, SP1ExtensionField> {
264    type Expression = SymbolicExt<SP1Field, SP1ExtensionField>;
265
266    fn uninit(builder: &mut Builder<C>) -> Self {
267        let idx = builder.variable_count();
268        let ext = Ext::<SP1Field, SP1ExtensionField>::new(idx, builder.ext_handle.as_mut());
269        builder.inner.get_mut().variable_count += 1;
270        ext
271    }
272
273    fn assign(&self, src: Self::Expression, builder: &mut Builder<C>) {
274        match src {
275            SymbolicExt::Const(src) => {
276                builder.push_op(DslIr::ImmE(*self, src));
277            }
278            SymbolicExt::Base(src) => match src {
279                SymbolicFelt::Const(src) => {
280                    builder.push_op(DslIr::ImmE(*self, SP1ExtensionField::from_base(src)));
281                }
282                SymbolicFelt::Val(src) => {
283                    builder.push_op(DslIr::AddEFFI(*self, src, SP1ExtensionField::zero()));
284                }
285            },
286            SymbolicExt::Val(src) => {
287                builder.push_op(DslIr::AddEI(*self, src, SP1ExtensionField::zero()));
288            }
289        }
290    }
291
292    fn assert_eq(
293        lhs: impl Into<Self::Expression>,
294        rhs: impl Into<Self::Expression>,
295        builder: &mut Builder<C>,
296    ) {
297        let lhs = lhs.into();
298        let rhs = rhs.into();
299
300        match (lhs, rhs) {
301            (SymbolicExt::Const(lhs), SymbolicExt::Const(rhs)) => {
302                assert_eq!(lhs, rhs, "Assertion failed at compile time");
303            }
304            (SymbolicExt::Const(lhs), SymbolicExt::Val(rhs)) => {
305                builder.push_traced_op(DslIr::AssertEqEI(rhs, lhs));
306            }
307            (SymbolicExt::Const(lhs), rhs) => {
308                let rhs_value = Self::uninit(builder);
309                rhs_value.assign(rhs, builder);
310                builder.push_traced_op(DslIr::AssertEqEI(rhs_value, lhs));
311            }
312            (SymbolicExt::Val(lhs), SymbolicExt::Const(rhs)) => {
313                builder.push_traced_op(DslIr::AssertEqEI(lhs, rhs));
314            }
315            (SymbolicExt::Val(lhs), SymbolicExt::Val(rhs)) => {
316                builder.push_traced_op(DslIr::AssertEqE(lhs, rhs));
317            }
318            (SymbolicExt::Val(lhs), rhs) => {
319                let rhs_value = Self::uninit(builder);
320                rhs_value.assign(rhs, builder);
321                builder.push_traced_op(DslIr::AssertEqE(lhs, rhs_value));
322            }
323            (lhs, rhs) => {
324                let lhs_value = Self::uninit(builder);
325                lhs_value.assign(lhs, builder);
326                let rhs_value = Self::uninit(builder);
327                rhs_value.assign(rhs, builder);
328                builder.push_traced_op(DslIr::AssertEqE(lhs_value, rhs_value));
329            }
330        }
331    }
332
333    fn assert_ne(
334        lhs: impl Into<Self::Expression>,
335        rhs: impl Into<Self::Expression>,
336        builder: &mut Builder<C>,
337    ) {
338        let lhs = lhs.into();
339        let rhs = rhs.into();
340
341        match (lhs, rhs) {
342            (SymbolicExt::Const(lhs), SymbolicExt::Const(rhs)) => {
343                assert_ne!(lhs, rhs, "Assertion failed at compile time");
344            }
345            (SymbolicExt::Const(lhs), SymbolicExt::Val(rhs)) => {
346                builder.push_traced_op(DslIr::AssertNeEI(rhs, lhs));
347            }
348            (SymbolicExt::Const(lhs), rhs) => {
349                let rhs_value = Self::uninit(builder);
350                rhs_value.assign(rhs, builder);
351                builder.push_traced_op(DslIr::AssertNeEI(rhs_value, lhs));
352            }
353            (SymbolicExt::Val(lhs), SymbolicExt::Const(rhs)) => {
354                builder.push_traced_op(DslIr::AssertNeEI(lhs, rhs));
355            }
356            (SymbolicExt::Val(lhs), SymbolicExt::Val(rhs)) => {
357                builder.push_traced_op(DslIr::AssertNeE(lhs, rhs));
358            }
359            (SymbolicExt::Val(lhs), rhs) => {
360                let rhs_value = Self::uninit(builder);
361                rhs_value.assign(rhs, builder);
362                builder.push_traced_op(DslIr::AssertNeE(lhs, rhs_value));
363            }
364            (lhs, rhs) => {
365                let lhs_value = Self::uninit(builder);
366                lhs_value.assign(lhs, builder);
367                let rhs_value = Self::uninit(builder);
368                rhs_value.assign(rhs, builder);
369                builder.push_traced_op(DslIr::AssertNeE(lhs_value, rhs_value));
370            }
371        }
372    }
373}
374
375impl<C: Config> FromConstant<C> for Var<C::N> {
376    type Constant = C::N;
377
378    fn constant(value: Self::Constant, builder: &mut Builder<C>) -> Self {
379        builder.eval(value)
380    }
381}
382
383impl<C: Config> FromConstant<C> for Felt<SP1Field> {
384    type Constant = SP1Field;
385
386    fn constant(value: Self::Constant, builder: &mut Builder<C>) -> Self {
387        builder.eval(value)
388    }
389}
390
391impl<C: Config> FromConstant<C> for Ext<SP1Field, SP1ExtensionField> {
392    type Constant = SP1ExtensionField;
393
394    fn constant(value: Self::Constant, builder: &mut Builder<C>) -> Self {
395        builder.eval(value.cons())
396    }
397}
sp1_recursion_compiler/ir/types.rs

sp1_recursion_compiler/ir/
types.rs
