1.1 The prior methods and the remaining problem

Typed assembly and proof-carrying code attach checkable safety facts to low-level programs [21, 22]. Bytecode is the instruction representation consumed by an interpreter. Its verification supplies structural checks before execution [23, 24]. For long-running work, sagas associate committed subtransactions with compensating actions [18]. Message-based designs also use idempotence and compensation when one distributed transaction cannot cover the operation [19].

These methods supply parts of the construction. The remaining problem here is to connect a checked instruction to the evidence and quantities that survive its external execution. A compensation is itself an operation with authority and an outcome. A retry key requires a provider contract specifying request equality and retention [20]. Neither the existence of a key nor a local record of success establishes what reached the beneficiary. Op makes these obligations explicit at the point where the program requests or consumes an external effect.

1.2 Inputs and limits

The source rule language encodes jurisdictional requirements. This paper assumes those predicates arrive as typed verdict procedures. The evaluator consumes each verdict without reinterpreting its legal content. Lex: A Logic for Jurisdictional Rules defines the predicates the evaluator calls [29]. The content-addressed compiler binds the source-rule digest to the generated bytecode digest. It does not claim that operational typing proves the substantive law. The companion paper How Compliance Composes develops the verdict algebra and corridor translation rules [5]. Here a corridor translation specifies how evidence passes between jurisdictions and which requirements need fresh evaluation.

The core semantics also does not prove provider honesty, network delivery, legal finality, confidentiality, or economic resource pricing. Those items appear as named assumptions or open problems. A type checker can prove that a witness is required. It cannot prove that the world described by a signed witness is true.

Theorems below follow from the formal rules in this paper. Conditional consequences add the stated environmental assumptions. Heuristics describe unproved operating practices, and open problems state unresolved formal or empirical questions.

3.1 Types

Base types include bounded integers, Booleans, normalized identifiers, jurisdiction identifiers, digests, and currency-indexed money. Compound types are finite records, variants, and lists with declared maximum length. The following constructors retain information that an ordinary value type would lose at the provider boundary. Here T is a result type, W a write kind, and E an evidence type. For a screening witness, S,J,L,t identify the subjects, jurisdiction, list-and-rule snapshot, and evaluation time. The index K binds evidence to its expected request or continuation, and O identifies an outcome class.

\begin{array}{ll} \mathsf{Linear}\langle T\rangle & \text{one value that must be consumed exactly once},\\ \mathsf{Deferred}\langle W\rangle & \text{one write request not yet dispatched},\\ \mathsf{Screened}\langle S,J,L,t\rangle & \text{a sanctions verdict bound to subjects and snapshot},\\ \mathsf{Authenticated}\langle E,K\rangle & \text{evidence of type $E$ for typed index $K$},\\ \mathsf{Suspended}\langle E,T,K\rangle & \text{a continuation waiting for authenticated $E$},\\ \mathsf{Receipt}\langle O\rangle & \text{a receipt for outcome class $O$}. \end{array}

Money uses a nominal currency index. There is no coercion from \mathsf{Money}\langle c_1\rangle to \mathsf{Money}\langle c_2\rangle. A conversion consumes an authenticated foreign-exchange witness and emits a separate effect.

\mathsf{CommandKey} and \mathsf{OccurrenceKey} are distinct nominal index types. A command key identifies an immutable request before dispatch. An occurrence key identifies a canonical external event after authenticated observation. An authenticated binding connects an occurrence to a command. Neither index coerces into the other.

3.2 Effects and reversal declarations

Let \mathsf{Eff}=\{\mathsf{Check}_{\mathrm{san}},\mathsf{Write}(k),\mathsf{Await}(E),\mathsf{Emit}(q),\mathsf{Read}(a)\}. Here \mathsf{Check}_{\mathrm{san}} checks sanctions, \mathsf{Write}(k) names a write capability, and \mathsf{Await}(E) waits for evidence of type E. The constructors \mathsf{Emit}(q) and \mathsf{Read}(a) emit record kind q and read address a. An effect row is a finite subset of \mathsf{Eff}, ordered by inclusion and composed by union. The row records which capabilities can occur. It does not encode a handler calculus. Compensation and suspension have dedicated syntax and rules.

If the first 100 units have already been paid, aborting the local program cannot remove that payment. The program must state which further act, if any, can respond to the effect. Every effect instance therefore carries exactly one reversal declaration: r ::= \mathsf{NoStateChange} \mid \mathsf{Compensate}(c) \mid \mathsf{Subsequent}(k) \mid \mathsf{Irreversible}(o). The executable encoding stores these declarations in the total finite map \chi_P:\mathsf{EffectInstanceId}\longrightarrow\mathsf{ReversalDecl}. The verifier rejects missing, extra, or inconsistent entries in \chi_P. A committed write inherits the declaration attached to its deferred request. \mathsf{NoStateChange} is valid only when the primitive changes no external or mutable business state. Append-only evidence emission changes the observation history and is never reversed. \mathsf{Compensate}(c) names a typed compensating command.

\mathsf{Subsequent}(k) names a later operation kind that refers to the original occurrence. \mathsf{Irreversible}(o) names the obstruction procedure required if the effect cannot be reversed. The declaration exhaustively states the response shape. Restoring the prior world requires a separate semantic contract.

A compensator is the separate command used to restore a specified business invariant after a forward effect. Its indexed type identifies the effect it answers and the condition its outcome can establish: c:\mathsf{Compensator}\langle W,I,s,a\rangle. The indices name the forward write kind, the invariant sought, the provider scope, and the authority required to invoke it. The declaration attaches to one forward command and governs its authenticated occurrences. On abort, the evaluator proposes eligible compensators in reverse dispatch order. Each proposal is a fresh deferred request with its own sanctions check, authority witness, reversal declaration, and receipt. A compensator can append a subsequent effect. It cannot delete the forward receipt or claim a legal unwind unless its declared kind and witness say so.

Write-class effects are \mathsf{Eff}_W=\{\mathsf{Write}(k):k\in\mathsf{WriteKind}\}. Provider dispatch is a write-class effect because it can change external state. Document production, filings, value movement, and mutable identity operations are also write class.

3.3 Compliance-carrying judgment

The typing judgment records more than the returned value. It also records which resources remain, which effects can occur, and which guarantees must have evidence. This distinguishes a historical statement such as “the payment was authorized” from a current requirement such as “this transmission is authorized.” The main judgment is \Gamma;\Delta;\kappa\vdash e:T\ !\rho \triangleright(\mathcal{R},\mathcal{Q},\mathcal{E});\Delta';\kappa'. \tag{1} Here \Gamma contains unrestricted typed values. The linear context \Delta contains resources that cannot be copied or dropped. The compliance context is \kappa=(\kappa^h,\kappa^s). Its historical part records authenticated assertions and evidence identifiers. Its current part contains predicates valid at the active evaluation cursor c. A cursor identifies the evidence prefix and continuation version at which a predicate is checked. The authenticated projection \mu_c contains mutable ledger state, provider projections, authority, policy, and evaluation time. Immutable program inputs remain separate. The row \rho is the inferred effect upper bound. The contract separates requirements \mathcal{R}, guarantees \mathcal{Q}=(\mathcal{Q}^h,\mathcal{Q}^s), and evidence types \mathcal{E}. A historical guarantee asserts that a specified authenticated record occurs in the bundle. A current guarantee asserts a predicate of the exit projection. Each current witness binds its predicate, cursor, dependencies, and establishing evidence. Transport to another cursor requires a checked derivation. The outputs \Delta',\kappa' expose resource and compliance changes.

Complete path screening means that each route to a write supplies its matching check. Reversal totality means that every effect instance has exactly one valid declaration in \chi_P. The following rules make the screening and resource requirements precise. This definition joins the effect row, the contract, and the bundle obligation. A claim in ensures cannot exist as an annotation alone. It must introduce a witness consumed by a matching proof-bundle entry.

3.4 Screening on every write path

The sanctions check in the example is unconditional. With branches, the same obligation can be met by a separate check on each route. Acceptance must require coverage of every route without requiring all routes to use one witness. Let G_P=(V,E) be the program graph. For a node n, let \mathsf{subj}(n) be its normalized subject set. A sanctions witness is w_s:\mathsf{Screened}\langle S,J,L,t\rangle, where S is the screened subject set, J is the jurisdiction, L is the list-and-rule snapshot digest, and t is evaluation time.

