sp1_core_executor/
air.rs

1use std::{
2    fmt::{Display, Formatter, Result as FmtResult},
3    str::FromStr,
4};
5
6use deepsize2::DeepSizeOf;
7use enum_map::{Enum, EnumMap};
8use serde::{Deserialize, Serialize};
9use sp1_hypercube::shape::Shape;
10use strum::{EnumIter, IntoEnumIterator, IntoStaticStr};
11use subenum::subenum;
12
13/// RV64IM AIR Identifiers.
14///
15/// These identifiers are for the various chips in the rv64im prover. We need them in the
16/// executor to compute the memory cost of the current shard of execution.
17///
18/// The [`CoreAirId`]s are the AIRs that are not part of precompile shards and not the program or
19/// byte AIR.
20#[subenum(CoreAirId)]
21#[derive(
22    Debug,
23    Clone,
24    Copy,
25    PartialEq,
26    Eq,
27    Hash,
28    Serialize,
29    Deserialize,
30    EnumIter,
31    IntoStaticStr,
32    PartialOrd,
33    Ord,
34    Enum,
35    DeepSizeOf,
36)]
37pub enum RiscvAirId {
38    /// The program chip.
39    Program = 0,
40    /// The SHA-256 extend chip.
41    ShaExtend = 1,
42    /// The sha extend control chip.
43    ShaExtendControl = 2,
44    /// The sha extend control chip for user mode.
45    ShaExtendControlUser = 3,
46    /// The SHA-256 compress chip.
47    ShaCompress = 4,
48    /// The sha compress control chip.
49    ShaCompressControl = 5,
50    /// The sha compress control chip for user mode.
51    ShaCompressControlUser = 6,
52    /// The Edwards add assign chip.
53    EdAddAssign = 7,
54    /// The Edwards add assign chip for user mode.
55    EdAddAssignUser = 8,
56    /// The Edwards decompress chip.
57    EdDecompress = 9,
58    /// The Edwards decompress chip for user mode.
59    EdDecompressUser = 10,
60    /// The secp256k1 add assign chip.
61    Secp256k1AddAssign = 11,
62    /// The secp256k1 add assign chip for user mode.
63    Secp256k1AddAssignUser = 12,
64    /// The secp256k1 double assign chip.
65    Secp256k1DoubleAssign = 13,
66    /// The secp256k1 double assign chip for user mode.
67    Secp256k1DoubleAssignUser = 14,
68    /// The secp256r1 add assign chip.
69    Secp256r1AddAssign = 15,
70    /// The secp256r1 add assign chip for user mode.
71    Secp256r1AddAssignUser = 16,
72    /// The secp256r1 double assign chip.
73    Secp256r1DoubleAssign = 17,
74    /// The secp256r1 double assign chip for user mode.
75    Secp256r1DoubleAssignUser = 18,
76    /// The Keccak permute chip.
77    KeccakPermute = 19,
78    /// The keccak permute control chip.
79    KeccakPermuteControl = 20,
80    /// The keccak permute control chip for user mode.
81    KeccakPermuteControlUser = 21,
82    /// The bn254 add assign chip.
83    Bn254AddAssign = 22,
84    /// The bn254 add assign chip for user mode.
85    Bn254AddAssignUser = 23,
86    /// The bn254 double assign chip.
87    Bn254DoubleAssign = 24,
88    /// The bn254 double assign chip for user mode.
89    Bn254DoubleAssignUser = 25,
90    /// The bls12-381 add assign chip.
91    Bls12381AddAssign = 26,
92    /// The bls12-381 add assign chip for user mode.
93    Bls12381AddAssignUser = 27,
94    /// The bls12-381 double assign chip.
95    Bls12381DoubleAssign = 28,
96    /// The bls12-381 double assign chip for user mode.
97    Bls12381DoubleAssignUser = 29,
98    /// The uint256 mul mod chip.
99    Uint256MulMod = 30,
100    /// The uint256 mul mod chip for user mode.
101    Uint256MulModUser = 31,
102    /// The uint256 ops chip.
103    Uint256Ops = 32,
104    /// The uint256 ops chip for user mode.
105    Uint256OpsUser = 33,
106    /// The bls12-381 fp op assign chip.
107    Bls12381FpOpAssign = 34,
108    /// The bls12-381 fp op assign chip for user mode.
109    Bls12381FpOpAssignUser = 35,
110    /// The bls12-381 fp2 add sub assign chip.
111    Bls12381Fp2AddSubAssign = 36,
112    /// The bls12-381 fp2 add sub assign chip for user mode.
113    Bls12381Fp2AddSubAssignUser = 37,
114    /// The bls12-381 fp2 mul assign chip.
115    Bls12381Fp2MulAssign = 38,
116    /// The bls12-381 fp2 mul assign chip for user mode.
117    Bls12381Fp2MulAssignUser = 39,
118    /// The bn254 fp op assign chip.
119    Bn254FpOpAssign = 40,
120    /// The bn254 fp op assign chip for user mode.
121    Bn254FpOpAssignUser = 41,
122    /// The bn254 fp2 add sub assign chip.
123    Bn254Fp2AddSubAssign = 42,
124    /// The bn254 fp2 add sub assign chip for user mode.
125    Bn254Fp2AddSubAssignUser = 43,
126    /// The bn254 fp2 mul assign chip.
127    Bn254Fp2MulAssign = 44,
128    /// The bn254 fp2 mul assign chip for user mode.
129    Bn254Fp2MulAssignUser = 45,
130    /// The poseidon2 chip.
131    Poseidon2 = 46,
132    /// The poseidon2 chip for user mode.
133    Poseidon2User = 47,
134    /// The syscall core chip.
135    #[subenum(CoreAirId)]
136    SyscallCore = 48,
137    /// The syscall core chip for user mode.
138    #[subenum(CoreAirId)]
139    SyscallCoreUser = 49,
140    /// The syscall precompile chip.
141    SyscallPrecompile = 50,
142    /// The syscall precompile chip for user mode.
143    SyscallPrecompileUser = 51,
144    /// The div rem chip.
145    #[subenum(CoreAirId)]
146    DivRem = 52,
147    /// The div rem chip for user mode.
148    #[subenum(CoreAirId)]
149    DivRemUser = 53,
150    /// The add chip.
151    #[subenum(CoreAirId)]
152    Add = 54,
153    /// The add chip for user mode.
154    #[subenum(CoreAirId)]
155    AddUser = 55,
156    /// The addi chip.
157    #[subenum(CoreAirId)]
158    Addi = 56,
159    /// The addi chip for user mode.
160    #[subenum(CoreAirId)]
161    AddiUser = 57,
162    /// The addw chip.
163    #[subenum(CoreAirId)]
164    Addw = 58,
165    /// The addw chip for user mode.
166    #[subenum(CoreAirId)]
167    AddwUser = 59,
168    /// The sub chip.
169    #[subenum(CoreAirId)]
170    Sub = 60,
171    /// The sub chip for user mode.
172    #[subenum(CoreAirId)]
173    SubUser = 61,
174    /// The subw chip.
175    #[subenum(CoreAirId)]
176    Subw = 62,
177    /// The subw chip for user mode.
178    #[subenum(CoreAirId)]
179    SubwUser = 63,
180    /// The bitwise chip.
181    #[subenum(CoreAirId)]
182    Bitwise = 64,
183    /// The bitwise chip for user mode.
184    #[subenum(CoreAirId)]
185    BitwiseUser = 65,
186    /// The mul chip.
187    #[subenum(CoreAirId)]
188    Mul = 66,
189    /// The mul chip for user mode.
190    #[subenum(CoreAirId)]
191    MulUser = 67,
192    /// The shift right chip.
193    #[subenum(CoreAirId)]
194    ShiftRight = 68,
195    /// The shift right chip for user mode.
196    #[subenum(CoreAirId)]
197    ShiftRightUser = 69,
198    /// The shift left chip.
199    #[subenum(CoreAirId)]
200    ShiftLeft = 70,
201    /// The shift left chip for user mode.
202    #[subenum(CoreAirId)]
203    ShiftLeftUser = 71,
204    /// The lt chip.
205    #[subenum(CoreAirId)]
206    Lt = 72,
207    /// The lt chip for user mode.
208    #[subenum(CoreAirId)]
209    LtUser = 73,
210    /// The load byte chip.
211    #[subenum(CoreAirId)]
212    LoadByte = 74,
213    /// The load byte chip for user mode.
214    #[subenum(CoreAirId)]
215    LoadByteUser = 75,
216    /// The load half chip.
217    #[subenum(CoreAirId)]
218    LoadHalf = 76,
219    /// The load half chip for user mode.
220    #[subenum(CoreAirId)]
221    LoadHalfUser = 77,
222    /// The load word chip.
223    #[subenum(CoreAirId)]
224    LoadWord = 78,
225    /// The load word chip for user mode.
226    #[subenum(CoreAirId)]
227    LoadWordUser = 79,
228    /// The load x0 chip.
229    #[subenum(CoreAirId)]
230    LoadX0 = 80,
231    /// The load x0 chip for user mode.
232    #[subenum(CoreAirId)]
233    LoadX0User = 81,
234    /// The load double chip.
235    #[subenum(CoreAirId)]
236    LoadDouble = 82,
237    /// The load double chip for user mode.
238    #[subenum(CoreAirId)]
239    LoadDoubleUser = 83,
240    /// The store byte chip.
241    #[subenum(CoreAirId)]
242    StoreByte = 84,
243    /// The store byte chip for user mode.
244    #[subenum(CoreAirId)]
245    StoreByteUser = 85,
246    /// The store half chip.
247    #[subenum(CoreAirId)]
248    StoreHalf = 86,
249    /// The store half chip for user mode.
250    #[subenum(CoreAirId)]
251    StoreHalfUser = 87,
252    /// The store word chip.
253    #[subenum(CoreAirId)]
254    StoreWord = 88,
255    /// The store word chip for user mode.
256    #[subenum(CoreAirId)]
257    StoreWordUser = 89,
258    /// The store double chip.
259    #[subenum(CoreAirId)]
260    StoreDouble = 90,
261    /// The store double chip for user mode.
262    #[subenum(CoreAirId)]
263    StoreDoubleUser = 91,
264    /// The utype chip.
265    #[subenum(CoreAirId)]
266    UType = 92,
267    /// The utype chip for user mode.
268    #[subenum(CoreAirId)]
269    UTypeUser = 93,
270    /// The branch chip.
271    #[subenum(CoreAirId)]
272    Branch = 94,
273    /// The branch chip for user mode.
274    #[subenum(CoreAirId)]
275    BranchUser = 95,
276    /// The jal chip.
277    #[subenum(CoreAirId)]
278    Jal = 96,
279    /// The jal chip for user mode.
280    #[subenum(CoreAirId)]
281    JalUser = 97,
282    /// The jalr chip.
283    #[subenum(CoreAirId)]
284    Jalr = 98,
285    /// The jalr chip for user mode.
286    #[subenum(CoreAirId)]
287    JalrUser = 99,
288    /// The syscall instructions chip.
289    #[subenum(CoreAirId)]
290    SyscallInstrs = 100,
291    /// The syscall instructions chip for user mode.
292    #[subenum(CoreAirId)]
293    SyscallInstrsUser = 101,
294    /// The memory bump chip.
295    #[subenum(CoreAirId)]
296    MemoryBump = 102,
297    /// The state bump chip.
298    #[subenum(CoreAirId)]
299    StateBump = 103,
300    /// The memory global init chip.
301    MemoryGlobalInit = 104,
302    /// The memory global finalize chip.
303    MemoryGlobalFinalize = 105,
304    /// The memory local chip.
305    #[subenum(CoreAirId)]
306    MemoryLocal = 106,
307    /// The global chip.
308    #[subenum(CoreAirId)]
309    Global = 107,
310    /// The byte chip.
311    Byte = 108,
312    /// The range chip.
313    Range = 109,
314    /// The ALU x0 chip (all ALU ops with rd = x0).
315    #[subenum(CoreAirId)]
316    AluX0 = 110,
317    /// The ALU x0 chip (all ALU ops with rd = x0) for user mode.
318    #[subenum(CoreAirId)]
319    AluX0User = 111,
320    /// The mprotect chip.
321    #[subenum(CoreAirId)]
322    Mprotect = 112,
323    /// The sigreturn chip.
324    SigReturn = 113,
325    /// The instruction decode chip.
326    #[subenum(CoreAirId)]
327    InstructionDecode = 114,
328    /// The instruction fetch chip.
329    #[subenum(CoreAirId)]
330    InstructionFetch = 115,
331    /// The page prot chip.
332    #[subenum(CoreAirId)]
333    PageProt = 116,
334    /// The page prot local chip.
335    #[subenum(CoreAirId)]
336    PageProtLocal = 117,
337    /// The page prot global init chip.
338    PageProtGlobalInit = 118,
339    /// The page prot global finalize chip.
340    PageProtGlobalFinalize = 119,
341    /// The trap exec chip.
342    #[subenum(CoreAirId)]
343    TrapExec = 120,
344    /// The trap memory chip.
345    #[subenum(CoreAirId)]
346    TrapMem = 121,
347}
348
349impl RiscvAirId {
350    /// Returns the AIRs that are not part of precompile shards and not the program or byte AIR.
351    #[must_use]
352    pub fn core() -> Vec<RiscvAirId> {
353        vec![
354            RiscvAirId::Add,
355            RiscvAirId::AddUser,
356            RiscvAirId::Addi,
357            RiscvAirId::AddiUser,
358            RiscvAirId::Addw,
359            RiscvAirId::AddwUser,
360            RiscvAirId::Sub,
361            RiscvAirId::SubUser,
362            RiscvAirId::Subw,
363            RiscvAirId::SubwUser,
364            RiscvAirId::Mul,
365            RiscvAirId::MulUser,
366            RiscvAirId::Bitwise,
367            RiscvAirId::BitwiseUser,
368            RiscvAirId::ShiftLeft,
369            RiscvAirId::ShiftLeftUser,
370            RiscvAirId::ShiftRight,
371            RiscvAirId::ShiftRightUser,
372            RiscvAirId::DivRem,
373            RiscvAirId::DivRemUser,
374            RiscvAirId::Lt,
375            RiscvAirId::LtUser,
376            RiscvAirId::UType,
377            RiscvAirId::UTypeUser,
378            RiscvAirId::MemoryLocal,
379            RiscvAirId::MemoryBump,
380            RiscvAirId::StateBump,
381            RiscvAirId::LoadByte,
382            RiscvAirId::LoadByteUser,
383            RiscvAirId::LoadHalf,
384            RiscvAirId::LoadHalfUser,
385            RiscvAirId::LoadWord,
386            RiscvAirId::LoadWordUser,
387            RiscvAirId::LoadDouble,
388            RiscvAirId::LoadDoubleUser,
389            RiscvAirId::LoadX0,
390            RiscvAirId::LoadX0User,
391            RiscvAirId::StoreByte,
392            RiscvAirId::StoreByteUser,
393            RiscvAirId::StoreHalf,
394            RiscvAirId::StoreHalfUser,
395            RiscvAirId::StoreWord,
396            RiscvAirId::StoreWordUser,
397            RiscvAirId::StoreDouble,
398            RiscvAirId::StoreDoubleUser,
399            RiscvAirId::Branch,
400            RiscvAirId::BranchUser,
401            RiscvAirId::Jal,
402            RiscvAirId::JalUser,
403            RiscvAirId::Jalr,
404            RiscvAirId::JalrUser,
405            RiscvAirId::SyscallCore,
406            RiscvAirId::SyscallInstrs,
407            RiscvAirId::SyscallInstrsUser,
408            RiscvAirId::Global,
409            RiscvAirId::AluX0,
410            RiscvAirId::AluX0User,
411            RiscvAirId::Mprotect,
412            RiscvAirId::InstructionDecode,
413            RiscvAirId::InstructionFetch,
414            RiscvAirId::PageProt,
415            RiscvAirId::PageProtLocal,
416            RiscvAirId::TrapExec,
417            RiscvAirId::TrapMem,
418        ]
419    }
420
421    /// Whether the ID represents a core AIR.
422    #[must_use]
423    pub fn is_core(self) -> bool {
424        CoreAirId::try_from(self).is_ok()
425    }
426
427    /// Whether the ID represents a memory AIR.
428    #[must_use]
429    pub fn is_memory(self) -> bool {
430        matches!(
431            self,
432            RiscvAirId::MemoryGlobalInit
433                | RiscvAirId::MemoryGlobalFinalize
434                | RiscvAirId::PageProtGlobalInit
435                | RiscvAirId::PageProtGlobalFinalize
436                | RiscvAirId::Global
437        )
438    }
439
440    /// Whether the ID represents a precompile AIR.
441    #[must_use]
442    pub fn is_precompile(self) -> bool {
443        matches!(
444            self,
445            RiscvAirId::ShaExtend
446                | RiscvAirId::ShaCompress
447                | RiscvAirId::EdAddAssign
448                | RiscvAirId::EdDecompress
449                | RiscvAirId::Secp256k1AddAssign
450                | RiscvAirId::Secp256k1DoubleAssign
451                | RiscvAirId::Secp256r1AddAssign
452                | RiscvAirId::Secp256r1DoubleAssign
453                | RiscvAirId::KeccakPermute
454                | RiscvAirId::Bn254AddAssign
455                | RiscvAirId::Bn254DoubleAssign
456                | RiscvAirId::Bls12381AddAssign
457                | RiscvAirId::Bls12381DoubleAssign
458                | RiscvAirId::Uint256MulMod
459                | RiscvAirId::Uint256Ops
460                | RiscvAirId::Bls12381FpOpAssign
461                | RiscvAirId::Bls12381Fp2AddSubAssign
462                | RiscvAirId::Bls12381Fp2MulAssign
463                | RiscvAirId::Bn254FpOpAssign
464                | RiscvAirId::Bn254Fp2AddSubAssign
465                | RiscvAirId::Bn254Fp2MulAssign
466                | RiscvAirId::Poseidon2
467                | RiscvAirId::SigReturn
468        )
469    }
470
471    /// The number of rows in the AIR produced by each event.
472    #[must_use]
473    pub fn rows_per_event(&self) -> usize {
474        match self {
475            Self::ShaCompress => 80,
476            Self::ShaExtend => 48,
477            Self::KeccakPermute => 24,
478            _ => 1,
479        }
480    }
481
482    /// Get the ID of the AIR used in the syscall control implementation.
483    #[must_use]
484    pub fn control_air_id(self, page_protect_enabled: bool) -> Option<RiscvAirId> {
485        if page_protect_enabled {
486            return match self {
487                RiscvAirId::ShaCompress => Some(RiscvAirId::ShaCompressControlUser),
488                RiscvAirId::ShaExtend => Some(RiscvAirId::ShaExtendControlUser),
489                RiscvAirId::KeccakPermute => Some(RiscvAirId::KeccakPermuteControlUser),
490                _ => None,
491            };
492        }
493        match self {
494            RiscvAirId::ShaCompress => Some(RiscvAirId::ShaCompressControl),
495            RiscvAirId::ShaExtend => Some(RiscvAirId::ShaExtendControl),
496            RiscvAirId::KeccakPermute => Some(RiscvAirId::KeccakPermuteControl),
497            _ => None,
498        }
499    }
500
501    /// Returns the string representation of the AIR.
502    #[must_use]
503    pub fn as_str(&self) -> &'static str {
504        self.into()
505    }
506}
507
508impl FromStr for RiscvAirId {
509    type Err = String;
510
511    fn from_str(s: &str) -> Result<Self, Self::Err> {
512        let air = Self::iter().find(|chip| chip.as_str() == s);
513        match air {
514            Some(air) => Ok(air),
515            None => Err(format!("Invalid RV64IMAir: {s}")),
516        }
517    }
518}
519
520impl Display for RiscvAirId {
521    fn fmt(&self, f: &mut Formatter<'_>) -> FmtResult {
522        write!(f, "{}", self.as_str())
523    }
524}
525
526/// Defines a set of maximal shapes for generating core proofs.
527#[derive(Debug, Clone, Serialize, Deserialize)]
528pub struct MaximalShapes {
529    inner: Vec<EnumMap<CoreAirId, u32>>,
530}
531
532impl FromIterator<Shape<RiscvAirId>> for MaximalShapes {
533    fn from_iter<T: IntoIterator<Item = Shape<RiscvAirId>>>(iter: T) -> Self {
534        let mut maximal_shapes = Vec::new();
535        for shape in iter {
536            let mut maximal_shape = EnumMap::<CoreAirId, u32>::default();
537            for (air, height) in shape {
538                if let Ok(core_air) = CoreAirId::try_from(air) {
539                    maximal_shape[core_air] = height as u32;
540                } else if air != RiscvAirId::Program
541                    && air != RiscvAirId::Byte
542                    && air != RiscvAirId::Range
543                {
544                    tracing::warn!("Invalid core air: {air}");
545                }
546            }
547            maximal_shapes.push(maximal_shape);
548        }
549        Self { inner: maximal_shapes }
550    }
551}
552
553impl MaximalShapes {
554    /// Returns an iterator over the maximal shapes.
555    pub fn iter(&self) -> impl Iterator<Item = &EnumMap<CoreAirId, u32>> {
556        self.inner.iter()
557    }
558}
sp1_core_executor/air.rs

sp1_core_executor/
air.rs
