Skip to main content

openvm_circuit/system/
mod.rs

1use std::sync::Arc;
2
3use derive_more::derive::From;
4use openvm_circuit_derive::{AnyEnum, Executor, MeteredExecutor, PreflightExecutor};
5#[cfg(feature = "aot")]
6use openvm_circuit_derive::{AotExecutor, AotMeteredExecutor};
7use openvm_circuit_primitives::{
8    var_range::{
9        SharedVariableRangeCheckerChip, VariableRangeCheckerAir, VariableRangeCheckerBus,
10        VariableRangeCheckerChip,
11    },
12    Chip,
13};
14use openvm_cpu_backend::{CpuBackend, CpuDevice};
15use openvm_instructions::{LocalOpcode, PhantomDiscriminant, SysPhantom, SystemOpcode};
16use openvm_stark_backend::{
17    interaction::{LookupBus, PermutationCheckBus},
18    p3_field::{Field, PrimeField32},
19    prover::{AirProvingContext, CommittedTraceData, ProverBackend},
20    StarkEngine, StarkProtocolConfig, Val,
21};
22use rustc_hash::FxHashMap;
23
24use self::{connector::VmConnectorAir, program::ProgramAir};
25use crate::{
26    arch::{
27        vm_poseidon2_config, AirInventory, AirInventoryError, AirRefWithColumns, BusIndexManager,
28        ChipInventory, ChipInventoryError, ExecutionBridge, ExecutionBus, ExecutionState,
29        ExecutorInventory, ExecutorInventoryError, MatrixRecordArena, PhantomSubExecutor,
30        RowMajorMatrixArena, SystemConfig, VmBuilder, VmChipComplex, VmCircuitConfig,
31        VmExecutionConfig, VmField, BOUNDARY_AIR_ID, CONNECTOR_AIR_ID, DEFAULT_BLOCK_SIZE,
32        PROGRAM_AIR_ID,
33    },
34    system::{
35        connector::VmConnectorChip,
36        memory::{
37            offline_checker::{MemoryBridge, MemoryBus},
38            online::GuestMemory,
39            MemoryAirInventory, MemoryController, TimestampedEquipartition, CHUNK,
40        },
41        phantom::{
42            CycleEndPhantomExecutor, CycleStartPhantomExecutor, NopPhantomExecutor, PhantomAir,
43            PhantomChip, PhantomExecutor, PhantomFiller,
44        },
45        poseidon2::{
46            air::Poseidon2PeripheryAir, new_poseidon2_periphery_air, Poseidon2PeripheryChip,
47        },
48        program::{ProgramBus, ProgramChip},
49    },
50};
51
52pub mod connector;
53#[cfg(feature = "cuda")]
54pub mod cuda;
55pub mod memory;
56pub mod phantom;
57pub mod poseidon2;
58pub mod program;
59
60/// **If** internal poseidon2 chip exists, then its insertion index is 1.
61const POSEIDON2_INSERTION_IDX: usize = 1;
62
63/// Trait for trace generation of all system AIRs. The system chip complex is special because we may
64/// not exactly following the exact matching between `Air` and `Chip`. Moreover we may require more
65/// flexibility than what is provided through the trait object
66/// [`AnyChip`](openvm_circuit_primitives::AnyChip).
67///
68/// The [SystemChipComplex] is meant to be constructible once the VM configuration is known, and it
69/// can be loaded with arbitrary programs supported by the instruction set available to its
70/// configuration. The [SystemChipComplex] is meant to persist between instances of proof
71/// generation.
72pub trait SystemChipComplex<RA, PB: ProverBackend> {
73    /// Loads the program in the form of a cached trace with prover data.
74    fn load_program(&mut self, cached_program_trace: CommittedTraceData<PB>);
75
76    /// Transport the initial memory state to device. This may be called before preflight execution
77    /// begins and start async device processes in parallel to execution.
78    fn transport_init_memory_to_device(&mut self, memory: &GuestMemory);
79
80    /// The caller must guarantee that `record_arenas` has length equal to the number of system
81    /// AIRs, although some arenas may be empty if they are unused.
82    fn generate_proving_ctx(
83        &mut self,
84        system_records: SystemRecords<PB::Val>,
85        record_arenas: Vec<RA>,
86    ) -> Vec<AirProvingContext<PB>>;
87
88    /// Returns the top merkle sub-tree of the memory merkle tree
89    /// as a segment tree with `2 * (2^addr_space_height) - 1` nodes, representing the Merkle
90    /// tree formed from the roots of the sub-trees for each address space.
91    ///
92    /// This function **must** return `Some` if called after
93    /// [`generate_proving_ctx`](Self::generate_proving_ctx) and may return `None` if called before
94    /// that.
95    fn memory_top_tree(&self) -> Option<&[[PB::Val; CHUNK]]>;
96}
97
98/// Trait meant to be implemented on a SystemChipComplex.
99pub trait SystemWithFixedTraceHeights {
100    /// `heights` will have length equal to number of system AIRs, in AIR ID order. This function
101    /// must guarantee that the system trace matrices generated have the required heights.
102    fn override_trace_heights(&mut self, heights: &[u32]);
103}
104
105pub struct SystemRecords<F> {
106    pub from_state: ExecutionState<u32>,
107    pub to_state: ExecutionState<u32>,
108    pub exit_code: Option<u32>,
109    /// `i` -> frequency of instruction in `i`th row of trace matrix. This requires filtering
110    /// `program.instructions_and_debug_infos` to remove gaps.
111    pub filtered_exec_frequencies: Vec<u32>,
112    // Perf[jpw]: this should be computed on-device and changed to just touched blocks
113    pub touched_memory: TouchedMemory<F>,
114}
115
116pub type TouchedMemory<F> = TimestampedEquipartition<F, DEFAULT_BLOCK_SIZE>;
117
118#[derive(Clone, AnyEnum, Executor, MeteredExecutor, PreflightExecutor, From)]
119#[cfg_attr(feature = "aot", derive(AotExecutor, AotMeteredExecutor))]
120pub enum SystemExecutor<F: Field> {
121    Phantom(PhantomExecutor<F>),
122}
123
124/// SystemPort combines system resources needed by most extensions
125#[derive(Clone, Copy)]
126pub struct SystemPort {
127    pub execution_bus: ExecutionBus,
128    pub program_bus: ProgramBus,
129    pub memory_bridge: MemoryBridge,
130}
131
132#[derive(Clone)]
133pub struct SystemAirInventory {
134    pub program: ProgramAir,
135    pub connector: VmConnectorAir,
136    pub memory: MemoryAirInventory,
137}
138
139impl SystemAirInventory {
140    pub fn new(
141        config: &SystemConfig,
142        port: SystemPort,
143        merkle_bus: PermutationCheckBus,
144        compression_bus: PermutationCheckBus,
145    ) -> Self {
146        let SystemPort {
147            execution_bus,
148            program_bus,
149            memory_bridge,
150        } = port;
151        let range_bus = memory_bridge.range_bus();
152        let program = ProgramAir::new(program_bus);
153        let connector = VmConnectorAir::new(
154            execution_bus,
155            program_bus,
156            range_bus,
157            config.memory_config.timestamp_max_bits,
158        );
159        let memory = MemoryAirInventory::new(
160            memory_bridge,
161            &config.memory_config,
162            merkle_bus,
163            compression_bus,
164        );
165
166        Self {
167            program,
168            connector,
169            memory,
170        }
171    }
172
173    pub fn port(&self) -> SystemPort {
174        SystemPort {
175            memory_bridge: self.memory.bridge,
176            program_bus: self.program.bus,
177            execution_bus: self.connector.execution_bus,
178        }
179    }
180
181    pub fn into_airs<SC: StarkProtocolConfig>(self) -> Vec<AirRefWithColumns<SC>> {
182        let mut airs: Vec<AirRefWithColumns<SC>> = Vec::new();
183        airs.push(Arc::new(self.program));
184        airs.push(Arc::new(self.connector));
185        airs.extend(self.memory.into_airs());
186        airs
187    }
188}
189
190impl<F: PrimeField32> VmExecutionConfig<F> for SystemConfig {
191    type Executor = SystemExecutor<F>;
192
193    /// The only way to create an [ExecutorInventory] is from a [SystemConfig]. This will always
194    /// add an executor for [PhantomChip], which handles all phantom sub-executors.
195    fn create_executors(
196        &self,
197    ) -> Result<ExecutorInventory<Self::Executor>, ExecutorInventoryError> {
198        let mut inventory = ExecutorInventory::new(self.clone());
199        let phantom_opcode = SystemOpcode::PHANTOM.global_opcode();
200        let mut phantom_executors: FxHashMap<PhantomDiscriminant, Arc<dyn PhantomSubExecutor<F>>> =
201            FxHashMap::default();
202        // Use NopPhantomExecutor so the discriminant is set but `DebugPanic` is handled specially.
203        phantom_executors.insert(
204            PhantomDiscriminant(SysPhantom::DebugPanic as u16),
205            Arc::new(NopPhantomExecutor),
206        );
207        phantom_executors.insert(
208            PhantomDiscriminant(SysPhantom::Nop as u16),
209            Arc::new(NopPhantomExecutor),
210        );
211        phantom_executors.insert(
212            PhantomDiscriminant(SysPhantom::CtStart as u16),
213            Arc::new(CycleStartPhantomExecutor),
214        );
215        phantom_executors.insert(
216            PhantomDiscriminant(SysPhantom::CtEnd as u16),
217            Arc::new(CycleEndPhantomExecutor),
218        );
219        let phantom = PhantomExecutor::new(phantom_executors, phantom_opcode);
220        inventory.add_executor(phantom, [phantom_opcode])?;
221
222        Ok(inventory)
223    }
224}
225
226impl<SC> VmCircuitConfig<SC> for SystemConfig
227where
228    SC: StarkProtocolConfig,
229    Val<SC>: VmField,
230{
231    /// Every VM circuit within the OpenVM circuit architecture **must** be initialized from the
232    /// [SystemConfig].
233    fn create_airs(&self) -> Result<AirInventory<SC>, AirInventoryError> {
234        let mut bus_idx_mgr = BusIndexManager::new();
235        let execution_bus = ExecutionBus::new(bus_idx_mgr.new_bus_idx());
236        let memory_bus = MemoryBus::new(bus_idx_mgr.new_bus_idx());
237        let program_bus = ProgramBus::new(bus_idx_mgr.new_bus_idx());
238        let range_bus =
239            VariableRangeCheckerBus::new(bus_idx_mgr.new_bus_idx(), self.memory_config.decomp);
240
241        let merkle_bus = PermutationCheckBus::new(bus_idx_mgr.new_bus_idx());
242        let compression_bus = PermutationCheckBus::new(bus_idx_mgr.new_bus_idx());
243        let direct_bus_idx = compression_bus.index;
244        let memory_bridge =
245            MemoryBridge::new(memory_bus, self.memory_config.timestamp_max_bits, range_bus);
246        let system_port = SystemPort {
247            execution_bus,
248            program_bus,
249            memory_bridge,
250        };
251        let system = SystemAirInventory::new(self, system_port, merkle_bus, compression_bus);
252
253        let mut inventory = AirInventory::new(self.clone(), system, bus_idx_mgr);
254
255        let range_checker = VariableRangeCheckerAir::new(range_bus);
256        // Range checker is always the first AIR in the inventory
257        inventory.add_air(range_checker);
258
259        assert_eq!(inventory.ext_airs().len(), POSEIDON2_INSERTION_IDX);
260        // Add direct poseidon2 AIR for memory merkle tree.
261        // Currently we never use poseidon2 opcodes directly: we will need
262        // special handling when that happens
263        let air = new_poseidon2_periphery_air(
264            vm_poseidon2_config(),
265            LookupBus::new(direct_bus_idx),
266            self.max_constraint_degree,
267        );
268        inventory.add_air_ref(air);
269        let execution_bridge = ExecutionBridge::new(execution_bus, program_bus);
270        let phantom = PhantomAir {
271            execution_bridge,
272            phantom_opcode: SystemOpcode::PHANTOM.global_opcode(),
273        };
274        inventory.add_air(phantom);
275
276        Ok(inventory)
277    }
278}
279
280// =================== CPU Backend Specific System Chip Complex Constructor ==================
281
282/// Base system chips for CPU backend. These chips must exactly correspond to the AIRs in
283/// [SystemAirInventory].
284pub struct SystemChipInventory<SC: StarkProtocolConfig>
285where
286    Val<SC>: VmField,
287{
288    pub program_chip: ProgramChip<SC>,
289    pub connector_chip: VmConnectorChip<Val<SC>>,
290    /// Contains all memory chips
291    pub memory_controller: MemoryController<Val<SC>>,
292}
293
294// Note[jpw]: We could get rid of the `mem_inventory` input because `MemoryController` doesn't need
295// the buses for tracegen. We leave it to use old interfaces.
296impl<SC: StarkProtocolConfig> SystemChipInventory<SC>
297where
298    Val<SC>: VmField,
299{
300    pub fn new(
301        config: &SystemConfig,
302        mem_inventory: &MemoryAirInventory,
303        range_checker: SharedVariableRangeCheckerChip,
304        hasher_chip: Arc<Poseidon2PeripheryChip<Val<SC>>>,
305    ) -> Self {
306        // We create an empty program chip: the program should be loaded later (and can be swapped
307        // out). The execution frequencies are supplied only after execution.
308        let program_chip = ProgramChip::unloaded();
309        let connector_chip = VmConnectorChip::<Val<SC>>::new(
310            range_checker.clone(),
311            config.memory_config.timestamp_max_bits,
312        );
313        let memory_bus = mem_inventory.bridge.memory_bus();
314        let memory_controller = MemoryController::<Val<SC>>::with_persistent_memory(
315            memory_bus,
316            config.memory_config.clone(),
317            range_checker.clone(),
318            mem_inventory.interface.merkle.merkle_bus,
319            mem_inventory.interface.merkle.compression_bus,
320            hasher_chip,
321        );
322
323        Self {
324            program_chip,
325            connector_chip,
326            memory_controller,
327        }
328    }
329}
330
331impl<RA, SC> SystemChipComplex<RA, CpuBackend<SC>> for SystemChipInventory<SC>
332where
333    RA: RowMajorMatrixArena<Val<SC>>,
334    SC: StarkProtocolConfig,
335    Val<SC>: VmField,
336{
337    fn load_program(&mut self, cached_program_trace: CommittedTraceData<CpuBackend<SC>>) {
338        let _ = self.program_chip.cached.replace(cached_program_trace);
339    }
340
341    fn transport_init_memory_to_device(&mut self, memory: &GuestMemory) {
342        self.memory_controller
343            .set_initial_memory(memory.memory.clone());
344    }
345
346    fn generate_proving_ctx(
347        &mut self,
348        system_records: SystemRecords<Val<SC>>,
349        _record_arenas: Vec<RA>,
350    ) -> Vec<AirProvingContext<CpuBackend<SC>>> {
351        let SystemRecords {
352            from_state,
353            to_state,
354            exit_code,
355            filtered_exec_frequencies,
356            touched_memory,
357        } = system_records;
358
359        self.program_chip.filtered_exec_frequencies = filtered_exec_frequencies;
360        let program_ctx = self.program_chip.generate_proving_ctx(());
361        self.connector_chip.begin(from_state);
362        self.connector_chip.end(to_state, exit_code);
363        let connector_ctx = self.connector_chip.generate_proving_ctx(());
364
365        let memory_ctxs = self.memory_controller.generate_proving_ctx(touched_memory);
366
367        [program_ctx, connector_ctx]
368            .into_iter()
369            .chain(memory_ctxs)
370            .collect()
371    }
372
373    fn memory_top_tree(&self) -> Option<&[[Val<SC>; CHUNK]]> {
374        let top_tree = &self.memory_controller.interface_chip.merkle_chip.top_tree;
375        (!top_tree.is_empty()).then_some(top_tree.as_slice())
376    }
377}
378
379#[derive(Clone)]
380pub struct SystemCpuBuilder;
381
382impl<SC, E> VmBuilder<E> for SystemCpuBuilder
383where
384    SC: StarkProtocolConfig,
385    E: StarkEngine<SC = SC, PB = CpuBackend<SC>, PD = CpuDevice<SC>>,
386    Val<SC>: VmField,
387    SC::EF: Ord,
388{
389    type VmConfig = SystemConfig;
390    type RecordArena = MatrixRecordArena<Val<SC>>;
391    type SystemChipInventory = SystemChipInventory<SC>;
392
393    fn create_chip_complex(
394        &self,
395        config: &SystemConfig,
396        airs: AirInventory<SC>,
397        _device_ctx: &openvm_stark_backend::EngineDeviceCtx<E>,
398    ) -> Result<
399        VmChipComplex<SC, MatrixRecordArena<Val<SC>>, CpuBackend<SC>, SystemChipInventory<SC>>,
400        ChipInventoryError,
401    > {
402        let range_bus = airs.range_checker().bus;
403        let range_checker = Arc::new(VariableRangeCheckerChip::new(range_bus));
404
405        let mut inventory = ChipInventory::new(airs);
406        inventory.next_air::<VariableRangeCheckerAir>()?;
407        inventory.add_periphery_chip(range_checker.clone());
408
409        assert_eq!(inventory.chips().len(), POSEIDON2_INSERTION_IDX);
410        // ATTENTION: The threshold 7 here must match the one in `new_poseidon2_periphery_air`
411        if config.max_constraint_degree >= 7 {
412            inventory.next_air::<Poseidon2PeripheryAir<Val<SC>, 0>>()?;
413        } else {
414            inventory.next_air::<Poseidon2PeripheryAir<Val<SC>, 1>>()?;
415        };
416        let hasher_chip = Arc::new(Poseidon2PeripheryChip::new(
417            vm_poseidon2_config(),
418            config.max_constraint_degree,
419        ));
420        inventory.add_periphery_chip(hasher_chip.clone());
421        let system = SystemChipInventory::new(
422            config,
423            &inventory.airs().system().memory,
424            range_checker,
425            hasher_chip,
426        );
427
428        let phantom_chip = PhantomChip::new(PhantomFiller, system.memory_controller.helper());
429        inventory.add_executor_chip(phantom_chip);
430
431        Ok(VmChipComplex { system, inventory })
432    }
433}
434
435impl<SC: StarkProtocolConfig> SystemWithFixedTraceHeights for SystemChipInventory<SC>
436where
437    Val<SC>: VmField,
438{
439    /// Warning: this does not set the override for the program chip. The program chip
440    /// override must be set via the RecordArena.
441    fn override_trace_heights(&mut self, heights: &[u32]) {
442        assert_eq!(
443            heights[PROGRAM_AIR_ID] as usize,
444            self.program_chip
445                .cached
446                .as_ref()
447                .expect("program not loaded")
448                .height()
449        );
450        assert_eq!(heights[CONNECTOR_AIR_ID], 2);
451        self.memory_controller
452            .set_override_trace_heights(&heights[BOUNDARY_AIR_ID..]);
453    }
454}