Skip to content

Commit ac2cea6

Browse files
vasilisnasopoulosclaude
vasilisnasopoulos
and
claude
committed
Move model-checking bounds out of the specifications
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 <noreply@anthropic.com> Signed-off-by: Vasilis Nasopoulos <vasilis_nasopoulos@hotmail.com>
1 parent 7c0b420 commit ac2cea6

21 files changed

Lines changed: 396 additions & 224 deletions

‎specifications/VortexDSE/MC_Vortex_DSE_CSlot.cfg‎

Lines changed: 8 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,15 @@
1-
\* TLC model configuration for Vortex_DSE_CSlot.
2-
\* Two nodes, two message ids, slot horizon 2 — bounded but non-trivial.
1+
\* Safety model. The horizon lives in MCNext, so no state constraint is
2+
\* needed: the reachable state graph is already finite.
33

4-
CONSTANT
5-
Nodes = {n1, n2}
6-
MsgIDs = {m1, m2}
7-
MaxSlot = 2
4+
SPECIFICATION MCSpec
85

9-
INIT Init
10-
NEXT Next
6+
CONSTANTS
7+
Nodes = {n1, n2}
8+
MsgIDs = {m1, m2}
9+
MaxSlot = 2
1110

12-
INVARIANT TypeInvariant
11+
INVARIANT MCTypeInvariant
1312
INVARIANT NoFutureAdmission
1413
INVARIANT ExactlyOncePerNode
1514
INVARIANT NoPhantomProcess
1615
INVARIANT DecisionLocalityOnly
17-
18-
CONSTRAINT StateConstraint

‎specifications/VortexDSE/MC_Vortex_DSE_CSlot.tla‎

Lines changed: 51 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,54 @@
11
---- 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 *)
2+
(***************************************************************************)
3+
(* TLC harness for Vortex_DSE_CSlot. *)
4+
(* *)
5+
(* The specification itself has no slot horizon: Tick is unbounded and *)
6+
(* DuplicateInject may forge any slot in Nat. The horizon is a *)
7+
(* model-checking concern and lives here. *)
8+
(* *)
9+
(* It is imposed inside the actions rather than as a CONSTRAINT, so the *)
10+
(* state graph is genuinely finite rather than merely truncated. That *)
11+
(* matters for the liveness model: under a state constraint TLC discards *)
12+
(* successor states, which can mask or invent violations of temporal *)
13+
(* properties. *)
14+
(***************************************************************************)
715
EXTENDS Vortex_DSE_CSlot
16+
17+
CONSTANT MaxSlot
18+
19+
Slots == 0..MaxSlot
20+
21+
\* The ticker stops at the horizon.
22+
MCTick ==
23+
/\ current_slot < MaxSlot
24+
/\ Tick
25+
26+
MCNext ==
27+
\/ \E id \in MsgIDs : Submit(id)
28+
\/ \E n \in Nodes, m \in network : Process(n, m)
29+
\/ \E n \in Nodes : Crash(n)
30+
\/ \E n \in Nodes : Rejoin(n)
31+
\/ \E id \in MsgIDs, k \in Slots : DuplicateInject(id, k)
32+
\/ MCTick
33+
34+
MCSpec == Init /\ [][MCNext]_vars
35+
36+
MCFairness ==
37+
/\ WF_vars(MCTick)
38+
/\ \A n \in Nodes : WF_vars(Rejoin(n))
39+
/\ \A n \in Nodes : SF_vars(\E m \in network : Process(n, m))
40+
41+
MCLiveSpec == Init /\ [][MCNext]_vars /\ MCFairness
42+
43+
\* Bounded counterpart of TickProgress, strengthened as suggested: once the
44+
\* ticker reaches the horizon MCTick is permanently disabled, so the slot
45+
\* counter stays there rather than merely visiting it.
46+
MCTickProgress == <>[](current_slot = MaxSlot)
47+
48+
\* Everything reachable in this model lies within the horizon.
49+
MCTypeInvariant ==
50+
/\ TypeInvariant
51+
/\ current_slot \in Slots
52+
/\ \A m \in network : m.cslot \in Slots
53+
854
====

‎specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE.tla‎

Lines changed: 43 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1,22 +1,52 @@
11
---------------- 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-
2+
(***************************************************************************)
3+
(* Harness for Vortex_DSE_CSlot_AE, used by both TLC and Apalache. *)
4+
(* *)
5+
(* The specification has no slot horizon; NextCslot advances without bound *)
6+
(* and DuplicateInject may forge any slot in Nat. The horizon is a *)
7+
(* model-checking concern and is imposed here inside the actions, not as a *)
8+
(* CONSTRAINT, so no successor state is discarded while temporal properties *)
9+
(* are checked. *)
10+
(* *)
11+
(* Invariants are deliberately left separate rather than bundled into one *)
12+
(* conjunction, so that a checker reports which one was violated. *)
13+
(***************************************************************************)
614
EXTENDS Vortex_DSE_CSlot_AE
715

