v31 (RefinementFair): Prove BlockingQueueFair implements BlockingQueu…

…eSplit.
lemmy · Dec 14, 2020 · 0761ecf · 0761ecf
1 parent e9cf852
commit 0761ecf
Show file tree

Hide file tree

Showing 2 changed files with 86 additions and 0 deletions.
diff --git a/BlockingQueueFair.tla b/BlockingQueueFair.tla
@@ -146,4 +146,84 @@ THEOREM ITypeInv == Spec => []TypeInv
 <1>3. QED BY <1>1, <1>2, PTL DEF Spec
 
 -----------------------------------------------------------------------------
+
+LEMMA EmptySeqRange == ASSUME NEW S, NEW seq \in Seq(S)
+                       PROVE seq = <<>> <=> Range(seq) = {}
+BY Isa DEF Range
+
+LEMMA RangeTail == 
+  ASSUME NEW S, NEW ws \in Seq(S), IsInjective(ws)
+         , ws # <<>>
+  PROVE \E x \in Range(ws): Range(Tail(ws)) = Range(ws) \ {x}
+\* BY Z3 DEF Range, IsInjective \* Proof goes through with Tail
+                                \* re-defined with the CASE
+                                \* statement omitted, which is
+                                \* equivalent here due to
+                                \* 'ws # <<>>' assumption.
+
+-----------------------------------------------------------------------------
+
+(* Prove BlockingQueueFair implements BlockingQueueSplit *)
+THEOREM Spec => BQS!Spec
+<1> USE Assumption DEF Range
+<1>1. Init => BQS!Init 
+   BY DEF Init, BQS!Init
+<1>2. TypeInv /\ [Next]_vars => [BQS!Next]_BQS!vars
+  <2> SUFFICES ASSUME TypeInv,
+                      [Next]_vars
+               PROVE  [BQS!Next]_BQS!vars
+    OBVIOUS
+  <2>1. ASSUME NEW p \in Producers,
+               Put(p, p)
+        PROVE  [BQS!Next]_BQS!vars
+    <3>1. CASE /\ Len(buffer) < BufCapacity
+               /\ buffer' = Append(buffer, p)
+               /\ NotifyOther(waitSeqC)
+               /\ UNCHANGED waitSeqP
+      <4>1. CASE /\ waitSeqC = <<>>
+                 /\ UNCHANGED waitSeqC
+        BY <4>1, <2>1, <3>1, Isa 
+        DEF Put, BQS!Next, BQS!vars, BQS!Put, BQS!NotifyOther
+      <4>2. CASE /\ waitSeqC # <<>>
+                 /\ waitSeqC' = Tail(waitSeqC)
+        BY <4>2, <2>1, <3>1, EmptySeqRange, RangeTail, Isa
+        DEF TypeInv, Put, BQS!Next, BQS!vars, BQS!Put, BQS!NotifyOther
+      <4>3. QED
+        BY <3>1, <4>1, <4>2 DEF NotifyOther
+    <3>2. CASE /\ Len(buffer) = BufCapacity
+               /\ Wait(waitSeqP, p)
+               /\ UNCHANGED waitSeqC
+      BY <2>1, <3>2
+      DEF Wait, BQS!Next, BQS!vars, BQS!Put, BQS!Wait
+    <3>3. QED
+      BY <2>1, <3>1, <3>2 DEF Put
+  <2>2. ASSUME NEW c \in Consumers,
+               Get(c)
+        PROVE  [BQS!Next]_BQS!vars
+    <3>1. CASE /\ buffer # <<>>
+               /\ buffer' = Tail(buffer)
+               /\ NotifyOther(waitSeqP)
+               /\ UNCHANGED waitSeqC
+      <4>1. CASE /\ waitSeqP = <<>>
+                 /\ UNCHANGED waitSeqP
+        BY <4>1, <2>2, <3>1, Isa 
+        DEF Get, BQS!Next, BQS!vars, BQS!Get, BQS!NotifyOther
+      <4>2. CASE /\ waitSeqP # <<>>
+                 /\ waitSeqP' = Tail(waitSeqP)
+        BY <4>2, <2>2, <3>1, EmptySeqRange, RangeTail, Isa
+        DEF TypeInv, Get, BQS!Next, BQS!vars, BQS!Get, BQS!NotifyOther
+      <4>3. QED
+        BY <3>1, <4>1, <4>2 DEF NotifyOther
+    <3>2. CASE /\ buffer = <<>>
+               /\ Wait(waitSeqC, c)
+               /\ UNCHANGED waitSeqP
+      BY <2>2, <3>2 DEF Wait, BQS!Next, BQS!vars, BQS!Get, BQS!Wait
+    <3>3. QED
+      BY <2>2, <3>1, <3>2 DEF Get
+  <2>3. CASE UNCHANGED vars
+    BY <2>3 DEF vars, BQS!Next, BQS!vars
+  <2>4. QED
+    BY <2>1, <2>2, <2>3 DEF Next
+<1>3. QED BY <1>1, <1>2, ITypeInv, PTL DEF Spec, BQS!Spec
+
 =============================================================================
diff --git a/README.md b/README.md
@@ -13,6 +13,12 @@ This tutorial is work in progress. More chapters will be added in the future. In
 
 --------------------------------------------------------------------------
 
+### v31 (Refinement Fair): Prove BlockingQueueFair implements BlockingQueueSplit.
+
+A proof showing that ```BlockingQueueSplit``` implements ```BlockingQueueSplit```.   Two lemmas show that it is sometimes necessary to prove simpler facts first to prove the main theorem.
+
+Compared to the previous proofs, this one is far more involved and more realistically reflects the efforts require to write proofs; the refinement proof took approximately three weeks.  Three weeks is quite an investment considering that the correctness of the refinement seems straight forward in the first place.  However, three weeks also includes the work to detect and help with a fix for a [regression in TLAPS 1.4.4](https://github.com/tlaplus/tlapm/releases/tag/v1.4.5), identifying [two](https://github.com/tlaplus/tlaplus/issues/434) Toolbox [issues](https://github.com/tlaplus/tlaplus/issues/433), and familiarizing myself with the TLAPS [build](https://github.com/tlaplus/tlapm/blob/master/tools/installer/tlaps-release.sh.in) and [development](https://www.youtube.com/watch?v=Eu46FmhpR_0&feature=youtu.be) process.
+
 ### v30 (Refinement Fair): Prove TypeInv is an inductive invariant of BlockingQueueFair.
 
 As a first step of proving that ```BlockingQueueFair``` refines ```BlockingQueueSplit```, we once again prove inductiveness of ```TypeInv```.