A branch can obtain its own matching witness. The verifier carries forward only facts present on every incoming path; this is a forward must-analysis. At a join it intersects the predecessor facts, while retaining the evidence supplied on each edge. A normalized obligation key q=(S_{req},J,\Pi) names required subjects, jurisdiction, and snapshot/freshness policy. Witness identifiers remain evidence operands, rather than obligation keys. In the equations below, \operatorname{Pred}_r(v) contains the statically reachable predecessors of node v. The sets GEN and KILL contain obligations established and invalidated at that node. For every statically reachable predecessor, compute \begin{aligned} \operatorname{IN}(v)&=\bigcap_{p\in\operatorname{Pred}_{r}(v)}\operatorname{OUT}(p),\\ \operatorname{OUT}(v)&=(\operatorname{IN}(v)\setminus\operatorname{KILL}(v)) \cup\operatorname{GEN}(v). \end{aligned} Entry has no inherited screening facts. A successful check generates each declared obligation it covers. Known invalidations remove affected facts. An obligation that survives the intersection still needs an actual witness when execution takes one incoming edge. The symbol \phi_q records that edge-dependent choice. Each join carries a complete edge-indexed operand w_q=\phi_q(p_1:w_1,\ldots,p_k:w_k). Every predecessor supplies a matching available witness. The runtime selects the operand from its actual incoming edge. It preserves that operand’s subject, snapshot, timestamp, and evidence identifier. It checks current validity again at dispatch. The existing linear rules prevent copied or consumed evidence operands. Thus distinct checks on both arms of a diamond remain admissible. There is no formation exception in this core. A newly created subject remains deferred until the runtime can screen the governing existing principals and the created identifier under the declared policy. This choice removes a bypass from the theorem boundary.

3.5 Deferred writes and linearity

The command sent before the crash must remain the same command after recovery. Linearity first establishes the local part of this requirement: a deferred request cannot be copied or silently discarded. Shared reservations and provider retry protection will supply the separate guarantees across programs and external transmissions. The write request rule is: \frac{\Gamma\vdash p:A\to W\quad \Gamma\vdash\bar v:A \quad \mathsf{rev}(p)=r} {\Gamma;\Delta;\kappa\vdash \mathbf{defer}_{k}(p,\bar v,r):\mathsf{Linear}\langle\mathsf{Deferred}\langle W\rangle\rangle !\{\mathsf{Write}(k)\}\triangleright(\varnothing,(\varnothing,\varnothing),\varnothing); \Delta,d;\kappa}. \tag{T-Defer}

The commit rule consumes the request and a matching screen. Its current-use predicate also checks the authority checkpoint \Theta_u, the authenticated authority and policy record required at this use. Section 4 defines how live execution records that checkpoint and replay verifies it. The rule is: \frac{ \begin{gathered} d:\mathsf{Linear}\langle\mathsf{Deferred}\langle W,S,J\rangle\rangle\in\Delta,\\ w:\mathsf{Screened}\langle S',J,L,t\rangle,\quad S\subseteq S',\quad \mathsf{fresh}(L,t),\\ \mathsf{validAt}(w,\mu_c,\Theta_u,d) \end{gathered} }{ \begin{gathered} \Gamma;\Delta,d;\kappa\vdash \mathbf{commit}(w,d): \mathsf{Linear}\langle\mathsf{Receipt}\langle W\rangle\rangle,\\ !\{\mathsf{Write}(k),\mathsf{Emit}(\mathsf{receipt})\}\triangleright (\{\mathsf{sanctions}(S,J)\},(\{\mathsf{dispatched}(k)\},\varnothing),\\ \{\mathsf{Receipt}\langle W\rangle\});\Delta;\kappa' \end{gathered}}. \tag{T-Commit}

In these rules, \Delta,d displays the named request beside the other linear bindings. The premise checks that it is available, and the conclusion removes its binding. The current-use predicate checks the witness cursor or a checked transport derivation. It applies to every witness consumer, including values retained in unrestricted \Gamma. Dispatch evidence is a historical guarantee. Its presence does not assert that authority or external state remains unchanged.

The verifier splits \Delta across branches. It requires identical residual linear contexts at each join. It rejects weakening and contraction.

3.6 Typed suspension

After the client restarts, evidence must reach the saved program for the original request. A correctly signed statement about another payment cannot supply its result. A provider wait therefore uses the indexed form \mathsf{Suspended}\langle\mathsf{ProviderOutcome}\langle s\rangle,T,k\rangle. The index s is provider scope and k:\mathsf{CommandKey} is the predispatch command key. The continuation accepts only \mathsf{Authenticated}\langle\mathsf{ProviderOutcome}\langle s\rangle,k\rangle. That evidence binds the provider statement to the immutable request indexed by k. Its payload can identify an external occurrence whose key became available after dispatch. The expected evidence constructor can require an open outcome or an outcome with a valid closure witness. An open outcome leaves the command’s execution right unclosed. Any further transmission still requires its own current authority check. A closure witness establishes the provider-enforced end of that execution right, including after a partial payment. The pause token commits to the program digest, program counter, environment digest, linear-context digest, expected evidence type, provider scope, command key, and prior bundle head. Its linear continuation identity and evidence cursor prevent a repeated assertion from executing the same continuation twice. Let D_{s,k}=\mathsf{Linear}\langle\mathsf{Receipt}\langle \mathsf{Dispatch}\langle s,k\rangle\rangle\rangle.

\frac{ \Gamma;\Delta;\kappa\vdash d:D_{s,k} }{ \begin{gathered} \Gamma;\Delta;\kappa\vdash\mathbf{await}_{\mathsf{ProviderOutcome}\langle s\rangle,T}(d): \mathsf{Suspended}\langle\mathsf{ProviderOutcome}\langle s\rangle,T,k\rangle,\\ !\{\mathsf{Await}(\mathsf{ProviderOutcome}\langle s\rangle),\mathsf{Emit}(\mathsf{pause})\} \triangleright(\varnothing,(\varnothing,\varnothing),\{\mathsf{PauseToken}\});\Delta';\kappa \end{gathered}}. \tag{T-Await}

Suspension stores current witnesses at the pause cursor. Resumption first applies admitted authenticated updates to \mu_c and \kappa^s. It processes every relevant update in the committed prefix, including unmatched revocations and policy changes. It invalidates affected witnesses unless a checked derivation transports them. The continuation then evaluates with the resulting current context. Historical witnesses remain available.

No timeout resumes the original provider continuation. An authenticated policy-clock event can append a timeout obstruction or authorize a separate cancellation request. The original wait remains suspended until an authenticated provider outcome arrives. This rule prevents silence, local inference, or a rail observation from becoming a provider statement.

3.7 Sequential composition

The preceding rules describe individual operations. Their composition must account for evidence that changes between one instruction and the next, especially across a wait. Sequential execution retains earlier facts when the continuation preserves or re-establishes them. An assertion that an authorization was granted differs from the predicate that it remains active. Grant followed by revocation preserves the first assertion and invalidates the second predicate.

For an exit predicate Q, the weakest successful-exit precondition states exactly what must hold initially for every successful exit to satisfy Q. The notation \Downarrow_{\mathrm{ok}} denotes successful evaluation from state \mu to result v and state \mu'. Define the weakest successful-exit precondition by \operatorname{wlp}_{e}(Q)(\mu) \iff \forall(v,\mu').\quad (\mu,e)\Downarrow_{\mathrm{ok}}(v,\mu')\Longrightarrow Q(v,\mu'). This relation includes authenticated updates admitted during execution and resumption. It states partial correctness. Failure and suspension retain their separate terminal contracts. Substitution of the first result into the continuation is implicit. Relational composition gives \operatorname{wlp}_{e_1;e_2}(Q) =\operatorname{wlp}_{e_1}\bigl(\operatorname{wlp}_{e_2}(Q)\bigr). The sequential rule retains a certified set F of current predicates: \frac{ \begin{gathered} \Gamma;\Delta;\kappa\vdash e_1:T_1!\rho_1 \triangleright(\mathcal{R}_1,\mathcal{Q}_1,\mathcal{E}_1);\Delta_1;\kappa_1,\\ \Gamma,x:T_1;\Delta_1;\kappa_1\vdash e_2:T_2!\rho_2 \triangleright(\mathcal{R}_2,\mathcal{Q}_2,\mathcal{E}_2);\Delta_2;\kappa_2,\\ \kappa_1\models\bigwedge\mathcal{R}_2,\quad F\subseteq\mathcal{Q}_1^s,\\ \kappa_1\vdash_{\mathrm{cert}} \operatorname{wlp}_{e_2}\!\left(\bigwedge F\right) \end{gathered} }{ \begin{gathered} \Gamma;\Delta;\kappa\vdash\mathbf{let}\ x=e_1\ \mathbf{in}\ e_2: T_2!(\rho_1\cup\rho_2),\\ \triangleright\bigl(\mathcal{R}_1, (\mathcal{Q}_1^h\cup\mathcal{Q}_2^h,F\cup\mathcal{Q}_2^s),\\ \mathcal{E}_1\uplus\mathcal{E}_2\uplus\mathcal{E}_F\bigr);\Delta_2;\kappa_2\oplus F \end{gathered} }. \tag{T-Seq} Here \mathcal{E}_F contains the exit-cursor derivations for retained predicates. The context extension \kappa_2\oplus F makes those fresh witnesses available to subsequent expressions. The complete entry assertion includes the input compliance context. Ambient facts used by the continuation remain explicit assumptions. Evidence identifiers distinguish separate guarantee occurrences and retain their original supporting records. Effect subsumption permits a row \rho' where \rho is expected when \rho'\subseteq\rho [25].

Checking that an earlier predicate survives can be cheaper than proving the whole continuation again. A dependency footprint records every part of the state on which that predicate depends. A dependency footprint D(p) satisfies \mu|_{D(p)}=\mu'|_{D(p)} \Longrightarrow \bigl(p(\mu)\iff p(\mu')\bigr). A mutation footprint W(e) contains every coordinate that a permitted execution can change. Both footprints include authority, policy, time, aliases, and collection membership when these affect the predicate. Thus inserting a hold invalidates a predicate that states that no holds exist. Sequence and choice take unions of mutation footprints. Await includes permitted imports and authority or time updates. An unresolved footprint covers its complete declared scope.

