Commit 4b017ac0 authored by Robbert Krebbers's avatar Robbert Krebbers

Misc clean up.

parent 1999bbc7
Require Import iris.program_logic.hoare.
Require Import iris.program_logic.lifting.
Require Import iris.algebra.upred_big_op.
Require Import iris_logrel.F_mu.lang iris_logrel.F_mu.typing
iris_logrel.F_mu.rules iris_logrel.F_mu.logrel.
From iris.program_logic Require Import lifting.
From iris.algebra Require Import upred_big_op.
From iris_logrel.F_mu Require Import lang typing rules logrel.
Import uPred.
Section typed_interp.
......
......@@ -48,6 +48,8 @@ Module lang.
| InjRV v => InjR (of_val v)
| FoldV v => Fold (of_val v)
end.
Notation "# v" := (of_val v) (at level 20).
Fixpoint to_val (e : expr) : option val :=
match e with
| Lam e => Some (LamV e)
......@@ -235,7 +237,7 @@ Program Canonical Structure lang : language := {|
Solve Obligations with eauto using lang.to_of_val, lang.of_to_val,
lang.values_stuck, lang.atomic_not_val, lang.atomic_step.
Global Instance lang_ctx K : LanguageCtx lang (lang.fill K).
Instance lang_ctx K : LanguageCtx lang (lang.fill K).
Proof.
split.
* eauto using lang.fill_not_val.
......@@ -249,8 +251,7 @@ Proof.
econstructor; eauto.
Qed.
Global Instance lang_ctx_item Ki :
LanguageCtx lang (lang.fill_item Ki).
Instance lang_ctx_item Ki : LanguageCtx lang (lang.fill_item Ki).
Proof. change (LanguageCtx lang (lang.fill [Ki])). by apply _. Qed.
Export lang.
Require Import iris.program_logic.hoare.
Require Import iris.program_logic.lifting.
Require Import iris.algebra.upred_big_op.
Require Import iris_logrel.F_mu.lang iris_logrel.F_mu.typing
......@@ -8,7 +7,6 @@ Import uPred.
(** interp : is a unary logical relation. *)
Section logrel.
Context {Σ : iFunctor}.
Notation "# v" := (of_val v) (at level 20).
(** Just to get nicer closed forms, we define extend_context_interp in three steps. *)
Program Definition extend_context_interp_fun1
......
......@@ -7,14 +7,6 @@ Section lang_rules.
Implicit Types P : iProp lang Σ.
Implicit Types Q : val iProp lang Σ.
Lemma wp_bind {E e} K Q :
wp E e (λ v, wp E (fill K (of_val v)) Q) wp E (fill K e) Q.
Proof. apply weakestpre.wp_bind. Qed.
Lemma wp_bindi {E e} Ki Q :
wp E e (λ v, wp E (fill_item Ki (of_val v)) Q) wp E (fill_item Ki e) Q.
Proof. apply weakestpre.wp_bind. Qed.
Ltac inv_step :=
repeat match goal with
| _ => progress simplify_map_eq/= (* simplify memory stuff *)
......@@ -78,6 +70,10 @@ Section lang_rules.
(** Helper Lemmas for weakestpre. *)
Lemma wp_bind {E e} K Q :
wp E e (λ v, wp E (fill K (of_val v)) Q) wp E (fill K e) Q.
Proof. apply weakestpre.wp_bind. Qed.
Lemma wp_lam E e1 e2 v Q :
to_val e2 = Some v wp E e1.[e2 /] Q wp E (App (Lam e1) e2) Q.
Proof.
......@@ -104,7 +100,7 @@ Section lang_rules.
Lemma wp_fst E e1 v1 e2 v2 Q :
to_val e1 = Some v1 to_val e2 = Some v2
Q v1 wp E (Fst (Pair e1 e2)) Q.
Q v1 wp E (Fst (Pair e1 e2)) Q.
Proof.
intros <-%of_to_val <-%of_to_val.
rewrite -(wp_lift_pure_det_step (Fst (Pair _ _)) (of_val v1) None) //=; auto.
......@@ -137,5 +133,4 @@ Section lang_rules.
rewrite -(wp_lift_pure_det_step (Case (InjR _) _ _) (e2.[of_val v0/]) None) //=; auto.
- rewrite right_id; auto using uPred.later_mono, wp_value'.
Qed.
End lang_rules.
\ No newline at end of file
End lang_rules.
Require Import iris.proofmode.tactics.
Require Import iris.program_logic.hoare.
Require Import iris.program_logic.lifting.
Require Import iris.algebra.upred_big_op.
Require Import iris_logrel.F_mu.lang iris_logrel.F_mu.typing
......@@ -41,4 +40,4 @@ Section Soundness.
- iIntros "H". iApply H1.
- constructor.
Qed.
End Soundness.
\ No newline at end of file
End Soundness.
......@@ -60,8 +60,6 @@ Qed.
Definition env_subst (vs : list val) (x : var) : expr :=
from_option id (Var x) (of_val <$> vs !! x).
Notation "# v" := (of_val v) (at level 20).
Lemma typed_subst_head_simpl Δ τ e w ws :
typed Δ e τ -> List.length Δ = S (List.length ws)
e.[# w .: env_subst ws] = e.[env_subst (w :: ws)].
......
Require Import iris.program_logic.hoare.
Require Import iris.program_logic.lifting.
Require Import iris.algebra.upred_big_op.
Require Import iris_logrel.F_mu_ref.lang iris_logrel.F_mu_ref.typing
......@@ -11,9 +10,8 @@ Require Import iris.proofmode.tactics iris.proofmode.invariants.
Import uPred.
Section typed_interp.
Context {Σ : gFunctors} `{i : heapG Σ} `{L : namespace}.
Context {Σ : gFunctors} `{i : heapG Σ} {L : namespace}.
Implicit Types P Q R : iPropG lang Σ.
Notation "# v" := (of_val v) (at level 20).
Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) :=
iApply (@wp_bind _ _ _ [ctx]);
......
......@@ -6,7 +6,7 @@ Require Export Autosubst.Autosubst.
Module lang.
Definition loc := positive.
Global Instance loc_dec_eq (l l' : loc) : Decision (l = l') := _.
Instance loc_dec_eq (l l' : loc) : Decision (l = l') := _.
Inductive expr :=
| Var (x : var)
......@@ -39,11 +39,8 @@ Module lang.
Instance Subst_expr : Subst expr. derive. Defined.
Instance SubstLemmas_expr : SubstLemmas expr. derive. Qed.
Global Instance expr_dec_eq (e e' : expr) : Decision (e = e').
Proof.
unfold Decision.
decide equality; [apply eq_nat_dec | apply loc_dec_eq].
Defined.
Instance expr_dec_eq (e e' : expr) : Decision (e = e').
Proof. solve_decision. Defined.
Inductive val :=
| LamV (e : {bind 1 of expr})
......@@ -55,13 +52,10 @@ Module lang.
| FoldV (v : val)
| LocV (l : loc).
Global Instance val_dec_eq (v v' : val) : Decision (v = v').
Proof.
unfold Decision; decide equality; try apply expr_dec_eq; apply loc_dec_eq.
Defined.
Instance val_dec_eq (v v' : val) : Decision (v = v').
Proof. solve_decision. Defined.
Global Instance val_inh : Inhabited val.
Proof. constructor. exact UnitV. Qed.
Instance val_inh : Inhabited val := populate UnitV.
Fixpoint of_val (v : val) : expr :=
match v with
......@@ -74,6 +68,7 @@ Module lang.
| FoldV v => Fold (of_val v)
| LocV l => Loc l
end.
Notation "# v" := (of_val v) (at level 20).
Fixpoint to_val (e : expr) : option val :=
match e with
......@@ -310,7 +305,7 @@ Program Canonical Structure lang : language := {|
Solve Obligations with eauto using lang.to_of_val, lang.of_to_val,
lang.values_stuck, lang.atomic_not_val, lang.atomic_step.
Global Instance lang_ctx K : LanguageCtx lang (lang.fill K).
Instance lang_ctx K : LanguageCtx lang (lang.fill K).
Proof.
split.
* eauto using lang.fill_not_val.
......@@ -324,8 +319,7 @@ Proof.
econstructor; eauto.
Qed.
Global Instance lang_ctx_item Ki :
LanguageCtx lang (lang.fill_item Ki).
Instance lang_ctx_item Ki : LanguageCtx lang (lang.fill_item Ki).
Proof. change (LanguageCtx lang (lang.fill [Ki])). by apply _. Qed.
Export lang.
Require Import iris.program_logic.hoare.
Require Import iris.program_logic.lifting.
Require Import iris.algebra.upred_big_op.
Require Import iris_logrel.F_mu_ref.lang iris_logrel.F_mu_ref.typing
......@@ -12,7 +11,6 @@ Import uPred.
(** interp : is a unary logical relation. *)
Section logrel.
Context {Σ : gFunctors}.
Notation "# v" := (of_val v) (at level 20).
(** Just to get nicer closed forms, we define extend_context_interp in three steps. *)
Program Definition extend_context_interp_fun1
......
......@@ -9,43 +9,39 @@ From iris.program_logic Require Import ownership auth.
Require Import iris.proofmode.tactics iris.proofmode.invariants.
Import uPred.
Section lang_rules.
Definition heapUR : ucmraT := gmapUR loc (prodR fracR (dec_agreeR val)).
(** The CMRA we need. *)
Class heapG Σ :=
HeapG {
heap_inG :> authG lang Σ heapUR;
heap_name : gname
}.
(** The Functor we need. *)
Definition heapGF : gFunctor := authGF heapUR.
Definition to_heap : state heapUR := fmap (λ v, (1%Qp, DecAgree v)).
Definition of_heap : heapUR state := omap (maybe DecAgree snd).
Section definitions.
Context `{i : heapG Σ}.
Definition heap_mapsto (l : loc) (q : Qp) (v: val) : iPropG lang Σ :=
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.
Global Instance heap_inv_proper : Proper (() ==> ()) heap_inv.
Proof. solve_proper. Qed.
Global Instance heap_ctx_always_stable N : PersistentP (heap_ctx N).
Proof. apply _. Qed.
End definitions.
Typeclasses Opaque heap_ctx heap_mapsto.
Definition heapUR : ucmraT := gmapUR loc (prodR fracR (dec_agreeR val)).
(** The CMRA we need. *)
Class heapG Σ :=
HeapG { heap_inG :> authG lang Σ heapUR; heap_name : gname }.
(** The Functor we need. *)
Definition heapGF : gFunctor := authGF heapUR.
Definition to_heap : state heapUR := fmap (λ v, (1%Qp, DecAgree v)).
Definition of_heap : heapUR state := omap (maybe DecAgree snd).
Section definitions.
Context `{heapG Σ}.
Definition heap_mapsto (l : loc) (q : Qp) (v: val) : iPropG lang Σ :=
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.
Global Instance heap_inv_proper : Proper (() ==> ()) heap_inv.
Proof. solve_proper. Qed.
Global Instance heap_ctx_always_stable N : PersistentP (heap_ctx N).
Proof. apply _. Qed.
End definitions.
Typeclasses Opaque heap_ctx heap_mapsto.
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.
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.
Section heap.
Section lang_rules.
Context {Σ : gFunctors}.
Implicit Types N : namespace.
Implicit Types P Q : iPropG lang Σ.
......@@ -53,15 +49,6 @@ Section lang_rules.
Implicit Types σ : state.
Implicit Types h g : heapUR.
Lemma wp_bind {E e} K Φ :
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 {{Φ}}.
Proof. apply weakestpre.wp_bind. Qed.
Ltac inv_step :=
repeat
match goal with
......@@ -302,9 +289,14 @@ Section lang_rules.
(** Helper Lemmas for weakestpre. *)
Lemma wp_bind {E e} K Φ :
WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }}
WP fill K e @ E {{ Φ }}.
Proof. apply weakestpre.wp_bind. Qed.
Lemma wp_lam E e1 e2 v Φ :
to_val e2 = Some v
WP e1.[e2 /] @ E {{Φ}} WP (App (Lam e1) e2) @ E {{Φ}}.
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) //=.
......@@ -313,7 +305,7 @@ Section lang_rules.
Qed.
Lemma wp_TLam E e Φ :
WP e @ E {{Φ}} WP (TApp (TLam e)) @ E {{Φ}}.
WP e @ E {{ Φ }} WP TApp (TLam e) @ E {{ Φ }}.
Proof.
rewrite -(wp_lift_pure_det_step (TApp _) e None) //=.
- by rewrite right_id.
......@@ -322,7 +314,7 @@ Section lang_rules.
Lemma wp_Fold E e v Φ :
to_val e = Some v
Φ v WP (Unfold (Fold e)) @ E {{Φ}}.
Φ v WP Unfold (Fold e) @ E {{ Φ }}.
Proof.
intros <-%of_to_val.
rewrite -(wp_lift_pure_det_step (Unfold _) (of_val v) None) //=; auto.
......@@ -332,7 +324,7 @@ Section lang_rules.
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 {{Φ}}.
Φ v1 WP Fst (Pair e1 e2) @ E {{ Φ }}.
Proof.
intros <-%of_to_val <-%of_to_val.
rewrite -(wp_lift_pure_det_step (Fst (Pair _ _)) (of_val v1) None) //=.
......@@ -342,7 +334,7 @@ Section lang_rules.
Lemma wp_snd E e1 v1 e2 v2 Φ :
to_val e1 = Some v1 to_val e2 = Some v2
Φ v2 WP (Snd (Pair e1 e2)) @ E {{Φ}}.
Φ v2 WP Snd (Pair e1 e2) @ E {{ Φ }}.
Proof.
intros <-%of_to_val <-%of_to_val.
rewrite -(wp_lift_pure_det_step (Snd (Pair _ _)) (of_val v2) None) //=.
......@@ -352,7 +344,7 @@ Section lang_rules.
Lemma wp_case_inl E e0 v0 e1 e2 Φ :
to_val e0 = Some v0
WP e1.[e0/] @ E {{Φ}} WP (Case (InjL e0) e1 e2) @ E {{Φ}}.
WP e1.[e0/] @ E {{ Φ }} WP Case (InjL e0) e1 e2 @ E {{ Φ }}.
Proof.
intros <-%of_to_val.
rewrite -(wp_lift_pure_det_step
......@@ -363,7 +355,7 @@ Section lang_rules.
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 {{Φ}}.
WP e2.[e0/] @ E {{ Φ }} WP Case (InjR e0) e1 e2 @ E {{ Φ }}.
Proof.
intros <-%of_to_val.
rewrite -(wp_lift_pure_det_step
......@@ -371,9 +363,4 @@ Section lang_rules.
- rewrite right_id; auto using uPred.later_mono, wp_value'.
- intros. inv_step; auto.
Qed.
End heap.
End lang_rules.
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.
Require Import iris.proofmode.weakestpre iris.proofmode.tactics.
Require Import iris.program_logic.hoare.
Require Import iris.program_logic.lifting.
Require Import iris.algebra.auth.
Require Import iris_logrel.F_mu_ref.lang iris_logrel.F_mu_ref.typing
......
......@@ -66,8 +66,6 @@ Qed.
Definition env_subst (vs : list val) (x : var) : expr :=
from_option id (Var x) (of_val <$> vs !! x).
Notation "# v" := (of_val v) (at level 20).
Lemma typed_subst_head_simpl Δ τ e w ws :
typed Δ e τ -> List.length Δ = S (List.length ws)
e.[# w .: env_subst ws] = e.[env_subst (w :: ws)].
......
......@@ -202,9 +202,7 @@ Definition context_refines Γ e e' τ :=
rtc step ([fill_ctx K e'], ) ((# v') :: thp', h').
Section bin_log_related_under_typed_context.
Context {Σ : gFunctors}
{iI : heapIG Σ} {iS : cfgSG Σ}
{N : namespace}.
Context {Σ : gFunctors} {iI : heapIG Σ} {iS : cfgSG Σ} {N : namespace}.
Implicit Types Δ : varC -n> bivalC -n> iPropG lang Σ.
Lemma bin_log_related_under_typed_context Γ e e' τ Γ' τ' K :
......
......@@ -373,8 +373,7 @@ End CG_Counter.
Definition Σ := #[auth.authGF heapUR; auth.authGF cfgUR].
Theorem counter_context_refinement :
context_refines
[] FG_counter CG_counter
context_refines [] FG_counter CG_counter
(TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
Proof.
eapply (@Binary_Soundness Σ);
......
......@@ -21,12 +21,10 @@ Definition with_lockV (e l : expr) : val :=
(App acquire l.[ren (+2)])
).
Lemma with_lock_to_val e l :
to_val (with_lock e l) = Some (with_lockV e l).
Lemma with_lock_to_val e l : to_val (with_lock e l) = Some (with_lockV e l).
Proof. trivial. Qed.
Lemma with_lock_of_val e l :
of_val (with_lockV e l) = with_lock e l.
Lemma with_lock_of_val e l : of_val (with_lockV e l) = with_lock e l.
Proof. trivial. Qed.
Global Opaque with_lockV.
......@@ -43,8 +41,7 @@ Lemma release_closed f : release.[f] = release.
Proof. by asimpl. Qed.
Hint Rewrite release_closed : autosubst.
Lemma with_lock_subst (e l : expr) f :
(with_lock e l).[f] = with_lock e.[f] l.[f].
Lemma with_lock_subst (e l : expr) f : (with_lock e l).[f] = with_lock e.[f] l.[f].
Proof. unfold with_lock; asimpl; trivial. Qed.
Lemma with_lock_closed e l:
......
......@@ -28,15 +28,13 @@ Section CG_Stack.
( f, st.[f] = st) f, (CG_push st).[f] = CG_push st.
Proof. intros H f. unfold CG_push. asimpl. rewrite ?H; trivial. Qed.
Lemma CG_push_subst (st : expr) f :
(CG_push st).[f] = CG_push st.[f].
Lemma CG_push_subst (st : expr) f : (CG_push st).[f] = CG_push st.[f].
Proof. unfold CG_push; asimpl; trivial. Qed.
Lemma steps_CG_push N E ρ j K st v w :
nclose N E
((Spec_ctx N ρ st ↦ₛ v
j (fill K (App (CG_push (Loc st)) (# w))))%I)
|={E}=>(j (fill K (Unit)) st ↦ₛ (FoldV (InjRV (PairV w v))))%I.
Spec_ctx N ρ st ↦ₛ v j fill K (App (CG_push (Loc st)) (# w))
={E}=> j fill K Unit st ↦ₛ FoldV (InjRV (PairV w v)).
Proof.
intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_push.
iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
......@@ -47,8 +45,7 @@ Section CG_Stack.
rewrite ?fill_app. simpl.
iFrame "Hspec Hj"; trivial.
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. by iFrame.
Unshelve.
......@@ -91,15 +88,14 @@ Section CG_Stack.
Qed.
Lemma CG_locked_push_subst (st l : expr) f :
(CG_locked_push st l).[f] = CG_locked_push st.[f] l.[f].
(CG_locked_push st l).[f] = CG_locked_push st.[f] l.[f].
Proof. by rewrite with_lock_subst CG_push_subst. Qed.
Lemma steps_CG_locked_push N E ρ j K st w v l :
nclose N E
((Spec_ctx N ρ st ↦ₛ v l ↦ₛ (v false)
j (fill K (App (CG_locked_push (Loc st) (Loc l)) (# w))))%I)
|={E}=>(j (fill K (Unit)) st ↦ₛ (FoldV (InjRV (PairV w v)))
l ↦ₛ (v false))%I.
Spec_ctx N ρ st ↦ₛ v l ↦ₛ (v false)
j fill K (App (CG_locked_push (Loc st) (Loc l)) (# w))
={E}=> j fill K Unit st ↦ₛ FoldV (InjRV (PairV w v)) l ↦ₛ (v false).
Proof.
intros HNE. iIntros "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_push.
iPvs (steps_with_lock
......@@ -290,12 +286,10 @@ Section CG_Stack.
Definition CG_snapV (st l : expr) : val :=
with_lockV (Lam (Load st.[ren (+2)])) l.
Lemma CG_snap_to_val st l :
to_val (CG_snap st l) = Some (CG_snapV st l).
Lemma CG_snap_to_val st l : to_val (CG_snap st l) = Some (CG_snapV st l).
Proof. trivial. Qed.
Lemma CG_snap_of_val st l :
of_val (CG_snapV st l) = CG_snap st l.
Lemma CG_snap_of_val st l : of_val (CG_snapV st l) = CG_snap st l.
Proof. trivial. Qed.
Global Opaque CG_snapV.
......@@ -403,8 +397,7 @@ Section CG_Stack.
( g, f.[g] = f) g, (CG_iter f).[g] = CG_iter f.
Proof. intros H g. unfold CG_iter. asimpl. rewrite ?H; trivial. Qed.
Lemma CG_iter_subst (f : expr) g :
(CG_iter f).[g] = CG_iter f.[g].
Lemma CG_iter_subst (f : expr) g : (CG_iter f).[g] = CG_iter f.[g].
Proof. unfold CG_iter; asimpl; trivial. Qed.
Lemma steps_CG_iter N E ρ j K f v w :
......@@ -461,14 +454,10 @@ Section CG_Stack.
Global Opaque CG_iter.
Definition CG_snap_iter (st l : expr) : expr :=
Lam (App (CG_iter (Var 1)) (App (CG_snap st.[ren (+2)] l.[ren (+2)]) Unit)).
Lemma CG_snap_iter_type st l Γ τ :
typed Γ st (Tref (CG_StackType τ))
typed Γ l LockType
typed Γ (CG_snap_iter st l)
(TArrow (TArrow τ TUnit) TUnit).
typed Γ (CG_snap_iter st l) (TArrow (TArrow τ TUnit) TUnit).
Proof.
intros H1 H2; repeat econstructor.
- eapply CG_iter_type; by constructor.
......@@ -476,8 +465,7 @@ Section CG_Stack.
Qed.
Lemma CG_snap_iter_closed (st l : expr) :
( f, st.[f] = st)
( f, l.[f] = l)
( f, st.[f] = st) ( f, l.[f] = l)
f, (CG_snap_iter st l).[f] = CG_snap_iter st l.
Proof.
intros H1 H2 f. unfold CG_snap_iter. asimpl. rewrite H1 H2.
......@@ -485,7 +473,7 @@ Section CG_Stack.
Qed.
Lemma CG_snap_iter_subst (st l : expr) g :
(CG_snap_iter st l).[g] = CG_snap_iter st.[g] l.[g].
(CG_snap_iter st l).[g] = CG_snap_iter st.[g] l.[g].
Proof.
unfold CG_snap_iter; asimpl.
rewrite CG_snap_subst CG_iter_subst. by asimpl.
......@@ -512,8 +500,7 @@ Section CG_Stack.
Opaque CG_snap_iter.
Lemma CG_stack_body_closed (st l : expr) :
( f, st.[f] = st)
( f, l.[f] = l)
( f, st.[f] = st) ( f, l.[f] = l)
f, (CG_stack_body st l).[f] = CG_stack_body st l.
Proof.
intros H1 H2 f. unfold CG_stack_body. asimpl.
......@@ -545,13 +532,10 @@ Section CG_Stack.
- eapply newlock_type.
Qed.
Lemma CG_stack_closed f :
CG_stack.[f] = CG_stack.
Lemma CG_stack_closed f : CG_stack.[f] = CG_stack.
Proof.
unfold CG_stack.
asimpl; rewrite ?CG_locked_push_subst ?CG_locked_pop_subst.
asimpl. rewrite ?CG_snap_iter_subst. by asimpl.
Qed.
Transparent CG_snap_iter.
End CG_Stack.
......@@ -5,7 +5,7 @@ Section FG_stack.
Context {Σ : gFunctors} {iI : heapIG Σ}.
Definition FG_StackType τ :=
(TRec (Tref (TSum TUnit (TProd τ.[ren (+1)] (TVar 0))))).
TRec (Tref (TSum TUnit (TProd τ.[ren (+1)] (TVar 0)))).
(* Fine-grained push *)
Definition FG_push (st : expr) : expr :=
......@@ -79,8 +79,7 @@ Section FG_stack.
( f, st.[f] = st) f, (FG_push st).[f] = FG_push st.
Proof. intros H f. asimpl. unfold FG_push. rewrite ?H; trivial. Qed.
Lemma FG_push_subst (st : expr) f :
(FG_push st).[f] = FG_push st.[f].
Lemma FG_push_subst (st : expr) f : (FG_push st).[f] = FG_push st.[f].
Proof. unfold FG_push. by asimpl. Qed.
Global Opaque FG_push.
......@@ -201,8 +200,7 @@ Section FG_stack.
( f, st.[f] = st) f, (FG_pop st).[f] = FG_pop st.
Proof. intros H f. asimpl. unfold FG_pop. rewrite ?H; trivial. Qed.
Lemma FG_pop_subst (st : expr) f :
(FG_pop st).[f] = FG_pop st.[f].
Lemma FG_pop_subst (st : expr) f : (FG_pop st).[f] = FG_pop st.[f].
Proof. unfold FG_pop. by asimpl. Qed.
Global Opaque FG_pop.
......@@ -265,8 +263,7 @@ Section FG_stack.
( g, f.[g] = f) g, (FG_iter f).[g] = FG_iter f.
Proof. intros H g. asimpl. unfold FG_iter. rewrite ?H; trivial. Qed.
Lemma FG_iter_subst (f : expr) g :
(FG_iter f).[g] = FG_iter f.[g].
Lemma FG_iter_subst (f : expr) g : (FG_iter f).[g] = FG_iter f.[g].
Proof. unfold FG_iter. by asimpl. Qed.
Global Opaque FG_iter.
......@@ -295,7 +292,7 @@ Section FG_stack.
Qed.
Lemma FG_read_iter_subst (st : expr) g :
(FG_read_iter st).[g] = FG_read_iter st.[g].
(FG_read_iter st).[g] = FG_read_iter st.[g].
Proof. by unfold FG_read_iter; asimpl. Qed.
Global Opaque FG_iter.
......@@ -363,17 +360,12 @@ Section FG_stack.
- eapply FG_read_iter_type; constructor; by simpl.
- asimpl. repeat constructor.
Qed.
End FG_stack_type.
Lemma FG_stack_closed f :
FG_stack.[f] = FG_stack.
Lemma FG_stack_closed f : FG_stack.[f] = FG_stack.
Proof.
unfold FG_stack.
asimpl; rewrite ?FG_push_subst ?FG_pop_subst.
asimpl. rewrite ?FG_read_iter_subst. by asimpl.
Qed.
Transparent FG_read_iter.
End FG_stack.
\ No newline at end of file
End FG_stack.
......@@ -208,8 +208,7 @@ Section Stack_refinement.
as "[Histk HLoe]".
{ by iFrame "Hmpt". }
iApply (wp_load _ _ _ _ _ _ _). iFrame "Hheap Histk".
iNext. iIntros "Histk".
iSplitR "Hj".
iIntros "> Histk". iSplitR "Hj".
{ iNext. iExists _, _, _. iFrame "Hstk' Hstk HLK Hl".
iDestruct ("HLoe" with "[Histk]") as "[Hh _]"; trivial.
}
......@@ -233,7 +232,7 @@ Section Stack_refinement.
as "[Histk HLoe]".
{ by iFrame "Hmpt". }
iApply (wp_load _ _ _ _ _ _ _). iFrame "Hheap Histk".
iNext. iIntros "Histk".
iIntros "> Histk".
iDestruct ("HLoe" with "[Histk]") as "[Hh Hmpt]"; trivial.
iSplitR "Hj Hmpt HLK'".
{ iNext. iExists _, _, _. by iFrame "Hstk' Hstk HLK Hl". }
......@@ -432,8 +431,7 @@ End Stack_refinement.
Definition Σ := #[authGF heapUR; authGF cfgUR; authGF stackUR].
Theorem stack_context_refinement :
context_refines
[] FG_stack CG_stack
context_refines [] FG_stack CG_stack
(TForall
(TProd
(TProd
......
......@@ -17,20 +17,17 @@ Proof.
Qed.
Class stackG Σ :=
StackG {
stack_inG :> authG lang Σ stackUR;
stack_name : gname