From 9a56943fd4171f8f73e24cf973e16c3593980793 Mon Sep 17 00:00:00 2001 From: Qian-Cheng-nju Date: Tue, 20 Oct 2026 17:09:23 +0000 Subject: [PATCH] Require Sailfish quorums to be upward closed Signed-off-by: Qian-Cheng-nju --- specifications/dag-consensus/Sailfish.tla | 4 ++++ specifications/dag-consensus/TLCSailfish1.tla | 1 + specifications/dag-consensus/TLCSailfish2.tla | 1 + 3 files changed, 6 insertions(+) diff --git a/specifications/dag-consensus/Sailfish.tla b/specifications/dag-consensus/Sailfish.tla index d80499b6..658ac741 100644 --- a/specifications/dag-consensus/Sailfish.tla +++ b/specifications/dag-consensus/Sailfish.tla @@ -43,6 +43,10 @@ ASSUME GSTIsARoundNumber == GST \in Nat \* have to form a quorum, or else no round could ever be entered: ASSUME CorrectNodesFormQuorum == IsQuorum(N \ F) +\* An additional vote cannot turn a quorum into a non-quorum. +ASSUME QuorumsAreMonotone == + \A Q, S \in SUBSET N : IsQuorum(Q) /\ Q \subseteq S => IsQuorum(S) + \* Removing the Byzantine nodes from a quorum leaves a blocking set: ASSUME QuorumMinusByzantineIsBlocking == \A Q \in SUBSET N : IsQuorum(Q) => IsBlocking(Q \ F) diff --git a/specifications/dag-consensus/TLCSailfish1.tla b/specifications/dag-consensus/TLCSailfish1.tla index 9f70d278..03784603 100644 --- a/specifications/dag-consensus/TLCSailfish1.tla +++ b/specifications/dag-consensus/TLCSailfish1.tla @@ -36,6 +36,7 @@ ASSUME RoundsStartAtOne ASSUME LeadersAreNodes ASSUME GSTIsARoundNumber ASSUME CorrectNodesFormQuorum +ASSUME QuorumsAreMonotone ASSUME QuorumMinusByzantineIsBlocking ASSUME BlockingSetsIntersectQuorums diff --git a/specifications/dag-consensus/TLCSailfish2.tla b/specifications/dag-consensus/TLCSailfish2.tla index 2a3facdc..28e02b12 100644 --- a/specifications/dag-consensus/TLCSailfish2.tla +++ b/specifications/dag-consensus/TLCSailfish2.tla @@ -34,6 +34,7 @@ ASSUME RoundsStartAtOne ASSUME LeadersAreNodes ASSUME GSTIsARoundNumber ASSUME CorrectNodesFormQuorum +ASSUME QuorumsAreMonotone ASSUME QuorumMinusByzantineIsBlocking ASSUME BlockingSetsIntersectQuorums