Skip to main content
Version: 0.16

Deferred state semantics and API contract

DeferredState is the host-side witness for deferred DAG verification and the deferred root commitment. It is not serialized directly: partial proofs carry DeferredStateWire; final non-empty proofs carry a precompile VM STARK proof for the exact deferred root.

The simplified state model is:

pub struct DeferredState {
    registry: Arc<PrecompileRegistry>,
    nodes: BTreeMap<Digest, Node>,
    root: Digest,
    remaining_elements: usize,
    // evaluation results may be memoized internally, but this is not part of the public contract
}

Vocabulary​

  • Registered means a digest has an entry in DeferredState.nodes. Registration can happen through DeferredState::register, evaluation storing canonical/helper nodes, log_statement storing framework AND nodes, or wire rehydration rebuilding entries.
  • Evaluated means a registered input digest has been semantically reduced to a canonical node under the installed PrecompileRegistry. The canonical node is also stored in nodes so it can be referenced by downstream nodes.
  • Logged or root-reachable means a registered digest contributes to DeferredState.root. Only the root-reachable closure is serialized by to_wire; registered/evaluated orphans are dropped.

Registered nodes​

nodes is the durable node store.

  • TRUE_DIGEST is always present and maps to Node::TRUE.
  • Node::TRUE costs no budget.
  • Every non-TRUE node is keyed by node.digest().
  • Structural nodes may reference only children already present in nodes, except for the implicit TRUE_DIGEST:
    • Join has two child digests.
    • PairList has one or more pairs of child digests.
  • Re-registering identical content is idempotent and free.
  • Reusing an existing digest for different content is rejected as a conflicting node.

Registration stores and shape-checks a node in nodes, evaluates it immediately, and stores the canonical result. False predicates and other semantic evaluation failures are reported by registration.

One remaining budget​

DeferredState::new(registry, max_elements) initializes one total budget:

remaining_elements = max_elements

Initialization also installs the registry's init() constants, charging them against that same budget. extend_precompiles(precompiles) merges additional precompiles into an existing state without discarding existing nodes, evaluation results, root, or budget accounting.

Every new unique durable node inserted into nodes decrements remaining_elements by the node's field-element footprint using checked subtraction. Duplicate insertion is free, so registering the same data node at the exact budget limit succeeds. Evaluation results do not have a separate budget and do not double-count canonical payloads; only canonical/helper nodes newly inserted into nodes are charged.

The precompile's decode result is the framework shape gate:

  • NodeType::Data authorizes a non-empty data payload. For memory-backed registration, the host reads exactly the stack-supplied n_chunks; precompile evaluation checks any tag-derived semantic data length.
  • NodeType::Join authorizes exactly one 8-felt payload block, interpreted as two child digests.
  • NodeType::PairList authorizes a non-empty list of lhs_digest || rhs_digest chunks. Precompile evaluation checks any tag-derived semantic pair count.

Processor handlers perform a cheap deferred-budget pre-check before allocating or reading a memory-backed payload, but exact data/pair-list arity remains precompile-specific semantics.

If insertion exhausts the remaining budget, execution aborts with a budget error. The insertion path owns this accounting; processor deferred handlers do not perform post-mutation deferred budget checks.

Evaluation​

Evaluation first requires the input digest to be present in nodes; evaluation state alone never creates durable DAG membership. A call to evaluate_digest(digest) returns the digest of the canonical node. This is a semantic operation: it may compute the result or use internal memoization, but callers do not observe that distinction. Callers that need canonical node contents can compose evaluate_digest with get_node.

Framework nodes evaluate as follows:

Node::TRUE => Node::TRUE
Node::AND(lhs, rhs) =>
  require evaluate_digest(lhs) == TRUE_DIGEST
  require evaluate_digest(rhs) == TRUE_DIGEST
  Node::TRUE

Precompile-owned nodes are evaluated by PrecompileRegistry::evaluate, which dispatches to the owning Precompile with a DeferredContext.

