Skip to content

Commit 23b889d

Browse files
vasilisnasopoulosclaude
vasilisnasopoulos
and
claude
committed
Add the agreement layer as a refinement of the core
Vortex_DSE_CSlot_AE is not a refinement of anything, as noted on tlaplus#220: its NextCslot clears processed for every node at a slot boundary, which no core action can do, and it models no crash. Calling it a layer on top of the core was an overstatement. Vortex_DSE_CSlot_AE_Refinement is the same Freeze / Reconcile / Commit cycle written so that it is one. It carries the core's variables unchanged, lets processed accumulate, and keeps the per-slot input set in committed rather than recovering it by wiping processed. Every action is either a core action or leaves the core's variables alone: Submit, DuplicateInject are the core's Process is the core's, additionally gated on Open, and with the stronger equality gate NextCslot is the core's Tick Freeze, Reconcile change only phase and committed so THEOREM Refinement == Spec => C!Spec holds under the identity mapping on the core's variables. Proved in Vortex_DSE_CSlot_AE_Refinement_Proofs, 25 obligations, exit 0 under tlapm --strict. Crash and Rejoin are absent, which costs nothing: refinement asks that every behaviour of this module be a behaviour of the core, not the reverse. TLC checks the refinement as well, against the core's next-state relation with the forged slot bounded, since the core quantifies it over Nat: 103805 states, no error, alongside the four safety invariants. Co-authored-by: Claude Opus 5 <noreply@anthropic.com> Signed-off-by: Vasilis Nasopoulos <vasilis_nasopoulos@hotmail.com>
1 parent 9b3d8a9 commit 23b889d

6 files changed

Lines changed: 316 additions & 3 deletions

‎specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_Refinement.cfg‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
SPECIFICATION MCSpec
2+
3+
CONSTANTS
4+
Nodes = {n1, n2}
5+
MsgIDs = {m1, m2}
6+
MaxSlot = 2
7+
8+
INVARIANT MCTypeInvariant
9+
INVARIANT MerkleAgreement
10+
INVARIANT CommittedSupersetsProcessed
11+
INVARIANT NoPhantomInCommitted
12+
INVARIANT PhaseProgressionValid
13+
14+
PROPERTY MCRefinement

‎specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_Refinement.tla‎

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
---- MODULE MC_Vortex_DSE_CSlot_AE_Refinement ----
2+
(***************************************************************************)
3+
(* TLC harness. The horizon lives here, inside MCNextCslot, for the reason *)
4+
(* recorded in MC_Vortex_DSE_CSlot. *)
5+
(***************************************************************************)
6+
EXTENDS Vortex_DSE_CSlot_AE_Refinement
7+
8+
CONSTANT MaxSlot
9+
10+
ASSUME MaxSlotAssumption == MaxSlot \in Nat
11+
12+
Slots == 0..MaxSlot
13+
14+
MCNextCslot ==
15+
/\ current_slot < MaxSlot
16+
/\ NextCslot
17+
18+
MCNext ==
19+
\/ \E id \in MsgIDs : Submit(id)
20+
\/ \E n \in Nodes, m \in network : Process(n, m)
21+
\/ \E n \in Nodes : Freeze(n)
22+
\/ Reconcile
23+
\/ \E id \in MsgIDs, k \in Slots : DuplicateInject(id, k)
24+
\/ MCNextCslot
25+
26+
MCSpec == Init /\ [][MCNext]_vars
27+
28+
MCTypeInvariant ==
29+
/\ current_slot \in Slots
30+
/\ network \subseteq [id: MsgIDs, cslot: Slots]
31+
/\ processed \in [Nodes -> SUBSET MsgIDs]
32+
/\ persisted \in [Nodes -> SUBSET MsgIDs]
33+
/\ node_state \in [Nodes -> {C!Up, C!Down}]
34+
/\ phase \in [Nodes -> {Open, Frozen, Committed}]
35+
/\ committed \in [Nodes -> SUBSET MsgIDs]
36+
37+
\* Refinement, checked by TLC as a temporal property. The core's own Next
38+
\* quantifies the forged slot over Nat, which TLC cannot enumerate, so the
39+
\* proxy below is the core's next-state relation with that one quantifier
40+
\* bounded by the same horizon. Nothing else about the core is changed.
41+
MCCoreNext ==
42+
\/ \E id \in MsgIDs : C!Submit(id)
43+
\/ \E n \in Nodes, m \in network : C!Process(n, m)
44+
\/ \E n \in Nodes : C!Crash(n)
45+
\/ \E n \in Nodes : C!Rejoin(n)
46+
\/ \E id \in MsgIDs, k \in Slots : C!DuplicateInject(id, k)
47+
\/ C!Tick
48+
49+
MCRefinement == C!Init /\ [][MCCoreNext]_coreVars
50+
51+
====

