From d0cb13b617a0599a8f408a770fedc0a689629956 Mon Sep 17 00:00:00 2001 From: Qian-Cheng-nju Date: Tue, 20 Oct 2026 17:09:23 +0000 Subject: [PATCH] Validate Byzantine leader proposals in Sailfish Signed-off-by: Qian-Cheng-nju --- specifications/dag-consensus/Sailfish.tla | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/specifications/dag-consensus/Sailfish.tla b/specifications/dag-consensus/Sailfish.tla index d80499b6..0fdbe2ba 100644 --- a/specifications/dag-consensus/Sailfish.tla +++ b/specifications/dag-consensus/Sailfish.tla @@ -128,6 +128,9 @@ l0: while (TRUE) { else with (delivered \in SUBSET {v \in vs : Round(v) = r-1}) { await IsQuorum({Node(v) : v \in delivered}); \* ignored otherwise + if (Leader(r) = self) + await \/ LeaderVertex(r-1) \in delivered + \/ NoLeaderVoteQuorum(r, {v \in vs : Round(v) = r}, {self}); vs := vs \cup {newV}; es := es \cup {<> : pv \in delivered} } @@ -135,8 +138,8 @@ l0: while (TRUE) { } } }*) -\* BEGIN TRANSLATION (chksum(pcal) = "c16dfa43" /\ chksum(tla) = "9cdbd4f5") -\* Label l0 of process correctNode at line 42 col 9 changed to l0_ +\* BEGIN TRANSLATION (chksum(pcal) = "1dcb31ed" /\ chksum(tla) = "afe5b430") +\* Label l0 of process correctNode at line 73 col 9 changed to l0_ VARIABLES vs, es (* define statement *) @@ -195,6 +198,10 @@ byzantineNode(self) == /\ \E r \in R: /\ es' = (es \cup {<>}) ELSE /\ \E delivered \in SUBSET {v \in vs : Round(v) = r-1}: /\ IsQuorum({Node(v) : v \in delivered}) + /\ IF Leader(r) = self + THEN /\ \/ LeaderVertex(r-1) \in delivered + \/ NoLeaderVoteQuorum(r, {v \in vs : Round(v) = r}, {self}) + ELSE /\ TRUE /\ vs' = (vs \cup {newV}) /\ es' = (es \cup {<> : pv \in delivered}) /\ UNCHANGED << round, log >>