DeferredContext gives precompile implementations the same semantic split:

  • get_node(digest) queries the registered/original node by digest without evaluating it.
  • evaluate_digest(digest) evaluates a registered child digest to its canonical digest.
  • evaluate_digest_pair(lhs, rhs) evaluates two registered child digests to canonical digests.
  • ensure_equal(lhs, rhs) evaluates two children and requires their canonical digests to match.
  • register(node) inserts a freshly minted helper node and returns its original digest.

Root and wire​

root starts at TRUE_DIGEST. log_statement(stmt_digest) evaluates the current root and statement, requires both to evaluate to Node::TRUE, then appends one framework AND node:

next_root = digest(Node::and(previous_root, stmt_digest))

to_wire serializes only the root-reachable closure in canonical child-first order:

  • data entries carry literal data chunks;
  • join entries emit two child indices;
  • pair-list entries emit pairs of child indices.

The wire root is implicit: empty wire opens TRUE_DIGEST, otherwise the root is the digest of the final entry. from_wire(registry, wire, max_elements) decodes untrusted wire, rejects non-canonical or dangling wire by requiring state.to_wire() == wire, then evaluates the implicit wire root to Node::TRUE. Evaluation may insert canonical/helper nodes in addition to the wire nodes.

Deferred proof root resolution​

DeferredProof carries the material needed to bind VM proof verification to a deferred root:

  • Empty is final and resolves to TRUE_DIGEST.
  • Wire is partial/delegable material backed by canonical DeferredStateWire.
  • Stark is final: verification checks the precompile STARK proof against its embedded public root, then returns that root.

The public final verifier accepts only final deferred proof forms. It rejects Wire; wire-backed partial proofs are handled by the explicit Verifier::verify_partial path. Partial verification rehydrates the wire into a DeferredState with the standard precompile registry, verifies the VM STARK against the hydrated state's root, and returns the hydrated state. It rejects Empty and Stark because neither carries wire material to hydrate.

The VM STARK public inputs are built with the resolved final root or hydrated partial root. High-level miden-prover proving APIs and the miden-vm proving facade produce final proofs by default: Empty when no precompile claims were logged, or Stark for non-empty deferred roots. The miden-vm facade exposes only final proving; callers that intentionally delegate or batch precompile proving use the explicit miden-prover::prove_partial* APIs to preserve Wire proof material, then verify_partial to validate and rehydrate that material before producing a final deferred proof.

The current STARK-backed variant is exact-root only; batch-backed proofs need a separate proof form.

Low-level framework API​

The preferred low-level miden_core::deferred::DeferredState surface is small. These APIs are framework APIs, not the public proof-verifier policy surface:

  • DeferredState::new(registry, max_elements) for a state booted with precompile constants
  • extend_precompiles(precompiles) for additive setup
  • registry()
  • root()
  • remaining_elements()
  • get_node(digest) and nodes() -> &BTreeMap<Digest, Node> for registered-node inspection
  • decode(tag) for structural tag decoding
  • register(node) for inserting concrete node content
  • evaluate_digest(digest) for the canonical digest
  • log_statement(stmt_digest)
  • to_wire()
  • from_wire(registry, wire, max_elements)

Callers that have a concrete node should explicitly register it; they may call evaluate_digest on the returned digest when they need the canonical result, and then get_node if they need canonical node contents. Raw evaluation memoization and direct root mutation are not part of the public contract.

Scope note​

Deferred state is the proof-bound precompile witness model. VM execution accumulates a deferred root for logged precompile claims; DeferredProof explains why that root should be accepted. Final public verification accepts only final proof forms, resolving Empty or a verified Stark root before VM STARK verification. Wire-backed material is partial/delegable: Verifier::verify_partial rehydrates Wire under the built-in miden_precompiles::registry(), verifies the VM STARK against the hydrated root, and returns the hydrated state.

The lower-level DeferredState APIs remain parameterized by PrecompileRegistry for framework construction, tests, and non-verifier wire validation. The default registry is empty, but the public VM/prover/verifier path installs the standard miden_precompiles::registry() policy and does not accept caller-supplied precompile registries.