Commit 42b71ff1 authored by Robbert Krebbers's avatar Robbert Krebbers

Use concrete invariant names.

parent ba2fcff2
......@@ -4,7 +4,7 @@ From iris_logrel.F_mu_ref Require Import rules.
From iris.algebra Require Export upred_big_op.
Section typed_interp.
Context `{heapG Σ} (L : namespace).
Context `{heapG Σ}.
Notation D := (valC -n> iPropG lang Σ).
Implicit Types Δ : listC D.
......@@ -15,11 +15,11 @@ Section typed_interp.
Local Ltac value_case := iApply wp_value; [cbn; rewrite ?to_of_val; trivial|].
Lemma typed_interp N Δ Γ vs e τ (HΔ : ctx_PersistentP Δ) (HNLdisj : N L) :
Lemma typed_interp Δ Γ vs e τ (HΔ : ctx_PersistentP Δ) :
Γ ⊢ₜ e : τ
length Γ = length vs
heap_ctx N [] zip_with (λ τ, interp L τ Δ) Γ vs
WP e.[env_subst vs] {{ interp L τ Δ }}.
heap_ctx [] zip_with (λ τ, interp τ Δ) Γ vs
WP e.[env_subst vs] {{ interp τ Δ }}.
Proof.
intros Htyped; revert Δ HΔ vs.
induction Htyped; iIntros {Δ HΔ vs Hlen} "#[Hheap HΓ] /=".
......@@ -76,13 +76,13 @@ Section typed_interp.
rewrite zip_with_fmap_l. by iApply context_interp_ren_S.
- (* TApp *)
smart_wp_bind TAppCtx v "#Hv" IHHtyped; cbn.
iApply wp_wand_r; iSplitL; [iApply ("Hv" $! (interp L τ' Δ)); iPureIntro; apply _|].
iApply wp_wand_r; iSplitL; [iApply ("Hv" $! (interp τ' Δ)); iPureIntro; apply _|].
iIntros {w} "?". by rewrite interp_subst.
- (* Fold *)
rewrite map_length in IHHtyped.
iApply (@wp_bind _ _ _ [FoldCtx]).
iApply wp_wand_l.
iSplitL; [|iApply (IHHtyped (interp L (TRec τ) Δ :: Δ)); trivial].
iSplitL; [|iApply (IHHtyped (interp (TRec τ) Δ :: Δ)); trivial].
+ iIntros {v} "#Hv". value_case.
rewrite fixpoint_unfold /=. iAlways; eauto 10.
+ iFrame "Hheap". rewrite zip_with_fmap_l. by iApply context_interp_ren_S.
......@@ -90,7 +90,7 @@ Section typed_interp.
iApply (@wp_bind _ _ _ [UnfoldCtx]);
iApply wp_wand_l; iSplitL; [|iApply IHHtyped; auto].
iIntros {v} "#Hv". rewrite /= fixpoint_unfold.
change (fixpoint _) with (interp L (TRec τ) Δ); simpl.
change (fixpoint _) with (interp (TRec τ) Δ); simpl.
iDestruct "Hv" as {w} "#[% Hw]"; subst.
iApply wp_Fold; cbn; auto using to_of_val.
iNext; iPvsIntro. by rewrite -interp_subst.
......@@ -107,8 +107,8 @@ Section typed_interp.
iDestruct "Hv" as {l} "[% #Hv]"; subst.
iApply wp_atomic; cbn; eauto using to_of_val.
iPvsIntro.
iInv (L .@ l) as {w} "[Hw1 #Hw2]".
iApply (wp_load _ _ _ 1); [|iFrame "Hheap"]; trivial. solve_ndisj.
iInv (logN .@ l) as {w} "[Hw1 #Hw2]".
iApply (wp_load _ _ 1); [|iFrame "Hheap"]; trivial. solve_ndisj.
iIntros "{$Hw1} > Hw1". iPvsIntro. iSplitL; eauto.
- (* Store *)
smart_wp_bind (StoreLCtx _) v "#Hv" IHHtyped1; cbn.
......@@ -116,9 +116,9 @@ Section typed_interp.
iDestruct "Hv" as {l} "[% #Hv]"; subst.
iApply wp_atomic; cbn; [trivial| rewrite ?to_of_val; auto |].
iPvsIntro.
iInv (L .@ l) as {z} "[Hz1 #Hz2]".
iInv (logN .@ l) as {z} "[Hz1 #Hz2]".
eapply bool_decide_spec; eauto using to_of_val.
iApply (wp_store N); auto using to_of_val. solve_ndisj.
iApply wp_store; auto using to_of_val. solve_ndisj.
iIntros "{$Hheap $Hz1} > Hz1". iPvsIntro.
iSplitL; eauto 10.
Qed.
......
From iris.prelude Require Import strings.
From iris.program_logic Require Export weakestpre.
From iris_logrel.F_mu_ref Require Export rules typing.
Import uPred.
Definition logN : namespace := nroot .@ "logN".
(** interp : is a unary logical relation. *)
Section logrel.
Context `{heapG Σ} (L : namespace).
Context `{heapG Σ}.
Notation D := (valC -n> iPropG lang Σ).
Implicit Types τi : D.
Implicit Types Δ : listC D.
......@@ -61,7 +64,7 @@ Section logrel.
Program Definition interp_ref
(interp : listC D -n> D) : listC D -n> D := λne Δ w,
( l, w = LocV l inv (L .@ l) (interp_ref_inv l (interp Δ)))%I.
( l, w = LocV l inv (logN .@ l) (interp_ref_inv l (interp Δ)))%I.
Solve Obligations with solve_proper.
Fixpoint interp (τ : type) : listC D -n> D :=
......
......@@ -6,6 +6,7 @@ From iris_logrel.F_mu_ref Require Export lang.
From iris.proofmode Require Import tactics weakestpre invariants.
Import uPred.
Definition heapN : namespace := nroot .@ "heap".
Definition heapUR : ucmraT := gmapUR loc (prodR fracR (dec_agreeR val)).
(** The CMRA we need. *)
......@@ -24,12 +25,11 @@ Section definitions.
auth_own heap_name {[ l := (q, DecAgree v) ]}.
Definition heap_inv (h : heapUR) : iPropG lang Σ :=
ownP (of_heap h).
Definition heap_ctx (N : namespace) : iPropG lang Σ :=
auth_ctx heap_name N heap_inv.
Definition heap_ctx : iPropG lang Σ := auth_ctx heap_name heapN heap_inv.
Global Instance heap_inv_proper : Proper (() ==> ()) heap_inv.
Proof. solve_proper. Qed.
Global Instance heap_ctx_always_stable N : PersistentP (heap_ctx N).
Global Instance heap_ctx_always_stable : PersistentP heap_ctx.
Proof. apply _. Qed.
End definitions.
Typeclasses Opaque heap_ctx heap_mapsto.
......@@ -40,7 +40,6 @@ Notation "l ↦ v" := (heap_mapsto l 1 v) (at level 20) : uPred_scope.
Section lang_rules.
Context {Σ : gFunctors}.
Implicit Types N : namespace.
Implicit Types P Q : iPropG lang Σ.
Implicit Types Φ : val iPropG lang Σ.
Implicit Types σ : state.
......@@ -159,13 +158,13 @@ Section lang_rules.
Proof. unfold of_heap; apply map_eq => i; rewrite !lookup_omap; f_equal. Qed.
(** Allocation *)
Lemma heap_alloc N E σ :
authG lang Σ heapUR nclose N E
ownP σ ={E}=> _ : heapG Σ, heap_ctx N [ map] l v σ, l v.
Lemma heap_alloc E σ :
authG lang Σ heapUR nclose heapN E
ownP σ ={E}=> _ : heapG Σ, heap_ctx [ map] l v σ, l v.
Proof.
intros. rewrite -{1}(from_to_heap σ). etrans.
{ rewrite [ownP _]later_intro.
apply (auth_alloc (ownP of_heap) N E (to_heap σ)); last done.
apply (auth_alloc (ownP of_heap) heapN E (to_heap σ)); last done.
apply to_heap_valid. }
apply pvs_mono, exist_elim=> γ.
rewrite -(exist_intro (HeapG _ _ γ)) /heap_ctx; apply and_mono_r.
......@@ -179,7 +178,7 @@ Section lang_rules.
by rewrite auth_own_op IH.
Qed.
Context `{HGΣ : heapG Σ}.
Context `{heapG Σ}.
(** General properties of mapsto *)
Lemma heap_mapsto_op_eq l q1 q2 v : l {q1} v l {q2} v ⊣⊢ l {q1+q2} v.
......@@ -217,7 +216,7 @@ Section lang_rules.
cbn; rewrite to_of_val.
apply pure_elim_l=>-[l [-> [-Heq [-> ?]]]]; inversion Heq; subst.
by rewrite (forall_elim l) right_id pure_equiv // left_id wand_elim_r.
cbn; rewrite H; eauto.
cbn; rewrite H0; eauto.
Qed.
Lemma wp_load_pst E σ l v Φ :
......@@ -238,9 +237,9 @@ Section lang_rules.
by intros; inv_step; eauto.
Qed.
Lemma wp_alloc N E e v Φ :
to_val e = Some v nclose N E
heap_ctx N ( l, l v ={E}= Φ (LocV l)) WP Alloc e @ E {{ Φ }}.
Lemma wp_alloc E e v Φ :
to_val e = Some v nclose heapN E
heap_ctx ( l, l v ={E}= Φ (LocV l)) WP Alloc e @ E {{ Φ }}.
Proof.
iIntros {??} "[#Hinv HΦ]". rewrite /heap_ctx.
iPvs (auth_empty heap_name) as "Hheap".
......@@ -255,9 +254,9 @@ Section lang_rules.
iIntros "Hheap". iApply "HΦ". by rewrite /heap_mapsto.
Qed.
Lemma wp_load N E l q v Φ :
nclose N E
heap_ctx N l {q} v (l {q} v ={E}= Φ v)
Lemma wp_load E l q v Φ :
nclose heapN E
heap_ctx l {q} v (l {q} v ={E}= Φ v)
WP Load (Loc l) @ E {{ Φ }}.
Proof.
iIntros {?} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
......@@ -269,9 +268,9 @@ Section lang_rules.
rewrite of_heap_singleton_op //. by iFrame.
Qed.
Lemma wp_store N E l v' e v Φ :
to_val e = Some v nclose N E
heap_ctx N l v' (l v ={E}= Φ UnitV)
Lemma wp_store E l v' e v Φ :
to_val e = Some v nclose heapN E
heap_ctx l v' (l v ={E}= Φ UnitV)
WP Store (Loc l) e @ E {{ Φ }}.
Proof.
iIntros {??} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
......
......@@ -7,16 +7,13 @@ Section soundness.
Lemma wp_soundness e τ σ :
[] ⊢ₜ e : τ
ownP σ WP e {{ v, H : heapG Σ, interp (nroot .@ 1) τ [] v}}.
ownP σ WP e {{ v, H : heapG Σ, interp τ [] v}}.
Proof.
iIntros {H1} "Hemp".
iPvs (heap_alloc (nroot .@ 2) with "Hemp")
as {H} "[Hheap Hemp]"; first solve_ndisj.
iPvs (heap_alloc with "Hemp") as {H} "[Hheap Hemp]"; first solve_ndisj.
iApply wp_wand_l. iSplitR.
{ iIntros {v} "HΦ". iExists H. iExact "HΦ". }
rewrite -(empty_env_subst e).
iApply (@typed_interp _ _ (nroot .@ 1) (nroot .@ 2)); eauto.
solve_ndisj.
rewrite -(empty_env_subst e). iApply typed_interp; eauto.
Qed.
Theorem soundness e τ e' thp σ σ' :
......
......@@ -191,7 +191,7 @@ Definition ctx_refines (Γ : list type)
thp' σ' v', rtc step ([fill_ctx K e'], ) (# v' :: thp', σ').
Section bin_log_related_under_typed_ctx.
Context `{heapIG Σ, cfgSG Σ} {N : namespace}.
Context `{heapIG Σ, cfgSG Σ}.
Notation D := (prodC valC valC -n> iPropG lang Σ).
Implicit Types Δ : listC D.
......@@ -199,9 +199,9 @@ Section bin_log_related_under_typed_ctx.
( f, e.[base.iter (length Γ) up f] = e)
( f, e'.[base.iter (length Γ) up f] = e')
typed_ctx K Γ τ Γ' τ'
( Δ (HΔ : ctx_PersistentP Δ), @bin_log_related _ _ _ N Δ Γ e e' τ)
( Δ (HΔ : ctx_PersistentP Δ), @bin_log_related _ _ _ Δ Γ e e' τ)
Δ (HΔ : ctx_PersistentP Δ),
@bin_log_related _ _ _ N Δ Γ' (fill_ctx K e) (fill_ctx K e') τ'.
@bin_log_related _ _ _ Δ Γ' (fill_ctx K e) (fill_ctx K e') τ'.
Proof.
revert Γ τ Γ' τ' e e'.
induction K as [|k K]=> Γ τ Γ' τ' e e' H1 H2; simpl.
......
......@@ -35,7 +35,7 @@ Definition FG_counter : expr :=
App (Lam (FG_counter_body (Var 1))) (Alloc ( 0)).
Section CG_Counter.
Context `{iS : cfgSG Σ, heapIG Σ}.
Context `{cfgSG Σ, heapIG Σ}.
Notation D := (prodC valC valC -n> iPropG lang Σ).
Implicit Types Δ : listC D.
......@@ -57,25 +57,24 @@ Section CG_Counter.
(CG_increment x).[f] = CG_increment x.[f].
Proof. unfold CG_increment; asimpl; trivial. Qed.
Lemma steps_CG_increment N E ρ j K x n:
nclose N E
Spec_ctx N ρ x ↦ₛ (v n) j fill K (App (CG_increment (Loc x)) Unit)
Lemma steps_CG_increment E ρ j K x n:
nclose specN E
spec_ctx ρ x ↦ₛ (v n) j fill K (App (CG_increment (Loc x)) Unit)
={E}=> j fill K (Unit) x ↦ₛ (v (S n)).
Proof.
iIntros {HNE} "[#Hspec [Hx Hj]]". unfold CG_increment.
iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
iPvs (step_load _ _ _ j (K ++ [StoreRCtx (LocV _); BinOpRCtx _ (v _)])
iPvs (step_lam _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
iPvs (step_load _ _ j (K ++ [StoreRCtx (LocV _); BinOpRCtx _ (v _)])
_ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto.
rewrite ?fill_app. simpl.
iFrame "Hspec Hj"; trivial.
rewrite ?fill_app. simpl.
iPvs (step_nat_bin_op _ _ _ j (K ++ [StoreRCtx (LocV _)])
iPvs (step_nat_bin_op _ _ j (K ++ [StoreRCtx (LocV _)])
_ _ _ with "[Hj]") as "Hj"; eauto.
rewrite ?fill_app. simpl.
iFrame "Hspec Hj"; trivial. simpl.
rewrite ?fill_app. simpl.
iPvs (step_store _ _ _ j K _ _ _ _ _
with "[Hj Hx]") as "[Hj Hx]"; eauto.
iPvs (step_store _ _ j K _ _ _ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto.
iFrame "Hspec Hj"; trivial.
iPvsIntro.
iFrame "Hj Hx"; trivial.
......@@ -118,15 +117,15 @@ Section CG_Counter.
rewrite with_lock_subst CG_increment_subst. asimpl; trivial.
Qed.
Lemma steps_CG_locked_increment N E ρ j K x n l :
nclose N E
Spec_ctx N ρ x ↦ₛ (v n) l ↦ₛ (v false)
Lemma steps_CG_locked_increment E ρ j K x n l :
nclose specN E
spec_ctx ρ x ↦ₛ (v n) l ↦ₛ (v false)
j fill K (App (CG_locked_increment (Loc x) (Loc l)) Unit)
={E}=> j fill K Unit x ↦ₛ (v S n) l ↦ₛ (v false).
Proof.
iIntros {HNE} "[#Hspec [Hx [Hl Hj]]]".
iPvs (steps_with_lock
_ _ _ j K _ _ _ _ UnitV UnitV _ _ with "[Hj Hx Hl]") as "Hj"; last done.
_ _ j K _ _ _ _ UnitV UnitV _ _ with "[Hj Hx Hl]") as "Hj"; last done.
- iIntros {K'} "[#Hspec [Hx Hj]]".
iApply steps_CG_increment; first done. iFrame "Hspec Hj Hx"; trivial.
- by iFrame "Hspec Hj Hx".
......@@ -158,16 +157,16 @@ Section CG_Counter.
(counter_read x).[f] = counter_read x.[f].
Proof. unfold counter_read. by asimpl. Qed.
Lemma steps_counter_read N E ρ j K x n :
nclose N E
Spec_ctx N ρ x ↦ₛ (v n)
Lemma steps_counter_read E ρ j K x n :
nclose specN E
spec_ctx ρ x ↦ₛ (v n)
j fill K (App (counter_read (Loc x)) Unit)
={E}=> j fill K ( n) x ↦ₛ (v n).
Proof.
intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold counter_read.
iPvs (step_lam _ _ _ j K _ Unit with "[Hj]") as "Hj"; eauto.
iPvs (step_lam _ _ j K _ Unit with "[Hj]") as "Hj"; eauto.
asimpl.
iPvs (step_load _ _ _ j K with "[Hj Hx]") as "[Hj Hx]"; eauto.
iPvs (step_load _ _ j K with "[Hj Hx]") as "[Hj Hx]"; eauto.
{ by iFrame "Hspec Hj". }
iPvsIntro. by iFrame "Hj Hx".
Qed.
......@@ -252,8 +251,10 @@ Section CG_Counter.
Lemma FG_counter_closed f : FG_counter.[f] = FG_counter.
Proof. asimpl; rewrite counter_read_subst; by asimpl. Qed.
Lemma FG_CG_counter_refinement N Δ {HΔ : ctx_PersistentP Δ} :
@bin_log_related _ _ _ N Δ [] FG_counter CG_counter
Definition counterN : namespace := nroot .@ "counter".
Lemma FG_CG_counter_refinement Δ {HΔ : ctx_PersistentP Δ} :
@bin_log_related _ _ _ Δ [] FG_counter CG_counter
(TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
Proof.
(* executing the preambles *)
......@@ -261,18 +262,18 @@ Section CG_Counter.
cbn -[FG_counter CG_counter].
iIntros "(#Hheap & #Hspec & _ & Hj)".
rewrite ?empty_env_subst /CG_counter /FG_counter.
iPvs (steps_newlock _ _ _ j (K ++ [AppRCtx (LamV _)]) _ with "[Hj]")
iPvs (steps_newlock _ _ j (K ++ [AppRCtx (LamV _)]) _ with "[Hj]")
as {l} "[Hj Hl]"; eauto.
{ rewrite fill_app /=. by iFrame. }
rewrite fill_app /=.
iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
iPvs (step_lam _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. rewrite CG_locked_increment_subst /=.
rewrite counter_read_subst /=.
iPvs (step_alloc _ _ _ j (K ++ [AppRCtx (LamV _)]) _ _ _ _ with "[Hj]")
iPvs (step_alloc _ _ j (K ++ [AppRCtx (LamV _)]) _ _ _ _ with "[Hj]")
as {cnt'} "[Hj Hcnt']"; eauto.
{ rewrite fill_app; simpl. by iFrame. }
rewrite fill_app; simpl.
iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
iPvs (step_lam _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. rewrite CG_locked_increment_subst /=.
rewrite counter_read_subst /=.
Unshelve.
......@@ -286,7 +287,7 @@ Section CG_Counter.
iAssert (( n, l ↦ₛ (v false) cnt ↦ᵢ (v n) cnt' ↦ₛ (v n) )%I)
with "[Hl Hcnt Hcnt']" as "Hinv".
{ iExists _. by iFrame. }
iPvs (inv_alloc (N .@ 4) with "[Hinv]") as "#Hinv"; trivial.
iPvs (inv_alloc counterN with "[Hinv]") as "#Hinv"; trivial.
{ iNext; iExact "Hinv". }
(* splitting increment and read *)
iApply wp_lam; trivial. iNext. asimpl.
......@@ -306,7 +307,7 @@ Section CG_Counter.
(* fine-grained reads the counter *)
iApply (@wp_bind _ _ _ [AppRCtx (LamV _)]);
iApply wp_wand_l; iSplitR; [iIntros {v} "Hv"; iExact "Hv"|].
iInv> (N .@4) as {n} "[Hl [Hcnt Hcnt']]".
iInv> counterN as {n} "[Hl [Hcnt Hcnt']]".
iApply wp_load; [|iFrame "Hheap"]. solve_ndisj.
iIntros "> {$Hcnt} Hcnt". iPvsIntro.
iSplitL "Hl Hcnt Hcnt'"; [iExists _; iFrame "Hl Hcnt Hcnt'"; trivial|].
......@@ -318,13 +319,13 @@ Section CG_Counter.
iNext. iPvsIntro.
iApply (@wp_bind _ _ _ [IfCtx _ _]);
iApply wp_wand_l; iSplitR; [iIntros {v} "Hv"; iExact "Hv"|].
iInv> (N .@4) as {n'} "[Hl [Hcnt Hcnt']]".
iInv> counterN as {n'} "[Hl [Hcnt Hcnt']]".
(* performing CAS *)
destruct (decide (n = n')) as [|Hneq]; subst.
+ (* CAS succeeds *)
(* In this case, we perform increment in the coarse-grained one *)
iPvs (steps_CG_locked_increment
_ _ _ _ _ _ _ _ _ with "[Hj Hl Hcnt']") as "[Hj [Hcnt' Hl]]".
_ _ _ _ _ _ _ _ with "[Hj Hl Hcnt']") as "[Hj [Hcnt' Hl]]".
{ iFrame "Hspec Hcnt' Hl Hj"; trivial. }
iApply wp_cas_suc; simpl; trivial; [|iFrame "Hheap"]. solve_ndisj.
iIntros "{$Hcnt} > Hcnt". iPvsIntro.
......@@ -333,7 +334,7 @@ Section CG_Counter.
iExists UnitV; iFrame; auto.
+ (* CAS fails *)
(* In this case, we perform a recursive call *)
iApply (wp_cas_fail _ _ _ _ (v n')); simpl; trivial;
iApply (wp_cas_fail _ _ _ (v n')); simpl; trivial;
[inversion 1; subst; auto | | iFrame "Hheap"]. solve_ndisj.
iIntros "{$Hcnt} > Hcnt". iPvsIntro.
iSplitL "Hl Hcnt Hcnt'"; [iExists _; iFrame "Hl Hcnt Hcnt'"; trivial|].
......@@ -345,8 +346,8 @@ Section CG_Counter.
Transparent counter_read.
unfold counter_read at 2.
iApply wp_lam; trivial. simpl.
iNext. iInv> (N .@4) as {n} "[Hl [Hcnt Hcnt']]".
iPvs (steps_counter_read (N .@ 3) with "[Hj Hcnt']") as "[Hj Hcnt']".
iNext. iInv> counterN as {n} "[Hl [Hcnt Hcnt']]".
iPvs (steps_counter_read with "[Hj Hcnt']") as "[Hj Hcnt']".
{ solve_ndisj. }
{ by iFrame "Hspec Hcnt' Hj". }
iApply wp_load; [|iFrame "Hheap"]. solve_ndisj.
......
......@@ -74,33 +74,33 @@ Proof.
Qed.
Section proof.
Context {Σ : gFunctors} {iS : cfgSG Σ}.
Context `{cfgSG Σ}.
Lemma steps_newlock N E ρ j K :
nclose N E
Spec_ctx N ρ j fill K newlock
Lemma steps_newlock E ρ j K :
nclose specN E
spec_ctx ρ j fill K newlock
={E}=> l, j fill K (Loc l) l ↦ₛ (v false).
Proof.
iIntros {HNE} "[#Hspec Hj]".
by iPvs (step_alloc _ _ _ j K with "[Hj]") as "Hj"; eauto.
by iPvs (step_alloc _ _ j K with "[Hj]") as "Hj"; eauto.
Qed.
Global Opaque newlock.
Lemma steps_acquire N E ρ j K l :
nclose N E
Spec_ctx N ρ l ↦ₛ (v false) j fill K (App acquire (Loc l))
Lemma steps_acquire E ρ j K l :
nclose specN E
spec_ctx ρ l ↦ₛ (v false) j fill K (App acquire (Loc l))
={E}=> j fill K Unit l ↦ₛ (v true).
Proof.
iIntros {HNE} "[#Hspec [Hl Hj]]". unfold acquire.
iPvs (step_lam _ _ _ j K with "[Hj]") as "Hj"; eauto. done.
iPvs (step_cas_suc _ _ _ j (K ++ [IfCtx _ _])
iPvs (step_lam _ _ j K with "[Hj]") as "Hj"; eauto. done.
iPvs (step_cas_suc _ _ j (K ++ [IfCtx _ _])
_ _ _ _ _ _ _ _ _ with "[Hj Hl]") as "[Hj Hl]"; trivial.
rewrite ?fill_app. simpl.
iFrame "Hspec Hj Hl"; trivial.
iNext; trivial.
rewrite ?fill_app. simpl.
iPvs (step_if_true _ _ _ j K _ _ _ with "[Hj]") as "Hj"; trivial.
iPvs (step_if_true _ _ j K _ _ _ with "[Hj]") as "Hj"; trivial.
iFrame "Hspec Hj"; trivial.
iPvsIntro. iFrame "Hj Hl"; trivial.
Unshelve. all:trivial.
......@@ -108,14 +108,14 @@ Section proof.
Global Opaque acquire.
Lemma steps_release N E ρ j K l b:
nclose N E
Spec_ctx N ρ l ↦ₛ (v b) j fill K (App release (Loc l))
Lemma steps_release E ρ j K l b:
nclose specN E
spec_ctx ρ l ↦ₛ (v b) j fill K (App release (Loc l))
={E}=> j fill K Unit l ↦ₛ (v false).
Proof.
iIntros {HNE} "[#Hspec [Hl Hj]]". unfold release.
iPvs (step_lam _ _ _ j K with "[Hj]") as "Hj"; eauto; try done.
iPvs (step_store _ _ _ j K _ _ _ _ _ with "[Hj Hl]") as "[Hj Hl]"; eauto.
iPvs (step_lam _ _ j K with "[Hj]") as "Hj"; eauto; try done.
iPvs (step_store _ _ j K _ _ _ _ _ with "[Hj Hl]") as "[Hj Hl]"; eauto.
iFrame "Hspec Hj"; trivial.
iPvsIntro. iFrame "Hj Hl"; trivial.
Unshelve. all: trivial.
......@@ -123,36 +123,36 @@ Section proof.
Global Opaque release.
Lemma steps_with_lock N E ρ j K e l P Q v w:
nclose N E
Lemma steps_with_lock E ρ j K e l P Q v w:
nclose specN E
( f, e.[f] = e) (* e is a closed term *)
( K', Spec_ctx N ρ P j fill K' (App e (# w))
( K', spec_ctx ρ P j fill K' (App e (# w))
={E}=> j fill K' (# v) Q)
Spec_ctx N ρ P l ↦ₛ (v false)
spec_ctx ρ P l ↦ₛ (v false)
j fill K (App (with_lock e (Loc l)) (# w))
={E}=> j fill K (# v) Q l ↦ₛ (v false).
Proof.
iIntros {HNE H1 H2} "[#Hspec [HP [Hl Hj]]]".
iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
iPvs (step_lam _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. rewrite H1.
iPvs (steps_acquire _ _ _ j (K ++ [AppRCtx (LamV _)])
iPvs (steps_acquire _ _ j (K ++ [AppRCtx (LamV _)])
_ _ with "[Hj Hl]") as "[Hj Hl]"; eauto.
rewrite fill_app; simpl.
iFrame "Hspec Hj"; trivial.
rewrite fill_app; simpl.
iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
iPvs (step_lam _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. rewrite H1.
iPvs (H2 (K ++ [AppRCtx (LamV _)]) with "[Hj HP]") as "[Hj HQ]"; eauto.
rewrite ?fill_app /=.
iFrame "Hspec HP"; trivial.
rewrite ?fill_app /=.
iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
iPvs (step_lam _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl.
iPvs (steps_release _ _ _ j (K ++ [AppRCtx (LamV _)]) _ _ with "[Hj Hl]")
iPvs (steps_release _ _ j (K ++ [AppRCtx (LamV _)]) _ _ with "[Hj Hl]")
as "[Hj Hl]"; eauto.
rewrite ?fill_app /=. by iFrame.
rewrite ?fill_app /=.
iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
iPvs (step_lam _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. iPvsIntro; by iFrame.
Unshelve.
all: try match goal with |- to_val _ = _ => auto using to_of_val end.
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -4,7 +4,7 @@ From iris.algebra Require Export upred_big_op.
From iris.proofmode Require Import tactics pviewshifts invariants.
Section typed_interp.
Context `{heapIG Σ} (L : namespace).
Context `{heapIG Σ}.
Notation D := (valC -n> iPropG lang Σ).
Implicit Types Δ : listC D.
......@@ -15,11 +15,11 @@ Section typed_interp.
Local Ltac value_case := iApply wp_value; [cbn; rewrite ?to_of_val; trivial|].
Lemma typed_interp N Δ Γ vs e τ (HΔ : ctx_PersistentP Δ) (HNLdisj : N L) :
Lemma typed_interp Δ Γ vs e τ (HΔ : ctx_PersistentP Δ) :
Γ ⊢ₜ e : τ
length Γ = length vs
heapI_ctx N [] zip_with (λ τ, interp L τ Δ) Γ vs
WP e.[env_subst vs] {{ interp L τ Δ }}.
heapI_ctx [] zip_with (λ τ, interp τ Δ) Γ vs
WP e.[env_subst vs] {{ interp τ Δ }}.
Proof.
intros Htyped; revert Δ HΔ vs.
induction Htyped; iIntros {Δ HΔ vs Hlen} "#[Hheap HΓ] /=".
......@@ -91,7 +91,7 @@ Section typed_interp.
rewrite zip_with_fmap_l. by iApply context_interp_ren_S.
- (* TApp *)
smart_wp_bind TAppCtx v "#Hv" IHHtyped; cbn.
iApply wp_wand_r; iSplitL; [iApply ("Hv" $! (interp L τ' Δ)); iPureIntro; apply _|]; cbn.
iApply wp_wand_r; iSplitL; [iApply ("Hv" $! (interp τ' Δ)); iPureIntro; apply _|]; cbn.
iIntros {w} "?". by rewrite -interp_subst; simpl.
- (* Fold *)
iApply (@wp_bind _ _ _ [FoldCtx]);
......@@ -103,7 +103,7 @@ Section typed_interp.
iApply (@wp_bind _ _ _ [UnfoldCtx]);
iApply wp_wand_l; iSplitL; [|iApply IHHtyped; auto].
iIntros {v} "#Hv". rewrite /= fixpoint_unfold.
change (fixpoint _) with (interp L (TRec τ) Δ); simpl.
change (fixpoint _) with (interp (TRec τ) Δ); simpl.
iDestruct "Hv" as {w} "#[% Hw]"; subst.
iApply wp_Fold; cbn; auto using to_of_val.
iNext; iPvsIntro. by rewrite -interp_subst.
......@@ -124,8 +124,8 @@ Section typed_interp.
iDestruct "Hv" as {l} "[% #Hv]"; subst.
iApply wp_atomic; cbn; eauto using to_of_val.
iPvsIntro.
iInv (L .@ l) as {w} "[Hw1 #Hw2]".
iApply (wp_load _ _ _ 1); [|iFrame "Hheap"]; trivial. solve_ndisj.
iInv (logN .@ l) as {w} "[Hw1 #Hw2]".
iApply (wp_load _ _ 1); [|iFrame "Hheap"]; trivial. solve_ndisj.
iIntros "{$Hw1} > Hw1". iPvsIntro; iSplitL; eauto.
- (* Store *)
smart_wp_bind (StoreLCtx _) v "#Hv" IHHtyped1; cbn.
......@@ -133,9 +133,9 @@ Section typed_interp.
iDestruct "Hv" as {l} "[% #Hv]"; subst.
iApply wp_atomic; cbn; [trivial| rewrite ?to_of_val; auto |].
iPvsIntro.
iInv (L .@ l) as {z} "[Hz1 #Hz2]".
iInv (logN .@ l) as {z} "[Hz1 #Hz2]".
eapply bool_decide_spec; eauto using to_of_val.
iApply (wp_store N); auto using to_of_val. solve_ndisj.
iApply wp_store; auto using to_of_val. solve_ndisj.
iIntros "{$Hheap $Hz1} > Hz1". iPvsIntro. iSplitL; eauto 10.
- (* CAS *)
smart_wp_bind (CasLCtx _ _) v1 "#Hv1" IHHtyped1; cbn.
......@@ -144,12 +144,12 @@ Section typed_interp.
iDestruct "Hv1" as {l} "[% Hinv]"; subst.
iApply wp_atomic; cbn; eauto 10 using to_of_val.
iPvsIntro.