‎specifications/VortexDSE/README.md‎

Lines changed: 19 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -33,6 +33,8 @@ memory concession, not a stronger version of the protocol.
3333
| `Vortex_DSE_CSlot_Skew` | replaces the single global slot with a per-node clock, plus Byzantine injection of forged slot stamps and origins |
3434
| `Vortex_DSE_CSlot_AE` | the agreement layer: `Freeze`, `Reconcile`, `Commit` over the strict mode |
3535
| `Vortex_DSE_CSlot_AE_Proofs` | deductive proofs for the agreement layer |
36+
| `Vortex_DSE_CSlot_AE_Refinement` | the agreement cycle as a refinement of the core |
37+
| `Vortex_DSE_CSlot_AE_Refinement_Proofs` | the refinement theorem |
3638

3739
None of these carries a slot horizon: the ticker is unbounded and the
3840
adversary may forge any slot in `Nat`. Horizons are a model-checking concern
@@ -42,9 +44,22 @@ states, which is unsound for the temporal properties. `MaxSkew` is the one
4244
bound that stays in a specification, because it is an assumption the protocol
4345
relies on rather than a checking artifact.
4446

45-
`Vortex_DSE_CSlot_AE` is specified over the strict admission rule; it is not a
46-
refinement of the default mode. Extending it to the late-tolerant rule requires
47-
restating what "no reordering across slots" means, and is not done here.
47+
`Vortex_DSE_CSlot_AE` is specified over the strict admission rule and is not a
48+
refinement of anything: its `NextCslot` clears `processed` for every node at a
49+
slot boundary, which no action of the core can do, and it models no crash.
50+
51+
`Vortex_DSE_CSlot_AE_Refinement` is the same agreement cycle written as an
52+
actual layer. It carries the core's variables unchanged, lets `processed`
53+
accumulate, and keeps the per-slot input set in `committed`. Every action is
54+
either a core action or leaves the core's variables alone, so
55+
56+
```
57+
THEOREM Refinement == Spec => C!Spec
58+
```
59+
60+
holds under the identity mapping — proved in
61+
`Vortex_DSE_CSlot_AE_Refinement_Proofs`, and checked by TLC as a temporal
62+
property besides.
4863

4964
## What is checked
5065

@@ -57,6 +72,7 @@ in both cases. There are no `OMITTED` steps in these modules.
5772
| `Vortex_DSE_CSlot_Proofs` | 191 |
5873
| `Vortex_DSE_CSlot_ExactlyOnce_Proof` | 128 |
5974
| `Vortex_DSE_CSlot_AE_Proofs` | 32 |
75+
| `Vortex_DSE_CSlot_AE_Refinement_Proofs` | 25 |
6076

6177
Every model completes in a few seconds. `Vortex_DSE_CSlot_AE` also carries
6278
Apalache type annotations, but no symbolic model is registered here; the models

‎specifications/VortexDSE/Vortex_DSE_CSlot_AE_Refinement.tla‎