The certificate checker has three constructors:

1. Frame: D(p)\cap W(e_2)=\varnothing transports the incoming witness to the exit cursor.

2. Preservation: a checked transition derivation establishes \{A\land p\}\ e_2\ \{p\}, with \kappa_1\models A\land p.

3. Re-establishment: a checked suffix derivation establishes \{A\}\ e_2\ \{p\}, with \kappa_1\models A. The final witness names the establishing transition.

Primitive certificates instantiate the pinned registry’s checked transition contracts. Sequence and choice certificates respectively compose derivations and cover every branch. Certificates have finite syntax and local decidable checking rules. The verifier checks a supplied derivation, rather than solving arbitrary semantic implications. Its input bound includes every certificate node.

Re-establishment proves exit validity. Each intermediate use still requires a witness valid at its own cursor. An earlier authorization occurrence does not regain authority merely because the same predicate later becomes true. Every authenticated update invalidates affected current witnesses before a subsequent consumer runs. This rule also applies to witnesses stored in \Gamma or serialized continuations. Historical evidence remains available after invalidation.

The transition contracts describe recorded execution. Their correspondence with external facts retains the assumptions of Proposition 5.12.

3.8 Bilateral signed commitment

Suppose the payment requires signed verdicts from two jurisdictions before the dispatch decision can be committed. A reply must identify both the operation and the same evaluation, and each side must follow the agreed message order. A bilateral session is the fixed exchange between those two roles. Its locks are single-use protocol resources for that exchange; they do not themselves establish that a provider has moved funds. A cross-jurisdiction commit uses the bilateral session below. The Sovereign Jurisdiction Network defines the bilateral commit and corridor receipt instantiated here [30]. Coordinator-based three-phase commit is outside this construction. Let \omega be the operation key and let \epsilon be the evaluation identifier. For roles A and B, the global session type is \begin{aligned} \mathsf{BSC}(\omega,\epsilon)={}& A\to B:\mathsf{Begin}(\omega,\epsilon);\\ &B\to A:\mathsf{Lock}_B(\omega,\epsilon);\quad A\to B:\mathsf{Lock}_A(\omega,\epsilon);\\ &A\to B:\mathsf{Verdict}_A(\omega,\epsilon);\quad B\to A:\mathsf{Verdict}_B(\omega,\epsilon);\\ &A\to B:\mathsf{Decision}(d);\quad B\to A:\mathsf{Ack}(d);\quad \mathsf{end}. \end{aligned} \tag{BSC} This fixed protocol is a finite session type in the sense of binary session typing [26]. Every message is authenticated and binds (\omega,\epsilon), the role, the message kind, the prior transcript head, and its payload. The projection for each role is the dual of the other projection.

Each role has states \mathsf{Init}\longrightarrow\mathsf{Locked}\longrightarrow \mathsf{Verified}\longrightarrow \mathsf{Committed}\mid\mathsf{Aborted}. The two locks are linear and indexed by (\omega,\epsilon,role). Entry to \mathsf{Verified} requires both signed verdicts in the authenticated transcript. The decision function is fixed. It returns Commit exactly when both verdicts admit the operation and returns Abort otherwise. Role A transmits that deterministic result but cannot choose it. The acknowledgement is part of the global type and cannot introduce a different decision. The signed Decision and Ack bind a transcript head that contains both verdicts.

Contradictory signed verdicts by one role at the same (\omega,\epsilon) form q:\mathsf{EquivocationEvidence}\langle role,\omega,\epsilon,v_0,v_1\rangle. The total function \mathsf{blame}(q) verifies both signatures and produces a typed blame witness naming that role. Silence alone does not produce blame. It produces a typed obstruction unless an authenticated policy event supplies the missing attribution rule.

This theorem is a safety and accountability result. Message delivery and nonblocking termination during a partition remain open.

4.1 Committed evidence epochs

A delayed reply can arrive after a newer message, and independent providers can reply in either order. Replay needs the order the machine actually committed, including the authority updates it admitted before resumption. An evidence epoch fixes a prefix of that admitted history for one execution interval. Each evidence item names its authenticated stream, sequence, evaluation time, and digest. Reception and execution admission are distinct transitions. The durable inbox retains authenticated arrivals. An admission transaction appends an item only when it is the next item in its stream. A gap remains pending until its missing predecessor arrives or an authenticated policy records an obstruction. Across independent streams, admission transactions assign immutable increasing execution ordinals.

Let A be that append-ordered admitted log. Before using evidence, the runtime commits an execution epoch \begin{aligned} E_e=\langle&e,r_{e-1},n_e,\operatorname{root}(A_{\le n_e}),\\ &M_e,F_e,\Theta_e,\operatorname{hash}(C_e)\rangle. \end{aligned} \tag{2} Here e is the epoch identifier, r_{e-1} its predecessor root, and n_e its final admitted ordinal. The state C_e starts the epoch, while \Theta_e fixes its trust inputs. Here M_e names authenticated stream membership and F_e records its contiguous stream frontiers. The record binds the previous epoch root, exact admitted prefix, starting state, and trust inputs. The evaluator selects the least unused matching execution ordinal within that prefix. Event timestamps remain policy evidence. They do not reorder committed execution. The continuation receipt binds the epoch, prior continuation version, selected ordinal, and resulting version.

Later evidence enters a successor epoch. A reassessment names that later prefix and references the historical source root. It retains the source receipts and cannot execute the historical continuation again. Receiving sequence 2 before sequence 1 leaves 2 pending. Once 1 arrives, that stream admits 1 followed by 2. An independent stream can advance in the intervening admission transactions.

The trust-root input is \Theta=\langle p_{rules},p_{types},K_{auth},R_{rev},C_{corr},t_{eval}\rangle. It pins the rule-pack digest, type-registry digest, authority-key registry, revocation snapshot, corridor map, and evaluation time. Each protected use also records an authenticated authority checkpoint \Theta_u as immutable evidence. The pinned trust root authenticates that checkpoint and its authority-update path. The checkpoint binds the exact request, current authority epoch, policy dependencies, validity interval, and required use stage. Live execution obtains the checkpoint required for that use. Replay verifies the recorded checkpoint instead of reading live authority state. Determinism never assumes the conclusion that replay agrees. It assumes identical bytes for P,x, the committed epochs, their trust inputs, and the authenticated evidence they bind. The order of receipt alone supplies no stronger reproducibility claim.

4.2 Small-step rules

Pure rules are conventional and deterministic. The three boundary rules determine when an external request is dispatched, when its evidence resumes the program, and how failure enters the record. The displayed tuples name the active expression directly in place of the program and counter. Coordinates suppressed from those displays retain the updates specified in the surrounding text.

4.3 Determinism

4.4 Append-only reversal semantics

A reversal declaration determines what can happen after a forward effect. It does not alter the historical occurrence. Define a subsequent-effect graph G_s=(N_s,E_s). Its root is the original command key k_0. Command nodes carry command keys. External-event nodes carry canonical occurrence keys and authenticated command bindings. A response command refers to the event that caused it. Repeated assertions append evidence for an existing event. They create no additional event node or quantity. The permitted node kinds are \mathsf{ForwardPosting},\ \mathsf{Return},\ \mathsf{Refund},\ \mathsf{RailReversal},\ \mathsf{LegalUnwind},\ \mathsf{Compensation}.

\mathsf{Return} is a provider or rail return of the original transfer. \mathsf{Refund} is a new payment initiated by the payee. \mathsf{RailReversal} records a provider reversal outcome. \mathsf{LegalUnwind} records a distinct legal act. \mathsf{Compensation} records a business response that may restore an invariant. These kinds are not synonyms. Recourse consumes provider finality in its recovery fold and keeps award, execution, satisfaction, and recovery as separate facts [33].

