Commit eb19a60c authored by William Mansky's avatar William Mansky

Progress on read proof.

parent d46f304e
......@@ -481,7 +481,7 @@ Proof.
( s, GPS_iSP_Reader (kvgroupN n) (ptrP n γv γm' γv' γs') (ptrP n γv γm' γv' γs' false)
(n >> data >> Z.of_nat j) ti1 s #li γi)))
v', (v1 v' - 1)%nat
( tv ts' ss', ts1 ts' ss1 ss'⌝
( tv ts' ss', ts1 ts' ss1 ss'⌝
GPS_iSP_Reader (kvgroupN n) (gversionP n γm γs)
(gversionP n γm γs false) (n >> version) tv
((v' - 1)%nat, (ts',ss')) #(v' - 1)%nat γv)
......@@ -490,7 +490,7 @@ Proof.
ti1 ti2 li si vi γj, ⌜γs !! j = Some γj
let '(γi, (γm', γv', γs')) := γj in
GPS_iSP_Reader (kvgroupN n) (ptrP n γv γm' γv' γs') (ptrP n γv γm' γv' γs' false)
(n >> 1 >> i) ti1 si #(LitLoc li) γi
(n >> 1 >> j) ti1 si #(LitLoc li) γi
kvnode_prots_R (gdataP n γv) (kvgroupN n) γm' γv' γs' li ti2 (map_nth j GL []) vi))%I.
iApply (wp_for_simple _ _ 0 "i" Nd with "[] [out]"); [done|..].
{ (* loop invariant maintained *)
......@@ -499,8 +499,9 @@ Proof.
iDestruct "Hφ" as (vals0) "(EqL & Hout & Hrest & H)".
iDestruct "EqL" as %EqL.
iDestruct "H" as (v') "(LE' & #kV' & Hvals)".
iDestruct "LE'" as %Lev'. iDestruct "kV'" as (tv' ts' ss' [Let' Les']) "kv'".
iDestruct "LE'" as %Lev'.
wp_let. wp_op. wp_op.
iDestruct "kV'" as (tv' ts' ss' [Let' Les']) "kv'".
(* look up ith kvnode *)
wp_bind (!ᵃᶜ_)%E.
destruct (8 - Z.to_nat i)%nat as [|ri] eqn: Hi.
......@@ -513,7 +514,7 @@ Proof.
[solve_ndisj|done|done|by right
|..].
{ iIntros (????) "!> !>". iSplit. by iIntros "#$". iSplit; by iIntros "#$". }
iIntros (?? p) "!> (% & Ri & KVi)". wp_let.
iIntros (t' s' p) "!> (% & Ri & KVi)". wp_let.
iDestruct "KVi" as (ni ? (?, ?)) "[% KVi]"; subst p.
(* reading *)
iDestruct (gdataObs_get_1 n GL1 γs γv (Z.to_nat i) with "DO'")
......@@ -523,7 +524,6 @@ Proof.
rewrite H in Hγi; inversion Hγi; subst γi'.
iDestruct "Hdi" as "[_ Hdi]".
wp_op. wp_op.
(* There's a later in read_spec that isn't in the single-location protocols. This is inconvenient when read is the last operation in the loop. *)
iApply (read_spec (gdataP n γv) (kvgroupN n) _ _ _ _ _ _ _ _ _ (fun t s v => gdataP n γv false γm' t s v)%I (fun t s v => gdataP n γv false γm' t s v)%I
with "[outi $KVi]"); try done. (* We have two kvprot snapshots here: one from the pointer, and one from the previous read.
The previous read may be from a different location, but might also have a more up-to-date log. Do we need to reconcile them? *)
......@@ -533,46 +533,49 @@ Proof.
iSplitR ""; auto.
iIntros "!>" (????).
by iSplit; iIntros "? !>"; unfold gdataP; rewrite <- bi.persistent_sep_dup; try typeclasses eauto. }
iIntros "!>" (ti' si' vi' vals') "(Exti & out & #kvi & HdP)". (* up to here *)
iDestruct "Exti" as %[Extvi ?].
iDestruct "HdP" as (zi veri) "[Eqi #kVeri]".
iDestruct "Eqi" as %[? Lli]. subst vi'. destruct LL1 as [vs1 Ll1].
have Lei: (v1 veri)%nat. { eapply log_latest_ord;
by [apply Extvi|apply fmap_nth_log_latest|apply Lli]. }
iDestruct "kVeri" as (tvi [tsi ssi]) "kVeri".
iAssert (|={E}=> (v' - 1)%nat (veri - 1)%nat ts' tsi ss' ssi
(veri - 1)%nat (v' - 1)%nat tsi ts' ssi ss'⌝)%I
as ">Case".
{ iMod (GPS_iSP_Readers_agree _ (versionP n γm γs) with "kv' [$kVeri]")
as "Le"; [done|by iDestruct "kv'" as "[? $]"|].
iClear "#". iIntros "!>".
iDestruct "Le" as "[[? _]|[? _]]"; [by iLeft|by iRight]. }
iDestruct "Case" as %Case.
(* writing *)
iDestruct "Hi" as (vw) "Hi". wp_write. clear vw.
iIntros "!>" (ti' si' vi' vals') "(Exti & out & #kvi & HdP)".
(* re-establish loop invariant *)
iApply "Post".
iSplit; first by iPureIntro; lia.
iExists (vals0 ++ [zi]). iSplit.
iExists (vals0 ++ [vals']). iSplit.
{ iPureIntro. rewrite app_length EqL /=. lia. }
rewrite big_sepL_app. iSplitL "Hout Hi".
{ iClear "#". iFrame "Hout". rewrite /= Nat.add_0_r -EqL. by iFrame "Hi". }
rewrite big_sepL_app. iSplitL "Hout out".
{ iClear "#". iFrame "Hout". rewrite /= Nat.add_0_r -EqL.
iSplit; last done.
iApply (big_sepL_mono with "out"); intros; simpl.
by rewrite shift_lblock_assoc Z.mul_comm. }
iSplitL "Hrest".
{ iClear "#".
rewrite (_: seq (Z.to_nat (i + 1)) (8 - Z.to_nat (i + 1))
= seq (S (Z.to_nat i)) ri); [by iFrame|f_equal].
= seq (S (Z.to_nat i)) ri); [|f_equal].
- iApply (big_sepL_mono with "Hrest"); intros; simpl.
by rewrite shift_lblock_assoc Z.mul_comm.
- rewrite Z2Nat.inj_succ; [done|lia].
- rewrite (_ : (ri = S ri - 1)%nat); last lia.
rewrite -Hi Z2Nat.inj_add; [|lia..]. by rewrite Nat.sub_add_distr. }
iDestruct "Exti" as %[? Extvi].
iDestruct "HdP" as (veri) "#HdP".
(* The SWReader is trapped under a later here. *)
iExists (Nat.max v' veri). iSplit.
{ iPureIntro. rewrite -Nat.sub_max_distr_r.
etrans; [apply Lev'|apply Nat.le_max_l]. } iSplitL "".
{ destruct Case as [(?&?&?)|(?&?&?)]; iExists _, _, _;
{ iNext. iDestruct "HdP" as "[Eqi #kVeri]".
iDestruct "Eqi" as %Lli. destruct LL1 as [vs1 Ll1].
iDestruct "kVeri" as (tvi [tsi ssi]) "kVeri".
iAssert (|={E}=> (v' - 1)%nat (veri - 1)%nat ts' tsi ss' ssi
(veri - 1)%nat (v' - 1)%nat tsi ts' ssi ss'⌝)%I
as ">Case".
{ iMod (GPS_iSP_Readers_agree _ (versionP n γm γs) with "kv' [$kVeri]")
as "Le"; [done|by iDestruct "kv'" as "[? $]"|].
iClear "#". iIntros "!>".
iDestruct "Le" as "[[? _]|[? _]]"; [by iLeft|by iRight]. }
iDestruct "Case" as %Case.
destruct Case as [(?&?&?)|(?&?&?)]; iExists _, _, _;
rewrite -Nat.sub_max_distr_r.
- rewrite Nat.max_r; [iFrame "kVeri"|done]. iDestruct "kv'" as "[_ $]".
iPureIntro. split; by etrans.
- rewrite Nat.max_l; [iFrame "kv'"|done].
iPureIntro. split; by etrans. }
iPureIntro. split; by etrans.*) admit. }
rewrite big_sepL_app. iSplitL "Hvals".
{ iApply (big_sepL_mono with "Hvals"). simpl.
iIntros (j dj Eqj). iDestruct 1 as (Lj vj) "[Eqj HRj]".
......@@ -581,10 +584,11 @@ Proof.
etrans; [apply Le2|apply Nat.le_max_l]. }
simpl. iSplitR ""; [|done].
iExists si', veri. iSplit.
{ iPureIntro. split; split; auto. apply Nat.le_max_r.
rewrite Nat.add_0_r. move : Extvi. by rewrite EqL Nat2Z.id. }
iExists ti', #zi, γi. rewrite Nat.add_0_r. iSplit; last by rewrite EqL.
iPureIntro. move : Hγi. by rewrite EqL Nat2Z.id.
{ (*iPureIntro. split; split; auto. apply Nat.le_max_r.
rewrite Nat.add_0_r. move : Extvi. by rewrite EqL Nat2Z.id.*) admit. }
iExists t', ti', ni, s', (vi', vals'), (γi, (γm', γv', γs')). rewrite Nat.add_0_r. iSplit; last (* by *) rewrite EqL.
iPureIntro. move : H. by rewrite EqL Nat2Z.id.
admit.
(* done with loop invariant *) }
{ (* first iteration condition *)
iSplit; first by (iPureIntro; lia).
......
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