Lines changed: 172 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,172 @@
1+
------------------- MODULE Vortex_DSE_CSlot_AE_Refinement -------------------
2+
(***************************************************************************)
3+
(* Vortex DSE — the agreement layer as a refinement of the core. *)
4+
(* *)
5+
(* Vortex_DSE_CSlot_AE specifies the Freeze / Reconcile / Commit cycle as *)
6+
(* a standalone state machine, and is deliberately not a refinement of *)
7+
(* anything: its NextCslot clears processed for every node at a slot *)
8+
(* boundary, which no action of Vortex_DSE_CSlot can do, and it models no *)
9+
(* crash. Presenting it as a layer on top of the core was therefore an *)
10+
(* overstatement. *)
11+
(* *)
12+
(* This module is the layer. It carries the core's variables unchanged and *)
13+
(* adds the two the agreement phase needs, and every action either is a *)
14+
(* core action or leaves the core's variables alone: *)
15+
(* *)
16+
(* Submit, DuplicateInject are the core's *)
17+
(* Process is the core's, additionally gated on Open *)
18+
(* NextCslot is the core's Tick *)
19+
(* Freeze, Reconcile change only phase and committed *)
20+
(* *)
21+
(* processed accumulates, as in the core; the per-slot input set lives in *)
22+
(* committed instead of being recovered by wiping processed. *)
23+
(* *)
24+
(* Crash and Rejoin are absent. That costs nothing here: refinement asks *)
25+
(* that every behaviour of this module be a behaviour of the core, not the *)
26+
(* reverse, so a layer may exercise fewer of the core's actions than the *)
27+
(* core allows. *)
28+
(***************************************************************************)
29+
30+
EXTENDS Naturals, FiniteSets
31+
32+
CONSTANTS Nodes, MsgIDs
33+
34+
ASSUME NodesAssumption == IsFiniteSet(Nodes) /\ Nodes # {}
35+
ASSUME MsgIDsAssumption == IsFiniteSet(MsgIDs)
36+
37+
Open == "open"
38+
Frozen == "frozen"
39+
Committed == "committed"
40+
41+
VARIABLES
42+
current_slot, \* core: global slot counter
43+
network, \* core: in-flight messages
44+
processed, \* core: ids admitted by each node, cumulative
45+
persisted, \* core: crash snapshot; constant here
46+
node_state, \* core: liveness; constant here
47+
phase, \* phase[n] \in {Open, Frozen, Committed}
48+
committed \* committed[n] = agreed input set after Reconcile
49+
50+
coreVars == <<current_slot, network, processed, persisted, node_state>>
51+
vars == <<current_slot, network, processed, persisted, node_state,
52+
phase, committed>>
53+
54+
\* The core, over the same variable names.
55+
C == INSTANCE Vortex_DSE_CSlot
56+
57+
MsgRecord == [id: MsgIDs, cslot: Nat]
58+
59+
-------------------------------------------------------------------------------
60+
(* INITIAL STATE *)
61+
62+
Init ==
63+
/\ current_slot = 0
64+
/\ network = {}
65+
/\ processed = [n \in Nodes |-> {}]
66+
/\ persisted = [n \in Nodes |-> {}]
67+
/\ node_state = [n \in Nodes |-> C!Up]
68+
/\ phase = [n \in Nodes |-> Open]
69+
/\ committed = [n \in Nodes |-> {}]
70+
71+
-------------------------------------------------------------------------------
72+
(* ACTIONS *)
73+
74+
\* Core actions, with the agreement variables left alone.
75+
76+
Submit(id) ==
77+
/\ C!Submit(id)
78+
/\ UNCHANGED <<phase, committed>>
79+
80+
DuplicateInject(id, fake_cslot) ==
81+
/\ C!DuplicateInject(id, fake_cslot)
82+
/\ UNCHANGED <<phase, committed>>
83+
84+
\* Admission, additionally closed once the node has frozen. The core admits
85+
\* on m.cslot <= current_slot; here the gate is equality, which is stronger,
86+
\* so every step of this action is still a step of the core's.
87+
Process(n, m) ==
88+
/\ phase[n] = Open
89+
/\ m.cslot = current_slot
90+
/\ C!Process(n, m)
91+
/\ UNCHANGED <<phase, committed>>
92+
93+
\* Advancing the slot is exactly the core's Tick: processed is carried over
94+
\* rather than cleared.
95+
NextCslot ==
96+
/\ \A n \in Nodes : phase[n] = Committed
97+
/\ C!Tick
98+
/\ phase' = [n \in Nodes |-> Open]
99+
/\ UNCHANGED committed
100+
101+
-------------------------------------------------------------------------------
102+
\* Agreement actions. These touch none of the core's variables, so they are
103+
\* stuttering steps of the core.
104+
105+
Freeze(n) ==
106+
/\ n \in Nodes
107+
/\ phase[n] = Open
108+
/\ phase' = [phase EXCEPT ![n] = Frozen]
109+
/\ UNCHANGED <<coreVars, committed>>
110+
111+
Reconcile ==
112+
/\ \A n \in Nodes : phase[n] = Frozen
113+
/\ LET union_view == UNION { processed[n] : n \in Nodes }
114+
IN committed' = [n \in Nodes |-> union_view]
115+
/\ phase' = [n \in Nodes |-> Committed]
116+
/\ UNCHANGED coreVars
117+
118+
-------------------------------------------------------------------------------
119+
120+
Next ==
121+
\/ \E id \in MsgIDs : Submit(id)
122+
\/ \E n \in Nodes, m \in network : Process(n, m)
123+
\/ \E n \in Nodes : Freeze(n)
124+
\/ Reconcile
125+
\/ \E id \in MsgIDs, k \in Nat : DuplicateInject(id, k)
126+
\/ NextCslot
127+
128+
Spec == Init /\ [][Next]_vars
129+
130+
-------------------------------------------------------------------------------
131+
(* INVARIANTS *)
132+
133+
TypeInvariant ==
134+
/\ current_slot \in Nat
135+
/\ network \subseteq MsgRecord
136+
/\ processed \in [Nodes -> SUBSET MsgIDs]
137+
/\ persisted \in [Nodes -> SUBSET MsgIDs]
138+
/\ node_state \in [Nodes -> {C!Up, C!Down}]
139+
/\ phase \in [Nodes -> {Open, Frozen, Committed}]
140+
/\ committed \in [Nodes -> SUBSET MsgIDs]
141+
142+
\* Nodes that have committed hold the same set.
143+
MerkleAgreement ==
144+
\A a, b \in Nodes :
145+
(phase[a] = Committed /\ phase[b] = Committed) =>
146+
committed[a] = committed[b]
147+
148+
\* Committing never drops what a node admitted locally.
149+
CommittedSupersetsProcessed ==
150+
\A n \in Nodes :
151+
phase[n] = Committed => processed[n] \subseteq committed[n]
152+
153+
\* Nothing is committed that was never in the network.
154+
NoPhantomInCommitted ==
155+
\A n \in Nodes :
156+
\A id \in committed[n] : \E m \in network : m.id = id
157+
158+
\* Nodes move Open -> Frozen -> Committed and reopen only on a slot change,
159+
\* so no node is ever behind a peer by more than one phase in a way that
160+
\* would let Reconcile run on a mixed view.
161+
PhaseProgressionValid ==
162+
(\E n \in Nodes : phase[n] = Committed) =>
163+
(\A n \in Nodes : phase[n] # Open)
164+
165+
-------------------------------------------------------------------------------
166+
(* REFINEMENT *)
167+
(* *)
168+
(* Every behaviour of this module is a behaviour of Vortex_DSE_CSlot, under *)
169+
(* the identity mapping on the core's variables. Stated and proved in *)
170+
(* Vortex_DSE_CSlot_AE_Refinement_Proofs. *)
171+
172+
=============================================================================

‎specifications/VortexDSE/Vortex_DSE_CSlot_AE_Refinement_Proofs.tla‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
---------------- MODULE Vortex_DSE_CSlot_AE_Refinement_Proofs ----------------
2+
(***************************************************************************)
3+
(* The agreement layer refines the core, under the identity mapping on the *)
4+
(* core's variables. *)
5+
(***************************************************************************)
6+
7+
EXTENDS Vortex_DSE_CSlot_AE_Refinement, TLAPS
8+
9+
THEOREM Refinement == Spec => C!Spec
10+
<1>1. Init => C!Init
11+
BY DEF Init, C!Init
12+
<1>2. [Next]_vars => [C!Next]_C!vars
13+
<2> SUFFICES ASSUME Next
14+
PROVE [C!Next]_coreVars
15+
BY DEF vars, coreVars, C!vars
16+
<2>1. CASE \E id \in MsgIDs : Submit(id)
17+
BY <2>1 DEF Submit, C!Next
18+
<2>2. CASE \E n \in Nodes, m \in network : Process(n, m)
19+
BY <2>2 DEF Process, C!Next
20+
<2>3. CASE \E n \in Nodes : Freeze(n)
21+
BY <2>3 DEF Freeze, coreVars, C!vars
22+
<2>4. CASE Reconcile
23+
BY <2>4 DEF Reconcile, coreVars, C!vars
24+
<2>5. CASE \E id \in MsgIDs, k \in Nat : DuplicateInject(id, k)
25+
BY <2>5 DEF DuplicateInject, C!Next
26+
<2>6. CASE NextCslot
27+
BY <2>6 DEF NextCslot, C!Next
28+
<2>. QED
29+
BY <2>1, <2>2, <2>3, <2>4, <2>5, <2>6 DEF Next
30+
<1>. QED
31+
BY <1>1, <1>2, PTL DEF Spec, C!Spec
32+
33+
=============================================================================

‎specifications/VortexDSE/manifest.json‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -49,6 +49,20 @@
4949
}
5050
]
5151
},
52+
{
53+
"path": "specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_Refinement.tla",
54+
"features": [],
55+
"models": [
56+
{
57+
"path": "specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_Refinement.cfg",
58+
"runtime": "00:00:02",
59+
"mode": "exhaustive search",
60+
"result": "success",
61+
"totalStates": 103805,
62+
"distinctStates": 13389
63+
}
64+
]
65+
},
5266
{
5367
"path": "specifications/VortexDSE/MC_Vortex_DSE_CSlot_Skew.tla",
5468
"features": [],
@@ -101,6 +115,19 @@
101115
"maxRuntimeMinutes": 1
102116
}
103117
},
118+
{
119+
"path": "specifications/VortexDSE/Vortex_DSE_CSlot_AE_Refinement.tla",
120+
"features": [],
121+
"models": []
122+
},
123+
{
124+
"path": "specifications/VortexDSE/Vortex_DSE_CSlot_AE_Refinement_Proofs.tla",
125+
"features": [],
126+
"models": [],
127+
"proof": {
128+
"maxRuntimeMinutes": 1
129+
}
130+
},
104131
{
105132
"path": "specifications/VortexDSE/Vortex_DSE_CSlot_ExactlyOnce_Proof.tla",
106133
"features": [],

0 commit comments

Comments
 (0)