For each authenticated provider-reversal occurrence key, the fold admits exactly one \mathsf{RailReversal} node. Repeated assertions about that occurrence may have distinct assertion identifiers. They deduplicate on occurrence key before the graph is extended.

5.1 Four distinct evidence types

The payment can be recorded on a ledger before the beneficiary receives usable funds. The following evidence types identify the different conclusions each record can support:

A ledger event can support a provider outcome when the provider says it does. It cannot substitute for the provider statement. A provider outcome is necessary for the provider-resume rule. It is not sufficient for legal finality.

5.2 The seven-coordinate state

The four evidence types answer different questions about the same operation. A state record must permit their answers to change separately. One provider-mediated operation has exactly the product state \mathcal{X}=\mathcal A\times\mathcal D\times\mathcal P\times \mathcal F\times\mathcal R\times\mathcal S\times\mathcal O. \tag{4} The coordinates, in order, are authorization, dispatch, provider phase, finality, reconciliation, subsequent effects, and obstructions. The provider coordinate contains a phase and an independent execution-closure state: \mathcal P=\mathsf{Phase}\times\mathsf{Closure},\qquad \mathsf{Closure}=\mathsf{Open}\mid\mathsf{Closed}(w_C). The phase constructors are Unobserved, Accepted, Processing, Partial, Succeeded, Failed, and Reversed. A closure witness w_C binds the command, request, provider scope, executed quantity, remaining quantity, and provider-enforced closure of further execution. Terminality comes from that witness, independently of the phase label. A partial outcome can therefore be open or terminal. Closing forward execution preserves its authenticated event history and any later correction or reversal rights. No confirmation counter or omnibus “status” replaces this product.

The obstruction coordinate also retains unresolved execution obligations and their reservation receipts. A reservation there records exposure that still requires discharge; it does not report a failed reservation. In the table, DAG means directed acyclic graph: its directed links contain no cycle. The state is deliberately redundant. A provider can report success while finality remains unassessed. The local and provider books can disagree after a final outcome. A subsequent refund can exist without changing the provider phase of the original payment. These combinations are necessary records, not anomalies to be normalized away.

5.3 Identifying requests and external events

The same 100-unit payment can produce repeated replies, appear on two delivery channels, and later receive a correction. Counting replies would count money more than once. The model distinguishes the business intent, the submitted request, the physical event, and each signed assertion about that event. An intent identifier names the authorized business action and its total quantity. An operation key, also called a command key, identifies one immutable execution request under that intent: \begin{split} k=k_{op}=H(&\mathsf{command},\mathsf{kernelNamespace}, \mathsf{intentId},\\ &\mathsf{programDigest},\mathsf{stepId},\mathsf{attempt},s,h_{req}). \end{split} Here H is the domain-separated content hash, and h_{req} hashes the canonical request bytes. The field \mathsf{kernelNamespace} identifies the issuing runtime’s command namespace. The program digest and step identifier identify the instruction that created the request. Every field exists before dispatch. The command registry binds k to the exact request bytes, provider scope, and authorized intent quantity. The attempt index identifies a distinct execution right. It does not count network retransmissions. Retransmission preserves the request, command key, and provider idempotency key. A new command under the same intent requires an authenticated transfer of unexecuted quantity or explicit authority for additional quantity. It also requires a reservation for its complete exposure.

An occurrence key identifies one authoritative external event: e=H(\mathsf{occurrence},N_{\mathrm{issuer}}, \mathsf{recordKind},\mathsf{stableEventId}). \tag{5} The provider contract fixes N_{\mathrm{issuer}}, the immutable record kind, and the meaning of each stable reference. The namespace includes the authoritative account or ledger namespace and its reference epoch. For an incoming credit, it also binds the recipient account and exact asset unit. A command reference, a transfer reference, and an individual posting reference have different types. The reference contract identifies the economic event unit represented by each posting. The occurrence key excludes command identity, quantity, phase, observation time, reporting channel, and legal origin.

An assertion identifier hashes the complete signed envelope, including support and delivery fields. An assertion points to an occurrence through its authenticated reference contract. An authoritative alias certificate can attach another reference to an existing canonical credit root. Reporter agreement alone cannot join two roots. Admission verifies the authoritative root before creating allocatable credit. The root fixes the recipient account, asset unit, reference namespace, and epoch. Different immutable payloads under one root produce one typed conflict. They do not create two credits. An authorized correction references the preceding canonical payload digest and preserves both assertions.

Provider progress and funded postings have different constructors. A progress assertion can change the observed phase of a command. It creates no allocatable quantity. Distinct posting identifiers can create distinct quantities for the same command. A cumulative report supports posting deltas only through an authenticated, gap-free progress contract. That contract identifies each increment once, binds its unique predecessor, and rejects conflicting branches. It cannot count both cumulative totals and their constituent postings as credit.

A provider outcome envelope is a=\langle s,k,h_{req},z,p,t_{event},seq,keyId,sig\rangle. \tag{6} z identifies the progress, posting, correction, or subsequent-effect constructor. The payload p contains its canonical event fields and authenticated command binding. A posting carries its occurrence key e. A progress assertion can precede the creation of that key. The verifier recomputes h_{req} from the immutable request stored under k. That request contains its original amount, asset, source, destination, and route. Executed quantity is an outcome field and does not replace the requested amount. The verifier authenticates every field in (6).

Key possession alone does not establish scoped designation. The designation names the provider, rail, rulebook, jurisdiction, asset, operation class, and validity interval. Authentic contradictory assertions remain evidence of a conflict even when they fail outcome admission. The evidence recorder preserves them without introducing additional credit.

5.4 Historical receipts after authority changes

A provider can perform an instruction, sign its receipt, and retire the signing key before the receipt reaches the client. The receipt describes the earlier performance. Its admission uses authority to attest at the established signing time. Every new transmission uses authority at the required current use stage. The physical occurrence keeps its original identity through both judgments.

Let I_a=[\ell_a,u_a] be an authenticated interval containing the signing time of the complete assertion a. The interval’s evidence binds the exact assertion digest and states how it constrains signing time. A timestamp written by the signer supplies a claimed time only. An inclusion timestamp can establish an upper bound on existence while leaving the lower bound unresolved. Such evidence must establish the bounds required by the applicable designation and lifecycle rule before admission proceeds.

The checkpoint’s authentication establishes its source and contents. Its completeness and timely delivery remain explicit authority-feed assumptions. An empty list of revocations supplies neither property. The host selects the checkpoint required for admission and records it with the admitted assertion. Replay verifies those recorded inputs. Later authenticated evidence creates a reassessment under a later checkpoint and preserves the earlier admission record. An adverse reassessment impairs affected execution until its governing correction or disposition resolves the obstruction.

Attestation time and performance time have different roles. A newly designated key can report an earlier occurrence when its reporting mandate covers that occurrence and reference contract. The earlier occurrence need not lie within the new key’s signing interval. Authority to report a fact establishes no legal authority to perform the reported act. An authentic report of unauthorized performance remains evidence of the effect and its associated obstruction. The applicable execution contract supplies the separate judgment of lawful performance.

For example, suppose an assertion is signed within [9,10], the key retires at 20, and the receipt arrives at 30. A complete checkpoint that retains the designation and establishes uncompromised signing admits the receipt. A signer who claims event time 9 after compromise at 8 gains no historical authority from that claim. If compromise from 8 is established after an earlier admission, reassessment records the changed support and impairs affected execution. It preserves the receipt and the physical event history.

5.5 Credit attribution after spending and correction

A received 100 can discharge claim A even after the recipient spends the cash. The payment’s attribution to A must remain recorded, or spending would allow the same receipt to discharge claim B. A later correction can reduce the supported receipt from 100 to 80. If support returns to 100, the restored 20 belongs to A’s retained allocation before a new claim can use it. This requires separate records for the original allocation, its currently supported quantity, and cash available for new payments.

A claim slice is a specified part of an obligation, and discharge is the reduction of that obligation under its governing transition rule. A purpose slice similarly identifies the authorized use to which credit is attributed. The slice owner is that claim or purpose, not a new owner inferred from possession of the cash. The allocation’s face quantity retains its assigned amount even when later evidence reduces current support. A family contract supplies the authority and discharge rules for the particular kind of obligation.

5.6 Provider chains and uncoupled legs

A transfer can pass through several providers. Each hop has its own scope, authenticated outcome, and seven-coordinate state. Success at one hop establishes only that provider’s stated phase. It does not establish a later provider’s outcome or the beneficiary’s receipt.

Swift’s September 2025 study covers first-quarter 2025 cross-border traffic to the top 40 receiving countries. The sample was mostly corporate and financial-market traffic. In that sample, 75 percent reached the beneficiary institution within ten minutes. International in-flight time was under 20 percent of elapsed time, while the last mile was over 80 percent [1]. Arrival at the beneficiary institution was not beneficiary credit. Du, Huang, and Scharfstein locate much of the remaining delay between the beneficiary bank and final account credit [2, Section 7.2]. These measurements motivate the evidence separation. They do not set a latency bound for this model.

