Instruction semantics

Every value in the DVM carries a typed-value schema: a base type, a secrecy kind, and axes. Four secrecy kinds cover the whole runtime: public_all (replicated, observable), secret_shared(A) (a share of a secret held across a signer set), local_private(R) (private to one role — a nonce witness, a locally finalized signature before disclosure), and cipher_to(R) (encrypted to a designated recipient).

Secrecy is part of the type, not a convention. A computed signature exists as local_private(R_agg) before the publication gate and as public_all only after it — the transition between those two types is itself an instruction, with its own contract.

Each instruction's locality — where it is allowed to execute — is computed from its secrecy inputs, its semantic effect, and its bound runtime parameters. The derived locality is one of: local (any node, no secret interaction), local_at(R) (exactly one designated role), spmd_local(P') (each peer in a set runs it over its own shares, no messages), or distributed(P', r) (a genuine multi-party session with network rounds).

Deterministic digest and projection ops derive local. Share-level linear arithmetic (share_add, share_mul_pub, div_share_by_pub) derives spmd_local: every signer computes over its own share with no wire traffic. Nonlinear operations (share_mul, share_inv, share_rand, open_to) derive distributed, because they need fresh correlated randomness or explicit exchange. Freeze, finalize, and publish sites derive local_at(R) — they are pinned to a designated role. You cannot mislabel a distributed operation as local: the type system computes the answer from the operands.

Beyond its denotational semantics, every instruction site fixes an operational envelope — SiteEffects = (runtimeCalls, requiresBindings, consumes, produces, pending, evidenceOnAbort, publication). The envelope names which local runtime calls the site may make (BindDecision, PrepareStep, AdvanceStep, PublishGate, AbortSession), which context bindings must be present, and which one-shot resources it consumes and produces.

One-shot resources — policy_receipt, permit_handle, step_permit, presign_handle, nonce_handle, mpc_session_handle — each carry a lifecycle class: issued, reserved, active, consumed, expired, revoked, or poisoned. Effect satisfaction is a judgment with five checks: required bindings are present in the canonical call context; every consumed resource is in an admissible lifecycle class before the call and reaches its required post-state after; every produced resource appears correctly bound to operation, session, epoch, phase, and slot; a non-terminal result is only allowed in PendingRemote-compatible form; and if the site declares a publication effect, the first public artifact can appear only after a successful PublishGate response.

• A site is secret-dependent exactly when it calls AdvanceStep or consumes a step_permit, presign_handle, or nonce_handle — and then its execution must pass through the local Runtime–Secret Kernel contract.
• The envelope does not replace the instruction's semantics; it constrains how that semantics is allowed to materialize on a real deployment.

Each instruction site declares plane effects over a fixed set of eleven execution planes: SemanticPlane (pure L1 semantics — typed values, locality, DAG, terminal statuses), DataPlane (materialized values, handles, artifact headers), SecretPlane (witness-local state in the secret kernel, HSM, or provider backend), ProtocolPlane (ingress/egress choreography, PendingRemote, session-slot progress), PolicyPlane (admission bindings, permits, admissibility predicates), ResourcePlane (one-shot lifecycle of nonces, presigns, step permits), ArtifactPlane (commitments, descriptors, content-addressed refs), PublicationPlane (local/private-to-public transitions), EvidencePlane (timeout, replay, equivocation, poison evidence), AuditPlane (secret-clean operational audit trail), and GovernancePlane (domain, epoch, profile, and key lifecycle).

A plane effect is a tuple: which entities the site reads and writes on that plane, the pre- and postconditions, the visibility and durability class, and the failure and audit obligations. The full per-site record — schema, site effects, ontology, plane effects, consequence specification, audit disposition — is what a reviewer audits: not 'what does this code do', but 'what is this instruction allowed to do, on which plane, leaving which record'.

Semantically, share_mul asserts one thing: a new shared value c exists such that c = a·b. Operationally, the same site is a typed transition across six planes:

• SemanticPlane — a new typed output with secrecy secret_shared(A) is born.
• ProtocolPlane — PendingRemote, egress bundles, and later ingress-driven replay are permitted states.
• PolicyPlane — the step requires profile, session, phase, and slot bindings plus a valid step_permit.
• ResourcePlane — the step_permit is consumed; it can never authorize a second execution.
• EvidencePlane — on abort, timeout receipts, replay evidence, and equivocation evidence are the admissible artifacts.
• AuditPlane — the site has at least a local-journal entry; external audit follows its declared disposition.

publish_sig converts Signature(local_private(R_agg)) into Signature(public_all) — that is its whole semantics. Plane-wise it is simultaneously: the first admissible public crossing on the PublicationPlane; the creation of the public signature artifact and publication header on the ArtifactPlane; a mandatory successful PublishGate on the PolicyPlane; publication-denial evidence on the EvidencePlane if refused; and a publication receipt on the AuditPlane.

No silent publication: in all signing families the public signature appears only after an explicit publish_sig. No other site makes a signing result observable — a locally finalized signature that never passes the gate never becomes public, and that property is a typing fact, not an operational convention.

The semantic layer and the effect layer are formally separated. The instruction's semantics defines parent-level truth conditions; the plane, consequence, and audit layers define operational materialization. The conservativity theorem states that adding the full ontology/effect/audit annotation to a program changes nothing observable: Obs(B(P_annotated)) = Obs(B(P)). Every plane effect either projects into an already-permitted semantic transition, enriches purely operational state outside the replicated observation layer, materializes an already-admissible publication or evidence artifact, or acts only on secret-local witness state hidden from observation.

This is the precise answer to 'deterministic execution with optional approval gates — which is it?': execution is deterministic over admitted inputs; policy and approval vary only which inputs are admitted and when a computed result is released. They never change what a program computes, and the theorem is what makes that a claim about the model rather than a promise about the code.