## miden::core::sys::vm
| Procedure | Description |
| ----------- | ------------- |
| compute_conjectured_security_level | Computes the conjectured security level (in bits) attained by the given proof parameters.<br /><br />Evaluates `min(((num_queries * C) >> 16) + query_pow_bits, 128)` using integer fixed point.<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 execution claim named by the caller-provided commitment and<br />returns the deferred obligation and transcript-bound security parameters.<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::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 />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 `compute_conjectured_security_level`) under its own policy. An estimate or policy<br />change therefore never moves this procedure's root - request keys and registered proof<br />packages stay valid across such changes.<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 />`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. `D == TRUE_DIGEST` means no deferred statements were logged.<br /><br />Inputs: [CLAIM_COMMITMENT, ...]<br />Outputs: [D, num_queries, query_pow_bits, deep_pow_bits, folding_pow_bits, ...]<br /><br />Where:<br />- CLAIM_COMMITMENT is supplied by the caller and binds the advice-supplied claim preimage.<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 /> |