An exchange with two uncoupled legs carries one product state per leg. If the asset leg is final while the cash leg is pending, the exchange is not final. A payment-versus-payment or delivery-versus-payment rule can condition the two final-settlement events [7, Principle 12].

An atomic ledger transaction that records both legs gives ledger confirmation of both. It gives legal finality of neither without the separate rulebook-and-law witness for each leg.

5.7 Finality is a produced witness

A provider’s terminal-partial receipt can close further execution of the request while leaving a separate question about the 100 already paid. The finality rule addresses that quantity under the applicable law and rulebook. Legal finality means that the transfer or disposition has the stated legal effect against the relevant parties and third parties, including the stated insolvency treatment. The definition is evaluated under a named body of law and system rulebook. Operational permanence and high ledger depth are not substitutes.

The witness type is \begin{split} w_F:\mathsf{FinalityWitness}\langle &outcomeDigest,provider,rail,rulebook, jurisdiction,asset,t_{eval},\\ &legalPolicyId,policyVersion,authority,signature\rangle. \end{split} \tag{7}

The only introduction rule is: \frac{ \begin{gathered} a:\mathsf{Authenticated}\langle\mathsf{ProviderOutcome}\langle s\rangle,k\rangle,\\ \mathsf{policyAuth}(w_F,\Theta),\quad \mathsf{binds}(w_F,a,s,t_{eval}),\\ \mathsf{policySaysFinal}(w_F) \end{gathered} }{ \mathsf{assessFinality}(a,w_F):\mathsf{Final}(w_F)}. \tag{T-Finality}

The binding predicate requires equality of provider, rail, rulebook, jurisdiction, asset, outcome digest, and evaluation time. The policy authority is named and authenticated. Finality requires T-Finality. An internal status change has no introduction rule.

5.8 Total component transitions

The state machine applies one authenticated event at a time. Each event has a defined result for every source coordinate. An invalid transition appends a typed obstruction and otherwise leaves the product unchanged.

Closed execution never reopens through a phase update. A later forward posting under a closed command remains recordable as a provider-contract breach. It supplies no new execution right and enters the credit and exposure reconciliation rules. An expiry after provider acceptance does not revoke an accepted outcome. It can create a breach, stale-authority, or review obstruction. The historical provider phase remains the authenticated phase that occurred. Likewise, a later correction has its own signed correction identity. It references the original occurrence and preceding canonical payload digest. It preserves the earlier envelope and changes the current fold through the authorized adjustment rule.

5.9 Partial outcomes and residual tranches

Return to the original request for 125 units. A report of 100 paid leaves 25 unexecuted, but it does not say whether the provider can still execute that remainder. A residual tranche is the remaining quantity assigned to a later command after the original execution right has been closed or transferred. A partial outcome contains an executed quantity q_e and an unexecuted quantity q_r, with q_e+q_r=q_0 in the asset’s exact integer unit. The original command records \mathsf{Partial}(q_e). Authenticated postings establish q_e. The original command retains the execution right and reservation for q_r while further completion remains possible. A signed terminal-partial outcome can close that remaining execution right. An authenticated provider-enforced cancellation fence or atomic capacity transfer can establish the same exclusivity. Local timeout alone establishes neither condition. Only then can an atomic split transfer residual intention and reservation to a child command. The child has a fresh attempt index, immutable request digest, sanctions witness, reversal declaration, and dispatch lifecycle. Its command key uses the complete predispatch construction in Section 5.3. The split receipt binds the parent key, child key, residual quantity, and provider fence. It preserves the total assigned intention and reserved exposure. It preserves the original request and outcome as historical records. An ordinary retransmission uses the original command key and creates no child.

The original business intent has a separate quantity ledger. Let Q_i be its immutable target, P_i its supported paid quantity, and R_i its distinct returned quantity. Let C_i be quantity discharged by an authorized cancellation or amendment, and U_i the outstanding target. The payment-family transition maintains Q_i=(P_i-R_i)+C_i+U_i,\qquad P_i-R_i\ge0,\quad C_i,U_i\ge0. \tag{I} All quantities use the same asset and exact unit. The sums group the existing allocation rows once across parent and child commands. Residual splitting changes command assignment and preserves this intent ledger. Closure of a provider execution right does not cancel the business obligation. Cancellation requires its own authority and family transition. Unallocated excess receipts remain explicit quantities for subsequent authorized allocation or return. They do not make the target negative. Returns within allocated credit reopen the target through the authorized family delta. A debit beyond supported credit enters a separate discrepancy obligation.

An intent is \mathsf{Paid} when P_i-R_i=Q_i and C_i=U_i=0. It is \mathsf{PartiallyMatched} when positive supported net payment leaves U_i>0. Authorized cancellation has a distinct terminal disposition. Thus 100 paid against a 125 target leaves 25 outstanding, even when the parent command matches its assigned 100.

5.10 Reconciliation as a signed fold

Reconciliation compares the quantity currently assigned to a command with the supported external quantity attributed to it. This comparison uses the event and allocation ledgers already defined; it cannot sum raw provider messages. A fold applies the recorded transitions in order to obtain those current quantities. Let L_t contain canonical requests, authenticated provider evidence, and committed intention, attribution, and correction receipts through evaluation time t. For an asset quantity group Q, meaning the exact-unit quantities with addition and signed differences, define two projections \alpha^L_t,\alpha^P_t:L_t\longrightarrow (\mathsf{OperationKey}\rightharpoonup Q). \tag{8} The symbol \rightharpoonup denotes a partial function: a command may occur on only one side of the comparison. The local projection maps each command to its current assigned intention. An authenticated residual split transfers intention between parent and child while preserving the total. The original request remains immutable. The provider projection groups supported credit rows and distinct linked debit rows by contributing command: \alpha^P_t(k)=\sum_{\lambda:\,k(\lambda)=k}q_t(\lambda) -\sum_{\mu:\,k(\mu)=k}b_t(\mu). Here b_t(\mu) is the active authenticated quantity of a distinct debit allocation row. Each row has one contributing command, even when several later commands refer to it. This projection reports command-level net external quantity. Equation (5b) separately reports claim discharge and outstanding balance. Authoritative occurrence normalization precedes attribution. Progress assertions check consistency with the posting fold and create no additional quantity. A failure before execution contributes zero. A later rail reversal enters \mathcal S and preserves the original event history. It preserves the original credit attribution and adds its distinct debit allocation to the net projection. Its authorized family transition updates the corresponding outstanding claim balance once. For a received 100 followed by an actual return of 100, the records remain credit 100, debit 100, and net zero. An amount-assertion correction instead revises original support and is not also a physical debit. The join compares local and provider projections: \mathsf{reconcile}_t(k)= \begin{cases} \mathsf{OrphanLocal},&k\in dom(\alpha_L)\setminus dom(\alpha_P),\\ \mathsf{OrphanProvider},&k\in dom(\alpha_P)\setminus dom(\alpha_L),\\ \mathsf{Matched}(q),&\alpha_L(k)=\alpha_P(k)=q,\\ \mathsf{Break}(\alpha_L(k)-\alpha_P(k)),&\text{otherwise.} \end{cases} \tag{9}

Corrections enter L_t with stable correction keys and references to the corrected occurrence. The fold applies each authorized adjustment once. It updates retained attribution and every affected obligation balance in the same transaction. It preserves every earlier event and attribution receipt.

The proposition is conditional. The bytecode cannot prove statement completeness or the absence of future corrections.

5.11 Global exposure reservations

Linearity prevents one program from copying a request. It does not by itself prevent two programs from each reserving 60 against a shared balance of 100. They need one admission decision over their combined commitments. A reservation records the quantity committed to a command until evidence permits its release or reclassification. Each operation refers to a shared durable reservation ledger. A risk scope g identifies the accountable limit owner and its complete set of covered operations. The scope registry assigns every covered command to that ledger before dispatch. Its complete scope set includes every overlapping limit that the command must satisfy. All issuers sharing a limit use the same reservation authority or a conserved partition of its capacity. An operation-local obstruction carries a receipt for \mathsf{ReservedEffect}(g,asset,u,k,h_{req},v), where u is the current declared exposure and v is the committed ledger version. Pending dispatch, uncertain execution, recognized exposure, reversal exposure, and residual obligations have distinct ledger components. The exposure policy specifies their units, overlap rules, and discharge conditions. Its predispatch envelope covers every admitted continuation under the provider contract. An event reclassifies existing exposure before any release. For example, an 80-unit reservation can become recognized exposure of 50 plus unresolved execution of 30. That reclassification preserves the total of 80.

