## miden::core::sys::vm
| Procedure | Description |
| ----------- | ------------- |
| load_air_context | Loads the VM-specific AIR context used by the generic STARK verifier.<br /><br />Advice supplies log heights in fixed instance order:<br />[log_core, log_chiplets, log_poseidon2_permutation]<br /><br />Writes the trace shape, proof-order tag, relation commitments, and fixed OOD/query-row<br />addresses to verifier memory.<br /> |
| verify_proof | Verifies a lifted-STARK proof of the Miden VM execution claim named by the caller-provided<br />commitment and returns the common security descriptor followed by the deferred obligation.<br /><br />The claim preimage is fetched from the advice map under the caller-provided claim commitment,<br />authenticated, and stored in verifier-owned memory. The proof is consumed from the advice<br />stack; request keys name this procedure's MAST root<br />(`CoreLibrary::vm_recursive_verifier_root` on the operator side). A consumer that fetches the<br />proof by content derives the identical root in-VM via `procref` of this procedure, computes<br />`proof_request_key(verifier_root, claim_commitment)` with `sys::build_proof_request_key`, and<br />moves the registered proof package onto the advice stack before calling it.<br /><br />The four proof parameters are loaded from advice, structurally validated, and bound into the<br />Fiat-Shamir transcript. The maximum trace height is likewise transcript-bound. The remaining<br />descriptor fields are fixed by this verifier's relation, except for the boundary count derived<br />from the kernel witness authenticated against the claim. The caller passes the returned twelve<br />elements unchanged to `stark::security::compute_conjectured_security_level`, then applies its<br />own acceptance policy. The estimation formula and policy remain outside this procedure.<br />Changing only the formula therefore changes the estimator root without changing this verifier's<br />root. A change to the proof format or to any value supplied by the verifier still changes this<br />procedure.<br /><br />This verifier accepts 7..=150 queries, 0..=31 query/DEEP/folding grinding bits, fixed zero<br />lookup grinding, 6..=29 for every AIR log trace height, and 0..=255 kernel procedures.<br /><br />The claim preimage is encoded as `P (+0) \| K (+4) \| I (+8) \| O (+24)`. The verifier checks its<br />commitment before using these values as AIR public inputs.<br /><br />The verifier fetches the kernel digest list from the advice map under K, copies it to<br />`layout::kernel_witness_ptr`, and checks that it hashes to K. It binds the transcript to the<br />claim commitment and checks the kernel-ROM boundary against this list.<br /><br />The returned deferred root is bound by the verified statement. The caller must settle it or<br />include it in its own statement. `D == TRUE_DIGEST` means no deferred statements were logged.<br /><br />Verification runs in an isolated execution context, preserving caller memory and stack elements<br />below the claim commitment.<br /><br />Inputs: [CLAIM_COMMITMENT, ...]<br />Outputs: [lookup_pow_bits, num_composed_constraints, max_constraint_degree, num_deep_terms,<br />max_message_width, num_lookup_boundary_terms, lookup_fractions_per_row,<br />log_max_height, num_queries, query_pow_bits, deep_pow_bits, folding_pow_bits, D, ...]<br /><br />Where:<br />- CLAIM_COMMITMENT is supplied by the caller and binds the advice-supplied claim preimage.<br />- The first twelve elements are the common security descriptor documented by<br />`stark::security::compute_conjectured_security_level`.<br />- D is the deferred root bound by the verified statement.<br /><br />Invocation: exec<br /> |