Deferred computation

Deferred computation is the mechanism by which a Miden program offloads an expensive or non-native computation such as a hash, a signature check, elliptic-curve arithmetic, or big-integer arithmetic. In its place, the program emits an auditable record of what was claimed. That record is a content-addressed DAG of nodes, committed by a single rolling digest (DeferredState.root, the deferred root commitment). The DAG is designed to be verified externally: either alongside the Miden VM's STARK proof, or by a dedicated Precompile VM whose proof attests that every committed node evaluates correctly.

The DAG can be read as a small program: each node is a term, and evaluating the deferred root to TRUE proves every claim it transitively references. The framework (miden_core::deferred) owns the data model, the root commitment, and the wire format; individual precompiles plug in the meaning of the nodes.

Status. VM proving produces an ExecutionProof in either the Deferred or Complete lifecycle state. A deferred proof carries one portable singleton witness. See Status and scope.

For the precise DeferredState, precompile, and public API contract, see Deferred state semantics and API contract. The digest construction and domain allocations are specified in Eidos framing and domain registry.

Motivation

The deferred subsystem models proof-bound work as a graph of content-addressed nodes and structural edges. This lets the Precompile VM prove computation at a finer grain. For example, it can prove a single curve or field operation without re-hashing every intermediate as an opaque standalone assertion. A calculation like (a + b) · c can reference and share sub-results by content address, so operation-heavy precompiles avoid duplicating the same hashing work.

Each deferred node evaluates to a canonical node; an operation references its operands by their content address; shared sub-computations are shared in the graph. When the framework needs ordered accumulation, it represents it as a chain of semantic AND nodes whose root is a statement that must evaluate to TRUE.

The DAG matches the Precompile VM model: a precompile's operations and constraints form a graph of canonical values, payloads, and joins. Modelling deferred computation the same way lets a precompile's native host implementation mirror its constraint implementation.

Precompile proof shape

The VM STARK authenticates one deferred root but does not prove its committed claims. See the deferred-proof semantics for portable transport, batch precompile proofs, completion, and verification.

The model

A non-TRUE node is a (frame, payload) pair, addressed by its 4-felt Eidos digest. Identical content yields an identical digest, so equal subterms are shared automatically (hash-consing).

• A frame is (domain_tag, param0, param1, param2), with every component represented by one u32. The registered domain selects the owner and defines the meaning of all three parameters, the payload grammar, and the compression schedule. The framework defines frames for semantic AND and opaque CHUNKS nodes. The canonical TRUE node is a zero-digest sentinel with no frame or payload. Deferred statement accumulation uses AND nodes as a restricted right-spined chain.
• A payload is the node's body, in one of four shapes:
  • the framework TRUE sentinel, carrying no data; it is the only zero-payload node;
  • a data payload: one or more 8-felt compression blocks, linearly hashed from the frame's initial chaining word. An empty data payload is forbidden; precompiles decide whether a data payload represents a scalar, digest, message, hash preimage, coordinate, or some other local value;
  • a join payload: two child digests (lhs, rhs) for anything referential, such as a binary operation, predicate, or AND step;
  • a pair-list payload: one or more structural digest pairs for precompile-specific multi-pair structures. Pairs are encoded in payload order as 8-felt chunks lhs || rhs, and their child order is lhs0, rhs0, lhs1, rhs1, and so on. Canonical wire encodes the same ordered pairs as topological child indices. Empty pair lists are rejected; exact pair-count/arity constraints are semantic and enforced by the owning precompile. Budget accounting treats each pair as one ordinary 8-felt payload block, in addition to the frame word.

The digest commits to both the frame and body. A non-TRUE node derives one Eidos initial chaining word from its complete frame, then compresses each 8-felt payload chunk exactly once. The domain, not the framework, assigns meaning to the frame parameters. The last payload compression produces the node digest.

Precompiles

A precompile is the framework's extension point: an implementation of the Precompile trait that claims one registered domain and defines a family of node types plus the rules that give them meaning. Think of it as a small typed sub-language embedded in the DAG. Concrete proof-bound precompiles live in the miden-precompiles crate; their MASM support code is an internal implementation detail.

A precompile defines the following methods:

• decode(params) -> Option<NodeType> checks which constructor a frame names and what structural shape it carries. Payload data is not available yet. The returned shape drives registration and wire handling:
  • NodeType::Data declares a non-empty opaque data payload.
  • NodeType::Join declares one payload block containing two child digests.
  • NodeType::PairList declares a non-empty list of structural lhs || rhs digest pairs.
  • NodeType::True is reserved for the framework TRUE sentinel; a precompile must not return it.
