Skip to content

Commit 50377ce

Browse files
vasilisnasopoulosclaude
vasilisnasopoulos
and
claude
committed
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 <noreply@anthropic.com> Signed-off-by: Vasilis Nasopoulos <vasilis_nasopoulos@hotmail.com>
1 parent 352084b commit 50377ce

18 files changed

Lines changed: 1828 additions & 0 deletions

‎README.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -108,6 +108,7 @@ Here is a list of specs included in this repository which are validated by the C
108108
| [DAG-based Consensus](specifications/dag-consensus) | Giuliano Losa | | | ✔ | ✔ | |
109109
| [German Cache-Coherence Protocol](specifications/GermanProtocol) | Markus Kuppe | | | | ✔ | ✔ |
110110
| [FLASH Cache-Coherence Protocol](specifications/FlashProtocol) | Markus Kuppe | | | | ✔ | ✔ |
111+
| [Vortex DSE](specifications/VortexDSE) | Vasilis Nasopoulos | | ✔ | | ✔ | |
111112

112113

113114
## Other Examples

‎specifications/VortexDSE/MC_Vortex_DSE_CSlot.cfg‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
\* TLC model configuration for Vortex_DSE_CSlot.
2+
\* Two nodes, two message ids, slot horizon 2 — bounded but non-trivial.
3+
4+
CONSTANT
5+
Nodes = {n1, n2}
6+
MsgIDs = {m1, m2}
7+
MaxSlot = 2
8+
9+
INIT Init
10+
NEXT Next
11+
12+
INVARIANT TypeInvariant
13+
INVARIANT NoFutureAdmission
14+
INVARIANT ExactlyOncePerNode
15+
INVARIANT NoPhantomProcess
16+
INVARIANT DecisionLocalityOnly
17+
18+
CONSTRAINT StateConstraint

‎specifications/VortexDSE/MC_Vortex_DSE_CSlot.tla‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
---- MODULE MC_Vortex_DSE_CSlot ----
2+
(* TLC bounded model-checking harness for Vortex_DSE_CSlot. *)
3+
(* Constants are assigned in MC_Vortex_DSE_CSlot.cfg: *)
4+
(* Nodes = {n1, n2} *)
5+
(* MsgIDs = {m1, m2} *)
6+
(* MaxSlot = 2 *)
7+
EXTENDS Vortex_DSE_CSlot
8+
====

‎specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE.tla‎

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
---------------- MODULE MC_Vortex_DSE_CSlot_AE ----------------
2+
(* Apalache harness for Vortex_DSE_CSlot_AE. *)
3+
(* Fixes constants and bundles the safety invariants for a single *)
4+
(* symbolic (SMT-backed) check via Apalache. *)
5+
6+
EXTENDS Vortex_DSE_CSlot_AE
7+
8+
ConstInit ==
9+
/\ Nodes = {"n1", "n2"}
10+
/\ MsgIDs = {"a", "b"}
11+
/\ MaxSlot = 1
12+
13+
\* Conjunction of every safety invariant in the module.
14+
AllInv ==
15+
/\ TypeInvariant
16+
/\ MerkleAgreement
17+
/\ CommittedSupersetsProcessed
18+
/\ NoPhantomInCommitted
19+
/\ NoReorderAcrossCslot
20+
/\ PhaseProgressionValid
21+
22+
===============================================================

‎specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_liveness.cfg‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
SPECIFICATION LiveSpec
2+
3+
CONSTANTS
4+
Nodes = {n1, n2}
5+
MsgIDs = {m1}
6+
MaxSlot = 1
7+
8+
PROPERTIES
9+
EventualCommit
10+
EventualAgreement
11+
12+
CONSTRAINT
13+
StateConstraint

‎specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_tiny.cfg‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
SPECIFICATION Spec
2+
3+
CONSTANTS
4+
Nodes = {n1, n2}
5+
MsgIDs = {m1, m2}
6+
MaxSlot = 2
7+
8+
INVARIANTS
9+
TypeInvariant
10+
MerkleAgreement
11+
CommittedSupersetsProcessed
12+
NoPhantomInCommitted
13+
NoReorderAcrossCslot
14+
PhaseProgressionValid
15+
16+
CONSTRAINT
17+
StateConstraint

‎specifications/VortexDSE/README.md‎

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
# Vortex DSE — C-slot admission and per-slot agreement
2+
3+
Vortex DSE is a deterministic consensus protocol in which a message carries its
4+
own slot stamp and each node decides admission locally, against its own clock.
5+
There is no leader, no quorum and no vote: admission is an O(1) local predicate,
6+
and cross-node agreement on the per-slot input set is established afterwards by
7+
a separate layer.
8+
9+
These specifications model that structure. They are the formal counterpart of a
10+
running implementation; the implementation itself is not part of this
11+
contribution.
12+
13+
## Two admission modes
14+
15+
The protocol has two admission rules, and the difference is one operator.
16+
17+
| module | rule | meaning |
18+
| --- | --- | --- |
19+
| `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. |
20+
| `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. |
21+
22+
Both modes are specified because both are implemented; the strict rule is a
23+
memory concession, not a stronger version of the protocol.
24+
25+
## Modules
26+
27+
| module | what it adds |
28+
| --- | --- |
29+
| `Vortex_DSE_CSlot` | admission, crash and rejoin via a persisted snapshot |
30+
| `Vortex_DSE_CSlot_Proofs` | `TypeCorrect`, `NoFutureAdmissionCorrect` |
31+
| `Vortex_DSE_CSlot_ExactlyOnce_Proof` | `StrictExactlyOnceCorrect` |
32+
| `Vortex_DSE_CSlot_TTL` | the strict admission mode |
33+
| `Vortex_DSE_CSlot_Skew` | replaces the single global slot with a per-node clock, plus Byzantine injection of forged slot stamps and origins |
34+
| `Vortex_DSE_CSlot_AE` | the agreement layer: `Freeze`, `Reconcile`, `Commit` over the strict mode |
35+
| `Vortex_DSE_CSlot_AE_Proofs` | deductive proofs for the agreement layer |
36+
37+
`Vortex_DSE_CSlot_AE` is specified over the strict admission rule; it is not a
38+
refinement of the default mode. Extending it to the late-tolerant rule requires
39+
restating what "no reordering across slots" means, and is not done here.
40+
41+
## What is checked
42+
43+
All TLAPS proofs discharge under `tlapm --strict`, which fails on unproved
44+
obligations and on proof steps left open — a plain `tlapm` invocation exits 0
45+
in both cases. There are no `OMITTED` steps in these modules.
46+
47+
| | obligations |
48+
| --- | --- |
49+
| `Vortex_DSE_CSlot_Proofs` | 194 |
50+
| `Vortex_DSE_CSlot_ExactlyOnce_Proof` | 131 |
51+
| `Vortex_DSE_CSlot_AE_Proofs` | 34 |
52+
53+
Every model completes in a few seconds. `Vortex_DSE_CSlot_AE` also carries
54+
Apalache type annotations, but no symbolic model is registered here; the models
55+
below are TLC only.
56+
57+
## Scope
58+
59+
`Vortex_DSE_CSlot_Skew` bounds pairwise clock skew structurally, by forbidding
60+
any tick that would breach the bound. It states the assumption; it does not
61+
model the mechanism that maintains it. Likewise `Reconcile` is a single atomic
62+
step at specification level — the multi-round protocol underneath is out of
63+
scope here.
64+
65+
Source repositories, including the whitepaper and the model-checking logs:
66+
<https://github.com/vasilisnasopoulos>

0 commit comments

Comments
 (0)