From b545678f2e420b808b3bdf340c7ad057ddfcb163 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe <github.com@lemmster.de> Date: Mon, 28 Oct 2024 10:51:41 -0700 Subject: [PATCH] Prove abs type-correct. Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de> --- tla/consensus/abs.tla | 3 ++- tla/consensus/abs_proof.tla | 10 ++++++++++ 2 files changed, 12 insertions(+), 1 deletion(-) create mode 100644 tla/consensus/abs_proof.tla diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla index f76a14891666..840e6fae8419 100644 --- a/tla/consensus/abs.tla +++ b/tla/consensus/abs.tla @@ -13,7 +13,8 @@ ASSUME /\ IsStrictlyTotallyOrderedUnder(<, Terms) /\ \E min \in Terms : \A t \in Terms : t <= min CONSTANT StartTerm -ASSUME /\ StartTerm \in Terms +ASSUME StartTermIsTerm == + /\ StartTerm \in Terms /\ \A t \in Terms : StartTerm <= t \* Commit logs from each node diff --git a/tla/consensus/abs_proof.tla b/tla/consensus/abs_proof.tla new file mode 100644 index 000000000000..520bbed8e82c --- /dev/null +++ b/tla/consensus/abs_proof.tla @@ -0,0 +1,10 @@ +---- MODULE abs_proof ---- +EXTENDS abs, TLAPS + +LEMMA Spec => TypeOK +<1> USE DEF TypeOK +<1>1. Init => TypeOK BY StartTermIsTerm DEF Init, InitialLogs +<1>2. TypeOK /\ [Next]_cLogs => TypeOK' BY DEF Next, Extend, Copy, CopyMaxAndExtend +<1>. QED BY <1>1, <1>2, PTL DEF Spec + +====== \ No newline at end of file