From 0761ecfdb0e3aef3db1aa78df6f4aa0b60e5736d Mon Sep 17 00:00:00 2001
From: Markus Alexander Kuppe <tlaplus.net@lemmster.de>
Date: Wed, 24 Jun 2020 17:59:29 -0700
Subject: [PATCH] v31 (RefinementFair): Prove BlockingQueueFair implements
 BlockingQueueSplit.

---
 BlockingQueueFair.tla | 80 +++++++++++++++++++++++++++++++++++++++++++
 README.md             |  6 ++++
 2 files changed, 86 insertions(+)

diff --git a/BlockingQueueFair.tla b/BlockingQueueFair.tla
index 2805cf4..4c6fc6e 100644
--- 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
index 7413979..bdde739 100644
--- 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```.