From 7da2f4df1296980eb38a7e9dd7e7dbe09a0c2974 Mon Sep 17 00:00:00 2001 From: Vasilis Nasopoulos Date: Wed, 5 Aug 2026 13:27:58 +0300 Subject: [PATCH 1/6] Add Vortex DSE specifications Deterministic slot-based admission with a separate per-slot agreement layer: a message carries its own slot stamp and each node decides admission locally, with no leader, quorum or vote. Two admission modes are specified because both are implemented: the default admits a late message into its own slot, while the opt-in TTL mode rejects it permanently to bound memory. Vortex_DSE_CSlot_AE is specified over the TTL mode; the README says so rather than implying it composes with the default. Six TLC models, all completing in under four seconds. Three TLAPS modules discharging 194, 131 and 34 obligations, all exit 0 under tlapm --strict with no OMITTED steps. Co-authored-by: Claude Opus 5 Signed-off-by: Vasilis Nasopoulos --- README.md | 1 + .../VortexDSE/MC_Vortex_DSE_CSlot.cfg | 18 ++ .../VortexDSE/MC_Vortex_DSE_CSlot.tla | 8 + .../VortexDSE/MC_Vortex_DSE_CSlot_AE.tla | 22 ++ .../MC_Vortex_DSE_CSlot_AE_liveness.cfg | 13 + .../VortexDSE/MC_Vortex_DSE_CSlot_AE_tiny.cfg | 17 + specifications/VortexDSE/README.md | 68 ++++ specifications/VortexDSE/Vortex_DSE_CSlot.tla | 242 ++++++++++++++ .../VortexDSE/Vortex_DSE_CSlot_AE.tla | 270 ++++++++++++++++ .../VortexDSE/Vortex_DSE_CSlot_AE_Proofs.tla | 59 ++++ .../Vortex_DSE_CSlot_ExactlyOnce_Proof.tla | 297 ++++++++++++++++++ .../VortexDSE/Vortex_DSE_CSlot_Proofs.tla | 264 ++++++++++++++++ .../VortexDSE/Vortex_DSE_CSlot_Skew.tla | 147 +++++++++ .../VortexDSE/Vortex_DSE_CSlot_Skew_tiny.cfg | 18 ++ .../VortexDSE/Vortex_DSE_CSlot_TTL.tla | 240 ++++++++++++++ .../Vortex_DSE_CSlot_TTL_liveness.cfg | 13 + .../VortexDSE/Vortex_DSE_CSlot_TTL_tiny.cfg | 18 ++ specifications/VortexDSE/manifest.json | 115 +++++++ 18 files changed, 1830 insertions(+) create mode 100644 specifications/VortexDSE/MC_Vortex_DSE_CSlot.cfg create mode 100644 specifications/VortexDSE/MC_Vortex_DSE_CSlot.tla create mode 100644 specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE.tla create mode 100644 specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_liveness.cfg create mode 100644 specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_tiny.cfg create mode 100644 specifications/VortexDSE/README.md create mode 100644 specifications/VortexDSE/Vortex_DSE_CSlot.tla create mode 100644 specifications/VortexDSE/Vortex_DSE_CSlot_AE.tla create mode 100644 specifications/VortexDSE/Vortex_DSE_CSlot_AE_Proofs.tla create mode 100644 specifications/VortexDSE/Vortex_DSE_CSlot_ExactlyOnce_Proof.tla create mode 100644 specifications/VortexDSE/Vortex_DSE_CSlot_Proofs.tla create mode 100644 specifications/VortexDSE/Vortex_DSE_CSlot_Skew.tla create mode 100644 specifications/VortexDSE/Vortex_DSE_CSlot_Skew_tiny.cfg create mode 100644 specifications/VortexDSE/Vortex_DSE_CSlot_TTL.tla create mode 100644 specifications/VortexDSE/Vortex_DSE_CSlot_TTL_liveness.cfg create mode 100644 specifications/VortexDSE/Vortex_DSE_CSlot_TTL_tiny.cfg create mode 100644 specifications/VortexDSE/manifest.json diff --git a/README.md b/README.md index 0e4a22cb..837ba788 100644 --- a/README.md +++ b/README.md @@ -108,6 +108,7 @@ Here is a list of specs included in this repository which are validated by the C | [DAG-based Consensus](specifications/dag-consensus) | Giuliano Losa | | | ✔ | ✔ | | | [German Cache-Coherence Protocol](specifications/GermanProtocol) | Markus Kuppe | | | | ✔ | ✔ | | [FLASH Cache-Coherence Protocol](specifications/FlashProtocol) | Markus Kuppe | | | | ✔ | ✔ | +| [Vortex DSE](specifications/VortexDSE) | Vasilis Nasopoulos | | ✔ | | ✔ | | ## Other Examples diff --git a/specifications/VortexDSE/MC_Vortex_DSE_CSlot.cfg b/specifications/VortexDSE/MC_Vortex_DSE_CSlot.cfg new file mode 100644 index 00000000..acfc46b1 --- /dev/null +++ b/specifications/VortexDSE/MC_Vortex_DSE_CSlot.cfg @@ -0,0 +1,18 @@ +\* TLC model configuration for Vortex_DSE_CSlot. +\* Two nodes, two message ids, slot horizon 2 — bounded but non-trivial. + +CONSTANT +Nodes = {n1, n2} +MsgIDs = {m1, m2} +MaxSlot = 2 + +INIT Init +NEXT Next + +INVARIANT TypeInvariant +INVARIANT NoFutureAdmission +INVARIANT ExactlyOncePerNode +INVARIANT NoPhantomProcess +INVARIANT DecisionLocalityOnly + +CONSTRAINT StateConstraint diff --git a/specifications/VortexDSE/MC_Vortex_DSE_CSlot.tla b/specifications/VortexDSE/MC_Vortex_DSE_CSlot.tla new file mode 100644 index 00000000..26879b51 --- /dev/null +++ b/specifications/VortexDSE/MC_Vortex_DSE_CSlot.tla @@ -0,0 +1,8 @@ +---- MODULE MC_Vortex_DSE_CSlot ---- +(* TLC bounded model-checking harness for Vortex_DSE_CSlot. *) +(* Constants are assigned in MC_Vortex_DSE_CSlot.cfg: *) +(* Nodes = {n1, n2} *) +(* MsgIDs = {m1, m2} *) +(* MaxSlot = 2 *) +EXTENDS Vortex_DSE_CSlot +==== diff --git a/specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE.tla b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE.tla new file mode 100644 index 00000000..472138c8 --- /dev/null +++ b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE.tla @@ -0,0 +1,22 @@ +---------------- MODULE MC_Vortex_DSE_CSlot_AE ---------------- +(* Apalache harness for Vortex_DSE_CSlot_AE. *) +(* Fixes constants and bundles the safety invariants for a single *) +(* symbolic (SMT-backed) check via Apalache. *) + +EXTENDS Vortex_DSE_CSlot_AE + +ConstInit == + /\ Nodes = {"n1", "n2"} + /\ MsgIDs = {"a", "b"} + /\ MaxSlot = 1 + +\* Conjunction of every safety invariant in the module. +AllInv == + /\ TypeInvariant + /\ MerkleAgreement + /\ CommittedSupersetsProcessed + /\ NoPhantomInCommitted + /\ NoReorderAcrossCslot + /\ PhaseProgressionValid + +=============================================================== diff --git a/specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_liveness.cfg b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_liveness.cfg new file mode 100644 index 00000000..1ea3fefe --- /dev/null +++ b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_liveness.cfg @@ -0,0 +1,13 @@ +SPECIFICATION LiveSpec + +CONSTANTS + Nodes = {n1, n2} + MsgIDs = {m1} + MaxSlot = 1 + +PROPERTIES + EventualCommit + EventualAgreement + +CONSTRAINT + StateConstraint diff --git a/specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_tiny.cfg b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_tiny.cfg new file mode 100644 index 00000000..a18a6543 --- /dev/null +++ b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_tiny.cfg @@ -0,0 +1,17 @@ +SPECIFICATION Spec + +CONSTANTS + Nodes = {n1, n2} + MsgIDs = {m1, m2} + MaxSlot = 2 + +INVARIANTS + TypeInvariant + MerkleAgreement + CommittedSupersetsProcessed + NoPhantomInCommitted + NoReorderAcrossCslot + PhaseProgressionValid + +CONSTRAINT + StateConstraint diff --git a/specifications/VortexDSE/README.md b/specifications/VortexDSE/README.md new file mode 100644 index 00000000..14e8ff8c --- /dev/null +++ b/specifications/VortexDSE/README.md @@ -0,0 +1,68 @@ +# Vortex DSE — C-slot admission and per-slot agreement + +Vortex DSE is a deterministic consensus protocol in which a message carries its +own slot stamp and each node decides admission locally, against its own clock. +There is no leader, no quorum and no vote: admission is an O(1) local predicate, +and cross-node agreement on the per-slot input set is established afterwards by +a separate layer. + +These specifications model that structure. They are the formal counterpart of a +running implementation; the implementation itself is not part of this +contribution. + +## Two admission modes + +The protocol has two admission rules, and the difference is one operator. + +| module | rule | meaning | +| --- | --- | --- | +| `Vortex_DSE_CSlot` | `m.cslot <= current_slot` | the default. A message stamped for slot *k* that arrives late is still admitted, into slot *k*. Nothing is dropped. | +| `Vortex_DSE_CSlot_TTL` | `m.cslot = current_slot` | an opt-in bounded-memory mode. A message that misses its slot is rejected permanently, so state does not grow behind the frontier. | + +Both modes are specified because both are implemented; the strict rule is a +memory concession, not a stronger version of the protocol. + +## Modules + +| module | what it adds | +| --- | --- | +| `Vortex_DSE_CSlot` | admission, crash and rejoin via a persisted snapshot | +| `Vortex_DSE_CSlot_Proofs` | `TypeCorrect`, `NoFutureAdmissionCorrect` | +| `Vortex_DSE_CSlot_ExactlyOnce_Proof` | `StrictExactlyOnceCorrect` | +| `Vortex_DSE_CSlot_TTL` | the strict admission mode | +| `Vortex_DSE_CSlot_Skew` | replaces the single global slot with a per-node clock, plus Byzantine injection of forged slot stamps and origins | +| `Vortex_DSE_CSlot_AE` | the agreement layer: `Freeze`, `Reconcile`, `Commit` over the strict mode | +| `Vortex_DSE_CSlot_AE_Proofs` | deductive proofs for the agreement layer | + +`Vortex_DSE_CSlot_AE` is specified over the strict admission rule; it is not a +refinement of the default mode. Extending it to the late-tolerant rule requires +restating what "no reordering across slots" means, and is not done here. + +## What is checked + +All TLAPS proofs discharge under `tlapm --strict`, which fails on unproved +obligations and on proof steps left open — a plain `tlapm` invocation exits 0 +in both cases. There are no `OMITTED` steps in these modules. + +| | obligations | +| --- | --- | +| `Vortex_DSE_CSlot_Proofs` | 194 | +| `Vortex_DSE_CSlot_ExactlyOnce_Proof` | 131 | +| `Vortex_DSE_CSlot_AE_Proofs` | 34 | + +Every model completes in a few seconds. `Vortex_DSE_CSlot_AE` also carries +Apalache type annotations, but no symbolic model is registered here; the models +below are TLC only. + +## Scope + +`Vortex_DSE_CSlot_Skew` bounds pairwise clock skew structurally, by forbidding +any tick that would breach the bound. It states the assumption; it does not +model the mechanism that maintains it. Likewise `Reconcile` is a single atomic +step at specification level — the multi-round protocol underneath is out of +scope here. + +Source repositories, including the whitepaper and the model-checking logs: + + +Prepared with AI assistance. diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot.tla b/specifications/VortexDSE/Vortex_DSE_CSlot.tla new file mode 100644 index 00000000..d74aae38 --- /dev/null +++ b/specifications/VortexDSE/Vortex_DSE_CSlot.tla @@ -0,0 +1,242 @@ +---------------------- MODULE Vortex_DSE_CSlot ---------------------- +(***************************************************************************) +(* Vortex DSE — Deterministic C-Slot Admission (V. Nasopoulos) *) +(* *) +(* C-slot law : *) +(* C_slot(TX) = floor( (T_hw - T_0) / Delta_t ) *) +(* *) +(* Admission rule (DEFAULT no-flag build — matches the running C code): *) +(* place tx into bucket[tx.C_slot]; admit once that slot is reached. *) +(* *) +(* A message keeps its OWN content-derived C_slot and is admitted into *) +(* THAT slot. Late delivery (the slot already passed) is NOT dropped — it *) +(* is admitted into its own (earlier) slot. Nothing is lost. No leader, *) +(* no quorum, no vote. *) +(* *) +(* The strict "one slot late => permanent reject" rule is NOT the default. *) +(* It is re-introduced only as the OPT-IN --ttl window (bounded memory), *) +(* which deliberately drops messages too far behind the frontier. *) +(* *) +(* Async hostile environment modeled: *) +(* - arbitrary message reordering (network is a SET), *) +(* - unbounded delivery delay (Process is nondeterministic), *) +(* - node crashes and rejoins (state survives only via mmap snapshot), *) +(* - adversarial duplicate injection (replay attack). *) +(* *) +(* T_0 = 0 by normalization. We model integer slots directly: each ts is *) +(* already the C_slot index of the message (i.e. ts = floor(T_hw/Delta_t)).*) +(* current_time IS the current slot index. Tick advances the slot by 1. *) +(***************************************************************************) + +EXTENDS Naturals, FiniteSets + +CONSTANTS + \* @type: Set(Str); + Nodes, \* finite set of node identifiers + \* @type: Set(Str); + MsgIDs, \* finite set of distinct message identifiers + \* @type: Int; + MaxSlot \* slot horizon (state-space bound) + +VARIABLES + \* @type: Int; + current_slot, + \* @type: Set({ id: Str, cslot: Int }); + network, \* in-flight messages (SET = no ordering) + \* @type: Str -> Set(Str); + processed, \* processed[n] = msg ids node n has admitted + \* @type: Str -> Set(Str); + persisted, \* persisted[n] = mmap snapshot (survives crash) + \* @type: Str -> Str; + node_state \* node_state[n] \in {"up", "down"} + +vars == <> + +MsgRecord == [id: MsgIDs, cslot: 0..MaxSlot] + +------------------------------------------------------------------------------- +(* INITIAL STATE *) + +Init == + /\ current_slot = 0 + /\ network = {} + /\ processed = [n \in Nodes |-> {}] + /\ persisted = [n \in Nodes |-> {}] + /\ node_state = [n \in Nodes |-> "up"] + +------------------------------------------------------------------------------- +(* ACTIONS *) + +\* Submit: sender stamps T_hw, which yields cslot = current_slot at emission. +\* Network may deliver this arbitrarily later (no ordering, no time bound). +Submit(id) == + /\ id \in MsgIDs + /\ id \notin {m.id : m \in network} + /\ \A n \in Nodes : id \notin processed[n] + /\ network' = network \cup {[id |-> id, cslot |-> current_slot]} + /\ UNCHANGED <> + +\* C-SLOT ADMISSION (default build — late tolerated, nothing dropped). +\* Local, O(1) decision. The node admits m iff it has not already been +\* processed AND the slot the message belongs to has been reached +\* (m.cslot <= current_slot). The message keeps its own C_slot. +\* Late delivery (m.cslot < current_slot) is ADMITTED, not dropped: it is +\* placed into its own (earlier) slot. Nothing is lost. +\* Future-dated (m.cslot > current_slot) waits: it cannot be admitted +\* before the ticker reaches its slot (that slot has not happened yet). +Process(n, m) == + /\ n \in Nodes + /\ m \in network + /\ node_state[n] = "up" + /\ m.id \notin processed[n] \* exactly-once guard (local) + /\ m.cslot <= current_slot \* admit present OR late (own slot) + /\ processed' = [processed EXCEPT ![n] = @ \cup {m.id}] + /\ UNCHANGED <> + +\* CRASH: node loses RAM. mmap snapshot in `persisted` survives. +Crash(n) == + /\ n \in Nodes + /\ node_state[n] = "up" + /\ persisted' = [persisted EXCEPT ![n] = processed[n]] + /\ node_state' = [node_state EXCEPT ![n] = "down"] + /\ processed' = [processed EXCEPT ![n] = {}] + /\ UNCHANGED <> + +\* REJOIN: node recovers from mmap snapshot. processed = persisted. +Rejoin(n) == + /\ n \in Nodes + /\ node_state[n] = "down" + /\ processed' = [processed EXCEPT ![n] = persisted[n]] + /\ node_state' = [node_state EXCEPT ![n] = "up"] + /\ UNCHANGED <> + +\* Adversarial duplicate / replay injection. +\* Attacker injects a message with arbitrary cslot value (past, present, +\* or future). The C-slot gate must still hold. +DuplicateInject(id, fake_cslot) == + /\ id \in MsgIDs + /\ fake_cslot \in 0..MaxSlot + /\ network' = network \cup {[id |-> id, cslot |-> fake_cslot]} + /\ UNCHANGED <> + +\* Slot ticker advances by 1. +Tick == + /\ current_slot < MaxSlot + /\ current_slot' = current_slot + 1 + /\ UNCHANGED <> + +Next == + \/ \E id \in MsgIDs : Submit(id) + \/ \E n \in Nodes, m \in network : Process(n, m) + \/ \E n \in Nodes : Crash(n) + \/ \E n \in Nodes : Rejoin(n) + \/ \E id \in MsgIDs, k \in 0..MaxSlot : DuplicateInject(id, k) + \/ Tick + +Spec == Init /\ [][Next]_vars + +------------------------------------------------------------------------------- +(* TYPE INVARIANT *) + +TypeInvariant == + /\ current_slot \in 0..MaxSlot + /\ network \subseteq MsgRecord + /\ processed \in [Nodes -> SUBSET MsgIDs] + /\ persisted \in [Nodes -> SUBSET MsgIDs] + /\ node_state \in [Nodes -> {"up", "down"}] + +------------------------------------------------------------------------------- +(* CORE SAFETY INVARIANTS *) + +\* I1: EXACTLY-ONCE PER NODE. +\* No node processes the same id twice (set semantics + guard). +ExactlyOncePerNode == + \A n \in Nodes : Cardinality(processed[n]) <= Cardinality(MsgIDs) + +\* I2: NO FUTURE ADMISSION (the headline safety property). +\* A node never admits a message whose slot has not yet been reached. +\* The gate is m.cslot <= current_slot and current_slot is monotonic, +\* so every admitted id has a network record whose cslot lies in +\* [0, current_slot]: a real, present-or-past slot, never future-dated. +\* Late messages (cslot < current_slot) ARE admitted here (into their +\* own slot) — that is intended; only future-dated admission is barred. +NoFutureAdmission == + \A n \in Nodes : \A id \in processed[n] : + \E m \in network : m.id = id /\ m.cslot <= current_slot + +\* I3: PERSISTED REFLECTS REALITY. +\* mmap snapshot never invents ids that were not in the network. +PersistedReflectsReality == + \A n \in Nodes : + node_state[n] = "down" => + persisted[n] \subseteq {m.id : m \in network} + +\* I4: NO PHANTOM PROCESS. +\* Every processed id corresponds to a real network record. +NoPhantomProcess == + \A n \in Nodes : processed[n] \subseteq {m.id : m \in network} + +\* I5: DECISION LOCALITY. +\* If two nodes have both processed id, that id exists in network. +\* Structural consequence: the gate depends only on (m.cslot, current_slot), +\* not on n. Same (m.cslot, current_slot) => same decision at every node. +DecisionLocalityOnly == + \A n1, n2 \in Nodes : \A id \in MsgIDs : + (id \in processed[n1] /\ id \in processed[n2]) => + (\E m \in network : m.id = id) + +------------------------------------------------------------------------------- +(* STATE-SPACE CONSTRAINT *) + +StateConstraint == + current_slot <= MaxSlot + +------------------------------------------------------------------------------- +(* LIVENESS LAYER *) +(* *) +(* DESIGN NOTE — fairness assignment is intentional: *) +(* *) +(* - SF(Tick): the slot ticker is fair, advancing eventually. This is a *) +(* physical-hardware assumption (the ticker process does not stall *) +(* forever). Strong fairness because Tick is always enabled until *) +(* current_slot reaches MaxSlot. *) +(* *) +(* - WF(Rejoin(n)) per node: a crashed node, given the chance, eventually *) +(* rejoins. This corresponds to operational recovery (operator restart). *) +(* *) +(* - SF(Process(n)): fairness ON Process. This matches the default code, *) +(* where a late message is NOT dropped but admitted into its own slot. *) +(* Strong fairness (not weak) because a crash intermittently disables *) +(* Process; SF guarantees that a message enabled infinitely often is *) +(* eventually admitted. This is what recovers VALIDITY: every TX that *) +(* reaches the network is eventually admitted by every up node. *) +(* *) +(* - NO fairness on Submit / DuplicateInject. Submit is a user action; *) +(* adversary injection is, by definition, not fair. *) +(***************************************************************************) + +Fairness == + /\ SF_vars(Tick) + /\ \A n \in Nodes : WF_vars(Rejoin(n)) + /\ \A n \in Nodes : SF_vars(\E m \in network : Process(n, m)) + +LiveSpec == Init /\ [][Next]_vars /\ Fairness + +\* L1 TICK PROGRESS. +\* Under SF(Tick), the slot counter eventually reaches the horizon. +TickProgress == <>(current_slot = MaxSlot) + +\* L2 EVENTUAL REJOIN. +\* Every crashed node eventually returns to "up", under WF(Rejoin(n)). +EventualRejoin == + \A n \in Nodes : (node_state[n] = "down") ~> (node_state[n] = "up") + +\* L3 EVENTUAL ADMISSION (VALIDITY — the property the new rule recovers). +\* Once a message is in the network, every node eventually admits it. +\* Nothing is permanently dropped: late messages reach their own slot. +\* This is exactly what the strict drop-late spec could NOT claim. +EventualAdmission == + \A n \in Nodes : \A id \in MsgIDs : + (\E m \in network : m.id = id) ~> (id \in processed[n]) + +============================================================================= diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot_AE.tla b/specifications/VortexDSE/Vortex_DSE_CSlot_AE.tla new file mode 100644 index 00000000..23593276 --- /dev/null +++ b/specifications/VortexDSE/Vortex_DSE_CSlot_AE.tla @@ -0,0 +1,270 @@ +-------------------- MODULE Vortex_DSE_CSlot_AE -------------------- +(***************************************************************************) +(* Vortex DSE — Agreement Extension Layer (L4) *) +(* *) +(* Companion module to Vortex_DSE_CSlot.tla. The core module models the *) +(* C-slot strict admission gate (per-node, per-message) plus crash/rejoin *) +(* via mmap snapshot. This module adds the per-cslot Agreement Extension *) +(* (AE) phase: after admission, live nodes Freeze their local processed *) +(* set, Reconcile via an abstract AE protocol (in implementation: Bloom *) +(* round + repeated Merkle/hashlist), and Commit a cslot-final input set *) +(* that is bit-identical across all correct live nodes. *) +(* *) +(* The headline property (MerkleAgreement) is the formal counterpart of *) +(* the claim: "all live nodes converge on the same input set per cslot, *) +(* cryptographically verified via Merkle root". *) +(* *) +(*--------------------------------------------------------------------------*) +(* SCOPE DELIMITATION (important): *) +(* *) +(* This module deliberately does NOT model crash/rejoin. The core module *) +(* Vortex_DSE_CSlot.tla already covers crash semantics via the persisted *) +(* mmap snapshot. Composing the two failure models in one module conflates*) +(* two concerns: AE freeze/reconcile correctness vs. crash recovery *) +(* bookkeeping. Initial attempt to combine them produced a spurious *) +(* counterexample (TLC trace 2026-05-27): a rejoin advanced a node to *) +(* "committed" while its processed view was stale, violating *) +(* CommittedSupersetsProcessed. The clean separation is: *) +(* *) +(* - Core module: admission + persistence under crash *) +(* - This module: agreement under bounded network loss, all-live *) +(* - Future composed module: cross-cuts both (out of scope here) *) +(* *) +(*--------------------------------------------------------------------------*) +(* ENVIRONMENTAL ASSUMPTIONS (kept out of the state machine, declared *) +(* here so they are visible at spec level): *) +(* *) +(* A1. Bounded clock skew. Let Delta_t be the slot duration and let *) +(* Delta_skew be the maximum pairwise wall-clock drift between any *) +(* two correct nodes. We require: *) +(* *) +(* Delta_skew < Delta_t / 2 *) +(* *) +(* Justification: the admission gate is m.cslot = node.current_slot. *) +(* A producer stamps m.cslot from its own clock; a consumer evaluates *) +(* the gate from its own clock. If skew < Delta_t/2, then at any *) +(* real-time instant all correct nodes observe the same current_slot *) +(* modulo edge transitions, so a message admitted by one correct *) +(* node is admissible by every other correct node that receives it *) +(* in time. This justifies abstracting the per-node clock as a *) +(* single global current_slot variable. *) +(* *) +(* A2. Freeze barrier within slot. The AE phase runs in the residual *) +(* portion of the slot after the admission deadline. This module *) +(* abstracts the timing: Freeze, Reconcile, and Commit fire as *) +(* separate atomic actions, ordered by guard. *) +(* *) +(* A3. Reconcile completeness under bounded loss. Within a bounded-loss *) +(* envelope the reconcile phase recovers the full union of admitted *) +(* messages; beyond that envelope the layer falls back to soft-commit *) +(* (out-of-spec). This module models only the in-spec case: Reconcile *) +(* atomically computes the union of frozen views across live nodes. *) +(* Out-of-spec behavior is a separate spec (future work). *) +(* *) +(* A4. All-live duration of AE phase. For each cslot k, the set of nodes *) +(* participating in AE is fixed at the moment of Freeze. Crash *) +(* during AE phase is out of scope here (see SCOPE DELIMITATION). *) +(***************************************************************************) + +EXTENDS Naturals, FiniteSets + +CONSTANTS + \* @type: Set(Str); + Nodes, \* finite set of node identifiers + \* @type: Set(Str); + MsgIDs, \* finite set of distinct message identifiers + \* @type: Int; + MaxSlot \* slot horizon (state-space bound) + +VARIABLES + \* @type: Int; + current_slot, \* global slot counter (justified by A1) + \* @type: Set({ id: Str, cslot: Int }); + network, \* in-flight messages (SET) + \* @type: Str -> Set(Str); + processed, \* processed[n] = msg ids admitted by n in current cslot + \* @type: Str -> Str; + phase, \* phase[n] \in {"open", "frozen", "committed"} + \* @type: Str -> Set(Str); + committed_set \* committed_set[n] = AE-final input set for n at current cslot + +vars == <> + +MsgRecord == [id: MsgIDs, cslot: 0..MaxSlot] + +------------------------------------------------------------------------------- +(* INITIAL STATE *) + +Init == + /\ current_slot = 0 + /\ network = {} + /\ processed = [n \in Nodes |-> {}] + /\ phase = [n \in Nodes |-> "open"] + /\ committed_set = [n \in Nodes |-> {}] + +------------------------------------------------------------------------------- +(* ACTIONS *) + +\* Submit: producer stamps cslot from its own clock (= current_slot under A1). +Submit(id) == + /\ id \in MsgIDs + /\ id \notin {m.id : m \in network} + /\ network' = network \cup {[id |-> id, cslot |-> current_slot]} + /\ UNCHANGED <> + +\* Process: C-slot strict admission. Only enabled in the open phase. +\* Once a node is frozen, it stops admitting new messages for this cslot. +Process(n, m) == + /\ n \in Nodes + /\ m \in network + /\ phase[n] = "open" + /\ m.id \notin processed[n] + /\ m.cslot = current_slot + /\ processed' = [processed EXCEPT ![n] = @ \cup {m.id}] + /\ UNCHANGED <> + +\* Freeze: node closes its admission window for this cslot. +\* In implementation: triggered by reaching the freeze deadline (~0.75 * Delta_t). +Freeze(n) == + /\ n \in Nodes + /\ phase[n] = "open" + /\ phase' = [phase EXCEPT ![n] = "frozen"] + /\ UNCHANGED <> + +\* Reconcile: abstract AE protocol. When ALL nodes are frozen, they +\* exchange their views and converge on the union, verified by Merkle root +\* equality. Atomic step at spec level; multi-round Bloom+Merkle at impl level. +\* Models assumption A3 (in-spec loss envelope). +Reconcile == + /\ \A n \in Nodes : phase[n] = "frozen" + /\ LET union_view == UNION { processed[n] : n \in Nodes } + IN committed_set' = [n \in Nodes |-> union_view] + /\ phase' = [n \in Nodes |-> "committed"] + /\ UNCHANGED <> + +\* Adversarial duplicate / replay injection. +DuplicateInject(id, fake_cslot) == + /\ id \in MsgIDs + /\ fake_cslot \in 0..MaxSlot + /\ network' = network \cup {[id |-> id, cslot |-> fake_cslot]} + /\ UNCHANGED <> + +\* NextCslot: advance to next slot. Only enabled when all nodes have +\* committed the current cslot (closing the AE phase deterministically). +\* Resets processed and phase for the new cslot. committed_set is overwritten +\* on next Reconcile (we do not retain history in-model; the implementation +\* logs each committed_set externally as the cslot-final ledger entry). +NextCslot == + /\ current_slot < MaxSlot + /\ \A n \in Nodes : phase[n] = "committed" + /\ current_slot' = current_slot + 1 + /\ processed' = [n \in Nodes |-> {}] + /\ phase' = [n \in Nodes |-> "open"] + /\ UNCHANGED <> + +Next == + \/ \E id \in MsgIDs : Submit(id) + \/ \E n \in Nodes, m \in network : Process(n, m) + \/ \E n \in Nodes : Freeze(n) + \/ Reconcile + \/ \E id \in MsgIDs, k \in 0..MaxSlot : DuplicateInject(id, k) + \/ NextCslot + +Spec == Init /\ [][Next]_vars + +------------------------------------------------------------------------------- +(* TYPE INVARIANT *) + +TypeInvariant == + /\ current_slot \in 0..MaxSlot + /\ network \subseteq MsgRecord + /\ processed \in [Nodes -> SUBSET MsgIDs] + /\ phase \in [Nodes -> {"open", "frozen", "committed"}] + /\ committed_set \in [Nodes -> SUBSET MsgIDs] + +------------------------------------------------------------------------------- +(* CORE SAFETY INVARIANTS *) + +\* AE-I1: MERKLE AGREEMENT (headline property of this module). +\* Any two nodes that have committed for the current cslot hold identical +\* committed_set. In implementation: equal Merkle roots. +\* This is the formal counterpart of the AE design guarantee. +MerkleAgreement == + \A n1, n2 \in Nodes : + (phase[n1] = "committed" /\ phase[n2] = "committed") + => committed_set[n1] = committed_set[n2] + +\* AE-I2: COMMITTED IS SUPERSET OF LOCAL PROCESSED. +\* AE Reconcile only adds, never removes. A node's committed_set always +\* contains every message it locally admitted (no in-spec rollback of local +\* admission). Local processed view is monotonically a subset of the merged +\* view. (This rules out the "frozen and then dropped" failure mode.) +CommittedSupersetsProcessed == + \A n \in Nodes : + phase[n] = "committed" => processed[n] \subseteq committed_set[n] + +\* AE-I3: NO PHANTOM IN COMMITTED. +\* Every id in any committed_set corresponds to a real network record with +\* m.cslot = current_slot. AE cannot fabricate messages, only union real +\* admissions. +NoPhantomInCommitted == + \A n \in Nodes : + phase[n] = "committed" => + \A id \in committed_set[n] : + \E m \in network : m.id = id /\ m.cslot = current_slot + +\* AE-I4: NO REORDER ACROSS CSLOT. +\* A message admitted in cslot k carries the cslot stamp k, never +\* re-attributed to another cslot. (Trivially follows from the gate +\* m.cslot = current_slot at admission time.) +NoReorderAcrossCslot == + \A n \in Nodes : \A id \in processed[n] : + \E m \in network : m.id = id /\ m.cslot = current_slot + +\* AE-I5: PHASE PROGRESSION VALID. +\* A node's phase is always one of the three legal states. Forward-only +\* transitions are enforced structurally by the Freeze, Reconcile, NextCslot +\* guards; declared here as an explicit type-level safety net. +PhaseProgressionValid == + \A n \in Nodes : phase[n] \in {"open", "frozen", "committed"} + +------------------------------------------------------------------------------- +(* STATE-SPACE CONSTRAINT *) + +StateConstraint == + current_slot <= MaxSlot + +------------------------------------------------------------------------------- +(* LIVENESS LAYER *) +(* *) +(* Fairness assignment: *) +(* - SF(Reconcile): once all nodes are frozen, AE must run. *) +(* - SF(NextCslot): once all nodes are committed, slot must advance. *) +(* - WF(Freeze(n)) per node: each node eventually freezes. *) +(* - NO fairness on Process / Submit / DuplicateInject (same rationale as *) +(* core module: late delivery is dropped by design; adversary unfair). *) +(***************************************************************************) + +Fairness == + /\ SF_vars(Reconcile) + /\ SF_vars(NextCslot) + /\ \A n \in Nodes : WF_vars(Freeze(n)) + +LiveSpec == Init /\ [][Next]_vars /\ Fairness + +\* AE-L1: EVENTUAL COMMIT. +\* Every node eventually commits for the cslot it participates in. +EventualCommit == + \A n \in Nodes : + (phase[n] = "open") ~> (phase[n] = "committed") + +\* AE-L2: EVENTUAL AGREEMENT. +\* If two nodes both reach the committed phase, MerkleAgreement holds. +\* (Safety + liveness composition.) +EventualAgreement == + \A n1, n2 \in Nodes : + (phase[n1] = "open" /\ phase[n2] = "open") + ~> (phase[n1] = "committed" /\ phase[n2] = "committed" + /\ committed_set[n1] = committed_set[n2]) + +============================================================================= diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot_AE_Proofs.tla b/specifications/VortexDSE/Vortex_DSE_CSlot_AE_Proofs.tla new file mode 100644 index 00000000..87954eb6 --- /dev/null +++ b/specifications/VortexDSE/Vortex_DSE_CSlot_AE_Proofs.tla @@ -0,0 +1,59 @@ +-------------------- MODULE Vortex_DSE_CSlot_AE_Proofs -------------------- +(***************************************************************************) +(* TLAPS target: Vortex_DSE_CSlot_AE (per-slot Merkle agreement layer). *) +(* *) +(* Public bundle today: TLC + Apalache (bounded). This module is the *) +(* deductive upgrade — see TLAPS_NEXT.md for scope and theorem order. *) +(* *) +(* Scaffold status: TypeInvariant proof structure started; remaining *) +(* obligations require TLAPS on a developer machine (tlapm not in CI here). *) +(***************************************************************************) + +EXTENDS Vortex_DSE_CSlot_AE, TLAPS + +ASSUME MaxSlotType == MaxSlot \in Nat + +------------------------------------------------------------------------------- +(* PART A — TYPE INVARIANT *) + +LEMMA InitType == Init => TypeInvariant + BY MaxSlotType DEF Init, TypeInvariant, MsgRecord + +LEMMA NextType == TypeInvariant /\ [Next]_vars => TypeInvariant' + <1> USE MaxSlotType DEF TypeInvariant, MsgRecord, vars + <1> SUFFICES ASSUME TypeInvariant, [Next]_vars + PROVE TypeInvariant' + OBVIOUS + <1>1. CASE \E id \in MsgIDs : Submit(id) + BY <1>1 DEF Submit + <1>2. CASE \E n \in Nodes, m \in network : Process(n, m) + BY <1>2 DEF Process + <1>3. CASE \E n \in Nodes : Freeze(n) + BY <1>3 DEF Freeze + <1>4. CASE Reconcile + BY <1>4 DEF Reconcile + <1>5. CASE \E id \in MsgIDs, k \in 0..MaxSlot : DuplicateInject(id, k) + BY <1>5 DEF DuplicateInject + <1>6. CASE NextCslot + BY <1>6 DEF NextCslot + <1>7. CASE UNCHANGED vars + BY <1>7 + <1>8. QED + BY <1>1, <1>2, <1>3, <1>4, <1>5, <1>6, <1>7 DEF Next + +THEOREM TypeCorrect == Spec => []TypeInvariant + <1>1. Init => TypeInvariant + BY InitType + <1>2. TypeInvariant /\ [Next]_vars => TypeInvariant' + BY NextType + <1>3. QED + BY <1>1, <1>2, PTL DEF Spec + +------------------------------------------------------------------------------- +(* PART B — MERKLE AGREEMENT (headline) *) +(* OPEN: MerkleAgreement is not inductive alone; expect strengthening with *) +(* CommittedSupersetsProcessed and/or phase synchronization lemmas. *) + +\* THEOREM MerkleAgreementAlways == Spec => []MerkleAgreement + +============================================================================= diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot_ExactlyOnce_Proof.tla b/specifications/VortexDSE/Vortex_DSE_CSlot_ExactlyOnce_Proof.tla new file mode 100644 index 00000000..0b122981 --- /dev/null +++ b/specifications/VortexDSE/Vortex_DSE_CSlot_ExactlyOnce_Proof.tla @@ -0,0 +1,297 @@ +-------------- MODULE Vortex_DSE_CSlot_ExactlyOnce_Proof -------------- +(***************************************************************************) +(* TLAPS (machine-checked, unbounded) proof of STRICT EXACTLY-ONCE *) +(* per node for the Vortex DSE C-Slot admission model. *) +(* *) +(* Author: Vasilis Nasopoulos — Vortex DSE / © 2026 *) +(* *) +(* What this proves: *) +(* StrictExactlyOnce: no node ever admits the same message id MORE THAN *) +(* ONCE — not across crash/rejoin cycles, not under adversarial replay, *) +(* not under arbitrary network reordering or delivery delay. *) +(* *) +(* Formally: *) +(* ∀ n ∈ Nodes, ∀ id ∈ MsgIDs: *) +(* id ∈ processed[n] ⟹ id ∉ processed[n] after any Process(n,m) *) +(* *) +(* Equivalently (set-membership formulation used here): *) +(* ∀ n ∈ Nodes: processed[n] ⊆ MsgIDs (no duplicates in a set) *) +(* AND the Process guard enforces id ∉ processed[n] before admission. *) +(* *) +(* Why this is non-trivial (and why TLC alone is insufficient): *) +(* The proof must cover: *) +(* (a) Normal admission path: guard `m.id ∉ processed[n]` *) +(* (b) Crash: processed[n] → {} (safe but not trivially inductive) *) +(* (c) Rejoin: processed[n] := persisted[n] (persisted must be clean) *) +(* (d) Adversarial DuplicateInject: attacker re-injects past ids; *) +(* the guard must still block re-admission. *) +(* (e) Tick: monotonic slot advance; already-admitted ids stay in set. *) +(* *) +(* Cases (c) and (d) together are why TLC model-checking over small *) +(* constants is not enough: the invariant must be proved inductively for *) +(* ANY Nodes set, ANY MsgIDs set, and ANY MaxSlot ∈ Nat. *) +(* *) +(* Proof structure (standard inductive-invariant pattern): *) +(* (1) Init ⟹ StrictExactlyOnceInv *) +(* (2) StrictExactlyOnceInv ∧ [Next]_vars ⟹ StrictExactlyOnceInv' *) +(* (3) Spec ⟹ []StrictExactlyOnce (by PTL from (1) and (2)) *) +(* *) +(* Relationship to existing proofs (Vortex_DSE_CSlot_Proofs.tla): *) +(* TypeCorrect (Spec => []TypeInvariant) and *) +(* NoFutureAdmissionCorrect (Spec => []NoFutureAdmission) are proved *) +(* separately. This file adds the strictly-once admission guarantee as *) +(* an independent deductive obligation. *) +(***************************************************************************) + +EXTENDS Vortex_DSE_CSlot, TLAPS + +ASSUME MaxSlotType == MaxSlot \in Nat + +------------------------------------------------------------------------------- +(* THE INVARIANT WE PROVE *) +(* *) +(* StrictExactlyOnce: every node's processed set is a genuine subset of *) +(* MsgIDs (sets have no duplicates by definition in TLA+), AND the Process *) +(* action's guard enforces that an id already in processed[n] can never *) +(* be added again (the set union with an existing element is idempotent, *) +(* but the guard blocks the action entirely — no double-counting). *) +(* *) +(* We strengthen to StrictExactlyOnceInv to make the invariant inductive *) +(* across the Rejoin action (processed := persisted): we need to know that *) +(* persisted[n] ⊆ MsgIDs as well, so that Rejoin cannot smuggle in a *) +(* duplicate. PersistedClean captures this. *) +(***************************************************************************) + +\* The core predicate: every id in processed[n] is a genuine MsgID, +\* and the set has no duplicates (TLA+ sets are duplicate-free by axiom). +ExactlyOnceCore == + \A n \in Nodes : processed[n] \subseteq MsgIDs + +\* Auxiliary: the mmap snapshot is also clean — only real MsgIDs. +\* Needed to close the inductive step for Rejoin(n). +PersistedClean == + \A n \in Nodes : persisted[n] \subseteq MsgIDs + +\* The full inductive invariant. +StrictExactlyOnceInv == ExactlyOnceCore /\ PersistedClean + +\* The exported safety theorem (what we actually care about). +StrictExactlyOnce == ExactlyOnceCore + +------------------------------------------------------------------------------- +(* PART 1 — INITIAL STATE *) +(* *) +(* In Init: processed[n] = {} ⊆ MsgIDs and persisted[n] = {} ⊆ MsgIDs. *) +(* Both conjuncts hold trivially. *) +(***************************************************************************) + +LEMMA InitStrictExactlyOnce == Init => StrictExactlyOnceInv + BY DEF Init, StrictExactlyOnceInv, ExactlyOnceCore, PersistedClean + +------------------------------------------------------------------------------- +(* PART 2 — INDUCTIVE STEP *) +(* *) +(* We must show: StrictExactlyOnceInv ∧ [Next]_vars => StrictExactlyOnceInv'*) +(* Case analysis over every action in Next. *) +(***************************************************************************) + +\* NOTE: TypeInvariant is REQUIRED as a hypothesis here. The Process(n,m) case +\* must conclude mm.id \in MsgIDs from mm \in network, which holds only because +\* network \subseteq MsgRecord — a TypeInvariant conjunct. Earlier this lemma +\* unfolded TypeInvariant via USE DEF but never ASSUMED it, so that fact was +\* not in scope and the mm.id \in MsgIDs obligation failed silently (tlapm does +\* not return a non-zero exit code on unproved obligations). TypeInvariant is +\* discharged in the theorem below via the machine-checked TypeCorrect. +LEMMA NextStrictExactlyOnce == + TypeInvariant /\ StrictExactlyOnceInv /\ [Next]_vars => StrictExactlyOnceInv' + <1> USE MaxSlotType + DEF StrictExactlyOnceInv, ExactlyOnceCore, PersistedClean, + TypeInvariant, MsgRecord, vars + <1> SUFFICES ASSUME TypeInvariant, StrictExactlyOnceInv, [Next]_vars + PROVE StrictExactlyOnceInv' + OBVIOUS + + \* ── Submit(id) ────────────────────────────────────────────────────────── + \* network grows; processed and persisted are UNCHANGED. + \* StrictExactlyOnceInv' follows immediately from UNCHANGED. + <1>1. CASE \E id \in MsgIDs : Submit(id) + <2> PICK i \in MsgIDs : Submit(i) + BY <1>1 + <2>1. /\ processed' = processed + /\ persisted' = persisted + BY DEF Submit + <2> QED BY <2>1 + + \* ── Process(n, m) ──────────────────────────────────────────────────────── + \* The guard `m.id ∉ processed[n]` prevents re-admission. + \* processed'[nn] = processed[nn] ∪ {mm.id}. + \* Since mm ∈ network ⊆ MsgRecord and MsgRecord has id: MsgIDs, + \* mm.id ∈ MsgIDs, so the union stays ⊆ MsgIDs. + \* persisted is UNCHANGED. + <1>2. CASE \E n \in Nodes, m \in network : Process(n, m) + <2> PICK nn \in Nodes, mm \in network : Process(nn, mm) + BY <1>2 + <2>1. /\ processed' = [processed EXCEPT ![nn] = processed[nn] \cup {mm.id}] + /\ persisted' = persisted + /\ mm \in network + /\ mm.id \in MsgIDs + BY DEF Process, MsgRecord + <2>2. ExactlyOnceCore' + <3> SUFFICES ASSUME NEW n \in Nodes + PROVE processed'[n] \subseteq MsgIDs + OBVIOUS + <3>1. CASE n = nn + BY <3>1, <2>1 + <3>2. CASE n # nn + BY <3>2, <2>1 + <3> QED BY <3>1, <3>2 + <2>3. PersistedClean' + BY <2>1 + <2> QED BY <2>2, <2>3 DEF StrictExactlyOnceInv + + \* ── Crash(n) ───────────────────────────────────────────────────────────── + \* processed[nn] → {}; persisted[nn] := processed[nn]. + \* {} ⊆ MsgIDs trivially. + \* persisted'[nn] = processed[nn] ⊆ MsgIDs by ExactlyOnceCore. + <1>3. CASE \E n \in Nodes : Crash(n) + <2> PICK nn \in Nodes : Crash(nn) + BY <1>3 + <2>1. /\ processed' = [processed EXCEPT ![nn] = {}] + /\ persisted' = [persisted EXCEPT ![nn] = processed[nn]] + BY DEF Crash + <2>2. ExactlyOnceCore' + <3> SUFFICES ASSUME NEW n \in Nodes + PROVE processed'[n] \subseteq MsgIDs + OBVIOUS + <3>1. CASE n = nn + BY <3>1, <2>1 + <3>2. CASE n # nn + BY <3>2, <2>1 + <3> QED BY <3>1, <3>2 + <2>3. PersistedClean' + <3> SUFFICES ASSUME NEW n \in Nodes + PROVE persisted'[n] \subseteq MsgIDs + OBVIOUS + <3>1. CASE n = nn + BY <3>1, <2>1 DEF ExactlyOnceCore + <3>2. CASE n # nn + BY <3>2, <2>1 DEF PersistedClean + <3> QED BY <3>1, <3>2 + <2> QED BY <2>2, <2>3 DEF StrictExactlyOnceInv + + \* ── Rejoin(n) ──────────────────────────────────────────────────────────── + \* processed[nn] := persisted[nn]. + \* PersistedClean ensures persisted[nn] ⊆ MsgIDs, so ExactlyOnceCore' holds. + \* persisted is UNCHANGED. + <1>4. CASE \E n \in Nodes : Rejoin(n) + <2> PICK nn \in Nodes : Rejoin(nn) + BY <1>4 + <2>1. /\ processed' = [processed EXCEPT ![nn] = persisted[nn]] + /\ persisted' = persisted + BY DEF Rejoin + <2>2. ExactlyOnceCore' + <3> SUFFICES ASSUME NEW n \in Nodes + PROVE processed'[n] \subseteq MsgIDs + OBVIOUS + <3>1. CASE n = nn + BY <3>1, <2>1 DEF PersistedClean + <3>2. CASE n # nn + BY <3>2, <2>1 DEF ExactlyOnceCore + <3> QED BY <3>1, <3>2 + <2>3. PersistedClean' + BY <2>1 + <2> QED BY <2>2, <2>3 DEF StrictExactlyOnceInv + + \* ── DuplicateInject(id, fake_cslot) ────────────────────────────────────── + \* Attacker injects a message with arbitrary cslot into the network. + \* processed and persisted are UNCHANGED. + \* The Process guard `m.id ∉ processed[n]` will block re-admission if + \* the injected id was already processed — but here we only need to show + \* the invariant is preserved by the injection itself (not by Process). + \* Since processed' = processed and persisted' = persisted, trivial. + <1>5. CASE \E id \in MsgIDs, k \in 0..MaxSlot : DuplicateInject(id, k) + <2> PICK i \in MsgIDs, k \in 0..MaxSlot : DuplicateInject(i, k) + BY <1>5 + <2>1. /\ processed' = processed + /\ persisted' = persisted + BY DEF DuplicateInject + <2> QED BY <2>1 + + \* ── Tick ───────────────────────────────────────────────────────────────── + \* current_slot advances; processed and persisted are UNCHANGED. + <1>6. CASE Tick + <2>1. /\ processed' = processed + /\ persisted' = persisted + BY <1>6 DEF Tick + <2> QED BY <2>1 + + \* ── Stutter ────────────────────────────────────────────────────────────── + <1>7. CASE UNCHANGED vars + BY <1>7 + + <1>8. QED + BY <1>1, <1>2, <1>3, <1>4, <1>5, <1>6, <1>7 DEF Next + +------------------------------------------------------------------------------- +(* PART 3 — TEMPORAL THEOREM *) +(* *) +(* By PTL (temporal induction): *) +(* Init ⟹ StrictExactlyOnceInv (Part 1) *) +(* StrictExactlyOnceInv ∧ [Next]_vars *) +(* ⟹ StrictExactlyOnceInv' (Part 2) *) +(* ∴ Spec ⟹ []StrictExactlyOnceInv (PTL) *) +(* ∴ Spec ⟹ []StrictExactlyOnce (projection onto core conjunct) *) +(***************************************************************************) + +\* Type-preservation, needed so the Process case above has network \subseteq +\* MsgRecord available at every reachable state. Same lemmas as the +\* machine-checked TypeCorrect in Vortex_DSE_CSlot_Proofs.tla, reproduced here +\* so this proof is self-contained. +LEMMA InitType == Init => TypeInvariant + BY MaxSlotType DEF Init, TypeInvariant, MsgRecord + +LEMMA NextType == TypeInvariant /\ [Next]_vars => TypeInvariant' + <1> USE MaxSlotType DEF TypeInvariant, MsgRecord, vars + <1> SUFFICES ASSUME TypeInvariant, [Next]_vars + PROVE TypeInvariant' + OBVIOUS + <1>1. CASE \E id \in MsgIDs : Submit(id) + BY <1>1 DEF Submit + <1>2. CASE \E n \in Nodes, m \in network : Process(n, m) + BY <1>2 DEF Process + <1>3. CASE \E n \in Nodes : Crash(n) + BY <1>3 DEF Crash + <1>4. CASE \E n \in Nodes : Rejoin(n) + BY <1>4 DEF Rejoin + <1>5. CASE \E id \in MsgIDs, k \in 0..MaxSlot : DuplicateInject(id, k) + BY <1>5 DEF DuplicateInject + <1>6. CASE Tick + BY <1>6 DEF Tick + <1>7. CASE UNCHANGED vars + BY <1>7 + <1>8. QED + BY <1>1, <1>2, <1>3, <1>4, <1>5, <1>6, <1>7 DEF Next + +\* We carry TypeInvariant /\ StrictExactlyOnceInv as ONE inductive invariant so +\* the Process case always has network \subseteq MsgRecord in scope. Projecting +\* onto the StrictExactlyOnce conjunct gives the exported safety theorem. +THEOREM StrictExactlyOnceCorrect == Spec => []StrictExactlyOnce + <1>1. Init => (TypeInvariant /\ StrictExactlyOnceInv) + BY InitType, InitStrictExactlyOnce + <1>2. (TypeInvariant /\ StrictExactlyOnceInv) /\ [Next]_vars + => (TypeInvariant /\ StrictExactlyOnceInv)' + <2>1. TypeInvariant /\ [Next]_vars => TypeInvariant' + BY NextType + <2>2. TypeInvariant /\ StrictExactlyOnceInv /\ [Next]_vars + => StrictExactlyOnceInv' + BY NextStrictExactlyOnce + <2> QED BY <2>1, <2>2 + <1>3. (TypeInvariant /\ StrictExactlyOnceInv) => StrictExactlyOnce + BY DEF StrictExactlyOnceInv, StrictExactlyOnce + <1>4. QED + BY <1>1, <1>2, <1>3, PTL DEF Spec + +============================================================================= +\* © 2026 Vasilis Nasopoulos — Vortex DSE +\* Registered/timestamped IP. Not for redistribution without permission. +============================================================================= diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot_Proofs.tla b/specifications/VortexDSE/Vortex_DSE_CSlot_Proofs.tla new file mode 100644 index 00000000..5986128c --- /dev/null +++ b/specifications/VortexDSE/Vortex_DSE_CSlot_Proofs.tla @@ -0,0 +1,264 @@ +---------------------- MODULE Vortex_DSE_CSlot_Proofs ---------------------- +(***************************************************************************) +(* TLAPS (machine-checked, unbounded) proofs for Vortex_DSE_CSlot. *) +(* *) +(* These are DEDUCTIVE proofs, not model checking. They establish *) +(* (A) Spec => []TypeInvariant (type-correctness) *) +(* (B) Spec => []NoFutureAdmission (the headline core safety property) *) +(* for ANY constants — any Nodes set, any MsgIDs set, any finite MaxSlot *) +(* in Nat — each in a single proof, whereas the TLC/Apalache results hold *) +(* only for the specific small instances they enumerated (e.g. 2 nodes, *) +(* MaxSlot=4). NOTE: unbounded over the PARAMETERS, not "infinite slots": *) +(* each instance still has a finite slot domain 0..MaxSlot. *) +(* *) +(* Standard inductive-invariant pattern: *) +(* (1) Init => Inv *) +(* (2) Inv /\ [Next]_vars => Inv' *) +(* (3) therefore Spec => []Inv (temporal induction, PTL) *) +(* *) +(* WHY NoFutureAdmission needs strengthening (honest scope note): *) +(* NoFutureAdmission alone is NOT inductive. The Rejoin action restores *) +(* processed[n] := persisted[n], but NoFutureAdmission says nothing *) +(* about persisted[n], so the induction step for Rejoin cannot close. *) +(* We therefore prove the strengthened invariant *) +(* SafeInv == TypeInvariant /\ NoFutureAdmission /\ PersistedSafe *) +(* where PersistedSafe constrains the mmap snapshot the same way. The *) +(* two safety conjuncts close MUTUALLY: Crash feeds PersistedSafe from *) +(* NoFutureAdmission, and Rejoin feeds NoFutureAdmission from *) +(* PersistedSafe. NoFutureAdmission is a conjunct of SafeInv, so *) +(* Spec => []SafeInv yields Spec => []NoFutureAdmission. *) +(* *) +(* Only typing assumption on the constants (a slot horizon is a natural). *) +(***************************************************************************) + +EXTENDS Vortex_DSE_CSlot, TLAPS + +ASSUME MaxSlotType == MaxSlot \in Nat + +------------------------------------------------------------------------------- +(* PART A — TYPE INVARIANT (type-correctness) *) + +\* (1) The initial state satisfies the type invariant. +LEMMA InitType == Init => TypeInvariant + BY MaxSlotType DEF Init, TypeInvariant, MsgRecord + +\* (2) Every step (or stutter) preserves the type invariant. +LEMMA NextType == TypeInvariant /\ [Next]_vars => TypeInvariant' + <1> USE MaxSlotType DEF TypeInvariant, MsgRecord, vars + <1> SUFFICES ASSUME TypeInvariant, [Next]_vars + PROVE TypeInvariant' + OBVIOUS + <1>1. CASE \E id \in MsgIDs : Submit(id) + BY <1>1 DEF Submit + <1>2. CASE \E n \in Nodes, m \in network : Process(n, m) + BY <1>2 DEF Process + <1>3. CASE \E n \in Nodes : Crash(n) + BY <1>3 DEF Crash + <1>4. CASE \E n \in Nodes : Rejoin(n) + BY <1>4 DEF Rejoin + <1>5. CASE \E id \in MsgIDs, k \in 0..MaxSlot : DuplicateInject(id, k) + BY <1>5 DEF DuplicateInject + <1>6. CASE Tick + BY <1>6 DEF Tick + <1>7. CASE UNCHANGED vars + BY <1>7 + <1>8. QED + BY <1>1, <1>2, <1>3, <1>4, <1>5, <1>6, <1>7 DEF Next + +\* (3) Temporal induction: the invariant holds in every reachable state. +THEOREM TypeCorrect == Spec => []TypeInvariant + <1>1. Init => TypeInvariant + BY InitType + <1>2. TypeInvariant /\ [Next]_vars => TypeInvariant' + BY NextType + <1>3. QED + BY <1>1, <1>2, PTL DEF Spec + +------------------------------------------------------------------------------- +(* PART B — NO FUTURE ADMISSION (the headline safety) *) + +\* Auxiliary invariant: the mmap snapshot never holds an id without a real, +\* present-or-past witness in the network. This is the missing piece that +\* makes NoFutureAdmission survive the Rejoin (processed := persisted) step. +PersistedSafe == + \A n \in Nodes : \A id \in persisted[n] : + \E m \in network : m.id = id /\ m.cslot <= current_slot + +\* The strengthened, inductive safety invariant. +SafeInv == TypeInvariant /\ NoFutureAdmission /\ PersistedSafe + +\* (1) Init. +LEMMA InitSafe == Init => SafeInv + BY InitType DEF Init, SafeInv, NoFutureAdmission, PersistedSafe + +\* (2) Inductive step for the strengthened invariant. +LEMMA NextSafe == SafeInv /\ [Next]_vars => SafeInv' + <1> USE MaxSlotType DEF SafeInv, TypeInvariant, MsgRecord, + NoFutureAdmission, PersistedSafe, vars + <1> SUFFICES ASSUME SafeInv, [Next]_vars + PROVE SafeInv' + OBVIOUS + <1>0. TypeInvariant' + BY NextType + <1> SUFFICES NoFutureAdmission' /\ PersistedSafe' + BY <1>0 DEF SafeInv + \* ---- Submit: network grows, processed/persisted/slot unchanged. ---- + <1>1. CASE \E id \in MsgIDs : Submit(id) + <2> PICK i \in MsgIDs : Submit(i) + BY <1>1 + <2>1. /\ network' = network \cup {[id |-> i, cslot |-> current_slot]} + /\ processed' = processed + /\ persisted' = persisted + /\ current_slot' = current_slot + BY DEF Submit + <2>2. \A m \in network : m \in network' + BY <2>1 + <2>3. NoFutureAdmission' + BY <2>1, <2>2 + <2>4. PersistedSafe' + BY <2>1, <2>2 + <2> QED BY <2>3, <2>4 + \* ---- Process: processed[nn] gains mm.id; the guard gives the witness. ---- + <1>2. CASE \E n \in Nodes, m \in network : Process(n, m) + <2> PICK nn \in Nodes, mm \in network : Process(nn, mm) + BY <1>2 + <2>1. /\ network' = network + /\ persisted' = persisted + /\ current_slot' = current_slot + /\ processed' = [processed EXCEPT ![nn] = processed[nn] \cup {mm.id}] + /\ mm \in network + /\ mm.cslot <= current_slot + BY DEF Process + <2>2. PersistedSafe' + BY <2>1 + <2>3. NoFutureAdmission' + <3> SUFFICES ASSUME NEW n \in Nodes, NEW id \in processed'[n] + PROVE \E m \in network' : m.id = id /\ m.cslot <= current_slot' + OBVIOUS + <3>1. CASE n = nn + <4>1. id \in processed[nn] \/ id = mm.id + BY <2>1, <3>1 + <4>2. CASE id \in processed[nn] + BY <4>2, <2>1 + <4>3. CASE id = mm.id + BY <4>3, <2>1 + <4> QED BY <4>1, <4>2, <4>3 + <3>2. CASE n # nn + BY <3>2, <2>1 + <3> QED BY <3>1, <3>2 + <2> QED BY <2>2, <2>3 + \* ---- Crash: processed[nn] -> {} (vacuous); persisted[nn] := processed[nn]. ---- + <1>3. CASE \E n \in Nodes : Crash(n) + <2> PICK nn \in Nodes : Crash(nn) + BY <1>3 + <2>1. /\ network' = network + /\ current_slot' = current_slot + /\ persisted' = [persisted EXCEPT ![nn] = processed[nn]] + /\ processed' = [processed EXCEPT ![nn] = {}] + BY DEF Crash + <2>2. NoFutureAdmission' + <3> SUFFICES ASSUME NEW n \in Nodes, NEW id \in processed'[n] + PROVE \E m \in network' : m.id = id /\ m.cslot <= current_slot' + OBVIOUS + <3>1. CASE n = nn + BY <3>1, <2>1 + <3>2. CASE n # nn + BY <3>2, <2>1 + <3> QED BY <3>1, <3>2 + <2>3. PersistedSafe' + <3> SUFFICES ASSUME NEW n \in Nodes, NEW id \in persisted'[n] + PROVE \E m \in network' : m.id = id /\ m.cslot <= current_slot' + OBVIOUS + <3>1. CASE n = nn + BY <3>1, <2>1 + <3>2. CASE n # nn + BY <3>2, <2>1 + <3> QED BY <3>1, <3>2 + <2> QED BY <2>2, <2>3 + \* ---- Rejoin: processed[nn] := persisted[nn]; PersistedSafe gives witness. ---- + <1>4. CASE \E n \in Nodes : Rejoin(n) + <2> PICK nn \in Nodes : Rejoin(nn) + BY <1>4 + <2>1. /\ network' = network + /\ current_slot' = current_slot + /\ persisted' = persisted + /\ processed' = [processed EXCEPT ![nn] = persisted[nn]] + BY DEF Rejoin + <2>2. PersistedSafe' + BY <2>1 + <2>3. NoFutureAdmission' + <3> SUFFICES ASSUME NEW n \in Nodes, NEW id \in processed'[n] + PROVE \E m \in network' : m.id = id /\ m.cslot <= current_slot' + OBVIOUS + <3>1. CASE n = nn + BY <3>1, <2>1 + <3>2. CASE n # nn + BY <3>2, <2>1 + <3> QED BY <3>1, <3>2 + <2> QED BY <2>2, <2>3 + \* ---- DuplicateInject: network grows with an arbitrary cslot; gate holds. ---- + <1>5. CASE \E id \in MsgIDs, k \in 0..MaxSlot : DuplicateInject(id, k) + <2> PICK i \in MsgIDs, k \in 0..MaxSlot : DuplicateInject(i, k) + BY <1>5 + <2>1. /\ network' = network \cup {[id |-> i, cslot |-> k]} + /\ processed' = processed + /\ persisted' = persisted + /\ current_slot' = current_slot + BY DEF DuplicateInject + <2>2. \A m \in network : m \in network' + BY <2>1 + <2>3. NoFutureAdmission' + BY <2>1, <2>2 + <2>4. PersistedSafe' + BY <2>1, <2>2 + <2> QED BY <2>3, <2>4 + \* ---- Tick: current_slot += 1; monotonicity keeps every past witness valid. ---- + <1>6. CASE Tick + <2>1. /\ network' = network + /\ processed' = processed + /\ persisted' = persisted + /\ current_slot' = current_slot + 1 + BY <1>6 DEF Tick + <2>2. current_slot \in Nat + OBVIOUS + <2>3. NoFutureAdmission' + <3> SUFFICES ASSUME NEW n \in Nodes, NEW id \in processed[n] + PROVE \E m \in network : m.id = id /\ m.cslot <= current_slot' + BY <2>1 + <3>1. PICK m \in network : m.id = id /\ m.cslot <= current_slot + OBVIOUS + <3>2. m.cslot \in Nat + BY <3>1 DEF MsgRecord + <3>3. m.cslot <= current_slot' + BY <3>1, <3>2, <2>1, <2>2 + <3> QED BY <3>1, <3>3 + <2>4. PersistedSafe' + <3> SUFFICES ASSUME NEW n \in Nodes, NEW id \in persisted[n] + PROVE \E m \in network : m.id = id /\ m.cslot <= current_slot' + BY <2>1 + <3>1. PICK m \in network : m.id = id /\ m.cslot <= current_slot + OBVIOUS + <3>2. m.cslot \in Nat + BY <3>1 DEF MsgRecord + <3>3. m.cslot <= current_slot' + BY <3>1, <3>2, <2>1, <2>2 + <3> QED BY <3>1, <3>3 + <2> QED BY <2>3, <2>4 + \* ---- Stutter. ---- + <1>7. CASE UNCHANGED vars + BY <1>7 + <1>8. QED + BY <1>1, <1>2, <1>3, <1>4, <1>5, <1>6, <1>7 DEF Next + +\* (3) Temporal induction, then project onto the headline conjunct. +THEOREM NoFutureAdmissionCorrect == Spec => []NoFutureAdmission + <1>1. Init => SafeInv + BY InitSafe + <1>2. SafeInv /\ [Next]_vars => SafeInv' + BY NextSafe + <1>3. SafeInv => NoFutureAdmission + BY DEF SafeInv + <1>4. QED + BY <1>1, <1>2, <1>3, PTL DEF Spec + +============================================================================= diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot_Skew.tla b/specifications/VortexDSE/Vortex_DSE_CSlot_Skew.tla new file mode 100644 index 00000000..3e001a60 --- /dev/null +++ b/specifications/VortexDSE/Vortex_DSE_CSlot_Skew.tla @@ -0,0 +1,147 @@ +---------------------- MODULE Vortex_DSE_CSlot_Skew ---------------------- +(***************************************************************************) +(* Vortex DSE C-slot under BOUNDED CLOCK SKEW + Byzantine inject. *) +(* *) +(* Extension of Vortex_DSE_CSlot.tla. The single global current_slot is *) +(* replaced with a per-node clock node_slot[n]. Two adversarial powers are *) +(* added beyond the baseline spec: *) +(* *) +(* 1. CLOCK SKEW: each node ticks independently. The system enforces *) +(* |node_slot[n1] - node_slot[n2]| <= MaxSkew as a structural *) +(* constraint on Tick. *) +(* *) +(* 2. BYZANTINE INJECT: adversary may inject a message with arbitrary *) +(* cslot AND arbitrary origin node id (spoof the sender). *) +(* *) +(* The same exactly-once / no-phantom / strict-equality properties must *) +(* still hold, locally per node. Decision-locality means each node makes *) +(* its own admission decision against its own clock. *) +(***************************************************************************) + +EXTENDS Naturals, FiniteSets + +CONSTANTS Nodes, MsgIDs, MaxSlot, MaxSkew + +VARIABLES + node_slot, \* [Nodes -> Int] per-node clock + network, \* set of msg records + processed, + persisted, + node_state + +vars == <> + +MsgRecord == [id: MsgIDs, cslot: 0..MaxSlot, origin: Nodes] + +------------------------------------------------------------------------------- +Init == + /\ node_slot = [n \in Nodes |-> 0] + /\ network = {} + /\ processed = [n \in Nodes |-> {}] + /\ persisted = [n \in Nodes |-> {}] + /\ node_state = [n \in Nodes |-> "up"] + +------------------------------------------------------------------------------- +\* Submit: sender n stamps with its own local slot. +Submit(id, n) == + /\ id \in MsgIDs + /\ n \in Nodes + /\ node_state[n] = "up" + /\ id \notin {m.id : m \in network} + /\ \A x \in Nodes : id \notin processed[x] + /\ network' = network \cup {[id |-> id, cslot |-> node_slot[n], origin |-> n]} + /\ UNCHANGED <> + +\* Process: STRICT slot equality, but vs LOCAL clock now. +Process(n, m) == + /\ n \in Nodes + /\ m \in network + /\ node_state[n] = "up" + /\ m.id \notin processed[n] + /\ m.cslot = node_slot[n] + /\ processed' = [processed EXCEPT ![n] = @ \cup {m.id}] + /\ UNCHANGED <> + +Crash(n) == + /\ n \in Nodes + /\ node_state[n] = "up" + /\ persisted' = [persisted EXCEPT ![n] = processed[n]] + /\ node_state' = [node_state EXCEPT ![n] = "down"] + /\ processed' = [processed EXCEPT ![n] = {}] + /\ UNCHANGED <> + +Rejoin(n) == + /\ n \in Nodes + /\ node_state[n] = "down" + /\ processed' = [processed EXCEPT ![n] = persisted[n]] + /\ node_state' = [node_state EXCEPT ![n] = "up"] + /\ UNCHANGED <> + +\* Byzantine inject: adversary spoofs both cslot AND origin. +ByzantineInject(id, fake_cslot, fake_origin) == + /\ id \in MsgIDs + /\ fake_cslot \in 0..MaxSlot + /\ fake_origin \in Nodes + /\ network' = network \cup + {[id |-> id, cslot |-> fake_cslot, origin |-> fake_origin]} + /\ UNCHANGED <> + +\* Per-node tick, bounded by MaxSkew vs slowest node. +SkewedTick(n) == + /\ n \in Nodes + /\ node_slot[n] < MaxSlot + /\ \A other \in Nodes : + (node_slot[n] + 1) - node_slot[other] <= MaxSkew + /\ node_slot' = [node_slot EXCEPT ![n] = @ + 1] + /\ UNCHANGED <> + +Next == + \/ \E id \in MsgIDs, n \in Nodes : Submit(id, n) + \/ \E n \in Nodes, m \in network : Process(n, m) + \/ \E n \in Nodes : Crash(n) + \/ \E n \in Nodes : Rejoin(n) + \/ \E id \in MsgIDs, k \in 0..MaxSlot, o \in Nodes : ByzantineInject(id, k, o) + \/ \E n \in Nodes : SkewedTick(n) + +Spec == Init /\ [][Next]_vars + +------------------------------------------------------------------------------- +(* INVARIANTS *) + +TypeInvariant == + /\ node_slot \in [Nodes -> 0..MaxSlot] + /\ network \subseteq MsgRecord + /\ processed \in [Nodes -> SUBSET MsgIDs] + /\ persisted \in [Nodes -> SUBSET MsgIDs] + /\ node_state \in [Nodes -> {"up", "down"}] + +\* The Tick guard guarantees this; it is asserted as invariant to make +\* the skew bound an explicit, machine-checked property. +BoundedSkew == + \A n1, n2 \in Nodes : + /\ node_slot[n1] - node_slot[n2] <= MaxSkew + /\ node_slot[n2] - node_slot[n1] <= MaxSkew + +ExactlyOncePerNode == + \A n \in Nodes : Cardinality(processed[n]) <= Cardinality(MsgIDs) + +\* Local admission: a processed id has a network record whose cslot +\* is at most the node's current local slot. (Strict equality holds +\* at admission time; monotone clock means cslot <= node_slot[n] later.) +CSlotLocalAdmission == + \A n \in Nodes : \A id \in processed[n] : + \E m \in network : m.id = id /\ m.cslot <= node_slot[n] + +PersistedReflectsReality == + \A n \in Nodes : + node_state[n] = "down" => + persisted[n] \subseteq {m.id : m \in network} + +NoPhantomProcess == + \A n \in Nodes : processed[n] \subseteq {m.id : m \in network} + +------------------------------------------------------------------------------- +StateConstraint == + \A n \in Nodes : node_slot[n] <= MaxSlot + +============================================================================= diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot_Skew_tiny.cfg b/specifications/VortexDSE/Vortex_DSE_CSlot_Skew_tiny.cfg new file mode 100644 index 00000000..f01ebab3 --- /dev/null +++ b/specifications/VortexDSE/Vortex_DSE_CSlot_Skew_tiny.cfg @@ -0,0 +1,18 @@ +SPECIFICATION Spec + +CONSTANTS + Nodes = {n1, n2} + MsgIDs = {m1} + MaxSlot = 2 + MaxSkew = 1 + +INVARIANTS + TypeInvariant + BoundedSkew + ExactlyOncePerNode + CSlotLocalAdmission + PersistedReflectsReality + NoPhantomProcess + +CONSTRAINT + StateConstraint diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot_TTL.tla b/specifications/VortexDSE/Vortex_DSE_CSlot_TTL.tla new file mode 100644 index 00000000..f9dde694 --- /dev/null +++ b/specifications/VortexDSE/Vortex_DSE_CSlot_TTL.tla @@ -0,0 +1,240 @@ +---------------------- MODULE Vortex_DSE_CSlot_TTL ---------------------- +(***************************************************************************) +(* Vortex DSE — Deterministic C-Slot Admission (V. Nasopoulos) *) +(* *) +(* C-slot law: *) +(* C_slot(TX) = floor( (T_hw - T_0) / Delta_t ) *) +(* *) +(* Strict admission rule: *) +(* if tx.C_slot != current_slot { reject } *) +(* *) +(* This is NOT a TTL window. A message whose timestamp belongs to slot k *) +(* is admissible at node n IFF the node is currently in slot k. One slot *) +(* late => permanent reject. No leader, no quorum, no vote. *) +(* *) +(* Async hostile environment modeled: *) +(* - arbitrary message reordering (network is a SET), *) +(* - unbounded delivery delay (Process is nondeterministic), *) +(* - node crashes and rejoins (state survives only via the persistent snapshot), *) +(* - adversarial duplicate injection (replay attack). *) +(* *) +(* T_0 = 0 by normalization. We model integer slots directly: each ts is *) +(* already the C_slot index of the message (i.e. ts = floor(T_hw/Delta_t)).*) +(* current_time IS the current slot index. Tick advances the slot by 1. *) +(***************************************************************************) + +EXTENDS Naturals, FiniteSets + +CONSTANTS + \* @type: Set(Str); + Nodes, \* finite set of node identifiers + \* @type: Set(Str); + MsgIDs, \* finite set of distinct message identifiers + \* @type: Int; + MaxSlot \* slot horizon (state-space bound) + +VARIABLES + \* @type: Int; + current_slot, + \* @type: Set({ id: Str, cslot: Int }); + network, \* in-flight messages (SET = no ordering) + \* @type: Str -> Set(Str); + processed, \* processed[n] = msg ids node n has admitted + \* @type: Str -> Set(Str); + persisted, \* persisted[n] = persistent snapshot (survives crash) + \* @type: Str -> Str; + node_state \* node_state[n] \in {"up", "down"} + +vars == <> + +MsgRecord == [id: MsgIDs, cslot: 0..MaxSlot] + +------------------------------------------------------------------------------- +(* INITIAL STATE *) + +Init == + /\ current_slot = 0 + /\ network = {} + /\ processed = [n \in Nodes |-> {}] + /\ persisted = [n \in Nodes |-> {}] + /\ node_state = [n \in Nodes |-> "up"] + +------------------------------------------------------------------------------- +(* ACTIONS *) + +\* Submit: sender stamps T_hw, which yields cslot = current_slot at emission. +\* Network may deliver this arbitrarily later (no ordering, no time bound). +Submit(id) == + /\ id \in MsgIDs + /\ id \notin {m.id : m \in network} + /\ \A n \in Nodes : id \notin processed[n] + /\ network' = network \cup {[id |-> id, cslot |-> current_slot]} + /\ UNCHANGED <> + +\* C-SLOT STRICT ADMISSION. +\* Local, O(1) decision. The node admits m iff m.cslot equals the node's +\* current slot AND it has not already been processed. No window, no TTL. +\* Late delivery (m.cslot < current_slot) => permanent reject. +\* Future-dated (m.cslot > current_slot) => reject now; would only be +\* admitted if the message is delivered when the slot matches. +Process(n, m) == + /\ n \in Nodes + /\ m \in network + /\ node_state[n] = "up" + /\ m.id \notin processed[n] \* exactly-once guard (local) + /\ m.cslot = current_slot \* STRICT C-slot equality + /\ processed' = [processed EXCEPT ![n] = @ \cup {m.id}] + /\ UNCHANGED <> + +\* CRASH: node loses RAM. persistent snapshot in `persisted` survives. +Crash(n) == + /\ n \in Nodes + /\ node_state[n] = "up" + /\ persisted' = [persisted EXCEPT ![n] = processed[n]] + /\ node_state' = [node_state EXCEPT ![n] = "down"] + /\ processed' = [processed EXCEPT ![n] = {}] + /\ UNCHANGED <> + +\* REJOIN: node recovers from persistent snapshot. processed = persisted. +Rejoin(n) == + /\ n \in Nodes + /\ node_state[n] = "down" + /\ processed' = [processed EXCEPT ![n] = persisted[n]] + /\ node_state' = [node_state EXCEPT ![n] = "up"] + /\ UNCHANGED <> + +\* Adversarial duplicate / replay injection. +\* Attacker injects a message with arbitrary cslot value (past, present, +\* or future). The C-slot gate must still hold. +DuplicateInject(id, fake_cslot) == + /\ id \in MsgIDs + /\ fake_cslot \in 0..MaxSlot + /\ network' = network \cup {[id |-> id, cslot |-> fake_cslot]} + /\ UNCHANGED <> + +\* Slot ticker advances by 1. +Tick == + /\ current_slot < MaxSlot + /\ current_slot' = current_slot + 1 + /\ UNCHANGED <> + +Next == + \/ \E id \in MsgIDs : Submit(id) + \/ \E n \in Nodes, m \in network : Process(n, m) + \/ \E n \in Nodes : Crash(n) + \/ \E n \in Nodes : Rejoin(n) + \/ \E id \in MsgIDs, k \in 0..MaxSlot : DuplicateInject(id, k) + \/ Tick + +Spec == Init /\ [][Next]_vars + +------------------------------------------------------------------------------- +(* TYPE INVARIANT *) + +TypeInvariant == + /\ current_slot \in 0..MaxSlot + /\ network \subseteq MsgRecord + /\ processed \in [Nodes -> SUBSET MsgIDs] + /\ persisted \in [Nodes -> SUBSET MsgIDs] + /\ node_state \in [Nodes -> {"up", "down"}] + +------------------------------------------------------------------------------- +(* CORE SAFETY INVARIANTS *) + +\* I1: EXACTLY-ONCE PER NODE. +\* No node processes the same id twice (set semantics + guard). +ExactlyOncePerNode == + \A n \in Nodes : Cardinality(processed[n]) <= Cardinality(MsgIDs) + +\* I2: STRICT C-SLOT ADMISSION (the headline property). +\* Every processed id corresponds to some network message whose cslot +\* equals the slot at which it was admitted. Because the gate is +\* m.cslot = current_slot and current_slot is monotonic, an admitted +\* message's cslot value lies in [0, current_slot]. +\* The strong form we check: for every processed id at node n, there +\* exists a network record with that id whose cslot is <= current_slot +\* (i.e. it was a real, present-or-past slot, never future-dated). +CSlotStrictAdmission == + \A n \in Nodes : \A id \in processed[n] : + \E m \in network : m.id = id /\ m.cslot <= current_slot + +\* I3: PERSISTED REFLECTS REALITY. +\* persistent snapshot never invents ids that were not in the network. +PersistedReflectsReality == + \A n \in Nodes : + node_state[n] = "down" => + persisted[n] \subseteq {m.id : m \in network} + +\* I4: NO PHANTOM PROCESS. +\* Every processed id corresponds to a real network record. +NoPhantomProcess == + \A n \in Nodes : processed[n] \subseteq {m.id : m \in network} + +\* I5: DECISION LOCALITY. +\* If two nodes have both processed id, that id exists in network. +\* Structural consequence: the gate depends only on (m.cslot, current_slot), +\* not on n. Same (m.cslot, current_slot) => same decision at every node. +DecisionLocalityOnly == + \A n1, n2 \in Nodes : \A id \in MsgIDs : + (id \in processed[n1] /\ id \in processed[n2]) => + (\E m \in network : m.id = id) + +\* I6: NO LATE ADMISSION. +\* This is the property that distinguishes C-slot from TTL. +\* If id was admitted by node n, then at the moment of admission, +\* m.cslot = current_slot_then. Since current_slot is monotonic and +\* messages with m.cslot > current_slot cannot be admitted (gate), +\* AND messages with m.cslot < current_slot also cannot be admitted, +\* the only admitted messages have m.cslot exactly equal to the +\* admission-time slot. The check is: no processed id has a sole +\* network record with cslot > current_slot (would mean we admitted +\* a future-dated message we should not yet see admitted). +NoLateAdmission == + \A n \in Nodes : \A id \in processed[n] : + \E m \in network : m.id = id /\ m.cslot <= current_slot + +------------------------------------------------------------------------------- +(* STATE-SPACE CONSTRAINT *) + +StateConstraint == + current_slot <= MaxSlot + +------------------------------------------------------------------------------- +(* LIVENESS LAYER *) +(* *) +(* DESIGN NOTE — fairness assignment is intentional: *) +(* *) +(* - SF(Tick): the slot ticker is fair, advancing eventually. This is a *) +(* physical-hardware assumption (the ticker process does not stall *) +(* forever). Strong fairness because Tick is always enabled until *) +(* current_slot reaches MaxSlot. *) +(* *) +(* - WF(Rejoin(n)) per node: a crashed node, given the chance, eventually *) +(* rejoins. This corresponds to operational recovery (operator restart). *) +(* *) +(* - NO fairness on Process. This is deliberate: the strict C-slot rule *) +(* by design allows a message to be permanently dropped if the network *) +(* delivers it after its slot has passed. That IS the feature, not a *) +(* bug. Adding WF(Process) would falsely claim "every TX eventually *) +(* admitted", which contradicts the strict admission gate. *) +(* *) +(* - NO fairness on Submit / DuplicateInject. Submit is a user action; *) +(* adversary injection is, by definition, not fair. *) +(***************************************************************************) + +Fairness == + /\ SF_vars(Tick) + /\ \A n \in Nodes : WF_vars(Rejoin(n)) + +LiveSpec == Init /\ [][Next]_vars /\ Fairness + +\* L1 TICK PROGRESS. +\* Under SF(Tick), the slot counter eventually reaches the horizon. +TickProgress == <>(current_slot = MaxSlot) + +\* L2 EVENTUAL REJOIN. +\* Every crashed node eventually returns to "up", under WF(Rejoin(n)). +EventualRejoin == + \A n \in Nodes : (node_state[n] = "down") ~> (node_state[n] = "up") + +============================================================================= diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot_TTL_liveness.cfg b/specifications/VortexDSE/Vortex_DSE_CSlot_TTL_liveness.cfg new file mode 100644 index 00000000..f5aa6646 --- /dev/null +++ b/specifications/VortexDSE/Vortex_DSE_CSlot_TTL_liveness.cfg @@ -0,0 +1,13 @@ +SPECIFICATION LiveSpec + +CONSTANTS + Nodes = {n1, n2} + MsgIDs = {m1} + MaxSlot = 2 + +PROPERTIES + TickProgress + EventualRejoin + +CONSTRAINT + StateConstraint diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot_TTL_tiny.cfg b/specifications/VortexDSE/Vortex_DSE_CSlot_TTL_tiny.cfg new file mode 100644 index 00000000..617a208f --- /dev/null +++ b/specifications/VortexDSE/Vortex_DSE_CSlot_TTL_tiny.cfg @@ -0,0 +1,18 @@ +SPECIFICATION Spec + +CONSTANTS + Nodes = {n1, n2} + MsgIDs = {m1, m2} + MaxSlot = 4 + +INVARIANTS + TypeInvariant + ExactlyOncePerNode + CSlotStrictAdmission + PersistedReflectsReality + NoPhantomProcess + DecisionLocalityOnly + NoLateAdmission + +CONSTRAINT + StateConstraint diff --git a/specifications/VortexDSE/manifest.json b/specifications/VortexDSE/manifest.json new file mode 100644 index 00000000..bb1c91b9 --- /dev/null +++ b/specifications/VortexDSE/manifest.json @@ -0,0 +1,115 @@ +{ + "sources": [ + "https://github.com/vasilisnasopoulos/vortex-dse-whitepaper", + "https://github.com/vasilisnasopoulos/vortex-dse-cslot-proofs", + "https://github.com/vasilisnasopoulos/vortex-merkle-agreement" + ], + "authors": [ + "Vasilis Nasopoulos" + ], + "tags": [], + "modules": [ + { + "path": "specifications/VortexDSE/MC_Vortex_DSE_CSlot.tla", + "features": [], + "models": [ + { + "path": "specifications/VortexDSE/MC_Vortex_DSE_CSlot.cfg", + "runtime": "00:00:01", + "mode": "exhaustive search", + "result": "success", + "totalStates": 186367, + "distinctStates": 18903 + } + ] + }, + { + "path": "specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE.tla", + "features": [], + "models": [ + { + "path": "specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_liveness.cfg", + "runtime": "00:00:01", + "mode": "exhaustive search", + "result": "success" + }, + { + "path": "specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_tiny.cfg", + "runtime": "00:00:01", + "mode": "exhaustive search", + "result": "success", + "totalStates": 79601, + "distinctStates": 10000 + } + ] + }, + { + "path": "specifications/VortexDSE/Vortex_DSE_CSlot.tla", + "features": [], + "models": [] + }, + { + "path": "specifications/VortexDSE/Vortex_DSE_CSlot_AE.tla", + "features": [], + "models": [] + }, + { + "path": "specifications/VortexDSE/Vortex_DSE_CSlot_AE_Proofs.tla", + "features": [], + "models": [], + "proof": { + "maxRuntimeMinutes": 1 + } + }, + { + "path": "specifications/VortexDSE/Vortex_DSE_CSlot_ExactlyOnce_Proof.tla", + "features": [], + "models": [], + "proof": { + "maxRuntimeMinutes": 1 + } + }, + { + "path": "specifications/VortexDSE/Vortex_DSE_CSlot_Proofs.tla", + "features": [], + "models": [], + "proof": { + "maxRuntimeMinutes": 1 + } + }, + { + "path": "specifications/VortexDSE/Vortex_DSE_CSlot_Skew.tla", + "features": [], + "models": [ + { + "path": "specifications/VortexDSE/Vortex_DSE_CSlot_Skew_tiny.cfg", + "runtime": "00:00:01", + "mode": "exhaustive search", + "result": "success", + "totalStates": 96481, + "distinctStates": 10099 + } + ] + }, + { + "path": "specifications/VortexDSE/Vortex_DSE_CSlot_TTL.tla", + "features": [], + "models": [ + { + "path": "specifications/VortexDSE/Vortex_DSE_CSlot_TTL_liveness.cfg", + "runtime": "00:00:01", + "mode": "exhaustive search", + "result": "success" + }, + { + "path": "specifications/VortexDSE/Vortex_DSE_CSlot_TTL_tiny.cfg", + "runtime": "00:00:05", + "mode": "exhaustive search", + "result": "success", + "totalStates": 8084795, + "distinctStates": 608477 + } + ] + } + ] +} From d8ba318767edd2eaba8ad612d9aab8c4630ddfa1 Mon Sep 17 00:00:00 2001 From: Vasilis Nasopoulos Date: Wed, 5 Aug 2026 14:17:31 +0300 Subject: [PATCH 2/6] Move model-checking bounds out of the specifications MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit MaxSlot was a state-space horizon living in the specifications. It is now gone from all four: Tick and NextCslot are unbounded, and the adversary may forge any slot in Nat. Each specification gets an MC_ module that fixes the horizon inside the actions rather than through a CONSTRAINT, so the state graph is finite instead of truncated — under a state constraint TLC drops successor states, which is unsound for the temporal properties. MaxSkew stays in Vortex_DSE_CSlot_Skew: it is an assumption the protocol relies on, not a checking artifact. Also: WF is enough for the now-unbounded ticker, so SF_vars(Tick) becomes WF_vars(Tick); TickProgress is stated unboundedly in the specifications and strengthened to <>[] in the MC modules, where the horizon makes it permanent; node states and AE phases are named rather than written as bare strings; and the AE harness no longer bundles its invariants into a single conjunction, so a checker reports which one failed. Type invariants now constrain the network elementwise, since MsgRecord ranges over Nat and cannot be enumerated. Seven TLC models, all completing in under five seconds. The three TLAPS modules discharge 191, 128 and 32 obligations and exit 0 under tlapm --strict. Co-authored-by: Claude Opus 5 Signed-off-by: Vasilis Nasopoulos --- .../VortexDSE/MC_Vortex_DSE_CSlot.cfg | 19 +++--- .../VortexDSE/MC_Vortex_DSE_CSlot.tla | 56 +++++++++++++-- .../VortexDSE/MC_Vortex_DSE_CSlot_AE.tla | 56 +++++++++++---- .../MC_Vortex_DSE_CSlot_AE_liveness.cfg | 7 +- .../VortexDSE/MC_Vortex_DSE_CSlot_AE_tiny.cfg | 9 ++- ..._tiny.cfg => MC_Vortex_DSE_CSlot_Skew.cfg} | 11 ++- .../VortexDSE/MC_Vortex_DSE_CSlot_Skew.tla | 34 ++++++++++ ...L_tiny.cfg => MC_Vortex_DSE_CSlot_TTL.cfg} | 9 ++- .../VortexDSE/MC_Vortex_DSE_CSlot_TTL.tla | 42 ++++++++++++ .../MC_Vortex_DSE_CSlot_TTL_liveness.cfg | 12 ++++ .../MC_Vortex_DSE_CSlot_liveness.cfg | 14 ++++ specifications/VortexDSE/README.md | 18 +++-- specifications/VortexDSE/Vortex_DSE_CSlot.tla | 63 ++++++++--------- .../VortexDSE/Vortex_DSE_CSlot_AE.tla | 60 ++++++++-------- .../VortexDSE/Vortex_DSE_CSlot_AE_Proofs.tla | 7 +- .../Vortex_DSE_CSlot_ExactlyOnce_Proof.tla | 16 ++--- .../VortexDSE/Vortex_DSE_CSlot_Proofs.tla | 13 ++-- .../VortexDSE/Vortex_DSE_CSlot_Skew.tla | 37 +++++----- .../VortexDSE/Vortex_DSE_CSlot_TTL.tla | 58 ++++++++-------- .../Vortex_DSE_CSlot_TTL_liveness.cfg | 13 ---- specifications/VortexDSE/manifest.json | 68 ++++++++++++------- 21 files changed, 396 insertions(+), 226 deletions(-) rename specifications/VortexDSE/{Vortex_DSE_CSlot_Skew_tiny.cfg => MC_Vortex_DSE_CSlot_Skew.cfg} (64%) create mode 100644 specifications/VortexDSE/MC_Vortex_DSE_CSlot_Skew.tla rename specifications/VortexDSE/{Vortex_DSE_CSlot_TTL_tiny.cfg => MC_Vortex_DSE_CSlot_TTL.cfg} (69%) create mode 100644 specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL.tla create mode 100644 specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL_liveness.cfg create mode 100644 specifications/VortexDSE/MC_Vortex_DSE_CSlot_liveness.cfg delete mode 100644 specifications/VortexDSE/Vortex_DSE_CSlot_TTL_liveness.cfg diff --git a/specifications/VortexDSE/MC_Vortex_DSE_CSlot.cfg b/specifications/VortexDSE/MC_Vortex_DSE_CSlot.cfg index acfc46b1..7f6c38b0 100644 --- a/specifications/VortexDSE/MC_Vortex_DSE_CSlot.cfg +++ b/specifications/VortexDSE/MC_Vortex_DSE_CSlot.cfg @@ -1,18 +1,15 @@ -\* TLC model configuration for Vortex_DSE_CSlot. -\* Two nodes, two message ids, slot horizon 2 — bounded but non-trivial. +\* Safety model. The horizon lives in MCNext, so no state constraint is +\* needed: the reachable state graph is already finite. -CONSTANT -Nodes = {n1, n2} -MsgIDs = {m1, m2} -MaxSlot = 2 +SPECIFICATION MCSpec -INIT Init -NEXT Next +CONSTANTS + Nodes = {n1, n2} + MsgIDs = {m1, m2} + MaxSlot = 2 -INVARIANT TypeInvariant +INVARIANT MCTypeInvariant INVARIANT NoFutureAdmission INVARIANT ExactlyOncePerNode INVARIANT NoPhantomProcess INVARIANT DecisionLocalityOnly - -CONSTRAINT StateConstraint diff --git a/specifications/VortexDSE/MC_Vortex_DSE_CSlot.tla b/specifications/VortexDSE/MC_Vortex_DSE_CSlot.tla index 26879b51..c34eed43 100644 --- a/specifications/VortexDSE/MC_Vortex_DSE_CSlot.tla +++ b/specifications/VortexDSE/MC_Vortex_DSE_CSlot.tla @@ -1,8 +1,54 @@ ---- MODULE MC_Vortex_DSE_CSlot ---- -(* TLC bounded model-checking harness for Vortex_DSE_CSlot. *) -(* Constants are assigned in MC_Vortex_DSE_CSlot.cfg: *) -(* Nodes = {n1, n2} *) -(* MsgIDs = {m1, m2} *) -(* MaxSlot = 2 *) +(***************************************************************************) +(* TLC harness for Vortex_DSE_CSlot. *) +(* *) +(* The specification itself has no slot horizon: Tick is unbounded and *) +(* DuplicateInject may forge any slot in Nat. The horizon is a *) +(* model-checking concern and lives here. *) +(* *) +(* It is imposed inside the actions rather than as a CONSTRAINT, so the *) +(* state graph is genuinely finite rather than merely truncated. That *) +(* matters for the liveness model: under a state constraint TLC discards *) +(* successor states, which can mask or invent violations of temporal *) +(* properties. *) +(***************************************************************************) EXTENDS Vortex_DSE_CSlot + +CONSTANT MaxSlot + +Slots == 0..MaxSlot + +\* The ticker stops at the horizon. +MCTick == + /\ current_slot < MaxSlot + /\ Tick + +MCNext == + \/ \E id \in MsgIDs : Submit(id) + \/ \E n \in Nodes, m \in network : Process(n, m) + \/ \E n \in Nodes : Crash(n) + \/ \E n \in Nodes : Rejoin(n) + \/ \E id \in MsgIDs, k \in Slots : DuplicateInject(id, k) + \/ MCTick + +MCSpec == Init /\ [][MCNext]_vars + +MCFairness == + /\ WF_vars(MCTick) + /\ \A n \in Nodes : WF_vars(Rejoin(n)) + /\ \A n \in Nodes : SF_vars(\E m \in network : Process(n, m)) + +MCLiveSpec == Init /\ [][MCNext]_vars /\ MCFairness + +\* Bounded counterpart of TickProgress, strengthened as suggested: once the +\* ticker reaches the horizon MCTick is permanently disabled, so the slot +\* counter stays there rather than merely visiting it. +MCTickProgress == <>[](current_slot = MaxSlot) + +\* Everything reachable in this model lies within the horizon. +MCTypeInvariant == + /\ TypeInvariant + /\ current_slot \in Slots + /\ \A m \in network : m.cslot \in Slots + ==== diff --git a/specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE.tla b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE.tla index 472138c8..bc8c8689 100644 --- a/specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE.tla +++ b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE.tla @@ -1,22 +1,52 @@ ---------------- MODULE MC_Vortex_DSE_CSlot_AE ---------------- -(* Apalache harness for Vortex_DSE_CSlot_AE. *) -(* Fixes constants and bundles the safety invariants for a single *) -(* symbolic (SMT-backed) check via Apalache. *) - +(***************************************************************************) +(* Harness for Vortex_DSE_CSlot_AE, used by both TLC and Apalache. *) +(* *) +(* The specification has no slot horizon; NextCslot advances without bound *) +(* and DuplicateInject may forge any slot in Nat. The horizon is a *) +(* model-checking concern and is imposed here inside the actions, not as a *) +(* CONSTRAINT, so no successor state is discarded while temporal properties *) +(* are checked. *) +(* *) +(* Invariants are deliberately left separate rather than bundled into one *) +(* conjunction, so that a checker reports which one was violated. *) +(***************************************************************************) EXTENDS Vortex_DSE_CSlot_AE +CONSTANT MaxSlot + +Slots == 0..MaxSlot + +MCNextCslot == + /\ current_slot < MaxSlot + /\ NextCslot + +MCNext == + \/ \E id \in MsgIDs : Submit(id) + \/ \E n \in Nodes, m \in network : Process(n, m) + \/ \E n \in Nodes : Freeze(n) + \/ Reconcile + \/ \E id \in MsgIDs, k \in Slots : DuplicateInject(id, k) + \/ MCNextCslot + +MCSpec == Init /\ [][MCNext]_vars + +MCFairness == + /\ SF_vars(Reconcile) + /\ SF_vars(MCNextCslot) + /\ \A n \in Nodes : WF_vars(Freeze(n)) + +MCLiveSpec == Init /\ [][MCNext]_vars /\ MCFairness + +MCTypeInvariant == + /\ TypeInvariant + /\ current_slot \in Slots + /\ \A m \in network : m.cslot \in Slots + +\* Apalache entry point: constants fixed symbolically. ConstInit == /\ Nodes = {"n1", "n2"} /\ MsgIDs = {"a", "b"} /\ MaxSlot = 1 -\* Conjunction of every safety invariant in the module. -AllInv == - /\ TypeInvariant - /\ MerkleAgreement - /\ CommittedSupersetsProcessed - /\ NoPhantomInCommitted - /\ NoReorderAcrossCslot - /\ PhaseProgressionValid - =============================================================== diff --git a/specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_liveness.cfg b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_liveness.cfg index 1ea3fefe..34d6b245 100644 --- a/specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_liveness.cfg +++ b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_liveness.cfg @@ -1,4 +1,6 @@ -SPECIFICATION LiveSpec +\* Liveness model. Bounded through MCNext rather than a CONSTRAINT. + +SPECIFICATION MCLiveSpec CONSTANTS Nodes = {n1, n2} @@ -8,6 +10,3 @@ CONSTANTS PROPERTIES EventualCommit EventualAgreement - -CONSTRAINT - StateConstraint diff --git a/specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_tiny.cfg b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_tiny.cfg index a18a6543..371f1fc3 100644 --- a/specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_tiny.cfg +++ b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_tiny.cfg @@ -1,4 +1,6 @@ -SPECIFICATION Spec +\* Safety model for the agreement layer, under adversarial replay. + +SPECIFICATION MCSpec CONSTANTS Nodes = {n1, n2} @@ -6,12 +8,9 @@ CONSTANTS MaxSlot = 2 INVARIANTS - TypeInvariant + MCTypeInvariant MerkleAgreement CommittedSupersetsProcessed NoPhantomInCommitted NoReorderAcrossCslot PhaseProgressionValid - -CONSTRAINT - StateConstraint diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot_Skew_tiny.cfg b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_Skew.cfg similarity index 64% rename from specifications/VortexDSE/Vortex_DSE_CSlot_Skew_tiny.cfg rename to specifications/VortexDSE/MC_Vortex_DSE_CSlot_Skew.cfg index f01ebab3..81d5f5f5 100644 --- a/specifications/VortexDSE/Vortex_DSE_CSlot_Skew_tiny.cfg +++ b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_Skew.cfg @@ -1,18 +1,17 @@ -SPECIFICATION Spec +\* Per-node clocks under bounded skew, with Byzantine slot/origin spoofing. + +SPECIFICATION MCSpec CONSTANTS Nodes = {n1, n2} MsgIDs = {m1} - MaxSlot = 2 MaxSkew = 1 + MaxSlot = 2 INVARIANTS - TypeInvariant + MCTypeInvariant BoundedSkew ExactlyOncePerNode CSlotLocalAdmission PersistedReflectsReality NoPhantomProcess - -CONSTRAINT - StateConstraint diff --git a/specifications/VortexDSE/MC_Vortex_DSE_CSlot_Skew.tla b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_Skew.tla new file mode 100644 index 00000000..bfcaa908 --- /dev/null +++ b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_Skew.tla @@ -0,0 +1,34 @@ +---- MODULE MC_Vortex_DSE_CSlot_Skew ---- +(***************************************************************************) +(* TLC harness for Vortex_DSE_CSlot_Skew. *) +(* *) +(* MaxSkew is a protocol parameter and stays in the specification: it is *) +(* the assumption the protocol relies on. MaxSlot is only a horizon for *) +(* model checking, so it lives here and bounds the actions directly. *) +(***************************************************************************) +EXTENDS Vortex_DSE_CSlot_Skew + +CONSTANT MaxSlot + +Slots == 0..MaxSlot + +MCTick(n) == + /\ node_slot[n] < MaxSlot + /\ SkewedTick(n) + +MCNext == + \/ \E id \in MsgIDs, n \in Nodes : Submit(id, n) + \/ \E n \in Nodes, m \in network : Process(n, m) + \/ \E n \in Nodes : Crash(n) + \/ \E n \in Nodes : Rejoin(n) + \/ \E id \in MsgIDs, k \in Slots, o \in Nodes : ByzantineInject(id, k, o) + \/ \E n \in Nodes : MCTick(n) + +MCSpec == Init /\ [][MCNext]_vars + +MCTypeInvariant == + /\ TypeInvariant + /\ node_slot \in [Nodes -> Slots] + /\ \A m \in network : m.cslot \in Slots + +==== diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot_TTL_tiny.cfg b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL.cfg similarity index 69% rename from specifications/VortexDSE/Vortex_DSE_CSlot_TTL_tiny.cfg rename to specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL.cfg index 617a208f..a12fb549 100644 --- a/specifications/VortexDSE/Vortex_DSE_CSlot_TTL_tiny.cfg +++ b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL.cfg @@ -1,4 +1,6 @@ -SPECIFICATION Spec +\* Safety model for the strict (opt-in TTL) admission mode. + +SPECIFICATION MCSpec CONSTANTS Nodes = {n1, n2} @@ -6,13 +8,10 @@ CONSTANTS MaxSlot = 4 INVARIANTS - TypeInvariant + MCTypeInvariant ExactlyOncePerNode CSlotStrictAdmission PersistedReflectsReality NoPhantomProcess DecisionLocalityOnly NoLateAdmission - -CONSTRAINT - StateConstraint diff --git a/specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL.tla b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL.tla new file mode 100644 index 00000000..b99c3b95 --- /dev/null +++ b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL.tla @@ -0,0 +1,42 @@ +---- MODULE MC_Vortex_DSE_CSlot_TTL ---- +(***************************************************************************) +(* TLC harness for Vortex_DSE_CSlot_TTL. *) +(* *) +(* As in MC_Vortex_DSE_CSlot, the slot horizon is a model-checking concern *) +(* and is imposed inside the actions rather than as a CONSTRAINT, so that *) +(* no successor state is discarded while temporal properties are checked. *) +(***************************************************************************) +EXTENDS Vortex_DSE_CSlot_TTL + +CONSTANT MaxSlot + +Slots == 0..MaxSlot + +MCTick == + /\ current_slot < MaxSlot + /\ Tick + +MCNext == + \/ \E id \in MsgIDs : Submit(id) + \/ \E n \in Nodes, m \in network : Process(n, m) + \/ \E n \in Nodes : Crash(n) + \/ \E n \in Nodes : Rejoin(n) + \/ \E id \in MsgIDs, k \in Slots : DuplicateInject(id, k) + \/ MCTick + +MCSpec == Init /\ [][MCNext]_vars + +MCFairness == + /\ WF_vars(MCTick) + /\ \A n \in Nodes : WF_vars(Rejoin(n)) + +MCLiveSpec == Init /\ [][MCNext]_vars /\ MCFairness + +MCTickProgress == <>[](current_slot = MaxSlot) + +MCTypeInvariant == + /\ TypeInvariant + /\ current_slot \in Slots + /\ \A m \in network : m.cslot \in Slots + +==== diff --git a/specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL_liveness.cfg b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL_liveness.cfg new file mode 100644 index 00000000..b289317c --- /dev/null +++ b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL_liveness.cfg @@ -0,0 +1,12 @@ +\* Liveness model. Bounded through MCNext rather than a CONSTRAINT. + +SPECIFICATION MCLiveSpec + +CONSTANTS + Nodes = {n1, n2} + MsgIDs = {m1} + MaxSlot = 2 + +PROPERTIES + MCTickProgress + EventualRejoin diff --git a/specifications/VortexDSE/MC_Vortex_DSE_CSlot_liveness.cfg b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_liveness.cfg new file mode 100644 index 00000000..0e7d9b76 --- /dev/null +++ b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_liveness.cfg @@ -0,0 +1,14 @@ +\* Liveness model. Bounded through MCNext rather than a CONSTRAINT, so no +\* successor states are discarded while temporal properties are checked. + +SPECIFICATION MCLiveSpec + +CONSTANTS + Nodes = {n1, n2} + MsgIDs = {m1} + MaxSlot = 1 + +PROPERTIES + MCTickProgress + EventualRejoin + EventualAdmission diff --git a/specifications/VortexDSE/README.md b/specifications/VortexDSE/README.md index 14e8ff8c..cd9cefe8 100644 --- a/specifications/VortexDSE/README.md +++ b/specifications/VortexDSE/README.md @@ -34,6 +34,14 @@ memory concession, not a stronger version of the protocol. | `Vortex_DSE_CSlot_AE` | the agreement layer: `Freeze`, `Reconcile`, `Commit` over the strict mode | | `Vortex_DSE_CSlot_AE_Proofs` | deductive proofs for the agreement layer | +None of these carries a slot horizon: the ticker is unbounded and the +adversary may forge any slot in `Nat`. Horizons are a model-checking concern +and live in the `MC_` modules, which bound the actions directly rather than +applying a state constraint — under a constraint TLC discards successor +states, which is unsound for the temporal properties. `MaxSkew` is the one +bound that stays in a specification, because it is an assumption the protocol +relies on rather than a checking artifact. + `Vortex_DSE_CSlot_AE` is specified over the strict admission rule; it is not a refinement of the default mode. Extending it to the late-tolerant rule requires restating what "no reordering across slots" means, and is not done here. @@ -46,9 +54,9 @@ in both cases. There are no `OMITTED` steps in these modules. | | obligations | | --- | --- | -| `Vortex_DSE_CSlot_Proofs` | 194 | -| `Vortex_DSE_CSlot_ExactlyOnce_Proof` | 131 | -| `Vortex_DSE_CSlot_AE_Proofs` | 34 | +| `Vortex_DSE_CSlot_Proofs` | 191 | +| `Vortex_DSE_CSlot_ExactlyOnce_Proof` | 128 | +| `Vortex_DSE_CSlot_AE_Proofs` | 32 | Every model completes in a few seconds. `Vortex_DSE_CSlot_AE` also carries Apalache type annotations, but no symbolic model is registered here; the models @@ -57,12 +65,10 @@ below are TLC only. ## Scope `Vortex_DSE_CSlot_Skew` bounds pairwise clock skew structurally, by forbidding -any tick that would breach the bound. It states the assumption; it does not +any tick that would breach `MaxSkew`. It states the assumption; it does not model the mechanism that maintains it. Likewise `Reconcile` is a single atomic step at specification level — the multi-round protocol underneath is out of scope here. Source repositories, including the whitepaper and the model-checking logs: - -Prepared with AI assistance. diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot.tla b/specifications/VortexDSE/Vortex_DSE_CSlot.tla index d74aae38..9de41803 100644 --- a/specifications/VortexDSE/Vortex_DSE_CSlot.tla +++ b/specifications/VortexDSE/Vortex_DSE_CSlot.tla @@ -34,9 +34,11 @@ CONSTANTS \* @type: Set(Str); Nodes, \* finite set of node identifiers \* @type: Set(Str); - MsgIDs, \* finite set of distinct message identifiers - \* @type: Int; - MaxSlot \* slot horizon (state-space bound) + MsgIDs \* finite set of distinct message identifiers + +\* Node liveness states, named rather than written as bare strings. +Up == "up" +Down == "down" VARIABLES \* @type: Int; @@ -48,11 +50,11 @@ VARIABLES \* @type: Str -> Set(Str); persisted, \* persisted[n] = mmap snapshot (survives crash) \* @type: Str -> Str; - node_state \* node_state[n] \in {"up", "down"} + node_state \* node_state[n] \in {Up, Down} vars == <> -MsgRecord == [id: MsgIDs, cslot: 0..MaxSlot] +MsgRecord == [id: MsgIDs, cslot: Nat] ------------------------------------------------------------------------------- (* INITIAL STATE *) @@ -62,7 +64,7 @@ Init == /\ network = {} /\ processed = [n \in Nodes |-> {}] /\ persisted = [n \in Nodes |-> {}] - /\ node_state = [n \in Nodes |-> "up"] + /\ node_state = [n \in Nodes |-> Up] ------------------------------------------------------------------------------- (* ACTIONS *) @@ -87,7 +89,7 @@ Submit(id) == Process(n, m) == /\ n \in Nodes /\ m \in network - /\ node_state[n] = "up" + /\ node_state[n] = Up /\ m.id \notin processed[n] \* exactly-once guard (local) /\ m.cslot <= current_slot \* admit present OR late (own slot) /\ processed' = [processed EXCEPT ![n] = @ \cup {m.id}] @@ -96,18 +98,18 @@ Process(n, m) == \* CRASH: node loses RAM. mmap snapshot in `persisted` survives. Crash(n) == /\ n \in Nodes - /\ node_state[n] = "up" + /\ node_state[n] = Up /\ persisted' = [persisted EXCEPT ![n] = processed[n]] - /\ node_state' = [node_state EXCEPT ![n] = "down"] + /\ node_state' = [node_state EXCEPT ![n] = Down] /\ processed' = [processed EXCEPT ![n] = {}] /\ UNCHANGED <> \* REJOIN: node recovers from mmap snapshot. processed = persisted. Rejoin(n) == /\ n \in Nodes - /\ node_state[n] = "down" + /\ node_state[n] = Down /\ processed' = [processed EXCEPT ![n] = persisted[n]] - /\ node_state' = [node_state EXCEPT ![n] = "up"] + /\ node_state' = [node_state EXCEPT ![n] = Up] /\ UNCHANGED <> \* Adversarial duplicate / replay injection. @@ -115,13 +117,12 @@ Rejoin(n) == \* or future). The C-slot gate must still hold. DuplicateInject(id, fake_cslot) == /\ id \in MsgIDs - /\ fake_cslot \in 0..MaxSlot + /\ fake_cslot \in Nat /\ network' = network \cup {[id |-> id, cslot |-> fake_cslot]} /\ UNCHANGED <> \* Slot ticker advances by 1. Tick == - /\ current_slot < MaxSlot /\ current_slot' = current_slot + 1 /\ UNCHANGED <> @@ -130,7 +131,7 @@ Next == \/ \E n \in Nodes, m \in network : Process(n, m) \/ \E n \in Nodes : Crash(n) \/ \E n \in Nodes : Rejoin(n) - \/ \E id \in MsgIDs, k \in 0..MaxSlot : DuplicateInject(id, k) + \/ \E id \in MsgIDs, k \in Nat : DuplicateInject(id, k) \/ Tick Spec == Init /\ [][Next]_vars @@ -139,11 +140,11 @@ Spec == Init /\ [][Next]_vars (* TYPE INVARIANT *) TypeInvariant == - /\ current_slot \in 0..MaxSlot - /\ network \subseteq MsgRecord + /\ current_slot \in Nat + /\ \A m \in network : m.id \in MsgIDs /\ m.cslot \in Nat /\ processed \in [Nodes -> SUBSET MsgIDs] /\ persisted \in [Nodes -> SUBSET MsgIDs] - /\ node_state \in [Nodes -> {"up", "down"}] + /\ node_state \in [Nodes -> {Up, Down}] ------------------------------------------------------------------------------- (* CORE SAFETY INVARIANTS *) @@ -168,7 +169,7 @@ NoFutureAdmission == \* mmap snapshot never invents ids that were not in the network. PersistedReflectsReality == \A n \in Nodes : - node_state[n] = "down" => + node_state[n] = Down => persisted[n] \subseteq {m.id : m \in network} \* I4: NO PHANTOM PROCESS. @@ -185,21 +186,15 @@ DecisionLocalityOnly == (id \in processed[n1] /\ id \in processed[n2]) => (\E m \in network : m.id = id) -------------------------------------------------------------------------------- -(* STATE-SPACE CONSTRAINT *) - -StateConstraint == - current_slot <= MaxSlot - ------------------------------------------------------------------------------- (* LIVENESS LAYER *) (* *) (* DESIGN NOTE — fairness assignment is intentional: *) (* *) -(* - SF(Tick): the slot ticker is fair, advancing eventually. This is a *) -(* physical-hardware assumption (the ticker process does not stall *) -(* forever). Strong fairness because Tick is always enabled until *) -(* current_slot reaches MaxSlot. *) +(* - WF(Tick): the slot ticker advances eventually. This is a physical- *) +(* hardware assumption (the ticker process does not stall forever). *) +(* Weak fairness suffices: Tick is unbounded here, so it is always *) +(* enabled and never intermittently disabled. *) (* *) (* - WF(Rejoin(n)) per node: a crashed node, given the chance, eventually *) (* rejoins. This corresponds to operational recovery (operator restart). *) @@ -216,20 +211,22 @@ StateConstraint == (***************************************************************************) Fairness == - /\ SF_vars(Tick) + /\ WF_vars(Tick) /\ \A n \in Nodes : WF_vars(Rejoin(n)) /\ \A n \in Nodes : SF_vars(\E m \in network : Process(n, m)) LiveSpec == Init /\ [][Next]_vars /\ Fairness \* L1 TICK PROGRESS. -\* Under SF(Tick), the slot counter eventually reaches the horizon. -TickProgress == <>(current_slot = MaxSlot) +\* Under WF(Tick) the slot counter grows without bound: no slot index is +\* ever a ceiling. A model-checkable form, bounded by a horizon, is in +\* MC_Vortex_DSE_CSlot. +TickProgress == \A k \in Nat : <>(current_slot > k) \* L2 EVENTUAL REJOIN. -\* Every crashed node eventually returns to "up", under WF(Rejoin(n)). +\* Every crashed node eventually returns to Up, under WF(Rejoin(n)). EventualRejoin == - \A n \in Nodes : (node_state[n] = "down") ~> (node_state[n] = "up") + \A n \in Nodes : (node_state[n] = Down) ~> (node_state[n] = Up) \* L3 EVENTUAL ADMISSION (VALIDITY — the property the new rule recovers). \* Once a message is in the network, every node eventually admits it. diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot_AE.tla b/specifications/VortexDSE/Vortex_DSE_CSlot_AE.tla index 23593276..9524d9e9 100644 --- a/specifications/VortexDSE/Vortex_DSE_CSlot_AE.tla +++ b/specifications/VortexDSE/Vortex_DSE_CSlot_AE.tla @@ -72,9 +72,12 @@ CONSTANTS \* @type: Set(Str); Nodes, \* finite set of node identifiers \* @type: Set(Str); - MsgIDs, \* finite set of distinct message identifiers - \* @type: Int; - MaxSlot \* slot horizon (state-space bound) + MsgIDs \* finite set of distinct message identifiers + +\* AE phase names, rather than bare strings. +Open == "open" +Frozen == "frozen" +Committed == "committed" VARIABLES \* @type: Int; @@ -84,13 +87,13 @@ VARIABLES \* @type: Str -> Set(Str); processed, \* processed[n] = msg ids admitted by n in current cslot \* @type: Str -> Str; - phase, \* phase[n] \in {"open", "frozen", "committed"} + phase, \* phase[n] \in {Open, Frozen, Committed} \* @type: Str -> Set(Str); committed_set \* committed_set[n] = AE-final input set for n at current cslot vars == <> -MsgRecord == [id: MsgIDs, cslot: 0..MaxSlot] +MsgRecord == [id: MsgIDs, cslot: Nat] ------------------------------------------------------------------------------- (* INITIAL STATE *) @@ -99,7 +102,7 @@ Init == /\ current_slot = 0 /\ network = {} /\ processed = [n \in Nodes |-> {}] - /\ phase = [n \in Nodes |-> "open"] + /\ phase = [n \in Nodes |-> Open] /\ committed_set = [n \in Nodes |-> {}] ------------------------------------------------------------------------------- @@ -117,7 +120,7 @@ Submit(id) == Process(n, m) == /\ n \in Nodes /\ m \in network - /\ phase[n] = "open" + /\ phase[n] = Open /\ m.id \notin processed[n] /\ m.cslot = current_slot /\ processed' = [processed EXCEPT ![n] = @ \cup {m.id}] @@ -127,8 +130,8 @@ Process(n, m) == \* In implementation: triggered by reaching the freeze deadline (~0.75 * Delta_t). Freeze(n) == /\ n \in Nodes - /\ phase[n] = "open" - /\ phase' = [phase EXCEPT ![n] = "frozen"] + /\ phase[n] = Open + /\ phase' = [phase EXCEPT ![n] = Frozen] /\ UNCHANGED <> \* Reconcile: abstract AE protocol. When ALL nodes are frozen, they @@ -136,16 +139,16 @@ Freeze(n) == \* equality. Atomic step at spec level; multi-round Bloom+Merkle at impl level. \* Models assumption A3 (in-spec loss envelope). Reconcile == - /\ \A n \in Nodes : phase[n] = "frozen" + /\ \A n \in Nodes : phase[n] = Frozen /\ LET union_view == UNION { processed[n] : n \in Nodes } IN committed_set' = [n \in Nodes |-> union_view] - /\ phase' = [n \in Nodes |-> "committed"] + /\ phase' = [n \in Nodes |-> Committed] /\ UNCHANGED <> \* Adversarial duplicate / replay injection. DuplicateInject(id, fake_cslot) == /\ id \in MsgIDs - /\ fake_cslot \in 0..MaxSlot + /\ fake_cslot \in Nat /\ network' = network \cup {[id |-> id, cslot |-> fake_cslot]} /\ UNCHANGED <> @@ -155,11 +158,10 @@ DuplicateInject(id, fake_cslot) == \* on next Reconcile (we do not retain history in-model; the implementation \* logs each committed_set externally as the cslot-final ledger entry). NextCslot == - /\ current_slot < MaxSlot - /\ \A n \in Nodes : phase[n] = "committed" + /\ \A n \in Nodes : phase[n] = Committed /\ current_slot' = current_slot + 1 /\ processed' = [n \in Nodes |-> {}] - /\ phase' = [n \in Nodes |-> "open"] + /\ phase' = [n \in Nodes |-> Open] /\ UNCHANGED <> Next == @@ -167,7 +169,7 @@ Next == \/ \E n \in Nodes, m \in network : Process(n, m) \/ \E n \in Nodes : Freeze(n) \/ Reconcile - \/ \E id \in MsgIDs, k \in 0..MaxSlot : DuplicateInject(id, k) + \/ \E id \in MsgIDs, k \in Nat : DuplicateInject(id, k) \/ NextCslot Spec == Init /\ [][Next]_vars @@ -176,10 +178,10 @@ Spec == Init /\ [][Next]_vars (* TYPE INVARIANT *) TypeInvariant == - /\ current_slot \in 0..MaxSlot - /\ network \subseteq MsgRecord + /\ current_slot \in Nat + /\ \A m \in network : m.id \in MsgIDs /\ m.cslot \in Nat /\ processed \in [Nodes -> SUBSET MsgIDs] - /\ phase \in [Nodes -> {"open", "frozen", "committed"}] + /\ phase \in [Nodes -> {Open, Frozen, Committed}] /\ committed_set \in [Nodes -> SUBSET MsgIDs] ------------------------------------------------------------------------------- @@ -191,7 +193,7 @@ TypeInvariant == \* This is the formal counterpart of the AE design guarantee. MerkleAgreement == \A n1, n2 \in Nodes : - (phase[n1] = "committed" /\ phase[n2] = "committed") + (phase[n1] = Committed /\ phase[n2] = Committed) => committed_set[n1] = committed_set[n2] \* AE-I2: COMMITTED IS SUPERSET OF LOCAL PROCESSED. @@ -201,7 +203,7 @@ MerkleAgreement == \* view. (This rules out the "frozen and then dropped" failure mode.) CommittedSupersetsProcessed == \A n \in Nodes : - phase[n] = "committed" => processed[n] \subseteq committed_set[n] + phase[n] = Committed => processed[n] \subseteq committed_set[n] \* AE-I3: NO PHANTOM IN COMMITTED. \* Every id in any committed_set corresponds to a real network record with @@ -209,7 +211,7 @@ CommittedSupersetsProcessed == \* admissions. NoPhantomInCommitted == \A n \in Nodes : - phase[n] = "committed" => + phase[n] = Committed => \A id \in committed_set[n] : \E m \in network : m.id = id /\ m.cslot = current_slot @@ -226,13 +228,7 @@ NoReorderAcrossCslot == \* transitions are enforced structurally by the Freeze, Reconcile, NextCslot \* guards; declared here as an explicit type-level safety net. PhaseProgressionValid == - \A n \in Nodes : phase[n] \in {"open", "frozen", "committed"} - -------------------------------------------------------------------------------- -(* STATE-SPACE CONSTRAINT *) - -StateConstraint == - current_slot <= MaxSlot + \A n \in Nodes : phase[n] \in {Open, Frozen, Committed} ------------------------------------------------------------------------------- (* LIVENESS LAYER *) @@ -256,15 +252,15 @@ LiveSpec == Init /\ [][Next]_vars /\ Fairness \* Every node eventually commits for the cslot it participates in. EventualCommit == \A n \in Nodes : - (phase[n] = "open") ~> (phase[n] = "committed") + (phase[n] = Open) ~> (phase[n] = Committed) \* AE-L2: EVENTUAL AGREEMENT. \* If two nodes both reach the committed phase, MerkleAgreement holds. \* (Safety + liveness composition.) EventualAgreement == \A n1, n2 \in Nodes : - (phase[n1] = "open" /\ phase[n2] = "open") - ~> (phase[n1] = "committed" /\ phase[n2] = "committed" + (phase[n1] = Open /\ phase[n2] = Open) + ~> (phase[n1] = Committed /\ phase[n2] = Committed /\ committed_set[n1] = committed_set[n2]) ============================================================================= diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot_AE_Proofs.tla b/specifications/VortexDSE/Vortex_DSE_CSlot_AE_Proofs.tla index 87954eb6..b72efdf9 100644 --- a/specifications/VortexDSE/Vortex_DSE_CSlot_AE_Proofs.tla +++ b/specifications/VortexDSE/Vortex_DSE_CSlot_AE_Proofs.tla @@ -11,16 +11,15 @@ EXTENDS Vortex_DSE_CSlot_AE, TLAPS -ASSUME MaxSlotType == MaxSlot \in Nat ------------------------------------------------------------------------------- (* PART A — TYPE INVARIANT *) LEMMA InitType == Init => TypeInvariant - BY MaxSlotType DEF Init, TypeInvariant, MsgRecord + BY DEF Init, TypeInvariant, MsgRecord LEMMA NextType == TypeInvariant /\ [Next]_vars => TypeInvariant' - <1> USE MaxSlotType DEF TypeInvariant, MsgRecord, vars + <1> USE DEF TypeInvariant, MsgRecord, vars <1> SUFFICES ASSUME TypeInvariant, [Next]_vars PROVE TypeInvariant' OBVIOUS @@ -32,7 +31,7 @@ LEMMA NextType == TypeInvariant /\ [Next]_vars => TypeInvariant' BY <1>3 DEF Freeze <1>4. CASE Reconcile BY <1>4 DEF Reconcile - <1>5. CASE \E id \in MsgIDs, k \in 0..MaxSlot : DuplicateInject(id, k) + <1>5. CASE \E id \in MsgIDs, k \in Nat : DuplicateInject(id, k) BY <1>5 DEF DuplicateInject <1>6. CASE NextCslot BY <1>6 DEF NextCslot diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot_ExactlyOnce_Proof.tla b/specifications/VortexDSE/Vortex_DSE_CSlot_ExactlyOnce_Proof.tla index 0b122981..f8ad9def 100644 --- a/specifications/VortexDSE/Vortex_DSE_CSlot_ExactlyOnce_Proof.tla +++ b/specifications/VortexDSE/Vortex_DSE_CSlot_ExactlyOnce_Proof.tla @@ -45,7 +45,6 @@ EXTENDS Vortex_DSE_CSlot, TLAPS -ASSUME MaxSlotType == MaxSlot \in Nat ------------------------------------------------------------------------------- (* THE INVARIANT WE PROVE *) @@ -104,9 +103,8 @@ LEMMA InitStrictExactlyOnce == Init => StrictExactlyOnceInv \* discharged in the theorem below via the machine-checked TypeCorrect. LEMMA NextStrictExactlyOnce == TypeInvariant /\ StrictExactlyOnceInv /\ [Next]_vars => StrictExactlyOnceInv' - <1> USE MaxSlotType - DEF StrictExactlyOnceInv, ExactlyOnceCore, PersistedClean, - TypeInvariant, MsgRecord, vars + <1> USE DEF StrictExactlyOnceInv, ExactlyOnceCore, PersistedClean, + TypeInvariant, MsgRecord, vars <1> SUFFICES ASSUME TypeInvariant, StrictExactlyOnceInv, [Next]_vars PROVE StrictExactlyOnceInv' OBVIOUS @@ -209,8 +207,8 @@ LEMMA NextStrictExactlyOnce == \* the injected id was already processed — but here we only need to show \* the invariant is preserved by the injection itself (not by Process). \* Since processed' = processed and persisted' = persisted, trivial. - <1>5. CASE \E id \in MsgIDs, k \in 0..MaxSlot : DuplicateInject(id, k) - <2> PICK i \in MsgIDs, k \in 0..MaxSlot : DuplicateInject(i, k) + <1>5. CASE \E id \in MsgIDs, k \in Nat : DuplicateInject(id, k) + <2> PICK i \in MsgIDs, k \in Nat : DuplicateInject(i, k) BY <1>5 <2>1. /\ processed' = processed /\ persisted' = persisted @@ -248,10 +246,10 @@ LEMMA NextStrictExactlyOnce == \* machine-checked TypeCorrect in Vortex_DSE_CSlot_Proofs.tla, reproduced here \* so this proof is self-contained. LEMMA InitType == Init => TypeInvariant - BY MaxSlotType DEF Init, TypeInvariant, MsgRecord + BY DEF Init, TypeInvariant, MsgRecord LEMMA NextType == TypeInvariant /\ [Next]_vars => TypeInvariant' - <1> USE MaxSlotType DEF TypeInvariant, MsgRecord, vars + <1> USE DEF TypeInvariant, MsgRecord, vars <1> SUFFICES ASSUME TypeInvariant, [Next]_vars PROVE TypeInvariant' OBVIOUS @@ -263,7 +261,7 @@ LEMMA NextType == TypeInvariant /\ [Next]_vars => TypeInvariant' BY <1>3 DEF Crash <1>4. CASE \E n \in Nodes : Rejoin(n) BY <1>4 DEF Rejoin - <1>5. CASE \E id \in MsgIDs, k \in 0..MaxSlot : DuplicateInject(id, k) + <1>5. CASE \E id \in MsgIDs, k \in Nat : DuplicateInject(id, k) BY <1>5 DEF DuplicateInject <1>6. CASE Tick BY <1>6 DEF Tick diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot_Proofs.tla b/specifications/VortexDSE/Vortex_DSE_CSlot_Proofs.tla index 5986128c..584b436c 100644 --- a/specifications/VortexDSE/Vortex_DSE_CSlot_Proofs.tla +++ b/specifications/VortexDSE/Vortex_DSE_CSlot_Proofs.tla @@ -33,18 +33,17 @@ EXTENDS Vortex_DSE_CSlot, TLAPS -ASSUME MaxSlotType == MaxSlot \in Nat ------------------------------------------------------------------------------- (* PART A — TYPE INVARIANT (type-correctness) *) \* (1) The initial state satisfies the type invariant. LEMMA InitType == Init => TypeInvariant - BY MaxSlotType DEF Init, TypeInvariant, MsgRecord + BY DEF Init, TypeInvariant, MsgRecord \* (2) Every step (or stutter) preserves the type invariant. LEMMA NextType == TypeInvariant /\ [Next]_vars => TypeInvariant' - <1> USE MaxSlotType DEF TypeInvariant, MsgRecord, vars + <1> USE DEF TypeInvariant, MsgRecord, vars <1> SUFFICES ASSUME TypeInvariant, [Next]_vars PROVE TypeInvariant' OBVIOUS @@ -56,7 +55,7 @@ LEMMA NextType == TypeInvariant /\ [Next]_vars => TypeInvariant' BY <1>3 DEF Crash <1>4. CASE \E n \in Nodes : Rejoin(n) BY <1>4 DEF Rejoin - <1>5. CASE \E id \in MsgIDs, k \in 0..MaxSlot : DuplicateInject(id, k) + <1>5. CASE \E id \in MsgIDs, k \in Nat : DuplicateInject(id, k) BY <1>5 DEF DuplicateInject <1>6. CASE Tick BY <1>6 DEF Tick @@ -93,7 +92,7 @@ LEMMA InitSafe == Init => SafeInv \* (2) Inductive step for the strengthened invariant. LEMMA NextSafe == SafeInv /\ [Next]_vars => SafeInv' - <1> USE MaxSlotType DEF SafeInv, TypeInvariant, MsgRecord, + <1> USE DEF SafeInv, TypeInvariant, MsgRecord, NoFutureAdmission, PersistedSafe, vars <1> SUFFICES ASSUME SafeInv, [Next]_vars PROVE SafeInv' @@ -197,8 +196,8 @@ LEMMA NextSafe == SafeInv /\ [Next]_vars => SafeInv' <3> QED BY <3>1, <3>2 <2> QED BY <2>2, <2>3 \* ---- DuplicateInject: network grows with an arbitrary cslot; gate holds. ---- - <1>5. CASE \E id \in MsgIDs, k \in 0..MaxSlot : DuplicateInject(id, k) - <2> PICK i \in MsgIDs, k \in 0..MaxSlot : DuplicateInject(i, k) + <1>5. CASE \E id \in MsgIDs, k \in Nat : DuplicateInject(id, k) + <2> PICK i \in MsgIDs, k \in Nat : DuplicateInject(i, k) BY <1>5 <2>1. /\ network' = network \cup {[id |-> i, cslot |-> k]} /\ processed' = processed diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot_Skew.tla b/specifications/VortexDSE/Vortex_DSE_CSlot_Skew.tla index 3e001a60..a6ba6f68 100644 --- a/specifications/VortexDSE/Vortex_DSE_CSlot_Skew.tla +++ b/specifications/VortexDSE/Vortex_DSE_CSlot_Skew.tla @@ -20,7 +20,11 @@ EXTENDS Naturals, FiniteSets -CONSTANTS Nodes, MsgIDs, MaxSlot, MaxSkew +CONSTANTS Nodes, MsgIDs, MaxSkew + +\* Node liveness states, named rather than written as bare strings. +Up == "up" +Down == "down" VARIABLES node_slot, \* [Nodes -> Int] per-node clock @@ -31,7 +35,7 @@ VARIABLES vars == <> -MsgRecord == [id: MsgIDs, cslot: 0..MaxSlot, origin: Nodes] +MsgRecord == [id: MsgIDs, cslot: Nat, origin: Nodes] ------------------------------------------------------------------------------- Init == @@ -39,14 +43,14 @@ Init == /\ network = {} /\ processed = [n \in Nodes |-> {}] /\ persisted = [n \in Nodes |-> {}] - /\ node_state = [n \in Nodes |-> "up"] + /\ node_state = [n \in Nodes |-> Up] ------------------------------------------------------------------------------- \* Submit: sender n stamps with its own local slot. Submit(id, n) == /\ id \in MsgIDs /\ n \in Nodes - /\ node_state[n] = "up" + /\ node_state[n] = Up /\ id \notin {m.id : m \in network} /\ \A x \in Nodes : id \notin processed[x] /\ network' = network \cup {[id |-> id, cslot |-> node_slot[n], origin |-> n]} @@ -56,7 +60,7 @@ Submit(id, n) == Process(n, m) == /\ n \in Nodes /\ m \in network - /\ node_state[n] = "up" + /\ node_state[n] = Up /\ m.id \notin processed[n] /\ m.cslot = node_slot[n] /\ processed' = [processed EXCEPT ![n] = @ \cup {m.id}] @@ -64,23 +68,23 @@ Process(n, m) == Crash(n) == /\ n \in Nodes - /\ node_state[n] = "up" + /\ node_state[n] = Up /\ persisted' = [persisted EXCEPT ![n] = processed[n]] - /\ node_state' = [node_state EXCEPT ![n] = "down"] + /\ node_state' = [node_state EXCEPT ![n] = Down] /\ processed' = [processed EXCEPT ![n] = {}] /\ UNCHANGED <> Rejoin(n) == /\ n \in Nodes - /\ node_state[n] = "down" + /\ node_state[n] = Down /\ processed' = [processed EXCEPT ![n] = persisted[n]] - /\ node_state' = [node_state EXCEPT ![n] = "up"] + /\ node_state' = [node_state EXCEPT ![n] = Up] /\ UNCHANGED <> \* Byzantine inject: adversary spoofs both cslot AND origin. ByzantineInject(id, fake_cslot, fake_origin) == /\ id \in MsgIDs - /\ fake_cslot \in 0..MaxSlot + /\ fake_cslot \in Nat /\ fake_origin \in Nodes /\ network' = network \cup {[id |-> id, cslot |-> fake_cslot, origin |-> fake_origin]} @@ -89,7 +93,6 @@ ByzantineInject(id, fake_cslot, fake_origin) == \* Per-node tick, bounded by MaxSkew vs slowest node. SkewedTick(n) == /\ n \in Nodes - /\ node_slot[n] < MaxSlot /\ \A other \in Nodes : (node_slot[n] + 1) - node_slot[other] <= MaxSkew /\ node_slot' = [node_slot EXCEPT ![n] = @ + 1] @@ -100,7 +103,7 @@ Next == \/ \E n \in Nodes, m \in network : Process(n, m) \/ \E n \in Nodes : Crash(n) \/ \E n \in Nodes : Rejoin(n) - \/ \E id \in MsgIDs, k \in 0..MaxSlot, o \in Nodes : ByzantineInject(id, k, o) + \/ \E id \in MsgIDs, k \in Nat, o \in Nodes : ByzantineInject(id, k, o) \/ \E n \in Nodes : SkewedTick(n) Spec == Init /\ [][Next]_vars @@ -109,11 +112,11 @@ Spec == Init /\ [][Next]_vars (* INVARIANTS *) TypeInvariant == - /\ node_slot \in [Nodes -> 0..MaxSlot] - /\ network \subseteq MsgRecord + /\ node_slot \in [Nodes -> Nat] + /\ \A m \in network : m.id \in MsgIDs /\ m.cslot \in Nat /\ m.origin \in Nodes /\ processed \in [Nodes -> SUBSET MsgIDs] /\ persisted \in [Nodes -> SUBSET MsgIDs] - /\ node_state \in [Nodes -> {"up", "down"}] + /\ node_state \in [Nodes -> {Up, Down}] \* The Tick guard guarantees this; it is asserted as invariant to make \* the skew bound an explicit, machine-checked property. @@ -134,14 +137,12 @@ CSlotLocalAdmission == PersistedReflectsReality == \A n \in Nodes : - node_state[n] = "down" => + node_state[n] = Down => persisted[n] \subseteq {m.id : m \in network} NoPhantomProcess == \A n \in Nodes : processed[n] \subseteq {m.id : m \in network} ------------------------------------------------------------------------------- -StateConstraint == - \A n \in Nodes : node_slot[n] <= MaxSlot ============================================================================= diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot_TTL.tla b/specifications/VortexDSE/Vortex_DSE_CSlot_TTL.tla index f9dde694..202285c9 100644 --- a/specifications/VortexDSE/Vortex_DSE_CSlot_TTL.tla +++ b/specifications/VortexDSE/Vortex_DSE_CSlot_TTL.tla @@ -29,9 +29,11 @@ CONSTANTS \* @type: Set(Str); Nodes, \* finite set of node identifiers \* @type: Set(Str); - MsgIDs, \* finite set of distinct message identifiers - \* @type: Int; - MaxSlot \* slot horizon (state-space bound) + MsgIDs \* finite set of distinct message identifiers + +\* Node liveness states, named rather than written as bare strings. +Up == "up" +Down == "down" VARIABLES \* @type: Int; @@ -43,11 +45,11 @@ VARIABLES \* @type: Str -> Set(Str); persisted, \* persisted[n] = persistent snapshot (survives crash) \* @type: Str -> Str; - node_state \* node_state[n] \in {"up", "down"} + node_state \* node_state[n] \in {Up, Down} vars == <> -MsgRecord == [id: MsgIDs, cslot: 0..MaxSlot] +MsgRecord == [id: MsgIDs, cslot: Nat] ------------------------------------------------------------------------------- (* INITIAL STATE *) @@ -57,7 +59,7 @@ Init == /\ network = {} /\ processed = [n \in Nodes |-> {}] /\ persisted = [n \in Nodes |-> {}] - /\ node_state = [n \in Nodes |-> "up"] + /\ node_state = [n \in Nodes |-> Up] ------------------------------------------------------------------------------- (* ACTIONS *) @@ -80,7 +82,7 @@ Submit(id) == Process(n, m) == /\ n \in Nodes /\ m \in network - /\ node_state[n] = "up" + /\ node_state[n] = Up /\ m.id \notin processed[n] \* exactly-once guard (local) /\ m.cslot = current_slot \* STRICT C-slot equality /\ processed' = [processed EXCEPT ![n] = @ \cup {m.id}] @@ -89,18 +91,18 @@ Process(n, m) == \* CRASH: node loses RAM. persistent snapshot in `persisted` survives. Crash(n) == /\ n \in Nodes - /\ node_state[n] = "up" + /\ node_state[n] = Up /\ persisted' = [persisted EXCEPT ![n] = processed[n]] - /\ node_state' = [node_state EXCEPT ![n] = "down"] + /\ node_state' = [node_state EXCEPT ![n] = Down] /\ processed' = [processed EXCEPT ![n] = {}] /\ UNCHANGED <> \* REJOIN: node recovers from persistent snapshot. processed = persisted. Rejoin(n) == /\ n \in Nodes - /\ node_state[n] = "down" + /\ node_state[n] = Down /\ processed' = [processed EXCEPT ![n] = persisted[n]] - /\ node_state' = [node_state EXCEPT ![n] = "up"] + /\ node_state' = [node_state EXCEPT ![n] = Up] /\ UNCHANGED <> \* Adversarial duplicate / replay injection. @@ -108,13 +110,12 @@ Rejoin(n) == \* or future). The C-slot gate must still hold. DuplicateInject(id, fake_cslot) == /\ id \in MsgIDs - /\ fake_cslot \in 0..MaxSlot + /\ fake_cslot \in Nat /\ network' = network \cup {[id |-> id, cslot |-> fake_cslot]} /\ UNCHANGED <> \* Slot ticker advances by 1. Tick == - /\ current_slot < MaxSlot /\ current_slot' = current_slot + 1 /\ UNCHANGED <> @@ -123,7 +124,7 @@ Next == \/ \E n \in Nodes, m \in network : Process(n, m) \/ \E n \in Nodes : Crash(n) \/ \E n \in Nodes : Rejoin(n) - \/ \E id \in MsgIDs, k \in 0..MaxSlot : DuplicateInject(id, k) + \/ \E id \in MsgIDs, k \in Nat : DuplicateInject(id, k) \/ Tick Spec == Init /\ [][Next]_vars @@ -132,11 +133,11 @@ Spec == Init /\ [][Next]_vars (* TYPE INVARIANT *) TypeInvariant == - /\ current_slot \in 0..MaxSlot - /\ network \subseteq MsgRecord + /\ current_slot \in Nat + /\ \A m \in network : m.id \in MsgIDs /\ m.cslot \in Nat /\ processed \in [Nodes -> SUBSET MsgIDs] /\ persisted \in [Nodes -> SUBSET MsgIDs] - /\ node_state \in [Nodes -> {"up", "down"}] + /\ node_state \in [Nodes -> {Up, Down}] ------------------------------------------------------------------------------- (* CORE SAFETY INVARIANTS *) @@ -162,7 +163,7 @@ CSlotStrictAdmission == \* persistent snapshot never invents ids that were not in the network. PersistedReflectsReality == \A n \in Nodes : - node_state[n] = "down" => + node_state[n] = Down => persisted[n] \subseteq {m.id : m \in network} \* I4: NO PHANTOM PROCESS. @@ -196,18 +197,16 @@ NoLateAdmission == ------------------------------------------------------------------------------- (* STATE-SPACE CONSTRAINT *) -StateConstraint == - current_slot <= MaxSlot ------------------------------------------------------------------------------- (* LIVENESS LAYER *) (* *) (* DESIGN NOTE — fairness assignment is intentional: *) (* *) -(* - SF(Tick): the slot ticker is fair, advancing eventually. This is a *) -(* physical-hardware assumption (the ticker process does not stall *) -(* forever). Strong fairness because Tick is always enabled until *) -(* current_slot reaches MaxSlot. *) +(* - WF(Tick): the slot ticker advances eventually. This is a physical- *) +(* hardware assumption (the ticker process does not stall forever). *) +(* Weak fairness suffices: Tick is unbounded here, so it is always *) +(* enabled and never intermittently disabled. *) (* *) (* - WF(Rejoin(n)) per node: a crashed node, given the chance, eventually *) (* rejoins. This corresponds to operational recovery (operator restart). *) @@ -223,18 +222,19 @@ StateConstraint == (***************************************************************************) Fairness == - /\ SF_vars(Tick) + /\ WF_vars(Tick) /\ \A n \in Nodes : WF_vars(Rejoin(n)) LiveSpec == Init /\ [][Next]_vars /\ Fairness \* L1 TICK PROGRESS. -\* Under SF(Tick), the slot counter eventually reaches the horizon. -TickProgress == <>(current_slot = MaxSlot) +\* Under WF(Tick) the slot counter grows without bound. A model-checkable +\* form, bounded by a horizon, is in MC_Vortex_DSE_CSlot_TTL. +TickProgress == \A k \in Nat : <>(current_slot > k) \* L2 EVENTUAL REJOIN. -\* Every crashed node eventually returns to "up", under WF(Rejoin(n)). +\* Every crashed node eventually returns to Up, under WF(Rejoin(n)). EventualRejoin == - \A n \in Nodes : (node_state[n] = "down") ~> (node_state[n] = "up") + \A n \in Nodes : (node_state[n] = Down) ~> (node_state[n] = Up) ============================================================================= diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot_TTL_liveness.cfg b/specifications/VortexDSE/Vortex_DSE_CSlot_TTL_liveness.cfg deleted file mode 100644 index f5aa6646..00000000 --- a/specifications/VortexDSE/Vortex_DSE_CSlot_TTL_liveness.cfg +++ /dev/null @@ -1,13 +0,0 @@ -SPECIFICATION LiveSpec - -CONSTANTS - Nodes = {n1, n2} - MsgIDs = {m1} - MaxSlot = 2 - -PROPERTIES - TickProgress - EventualRejoin - -CONSTRAINT - StateConstraint diff --git a/specifications/VortexDSE/manifest.json b/specifications/VortexDSE/manifest.json index bb1c91b9..035575dc 100644 --- a/specifications/VortexDSE/manifest.json +++ b/specifications/VortexDSE/manifest.json @@ -20,6 +20,12 @@ "result": "success", "totalStates": 186367, "distinctStates": 18903 + }, + { + "path": "specifications/VortexDSE/MC_Vortex_DSE_CSlot_liveness.cfg", + "runtime": "00:00:01", + "mode": "exhaustive search", + "result": "success" } ] }, @@ -43,6 +49,40 @@ } ] }, + { + "path": "specifications/VortexDSE/MC_Vortex_DSE_CSlot_Skew.tla", + "features": [], + "models": [ + { + "path": "specifications/VortexDSE/MC_Vortex_DSE_CSlot_Skew.cfg", + "runtime": "00:00:01", + "mode": "exhaustive search", + "result": "success", + "totalStates": 96481, + "distinctStates": 10099 + } + ] + }, + { + "path": "specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL.tla", + "features": [], + "models": [ + { + "path": "specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL.cfg", + "runtime": "00:00:05", + "mode": "exhaustive search", + "result": "success", + "totalStates": 8084795, + "distinctStates": 608477 + }, + { + "path": "specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL_liveness.cfg", + "runtime": "00:00:01", + "mode": "exhaustive search", + "result": "success" + } + ] + }, { "path": "specifications/VortexDSE/Vortex_DSE_CSlot.tla", "features": [], @@ -80,36 +120,12 @@ { "path": "specifications/VortexDSE/Vortex_DSE_CSlot_Skew.tla", "features": [], - "models": [ - { - "path": "specifications/VortexDSE/Vortex_DSE_CSlot_Skew_tiny.cfg", - "runtime": "00:00:01", - "mode": "exhaustive search", - "result": "success", - "totalStates": 96481, - "distinctStates": 10099 - } - ] + "models": [] }, { "path": "specifications/VortexDSE/Vortex_DSE_CSlot_TTL.tla", "features": [], - "models": [ - { - "path": "specifications/VortexDSE/Vortex_DSE_CSlot_TTL_liveness.cfg", - "runtime": "00:00:01", - "mode": "exhaustive search", - "result": "success" - }, - { - "path": "specifications/VortexDSE/Vortex_DSE_CSlot_TTL_tiny.cfg", - "runtime": "00:00:05", - "mode": "exhaustive search", - "result": "success", - "totalStates": 8084795, - "distinctStates": 608477 - } - ] + "models": [] } ] } From 9b3d8a985135b239815438264fe4bf9c6671ee61 Mon Sep 17 00:00:00 2001 From: Vasilis Nasopoulos Date: Wed, 5 Aug 2026 20:10:29 +0300 Subject: [PATCH 3/6] Apply the TLA+ review guidelines Four things in the review guidelines were not being followed. Constants now carry named assumptions. All four specifications declared Nodes and MsgIDs with nothing constraining them, and Skew's MaxSkew with nothing saying it is a natural number. The guidelines call this crucial for TLAPS, and these modules do carry proofs. Type invariants are back to the var \in S form: network \subseteq MsgRecord rather than a quantifier over its elements. MsgRecord ranges over Nat and so cannot be enumerated, which is why the MC module carries its own bounded MCTypeInvariant for TLC. Strong fairness on Process is now justified by measurement rather than assertion. Weak fairness was tried, as the guidelines ask: the liveness model reports a temporal-property violation under it, because a crash intermittently disables Process. The module says so. The horizon stays inside MCTick rather than moving to a state CONSTRAINT, which the guidelines otherwise prefer. A constraint was tried first and does not work here: TLC evaluates invariants on the state that crosses the boundary before the constraint discards it, so with MaxSlot = 2 a Tick reaches current_slot = 3 and any invariant mentioning the horizon fails there. The reason is recorded in the module header rather than left as an unexplained deviation. Seven TLC models, all completing in under five seconds. The three TLAPS modules discharge 191, 128 and 32 obligations and exit 0 under tlapm --strict. Co-authored-by: Claude Opus 5 Signed-off-by: Vasilis Nasopoulos --- .../VortexDSE/MC_Vortex_DSE_CSlot.cfg | 6 ++- .../VortexDSE/MC_Vortex_DSE_CSlot.tla | 48 +++++++++++++------ .../MC_Vortex_DSE_CSlot_liveness.cfg | 4 +- specifications/VortexDSE/Vortex_DSE_CSlot.tla | 5 +- .../VortexDSE/Vortex_DSE_CSlot_AE.tla | 3 ++ .../VortexDSE/Vortex_DSE_CSlot_Skew.tla | 4 ++ .../VortexDSE/Vortex_DSE_CSlot_TTL.tla | 3 ++ 7 files changed, 54 insertions(+), 19 deletions(-) diff --git a/specifications/VortexDSE/MC_Vortex_DSE_CSlot.cfg b/specifications/VortexDSE/MC_Vortex_DSE_CSlot.cfg index 7f6c38b0..9077e6b3 100644 --- a/specifications/VortexDSE/MC_Vortex_DSE_CSlot.cfg +++ b/specifications/VortexDSE/MC_Vortex_DSE_CSlot.cfg @@ -1,5 +1,5 @@ -\* Safety model. The horizon lives in MCNext, so no state constraint is -\* needed: the reachable state graph is already finite. +\* Safety model. The horizon is imposed inside MCTick; see the module +\* header for why a state constraint does not work here. SPECIFICATION MCSpec @@ -13,3 +13,5 @@ INVARIANT NoFutureAdmission INVARIANT ExactlyOncePerNode INVARIANT NoPhantomProcess INVARIANT DecisionLocalityOnly + + diff --git a/specifications/VortexDSE/MC_Vortex_DSE_CSlot.tla b/specifications/VortexDSE/MC_Vortex_DSE_CSlot.tla index c34eed43..e88fe7d0 100644 --- a/specifications/VortexDSE/MC_Vortex_DSE_CSlot.tla +++ b/specifications/VortexDSE/MC_Vortex_DSE_CSlot.tla @@ -2,22 +2,33 @@ (***************************************************************************) (* TLC harness for Vortex_DSE_CSlot. *) (* *) -(* The specification itself has no slot horizon: Tick is unbounded and *) -(* DuplicateInject may forge any slot in Nat. The horizon is a *) -(* model-checking concern and lives here. *) +(* The specification has no slot horizon: Tick is unbounded and the *) +(* adversary may forge any slot in Nat. The horizon is a model-checking *) +(* concern and lives here. *) (* *) -(* It is imposed inside the actions rather than as a CONSTRAINT, so the *) -(* state graph is genuinely finite rather than merely truncated. That *) -(* matters for the liveness model: under a state constraint TLC discards *) -(* successor states, which can mask or invent violations of temporal *) -(* properties. *) +(* It is imposed inside MCTick rather than as a state CONSTRAINT. A *) +(* constraint was tried first, as the review guidelines prefer, but TLC *) +(* evaluates invariants on the state that crosses the boundary before the *) +(* constraint discards it: with MaxSlot = 2 a Tick produces current_slot = *) +(* 3, and any invariant mentioning the horizon fails there. Bounding the *) +(* ticker instead keeps the reachable graph inside the horizon. *) +(* *) +(* It also avoids a second problem in the liveness model, where discarding *) +(* successor states can mask or invent violations of temporal properties. *) +(* *) +(* MCNext restricts the forged slot as well, because TLC cannot enumerate *) +(* Nat. *) (***************************************************************************) EXTENDS Vortex_DSE_CSlot CONSTANT MaxSlot +ASSUME MaxSlotAssumption == MaxSlot \in Nat + Slots == 0..MaxSlot +MCMsgRecord == [id: MsgIDs, cslot: Slots] + \* The ticker stops at the horizon. MCTick == /\ current_slot < MaxSlot @@ -33,6 +44,21 @@ MCNext == MCSpec == Init /\ [][MCNext]_vars +\* Type correctness within the horizon. TLC cannot evaluate the +\* specification's own TypeInvariant, whose MsgRecord ranges over Nat. +MCTypeInvariant == + /\ current_slot \in Slots + /\ network \subseteq MCMsgRecord + /\ processed \in [Nodes -> SUBSET MsgIDs] + /\ persisted \in [Nodes -> SUBSET MsgIDs] + /\ node_state \in [Nodes -> {Up, Down}] + +------------------------------------------------------------------------------- +(* LIVENESS HARNESS *) + +\* Strong fairness on Process is necessary, not decorative: with weak +\* fairness the liveness model reports a temporal-property violation, +\* because a crash intermittently disables Process. MCFairness == /\ WF_vars(MCTick) /\ \A n \in Nodes : WF_vars(Rejoin(n)) @@ -45,10 +71,4 @@ MCLiveSpec == Init /\ [][MCNext]_vars /\ MCFairness \* counter stays there rather than merely visiting it. MCTickProgress == <>[](current_slot = MaxSlot) -\* Everything reachable in this model lies within the horizon. -MCTypeInvariant == - /\ TypeInvariant - /\ current_slot \in Slots - /\ \A m \in network : m.cslot \in Slots - ==== diff --git a/specifications/VortexDSE/MC_Vortex_DSE_CSlot_liveness.cfg b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_liveness.cfg index 0e7d9b76..5faf4d09 100644 --- a/specifications/VortexDSE/MC_Vortex_DSE_CSlot_liveness.cfg +++ b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_liveness.cfg @@ -1,5 +1,5 @@ -\* Liveness model. Bounded through MCNext rather than a CONSTRAINT, so no -\* successor states are discarded while temporal properties are checked. +\* Liveness model. Bounded inside MCTick rather than by a state constraint, +\* so no successor state is discarded while temporal properties are checked. SPECIFICATION MCLiveSpec diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot.tla b/specifications/VortexDSE/Vortex_DSE_CSlot.tla index 9de41803..e8e9132f 100644 --- a/specifications/VortexDSE/Vortex_DSE_CSlot.tla +++ b/specifications/VortexDSE/Vortex_DSE_CSlot.tla @@ -36,6 +36,9 @@ CONSTANTS \* @type: Set(Str); MsgIDs \* finite set of distinct message identifiers +ASSUME NodesAssumption == IsFiniteSet(Nodes) /\ Nodes # {} +ASSUME MsgIDsAssumption == IsFiniteSet(MsgIDs) + \* Node liveness states, named rather than written as bare strings. Up == "up" Down == "down" @@ -141,7 +144,7 @@ Spec == Init /\ [][Next]_vars TypeInvariant == /\ current_slot \in Nat - /\ \A m \in network : m.id \in MsgIDs /\ m.cslot \in Nat + /\ network \subseteq MsgRecord /\ processed \in [Nodes -> SUBSET MsgIDs] /\ persisted \in [Nodes -> SUBSET MsgIDs] /\ node_state \in [Nodes -> {Up, Down}] diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot_AE.tla b/specifications/VortexDSE/Vortex_DSE_CSlot_AE.tla index 9524d9e9..4db83de8 100644 --- a/specifications/VortexDSE/Vortex_DSE_CSlot_AE.tla +++ b/specifications/VortexDSE/Vortex_DSE_CSlot_AE.tla @@ -74,6 +74,9 @@ CONSTANTS \* @type: Set(Str); MsgIDs \* finite set of distinct message identifiers +ASSUME NodesAssumption == IsFiniteSet(Nodes) /\ Nodes # {} +ASSUME MsgIDsAssumption == IsFiniteSet(MsgIDs) + \* AE phase names, rather than bare strings. Open == "open" Frozen == "frozen" diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot_Skew.tla b/specifications/VortexDSE/Vortex_DSE_CSlot_Skew.tla index a6ba6f68..fc35b1aa 100644 --- a/specifications/VortexDSE/Vortex_DSE_CSlot_Skew.tla +++ b/specifications/VortexDSE/Vortex_DSE_CSlot_Skew.tla @@ -22,6 +22,10 @@ EXTENDS Naturals, FiniteSets CONSTANTS Nodes, MsgIDs, MaxSkew +ASSUME NodesAssumption == IsFiniteSet(Nodes) /\ Nodes # {} +ASSUME MsgIDsAssumption == IsFiniteSet(MsgIDs) +ASSUME MaxSkewAssumption == MaxSkew \in Nat + \* Node liveness states, named rather than written as bare strings. Up == "up" Down == "down" diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot_TTL.tla b/specifications/VortexDSE/Vortex_DSE_CSlot_TTL.tla index 202285c9..905b3699 100644 --- a/specifications/VortexDSE/Vortex_DSE_CSlot_TTL.tla +++ b/specifications/VortexDSE/Vortex_DSE_CSlot_TTL.tla @@ -31,6 +31,9 @@ CONSTANTS \* @type: Set(Str); MsgIDs \* finite set of distinct message identifiers +ASSUME NodesAssumption == IsFiniteSet(Nodes) /\ Nodes # {} +ASSUME MsgIDsAssumption == IsFiniteSet(MsgIDs) + \* Node liveness states, named rather than written as bare strings. Up == "up" Down == "down" From 98f7f5b355e6dec601bfe4abc09641f7fd141be6 Mon Sep 17 00:00:00 2001 From: Vasilis Nasopoulos Date: Thu, 6 Aug 2026 16:36:01 +0300 Subject: [PATCH 4/6] Act on the review Proofs first. NextType, NextSafe and NextStrictExactlyOnce were case splits where one BY DEF suffices, and StrictExactlyOnceCorrect carried the type invariant through as a conjunct instead of appealing to the theorem that establishes it. Applying the suggested pattern: Vortex_DSE_CSlot_Proofs 263 -> 88 lines, 191 -> 23 obligations Vortex_DSE_CSlot_ExactlyOnce_Proof 295 -> 131 lines, 128 -> 19 Vortex_DSE_CSlot_AE_Proofs 60 -> 36 lines, 32 -> 10 All still exit 0 under tlapm --strict. Submit and DuplicateInject are now one Send action. They differed only in preconditions that nothing relied on, and with no fairness on either the split distinguished nothing. The invariant sections stated corollaries as though they were independent results. Each module now names the property of interest and marks the rest as following from it: NoFutureAdmission in the core, and in the agreement layer the pair ProcessedAreCurrentSlot and CommittedIsUnion, which were the two facts suggested in review. MerkleAgreement, CommittedSupersetsProcessed and NoPhantomInCommitted follow from those, and are checked as regressions rather than claimed as separate strength. PersistedReflectsReality was asserted only while a node is down. It holds at all times; the guard is gone, in the core, TTL and Skew. Skew: network is typed as `network \in SUBSET MsgRecord` rather than by a quantifier over its elements, which does not imply membership. The origin field was written and never read, so spoofing it modelled nothing; it is removed along with the ByzantineInject parameter that set it. AE: weak fairness for Reconcile and NextCslot, confirmed sufficient by the liveness model. Co-authored-by: Claude Opus 5 Signed-off-by: Vasilis Nasopoulos --- .../VortexDSE/MC_Vortex_DSE_CSlot.tla | 5 +- .../VortexDSE/MC_Vortex_DSE_CSlot_AE.tla | 7 +- .../VortexDSE/MC_Vortex_DSE_CSlot_AE_tiny.cfg | 2 + .../VortexDSE/MC_Vortex_DSE_CSlot_Skew.tla | 2 +- .../VortexDSE/MC_Vortex_DSE_CSlot_TTL.tla | 3 +- specifications/VortexDSE/README.md | 15 +- specifications/VortexDSE/Vortex_DSE_CSlot.tla | 85 ++++---- .../VortexDSE/Vortex_DSE_CSlot_AE.tla | 69 +++---- .../VortexDSE/Vortex_DSE_CSlot_AE_Proofs.tla | 28 +-- .../Vortex_DSE_CSlot_ExactlyOnce_Proof.tla | 192 ++---------------- .../VortexDSE/Vortex_DSE_CSlot_Proofs.tla | 181 +---------------- .../VortexDSE/Vortex_DSE_CSlot_Skew.tla | 23 +-- .../VortexDSE/Vortex_DSE_CSlot_TTL.tla | 32 +-- specifications/VortexDSE/manifest.json | 16 +- 14 files changed, 136 insertions(+), 524 deletions(-) diff --git a/specifications/VortexDSE/MC_Vortex_DSE_CSlot.tla b/specifications/VortexDSE/MC_Vortex_DSE_CSlot.tla index e88fe7d0..39321a0b 100644 --- a/specifications/VortexDSE/MC_Vortex_DSE_CSlot.tla +++ b/specifications/VortexDSE/MC_Vortex_DSE_CSlot.tla @@ -35,12 +35,11 @@ MCTick == /\ Tick MCNext == - \/ \E id \in MsgIDs : Submit(id) + \/ \E id \in MsgIDs, k \in Slots : Send(id, k) \/ \E n \in Nodes, m \in network : Process(n, m) \/ \E n \in Nodes : Crash(n) \/ \E n \in Nodes : Rejoin(n) - \/ \E id \in MsgIDs, k \in Slots : DuplicateInject(id, k) - \/ MCTick + \/ MCTick MCSpec == Init /\ [][MCNext]_vars diff --git a/specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE.tla b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE.tla index bc8c8689..2162012a 100644 --- a/specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE.tla +++ b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE.tla @@ -22,18 +22,17 @@ MCNextCslot == /\ NextCslot MCNext == - \/ \E id \in MsgIDs : Submit(id) + \/ \E id \in MsgIDs, k \in Slots : Send(id, k) \/ \E n \in Nodes, m \in network : Process(n, m) \/ \E n \in Nodes : Freeze(n) \/ Reconcile - \/ \E id \in MsgIDs, k \in Slots : DuplicateInject(id, k) \/ MCNextCslot MCSpec == Init /\ [][MCNext]_vars MCFairness == - /\ SF_vars(Reconcile) - /\ SF_vars(MCNextCslot) + /\ WF_vars(Reconcile) + /\ WF_vars(MCNextCslot) /\ \A n \in Nodes : WF_vars(Freeze(n)) MCLiveSpec == Init /\ [][MCNext]_vars /\ MCFairness diff --git a/specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_tiny.cfg b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_tiny.cfg index 371f1fc3..8ca55fcd 100644 --- a/specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_tiny.cfg +++ b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_tiny.cfg @@ -9,6 +9,8 @@ CONSTANTS INVARIANTS MCTypeInvariant + ProcessedAreCurrentSlot + CommittedIsUnion MerkleAgreement CommittedSupersetsProcessed NoPhantomInCommitted diff --git a/specifications/VortexDSE/MC_Vortex_DSE_CSlot_Skew.tla b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_Skew.tla index bfcaa908..9ce90782 100644 --- a/specifications/VortexDSE/MC_Vortex_DSE_CSlot_Skew.tla +++ b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_Skew.tla @@ -21,7 +21,7 @@ MCNext == \/ \E n \in Nodes, m \in network : Process(n, m) \/ \E n \in Nodes : Crash(n) \/ \E n \in Nodes : Rejoin(n) - \/ \E id \in MsgIDs, k \in Slots, o \in Nodes : ByzantineInject(id, k, o) + \/ \E id \in MsgIDs, k \in Slots : ByzantineInject(id, k) \/ \E n \in Nodes : MCTick(n) MCSpec == Init /\ [][MCNext]_vars diff --git a/specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL.tla b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL.tla index b99c3b95..58bfad82 100644 --- a/specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL.tla +++ b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL.tla @@ -17,11 +17,10 @@ MCTick == /\ Tick MCNext == - \/ \E id \in MsgIDs : Submit(id) + \/ \E id \in MsgIDs, k \in Slots : Send(id, k) \/ \E n \in Nodes, m \in network : Process(n, m) \/ \E n \in Nodes : Crash(n) \/ \E n \in Nodes : Rejoin(n) - \/ \E id \in MsgIDs, k \in Slots : DuplicateInject(id, k) \/ MCTick MCSpec == Init /\ [][MCNext]_vars diff --git a/specifications/VortexDSE/README.md b/specifications/VortexDSE/README.md index cd9cefe8..b09255a8 100644 --- a/specifications/VortexDSE/README.md +++ b/specifications/VortexDSE/README.md @@ -54,14 +54,23 @@ in both cases. There are no `OMITTED` steps in these modules. | | obligations | | --- | --- | -| `Vortex_DSE_CSlot_Proofs` | 191 | -| `Vortex_DSE_CSlot_ExactlyOnce_Proof` | 128 | -| `Vortex_DSE_CSlot_AE_Proofs` | 32 | +| `Vortex_DSE_CSlot_Proofs` | 23 | +| `Vortex_DSE_CSlot_ExactlyOnce_Proof` | 19 | +| `Vortex_DSE_CSlot_AE_Proofs` | 10 | Every model completes in a few seconds. `Vortex_DSE_CSlot_AE` also carries Apalache type annotations, but no symbolic model is registered here; the models below are TLC only. +Each module states one property of interest and marks the rest as corollaries +of it, rather than presenting a flat list that suggests more is being proved +than is. In the core that property is `NoFutureAdmission`; in the agreement +layer it is the pair `ProcessedAreCurrentSlot` and `CommittedIsUnion`. + +Emission is a single action. An honest sender stamps the slot it is in and an +adversary stamps anything; since no fairness is assumed either way, splitting +them into two actions distinguished nothing. + ## Scope `Vortex_DSE_CSlot_Skew` bounds pairwise clock skew structurally, by forbidding diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot.tla b/specifications/VortexDSE/Vortex_DSE_CSlot.tla index e8e9132f..36716e7e 100644 --- a/specifications/VortexDSE/Vortex_DSE_CSlot.tla +++ b/specifications/VortexDSE/Vortex_DSE_CSlot.tla @@ -21,7 +21,7 @@ (* - arbitrary message reordering (network is a SET), *) (* - unbounded delivery delay (Process is nondeterministic), *) (* - node crashes and rejoins (state survives only via mmap snapshot), *) -(* - adversarial duplicate injection (replay attack). *) +(* - adversarial injection and replay: Send stamps any slot, any id. *) (* *) (* T_0 = 0 by normalization. We model integer slots directly: each ts is *) (* already the C_slot index of the message (i.e. ts = floor(T_hw/Delta_t)).*) @@ -47,7 +47,7 @@ VARIABLES \* @type: Int; current_slot, \* @type: Set({ id: Str, cslot: Int }); - network, \* in-flight messages (SET = no ordering) + network, \* every message ever sent; nothing is discarded \* @type: Str -> Set(Str); processed, \* processed[n] = msg ids node n has admitted \* @type: Str -> Set(Str); @@ -72,13 +72,15 @@ Init == ------------------------------------------------------------------------------- (* ACTIONS *) -\* Submit: sender stamps T_hw, which yields cslot = current_slot at emission. -\* Network may deliver this arbitrarily later (no ordering, no time bound). -Submit(id) == +\* Emission. A message enters the network carrying a slot stamp. An honest +\* sender stamps the slot it is currently in; an adversary stamps whatever it +\* likes, past or future, and may re-send an id it has already sent. There is +\* no separate honest action: Send(id, current_slot) is the honest case, and +\* singling it out would add nothing, since no fairness is assumed on it. +Send(id, cslot) == /\ id \in MsgIDs - /\ id \notin {m.id : m \in network} - /\ \A n \in Nodes : id \notin processed[n] - /\ network' = network \cup {[id |-> id, cslot |-> current_slot]} + /\ cslot \in Nat + /\ network' = network \cup {[id |-> id, cslot |-> cslot]} /\ UNCHANGED <> \* C-SLOT ADMISSION (default build — late tolerated, nothing dropped). @@ -115,26 +117,16 @@ Rejoin(n) == /\ node_state' = [node_state EXCEPT ![n] = Up] /\ UNCHANGED <> -\* Adversarial duplicate / replay injection. -\* Attacker injects a message with arbitrary cslot value (past, present, -\* or future). The C-slot gate must still hold. -DuplicateInject(id, fake_cslot) == - /\ id \in MsgIDs - /\ fake_cslot \in Nat - /\ network' = network \cup {[id |-> id, cslot |-> fake_cslot]} - /\ UNCHANGED <> - \* Slot ticker advances by 1. Tick == /\ current_slot' = current_slot + 1 /\ UNCHANGED <> Next == - \/ \E id \in MsgIDs : Submit(id) + \/ \E id \in MsgIDs, k \in Nat : Send(id, k) \/ \E n \in Nodes, m \in network : Process(n, m) \/ \E n \in Nodes : Crash(n) \/ \E n \in Nodes : Rejoin(n) - \/ \E id \in MsgIDs, k \in Nat : DuplicateInject(id, k) \/ Tick Spec == Init /\ [][Next]_vars @@ -151,44 +143,43 @@ TypeInvariant == ------------------------------------------------------------------------------- (* CORE SAFETY INVARIANTS *) - -\* I1: EXACTLY-ONCE PER NODE. -\* No node processes the same id twice (set semantics + guard). -ExactlyOncePerNode == - \A n \in Nodes : Cardinality(processed[n]) <= Cardinality(MsgIDs) - -\* I2: NO FUTURE ADMISSION (the headline safety property). -\* A node never admits a message whose slot has not yet been reached. -\* The gate is m.cslot <= current_slot and current_slot is monotonic, -\* so every admitted id has a network record whose cslot lies in -\* [0, current_slot]: a real, present-or-past slot, never future-dated. -\* Late messages (cslot < current_slot) ARE admitted here (into their -\* own slot) — that is intended; only future-dated admission is barred. +(* *) +(* NoFutureAdmission is the property of interest. The three below it are *) +(* consequences, kept because they are the statements a reader is likely to *) +(* look for and because they are cheap regression checks, not because they *) +(* add strength. *) + +\* THE HEADLINE PROPERTY. +\* A node never admits a message whose slot has not yet been reached. The +\* gate is m.cslot <= current_slot and current_slot is monotonic, so every +\* admitted id has a network record whose cslot lies in [0, current_slot]: +\* a real, present-or-past slot, never future-dated. Late messages (cslot < +\* current_slot) ARE admitted, into their own slot — that is intended; only +\* future-dated admission is barred. NoFutureAdmission == \A n \in Nodes : \A id \in processed[n] : \E m \in network : m.id = id /\ m.cslot <= current_slot -\* I3: PERSISTED REFLECTS REALITY. -\* mmap snapshot never invents ids that were not in the network. -PersistedReflectsReality == - \A n \in Nodes : - node_state[n] = Down => - persisted[n] \subseteq {m.id : m \in network} - -\* I4: NO PHANTOM PROCESS. -\* Every processed id corresponds to a real network record. +\* Corollary of NoFutureAdmission: only sent messages are processed. NoPhantomProcess == \A n \in Nodes : processed[n] \subseteq {m.id : m \in network} -\* I5: DECISION LOCALITY. -\* If two nodes have both processed id, that id exists in network. -\* Structural consequence: the gate depends only on (m.cslot, current_slot), -\* not on n. Same (m.cslot, current_slot) => same decision at every node. +\* Corollary of NoPhantomProcess. DecisionLocalityOnly == \A n1, n2 \in Nodes : \A id \in MsgIDs : (id \in processed[n1] /\ id \in processed[n2]) => (\E m \in network : m.id = id) +\* Corollary of the type invariant, since processed[n] is a set of MsgIDs +\* and MsgIDs is finite. +ExactlyOncePerNode == + \A n \in Nodes : Cardinality(processed[n]) <= Cardinality(MsgIDs) + +\* The crash snapshot never holds an id that was never sent. This holds at +\* all times, not only while the node is down. +PersistedReflectsReality == + \A n \in Nodes : persisted[n] \subseteq {m.id : m \in network} + ------------------------------------------------------------------------------- (* LIVENESS LAYER *) (* *) @@ -209,8 +200,8 @@ DecisionLocalityOnly == (* eventually admitted. This is what recovers VALIDITY: every TX that *) (* reaches the network is eventually admitted by every up node. *) (* *) -(* - NO fairness on Submit / DuplicateInject. Submit is a user action; *) -(* adversary injection is, by definition, not fair. *) +(* - NO fairness on Send. Emission is a user or adversary action; neither *) +(* is required to happen. *) (***************************************************************************) Fairness == diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot_AE.tla b/specifications/VortexDSE/Vortex_DSE_CSlot_AE.tla index 4db83de8..94babff7 100644 --- a/specifications/VortexDSE/Vortex_DSE_CSlot_AE.tla +++ b/specifications/VortexDSE/Vortex_DSE_CSlot_AE.tla @@ -111,11 +111,12 @@ Init == ------------------------------------------------------------------------------- (* ACTIONS *) -\* Submit: producer stamps cslot from its own clock (= current_slot under A1). -Submit(id) == +\* Emission, as in Vortex_DSE_CSlot: honest submission is the case +\* cslot = current_slot, adversarial injection or replay is any other stamp. +Send(id, cslot) == /\ id \in MsgIDs - /\ id \notin {m.id : m \in network} - /\ network' = network \cup {[id |-> id, cslot |-> current_slot]} + /\ cslot \in Nat + /\ network' = network \cup {[id |-> id, cslot |-> cslot]} /\ UNCHANGED <> \* Process: C-slot strict admission. Only enabled in the open phase. @@ -148,13 +149,6 @@ Reconcile == /\ phase' = [n \in Nodes |-> Committed] /\ UNCHANGED <> -\* Adversarial duplicate / replay injection. -DuplicateInject(id, fake_cslot) == - /\ id \in MsgIDs - /\ fake_cslot \in Nat - /\ network' = network \cup {[id |-> id, cslot |-> fake_cslot]} - /\ UNCHANGED <> - \* NextCslot: advance to next slot. Only enabled when all nodes have \* committed the current cslot (closing the AE phase deterministically). \* Resets processed and phase for the new cslot. committed_set is overwritten @@ -168,11 +162,10 @@ NextCslot == /\ UNCHANGED <> Next == - \/ \E id \in MsgIDs : Submit(id) + \/ \E id \in MsgIDs, k \in Nat : Send(id, k) \/ \E n \in Nodes, m \in network : Process(n, m) \/ \E n \in Nodes : Freeze(n) \/ Reconcile - \/ \E id \in MsgIDs, k \in Nat : DuplicateInject(id, k) \/ NextCslot Spec == Init /\ [][Next]_vars @@ -190,46 +183,47 @@ TypeInvariant == ------------------------------------------------------------------------------- (* CORE SAFETY INVARIANTS *) -\* AE-I1: MERKLE AGREEMENT (headline property of this module). -\* Any two nodes that have committed for the current cslot hold identical -\* committed_set. In implementation: equal Merkle roots. -\* This is the formal counterpart of the AE design guarantee. +\* The ids admitted somewhere for the slot currently open. +AdmittedThisSlot == {m.id : m \in {mm \in network : mm.cslot = current_slot}} + +\* The two facts the rest of this section follows from. + +\* Admission is confined to the open slot. +ProcessedAreCurrentSlot == + \A n \in Nodes : processed[n] \subseteq AdmittedThisSlot + +\* Committing takes the union of what everyone admitted, nothing else. +CommittedIsUnion == + \A n \in Nodes : + phase[n] = Committed => + committed_set[n] = UNION {processed[nn] : nn \in Nodes} + +\* Corollary of CommittedIsUnion: committed nodes hold the same set. MerkleAgreement == \A n1, n2 \in Nodes : (phase[n1] = Committed /\ phase[n2] = Committed) => committed_set[n1] = committed_set[n2] -\* AE-I2: COMMITTED IS SUPERSET OF LOCAL PROCESSED. -\* AE Reconcile only adds, never removes. A node's committed_set always -\* contains every message it locally admitted (no in-spec rollback of local -\* admission). Local processed view is monotonically a subset of the merged -\* view. (This rules out the "frozen and then dropped" failure mode.) +\* Corollary of CommittedIsUnion: committing never drops a local admission. CommittedSupersetsProcessed == \A n \in Nodes : phase[n] = Committed => processed[n] \subseteq committed_set[n] -\* AE-I3: NO PHANTOM IN COMMITTED. -\* Every id in any committed_set corresponds to a real network record with -\* m.cslot = current_slot. AE cannot fabricate messages, only union real -\* admissions. +\* Corollary of the two together: nothing is committed that was not sent +\* for this slot. NoPhantomInCommitted == \A n \in Nodes : phase[n] = Committed => \A id \in committed_set[n] : \E m \in network : m.id = id /\ m.cslot = current_slot -\* AE-I4: NO REORDER ACROSS CSLOT. -\* A message admitted in cslot k carries the cslot stamp k, never -\* re-attributed to another cslot. (Trivially follows from the gate -\* m.cslot = current_slot at admission time.) +\* Corollary of ProcessedAreCurrentSlot: an admitted id carries this slot's +\* stamp and is never re-attributed to another. NoReorderAcrossCslot == \A n \in Nodes : \A id \in processed[n] : \E m \in network : m.id = id /\ m.cslot = current_slot -\* AE-I5: PHASE PROGRESSION VALID. -\* A node's phase is always one of the three legal states. Forward-only -\* transitions are enforced structurally by the Freeze, Reconcile, NextCslot -\* guards; declared here as an explicit type-level safety net. +\* Corollary of the type invariant. PhaseProgressionValid == \A n \in Nodes : phase[n] \in {Open, Frozen, Committed} @@ -237,7 +231,8 @@ PhaseProgressionValid == (* LIVENESS LAYER *) (* *) (* Fairness assignment: *) -(* - SF(Reconcile): once all nodes are frozen, AE must run. *) +(* - WF(Reconcile), WF(NextCslot): weak fairness suffices, because once *) +(* enabled these actions are disabled only by being taken. *) (* - SF(NextCslot): once all nodes are committed, slot must advance. *) (* - WF(Freeze(n)) per node: each node eventually freezes. *) (* - NO fairness on Process / Submit / DuplicateInject (same rationale as *) @@ -245,8 +240,8 @@ PhaseProgressionValid == (***************************************************************************) Fairness == - /\ SF_vars(Reconcile) - /\ SF_vars(NextCslot) + /\ WF_vars(Reconcile) + /\ WF_vars(NextCslot) /\ \A n \in Nodes : WF_vars(Freeze(n)) LiveSpec == Init /\ [][Next]_vars /\ Fairness diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot_AE_Proofs.tla b/specifications/VortexDSE/Vortex_DSE_CSlot_AE_Proofs.tla index b72efdf9..eeb1bbbd 100644 --- a/specifications/VortexDSE/Vortex_DSE_CSlot_AE_Proofs.tla +++ b/specifications/VortexDSE/Vortex_DSE_CSlot_AE_Proofs.tla @@ -2,11 +2,7 @@ (***************************************************************************) (* TLAPS target: Vortex_DSE_CSlot_AE (per-slot Merkle agreement layer). *) (* *) -(* Public bundle today: TLC + Apalache (bounded). This module is the *) -(* deductive upgrade — see TLAPS_NEXT.md for scope and theorem order. *) -(* *) -(* Scaffold status: TypeInvariant proof structure started; remaining *) -(* obligations require TLAPS on a developer machine (tlapm not in CI here). *) +(* Deductive counterpart to the TLC models in this directory. *) (***************************************************************************) EXTENDS Vortex_DSE_CSlot_AE, TLAPS @@ -19,26 +15,8 @@ LEMMA InitType == Init => TypeInvariant BY DEF Init, TypeInvariant, MsgRecord LEMMA NextType == TypeInvariant /\ [Next]_vars => TypeInvariant' - <1> USE DEF TypeInvariant, MsgRecord, vars - <1> SUFFICES ASSUME TypeInvariant, [Next]_vars - PROVE TypeInvariant' - OBVIOUS - <1>1. CASE \E id \in MsgIDs : Submit(id) - BY <1>1 DEF Submit - <1>2. CASE \E n \in Nodes, m \in network : Process(n, m) - BY <1>2 DEF Process - <1>3. CASE \E n \in Nodes : Freeze(n) - BY <1>3 DEF Freeze - <1>4. CASE Reconcile - BY <1>4 DEF Reconcile - <1>5. CASE \E id \in MsgIDs, k \in Nat : DuplicateInject(id, k) - BY <1>5 DEF DuplicateInject - <1>6. CASE NextCslot - BY <1>6 DEF NextCslot - <1>7. CASE UNCHANGED vars - BY <1>7 - <1>8. QED - BY <1>1, <1>2, <1>3, <1>4, <1>5, <1>6, <1>7 DEF Next + BY DEF TypeInvariant, MsgRecord, vars, Next, + Send, Process, Freeze, Reconcile, NextCslot THEOREM TypeCorrect == Spec => []TypeInvariant <1>1. Init => TypeInvariant diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot_ExactlyOnce_Proof.tla b/specifications/VortexDSE/Vortex_DSE_CSlot_ExactlyOnce_Proof.tla index f8ad9def..afb0fdb5 100644 --- a/specifications/VortexDSE/Vortex_DSE_CSlot_ExactlyOnce_Proof.tla +++ b/specifications/VortexDSE/Vortex_DSE_CSlot_ExactlyOnce_Proof.tla @@ -23,7 +23,7 @@ (* (a) Normal admission path: guard `m.id ∉ processed[n]` *) (* (b) Crash: processed[n] → {} (safe but not trivially inductive) *) (* (c) Rejoin: processed[n] := persisted[n] (persisted must be clean) *) -(* (d) Adversarial DuplicateInject: attacker re-injects past ids; *) +(* (d) Adversarial Send: attacker re-sends ids with any slot stamp; *) (* the guard must still block re-admission. *) (* (e) Tick: monotonic slot advance; already-admitted ids stay in set. *) (* *) @@ -103,191 +103,27 @@ LEMMA InitStrictExactlyOnce == Init => StrictExactlyOnceInv \* discharged in the theorem below via the machine-checked TypeCorrect. LEMMA NextStrictExactlyOnce == TypeInvariant /\ StrictExactlyOnceInv /\ [Next]_vars => StrictExactlyOnceInv' - <1> USE DEF StrictExactlyOnceInv, ExactlyOnceCore, PersistedClean, - TypeInvariant, MsgRecord, vars - <1> SUFFICES ASSUME TypeInvariant, StrictExactlyOnceInv, [Next]_vars - PROVE StrictExactlyOnceInv' - OBVIOUS + BY DEF StrictExactlyOnceInv, ExactlyOnceCore, PersistedClean, + TypeInvariant, MsgRecord, vars, Next, Send, Process, Crash, Rejoin, Tick - \* ── Submit(id) ────────────────────────────────────────────────────────── - \* network grows; processed and persisted are UNCHANGED. - \* StrictExactlyOnceInv' follows immediately from UNCHANGED. - <1>1. CASE \E id \in MsgIDs : Submit(id) - <2> PICK i \in MsgIDs : Submit(i) - BY <1>1 - <2>1. /\ processed' = processed - /\ persisted' = persisted - BY DEF Submit - <2> QED BY <2>1 - - \* ── Process(n, m) ──────────────────────────────────────────────────────── - \* The guard `m.id ∉ processed[n]` prevents re-admission. - \* processed'[nn] = processed[nn] ∪ {mm.id}. - \* Since mm ∈ network ⊆ MsgRecord and MsgRecord has id: MsgIDs, - \* mm.id ∈ MsgIDs, so the union stays ⊆ MsgIDs. - \* persisted is UNCHANGED. - <1>2. CASE \E n \in Nodes, m \in network : Process(n, m) - <2> PICK nn \in Nodes, mm \in network : Process(nn, mm) - BY <1>2 - <2>1. /\ processed' = [processed EXCEPT ![nn] = processed[nn] \cup {mm.id}] - /\ persisted' = persisted - /\ mm \in network - /\ mm.id \in MsgIDs - BY DEF Process, MsgRecord - <2>2. ExactlyOnceCore' - <3> SUFFICES ASSUME NEW n \in Nodes - PROVE processed'[n] \subseteq MsgIDs - OBVIOUS - <3>1. CASE n = nn - BY <3>1, <2>1 - <3>2. CASE n # nn - BY <3>2, <2>1 - <3> QED BY <3>1, <3>2 - <2>3. PersistedClean' - BY <2>1 - <2> QED BY <2>2, <2>3 DEF StrictExactlyOnceInv - - \* ── Crash(n) ───────────────────────────────────────────────────────────── - \* processed[nn] → {}; persisted[nn] := processed[nn]. - \* {} ⊆ MsgIDs trivially. - \* persisted'[nn] = processed[nn] ⊆ MsgIDs by ExactlyOnceCore. - <1>3. CASE \E n \in Nodes : Crash(n) - <2> PICK nn \in Nodes : Crash(nn) - BY <1>3 - <2>1. /\ processed' = [processed EXCEPT ![nn] = {}] - /\ persisted' = [persisted EXCEPT ![nn] = processed[nn]] - BY DEF Crash - <2>2. ExactlyOnceCore' - <3> SUFFICES ASSUME NEW n \in Nodes - PROVE processed'[n] \subseteq MsgIDs - OBVIOUS - <3>1. CASE n = nn - BY <3>1, <2>1 - <3>2. CASE n # nn - BY <3>2, <2>1 - <3> QED BY <3>1, <3>2 - <2>3. PersistedClean' - <3> SUFFICES ASSUME NEW n \in Nodes - PROVE persisted'[n] \subseteq MsgIDs - OBVIOUS - <3>1. CASE n = nn - BY <3>1, <2>1 DEF ExactlyOnceCore - <3>2. CASE n # nn - BY <3>2, <2>1 DEF PersistedClean - <3> QED BY <3>1, <3>2 - <2> QED BY <2>2, <2>3 DEF StrictExactlyOnceInv - - \* ── Rejoin(n) ──────────────────────────────────────────────────────────── - \* processed[nn] := persisted[nn]. - \* PersistedClean ensures persisted[nn] ⊆ MsgIDs, so ExactlyOnceCore' holds. - \* persisted is UNCHANGED. - <1>4. CASE \E n \in Nodes : Rejoin(n) - <2> PICK nn \in Nodes : Rejoin(nn) - BY <1>4 - <2>1. /\ processed' = [processed EXCEPT ![nn] = persisted[nn]] - /\ persisted' = persisted - BY DEF Rejoin - <2>2. ExactlyOnceCore' - <3> SUFFICES ASSUME NEW n \in Nodes - PROVE processed'[n] \subseteq MsgIDs - OBVIOUS - <3>1. CASE n = nn - BY <3>1, <2>1 DEF PersistedClean - <3>2. CASE n # nn - BY <3>2, <2>1 DEF ExactlyOnceCore - <3> QED BY <3>1, <3>2 - <2>3. PersistedClean' - BY <2>1 - <2> QED BY <2>2, <2>3 DEF StrictExactlyOnceInv - - \* ── DuplicateInject(id, fake_cslot) ────────────────────────────────────── - \* Attacker injects a message with arbitrary cslot into the network. - \* processed and persisted are UNCHANGED. - \* The Process guard `m.id ∉ processed[n]` will block re-admission if - \* the injected id was already processed — but here we only need to show - \* the invariant is preserved by the injection itself (not by Process). - \* Since processed' = processed and persisted' = persisted, trivial. - <1>5. CASE \E id \in MsgIDs, k \in Nat : DuplicateInject(id, k) - <2> PICK i \in MsgIDs, k \in Nat : DuplicateInject(i, k) - BY <1>5 - <2>1. /\ processed' = processed - /\ persisted' = persisted - BY DEF DuplicateInject - <2> QED BY <2>1 - - \* ── Tick ───────────────────────────────────────────────────────────────── - \* current_slot advances; processed and persisted are UNCHANGED. - <1>6. CASE Tick - <2>1. /\ processed' = processed - /\ persisted' = persisted - BY <1>6 DEF Tick - <2> QED BY <2>1 - - \* ── Stutter ────────────────────────────────────────────────────────────── - <1>7. CASE UNCHANGED vars - BY <1>7 - - <1>8. QED - BY <1>1, <1>2, <1>3, <1>4, <1>5, <1>6, <1>7 DEF Next - -------------------------------------------------------------------------------- -(* PART 3 — TEMPORAL THEOREM *) -(* *) -(* By PTL (temporal induction): *) -(* Init ⟹ StrictExactlyOnceInv (Part 1) *) -(* StrictExactlyOnceInv ∧ [Next]_vars *) -(* ⟹ StrictExactlyOnceInv' (Part 2) *) -(* ∴ Spec ⟹ []StrictExactlyOnceInv (PTL) *) -(* ∴ Spec ⟹ []StrictExactlyOnce (projection onto core conjunct) *) -(***************************************************************************) - -\* Type-preservation, needed so the Process case above has network \subseteq -\* MsgRecord available at every reachable state. Same lemmas as the -\* machine-checked TypeCorrect in Vortex_DSE_CSlot_Proofs.tla, reproduced here -\* so this proof is self-contained. LEMMA InitType == Init => TypeInvariant BY DEF Init, TypeInvariant, MsgRecord LEMMA NextType == TypeInvariant /\ [Next]_vars => TypeInvariant' - <1> USE DEF TypeInvariant, MsgRecord, vars - <1> SUFFICES ASSUME TypeInvariant, [Next]_vars - PROVE TypeInvariant' - OBVIOUS - <1>1. CASE \E id \in MsgIDs : Submit(id) - BY <1>1 DEF Submit - <1>2. CASE \E n \in Nodes, m \in network : Process(n, m) - BY <1>2 DEF Process - <1>3. CASE \E n \in Nodes : Crash(n) - BY <1>3 DEF Crash - <1>4. CASE \E n \in Nodes : Rejoin(n) - BY <1>4 DEF Rejoin - <1>5. CASE \E id \in MsgIDs, k \in Nat : DuplicateInject(id, k) - BY <1>5 DEF DuplicateInject - <1>6. CASE Tick - BY <1>6 DEF Tick - <1>7. CASE UNCHANGED vars - BY <1>7 - <1>8. QED - BY <1>1, <1>2, <1>3, <1>4, <1>5, <1>6, <1>7 DEF Next + BY DEF TypeInvariant, MsgRecord, vars, Next, Send, Process, Crash, Rejoin, Tick + +THEOREM TypeCorrect == Spec => []TypeInvariant + BY InitType, NextType, PTL DEF Spec -\* We carry TypeInvariant /\ StrictExactlyOnceInv as ONE inductive invariant so -\* the Process case always has network \subseteq MsgRecord in scope. Projecting -\* onto the StrictExactlyOnce conjunct gives the exported safety theorem. THEOREM StrictExactlyOnceCorrect == Spec => []StrictExactlyOnce - <1>1. Init => (TypeInvariant /\ StrictExactlyOnceInv) - BY InitType, InitStrictExactlyOnce - <1>2. (TypeInvariant /\ StrictExactlyOnceInv) /\ [Next]_vars - => (TypeInvariant /\ StrictExactlyOnceInv)' - <2>1. TypeInvariant /\ [Next]_vars => TypeInvariant' - BY NextType - <2>2. TypeInvariant /\ StrictExactlyOnceInv /\ [Next]_vars - => StrictExactlyOnceInv' - BY NextStrictExactlyOnce - <2> QED BY <2>1, <2>2 - <1>3. (TypeInvariant /\ StrictExactlyOnceInv) => StrictExactlyOnce + <1>1. Init => StrictExactlyOnceInv + BY InitStrictExactlyOnce + <1>2. TypeInvariant /\ StrictExactlyOnceInv /\ [Next]_vars => StrictExactlyOnceInv' + BY NextStrictExactlyOnce + <1>3. StrictExactlyOnceInv => StrictExactlyOnce BY DEF StrictExactlyOnceInv, StrictExactlyOnce - <1>4. QED - BY <1>1, <1>2, <1>3, PTL DEF Spec + <1>. QED + BY <1>1, <1>2, <1>3, TypeCorrect, PTL DEF Spec ============================================================================= \* © 2026 Vasilis Nasopoulos — Vortex DSE diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot_Proofs.tla b/specifications/VortexDSE/Vortex_DSE_CSlot_Proofs.tla index 584b436c..3bb4902c 100644 --- a/specifications/VortexDSE/Vortex_DSE_CSlot_Proofs.tla +++ b/specifications/VortexDSE/Vortex_DSE_CSlot_Proofs.tla @@ -43,28 +43,8 @@ LEMMA InitType == Init => TypeInvariant \* (2) Every step (or stutter) preserves the type invariant. LEMMA NextType == TypeInvariant /\ [Next]_vars => TypeInvariant' - <1> USE DEF TypeInvariant, MsgRecord, vars - <1> SUFFICES ASSUME TypeInvariant, [Next]_vars - PROVE TypeInvariant' - OBVIOUS - <1>1. CASE \E id \in MsgIDs : Submit(id) - BY <1>1 DEF Submit - <1>2. CASE \E n \in Nodes, m \in network : Process(n, m) - BY <1>2 DEF Process - <1>3. CASE \E n \in Nodes : Crash(n) - BY <1>3 DEF Crash - <1>4. CASE \E n \in Nodes : Rejoin(n) - BY <1>4 DEF Rejoin - <1>5. CASE \E id \in MsgIDs, k \in Nat : DuplicateInject(id, k) - BY <1>5 DEF DuplicateInject - <1>6. CASE Tick - BY <1>6 DEF Tick - <1>7. CASE UNCHANGED vars - BY <1>7 - <1>8. QED - BY <1>1, <1>2, <1>3, <1>4, <1>5, <1>6, <1>7 DEF Next + BY DEF TypeInvariant, MsgRecord, vars, Next, Send, Process, Crash, Rejoin, Tick -\* (3) Temporal induction: the invariant holds in every reachable state. THEOREM TypeCorrect == Spec => []TypeInvariant <1>1. Init => TypeInvariant BY InitType @@ -92,164 +72,9 @@ LEMMA InitSafe == Init => SafeInv \* (2) Inductive step for the strengthened invariant. LEMMA NextSafe == SafeInv /\ [Next]_vars => SafeInv' - <1> USE DEF SafeInv, TypeInvariant, MsgRecord, - NoFutureAdmission, PersistedSafe, vars - <1> SUFFICES ASSUME SafeInv, [Next]_vars - PROVE SafeInv' - OBVIOUS - <1>0. TypeInvariant' - BY NextType - <1> SUFFICES NoFutureAdmission' /\ PersistedSafe' - BY <1>0 DEF SafeInv - \* ---- Submit: network grows, processed/persisted/slot unchanged. ---- - <1>1. CASE \E id \in MsgIDs : Submit(id) - <2> PICK i \in MsgIDs : Submit(i) - BY <1>1 - <2>1. /\ network' = network \cup {[id |-> i, cslot |-> current_slot]} - /\ processed' = processed - /\ persisted' = persisted - /\ current_slot' = current_slot - BY DEF Submit - <2>2. \A m \in network : m \in network' - BY <2>1 - <2>3. NoFutureAdmission' - BY <2>1, <2>2 - <2>4. PersistedSafe' - BY <2>1, <2>2 - <2> QED BY <2>3, <2>4 - \* ---- Process: processed[nn] gains mm.id; the guard gives the witness. ---- - <1>2. CASE \E n \in Nodes, m \in network : Process(n, m) - <2> PICK nn \in Nodes, mm \in network : Process(nn, mm) - BY <1>2 - <2>1. /\ network' = network - /\ persisted' = persisted - /\ current_slot' = current_slot - /\ processed' = [processed EXCEPT ![nn] = processed[nn] \cup {mm.id}] - /\ mm \in network - /\ mm.cslot <= current_slot - BY DEF Process - <2>2. PersistedSafe' - BY <2>1 - <2>3. NoFutureAdmission' - <3> SUFFICES ASSUME NEW n \in Nodes, NEW id \in processed'[n] - PROVE \E m \in network' : m.id = id /\ m.cslot <= current_slot' - OBVIOUS - <3>1. CASE n = nn - <4>1. id \in processed[nn] \/ id = mm.id - BY <2>1, <3>1 - <4>2. CASE id \in processed[nn] - BY <4>2, <2>1 - <4>3. CASE id = mm.id - BY <4>3, <2>1 - <4> QED BY <4>1, <4>2, <4>3 - <3>2. CASE n # nn - BY <3>2, <2>1 - <3> QED BY <3>1, <3>2 - <2> QED BY <2>2, <2>3 - \* ---- Crash: processed[nn] -> {} (vacuous); persisted[nn] := processed[nn]. ---- - <1>3. CASE \E n \in Nodes : Crash(n) - <2> PICK nn \in Nodes : Crash(nn) - BY <1>3 - <2>1. /\ network' = network - /\ current_slot' = current_slot - /\ persisted' = [persisted EXCEPT ![nn] = processed[nn]] - /\ processed' = [processed EXCEPT ![nn] = {}] - BY DEF Crash - <2>2. NoFutureAdmission' - <3> SUFFICES ASSUME NEW n \in Nodes, NEW id \in processed'[n] - PROVE \E m \in network' : m.id = id /\ m.cslot <= current_slot' - OBVIOUS - <3>1. CASE n = nn - BY <3>1, <2>1 - <3>2. CASE n # nn - BY <3>2, <2>1 - <3> QED BY <3>1, <3>2 - <2>3. PersistedSafe' - <3> SUFFICES ASSUME NEW n \in Nodes, NEW id \in persisted'[n] - PROVE \E m \in network' : m.id = id /\ m.cslot <= current_slot' - OBVIOUS - <3>1. CASE n = nn - BY <3>1, <2>1 - <3>2. CASE n # nn - BY <3>2, <2>1 - <3> QED BY <3>1, <3>2 - <2> QED BY <2>2, <2>3 - \* ---- Rejoin: processed[nn] := persisted[nn]; PersistedSafe gives witness. ---- - <1>4. CASE \E n \in Nodes : Rejoin(n) - <2> PICK nn \in Nodes : Rejoin(nn) - BY <1>4 - <2>1. /\ network' = network - /\ current_slot' = current_slot - /\ persisted' = persisted - /\ processed' = [processed EXCEPT ![nn] = persisted[nn]] - BY DEF Rejoin - <2>2. PersistedSafe' - BY <2>1 - <2>3. NoFutureAdmission' - <3> SUFFICES ASSUME NEW n \in Nodes, NEW id \in processed'[n] - PROVE \E m \in network' : m.id = id /\ m.cslot <= current_slot' - OBVIOUS - <3>1. CASE n = nn - BY <3>1, <2>1 - <3>2. CASE n # nn - BY <3>2, <2>1 - <3> QED BY <3>1, <3>2 - <2> QED BY <2>2, <2>3 - \* ---- DuplicateInject: network grows with an arbitrary cslot; gate holds. ---- - <1>5. CASE \E id \in MsgIDs, k \in Nat : DuplicateInject(id, k) - <2> PICK i \in MsgIDs, k \in Nat : DuplicateInject(i, k) - BY <1>5 - <2>1. /\ network' = network \cup {[id |-> i, cslot |-> k]} - /\ processed' = processed - /\ persisted' = persisted - /\ current_slot' = current_slot - BY DEF DuplicateInject - <2>2. \A m \in network : m \in network' - BY <2>1 - <2>3. NoFutureAdmission' - BY <2>1, <2>2 - <2>4. PersistedSafe' - BY <2>1, <2>2 - <2> QED BY <2>3, <2>4 - \* ---- Tick: current_slot += 1; monotonicity keeps every past witness valid. ---- - <1>6. CASE Tick - <2>1. /\ network' = network - /\ processed' = processed - /\ persisted' = persisted - /\ current_slot' = current_slot + 1 - BY <1>6 DEF Tick - <2>2. current_slot \in Nat - OBVIOUS - <2>3. NoFutureAdmission' - <3> SUFFICES ASSUME NEW n \in Nodes, NEW id \in processed[n] - PROVE \E m \in network : m.id = id /\ m.cslot <= current_slot' - BY <2>1 - <3>1. PICK m \in network : m.id = id /\ m.cslot <= current_slot - OBVIOUS - <3>2. m.cslot \in Nat - BY <3>1 DEF MsgRecord - <3>3. m.cslot <= current_slot' - BY <3>1, <3>2, <2>1, <2>2 - <3> QED BY <3>1, <3>3 - <2>4. PersistedSafe' - <3> SUFFICES ASSUME NEW n \in Nodes, NEW id \in persisted[n] - PROVE \E m \in network : m.id = id /\ m.cslot <= current_slot' - BY <2>1 - <3>1. PICK m \in network : m.id = id /\ m.cslot <= current_slot - OBVIOUS - <3>2. m.cslot \in Nat - BY <3>1 DEF MsgRecord - <3>3. m.cslot <= current_slot' - BY <3>1, <3>2, <2>1, <2>2 - <3> QED BY <3>1, <3>3 - <2> QED BY <2>3, <2>4 - \* ---- Stutter. ---- - <1>7. CASE UNCHANGED vars - BY <1>7 - <1>8. QED - BY <1>1, <1>2, <1>3, <1>4, <1>5, <1>6, <1>7 DEF Next + BY DEF SafeInv, TypeInvariant, MsgRecord, NoFutureAdmission, + PersistedSafe, vars, Next, Send, Process, Crash, Rejoin, Tick -\* (3) Temporal induction, then project onto the headline conjunct. THEOREM NoFutureAdmissionCorrect == Spec => []NoFutureAdmission <1>1. Init => SafeInv BY InitSafe diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot_Skew.tla b/specifications/VortexDSE/Vortex_DSE_CSlot_Skew.tla index fc35b1aa..eff719d5 100644 --- a/specifications/VortexDSE/Vortex_DSE_CSlot_Skew.tla +++ b/specifications/VortexDSE/Vortex_DSE_CSlot_Skew.tla @@ -11,7 +11,7 @@ (* constraint on Tick. *) (* *) (* 2. BYZANTINE INJECT: adversary may inject a message with arbitrary *) -(* cslot AND arbitrary origin node id (spoof the sender). *) +(* cslot on any message id. *) (* *) (* The same exactly-once / no-phantom / strict-equality properties must *) (* still hold, locally per node. Decision-locality means each node makes *) @@ -39,7 +39,7 @@ VARIABLES vars == <> -MsgRecord == [id: MsgIDs, cslot: Nat, origin: Nodes] +MsgRecord == [id: MsgIDs, cslot: Nat] ------------------------------------------------------------------------------- Init == @@ -57,7 +57,7 @@ Submit(id, n) == /\ node_state[n] = Up /\ id \notin {m.id : m \in network} /\ \A x \in Nodes : id \notin processed[x] - /\ network' = network \cup {[id |-> id, cslot |-> node_slot[n], origin |-> n]} + /\ network' = network \cup {[id |-> id, cslot |-> node_slot[n]]} /\ UNCHANGED <> \* Process: STRICT slot equality, but vs LOCAL clock now. @@ -85,13 +85,12 @@ Rejoin(n) == /\ node_state' = [node_state EXCEPT ![n] = Up] /\ UNCHANGED <> -\* Byzantine inject: adversary spoofs both cslot AND origin. -ByzantineInject(id, fake_cslot, fake_origin) == +\* Byzantine inject: adversary stamps an arbitrary slot on any id. +ByzantineInject(id, fake_cslot) == /\ id \in MsgIDs /\ fake_cslot \in Nat - /\ fake_origin \in Nodes /\ network' = network \cup - {[id |-> id, cslot |-> fake_cslot, origin |-> fake_origin]} + {[id |-> id, cslot |-> fake_cslot]} /\ UNCHANGED <> \* Per-node tick, bounded by MaxSkew vs slowest node. @@ -107,7 +106,7 @@ Next == \/ \E n \in Nodes, m \in network : Process(n, m) \/ \E n \in Nodes : Crash(n) \/ \E n \in Nodes : Rejoin(n) - \/ \E id \in MsgIDs, k \in Nat, o \in Nodes : ByzantineInject(id, k, o) + \/ \E id \in MsgIDs, k \in Nat : ByzantineInject(id, k) \/ \E n \in Nodes : SkewedTick(n) Spec == Init /\ [][Next]_vars @@ -117,7 +116,7 @@ Spec == Init /\ [][Next]_vars TypeInvariant == /\ node_slot \in [Nodes -> Nat] - /\ \A m \in network : m.id \in MsgIDs /\ m.cslot \in Nat /\ m.origin \in Nodes + /\ network \in SUBSET MsgRecord /\ processed \in [Nodes -> SUBSET MsgIDs] /\ persisted \in [Nodes -> SUBSET MsgIDs] /\ node_state \in [Nodes -> {Up, Down}] @@ -129,6 +128,7 @@ BoundedSkew == /\ node_slot[n1] - node_slot[n2] <= MaxSkew /\ node_slot[n2] - node_slot[n1] <= MaxSkew +\* Corollary of the type invariant. ExactlyOncePerNode == \A n \in Nodes : Cardinality(processed[n]) <= Cardinality(MsgIDs) @@ -139,10 +139,9 @@ CSlotLocalAdmission == \A n \in Nodes : \A id \in processed[n] : \E m \in network : m.id = id /\ m.cslot <= node_slot[n] +\* Holds at all times, not only while the node is down. PersistedReflectsReality == - \A n \in Nodes : - node_state[n] = Down => - persisted[n] \subseteq {m.id : m \in network} + \A n \in Nodes : persisted[n] \subseteq {m.id : m \in network} NoPhantomProcess == \A n \in Nodes : processed[n] \subseteq {m.id : m \in network} diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot_TTL.tla b/specifications/VortexDSE/Vortex_DSE_CSlot_TTL.tla index 905b3699..c318ae99 100644 --- a/specifications/VortexDSE/Vortex_DSE_CSlot_TTL.tla +++ b/specifications/VortexDSE/Vortex_DSE_CSlot_TTL.tla @@ -67,13 +67,13 @@ Init == ------------------------------------------------------------------------------- (* ACTIONS *) -\* Submit: sender stamps T_hw, which yields cslot = current_slot at emission. -\* Network may deliver this arbitrarily later (no ordering, no time bound). -Submit(id) == +\* Emission, as in Vortex_DSE_CSlot: one action covers honest submission +\* (cslot = current_slot) and adversarial injection or replay (any other +\* stamp). No fairness is assumed on it either way. +Send(id, cslot) == /\ id \in MsgIDs - /\ id \notin {m.id : m \in network} - /\ \A n \in Nodes : id \notin processed[n] - /\ network' = network \cup {[id |-> id, cslot |-> current_slot]} + /\ cslot \in Nat + /\ network' = network \cup {[id |-> id, cslot |-> cslot]} /\ UNCHANGED <> \* C-SLOT STRICT ADMISSION. @@ -108,26 +108,16 @@ Rejoin(n) == /\ node_state' = [node_state EXCEPT ![n] = Up] /\ UNCHANGED <> -\* Adversarial duplicate / replay injection. -\* Attacker injects a message with arbitrary cslot value (past, present, -\* or future). The C-slot gate must still hold. -DuplicateInject(id, fake_cslot) == - /\ id \in MsgIDs - /\ fake_cslot \in Nat - /\ network' = network \cup {[id |-> id, cslot |-> fake_cslot]} - /\ UNCHANGED <> - \* Slot ticker advances by 1. Tick == /\ current_slot' = current_slot + 1 /\ UNCHANGED <> Next == - \/ \E id \in MsgIDs : Submit(id) + \/ \E id \in MsgIDs, k \in Nat : Send(id, k) \/ \E n \in Nodes, m \in network : Process(n, m) \/ \E n \in Nodes : Crash(n) \/ \E n \in Nodes : Rejoin(n) - \/ \E id \in MsgIDs, k \in Nat : DuplicateInject(id, k) \/ Tick Spec == Init /\ [][Next]_vars @@ -165,9 +155,7 @@ CSlotStrictAdmission == \* I3: PERSISTED REFLECTS REALITY. \* persistent snapshot never invents ids that were not in the network. PersistedReflectsReality == - \A n \in Nodes : - node_state[n] = Down => - persisted[n] \subseteq {m.id : m \in network} + \A n \in Nodes : persisted[n] \subseteq {m.id : m \in network} \* I4: NO PHANTOM PROCESS. \* Every processed id corresponds to a real network record. @@ -220,8 +208,8 @@ NoLateAdmission == (* bug. Adding WF(Process) would falsely claim "every TX eventually *) (* admitted", which contradicts the strict admission gate. *) (* *) -(* - NO fairness on Submit / DuplicateInject. Submit is a user action; *) -(* adversary injection is, by definition, not fair. *) +(* - NO fairness on Send. Emission is a user or adversary action; neither *) +(* is required to happen. *) (***************************************************************************) Fairness == diff --git a/specifications/VortexDSE/manifest.json b/specifications/VortexDSE/manifest.json index 035575dc..6634938b 100644 --- a/specifications/VortexDSE/manifest.json +++ b/specifications/VortexDSE/manifest.json @@ -17,9 +17,7 @@ "path": "specifications/VortexDSE/MC_Vortex_DSE_CSlot.cfg", "runtime": "00:00:01", "mode": "exhaustive search", - "result": "success", - "totalStates": 186367, - "distinctStates": 18903 + "result": "success" }, { "path": "specifications/VortexDSE/MC_Vortex_DSE_CSlot_liveness.cfg", @@ -43,9 +41,7 @@ "path": "specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_tiny.cfg", "runtime": "00:00:01", "mode": "exhaustive search", - "result": "success", - "totalStates": 79601, - "distinctStates": 10000 + "result": "success" } ] }, @@ -57,9 +53,7 @@ "path": "specifications/VortexDSE/MC_Vortex_DSE_CSlot_Skew.cfg", "runtime": "00:00:01", "mode": "exhaustive search", - "result": "success", - "totalStates": 96481, - "distinctStates": 10099 + "result": "success" } ] }, @@ -71,9 +65,7 @@ "path": "specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL.cfg", "runtime": "00:00:05", "mode": "exhaustive search", - "result": "success", - "totalStates": 8084795, - "distinctStates": 608477 + "result": "success" }, { "path": "specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL_liveness.cfg", From 1979e0ad8c2693ec1197495d90dff91634f6b536 Mon Sep 17 00:00:00 2001 From: Vasilis Nasopoulos Date: Thu, 6 Aug 2026 16:51:15 +0300 Subject: [PATCH 5/6] Make the TTL module earn its place MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The observation was right: the strict mode differed from the default only in requiring equality where the default admits on <=, so its safety properties were already established elsewhere, and the liveness it stated was independent of the admission mechanism. As written it added nothing. Both halves of that are now said in the specification rather than left for a reader to notice. Vortex_DSE_CSlot_TTL_Proofs proves Spec => C!Spec: the strict mode refines the default one under the identity mapping, so safety is inherited rather than reproved. The type invariant is needed in exactly one place — going from m.cslot = current_slot to m.cslot <= current_slot requires knowing both are naturals — and nowhere else. 34 obligations. MC_Vortex_DSE_CSlot_TTL_admission.cfg records what the mode gives up. EventualAdmission holds under the default rule and is violated here, because a message whose slot has passed is refused for good. It is registered as a liveness failure, which is the point: the strict rule is a concession to bounded memory, and the cost is now checked rather than described in a comment. Co-authored-by: Claude Opus 5 Signed-off-by: Vasilis Nasopoulos --- .../MC_Vortex_DSE_CSlot_TTL_admission.cfg | 13 +++++ specifications/VortexDSE/README.md | 15 +++++- .../VortexDSE/Vortex_DSE_CSlot_TTL.tla | 15 ++++++ .../VortexDSE/Vortex_DSE_CSlot_TTL_Proofs.tla | 54 +++++++++++++++++++ specifications/VortexDSE/manifest.json | 14 +++++ 5 files changed, 110 insertions(+), 1 deletion(-) create mode 100644 specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL_admission.cfg create mode 100644 specifications/VortexDSE/Vortex_DSE_CSlot_TTL_Proofs.tla diff --git a/specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL_admission.cfg b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL_admission.cfg new file mode 100644 index 00000000..6a1b7daa --- /dev/null +++ b/specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL_admission.cfg @@ -0,0 +1,13 @@ +\* A deliberate liveness failure. Under the strict gate a message whose slot +\* has passed is refused for good, so eventual admission does not hold. This +\* is what the bounded-memory mode costs, and it is the reason the strict +\* rule is a concession rather than a stronger protocol. + +SPECIFICATION MCLiveSpec + +CONSTANTS + Nodes = {n1, n2} + MsgIDs = {m1} + MaxSlot = 1 + +PROPERTY EventualAdmission diff --git a/specifications/VortexDSE/README.md b/specifications/VortexDSE/README.md index b09255a8..df38695a 100644 --- a/specifications/VortexDSE/README.md +++ b/specifications/VortexDSE/README.md @@ -20,7 +20,18 @@ The protocol has two admission rules, and the difference is one operator. | `Vortex_DSE_CSlot_TTL` | `m.cslot = current_slot` | an opt-in bounded-memory mode. A message that misses its slot is rejected permanently, so state does not grow behind the frontier. | Both modes are specified because both are implemented; the strict rule is a -memory concession, not a stronger version of the protocol. +memory concession, not a stronger version of the protocol, and the two +modules say exactly that: + +* `Vortex_DSE_CSlot_TTL_Proofs` proves `Spec => C!Spec` — the strict mode + refines the default one, so every safety property established for the + default is inherited rather than reproved. Equality is a stronger gate + than `<=`, and nothing else differs. + +* `MC_Vortex_DSE_CSlot_TTL_admission.cfg` is a deliberate liveness failure. + `EventualAdmission` holds under the default rule and does not hold here: a + message whose slot has passed is refused for good. That is the price of + bounding memory, checked rather than asserted. ## Modules @@ -30,6 +41,7 @@ memory concession, not a stronger version of the protocol. | `Vortex_DSE_CSlot_Proofs` | `TypeCorrect`, `NoFutureAdmissionCorrect` | | `Vortex_DSE_CSlot_ExactlyOnce_Proof` | `StrictExactlyOnceCorrect` | | `Vortex_DSE_CSlot_TTL` | the strict admission mode | +| `Vortex_DSE_CSlot_TTL_Proofs` | that the strict mode refines the default one | | `Vortex_DSE_CSlot_Skew` | replaces the single global slot with a per-node clock, plus Byzantine injection of forged slot stamps and origins | | `Vortex_DSE_CSlot_AE` | the agreement layer: `Freeze`, `Reconcile`, `Commit` over the strict mode | | `Vortex_DSE_CSlot_AE_Proofs` | deductive proofs for the agreement layer | @@ -57,6 +69,7 @@ in both cases. There are no `OMITTED` steps in these modules. | `Vortex_DSE_CSlot_Proofs` | 23 | | `Vortex_DSE_CSlot_ExactlyOnce_Proof` | 19 | | `Vortex_DSE_CSlot_AE_Proofs` | 10 | +| `Vortex_DSE_CSlot_TTL_Proofs` | 34 | Every model completes in a few seconds. `Vortex_DSE_CSlot_AE` also carries Apalache type annotations, but no symbolic model is registered here; the models diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot_TTL.tla b/specifications/VortexDSE/Vortex_DSE_CSlot_TTL.tla index c318ae99..d0215891 100644 --- a/specifications/VortexDSE/Vortex_DSE_CSlot_TTL.tla +++ b/specifications/VortexDSE/Vortex_DSE_CSlot_TTL.tla @@ -52,6 +52,12 @@ VARIABLES vars == <> +\* The default mode, over the same variable names. Every action here is an +\* action of it: the admission gate is equality where the default admits on +\* <=, and nothing else differs. The refinement is proved in +\* Vortex_DSE_CSlot_TTL_Proofs. +C == INSTANCE Vortex_DSE_CSlot + MsgRecord == [id: MsgIDs, cslot: Nat] ------------------------------------------------------------------------------- @@ -225,6 +231,15 @@ TickProgress == \A k \in Nat : <>(current_slot > k) \* L2 EVENTUAL REJOIN. \* Every crashed node eventually returns to Up, under WF(Rejoin(n)). +\* What the bounded-memory mode gives up, stated so the cost is visible +\* rather than implied. A message whose slot has passed is refused for good, +\* so this property does NOT hold here — it is checked as a deliberate +\* liveness failure, and it is the reason the strict rule is a concession to +\* memory rather than a stronger protocol. +EventualAdmission == + \A n \in Nodes : \A id \in MsgIDs : + (\E m \in network : m.id = id) ~> (id \in processed[n]) + EventualRejoin == \A n \in Nodes : (node_state[n] = Down) ~> (node_state[n] = Up) diff --git a/specifications/VortexDSE/Vortex_DSE_CSlot_TTL_Proofs.tla b/specifications/VortexDSE/Vortex_DSE_CSlot_TTL_Proofs.tla new file mode 100644 index 00000000..3b239d9b --- /dev/null +++ b/specifications/VortexDSE/Vortex_DSE_CSlot_TTL_Proofs.tla @@ -0,0 +1,54 @@ +------------------- MODULE Vortex_DSE_CSlot_TTL_Proofs ------------------- +(***************************************************************************) +(* The bounded-memory mode refines the default one. *) +(* *) +(* Its admission gate is m.cslot = current_slot where the default admits on *) +(* m.cslot <= current_slot, and no other action differs, so every behaviour *) +(* of this module is a behaviour of Vortex_DSE_CSlot under the identity *) +(* mapping. Every safety property established for the default mode is *) +(* therefore inherited here and does not need reproving. *) +(***************************************************************************) + +EXTENDS Vortex_DSE_CSlot_TTL, TLAPS + +LEMMA InitType == Init => TypeInvariant + BY DEF Init, TypeInvariant, MsgRecord + +LEMMA NextType == TypeInvariant /\ [Next]_vars => TypeInvariant' + BY DEF TypeInvariant, MsgRecord, vars, Next, Send, Process, Crash, Rejoin, Tick + +THEOREM TypeCorrect == Spec => []TypeInvariant + BY InitType, NextType, PTL DEF Spec + +\* The admission gate here is equality where the default admits on <=, so +\* the step needs to know that both are natural numbers: that is where the +\* type invariant is used, and nowhere else. +THEOREM Refinement == Spec => C!Spec +<1>1. Init => C!Init + BY DEF Init, C!Init, Up, C!Up +<1>2. TypeInvariant /\ [Next]_vars => [C!Next]_C!vars + <2> SUFFICES ASSUME TypeInvariant, Next PROVE [C!Next]_C!vars + BY DEF vars, C!vars + <2>1. CASE \E id \in MsgIDs, k \in Nat : Send(id, k) + BY <2>1 DEF Send, C!Next, C!Send + <2>2. CASE \E n \in Nodes, m \in network : Process(n, m) + <3> PICK nn \in Nodes, mm \in network : Process(nn, mm) + BY <2>2 + <3>1. mm.cslot \in Nat /\ current_slot \in Nat + BY DEF TypeInvariant, MsgRecord + <3>2. mm.cslot <= current_slot + BY <3>1 DEF Process + <3>. QED + BY <3>2 DEF Process, C!Next, C!Process, Up, C!Up + <2>3. CASE \E n \in Nodes : Crash(n) + BY <2>3 DEF Crash, C!Next, C!Crash, Up, Down, C!Up, C!Down + <2>4. CASE \E n \in Nodes : Rejoin(n) + BY <2>4 DEF Rejoin, C!Next, C!Rejoin, Up, Down, C!Up, C!Down + <2>5. CASE Tick + BY <2>5 DEF Tick, C!Next, C!Tick + <2>. QED + BY <2>1, <2>2, <2>3, <2>4, <2>5 DEF Next +<1>. QED + BY <1>1, <1>2, TypeCorrect, PTL DEF Spec, C!Spec + +============================================================================= diff --git a/specifications/VortexDSE/manifest.json b/specifications/VortexDSE/manifest.json index 6634938b..e36ca82c 100644 --- a/specifications/VortexDSE/manifest.json +++ b/specifications/VortexDSE/manifest.json @@ -67,6 +67,12 @@ "mode": "exhaustive search", "result": "success" }, + { + "path": "specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL_admission.cfg", + "runtime": "00:00:01", + "mode": "exhaustive search", + "result": "liveness failure" + }, { "path": "specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL_liveness.cfg", "runtime": "00:00:01", @@ -118,6 +124,14 @@ "path": "specifications/VortexDSE/Vortex_DSE_CSlot_TTL.tla", "features": [], "models": [] + }, + { + "path": "specifications/VortexDSE/Vortex_DSE_CSlot_TTL_Proofs.tla", + "features": [], + "models": [], + "proof": { + "maxRuntimeMinutes": 1 + } } ] } From 0bc3d2383604e7e2f756aa5716e6411251e5d16d Mon Sep 17 00:00:00 2001 From: Vasilis Nasopoulos Date: Sat, 8 Aug 2026 21:12:46 +0300 Subject: [PATCH 6/6] VortexDSE: remove the README pending a rewrite The current one describes the modules without stating the problem they address or what they deliberately do not cover, which is the substance review asked for. A README that misleads is worse than none while the replacement is written; several specs here carry no README at all. Co-Authored-By: Claude Opus 5 Signed-off-by: Vasilis Nasopoulos --- specifications/VortexDSE/README.md | 96 ------------------------------ 1 file changed, 96 deletions(-) delete mode 100644 specifications/VortexDSE/README.md diff --git a/specifications/VortexDSE/README.md b/specifications/VortexDSE/README.md deleted file mode 100644 index df38695a..00000000 --- a/specifications/VortexDSE/README.md +++ /dev/null @@ -1,96 +0,0 @@ -# Vortex DSE — C-slot admission and per-slot agreement - -Vortex DSE is a deterministic consensus protocol in which a message carries its -own slot stamp and each node decides admission locally, against its own clock. -There is no leader, no quorum and no vote: admission is an O(1) local predicate, -and cross-node agreement on the per-slot input set is established afterwards by -a separate layer. - -These specifications model that structure. They are the formal counterpart of a -running implementation; the implementation itself is not part of this -contribution. - -## Two admission modes - -The protocol has two admission rules, and the difference is one operator. - -| module | rule | meaning | -| --- | --- | --- | -| `Vortex_DSE_CSlot` | `m.cslot <= current_slot` | the default. A message stamped for slot *k* that arrives late is still admitted, into slot *k*. Nothing is dropped. | -| `Vortex_DSE_CSlot_TTL` | `m.cslot = current_slot` | an opt-in bounded-memory mode. A message that misses its slot is rejected permanently, so state does not grow behind the frontier. | - -Both modes are specified because both are implemented; the strict rule is a -memory concession, not a stronger version of the protocol, and the two -modules say exactly that: - -* `Vortex_DSE_CSlot_TTL_Proofs` proves `Spec => C!Spec` — the strict mode - refines the default one, so every safety property established for the - default is inherited rather than reproved. Equality is a stronger gate - than `<=`, and nothing else differs. - -* `MC_Vortex_DSE_CSlot_TTL_admission.cfg` is a deliberate liveness failure. - `EventualAdmission` holds under the default rule and does not hold here: a - message whose slot has passed is refused for good. That is the price of - bounding memory, checked rather than asserted. - -## Modules - -| module | what it adds | -| --- | --- | -| `Vortex_DSE_CSlot` | admission, crash and rejoin via a persisted snapshot | -| `Vortex_DSE_CSlot_Proofs` | `TypeCorrect`, `NoFutureAdmissionCorrect` | -| `Vortex_DSE_CSlot_ExactlyOnce_Proof` | `StrictExactlyOnceCorrect` | -| `Vortex_DSE_CSlot_TTL` | the strict admission mode | -| `Vortex_DSE_CSlot_TTL_Proofs` | that the strict mode refines the default one | -| `Vortex_DSE_CSlot_Skew` | replaces the single global slot with a per-node clock, plus Byzantine injection of forged slot stamps and origins | -| `Vortex_DSE_CSlot_AE` | the agreement layer: `Freeze`, `Reconcile`, `Commit` over the strict mode | -| `Vortex_DSE_CSlot_AE_Proofs` | deductive proofs for the agreement layer | - -None of these carries a slot horizon: the ticker is unbounded and the -adversary may forge any slot in `Nat`. Horizons are a model-checking concern -and live in the `MC_` modules, which bound the actions directly rather than -applying a state constraint — under a constraint TLC discards successor -states, which is unsound for the temporal properties. `MaxSkew` is the one -bound that stays in a specification, because it is an assumption the protocol -relies on rather than a checking artifact. - -`Vortex_DSE_CSlot_AE` is specified over the strict admission rule; it is not a -refinement of the default mode. Extending it to the late-tolerant rule requires -restating what "no reordering across slots" means, and is not done here. - -## What is checked - -All TLAPS proofs discharge under `tlapm --strict`, which fails on unproved -obligations and on proof steps left open — a plain `tlapm` invocation exits 0 -in both cases. There are no `OMITTED` steps in these modules. - -| | obligations | -| --- | --- | -| `Vortex_DSE_CSlot_Proofs` | 23 | -| `Vortex_DSE_CSlot_ExactlyOnce_Proof` | 19 | -| `Vortex_DSE_CSlot_AE_Proofs` | 10 | -| `Vortex_DSE_CSlot_TTL_Proofs` | 34 | - -Every model completes in a few seconds. `Vortex_DSE_CSlot_AE` also carries -Apalache type annotations, but no symbolic model is registered here; the models -below are TLC only. - -Each module states one property of interest and marks the rest as corollaries -of it, rather than presenting a flat list that suggests more is being proved -than is. In the core that property is `NoFutureAdmission`; in the agreement -layer it is the pair `ProcessedAreCurrentSlot` and `CommittedIsUnion`. - -Emission is a single action. An honest sender stamps the slot it is in and an -adversary stamps anything; since no fairness is assumed either way, splitting -them into two actions distinguished nothing. - -## Scope - -`Vortex_DSE_CSlot_Skew` bounds pairwise clock skew structurally, by forbidding -any tick that would breach `MaxSkew`. It states the assumption; it does not -model the mechanism that maintains it. Likewise `Reconcile` is a single atomic -step at specification level — the multi-round protocol underneath is out of -scope here. - -Source repositories, including the whitepaper and the model-checking logs: -