Prove abs type-correct.

Signed-off-by: Markus Alexander Kuppe <[email protected]>
microsoft · Oct 28, 2024 · ccece6d · ccece6d
1 parent 6f7048b
commit ccece6d
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 1 deletion.
diff --git 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
@@ -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
+
+======