Deferred state semantics and API contract

DeferredState is the host-side witness for deferred DAG verification and the deferred root commitment. The in-memory state is not serialized directly; ExecutionProof carries DeferredStateWire, and DeferredState::from_wire rebuilds a trusted state by decoding canonical wire and evaluating the wire's implicit root under the installed PrecompileRegistry.

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. Proof verification compares the returned state.root() to the externally committed deferred root.

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: proofs carry DeferredStateWire, verification rehydrates it under the built-in miden_precompiles::registry() in the public VM/prover/verifier path, and the final deferred root is the public value checked by the STARK proof. The lower-level DeferredState APIs remain parameterized by PrecompileRegistry for framework construction, tests, and non-verifier wire validation. Public proof verification always uses the built-in miden_precompiles::registry() policy.