• validate_payload(params, payload) -> bool checks any fixed or parameter-dependent number of data chunks or digest pairs. This method is required and runs after shape validation, before insertion. Returning false rejects the node with InvalidNode.
• evaluate(params, payload, …) -> Result<Node> computes a node's canonical form. The common roles are: validate a canonical value represented as data (its canonical is itself), evaluate an operation (evaluate the child canonicals, then combine), or check a predicate (evaluate operands, return the TRUE node on success or fail otherwise). These roles are conventions rather than a fixed taxonomy. A precompile is free to define multi-ary constructors over data, join, and pair-list payloads.
• init() -> Vec<Node> contributes any canonical constant values (e.g. ZERO, ONE, a curve generator) at registry-initialization time.

Precompiles are collected in a PrecompileRegistry, the framework's dispatcher: it routes each domain tag to its owning precompile and is otherwise indifferent to how the precompile behaves. Each precompile uses an explicitly registered domain tag; names are diagnostic only and are never hashed into protocol identifiers. The registry rejects malformed, framework-reserved, or duplicate tags at construction. PrecompileRegistry::new() creates an empty low-level registry that rejects every precompile-owned frame. A DeferredState carries the registry it evaluates under, and PrecompileRegistry remains defined in miden-core so the framework does not depend on concrete precompile implementations.

During evaluation the framework hands the precompile a DeferredContext, through which it can get_node for a registered digest, evaluate_digest a child digest to its canonical digest, or register a freshly-minted helper node into the DAG. Registered helper nodes are validated under the same registry and must satisfy the ordinary child-closure rules. The precompile never touches the commitment directly. It supplies only per-node meaning, and the framework drives the depth-first recursion.

The in-memory DeferredState may memoize evaluation results internally. That memoization is transparent to precompile implementations and is not serialized as trusted state.

Building the DAG from a program

A program grows and evaluates the DAG through deferred system events. Each event mutates only the host-side DeferredState; no register event hands a digest back through advice. Code that later uses or logs that digest must derive it inside the VM from the same operand-stack payload or ordered memory chunk sequence in a precompile-specific assembly procedure.

Event (adv.*)	Operand stack in	Effect
register_deferred	[CV, PAYLOAD_LO, PAYLOAD_HI, ...]	Recovers the frame from the initial chaining word CV, registers one stack-resident 8-felt payload block, and evaluates the node immediately. The frame determines whether the block is data, two child digests for a precompile-owned join, or one digest pair. Registration rejects an incompatible payload shape or arity before insertion. Structural children may reference only registered nodes or TRUE_DIGEST. The event returns nothing; code that uses the digest must compress the same block from the same CV.
register_deferred_data	[n_chunks, CV, ptr, ...]	Recovers the frame from CV, reads n_chunks non-empty 8-felt blocks from word-aligned memory, registers the corresponding data, pair-list, or one-block precompile-owned join node, and evaluates it immediately. The event returns nothing; code that uses the digest must hash the same memory range from the same CV.
evaluate_deferred	[NODE_DIGEST, ...]	Looks the node up, evaluates it to canonical form, and pushes its frame and payload felts onto the advice stack. For a non-TRUE node, the frame is first in advice-pop order; for a single 8-felt payload, adv_pushw adv_pushw adv_pushw leaves [PAYLOAD_LO, PAYLOAD_HI, FRAME, ...] on the operand stack. TRUE emits one zero word in the frame slot.
evaluate_deferred_frame	[NODE_DIGEST, ...]	Looks the node up, evaluates it to canonical form, and pushes its frame onto the advice stack. TRUE emits one zero word in the frame slot.
evaluate_deferred_payload	[NODE_DIGEST, ...]	Looks the node up, evaluates it to canonical form, and pushes only the canonical payload felts onto the advice stack. For each 8-felt data chunk, advice is arranged as HIGH then LOW so adv_pushw adv_pushw leaves LOW on top and HIGH beneath it; chunks preserve canonical chunk order. Join payloads use the same two-word LIFO convention, leaving lhs_digest above rhs_digest after two adv_pushws. TRUE emits no advice.

register_* validate the decoded shape, require non-empty data and pair lists, and check child closure for structural payloads. The precompile's validate_payload checks any required data or pair-list arity before insertion. Registration stores the original node under its digest, evaluates it immediately, and fails immediately if semantic evaluation fails.

The generic registration events accept precompile-owned nodes and framework CHUNKS nodes, but not the framework-owned DEFERRED_AND_FRAME (or malformed parameterized frames in that domain). Execution constructs rolling AND nodes through log_deferred; state merge and wire rehydration use the same framework-owned node construction directly.