Let \mathcal L_g[a,k] be the active reserved quantity for asset a and command k. Define U_{g,a}(\mathcal L)=\sum_k\mathcal L_g[a,k]. Prepare atomically tests the current ledger version, inserts the reservation, and commits the immutable outbox entry. Its premise is U_{g,a}(\mathcal L)+u_{g,a,new}\leq Cap_{g,a} \quad\text{for every required pair }(g,a). \tag{10} A repeated command with identical request bytes returns its existing reservation and outbox record. A different request under the same key produces a typed conflict. The dispatcher obtains its permit only from the committed outbox record. It preserves the command key across retransmissions. Before a provider call becomes possible, the dispatcher checks current use-stage authority and atomically changes Prepared to Armed. It verifies the required authority again at actual transmission, including transmission after recovery or retry. Where effect-time authority is required, the declared transaction authorization or provider-enforced effect boundary supplies that condition. A local cancellation can release capacity only by changing Prepared to Cancelled in that same state machine. Exactly one of those transitions can succeed. An Armed entry remains reserved even when the process crashes before the provider call. Its execution right closes through an authenticated provider fence or outcome.

The global machine contains all active operation states and the common command, credit, attribution, funding, reservation, and outbox ledgers. Its risk-reservation component is \mathcal L. Creation and increases serialize against the complete set of risk scopes. Changes commit together against every required scope and asset row. Reclassification and parent-child splits preserve the total reserved quantity. An authenticated discharge decreases that total under the declared exposure policy. A predispatch cancellation releases capacity only while atomically fencing its outbox entry against dispatch. After dispatch, a timeout or process crash preserves the reservation. Release requires authenticated evidence that discharges the relevant exposure. The admission headroom and current excess are \begin{gathered} H_{g,a}=[Cap_{g,a}-U_{g,a}]_+,\\ X_{g,a}=[U_{g,a}-Cap_{g,a}]_+. \end{gathered} \tag{10a} An authoritative limit change updates Cap_{g,a} even when it falls below outstanding reservations. It preserves those reservations and records the resulting X_{g,a}. Every new reservation or increase must fit current admission headroom. A discretionary quota reduction also transfers or releases the affected reservation rights before they can be issued elsewhere. All transitions append durable receipts. Replay verifies those receipts and performs no new reservation or external dispatch.

A federated implementation can allocate disjoint quotas to sovereign kernels, the participating jurisdictional execution runtimes. Within one committed aggregate-limit epoch, the quota authority preserves \sum_j Cap_{g,a,j}\leq Cap_{g,a}. Each kernel applies (10) within its committed quota. A quota transfer locks the sender’s amount before issuing its unique transfer certificate. The receiver activates it once. The sender recovers it only through an authenticated cancellation that fences receiver activation. Both kernels retain the certificate epoch and consumed-transfer record across restart. Summing the local bounds gives the global bound. Partitioned execution continues within each kernel’s committed quota. A successor quota epoch fences further issuance under the preceding epoch before capacity can be reassigned. An externally effective limit reduction remains recordable during that process. It exposes excess against the effective limit and does not erase existing quota commitments. The fixed-epoch quota guarantee and the current-limit excess record are distinct conclusions.

The theorem concerns the declared exposure measure. Physical-position correspondence requires correct quantity contracts, complete event feeds, and an adequate exposure policy. Admission controls cannot suppress contradictory external evidence. An observed exposure above its reservation creates a quantified excess-exposure record and recovery obligation. It does not silently acquire capacity or alter the admitted reservation history. The evidence and exposure records remain available for an authenticated response.

5.12 The structural and semantic claims

7.1 Canonical bytes

Equal records must have equal bytes if replay is to reproduce hashes and signatures. Ordinary JSON (JavaScript Object Notation) permits differences in key order, whitespace, and number spelling that preserve a value while changing its bytes. The executable profile chooses one encoding and rejects the others. It uses UTF-8, a standard encoding of Unicode text, and a closed JSON schema that admits only declared fields. The profile follows the JSON Canonicalization Scheme (JCS) and Internet JSON (I-JSON) admission restrictions [4, 3]. Object names are unique after JSON escape decoding. UTF-16 code units are the 16-bit units of another Unicode encoding; JCS uses their order for object names. NFC denotes Unicode Normalization Form C. The encoder recursively sorts decoded names by unsigned UTF-16 code units. Arrays preserve order. For example, U+10000 sorts before U+E000, despite their opposite Unicode code-point order. Strings use JCS escaping and retain their admitted Unicode sequence. The profile pins Unicode 17.0.0 normalization tables for both implementations. Admission rejects non-NFC strings, unpaired surrogates, and Unicode noncharacters. It performs no normalization rewrite. Canonical round trip rejects alternate escapes, ordering, whitespace, and duplicate names.

JSON numeric tokens admit only exact integers between -(2^{53}-1) and 2^{53}-1. Admission rejects fractional or exponent tokens and negative zero before numeric conversion. This narrower domain has the same number encoding as JCS. Full signed 64-bit application values retain their complete range through an exact string representation:

{"decimal":"9223372036854775807","type":"i64"}

Every field of this type uses the same representation, including small values. Its decimal grammar is 0 or an optional minus followed by a nonzero digit and zero or more decimal digits. The checker consumes the entire string and checks the signed 64-bit range. Money uses this exact integer coefficient with its asset and unit indices. Thus 2^{53}+1 remains exact without entering a binary64 JSON number. Unknown fields and alternate encodings of a typed value reject.

The profile identifier is op:jcs-exact:2. Each digest hashes its profile and object-kind domain separator, one zero byte, and the canonical bytes. Kinds distinguish programs, requests, outcomes, continuations, bundles, policy witnesses, and receipts. The schema and domain identifier bind signatures to this encoding. Existing profile records retain their original bytes and digests. An authenticated migration binds the original record, the target schema, and the newly encoded record. It never reinterprets an existing signature under another profile. Collision resistance and signature unforgeability remain explicit cryptographic assumptions.

The verifier consumes four top-level objects: I=\langle program,inputs,trustRoot,evidenceLog\rangle \quad\text{and a claimed proof bundle }\mathcal{B}_c. \tag{11} The trust root is \Theta from Section 4. It binds every rule pack, registry, revocation view, corridor map, and evaluation time used during replay. The evidence-log object contains the committed epochs, exact admitted prefixes, stream frontiers, and epoch transition receipts.

7.2 Total verifier

The checker must reject a malformed payment record as a defined result, including when parsing or evidence validation fails. The verifier returns one member of \mathsf{Accept}(h)\mid\mathsf{Reject}(code,path,detail). Syntax reject codes cover malformed bytes, noncanonical encoding, unknown fields, type mismatch, and graph cycles. Structural codes cover missing reversals, sanctions bypasses, linear-use errors, and continuation mismatches. Evidence codes cover signatures, authority, revocation, digests, occurrences, log gaps, finality bindings, reconciliation, bundle equality, and resource bounds. There is no undefined result.

The algorithm is:

1. Check byte limits before allocation. Parse each object with duplicate-key rejection and canonical round trip.

2. Validate the closed schema, integer ranges, string normalization, and array limits.

3. Construct the control-flow graph. Reject cycles and unreachable write nodes.

4. Infer types, effect rows, reversal declarations, evidence obligations, and linear contexts by forward data flow. Check dependency footprints, mutation footprints, cursor indices, and finite retention certificates.

5. Compute screening must-facts by predecessor intersection. Check complete edge operands and sanctions subject, jurisdiction, snapshot, and freshness indices at every write.

6. Validate the bilateral session projection, linear locks, Verified-entry invariant, signed decision, acknowledgement, and any blame witness.

7. Validate the trust root and every evidence signature. Check each committed prefix root, stream membership, contiguous frontier, and epoch successor relation. Enforce admitted stream order, authoritative occurrence normalization, and conflict classification. Verify intention, attribution, correction, reservation, and outbox receipts under their declared transition contracts.

8. Replay the deterministic small-step machine. At every suspension, consume only the indexed event from the committed epoch. Advance its continuation version once and check current witnesses at every consumer.

9. Re-encode each emitted receipt, extend the bundle hash chain, and compare every entry with \mathcal{B}_c. Reject missing, reordered, duplicate, or trailing entries.

10. Recompute the seven-coordinate provider state, finality bindings, reconciliation fold, and subsequent-effect graph. Return \mathsf{Accept} only if all comparisons succeed.

A mebibyte (MiB) is 1,048,576 bytes. The reference profile accepts at most 1 MiB of program bytes, 1 MiB of typed inputs, 4 MiB of evidence, and 4 MiB of bundle bytes. It admits at most 4,096 instructions, 8,192 graph edges, 4,096 signed evidence entries, and schema depth 16. These are verifier safety limits, not gas prices.

7.3 Replay in another jurisdiction