16+
CONSTANT MaxSlot
17+
18+
Slots == 0..MaxSlot
19+
20+
MCNextCslot ==
21+
/\ current_slot < MaxSlot
22+
/\ NextCslot
23+
24+
MCNext ==
25+
\/ \E id \in MsgIDs : Submit(id)
26+
\/ \E n \in Nodes, m \in network : Process(n, m)
27+
\/ \E n \in Nodes : Freeze(n)
28+
\/ Reconcile
29+
\/ \E id \in MsgIDs, k \in Slots : DuplicateInject(id, k)
30+
\/ MCNextCslot
31+
32+
MCSpec == Init /\ [][MCNext]_vars
33+
34+
MCFairness ==
35+
/\ SF_vars(Reconcile)
36+
/\ SF_vars(MCNextCslot)
37+
/\ \A n \in Nodes : WF_vars(Freeze(n))
38+
39+
MCLiveSpec == Init /\ [][MCNext]_vars /\ MCFairness
40+
41+
MCTypeInvariant ==
42+
/\ TypeInvariant
43+
/\ current_slot \in Slots
44+
/\ \A m \in network : m.cslot \in Slots
45+
46+
\* Apalache entry point: constants fixed symbolically.
847
ConstInit ==
948
/\ Nodes = {"n1", "n2"}
1049
/\ MsgIDs = {"a", "b"}
1150
/\ MaxSlot = 1
1251

13-
\* Conjunction of every safety invariant in the module.
14-
AllInv ==
15-
/\ TypeInvariant
16-
/\ MerkleAgreement
17-
/\ CommittedSupersetsProcessed
18-
/\ NoPhantomInCommitted
19-
/\ NoReorderAcrossCslot
20-
/\ PhaseProgressionValid
21-
2252
===============================================================

‎specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_liveness.cfg‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,6 @@
1-
SPECIFICATION LiveSpec
1+
\* Liveness model. Bounded through MCNext rather than a CONSTRAINT.
2+
3+
SPECIFICATION MCLiveSpec
24

35
CONSTANTS
46
Nodes = {n1, n2}
@@ -8,6 +10,3 @@ CONSTANTS
810
PROPERTIES
911
EventualCommit
1012
EventualAgreement
11-
12-
CONSTRAINT
13-
StateConstraint

‎specifications/VortexDSE/MC_Vortex_DSE_CSlot_AE_tiny.cfg‎

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,17 +1,16 @@
1-
SPECIFICATION Spec
1+
\* Safety model for the agreement layer, under adversarial replay.
2+
3+
SPECIFICATION MCSpec
24

35
CONSTANTS
46
Nodes = {n1, n2}
57
MsgIDs = {m1, m2}
68
MaxSlot = 2
79

810
INVARIANTS
9-
TypeInvariant
11+
MCTypeInvariant
1012
MerkleAgreement
1113
CommittedSupersetsProcessed
1214
NoPhantomInCommitted
1315
NoReorderAcrossCslot
1416
PhaseProgressionValid
15-
16-
CONSTRAINT
17-
StateConstraint

specifications/VortexDSE/Vortex_DSE_CSlot_Skew_tiny.cfg renamed to specifications/VortexDSE/MC_Vortex_DSE_CSlot_Skew.cfg

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,17 @@
1-
SPECIFICATION Spec
1+
\* Per-node clocks under bounded skew, with Byzantine slot/origin spoofing.
2+
3+
SPECIFICATION MCSpec
24

35
CONSTANTS
46
Nodes = {n1, n2}
57
MsgIDs = {m1}
6-
MaxSlot = 2
78
MaxSkew = 1
9+
MaxSlot = 2
810

911
INVARIANTS
10-
TypeInvariant
12+
MCTypeInvariant
1113
BoundedSkew
1214
ExactlyOncePerNode
1315
CSlotLocalAdmission
1416
PersistedReflectsReality
1517
NoPhantomProcess
16-
17-
CONSTRAINT
18-
StateConstraint

