Commit 9fde2cfd authored by William Mansky's avatar William Mansky

Protocol history should allow earlier operations in actual history.

parent ed763e68
Pipeline #14180 passed with stage
in 16 minutes and 52 seconds
......@@ -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]");
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment