1use std::{
10 any::TypeId,
11 borrow::Borrow,
12 collections::{HashMap, VecDeque},
13 marker::PhantomData,
14 sync::Arc,
15};
16
17use getset::{Getters, MutGetters, Setters, WithSetters};
18use itertools::{zip_eq, Itertools};
19use openvm_circuit::system::program::trace::compute_exe_commit;
20use openvm_instructions::{
21 exe::{SparseMemoryImage, VmExe},
22 program::Program,
23};
24use openvm_stark_backend::{
25 config::{Com, StarkGenericConfig, Val},
26 engine::StarkEngine,
27 keygen::types::{MultiStarkProvingKey, MultiStarkVerifyingKey},
28 p3_field::{FieldAlgebra, FieldExtensionAlgebra, PrimeField32, TwoAdicField},
29 p3_util::{log2_ceil_usize, log2_strict_usize},
30 proof::Proof,
31 prover::{
32 hal::{DeviceDataTransporter, MatrixDimensions, TraceCommitter},
33 types::{CommittedTraceData, DeviceMultiStarkProvingKey, ProvingContext},
34 },
35 verifier::VerificationError,
36};
37use p3_baby_bear::BabyBear;
38use serde::{Deserialize, Serialize};
39use thiserror::Error;
40use tracing::{info_span, instrument};
41
42use super::{
43 execution_mode::{ExecutionCtx, MeteredCostCtx, MeteredCtx, PreflightCtx, Segment},
44 hasher::poseidon2::vm_poseidon2_hasher,
45 interpreter::InterpretedInstance,
46 interpreter_preflight::PreflightInterpretedInstance,
47 AirInventoryError, ChipInventoryError, ExecutionError, ExecutionState, Executor,
48 ExecutorInventory, ExecutorInventoryError, MemoryConfig, MeteredExecutor, PreflightExecutor,
49 StaticProgramError, SystemConfig, VmBuilder, VmChipComplex, VmCircuitConfig, VmExecState,
50 VmExecutionConfig, VmState, CONNECTOR_AIR_ID, MERKLE_AIR_ID, PROGRAM_AIR_ID,
51 PROGRAM_CACHED_TRACE_INDEX, PUBLIC_VALUES_AIR_ID,
52};
53use crate::{
54 arch::DEFAULT_RNG_SEED,
55 execute_spanned,
56 system::{
57 connector::{VmConnectorPvs, DEFAULT_SUSPEND_EXIT_CODE},
58 memory::{
59 adapter::records,
60 merkle::{
61 public_values::{UserPublicValuesProof, UserPublicValuesProofError},
62 MemoryMerklePvs,
63 },
64 online::{GuestMemory, TracingMemory},
65 AddressMap, CHUNK,
66 },
67 program::trace::{generate_cached_trace, VmCommittedExe},
68 SystemChipComplex, SystemRecords, SystemWithFixedTraceHeights,
69 },
70};
71
72#[derive(Error, Debug)]
73pub enum GenerationError {
74 #[error("unexpected number of arenas: {actual} (expected num_airs={expected})")]
75 UnexpectedNumArenas { actual: usize, expected: usize },
76 #[error("trace height for air_idx={air_idx} must be fixed to {expected}, actual={actual}")]
77 ForceTraceHeightIncorrect {
78 air_idx: usize,
79 actual: usize,
80 expected: usize,
81 },
82 #[error("trace height of air {air_idx} has height {height} greater than maximum {max_height}")]
83 TraceHeightsLimitExceeded {
84 air_idx: usize,
85 height: usize,
86 max_height: usize,
87 },
88 #[error("trace heights violate linear constraint {constraint_idx} ({value} >= {threshold})")]
89 LinearTraceHeightConstraintExceeded {
90 constraint_idx: usize,
91 value: u64,
92 threshold: u32,
93 },
94}
95
96pub trait KvStore: Send + Sync {
98 fn get(&self, key: &[u8]) -> Option<&[u8]>;
99}
100
101impl KvStore for HashMap<Vec<u8>, Vec<u8>> {
102 fn get(&self, key: &[u8]) -> Option<&[u8]> {
103 self.get(key).map(|v| v.as_slice())
104 }
105}
106
107#[derive(Clone)]
108pub struct Streams<F> {
109 pub input_stream: VecDeque<Vec<F>>,
110 pub hint_stream: VecDeque<F>,
111 pub hint_space: Vec<Vec<F>>,
112 pub kv_store: Arc<dyn KvStore>,
115}
116
117impl<F> Streams<F> {
118 pub fn new(input_stream: impl Into<VecDeque<Vec<F>>>) -> Self {
119 Self {
120 input_stream: input_stream.into(),
121 hint_stream: VecDeque::default(),
122 hint_space: Vec::default(),
123 kv_store: Arc::new(HashMap::new()),
124 }
125 }
126}
127
128impl<F> Default for Streams<F> {
129 fn default() -> Self {
130 Self::new(VecDeque::default())
131 }
132}
133
134impl<F> From<VecDeque<Vec<F>>> for Streams<F> {
135 fn from(value: VecDeque<Vec<F>>) -> Self {
136 Streams::new(value)
137 }
138}
139
140impl<F> From<Vec<Vec<F>>> for Streams<F> {
141 fn from(value: Vec<Vec<F>>) -> Self {
142 Streams::new(value)
143 }
144}
145
146type PreflightInterpretedInstance2<F, VC> =
148 PreflightInterpretedInstance<F, <VC as VmExecutionConfig<F>>::Executor>;
149
150#[derive(Clone)]
156pub struct VmExecutor<F, VC>
157where
158 VC: VmExecutionConfig<F>,
159{
160 pub config: VC,
161 inventory: Arc<ExecutorInventory<VC::Executor>>,
162 phantom: PhantomData<F>,
163}
164
165#[repr(i32)]
166pub enum ExitCode {
167 Success = 0,
168 Error = 1,
169 Suspended = -1, }
171
172pub struct PreflightExecutionOutput<F, RA> {
173 pub system_records: SystemRecords<F>,
174 pub record_arenas: Vec<RA>,
175 pub to_state: VmState<F, GuestMemory>,
176}
177
178impl<F, VC> VmExecutor<F, VC>
179where
180 VC: VmExecutionConfig<F>,
181{
182 pub fn new(config: VC) -> Result<Self, ExecutorInventoryError> {
186 let inventory = config.create_executors()?;
187 Ok(Self {
188 config,
189 inventory: Arc::new(inventory),
190 phantom: PhantomData,
191 })
192 }
193}
194
195impl<F, VC> VmExecutor<F, VC>
196where
197 VC: VmExecutionConfig<F> + AsRef<SystemConfig>,
198{
199 pub fn build_metered_ctx(
200 &self,
201 constant_trace_heights: &[Option<usize>],
202 air_names: &[String],
203 widths: &[usize],
204 interactions: &[usize],
205 ) -> MeteredCtx {
206 MeteredCtx::new(
207 constant_trace_heights.to_vec(),
208 air_names.to_vec(),
209 widths.to_vec(),
210 interactions.to_vec(),
211 self.config.as_ref(),
212 )
213 }
214
215 pub fn build_metered_cost_ctx(&self, widths: &[usize]) -> MeteredCostCtx {
216 MeteredCostCtx::new(widths.to_vec(), self.config.as_ref())
217 }
218}
219
220impl<F, VC> VmExecutor<F, VC>
221where
222 F: PrimeField32,
223 VC: VmExecutionConfig<F>,
224 VC::Executor: Executor<F>,
225{
226 pub fn instance(
231 &self,
232 exe: &VmExe<F>,
233 ) -> Result<InterpretedInstance<F, ExecutionCtx>, StaticProgramError> {
234 InterpretedInstance::new(&self.inventory, exe)
235 }
236}
237
238impl<F, VC> VmExecutor<F, VC>
239where
240 F: PrimeField32,
241 VC: VmExecutionConfig<F>,
242 VC::Executor: MeteredExecutor<F>,
243{
244 pub fn metered_instance(
246 &self,
247 exe: &VmExe<F>,
248 executor_idx_to_air_idx: &[usize],
249 ) -> Result<InterpretedInstance<F, MeteredCtx>, StaticProgramError> {
250 InterpretedInstance::new_metered(&self.inventory, exe, executor_idx_to_air_idx)
251 }
252
253 pub fn metered_cost_instance(
256 &self,
257 exe: &VmExe<F>,
258 executor_idx_to_air_idx: &[usize],
259 ) -> Result<InterpretedInstance<F, MeteredCostCtx>, StaticProgramError> {
260 InterpretedInstance::new_metered(&self.inventory, exe, executor_idx_to_air_idx)
261 }
262}
263
264#[derive(Error, Debug)]
265pub enum VmVerificationError {
266 #[error("no proof is provided")]
267 ProofNotFound,
268
269 #[error("program commit mismatch (index of mismatch proof: {index}")]
270 ProgramCommitMismatch { index: usize },
271
272 #[error("exe commit mismatch (expected: {expected:?}, actual: {actual:?})")]
273 ExeCommitMismatch {
274 expected: [u32; CHUNK],
275 actual: [u32; CHUNK],
276 },
277
278 #[error("initial pc mismatch (initial: {initial}, prev_final: {prev_final})")]
279 InitialPcMismatch { initial: u32, prev_final: u32 },
280
281 #[error("initial memory root mismatch")]
282 InitialMemoryRootMismatch,
283
284 #[error("is terminate mismatch (expected: {expected}, actual: {actual})")]
285 IsTerminateMismatch { expected: bool, actual: bool },
286
287 #[error("exit code mismatch")]
288 ExitCodeMismatch { expected: u32, actual: u32 },
289
290 #[error("AIR has unexpected public values (expected: {expected}, actual: {actual})")]
291 UnexpectedPvs { expected: usize, actual: usize },
292
293 #[error("Invalid number of AIRs: expected at least 3, got {0}")]
294 NotEnoughAirs(usize),
295
296 #[error("missing system AIR with ID {air_id}")]
297 SystemAirMissing { air_id: usize },
298
299 #[error("stark verification error: {0}")]
300 StarkError(#[from] VerificationError),
301
302 #[error("user public values proof error: {0}")]
303 UserPublicValuesError(#[from] UserPublicValuesProofError),
304}
305
306#[derive(Error, Debug)]
307pub enum VirtualMachineError {
308 #[error("executor inventory error: {0}")]
309 ExecutorInventory(#[from] ExecutorInventoryError),
310 #[error("air inventory error: {0}")]
311 AirInventory(#[from] AirInventoryError),
312 #[error("chip inventory error: {0}")]
313 ChipInventory(#[from] ChipInventoryError),
314 #[error("static program error: {0}")]
315 StaticProgram(#[from] StaticProgramError),
316 #[error("execution error: {0}")]
317 Execution(#[from] ExecutionError),
318 #[error("trace generation error: {0}")]
319 Generation(#[from] GenerationError),
320 #[error("program committed trade data not loaded")]
321 ProgramIsNotCommitted,
322 #[error("verification error: {0}")]
323 Verification(#[from] VmVerificationError),
324}
325
326#[derive(Getters, MutGetters, Setters, WithSetters)]
334pub struct VirtualMachine<E, VB>
335where
336 E: StarkEngine,
337 VB: VmBuilder<E>,
338{
339 pub engine: E,
341 #[getset(get = "pub")]
343 executor: VmExecutor<Val<E::SC>, VB::VmConfig>,
344 #[getset(get = "pub", get_mut = "pub")]
345 pk: DeviceMultiStarkProvingKey<E::PB>,
346 chip_complex: VmChipComplex<E::SC, VB::RecordArena, E::PB, VB::SystemChipInventory>,
347 #[cfg(feature = "stark-debug")]
348 pub h_pk: Option<MultiStarkProvingKey<E::SC>>,
349}
350
351impl<E, VB> VirtualMachine<E, VB>
352where
353 E: StarkEngine,
354 VB: VmBuilder<E>,
355{
356 pub fn new(
357 engine: E,
358 builder: VB,
359 config: VB::VmConfig,
360 d_pk: DeviceMultiStarkProvingKey<E::PB>,
361 ) -> Result<Self, VirtualMachineError> {
362 let circuit = config.create_airs()?;
363 let chip_complex = builder.create_chip_complex(&config, circuit)?;
364 let executor = VmExecutor::<Val<E::SC>, _>::new(config)?;
365 Ok(Self {
366 engine,
367 executor,
368 pk: d_pk,
369 chip_complex,
370 #[cfg(feature = "stark-debug")]
371 h_pk: None,
372 })
373 }
374
375 pub fn new_with_keygen(
376 engine: E,
377 builder: VB,
378 config: VB::VmConfig,
379 ) -> Result<(Self, MultiStarkProvingKey<E::SC>), VirtualMachineError> {
380 let circuit = config.create_airs()?;
381 let pk = circuit.keygen(&engine);
382 let d_pk = engine.device().transport_pk_to_device(&pk);
383 let vm = Self::new(engine, builder, config, d_pk)?;
384 Ok((vm, pk))
385 }
386
387 pub fn config(&self) -> &VB::VmConfig {
388 &self.executor.config
389 }
390
391 pub fn interpreter(
393 &self,
394 exe: &VmExe<Val<E::SC>>,
395 ) -> Result<InterpretedInstance<Val<E::SC>, ExecutionCtx>, StaticProgramError>
396 where
397 Val<E::SC>: PrimeField32,
398 <VB::VmConfig as VmExecutionConfig<Val<E::SC>>>::Executor: Executor<Val<E::SC>>,
399 {
400 self.executor().instance(exe)
401 }
402
403 pub fn metered_interpreter(
404 &self,
405 exe: &VmExe<Val<E::SC>>,
406 ) -> Result<InterpretedInstance<Val<E::SC>, MeteredCtx>, StaticProgramError>
407 where
408 Val<E::SC>: PrimeField32,
409 <VB::VmConfig as VmExecutionConfig<Val<E::SC>>>::Executor: MeteredExecutor<Val<E::SC>>,
410 {
411 let executor_idx_to_air_idx = self.executor_idx_to_air_idx();
412 self.executor()
413 .metered_instance(exe, &executor_idx_to_air_idx)
414 }
415
416 pub fn metered_cost_interpreter(
417 &self,
418 exe: &VmExe<Val<E::SC>>,
419 ) -> Result<InterpretedInstance<Val<E::SC>, MeteredCostCtx>, StaticProgramError>
420 where
421 Val<E::SC>: PrimeField32,
422 <VB::VmConfig as VmExecutionConfig<Val<E::SC>>>::Executor: MeteredExecutor<Val<E::SC>>,
423 {
424 let executor_idx_to_air_idx = self.executor_idx_to_air_idx();
425 self.executor()
426 .metered_cost_instance(exe, &executor_idx_to_air_idx)
427 }
428
429 pub fn preflight_interpreter(
430 &self,
431 exe: &VmExe<Val<E::SC>>,
432 ) -> Result<PreflightInterpretedInstance2<Val<E::SC>, VB::VmConfig>, StaticProgramError> {
433 PreflightInterpretedInstance::new(
434 &exe.program,
435 self.executor.inventory.clone(),
436 self.executor_idx_to_air_idx(),
437 )
438 }
439
440 #[instrument(name = "execute_preflight", skip_all)]
448 pub fn execute_preflight(
449 &self,
450 interpreter: &mut PreflightInterpretedInstance2<Val<E::SC>, VB::VmConfig>,
451 state: VmState<Val<E::SC>, GuestMemory>,
452 num_insns: Option<u64>,
453 trace_heights: &[u32],
454 ) -> Result<PreflightExecutionOutput<Val<E::SC>, VB::RecordArena>, ExecutionError>
455 where
456 Val<E::SC>: PrimeField32,
457 <VB::VmConfig as VmExecutionConfig<Val<E::SC>>>::Executor:
458 PreflightExecutor<Val<E::SC>, VB::RecordArena>,
459 {
460 debug_assert!(interpreter
461 .executor_idx_to_air_idx
462 .iter()
463 .all(|&air_idx| air_idx < trace_heights.len()));
464
465 let instret_end = num_insns.map(|ni| state.instret.saturating_add(ni));
466 let main_widths = self
468 .pk
469 .per_air
470 .iter()
471 .map(|pk| pk.vk.params.width.main_width())
472 .collect_vec();
473 let capacities = zip_eq(trace_heights, main_widths)
474 .map(|(&h, w)| (h as usize, w))
475 .collect::<Vec<_>>();
476 let ctx = PreflightCtx::new_with_capacity(&capacities, instret_end);
477
478 let system_config: &SystemConfig = self.config().as_ref();
479 let adapter_offset = system_config.access_adapter_air_id_offset();
480 let num_adapters = log2_strict_usize(system_config.memory_config.max_access_adapter_n);
482 assert_eq!(adapter_offset + num_adapters, system_config.num_airs());
483 let access_adapter_arena_size_bound = records::arena_size_bound(
484 &trace_heights[adapter_offset..adapter_offset + num_adapters],
485 );
486 let memory = TracingMemory::from_image(
487 state.memory,
488 system_config.initial_block_size(),
489 access_adapter_arena_size_bound,
490 );
491 let from_state = ExecutionState::new(state.pc, memory.timestamp());
492 let vm_state = VmState {
493 instret: state.instret,
494 pc: state.pc,
495 memory,
496 streams: state.streams,
497 rng: state.rng,
498 custom_pvs: state.custom_pvs,
499 #[cfg(feature = "metrics")]
500 metrics: state.metrics,
501 };
502 let mut exec_state = VmExecState::new(vm_state, ctx);
503 interpreter.reset_execution_frequencies();
504 execute_spanned!("execute_preflight", interpreter, &mut exec_state)?;
505 let filtered_exec_frequencies = interpreter.filtered_execution_frequencies();
506 let touched_memory = exec_state
507 .vm_state
508 .memory
509 .finalize::<Val<E::SC>>(system_config.continuation_enabled);
510 #[cfg(feature = "perf-metrics")]
511 crate::metrics::end_segment_metrics(&mut exec_state);
512
513 let memory = exec_state.vm_state.memory;
514 let to_state = ExecutionState::new(exec_state.vm_state.pc, memory.timestamp());
515 let public_values = exec_state
516 .vm_state
517 .custom_pvs
518 .iter()
519 .map(|&x| x.unwrap_or(Val::<E::SC>::ZERO))
520 .collect();
521 let exit_code = exec_state.exit_code?;
522 let system_records = SystemRecords {
523 from_state,
524 to_state,
525 exit_code,
526 filtered_exec_frequencies,
527 access_adapter_records: memory.access_adapter_records,
528 touched_memory,
529 public_values,
530 };
531 let record_arenas = exec_state.ctx.arenas;
532 let to_state = VmState {
533 instret: exec_state.vm_state.instret,
534 pc: exec_state.vm_state.pc,
535 memory: memory.data,
536 streams: exec_state.vm_state.streams,
537 rng: exec_state.vm_state.rng,
538 custom_pvs: exec_state.vm_state.custom_pvs,
539 #[cfg(feature = "metrics")]
540 metrics: exec_state.vm_state.metrics,
541 };
542 Ok(PreflightExecutionOutput {
543 system_records,
544 record_arenas,
545 to_state,
546 })
547 }
548
549 #[instrument(name = "vm.create_initial_state", level = "debug", skip_all)]
552 pub fn create_initial_state(
553 &self,
554 exe: &VmExe<Val<E::SC>>,
555 inputs: impl Into<Streams<Val<E::SC>>>,
556 ) -> VmState<Val<E::SC>, GuestMemory> {
557 #[allow(unused_mut)]
558 let mut state = VmState::initial(
559 self.config().as_ref(),
560 &exe.init_memory,
561 exe.pc_start,
562 inputs,
563 );
564 #[cfg(all(feature = "metrics", any(feature = "perf-metrics", debug_assertions)))]
568 {
569 state.metrics.fn_bounds = exe.fn_bounds.clone();
570 state.metrics.debug_infos = exe.program.debug_infos();
571 }
572 #[cfg(feature = "perf-metrics")]
573 {
574 state.metrics.set_pk_info(&self.pk);
575 state.metrics.num_sys_airs = self.config().as_ref().num_airs();
576 state.metrics.access_adapter_offset =
577 self.config().as_ref().access_adapter_air_id_offset();
578 }
579 state
580 }
581
582 #[instrument(name = "trace_gen", skip_all)]
588 pub fn generate_proving_ctx(
589 &mut self,
590 system_records: SystemRecords<Val<E::SC>>,
591 record_arenas: Vec<VB::RecordArena>,
592 ) -> Result<ProvingContext<E::PB>, GenerationError> {
593 #[cfg(feature = "metrics")]
594 let mut current_trace_heights =
595 self.get_trace_heights_from_arenas(&system_records, &record_arenas);
596 let ctx = self
598 .chip_complex
599 .generate_proving_ctx(system_records, record_arenas)?;
600
601 let idx_trace_heights = ctx
603 .per_air
604 .iter()
605 .map(|(air_idx, ctx)| (*air_idx, ctx.main_trace_height()))
606 .collect_vec();
607 let max_trace_height = if TypeId::of::<Val<E::SC>>() == TypeId::of::<BabyBear>() {
609 let min_log_blowup = log2_ceil_usize(self.config().as_ref().max_constraint_degree - 1);
610 1 << (BabyBear::TWO_ADICITY - min_log_blowup)
611 } else {
612 tracing::warn!(
613 "constructing VirtualMachine for unrecognized field; using max_trace_height=2^30"
614 );
615 1 << 30
616 };
617 if let Some(&(air_idx, height)) = idx_trace_heights
618 .iter()
619 .find(|(_, height)| *height > max_trace_height)
620 {
621 return Err(GenerationError::TraceHeightsLimitExceeded {
622 air_idx,
623 height,
624 max_height: max_trace_height,
625 });
626 }
627 let trace_height_constraints = &self.pk.trace_height_constraints;
629 if trace_height_constraints.is_empty() {
630 tracing::warn!("generating proving context without trace height constraints");
631 }
632 for (i, constraint) in trace_height_constraints.iter().enumerate() {
633 let value = idx_trace_heights
634 .iter()
635 .map(|&(air_idx, h)| constraint.coefficients[air_idx] as u64 * h as u64)
636 .sum::<u64>();
637
638 if value >= constraint.threshold as u64 {
639 tracing::info!(
640 "trace heights {:?} violate linear constraint {} ({} >= {})",
641 idx_trace_heights,
642 i,
643 value,
644 constraint.threshold
645 );
646 return Err(GenerationError::LinearTraceHeightConstraintExceeded {
647 constraint_idx: i,
648 value,
649 threshold: constraint.threshold,
650 });
651 }
652 }
653 #[cfg(feature = "metrics")]
654 self.finalize_metrics(&mut current_trace_heights);
655 #[cfg(feature = "stark-debug")]
656 self.debug_proving_ctx(&ctx);
657
658 Ok(ctx)
659 }
660
661 pub fn prove(
672 &mut self,
673 interpreter: &mut PreflightInterpretedInstance2<Val<E::SC>, VB::VmConfig>,
674 state: VmState<Val<E::SC>, GuestMemory>,
675 num_insns: Option<u64>,
676 trace_heights: &[u32],
677 ) -> Result<(Proof<E::SC>, Option<GuestMemory>), VirtualMachineError>
678 where
679 Val<E::SC>: PrimeField32,
680 <VB::VmConfig as VmExecutionConfig<Val<E::SC>>>::Executor:
681 PreflightExecutor<Val<E::SC>, VB::RecordArena>,
682 {
683 self.transport_init_memory_to_device(&state.memory);
684
685 let PreflightExecutionOutput {
686 system_records,
687 record_arenas,
688 to_state,
689 } = self.execute_preflight(interpreter, state, num_insns, trace_heights)?;
690 let final_memory =
692 (system_records.exit_code == Some(ExitCode::Success as u32)).then_some(to_state.memory);
693 let ctx = self.generate_proving_ctx(system_records, record_arenas)?;
694 let proof = self.engine.prove(&self.pk, ctx);
695
696 Ok((proof, final_memory))
697 }
698
699 pub fn verify(
704 &self,
705 vk: &MultiStarkVerifyingKey<E::SC>,
706 proofs: &[Proof<E::SC>],
707 ) -> Result<(), VmVerificationError>
708 where
709 Com<E::SC>: AsRef<[Val<E::SC>; CHUNK]> + From<[Val<E::SC>; CHUNK]>,
710 Val<E::SC>: PrimeField32,
711 {
712 if self.config().as_ref().continuation_enabled {
713 verify_segments(&self.engine, vk, proofs).map(|_| ())
714 } else {
715 assert_eq!(proofs.len(), 1);
716 verify_single(&self.engine, vk, &proofs[0]).map_err(VmVerificationError::StarkError)
717 }
718 }
719
720 pub fn commit_program_on_device(
727 &self,
728 program: &Program<Val<E::SC>>,
729 ) -> CommittedTraceData<E::PB> {
730 let trace = generate_cached_trace(program);
731 let d_trace = self
732 .engine
733 .device()
734 .transport_matrix_to_device(&Arc::new(trace));
735 let (commitment, data) = self.engine.device().commit(std::slice::from_ref(&d_trace));
736 CommittedTraceData {
737 commitment,
738 trace: d_trace,
739 data,
740 }
741 }
742
743 pub fn transport_committed_exe_to_device(
749 &self,
750 committed_exe: &VmCommittedExe<E::SC>,
751 ) -> CommittedTraceData<E::PB> {
752 let commitment = committed_exe.get_program_commit();
753 let trace = &committed_exe.trace;
754 let prover_data = &committed_exe.prover_data;
755 self.engine
756 .device()
757 .transport_committed_trace_to_device(commitment, trace, prover_data)
758 }
759
760 pub fn load_program(&mut self, cached_program_trace: CommittedTraceData<E::PB>) {
762 self.chip_complex.system.load_program(cached_program_trace);
763 }
764
765 pub fn transport_init_memory_to_device(&mut self, memory: &GuestMemory) {
766 self.chip_complex
767 .system
768 .transport_init_memory_to_device(memory);
769 }
770
771 pub fn executor_idx_to_air_idx(&self) -> Vec<usize> {
772 let ret = self.chip_complex.inventory.executor_idx_to_air_idx();
773 tracing::debug!("executor_idx_to_air_idx: {:?}", ret);
774 assert_eq!(self.executor().inventory.executors().len(), ret.len());
775 ret
776 }
777
778 pub fn build_metered_ctx(&self) -> MeteredCtx {
780 let (constant_trace_heights, air_names, widths, interactions): (
781 Vec<_>,
782 Vec<_>,
783 Vec<_>,
784 Vec<_>,
785 ) = self
786 .pk
787 .per_air
788 .iter()
789 .map(|pk| {
790 let constant_trace_height =
791 pk.preprocessed_data.as_ref().map(|pd| pd.trace.height());
792 let air_names = pk.air_name.clone();
793 let width = pk
794 .vk
795 .params
796 .width
797 .total_width(<<E::SC as StarkGenericConfig>::Challenge>::D);
798 let num_interactions = pk.vk.symbolic_constraints.interactions.len();
799 (constant_trace_height, air_names, width, num_interactions)
800 })
801 .multiunzip();
802
803 self.executor().build_metered_ctx(
804 &constant_trace_heights,
805 &air_names,
806 &widths,
807 &interactions,
808 )
809 }
810
811 pub fn build_metered_cost_ctx(&self) -> MeteredCostCtx {
813 let widths: Vec<_> = self
814 .pk
815 .per_air
816 .iter()
817 .map(|pk| {
818 pk.vk
819 .params
820 .width
821 .total_width(<<E::SC as StarkGenericConfig>::Challenge>::D)
822 })
823 .collect();
824
825 self.executor().build_metered_cost_ctx(&widths)
826 }
827
828 pub fn num_airs(&self) -> usize {
829 let num_airs = self.pk.per_air.len();
830 debug_assert_eq!(num_airs, self.chip_complex.inventory.airs().num_airs());
831 num_airs
832 }
833
834 pub fn air_names(&self) -> impl Iterator<Item = &'_ str> {
835 self.pk.per_air.iter().map(|pk| pk.air_name.as_str())
836 }
837
838 #[cfg(feature = "stark-debug")]
840 pub fn debug_proving_ctx(&mut self, ctx: &ProvingContext<E::PB>) {
841 if self.h_pk.is_none() {
842 let air_inv = self.config().create_airs().unwrap();
843 self.h_pk = Some(air_inv.keygen(&self.engine));
844 }
845 let pk = self.h_pk.as_ref().unwrap();
846 debug_proving_ctx(self, pk, ctx);
847 }
848}
849
850#[derive(Serialize, Deserialize)]
851#[serde(bound(
852 serialize = "Com<SC>: Serialize",
853 deserialize = "Com<SC>: Deserialize<'de>"
854))]
855pub struct ContinuationVmProof<SC: StarkGenericConfig> {
856 pub per_segment: Vec<Proof<SC>>,
857 pub user_public_values: UserPublicValuesProof<{ CHUNK }, Val<SC>>,
858}
859
860pub trait ContinuationVmProver<SC: StarkGenericConfig> {
862 fn prove(
863 &mut self,
864 input: impl Into<Streams<Val<SC>>>,
865 ) -> Result<ContinuationVmProof<SC>, VirtualMachineError>;
866}
867
868pub trait SingleSegmentVmProver<SC: StarkGenericConfig> {
874 fn prove(
875 &mut self,
876 input: impl Into<Streams<Val<SC>>>,
877 trace_heights: &[u32],
878 ) -> Result<Proof<SC>, VirtualMachineError>;
879}
880
881#[derive(Getters, MutGetters)]
887pub struct VmInstance<E, VB>
888where
889 E: StarkEngine,
890 VB: VmBuilder<E>,
891{
892 pub vm: VirtualMachine<E, VB>,
893 pub interpreter: PreflightInterpretedInstance2<Val<E::SC>, VB::VmConfig>,
894 #[getset(get = "pub")]
895 program_commitment: Com<E::SC>,
896 #[getset(get = "pub")]
897 exe: Arc<VmExe<Val<E::SC>>>,
898 #[getset(get = "pub", get_mut = "pub")]
899 state: Option<VmState<Val<E::SC>, GuestMemory>>,
900}
901
902impl<E, VB> VmInstance<E, VB>
903where
904 E: StarkEngine,
905 VB: VmBuilder<E>,
906{
907 pub fn new(
908 mut vm: VirtualMachine<E, VB>,
909 exe: Arc<VmExe<Val<E::SC>>>,
910 cached_program_trace: CommittedTraceData<E::PB>,
911 ) -> Result<Self, StaticProgramError> {
912 let program_commitment = cached_program_trace.commitment.clone();
913 vm.load_program(cached_program_trace);
914 let interpreter = vm.preflight_interpreter(&exe)?;
915 let state = vm.create_initial_state(&exe, vec![]);
916 Ok(Self {
917 vm,
918 interpreter,
919 program_commitment,
920 exe,
921 state: Some(state),
922 })
923 }
924
925 #[instrument(name = "vm.reset_state", level = "debug", skip_all)]
926 pub fn reset_state(&mut self, inputs: impl Into<Streams<Val<E::SC>>>) {
927 self.state
928 .as_mut()
929 .unwrap()
930 .reset(&self.exe.init_memory, self.exe.pc_start, inputs);
931 }
932}
933
934impl<E, VB> ContinuationVmProver<E::SC> for VmInstance<E, VB>
935where
936 E: StarkEngine,
937 Val<E::SC>: PrimeField32,
938 VB: VmBuilder<E>,
939 <VB::VmConfig as VmExecutionConfig<Val<E::SC>>>::Executor: Executor<Val<E::SC>>
940 + MeteredExecutor<Val<E::SC>>
941 + PreflightExecutor<Val<E::SC>, VB::RecordArena>,
942{
943 fn prove(
947 &mut self,
948 input: impl Into<Streams<Val<E::SC>>>,
949 ) -> Result<ContinuationVmProof<E::SC>, VirtualMachineError> {
950 self.prove_continuations(input, |_, _| {})
951 }
952}
953
954impl<E, VB> VmInstance<E, VB>
955where
956 E: StarkEngine,
957 Val<E::SC>: PrimeField32,
958 VB: VmBuilder<E>,
959 <VB::VmConfig as VmExecutionConfig<Val<E::SC>>>::Executor: Executor<Val<E::SC>>
960 + MeteredExecutor<Val<E::SC>>
961 + PreflightExecutor<Val<E::SC>, VB::RecordArena>,
962{
963 pub fn prove_continuations(
967 &mut self,
968 input: impl Into<Streams<Val<E::SC>>>,
969 mut modify_ctx: impl FnMut(usize, &mut ProvingContext<E::PB>),
970 ) -> Result<ContinuationVmProof<E::SC>, VirtualMachineError> {
971 let input = input.into();
972 self.reset_state(input.clone());
973 let vm = &mut self.vm;
974 let metered_ctx = vm.build_metered_ctx();
975 let metered_interpreter = vm.metered_interpreter(&self.exe)?;
976 let (segments, _) = metered_interpreter.execute_metered(input, metered_ctx)?;
977 let mut proofs = Vec::with_capacity(segments.len());
978 let mut state = self.state.take();
979 for (seg_idx, segment) in segments.into_iter().enumerate() {
980 let _segment_span = info_span!("prove_segment", segment = seg_idx).entered();
981 let _prove_span = info_span!("total_proof").entered();
983 let Segment {
984 instret_start,
985 num_insns,
986 trace_heights,
987 } = segment;
988 assert_eq!(state.as_ref().unwrap().instret, instret_start);
989 let from_state = Option::take(&mut state).unwrap();
990 vm.transport_init_memory_to_device(&from_state.memory);
991 let PreflightExecutionOutput {
992 system_records,
993 record_arenas,
994 to_state,
995 } = vm.execute_preflight(
996 &mut self.interpreter,
997 from_state,
998 Some(num_insns),
999 &trace_heights,
1000 )?;
1001 state = Some(to_state);
1002
1003 let mut ctx = vm.generate_proving_ctx(system_records, record_arenas)?;
1004 modify_ctx(seg_idx, &mut ctx);
1005 let proof = vm.engine.prove(vm.pk(), ctx);
1006 proofs.push(proof);
1007 }
1008 let to_state = state.unwrap();
1009 let final_memory = &to_state.memory.memory;
1010 let user_public_values = UserPublicValuesProof::compute(
1011 vm.config().as_ref().memory_config.memory_dimensions(),
1012 vm.config().as_ref().num_public_values,
1013 &vm_poseidon2_hasher(),
1014 final_memory,
1015 );
1016 self.state = Some(to_state);
1017 Ok(ContinuationVmProof {
1018 per_segment: proofs,
1019 user_public_values,
1020 })
1021 }
1022}
1023
1024impl<E, VB> SingleSegmentVmProver<E::SC> for VmInstance<E, VB>
1025where
1026 E: StarkEngine,
1027 Val<E::SC>: PrimeField32,
1028 VB: VmBuilder<E>,
1029 <VB::VmConfig as VmExecutionConfig<Val<E::SC>>>::Executor:
1030 PreflightExecutor<Val<E::SC>, VB::RecordArena>,
1031{
1032 #[instrument(name = "total_proof", skip_all)]
1033 fn prove(
1034 &mut self,
1035 input: impl Into<Streams<Val<E::SC>>>,
1036 trace_heights: &[u32],
1037 ) -> Result<Proof<E::SC>, VirtualMachineError> {
1038 self.reset_state(input);
1039 let vm = &mut self.vm;
1040 let exe = &self.exe;
1041 assert!(!vm.config().as_ref().continuation_enabled);
1042 let mut trace_heights = trace_heights.to_vec();
1043 trace_heights[PUBLIC_VALUES_AIR_ID] = vm.config().as_ref().num_public_values as u32;
1044 let state = self.state.take().expect("State should always be present");
1045 let num_custom_pvs = state.custom_pvs.len();
1046 let (proof, final_memory) = vm.prove(&mut self.interpreter, state, None, &trace_heights)?;
1047 let final_memory = final_memory.ok_or(ExecutionError::DidNotTerminate)?;
1048 self.state = Some(VmState::new(
1050 0,
1051 exe.pc_start,
1052 final_memory,
1053 vec![],
1054 DEFAULT_RNG_SEED,
1055 num_custom_pvs,
1056 ));
1057 Ok(proof)
1058 }
1059}
1060
1061pub fn verify_single<E>(
1067 engine: &E,
1068 vk: &MultiStarkVerifyingKey<E::SC>,
1069 proof: &Proof<E::SC>,
1070) -> Result<(), VerificationError>
1071where
1072 E: StarkEngine,
1073{
1074 engine.verify(vk, proof)
1075}
1076
1077pub struct VerifiedExecutionPayload<F> {
1079 pub exe_commit: [F; CHUNK],
1087 pub final_memory_root: [F; CHUNK],
1089}
1090
1091pub fn verify_segments<E>(
1108 engine: &E,
1109 vk: &MultiStarkVerifyingKey<E::SC>,
1110 proofs: &[Proof<E::SC>],
1111) -> Result<VerifiedExecutionPayload<Val<E::SC>>, VmVerificationError>
1112where
1113 E: StarkEngine,
1114 Val<E::SC>: PrimeField32,
1115 Com<E::SC>: AsRef<[Val<E::SC>; CHUNK]>,
1116{
1117 if proofs.is_empty() {
1118 return Err(VmVerificationError::ProofNotFound);
1119 }
1120 let mut prev_final_memory_root = None;
1121 let mut prev_final_pc = None;
1122 let mut start_pc = None;
1123 let mut initial_memory_root = None;
1124 let mut program_commit = None;
1125
1126 for (i, proof) in proofs.iter().enumerate() {
1127 let res = engine.verify(vk, proof);
1128 match res {
1129 Ok(_) => (),
1130 Err(e) => return Err(VmVerificationError::StarkError(e)),
1131 };
1132
1133 let mut program_air_present = false;
1134 let mut connector_air_present = false;
1135 let mut merkle_air_present = false;
1136
1137 for air_proof_data in proof.per_air.iter() {
1139 let pvs = &air_proof_data.public_values;
1140 let air_vk = &vk.inner.per_air[air_proof_data.air_id];
1141 if air_proof_data.air_id == PROGRAM_AIR_ID {
1142 program_air_present = true;
1143 if i == 0 {
1144 program_commit =
1145 Some(proof.commitments.main_trace[PROGRAM_CACHED_TRACE_INDEX].as_ref());
1146 } else if program_commit.unwrap()
1147 != proof.commitments.main_trace[PROGRAM_CACHED_TRACE_INDEX].as_ref()
1148 {
1149 return Err(VmVerificationError::ProgramCommitMismatch { index: i });
1150 }
1151 } else if air_proof_data.air_id == CONNECTOR_AIR_ID {
1152 connector_air_present = true;
1153 let pvs: &VmConnectorPvs<_> = pvs.as_slice().borrow();
1154
1155 if i != 0 {
1156 if pvs.initial_pc != prev_final_pc.unwrap() {
1158 return Err(VmVerificationError::InitialPcMismatch {
1159 initial: pvs.initial_pc.as_canonical_u32(),
1160 prev_final: prev_final_pc.unwrap().as_canonical_u32(),
1161 });
1162 }
1163 } else {
1164 start_pc = Some(pvs.initial_pc);
1165 }
1166 prev_final_pc = Some(pvs.final_pc);
1167
1168 let expected_is_terminate = i == proofs.len() - 1;
1169 if pvs.is_terminate != FieldAlgebra::from_bool(expected_is_terminate) {
1170 return Err(VmVerificationError::IsTerminateMismatch {
1171 expected: expected_is_terminate,
1172 actual: pvs.is_terminate.as_canonical_u32() != 0,
1173 });
1174 }
1175
1176 let expected_exit_code = if expected_is_terminate {
1177 ExitCode::Success as u32
1178 } else {
1179 DEFAULT_SUSPEND_EXIT_CODE
1180 };
1181 if pvs.exit_code != FieldAlgebra::from_canonical_u32(expected_exit_code) {
1182 return Err(VmVerificationError::ExitCodeMismatch {
1183 expected: expected_exit_code,
1184 actual: pvs.exit_code.as_canonical_u32(),
1185 });
1186 }
1187 } else if air_proof_data.air_id == MERKLE_AIR_ID {
1188 merkle_air_present = true;
1189 let pvs: &MemoryMerklePvs<_, CHUNK> = pvs.as_slice().borrow();
1190
1191 if i != 0 {
1193 if pvs.initial_root != prev_final_memory_root.unwrap() {
1194 return Err(VmVerificationError::InitialMemoryRootMismatch);
1195 }
1196 } else {
1197 initial_memory_root = Some(pvs.initial_root);
1198 }
1199 prev_final_memory_root = Some(pvs.final_root);
1200 } else {
1201 if !pvs.is_empty() {
1202 return Err(VmVerificationError::UnexpectedPvs {
1203 expected: 0,
1204 actual: pvs.len(),
1205 });
1206 }
1207 debug_assert_eq!(air_vk.params.num_public_values, 0);
1209 }
1210 }
1211 if !program_air_present {
1212 return Err(VmVerificationError::SystemAirMissing {
1213 air_id: PROGRAM_AIR_ID,
1214 });
1215 }
1216 if !connector_air_present {
1217 return Err(VmVerificationError::SystemAirMissing {
1218 air_id: CONNECTOR_AIR_ID,
1219 });
1220 }
1221 if !merkle_air_present {
1222 return Err(VmVerificationError::SystemAirMissing {
1223 air_id: MERKLE_AIR_ID,
1224 });
1225 }
1226 }
1227 let exe_commit = compute_exe_commit(
1228 &vm_poseidon2_hasher(),
1229 program_commit.unwrap(),
1230 initial_memory_root.as_ref().unwrap(),
1231 start_pc.unwrap(),
1232 );
1233 Ok(VerifiedExecutionPayload {
1234 exe_commit,
1235 final_memory_root: prev_final_memory_root.unwrap(),
1236 })
1237}
1238
1239impl<SC: StarkGenericConfig> Clone for ContinuationVmProof<SC>
1240where
1241 Com<SC>: Clone,
1242{
1243 fn clone(&self) -> Self {
1244 Self {
1245 per_segment: self.per_segment.clone(),
1246 user_public_values: self.user_public_values.clone(),
1247 }
1248 }
1249}
1250
1251pub(super) fn create_memory_image(
1252 memory_config: &MemoryConfig,
1253 init_memory: &SparseMemoryImage,
1254) -> GuestMemory {
1255 let mut inner = AddressMap::new(memory_config.addr_spaces.clone());
1256 inner.set_from_sparse(init_memory);
1257 GuestMemory::new(inner)
1258}
1259
1260impl<E, VC> VirtualMachine<E, VC>
1261where
1262 E: StarkEngine,
1263 VC: VmBuilder<E>,
1264 VC::SystemChipInventory: SystemWithFixedTraceHeights,
1265{
1266 pub fn override_system_trace_heights(&mut self, heights: &[u32]) {
1268 let num_sys_airs = self.config().as_ref().num_airs();
1269 assert!(heights.len() >= num_sys_airs);
1270 self.chip_complex
1271 .system
1272 .override_trace_heights(&heights[..num_sys_airs]);
1273 }
1274}
1275
1276#[cfg(any(debug_assertions, feature = "test-utils", feature = "stark-debug"))]
1286#[tracing::instrument(level = "debug", skip_all)]
1287pub fn debug_proving_ctx<E, VB>(
1288 vm: &VirtualMachine<E, VB>,
1289 pk: &MultiStarkProvingKey<E::SC>,
1290 ctx: &ProvingContext<E::PB>,
1291) where
1292 E: StarkEngine,
1293 VB: VmBuilder<E>,
1294{
1295 use itertools::multiunzip;
1296 use openvm_stark_backend::prover::types::AirProofRawInput;
1297
1298 let device = vm.engine.device();
1299 let air_inv = vm.config().create_airs().unwrap();
1300 let global_airs = air_inv.into_airs().collect_vec();
1301 let (airs, pks, proof_inputs): (Vec<_>, Vec<_>, Vec<_>) =
1302 multiunzip(ctx.per_air.iter().map(|(air_id, air_ctx)| {
1303 let cached_mains = air_ctx
1305 .cached_mains
1306 .iter()
1307 .map(|pre| device.transport_matrix_from_device_to_host(&pre.trace))
1308 .collect_vec();
1309 let common_main = air_ctx
1310 .common_main
1311 .as_ref()
1312 .map(|m| device.transport_matrix_from_device_to_host(m));
1313 let public_values = air_ctx.public_values.clone();
1314 let raw = AirProofRawInput {
1315 cached_mains,
1316 common_main,
1317 public_values,
1318 };
1319 (
1320 global_airs[*air_id].clone(),
1321 pk.per_air[*air_id].clone(),
1322 raw,
1323 )
1324 }));
1325 vm.engine.debug(&airs, &pks, &proof_inputs);
1326}
1327
1328#[cfg(feature = "metrics")]
1329mod vm_metrics {
1330 use std::iter::zip;
1331
1332 use metrics::counter;
1333
1334 use super::*;
1335 use crate::arch::Arena;
1336
1337 impl<E, VB> VirtualMachine<E, VB>
1338 where
1339 E: StarkEngine,
1340 VB: VmBuilder<E>,
1341 {
1342 pub(crate) fn get_trace_heights_from_arenas(
1350 &self,
1351 system_records: &SystemRecords<Val<E::SC>>,
1352 record_arenas: &[VB::RecordArena],
1353 ) -> Vec<usize> {
1354 let num_airs = self.num_airs();
1355 assert_eq!(num_airs, record_arenas.len());
1356 let mut heights: Vec<usize> = record_arenas
1357 .iter()
1358 .map(|arena| arena.current_trace_height())
1359 .collect();
1360 for (pk, height) in zip(&self.pk.per_air, &mut heights) {
1362 if let Some(constant_height) =
1363 pk.preprocessed_data.as_ref().map(|pd| pd.trace.height())
1364 {
1365 *height = constant_height;
1366 }
1367 }
1368 heights[PROGRAM_AIR_ID] = system_records.filtered_exec_frequencies.len();
1370
1371 heights
1372 }
1373
1374 pub(crate) fn finalize_metrics(&self, heights: &mut [usize]) {
1377 self.chip_complex.system.finalize_trace_heights(heights);
1378 let mut main_cells_used = 0usize;
1379 let mut total_cells_used = 0usize;
1380 for (pk, height) in zip(&self.pk.per_air, heights.iter()) {
1381 let width = &pk.vk.params.width;
1382 main_cells_used += width.main_width() * *height;
1383 total_cells_used +=
1384 width.total_width(<E::SC as StarkGenericConfig>::Challenge::D) * *height;
1385 }
1386 tracing::debug!(?heights);
1387 tracing::info!(main_cells_used, total_cells_used);
1388 counter!("main_cells_used").absolute(main_cells_used as u64);
1389 counter!("total_cells_used").absolute(total_cells_used as u64);
1390
1391 #[cfg(feature = "perf-metrics")]
1392 {
1393 for (name, value) in zip(self.air_names(), heights) {
1394 let labels = [("air_name", name.to_string())];
1395 counter!("rows_used", &labels).absolute(*value as u64);
1396 }
1397 }
1398 }
1399 }
1400}