Paper 2025/592

Deterministic State Machines as Guarded Linear Constraint Systems: Double-spend prevention as a state property

Abstract

This paper formalizes the Deterministic State Machine, or DSM, as a guarded, linear, forward only, constraint based computation model. DSM does not require a blockchain, validator set, sequencer, gas market, mempool, clock based ordering rule, or global consensus layer for ordinary state evolution. State validity is determined by local verification of cryptographically precommitted candidate futures, deterministic fulfillment guards, explicit resource consumption keys, canonical encodings, signatures, and Sparse Merkle Tree commitments. The architectural shift is that finality moves from a network decision to a state property. Instead of requiring some external party, committee, sequencer, validator set, or global clock to agree that a transition happened, DSM asks whether the proposed transition consumes the committed state resource and advances it deterministically. If it does, the successor is locally realized. If it does not, it is not state. Finality is therefore not provided as a service by an ordering network; it is a consequence of the consumed resource itself. This is global realization without global ordering: local acceptance composes into a coherent realized history because incompatible histories cannot merge. The central claim is not that DSM forbids all branching at the level of precommitment. DSM explicitly permits precommitment forking. Multiple candidate futures may be prepared for a common parent, including Deterministic Limbo Vault release paths, refund paths, hash fulfillment paths, recovery paths, abort paths, contingent payment paths, CPTA token operations, offline bearer steps, and other mutually exclusive branches. The invariant is: multiple futures may be described, but for a fixed consumed resource, at most one may be realized. A resource is the thing that produces exactly one realized successor. A relationship parent, spendable object, vault generation, token balance object, source vault generation, recovery generation, or offline anchor step is a resource in this sense. Candidate branches are only possible futures. Realization consumes the resource. A generation is a logical version of a resource family. It is not a time period, not a clock interval, not a scheduling unit, and not an external ordering coordinate. Generations are ordered only by DSM derivability and resource consumption. This paper makes explicit the machinery required for that statement. Guard exclusivity is not left as convention. A DSM precommit set is valid only if its guard family is well formed. A well formed guard family gives either a deterministic branch selector, a mechanically proven exclusive guard class, or a set of branch predicates that are structurally tied to the same consumed resource. Parent consumption is modeled through canonical resource consumption keys and a consumed parent set committed by the DSM root. Branch local keys may exist for indexing or audit, but the shared resource key is what enforces linear exclusion. A hardened form of the model is also stated: for any conflict class, all conflicting candidates must resolve to an identical canonical resource consumption set, and those keys must be derived from the committed parent state rather than supplied as discretionary branch data. This removes the implementation hazard where release, refund, recovery, or policy branches accidentally consume different keys. The role of guard exclusivity is clarified. Pairwise guard exclusivity is useful and required for guard classes that claim exclusive fulfillment, but it is not the only safety mechanism. When conflicting branches share the same derived resource consumption key set, linearity alone prevents co realization even if several guards are simultaneously fulfilled. Thus the load bearing safety rule is not merely that guards should not overlap. The load bearing safety rule is that conflicting futures must fight over the same derived resource. Tripwire is formalized as the theorem that two conflicting realized successors from the same consumed resource cannot both be derivable. More precisely, conflicting candidates may be constructed or transmitted as bytes, but they cannot both validate under the DSM step predicate and cannot both go through as accepted state transitions for the same consumed resource. Forks are therefore not selected against by consensus. They are excluded by guarded realization and exposed by reconciliation if conflicting invalid bytes are presented outside the valid model. Offline bearer mode is treated as an optional mode predicate, and this revision states its corrected form. Transfer uniqueness, including offline transfer uniqueness, is a software theorem of the guarded linear kernel. An SMT committed anchor counter makes the offline origin an explicit coordinate of the committed state, every offline candidate from that origin consumes the same derived anchor step resource key, and realized history uniqueness applies without a hardware term. Hardware is thereby demoted to the one job software cannot perform: uniqueness of the physical device instance. Every offline release carries a three factor identity witness, a seed rooted DSM signature, a PUF rooted non exportable chip signature, and a partition sealed host signature over the same root advance message, and the physical monotonic counter survives only as a tracker of the SMT counter: a non rewind floor, a stale image tripwire, and an offline exposure cap. The receiver witnessed counter positioned commit of earlier drafts is superseded: a scalar counter read never binds the transition it brackets, and the binding was never needed. The safety theorems of this paper are supported by machine checked artifacts. The general key scoped fork exclusion theorems are proved in Lean 4 over an abstract guarded model, with the uniqueness and Tripwire core depending on no axioms. A companion TLA${}^{+}$ development model checks the same statements in both a per state form and a realized history form on concrete guard families, and by deliberate falsification of a malformed family confirms that guard family well formedness is load bearing. A relationship scoped model checks that same parent multi receiver forks are unconstructible in online DSM. Appendices A and B point to these artifacts. Their exact scope and boundary are stated in the Claim Boundary section.