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 instret = state.instret();
487 let pc = state.pc();
488 let memory = TracingMemory::from_image(
489 state.memory,
490 system_config.initial_block_size(),
491 access_adapter_arena_size_bound,
492 );
493 let from_state = ExecutionState::new(pc, memory.timestamp());
494 let vm_state = VmState::new(
495 instret,
496 pc,
497 memory,
498 state.streams,
499 state.rng,
500 state.custom_pvs,
501 #[cfg(feature = "metrics")]
502 state.metrics,
503 );
504 let mut exec_state = VmExecState::new(vm_state, ctx);
505 interpreter.reset_execution_frequencies();
506 execute_spanned!("execute_preflight", interpreter, &mut exec_state)?;
507 let filtered_exec_frequencies = interpreter.filtered_execution_frequencies();
508 let touched_memory = exec_state
509 .vm_state
510 .memory
511 .finalize::<Val<E::SC>>(system_config.continuation_enabled);
512 #[cfg(feature = "perf-metrics")]
513 crate::metrics::end_segment_metrics(&mut exec_state);
514
515 let instret = exec_state.vm_state.instret();
516 let pc = exec_state.vm_state.pc();
517 let memory = exec_state.vm_state.memory;
518 let to_state = ExecutionState::new(pc, memory.timestamp());
519 let public_values = exec_state
520 .vm_state
521 .custom_pvs
522 .iter()
523 .map(|&x| x.unwrap_or(Val::<E::SC>::ZERO))
524 .collect();
525 let exit_code = exec_state.exit_code?;
526 let system_records = SystemRecords {
527 from_state,
528 to_state,
529 exit_code,
530 filtered_exec_frequencies,
531 access_adapter_records: memory.access_adapter_records,
532 touched_memory,
533 public_values,
534 };
535 let record_arenas = exec_state.ctx.arenas;
536 let to_state = VmState::new(
537 instret,
538 pc,
539 memory.data,
540 exec_state.vm_state.streams,
541 exec_state.vm_state.rng,
542 exec_state.vm_state.custom_pvs,
543 #[cfg(feature = "metrics")]
544 exec_state.vm_state.metrics,
545 );
546 Ok(PreflightExecutionOutput {
547 system_records,
548 record_arenas,
549 to_state,
550 })
551 }
552
553 #[instrument(name = "vm.create_initial_state", level = "debug", skip_all)]
556 pub fn create_initial_state(
557 &self,
558 exe: &VmExe<Val<E::SC>>,
559 inputs: impl Into<Streams<Val<E::SC>>>,
560 ) -> VmState<Val<E::SC>, GuestMemory> {
561 #[allow(unused_mut)]
562 let mut state = VmState::initial(
563 self.config().as_ref(),
564 &exe.init_memory,
565 exe.pc_start,
566 inputs,
567 );
568 #[cfg(all(feature = "metrics", any(feature = "perf-metrics", debug_assertions)))]
572 {
573 state.metrics.fn_bounds = exe.fn_bounds.clone();
574 state.metrics.debug_infos = exe.program.debug_infos();
575 }
576 #[cfg(feature = "perf-metrics")]
577 {
578 state.metrics.set_pk_info(&self.pk);
579 state.metrics.num_sys_airs = self.config().as_ref().num_airs();
580 state.metrics.access_adapter_offset =
581 self.config().as_ref().access_adapter_air_id_offset();
582 }
583 state
584 }
585
586 #[instrument(name = "trace_gen", skip_all)]
592 pub fn generate_proving_ctx(
593 &mut self,
594 system_records: SystemRecords<Val<E::SC>>,
595 record_arenas: Vec<VB::RecordArena>,
596 ) -> Result<ProvingContext<E::PB>, GenerationError> {
597 #[cfg(feature = "metrics")]
598 let mut current_trace_heights =
599 self.get_trace_heights_from_arenas(&system_records, &record_arenas);
600 let ctx = self
602 .chip_complex
603 .generate_proving_ctx(system_records, record_arenas)?;
604
605 let idx_trace_heights = ctx
607 .per_air
608 .iter()
609 .map(|(air_idx, ctx)| (*air_idx, ctx.main_trace_height()))
610 .collect_vec();
611 let max_trace_height = if TypeId::of::<Val<E::SC>>() == TypeId::of::<BabyBear>() {
613 let min_log_blowup = log2_ceil_usize(self.config().as_ref().max_constraint_degree - 1);
614 1 << (BabyBear::TWO_ADICITY - min_log_blowup)
615 } else {
616 tracing::warn!(
617 "constructing VirtualMachine for unrecognized field; using max_trace_height=2^30"
618 );
619 1 << 30
620 };
621 if let Some(&(air_idx, height)) = idx_trace_heights
622 .iter()
623 .find(|(_, height)| *height > max_trace_height)
624 {
625 return Err(GenerationError::TraceHeightsLimitExceeded {
626 air_idx,
627 height,
628 max_height: max_trace_height,
629 });
630 }
631 let trace_height_constraints = &self.pk.trace_height_constraints;
633 if trace_height_constraints.is_empty() {
634 tracing::warn!("generating proving context without trace height constraints");
635 }
636 for (i, constraint) in trace_height_constraints.iter().enumerate() {
637 let value = idx_trace_heights
638 .iter()
639 .map(|&(air_idx, h)| constraint.coefficients[air_idx] as u64 * h as u64)
640 .sum::<u64>();
641
642 if value >= constraint.threshold as u64 {
643 tracing::info!(
644 "trace heights {:?} violate linear constraint {} ({} >= {})",
645 idx_trace_heights,
646 i,
647 value,
648 constraint.threshold
649 );
650 return Err(GenerationError::LinearTraceHeightConstraintExceeded {
651 constraint_idx: i,
652 value,
653 threshold: constraint.threshold,
654 });
655 }
656 }
657 #[cfg(feature = "metrics")]
658 self.finalize_metrics(&mut current_trace_heights);
659 #[cfg(feature = "stark-debug")]
660 self.debug_proving_ctx(&ctx);
661
662 Ok(ctx)
663 }
664
665 pub fn prove(
676 &mut self,
677 interpreter: &mut PreflightInterpretedInstance2<Val<E::SC>, VB::VmConfig>,
678 state: VmState<Val<E::SC>, GuestMemory>,
679 num_insns: Option<u64>,
680 trace_heights: &[u32],
681 ) -> Result<(Proof<E::SC>, Option<GuestMemory>), VirtualMachineError>
682 where
683 Val<E::SC>: PrimeField32,
684 <VB::VmConfig as VmExecutionConfig<Val<E::SC>>>::Executor:
685 PreflightExecutor<Val<E::SC>, VB::RecordArena>,
686 {
687 self.transport_init_memory_to_device(&state.memory);
688
689 let PreflightExecutionOutput {
690 system_records,
691 record_arenas,
692 to_state,
693 } = self.execute_preflight(interpreter, state, num_insns, trace_heights)?;
694 let final_memory =
696 (system_records.exit_code == Some(ExitCode::Success as u32)).then_some(to_state.memory);
697 let ctx = self.generate_proving_ctx(system_records, record_arenas)?;
698 let proof = self.engine.prove(&self.pk, ctx);
699
700 Ok((proof, final_memory))
701 }
702
703 pub fn verify(
708 &self,
709 vk: &MultiStarkVerifyingKey<E::SC>,
710 proofs: &[Proof<E::SC>],
711 ) -> Result<(), VmVerificationError>
712 where
713 Com<E::SC>: AsRef<[Val<E::SC>; CHUNK]> + From<[Val<E::SC>; CHUNK]>,
714 Val<E::SC>: PrimeField32,
715 {
716 if self.config().as_ref().continuation_enabled {
717 verify_segments(&self.engine, vk, proofs).map(|_| ())
718 } else {
719 assert_eq!(proofs.len(), 1);
720 verify_single(&self.engine, vk, &proofs[0]).map_err(VmVerificationError::StarkError)
721 }
722 }
723
724 pub fn commit_program_on_device(
731 &self,
732 program: &Program<Val<E::SC>>,
733 ) -> CommittedTraceData<E::PB> {
734 let trace = generate_cached_trace(program);
735 let d_trace = self
736 .engine
737 .device()
738 .transport_matrix_to_device(&Arc::new(trace));
739 let (commitment, data) = self.engine.device().commit(std::slice::from_ref(&d_trace));
740 CommittedTraceData {
741 commitment,
742 trace: d_trace,
743 data,
744 }
745 }
746
747 pub fn transport_committed_exe_to_device(
753 &self,
754 committed_exe: &VmCommittedExe<E::SC>,
755 ) -> CommittedTraceData<E::PB> {
756 let commitment = committed_exe.get_program_commit();
757 let trace = &committed_exe.trace;
758 let prover_data = &committed_exe.prover_data;
759 self.engine
760 .device()
761 .transport_committed_trace_to_device(commitment, trace, prover_data)
762 }
763
764 pub fn load_program(&mut self, cached_program_trace: CommittedTraceData<E::PB>) {
766 self.chip_complex.system.load_program(cached_program_trace);
767 }
768
769 pub fn transport_init_memory_to_device(&mut self, memory: &GuestMemory) {
770 self.chip_complex
771 .system
772 .transport_init_memory_to_device(memory);
773 }
774
775 pub fn executor_idx_to_air_idx(&self) -> Vec<usize> {
776 let ret = self.chip_complex.inventory.executor_idx_to_air_idx();
777 tracing::debug!("executor_idx_to_air_idx: {:?}", ret);
778 assert_eq!(self.executor().inventory.executors().len(), ret.len());
779 ret
780 }
781
782 pub fn build_metered_ctx(&self, exe: &VmExe<Val<E::SC>>) -> MeteredCtx {
784 let config = self.config().as_ref();
785 let program_len = exe.program.num_defined_instructions();
786
787 let (mut constant_trace_heights, air_names, widths, interactions): (
788 Vec<_>,
789 Vec<_>,
790 Vec<_>,
791 Vec<_>,
792 ) = self
793 .pk
794 .per_air
795 .iter()
796 .map(|pk| {
797 let constant_trace_height =
798 pk.preprocessed_data.as_ref().map(|pd| pd.trace.height());
799 let air_names = pk.air_name.clone();
800 let width = pk
801 .vk
802 .params
803 .width
804 .total_width(<<E::SC as StarkGenericConfig>::Challenge>::D);
805 let num_interactions = pk.vk.symbolic_constraints.interactions.len();
806 (constant_trace_height, air_names, width, num_interactions)
807 })
808 .multiunzip();
809
810 constant_trace_heights[PROGRAM_AIR_ID] = Some(program_len);
812 if config.has_public_values_chip() {
813 constant_trace_heights[PUBLIC_VALUES_AIR_ID] = Some(config.num_public_values);
815 }
816
817 self.executor().build_metered_ctx(
818 &constant_trace_heights,
819 &air_names,
820 &widths,
821 &interactions,
822 )
823 }
824
825 pub fn build_metered_cost_ctx(&self) -> MeteredCostCtx {
827 let widths: Vec<_> = self
828 .pk
829 .per_air
830 .iter()
831 .map(|pk| {
832 pk.vk
833 .params
834 .width
835 .total_width(<<E::SC as StarkGenericConfig>::Challenge>::D)
836 })
837 .collect();
838
839 self.executor().build_metered_cost_ctx(&widths)
840 }
841
842 pub fn num_airs(&self) -> usize {
843 let num_airs = self.pk.per_air.len();
844 debug_assert_eq!(num_airs, self.chip_complex.inventory.airs().num_airs());
845 num_airs
846 }
847
848 pub fn air_names(&self) -> impl Iterator<Item = &'_ str> {
849 self.pk.per_air.iter().map(|pk| pk.air_name.as_str())
850 }
851
852 #[cfg(feature = "stark-debug")]
854 pub fn debug_proving_ctx(&mut self, ctx: &ProvingContext<E::PB>) {
855 if self.h_pk.is_none() {
856 let air_inv = self.config().create_airs().unwrap();
857 self.h_pk = Some(air_inv.keygen(&self.engine));
858 }
859 let pk = self.h_pk.as_ref().unwrap();
860 debug_proving_ctx(self, pk, ctx);
861 }
862}
863
864#[derive(Serialize, Deserialize)]
865#[serde(bound(
866 serialize = "Com<SC>: Serialize",
867 deserialize = "Com<SC>: Deserialize<'de>"
868))]
869pub struct ContinuationVmProof<SC: StarkGenericConfig> {
870 pub per_segment: Vec<Proof<SC>>,
871 pub user_public_values: UserPublicValuesProof<{ CHUNK }, Val<SC>>,
872}
873
874pub trait ContinuationVmProver<SC: StarkGenericConfig> {
876 fn prove(
877 &mut self,
878 input: impl Into<Streams<Val<SC>>>,
879 ) -> Result<ContinuationVmProof<SC>, VirtualMachineError>;
880}
881
882pub trait SingleSegmentVmProver<SC: StarkGenericConfig> {
888 fn prove(
889 &mut self,
890 input: impl Into<Streams<Val<SC>>>,
891 trace_heights: &[u32],
892 ) -> Result<Proof<SC>, VirtualMachineError>;
893}
894
895#[derive(Getters, MutGetters)]
901pub struct VmInstance<E, VB>
902where
903 E: StarkEngine,
904 VB: VmBuilder<E>,
905{
906 pub vm: VirtualMachine<E, VB>,
907 pub interpreter: PreflightInterpretedInstance2<Val<E::SC>, VB::VmConfig>,
908 #[getset(get = "pub")]
909 program_commitment: Com<E::SC>,
910 #[getset(get = "pub")]
911 exe: Arc<VmExe<Val<E::SC>>>,
912 #[getset(get = "pub", get_mut = "pub")]
913 state: Option<VmState<Val<E::SC>, GuestMemory>>,
914}
915
916impl<E, VB> VmInstance<E, VB>
917where
918 E: StarkEngine,
919 VB: VmBuilder<E>,
920{
921 pub fn new(
922 mut vm: VirtualMachine<E, VB>,
923 exe: Arc<VmExe<Val<E::SC>>>,
924 cached_program_trace: CommittedTraceData<E::PB>,
925 ) -> Result<Self, StaticProgramError> {
926 let program_commitment = cached_program_trace.commitment.clone();
927 vm.load_program(cached_program_trace);
928 let interpreter = vm.preflight_interpreter(&exe)?;
929 let state = vm.create_initial_state(&exe, vec![]);
930 Ok(Self {
931 vm,
932 interpreter,
933 program_commitment,
934 exe,
935 state: Some(state),
936 })
937 }
938
939 #[instrument(name = "vm.reset_state", level = "debug", skip_all)]
940 pub fn reset_state(&mut self, inputs: impl Into<Streams<Val<E::SC>>>) {
941 self.state
942 .as_mut()
943 .unwrap()
944 .reset(&self.exe.init_memory, self.exe.pc_start, inputs);
945 }
946}
947
948impl<E, VB> ContinuationVmProver<E::SC> for VmInstance<E, VB>
949where
950 E: StarkEngine,
951 Val<E::SC>: PrimeField32,
952 VB: VmBuilder<E>,
953 <VB::VmConfig as VmExecutionConfig<Val<E::SC>>>::Executor: Executor<Val<E::SC>>
954 + MeteredExecutor<Val<E::SC>>
955 + PreflightExecutor<Val<E::SC>, VB::RecordArena>,
956{
957 fn prove(
961 &mut self,
962 input: impl Into<Streams<Val<E::SC>>>,
963 ) -> Result<ContinuationVmProof<E::SC>, VirtualMachineError> {
964 self.prove_continuations(input, |_, _| {})
965 }
966}
967
968impl<E, VB> VmInstance<E, VB>
969where
970 E: StarkEngine,
971 Val<E::SC>: PrimeField32,
972 VB: VmBuilder<E>,
973 <VB::VmConfig as VmExecutionConfig<Val<E::SC>>>::Executor: Executor<Val<E::SC>>
974 + MeteredExecutor<Val<E::SC>>
975 + PreflightExecutor<Val<E::SC>, VB::RecordArena>,
976{
977 pub fn prove_continuations(
981 &mut self,
982 input: impl Into<Streams<Val<E::SC>>>,
983 mut modify_ctx: impl FnMut(usize, &mut ProvingContext<E::PB>),
984 ) -> Result<ContinuationVmProof<E::SC>, VirtualMachineError> {
985 let input = input.into();
986 self.reset_state(input.clone());
987 let vm = &mut self.vm;
988 let metered_ctx = vm.build_metered_ctx(&self.exe);
989 let metered_interpreter = vm.metered_interpreter(&self.exe)?;
990 let (segments, _) = metered_interpreter.execute_metered(input, metered_ctx)?;
991 let mut proofs = Vec::with_capacity(segments.len());
992 let mut state = self.state.take();
993 for (seg_idx, segment) in segments.into_iter().enumerate() {
994 let _segment_span = info_span!("prove_segment", segment = seg_idx).entered();
995 let _prove_span = info_span!("total_proof").entered();
997 let Segment {
998 instret_start,
999 num_insns,
1000 trace_heights,
1001 } = segment;
1002 assert_eq!(state.as_ref().unwrap().instret(), instret_start);
1003 let from_state = Option::take(&mut state).unwrap();
1004 vm.transport_init_memory_to_device(&from_state.memory);
1005 let PreflightExecutionOutput {
1006 system_records,
1007 record_arenas,
1008 to_state,
1009 } = vm.execute_preflight(
1010 &mut self.interpreter,
1011 from_state,
1012 Some(num_insns),
1013 &trace_heights,
1014 )?;
1015 state = Some(to_state);
1016
1017 let mut ctx = vm.generate_proving_ctx(system_records, record_arenas)?;
1018 modify_ctx(seg_idx, &mut ctx);
1019 let proof = vm.engine.prove(vm.pk(), ctx);
1020 proofs.push(proof);
1021 }
1022 let to_state = state.unwrap();
1023 let final_memory = &to_state.memory.memory;
1024 let user_public_values = UserPublicValuesProof::compute(
1025 vm.config().as_ref().memory_config.memory_dimensions(),
1026 vm.config().as_ref().num_public_values,
1027 &vm_poseidon2_hasher(),
1028 final_memory,
1029 );
1030 self.state = Some(to_state);
1031 Ok(ContinuationVmProof {
1032 per_segment: proofs,
1033 user_public_values,
1034 })
1035 }
1036}
1037
1038impl<E, VB> SingleSegmentVmProver<E::SC> for VmInstance<E, VB>
1039where
1040 E: StarkEngine,
1041 Val<E::SC>: PrimeField32,
1042 VB: VmBuilder<E>,
1043 <VB::VmConfig as VmExecutionConfig<Val<E::SC>>>::Executor:
1044 PreflightExecutor<Val<E::SC>, VB::RecordArena>,
1045{
1046 #[instrument(name = "total_proof", skip_all)]
1047 fn prove(
1048 &mut self,
1049 input: impl Into<Streams<Val<E::SC>>>,
1050 trace_heights: &[u32],
1051 ) -> Result<Proof<E::SC>, VirtualMachineError> {
1052 self.reset_state(input);
1053 let vm = &mut self.vm;
1054 let exe = &self.exe;
1055 assert!(!vm.config().as_ref().continuation_enabled);
1056 let mut trace_heights = trace_heights.to_vec();
1057 trace_heights[PUBLIC_VALUES_AIR_ID] = vm.config().as_ref().num_public_values as u32;
1058 let state = self.state.take().expect("State should always be present");
1059 let num_custom_pvs = state.custom_pvs.len();
1060 let (proof, final_memory) = vm.prove(&mut self.interpreter, state, None, &trace_heights)?;
1061 let final_memory = final_memory.ok_or(ExecutionError::DidNotTerminate)?;
1062 self.state = Some(VmState::new_with_defaults(
1064 0,
1065 exe.pc_start,
1066 final_memory,
1067 vec![],
1068 DEFAULT_RNG_SEED,
1069 num_custom_pvs,
1070 ));
1071 Ok(proof)
1072 }
1073}
1074
1075pub fn verify_single<E>(
1081 engine: &E,
1082 vk: &MultiStarkVerifyingKey<E::SC>,
1083 proof: &Proof<E::SC>,
1084) -> Result<(), VerificationError>
1085where
1086 E: StarkEngine,
1087{
1088 engine.verify(vk, proof)
1089}
1090
1091pub struct VerifiedExecutionPayload<F> {
1093 pub exe_commit: [F; CHUNK],
1101 pub final_memory_root: [F; CHUNK],
1103}
1104
1105pub fn verify_segments<E>(
1122 engine: &E,
1123 vk: &MultiStarkVerifyingKey<E::SC>,
1124 proofs: &[Proof<E::SC>],
1125) -> Result<VerifiedExecutionPayload<Val<E::SC>>, VmVerificationError>
1126where
1127 E: StarkEngine,
1128 Val<E::SC>: PrimeField32,
1129 Com<E::SC>: AsRef<[Val<E::SC>; CHUNK]>,
1130{
1131 if proofs.is_empty() {
1132 return Err(VmVerificationError::ProofNotFound);
1133 }
1134 let mut prev_final_memory_root = None;
1135 let mut prev_final_pc = None;
1136 let mut start_pc = None;
1137 let mut initial_memory_root = None;
1138 let mut program_commit = None;
1139
1140 for (i, proof) in proofs.iter().enumerate() {
1141 let res = engine.verify(vk, proof);
1142 match res {
1143 Ok(_) => (),
1144 Err(e) => return Err(VmVerificationError::StarkError(e)),
1145 };
1146
1147 let mut program_air_present = false;
1148 let mut connector_air_present = false;
1149 let mut merkle_air_present = false;
1150
1151 for air_proof_data in proof.per_air.iter() {
1153 let pvs = &air_proof_data.public_values;
1154 let air_vk = &vk.inner.per_air[air_proof_data.air_id];
1155 if air_proof_data.air_id == PROGRAM_AIR_ID {
1156 program_air_present = true;
1157 if i == 0 {
1158 program_commit =
1159 Some(proof.commitments.main_trace[PROGRAM_CACHED_TRACE_INDEX].as_ref());
1160 } else if program_commit.unwrap()
1161 != proof.commitments.main_trace[PROGRAM_CACHED_TRACE_INDEX].as_ref()
1162 {
1163 return Err(VmVerificationError::ProgramCommitMismatch { index: i });
1164 }
1165 } else if air_proof_data.air_id == CONNECTOR_AIR_ID {
1166 connector_air_present = true;
1167 let pvs: &VmConnectorPvs<_> = pvs.as_slice().borrow();
1168
1169 if i != 0 {
1170 if pvs.initial_pc != prev_final_pc.unwrap() {
1172 return Err(VmVerificationError::InitialPcMismatch {
1173 initial: pvs.initial_pc.as_canonical_u32(),
1174 prev_final: prev_final_pc.unwrap().as_canonical_u32(),
1175 });
1176 }
1177 } else {
1178 start_pc = Some(pvs.initial_pc);
1179 }
1180 prev_final_pc = Some(pvs.final_pc);
1181
1182 let expected_is_terminate = i == proofs.len() - 1;
1183 if pvs.is_terminate != FieldAlgebra::from_bool(expected_is_terminate) {
1184 return Err(VmVerificationError::IsTerminateMismatch {
1185 expected: expected_is_terminate,
1186 actual: pvs.is_terminate.as_canonical_u32() != 0,
1187 });
1188 }
1189
1190 let expected_exit_code = if expected_is_terminate {
1191 ExitCode::Success as u32
1192 } else {
1193 DEFAULT_SUSPEND_EXIT_CODE
1194 };
1195 if pvs.exit_code != FieldAlgebra::from_canonical_u32(expected_exit_code) {
1196 return Err(VmVerificationError::ExitCodeMismatch {
1197 expected: expected_exit_code,
1198 actual: pvs.exit_code.as_canonical_u32(),
1199 });
1200 }
1201 } else if air_proof_data.air_id == MERKLE_AIR_ID {
1202 merkle_air_present = true;
1203 let pvs: &MemoryMerklePvs<_, CHUNK> = pvs.as_slice().borrow();
1204
1205 if i != 0 {
1207 if pvs.initial_root != prev_final_memory_root.unwrap() {
1208 return Err(VmVerificationError::InitialMemoryRootMismatch);
1209 }
1210 } else {
1211 initial_memory_root = Some(pvs.initial_root);
1212 }
1213 prev_final_memory_root = Some(pvs.final_root);
1214 } else {
1215 if !pvs.is_empty() {
1216 return Err(VmVerificationError::UnexpectedPvs {
1217 expected: 0,
1218 actual: pvs.len(),
1219 });
1220 }
1221 debug_assert_eq!(air_vk.params.num_public_values, 0);
1223 }
1224 }
1225 if !program_air_present {
1226 return Err(VmVerificationError::SystemAirMissing {
1227 air_id: PROGRAM_AIR_ID,
1228 });
1229 }
1230 if !connector_air_present {
1231 return Err(VmVerificationError::SystemAirMissing {
1232 air_id: CONNECTOR_AIR_ID,
1233 });
1234 }
1235 if !merkle_air_present {
1236 return Err(VmVerificationError::SystemAirMissing {
1237 air_id: MERKLE_AIR_ID,
1238 });
1239 }
1240 }
1241 let exe_commit = compute_exe_commit(
1242 &vm_poseidon2_hasher(),
1243 program_commit.unwrap(),
1244 initial_memory_root.as_ref().unwrap(),
1245 start_pc.unwrap(),
1246 );
1247 Ok(VerifiedExecutionPayload {
1248 exe_commit,
1249 final_memory_root: prev_final_memory_root.unwrap(),
1250 })
1251}
1252
1253impl<SC: StarkGenericConfig> Clone for ContinuationVmProof<SC>
1254where
1255 Com<SC>: Clone,
1256{
1257 fn clone(&self) -> Self {
1258 Self {
1259 per_segment: self.per_segment.clone(),
1260 user_public_values: self.user_public_values.clone(),
1261 }
1262 }
1263}
1264
1265pub(super) fn create_memory_image(
1266 memory_config: &MemoryConfig,
1267 init_memory: &SparseMemoryImage,
1268) -> GuestMemory {
1269 let mut inner = AddressMap::new(memory_config.addr_spaces.clone());
1270 inner.set_from_sparse(init_memory);
1271 GuestMemory::new(inner)
1272}
1273
1274impl<E, VC> VirtualMachine<E, VC>
1275where
1276 E: StarkEngine,
1277 VC: VmBuilder<E>,
1278 VC::SystemChipInventory: SystemWithFixedTraceHeights,
1279{
1280 pub fn override_system_trace_heights(&mut self, heights: &[u32]) {
1282 let num_sys_airs = self.config().as_ref().num_airs();
1283 assert!(heights.len() >= num_sys_airs);
1284 self.chip_complex
1285 .system
1286 .override_trace_heights(&heights[..num_sys_airs]);
1287 }
1288}
1289
1290#[cfg(any(debug_assertions, feature = "test-utils", feature = "stark-debug"))]
1300#[tracing::instrument(level = "debug", skip_all)]
1301pub fn debug_proving_ctx<E, VB>(
1302 vm: &VirtualMachine<E, VB>,
1303 pk: &MultiStarkProvingKey<E::SC>,
1304 ctx: &ProvingContext<E::PB>,
1305) where
1306 E: StarkEngine,
1307 VB: VmBuilder<E>,
1308{
1309 use itertools::multiunzip;
1310 use openvm_stark_backend::prover::types::AirProofRawInput;
1311
1312 let device = vm.engine.device();
1313 let air_inv = vm.config().create_airs().unwrap();
1314 let global_airs = air_inv.into_airs().collect_vec();
1315 let (airs, pks, proof_inputs): (Vec<_>, Vec<_>, Vec<_>) =
1316 multiunzip(ctx.per_air.iter().map(|(air_id, air_ctx)| {
1317 let cached_mains = air_ctx
1319 .cached_mains
1320 .iter()
1321 .map(|pre| device.transport_matrix_from_device_to_host(&pre.trace))
1322 .collect_vec();
1323 let common_main = air_ctx
1324 .common_main
1325 .as_ref()
1326 .map(|m| device.transport_matrix_from_device_to_host(m));
1327 let public_values = air_ctx.public_values.clone();
1328 let raw = AirProofRawInput {
1329 cached_mains,
1330 common_main,
1331 public_values,
1332 };
1333 (
1334 global_airs[*air_id].clone(),
1335 pk.per_air[*air_id].clone(),
1336 raw,
1337 )
1338 }));
1339 vm.engine.debug(&airs, &pks, &proof_inputs);
1340}
1341
1342#[cfg(feature = "metrics")]
1343mod vm_metrics {
1344 use std::iter::zip;
1345
1346 use metrics::counter;
1347
1348 use super::*;
1349 use crate::arch::Arena;
1350
1351 impl<E, VB> VirtualMachine<E, VB>
1352 where
1353 E: StarkEngine,
1354 VB: VmBuilder<E>,
1355 {
1356 pub(crate) fn get_trace_heights_from_arenas(
1364 &self,
1365 system_records: &SystemRecords<Val<E::SC>>,
1366 record_arenas: &[VB::RecordArena],
1367 ) -> Vec<usize> {
1368 let num_airs = self.num_airs();
1369 assert_eq!(num_airs, record_arenas.len());
1370 let mut heights: Vec<usize> = record_arenas
1371 .iter()
1372 .map(|arena| arena.current_trace_height())
1373 .collect();
1374 for (pk, height) in zip(&self.pk.per_air, &mut heights) {
1376 if let Some(constant_height) =
1377 pk.preprocessed_data.as_ref().map(|pd| pd.trace.height())
1378 {
1379 *height = constant_height;
1380 }
1381 }
1382 heights[PROGRAM_AIR_ID] = system_records.filtered_exec_frequencies.len();
1384
1385 heights
1386 }
1387
1388 pub(crate) fn finalize_metrics(&self, heights: &mut [usize]) {
1391 self.chip_complex.system.finalize_trace_heights(heights);
1392 let mut main_cells_used = 0usize;
1393 let mut total_cells_used = 0usize;
1394 for (pk, height) in zip(&self.pk.per_air, heights.iter()) {
1395 let width = &pk.vk.params.width;
1396 main_cells_used += width.main_width() * *height;
1397 total_cells_used +=
1398 width.total_width(<E::SC as StarkGenericConfig>::Challenge::D) * *height;
1399 }
1400 tracing::debug!(?heights);
1401 tracing::info!(main_cells_used, total_cells_used);
1402 counter!("main_cells_used").absolute(main_cells_used as u64);
1403 counter!("total_cells_used").absolute(total_cells_used as u64);
1404
1405 #[cfg(feature = "perf-metrics")]
1406 {
1407 for (name, value) in zip(self.air_names(), heights) {
1408 let labels = [("air_name", name.to_string())];
1409 counter!("rows_used", &labels).absolute(*value as u64);
1410 }
1411 }
1412 }
1413 }
1414}