Let J_A be the source jurisdiction and J_B the receiver. The receiver first replays under the pinned source trust root. It then evaluates the imported facts under its own pack. The two verdicts remain separate: v_A:\mathsf{Verdict}\langle J_A,p_A,t_A\rangle, \qquad v_B:\mathsf{Verdict}\langle J_B,p_B,t_B\rangle.

A corridor witness specifies which evidence fields can be carried and which domains require fresh evaluation. The receiver never imports the source verdict as its own. When route data disagree, replay returns a typed route-coherence obstruction. The finite normalized checker for direct and staged corridor snapshots is machine-checked in CorridorMonotone.v at public commit fda26c71d75a [6]. Its theorem is limited to normalized snapshot equality. The semantic lift from legal corridor instruments to those snapshots remains open.

The verdict composition and applicability rules belong to the companion compliance paper [5]. Op contributes the typed obstruction and replay boundary.

This theorem does not say that v_A=v_B. Different laws, evaluation times, or fresh facts can produce different local verdicts. It says each verifier agrees on what the source program and evidence actually encode.

7.4 Single-outcome reference adapter

The smallest crash-recovery case has one request and one provider outcome. It isolates whether the client can consume that outcome once while its database and the provider persist independently. The executable reference uses one SQLite client database and a separate persistent provider fixture. Both use explicit transactions, write-ahead logging, and synchronous=FULL. The storage assumption is atomic durable commit on the tested filesystem. The client stores immutable command bytes, a reservation, dispatch state, authenticated inbox outcomes, and committed consumption receipts. The single-step adapter uses the command as its continuation identity. A general continuation additionally indexes the expected prior program version.

Prepare creates the command, reservation, and outbox record in one transaction. Arm conditionally changes Prepared to Armed under current authority. Transmission runs outside that transaction and rechecks current authority. It submits the identical command and bytes. Recovery first queries the provider for an existing authenticated outcome. It can consume an already executed outcome after revocation without creating another effect. The inbox checks authentication and exact command/request binding. Its committed outcome and the unique consumption receipt survive restart. Consumption atomically appends that receipt, marks the command complete, and releases its resolved reservation.

The executable fixture implements its provider contract in a second database. Its fixed authentication key tests message binding rather than cryptographic key custody. Tests terminate child processes at twelve transaction or delivery boundaries, reopen both databases, and recover. They also exercise four concurrent workers, changed request bytes, revoked dispatch authority, and an invalid outcome authenticator. Each recovered positive trace has one fixture effect, one inbox record, one consumption, and a resolved reservation. This establishes the reference adapter’s specified single-step boundary. Production adapters require their actual retention, delivery, authentication, authority, and storage contracts. Full continuation graphs and federated reservations retain their separate refinement obligations.

7.5 Durable partial settlement

The single-outcome adapter cannot express the opening payment’s separate postings, unpaid remainder, and later return. Partial settlement requires a target that outlives its individual commands and a funding pool shared by those commands. A settlement target binds an immutable source, quantity, asset unit, payer account, and payee account. Several commands can contribute to that target. Several targets can use the same funded pool. The durable implementation applies the identity and reservation contracts above to this shared state. Its target identifier can name an obligation or a resolved payoff entitlement. The host admits the source digest, account mapping, and unit scale before dispatch.

The store keeps one current database row for the complete model state. That row contains targets, commands, reservations, authenticated assertions, physical occurrences, allocation records, and continuation positions. Each serialized transaction appends its event and state hash to a journal and replaces that row atomically. Preparing a command creates its immutable request, reservation, and outbox state together. The admission guard checks both pool funding and outstanding unreserved target quantity. Two commands therefore cannot each reserve the same available cash. An adverse backing change remains recordable and exposes any resulting deficit. Existing commitments remain recorded while further reservation and transmission require sufficient funding.

7.6 Executable evidence and model scope

The Python module canonical_profile.py supplies strict byte admission and exact integer encoding. The JavaScript module canonical_profile.mjs independently encodes values and decodes signed integers. The JavaScript oracle encodes already admitted values. The Python parser checks raw bytes before numeric conversion or duplicate-name loss. Their shared vectors cover UTF-16 ordering, Unicode 17 admission, unsafe numeric tokens, and both signed 64-bit endpoints. The module reference_adapter.py supplies the persistent single-step adapter. The test suite test_upgrade.py checks these modules and the composition, epoch, screening, and intent constructions. The module semantic_core.py implements their finite witness transitions, retention certificates, branch operands, and epoch selection. The durable settlement modules model.py and store.py implement the shared-pool transitions in Section 7.5. The modules online.py and replay.py separate provider access from journal reconstruction. Their suite test_durable.py checks partial effects, returns, concurrent reservations, and process recovery. These executable results concern their named finite models.

The accompanying verify_op.py implements a bounded model of the core instructions. Its supplied fixtures exercise:

1. A single-screen dominator check, subject matching, and deferred-write admission.

2. Exhaustive reversal declarations.

3. Exact linear consumption and suspended ownership.

4. Bilateral message order, linear locks, Verified entry, deterministic decision, acknowledgement, and blame extraction.

5. Sorting a supplied evidence set and rejecting stream gaps.

6. Provider-scope authorization, revocation, request-digest binding, and the supplied occurrence-key construction.

7. Provider-only resumption and evidence-type separation.

8. Finality-witness binding across all seven named fields.

9. Deduplication under those supplied keys and exactly one rail-reversal node per accepted key.

10. The supplied partial-outcome and residual-child fixtures.

11. Reconciliation across matched and both orphan cases.

12. The sum of uncertainty entries supplied in one document.

13. append-only proof-bundle replay with failure receipts.

Its self-test first accepts a complete witness. It then injects one defect for each negative branch and requires every mutant to fail with its expected reject code. The model uses deterministic signature fixtures. The test establishes control and binding logic under the fixture assumption. Cryptographic strength remains an external assumption.

The executable model already indexes provider waits by the operation key. Its occurrence-key function also includes command identity, event time, phase, and quantity. Its uncertainty checker has one supplied document as its scope. Those fixtures do not establish the authoritative credit-root or shared-reservation construction. Their signed-integer serializer, single-screen dominance check, and evidence-time sort also differ from the profile specified here. The separate modules above supply the stated canonicalization and durable adapter evidence. Full-language acceptance requires integration of framed contracts, complete branch operands, and committed epochs into the instruction verifier. Full implementation acceptance for Sections 5.3 and 5.11 requires the following refinement cases:

1. Command identity binds the immutable request, provider scope, intent quantity, and authorized execution attempt. The provider can assign its event identifier after dispatch.

2. Authoritative aliases preserve one recipient-credit root across delivery channels. Conflicting event payloads and duplicate funded roots produce explicit discrepancy states.

3. Distinct postings contribute their disjoint quantities once. Cumulative progress contributes no duplicate credit.

4. Spending preserves retained attribution. Authorized reassignment changes both obligation balances atomically. Corrections preserve funded shortfalls and outstanding obligations.

5. Shared reservation and outbox creation are atomic across the complete risk scope. Concurrent admission refines the serialized reference transitions.

6. Crash, retry, partial execution, residual fencing, and retention expiry preserve the correct reservation and execution right.

7. Federated quota transfer preserves a single spending right across crash, partition, cancellation, and receiver activation.

These obligations preserve the useful execution capability and test its compositional guarantees. They require positive execution cases as well as rejection cases. The shared-pool implementation supplies command binding, distinct partial postings, atomic aggregate reservations, and durable recovery cases. It retains the complete target when closure releases an execution reservation. The general correction, alias, federation, and instruction-integration cases require their own admitted transition evidence. The source-level proofs above establish properties of the specified transitions. Executable refinement remains a separate acceptance obligation.

8.1 Typed compliance verdict

Compliance evaluation returns one closed variant: \begin{aligned} \mathsf{ComplianceVerdict}\langle T\rangle={}& \mathsf{Admit}(T,\mathsf{VerdictWitness})\\ &\mid\mathsf{Reject}(\mathsf{Reason},\mathsf{VerdictWitness})\\ &\mid\mathsf{Pending}(\mathsf{SuspensionToken}). \end{aligned} \tag{12}

There is no Boolean coercion. \mathsf{Pending} cannot enter the admitted branch. \mathsf{Reject} carries evidence and emits a failure receipt. \mathsf{Admit} carries the exact witness that the parent runtime must match against a deferred request.

8.2 Writes are deferred requests

VM code has no durable-write opcode. Its only state-changing surface is \mathsf{requestWrite}: \mathsf{Action}\times\mathsf{ReversalDecl}\to \mathsf{Linear}\langle\mathsf{DeferredWrite}\rangle. The return value is a proposal. The parent runtime validates the compliance verdict, subject set, sanctions snapshot, asset authority, reversal declaration, and current state version. It either consumes the proposal into a committed receipt or consumes it into a failure receipt.

