From 9fde2cfd8e8e2a2a2faf4a3ba2e9d96c886c153f Mon Sep 17 00:00:00 2001
From: William Mansky <mansky1@uic.edu>
Date: Mon, 28 Jan 2019 09:14:07 -0600
Subject: [PATCH] Protocol history should allow earlier operations in actual
 history.

---
 theories/examples/kvnode2.v | 32 +++++++++++++++++++++++---------
 1 file changed, 23 insertions(+), 9 deletions(-)

diff --git a/theories/examples/kvnode2.v b/theories/examples/kvnode2.v
index d8ac2896..df0b36ec 100644
--- a/theories/examples/kvnode2.v
+++ b/theories/examples/kvnode2.v
@@ -738,9 +738,12 @@ Notation kvnode_state_type Prtcl := (gset (kvnode_state_sort Prtcl)).
 
 Context `{PF : !protocol_facts Prtcl} `{GPSG : !gpsG(A := kvtype) Σ Prtcl PF} `(IP : gname -> kvnode_interpC Σ Prtcl).
 
+Definition earlier_hist (h h' : History) :=
+  ∃l, h' = of_list l ∧ Forall2 (fun '(d, V) '(d', V') => d' = d ∧ V ⊑ V') (elements h) l.
+
 Definition kvnode_Hist (n : loc) (h : gset (kvtype * View)) :=
-  (Hist (ZplusPos version n) (map_gset (fun '(d, V) => (VInj (Z.of_nat (fst d)), V)) h) ∗
-   [∗ list] i ∈ seq 0 8, Hist (ZplusPos (Z.of_nat i) (ZplusPos data n)) (map_gset (fun '(d, V) => (VInj (kvget i d), V)) h))%I.
+  ((∃ h', ⌜earlier_hist h' (map_gset (fun '(d, V) => (VInj (Z.of_nat (fst d)), V)) h)⌝ ∗ Hist (ZplusPos version n) h') ∗
+   [∗ list] i ∈ seq 0 8, ∃ h', ⌜earlier_hist h' (map_gset (fun '(d, V) => (VInj (kvget (Z.of_nat i) d), V)) h)⌝ ∗ Hist (ZplusPos (Z.of_nat i) (ZplusPos data n)) h')%I.
 
 Definition kvnode_list (d : kvtype) :=
   let '(_, (a, b, c, d, e, f, g, h)) := d in a :: b :: c :: d :: e :: f :: g :: h :: nil.
@@ -759,7 +762,7 @@ Definition kvnode_list (d : kvtype) :=
        [XP (ZplusPos (Z.of_nat i) (ZplusPos data n)) in map_nth i L 0 | dataP n g]_W)%I.
 
 Definition kvnode_IP γ γ' b n  ζ (e_x : kvtype) :=
-  (IP γ b n  ζ e_x ∗ if b then kvnode_prots_W γ' n (fst e_x) (kvnode_list e_x) else kvnode_prots_R γ' n (fst e_x) (kvnode_list e_x))%I.
+  (IP γ b n ζ e_x ∗ if b then kvnode_prots_W γ' n (fst e_x) (kvnode_list e_x) else kvnode_prots_R γ' n (fst e_x) (kvnode_list e_x))%I.
 
 Definition kvnode_inv n γ γ_x γ' : iProp Σ
       := (∃ ζ h e_x, own.own γ (● (● ζ ⋅ ◯ ζ))
@@ -768,6 +771,10 @@ Definition kvnode_inv n γ γ_x γ' : iProp Σ
                          ∗ (*⌜init n h⌝ ∗*) ⌜SortInv n ζ⌝ ∗ ⌜e_x ∈ ζ⌝
                          ∗ ⌜Consistent ζ h⌝ ∗ ⌜FinalInv n e_x ζ⌝ ∗ ⌜StateInjection ζ⌝)%I.
 
+(*  (* middleware approach *)
+  Program Definition kvnode_inv_vProp n γ γ_x γ' : vProp Σ := MonPred (fun _ => kvnode_inv n γ γ_x γ') _.
+(*  Next Obligation. rewrite /gps_inv. solve_proper. Qed.*)*)
+
   Definition kvnodeSWnRaw γ l n : iProp Σ :=
     (∃ (γ_x: gname) γ',
       ⌜n = encode (γ,γ_x,γ')⌝ ∗ kvnode_inv l γ γ_x γ')%I.
@@ -776,9 +783,9 @@ Definition kvnode_inv n γ γ_x γ' : iProp Σ
     (∃ (γ_x: gname) (γ': gname),
       ⌜n = encode (γ,γ_x,γ')⌝ ∗ WAEx(A := kvtype)(GPSG := GPSG) l γ γ_x s)%I.
 
-Program Definition kvnode_nWSP_def γ l s : vProp Σ :=
-  MonPred (λ V, persisted l (kvnodeSWnRaw γ) (λ l X, kvnodeWriterSWnRaw γ s l X V)) _.
-Next Obligation. solve_proper. Qed.
+  Program Definition kvnode_nWSP_def γ l s : vProp Σ :=
+    MonPred (λ V, persisted l (kvnodeSWnRaw γ) (λ l X, kvnodeWriterSWnRaw γ s l X V)) _.
+  Next Obligation. solve_proper. Qed.
 
   Notation F γ := (IP γ true).
   Notation F_past γ := (IP γ false).
@@ -792,15 +799,22 @@ Next Obligation. solve_proper. Qed.
       ∗ P ∗ kvnode_nWSP_def γ n s }}} write #n #ain
     {{{ RET #(); Q γ s' }}}.
   Proof.
-    iIntros (Φ) "(#ctx & in & Hshift & P & prot) Hpost".
+    iStartProof (iProp Σ).
+    iIntros (Φ V) "(#ctx & in & Hshift & P & prot)".
+    unseal.
+    rewrite monPred_wand_eq /=.
+    iIntros (V' ?) "Hpost".
+    iIntros (V'' ? π) "seen".
 
     unfold write.
     unfold of_val.
-    wp_rec'. wp_rec'.
+    wp_rec. wp_rec'.
     match goal with |-context[App (Rec _ ?b ?e) _] => assert (Closed (b :b: nil) e) as Hclosed by apply I end.
     wp_op.
     wp_bind ([_]_at)%E; clear Hclosed.
-    iMod (persistor_open with "prot").
+
+
+    iMod (persistor_open with "[$prot]").
 
 (*    iDestruct "node_state" as "(% & kV & oL & data)".
     iApply (GPS_SW_Read_ex (versionP n g) with "[$kI $kV]");
-- 
GitLab