Skip to content

Commit

Permalink
Rewrite TypeOK into monstrous universal quantification that avoids co…
Browse files Browse the repository at this point in the history 
…nstraint explosion.

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
  • Loading branch information
@lemmy
lemmy committed Sep 3, 2024
1 parent a323287 commit 61e7b5e
Show file tree
Hide file tree
Showing 2 changed files with 177 additions and 1 deletion.
2 changes: 2 additions & 0 deletions APApbft.cfg
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,8 @@ CONSTANTS
\* (compare https://github.com/heidihoward/pbft-tlaplus/issues/5#issuecomment-2315767599)
Tstamps <- MC_Tstamps
Views <- MC_Views

Init <- GenInit

INVARIANTS
TypeOK
Expand Down
176 changes: 175 additions & 1 deletion APApbft.tla
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ $ bin/apalache-mc check --config=APApbft.cfg --no-deadlock APApbft.tla
---- MODULE APApbft ----
\* PBFT model for checking with Apalache

EXTENDS pbft
EXTENDS pbft, Apalache

\* Set of replicas
MC_R == 0..3
Expand All @@ -21,4 +21,178 @@ MC_Views == 0..2
\* @type: Set(Int);
MC_Checkpoints == {2}

-------------------------

MsgsConstraintEmpty ==
/\ msgs = [
request |-> [t : Tstamps],
preprepare |-> {},
prepare |-> {},
commit |-> {},
reply |-> {},
checkpoint |-> {},
viewchange |-> {},
newview |-> {}]

MsgsConstraint ==
/\ \A r \in msgs.request :
/\ r.t \in Tstamps
/\ \A pp \in msgs.preprepare :
/\ pp.v \in Views
/\ pp.p \in R
/\ pp.n \in SeqNums
/\ pp.d \in RequestDigests
/\ \A p \in msgs.prepare :
/\ p.v \in Views
/\ p.i \in R
/\ p.n \in SeqNums
/\ p.d \in RequestDigests
/\ \A c \in msgs.commit :
/\ c.v \in Views
/\ c.i \in R
/\ c.n \in SeqNums
/\ c.d \in RequestDigests
/\ \A r \in msgs.reply :
/\ r.v \in Views
/\ r.i \in R
/\ r.t \in Tstamps
/\ r.r \in Results
/\ \A c \in msgs.checkpoint :
/\ c.n \in SeqNums
/\ c.d \in StateDigests
/\ c.i \in R
/\ \A v \in msgs.viewchange :
/\ v.v \in Views
/\ v.i \in R
/\ v.n \in SeqNums \union {0}
/\ \A c \in v.c : \* SUBSET CheckpointMessages
/\ c.n \in SeqNums
/\ c.d \in StateDigests
/\ c.i \in R
/\ \A p \in v.p : \* SUBSET PrepareProof
/\ p.preprepare.v \in Views
/\ p.preprepare.p \in R
/\ p.preprepare.n \in SeqNums
/\ p.preprepare.d \in RequestDigests
/\ \A p1 \in p.prepare : \* SUBSET PrepareMessages
/\ p1.v \in Views
/\ p1.i \in R
/\ p1.n \in SeqNums
/\ p1.d \in RequestDigests
/\ \A n \in msgs.newview :
/\ n.v \in Views
/\ n.p \in R
/\ \A v \in n.vc : \* SUBSET ViewChangeMessages
/\ v.v \in Views
/\ v.i \in R
/\ v.n \in SeqNums
/\ \A c \in v.c : \* SUBSET CheckpointMessages
/\ c.n \in SeqNums
/\ c.d \in StateDigests
/\ c.i \in R
/\ \A p \in v.p : \* SUBSET PrepareProof
/\ p.preprepare.v \in Views
/\ p.preprepare.p \in R
/\ p.preprepare.n \in SeqNums
/\ p.preprepare.d \in RequestDigests
/\ \A p1 \in p.prepare : \* SUBSET PrepareMessages
/\ p1.v \in Views
/\ p1.i \in R
/\ p1.n \in SeqNums
/\ p1.d \in RequestDigests
/\ \A pp \in n.o : \* SUBEST PrePrepareMessages
/\ pp.v \in Views
/\ pp.p \in R
/\ pp.n \in SeqNums
/\ pp.d \in RequestDigests

\* THEOREM msgs \in Messages => MsgsConstraint
\* BY DEF Messages, MsgsConstraint, NewViewMessages, PrepareProof, PrepareMessages, ViewChangeMessages, CheckpointMessages, PrePrepareMessages, CommitMessages, ReplyMessages, RequestMessages

MlogsConstraintEmpty ==
/\ mlogs = [r \in R |-> [
request |-> {},
preprepare |-> {},
prepare |-> {},
commit |-> {},
reply |-> {},
checkpoint |-> {},
viewchange |-> {}]
]

MlogsConstraint ==
/\ \A rr \in DOMAIN mlogs :
/\ \A r \in mlogs[rr].request :
/\ r.t \in Tstamps
/\ \A pp \in mlogs[rr].preprepare :
/\ pp.v \in Views
/\ pp.p \in R
/\ pp.n \in SeqNums
/\ pp.d \in RequestDigests
/\ \A p \in mlogs[rr].prepare :
/\ p.v \in Views
/\ p.i \in R
/\ p.n \in SeqNums
/\ p.d \in RequestDigests
/\ \A c \in mlogs[rr].commit :
/\ c.v \in Views
/\ c.i \in R
/\ c.n \in SeqNums
/\ c.d \in RequestDigests
/\ \A r \in mlogs[rr].reply :
/\ r.v \in Views
/\ r.i \in R
/\ r.t \in Tstamps
/\ r.r \in Results
/\ \A c \in mlogs[rr].checkpoint :
/\ c.n \in SeqNums
/\ c.d \in StateDigests
/\ c.i \in R
/\ \A v \in mlogs[rr].viewchange :
/\ v.v \in Views
/\ v.i \in R
/\ v.n \in SeqNums \union {0}
/\ \A c \in v.c : \* SUBSET CheckpointMessages
/\ c.n \in SeqNums
/\ c.d \in StateDigests
/\ c.i \in R
/\ \A p \in v.p : \* SUBSET PrepareProof
/\ p.preprepare.v \in Views
/\ p.preprepare.p \in R
/\ p.preprepare.n \in SeqNums
/\ p.preprepare.d \in RequestDigests
/\ \A p1 \in p.prepare : \* SUBSET PrepareMessages
/\ p1.v \in Views
/\ p1.i \in R
/\ p1.n \in SeqNums
/\ p1.d \in RequestDigests

GenInit ==
/\ msgs = Gen(10)
/\ mlogs = Gen(10)
/\ views = Gen(10)
/\ states = Gen(10)
/\ sCheckpoint = Gen(10)
/\ vChange = Gen(10)

\* Apalache's documentation advises to conjoin TypeOK to GenInit to further constraint
\* the values generated by Gen. This is necessary because Gen generates values that
\* satisfy Apalache's type system, but not necessarily the spec's TypeOK predicate.
\* /\ TypeOK
\* Unfortunately, Apalache explodes when it encounters the spec's TypeOK predicate
\* because of multiple levels of nested subsets. Therefore, we inline and partially
\* rewrite the definition of TypeOK into the following abomination.
/\ MsgsConstraint
/\ MlogsConstraint
\* TypeOK!3 to TypeOK!6 are inlined from the original TypeOK predicate
\* (! not supported by Apalache).
/\ views \in [R -> Views]
/\ states \in [R -> States]
/\ sCheckpoint \in [R -> SUBSET CheckpointMessages]