From a27c9df0930884bf7aaed02a29de6a34415a54c4 Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@mpi-sws.org>
Date: Fri, 11 Aug 2017 16:07:27 +0200
Subject: [PATCH] Make TIDs pure ghosts; inst. Iris with (exp, View).
---
coq/ra/adequacy.v | 22 +-
coq/ra/base/accessors.v | 110 ++++--
coq/ra/base/alloc.v | 173 +++++----
coq/ra/base/at_cas.v | 65 ++--
coq/ra/base/at_fai.v | 48 +--
coq/ra/base/at_read.v | 33 +-
coq/ra/base/at_shared.v | 4 +-
coq/ra/base/at_write.v | 37 +-
coq/ra/base/dealloc.v | 34 +-
coq/ra/base/fork.v | 31 +-
coq/ra/base/ghosts.v | 21 +-
coq/ra/base/helpers.v | 20 +-
coq/ra/base/na_read.v | 67 ++--
coq/ra/base/na_shared.v | 4 +-
coq/ra/base/na_write.v | 53 ++-
coq/ra/examples/message_passing.v | 6 +-
coq/ra/examples/message_passing_base.v | 52 +--
coq/ra/examples/repeat.v | 6 +-
coq/ra/gps/cas.v | 8 +-
coq/ra/gps/fai.v | 4 +-
coq/ra/gps/init.v | 8 +-
coq/ra/gps/read.v | 8 +-
coq/ra/gps/write.v | 12 +-
coq/ra/lang.v | 36 +-
coq/ra/lifting.v | 507 ++++++++++++-------------
coq/ra/machine.v | 126 +++---
coq/ra/rsl.v | 28 +-
coq/ra/tactics.v | 2 +-
coq/ra/tests/message_passing.v | 11 +-
coq/ra/types.v | 2 +-
coq/ra/weakestpre.v | 122 +++---
31 files changed, 791 insertions(+), 869 deletions(-)
diff --git a/coq/ra/adequacy.v b/coq/ra/adequacy.v
index 632bf2c2..b1d2c547 100644
--- a/coq/ra/adequacy.v
+++ b/coq/ra/adequacy.v
@@ -20,7 +20,7 @@ Definition baseΣ : gFunctors := #[ownPΣ (language.state ra_lang);
Instance subG_basePreG {Σ} : subG baseΣ Σ → basePreG Σ.
Proof. solve_inG. Qed.
-Definition to_view (σ : language.state ra_lang) : Views := (Excl <$> threads σ).
+(* Definition to_view (σ : language.state ra_lang) : Views := (Excl <$> threads σ). *)
Definition loc_sets (σ : language.state ra_lang) : gmap loc (gset message) :=
let locs := {[ mloc m | m <- msgs (mem σ) ]} in
map_imap (λ l _, Some {[ m <- msgs (mem σ) | mloc m = l ]}) (to_gmap () locs).
@@ -180,17 +180,19 @@ Qed.
Definition base_adequacy Σ `{!basePreG Σ} e V σ φ :
phys_inv σ ->
- threads σ !! e.2 = Some V →
- (∀ `{!foundationG Σ}, PSCtx ∗ Seen (e.2) V ⊢ WP e {{ v, ⌜φ v⌝ }}) →
+ view_ok (mem σ) V ->
+ (∀ `{!foundationG Σ} π, PSCtx ∗ Seen π V ⊢ WP e {{ v, ⌜φ v⌝ }}) →
adequate e σ φ.
Proof.
- intros Inv View Hwp; eapply (ownP_adequacy _ _). iIntros (?).
- iMod (own_alloc (● to_view σ ⋅ ◯ to_view σ)) as (γV) "HV".
+ intros Inv VOk Hwp; eapply (ownP_adequacy _ _). iIntros (?).
+ iMod (own_alloc (● {[1%positive := Excl V]} ⋅ ◯ {[1%positive:=Excl V]})) as (γV) "HV".
{ rewrite auth_valid_discrete /=. split.
- exists ∅. intros ?. rewrite !gmap.lookup_op lookup_empty.
by case: (_ !! _).
- - move => ?. rewrite lookup_fmap.
- case: (_ !! _) => [?|//] /=. by constructor. }
+ - move => ?.
+ case H: (_ !! _) => [?|//] /=.
+ move: H. rewrite lookup_singleton_Some => [] [_ <-] //.
+ }
iMod (own_alloc (● to_hist σ ⋅ ◯ to_hist σ)) as (γH) "HH".
{ rewrite auth_valid_discrete /=. split.
- exists ∅. intros ?. rewrite !gmap.lookup_op lookup_empty.
@@ -210,10 +212,7 @@ Proof.
(* iModIntro. iExists (λ σ, own γV (to_view σ) ∗ own γH (to_hist σ) ∗ own γI (to_info σ))%I; iFrame. *)
set (HBase := FoundationG Σ _ _ _ _ γV γH γI).
iMod (inv_alloc physN top PSInv with "[- HV']"); last first.
- { iApply (Hwp (HBase)). iFrame.
- rewrite (gmap_bigop (to_view σ)) auth_big_op own_big_op.
- rewrite big_opM_delete; first by iDestruct "HV'" as "[$ ?]".
- by rewrite /to_view lookup_fmap View. }
+ { iApply (Hwp (HBase)). by iFrame. }
iNext. rewrite /PSInv. iExists _, _, _, _. iFrame (Inv) "∗".
repeat iSplit; auto.
- rewrite /DInv.
@@ -231,6 +230,7 @@ Proof.
+ iIntros (? ?). iFrame. iExists _. iFrame.
+ iDestruct (own_valid with "A") as "%".
move: (H0 a) => /=. by rewrite lookup_singleton.
+ - iPureIntro => ? ?. by rewrite lookup_singleton_Some => [] [_ [<-] //].
- by rewrite to_hist_dom.
- iPureIntro. intros ? ?. rewrite /to_hist.
rewrite !lookup_fmap. move/fmap_Some => [?] [].
diff --git a/coq/ra/base/accessors.v b/coq/ra/base/accessors.v
index 0d7ab523..49b349ad 100644
--- a/coq/ra/base/accessors.v
+++ b/coq/ra/base/accessors.v
@@ -45,46 +45,77 @@ Section Accessors.
∃ ς HIST INFO,
▷ ownP ς
∗ ⌜phys_inv ς⌝
- ∗ ⌜Some V = threads ς !! π⌝
+ ∗ ⌜view_ok (mem ς) V⌝
∗ ⌜HInv ς HIST⌝
∗ ⌜IInv ς INFO⌝
∗ own IN (● INFO)
- ∗ own HN (● HIST)
- ∗ ∀ l v ς' V',
+ (* ∗ own HN (● HIST) *)
+ ∗ ∀ l v ς' V' t,
(ownP ς'
∗ ⌜phys_inv ς'⌝
∗ ⌜rel_inv ς ς'⌝
- ∗ ⌜threads ς' !! π = Some V'⌝
- ∗ ⌜VInv ς' (<[π := Excl V']> (Excl <$> threads ς))⌝
- ∗ ⌜HInv ς' (<[l := Excl {[A,V']}]> HIST)⌝
+ ∗ ⌜view_ok (mem ς') V'⌝
+ ∗ ⌜HIST !! l = None⌝
+ ∗ ⌜msgs (mem ς') ≡ msgs (mem ς) ∪ {[<l → A @ t, (V ⊔ {[l := t]}) >]}⌝
+ ∗ ⌜nats ς' ≡ <[l := t]>(nats ς)⌝
+ ∗ ⌜LInv ς' l {[A, V']}⌝
+ (* ∗ ⌜HInv ς' (<[l := Excl {[A,V']}]> HIST)⌝ *)
∗ ⌜IInv ς' (<[l := (1%Qp, v)]> INFO)⌝
- ∗ (DInv HIST -∗ DInv (<[l := Excl {[(A,V')]}]> HIST))
+ (* ∗ (DInv HIST -∗ DInv (<[l := Excl {[(A,V')]}]> HIST)) *)
∗ own IN (● (<[l := (1%Qp, v)]> INFO) ⋅ ◯ {[l := (1%Qp, v)]})
- ∗ own HN (● (<[l := Excl {[A,V']}]> HIST) ⋅ ◯ {[l := Excl {[A,V']}]}))
+ (* ∗ own HN (● (<[l := Excl {[A,V']}]> HIST) ⋅ ◯ {[l := Excl {[A,V']}]}) *)
+ )
={E∖↑physN,E}=∗ Seen π V' ∗ Hist l {[(A,V')]} ∗ Info l 1 v.
Proof.
iIntros (?) "[#HInv >FV]".
iInv physN as (ς VIEW HIST INFO)
- "[HoP [>AV [>AH [>AI [>% [DInv [>% [>% >%]]]]]]]]"
+ "(HoP & >AV & >AH & >AI & >% & DInv & >% & >% & >%)"
"HClose".
iCombine "AV" "FV" as "HV".
iDestruct (own_valid with "HV") as %?%Views_frag_valid_le.
iModIntro.
- iExists ς, HIST, INFO. iFrame "HoP AH AI".
+ iExists ς, HIST, INFO. iFrame "HoP AI".
repeat (iSplitL ""; first auto).
- { iPureIntro. move: H1 H5 => <-. rewrite lookup_fmap.
- case: (threads _ !! _) => // [?] [->] //. }
- iIntros (l v ς' V')
- "[HoP' [% [% [% [% [% [% [DVs [[AI FI] [AH FH]]]]]]]]]]".
- iFrame "FI FH".
+ { iPureIntro. exact: (H1 _ _ H5). }
+ iIntros (l v ς' V' t)
+ "(HoP' & % & % & % & % & % & % & % & DVs & [AI FI])".
+ iFrame "FI".
iMod (Views_update_override with "[$HV]") as "[HV1 FV']".
- iFrame "FV'". iApply "HClose". iNext.
- iDestruct ("DVs" with "DInv") as "DInv".
+ iFrame "FV'".
+ iMod ((Hists_alloc _ _ {[A,V']}) with "AH") as "[AH $]"; first eauto.
+ iApply "HClose". iNext.
+ (* iDestruct ("DVs" with "DInv") as "DInv". *)
iExists _,_,_,_. iFrame. repeat (iSplit; auto).
- by rewrite H1 in H8.
+ - rewrite /DInv. rewrite big_op.big_opM_insert => //. iFrame.
+ iIntros (?) "%". exfalso. specialize (H12 (A,V')). by set_solver+H12.
+ - iPureIntro => ? ?.
+ rewrite lookup_insert_Some => [] [[_ [<- //]]|[_ /H1]].
+ apply: view_ok_mono => //. by apply H6.
+ - iPureIntro. rewrite dom_insert. rewrite (proj1 (H2)) /locs H9.
+ rewrite -> (comm (∪)). by rewrite gset_map_union gset_map_singleton.
+ - iPureIntro => l' ?.
+ rewrite lookup_insert_Some => [] [[<- [<- //]]|[NEq /(proj2 H2)]].
+ intros ([v'' V''] & In & ? & ? & ? & ?).
+ eexists; split; first eassumption.
+ split; [|split; [|split]]; try auto.
+ + rewrite -H13.
+ case C: (nats ς' !! _); [|];
+ move: C (H10 l') => -> C;
+ symmetry in C;
+ (rewrite lookup_insert_ne in C; last by auto);
+ apply leibniz_equiv in C;
+ by rewrite C.
+ + rewrite H14. f_equiv.
+ rewrite /hist_from_opt.
+ move => ?.
+ rewrite !elem_of_filter H9.
+ split; intros (? & Eq & ?); (split; [|split]; try done).
+ * rewrite elem_of_union; by left.
+ * move: H17 NEq. rewrite elem_of_union ?elem_of_singleton => [] [//|].
+ by rewrite <- Eq => [] ->.
Qed.
Lemma PSInv_open_VH E π V l h :
@@ -92,7 +123,7 @@ Section Accessors.
PSCtx ∗ ▷ Seen π V ∗ ▷ Hist l h ={E,E∖↑physN}=∗
∃ ς HIST,
▷ ownP ς ∗ ⌜phys_inv ς⌝
- ∗ ⌜Some V = threads ς !! π⌝
+ ∗ ⌜view_ok (mem ς) V⌝
∗ ⌜Some $ Excl h = HIST !! l⌝
∗ ▷ DInv HIST
∗ ⌜HInv ς HIST⌝
@@ -100,15 +131,14 @@ Section Accessors.
ownP ς'
∗ ⌜phys_inv ς'⌝
∗ ⌜rel_inv ς ς'⌝
- ∗ ⌜threads ς' !! π = Some V'⌝
∗ ▷ DInv (<[l := Excl h']> HIST)
- ∗ ⌜VInv ς' (<[π := Excl V']> (Excl <$> threads ς))⌝
+ ∗ ⌜view_ok (mem ς') V'⌝
∗ ⌜HInv ς' (<[l := Excl h']> HIST)⌝
={E∖↑physN,E}=∗ Seen π V' ∗ Hist l h'.
Proof.
- iIntros (?) "[#HInv [>FV >FH]]".
+ iIntros (?) "(#HInv & >FV & >FH)".
iInv physN as (ς VIEW HIST INFO)
- "[HoP [>AV [>AH [>AI [>% [DInv [>% [>% >%]]]]]]]]" "HClose".
+ "(HoP & >AV & >AH & >AI & >% & DInv & >% & >% & >%)" "HClose".
iCombine "AV" "FV" as "HV".
iCombine "AH" "FH" as "HH".
iDestruct (own_valid with "HV") as %?%Views_frag_valid_le.
@@ -116,17 +146,18 @@ Section Accessors.
iModIntro.
iExists ς, HIST. iFrame "HoP DInv". repeat (iSplit; auto).
- { iPureIntro. move: H1 H5 => <-. rewrite lookup_fmap.
- case: (threads _ !! _) => // [?] [->] //. }
- iIntros (ς' V' h') "[HoP' [% [% [% [DInv' [% %]]]]]]".
+ { iPureIntro. by apply: H1. }
+ iIntros (ς' V' h') "(HoP' & % & % & DInv' & % & %)".
iMod (Views_update_override with "[$HV]") as "[HV1 FV']".
iFrame "FV'".
iMod (Hists_update_override with "[$HH]") as "[HH1 HH2]".
iFrame "HH2".
iApply "HClose".
iNext. iExists _, _, _ ,_.
- rewrite -H1. iFrame (H4 H9 H10) "∗".
- iPureIntro. by apply (IInv_update_addins ς _ HIST _ l h h').
+ iFrame (H4 H9) "∗". iPureIntro.
+ split; last by apply (IInv_update_addins ς _ HIST _ l h h').
+ move => ? ?. rewrite lookup_insert_Some => [] [[_ [<- //]]|[_ /H1]].
+ apply: view_ok_mono => //. by apply H7.
Qed.
Lemma PSInv_open_V E π V l h :
@@ -134,8 +165,8 @@ Section Accessors.
PSCtx ∗ ▷ Seen π V ∗ ▷ Hist l h ={E,E∖↑physN}=∗
∃ ς HIST,
▷ ownP ς ∗ ⌜phys_inv ς⌝
- ∗ ⌜Some V = threads ς !! π⌝
∗ ⌜Some $ Excl h = HIST !! l⌝
+ ∗ ⌜view_ok (mem ς) V⌝
∗ ▷ DInv HIST
∗ ⌜HInv ς HIST⌝
∗ ∀ ς' V' h',
@@ -143,38 +174,35 @@ Section Accessors.
-∗ ownP ς'
∗ ⌜phys_inv ς'⌝
∗ ⌜rel_inv ς ς'⌝
- ∗ ⌜threads ς' !! π = Some V'⌝
∗ ▷ DInv (<[l := Excl h']> HIST)
- ∗ ⌜VInv ς' (<[π := Excl V']> (Excl <$> threads ς))⌝
+ ∗ ⌜view_ok (mem ς') V'⌝
∗ ⌜HInv ς' (<[l := Excl h']> HIST)⌝)
={E∖↑physN,E}=∗ Seen π V'.
Proof.
- iIntros (?) "[#HInv [>FV >FH]]".
+ iIntros (?) "(#HInv & >FV & >FH)".
iInv physN as (ς VIEW HIST INFO)
- "[HoP [>AV [>AH [>AI [>% [DInv [>% [>% >%]]]]]]]]" "HClose".
+ "(HoP & >AV & >AH & >AI & >% & DInv & >% & >% & >%)" "HClose".
iCombine "AV" "FV" as "HV".
iCombine "AH" "FH" as "HH".
iDestruct (own_valid with "HV") as %?%Views_frag_valid_le.
iDestruct (own_valid with "HH") as %?%Hists_frag_valid_eq.
iModIntro.
- iExists ς, HIST. rewrite H1. iFrame (H0 H2 (eq_sym H6)) "HoP DInv".
- iSplitR.
- { iPureIntro. move: H1 H5 => <-. rewrite lookup_fmap.
- case: (threads _ !! _) => // [?] [->] //. }
-
+ iExists ς, HIST. iFrame (H0 H2 (H1 _ _ H5) (eq_sym H6)) "HoP DInv".
iIntros (ς' V' h') "Hist'".
iMod (Hists_update_override with "[$HH]") as "[HH1 HH2]".
- iDestruct ("Hist'" with "HH2") as "[HoP' [% [% [% [DInv' [% %]]]]]]".
+ iDestruct ("Hist'" with "HH2") as "(HoP' & % & % & DInv' & % & %)".
iMod (Views_update_override with "[$HV]") as "[HV1 FV']".
iFrame "FV'".
iApply "HClose".
iNext.
- iExists _, _, _, _. iFrame (H4 H9 H10) "∗".
- iPureIntro. by apply (IInv_update_addins ς _ HIST _ l h h').
+ iExists _, _, _, _. iFrame (H4 H9) "∗".
+ iPureIntro. split; last by apply (IInv_update_addins ς _ HIST _ l h h').
+ move => ? ?. rewrite lookup_insert_Some => [] [[_ [<- //]]|[_ /H1]].
+ apply: view_ok_mono => //. by apply H7.
Qed.
End Accessors.
\ No newline at end of file
diff --git a/coq/ra/base/alloc.v b/coq/ra/base/alloc.v
index dc2c1545..f18e163e 100644
--- a/coq/ra/base/alloc.v
+++ b/coq/ra/base/alloc.v
@@ -41,97 +41,108 @@ Section Alloc.
Local Coercion of_Z := LitV ∘ LitInt.
- Lemma alloc_update_HInv
- ς ς' l m HIST V
- (Inv: HInv ς HIST)
- (Disj : MS_msg_disj (msgs (mem ς)) m)
- (MUpd : mem ς' = add_ins (mem ς) m Disj)
- (NAUpd : nats ς' = <[l:=mtime m]> (nats ς))
- (EqLoc : mloc m = l)
- (EqV : mview m = V)
- (EqVal: mval m = A)
- (OK: msg_ok m)
- (Fresh: ∀ m : message, m ∈ msgs $ mem ς → mloc m ≠ l)
- : HInv ς' (<[l:=Excl {[A, V]}]> HIST).
- Proof.
- split.
- - rewrite dom_insert (proj1 Inv) MUpd /=. abstract set_solver+EqLoc.
- - move => l0 V0.
- case: (decide (l = l0)) => [<- {l0}|NEq].
- + rewrite lookup_insert => [[<- {V0}]].
- exists (A,V). apply set_unfold_2. repeat split.
- * abstract naive_solver.
- * by rewrite NAUpd lookup_insert -EqLoc -EqV OK.
- * move: x => [? ?] [-> ->]. exists m. split; first by rewrite EqVal EqV.
- repeat split; [by rewrite -EqLoc -EqV OK|auto|].
- rewrite MUpd. apply set_unfold_2. by right.
- * move: x => [? ?] [m' [[? ?]]]. subst. rewrite MUpd.
- apply set_unfold_2.
- move => [_ [EqLoc [Inm'|->]]]; last by rewrite EqVal.
- abstract naive_solver.
- * abstract naive_solver.
- + rewrite NAUpd !lookup_insert_ne; [|auto|auto].
- move/(proj2 Inv) => [m' [H1 [H2 [H3 [H H4]]]]].
- exists m'. repeat split; auto; rewrite MUpd H.
- * rewrite /map_vt /hist_from_opt. abstract set_solver+.
- * abstract set_solver.
- Qed.
+ (* Lemma alloc_update_HInv *)
+ (* ς ς' l m HIST V *)
+ (* (Inv: HInv ς HIST) *)
+ (* (Disj : MS_msg_disj (msgs (mem ς)) m) *)
+ (* (MUpd : mem ς' = add_ins (mem ς) m Disj) *)
+ (* (NAUpd : nats ς' = <[l:=mtime m]> (nats ς)) *)
+ (* (EqLoc : mloc m = l) *)
+ (* (EqV : mview m = V) *)
+ (* (EqVal: mval m = A) *)
+ (* (OK: msg_ok m) *)
+ (* (Fresh: ∀ m : message, m ∈ msgs $ mem ς → mloc m ≠ l) *)
+ (* : HInv ς' (<[l:=Excl {[A, V]}]> HIST). *)
+ (* Proof. *)
+ (* split. *)
+ (* - rewrite dom_insert (proj1 Inv) MUpd /=. abstract set_solver+EqLoc. *)
+ (* - move => l0 V0. *)
+ (* case: (decide (l = l0)) => [<- {l0}|NEq]. *)
+ (* + rewrite lookup_insert => [[<- {V0}]]. *)
+ (* exists (A,V). apply set_unfold_2. repeat split. *)
+ (* * abstract naive_solver. *)
+ (* * by rewrite NAUpd lookup_insert -EqLoc -EqV OK. *)
+ (* * move: x => [? ?] [-> ->]. exists m. split; first by rewrite EqVal EqV. *)
+ (* repeat split; [by rewrite -EqLoc -EqV OK|auto|]. *)
+ (* rewrite MUpd. apply set_unfold_2. by right. *)
+ (* * move: x => [? ?] [m' [[? ?]]]. subst. rewrite MUpd. *)
+ (* apply set_unfold_2. *)
+ (* move => [_ [EqLoc [Inm'|->]]]; last by rewrite EqVal. *)
+ (* abstract naive_solver. *)
+ (* * abstract naive_solver. *)
+ (* + rewrite /LInv NAUpd !lookup_insert_ne; [|auto|auto]. *)
+ (* move/(proj2 Inv) => [m' [H1 [H2 [H3 [H H4]]]]]. *)
+ (* exists m'. repeat split; auto; rewrite MUpd H. *)
+ (* * rewrite /map_vt /hist_from_opt. abstract set_solver+. *)
+ (* * abstract set_solver. *)
+ (* Qed. *)
Lemma f_alloc π V:
{{{ PSCtx ∗ ▷ Seen π V }}}
- (Alloc, π) @ ↑physN
- {{{ l V' h' v, RET (#l, π);
+ (Alloc, V) @ ↑physN
+ {{{ l V' h' v, RET (#l, V');
⌜V ⊑ V'⌝ ∗ Seen π V' ∗ Hist l h' ∗ Info l 1 v
∗ ⌜na_safe l h' V'⌝ ∗ ⌜alloc_local h' V'⌝ ∗ ⌜uninit h'⌝ }}}.
Proof.
iIntros (Φ) "[#? HSeen] Post".
iMod (PSInv_open_alloc with "[-Post]")
- as (ς HIST INFO) "(oPS & % & % & % & % & oAI & oAH & HClose)" ; auto.
+ as (ς HIST INFO) "(oPS & % & % & % & % & oAI & HClose)" ; auto.
iApply (wp_alloc_pst with "oPS"); eauto.
- - destruct (threads ς !! π) eqn:TV; [by econstructor|done].
- - iNext. iFrame. iIntros (l ς') "(% & % & % & ownς')".
- inversion H5.
-
- assert (INone: INFO !! l = None).
- { rewrite <- (not_elem_of_dom (D:= (gset loc)) INFO).
- rewrite (H2 l). abstract set_solver+Fresh. }
-
- iDestruct (own_valid with "oAH") as %[_ HValid]%auth_valid_discrete.
- assert (HNone: HIST !! l = None).
- { by rewrite Hist_Info_fresh. }
-
- pose v := DecAgree 1%positive.
-
- iMod ((Infos_alloc _ _ v) with "oAI") as "oAI"; [eauto|done|].
- iMod ((Hists_alloc _ _ {[A,V']}) with "oAH") as "oAH"; first eauto.
-
- iMod ("HClose" $! l v ς' V' with "[-Post]") as "[? [? ?]]".
- { iFrame (H3 H4) "∗".
- iSplit; [|iSplit; [|iSplit; [|iSplit]]]; try iPureIntro.
- - by rewrite TUpd lookup_insert.
- - by rewrite /VInv TUpd -!fmap_insert.
- - eapply alloc_update_HInv; eauto.
- + by rewrite /msg_ok EqLoc EqView VUpd
- lookup_join_max Local lookup_singleton.
- + move => m0 ? ?. apply (not_elem_of_empty (C:=gset message) m0).
- rewrite -Fresh. by apply set_unfold_2.
- - eapply IInv_update_alloc => //.
- - iIntros "DInv".
- rewrite /DInv big_op.big_sepM_insert; last auto. iFrame.
- iIntros (V1) "%". exfalso.
- assert (EqD: (D,V1) = (A,V')).
- { by rewrite -(elem_of_singleton (C:= History))
- H6 elem_of_singleton. }
- by inversion EqD. }
-
- iApply ("Post" $! l V' _ v). iFrame. iPureIntro.
- repeat split.
- + rewrite VUpd. rewrite ViewOf in H0. move: H0 => [->]. solve_jsl.
- + repeat eexists; first exact/elem_of_singleton; last reflexivity.
- move => [? ?] /elem_of_singleton [_ ->] //=.
- + repeat eexists; first exact/elem_of_singleton; eauto. solve_jsl.
- + by eexists.
+ iNext. iFrame. iIntros (l ς' V') "(% & % & % & % & ownς')".
+ inversion H6.
+
+ assert (INone: INFO !! l = None).
+ { rewrite <- (not_elem_of_dom (D:= (gset loc)) INFO).
+ rewrite H2. abstract set_solver+Fresh. }
+
+ (* iDestruct (own_valid with "oAH") as %[_ HValid]%auth_valid_discrete. *)
+ (* assert (HNone: HIST !! l = None). *)
+ (* { by rewrite Hist_Info_fresh. } *)
+
+ pose v := DecAgree 1%positive.
+
+ iMod ((Infos_alloc _ _ v) with "oAI") as "oAI"; [eauto|done|].
+
+ iMod ("HClose" $! l v ς' V' (mtime m) with "[-Post]") as "[? [? ?]]".
+ { iFrame (H3 H4 H5) "∗".
+ iSplit; [|iSplit; [|iSplit; [|iSplit]]]; try iPureIntro.
+ - by apply/Hist_Info_fresh.
+ - rewrite MUpd /=. destruct m. cbn in *. subst. done.
+ - by rewrite NATSOld.
+ - rewrite /LInv.
+ eexists (_,_); split; [|split; [|split; [|split]]].
+ + rewrite elem_of_singleton. reflexivity.
+ + move => ?. rewrite elem_of_singleton => <- //.
+ + rewrite NATSOld lookup_insert VUpd infrastructure.lookup_join lookup_singleton /=.
+ solve_jsl.
+ + move => ?. rewrite elem_of_singleton.
+ split.
+ * move => -> /=. rewrite MUpd /=.
+ apply/elem_of_map_gset. eexists (<l → A@mtime m,_>). split; first reflexivity.
+ apply/elem_of_filter; split; last first.
+ { apply/elem_of_hist; split; first reflexivity.
+ apply/elem_of_union. right. rewrite elem_of_singleton.
+ destruct m. cbn in *. by subst.
+ }
+ rewrite VUpd infrastructure.lookup_join lookup_singleton Local. solve_jsl.
+ * move/elem_of_map_gset => [m' [->]].
+ move/elem_of_filter => [?]. move/elem_of_hist => [EqLoc'].
+ rewrite MUpd /= elem_of_union => [] [In|].
+ { exfalso. move: (Fresh m').
+ rewrite elem_of_filter -EqLoc' => /=. by set_solver+In. }
+ rewrite elem_of_singleton => ->. by rewrite -EqVal -EqView.
+ + set_solver+.
+ - apply: (IInv_update_alloc _ _ _ _ _ _ _ _ Disj); try done.
+ }
+
+ iApply ("Post" $! l V' _ v). iFrame. iPureIntro.
+ repeat split.
+ - rewrite VUpd. solve_jsl.
+ - repeat eexists; first exact/elem_of_singleton; last reflexivity.
+ move => [? ?] /elem_of_singleton [_ ->] //=.
+ - repeat eexists; first exact/elem_of_singleton; eauto. solve_jsl.
+ - by eexists.
Qed.
End Alloc.
\ No newline at end of file
diff --git a/coq/ra/base/at_cas.v b/coq/ra/base/at_cas.v
index ee3918ba..305d7939 100644
--- a/coq/ra/base/at_cas.v
+++ b/coq/ra/base/at_cas.v
@@ -2,8 +2,8 @@ From ra.base Require Import at_shared.
Lemma f_CAS `{fG : !foundationG Σ} π V l h (v_r v_w: Z):
{{{ PSCtx ∗ ▷ Seen π V ∗ ▷ Hist l h ∗ ⌜init_local h V⌝ }}}
- (CAS #l #v_r #v_w, π) @ ↑physN
- {{{ b V' h', RET (LitV $ LitInt b, π);
+ (CAS #l #v_r #v_w, V) @ ↑physN
+ {{{ b V' h', RET (LitV $ LitInt b, V');
⌜V ⊑ V'⌝ ∗ Seen π V' ∗ Hist l h' ∗ ⌜init_local h' V'⌝
∗ ∃ (V1: View) v, ⌜V1 ⊑ V'⌝
∗ ⌜value_at h V1 (VInj v)⌝
@@ -27,8 +27,6 @@ Proof.
destruct H3 as [HInv1 HInv2]. symmetry in H2.
move: (HInv2 _ _ H2) => [[v0 V0] [In0 [Min0 [/= NA0 [Eqh Val]]]]].
- destruct (threads ς !! π) as [Vl|] eqn:HV1; last done.
-
destruct H as [v' [V' [In' [Local' IsVal']]]].
assert (∃ t, V0 !! l = Some t) as [t EqV0].
@@ -39,32 +37,23 @@ Proof.
rewrite EqV0 in Eqh.
assert (Eqh2: h ≡ map_vt (hist_from (mem ς) l t)).
{ move: Eqh. abstract set_solver+. }
- move: H1 => [H1].
- iApply (wp_CAS_pst with "oPS"); first auto.
+ iApply (wp_CAS_pst with "oPS"); [done|done|..].
- (* drf_pre ς π l *)
- econstructor; eauto. rewrite NA0 -H1. by move: (Min0 _ In') => /= ->.
+ econstructor; eauto. rewrite NA0. by move: (Min0 _ In') => /= ->.
- (* init_pre ς π l *)
eapply init_pre_helper with (t:=t) (v:=v') (V:=V'); eauto.
- + by rewrite -H1.
- + exists (v0, V0). split;[|split]; auto. by move => [].
- + apply H0.
+ exists (v0, V0). split;[|split]; auto. by move => [].
- (* frame update and re-establish the PSInv *)
- iNext. iIntros (b ς') "(% & % & % & HP)".
+ iNext. iIntros (b ς' V'') "(% & % & % & % & HP)".
- destruct H4 as [[bTrue CPost]|[bFalse CPost]]; inversion CPost;
- rewrite HV1 in ViewOf; inversion ViewOf; subst V1.
+ destruct H5 as [[bTrue CPost]|[bFalse CPost]]; inversion CPost.
{ (* CAS succeeds *)
- assert (threads ς' !! π = Some V'0 ∧ V ⊑ V'0) as [HV'1 HV'2].
- { split.
- - by rewrite TUpd lookup_insert.
- - cbn in H1. rewrite VUpd H1. solve_jsl. }
-
assert (V0 !! l ⊏ Some (mtime m')).
{ rewrite EqV0. cbn. rewrite EqTime'.
eapply Pos.le_lt_trans; last by apply Pos.lt_add_r.
etrans; eauto.
change (Some t ⊑ Some tl).
- rewrite -EqV0 -Local -H1.
+ rewrite -EqV0 -Local.
by move: (Min0 (v', V')) => /= ->. }
(* get h' *)
@@ -87,20 +76,19 @@ Proof.
assert (t ⊑ mtime m).
{ rewrite EqTime. rewrite -TimeLe.
change (Some t ⊑ Some tl).
- rewrite -Local -EqV0 -H1.
+ rewrite -Local -EqV0.
etrans; first by apply (Min0 _ In'). by simpl. }
assert (Inm': m' ∈ msgs (mem ς')).
{ rewrite MUpd elem_of_union elem_of_singleton. by right. }
- assert (EqVt: Some (mtime m') = V'0 !! l).
+ assert (EqVt: Some (mtime m') = V'' !! l).
{ destruct (IMOk _ H _ Inm') as [VTEq _].
by rewrite -EqView' -EqLoc' VTEq. }
- iApply ("Post" $! b V'0 h').
+ iApply ("Post" $! b _ h').
- iMod ("HClose" $! ς' V'0 h' with "[DInv $HP]") as "[Seen' Hist']".
+ iMod ("HClose" $! ς' _ h' with "[DInv $HP]") as "[Seen' Hist']".
{ (* re-establish PSInv *)
- rewrite HV'1. iFrame (H H3 HInv'). iSplitL ""; first auto.
- iSplitL; last by rewrite /VInv TUpd fmap_insert.
+ iFrame (H H3 H4 HInv').
iNext. iApply (DInv_update_value with "DInv"); last eauto.
move => ? Eq2. move: Inh'.
rewrite Eq2 elem_of_singleton. by inversion 1. }
@@ -108,6 +96,7 @@ Proof.
(* show post-condition *)
iModIntro. iFrame "Hist' Seen'".
repeat (iSplit; first auto).
+ - iPureIntro. rewrite VUpd. solve_jsl.
- iPureIntro. exists (VInj v_w), (mview m'). repeat (split; auto).
by rewrite EqView'.
- iExists (mview m), v_r. repeat (iSplit).
@@ -115,7 +104,7 @@ Proof.
+ iPureIntro. rewrite -EqVal /value_at.
rewrite Eqh2 elem_of_map_gset. exists m. split; auto.
by apply elem_of_hist_from.
- + iPureIntro. by rewrite H1 Eqtr Local.
+ + iPureIntro. by rewrite Eqtr Local.
+ iLeft. rewrite -EqView'.
iFrame (bTrue (Logic.eq_refl v_r) Eqh'2 Disjh' Inh').
iSplit; [|iSplit]; iPureIntro.
@@ -136,27 +125,20 @@ Proof.
by inversion Eq2'. } }
{ (* CAS fails *)
- assert (threads ς' !! π = Some V'0 ∧ V ⊑ V'0) as [HV'1 HV'2].
- { split.
- - by rewrite TUpd lookup_insert.
- - cbn in H1. rewrite VUpd H1. solve_jsl. }
- iApply ("Post" $! _ V'0 h).
+ iApply ("Post" $! _ _ h).
- iMod ("HClose" $! ς' V'0 h with "[DInv $HP]") as "[Seen' Hist]".
+ iMod ("HClose" $! ς' _ h with "[DInv $HP]") as "[Seen' Hist]".
{ rewrite (insert_id HIST); last auto.
(* re-establish PSInv *)
- iFrame (H H3) "∗".
- iSplit;[|iSplit]; iPureIntro.
- - by rewrite HV'1.
- - by rewrite /VInv TUpd fmap_insert.
- - rewrite /HInv MOld NATSOld. repeat (split; auto). }
+ iFrame (H H3 H4) "∗".
+ by rewrite /HInv /= MOld NATSOld. }
assert (Eqtr: mview m !! l = Some (mtime m)).
{ destruct (IMOk _ H0 _ InR) as [VTEq _].
by rewrite -EqLoc VTEq. }
- assert (Vl !! l ⊑ Some (mtime m)).
+ assert (V !! l ⊑ Some (mtime m)).
{ by rewrite Local. }
assert ((VInj v, mview m) ∈ h).
@@ -164,17 +146,18 @@ Proof.
apply elem_of_hist_from. repeat (split; auto).
etrans; last by apply TimeLe.
change (Some t ⊑ Some t0).
- rewrite -Local -EqV0 -H1.
+ rewrite -Local -EqV0.
etrans; first by apply (Min0 _ In'). by simpl. }
(* show post-condition *)
- iModIntro. iFrame (HV'2) "Hist Seen'".
+ iModIntro. iFrame "Hist Seen'".
repeat iSplit.
+ - iPureIntro. rewrite VUpd. solve_jsl.
- iPureIntro. exists (VInj v), (mview m). repeat (split; auto).
rewrite VUpd. solve_jsl.
- iExists (mview m), v. repeat iSplit; auto.
+ iPureIntro. rewrite VUpd. solve_jsl.
- + by rewrite H1 Eqtr Local.
+ + by rewrite Eqtr Local.
+ iRight. repeat (iSplit; auto). iPureIntro.
rewrite VUpd lookup_join_max. apply: (anti_symm (⊑)); [solve_jsl|].
rewrite Local Eqtr. solve_jsl. }
diff --git a/coq/ra/base/at_fai.v b/coq/ra/base/at_fai.v
index 7d5a9227..076b4024 100644
--- a/coq/ra/base/at_fai.v
+++ b/coq/ra/base/at_fai.v
@@ -2,8 +2,8 @@ From ra.base Require Import at_shared.
Lemma f_FAI `{fG : !foundationG Σ} C π V l h:
{{{ PSCtx ∗ ▷ Seen π V ∗ ▷ Hist l h ∗ ⌜init_local h V⌝ }}}
- (FAI C #l, π) @ ↑physN
- {{{ (v: Z) V' h', RET (LitV $ LitInt v, π);
+ (FAI C #l, V) @ ↑physN
+ {{{ (v: Z) V' h', RET (LitV $ LitInt v, V');
⌜V ⊑ V'⌝ ∗ Seen π V' ∗ Hist l h' ∗ ⌜init_local h' V'⌝
∗ ∃ (V1: View) (v': Z), ⌜V1 ⊑ V'⌝
∗ ⌜value_at h V1 (VInj v)⌝
@@ -25,8 +25,6 @@ Proof.
destruct H3 as [HInv1 HInv2]. symmetry in H2.
move: (HInv2 _ _ H2) => [[v0 V0] [In0 [Min0 [/= NA0 [Eqh Val]]]]].
- destruct (threads ς !! π) as [Vl|] eqn:HV; last done.
-
destruct H as [vx [Vx [Inx [Localx IsValx]]]].
assert (∃ t, V0 !! l = Some t) as [t EqV0].
@@ -37,29 +35,21 @@ Proof.
rewrite EqV0 in Eqh.
assert (Eqh2: h ≡ map_vt (hist_from (mem ς) l t)).
{ move: Eqh. abstract set_solver+. }
- move: H1 => [H1].
- iApply (wp_FAI_pst with "oPS"); first auto.
+ iApply (wp_FAI_pst with "oPS"); [done|done|..].
- (* drf_pre ς π l *)
- econstructor; eauto. rewrite NA0 -H1. by move: (Min0 _ Inx) => /= ->.
+ econstructor; eauto. rewrite NA0. by move: (Min0 _ Inx) => /= ->.
- (* init_pre ς π l *)
eapply init_pre_helper with (t:=t) (v:=vx) (V:=Vx); eauto.
- + by rewrite -H1.
- + exists (v0, V0). split;[|split]; auto. by move => [].
- + apply H0.
+ exists (v0, V0). split;[|split]; auto. by move => [].
- (* frame update and re-establish the PSInv *)
- iNext. iIntros (v ς') "(% & % & % & HP)".
- inversion H4. rewrite HV in ViewOf. inversion ViewOf. subst V1.
-
- assert (threads ς' !! π = Some V' ∧ V ⊑ V') as [HV'1 HV'2].
- { split.
- - by rewrite TUpd lookup_insert.
- - rewrite VUpd -H1. do 2 (etrans; last by apply join_ext_l). done. }
+ iNext. iIntros (v ς' V'') "(% & % & % & % & HP)".
+ inversion H5.
assert (V0 !! l ⊏ Some (mtime m')).
{ rewrite EqV0. cbn. rewrite EqTime'.
eapply Pos.le_lt_trans; last by apply Pos.lt_add_r. etrans; eauto.
change (Some t ⊑ Some tl).
- rewrite -EqV0 -Local -H1.
+ rewrite -EqV0 -Local.
by move : (Min0 (vx, Vx)) => /= ->. }
(* get h' *)
@@ -82,30 +72,28 @@ Proof.
assert (t ⊑ mtime m).
{ rewrite EqTime. etrans; last by apply TimeLe.
change (Some t ⊑ Some tl).
- rewrite -Local -EqV0 -H1.
+ rewrite -Local -EqV0.
etrans; first by apply (Min0 _ Inx). by simpl. }
assert (Inm': m' ∈ msgs (mem ς')).
{ rewrite MUpd elem_of_union elem_of_singleton. by right. }
- assert (EqVt: Some (mtime m') = V' !! l).
+ assert (EqVt: Some (mtime m') = V'' !! l).
{ destruct (IMOk _ H _ Inm') as [VTEq _].
by rewrite -EqView' -EqLoc' VTEq. }
- iApply ("Post" $! _ V' h').
+ iApply ("Post" $! _ _ h').
- iMod ("HClose" $! ς' V' h' with "[DInv $HP]") as "[Seen' Hist']".
+ iMod ("HClose" $! ς' _ h' with "[DInv $HP]") as "[Seen' Hist']".
{ (* re-establish PSInv *)
- rewrite HV'1.
- iFrame (H H3 HInv'). iSplit.
- - iPureIntro. reflexivity.
- - iSplitL; last by rewrite /VInv TUpd fmap_insert.
- iNext. iApply (DInv_update_value with "DInv"); last eauto.
- move => ? Eq2. move: Inh'.
- rewrite Eq2 elem_of_singleton. by inversion 1. }
+ iFrame (H H3 H4 HInv').
+ iNext. iApply (DInv_update_value with "DInv"); last eauto.
+ move => ? Eq2. move: Inh'.
+ rewrite Eq2 elem_of_singleton. by inversion 1. }
set v': Z := ((v + 1) `mod` Z.pos C)%Z.
(* show post-condition *)
iModIntro. iFrame "Seen' Hist'".
repeat iSplit; first auto.
+ + iPureIntro. rewrite VUpd. solve_jsl.
+ iPureIntro. exists (VInj v'), (mview m'). by rewrite {2}EqView'.
+ iExists (mview m), v'.
rewrite -EqView'. iFrame ((Logic.eq_refl v') Eqh'2 Disjh' Inh').
@@ -113,7 +101,7 @@ Proof.
* rewrite EqView' VUpd. etrans; [done|apply join_ext_r].
* rewrite -EqVal /value_at Eqh2 elem_of_map_gset.
exists m. by rewrite elem_of_hist_from.
- * by rewrite H1 Eqtr Local.
+ * by rewrite Eqtr Local.
* by do 2 eexists.
* assert (EqL: (<[l:=Excl h']> HIST !! l = Excl' h')).
{ by rewrite lookup_insert. }
diff --git a/coq/ra/base/at_read.v b/coq/ra/base/at_read.v
index b2f215e8..2d09f3df 100644
--- a/coq/ra/base/at_read.v
+++ b/coq/ra/base/at_read.v
@@ -3,8 +3,8 @@ From ra.base Require Import at_shared.
Lemma f_read_at `{fG : !foundationG Σ} π V_l l h :
{{{ PSCtx
∗ ▷ Seen π V_l ∗ ▷ Hist l h ∗ ⌜init_local h V_l⌝ }}}
- ([ #l ]_at, π) @ ↑physN
- {{{ (v : Z) V', RET (#v, π);
+ ([ #l ]_at, V_l) @ ↑physN
+ {{{ (v : Z) V', RET (#v, V');
⌜V_l ⊑ V'⌝ ∗ Seen π V' ∗ Hist l h ∗ ⌜at_safe h V'⌝
∗ ∃ V_1, ⌜V_1 ⊑ V'⌝
∗ ⌜V_1 !! l = V' !! l⌝
@@ -18,7 +18,6 @@ Proof.
destruct H3 as [HInv1 HInv2]. symmetry in H2.
move: (HInv2 _ _ H2) => [[v0 V0] [In0 [Min0 [/= NA0 [Eqh Val]]]]].
- destruct (threads ς !! π) as [Vl|] eqn:HV1; last done. cbn in H1.
destruct H as [v' [V' [In' [Local' IsVal']]]].
assert (∃ t, V0 !! l = Some t) as [t EqV0].
@@ -28,36 +27,26 @@ Proof.
rewrite EqV0 in Eqh.
assert (Eqh2: h ≡ map_vt (hist_from(mem ς) l t)).
{ move: Eqh. abstract set_solver+. }
- move: H1 => [H1].
- iApply (wp_load_at_pst with "oPS"); first auto.
+ iApply (wp_load_at_pst with "oPS"); [by auto|by auto|..].
- (* drf_pre ς π l *)
- econstructor; eauto. rewrite NA0. move: (Min0 _ In') => /= ->.
- by rewrite -H1.
+ econstructor; eauto. rewrite NA0. by move: (Min0 _ In') => /= ->.
- (* init_pre ς π l *)
eapply init_pre_helper with (t:=t) (v:=v') (V:=V'); eauto.
- + by rewrite -H1.
+ exists (v0, V0). split; [|split] => //. by move => [].
- + apply H0.
- (* frame update and re-establish the PSInv *)
- iNext. iIntros (v1 ς') "[% [% [% HP]]]".
+ iNext. iIntros (v1 ς' V'') "(% & % & % & % & HP)".
- inversion H4. rewrite HV1 in ViewOf. inversion ViewOf. subst Vl.
+ inversion H5.
- assert (threads ς' !! π = Some V'0 ∧ V ⊑ V'0) as [HV'1 HV'2].
- { split.
- - by rewrite TUpd lookup_insert.
- - rewrite VUpd. solve_jsl. }
-
- iApply ("Post" $! _ V'0).
- iMod ("HClose" $! ς' V'0 h with "[DInv $HP]") as "[Seen' Hist']".
+ iApply ("Post" $! _ _).
+ iMod ("HClose" $! ς' _ h with "[DInv $HP]") as "[Seen' Hist']".
{ rewrite (insert_id HIST); last auto.
(* re-establish PSInv *)
- iFrame (H H3) "∗". rewrite HV'1 /HInv MOld NATSOld.
- repeat (iSplit; auto). by rewrite /VInv TUpd fmap_insert. }
+ iFrame (H H3 H4) "∗". by rewrite /HInv /= MOld NATSOld. }
(* show post-condition *)
iModIntro. iFrame "Hist' Seen'". repeat iSplit.
- + by rewrite H6.
- + iPureIntro. exists v', V'. split; auto. by rewrite -HV'2 -H6.
+ + iPureIntro. rewrite VUpd. solve_jsl.
+ + iPureIntro. exists v', V'. split; auto. rewrite VUpd Local'. solve_jsl.
+ iExists (mview m).
destruct (IMOk _ H0 _ In) as [EqT _]. subst.
rewrite EqT. repeat iSplit; iPureIntro; [solve_jsl|..].
diff --git a/coq/ra/base/at_shared.v b/coq/ra/base/at_shared.v
index 526346fb..d09b4485 100644
--- a/coq/ra/base/at_shared.v
+++ b/coq/ra/base/at_shared.v
@@ -77,12 +77,12 @@ Proof.
apply set_unfold_2; abstract naive_solver.
- move => l0 V0.
case: (decide (l = l0)) => [<- {l0}|?]; last first.
- + rewrite NATSOld lookup_insert_ne; last auto.
+ + rewrite /LInv NATSOld lookup_insert_ne; last auto.
move/(proj2 HInvς) => [m' [? [? [? [H ?]]]]].
exists m'. do 4!(try split); auto.
rewrite MUpd H. rewrite /map_vt /hist_from_opt.
apply set_unfold_2. abstract naive_solver.
- + rewrite MUpd NATSOld lookup_insert => [[<- {V0}]].
+ + rewrite /LInv MUpd NATSOld lookup_insert => [[<- {V0}]].
move: (proj2 HInvς _ _ HH) => [[v1 V1] [? [Min1 [? [H IS]]]]].
assert (Inm: m ∈ msgs $ mem ς').
{ rewrite MUpd elem_of_union elem_of_singleton. by right. }
diff --git a/coq/ra/base/at_write.v b/coq/ra/base/at_write.v
index 1f5a6950..d2b1ad49 100644
--- a/coq/ra/base/at_write.v
+++ b/coq/ra/base/at_write.v
@@ -3,8 +3,8 @@ From ra.base Require Import at_shared.
Lemma f_write_at `{fG : !foundationG Σ} π V_l l h v:
{{{ PSCtx
∗ ▷ Seen π V_l ∗ ▷ Hist l h ∗ ⌜alloc_local h V_l⌝ }}}
- ([ #l ]_at <- #v, π) @ ↑physN
- {{{ V' h', RET (LitV LitUnit, π);
+ ([ #l ]_at <- #v, V_l) @ ↑physN
+ {{{ V' h', RET (LitV LitUnit, V');
⌜V_l ⊑ V'⌝ ∗ Seen π V'
∗ Hist l h' ∗ ⌜init_local h' V'⌝ ∗ ⌜init l h'⌝
∗ ⌜h' ≡ {[VInj v, V']} ∪ h⌝
@@ -20,8 +20,6 @@ Proof.
destruct H3 as [HInv1 HInv2]. symmetry in H2.
move: (HInv2 _ _ H2) => [[v0 V0] [In0 [Min0 [/= NA0 [Eqh Val]]]]].
- destruct (threads ς !! π) as [V1|] eqn:HV1; last done. cbn in H1.
-
destruct H as [v' [V' [In' [Local' IsND']]]].
assert (∃ t, V0 !! l = Some t) as [t EqV0].
@@ -31,29 +29,23 @@ Proof.
rewrite EqV0 in Eqh.
assert (Eqh2: h ≡ map_vt (hist_from(mem ς) l t)).
{ move: Eqh. abstract set_solver+. }
- move: H1 => [H1].
- iApply (wp_store_at_pst with "oPS"); first auto.
+ iApply (wp_store_at_pst with "oPS"); [by auto|by auto|..].
- (* drf_pre ς π l *)
- econstructor; eauto. rewrite NA0. move: (Min0 _ In') => /= ->. by rewrite -H1.
+ econstructor; eauto. rewrite NA0. by move: (Min0 _ In') => /= ->.
- (* alloc_pre ς π l *)
eapply alloc_pre_helper; eauto.
- + eapply alloc_local_Mono; first by rewrite H1. exists v', V'. by erewrite <-Eqh2, <-H1.
+ + eapply alloc_local_Mono; first by auto. exists v', V'. by erewrite <-Eqh2.
+ exists (v0, V0). repeat setoid_rewrite <-Eqh2.
split; last (split); auto; by move => [].
+ apply H0.
- (* frame update and re-establish the PSInv *)
- iNext. iIntros (ς') "(% & % & % & HP)".
-
- inversion H4. rewrite HV1 in ViewOf. inversion ViewOf. subst V1.
+ iNext. iIntros (ς' V'') "(% & % & % & % & HP)".
- assert (threads ς' !! π = Some V'0 ∧ V ⊑ V'0) as [HV'1 HV'2].
- { split.
- - by rewrite TUpd lookup_insert.
- - rewrite VUpd; solve_jsl. }
+ inversion H5.
- assert (Le: V0 !! l ⊑ V !! l).
- { rewrite -H6 -(Local' _). by apply :(Min0 (v', V')). }
+ assert (Le: V0 !! l ⊑ V_l !! l).
+ { rewrite -(Local' _). by apply :(Min0 (v', V')). }
assert (V0 !! l ⊏ Some (mtime m)).
{ by move: Le Local ->. }
@@ -69,13 +61,10 @@ Proof.
- apply H. }
- iApply ("Post" $! V'0 h').
- iMod ("HClose" $! ς' V'0 h' with "[DInv $HP]") as "[Seen' Hist']".
+ iApply ("Post" $! _ h').
+ iMod ("HClose" $! ς' _ h' with "[DInv $HP]") as "[Seen' Hist']".
{ (* re-establish PSInv *)
- rewrite HV'1.
- iFrame (H H3 HInv').
- iSplit; first auto.
- iSplit; last by rewrite /VInv TUpd fmap_insert.
+ iFrame (H H3 H4 HInv').
iNext. iApply (DInv_update_value with "DInv"); last eauto.
move => ? Eqh3. move : Inh'.
rewrite Eqh3 elem_of_singleton. by inversion 1. }
@@ -84,7 +73,7 @@ Proof.
(* show post-condition *)
iModIntro. rewrite -EqView. iFrame (Eqh'2 Disjh' Inh') "# ∗".
iSplit; [|iSplit]; iPureIntro.
- + rewrite EqView. by rewrite H6.
+ + rewrite EqView VUpd. solve_jsl.
+ by exists (VInj v), (mview m).
+ split; first by do 2 eexists.
assert (EqL: (<[l:=Excl h']> HIST !! l = Excl' h')).
diff --git a/coq/ra/base/dealloc.v b/coq/ra/base/dealloc.v
index 05d3fabe..0307287c 100644
--- a/coq/ra/base/dealloc.v
+++ b/coq/ra/base/dealloc.v
@@ -3,8 +3,8 @@ From ra.base Require Import na_shared.
Lemma f_dealloc `{fG : !foundationG Σ} π V_l l h v :
{{{ PSCtx ∗ ▷ Seen π V_l
∗ ▷ Hist l h ∗ ▷ Info l 1 v ∗ ⌜alloc_local h V_l⌝ }}}
- (Dealloc #l, π) @ ↑physN
- {{{ V', RET (#(), π);
+ (Dealloc #l, V_l) @ ↑physN
+ {{{ V', RET (#(), V');
⌜V_l ⊑ V'⌝ ∗ Seen π V' }}}.
Proof.
iIntros (Φ) "(#I & Seen & Hist & Info & %) Post".
@@ -13,9 +13,8 @@ Proof.
iMod (PSInv_open_V with "[$I $Seen $Hist]")
as (ς HIST) "(oPS & % & % & % & DInv & % & HClose)"; first auto.
- destruct H3 as [HInv1 HInv2]. symmetry in H2.
- move: (HInv2 _ _ H2) => [[v0 V0] [In0 [Min0 [/= NA0 [Eqh Val]]]]].
- destruct (threads ς !! π) as [Vl|] eqn:HV1; last done. cbn in H1.
+ destruct H3 as [HInv1 HInv2].
+ move: (HInv2 _ _ (eq_sym H1)) => [[v0 V0] [In0 [Min0 [/= NA0 [Eqh Val]]]]].
assert (∃ t, V0 !! l = Some t) as [t EqV0].
{ apply (elem_of_hist_view_ok v0 _ (mem ς) _ (V0 !! l)).
@@ -26,24 +25,19 @@ Proof.
destruct H as [v' [V' [In' [Local' IsND']]]].
move : H1 => [H1].
- iApply (wp_dealloc_pst with "oPS"); first eauto.
+ iApply (wp_dealloc_pst with "oPS"); [eauto|auto|..].
- (* drf_pre ς π l *)
- econstructor; eauto. rewrite NA0 -H1. by move : (Min0 _ In') => /= ->.
+ econstructor; eauto. rewrite NA0. by move : (Min0 _ In') => /= ->.
- (* alloc_pre ς π l *)
eapply alloc_pre_helper; eauto.
- + eapply alloc_local_Mono; first by rewrite H1. exists v', V'. by erewrite <- Eqh2.
+ + eapply alloc_local_Mono; first by auto. exists v', V'. by erewrite <- Eqh2.
+ exists (v0, V0). repeat setoid_rewrite <-Eqh2. do 2 (split; first auto).
by move => [].
+ apply H0.
- (* frame update and re-establish the PSInv *)
- iNext. iIntros (ς') "[% [% [% HP]]]".
+ iNext. iIntros (ς' V'') "[% [% [% [% HP]]]]".
- inversion H4. rewrite HV1 in ViewOf. inversion ViewOf. subst Vl.
-
- assert (threads ς' !! π = Some V'0 ∧ V ⊑ V'0) as [HV'1 HV'2].
- { split.
- - by rewrite TUpd lookup_insert.
- - rewrite VUpd; apply join_ext_l. }
+ inversion H5.
(* get h' *)
pose (h' := {[(mval m, mview m)]}: History).
@@ -51,16 +45,14 @@ Proof.
assert (HInv': HInv ς' (<[l:=Excl h']> HIST)). {
eapply (write_na_update_HInv ς) => //. apply H. }
- iApply ("Post" $! V'0).
- iMod ("HClose" $! ς' V'0 h' with "[DInv $HP Info]") as "Seen'".
- { iIntros "Hist'". iFrame (H H3 HInv').
+ iApply ("Post" $! _).
+ iMod ("HClose" $! ς' _ h' with "[DInv $HP Info]") as "Seen'".
+ { iIntros "Hist'". iFrame (H H3 H4 HInv').
(* re-establish PSInv *)
- iSplit; first by rewrite HV'1.
- iSplit; last by rewrite /VInv TUpd fmap_insert.
iNext.
iApply (DInv_update_return with "[$Hist' $DInv Info]"); first eauto.
by iExists _. } (* TODO: add Frame exist *)
(* show post-condition *)
- iFrame "Seen'". iPureIntro. by rewrite H6.
+ iFrame "Seen'". iPureIntro. subst. rewrite VUpd. solve_jsl.
Qed.
\ No newline at end of file
diff --git a/coq/ra/base/fork.v b/coq/ra/base/fork.v
index 3ee85520..49c7a69a 100644
--- a/coq/ra/base/fork.v
+++ b/coq/ra/base/fork.v
@@ -3,9 +3,9 @@ From ra.base Require Import na_shared.
Lemma f_fork `{fG : foundationG Σ} (Φ : val ra_lang → iProp _) (P: iProp _) π V e:
PSCtx
∗ ▷ Seen π V ∗ ▷ P
- ∗ ▷ (Seen π V -∗ Φ (#(), π))
- ∗ ▷ (∀ ρ, PSCtx ∗ Seen ρ V ∗ P -∗ WP (e, ρ) {{ _, True }})
- ⊢ WP (Fork e, π) @ ↑physN {{ Φ }}.
+ ∗ ▷ (∀ V', ⌜V ⊑ V'⌝ -∗ Seen π V' -∗ Φ (#(), V'))
+ ∗ ▷ (∀ ρ V', ⌜V ⊑ V'⌝ -∗ PSCtx -∗ Seen ρ V' -∗ P -∗ WP (e, V') {{ _, True }})
+ ⊢ WP (Fork e, V) @ ↑physN {{ Φ }}.
Proof.
iIntros "[#? [>FV [HP [Post HFork]]]]".
iInv physN as (ς VIEW HIST INFO)
@@ -16,24 +16,23 @@ Proof.
iDestruct "HV" as "[HV FV]".
- iApply wp_fork_pst => //.
- - rewrite -H0 lookup_fmap in H4.
- move/fmap_Some: H4 => [? [? ?]]. eauto.
+ iApply wp_fork_pst => //; first by exact: H0.
- iNext. iFrame "HoP".
- iIntros (ρ ς') "[% [% [% Oς']]]". inversion H6.
+ iIntros (ς' V') "(% & % & % & % & Oς')". inversion H7. subst.
- iMod ((Views_alloc _ ρ V) with "[$HV]") as "[AV' FV']".
- { by rewrite -H0 lookup_fmap ViewNew. }
+ have: (∃ ρ : thread, VIEW !! ρ = None) => [|[ρ Hρ]].
+ { exists (fresh (dom _ (VIEW))).
+ by generalize (is_fresh (dom (gset positive) VIEW)) => /not_elem_of_dom. }
- iSplitR "HP FV' HFork"; last by (iApply "HFork"; iFrame).
+ iMod ((Views_alloc _ ρ) with "[$HV]") as "[AV' FV']"; first done.
+
+ iSplitR "HP FV' HFork"; last by (iApply ("HFork" with "[//] [//] [$FV']")).
do 2 iModIntro.
iMod ("HClose" with "[-Post FV]"); last by iApply "Post".
- iNext. iExists ς', (<[ρ:=Excl V]> VIEW). iExists HIST, INFO.
+ iNext. iExists ς, (<[ρ:=Excl V]> VIEW). iExists HIST, INFO.
iFrame (H3) "∗".
- iSplit;[|iSplit]; iPureIntro.
- + rewrite -H0 /VInv TUpd !fmap_insert.
- move : H4. rewrite -H0 lookup_fmap ViewOf /=. by move => [->].
- + rewrite /HInv MemOld NATSOld. by apply H1.
- + by rewrite /IInv MemOld.
+ iSplit;[|iSplit]; iPureIntro; [|done|done].
+ move => ? ?.
+ by rewrite lookup_insert_Some => [] [[_ [<- //]]|[_ /H0 //]].
Qed.
\ No newline at end of file
diff --git a/coq/ra/base/ghosts.v b/coq/ra/base/ghosts.v
index 50c74535..875c6831 100644
--- a/coq/ra/base/ghosts.v
+++ b/coq/ra/base/ghosts.v
@@ -182,18 +182,19 @@ Section GhostDefs.
Definition Info : loc -> frac -> dec_agree InfoT -> iProp Σ :=
λ l q v, own IN (◯ ({[l := (q, v)]})).
- Definition HInv ς HIST : Prop :=
- dom _ (HIST) ≡ locs (mem ς) ∧
- ∀ l h, (HIST !! l = Some (Excl h)
- →
+ Definition LInv ς l h :=
∃min_[rel_of (hTime l) (⊑)] vV ∈ h,
nats ς !! l ⊑ snd vV !! l
∧ h ≡ map_vt (hist_from_opt (mem ς) l (snd vV !! l))
∧ ∀ v V, (v, V) ∈ h ∖ {[vV]} → isval v
- ).
+ .
+
+ Definition HInv ς HIST : Prop :=
+ dom _ (HIST) ≡ locs (mem ς) ∧
+ ∀ l h, HIST !! l = Some (Excl h) → LInv ς l h.
Definition VInv ς VIEW : Prop :=
- Excl <$> threads ς = VIEW.
+ ∀ π V, VIEW !! π = Some (Excl V) → view_ok (mem ς) V.
Definition IInv ς INFO: Prop :=
dom (gset _) INFO ≡ locs (mem ς).
@@ -213,7 +214,7 @@ Section GhostDefs.
Definition DInv HIST : iProp Σ :=
[∗ map] l↦hh ∈ HIST,
match hh with
- | Excl h => ∀ V, ⌜(h: History) = {[D, V]}⌝ → Hist l h ∗ ∃ v, Info l 1 v
+ | Excl h => ∀ V, ⌜(h: History) ≡ {[D, V]}⌝ → Hist l h ∗ ∃ v, Info l 1 v
| _ => False
end
.
@@ -233,6 +234,8 @@ Section GhostDefs.
End GhostDefs.
+Arguments LInv _ _ _ /.
+
Definition physN : namespace := nroot .@ "phys".
Notation PSCtx := (inv physN PSInv).
@@ -560,7 +563,7 @@ Section UpdateGhosts.
last by rewrite (lookup_insert HIST l (Excl h')).
rewrite HDel.
iIntros "[_ $]".
- iIntros (?) "%". exfalso. by eapply NotD.
+ iIntros (?) "%". exfalso. eapply NotD. by apply/leibniz_equiv.
Qed.
Lemma DInv_update_return l h (h': History) (HIST: Hists)
@@ -576,7 +579,7 @@ Section UpdateGhosts.
last by rewrite lookup_insert.
rewrite HDel.
iIntros "[HInfo [HHist [_ $]]]".
- iIntros (?) "%". iFrame "HInfo". by rewrite H.
+ iIntros (?) "%". by iFrame "HInfo".
Qed.
Close Scope I.
diff --git a/coq/ra/base/helpers.v b/coq/ra/base/helpers.v
index 5b7f7a92..51e411b2 100644
--- a/coq/ra/base/helpers.v
+++ b/coq/ra/base/helpers.v
@@ -6,16 +6,14 @@ From ra Require Export ghosts.
Set Bullet Behavior "Strict Subproofs".
-Lemma init_pre_helper ς π h t l V_l v V
+Lemma init_pre_helper ς h t l V_l v V
(Hinv: phys_inv ς)
(HH : h ≡ map_vt (hist_from (mem ς) l t))
- (HV : threads ς !! π = Some V_l)
(In: (v, V) ∈ h)
(IsVal: isval v)
(Local: V !! l ⊑ V_l !! l)
(HVal : val_but_min l h)
- (MSOK: msgs_ok (mem ς))
- : init_pre ς π l.
+ : init_pre ς V_l l.
Proof.
assert ((v, V) ∈ h). { by apply In. }
move: In. rewrite HH /map_vt elem_of_map_gset.
@@ -25,7 +23,7 @@ Proof.
rewrite /msg_ok in VT. rewrite VT in Local.
destruct (V_l !! mloc m) as [tl|] eqn: HVT; last done.
econstructor; eauto.
- apply (init_time_mono _ _ (mtime m)); last auto.
+ apply (init_time_mono _ _ (mtime m)); [..|auto|by auto].
assert (Alloc := IAlloc _ Hinv _ Hm3). inversion IsVal as [v0 VEq].
rewrite /AllocInv -VEq in Alloc.
eapply allocated_next_init; eauto.
@@ -40,14 +38,13 @@ Proof.
eapply Pos.lt_le_incl, Pos.le_lt_trans; eauto.
Qed.
-Lemma alloc_pre_helper ς π h t l V_l
+Lemma alloc_pre_helper ς h t l V_l
(Hinv: phys_inv ς)
(HH : h = map_vt (hist_from (mem ς) l t))
- (HV : threads ς !! π = Some V_l)
(Alloc : alloc_local h V_l)
(HVal : val_but_min l h)
(MSOK: msgs_ok (mem ς))
- : alloc_pre ς π l.
+ : alloc_pre ς V_l l.
Proof.
destruct Alloc as [v [V [In [Local ND]]]].
assert (In1: (v, V) ∈ h). { by apply In. }
@@ -62,9 +59,10 @@ Proof.
assert (Alloc := IAlloc _ Hinv _ Hm3). rewrite /AllocInv in Alloc.
destruct (mval m) eqn: vEq => //; last first.
+ apply init_is_alloc.
- assert (Init: init_pre ς π (mloc m)). { by eapply init_pre_helper. }
- inversion Init. rewrite ViewOf in HV.
- inversion HV. subst. rewrite HVT in Local0. by simplify_option_eq.
+ have Init: init_pre ς (mview m) (mloc m) by eapply init_pre_helper.
+ inversion Init.
+ apply: init_time_mono; first exact: Init0.
+ have := (Local (mloc m)). by rewrite HVT Local0.
+ destruct HVal as [[v0 V0] [In0 [Min0 Val]]].
assert (EqvV: (v0, V0) = (A, mview m)).
{ case (decide ((v0, V0) = (A, mview m))) => [//|NEq].
diff --git a/coq/ra/base/na_read.v b/coq/ra/base/na_read.v
index 3b0c9809..7552c034 100644
--- a/coq/ra/base/na_read.v
+++ b/coq/ra/base/na_read.v
@@ -3,8 +3,8 @@ From ra.base Require Import na_shared.
Lemma f_read_na `{fG : foundationG Σ} π V_l l h :
{{{ PSCtx ∗ ▷ Seen π V_l ∗ ▷ Hist l h
∗ ⌜na_safe l h V_l⌝ ∗ ⌜init_local h V_l⌝ }}}
- ([ #l ]_na, π) @ ↑physN
- {{{ (v: Z) V', RET (#v, π);
+ ([ #l ]_na, V_l) @ ↑physN
+ {{{ (v: Z) V', RET (#v, V');
⌜V_l ⊑ V'⌝ ∗ Seen π V' ∗ Hist l h ∗ ⌜na_safe l h V'⌝
∗ ∃ V_1, ⌜V_1 ⊑ V'⌝ ∗ ⌜V_1 !! l = V' !! l⌝
∗ ⌜value_at_hd l h V_1 (VInj v)⌝ }}}.
@@ -17,8 +17,6 @@ Proof.
destruct H4 as [HInv1 HInv2]. symmetry in H3.
move: (HInv2 _ _ H3) => [[v0 V0] [In0 [Min0 [/= NA0 [Eqh Val]]]]].
- destruct (threads ς !! π) as [Vl|] eqn:HV1; last done. cbn in H1.
- move: H2 => [H2].
assert (VBM: val_but_min l h).
{ exists (v0, V0). repeat split; [auto|auto|by move => []]. }
@@ -40,24 +38,23 @@ Proof.
(* TODO : so many weird obligations *)
assert (V0 !! l ⊑ V !! l).
{ apply (Min0 _ InV). }
- assert (Le0: V0 !! l ⊑ Vl !! l).
+ assert (Le0: V0 !! l ⊑ V_l !! l).
{ rewrite H4 (Local _). by subst. }
- assert (∃ t1, Vl !! l = Some t1) as [t1 EqV1].
- { destruct (Vl !! l) eqn:Eqt1; [auto| by rewrite EqV0 in Le0].
+ assert (∃ t1, V_l !! l = Some t1) as [t1 EqV1].
+ { destruct (V_l !! l) eqn:Eqt1; [auto| by rewrite EqV0 in Le0].
by eexists. }
- assert (HVl: Vl !! l = V !! l).
- { apply: anti_symm; last first.
- - cbn in H2. by rewrite -H2.
- - destruct (ITOk _ H1 _ _ HV1 _ _ EqV1)
- as [m' [Hm'1 [Hm'2 [Hm'3 Hm'4]]]].
- destruct (IMOk _ H1 _ Hm'1) as [VT' _].
- rewrite EqV1 -Hm'3.
- destruct (decide (t ⊑ mtime m')) as [TLe|TGt].
- + rewrite -VT' Hm'2. apply (Max (mval m',_)).
- rewrite Eqh2 elem_of_map_gset. exists m'.
- by rewrite elem_of_hist_from.
- + apply Pos.lt_nle in TGt. etrans; eauto. rewrite EqV0.
- by apply Pos.lt_le_incl. }
+ assert (HVl: V_l !! l = V !! l).
+ { apply: anti_symm; last by auto.
+ destruct (H2 _ _ EqV1)
+ as [m' [Hm'1 [Hm'2 [Hm'3 Hm'4]]]].
+ destruct (IMOk _ H1 _ Hm'1) as [VT' _].
+ rewrite EqV1 -Hm'3.
+ destruct (decide (t ⊑ mtime m')) as [TLe|TGt].
+ - rewrite -VT' Hm'2. apply (Max (mval m',_)).
+ rewrite Eqh2 elem_of_map_gset. exists m'.
+ by rewrite elem_of_hist_from.
+ - apply Pos.lt_nle in TGt. etrans; eauto. rewrite EqV0.
+ by apply Pos.lt_le_incl. }
have : (∃ m, (v,V) = (mval m, mview m) ∧ m ∈ (hist_from (mem ς) l t))
=> [|[m [[Eqv EqV] Inm]]].
@@ -84,35 +81,31 @@ Proof.
rewrite Eqh2 elem_of_map_gset. exists m0.
by rewrite elem_of_hist_from.
* apply Pos.lt_nle in TGt. etrans; eauto. by apply Pos.lt_le_incl.
- - apply: (init_pre_helper _ _ _ t _ _ v V); eauto.
- + by rewrite HVl.
- + apply H1.
+ - exact: (init_pre_helper).
- (* frame update and re-establish the PSInv *)
- iNext. iIntros (v1 ς') "[% [% [% HP]]]".
-
- inversion H7. rewrite HV1 in ViewOf. inversion ViewOf. subst V1.
+ iNext. iIntros (v1 ς' V') "(% & % & % & % & HP)".
+ inversion H8.
+ (* inversion H7. rewrite HV1 in ViewOf. inversion ViewOf. subst V1. *)
- assert (threads ς' !! π = Some V' ∧ Vl ⊑ V') as [HV'1 HV'2].
- { split.
- - by rewrite TUpd lookup_insert.
- - rewrite VUpd; apply join_ext_l. }
+ (* assert (VIEW ς' !! π = Some V' ∧ Vl ⊑ V') as [HV'1 HV'2]. *)
+ (* { split. *)
+ (* - by rewrite TUpd lookup_insert. *)
+ (* - rewrite VUpd; apply join_ext_l. } *)
iApply ("Post" $! _ V').
iMod ("HClose" $! ς' V' h with "[DInv $HP]") as "[Seen' Hist']".
{ rewrite (insert_id HIST); last auto.
(* re-establish PSInv *)
- iFrame (H5 H6) "∗". rewrite HV'1.
- iSplit;[|iSplit]; try (iNext; iAssumption); iPureIntro; [done| |].
- - by rewrite /VInv TUpd fmap_insert.
- - by rewrite /HInv MOld NATSOld. }
+ iFrame (H5 H6 H7) "∗".
+ by rewrite /HInv /= MOld NATSOld. }
(* show post-condition *)
iModIntro. iFrame "Hist' Seen'". repeat (iSplit; auto).
- + iPureIntro. etrans; eauto. by subst.
- + iPureIntro. exists (v, V). repeat (split; auto). do 2 (etrans; eauto). by subst.
+ + iPureIntro. subst. solve_jsl.
+ + iPureIntro. exists (v, V). repeat (split; auto). subst. do 2 (etrans; eauto). by subst. solve_jsl.
+ iExists (mview m0). destruct (IMOk _ H1 _ In) as [EqT _]. subst.
rewrite -EqLoc EqT. repeat iSplit; iPureIntro.
- * apply join_ext_r.
+ * solve_jsl.
* rewrite lookup_join_max EqT.
apply (anti_symm extension); first by apply join_ext_r.
apply join_least; last by reflexivity.
diff --git a/coq/ra/base/na_shared.v b/coq/ra/base/na_shared.v
index cf4f9879..b9e1b635 100644
--- a/coq/ra/base/na_shared.v
+++ b/coq/ra/base/na_shared.v
@@ -24,13 +24,13 @@ Proof.
apply set_unfold_2; abstract naive_solver.
- move => l0 V0.
case: (decide (l = l0)) => [<- {l0}|?]; last first.
- + rewrite NATSUpd lookup_insert_ne; last auto.
+ + rewrite /LInv NATSUpd lookup_insert_ne; last auto.
move/(proj2 HInvς) => [m' [? [? [? [H ?]]]]].
exists m'. rewrite lookup_insert_ne; last auto.
split; last split; last split; last split; auto.
rewrite MUpd H. rewrite /map_vt /hist_from_opt. clear H.
apply set_unfold_2. abstract naive_solver.
- + rewrite MUpd NATSUpd lookup_insert => [[<- {V0}]].
+ + rewrite /LInv MUpd NATSUpd lookup_insert => [[<- {V0}]].
exists (mval m, mview m).
rewrite lookup_insert.
setoid_rewrite elem_of_singleton.
diff --git a/coq/ra/base/na_write.v b/coq/ra/base/na_write.v
index a57e15ba..c006cdbd 100644
--- a/coq/ra/base/na_write.v
+++ b/coq/ra/base/na_write.v
@@ -3,8 +3,8 @@ From ra.base Require Import na_shared.
Lemma f_write_na `{fG : !foundationG Σ} π V_l l h v:
{{{ PSCtx
∗ ▷ Seen π V_l ∗ ▷ Hist l h ∗ ⌜alloc_local h V_l⌝ }}}
- ([ #l ]_na <- #v, π) @ ↑physN
- {{{ V' h', RET (#(), π);
+ ([ #l ]_na <- #v, V_l) @ ↑physN
+ {{{ V' h', RET (#(), V');
⌜V_l ⊑ V'⌝ ∗ Seen π V' ∗ Hist l h'
∗ ⌜init_local h' V'⌝ ∗ ⌜na_safe l h' V'⌝ ∗ ⌜init l h'⌝
∗ ⌜value_at_hd l h' V' (VInj v)⌝
@@ -18,7 +18,6 @@ Proof.
destruct H3 as [HInv1 HInv2]. symmetry in H2.
move: (HInv2 _ _ H2) => [[v0 V0] [In0 [Min0 [/= NA0 [Eqh Val]]]]].
- destruct (threads ς !! π) as [Vl|] eqn:HV1; last done. cbn in H1.
assert (∃ t, V0 !! l = Some t) as [t EqV0].
{ apply (elem_of_hist_view_ok v0 _ (mem ς) _ (V0 !! l)).
@@ -29,25 +28,20 @@ Proof.
{ move: Eqh; set_solver+. }
destruct H as [v' [V' [In' [Local' IsND']]]].
- move: H1 => [H1].
- iApply (wp_store_na_pst with "oPS"); first eauto.
+ (* move: H1 => [H1]. *)
+ iApply (wp_store_na_pst with "oPS"); [eauto|auto|..].
- (* drf_pre ς π l *)
- econstructor; eauto. rewrite -H1 NA0. by move : (Min0 _ In') => /= ->.
+ econstructor; eauto. rewrite NA0. by move : (Min0 _ In') => /= ->.
- (* alloc_pre ς π l *)
eapply alloc_pre_helper; eauto.
- + eapply alloc_local_Mono; first by rewrite H1. exists v', V'. by erewrite <- Eqh2.
+ + eapply alloc_local_Mono; first by auto. exists v', V'. by erewrite <- Eqh2.
+ exists (v0, V0). repeat setoid_rewrite <-Eqh2.
split; first auto. split; first auto. by move => [].
+ apply H0.
- (* frame update and re-establish the PSInv *)
- iNext. iIntros (ς') "(% & % & % & HP)".
+ iNext. iIntros (ς' V'') "(% & % & % & % & HP)".
- inversion H4. rewrite HV1 in ViewOf. inversion ViewOf. subst Vl.
-
- assert (threads ς' !! π = Some V'0 ∧ V ⊑ V'0) as [HV'1 HV'2].
- { split.
- - by rewrite TUpd lookup_insert.
- - rewrite VUpd; apply join_ext_l. }
+ inversion H5.
(* get h' *)
pose (h' := {[(mval m, mview m)]}: History).
@@ -55,28 +49,27 @@ Proof.
assert (HInv': HInv ς' (<[l:=Excl h']> HIST)). {
eapply (write_na_update_HInv ς) => //. apply H. }
- iApply ("Post" $! V'0 h').
- iMod ("HClose" $! ς' V'0 h' with "[DInv $HP]") as "[Seen' Hist']".
+ iApply ("Post" $! _ _).
+ iMod ("HClose" $! ς' _ h' with "[DInv $HP]") as "[Seen' Hist']".
{ (* re-establish PSInv *)
- iFrame (H H3 HInv'). iSplit; first by rewrite HV'1.
- iSplitR "".
- - iNext. iApply (DInv_update_value with "DInv"); last eauto.
- move => VD. rewrite /h' EqVal => Eq.
- assert (EqD: (VInj v, mview m) = (D, VD)).
- { by rewrite -(elem_of_singleton (C:= History))
- -Eq elem_of_singleton. }
- by inversion EqD.
- - by rewrite /VInv TUpd !fmap_insert. }
+ iFrame (H H3 H4 HInv').
+ iNext. iApply (DInv_update_value with "DInv"); last eauto.
+ move => VD. rewrite /h' EqVal => Eq.
+ assert (EqD: (VInj v, mview m) = (D, VD)).
+ { by rewrite -(elem_of_singleton (C:= History))
+ -Eq elem_of_singleton. }
+ by inversion EqD.
+ }
(* show post-condition *)
(* TODO : redundant proofs *)
iModIntro. iFrame "Hist' Seen'". rewrite /h'.
rewrite EqVal EqView.
repeat iSplitL ""; last done; iPureIntro.
- + by rewrite H6.
- + exists (VInj v), V'0. by rewrite elem_of_singleton.
+ + rewrite VUpd. solve_jsl.
+ + eexists (VInj v), _. by rewrite elem_of_singleton.
+ exists (VInj v, mview m). rewrite -EqView. abstract set_solver+.
- + exists (VInj v), V'0. by rewrite elem_of_singleton.
- + exists (VInj v, V'0) => /=. abstract set_solver+.
- + exists (VInj v, V'0). abstract set_solver+.
+ + eexists (VInj v), _. by rewrite elem_of_singleton.
+ + exists (VInj v, V''). abstract set_solver+.
+ + exists (VInj v, V''). abstract set_solver+.
Qed.
\ No newline at end of file
diff --git a/coq/ra/examples/message_passing.v b/coq/ra/examples/message_passing.v
index ed1d2997..361b85d1 100644
--- a/coq/ra/examples/message_passing.v
+++ b/coq/ra/examples/message_passing.v
@@ -95,7 +95,7 @@ Section proof.
iApply (f_fork _ ((x ↦ 0) V_l ∗ [PP y in false @ () | mpInt x γ ] V_l)%I
with "[$kI $kS $SndT Post Tok]").
iSplitL "Post Tok".
- - iNext. iIntros "kS".
+ - iNext. iViewUp. iIntros "kS".
wp_seq. iNext. wp_bind ((rec: "f" <> := _ ) _)%E.
(iLöb as "IH" forall (V_l) "kIp yPRT ∗").
(* TODO: kIp is a spurious dependency *)
@@ -128,7 +128,7 @@ Section proof.
iApply ("IH" $! _ with "[kIp] [yPRT5] Post Tok kS").
{ iIntros "!#"; iFrame "kIp". }
{ iIntros "!#"; iFrame "yPRT5". }
- - iNext. iIntros (ρ) "(_ & kS & Nax & #yPRT')".
+ - iNext. iIntros (ρ). iViewUp. iIntros "_ kS (Nax & #yPRT')". move: HV => ->.
wp_bind ([_]_na <- _)%E.
iApply (na_write with "[%] kI kS [$Nax]"); [done|done|].
iNext. iViewUp; iIntros "kS Nax".
@@ -142,7 +142,7 @@ Section proof.
(* write release to final state *)
iApply (GPS_PP_Write (p:=()) (mpInt x γ) true (XE x γ) (λ _, True)
- with "[%] kI kS [$yPRT' XE]"); [done|done|move=>[|]; done|done|..].
+ with "[%] kI kS [yPRT' XE]"); [done|done|move=>[|]; done|done|..].
{ iSplitL ""; [|by iFrame "XE"].
iNext. iViewUp; iIntros "[oL _]". iModIntro.
iSplitL ""; [done|]. iSplit; iNext; auto. by iFrame "oL". }
diff --git a/coq/ra/examples/message_passing_base.v b/coq/ra/examples/message_passing_base.v
index 31db5e54..f32ae78f 100644
--- a/coq/ra/examples/message_passing_base.v
+++ b/coq/ra/examples/message_passing_base.v
@@ -32,8 +32,8 @@ Section proof.
Lemma message_passing_base_spec V π:
{{{ PSCtx ∗ Seen π V }}}
- (message_passing, π)
- {{{ V' (v: Z), RET (#v, π); ⌜V ⊑ V'⌝ ∗ Seen π V' ∗ ⌜v = 37⌝ }}}.
+ (message_passing, V)
+ {{{ V' (v: Z), RET (#v, V'); ⌜V ⊑ V'⌝ ∗ Seen π V' ∗ ⌜v = 37⌝ }}}.
Proof.
iIntros (Φ) "(#kI & kS) Post". rewrite /message_passing.
@@ -78,28 +78,32 @@ Section proof.
iApply (f_fork _ (Hist x {[VInj 0, V3]} ∗ Info x 1 vx)%I
with "[$kI $kS $SndT Post Tok]").
iSplitL "Post Tok"; iNext.
- - iIntros "kS".
+ - iIntros (V') "% kS".
wp_seq. iNext. wp_bind ((rec: "f" <> := _ ) _)%E.
- move EqV4 : {2}V4 => V5.
- have H6: V4 ⊑ V5 by subst. clear EqV4.
- iLöb as "IH" forall (V5 H6) "Invy ∗".
+ move EqV4 : {1}V4 => V5.
+ have H6: V4 ⊑ V5 by subst.
+ have H7: V5 ⊑ V' by subst.
+ clear EqV4.
+ iLöb as "IH" forall (V' H4 V5 H6 H7) "Invy ∗".
iApply wp_repeat; first auto.
iInv mpN as (hy') "(Histy & Infoy & >% & #Invx)" "HClose".
iApply wp_mask_mono; last
iApply (f_read_at with "[$kI $kS $Histy]"); first solve_ndisj.
- { iPureIntro. by exists (VInj 0), V4. }
+ { iPureIntro. by exists (VInj 0), V5. }
iNext. iIntros (v V6) "(% & kS & Histy & _ & HRead)".
iMod ("HClose" with "[Histy Infoy]") as "_".
- { iNext. iExists hy'. iFrame "Histy Infoy". iFrame (H4) "Invx". }
+ { iNext. iExists hy'. iFrame "Histy Infoy". iFrame (H8) "Invx". }
iModIntro. iExists v. iSplit; first auto.
case (decide (v = 0)) =>[Eq0|NEq0].
{ subst v. iNext. iNext.
- iApply ("IH" $! _ with "[%] [] Post Tok kS").
- - by etrans.
- - iIntros "!#". iFrame "Invy". }
+ iApply ("IH" $! _ with "[%] [%] [%] [$Invy] Post Tok kS").
+ - by rewrite H6 H7.
+ - by rewrite H6.
+ - by rewrite H7.
+ }
iClear "IH Invy". iNext. iNext. wp_seq. iNext.
- iDestruct "HRead" as (V_1) "%". destruct H8 as (H81 & H82 & H83).
+ iDestruct "HRead" as (V_1) "%". destruct H10 as (H81 & H82 & H83).
iDestruct ("Invx" $! V_1 v with "[%]") as (V37) "[% #Invx2]"; first done.
iClear "Invx".
iInv mpN as "Disj" "HClose".
@@ -119,18 +123,18 @@ Section proof.
iNext. iIntros (v' V7) "(% & kS & Histx & _ & Hv37)".
iMod ("HClose" with "[Tok]") as "_". { iNext. by iLeft. }
- iDestruct "Hv37" as (V') "(_&_&%)".
- move: H10 => [vV [/elem_of_singleton -> [_ [Eqv EqV]]]]. subst v'.
+ iDestruct "Hv37" as (V'') "(_&_&%)".
+ move: H12 => [vV [/elem_of_singleton -> [_ [Eqv EqV]]]]. subst v'.
iApply ("Post" $! V7 with "[$kS]"). iSplit; last done.
iPureIntro. repeat (etrans; eauto).
- - iIntros (ρ) "(_ & kS & Histx & Infox)".
+ - iIntros (ρ V') "% _ kS [Histx Infox]".
wp_bind ([_]_na <- _)%E.
iApply wp_mask_mono; [auto|];
last iApply (f_write_na with "[$kI $kS $Histx]").
{ iPureIntro.
- apply (alloc_local_Mono _ _ _ H5). by apply alloc_init_local. }
+ apply: (alloc_local_Mono); last exact: alloc_init_local. by rewrite H5. }
iNext. iIntros (V5 hx') "(% & kS & Histx & %)".
- destruct H6 as (_&_&_&_&H6). subst hx'.
+ destruct H7 as (_&_&_&_&H7). subst hx'.
iMod (inv_alloc mpN top (Invx x γ V5)%I with "[Histx Infox]") as "Invx".
{ iNext. iRight. iFrame "Histx". by iExists _. }
wp_seq. iNext.
@@ -138,18 +142,18 @@ Section proof.
iDestruct "Invx" as "#Invx".
iApply wp_mask_mono; last iApply (f_write_at with "[$kI $kS $Histy]");
first solve_ndisj.
- { iPureIntro. by exists (VInj 0), V4. }
+ { iPureIntro. exists (VInj 0), V4; split; [|split]; auto. by rewrite H4. }
iNext. iIntros (V6 hy2) "(% & kS & Histy & %)".
iMod ("HClose" with "[Histy Infoy]") as "_"; last done.
iNext. iExists hy2. iFrame "Histy Infoy".
- destruct H8 as (H81 & H82 & H83 & H84 & H85). iSplit.
- + iPureIntro. rewrite H83 elem_of_union. by right.
+ destruct H9 as (H91 & H92 & H93 & H94 & H95). iSplit.
+ + iPureIntro. rewrite H93 elem_of_union. by right.
+ iIntros "!#".
- iIntros (V' v'). iIntros (HV).
- move: HV. rewrite H83 elem_of_union elem_of_singleton.
+ iIntros (V'' v'). iIntros (HV).
+ move: HV. rewrite H93 elem_of_union elem_of_singleton.
move => [Hv [[Eqv EqV]|HV]].
- * subst V'. iExists V5. by iFrame "Invx".
- * by iApply ("Invxs" $! V' v').
+ * subst V''. iExists V5. by iFrame "Invx".
+ * by iApply ("Invxs" $! _ v').
Qed.
End proof.
\ No newline at end of file
diff --git a/coq/ra/examples/repeat.v b/coq/ra/examples/repeat.v
index 2b10acca..c679a690 100644
--- a/coq/ra/examples/repeat.v
+++ b/coq/ra/examples/repeat.v
@@ -32,14 +32,10 @@ Lemma wp_repeat `{ownPG ra_lang Σ} E e π Φ `{base.is_closed nil e} :
WP ((e, π) : ra_lang.expr) @ E
{{ v, ∃ z, ⌜v.1 = LitV $ LitInt z⌝
∧ if decide (z = 0)
- then ▷ ▷ (WP (repeat e, π) @ E {{v, Φ v }}) else ▷ ▷ Φ (#z, π) }}
+ then ▷ ▷ (WP (repeat e, v.2) @ E {{v, Φ v }}) else ▷ ▷ Φ (#z, v.2) }}
⊢ WP (repeat e, π) @ E {{ Φ }}.
Proof.
iIntros "H".
- iDestruct (wp_thread E (λ v, ∃ z, ⌜v.1 = LitV $ LitInt z⌝
- ∧ if decide (z = 0)
- then ▷ ▷ (WP (repeat e, v.2) @ E {{v, Φ v }})
- else ▷ ▷ Φ (#z, v.2) )%I (e, π) with "H") as "H".
wp_rec. iNext.
wp_bind e. iApply wp_mono; [|iExact "H"].
iIntros (v) "H". iDestruct "H" as (l) "(% & R)". rewrite H0 {H0}.
diff --git a/coq/ra/gps/cas.v b/coq/ra/gps/cas.v
index 4ee916a6..08754e44 100644
--- a/coq/ra/gps/cas.v
+++ b/coq/ra/gps/cas.v
@@ -37,8 +37,8 @@ Section CAS.
∗ ▷ (gps_inv IP l γ γ_x) ∗ P V
∗ exwr γ_x q (s_x, (v_x, V_x))
∗ Reader γ {[s_r, (v_r, V_r)]} }}}
- (CAS #l #v_o #v_n, π) @ E
- {{{ s'' (b: bool) v Vr V', RET (#b, π) ;
+ (CAS #l #v_o #v_n, V) @ E
+ {{{ s'' (b: bool) v Vr V', RET (#b, V') ;
⌜V ⊑ V'⌝ ∗ Seen π V' ∗ ⌜s_r ⊑ s''⌝
∗ ▷ (gps_inv IP l γ γ_x) ∗ (if b then Q s'' else R s'' v) V'
∗ exwr γ_x q (s_x, (v_x, V_x))
@@ -281,8 +281,8 @@ Section CAS.
∗ exwr γ_x q (s_x, (v_x, V_x))
∗ Reader γ {[s_r, (v_r, V_r)]}
∗ (∃ ζ, Writer γ ζ) }}}
- (CAS #l #v_o #v_n, π) @ E
- {{{ s'' (b: bool) v Vr V', RET (LitV $ LitInt b, π) ;
+ (CAS #l #v_o #v_n, V) @ E
+ {{{ s'' (b: bool) v Vr V', RET (LitV $ LitInt b, V') ;
⌜V ⊑ V'⌝ ∗ Seen π V' ∗ ⌜s_r ⊑ s''⌝
∗ ▷ (gps_inv IP l γ γ_x) ∗ (if b then Q s'' else R s'' v) V'
∗ exwr γ_x q (s_x, (v_x, V_x))
diff --git a/coq/ra/gps/fai.v b/coq/ra/gps/fai.v
index 11b825fd..ad5500cc 100644
--- a/coq/ra/gps/fai.v
+++ b/coq/ra/gps/fai.v
@@ -30,8 +30,8 @@ Section FAI.
∗ exwr γ_x q (s_x, (v_x, V_x))
∗ Reader γ {[s_r, (v_r, V_r)]}
∗ (∃ ζ, Writer γ ζ) }}}
- (FAI C #l, π) @ E
- {{{ s'' (v: Z) Vr V', RET (#v, π) ;
+ (FAI C #l, V) @ E
+ {{{ s'' (v: Z) Vr V', RET (#v, V') ;
⌜V ⊑ V'⌝ ∗ Seen π V' ∗ ⌜s_r ⊑ s''⌝
∗ ▷ (gps_inv IP l γ γ_x) ∗ Q s'' v V'
∗ exwr γ_x q (s_x, (v_x, V_x))
diff --git a/coq/ra/gps/init.v b/coq/ra/gps/init.v
index 1ee841d6..c2f4fdb0 100644
--- a/coq/ra/gps/init.v
+++ b/coq/ra/gps/init.v
@@ -23,8 +23,8 @@ Section Init_Strong.
(HEN : ↑physN ⊆ E):
{{{ PSCtx ∗ Seen π V
∗ ▷ Hist l h ∗ ⌜alloc_local h V⌝ }}}
- ([ #l ]_na <- #v, π) @ E
- {{{ V' γ γ_x, RET (#(), π) ;
+ ([ #l ]_na <- #v, V) @ E
+ {{{ V' γ γ_x, RET (#(), V') ;
⌜V ⊑ V'⌝ ∗ Seen π V'
∗ (▷ F γ (s γ) v V' ∗ ▷ F_past γ (s γ) v V' -∗ ▷ (gps_inv (IP γ) l γ γ_x))
∗ exwr γ_x 1%Qp ((s γ), (v, V'))
@@ -104,8 +104,8 @@ Section Init.
{{{ PSCtx ∗ Seen π V
∗ ▷ Hist l h ∗ ⌜alloc_local h V⌝
∗ ▷ F s v V ∗ ▷ F_past s v V}}}
- ([ #l ]_na <- #v, π) @ E
- {{{ V' γ γ_x, RET (#(), π) ;
+ ([ #l ]_na <- #v, V) @ E
+ {{{ V' γ γ_x, RET (#(), V') ;
⌜V ⊑ V'⌝ ∗ Seen π V'
∗ ▷ (gps_inv IP l γ γ_x)
∗ exwr γ_x 1%Qp (s, (v, V'))
diff --git a/coq/ra/gps/read.v b/coq/ra/gps/read.v
index 16a3f487..ec61e0e1 100644
--- a/coq/ra/gps/read.v
+++ b/coq/ra/gps/read.v
@@ -26,8 +26,8 @@ Section Read.
∗ PSCtx ∗ Seen π V
∗ ▷ (gps_inv IP l γ γ_x) ∗ P V
∗ Reader γ {[s_r, (v_r, V_r)]} }}}
- ([ #l ]_at, π) @ E
- {{{ s' v Vr V', RET (#v, π) ;
+ ([ #l ]_at, V) @ E
+ {{{ s' v Vr V', RET (#v, V') ;
⌜V ⊑ V'⌝ ∗ Seen π V' ∗ ⌜s_r ⊑ s'⌝
∗ ▷ (gps_inv IP l γ γ_x) ∗ Q s' v V'
∗ Reader γ {[s', (v, Vr)]} ∗ ⌜Vr ⊑ V'⌝ ∗ ⌜V !! l ⊑ Vr !! l⌝}}}.
@@ -127,8 +127,8 @@ Section Read.
∗ exwr γ_x 1%Qp (s, (v, V))
∗ Reader γ {[s, (v, V)]}
∗ Writer γ ζ }}}
- ([ #l ]_at, π) @ E
- {{{ v' V', RET (#v', π) ;
+ ([ #l ]_at, Vl) @ E
+ {{{ v' V', RET (#v', V') ;
⌜Vl ⊑ V'⌝ ∗ Seen π V'
∗ ▷ (gps_inv IP l γ γ_x) ∗ F_past s v' V'
∗ exwr γ_x 1%Qp (s, (v, V))
diff --git a/coq/ra/gps/write.v b/coq/ra/gps/write.v
index e38fd63d..b26c3ca6 100644
--- a/coq/ra/gps/write.v
+++ b/coq/ra/gps/write.v
@@ -27,8 +27,8 @@ Section Write.
∗ exwr γ_x q (s_x, (v_x, V_x))
∗ Reader γ {[s_r, (v_r, V_r)]}
∗ Writer γ ζ }}}
- ([ #l ]_at <- #v, π) @ E
- {{{ V', RET (#(), π) ;
+ ([ #l ]_at <- #v, V) @ E
+ {{{ V', RET (#(), V') ;
⌜V ⊑ V'⌝ ∗ Seen π V'
∗ (▷ F s' v V' ∗ ▷ F_past s' v V' -∗ ▷ (gps_inv IP l γ γ_x))
∗ exwr γ_x q (s_x, (v_x, V_x))
@@ -166,8 +166,8 @@ Section Write.
∗ exwr γ_x 1%Qp (s_x, (v_x, V_x))
∗ Reader γ {[s_x, (v_x, V_x)]}
∗ Writer γ ζ }}}
- ([ #l ]_at <- #v, π) @ E
- {{{ V', RET (#(), π) ;
+ ([ #l ]_at <- #v, V) @ E
+ {{{ V', RET (#(), V') ;
⌜V ⊑ V'⌝ ∗ Seen π V'
∗ (▷ F s' v V' ∗ ▷ F_past s' v V' -∗ ▷ (gps_inv IP l γ γ_x))
∗ F s_x v_x V'
@@ -329,8 +329,8 @@ Section Write.
∗ exwr γ_x 1%Qp (s_x, (v_x, V_x))
∗ Reader γ {[s_x, (v_x, V_x)]}
∗ Writer γ ζ }}}
- ([ #l ]_at <- #v, π) @ E
- {{{ V', RET (#(), π) ;
+ ([ #l ]_at <- #v, V) @ E
+ {{{ V', RET (#(), V') ;
⌜V ⊑ V'⌝ ∗ Seen π V'
∗ (▷ F s' v V' ∗ ▷ F_past s' v V' -∗ ▷ (gps_inv IP l γ γ_x))
∗ F s_x v_x V'
diff --git a/coq/ra/lang.v b/coq/ra/lang.v
index e5809011..fedfbeae 100644
--- a/coq/ra/lang.v
+++ b/coq/ra/lang.v
@@ -297,8 +297,8 @@ Module base.
End base.
Module ra_lang.
- Definition expr : Type := base.expr * thread.
- Definition val : Type := base.val * thread.
+ Definition expr : Type := base.expr * View.
+ Definition val : Type := base.val * View.
Definition ectx_item := base.ectx_item.
Definition fill_item : _ -> _ -> expr := λ Ki e, (base.fill_item Ki (e.1), e.2).
Definition of_val : val -> expr := λ v, (base.of_val (v.1), v.2).
@@ -321,35 +321,35 @@ Module ra_lang.
(* Definition state := @machine.state base.loc _ _ Z _ _. *)
(* Definition event := @machine.event base.loc Z. *)
- Inductive step (π : thread)
+ Inductive step (V : View)
: ∀ (e : base.expr) (evt : event) (e' : base.expr) (ef : list expr), Prop :=
- | ForkS e ρ : (* π ≠ ρ ? *)
- step π
+ | ForkS e V' : (* π ≠ ρ ? *)
+ step V
(base.Fork e)
- (EFork ρ)
+ (EFork V')
(base.Lit base.LitUnit)
- [(e, ρ)]
+ [(e, V')]
| AllocS l:
- step π
+ step V
base.Alloc
(EWrite na l A)
(base.Lit $ base.LitLoc l)
[]
| DeallocS l :
- step π
+ step V
(base.Dealloc (base.Lit $ base.LitLoc l))
(EWrite na l D)
(base.Lit $ base.LitUnit)
[]
| LoadS (l : loc) (v : Z) acc :
- step π
+ step V
(base.Load acc (base.Lit $ base.LitLoc l))
(ERead acc l (VInj v))
(base.of_val (base.LitV $ base.LitInt v))
[]
| StoreS l e v acc :
base.to_val e = Some (base.LitV $ base.LitInt v) ->
- step π
+ step V
(base.Store acc (base.Lit $ base.LitLoc l) e)
(EWrite acc l (VInj v))
(base.Lit $ base.LitUnit)
@@ -358,7 +358,7 @@ Module ra_lang.
base.to_val e1 = Some (base.LitV $ base.LitInt v1) →
base.to_val e2 = Some (base.LitV $ base.LitInt v2) →
vl ≠ v1 →
- step π
+ step V
(base.CAS (base.Lit $ base.LitLoc l) e1 e2)
(ERead at_hack l (VInj vl))
(base.Lit $ base.LitInt false)
@@ -366,13 +366,13 @@ Module ra_lang.
| CasSucS l e1 v1 e2 v2 :
base.to_val e1 = Some (base.LitV $ base.LitInt v1) →
base.to_val e2 = Some (base.LitV $ base.LitInt v2) →
- step π
+ step V
(base.CAS (base.Lit $ base.LitLoc l) e1 e2)
(EUpdate l (VInj v1) (VInj v2))
(base.Lit $ base.LitInt true)
[]
| FAIS l C (v: Z):
- step π
+ step V
(base.FAI C (base.Lit $ base.LitLoc l))
(EUpdate l (VInj v) (VInj ((v + 1) `mod` Z.pos C)))
(base.Lit $ base.LitInt v)
@@ -383,10 +383,10 @@ Module ra_lang.
∀ (e : expr) (σ : state) (e' : expr) (σ' : state) (ef : list expr), Prop :=
| pure_step σ π e e' (BaseStep : base.head_step e e')
: head_step (e, π) σ (e', π) σ []
- | impure_step σ σ' π e e' ef evt
- (ExprStep : step π e evt e' ef)
- (MachStep : machine_red σ evt π σ')
- : head_step (e, π) σ (e', π) σ' ef
+ | impure_step σ σ' V V' e e' ef evt
+ (ExprStep : step V e evt e' ef)
+ (MachStep : machine_red σ evt V σ' V')
+ : head_step (e, V) σ (e', V') σ' ef
.
Lemma to_of_val v : to_val (of_val v) = Some v.
diff --git a/coq/ra/lifting.v b/coq/ra/lifting.v
index cb5a0675..3000bb88 100644
--- a/coq/ra/lifting.v
+++ b/coq/ra/lifting.v
@@ -93,56 +93,56 @@ Proof.
- move => ac. by rewrite H -IH.
Qed.
-Lemma wp_thread (E : coPset)
- (Φ : ra_lang.val → iProp Σ) e:
- WP e @ E {{ v, Φ (fst v, snd e) }} ⊢ WP e @ E {{ v, Φ v }}.
-Proof.
- (iLöb as "IH" forall (e)).
- rewrite ![in X in _ ⊢ X]wp_unfold.
- destruct e as [e π]. simpl. unfold wp_pre. case_match.
- + iIntros "H1". destruct v as [v π'].
- by rewrite (option_fmap_pair Heqo).
- + iIntros "H1".
- iIntros (σ) "O".
- iDestruct ("H1" $! σ with "O") as ">[$ H2]".
- iModIntro. iNext.
- iIntros (e2 σ2 ef2) "#T". iDestruct "T" as %Step.
- iMod ("H2" $! _ _ _ with "[%]") as "($ & I & $)"; [done|].
- inversion Step. simpl in *. simplify_eq.
- rewrite /fill /fill_item in H. rewrite foldl_pair //= in H.
- inversion H. subst.
- assert (snd e1' = snd e2').
- { inversion H1; by simplify_eq. }
- subst.
- rewrite /fill foldl_pair //= -H0.
- iApply ("IH" $! (_,_) with "I").
-Qed.
-
-
-Lemma wp_thread_rev (E : coPset)
- (Φ : ra_lang.val → iProp Σ) e:
- WP e @ E {{ v, Φ v }} ⊢ WP e @ E {{ v, Φ (fst v, snd e) }}.
-Proof.
- (iLöb as "IH" forall (e)).
- rewrite ![in X in _ ⊢ X]wp_unfold.
- destruct e as [e π]. simpl. unfold wp_pre. case_match.
- + iIntros "H1". destruct v as [v π'].
- by rewrite (option_fmap_pair Heqo).
- + iIntros "H1".
- iIntros (σ) "O".
- iDestruct ("H1" $! σ with "O") as ">[$ H2]".
- iModIntro. iNext.
- iIntros (e2 σ2 ef2) "#T". iDestruct "T" as %Step.
- iMod ("H2" $! _ _ _ with "[%]") as "($ & I & $)"; [done|].
- inversion Step. simpl in *. simplify_eq.
- rewrite /fill /fill_item in H. rewrite foldl_pair //= in H.
- inversion H. subst.
- assert (snd e1' = snd e2').
- { inversion H1; by simplify_eq. }
- subst.
- rewrite /fill foldl_pair //= -H0.
- iApply ("IH" $! (_,_) with "I").
-Qed.
+(* Lemma wp_thread (E : coPset) *)
+(* (Φ : ra_lang.val → iProp Σ) e: *)
+(* WP e @ E {{ v, Φ (fst v, snd e) }} ⊢ WP e @ E {{ v, Φ v }}. *)
+(* Proof. *)
+(* (iLöb as "IH" forall (e)). *)
+(* rewrite ![in X in _ ⊢ X]wp_unfold. *)
+(* destruct e as [e π]. simpl. unfold wp_pre. case_match. *)
+(* + iIntros "H1". destruct v as [v π']. *)
+(* by rewrite (option_fmap_pair Heqo). *)
+(* + iIntros "H1". *)
+(* iIntros (σ) "O". *)
+(* iDestruct ("H1" $! σ with "O") as ">[$ H2]". *)
+(* iModIntro. iNext. *)
+(* iIntros (e2 σ2 ef2) "#T". iDestruct "T" as %Step. *)
+(* iMod ("H2" $! _ _ _ with "[%]") as "($ & I & $)"; [done|]. *)
+(* inversion Step. simpl in *. simplify_eq. *)
+(* rewrite /fill /fill_item in H. rewrite foldl_pair //= in H. *)
+(* inversion H. subst. *)
+(* assert (snd e1' = snd e2'). *)
+(* { inversion H1; by simplify_eq. } *)
+(* subst. *)
+(* rewrite /fill foldl_pair //= -H0. *)
+(* iApply ("IH" $! (_,_) with "I"). *)
+(* Qed. *)
+
+
+(* Lemma wp_thread_rev (E : coPset) *)
+(* (Φ : ra_lang.val → iProp Σ) e: *)
+(* WP e @ E {{ v, Φ v }} ⊢ WP e @ E {{ v, Φ (fst v, snd e) }}. *)
+(* Proof. *)
+(* (iLöb as "IH" forall (e)). *)
+(* rewrite ![in X in _ ⊢ X]wp_unfold. *)
+(* destruct e as [e π]. simpl. unfold wp_pre. case_match. *)
+(* + iIntros "H1". destruct v as [v π']. *)
+(* by rewrite (option_fmap_pair Heqo). *)
+(* + iIntros "H1". *)
+(* iIntros (σ) "O". *)
+(* iDestruct ("H1" $! σ with "O") as ">[$ H2]". *)
+(* iModIntro. iNext. *)
+(* iIntros (e2 σ2 ef2) "#T". iDestruct "T" as %Step. *)
+(* iMod ("H2" $! _ _ _ with "[%]") as "($ & I & $)"; [done|]. *)
+(* inversion Step. simpl in *. simplify_eq. *)
+(* rewrite /fill /fill_item in H. rewrite foldl_pair //= in H. *)
+(* inversion H. subst. *)
+(* assert (snd e1' = snd e2'). *)
+(* { inversion H1; by simplify_eq. } *)
+(* subst. *)
+(* rewrite /fill foldl_pair //= -H0. *)
+(* iApply ("IH" $! (_,_) with "I"). *)
+(* Qed. *)
(** Base axioms for core primitives of the language: Stateless reductions *)
Lemma wp_rec E π f x erec e1 e2 Φ :
@@ -203,86 +203,75 @@ Qed.
(** Base axioms for core primitives of the language: Stateful reductions. *)
-Inductive Fork_post (σ σ' : state) (π ρ: thread) : Prop :=
- | ForkPost (V: View)
- (ViewOf: threads σ !! π = Some V)
- (ViewNew: threads σ !! ρ = None)
- (MemOld : mem σ' = mem σ)
- (TUpd : threads σ' = <[ρ := V]>(threads σ))
- (NATSOld: nats σ' = nats σ)
- .
+Inductive Fork_post (σ σ' : state) (V V': View) : Prop :=
+| ForkPost
+ (HV : V' = V)
+ (Hstate : σ' = σ)
+.
- Lemma wp_fork_help {e1 e2 π K} :
- (Fork e1, π) = fill K e2 → K = [].
- Proof.
- move : e2. induction K as [|fi K]; first done.
- move => e2. simpl => EH.
- specialize (IHK _ EH). subst K. simpl in EH.
- destruct fi; done.
- Qed.
-
-Lemma wp_fork_pst E π (σ: state) e Φ :
- (∃ V, threads σ !! π = Some V) →
- phys_inv σ →
+Lemma wp_fork_help {e1 e2 π K} :
+ (Fork e1, π) = fill K e2 → K = [].
+Proof.
+ move : e2. induction K as [|fi K]; first done.
+ move => e2. simpl => EH.
+ specialize (IHK _ EH). subst K. simpl in EH.
+ destruct fi; done.
+Qed.
+
+Lemma wp_fork_pst E (σ: state) (V V': View) e Φ :
+ phys_inv σ → view_ok (mem σ) V →
▷ ownP σ
- ∗ ▷(∀ ρ (σ': state),
- ⌜phys_inv σ'⌝ ∧ ⌜rel_inv σ σ'⌝
- ∧ ⌜Fork_post σ σ' π ρ⌝
- ∧ ownP σ' -∗ |==> ((|={E}=> Φ (LitV $ LitUnit, π)) ∗ WP (e, ρ) {{ _, True }}))
- ⊢ WP (Fork e, π) @ E {{ Φ }}.
+ ∗ ▷(∀ (σ': state) V',
+ ⌜phys_inv σ'⌝ ∧ ⌜rel_inv σ σ'⌝ ∧ ⌜view_ok (mem σ') V'⌝
+ ∧ ⌜Fork_post σ σ' V V'⌝
+ ∧ ownP σ' -∗ |==> ((|={E}=> Φ (LitV $ LitUnit, V')) ∗ WP (e, V') {{ _, True }}))
+ ⊢ WP (Fork e, V) @ E {{ Φ }}.
Proof.
- intros [V ViewOf] Inv.
+ intros Inv VOk.
iIntros "[HP HΦ]".
- iApply (wp_lift_atomic_head_step2 (Fork _, π) σ).
+ iApply (wp_lift_atomic_head_step2 (Fork _, _) σ).
- induction 1 as [? ? ? ? ? Step].
have ? := (wp_fork_help H). subst; simpl in *; simplify_eq.
inversion Step; simplify_eq;
[inversion BaseStep|inversion ExprStep]; simplify_eq; eauto.
- - assert (HNew: ∃ ρ, ρ ∉ dom (gset thread) (threads σ)).
- { eexists (fresh (dom _ (threads σ))). eapply is_fresh. }
- destruct HNew as [ρ HNew].
- assert (Hρ: threads σ !! ρ = None).
- { move /elem_of_dom : HNew. case: (_ !! _) => ? //= ?. exfalso. eauto. }
- eexists.
- exists (mkState (<[ρ := V]> (threads σ)) (mem σ) (nats σ)).
- econstructor. eright; first by constructor.
- econstructor 2; eauto. econstructor; eauto.
+ - eexists _, σ, _.
+ eright.
+ + by econstructor.
+ + by eright.
- iSplitL "HP"; first by [].
iNext. iIntros "% % % [% HP]". destruct a.
inversion H; [by inversion BaseStep|inversion ExprStep].
- assert (Inv' : phys_inv a0) by apply (proj1 (machine_red_safe _ _ _ _ MachStep Inv)).
+ assert (Inv' : phys_inv a0) by exact: (proj1 (machine_red_safe _ _ _)).
inversion MachStep; subst; first by inversion ThreadRed. simpl.
destruct v; try discriminate.
destruct l; try discriminate.
inversion H10. simplify_eq.
iDestruct ("HΦ" with "[$HP]") as ">[$ $]"; last done.
- iFrame (Inv'). iSplit; iPureIntro.
- + apply (machine_red_safe _ _ _ _ MachStep Inv).
+ iFrame (Inv'). iSplit; [|iSplit]; iPureIntro.
+ + inversion FRed; subst. by destruct (machine_red_safe Inv VOk MachStep).
+ + inversion FRed; subst. by destruct (machine_red_safe Inv VOk MachStep).
+ inversion FRed. subst. econstructor; subst; eauto.
Qed.
Instance constant_dec {T : Prop} {X : Type}
`{Decision T} : ∀ x, (Decision ((λ x : X, T) x)) := _.
-Inductive drf_pre (σ : state) π l : Prop :=
- | _singleton_drf (V : View)
+Inductive drf_pre (σ : state) V l : Prop :=
+ | _singleton_drf
otl otn
- (ViewOf : threads σ !! π = Some V)
(Local : V !! l = otl)
(NATS : nats σ !! l = otn)
(LE : otn ⊑ otl).
-Inductive drf_pre_read_na (σ : state) π l : Prop :=
- | _singleton_drf_read_na (V : View)
+Inductive drf_pre_read_na (σ : state) V l : Prop :=
+ | _singleton_drf_read_na
otl
- (ViewOf : threads σ !! π = Some V)
(Local : V !! l = otl)
(Max : MaxTime (mem σ) l otl).
-Inductive init_pre (σ : state) π l : Prop :=
- | _singleton_init (V : View)
+Inductive init_pre (σ : state) V l : Prop :=
+ | _singleton_init
(tl : positive)
- (ViewOf : threads σ !! π = Some V)
(Local : V !! l = Some tl)
(Init : initialized (mem σ) l tl).
@@ -308,58 +297,55 @@ Qed.
Open Scope positive.
-Inductive read_at_post (σ σ' : state) (π : thread) x (v : Z) : Prop :=
- | ReadAtPost (V V': View)
+Inductive read_at_post (σ σ' : state) V V' x (v : Z) : Prop :=
+ | ReadAtPost
(t' : positive)
m
(EqVal : mval m = VInj v)
(EqLoc : mloc m = x)
(In : m ∈ msgs $ mem σ)
- (ViewOf : (threads σ) !! π = Some V)
(Local : V !! x = Some t')
(TimeLe : t' ⊑ mtime m)
(VUpd : V' = V ⊔ mview m)
- (TUpd : threads σ' = <[π := V']>(threads σ))
(MOld : mem σ' = mem σ)
(NATSOld : nats σ' = nats σ)
.
-Inductive read_na_post (σ σ' : state) (π : thread) x (v : Z) : Prop :=
- | ReadNAPost (V V': View)
+Inductive read_na_post (σ σ' : state) V V' x (v : Z) : Prop :=
+ | ReadNAPost
(t' : positive)
m
(EqVal : mval m = VInj v)
(EqLoc : mloc m = x)
(In : m ∈ msgs $ mem σ)
- (ViewOf : (threads σ) !! π = Some V)
(Local : V !! x = Some t')
(TimeLe : t' ⊑ mtime m)
(VUpd : V' = V ⊔ mview m)
- (TUpd : threads σ' = <[π := V']>(threads σ))
(MOld : mem σ' = mem σ)
(NATSOld : nats σ' = nats σ)
(Max : MaxTime (mem σ) x (Some $ mtime m))
.
-Lemma wp_load_at_pst E π σ l :
+Lemma wp_load_at_pst E V σ l :
phys_inv σ →
- drf_pre σ π l →
- init_pre σ π l →
+ view_ok (mem σ) V →
+ drf_pre σ V l →
+ init_pre σ V l →
{{{ ▷ ownP σ }}}
- (Load at_hack (Lit $ (LitLoc l)), π) @ E
- {{{ v σ', RET (LitV (LitInt v), π);
- ⌜phys_inv σ'⌝ ∧ ⌜rel_inv σ σ'⌝ ∧ ⌜read_at_post σ σ' π l v⌝ ∧ ownP σ' }}}.
+ (Load at_hack (Lit $ (LitLoc l)), V) @ E
+ {{{ v σ' V', RET (LitV (LitInt v), V');
+ ⌜phys_inv σ'⌝ ∧ ⌜rel_inv σ σ'⌝ ∧ ⌜view_ok (mem σ') V'⌝ ∧ ⌜read_at_post σ σ' V V' l v⌝ ∧ ownP σ' }}}.
Proof.
- intros Inv A B Φ.
+ intros Inv VOk A B Φ.
iIntros "HP HΦ".
- iApply (ownP_lift_atomic_head_step (Load at_hack _, π) σ); eauto.
+ iApply (ownP_lift_atomic_head_step (Load at_hack _, _) σ); eauto.
- inversion A; inversion B; simplify_option_eq.
subst.
- move: (ITOk _ Inv _ _ ViewOf _ _ Local0) => [m [In [EqLoc [EqTime SubView]]]].
+ move: (VOk _ _ Local0) => [m [In [EqLoc [EqTime SubView]]]].
assert (IsVal := initialized_reads_value _ _ _ Init m In EqLoc EqTime).
case HVal: (mval m) => [| |v]; try (by rewrite HVal in IsVal; inversion IsVal).
eexists.
- exists (mkState (<[π:=V ⊔ mview m]> (threads σ)) (mem σ) (nats σ)).
+ exists σ.
econstructor. eright; first by constructor.
econstructor; try eauto.
+ move => ? [<-]. by econstructor.
@@ -371,38 +357,40 @@ Proof.
- iSplitL "HP"; first by [].
iNext. iIntros "% % % % HP". destruct a.
inversion H; [by inversion BaseStep|inversion ExprStep].
- assert (Inv' : phys_inv a0)
- by apply (proj1 (machine_red_safe _ _ _ _ MachStep Inv)).
+ assert (Inv' : phys_inv a0) by exact: (proj1 (machine_red_safe _ _ _)).
inversion MachStep; last by (subst; discriminate).
subst. iSplit; last by rewrite big_opL_nil.
inversion ThreadRed. subst.
- iApply "HΦ". iSplit; [|iSplit; [|iSplit]]; try by []; iPureIntro.
- + apply (machine_red_safe _ _ _ _ MachStep Inv).
+ iApply "HΦ". iFrame "HP". iSplit; [|iSplit; [|iSplit]]; try by []; iPureIntro.
+ + rewrite /rel_inv NoWriteNats // H7.
+ by destruct (machine_red_safe Inv VOk MachStep) as (?&?&?&?&?).
+ + by destruct (machine_red_safe Inv VOk MachStep) as (?&?&?&?&?).
+ destruct Lt as [t' [Lt ?]].
inversion DRFRed. subst.
econstructor; subst; eauto.
rewrite LV in Lt. by simplify_option_eq.
Qed.
-Lemma wp_load_na_pst E π σ l:
+Lemma wp_load_na_pst E V σ l:
phys_inv σ →
- drf_pre_read_na σ π l →
- init_pre σ π l →
+ view_ok (mem σ) V →
+ drf_pre_read_na σ V l →
+ init_pre σ V l →
{{{ ▷ ownP σ }}}
- (Load na (Lit $ (LitLoc l)), π) @ E
- {{{ v σ', RET (LitV (LitInt v), π);
- ⌜phys_inv σ'⌝ ∧ ⌜rel_inv σ σ'⌝ ∧ ⌜read_na_post σ σ' π l v⌝ ∧ ownP σ' }}}.
+ (Load na (Lit $ (LitLoc l)), V) @ E
+ {{{ v σ' V', RET (LitV (LitInt v), V');
+ ⌜phys_inv σ'⌝ ∧ ⌜rel_inv σ σ'⌝ ∧ ⌜view_ok (mem σ') V'⌝ ∧ ⌜read_na_post σ σ' V V' l v⌝ ∧ ownP σ' }}}.
Proof.
- intros Inv A B Φ.
+ intros Inv VOk A B Φ.
iIntros "HP HΦ".
- iApply (ownP_lift_atomic_head_step (Load na _, π) σ); eauto.
+ iApply (ownP_lift_atomic_head_step (Load na _, _) σ); eauto.
- inversion A; inversion B; simplify_option_eq.
- move: (ITOk _ Inv _ _ ViewOf _ _ Local0) => [m [In [EqLoc [EqTime SubView]]]].
+ move: (VOk _ _ Local0) => [m [In [EqLoc [EqTime SubView]]]].
assert (IsVal := initialized_reads_value _ _ _ Init m In EqLoc EqTime).
case Hmv: (mval m) => [| |v];
try (by rewrite Hmv in IsVal; inversion IsVal).
eexists.
- exists (mkState (<[π:=V ⊔ mview m]> (threads σ)) (mem σ) (nats σ)).
+ exists σ.
econstructor. eright; first by constructor.
econstructor; try eauto.
+ move => ? [<-]. by econstructor.
@@ -413,55 +401,53 @@ Proof.
- iSplitL "HP"; first by [].
iNext. iIntros "% % % % HP". destruct a.
inversion H; [by inversion BaseStep|inversion ExprStep].
- assert (Inv' : phys_inv a0)
- by apply (proj1 (machine_red_safe _ _ _ _ MachStep Inv)).
+ assert (Inv' : phys_inv a0) by exact: (proj1 (machine_red_safe _ _ _)).
inversion MachStep; last by (subst; discriminate).
subst. iSplit; last by rewrite big_opL_nil.
inversion ThreadRed. subst.
- iApply "HΦ". iSplit; [|iSplit; [|iSplit]]; try by []; iPureIntro.
- + apply (machine_red_safe _ _ _ _ MachStep Inv).
+ iApply "HΦ". iFrame "HP". iSplit; [|iSplit; [|iSplit]]; try by []; iPureIntro.
+ + by rewrite /rel_inv H7 NoWriteNats //.
+ + by destruct (machine_red_safe Inv VOk MachStep) as (?&?&?&?&?).
+ destruct Lt as [t' [Lt ?]].
inversion DRFRed. rewrite Lt in LV. simplify_option_eq.
econstructor; subst; eauto.
Qed.
-Inductive alloc_pre (σ : state) π l : Prop :=
- | _singleton_alloc (V : View)
+Inductive alloc_pre (σ : state) V l : Prop :=
+ | _singleton_alloc
(tl : positive)
- (ViewOf : threads σ !! π = Some V)
(Local : V !! l = Some tl)
(Alloc : allocated (mem σ) l tl).
-Inductive write_at_post (σ σ' : state) (π : thread) x (v : Z) : Prop :=
- | WriteAtPost (V V': View)
+Inductive write_at_post (σ σ' : state) V V' x (v : Z) : Prop :=
+ | WriteAtPost
m
(EqVal : mval m = VInj v)
(EqLoc : mloc m = x)
(EqView: mview m = V')
- (ViewOf: (threads σ) !! π = Some V)
(Local : V !! x ⊏ Some (mtime m))
(VUpd : V' = V ⊔ {[x := mtime m]})
- (TUpd : threads σ' = <[π := V']>(threads σ))
(NATSOld : nats σ' = nats σ)
(Disj : MS_msg_disj (msgs $ mem σ) m)
(MUpd : mem σ' = add_ins (mem σ) m Disj)
.
-Lemma wp_store_at_pst E π σ l v:
+Lemma wp_store_at_pst E V σ l v:
phys_inv σ →
- drf_pre σ π l →
- alloc_pre σ π l →
+ view_ok (mem σ) V →
+ drf_pre σ V l →
+ alloc_pre σ V l →
{{{ ▷ ownP σ }}}
- (Store at_hack (Lit $ (LitLoc l)) (Lit $ LitInt v), π) @ E
- {{{ σ', RET (LitV (LitUnit), π);
- ⌜phys_inv σ'⌝ ∧ ⌜rel_inv σ σ'⌝ ∧ ⌜write_at_post σ σ' π l v⌝ ∧ ownP σ' }}}.
+ (Store at_hack (Lit $ (LitLoc l)) (Lit $ LitInt v), V) @ E
+ {{{ σ' V', RET (LitV (LitUnit), V');
+ ⌜phys_inv σ'⌝ ∧ ⌜rel_inv σ σ'⌝ ∧ ⌜view_ok (mem σ') V'⌝ ∧ ⌜write_at_post σ σ' V V' l v⌝ ∧ ownP σ' }}}.
Proof.
- intros Inv A B Φ.
+ intros Inv VOk A B Φ.
iIntros "HP HΦ".
- iApply (ownP_lift_atomic_head_step (Store _ _ _, π) σ); eauto.
+ iApply (ownP_lift_atomic_head_step (Store _ _ _, _) σ); eauto.
- inversion A; inversion B; simplify_option_eq.
subst.
- move: (ITOk _ Inv _ _ ViewOf _ _ Local0) => [ml [In [EqLoc [EqTime SubView]]]].
+ move: (VOk _ _ Local0) => [ml [In [EqLoc [EqTime SubView]]]].
assert (NE: hist (mem σ) l ≢ ∅).
{ by apply (non_empty_inhabited ml), elem_of_hist. }
destruct (hist_max_time _ _ NE) as [m' [Inm' tMax]].
@@ -479,7 +465,7 @@ Proof.
by apply tMax, elem_of_hist. }
eexists.
- exists (mkState (<[π:=V ⊔ {[l := mtime m]}]> (threads σ))
+ exists (mkState
(add_ins (mem σ) m Disj)
(nats σ)).
econstructor. eright; first by constructor.
@@ -490,28 +476,27 @@ Proof.
- iSplitL "HP"; first by [].
iNext. iIntros "% % % % HP". destruct a as [v' π'].
inversion H; [by inversion BaseStep|inversion ExprStep].
- assert (Inv' : phys_inv a0)
- by apply (proj1 (machine_red_safe _ _ _ _ MachStep Inv)).
+ assert (Inv' : phys_inv a0) by exact: (proj1 (machine_red_safe _ _ _)).
inversion MachStep; last by (subst; discriminate).
subst. iSplit; last by rewrite big_opL_nil.
inversion ThreadRed. subst. simplify_option_eq.
- iApply "HΦ". iSplit; [|iSplit; [|iSplit]]; try by []; iPureIntro.
- + apply (machine_red_safe _ _ _ _ MachStep Inv).
+ iApply "HΦ". iFrame "HP". iSplit; [|iSplit; [|iSplit]]; try by []; iPureIntro.
+ + rewrite /rel_inv /=.
+ by edestruct (machine_red_safe Inv VOk MachStep) as (?&?&?&?&?).
+ + by edestruct (machine_red_safe Inv VOk MachStep) as (?&?&?&?&?).
+ econstructor; subst; eauto; simpl; eauto.
by inversion DRFRed.
Qed.
-Inductive write_na_post (σ σ' : state) (π : thread) x (v : Z) : Prop :=
- | WriteNAPost (V V': View)
+Inductive write_na_post (σ σ' : state) V V' x (v : Z) : Prop :=
+ | WriteNAPost
m
(EqVal : mval m = VInj v)
(EqLoc : mloc m = x)
(EqView: mview m = V')
- (ViewOf: (threads σ) !! π = Some V)
(Local : V !! x ⊏ Some (mtime m))
(VUpd : V' = V ⊔ {[x := mtime m]})
- (TUpd : threads σ' = <[π := V']>(threads σ))
(NATSUpd : nats σ' = <[x := mtime m]>(nats σ))
(Disj : MS_msg_disj (msgs $ mem σ) m)
(MUpd : mem σ' = add_ins (mem σ) m Disj)
@@ -519,21 +504,22 @@ Inductive write_na_post (σ σ' : state) (π : thread) x (v : Z) : Prop :=
.
-Lemma wp_store_na_pst E π σ l v:
+Lemma wp_store_na_pst E σ V l v:
phys_inv σ →
- drf_pre σ π l →
- alloc_pre σ π l →
+ view_ok (mem σ) V →
+ drf_pre σ V l →
+ alloc_pre σ V l →
{{{ ▷ ownP σ }}}
- (Store na (Lit $ (LitLoc l)) (Lit $ LitInt v), π) @ E
- {{{ σ', RET (LitV (LitUnit), π);
- ⌜phys_inv σ'⌝ ∧ ⌜rel_inv σ σ'⌝ ∧ ⌜write_na_post σ σ' π l v⌝ ∧ ownP σ' }}}.
+ (Store na (Lit $ (LitLoc l)) (Lit $ LitInt v), V) @ E
+ {{{ σ' V', RET (LitV (LitUnit), V');
+ ⌜phys_inv σ'⌝ ∧ ⌜rel_inv σ σ'⌝ ∧ ⌜view_ok (mem σ') V'⌝ ∧ ⌜write_na_post σ σ' V V' l v⌝ ∧ ownP σ' }}}.
Proof.
- intros Inv A B Φ.
+ intros Inv VOk A B Φ.
iIntros "HP HΦ".
- iApply (ownP_lift_atomic_head_step (Store _ _ _, π) σ); eauto.
+ iApply (ownP_lift_atomic_head_step (Store _ _ _, _) σ); eauto.
- inversion A; inversion B; simplify_option_eq.
subst.
- move: (ITOk _ Inv _ _ ViewOf _ _ Local0) => [ml [In [EqLoc [EqTime SubView]]]].
+ move: (VOk _ _ Local0) => [ml [In [EqLoc [EqTime SubView]]]].
assert (NE: hist (mem σ) l ≢ ∅).
{ by apply (non_empty_inhabited ml), elem_of_hist. }
destruct (hist_max_time _ _ NE) as [m' [Inm' tMax]].
@@ -551,9 +537,8 @@ Proof.
by apply tMax, elem_of_hist. }
eexists.
- exists (mkState (<[π:=V ⊔ {[l := mtime m]}]> (threads σ))
- (add_ins (mem σ) m Disj)
- (<[l:= mtime m]> (nats σ))).
+ exists (mkState (add_ins (mem σ) m Disj)
+ (<[l:= mtime m]> (nats σ))).
econstructor. eright; first by constructor.
econstructor; try eauto => //.
+ move => ? [<-]. by econstructor.
@@ -569,49 +554,49 @@ Proof.
- iSplitL "HP"; first by [].
iNext. iIntros "% % % % HP". destruct a as [v' π'].
inversion H; [by inversion BaseStep|inversion ExprStep].
- assert (Inv' : phys_inv a0)
- by apply (proj1 (machine_red_safe _ _ _ _ MachStep Inv)).
+ assert (Inv' : phys_inv a0) by exact: (proj1 (machine_red_safe _ _ _)).
inversion MachStep; last by (subst; discriminate).
subst. iSplit; last by rewrite big_opL_nil.
inversion ThreadRed. subst. simplify_option_eq.
- iApply "HΦ". iSplit; [|iSplit; [|iSplit]]; try by []; iPureIntro.
- + apply (machine_red_safe _ _ _ _ MachStep Inv).
+ iApply "HΦ". iFrame "HP". iSplit; [|iSplit; [|iSplit]]; try by []; iPureIntro.
+ + rewrite /rel_inv /=.
+ by destruct (machine_red_safe Inv VOk MachStep) as (?&?&?&?&?).
+ + by destruct (machine_red_safe Inv VOk MachStep) as (?&?&?&?&?).
+ inversion DRFRed.
econstructor; subst; eauto; simpl; eauto.
Qed.
-Inductive dealloc_post (σ σ' : state) (π : thread) x : Prop :=
- | DeallocPost (V V': View)
+Inductive dealloc_post (σ σ' : state) V V' x : Prop :=
+ | DeallocPost
m
(EqVal : mval m = D)
(EqLoc : mloc m = x)
(EqView: mview m = V')
- (ViewOf: (threads σ) !! π = Some V)
(Local : V !! x ⊏ Some (mtime m))
(VUpd : V' = V ⊔ {[x := mtime m]})
- (TUpd : threads σ' = <[π := V']>(threads σ))
(NATSUpd : nats σ' = <[x := mtime m]>(nats σ))
(Disj : MS_msg_disj (msgs $ mem σ) m)
(MUpd : mem σ' = add_ins (mem σ) m Disj)
(Max : MaxTime (mem σ') x (Some $ mtime m))
.
-Lemma wp_dealloc_pst E π σ l:
+Lemma wp_dealloc_pst E V σ l:
phys_inv σ →
- drf_pre σ π l →
- alloc_pre σ π l →
+ view_ok (mem σ) V →
+ drf_pre σ V l →
+ alloc_pre σ V l →
{{{ ▷ ownP σ }}}
- (Dealloc (Lit $ LitLoc l), π) @ E
- {{{ σ', RET (LitV $ LitUnit, π);
- ⌜phys_inv σ'⌝ ∧ ⌜rel_inv σ σ'⌝ ∧ ⌜dealloc_post σ σ' π l⌝ ∧ ownP σ' }}}.
+ (Dealloc (Lit $ LitLoc l), V) @ E
+ {{{ σ' V', RET (LitV $ LitUnit, V');
+ ⌜phys_inv σ'⌝ ∧ ⌜rel_inv σ σ'⌝ ∧ ⌜view_ok (mem σ') V'⌝ ∧ ⌜dealloc_post σ σ' V V' l⌝ ∧ ownP σ' }}}.
Proof.
- intros Inv A B Φ.
+ intros Inv VOk A B Φ.
iIntros "HP HΦ".
- iApply (ownP_lift_atomic_head_step (Dealloc _, π) σ); eauto.
+ iApply (ownP_lift_atomic_head_step (Dealloc _, _) σ); eauto.
- inversion A; inversion B; simplify_option_eq.
subst.
- move: (ITOk _ Inv _ _ ViewOf _ _ Local0) => [ml [In [EqLoc [EqTime SubView]]]].
+ move: (VOk _ _ Local0) => [ml [In [EqLoc [EqTime SubView]]]].
assert (NE: hist (mem σ) l ≢ ∅).
{ by apply (non_empty_inhabited ml), elem_of_hist. }
destruct (hist_max_time _ _ NE) as [m' [Inm' tMax]].
@@ -628,9 +613,8 @@ Proof.
eapply Pos.le_lt_trans; last by apply Pos.lt_add_r.
by apply tMax, elem_of_hist. }
eexists.
- exists (mkState (<[π:=V ⊔ {[l := mtime m]}]> (threads σ))
- (add_ins (mem σ) m Disj)
- (<[l:=mtime m]> (nats σ))).
+ exists (mkState (add_ins (mem σ) m Disj)
+ (<[l:=mtime m]> (nats σ))).
econstructor. eright; first by constructor.
econstructor; try eauto => //.
+ move => ? [<-]. by econstructor.
@@ -647,18 +631,19 @@ Proof.
iNext. iIntros "% % % % HP". destruct a as [v' π'].
inversion H; [by inversion BaseStep|inversion ExprStep].
subst.
- assert (Inv' : phys_inv a0) by apply (proj1 (machine_red_safe _ _ _ _ MachStep Inv)).
+ assert (Inv' : phys_inv a0) by exact: (proj1 (machine_red_safe _ _ _)).
inversion MachStep; last by (subst; discriminate).
subst. simpl. iSplit; last done.
inversion ThreadRed. subst.
- iApply "HΦ". iSplit; [|iSplit; [|iSplit]]; try by []; iPureIntro.
- + apply (machine_red_safe _ _ _ _ MachStep Inv).
+ iApply "HΦ". iFrame "HP". iSplit; [|iSplit; [|iSplit]]; try by []; iPureIntro.
+ + by destruct (machine_red_safe Inv VOk MachStep) as (?&?&?&?&?).
+ + by destruct (machine_red_safe Inv VOk MachStep) as (?&?&?&?&?).
+ inversion DRFRed.
econstructor; subst; eauto; simpl; eauto.
Qed.
-Inductive CAS_succ_post (σ σ' : state) (π : thread) x (v_r v_w: Z) : Prop :=
- | CASSuccPost (V V': View)
+Inductive CAS_succ_post (σ σ' : state) V V' x (v_r v_w: Z) : Prop :=
+ | CASSuccPost
(tl tr : positive)
m m'
(InR: m ∈ (msgs $ mem σ))
@@ -670,17 +655,15 @@ Inductive CAS_succ_post (σ σ' : state) (π : thread) x (v_r v_w: Z) : Prop :=
(EqView': mview m' = V')
(EqTime': mtime m' = tr + 1)
(VUpd : V' = V ⊔ {[x := tr + 1]} ⊔ mview m)
- (ViewOf: (threads σ) !! π = Some V)
(Local : V !! x = Some tl)
(TimeLe: tl ⊑ tr)
(Disj : MS_msg_disj (msgs $ mem σ) m')
(MUpd : mem σ' = add_ins (mem σ) m' Disj)
- (TUpd : threads σ' = <[π := V']>(threads σ))
(NATSOld: nats σ' = nats σ)
.
-Inductive CAS_fail_post (σ σ' : state) (π : thread) x (v_r: Z) : Prop :=
- | CASFailPost (V V': View)
+Inductive CAS_fail_post (σ σ' : state) V V' x (v_r: Z) : Prop :=
+ | CASFailPost
(t : positive)
m v
(InR: m ∈ (msgs $ mem σ))
@@ -688,32 +671,31 @@ Inductive CAS_fail_post (σ σ' : state) (π : thread) x (v_r: Z) : Prop :=
(NEqVal : v ≠ v_r)
(EqLoc : mloc m = x)
(VUpd : V' = V ⊔ mview m)
- (ViewOf: (threads σ) !! π = Some V)
(Local : V !! x = Some t)
(TimeLe : t ⊑ mtime m)
- (TUpd : threads σ' = <[π := V']>(threads σ))
(MOld : mem σ' = mem σ)
(NATSOld : nats σ' = nats σ)
.
-Lemma wp_CAS_pst E π σ l v_r v_w:
+Lemma wp_CAS_pst E V σ l v_r v_w:
phys_inv σ →
- drf_pre σ π l →
- init_pre σ π l →
+ view_ok (mem σ) V →
+ drf_pre σ V l →
+ init_pre σ V l →
{{{ ▷ ownP σ }}}
- (CAS (Lit $ LitLoc l) (Lit $ LitInt v_r) (Lit $ LitInt v_w), π) @ E
- {{{ b σ', RET (LitV $ LitInt b, π);
- ⌜phys_inv σ'⌝ ∧ ⌜rel_inv σ σ'⌝
- ∧ ⌜ b = true ∧ CAS_succ_post σ σ' π l v_r v_w
- ∨ b = false ∧ CAS_fail_post σ σ' π l v_r ⌝
+ (CAS (Lit $ LitLoc l) (Lit $ LitInt v_r) (Lit $ LitInt v_w), V) @ E
+ {{{ b σ' V', RET (LitV $ LitInt b, V');
+ ⌜phys_inv σ'⌝ ∧ ⌜rel_inv σ σ'⌝ ∧ ⌜view_ok (mem σ') V'⌝
+ ∧ ⌜ b = true ∧ CAS_succ_post σ σ' V V' l v_r v_w
+ ∨ b = false ∧ CAS_fail_post σ σ' V V' l v_r ⌝
∧ ownP σ' }}}.
Proof.
- intros Inv A B Φ.
+ intros Inv VOk A B Φ.
iIntros "HP HΦ".
- iApply (ownP_lift_atomic_head_step (CAS _ _ _, π) σ); eauto.
+ iApply (ownP_lift_atomic_head_step (CAS _ _ _, _) σ); eauto.
- inversion A; inversion B; simplify_option_eq.
subst.
- move: (ITOk _ Inv _ _ ViewOf _ _ Local0) => [ml [In [EqLoc [EqTime SubView]]]].
+ move: (VOk _ _ Local0) => [ml [In [EqLoc [EqTime SubView]]]].
assert (NE: hist (mem σ) l ≢ ∅).
{ by apply (non_empty_inhabited ml), elem_of_hist. }
destruct (hist_max_time _ _ NE) as [m' [Inm' tMax]].
@@ -746,9 +728,8 @@ Proof.
rewrite -{2}Eq. eapply Pos.le_lt_trans; last by apply Pos.lt_add_r.
by apply tMax, elem_of_hist. }
eexists.
- exists (mkState (<[π:=V ⊔ {[l := mtime m' + 1]} ⊔ mview m']> (threads σ))
- (add_ins (mem σ) m Disj)
- (nats σ)).
+ exists (mkState (add_ins (mem σ) m Disj)
+ (nats σ)).
econstructor. eright; first by constructor.
econstructor; try eauto => //=.
* move => ? [<-]. by econstructor.
@@ -758,7 +739,7 @@ Proof.
{ exists tl. split => //. rewrite -EqTime.
by apply tMax, elem_of_hist. }
+ eexists.
- exists (mkState (<[π:=V ⊔ mview m']> (threads σ)) (mem σ) (nats σ)).
+ exists (mkState (mem σ) (nats σ)).
econstructor. eright. eapply CasFailS; eauto.
econstructor; try eauto => //=.
* move => ? [<-]. by econstructor.
@@ -771,27 +752,29 @@ Proof.
- iSplitL "HP"; first by [].
iNext. iIntros "% % % % HP". destruct a as [v' π'].
inversion H; first by inversion BaseStep.
- assert (Inv' : phys_inv a0) by apply (proj1 (machine_red_safe _ _ _ _ MachStep Inv)).
+ assert (Inv' : phys_inv a0) by exact: (proj1 (machine_red_safe _ _ _)).
subst.
inversion ExprStep; inversion MachStep; subst; try discriminate; simpl;
(iSplit; last done).
+ inversion ThreadRed; subst. simplify_option_eq.
- iApply ("HΦ" $! false with "[$HP]"). iFrame (Inv'). iSplit; iPureIntro.
- * apply (machine_red_safe _ _ _ _ MachStep Inv).
+ iApply ("HΦ" $! false with "[$HP]"). iFrame (Inv'). iSplit; [|iSplit]; iPureIntro.
+ * by destruct (machine_red_safe Inv VOk MachStep) as (?&?&?&?&?).
+ * by destruct (machine_red_safe Inv VOk MachStep) as (?&?&?&?&?).
* destruct Lt as [t' [Lt1 Lt2]].
right. split => //.
econstructor; subst; eauto; simpl; eauto.
+ inversion ThreadRed; subst. simplify_option_eq.
iApply ("HΦ" $! true with "[$HP]").
- iFrame (Inv'). iSplit; iPureIntro.
- * apply (machine_red_safe _ _ _ _ MachStep Inv).
+ iFrame (Inv'). iSplit; [|iSplit]; iPureIntro.
+ * by destruct (machine_red_safe Inv VOk MachStep) as (?&?&?&?&?).
+ * by destruct (machine_red_safe Inv VOk MachStep) as (?&?&?&?&?).
* destruct Lt as [t' [Lt1 Lt2]].
left. split =>//. econstructor; subst; eauto; simpl; eauto.
by inversion DRFRed.
Qed.
-Inductive FAI_post C (σ σ' : state) (π : thread) x (v: Z) : Prop :=
- | FAIPost (V V': View)
+Inductive FAI_post C (σ σ' : state) V V' x (v: Z) : Prop :=
+ | FAIPost
(tl tr : positive)
m m'
(InR: m ∈ (msgs $ mem σ))
@@ -803,31 +786,30 @@ Inductive FAI_post C (σ σ' : state) (π : thread) x (v: Z) : Prop :=
(EqView': mview m' = V')
(EqTime': mtime m' = tr + 1)
(VUpd : V' = V ⊔ {[x := tr + 1]} ⊔ mview m)
- (ViewOf: (threads σ) !! π = Some V)
(Local : V !! x = Some tl)
(TimeLe: tl ⊑ tr)
(Disj : MS_msg_disj (msgs $ mem σ) m')
(MUpd : mem σ' = add_ins (mem σ) m' Disj)
- (TUpd : threads σ' = <[π := V']>(threads σ))
(NATSOld: nats σ' = nats σ)
.
-Lemma wp_FAI_pst C E π σ l :
+Lemma wp_FAI_pst C E V σ l :
phys_inv σ →
- drf_pre σ π l →
- init_pre σ π l →
+ view_ok (mem σ) V →
+ drf_pre σ V l →
+ init_pre σ V l →
{{{ ▷ ownP σ }}}
- (FAI C (Lit $ LitLoc l), π) @ E
- {{{ v σ', RET (LitV $ LitInt v, π);
- ⌜phys_inv σ'⌝ ∧ ⌜rel_inv σ σ'⌝ ∧ ⌜FAI_post C σ σ' π l v⌝ ∧ ownP σ' }}}.
+ (FAI C (Lit $ LitLoc l), V) @ E
+ {{{ v σ' V', RET (LitV $ LitInt v, V');
+ ⌜phys_inv σ'⌝ ∧ ⌜rel_inv σ σ'⌝ ∧ ⌜view_ok (mem σ') V'⌝ ∧ ⌜FAI_post C σ σ' V V' l v⌝ ∧ ownP σ' }}}.
Proof.
- intros Inv A B Φ.
+ intros Inv VOk A B Φ.
iIntros "HP HΦ".
- iApply (ownP_lift_atomic_head_step (FAI _ _, π) σ); eauto.
+ iApply (ownP_lift_atomic_head_step (FAI _ _, _) σ); eauto.
- inversion A; inversion B; simplify_option_eq.
subst.
- move: (ITOk _ Inv _ _ ViewOf _ _ Local0) => [ml [In [EqLoc [EqTime SubView]]]].
+ move: (VOk _ _ Local0) => [ml [In [EqLoc [EqTime SubView]]]].
assert (NE: hist (mem σ) l ≢ ∅).
{ by apply (non_empty_inhabited ml), elem_of_hist. }
destruct (hist_max_time _ _ NE) as [m' [Inm' tMax]].
@@ -858,9 +840,8 @@ Proof.
- rewrite TEq. by apply tMax, elem_of_hist.
- apply Pos.lt_add_r. }
eexists.
- exists (mkState (<[π:=V ⊔ {[l := mtime m' + 1]} ⊔ mview m']> (threads σ))
- (add_ins (mem σ) m Disj)
- (nats σ)).
+ exists (mkState (add_ins (mem σ) m Disj)
+ (nats σ)).
econstructor. eright; first by constructor.
econstructor; try eauto => //=.
* move => ? [<-]. by econstructor.
@@ -872,53 +853,47 @@ Proof.
- iSplitL "HP"; first by [].
iNext. iIntros "% % % % HP". destruct a as [v' π'].
inversion H; first by inversion BaseStep.
- assert (Inv' : phys_inv a0) by apply (proj1 (machine_red_safe _ _ _ _ MachStep Inv)).
+ assert (Inv' : phys_inv a0) by exact: (proj1 (machine_red_safe _ _ _)).
subst.
inversion ExprStep; inversion MachStep; subst; try discriminate; simpl;
iSplit; last done.
inversion ThreadRed; subst.
- iApply ("HΦ" with "[$HP]"). iFrame (Inv'). iSplit; iPureIntro.
- + apply (machine_red_safe _ _ _ _ MachStep Inv).
+ iApply ("HΦ" with "[$HP]"). iFrame (Inv'). iSplit; [|iSplit]; iPureIntro.
+ + by destruct (machine_red_safe Inv VOk MachStep) as (?&?&?&?&?).
+ + by destruct (machine_red_safe Inv VOk MachStep) as (?&?&?&?&?).
+ destruct Lt as [t' [Lt1 Lt2]].
econstructor; subst; eauto; simpl; eauto.
by inversion DRFRed.
Qed.
-Inductive alloc_post (σ σ' : state) (π : thread) x : Prop :=
- | AllocPost (V V': View)
- (ViewOf: (threads σ) !! π = Some V)
+Inductive alloc_post (σ σ' : state) V V' x : Prop :=
+ | AllocPost m
(Local : V !! x = None)
- m
(EqVal : mval m = A)
(EqLoc : mloc m = x)
(EqView : mview m = V')
(VUpd : V' = V ⊔ {[x := mtime m]})
(Disj : MS_msg_disj (mem σ) m)
(MUpd : mem σ' = add_ins (mem σ) m Disj)
- (TUpd : threads σ' = <[π := V']>(threads σ))
(NATSOld: nats σ' = <[x := mtime m]>(nats σ))
(Fresh: filter ((= x) ∘ mloc) (msgs (mem σ)) ≡ ∅)
.
-Inductive thread_pre (σ : state) (π : thread) : Prop :=
- | _singleton_thread V: threads σ !! π = Some V → thread_pre σ π.
-
-Lemma wp_alloc_pst E π σ:
+Lemma wp_alloc_pst E V σ:
phys_inv σ →
- thread_pre σ π →
+ view_ok (mem σ) V →
{{{ ▷ ownP σ }}}
- (Alloc, π) @ E
- {{{ l σ', RET (LitV $ LitLoc l, π);
- ⌜phys_inv σ'⌝ ∧ ⌜rel_inv σ σ'⌝ ∧ ⌜alloc_post σ σ' π l⌝ ∧ ownP σ' }}}.
+ (Alloc, V) @ E
+ {{{ l σ' V', RET (LitV $ LitLoc l, V');
+ ⌜phys_inv σ'⌝ ∧ ⌜rel_inv σ σ'⌝ ∧ ⌜view_ok (mem σ') V'⌝ ∧ ⌜alloc_post σ σ' V V' l⌝ ∧ ownP σ' }}}.
Proof.
- intros Inv ThreadPre Φ.
+ intros Inv VOk Φ.
iIntros "HP HΦ".
- iApply (ownP_lift_atomic_head_step (Alloc, π) σ); eauto.
- - inversion ThreadPre as [V ViewOf].
- destruct (fresh_location (msgs (mem σ))) as [l Fresh].
+ iApply (ownP_lift_atomic_head_step (Alloc, _) σ); eauto.
+ - destruct (fresh_location (msgs (mem σ))) as [l Fresh].
assert (NVl: V !! l = None).
{ destruct (V !! l) eqn:TEq => //.
- destruct (ITOk _ Inv _ _ ViewOf _ _ TEq) as [m' [In [? _]]].
+ destruct (VOk _ _ TEq) as [m' [In [? _]]].
exfalso. by apply (Fresh _ In). }
assert (nats σ !! l = None).
{ destruct (nats σ !! l) eqn:NAEq => //.
@@ -931,9 +906,8 @@ Proof.
last by left. exfalso. apply (Fresh _ HIn). rewrite /m in LEq.
by simpl in LEq. }
eexists.
- exists (mkState (<[π:=V ⊔ {[l := mtime m]}]> (threads σ))
- (add_ins (mem σ) m Disj)
- (<[l := mtime m]> (nats σ))).
+ exists (mkState (add_ins (mem σ) m Disj)
+ (<[l := mtime m]> (nats σ))).
econstructor. eright; first by constructor.
econstructor; try eauto => //.
+ move => x. instantiate (1 := l). move => /= EqLoc.
@@ -952,17 +926,18 @@ Proof.
- iSplitL "HP"; first by [].
iNext. iIntros "% % % % HP". destruct a as [v' π'].
inversion H; [by inversion BaseStep|inversion ExprStep].
- assert (Inv' : phys_inv a0) by apply (proj1 (machine_red_safe _ _ _ _ MachStep Inv)).
+ assert (Inv' : phys_inv a0) by exact: (proj1 (machine_red_safe _ _ _)).
inversion MachStep; last by (subst; discriminate).
subst. simpl. iSplit; last done.
assert (AllocRed: alloc_red (mem σ) V l (EWrite na l A)). { by apply ARed. }
inversion ThreadRed. subst. simplify_option_eq.
- iApply ("HΦ" with "[$HP]"). iFrame (Inv'). iSplit; iPureIntro.
- + apply (machine_red_safe _ _ _ _ MachStep Inv).
+ iApply ("HΦ" with "[$HP]"). iFrame (Inv'). iSplit; [|iSplit]; iPureIntro.
+ + by destruct (machine_red_safe Inv VOk MachStep) as (?&?&?&?&?).
+ + by destruct (machine_red_safe Inv VOk MachStep) as (?&?&?&?&?).
+ inversion AllocRed. inversion DRFRed. subst.
econstructor; subst; eauto; simpl; eauto.
case Vl: (V !! _) => //.
- destruct (ITOk _ Inv _ _ ViewOf _ _ Vl) as [m [In [EqLoc _]]].
+ destruct (VOk _ _ Vl) as [m [In [EqLoc _]]].
exfalso. apply (not_elem_of_empty (C:=gset _) m).
rewrite -Fresh. move: In EqLoc; set_solver+.
Qed.
diff --git a/coq/ra/machine.v b/coq/ra/machine.v
index 48774f79..e15203d6 100644
--- a/coq/ra/machine.v
+++ b/coq/ra/machine.v
@@ -291,7 +291,6 @@ Section RAMachine.
Record state :=
mkState {
- threads : gmap thread View;
mem : memory;
nats : View
}.
@@ -311,11 +310,11 @@ Section RAMachine.
Qed.
Definition msgs_ok M := ∀ m, m ∈ msgs M → msg_ok m ∧ view_ok (msgs M) m.(mview).
- Definition threads_ok σ := ∀ π V, threads σ !! π = Some V → view_ok (mem σ) V.
+ (* Definition thread_ok σ V :=view_ok (mem σ) V. *)
Notation view_mono V V' := (V ⊑ V').
Definition thread_inv (V : View) (M : memory) := msgs_ok M ∧ view_ok M V.
Global Arguments msgs_ok _ /.
- Global Arguments threads_ok _ /.
+ (* Global Arguments thread_ok _ _ /. *)
Global Arguments thread_inv _ _ /.
Definition msgs_mono M M' := msgs M ⊆ msgs M'.
@@ -824,9 +823,8 @@ Section RAMachine.
End alloc_inv_helpers.
- Lemma alloc_thread_red_alloc σ π x otr otw evt V V' σ' acc
+ Lemma alloc_thread_red_alloc σ x otr otw evt V V' σ' acc
(HAcc : acc_of evt = Some acc)
- (ViewOf : threads σ !! π = Some V)
(ThRed : thread_red V (mem σ) otr otw evt V' (mem σ'))
(DRFRed : drf_red σ σ' V otr otw evt)
(ARed : alloc_red (mem σ) V x evt)
@@ -927,9 +925,8 @@ Section RAMachine.
- exact: MT_msg_loc.
Qed.
- Lemma alloc_thread_red_dealloc σ π x otr otw evt V V' σ' acc
+ Lemma alloc_thread_red_dealloc σ x otr otw evt V V' σ' acc
(HAcc : acc_of evt = Some acc)
- (ViewOf : threads σ !! π = Some V)
(ThRed : thread_red V (mem σ) otr otw evt V' (mem σ'))
(DRFRed : drf_red σ σ' V otr otw evt)
(ARed : alloc_red (mem σ) V x evt)
@@ -1025,7 +1022,7 @@ Section RAMachine.
(* any timestamp of nats corresponds to some message in mem *)
(* INCom : nats_complete (mem σ) (nats σ); *)
(* any loc ever occurs must have been registered in nats *)
- ITOk : threads_ok σ;
+ (* ITOk : threads_ok σ; *)
(* view by any thread agrees with mem *)
IMOk : msgs_ok (mem σ); (* TODO: view_ok is useless!!! *)
(* any message in mem is well-formed and agrees with mem *)
@@ -1034,19 +1031,15 @@ Section RAMachine.
IDeAlloc : dealloc_inv (mem σ);
}.
- Definition views_mono σ σ'
- := ∀ π, (threads σ !! π : option View) ⊑ (threads σ' !! π).
+ (* Definition views_mono σ σ' *)
+ (* := ∀ π, (threads σ !! π : option View) ⊑ (threads σ' !! π). *)
Definition rel_inv σ σ'
- := msgs_mono (mem σ) (mem σ') ∧ views_mono σ σ' ∧ (nats σ) ⊑ (nats σ').
- Definition all_inv σ σ' := phys_inv σ → phys_inv σ' ∧ rel_inv σ σ'.
+ := msgs_mono (mem σ) (mem σ') ∧ (nats σ) ⊑ (nats σ').
-
- Inductive fork_red (σ : state) (π : thread) : event -> state -> Prop :=
- | fork_fork ρ σ' V
- (ViewOf : threads σ !! π = Some V)
- (Fresh : threads σ !! ρ = None)
- (Hσ : σ' = mkState (<[ρ := V]>(threads σ)) (mem σ) (nats σ))
- : fork_red σ π (EFork ρ) σ'.
+ Inductive fork_red (σ : state) V : event -> state -> Prop :=
+ | fork_fork σ'
+ (Hσ : σ' = σ)
+ : fork_red σ V (EFork V) σ'.
Definition NoWrite (e: event): Prop :=
match e with
@@ -1056,75 +1049,66 @@ Section RAMachine.
| EFork _ => True
end.
- Inductive machine_red (σ : state) (evt : event) (π : thread) (σ' : state) : Prop :=
- | machine_thread V V' otr otw
- (ViewOf : threads σ !! π = Some V)
+ Inductive machine_red (σ : state) (evt : event) V (σ' : state) V' : Prop :=
+ | machine_thread otr otw
(ARed : ∀ x, loc_of evt = Some x -> alloc_red (mem σ) V x evt)
(DRFRed : drf_red σ σ' V otr otw evt)
(NoWriteNats : NoWrite evt -> nats σ' = nats σ)
(NoWriteMsgs : NoWrite evt -> msgs (mem σ') = msgs (mem σ))
(ThreadRed : thread_red V (mem σ) otr otw evt V' (mem σ'))
- (Hσ' : threads σ' = <[π := V']>(threads σ))
- | machine_fork ρ
- (HEvt : evt = EFork ρ)
- (FRed : fork_red σ π evt σ')
+ | machine_fork
+ (HEvt : evt = EFork V')
+ (FRed : fork_red σ V evt σ')
.
- Lemma fork_red_neq σ π ρ σ' : fork_red σ π (EFork ρ) σ' -> ρ ≠ π.
+ (* Lemma fork_red_neq σ π ρ σ' : fork_red σ π (EFork ρ) σ' -> ρ ≠ π. *)
+ (* Proof. *)
+ (* inversion 1. *)
+ (* move => ?; subst. by rewrite Fresh in ViewOf. *)
+ (* Qed. *)
+
+ Lemma machine_red_safe σ evt V σ' V' :
+ phys_inv σ →
+ view_ok (mem σ) V →
+ machine_red σ evt V σ' V' ->
+ phys_inv σ'
+ ∧ view_ok (mem σ') V'
+ ∧ msgs_mono (mem σ) (mem σ')
+ ∧ nats σ ⊑ nats σ'
+ ∧ V ⊑ V'.
Proof.
- inversion 1.
- move => ?; subst. by rewrite Fresh in ViewOf.
- Qed.
-
- Lemma machine_red_safe σ evt π σ' : machine_red σ evt π σ' -> all_inv σ σ'.
- Proof.
- inversion 1.
- - move => Invσ.
- assert (msgs_mono (mem σ) (mem σ')). by eapply thread_red_msgs_mono.
- assert (Tinv': thread_inv V' (mem σ')).
- { eapply thread_red_safe; eauto. split; eapply Invσ; eauto. }
- assert (Tinv: thread_inv V (mem σ)). { split; eapply Invσ; eauto. }
- destruct Tinv as [? HVok], Tinv'.
+ intros [INOk IMOk IAlloc IDealloc] VOk.
+ inversion 1; last first.
+ - inversion FRed. subst. inversion H0. subst.
+ repeat split; auto.
+ + by apply IMOk.
+ + by apply IMOk.
+ + reflexivity.
+ + reflexivity.
+ + reflexivity.
+ - assert (msgs_mono (mem σ) (mem σ')) by by eapply thread_red_msgs_mono.
+ have: (thread_inv V' (mem σ')) => [|[IMOk' VOk']].
+ { eapply thread_red_safe; eauto. by split; auto. }
assert (nats σ ⊑ nats σ'). (* nats_mono *)
- { inversion ThreadRed; subst; first rewrite NoWriteNats => //;
- eapply drf_red_nats_mono; eauto; apply Invσ. }
- do 2 split; auto; last 1 first. split; auto.
- + move => π1. rewrite Hσ'. (* views_mono *)
- apply ext_insert. rewrite ViewOf.
- exact: thread_red_view_mono.
+ { inversion ThreadRed; subst; first rewrite NoWriteNats; (try by auto);
+ eapply drf_red_nats_mono; by eauto. }
+ repeat (split; last split); first split; auto.
+ inversion ThreadRed. (* nats_ok *)
- * rewrite NoWriteNats; subst => //. apply Invσ.
+ * by rewrite NoWriteNats; subst => //.
* replace (add_ins (mem σ) m Disj) with (mem σ').
- eapply drf_red_safe; eauto. apply Invσ.
+ by eapply drf_red_safe; eauto.
* replace (add_ins (mem σ) m Disj) with (mem σ').
- eapply drf_red_safe; eauto. apply Invσ.
- + move => π1 V1 Hlk. rewrite Hσ' in Hlk. (* threads_ok *)
- case (decide (π1 = π)) => Eq; last first.
- * rewrite lookup_insert_ne in Hlk; auto.
- assert (view_ok (mem σ) V1). { eapply Invσ; eauto. }
- eapply view_ok_mono; eauto.
- * rewrite Eq lookup_insert in Hlk. inversion Hlk. by subst.
- + inversion ThreadRed; try (subst; apply Invσ); (* alloc_inv *)
+ by eapply drf_red_safe; eauto.
+ + inversion ThreadRed; try (by subst; apply IAlloc); (* alloc_inv *)
replace (add_ins (mem σ) m Disj) with (mem σ'); subst;
eapply alloc_thread_red_alloc; eauto; subst; auto; apply Invσ.
- + inversion ThreadRed; try (subst; apply Invσ); (* dealloc_inv *)
+ + inversion ThreadRed; try (by subst; apply IDealloc); (* dealloc_inv *)
replace (add_ins (mem σ) m Disj) with (mem σ'); subst;
eapply alloc_thread_red_dealloc; eauto; subst; auto; apply Invσ.
- - inversion FRed; simplify_eq/=. subst.
- destruct 1.
- assert (Tσ : thread_inv V (mem σ)) by (split; eauto).
- split; first split => //=; last split; last split.
- + move => π' /= Vπ'.
- case: (decide (π' = ρ)) => [->|?].
- * rewrite lookup_insert => [[<-]]. by eauto.
- * by rewrite lookup_insert_ne // => /ITOk0.
- + by move => ?.
- + move => π' /=.
- apply: ext_insert.
- by rewrite Fresh.
- + reflexivity.
+ + eapply thread_red_view_mono; eauto. by split.
Qed.
-
End Machine.
End RAMachine.
+
+Arguments machine_red_safe [_ _ _ _ _] _ _ _.
\ No newline at end of file
diff --git a/coq/ra/rsl.v b/coq/ra/rsl.v
index 0584d7a4..4913a719 100644
--- a/coq/ra/rsl.v
+++ b/coq/ra/rsl.v
@@ -249,8 +249,8 @@ Instance InitRaw_persistent V jγ : PersistentP (InitRaw V jγ) := _.
nclose physN ⊆ E →
{{{ PSCtx ∗ ▷ Seen π V ∗ ▷ φ v V ∗ ▷ φd v V
∗ ▷ RSLInv φR φd l n ∗ RelRaw V φ φR n }}}
- ([(#l)]_at <- #v, π) @ E
- {{{ V', RET (#(), π) ;
+ ([(#l)]_at <- #v, V) @ E
+ {{{ V', RET (#(), V') ;
⌜V ⊑ V'⌝ ∗ Seen π V'
∗ ▷ RSLInv φR φd l n ∗ RelRaw V' φ φR n ∗ InitRaw V' n}}}%C.
Proof.
@@ -371,8 +371,8 @@ Instance InitRaw_persistent V jγ : PersistentP (InitRaw V jγ) := _.
nclose physN ⊆ E →
{{{ inv physN PSInv ∗ ▷ Seen π V ∗ (∀ V v, φd v V -∗ φd v V ∗ φd v V)
∗ ▷ RSLInv φR φd l n ∗ AcqRaw V φ n ∗ InitRaw V n }}}
- ([(#l)]_at, π) @ E
- {{{ (v:Z) V', RET (#v, π);
+ ([(#l)]_at, V) @ E
+ {{{ (v:Z) V', RET (#v, V');
⌜V ⊑ V'⌝ ∗ Seen π V'
∗ ▷ RSLInv φR φd l n
∗ AcqRaw V' (<[v:=True%VP]>φ) n ∗ InitRaw V' n
@@ -645,8 +645,8 @@ Instance InitRaw_persistent V jγ : PersistentP (InitRaw V jγ) := _.
Lemma AcqRaw_alloc (φ φd: Z → vPred) E π V:
nclose physN ⊆ E →
{{{ inv physN PSInv ∗ ▷ Seen π V }}}
- (Alloc, π) @ E
- {{{ (l: loc) V' n X, RET (LitV $ LitLoc l, π);
+ (Alloc, V) @ E
+ {{{ (l: loc) V' n X, RET (LitV $ LitLoc l, V');
⌜V ⊑ V'⌝ ∗ Seen π V' ∗ Info l 1 X
∗ ▷ RSLInv φ φd l n ∗ RelRaw V' φ φ n ∗ AcqRaw V' φ n }}}%C.
Proof.
@@ -696,8 +696,8 @@ Instance InitRaw_persistent V jγ : PersistentP (InitRaw V jγ) := _.
Lemma RMWAcqRaw_alloc (φ φd: Z → vPred) E π V:
nclose physN ⊆ E →
{{{ inv physN PSInv ∗ ▷ Seen π V }}}
- (Alloc, π) @ E
- {{{ (l: loc) V' n X, RET (LitV $ LitLoc l, π);
+ (Alloc, V) @ E
+ {{{ (l: loc) V' n X, RET (LitV $ LitLoc l, V');
⌜V ⊑ V'⌝ ∗ Seen π V' ∗ Info l 1 X
∗ ▷ RSLInv φ φd l n ∗ RelRaw V' φ φ n ∗ RMWAcqRaw V' n }}}%C.
Proof.
@@ -807,8 +807,8 @@ Instance InitRaw_persistent V jγ : PersistentP (InitRaw V jγ) := _.
{{{ inv physN PSInv ∗ ▷ Seen π V
∗ ▷ Hist l h ∗ ⌜alloc_local h V⌝
∗ ▷ φ v V ∗ ▷ φd v V}}}
- ([ #l ]_na <- #v, π) @ E
- {{{ V' n, RET (#(), π);
+ ([ #l ]_na <- #v, V) @ E
+ {{{ V' n, RET (#(), V');
⌜V ⊑ V'⌝ ∗ Seen π V' ∗ ▷ RSLInv φ φd l n
∗ RelRaw V' φ φ n ∗ AcqRaw V' φ n ∗ InitRaw V' n }}}%C.
Proof.
@@ -834,8 +834,8 @@ Instance InitRaw_persistent V jγ : PersistentP (InitRaw V jγ) := _.
{{{ inv physN PSInv ∗ ▷ Seen π V
∗ ▷ Hist l h ∗ ⌜alloc_local h V⌝
∗ ▷ φ v V ∗ ▷ φd v V}}}
- ([ #l ]_na <- #v, π) @ E
- {{{ V' n, RET (#(), π);
+ ([ #l ]_na <- #v, V) @ E
+ {{{ V' n, RET (#(), V');
⌜V ⊑ V'⌝ ∗ Seen π V' ∗ ▷ RSLInv φ φd l n
∗ RelRaw V' φ φ n ∗ RMWAcqRaw V' n ∗ InitRaw V' n }}}%C.
Proof.
@@ -865,8 +865,8 @@ Instance InitRaw_persistent V jγ : PersistentP (InitRaw V jγ) := _.
∗ (∀ v, ■ (v ≠ v_r) → P ∗ ▷ φd v ={ E }=∗ R false v)%VP V
∗ inv physN PSInv ∗ ▷ Seen π V
∗ ▷ RSLInv φ φd l n ∗ RMWAcqRaw V n ∗ InitRaw V n ∗ P V}}}
- (CAS #l #v_r #v_w, π) @ E
- {{{ (b: bool) (v': Z) V', RET (LitV $ LitInt b, π);
+ (CAS #l #v_r #v_w, V) @ E
+ {{{ (b: bool) (v': Z) V', RET (LitV $ LitInt b, V');
⌜V ⊑ V'⌝ ∗ Seen π V'
∗ ▷ RSLInv φ φd l n ∗ RMWAcqRaw V' n ∗ InitRaw V' n ∗ R b v' V'}}}.
Proof.
diff --git a/coq/ra/tactics.v b/coq/ra/tactics.v
index cc38b13a..7d4f6912 100644
--- a/coq/ra/tactics.v
+++ b/coq/ra/tactics.v
@@ -29,7 +29,7 @@ Inductive expr0 :=
| CAS (e0 : expr0) (e1 : expr0) (e2 : expr0)
| FAI (C: positive) (e: expr0).
-Definition expr : Type := expr0 * thread.
+Definition expr : Type := expr0 * View.
Fixpoint to_expr' (e : expr0) : base.expr :=
match e return base.expr with
diff --git a/coq/ra/tests/message_passing.v b/coq/ra/tests/message_passing.v
index adcbd2c9..31e61ee4 100644
--- a/coq/ra/tests/message_passing.v
+++ b/coq/ra/tests/message_passing.v
@@ -10,22 +10,19 @@ Let Σ : gFunctors := #[ baseΣ;
uTokΣ ].
Program Definition initial_state :=
- {| threads := {[ 1%positive := ∅ ]};
- mem := mkMemory ∅ (_);
+ {| mem := mkMemory ∅ (_);
nats := ∅ |}.
Next Obligation.
rewrite /pairwise_disj. set_solver.
Qed.
Lemma message_passing :
- adequate (message_passing, 1%positive) initial_state (λ v, v = (LitV (LitInt 37), 1%positive)).
+ adequate (message_passing, ∅) initial_state (λ v, v.1 = LitV (LitInt 37)).
Proof.
apply (base_adequacy Σ _ ∅); auto.
- split; repeat red; rewrite /initial_state /=; try set_solver.
- intros ? ?. case: (decide (π = 1%positive)) => [->|?].
- + rewrite lookup_singleton. move => [<- {V}]. set_solver.
- + rewrite lookup_singleton_ne //.
- - iIntros (?) "[#PS Seen]".
+ - move => ? ?. done.
+ - iIntros (? ?) "[#PS Seen]".
iApply fupd_wp.
iApply fupd_mask_mono;
last iMod (persistor_init with "PS") as (?) "#Pers".
diff --git a/coq/ra/types.v b/coq/ra/types.v
index 0193f6d2..10276756 100644
--- a/coq/ra/types.v
+++ b/coq/ra/types.v
@@ -67,7 +67,7 @@ Section Definitions.
| ERead : access -> positive -> Val -> event
| EWrite : access -> positive -> Val -> event
| EUpdate : positive -> Val -> Val -> event
- | EFork : thread -> event
+ | EFork : View -> event
.
Definition acc_of : event -> option access :=
diff --git a/coq/ra/weakestpre.v b/coq/ra/weakestpre.v
index 55d0f81f..368bf27c 100644
--- a/coq/ra/weakestpre.v
+++ b/coq/ra/weakestpre.v
@@ -2,56 +2,56 @@ From iris.program_logic Require Import weakestpre.
From ra Require Import lang viewpred.
From ra.base Require Import ghosts.
-Section WeakestPre.
- Context `{foundationG Σ}.
- Notation iProp := (iProp Σ).
- Notation vPred := (@vPred Σ).
+(* Section WeakestPre. *)
+(* Context `{foundationG Σ}. *)
+(* Notation iProp := (iProp Σ). *)
+(* Notation vPred := (@vPred Σ). *)
- Definition vPred_wp_aux E (e : ra_lang.expr) (Φ : base.val -> vPred) : View -> iProp :=
- (↑ (λ V, ∀ Ψ,
- PSCtx
- -∗ Seen (snd e) V
- -∗ (∀ v V', ⌜V ⊑ V'⌝ -∗ Seen (snd e) V' -∗ Φ v V' -∗ Ψ (v, snd e))
- -∗ WP e @ E {{ Ψ }}
- )%I).
- Definition vPred_wp_mono E e Φ : vPred_Mono (vPred_wp_aux E e Φ) := vProp_upclose_mono _.
- Canonical Structure vPred_wp E e Φ : vPred :=
- Build_vPred _ (vPred_wp_mono E e Φ).
+(* Definition vPred_wp_aux E (e : ra_lang.expr) (Φ : base.val -> vPred) : View -> iProp := *)
+(* (↑ (λ V, ∀ π Ψ, *)
+(* PSCtx *)
+(* -∗ Seen π V *)
+(* -∗ (∀ v V', ⌜V ⊑ V'⌝ -∗ Seen π V' -∗ Φ v V' -∗ Ψ (v, snd e)) *)
+(* -∗ WP e @ E {{ Ψ }} *)
+(* )%I). *)
+(* Definition vPred_wp_mono E e Φ : vPred_Mono (vPred_wp_aux E e Φ) := vProp_upclose_mono _. *)
+(* Canonical Structure vPred_wp E e Φ : vPred := *)
+(* Build_vPred _ (vPred_wp_mono E e Φ). *)
- (* Definition vPred_hoare_aux E e Φ P := *)
- (* vPred_ipure (∀ π V, Seen π V -∗ P V -∗ vPred_wp E (e,π) Φ V)%I. *)
+(* (* Definition vPred_hoare_aux E e Φ P := *) *)
+(* (* vPred_ipure (∀ π V, Seen π V -∗ P V -∗ vPred_wp E (e,π) Φ V)%I. *) *)
- (* Lemma vwp_bind *)
- (* (E : coPset) (e : ra_lang.expr) *)
- (* (K : list base.ectx_item) (Φ : _ → vPred) V: *)
- (* (WP e @ E {{ v, ∃ V', ⌜V ⊑ V'⌝ ∗ Seen (snd e) V' ∗ vPred_wp E (foldr base.fill_item (base.of_val (v.1)) K, (snd e)) Φ V' }} -∗ PSCtx -∗ WP fill K (e) @ E {{ v, ∃ V', ⌜V ⊑ V'⌝ ∗ Seen (snd e) V' ∗ Φ (v.1) V' }}). *)
- (* Proof. *)
- (* iIntros "WP #kI". *)
- (* destruct e. *)
- (* etrans; [|fast_by apply (lifting.wp_bindt K)]. *)
- (* iApply lifting.wp_thread. simpl. *)
- (* iApply (wp_mono with "[kI WP]"); last first. *)
- (* - iApply (wp_frame_l). iCombine "kI" "kS" as "k". by iFrame "k WP". *)
- (* - iIntros (?) "([#kI kS] & WP)". *)
- (* iDestruct "WP" as (V') "(% & kS' & WP)" . *)
- (* iSpecialize ("WP" $! V' with "[%] kI kS'"); [done|]. simpl. *)
- (* rewrite tactics.W.fill_unfold. simpl. *)
- (* iApply (wp_mono with "WP"). iIntros (?) "P". *)
- (* iDestruct "P" as (V'') "(% & ? & ?)". *)
- (* iExists V''. iFrame "∗". iPureIntro. etrans; eauto. *)
- (* Qed. *)
+(* (* Lemma vwp_bind *) *)
+(* (* (E : coPset) (e : ra_lang.expr) *) *)
+(* (* (K : list base.ectx_item) (Φ : _ → vPred) V: *) *)
+(* (* (WP e @ E {{ v, ∃ V', ⌜V ⊑ V'⌝ ∗ Seen (snd e) V' ∗ vPred_wp E (foldr base.fill_item (base.of_val (v.1)) K, (snd e)) Φ V' }} -∗ PSCtx -∗ WP fill K (e) @ E {{ v, ∃ V', ⌜V ⊑ V'⌝ ∗ Seen (snd e) V' ∗ Φ (v.1) V' }}). *) *)
+(* (* Proof. *) *)
+(* (* iIntros "WP #kI". *) *)
+(* (* destruct e. *) *)
+(* (* etrans; [|fast_by apply (lifting.wp_bindt K)]. *) *)
+(* (* iApply lifting.wp_thread. simpl. *) *)
+(* (* iApply (wp_mono with "[kI WP]"); last first. *) *)
+(* (* - iApply (wp_frame_l). iCombine "kI" "kS" as "k". by iFrame "k WP". *) *)
+(* (* - iIntros (?) "([#kI kS] & WP)". *) *)
+(* (* iDestruct "WP" as (V') "(% & kS' & WP)" . *) *)
+(* (* iSpecialize ("WP" $! V' with "[%] kI kS'"); [done|]. simpl. *) *)
+(* (* rewrite tactics.W.fill_unfold. simpl. *) *)
+(* (* iApply (wp_mono with "WP"). iIntros (?) "P". *) *)
+(* (* iDestruct "P" as (V'') "(% & ? & ?)". *) *)
+(* (* iExists V''. iFrame "∗". iPureIntro. etrans; eauto. *) *)
+(* (* Qed. *) *)
- (* Lemma vwp_bindt *)
- (* {E : coPset} {e : base.expr} {π : thread} *)
- (* (K : list base.ectx_item) (Φ : _ → vPred) V: *)
- (* (WP ((e, π) : ra_lang.expr) @ E {{ v, vPred_wp E (fill K (of_val v)) Φ V }} -∗ PSCtx -∗ Seen π V -∗ WP fill K (e, π) @ E {{ v, ∃ V', ⌜V ⊑ V'⌝ ∗ Seen π V' ∗ Φ (v.1) V' }}). *)
- (* Proof. *)
- (* iIntros. iApply (vwp_bind _ (e, π) with "[-] [#] [#]"); auto. *)
- (* rewrite /of_val. setoid_rewrite tactics.W.fill_unfold. *)
- (* iPoseProof (lifting.wp_thread_rev with "[-]") as "T"; [done|done]. *)
- (* Qed. *)
+(* (* Lemma vwp_bindt *) *)
+(* (* {E : coPset} {e : base.expr} {π : thread} *) *)
+(* (* (K : list base.ectx_item) (Φ : _ → vPred) V: *) *)
+(* (* (WP ((e, V_l) : ra_lang.expr) @ E {{ v, vPred_wp E (fill K (of_val v)) Φ V }} -∗ PSCtx -∗ Seen π V -∗ WP fill K (e, V_l) @ E {{ v, ∃ V', ⌜V ⊑ V'⌝ ∗ Seen π V' ∗ Φ (v.1) V' }}). *) *)
+(* (* Proof. *) *)
+(* (* iIntros. iApply (vwp_bind _ (e, V_l) with "[-] [#] [#]"); auto. *) *)
+(* (* rewrite /of_val. setoid_rewrite tactics.W.fill_unfold. *) *)
+(* (* iPoseProof (lifting.wp_thread_rev with "[-]") as "T"; [done|done]. *) *)
+(* (* Qed. *) *)
-End WeakestPre.
+(* End WeakestPre. *)
(* Ltac vwp_bind_core K := *)
(* lazymatch eval hnf in K with *)
@@ -93,8 +93,8 @@ Notation "'{{{{' P } } } } e {{{{ x .. y , 'RET' pat ; Q } } } }" :=
PSCtx
-∗ Seen π V_l
-∗ ((P V_l)%VP)%VP
- -∗ ▷ (vProp_upclose (λ V, ∀ x, .. (∀ y, Seen π V -∗ ((Q V)%VP)%VP -∗ Φ (pat, π)%Val) .. ) V_l)
- -∗ WP (e, π) {{ Φ }}
+ -∗ ▷ (vProp_upclose (λ V, ∀ x, .. (∀ y, Seen π V -∗ ((Q V)%VP)%VP -∗ Φ (pat, V)%Val) .. ) V_l)
+ -∗ WP (e, V_l) {{ Φ }}
) V_l)
)%I
(at level 20, x closed binder, y closed binder,
@@ -105,8 +105,8 @@ Notation "'{{{{' P } } } } e @ E {{{{ x .. y , 'RET' pat ; Q } } } }" :=
PSCtx
-∗ Seen π V_l
-∗ ((P V_l)%VP)%VP
- -∗ ▷ (vProp_upclose (λ V, ∀ x, .. (∀ y, Seen π V -∗ (Q V)%VP -∗ Φ (pat, π)%Val) .. ) V_l)
- -∗ WP (e, π) @ E {{ Φ }}
+ -∗ ▷ (vProp_upclose (λ V, ∀ x, .. (∀ y, Seen π V -∗ (Q V)%VP -∗ Φ (pat, V)%Val) .. ) V_l)
+ -∗ WP (e, V_l) @ E {{ Φ }}
) V_l)
)%I
(at level 20, x closed binder, y closed binder,
@@ -117,8 +117,8 @@ Notation "'{{{{' P } } } } e {{{{ 'RET' pat ; Q } } } }" :=
PSCtx
-∗ Seen π V_l
-∗ ((P V_l)%VP)%VP
- -∗ ▷ (vProp_upclose (λ V, Seen π V -∗ (Q V)%VP -∗ Φ (pat, π)%Val) V_l)
- -∗ WP (e, π) {{ Φ }}
+ -∗ ▷ (vProp_upclose (λ V, Seen π V -∗ (Q V)%VP -∗ Φ (pat, V)%Val) V_l)
+ -∗ WP (e, V_l) {{ Φ }}
) V_l)
)%I
(at level 20,
@@ -129,8 +129,8 @@ Notation "'{{{{' P } } } } e @ E {{{{ 'RET' pat ; Q } } } }" :=
PSCtx
-∗ Seen π V_l
-∗ ((P V_l)%VP)%VP
- -∗ ▷ (vProp_upclose (λ V, Seen π V -∗ (Q V)%VP -∗ Φ (pat, π)%Val) V_l)
- -∗ WP (e, π) @ E {{ Φ }}
+ -∗ ▷ (vProp_upclose (λ V, Seen π V -∗ (Q V)%VP -∗ Φ (pat, V)%Val) V_l)
+ -∗ WP (e, V_l) @ E {{ Φ }}
) V_l)
)%I
(at level 20,
@@ -143,8 +143,8 @@ Notation "'{{{{' P } } } } e {{{{ x .. y , 'RET' pat ; Q } } } }" :=
PSCtx
-∗ Seen π V_l
-∗ (P V_l)%VP
- -∗ ▷ (vProp_upclose (λ V, ∀ x, .. (∀ y, Seen π V -∗ (Q V)%VP -∗ Φ (pat, π)%Val) .. ) V_l)
- -∗ WP (e, π) {{ Φ }}
+ -∗ ▷ (vProp_upclose (λ V, ∀ x, .. (∀ y, Seen π V -∗ (Q V)%VP -∗ Φ (pat, V)%Val) .. ) V_l)
+ -∗ WP (e, V_l) {{ Φ }}
)%I V_l
)
(at level 20, x closed binder, y closed binder,
@@ -155,8 +155,8 @@ Notation "'{{{{' P } } } } e @ E {{{{ x .. y , 'RET' pat ; Q } } } }" :=
PSCtx
-∗ Seen π V_l
-∗ ((P V_l)%VP)%VP
- -∗ ▷ (vProp_upclose (λ V, ∀ x, .. (∀ y, Seen π V -∗ (Q V)%VP -∗ Φ (pat, π)%Val) .. ) V_l)
- -∗ WP (e, π) @ E {{ Φ }}
+ -∗ ▷ (vProp_upclose (λ V, ∀ x, .. (∀ y, Seen π V -∗ (Q V)%VP -∗ Φ (pat, V)%Val) .. ) V_l)
+ -∗ WP (e, V_l) @ E {{ Φ }}
)%I V_l
)
(at level 20, x closed binder, y closed binder,
@@ -167,8 +167,8 @@ Notation "'{{{{' P } } } } e {{{{ 'RET' pat ; Q } } } }" :=
PSCtx
-∗ Seen π V_l
-∗ ((P V_l)%VP)%VP
- -∗ ▷ (vProp_upclose (λ V, Seen π V -∗ (Q V)%VP -∗ Φ (pat, π)%Val) V_l)
- -∗ WP (e, π) {{ Φ }}
+ -∗ ▷ (vProp_upclose (λ V, Seen π V -∗ (Q V)%VP -∗ Φ (pat, V)%Val) V_l)
+ -∗ WP (e, V_l) {{ Φ }}
)%I V_l
)
(at level 20,
@@ -179,8 +179,8 @@ Notation "'{{{{' P } } } } e @ E {{{{ 'RET' pat ; Q } } } }" :=
PSCtx
-∗ Seen π V_l
-∗ ((P V_l)%VP)%VP
- -∗ ▷ (vProp_upclose (λ V, Seen π V -∗ (Q V)%VP -∗ Φ (pat, π)%Val) V_l)
- -∗ WP (e, π) @ E {{ Φ }}
+ -∗ ▷ (vProp_upclose (λ V, Seen π V -∗ (Q V)%VP -∗ Φ (pat, V)%Val) V_l)
+ -∗ WP (e, V_l) @ E {{ Φ }}
)%I V_l
)
(at level 20,
--
GitLab