Commit b1515733 authored by Amin Timany's avatar Amin Timany

Add binary logical relations for F_mu_ref

parent e724ddf8
From iris_logrel.F_mu_ref Require Export fundamental_binary.
Inductive ctx_item :=
| CTX_Lam
| CTX_AppL (e2 : expr)
| CTX_AppR (e1 : expr)
(* Products *)
| CTX_PairL (e2 : expr)
| CTX_PairR (e1 : expr)
| CTX_Fst
| CTX_Snd
(* Sums *)
| CTX_InjL
| CTX_InjR
| CTX_CaseL (e1 : expr) (e2 : expr)
| CTX_CaseM (e0 : expr) (e2 : expr)
| CTX_CaseR (e0 : expr) (e1 : expr)
(* Recursive Types *)
| CTX_Fold
| CTX_Unfold
(* Polymorphic Types *)
| CTX_TLam
| CTX_TApp
(* Reference Types *)
| CTX_Alloc
| CTX_Load
| CTX_StoreL (e2 : expr)
| CTX_StoreR (e1 : expr).
Fixpoint fill_ctx_item (ctx : ctx_item) (e : expr) : expr :=
match ctx with
| CTX_Lam => Lam e
| CTX_AppL e2 => App e e2
| CTX_AppR e1 => App e1 e
| CTX_PairL e2 => Pair e e2
| CTX_PairR e1 => Pair e1 e
| CTX_Fst => Fst e
| CTX_Snd => Snd e
| CTX_InjL => InjL e
| CTX_InjR => InjR e
| CTX_CaseL e1 e2 => Case e e1 e2
| CTX_CaseM e0 e2 => Case e0 e e2
| CTX_CaseR e0 e1 => Case e0 e1 e
| CTX_Fold => Fold e
| CTX_Unfold => Unfold e
| CTX_TLam => TLam e
| CTX_TApp => TApp e
| CTX_Alloc => Alloc e
| CTX_Load => Load e
| CTX_StoreL e2 => Store e e2
| CTX_StoreR e1 => Store e1 e
end.
Definition ctx := list ctx_item.
Definition fill_ctx (K : ctx) (e : expr) : expr := foldr fill_ctx_item e K.
(** typed ctx *)
Inductive typed_ctx_item :
ctx_item list type type list type type Prop :=
| TP_CTX_Lam Γ τ τ' :
typed_ctx_item CTX_Lam (τ :: Γ) τ' Γ (TArrow τ τ')
| TP_CTX_AppL Γ e2 τ τ' :
typed Γ e2 τ
typed_ctx_item (CTX_AppL e2) Γ (TArrow τ τ') Γ τ'
| TP_CTX_AppR Γ e1 τ τ' :
typed Γ e1 (TArrow τ τ')
typed_ctx_item (CTX_AppR e1) Γ τ Γ τ'
| TP_CTX_PairL Γ e2 τ τ' :
typed Γ e2 τ'
typed_ctx_item (CTX_PairL e2) Γ τ Γ (TProd τ τ')
| TP_CTX_PairR Γ e1 τ τ' :
typed Γ e1 τ
typed_ctx_item (CTX_PairR e1) Γ τ' Γ (TProd τ τ')
| TP_CTX_Fst Γ τ τ' :
typed_ctx_item CTX_Fst Γ (TProd τ τ') Γ τ
| TP_CTX_Snd Γ τ τ' :
typed_ctx_item CTX_Snd Γ (TProd τ τ') Γ τ'
| TP_CTX_InjL Γ τ τ' :
typed_ctx_item CTX_InjL Γ τ Γ (TSum τ τ')
| TP_CTX_InjR Γ τ τ' :
typed_ctx_item CTX_InjR Γ τ' Γ (TSum τ τ')
| TP_CTX_CaseL Γ e1 e2 τ1 τ2 τ' :
typed (τ1 :: Γ) e1 τ' typed (τ2 :: Γ) e2 τ'
typed_ctx_item (CTX_CaseL e1 e2) Γ (TSum τ1 τ2) Γ τ'
| TP_CTX_CaseM Γ e0 e2 τ1 τ2 τ' :
typed Γ e0 (TSum τ1 τ2) typed (τ2 :: Γ) e2 τ'
typed_ctx_item (CTX_CaseM e0 e2) (τ1 :: Γ) τ' Γ τ'
| TP_CTX_CaseR Γ e0 e1 τ1 τ2 τ' :
typed Γ e0 (TSum τ1 τ2) typed (τ1 :: Γ) e1 τ'
typed_ctx_item (CTX_CaseR e0 e1) (τ2 :: Γ) τ' Γ τ'
| TP_CTX_Fold Γ τ :
typed_ctx_item CTX_Fold Γ τ.[(TRec τ)/] Γ (TRec τ)
| TP_CTX_Unfold Γ τ :
typed_ctx_item CTX_Unfold Γ (TRec τ) Γ τ.[(TRec τ)/]
| TP_CTX_TLam Γ τ :
typed_ctx_item CTX_TLam (subst (ren (+1)) <$> Γ) τ Γ (TForall τ)
| TP_CTX_TApp Γ τ τ' :
typed_ctx_item CTX_TApp Γ (TForall τ) Γ τ.[τ'/]
| TPCTX_Alloc Γ τ :
typed_ctx_item CTX_Alloc Γ τ Γ (Tref τ)
| TP_CTX_Load Γ τ :
typed_ctx_item CTX_Load Γ (Tref τ) Γ τ
| TP_CTX_StoreL Γ e2 τ :
typed Γ e2 τ typed_ctx_item (CTX_StoreL e2) Γ (Tref τ) Γ TUnit
| TP_CTX_StoreR Γ e1 τ :
typed Γ e1 (Tref τ)
typed_ctx_item (CTX_StoreR e1) Γ τ Γ TUnit.
Lemma typed_ctx_item_typed k Γ τ Γ' τ' e :
typed Γ e τ typed_ctx_item k Γ τ Γ' τ'
typed Γ' (fill_ctx_item k e) τ'.
Proof. induction 2; simpl; eauto using typed. Qed.
Inductive typed_ctx: ctx list type type list type type Prop :=
| TPCTX_nil Γ τ :
typed_ctx nil Γ τ Γ τ
| TPCTX_cons Γ1 τ1 Γ2 τ2 Γ3 τ3 k K :
typed_ctx_item k Γ2 τ2 Γ3 τ3
typed_ctx K Γ1 τ1 Γ2 τ2
typed_ctx (k :: K) Γ1 τ1 Γ3 τ3.
Lemma typed_ctx_typed K Γ τ Γ' τ' e :
typed Γ e τ typed_ctx K Γ τ Γ' τ' typed Γ' (fill_ctx K e) τ'.
Proof. induction 2; simpl; eauto using typed_ctx_item_typed. Qed.
Lemma typed_ctx_n_closed K Γ τ Γ' τ' e :
( f, e.[upn (length Γ) f] = e) typed_ctx K Γ τ Γ' τ'
f, (fill_ctx K e).[upn (length Γ') f] = (fill_ctx K e).
Proof.
intros H1 H2; induction H2; simpl; auto.
induction H => f; asimpl; simpl in *;
repeat match goal with H : _ |- _ => rewrite fmap_length in H end;
try f_equal;
eauto using typed_n_closed;
try match goal with H : _ |- _ => eapply (typed_n_closed _ _ _ H) end.
Qed.
Definition ctx_refines (Γ : list type)
(e e' : expr) (τ : type) := K thp σ v,
typed_ctx K Γ τ [] TUnit
rtc step ([fill_ctx K e], ) (of_val v :: thp, σ)
thp' σ' v', rtc step ([fill_ctx K e'], ) (of_val v' :: thp', σ').
Notation "Γ ⊨ e '≤ctx≤' e' : τ" :=
(ctx_refines Γ e e' τ) (at level 74, e, e', τ at next level).
Ltac fold_interp :=
match goal with
| |- context [ interp_expr (interp_arrow (interp ?A) (interp ?A'))
?B (?C, ?D) ] =>
change (interp_expr (interp_arrow (interp A) (interp A')) B (C, D)) with
(interp_expr (interp (TArrow A A')) B (C, D))
| |- context [ interp_expr (interp_prod (interp ?A) (interp ?A'))
?B (?C, ?D) ] =>
change (interp_expr (interp_prod (interp A) (interp A')) B (C, D)) with
(interp_expr (interp (TProd A A')) B (C, D))
| |- context [ interp_expr (interp_prod (interp ?A) (interp ?A'))
?B (?C, ?D) ] =>
change (interp_expr (interp_prod (interp A) (interp A')) B (C, D)) with
(interp_expr (interp (TProd A A')) B (C, D))
| |- context [ interp_expr (interp_sum (interp ?A) (interp ?A'))
?B (?C, ?D) ] =>
change (interp_expr (interp_sum (interp A) (interp A')) B (C, D)) with
(interp_expr (interp (TSum A A')) B (C, D))
| |- context [ interp_expr (interp_rec (interp ?A)) ?B (?C, ?D) ] =>
change (interp_expr (interp_rec (interp A)) B (C, D)) with
(interp_expr (interp (TRec A)) B (C, D))
| |- context [ interp_expr (interp_forall (interp ?A))
?B (?C, ?D) ] =>
change (interp_expr (interp_forall (interp A)) B (C, D)) with
(interp_expr (interp (TForall A)) B (C, D))
| |- context [ interp_expr (interp_ref (interp ?A))
?B (?C, ?D) ] =>
change (interp_expr (interp_ref (interp A)) B (C, D)) with
(interp_expr (interp (Tref A)) B (C, D))
end.
Section bin_log_related_under_typed_ctx.
Context `{heapG Σ, cfgSG Σ}.
Lemma bin_log_related_under_typed_ctx Γ e e' τ Γ' τ' K :
( f, e.[upn (length Γ) f] = e)
( f, e'.[upn (length Γ) f] = e')
typed_ctx K Γ τ Γ' τ'
Γ e log e' : τ Γ' fill_ctx K e log fill_ctx K e' : τ'.
Proof.
revert Γ τ Γ' τ' e e'.
induction K as [|k K]=> Γ τ Γ' τ' e e' H1 H2; simpl.
- inversion_clear 1; trivial.
- inversion_clear 1 as [|? ? ? ? ? ? ? ? Hx1 Hx2]. intros H3.
specialize (IHK _ _ _ _ e e' H1 H2 Hx2 H3).
inversion Hx1; subst; simpl; try fold_interp.
+ eapply bin_log_related_lam; eauto;
match goal with
H : _ |- _ => eapply (typed_ctx_n_closed _ _ _ _ _ _ _ H)
end.
+ eapply bin_log_related_app; eauto using binary_fundamental.
+ eapply bin_log_related_app; eauto using binary_fundamental.
+ eapply bin_log_related_pair; eauto using binary_fundamental.
+ eapply bin_log_related_pair; eauto using binary_fundamental.
+ eapply bin_log_related_fst; eauto.
+ eapply bin_log_related_snd; eauto.
+ eapply bin_log_related_injl; eauto.
+ eapply bin_log_related_injr; eauto.
+ match goal with
H : typed_ctx_item _ _ _ _ _ |- _ => inversion H; subst
end.
eapply bin_log_related_case;
eauto using binary_fundamental;
match goal with
H : _ |- _ => eapply (typed_n_closed _ _ _ H)
end.
+ match goal with
H : typed_ctx_item _ _ _ _ _ |- _ => inversion H; subst
end.
eapply bin_log_related_case;
eauto using binary_fundamental;
try match goal with
H : _ |- _ => eapply (typed_n_closed _ _ _ H)
end;
match goal with
H : _ |- _ => eapply (typed_ctx_n_closed _ _ _ _ _ _ _ H)
end.
+ match goal with
H : typed_ctx_item _ _ _ _ _ |- _ => inversion H; subst
end.
eapply bin_log_related_case;
eauto using binary_fundamental;
try match goal with
H : _ |- _ => eapply (typed_n_closed _ _ _ H)
end;
match goal with
H : _ |- _ => eapply (typed_ctx_n_closed _ _ _ _ _ _ _ H)
end.
+ eapply bin_log_related_fold; eauto.
+ eapply bin_log_related_unfold; eauto.
+ eapply bin_log_related_tlam; eauto with typeclass_instances.
+ eapply bin_log_related_tapp; eauto.
+ eapply bin_log_related_alloc; eauto.
+ eapply bin_log_related_load; eauto.
+ eapply bin_log_related_store; eauto using binary_fundamental.
+ eapply bin_log_related_store; eauto using binary_fundamental.
Unshelve. all: trivial.
Qed.
End bin_log_related_under_typed_ctx.
This diff is collapsed.
......@@ -124,8 +124,6 @@ Module lang.
| 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 list expr Prop :=
......@@ -247,4 +245,4 @@ Ltac solve_atomic :=
rewrite ?to_of_val; eapply mk_is_Some; fast_done.
Hint Extern 0 (language.atomic _) => solve_atomic.
Hint Extern 0 (language.atomic _) => solve_atomic : typeclass_instances.
Hint Extern 0 (language.atomic _) => solve_atomic : atomic.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.base_logic Require Export big_op invariants.
From iris_logrel.F_mu_ref Require Export rules_binary typing.
From iris.algebra Require Import list.
From iris.prelude Require Import tactics.
Import uPred.
(* HACK: move somewhere else *)
Ltac auto_equiv ::=
(* Deal with "pointwise_relation" *)
repeat lazymatch goal with
| |- pointwise_relation _ _ _ _ => intros ?
end;
(* Normalize away equalities. *)
repeat match goal with
| H : _ {_} _ |- _ => apply (timeless_iff _ _) in H
| _ => progress simplify_eq
end;
(* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *)
try (f_equiv; fast_done || auto_equiv).
Definition logN : namespace := nroot .@ "logN".
(** interp : is a unary logical relation. *)
Section logrel.
Context `{heapG Σ, cfgSG Σ}.
Notation D := (prodC valC valC -n> iProp Σ).
Implicit Types τi : D.
Implicit Types Δ : listC D.
Implicit Types interp : listC D D.
Definition interp_expr (τi : listC D -n> D) (Δ : listC D)
(ee : expr * expr) : iProp Σ := ( K,
fill K (ee.2)
WP ee.1 {{ v, v', fill K (of_val v') τi Δ (v, v') }})%I.
Global Instance interp_expr_ne n :
Proper (dist n ==> dist n ==> (=) ==> dist n) interp_expr.
Proof. solve_proper. Qed.
Program Definition ctx_lookup (x : var) : listC D -n> D := λne Δ,
from_option id (cconst True)%I (Δ !! x).
Solve Obligations with solve_proper_alt.
Program Definition interp_unit : listC D -n> D := λne Δ ww,
(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))
interp1 Δ vv1 interp2 Δ vv2)%I.
Solve Obligations with solve_proper.
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.
Program Definition interp_arrow
(interp1 interp2 : listC D -n> D) : listC D -n> D :=
λne Δ ww,
( vv, interp1 Δ vv
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.
Program Definition interp_forall
(interp : listC D -n> D) : listC D -n> D := λne Δ ww,
( τi,
( ww, PersistentP (τi ww))
interp_expr
interp (τi :: Δ) (TApp (of_val (ww.1)), TApp (of_val (ww.2))))%I.
Solve Obligations with solve_proper.
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.
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.
Program Definition interp_rec (interp : listC D -n> D) : listC D -n> D := λne Δ,
fixpoint (interp_rec1 interp Δ).
Next Obligation.
intros interp n Δ1 Δ2 HΔ; apply fixpoint_ne => τi ww. solve_proper.
Qed.
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.
Program Definition interp_ref
(interp : listC D -n> D) : listC D -n> D := λne Δ ww,
( ll, ww = (LocV (ll.1), LocV (ll.2))
inv (logN .@ ll) (interp_ref_inv ll (interp Δ)))%I.
Solve Obligations with solve_proper.
Fixpoint interp (τ : type) : listC D -n> D :=
match τ return _ with
| TUnit => interp_unit
| TProd τ1 τ2 => interp_prod (interp τ1) (interp τ2)
| TSum τ1 τ2 => interp_sum (interp τ1) (interp τ2)
| TArrow τ1 τ2 => interp_arrow (interp τ1) (interp τ2)
| TVar x => ctx_lookup x
| TForall τ' => interp_forall (interp τ')
| TRec τ' => interp_rec (interp τ')
| Tref τ' => interp_ref (interp τ')
end.
Notation "⟦ τ ⟧" := (interp τ).
Definition interp_env (Γ : list type)
(Δ : listC D) (vvs : list (val * val)) : iProp Σ :=
(length Γ = length vvs [] zip_with (λ τ, τ Δ) Γ vvs)%I.
Notation "⟦ Γ ⟧*" := (interp_env Γ).
Class env_PersistentP Δ :=
ctx_persistentP : Forall (λ τi, vv, PersistentP (τi vv)) Δ.
Global Instance ctx_persistent_nil : env_PersistentP [].
Proof. by constructor. Qed.
Global Instance ctx_persistent_cons τi Δ :
( vv, PersistentP (τi vv)) env_PersistentP Δ env_PersistentP (τi :: Δ).
Proof. by constructor. Qed.
Global Instance ctx_persistent_lookup Δ x vv :
env_PersistentP Δ PersistentP (ctx_lookup x Δ vv).
Proof. intros HΔ; revert x; induction HΔ=>-[|?] /=; apply _. Qed.
Global Instance interp_persistent τ Δ vv :
env_PersistentP Δ PersistentP ( τ Δ vv).
Proof.
revert vv Δ; induction τ=> vv Δ HΔ; simpl; try apply _.
rewrite /PersistentP /interp_rec fixpoint_unfold /interp_rec1 /=.
by apply always_intro'.
Qed.
Global Instance interp_env_persistent Γ Δ vvs :
env_PersistentP Δ PersistentP ( Γ * Δ vvs) := _.
Lemma interp_weaken Δ1 Π Δ2 τ :
τ.[upn (length Δ1) (ren (+ length Π))] (Δ1 ++ Π ++ Δ2)
τ (Δ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.
intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
- apply fixpoint_proper=> τi ww /=.
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.
- unfold interp_expr.
intros ww; simpl; properness; auto. by apply (IHτ (_ :: _)).
- intros ww; simpl; properness; auto. by apply IHτ.
Qed.
Lemma interp_subst_up Δ1 Δ2 τ τ' :
τ (Δ1 ++ interp τ' Δ2 :: Δ2)
τ.[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.
intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
- apply fixpoint_proper=> τi ww /=.
properness; auto. apply (IHτ (_ :: _)).
- rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
{ by rewrite !lookup_app_l. }
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.
- unfold interp_expr.
intros ww; simpl; properness; auto. apply (IHτ (_ :: _)).
- intros ww; simpl; properness; auto. by apply IHτ.
Qed.
Lemma interp_subst Δ2 τ τ' : τ ( τ' Δ2 :: Δ2) τ.[τ'/] Δ2.
Proof. apply (interp_subst_up []). Qed.
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.
Proof.
iIntros (?) "[Hlen HΓ]"; iDestruct "Hlen" as %Hlen.
destruct (lookup_lt_is_Some_2 vvs x) as [v Hv].
{ by rewrite -Hlen; apply lookup_lt_Some with τ. }
iExists v; iSplit. done. iApply (big_sep_elem_of with "HΓ").
apply elem_of_list_lookup_2 with x.
rewrite lookup_zip_with; by simplify_option_eq.
Qed.
Lemma interp_env_nil Δ : True [] * Δ [].
Proof. iIntros ""; iSplit; auto. Qed.
Lemma interp_env_cons Δ Γ vvs τ vv :
τ :: Γ * Δ (vv :: vvs) ⊣⊢ τ Δ vv Γ * Δ vvs.
Proof.
rewrite /interp_env /= (assoc _ ( _ _ _)) -(comm _ (_ = _)%I) -assoc.
by apply sep_proper; [apply pure_proper; omega|].
Qed.
Lemma interp_env_ren Δ (Γ : list type) vvs τi :
subst (ren (+1)) <$> Γ * (τi :: Δ) vvs ⊣⊢ Γ * Δ vvs.
Proof.
apply sep_proper; [apply pure_proper; by rewrite fmap_length|].
revert Δ vvs τi; induction Γ=> Δ [|v vs] τi; csimpl; auto.
apply sep_proper; auto. apply (interp_weaken [] [τi] Δ).
Qed.
End logrel.
Typeclasses Opaque interp_env.
Notation "⟦ τ ⟧" := (interp τ).
Notation "⟦ τ ⟧ₑ" := (interp_expr (interp τ)).
Notation "⟦ Γ ⟧*" := (interp_env Γ).
From iris.program_logic Require Import lifting.
From iris.algebra Require Import frac dec_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.
Import uPred.
Definition specN := nroot .@ "spec".
(** The CMRA for the heap of the specification. *)
Definition cfgUR := prodUR (optionUR (exclR exprC)) heapUR.
(** The CMRA for the thread pool. *)
Class cfgSG Σ :=
CFGSG { ctg_heapG :> heapG Σ; cfg_inG :> authG Σ cfgUR; cfg_name : gname }.
Section definitionsS.
Context `{cfgSG Σ}.
Definition heapS_mapsto (l : loc) (q : Qp) (v: val) : iProp Σ :=
own cfg_name ( (, {[ l := (q, DecAgree 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.
Notation "l ↦ₛ{ q } v" := (heapS_mapsto l q v)
(at level 20, q at level 50, format "l ↦ₛ{ q } v") : uPred_scope.
Notation "l ↦ₛ v" := (heapS_mapsto l 1 v) (at level 20) : uPred_scope.
Notation "⤇ e" := (tpool_mapsto e) (at level 20) : uPred_scope.
Section cfg.
Context `{cfgSG Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val iProp Σ.
Implicit Types σ : state.
Implicit Types g : heapUR.
Implicit Types e : expr.
Implicit Types v : val.
(** Conversion to tpools and back *)
Lemma step_insert_no_fork K e σ e' σ' :
head_step e σ e' σ' [] step ([fill K e], σ) ([fill K e'], σ').
Proof. intros Hst. eapply (step_atomic _ _ _ _ _ _ [] [] []); eauto.
by apply: Ectx_step'.
Qed.
Lemma step_pure E ρ K e e' :
( σ, head_step e σ e' σ [])
nclose specN E
spec_ctx ρ 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.
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.
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.
Proof.
iIntros (??) "[#Hinv Hj]". rewrite /spec_ctx /tpool_mapsto.
iInv specN as ">Hinv'" "Hclose". iDestruct "Hinv'" as (e2 σ) "[Hown %]".
destruct (exist_fresh (dom (gset positive) σ)) as [l Hl%not_elem_of_dom].
iDestruct (own_valid_2 _ with "[$Hown $Hj]")
as %[[?%Excl_included%leibniz_equiv _]%prod_included ?]%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 (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. }
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.
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
={E}= fill K (of_val v) l ↦ₛ{q} v.
Proof.
iIntros (?) "(#Hinv & Hj & Hl)".
rewrite /spec_ctx /tpool_mapsto /heapS_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.
iDestruct (own_valid_2 _ with "[$Hown $Hl]")
as %[[_ ?%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)))). }
iFrame "Hj Hl". iApply "Hclose". iNext.
iExists (fill K (of_val v)), σ.
iFrame. iPureIntro.
eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
Qed.
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'
={E}= fill K Unit l ↦ₛ v.
Proof.
iIntros (??) "(#Hinv & Hj & Hl)".
rewrite /spec_ctx /tpool_mapsto /heapS_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.
iDestruct (own_valid_2 _ with "[$Hown $Hl]")
as %[[_ Hl%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. }
iFrame "Hj Hl". iApply "Hclose". iNext.
iExists (fill K Unit), (<[l:=v]>σ).
rewrite to_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)
={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.
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.
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)
={E}= fill K (e1.[e0/]).