‎specifications/VortexDSE/MC_Vortex_DSE_CSlot_Skew.tla‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
---- MODULE MC_Vortex_DSE_CSlot_Skew ----
2+
(***************************************************************************)
3+
(* TLC harness for Vortex_DSE_CSlot_Skew. *)
4+
(* *)
5+
(* MaxSkew is a protocol parameter and stays in the specification: it is *)
6+
(* the assumption the protocol relies on. MaxSlot is only a horizon for *)
7+
(* model checking, so it lives here and bounds the actions directly. *)
8+
(***************************************************************************)
9+
EXTENDS Vortex_DSE_CSlot_Skew
10+
11+
CONSTANT MaxSlot
12+
13+
Slots == 0..MaxSlot
14+
15+
MCTick(n) ==
16+
/\ node_slot[n] < MaxSlot
17+
/\ SkewedTick(n)
18+
19+
MCNext ==
20+
\/ \E id \in MsgIDs, n \in Nodes : Submit(id, n)
21+
\/ \E n \in Nodes, m \in network : Process(n, m)
22+
\/ \E n \in Nodes : Crash(n)
23+
\/ \E n \in Nodes : Rejoin(n)
24+
\/ \E id \in MsgIDs, k \in Slots, o \in Nodes : ByzantineInject(id, k, o)
25+
\/ \E n \in Nodes : MCTick(n)
26+
27+
MCSpec == Init /\ [][MCNext]_vars
28+
29+
MCTypeInvariant ==
30+
/\ TypeInvariant
31+
/\ node_slot \in [Nodes -> Slots]
32+
/\ \A m \in network : m.cslot \in Slots
33+
34+
====

specifications/VortexDSE/Vortex_DSE_CSlot_TTL_tiny.cfg renamed to specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL.cfg

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,17 @@
1-
SPECIFICATION Spec
1+
\* Safety model for the strict (opt-in TTL) admission mode.
2+
3+
SPECIFICATION MCSpec
24

35
CONSTANTS
46
Nodes = {n1, n2}
57
MsgIDs = {m1, m2}
68
MaxSlot = 4
79

810
INVARIANTS
9-
TypeInvariant
11+
MCTypeInvariant
1012
ExactlyOncePerNode
1113
CSlotStrictAdmission
1214
PersistedReflectsReality
1315
NoPhantomProcess
1416
DecisionLocalityOnly
1517
NoLateAdmission
16-
17-
CONSTRAINT
18-
StateConstraint

‎specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL.tla‎

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
---- MODULE MC_Vortex_DSE_CSlot_TTL ----
2+
(***************************************************************************)
3+
(* TLC harness for Vortex_DSE_CSlot_TTL. *)
4+
(* *)
5+
(* As in MC_Vortex_DSE_CSlot, the slot horizon is a model-checking concern *)
6+
(* and is imposed inside the actions rather than as a CONSTRAINT, so that *)
7+
(* no successor state is discarded while temporal properties are checked. *)
8+
(***************************************************************************)
9+
EXTENDS Vortex_DSE_CSlot_TTL
10+
11+
CONSTANT MaxSlot
12+
13+
Slots == 0..MaxSlot
14+
15+
MCTick ==
16+
/\ current_slot < MaxSlot
17+
/\ Tick
18+
19+
MCNext ==
20+
\/ \E id \in MsgIDs : Submit(id)
21+
\/ \E n \in Nodes, m \in network : Process(n, m)
22+
\/ \E n \in Nodes : Crash(n)
23+
\/ \E n \in Nodes : Rejoin(n)
24+
\/ \E id \in MsgIDs, k \in Slots : DuplicateInject(id, k)
25+
\/ MCTick
26+
27+
MCSpec == Init /\ [][MCNext]_vars
28+
29+
MCFairness ==
30+
/\ WF_vars(MCTick)
31+
/\ \A n \in Nodes : WF_vars(Rejoin(n))
32+
33+
MCLiveSpec == Init /\ [][MCNext]_vars /\ MCFairness
34+
35+
MCTickProgress == <>[](current_slot = MaxSlot)
36+
37+
MCTypeInvariant ==
38+
/\ TypeInvariant
39+
/\ current_slot \in Slots
40+
/\ \A m \in network : m.cslot \in Slots
41+
42+
====

‎specifications/VortexDSE/MC_Vortex_DSE_CSlot_TTL_liveness.cfg‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
\* Liveness model. Bounded through MCNext rather than a CONSTRAINT.
2+
3+
SPECIFICATION MCLiveSpec
4+
5+
CONSTANTS
6+
Nodes = {n1, n2}
7+
MsgIDs = {m1}
8+
MaxSlot = 2
9+
10+
PROPERTIES
11+
MCTickProgress
12+
EventualRejoin

0 commit comments

Comments
 (0)