Commit 2fc89d3d authored by Joseph Tassarotti's avatar Joseph Tassarotti
Browse files

Fix some import structure; make some uPred notation local to avoid conflict;...

Fix some import structure; make some uPred notation local to avoid conflict; make iPsvs closer to old behavior.
parent 274019f4
......@@ -22,9 +22,6 @@ theories/algebra/excl.v
theories/algebra/iprod.v
theories/algebra/upred.v
theories/algebra/upred_bi.v
theories/algebra/upred_tactics.v
theories/algebra/upred_big_op.v
theories/algebra/upred_hlist.v
theories/algebra/base_logic.v
theories/algebra/frac.v
theories/algebra/csum.v
......
From fri.algebra Require Export cmra.
From fri.algebra Require Import upred.
From fri.algebra Require Import upred upred_bi.
Local Hint Extern 10 (_ _) => omega.
Record agree (A : Type) : Type := Agree {
......@@ -110,7 +110,7 @@ Canonical Structure agreeR : cmraT :=
Global Instance agree_total : CMRATotal agreeR.
Proof. rewrite /CMRATotal; eauto. Qed.
Global Instance agree_persistent (x : agree A) : Persistent x.
Global Instance agree_persistent (x : agree A) : cmra.Persistent x.
Proof. by constructor. Qed.
Program Definition to_agree (x : A) : agree A :=
......
From iris.bi Require Export bi.
From iris.proofmode Require Import tactics.
(*
From iris.algebra Require Import proofmode_classes.
*)
From fri.algebra Require Export upred_bi.
From fri.algebra Require Export upred upred_bi.
Module Import uPred.
Export upred.uPred.
Export bi.
......
From fri.algebra Require Export cmra.
From fri.algebra Require Import upred updates local_updates.
From fri.algebra Require Import upred upred_bi updates local_updates.
Local Arguments pcore _ _ !_ /.
Local Arguments cmra_pcore _ !_ /.
Local Arguments validN _ _ _ !_ /.
......@@ -235,10 +235,10 @@ Proof.
by move=>[a|b|] HH /=; try apply cmra_discrete_valid.
Qed.
Global Instance Cinl_persistent a : Persistent a Persistent (Cinl a).
Proof. rewrite /Persistent /=. inversion_clear 1; by repeat constructor. Qed.
Global Instance Cinr_persistent b : Persistent b Persistent (Cinr b).
Proof. rewrite /Persistent /=. inversion_clear 1; by repeat constructor. Qed.
Global Instance Cinl_persistent a : cmra.Persistent a cmra.Persistent (Cinl a).
Proof. rewrite /cmra.Persistent /=. inversion_clear 1; by repeat constructor. Qed.
Global Instance Cinr_persistent b : cmra.Persistent b cmra.Persistent (Cinr b).
Proof. rewrite /cmra.Persistent /=. inversion_clear 1; by repeat constructor. Qed.
Global Instance Cinl_exclusive a : Exclusive a Exclusive (Cinl a).
Proof. by move=> H[]? =>[/H||]. Qed.
......
From fri.algebra Require Export cmra.
From fri.algebra Require Import upred.
From fri.algebra Require Import upred upred_bi.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
......
From Coq.QArith Require Import Qcanon.
From fri.algebra Require Export cmra.
From fri.algebra Require Import upred.
From fri.algebra Require Import upred upred_bi.
Notation frac := Qp (only parsing).
......@@ -24,7 +24,7 @@ Proof. eauto with typeclass_instances. Qed.
End frac.
(** Internalized properties *)
Lemma frac_equivI {M} (x y : frac) : x y ⊣⊢ (x = y : uPred M).
Lemma frac_equivI {M} (x y : frac) : x y ⊣⊢ ( (x = y) : uPred M).
Proof. by uPred.unseal. Qed.
Lemma frac_validI {M} (x : frac) : x ⊣⊢ ( (x 1)%Qc : uPred M).
Proof. by uPred.unseal. Qed.
......
From fri.algebra Require Export cmra.
From stdpp Require Export gmap.
From fri.algebra Require Import upred updates local_updates.
From fri.algebra Require Import upred upred_bi updates local_updates.
Section cofe.
Context `{Countable K} {A : ofeT}.
......@@ -222,13 +222,13 @@ Lemma op_singleton (i : K) (x y : A) :
{[ i := x ]} {[ i := y ]} = ({[ i := x y ]} : gmap K A).
Proof. by apply (merge_singleton _ _ _ x y). Qed.
Global Instance gmap_persistent m : ( x : A, Persistent x) Persistent m.
Global Instance gmap_persistent m : ( x : A, cmra.Persistent x) cmra.Persistent m.
Proof.
intros; apply persistent_total=> i.
rewrite lookup_core. apply (persistent_core _).
Qed.
Global Instance gmap_singleton_persistent i (x : A) :
Persistent x Persistent {[ i := x ]}.
cmra.Persistent x cmra.Persistent {[ i := x ]}.
Proof. intros. by apply persistent_total, core_singleton'. Qed.
Lemma singleton_includedN n m i x :
......
From fri.algebra Require Export cmra updates.
From fri.algebra Require Import upred.
From fri.algebra Require Import upred upred_bi.
From stdpp Require Import finite.
(** * Indexed product *)
......@@ -211,7 +211,7 @@ Section iprod_singleton.
Qed.
Global Instance iprod_singleton_persistent x (y : B x) :
Persistent y Persistent (iprod_singleton x y).
cmra.Persistent y cmra.Persistent (iprod_singleton x y).
Proof. by rewrite !persistent_total iprod_core_singleton=> ->. Qed.
Lemma iprod_op_singleton (x : A) (y1 y2 : B x) :
......
From fri.algebra Require Export cmra.
From stdpp Require Export list.
From fri.algebra Require Import upred updates local_updates.
From fri.algebra Require Import upred upred_bi updates local_updates.
Section cofe.
Context {A : ofeT}.
......@@ -209,7 +209,7 @@ Section cmra.
by apply cmra_discrete_valid.
Qed.
Global Instance list_persistent l : ( x : A, Persistent x) Persistent l.
Global Instance list_persistent l : ( x : A, cmra.Persistent x) cmra.Persistent l.
Proof.
intros ?; constructor; apply list_equiv_lookup=> i.
by rewrite list_lookup_core (persistent_core (l !! i)).
......@@ -306,7 +306,7 @@ Section properties.
rewrite /singletonM /list_singletonM /=. induction i; f_equal/=; auto.
Qed.
Global Instance list_singleton_persistent i (x : A) :
Persistent x Persistent {[ i := x ]}.
cmra.Persistent x cmra.Persistent {[ i := x ]}.
Proof. by rewrite !persistent_total list_core_singletonM=> ->. Qed.
(* Update *)
......
......@@ -357,13 +357,13 @@ Definition uPred_emp_eq :
@uPred_emp = @uPred_emp_def := proj2_sig uPred_emp_aux.
Notation "P ⊢ Q" := (uPred_entails P%IP Q%IP)
Local Notation "P ⊢ Q" := (uPred_entails P%IP Q%IP)
(at level 99, Q at level 200, right associativity) : stdpp_scope.
Notation "(⊢)" := uPred_entails (only parsing) : stdpp_scope.
Notation "P ⊣⊢ Q" := (equiv (A:=uPred _) P%IP Q%IP)
Local Notation "(⊢)" := uPred_entails (only parsing) : stdpp_scope.
Local Notation "P ⊣⊢ Q" := (equiv (A:=uPred _) P%IP Q%IP)
(at level 95, no associativity) : stdpp_scope.
Notation "(⊣⊢)" := (equiv (A:=uPred _)) (only parsing) : stdpp_scope.
Notation "■ φ" := (uPred_pure φ%stdpp%type)
Local Notation "(⊣⊢)" := (equiv (A:=uPred _)) (only parsing) : stdpp_scope.
Local Notation "■ φ" := (uPred_pure φ%stdpp%type)
(at level 20, right associativity) : uPred_scope.
Notation "x = y" := (uPred_pure (x%stdpp%type = y%stdpp%type)) : uPred_scope.
Notation "x ## y" := (uPred_pure (x%stdpp%type ## y%stdpp%type)) : uPred_scope.
......
From stdpp Require Export hlist.
From fri.algebra Require Export upred.
From fri.algebra Require Export upred upred_bi.
Import uPred.
Fixpoint uPred_hexist {M As} : himpl As (uPred M) uPred M :=
......@@ -21,9 +21,9 @@ Lemma hexist_exist {As B} (f : himpl As B) (Φ : B → uPred M) :
Proof.
apply (anti_symm _).
- induction As as [|A As IH]; simpl.
+ by rewrite -(exist_intro hnil) .
+ by rewrite -(bi.exist_intro hnil) .
+ apply exist_elim=> x; rewrite IH; apply exist_elim=> xs.
by rewrite -(exist_intro (hcons x xs)).
by rewrite -(bi.exist_intro (hcons x xs)).
- apply exist_elim=> xs; induction xs as [|A As x xs IH]; simpl; auto.
by rewrite -(exist_intro x) IH.
Qed.
......@@ -35,8 +35,8 @@ Proof.
- apply forall_intro=> xs; induction xs as [|A As x xs IH]; simpl; auto.
by rewrite (forall_elim x) IH.
- induction As as [|A As IH]; simpl.
+ by rewrite (forall_elim hnil) .
+ by rewrite (bi.forall_elim hnil) .
+ apply forall_intro=> x; rewrite -IH; apply forall_intro=> xs.
by rewrite (forall_elim (hcons x xs)).
by rewrite (bi.forall_elim (hcons x xs)).
Qed.
End hlist.
From fri.algebra Require Export base_logic.
From fri.heap_lang Require Export lifting.
Import uPred.
......
From fri.heap_lang Require Export lifting.
From fri.algebra Require Import upred_big_op frac dec_agree.
From fri.algebra Require Import base_logic frac dec_agree.
From fri.program_logic Require Export invariants ghost_ownership.
From fri.program_logic Require Import ownership auth.
From fri.proofmode Require Import weakestpre.
From iris.proofmode Require Import tactics.
Import uPred.
(* TODO: The entire construction could be generalized to arbitrary languages that have
a finmap as their state. Or maybe even beyond "as their state", i.e. arbitrary
......@@ -39,9 +39,9 @@ Section definitions.
Global Instance heap_inv_proper : Proper (() ==> (⊣⊢)) heap_inv.
Proof. solve_proper. Qed.
Global Instance heap_ctx_relevant : RelevantP heap_ctx.
Global Instance heap_ctx_relevant : derived_connectives.Persistent heap_ctx.
Proof. apply _. Qed.
Global Instance heap_ctx_affine : AffineP heap_ctx.
Global Instance heap_ctx_affine : Affine heap_ctx.
Proof. apply _. Qed.
End definitions.
......@@ -51,8 +51,8 @@ Instance: Params (@heap_mapsto) 4.
Instance: Params (@heap_ctx) 2.
Notation "l ↦{ q } v" := (heap_mapsto l q v)
(at level 20, q at level 50, format "l ↦{ q } v") : uPred_scope.
Notation "l ↦ v" := (heap_mapsto l 1 v) (at level 20) : uPred_scope.
(at level 20, q at level 50, format "l ↦{ q } v") : bi_scope.
Notation "l ↦ v" := (heap_mapsto l 1 v) (at level 20) : bi_scope.
Section heap.
Context {Σ : gFunctors}.
......@@ -107,18 +107,18 @@ Section heap.
(** Allocation *)
Lemma heap_alloc E σ :
authG heap_lang Σ heapUR nclose heapN E
ownP σ ={E}=> _ : heapG Σ, heap_ctx [ map] lv σ, l v.
ownP σ ={E}=> _ : heapG Σ, heap_ctx [ map] lv σ, l v.
Proof.
intros. rewrite -{1}(from_to_heap σ). etrans.
{rewrite [ownP _](affine_intro _ (ownP (of_heap (to_heap σ)))); last auto.
{rewrite [ownP _](affinely_intro _ (ownP (of_heap (to_heap σ)))); last auto.
rewrite [ownP _]later_intro.
apply (auth_alloc (ownP of_heap) heapN E); auto using to_heap_valid. }
apply pvs_mono, exist_elim=> γ.
rewrite -(exist_intro (HeapG _ _ γ)) /heap_ctx. apply sep_mono_r.
rewrite heap_mapsto_eq /heap_mapsto_def /heap_name.
induction σ as [|l v σ Hl IH] using map_ind.
{ rewrite big_sepM_empty. rewrite emp_True.
rewrite /auth_own. apply affine_intro; first apply _; auto. }
{ rewrite big_sepM_empty. rewrite -(affinely_affine emp%I) -affinely_True_emp.
rewrite /auth_own. apply affinely_intro; first apply _; auto. }
rewrite to_heap_insert big_sepM_insert //.
rewrite (insert_singleton_op (to_heap σ));
first by rewrite lookup_fmap Hl; auto.
......@@ -128,47 +128,46 @@ Section heap.
Context `{heapG Σ}.
(** General properties of mapsto *)
Global Instance heap_mapsto_timeless l q v : ATimelessP (l {q} v).
Global Instance heap_mapsto_timeless l q v : ATimeless (l {q} v).
Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
Global Instance heap_mapsto_affine l q v : AffineP (l {q} v).
Global Instance heap_mapsto_affine l q v : Affine (l {q} v).
Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
Global Instance heap_mapsto_map_affine σ:
AffineP ([ map] lv ∈σ, l v)%I.
Proof.
intros; apply big_sep_affine.
rewrite /AffineL. induction map_to_list as [| a ?]; simpl; eauto using nil_affine.
destruct a; simpl; apply cons_affine; eauto using heap_mapsto_affine.
Qed.
Affine ([ map] lv σ, l v)%I.
Proof. apply big_sepM_affine => ??; apply _. Qed.
Lemma heap_mapsto_op_eq l q1 q2 v : (l {q1} v l {q2} v) ⊣⊢ l {q1+q2} v.
Lemma heap_mapsto_op_eq l q1 q2 v : (l {q1} v l {q2} v)%I ⊣⊢ (l {q1+q2} v)%I.
Proof. by rewrite heap_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_idemp. Qed.
Lemma heap_mapsto_op l q1 q2 v1 v2 :
(l {q1} v1 l {q2} v2) ⊣⊢ ( (v1 = v2) l {q1+q2} v1).
(l {q1} v1 l {q2} v2)%I ⊣⊢ ( (v1 = v2) l {q1+q2} v1)%I.
Proof.
destruct (decide (v1 = v2)) as [->|].
{ by rewrite heap_mapsto_op_eq pure_equiv // -emp_True left_id. }
{ rewrite heap_mapsto_op_eq //=.
setoid_replace (v2 = v2) with True by rewrite //=.
by rewrite affinely_True_emp affinely_emp left_id. }
rewrite heap_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_ne //.
apply (anti_symm ()); last by apply pure_elim_sep_l.
apply (anti_symm ()); last first.
{ iIntros "(%&?)"; subst; rewrite //=. }
rewrite auth_own_valid gmap_validI (forall_elim l) lookup_singleton.
rewrite option_validI prod_validI frac_validI discrete_valid.
rewrite affine_and comm affine_elim comm.
rewrite affinely_and comm affinely_elim comm.
by apply pure_elim_r.
Qed.
Lemma heap_mapsto_op_split l q v : l {q} v ⊣⊢ (l {q/2} v l {q/2} v).
Lemma heap_mapsto_op_split l q v : (l {q} v)%I ⊣⊢ (l {q/2} v l {q/2} v)%I.
Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed.
(** Weakest precondition *)
(* FIXME: try to reduce usage of wp_pvs. We're losing view shifts here. *)
Lemma wp_alloc E e v Φ :
to_val e = Some v nclose heapN E
(heap_ctx l, l v - |={E heapN}=>> Φ (LitV $ LitLoc l)) WP Alloc e @ E {{ Φ }}.
to_val e = Some v heapN E
(heap_ctx l, l v - |={E heapN}=>> Φ (LitV $ LitLoc l)) WP Alloc e @ E {{ Φ }}.
Proof.
iIntros (<-%of_to_val ?) "[#Hinv HΦ]". rewrite /heap_ctx.
iPvs (auth_empty heap_name) as "Hheap".
iMod (auth_empty heap_name with "[#]") as "Hheap"; first auto.
iApply wp_pvs; iApply (auth_afsa_alt heap_inv (wp_fsa _)); eauto with fsaV.
iFrame "Hinv". iSplitL "Hheap"; first (iIntros "@"; by iNext).
iFrame "Hinv". iSplitL "Hheap"; first (iAlways; by iNext).
iIntros (h). rewrite left_id.
iIntros "[% Hheap]". rewrite /heap_inv.
pose (l := fresh (dom (gset loc) (of_heap h))).
......@@ -182,7 +181,7 @@ Section heap.
iApply wp_alloc_pst'. iFrame "Hheap". iNext.
iIntros "Hheap".
rewrite -of_heap_insert.
rewrite -{1}(affine_affine (ownP _)) {1}(later_intro (ownP _)).
rewrite -{1}(affine_affinely (ownP _)) {1}(later_intro (ownP _)).
iFrame "Hheap".
iSpecialize ("HΦ" $! l). rewrite -(pvs_intro).
iApply "HΦ". by rewrite heap_mapsto_eq /heap_mapsto_def.
......@@ -190,7 +189,7 @@ Section heap.
Lemma wp_load E l q v Φ :
nclose heapN E
(heap_ctx ⧆▷ l {q} v ( l {q} v - |={E heapN}=>> (Φ v)))
(heap_ctx ⧆▷ l {q} v ( l {q} v - |={E heapN}=>> (Φ v)))
WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Proof.
iIntros (?) "[#Hh [Hl HΦ]]".
......@@ -203,16 +202,16 @@ Section heap.
iIntros "Hauth".
iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));first by rewrite lookup_insert.
rewrite of_heap_singleton_op //. iFrame "Hl".
iIntros "> Hown".
rewrite -{1}(affine_affine (ownP _)).
iNext. iIntros "Hown".
rewrite -{1}(affine_affinely (ownP _)).
rewrite {1}(later_intro (ownP _)).
iFrame "Hown". rewrite -pvs_intro. iApply "HΦ".
by iIntros "@".
by iAlways.
Qed.
Lemma wp_store E l v' e v Φ :
to_val e = Some v nclose heapN E
(heap_ctx ⧆▷ l v' (l v - |={E heapN}=>> ( Φ (LitV LitUnit))))
(heap_ctx ⧆▷ l v' (l v - |={E heapN}=>> ( Φ (LitV LitUnit))))
WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Proof.
iIntros (<-%of_to_val ?) "[#Hh [Hl HΦ]]".
......@@ -225,8 +224,8 @@ Section heap.
iIntros "Hauth".
iApply (wp_store_pst _ (<[l:=v']>(of_heap h))); eauto; first by rewrite lookup_insert.
rewrite of_heap_singleton_op //. iFrame "Hl".
iIntros "> Hown".
rewrite -{1}(affine_affine (ownP _)).
iNext; iIntros "Hown".
rewrite -{1}(affine_affinely (ownP _)).
rewrite {1}(later_intro (ownP _)).
rewrite insert_insert !of_heap_singleton_op; eauto.
iFrame "Hown". rewrite -pvs_intro. by iApply "HΦ".
......@@ -235,7 +234,7 @@ Section heap.
Lemma wp_cas_fail E l q v' e1 v1 e2 v2 Φ :
to_val e1 = Some v1 to_val e2 = Some v2 v' v1 nclose heapN E
heap_ctx ⧆▷ l {q} v' (l {q} v' - |={E heapN}=>> Φ (LitV (LitBool false)))
heap_ctx ⧆▷ l {q} v' (l {q} v' - |={E heapN}=>> Φ (LitV (LitBool false)))
WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof.
iIntros (<-%of_to_val <-%of_to_val ??) "[#Hh [Hl HΦ]]".
......@@ -249,14 +248,14 @@ Section heap.
iApply (wp_cas_fail_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
rewrite of_heap_singleton_op //. iFrame "Hl". iNext.
iIntros "HownP".
rewrite -{1}(affine_affine (ownP _)).
rewrite -{1}(affine_affinely (ownP _)).
rewrite {1}(later_intro (ownP _)).
iFrame "HownP". iApply "HΦ"; done.
Qed.
Lemma wp_cas_suc E l e1 v1 e2 v2 Φ :
to_val e1 = Some v1 to_val e2 = Some v2 nclose heapN E
heap_ctx ⧆▷ l v1 (l v2 - |={E heapN}=>> (Φ (LitV (LitBool true))))
heap_ctx ⧆▷ l v1 (l v2 - |={E heapN}=>> (Φ (LitV (LitBool true))))
WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof.
iIntros (<-%of_to_val <-%of_to_val ?) "[#Hh [Hl HΦ]]".
......@@ -271,16 +270,15 @@ Section heap.
rewrite insert_insert !of_heap_singleton_op; eauto.
iFrame "Hl". iNext.
iIntros "HownP".
rewrite -{1}(affine_affine (ownP _)).
rewrite -{1}(affine_affinely (ownP _)).
rewrite {1}(later_intro (ownP _)).
iFrame "HownP".
iApply psvs_mono; last auto. iIntros "$"; auto.
iApply ("HΦ"); done.
by iApply "HΦ".
Qed.
Lemma wp_swap E l v e v' Φ :
to_val e = Some v' nclose heapN E
heap_ctx ⧆▷ l v (l v' - |={E heapN}=>> (Φ v))
heap_ctx ⧆▷ l v (l v' - |={E heapN}=>> (Φ v))
WP Swap (Lit (LitLoc l)) e @ E {{ Φ }}.
Proof.
iIntros (<-%of_to_val ?) "[#Hh [Hl HΦ]]".
......@@ -295,17 +293,16 @@ Section heap.
rewrite insert_insert !of_heap_singleton_op; eauto.
iFrame "Hl". iNext.
iIntros "HownP".
rewrite -{1}(affine_affine (ownP _)).
rewrite -{1}(affine_affinely (ownP _)).
rewrite {1}(later_intro (ownP _)).
iFrame "HownP".
iApply psvs_mono; last auto. iIntros "$"; auto.
iApply ("HΦ"); done.
by iApply "HΦ".
Qed.
Lemma wp_fai E l k Φ :
nclose heapN E
heap_ctx ⧆▷ l (LitV $ LitInt k)
(l (LitV $ LitInt (k+1)) - |={E heapN}=>> (Φ (LitV $ LitInt k)))
(l (LitV $ LitInt (k+1)) - |={E heapN}=>> (Φ (LitV $ LitInt k)))
WP FAI (Lit (LitLoc l)) @ E {{ Φ }}.
Proof.
iIntros (?) "[#Hh [Hl HΦ]]".
......@@ -320,11 +317,10 @@ Section heap.
rewrite insert_insert !of_heap_singleton_op; eauto.
iFrame "Hl". iNext.
iIntros "HownP".
rewrite -{1}(affine_affine (ownP _)).
rewrite -{1}(affine_affinely (ownP _)).
rewrite {1}(later_intro (ownP _)).
iFrame "HownP".
iApply psvs_mono; last auto. iIntros "$"; auto.
iApply ("HΦ"); done.
by iApply ("HΦ").
Qed.
End heap.
From fri.algebra Require Export upred.
From fri.algebra Require Export base_logic.
From fri.program_logic Require Export weakestpre.
From fri.program_logic Require Import ownership ectx_lifting. (* for ownP *)
From fri.heap_lang Require Export lang.
......@@ -25,21 +25,24 @@ Proof. exact: weakestpre.wp_bind. Qed.
(** Base axioms for core primitives of the language: Stateful reductions. *)
Lemma wp_alloc_pst E σ v Φ :
(⧆▷ ownP σ ( l, (σ !! l = None) ownP (<[l:=v]>σ) - |={E}=>> Φ (LitV (LitLoc l))))
(⧆▷ ownP σ ( l, (σ !! l = None) ownP (<[l:=v]>σ) - |={E}=>> Φ (LitV (LitLoc l))))
WP Alloc (of_val v) @ E {{ Φ }}.
Proof.
iIntros "[HP HΦ]".
iApply (wp_lift_atomic_head_step (Alloc (of_val v)) σ); eauto with fsaV.
iFrame "HP". iNext. iIntros (v2 σ2 ef). rewrite affine_and_r. iIntros "[% HP]". inv_head_step.
iFrame "HP". iNext. iIntros (v2 σ2 ef). rewrite bi.affinely_and_r bi.affinely_and.
iIntros "[% HP]"; inv_head_step.
set (l := fresh (dom (gset positive) σ)).
iSpecialize ("HΦ" $! l).
rewrite pure_equiv //=; last first.
{ apply (not_elem_of_dom (D:= gset loc)), is_fresh. }
rewrite -emp_True left_id. rewrite /ownP.
iPsvs ("HΦ" with "HP").
iSpecialize ("HΦ" with "[HP]").
{ iSplitR.
- iPureIntro. apply (not_elem_of_dom (D:= gset loc)), is_fresh.
- by rewrite /ownP.
}
iPsvs ("HΦ").
rewrite ?right_id.
match goal with H: _ = of_val v2 |- _ => apply (inj of_val (LitV _)) in H end.
iPvsIntro. by subst v2.
iModIntro; by subst v2.
Qed.
(* Stronger form of the above that relies on deterministic allocation *)
......@@ -51,12 +54,13 @@ Proof.
iIntros "[HP HΦ]".
(* TODO: This works around ssreflect bug #22. *)
iApply (wp_lift_atomic_head_step (Alloc (of_val v)) σ); eauto with fsaV.
iFrame "HP". iNext. iIntros (v2 σ2 ef). rewrite affine_and_r. iIntros "[% HP]". inv_head_step.
iFrame "HP". iNext. iIntros (v2 σ2 ef). rewrite bi.affinely_and_r bi.affinely_and.
iIntros "[% HP]". inv_head_step.
set (l := fresh (dom (gset positive) σ)).
rewrite /ownP. iPsvs ("HΦ" with "HP").
rewrite ?right_id.
match goal with H: _ = of_val v2 |- _ => apply (inj of_val (LitV _)) in H end.
iPvsIntro. by subst v2.
iModIntro; by subst v2.
Qed.
Lemma wp_load_pst E σ l v Φ :
......@@ -144,7 +148,7 @@ Lemma wp_un_op E op l l' Φ :
Proof.
intros. rewrite -(wp_lift_pure_det_head_step (UnOp op _) (Lit l') None)
?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
iIntros "HP". iNext. iPsvs "HP". by do 2 iPvsIntro.
iIntros "HP". iNext. iPsvs "HP". by do 2 iModIntro.
Qed.
Lemma wp_bin_op E op l1 l2 l' Φ :
......@@ -153,7 +157,7 @@ Lemma wp_bin_op E op l1 l2 l' Φ :
Proof.
intros Heval. rewrite -(wp_lift_pure_det_head_step (BinOp op _ _) (Lit l') None)
?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
iIntros "HP". iNext. iPsvs "HP". by do 2 iPvsIntro.
iIntros "HP". iNext. iPsvs "HP". by do 2 iModIntro.
Qed.
Lemma wp_if_true E e1 e2 Φ :
......@@ -176,7 +180,7 @@ Lemma wp_fst E e1 v1 e2 Φ :
Proof.
intros ? [v2 ?]. rewrite -(wp_lift_pure_det_head_step (Fst _) e1 None)
?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
iIntros "HP". iNext. iPsvs "HP". by do 2 iPvsIntro.
iIntros "HP". iNext. iPsvs "HP". by do 2 iModIntro.
Qed.
Lemma wp_snd E e1 e2 v2 Φ :
......@@ -185,7 +189,7 @@ Lemma wp_snd E e1 e2 v2 Φ :
Proof.
intros [v1 ?] ?. rewrite -(wp_lift_pure_det_head_step (Snd _) e2 None)
?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
iIntros "HP". iNext. iPsvs "HP". by do 2 iPvsIntro.
iIntros "HP". iNext. iPsvs "HP". by do 2 iModIntro.
Qed.
Lemma wp_letp E x y e1 e2 eb Φ :
......
From fri.heap_lang Require Export lifting.
From fri.heap_lang Require Import lang tactics.
From fri.algebra Require Import upred_big_op frac dec_agree.
From fri.algebra Require Import base_logic frac dec_agree.
From fri.program_logic Require Export invariants ghost_ownership refine_ectx_delay
refine_raw_adequacy nat_delayed_language.
From fri.program_logic Require Import ownership auth refine_raw ectx_lifting.
From fri.proofmode Require Import weakestpre.
From iris.proofmode Require Import tactics.
Import uPred.
Hint Resolve head_prim_reducible head_reducible_prim_step.
......
From fri.heap_lang Require Export refine heap lifting notation wp_tactics.
From fri.algebra Require Import upred_big_op frac dec_agree.
From fri.algebra Require Import base_logic frac dec_agree.
From fri.program_logic Require Export invariants ghost_ownership.
From fri.program_logic Require Import ownership auth.
From fri.proofmode Require Import weakestpre invariants.
From iris.proofmode Require Import tactics.
Import uPred.
Definition sheapN : namespace := nroot .@ "sheap".
......@@ -40,16 +40,16 @@ Section definitions.
Global Instance sheap_inv_proper : Proper (() ==> (⊣⊢)) sheap_inv.
Proof. solve_proper. Qed.
Global Instance sheap_ctx_relevant : RelevantP sheap_ctx.
Global Instance sheap_ctx_relevant : Persistent sheap_ctx.
Proof. apply _. Qed.
Global Instance sheap_ctx_affine : AffineP sheap_ctx.
Global Instance sheap_ctx_affine : Affine sheap_ctx.