Why the digest is computed inside the VM

A system event is a host hook. Its stack arguments are visible in the VM execution trace, but its host-side state changes are not constrained by the AIR. In particular, a memory-backed register event reads n_chunks chunks at ptr without adding AIR memory accesses that bind the registered contents to those cells. A proof-relevant digest must therefore be derived with VM instructions: compress for a stack payload, or mem_stream plus compress for the same initial chaining word and ordered memory chunk sequence.

This composes with the verifier:

• the VM-computed hash binds the digest to the exact operand-stack values or memory reads consumed by those instructions;
• the VM STARK authenticates the final deferred root accumulated from those digests;
• the precompile STARK proves the aggregate of the ordered constituent roots carried by PrecompileProof.

Together these pieces bind every settled precompile obligation to data committed by the VM execution trace.

Why evaluate_deferred is a bare event

A deferred-evaluation event delegates work the VM does not perform and returns the result through advice, making it an unbound host hint. Using it soundly requires re-hashing the returned payload with VM instructions (and, for the full event, checking the returned frame) and logging a predicate that precompile proving checks; a VM eq/assert over two raw advice results proves nothing about their correctness. Because that obligation is precompile-specific (which predicate to log is the precompile's business), deferred evaluation is intentionally not exposed as a generic safe sys procedure. A precompile-specific assembly procedure must use VM instructions to relate the raw event output to stack or memory values established independently of that advice. Registration has the same binding obligation: the wrapper must compute the node digest from the exact stack payload or ordered memory chunk sequence supplied to the event. A mismatch cannot support a proof-relevant claim about the registered node.

Predicates are not special-cased on evaluation: their canonical is the TRUE node like any other successful predicate. evaluate_deferred_payload emits no advice for TRUE because TRUE has no payload, while evaluate_deferred_frame and full evaluate_deferred emit one zero word. A failed predicate has already surfaced as an error before any felts are pushed.

The deferred root commitment

The deferred root commitment is a rolling AND-chain. DeferredState.root starts at the zero word (TRUE_DIGEST), which is also the digest of the always-present canonical Node::TRUE. A verified statement is any registered digest that evaluates to TRUE and need not be a primitive predicate node. To fold one, the framework registers an AND node { frame: DEFERRED_AND_FRAME, payload: prev_root || stmt_digest } and advances the root to that node's digest. The append path first evaluates the statement under the installed registry and rejects missing or non-TRUE statements. Precompile proving opens the committed root and proves its assertions directly, without reconstructing append history. The digest is structural: even AND(TRUE, TRUE) is hashed with the distinct DEFERRED_AND_DOMAIN Eidos framing and is not equal to TRUE_DIGEST, though it evaluates semantically to TRUE.

Portable decoding checks the committed graph's structure. Session import then validates the operations and assertions needed to prove its root. Neither step rebuilds the execution evaluator.

Portable witnesses and verification

DeferredState::into_witness consumes runtime state and exports the logged root's reachable closure as a PrecompileWitness. Empty work is represented by None; each witness opens one non-TRUE root. The in-memory graph and serialized graph have the same representation:

• index 0 is implicit TRUE_DIGEST;
• entries[i] has index i + 1;
• data entries carry literal data chunks;
• joins carry two backward child indices;
• pair lists carry ordered pairs of backward child indices;
• the root is the digest of the final entry.

Export uses deterministic child-first DFS and omits unreachable nodes. Checked construction and canonical decoding validate framework shapes, nonempty payloads, backward references, reconstructed commitments, duplicate-free entries, root reachability, and exact DFS order. They use bounded, iterative graph traversal without running the evaluator.

ExecutionProof::read_from_bytes decodes portable material without a precompile registry. A prover passes singleton witnesses directly to Prover::prove_precompiles, which validates their operations and assertions while importing into one Session. Computations may be shared across inputs, while each parent operand and each ordered root occurrence retains its proof-binding use. The resulting proof carries the exact ordered roots. Completing an execution proof preserves its compatibility declaration. See the API contract for format versions and input limits.

Status and scope

This framework is the proof-bound precompile substrate. Execution accumulates host-side DeferredState; log_deferred advances its root by folding registered statements with DEFERRED_AND_FRAME. The miden-precompiles crate supplies the bundled implementations used by core-library facades and standard proving. See the API contract for the portable transport, batching, completion, and verification lifecycle.

Generic DAG resource accounting and the external STARK that verifies a committed DAG are outside this framework's scope.