fn transfer(a: Asset, to: Party, q: Quantity)
  -> ExecutionReceipt {
  let verdict = compliance_eval(a, to, q);
  match verdict {
    Admit(_, witness) => {
      let req = request_write(
        Transfer(a, to, q),
        Subsequent<RailReversal>);
      parent_commit(req, witness)
    }
    Reject(reason, witness) =>
      failure_receipt("COMPLIANCE_REJECT", reason, witness),
    Pending(token) => suspended_receipt(token)
  }
}

Every branch returns \mathsf{ExecutionReceipt}. A trap, invalid instruction, out-of-resource condition, bad witness, or host refusal also returns a failure receipt before the run terminates. The receipt chain therefore records success, rejection, suspension, and execution failure under one closed terminal type.

8.3 External calls

An asset VM can request an external provider effect only through the seven-coordinate model of Section 5. The VM receives a linear dispatch receipt and then a typed suspension token. Only the parent runtime can verify and inject \mathsf{Authenticated}\langle\mathsf{ProviderOutcome}\rangle. The VM cannot manufacture a callback or inspect an unsigned webhook body as an outcome.

8.4 Gas is an assumption

9.1 Theorems

Theorems 3.4 and 3.5 are static omission-exclusion results. Theorem 3.6 establishes sequential contract soundness for the checked transition system. Theorems 4.1, 4.3, 5.5, and 5.10 are operational safety results. Theorem 7.1 establishes total bounded checking. Theorem 7.2 establishes conditional byte equality across conforming verifiers under explicit cryptographic assumptions. Theorem 5.8 preserves declared capacity across commands, retries, partial outcomes, and residual splits. Proposition 5.4 preserves supported discharge across evidence copies, spending, reassignment, and authorized correction. Their physical interpretation requires the named identity, quantity, completeness, and exposure-policy contracts.

Together they yield the central structural result.

9.2 Conditional consequences

External correspondence requires Proposition 5.12’s assumptions. Stable reconciliation requires Proposition 5.7’s complete-statement premise. Semantic compensation requires a primitive contract proving the named invariant. Cross-jurisdiction legal acceptance requires the receiver’s rule pack and corridor instrument. Provider retry safety requires provider idempotency over the documented key scope and retention window.

None of these consequences is promoted to an unconditional theorem.

9.3 Heuristics

Use independent evidence channels for detection. Set each exposure cap and its discharge policy for the complete covered operation set. Choose short authority and revocation snapshot windows. Review forward and reversal declarations together. Treat orphan provider events as investigation priorities because they can indicate hidden external effects.

These practices improve operation quality. They do not change the formal guarantee.

10.1 Payment systems

The Principles for Financial Market Infrastructures separate legal basis, settlement finality, money settlements, exchange-of-value settlement, and operational risk in Principles 1, 8, 9, 12, and 17 [7]. That separation motivates distinct Op evidence types. One provider message cannot silently discharge all five questions.

Article 4A of the Uniform Commercial Code (UCC) distinguishes payment-order acceptance, execution, payment by the sender, and payment to the beneficiary [9]. The Federal Reserve Banks’ operating circular applies those rules to Fedwire Funds Service transfers and states system-specific finality conditions [10]. The Board of Governors describes Fedwire as a real-time gross settlement system. It states that transfers are immediate, final, and irrevocable once processed [11]. A policy for that rail can require the authenticated processed outcome and the controlling rule. A rail that permits ordinary returns after a provider reports success needs a different policy witness. Thus a system record, provider outcome, legal finality, and beneficiary receipt can occur at different legal moments.

A settlement asset is a separate legal predicate. Its policy names the asset, issuer or custodian, eligible holders, redemption terms, transfer rule, and governing law. Central-bank money and commercial-bank money carry finality points under their own rulebooks. A tokenized claim on an issuer, bank, or custodian remains a claim on that party. Its ledger confirmation rule does not establish legal finality or redemption into bank money. Guidance from the Committee on Payments and Market Infrastructures and the International Organization of Securities Commissions separates ledger state from legal finality [8]. That guidance also applies distinct settlement-asset analysis. Du, Huang, and Scharfstein document a February 2026 issuer route with standard T+1 redemption and a fee for expedited same-day redemption [2, Section 7.2]. The model records the token transfer and redemption as separate operations under separate policies. The same rule separates a metal-account transfer from physical release or delivery. Allocated Title applies provider finality to the cash and custody legs of allocated metal [32].

The European payment-services regime similarly separates execution obligations from refund rights for unauthorized or incorrectly executed transactions [12]. Electronic-money redemption under the second Electronic Money Directive is another claim with its own legal basis [13]. A refund or redemption can therefore be a subsequent operation without negating the historical payment occurrence.

The International Organization for Standardization publishes ISO 20022, which defines structured financial-message semantics and business-process syntax [14]. It does not, by message shape alone, decide which jurisdictional rule makes a transfer final. Op treats an ISO 20022 message as typed evidence whose legal use still requires T-Finality.

10.2 Securities and custody

UCC Article 8 distinguishes securities, security entitlements, entitlement orders, and the duties of securities intermediaries [15]. A ledger entry and an entitlement against an intermediary are therefore different objects. The provider scope names the asset and rulebook so that an outcome cannot cross that distinction by accident.

The London Bullion Market Association distinguishes allocated and unallocated precious-metal accounts in its market materials [16]. An allocated holding, an unallocated claim, a provider statement, and physical receipt have different evidence requirements. The seven-coordinate model can carry those differences without adding a metal-specific state machine.

Narrow-banking proposals separate payment utility from balance-sheet risk by constraining the assets behind transaction liabilities [17]. Op does not make a provider solvent or an asset bankruptcy remote. It only prevents the workflow from treating an operational message as proof of those legal or balance-sheet properties.

10.3 Long-running computation

Sagas attach compensating actions to committed subtransactions [18]. Helland explains why systems beyond distributed transactions must use messages, activities, idempotence, and commutative or compensating work [19]. Op adds static reversal declarations, typed evidence, and an immutable subsequent-effect graph. It does not claim that every compensation is an inverse.

The Hypertext Transfer Protocol (HTTP) carries client requests to a server. The Internet Engineering Task Force has a working group for HTTP application programming interfaces (HTTPAPI). Its draft defines a request key that makes retry intent explicit at an HTTP boundary [20]. Such a key is useful but insufficient. The provider must honor a documented equality scope and retention interval. Accordingly, provider idempotency remains an assumption in Section 5.

10.4 Typed bytecode and evidence

Typed assembly and proof-carrying code show how low-level programs can carry machine-checkable safety facts [21, 22]. The Java Virtual Machine (JVM) verifier demonstrates total structural checking before execution [23, 24]. Op adds institutional effects, complete path screening, reversal declarations, evidence-indexed suspension, and proof-bundle replay.

The fixed effect rows follow the type-and-effect tradition [25]. They are finite capability sets, not algebraic-effect handlers. The linear context follows linear logic and resource-aware bytecodes [27, 28]. The paper’s contribution is their joint use at an external evidence boundary.

External truth and event completeness.

The external-correspondence proposition assumes that admitted evidence correctly describes a complete event stream. An adversarial semantics must classify authenticated falsehoods, omissions, and inconsistent streams, then bind each class to a supervisory or contractual remedy.

Legal-policy verification.

A legal-policy module must formalize statute, system, insolvency rule, authority, and evaluation time without reducing legal judgment to a mechanical constant.

Provider retry semantics.

Provider conformance tests must identify retention windows, deduplication scope, failover behavior, and dispute evidence because local operation keys cannot prove them.

Confidential replay.

Confidential replay needs an observer model, declassification rules, and proof that redaction or zero-knowledge compression preserves the required verification result.

Concurrency and isolation.

Section 5.11 gives the serialized reservation construction and its concurrent refinement condition. An implementation must establish that refinement under its actual transaction, outbox, recovery, and quota-transfer mechanisms. Parallel bytecode execution also requires resource disjointness, a memory model, and provider isolation contracts.

Multilateral commitment.

Multilateral commitment remains open for session composition, lock ordering, Byzantine blame, and nonblocking partition liveness beyond Section 3.8’s bilateral result.

Gas calibration.

Gas calibration requires measured instruction costs, signature-check prices, payer liability, and resistance to underpriced inputs under the positive-metering assumption.

Rule-language compilation.

Source-language compilation must preserve the companion paper’s typed verdicts, evidence dependencies, authority scopes, and evaluation times without reinterpreting their legal content.

Executable supplement.

The accompanying archive op-supplement.zip contains the executable reference sources and fixtures described in this paper. Its README specifies the dependencies and reproduction commands. The archive includes a SHA-256 file manifest.

SHA-256:64d85cda09c5c1dadc876091ca514d5b9b09aede15529b95e785ae37f73662f4