## miden::core::sys::vm
| Procedure | Description |
| ----------- | ------------- |
| conjectured_security_level | Computes the conjectured security level (in bits) attained by the given proof parameters.<br /><br />Evaluates the integer fixed-point formula `min((num_queries * C) >> 16 + query_pow_bits, 128)`.<br />Must match miden_air::config::conjectured_security_level bit-for-bit (enforced by<br />cross-tests). Holds no policy: the caller applies its own acceptance threshold to the result.<br /><br />PRECONDITION: `num_queries <= 150`, so `num_queries * C` fits in a u32 (the `u32shr` below<br />requires that). Parameters returned by `verify_vm_proof` satisfy this bound: the generic<br />verifier enforces it.<br /><br />Inputs: [num_queries, query_pow_bits, ...]<br />Outputs: [level, ...]<br /> |
| 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 per-AIR log heights, the maximum log height, ORDER_TAG, RELATION_DIGEST, and<br />ACE_REGISTRY_ROOT to memory.<br /> |
| verify_vm_proof | Verifies a STARK proof of the caller-staged execution claim and returns the deferred<br />obligation the proof binds and the proof's transcript-bound security parameters.<br /><br />The proof is consumed from the advice stack; request keys name this procedure's MAST root<br />(`CoreLibrary::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 />`request_key(verifier_root, claim_commitment)` with `claim::request_key`, and moves the<br />registered proof package onto the advice stack before calling it.<br /><br />Security parameters (num_queries, query_pow_bits, deep_pow_bits, folding_pow_bits) are loaded<br />from the advice stack and stored in memory for the generic verifier, which enforces their<br />structural bounds and binds them into the Fiat-Shamir transcript - so a proof cannot claim<br />parameters it was not produced with. This procedure holds no security-estimate formula and<br />no acceptance policy: it returns the transcript-bound parameters for the caller to grade<br />(e.g. with `conjectured_security_level`) under its own policy. An estimate or policy change<br />therefore never moves this procedure's root - request keys and registered proof packages<br />stay valid across such changes.<br /><br />The caller stores the claim as `P (+0) \| K (+4) \| I (+8) \| O (+24)`. The complete 40-felt<br />region must be below `constants::verifier_memory_start`.<br /><br />The verifier fetches the kernel digest list from the advice map under K, copies it to<br />`constants::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.<br /><br />Inputs: [claim_ptr, ...]<br />Outputs: [D, num_queries, query_pow_bits, deep_pow_bits, folding_pow_bits, ...]<br /><br />Where:<br />- claim_ptr is word-aligned; its 40-felt region ends at or before<br />`constants::verifier_memory_start`.<br />- D is the deferred root bound by the verified statement.<br />- num_queries, query_pow_bits, deep_pow_bits, folding_pow_bits are the proof's<br />transcript-bound security parameters.<br /> |