Skip to content

GitLab

R
ReLoC-v1
Commit 70299030 authored by Dan Frumin's avatar Dan Frumin
Browse files
Options

Update F_mu_ref to work with Iris 3 

Main changes:
- Rewrite cfgG and cfgUR
- Use gen_heap from iris
parent 6d458e00
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 270 additions and 322 deletions
F_mu_ref/fundamental.v
View file @ 70299030
......@@ -5,7 +5,7 @@ From iris.base_logic Require Export big_op.
Definition log_typed `{heapG Σ} (Γ : list type) (e : expr) (τ : type) := ∀ Δ vs,
env_PersistentP Δ →
heap_ctx ∧ ⟦ Γ ⟧* Δ vs ⊢ ⟦ τ ⟧ₑ Δ e.[env_subst vs].
⟦ Γ ⟧* Δ vs ⊢ ⟦ τ ⟧ₑ Δ e.[env_subst vs].
Notation "Γ ⊨ e : τ" := (log_typed Γ e τ) (at level 74, e, τ at next level).
Section fundamental.
......@@ -15,13 +15,13 @@ Section fundamental.
Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) :=
iApply (wp_bind [ctx]);
iApply wp_wand_l;
iSplitL; [|iApply Hp; trivial]; [iIntros (v) Hv|iSplit; trivial]; cbn.
iSplitR; [|iApply Hp; trivial]; iIntros (v) Hv; cbn.
Local Ltac value_case := iApply wp_value; [cbn; rewrite ?to_of_val; trivial|].
Theorem fundamental Γ e τ : Γ ⊢ₜ e : τ → Γ ⊨ e : τ.
Proof.
induction 1; iIntros (Δ vs HΔ) "#[Hheap HΓ] /=".
induction 1; iIntros (Δ vs HΔ) "#HΓ /=".
- (* var *)
iDestruct (interp_env_Some_l with "HΓ") as (v) "[% ?]"; first done.
rewrite /env_subst. simplify_option_eq. by value_case.
......@@ -29,7 +29,7 @@ Section fundamental.
- (* pair *)
smart_wp_bind (PairLCtx e2.[env_subst vs]) v "#Hv" IHtyped1.
smart_wp_bind (PairRCtx v) v' "# Hv'" IHtyped2.
value_case; eauto 10.
value_case; eauto 10.
- (* fst *)
smart_wp_bind (FstCtx) v "# Hv" IHtyped; cbn.
iDestruct "Hv" as (w1 w2) "#[% [H2 H3]]"; subst.
......@@ -50,16 +50,16 @@ Section fundamental.
iDestruct "Hv" as "[Hv|Hv]"; iDestruct "Hv" as (w) "[% Hw]"; simplify_eq/=.
+ iApply wp_case_inl; auto 1 using to_of_val; asimpl. iNext.
erewrite typed_subst_head_simpl by naive_solver.
iApply (IHtyped2 Δ (w :: vs)). iSplit; [|iApply interp_env_cons]; auto.
iApply (IHtyped2 Δ (w :: vs)). iApply interp_env_cons; auto.
+ iApply wp_case_inr; auto 1 using to_of_val; asimpl. iNext.
erewrite typed_subst_head_simpl by naive_solver.
iApply (IHtyped3 Δ (w :: vs)). iSplit; [|iApply interp_env_cons]; auto.
iApply (IHtyped3 Δ (w :: vs)). iApply interp_env_cons; auto.
- (* lam *)
value_case; iAlways; iIntros (w) "#Hw".
value_case. simpl. iAlways. iIntros (w) "#Hw".
iDestruct (interp_env_length with "HΓ") as %?.
iApply wp_lam; auto 1 using to_of_val. iNext.
asimpl. erewrite typed_subst_head_simpl by naive_solver.
iApply (IHtyped Δ (w :: vs)). iFrame "Hheap". iApply interp_env_cons; auto.
iApply (IHtyped Δ (w :: vs)). iApply interp_env_cons; auto.
- (* app *)
smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHtyped1.
smart_wp_bind (AppRCtx v) w "#Hw" IHtyped2.
......@@ -67,7 +67,7 @@ Section fundamental.
- (* TLam *)
value_case.
iAlways; iIntros (τi) "%". iApply wp_tlam; iNext.
iApply IHtyped. iFrame "Hheap". by iApply interp_env_ren.
iApply IHtyped. by iApply interp_env_ren.
- (* TApp *)
smart_wp_bind TAppCtx v "#Hv" IHtyped; cbn.
iApply wp_wand_r; iSplitL; [iApply ("Hv" $! (interp τ' Δ)); iPureIntro; apply _|].
......@@ -88,7 +88,7 @@ Section fundamental.
iNext; iModIntro. by rewrite -interp_subst.
- (* Alloc *)
smart_wp_bind AllocCtx v "#Hv" IHtyped; cbn. iClear "HΓ". iApply wp_fupd.
iApply (wp_alloc with "Hheap []"); auto 1 using to_of_val.
iApply wp_alloc; auto 1 using to_of_val.
iNext; iIntros (l) "Hl".
iMod (inv_alloc _ with "[Hl]") as "HN";
[| iModIntro; iExists _; iSplit; trivial]; eauto.
......@@ -96,16 +96,15 @@ Section fundamental.
smart_wp_bind LoadCtx v "#Hv" IHtyped; cbn. iClear "HΓ".
iDestruct "Hv" as (l) "[% #Hv]"; subst.
iInv (logN .@ l) as (w) "[Hw1 #Hw2]" "Hclose".
iApply ((wp_load _ _ 1) with "[Hw1] [Hclose]"); [|iFrame "Hheap"|];
trivial. solve_ndisj. iNext.
iIntros "Hw1". iMod ("Hclose" with "[-]"); eauto.
iApply (wp_load with "Hw1 [Hclose]").
iNext.
iIntros "Hw1". iMod ("Hclose" with "[Hw1 Hw2]"); eauto.
- (* Store *)
smart_wp_bind (StoreLCtx _) v "#Hv" IHtyped1; cbn.
smart_wp_bind (StoreRCtx _) w "#Hw" IHtyped2; cbn. iClear "HΓ".
iDestruct "Hv" as (l) "[% #Hv]"; subst.
iInv (logN .@ l) as (z) "[Hz1 #Hz2]" "Hclose".
iApply (wp_store with "[Hz1] [Hclose]"); [| |iFrame "Hheap Hz1"|].
by rewrite to_of_val. solve_ndisj. iNext.
iIntros "Hz1". iMod ("Hclose" with "[-]"); eauto.
iApply (wp_store with "Hz1 [Hclose]"); eauto using to_of_val. iNext.
iIntros "Hz1". iMod ("Hclose" with "[Hz1 Hz2]"); eauto.
Qed.
End fundamental.
F_mu_ref/fundamental_binary.v
View file @ 70299030
This diff is collapsed.
F_mu_ref/lang.v
View file @ 70299030
From iris.program_logic Require Export ectx_language ectxi_language.
From iris_logrel.prelude Require Export base.
From iris.algebra Require Export cofe.
From iris.algebra Require Export ofe.
From iris.prelude Require Import gmap.
Module lang.
......@@ -232,10 +232,13 @@ Definition is_atomic (e : expr) : Prop :=
| Store e1 e2 => is_Some (to_val e1) ∧ is_Some (to_val e2)
| _ => False
end.
Local Hint Resolve language.val_irreducible.
Local Hint Resolve to_of_val.
Local Hint Unfold language.irreducible.
Lemma is_atomic_correct e : is_atomic e → language.atomic e.
Proof.
intros ?; apply ectx_language_atomic.
- destruct 1; simpl; by eauto using to_of_val.
- destruct 1; simpl; eauto.
- intros [|Ki K] e' -> Hval%eq_None_not_Some; [done|].
destruct Hval; apply (fill_val K e'). destruct Ki; naive_solver.
Qed.
......
F_mu_ref/logrel.v
View file @ 70299030
......@@ -19,16 +19,16 @@ Section logrel.
from_option id (cconst True)%I (Δ !! x).
Solve Obligations with solve_proper_alt.
Definition interp_unit : listC D -n> D := λne Δ w, (w = UnitV)%I.
Definition interp_unit : listC D -n> D := λne Δ w, ⌜w = UnitV⌝%I.
Program Definition interp_prod
(interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ w,
(∃ w1 w2, w = PairV w1 w2 ∧ interp1 Δ w1 ∧ interp2 Δ w2)%I.
(∃ w1 w2, ⌜w = PairV w1 w2⌝ ∧ interp1 Δ w1 ∧ interp2 Δ w2)%I.
Solve Obligations with solve_proper.
Program Definition interp_sum
(interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ w,
((∃ w1, w = InjLV w1 ∧ interp1 Δ w1) ∨ (∃ w2, w = InjRV w2 ∧ interp2 Δ w2))%I.
((∃ w1, ⌜w = InjLV w1⌝ ∧ interp1 Δ w1) ∨ (∃ w2, ⌜w = InjRV w2⌝ ∧ interp2 Δ w2))%I.
Solve Obligations with solve_proper.
Program Definition interp_arrow
......@@ -39,20 +39,16 @@ Section logrel.
Program Definition interp_forall
(interp : listC D -n> D) : listC D -n> D := λne Δ w,
(□ ∀ τi : D,
■ (∀ v, PersistentP (τi v)) → WP TApp (# w) {{ interp (τi :: Δ) }})%I.
⌜(∀ v, PersistentP (τi v))⌝ → WP TApp (# w) {{ interp (τi :: Δ) }})%I.
Solve Obligations with solve_proper.
Definition interp_rec1
(interp : listC D -n> D) (Δ : listC D) (τi : D) : D := λne w,
(□ (∃ v, w = FoldV v ∧ ▷ interp (τi :: Δ) v))%I.
(□ (∃ v, ⌜w = FoldV v⌝ ∧ ▷ interp (τi :: Δ) v))%I.
Global Instance interp_rec1_contractive
(interp : listC D -n> D) (Δ : listC D) : Contractive (interp_rec1 interp Δ).
Proof.
intros n τi1 τi2 Hτi w; cbn.
apply always_ne, exist_ne; intros v; apply and_ne; trivial.
apply later_contractive =>i Hi. by rewrite Hτi.
Qed.
Proof. by solve_contractive. Qed.
Program Definition interp_rec (interp : listC D -n> D) : listC D -n> D := λne Δ,
fixpoint (interp_rec1 interp Δ).
......@@ -66,7 +62,7 @@ Section logrel.
Program Definition interp_ref
(interp : listC D -n> D) : listC D -n> D := λne Δ w,
(∃ l, w = LocV l ∧ inv (logN .@ 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 :=
......@@ -84,7 +80,7 @@ Section logrel.
Definition interp_env (Γ : list type)
(Δ : listC D) (vs : list val) : iProp Σ :=
(length Γ = length vs ∗ [∗] zip_with (λ τ, ⟦ τ ⟧ Δ) Γ vs)%I.
(⌜length Γ = length vs⌝ ∗ [∗] zip_with (λ τ, ⟦ τ ⟧ Δ) Γ vs)%I.
Notation "⟦ Γ ⟧*" := (interp_env Γ).
Definition interp_expr (τ : type) (Δ : listC D) (e : expr) : iProp Σ :=
......@@ -122,7 +118,7 @@ Section logrel.
properness; auto. apply (IHτ (_ :: _)).
- rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
{ by rewrite !lookup_app_l. }
rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia. done.
rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia.
- intros w; simpl; properness; auto. apply (IHτ (_ :: _)).
- intros w; simpl; properness; auto. by apply IHτ.
Qed.
......@@ -143,7 +139,7 @@ Section logrel.
rewrite !lookup_app_r; [|lia ..].
destruct (x - length Δ1) as [|n] eqn:?; simpl.
{ symmetry. asimpl. apply (interp_weaken [] Δ1 Δ2 τ'). }
rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia. done.
rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia.
- intros w; simpl; properness; auto. apply (IHτ (_ :: _)).
- intros w; simpl; properness; auto. by apply IHτ.
Qed.
......@@ -151,11 +147,11 @@ Section logrel.
Lemma interp_subst Δ2 τ τ' : ⟦ τ ⟧ (⟦ τ' ⟧ Δ2 :: Δ2) ≡ ⟦ τ.[τ'/] ⟧ Δ2.
Proof. apply (interp_subst_up []). Qed.
Lemma interp_env_length Δ Γ vs : ⟦ Γ ⟧* Δ vs ⊢ length Γ = length vs.
Lemma interp_env_length Δ Γ vs : ⟦ Γ ⟧* Δ vs ⊢ ⌜length Γ = length vs⌝.
Proof. by iIntros "[% ?]". Qed.
Lemma interp_env_Some_l Δ Γ vs x τ :
Γ !! x = Some τ → ⟦ Γ ⟧* Δ vs ⊢ ∃ v, vs !! x = Some v ∧ ⟦ τ ⟧ Δ v.
Γ !! x = Some τ → ⟦ Γ ⟧* Δ vs ⊢ ∃ v, ⌜vs !! x = Some v⌝ ∧ ⟦ τ ⟧ Δ v.
Proof.
iIntros (?) "[Hlen HΓ]"; iDestruct "Hlen" as %Hlen.
destruct (lookup_lt_is_Some_2 vs x) as [v Hv].
......@@ -170,7 +166,7 @@ Section logrel.
Lemma interp_env_cons Δ Γ vs τ v :
⟦ τ :: Γ ⟧* Δ (v :: vs) ⊣⊢ ⟦ τ ⟧ Δ v ∗ ⟦ Γ ⟧* Δ vs.
Proof.
rewrite /interp_env /= (assoc _ (⟦ _ ⟧ _ _)) -(comm _ (_ = _)%I) -assoc.
rewrite /interp_env /= (assoc _ (⟦ _ ⟧ _ _)) -(comm _ ⌜(_ = _)⌝%I) -assoc.
by apply sep_proper; [apply pure_proper; omega|].
Qed.
......
F_mu_ref/logrel_binary.v
View file @ 70299030
......@@ -7,7 +7,7 @@ From iris.prelude Require Import tactics.
Import uPred.
(* HACK: move somewhere else *)
Ltac auto_equiv ::=
Ltac auto_equiv :=
(* Deal with "pointwise_relation" *)
repeat lazymatch goal with
| |- pointwise_relation _ _ _ _ => intros ?
......@@ -43,20 +43,20 @@ Section logrel.
Solve Obligations with solve_proper_alt.
Program Definition interp_unit : listC D -n> D := λne Δ ww,
(ww.1 = UnitV ∧ ww.2 = UnitV)%I.
(⌜ww.1 = UnitV⌝ ∧ ⌜ww.2 = UnitV⌝)%I.
Solve Obligations with solve_proper_alt.
Program Definition interp_prod
(interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ ww,
(∃ vv1 vv2, ww = (PairV (vv1.1) (vv2.1), PairV (vv1.2) (vv2.2)) ∧
(∃ vv1 vv2, ⌜ww = (PairV (vv1.1) (vv2.1), PairV (vv1.2) (vv2.2))⌝ ∧
interp1 Δ vv1 ∧ interp2 Δ vv2)%I.
Solve Obligations with solve_proper.
Solve Obligations with (preprocess_solve_proper; auto_equiv).
Program Definition interp_sum
(interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ ww,
((∃ vv, ww = (InjLV (vv.1), InjLV (vv.2)) ∧ interp1 Δ vv) ∨
(∃ vv, ww = (InjRV (vv.1), InjRV (vv.2)) ∧ interp2 Δ vv))%I.
Solve Obligations with solve_proper.
((∃ vv, ⌜ww = (InjLV (vv.1), InjLV (vv.2))⌝ ∧ interp1 Δ vv) ∨
(∃ vv, ⌜ww = (InjRV (vv.1), InjRV (vv.2))⌝ ∧ interp2 Δ vv))%I.
Solve Obligations with (preprocess_solve_proper; auto_equiv).
Program Definition interp_arrow
(interp1 interp2 : listC D -n> D) : listC D -n> D :=
......@@ -65,28 +65,24 @@ Section logrel.
interp_expr
interp2 Δ (App (of_val (ww.1)) (of_val (vv.1)),
App (of_val (ww.2)) (of_val (vv.2))))%I.
Solve Obligations with solve_proper.
Solve Obligations with (preprocess_solve_proper; auto_equiv).
Program Definition interp_forall
(interp : listC D -n> D) : listC D -n> D := λne Δ ww,
(□ ∀ τi,
(■ ∀ ww, PersistentP (τi ww)) →
⌜∀ ww, PersistentP (τi ww)⌝ →
interp_expr
interp (τi :: Δ) (TApp (of_val (ww.1)), TApp (of_val (ww.2))))%I.
Solve Obligations with solve_proper.
Solve Obligations with (preprocess_solve_proper; auto_equiv).
Program Definition interp_rec1
(interp : listC D -n> D) (Δ : listC D) (τi : D) : D := λne ww,
(□ ∃ vv, ww = (FoldV (vv.1), FoldV (vv.2)) ∧ ▷ interp (τi :: Δ) vv)%I.
Solve Obligations with solve_proper.
(□ ∃ vv, ⌜ww = (FoldV (vv.1), FoldV (vv.2))⌝ ∧ ▷ interp (τi :: Δ) vv)%I.
Solve Obligations with (preprocess_solve_proper; auto_equiv).
Global Instance interp_rec1_contractive
(interp : listC D -n> D) (Δ : listC D) : Contractive (interp_rec1 interp Δ).
Proof.
intros n τi1 τi2 Hτi ww; cbn.
apply always_ne, exist_ne; intros vv; apply and_ne; trivial.
apply later_contractive =>i Hi. by rewrite Hτi.
Qed.
Proof. by solve_contractive. Qed.
Program Definition interp_rec (interp : listC D -n> D) : listC D -n> D := λne Δ,
fixpoint (interp_rec1 interp Δ).
......@@ -96,13 +92,13 @@ Section logrel.
Program Definition interp_ref_inv (ll : loc * loc) : D -n> iProp Σ := λne τi,
(∃ vv, ll.1 ↦ vv.1 ∗ ll.2 ↦ₛ vv.2 ∗ τi vv)%I.
Solve Obligations with solve_proper.
Solve Obligations with (preprocess_solve_proper; auto_equiv).
Program Definition interp_ref
(interp : listC D -n> D) : listC D -n> D := λne Δ ww,
(∃ ll, ww = (LocV (ll.1), LocV (ll.2)) ∧
(∃ ll, ⌜ww = (LocV (ll.1), LocV (ll.2))⌝ ∧
inv (logN .@ ll) (interp_ref_inv ll (interp Δ)))%I.
Solve Obligations with solve_proper.
Solve Obligations with (preprocess_solve_proper; auto_equiv).
Fixpoint interp (τ : type) : listC D -n> D :=
match τ return _ with
......@@ -119,7 +115,7 @@ Section logrel.
Definition interp_env (Γ : list type)
(Δ : listC D) (vvs : list (val * val)) : iProp Σ :=
(length Γ = length vvs ∗ [∗] zip_with (λ τ, ⟦ τ ⟧ Δ) Γ vvs)%I.
(⌜length Γ = length vvs⌝ ∗ [∗] zip_with (λ τ, ⟦ τ ⟧ Δ) Γ vvs)%I.
Notation "⟦ Γ ⟧*" := (interp_env Γ).
Class env_PersistentP Δ :=
......@@ -147,7 +143,6 @@ Section logrel.
≡ ⟦ τ ⟧ (Δ1 ++ Δ2).
Proof.
revert Δ1 Π Δ2. induction τ=> Δ1 Π Δ2; simpl; auto.
- intros ww; simpl; properness; auto.
- intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
- intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
- unfold interp_expr.
......@@ -156,7 +151,7 @@ Section logrel.
properness; auto. apply (IHτ (_ :: _)).
- rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
{ by rewrite !lookup_app_l. }
rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia. done.
rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia.
- unfold interp_expr.
intros ww; simpl; properness; auto. by apply (IHτ (_ :: _)).
- intros ww; simpl; properness; auto. by apply IHτ.
......@@ -167,7 +162,6 @@ Section logrel.
≡ ⟦ τ.[upn (length Δ1) (τ' .: ids)] ⟧ (Δ1 ++ Δ2).
Proof.
revert Δ1 Δ2; induction τ=> Δ1 Δ2; simpl; auto.
- intros ww; simpl; properness; auto.
- intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
- intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
- unfold interp_expr.
......@@ -179,7 +173,7 @@ Section logrel.
rewrite !lookup_app_r; [|lia ..].
destruct (x - length Δ1) as [|n] eqn:?; simpl.
{ symmetry. asimpl. apply (interp_weaken [] Δ1 Δ2 τ'). }
rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia. done.
rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia.
- unfold interp_expr.
intros ww; simpl; properness; auto. apply (IHτ (_ :: _)).
- intros ww; simpl; properness; auto. by apply IHτ.
......@@ -188,11 +182,11 @@ Section logrel.
Lemma interp_subst Δ2 τ τ' : ⟦ τ ⟧ (⟦ τ' ⟧ Δ2 :: Δ2) ≡ ⟦ τ.[τ'/] ⟧ Δ2.
Proof. apply (interp_subst_up []). Qed.
Lemma interp_env_length Δ Γ vvs : ⟦ Γ ⟧* Δ vvs ⊢ length Γ = length vvs.
Lemma interp_env_length Δ Γ vvs : ⟦ Γ ⟧* Δ vvs ⊢ ⌜length Γ = length vvs⌝.
Proof. by iIntros "[% ?]". Qed.
Lemma interp_env_Some_l Δ Γ vvs x τ :
Γ !! x = Some τ → ⟦ Γ ⟧* Δ vvs ⊢ ∃ vv, vvs !! x = Some vv ∧ ⟦ τ ⟧ Δ vv.
Γ !! x = Some τ → ⟦ Γ ⟧* Δ vvs ⊢ ∃ vv, ⌜vvs !! x = Some vv⌝ ∧ ⟦ τ ⟧ Δ vv.
Proof.
iIntros (?) "[Hlen HΓ]"; iDestruct "Hlen" as %Hlen.
destruct (lookup_lt_is_Some_2 vvs x) as [v Hv].
......@@ -207,7 +201,7 @@ Section logrel.
Lemma interp_env_cons Δ Γ vvs τ vv :
⟦ τ :: Γ ⟧* Δ (vv :: vvs) ⊣⊢ ⟦ τ ⟧ Δ vv ∗ ⟦ Γ ⟧* Δ vvs.
Proof.
rewrite /interp_env /= (assoc _ (⟦ _ ⟧ _ _)) -(comm _ (_ = _)%I) -assoc.
rewrite /interp_env /= (assoc _ (⟦ _ ⟧ _ _)) -(comm _ ⌜_ = _⌝%I) -assoc.
by apply sep_proper; [apply pure_proper; omega|].
Qed.
......
F_mu_ref/rules.v
View file @ 70299030
This diff is collapsed.
F_mu_ref/rules_binary.v
View file @ 70299030
From iris.program_logic Require Import lifting.
From iris.algebra Require Import frac dec_agree gmap list.
From iris.algebra Require Import frac agree gmap list.
From iris.base_logic Require Import big_op auth.
From iris_logrel.F_mu_ref Require Export rules.
From iris.proofmode Require Import tactics.
......@@ -8,30 +8,34 @@ Import uPred.
Definition specN := nroot .@ "spec".
(** The CMRA for the heap of the specification. *)
Definition cfgUR := prodUR (optionUR (exclR exprC)) heapUR.
Definition cfgUR := prodUR (optionUR (exclR exprC)) (gen_heapUR loc val).
(** The CMRA for the thread pool. *)
Class cfgSG Σ :=
CFGSG { ctg_heapG :> heapG Σ; cfg_inG :> authG Σ cfgUR; cfg_name : gname }.
CFGSG {
cfg_inG :> inG Σ (authR cfgUR);
cfg_name : gname
}.
Definition spec_ctx `{cfgSG Σ} (ρ : cfg lang) : iProp Σ :=
(∃ e, ∃ σ, own cfg_name (● (Excl' e, to_gen_heap σ))
∗ ⌜rtc step ρ ([e],σ)⌝)%I.
Definition spec_inv `{cfgSG Σ} `{invG Σ} (ρ : cfg lang) : iProp Σ :=
inv specN (spec_ctx ρ).
Section definitionsS.
Context `{cfgSG Σ}.
Definition heapS_mapsto (l : loc) (q : Qp) (v: val) : iProp Σ :=
own cfg_name (◯ (∅, {[ l := (q, DecAgree v) ]})).
own cfg_name (◯ (∅, {[ l := (q, to_agree v) ]})).
Definition tpool_mapsto (e: expr) : iProp Σ :=
own cfg_name (◯ (Excl' e, ∅)).
Definition spec_inv (ρ : cfg lang) : iProp Σ :=
(∃ e σ, own cfg_name (● (Excl' e , to_heap σ)) ∗ ■ rtc step ρ ([e],σ))%I.
Definition spec_ctx (ρ : cfg lang) : iProp Σ :=
inv specN (spec_inv ρ).
Global Instance heapS_mapsto_timeless l q v : TimelessP (heapS_mapsto l q v).
Proof. apply _. Qed.
Global Instance spec_ctx_persistent ρ : PersistentP (spec_ctx ρ).
Proof. apply _. Qed.
End definitionsS.
Typeclasses Opaque heapS_mapsto tpool_mapsto.
......@@ -42,10 +46,10 @@ Notation "⤇ e" := (tpool_mapsto e) (at level 20) : uPred_scope.
Section cfg.
Context `{cfgSG Σ}.
Context `{!invG Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val → iProp Σ.
Implicit Types σ : state.
Implicit Types g : heapUR.
Implicit Types e : expr.
Implicit Types v : val.
......@@ -59,23 +63,39 @@ Section cfg.
Lemma step_pure E ρ K e e' :
(∀ σ, head_step e σ e' σ []) →
nclose specN ⊆ E →
spec_ctx ρ ∗ ⤇ fill K e ={E}=∗ ⤇ fill K e'.
spec_inv ρ ∗ ⤇ fill K e ={E}=∗ ⤇ fill K e'.
Proof.
iIntros (??) "[#Hspec Hj]". rewrite /spec_ctx /tpool_mapsto.
iInv specN as ">Hinv" "Hclose". iDestruct "Hinv" as (e2 σ) "[Hown %]".
iDestruct (own_valid_2 _ with "Hown Hj")
as %[[?%Excl_included%leibniz_equiv _]%prod_included ?]%auth_valid_discrete_2.
subst.
iIntros (??) "[Hinv Hj]". rewrite /spec_ctx /auth_inv /tpool_mapsto.
iInv specN as ">Hspec" "Hclose".
iDestruct "Hspec" as (e'' σ) "[Hown %]".
iDestruct (((@own_valid_2 Σ _ _ cfg_name (● (Excl' e'', to_gen_heap σ))) (◯ (Excl' (fill K e), ∅))) with "Hown Hj")
as %[[?%Excl_included%leibniz_equiv _]%prod_included Hvalid]%auth_valid_discrete_2.
subst.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, option_local_update,
(exclusive_local_update _ (Excl (fill K e'))). }
iFrame "Hj". iApply "Hclose". iNext. iExists (fill K e'), σ.
iFrame. iPureIntro. eapply rtc_r, step_insert_no_fork; eauto.
{ eapply auth_update, prod_local_update_1, option_local_update,
(exclusive_local_update _ (Excl (fill K e'))).
by inversion Hvalid.
}
iFrame "Hj".
iApply "Hclose". iNext. iExists (fill K e'). iExists σ.
iFrame.
iPureIntro. eapply rtc_r, step_insert_no_fork; eauto.
Qed.
Lemma step_fst E ρ K e1 v1 e2 v2 :
to_val e1 = Some v1 → to_val e2 = Some v2 →
nclose specN ⊆ E →
spec_inv ρ ∗ ⤇ fill K (Fst (Pair e1 e2)) ={E}=∗ ⤇ fill K e1.
Proof. intros H1 H2. apply step_pure => σ; econstructor; eauto. Qed.
Lemma step_snd E ρ K e1 v1 e2 v2 :
to_val e1 = Some v1 → to_val e2 = Some v2 → nclose specN ⊆ E →
spec_inv ρ ∗ ⤇ fill K (Snd (Pair e1 e2)) ={E}=∗ ⤇ fill K e2.
Proof. intros H1 H2; apply step_pure => σ; econstructor; eauto. Qed.
Lemma step_alloc E ρ K e v:
to_val e = Some v → nclose specN ⊆ E →
spec_ctx ρ ∗ ⤇ fill K (Alloc e) ={E}=∗ ∃ l, ⤇ fill K (Loc l) ∗ l ↦ₛ v.
spec_inv ρ ∗ ⤇ fill K (Alloc e) ={E}=∗ ∃ l, ⤇ fill K (Loc l) ∗ l ↦ₛ v.
Proof.
iIntros (??) "[#Hinv Hj]". rewrite /spec_ctx /tpool_mapsto.
iInv specN as ">Hinv'" "Hclose". iDestruct "Hinv'" as (e2 σ) "[Hown %]".
......@@ -88,17 +108,17 @@ Section cfg.
(exclusive_local_update _ (Excl (fill K (Loc l)))). }
iMod (own_update with "Hown") as "[Hown Hl]".
{ eapply auth_update_alloc, prod_local_update_2,
(alloc_singleton_local_update _ l (1%Qp,DecAgree v)); last done.
by apply lookup_to_heap_None. }
(alloc_singleton_local_update _ l (1%Qp,to_agree v)); last done.
by apply lookup_to_gen_heap_None. }
iExists l. rewrite /heapS_mapsto. iFrame "Hj Hl". iApply "Hclose". iNext.
iExists (fill K (Loc l)), (<[l:=v]>σ).
rewrite to_heap_insert; last eauto. iFrame. iPureIntro.
rewrite to_gen_heap_insert; last eauto. iFrame. iPureIntro.
eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
Qed.
Lemma step_load E ρ K l q v:
nclose specN ⊆ E →
spec_ctx ρ ∗ ⤇ fill K (Load (Loc l)) ∗ l ↦ₛ{q} v
spec_inv ρ ∗ ⤇ fill K (Load (Loc l)) ∗ l ↦ₛ{q} v
={E}=∗ ⤇ fill K (of_val v) ∗ l ↦ₛ{q} v.
Proof.
iIntros (?) "(#Hinv & Hj & Hl)".
......@@ -107,8 +127,8 @@ Section cfg.
iDestruct (own_valid_2 _ with "Hown Hj")
as %[[?%Excl_included%leibniz_equiv _]%prod_included ?]%auth_valid_discrete_2.
subst.
iDestruct (own_valid_2 _ with "Hown Hl")
as %[[_ ?%heap_singleton_included]%prod_included _]%auth_valid_discrete_2.
iDestruct (own_valid_2 with "Hown Hl")
as %[[_ ?%gen_heap_singleton_included]%prod_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, option_local_update,
(exclusive_local_update _ (Excl (fill K (of_val v)))). }
......@@ -120,7 +140,7 @@ Section cfg.
Lemma step_store E ρ K l v' e v:
to_val e = Some v → nclose specN ⊆ E →
spec_ctx ρ ∗ ⤇ fill K (Store (Loc l) e) ∗ l ↦ₛ v'
spec_inv ρ ∗ ⤇ fill K (Store (Loc l) e) ∗ l ↦ₛ v'
={E}=∗ ⤇ fill K Unit ∗ l ↦ₛ v.
Proof.
iIntros (??) "(#Hinv & Hj & Hl)".
......@@ -130,55 +150,45 @@ Section cfg.
as %[[?%Excl_included%leibniz_equiv _]%prod_included ?]%auth_valid_discrete_2.
subst.
iDestruct (own_valid_2 _ with "Hown Hl")
as %[[_ Hl%heap_singleton_included]%prod_included _]%auth_valid_discrete_2.
as %[[_ Hl%gen_heap_singleton_included]%prod_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, option_local_update,
(exclusive_local_update _ (Excl (fill K Unit))). }
iMod (own_update_2 with "Hown Hl") as "[Hown Hl]".
{ eapply auth_update, prod_local_update_2, singleton_local_update,
(exclusive_local_update _ (1%Qp, DecAgree v)); last done.
by rewrite /to_heap lookup_fmap Hl. }
(exclusive_local_update _ (1%Qp, to_agree v)); last done.
by rewrite /to_gen_heap lookup_fmap Hl. }
iFrame "Hj Hl". iApply "Hclose". iNext.
iExists (fill K Unit), (<[l:=v]>σ).
rewrite to_heap_insert; last eauto. iFrame. iPureIntro.
rewrite to_gen_heap_insert; last eauto. iFrame. iPureIntro.
eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
Qed.
Lemma step_lam E ρ K e1 e2 v :
to_val e2 = Some v → nclose specN ⊆ E →
spec_ctx ρ ∗ ⤇ fill K (App (Lam e1) e2)
spec_inv ρ ∗ ⤇ fill K (App (Lam e1) e2)
={E}=∗ ⤇ fill K (e1.[e2/]).
Proof. intros ?; apply step_pure => σ; econstructor; eauto. Qed.
Lemma step_tlam E ρ K e :
nclose specN ⊆ E →
spec_ctx ρ ∗ ⤇ fill K (TApp (TLam e)) ={E}=∗ ⤇ fill K e.
spec_inv ρ ∗ ⤇ fill K (TApp (TLam e)) ={E}=∗ ⤇ fill K e.
Proof. apply step_pure => σ; econstructor; eauto. Qed.
Lemma step_Fold E ρ K e v :
to_val e = Some v → nclose specN ⊆ E →
spec_ctx ρ ∗ ⤇ fill K (Unfold (Fold e)) ={E}=∗ ⤇ fill K e.
spec_inv ρ ∗ ⤇ fill K (Unfold (Fold e)) ={E}=∗ ⤇ fill K e.
Proof. intros H1; apply step_pure => σ; econstructor; eauto. Qed.
Lemma step_fst E ρ K e1 v1 e2 v2 :
to_val e1 = Some v1 → to_val e2 = Some v2 → nclose specN ⊆ E →
spec_ctx ρ ∗ ⤇ fill K (Fst (Pair e1 e2)) ={E}=∗ ⤇ fill K e1.
Proof. intros H1 H2; apply step_pure => σ; econstructor; eauto. Qed.
Lemma step_snd E ρ K e1 v1 e2 v2 :
to_val e1 = Some v1 → to_val e2 = Some v2 → nclose specN ⊆ E →
spec_ctx ρ ∗ ⤇ fill K (Snd (Pair e1 e2)) ={E}=∗ ⤇ fill K e2.
Proof. intros H1 H2; apply step_pure => σ; econstructor; eauto. Qed.
Lemma step_case_inl E ρ K e0 v0 e1 e2 :
to_val e0 = Some v0 → nclose specN ⊆ E →
spec_ctx ρ ∗ ⤇ fill K (Case (InjL e0) e1 e2)
spec_inv ρ ∗ ⤇ fill K (Case (InjL e0) e1 e2)
={E}=∗ ⤇ fill K (e1.[e0/]).
Proof. intros H1; apply step_pure => σ; econstructor; eauto. Qed.
Lemma step_case_inr E ρ K e0 v0 e1 e2 :
to_val e0 = Some v0 → nclose specN ⊆ E →
spec_ctx ρ ∗ ⤇ fill K (Case (InjR e0) e1 e2)
spec_inv ρ ∗ ⤇ fill K (Case (InjR e0) e1 e2)
={E}=∗ ⤇ fill K (e2.[e0/]).
Proof. intros H1; apply step_pure => σ; econstructor; eauto. Qed.
......
F_mu_ref/soundness.v
View file @ 70299030
......@@ -3,18 +3,28 @@ From iris.proofmode Require Import tactics.
From iris.program_logic Require Import adequacy.
From iris.base_logic Require Import auth.
Theorem soundness Σ `{irisPreG lang Σ, HAG: authG Σ heapUR} e τ e' thp σ σ' :
Class heapPreG Σ := HeapPreG {
heap_preG_iris :> invPreG Σ;
heap_preG_heap :> gen_heapPreG loc val Σ
}.
Theorem soundness Σ `{heapPreG Σ} e τ e' thp σ σ' :
(∀ `{heapG Σ}, log_typed [] e τ) →
rtc step ([e], σ) (thp, σ') → e' ∈ thp →
is_Some (to_val e') ∨ reducible e' σ'.
Proof.
intros Hlog ??. cut (adequate e σ (λ _, True)); first (intros [_ ?]; eauto).
eapply (wp_adequacy Σ); iIntros (?) "Hσ". rewrite -(empty_env_subst e).
iMod (auth_alloc to_heap ownP heapN _ σ with "[Hσ]") as (γ) "[??]".
- auto using to_heap_valid.
- by iNext.
- iApply wp_wand_l; iSplitR; [|iApply (Hlog (HeapG _ _ _ γ))]; eauto.
iSplit. by rewrite /heap_ctx. iApply (@interp_env_nil _ (HeapG _ _ _ γ)).
eapply (wp_adequacy Σ _); eauto.
iIntros (Hinv).
iMod (own_alloc (● to_gen_heap σ)) as (γ) "Hh".
- apply (auth_auth_valid _ (to_gen_heap_valid _ _ σ)).
- iModIntro. iExists (λ σ, own γ (● to_gen_heap σ)); iFrame.
set (HΣ := IrisG _ _ Hinv (λ σ, own γ (● to_gen_heap σ))%I).
iApply wp_wand_r.