Commit 5cb904ba authored by Amin Timany's avatar Amin Timany

Update to work with last iris master

parent 799cda60
......@@ -61,7 +61,7 @@ Section typed_interp.
destruct (lookup_lt_is_Some_2 vs x) as [v Hv].
{ by rewrite -Hlen; apply lookup_lt_Some with τ. }
rewrite /env_subst Hv; value_case.
iApply big_and_elem_of "HΓ"; eauto.
iApply (big_and_elem_of with "HΓ").
apply elem_of_list_lookup_2 with x.
rewrite lookup_zip_with; simplify_option_eq; trivial.
- (* unit *) value_case.
......@@ -108,7 +108,7 @@ Section typed_interp.
- (* TLam *)
value_case; iApply exist_intro; iSplit; trivial.
iIntros {τi}; destruct τi as [τi τiPr].
iPoseProof always_intro "HΓ" as "HP"; try typeclasses eauto; try iExact "HP".
iPoseProof (always_intro with "HΓ") as "HP"; try typeclasses eauto; try iExact "HP".
iIntros "#HΓ"; iNext.
iApply IHHtyped; [rewrite map_length|]; trivial.
iRevert "HΓ".
......@@ -118,7 +118,7 @@ Section typed_interp.
smart_wp_bind TAppCtx v "#Hv" IHHtyped; cbn.
iDestruct "Hv" as {e'} "[% He']"; rewrite H.
iApply wp_TLam.
iSpecialize "He'" {((interp τ' Δ) _)}; cbn.
iSpecialize ("He'" $! ((interp τ' Δ) _)); cbn.
iApply always_elim. iApply always_mono; [|trivial].
iIntros "He'"; iNext.
iApply wp_mono; [|trivial].
......
......@@ -6,6 +6,7 @@ From iris.program_logic Require Export lifting.
From iris.algebra Require Import upred_big_op frac dec_agree.
From iris.program_logic Require Export invariants ghost_ownership.
From iris.program_logic Require Import ownership auth.
Require Import iris.proofmode.tactics iris.proofmode.invariants.
Import uPred.
Section typed_interp.
......@@ -72,7 +73,7 @@ Section typed_interp.
destruct (lookup_lt_is_Some_2 vs x) as [v Hv].
{ by rewrite -Hlen; apply lookup_lt_Some with τ. }
rewrite /env_subst Hv; value_case.
iApply big_and_elem_of "HΓ"; eauto.
iApply (big_and_elem_of with "HΓ").
apply elem_of_list_lookup_2 with x.
rewrite lookup_zip_with; simplify_option_eq; trivial.
- (* unit *) value_case; trivial.
......@@ -120,7 +121,7 @@ Section typed_interp.
value_case; iApply exist_intro; iSplit; trivial.
iIntros {τi}; destruct τi as [τi τiPr].
iRevert "Hheap".
iPoseProof always_intro "HΓ" as "HP"; try typeclasses eauto;
iPoseProof (always_intro with "HΓ") as "HP"; try typeclasses eauto;
try (iApply always_impl; iExact "HP").
iIntros "#HΓ #Hheap"; iNext.
iApply IHHtyped; [rewrite map_length|]; trivial.
......@@ -131,7 +132,7 @@ Section typed_interp.
smart_wp_bind TAppCtx v "#Hv" IHHtyped; cbn.
iDestruct "Hv" as {e'} "[% He']"; rewrite H.
iApply wp_TLam.
iSpecialize "He'" {((interp τ' Δ) _)}; cbn.
iSpecialize ("He'" $! ((interp τ' Δ) _)); cbn.
iApply always_elim. iApply always_mono; [|trivial].
iIntros "He'"; iNext.
iApply wp_mono; [|trivial].
......@@ -166,60 +167,42 @@ Section typed_interp.
- (* Alloc *)
smart_wp_bind AllocCtx v "#Hv" IHHtyped; cbn. iClear "HΓ".
iApply wp_atomic; cbn; trivial; [rewrite to_of_val; auto|].
iApply pvs_intro.
iApply wp_alloc; [| | | |iSplit;[iExact "Hheap"|iExact "Hv"]];
[|iIntros "#[Hheap Hv]"| |]; auto using to_of_val.
iIntros "#[Hheap Hv]". iNext.
iPvsIntro.
iApply wp_alloc; auto 1 using to_of_val.
iFrame "Hheap". iNext.
iIntros {l} "Hl".
iApply exist_intro.
iApply and_intro; [| trivial |]; auto.
iApply inv_alloc; trivial. iNext.
iApply exist_intro.
iSplit; trivial.
iPvs (inv_alloc _ with "[Hl]") as "HN";
[| | iPvsIntro; iExists _; iSplit; trivial].
trivial.
iNext; iExists _; iFrame "Hl"; trivial.
- (* Load *)
smart_wp_bind LoadCtx v "#Hv" IHHtyped; cbn. iClear "HΓ".
iRevert "Hheap". iApply exist_elim; [|iExact "Hv"].
iIntros {l} "[% #Hv] #Hheap"; rewrite H.
iApply wp_atomic; cbn; eauto using to_of_val.
iApply wp_inv; [auto using to_of_val| trivial
| apply and_elim_r | apply and_elim_l | ].
iApply pvs_intro. iSplit; trivial.
iIntros "Hl".
iPoseProof later_exist_turnstile "Hl" as "Hl'"; [typeclasses eauto|].
iRevert "Hheap".
iApply exist_elim; [|iExact "Hl'"].
iIntros {w} "[Hl1 #Hl2] #Hheap".
iApply (wp_load _ _ _ 1);
[apply and_elim_r| trivial | apply and_elim_l | iSplit; trivial].
iPvsIntro.
iInv (L .@ l) as {w} "[Hw1 #Hw2]".
iApply (wp_load _ _ _ 1); [|iFrame "Hheap"]; trivial.
specialize (HNLdisj l); set_solver_ndisj.
iNext.
iSplitL; trivial.
iIntros "Hl".
iSplitL.
+ iNext. iApply exist_intro; iSplitL; trivial.
+ iApply pvs_intro; trivial.
iFrame "Hw1". iNext.
iIntros "Hw1". iSplitL; trivial.
iNext; iExists _. iFrame "Hw1"; trivial.
- (* Store *)
smart_wp_bind (StoreLCtx _) v "#Hv" IHHtyped1; cbn.
smart_wp_bind (StoreRCtx _) w "#Hw" IHHtyped2; cbn. iClear "HΓ".
iRevert "Hheap Hw". iApply exist_elim; [|iExact "Hv"].
iIntros {l} "#[% Hl] #Hheap #Hw"; rewrite H.
iApply wp_atomic; cbn; [trivial| rewrite ?to_of_val; auto |].
iApply wp_inv; [cbn; rewrite ?to_of_val; auto| trivial
| apply and_elim_r | apply and_elim_l | ].
iApply pvs_intro. iSplit; trivial.
iClear "Hl". iIntros "Hl".
iPoseProof later_exist_turnstile "Hl" as "Hl'"; [typeclasses eauto|].
iRevert "Hheap Hw".
iApply exist_elim; [|iExact "Hl'"].
iIntros {u} "[Hl1 #Hl2] #Hheap #Hw".
iApply wp_store;
[rewrite to_of_val; trivial | apply and_elim_r
| | apply and_elim_l | iSplit; trivial].
iPvsIntro.
iInv (L .@ l) as {z} "[Hz1 #Hz2]".
eapply bool_decide_spec; eauto using to_of_val.
iApply (wp_store N); auto using to_of_val.
specialize (HNLdisj l); set_solver_ndisj.
iSplitL; trivial.
iNext. iIntros "Hl".
iSplitL; [|iApply pvs_intro; trivial].
iNext. iApply exist_intro; iSplitL; trivial.
iFrame "Hheap Hz1".
iNext.
iIntros "Hz1".
iSplitL; [|iPvsIntro; trivial].
iNext; iExists _. iFrame "Hz1"; trivial.
(* unshelving *)
Unshelve.
cbn; typeclasses eauto.
......
......@@ -7,7 +7,7 @@ Module lang.
Definition loc := positive.
Global Instance loc_dec_eq (l l' : loc) : Decision (l = l') := _.
Inductive expr :=
| Var (x : var)
| Lam (e : {bind 1 of expr})
......@@ -45,7 +45,7 @@ Module lang.
unfold Decision.
decide equality; [apply eq_nat_dec | apply loc_dec_eq].
Defined.
Inductive val :=
| LamV (e : {bind 1 of expr})
| TLamV (e : {bind 1 of expr})
......@@ -75,7 +75,7 @@ Module lang.
| FoldV v => Fold (of_val v)
| LocV l => Loc l
end.
Fixpoint to_val (e : expr) : option val :=
match e with
| Lam e => Some (LamV e)
......@@ -88,7 +88,7 @@ Module lang.
| Loc l => Some (LocV l)
| _ => None
end.
(** Evaluation contexts *)
Inductive ectx_item :=
| AppLCtx (e2 : expr)
......@@ -129,9 +129,9 @@ Module lang.
| StoreLCtx e2 => Store e e2
| StoreRCtx v1 => Store (of_val v1) e
end.
Definition fill (K : ectx) (e : expr) : expr := fold_right fill_item e K.
Definition state : Type := gmap loc val.
Inductive head_step : expr -> state -> expr -> state -> option expr -> Prop :=
......@@ -174,12 +174,9 @@ Module lang.
(** Atomic expressions: we don't consider any atomic operations. *)
Definition atomic (e: expr) :=
match e with
| Alloc e => match (to_val e) with | Some _ => true | None => false end
| Load e => match (to_val e) with | Some _ => true | None => false end
| Store e1 e2 =>
andb
match (to_val e1) with | Some _ => true | None => false end
match (to_val e2) with | Some _ => true | None => false end
| Alloc e => bool_decide (is_Some (to_val e))
| Load e => bool_decide (is_Some (to_val e))
| Store e1 e2 => bool_decide (is_Some (to_val e1) is_Some (to_val e2))
| _ => false
end.
......
......@@ -4,7 +4,9 @@ Require Import F_mu_ref.lang.
From iris.program_logic Require Export lifting.
From iris.algebra Require Import upred_big_op frac dec_agree.
From iris.program_logic Require Export invariants ghost_ownership.
From iris.proofmode Require Import weakestpre.
From iris.program_logic Require Import ownership auth.
Require Import iris.proofmode.tactics iris.proofmode.invariants.
Import uPred.
Section lang_rules.
......@@ -54,11 +56,12 @@ Section lang_rules.
Lemma wp_bind {E e} K Φ :
WP e @ E {{ (λ v, WP (fill K (of_val v)) @ E {{Φ}}) }} WP (fill K e) @ E {{Φ}}.
WP e @ E {{ (λ v, WP (fill K (of_val v)) @ E {{Φ}}) }}
WP (fill K e) @ E {{Φ}}.
Proof. apply weakestpre.wp_bind. Qed.
Lemma wp_bindi {E e} Ki Φ :
WP e @ E {{ (λ v, WP (fill_item Ki (of_val v)) @ E {{Φ}}) }} WP (fill_item Ki e) @ E {{Φ}}.
WP e @ E {{ (λ v, WP (fill_item Ki (of_val v)) @ E {{Φ}}) }}
WP (fill_item Ki e) @ E {{Φ}}.
Proof. apply weakestpre.wp_bind. Qed.
Ltac inv_step :=
......@@ -126,7 +129,7 @@ Section lang_rules.
end.
Local Hint Extern 0 => do_step ltac:(eauto 2).
(** Conversion to heaps and back *)
Global Instance of_heap_proper : Proper (() ==> (=)) of_heap.
Proof. solve_proper. Qed.
......@@ -250,75 +253,66 @@ Section lang_rules.
Proof.
intros. rewrite -(wp_lift_atomic_det_step σ (UnitV) (<[l:=v]>σ) None)
?right_id //; cbn; eauto.
rewrite H; auto.
by intros; inv_step; eauto.
Qed.
(** Weakest precondition *)
Lemma wp_alloc N E e v P Φ :
to_val e = Some v
P heap_ctx N nclose N E
P ( l, l v - Φ (LocV l))
P WP Alloc e @ E {{ Φ }}.
Lemma wp_alloc N E e v Φ :
to_val e = Some v nclose N E
(heap_ctx N l, l v - Φ (LocV l)) WP Alloc e @ E {{ Φ }}.
Proof.
rewrite /heap_ctx /heap_inv=> H ?? HP.
trans (|={E}=> auth_own heap_name P)%I.
{ by rewrite -pvs_frame_r -(auth_empty _ E) left_id. }
apply wp_strip_pvs, (auth_fsa heap_inv (wp_fsa (Alloc e)))
with N heap_name ; simpl; eauto with I; [rewrite H; auto|].
rewrite -later_intro. apply sep_mono_r,forall_intro=> h; apply wand_intro_l.
rewrite -assoc left_id; apply const_elim_sep_l=> ?.
rewrite -(wp_alloc_pst _ (of_heap h)) //.
apply sep_mono_r; rewrite HP; apply later_mono.
apply forall_mono=> l; apply wand_intro_l.
rewrite always_and_sep_l -assoc; apply const_elim_sep_l=> ?.
rewrite -(exist_intro (op {[ l := Frac 1 (DecAgree v) ]})).
repeat erewrite <-exist_intro by apply _; simpl.
rewrite -of_heap_insert left_id right_id.
rewrite /heap_mapsto. ecancel [_ - Φ _]%I.
rewrite -(insert_singleton_op h); last by apply of_heap_None.
rewrite const_equiv; last by apply (insert_valid h).
by rewrite left_id -later_intro.
iIntros {??} "[#Hinv HΦ]". rewrite /heap_ctx.
iPvs (auth_empty heap_name) as "Hheap".
iApply (auth_fsa heap_inv (wp_fsa (Alloc e)) _ N); simpl; eauto.
iFrame "Hinv Hheap". iIntros {h}. rewrite [ h]left_id.
iIntros "[% Hheap]". rewrite /heap_inv.
iApply wp_alloc_pst; first done. iFrame "Hheap". iNext.
iIntros {l} "[% Hheap]".
iExists (op {[ l := Frac 1 (DecAgree v) ]}), _, _.
rewrite [{[ _ := _ ]} ]right_id.
rewrite -of_heap_insert -(insert_singleton_op h);
last by apply of_heap_None.
iFrame "Hheap". iSplit.
{ iPureIntro; split; first done. by apply (insert_valid h). }
iIntros "Hheap". iApply "HΦ". by rewrite /heap_mapsto.
Qed.
Lemma wp_load N E l q v P Φ :
P heap_ctx N nclose N E
P ( l {q} v (l {q} v - Φ v))
P WP Load (Loc l) @ E {{ Φ }}.
Lemma wp_load N E l q v Φ :
nclose N E
(heap_ctx N l {q} v (l {q} v - Φ v))
WP Load (Loc l) @ E {{ Φ }}.
Proof.
rewrite /heap_ctx /heap_inv=> ?? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) id)
with N heap_name {[ l := Frac q (DecAgree v) ]}; simpl; eauto with I.
rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
rewrite -assoc; apply const_elim_sep_l=> ?.
rewrite -(wp_load_pst _ (<[l:=v]>(of_heap h))) ?lookup_insert //.
rewrite const_equiv // left_id.
rewrite /heap_inv of_heap_singleton_op //.
apply sep_mono_r, later_mono, wand_intro_l. by rewrite -later_intro.
iIntros {?} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
iApply (auth_fsa' heap_inv (wp_fsa _) id _ N _
heap_name {[ l := Frac q (DecAgree v) ]}); simpl; eauto.
iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));
first by rewrite lookup_insert.
rewrite of_heap_singleton_op //. iFrame "Hl". iNext.
iIntros "$". by iSplit.
Qed.
Lemma wp_store N E l v' e v P Φ :
to_val e = Some v
P heap_ctx N nclose N E
P ( l v' (l v - Φ UnitV))
P WP Store (Loc l) e @ E {{ Φ }}.
Lemma wp_store N E l v' e v Φ :
to_val e = Some v nclose N E
(heap_ctx N l v' (l v - Φ UnitV))
WP Store (Loc l) e @ E {{ Φ }}.
Proof.
rewrite /heap_ctx /heap_inv=> H ?? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v)) l))
with N heap_name {[ l := Frac 1 (DecAgree v') ]}; simpl; eauto with I;
[rewrite H; auto|].
rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
rewrite -assoc; apply const_elim_sep_l=> ?.
rewrite -(wp_store_pst _ (<[l:=v']>(of_heap h))) ?lookup_insert //.
rewrite /heap_inv alter_singleton insert_insert !of_heap_singleton_op; eauto.
rewrite const_equiv; last naive_solver.
apply sep_mono_r, later_mono, wand_intro_l. by rewrite left_id -later_intro.
iIntros {??} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
iApply (auth_fsa' heap_inv (wp_fsa _)
(alter (λ _, Frac 1 (DecAgree v)) l) _
N _ heap_name {[ l := Frac 1 (DecAgree v') ]});
simpl; eauto.
iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
iApply (wp_store_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
rewrite alter_singleton insert_insert !of_heap_singleton_op; eauto.
iFrame "Hl". iNext. iIntros "$". iFrame "HΦ". iPureIntro; naive_solver.
Qed.
(** Helper Lemmas for weakestpre. *)
Lemma wp_lam E e1 e2 v Φ :
to_val e2 = Some v WP e1.[e2 /] @ E {{Φ}} WP (App (Lam e1) e2) @ E {{Φ}}.
to_val e2 = Some v
WP e1.[e2 /] @ E {{Φ}} WP (App (Lam e1) e2) @ E {{Φ}}.
Proof.
intros <-%of_to_val.
rewrite -(wp_lift_pure_det_step (App _ _) e1.[of_val v /] None) //=.
......@@ -343,7 +337,7 @@ Section lang_rules.
- rewrite right_id; auto using uPred.later_mono, wp_value'.
- intros. inv_step; auto.
Qed.
Lemma wp_fst E e1 v1 e2 v2 Φ :
to_val e1 = Some v1 to_val e2 = Some v2
Φ v1 WP (Fst (Pair e1 e2)) @ E {{Φ}}.
......@@ -369,17 +363,19 @@ Section lang_rules.
WP e1.[e0/] @ E {{Φ}} WP (Case (InjL e0) e1 e2) @ E {{Φ}}.
Proof.
intros <-%of_to_val.
rewrite -(wp_lift_pure_det_step (Case (InjL _) _ _) (e1.[of_val v0/]) None) //=.
rewrite -(wp_lift_pure_det_step
(Case (InjL _) _ _) (e1.[of_val v0/]) None) //=.
- rewrite right_id; auto using uPred.later_mono, wp_value'.
- intros. inv_step; auto.
Qed.
Qed.
Lemma wp_case_inr E e0 v0 e1 e2 Φ :
to_val e0 = Some v0
WP e2.[e0/] @ E {{Φ}} WP (Case (InjR e0) e1 e2) @ E {{Φ}}.
Proof.
intros <-%of_to_val.
rewrite -(wp_lift_pure_det_step (Case (InjR _) _ _) (e2.[of_val v0/]) None) //=.
rewrite -(wp_lift_pure_det_step
(Case (InjR _) _ _) (e2.[of_val v0/]) None) //=.
- rewrite right_id; auto using uPred.later_mono, wp_value'.
- intros. inv_step; auto.
Qed.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment