Commit 775d1b06 authored by Dan Frumin's avatar Dan Frumin

Changes to the formulation of a relational interpretation for F_mu_ref_conc

A new formulation allows for doing more work inside HOSL.

Γ ⊨ e ≤log≤ e' : τ <=>
∀ Δ vvs ρ,
  spec_ctx ρ -∗
  □ ⟦ Γ ⟧* Δ vvs -∗
  ⟦ τ ⟧ₑ Δ (e.[env_subst (vvs.*1)], e'.[env_subst (vvs.*2)])
parent 926a3657
From iris_logrel.F_mu_ref_conc Require Export fundamental_binary.
From iris.proofmode Require Import tactics classes.
Inductive ctx_item :=
| CTX_Rec
......@@ -226,79 +227,114 @@ Ltac fold_interp :=
Section bin_log_related_under_typed_ctx.
Context `{heapIG Σ, cfgSG Σ}.
Ltac fundamental :=
lazymatch goal with
| [ H : _ ⊢ₜ ?e : _ |- (_ ?Γ ?e log ?e : _)] =>
let Z := iFresh in
iPoseProof (binary_fundamental _ e _) as Z; [apply H | iFrame Z]
end.
Ltac solve_closed_typed :=
lazymatch goal with
| [ H : ?Γ ⊢ₜ ?e : _ |- f, ?e.[_] = ?e ]
=> eapply (typed_n_closed Γ _ e H)
end.
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.
(Γ 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_clear 1; trivial. iIntros "#H"; eauto.
- inversion_clear 1 as [|? ? ? ? ? ? ? ? Hx1 Hx2].
iIntros "#Hrel".
specialize (IHK _ _ _ _ e e' H1 H2 Hx2).
inversion Hx1; subst; simpl; try fold_interp.
+ eapply bin_log_related_rec; 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.
+ iApply (bin_log_related_rec with "[]"); auto.
eapply (typed_ctx_n_closed _ _ _ (_::_::Γ') _ _ H1); eauto.
eapply (typed_ctx_n_closed _ _ _ (_::_::Γ') _ _ H2); eauto.
iAlways. iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_app with "[]").
iApply (IHK with "[Hrel]"); auto.
fundamental.
+ iApply (bin_log_related_app with "[]"); try fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_pair with "[]"); try fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_pair with "[]"); try fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply bin_log_related_fst.
iApply (IHK with "[Hrel]"); auto.
+ iApply bin_log_related_snd.
iApply (IHK with "[Hrel]"); auto.
+ iApply bin_log_related_injl.
iApply (IHK with "[Hrel]"); auto.
+ iApply bin_log_related_injr.
iApply (IHK with "[Hrel]"); auto.
+ inversion Hx2; subst.
* iApply (bin_log_related_case with "[] []"); try fundamental.
all: try solve_closed_typed.
iApply (IHK with "[Hrel]"); auto.
* iApply (bin_log_related_case with "[] []"); try fundamental.
all: try solve_closed_typed.
iApply (IHK with "[Hrel]"); auto.
+ 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.
iApply (bin_log_related_case with "[] []"); try fundamental.
eapply (typed_ctx_n_closed _ _ _ (_::Γ') _ _ _); eauto.
solve_closed_typed.
eapply (typed_ctx_n_closed _ _ _ (_::Γ') _ _ _); eauto.
solve_closed_typed.
iApply (IHK with "[Hrel]"); auto.
Unshelve. all: trivial.
+ 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_if; eauto using typed_ctx_typed, binary_fundamental.
+ eapply bin_log_related_if; eauto using typed_ctx_typed, binary_fundamental.
+ eapply bin_log_related_if; eauto using typed_ctx_typed, binary_fundamental.
+ eapply bin_log_related_nat_binop;
eauto using typed_ctx_typed, binary_fundamental.
+ eapply bin_log_related_nat_binop;
eauto using typed_ctx_typed, binary_fundamental.
+ 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_fork; 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.
+ eapply bin_log_related_CAS; eauto using binary_fundamental.
+ eapply bin_log_related_CAS; eauto using binary_fundamental.
+ eapply bin_log_related_CAS; eauto using binary_fundamental.
iApply (bin_log_related_case with "[] []"); try fundamental.
all: try solve_closed_typed.
eapply (typed_ctx_n_closed _ _ _ (_::Γ') _ _ _); eauto.
eapply (typed_ctx_n_closed _ _ _ (_::Γ') _ _ _); eauto.
iApply (IHK with "[Hrel]"); auto.
Unshelve. all: trivial.
Qed.
+ iApply (bin_log_related_if with "[] []"); try fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_if with "[] []"); try fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_if with "[] []"); try fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_nat_binop with "[]"); try fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_nat_binop with "[]"); try fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_fold with "[]"); try fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_unfold with "[]"); try fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_tlam with "[]"); try fundamental.
iAlways. iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_tapp with "[]"); try fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_fork with "[]"); try fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_alloc with "[]"); try fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_load with "[]"); try fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_store with "[]"); try fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_store with "[]"); try fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_CAS with "[] []"); try fundamental.
assumption.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_CAS with "[] []"); try fundamental.
assumption.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_CAS with "[] []"); try fundamental.
assumption.
iApply (IHK with "[Hrel]"); auto.
Qed.
End bin_log_related_under_typed_ctx.
......@@ -245,7 +245,7 @@ Section CG_Counter.
Lemma FG_CG_counter_refinement :
[] FG_counter log CG_counter : TProd (TArrow TUnit TUnit) (TArrow TUnit TNat).
Proof.
iIntros (Δ [|??] ρ ?) "#(Hspec & HΓ)"; iIntros (j K) "Hj"; last first.
iIntros (Δ [|??] ρ) "#Hspec #HΓ"; iIntros (j K) "Hj"; last first.
{ iDestruct (interp_env_length with "HΓ") as %[=]. }
iClear "HΓ". cbn -[FG_counter CG_counter].
rewrite ?empty_env_subst /CG_counter /FG_counter.
......
......@@ -46,21 +46,9 @@ Section Stack_refinement.
iApply (wp_load with "Hst"). iNext. iIntros "Hst".
tp_rec j; auto using to_of_val.
tp_normalise j.
rewrite CG_iter_subst CG_snap_subst. asimpl.
replace (match @up_close namespace coPset nclose stackN return coPset with
| @exist _ _ t2 _ =>
@exist coPset_raw (fun t : coPset_raw => Is_true (coPset_wf t))
match coPset_opp_raw t2 return coPset_raw with
| coPLeaf b =>
match b return coPset_raw with
| true => coPLeaf true
| false => coPLeaf false
end
| coPNode b l0 r => coPNode b l0 r
end
(coPset_intersection_wf (coPLeaf true)
(coPset_opp_raw t2) I (coPset_opp_wf t2))
end) with ( stackN) by reflexivity.
rewrite CG_iter_subst CG_snap_subst.
Opaque coPset_difference.
asimpl.
replace (CG_iter (of_val f2)) with (of_val (CG_iterV (of_val f2))) by (rewrite CG_iter_of_val; done).
tp_bind j (App (CG_snap _ _) ())%E.
tp_apply j steps_CG_snap with "Hst' Hl" as "[Hst' Hl]".
......@@ -102,7 +90,7 @@ Section Stack_refinement.
tp_apply j steps_CG_iter.
rewrite CG_iter_subst.
tp_bind j (App (of_val f2) _).
iSpecialize ("Hff" $! (y1, y2) with "Hy").
iSpecialize ("Hff" $! (y1, y2) with "[Hy]"); first by iFrame.
iSpecialize ("Hff" $! j (K ++ _) with "Hj"). simpl.
iApply (wp_wand with "Hff").
iIntros (v). iDestruct 1 as (v2) "[Hj [% %]]".
......@@ -280,11 +268,11 @@ Section Stack_refinement.
(TArrow (TArrow (TVar 0) TUnit) TUnit)).
Proof.
(* executing the preambles *)
iIntros (Δ [|??] ρ ?) "#[Hspec HΓ]"; iIntros (j K) "Hj"; last first.
iIntros (Δ [|??] ρ) "#Hspec #HΓ"; iIntros (j K) "Hj"; last first.
{ iDestruct (interp_env_length with "HΓ") as %[=]. }
iClear "HΓ". cbn -[FG_stack CG_stack].
rewrite ?empty_env_subst /CG_stack /FG_stack.
iApply wp_value; eauto.
iApply wp_value; eauto.
iExists (Λ: _)%V; iFrame "Hj".
fold (interp (TProd (TProd
(TArrow (TVar 0) TUnit)
......@@ -342,27 +330,18 @@ Section Stack_refinement.
- iExists (_, _), (_, _); iSplit; eauto. iSplit.
+ simpl.
(* TODO: fold (interp (...)) does not work here *)
replace ( ( vv : prodC valC valC, τi vv
interp_expr interp_unit (τi :: Δ)
((of_val
((RecV
((rec: if: CAS #stk (Var 1)
(Fold (ref InjR (Var 3, Var 1))) then
() else (Var 2) (Var 3))%E
(! #stk)%E), CG_locked_pushV (#stk')%E (#l')%E).1))
(of_val (vv.1)),
(of_val
((RecV
((rec: if: CAS #stk (Var 1)
(Fold (ref InjR (Var 3, Var 1))) then
() else (Var 2) (Var 3))%E
(! #stk)%E), CG_locked_pushV (#stk')%E (#l')%E).2))
change ( ( vv : prodC valC valC,
τi vv
interp_expr interp_unit (τi :: Δ)
((rec: (rec: if: CAS #stk (Var 1)
(Fold (ref InjR (Var 3, Var 1)))
then () else (Var 2) (Var 3))
! #stk)%E (of_val (vv.1)),
(of_val (CG_locked_pushV (#stk')%E (#l')%E))
(of_val (vv.2)))))%I
with
(interp (TArrow (TVar 0) TUnit) (τi :: Δ)
with (interp (TArrow (TVar 0) TUnit) (τi :: Δ)
((FG_pushV (#stk)%E)%V,
(CG_locked_pushV (#stk')%E (#l')%E))); last first.
{ simpl. unlock. (* TODO: WTF???? *) auto. }
(CG_locked_pushV (#stk')%E (#l')%E))).
iApply (FG_CG_push_refinement with "Hspec Hinv").
+ simpl.
iApply (FG_CG_pop_refinement with "Hspec Hinv").
......
This diff is collapsed.
......@@ -75,7 +75,7 @@ Module lang.
| FoldV (v : val)
| PackV (v : val)
| LocV (l : loc).
(* Notation for bool and nat *)
Notation "'#♭v' b" := (BoolV b) (at level 20).
Notation "'#nv' n" := (NatV n) (at level 20).
......@@ -125,6 +125,69 @@ Module lang.
| _ => None
end.
Fixpoint subst_val (s : var -> expr) t :=
match t with
| RecV e => RecV e.[upn 2 s]
| TLamV e => TLamV e.[s]
| UnitV => UnitV
| NatV n => NatV n
| BoolV b => BoolV b
| PairV v1 v2 => PairV (subst_val s v1) (subst_val s v2)
| InjLV v => InjLV (subst_val s v)
| InjRV v => InjRV (subst_val s v)
| FoldV v => FoldV (subst_val s v)
| PackV v => PackV (subst_val s v)
| LocV l => LocV l
end.
Instance Subst_val : Subst val := fun s t =>
subst_val (fun x => of_val (s x)) t.
Lemma of_val_subst (e : expr) (v : val) (s : var -> expr) :
of_val (subst_val s v) = (of_val v).[s].
Proof.
generalize dependent s.
induction v; simpl; eauto; intro s;
repeat match goal with
| [ H : forall s, of_val (subst_val s _) = (of_val _).[s] |- _] =>
specialize (H s); rewrite H
end; eauto.
Qed.
Lemma to_val_subst (e : expr) (v : val) (s : var -> expr) :
to_val e = Some v ->
to_val (e.[s]) = Some (subst_val s v).
Proof.
generalize dependent v. generalize dependent s.
induction e; intuition; try by inversion H; asimpl.
- simpl. simpl in H.
remember (to_val e1) as O1.
remember (to_val e2) as O2.
destruct (O1).
destruct (O2). simpl in H.
all: try inversion H.
rewrite (IHe1 s v0); auto. rewrite (IHe2 s v1); auto.
- simpl. simpl in H.
specialize (IHe s).
destruct (to_val e); try by inversion H.
simpl in H. inversion H. subst.
rewrite (IHe v0); auto.
- simpl. simpl in H.
specialize (IHe s).
destruct (to_val e); try by inversion H.
simpl in H. inversion H. subst.
rewrite (IHe v0); auto.
- simpl. simpl in H.
specialize (IHe s).
destruct (to_val e); try by inversion H.
simpl in H. inversion H. subst.
rewrite (IHe v0); auto.
- simpl. simpl in H.
specialize (IHe s).
destruct (to_val e); try by inversion H.
simpl in H. inversion H. subst.
rewrite (IHe v0); auto.
Qed.
(** Evaluation contexts *)
Inductive ectx_item :=
| AppLCtx (e2 : expr)
......@@ -180,6 +243,43 @@ Module lang.
| CasRCtx v0 v1 => CAS (of_val v0) (of_val v1) e
end.
Fixpoint subst_ctx_item σ (K : ectx_item) :=
match K with
| AppLCtx e2 => AppLCtx e2.[σ]
| AppRCtx v1 => AppRCtx (subst_val σ v1)
| TAppCtx => TAppCtx
| PairLCtx e2 => PairLCtx e2.[σ]
| PairRCtx v1 => PairRCtx (subst_val σ v1)
| BinOpLCtx op e2 => BinOpLCtx op e2.[σ]
| BinOpRCtx op v1 => BinOpRCtx op (subst_val σ v1)
| FstCtx => FstCtx
| SndCtx => SndCtx
| InjLCtx => InjLCtx
| InjRCtx => InjRCtx
| CaseCtx e1 e2 => CaseCtx e1.[up σ] e2.[up σ]
| IfCtx e1 e2 => IfCtx e1.[σ] e2.[σ]
| FoldCtx => FoldCtx
| UnfoldCtx => UnfoldCtx
| PackCtx => PackCtx
| UnpackLCtx e2 => UnpackLCtx e2.[up σ]
| AllocCtx => AllocCtx
| LoadCtx => LoadCtx
| StoreLCtx e2 => StoreLCtx e2.[σ]
| StoreRCtx v1 => StoreRCtx (subst_val σ v1)
| CasLCtx e1 e2 => CasLCtx e1.[σ] e2.[σ]
| CasMCtx v0 e2 => CasMCtx (subst_val σ v0) e2.[σ]
| CasRCtx v0 v1 => CasRCtx (subst_val σ v0) (subst_val σ v1)
end.
Definition subst_ctx σ (K : list ectx_item) := map (subst_ctx_item σ) K.
Lemma fill_item_subst σ Ki e :
(fill_item Ki e).[σ] = fill_item (subst_ctx_item σ Ki) e.[σ].
Proof.
induction Ki; eauto; asimpl;
rewrite ?of_val_subst; eauto.
Qed.
Definition state : Type := gmap loc val.
Inductive head_step : expr state expr state list expr Prop :=
......@@ -303,6 +403,16 @@ Solve Obligations with eauto using lang.to_of_val, lang.of_to_val,
Canonical Structure lang := ectx_lang (lang.expr).
Lemma fill_subst σ K e :
(fill K e).[σ] = fill (lang.subst_ctx σ K) e.[σ].
Proof.
generalize dependent e. generalize dependent σ.
induction K; eauto.
intros. simpl.
rewrite ?lang.fill_item_subst.
rewrite IHK. done.
Qed.
Export lang.
Definition is_atomic (e : expr) : Prop :=
......
......@@ -34,14 +34,14 @@ Section logrel.
Definition interp_expr (τi : listC D -n> D) (Δ : listC D)
(ee : expr * expr) : iProp Σ := ( j K,
j fill K (ee.2)
j fill K (ee.2) -
WP ee.1 {{ v, v', j 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).
Program Definition ctx_lookup (x : var) : listC D -n> D := λne Δ ww,
( from_option id (cconst True)%I (Δ !! x) ww)%I.
Solve Obligations with solve_proper_alt.
Program Definition interp_unit : listC D -n> D := λne Δ ww,
......@@ -136,25 +136,15 @@ Section logrel.
(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).
PersistentP ( τ Δ vv).
Proof.
revert vv Δ; induction τ=> vv Δ HΔ; simpl; try apply _.
revert vv Δ; induction τ=> vv Δ; 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) := _.
PersistentP ( Γ * Δ vvs) := _.
Lemma interp_weaken Δ1 Π Δ2 τ :
τ.[upn (length Δ1) (ren (+ length Π))] (Δ1 ++ Π ++ Δ2)
......@@ -167,9 +157,10 @@ Section logrel.
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.
- intros ww; simpl; properness; auto.
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.
rewrite !lookup_app_r; [|lia ..]. do 4 f_equiv. lia.
- unfold interp_expr.
intros ww; simpl; properness; auto. by apply (IHτ (_ :: _)).
- intros ww; simpl; properness; auto. by apply (IHτ (_ :: _)).
......@@ -187,12 +178,13 @@ Section logrel.
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.
- intros ww; simpl.
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.
{ symmetry. rewrite always_always. asimpl. apply (interp_weaken [] Δ1 Δ2 τ'). }
rewrite !lookup_app_r; [|lia ..]. do 4 f_equiv. lia.
- unfold interp_expr.
intros ww; simpl; properness; auto. apply (IHτ (_ :: _)).
- intros ww; simpl; properness; auto. apply (IHτ (_ :: _)).
......@@ -234,9 +226,9 @@ Section logrel.
Qed.
Lemma interp_EqType_agree τ v v' Δ :
env_PersistentP Δ EqType τ interp τ Δ (v, v') v = v'⌝.
EqType τ interp τ Δ (v, v') v = v'⌝.
Proof.
intros ? Hτ; revert v v'; induction Hτ; iIntros (v v') "#H1 /=".
intros Hτ; revert v v'; induction Hτ; iIntros (v v') "#H1 /=".
- by iDestruct "H1" as "[% %]"; subst.
- by iDestruct "H1" as (n) "[% %]"; subst.
- by iDestruct "H1" as (b) "[% %]"; subst.
......
......@@ -27,8 +27,9 @@ Proof.
iExists (λ σ, own γ ( to_gen_heap σ)); iFrame.
iApply wp_fupd. iApply wp_wand_r.
iSplitL.
iPoseProof ((Hlog _ _ [] [] ([e'], )) with "[$Hcfg]") as "Hrel".
{ iApply (@logrel_binary.interp_env_nil Σ HeapΣ). }
iPoseProof (Hlog _ _) as "Hrel".
iSpecialize ("Hrel" $! [] [] with "* [$Hcfg] []").
{ iAlways. iApply logrel_binary.interp_env_nil. }
simpl.
rewrite empty_env_subst empty_env_subst. iApply ("Hrel" $! 0 []).
{ rewrite tpool_mapsto_eq /tpool_mapsto_def. asimpl. iFrame. }
......@@ -51,5 +52,6 @@ Lemma binary_soundness Σ `{heapPreIG Σ, inG Σ (authR cfgUR)}
Γ e ctx e' : τ.
Proof.
intros He He' Hlog K thp σ v ?. eapply (basic_soundness Σ _)=> ??.
eapply (bin_log_related_under_typed_ctx _ _ _ _ []); eauto.
iApply (bin_log_related_under_typed_ctx _ _ _ _ []); eauto.
iPoseProof (Hlog _ _) as "Hrel". auto.
Qed.
(** TODO: move this somewhere else!!! *)
From iris.program_logic Require Import ectx_language.
From iris.program_logic Require Import ectxi_language.
From iris.program_logic Require Import weakestpre.
From iris.proofmode Require Import tactics classes.
Section wp.
Context {expr val ectx state} {Λ : EctxiLanguage expr val ectx state}.
Definition lang : language := (ectx_lang expr).
Context `{irisG lang Σ}.
Implicit Types P : iProp Σ.
Implicit Types Φ : val iProp Σ.
Implicit Types v : val.
Implicit Types e : expr.
(* Inverse bind lemma *)
Lemma wp_bind_inv K e Φ :
WP fill K e {{ Φ }} WP e {{ v, WP fill K (of_val v) {{ Φ }} }}.
Proof.
iIntros "H". iLöb as "IH" forall (e Φ). rewrite wp_unfold /wp_pre.
iDestruct "H" as "[Hv|[% H]]".
{ iDestruct "Hv" as (v) "[Hev Hv]".
iDestruct "Hev" as %Hval.
assert (is_Some (to_val (fill K e))) by (eexists; eauto).
destruct (fill_val _ e H) as [v' Hval'].
iApply wp_value; simpl; auto. eassumption.
iApply wp_fupd. iApply wp_value; simpl; eauto using to_of_val.
simpl in *.
change (ectxi_language.of_val v')
with (of_val v').
rewrite (of_to_val e v'); eauto. }
remember (to_val e) as eval.
destruct eval.
- iApply wp_value. symmetry. eauto.
replace e with (of_val v) in H; last first.
{ by rewrite (of_to_val e). }
rewrite wp_unfold /wp_pre; iRight; iSplit; eauto.
iIntros (σ1) "Hσ". iMod ("H" $! _ with "Hσ") as "[% H]".
iModIntro; iSplit.
replace (of_val v) with e; last first.
{ by rewrite (of_to_val e). }
{ iPureIntro. unfold reducible in *. naive_solver eauto using fill_step. }
iNext; iIntros (e2 σ2 efs Hstep).
replace (of_val v) with e in Hstep; last first.
{ by rewrite (of_to_val e). }
iSpecialize ("H" with "* []").
{ iPureIntro. apply Hstep. }
iFrame.
- rewrite wp_unfold /wp_pre. iRight; iSplit; eauto using fill_not_val.
iIntros (σ1) "Hσ". iMod ("H" $! _ with "Hσ") as "[% H]".
assert (LanguageCtx (ectx_lang expr) (fill K)).
{ change (fill K) with
(ectx_language.fill K). apply ectx_lang_ctx. }
iModIntro; iSplit.
{ iPureIntro. unfold reducible in *.
destruct H0 as [e' [σ' [efs H']]].
symmetry in Heqeval.
destruct (fill_step_inv e σ1 e' σ' efs Heqeval H').
naive_solver eauto. }
iNext; iIntros (e2 σ2 efs Hstep).
iSpecialize ("H" with "* []").
{ iPureIntro. apply fill_step. eauto. }
iMod "H" as "[$ [H $]]".
by iApply "IH".
Qed.
End wp.
-Q . iris_logrel
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
prelude/base.v
stlc/lang.v
stlc/typing.v
......@@ -30,6 +31,7 @@ F_mu_ref_conc/logrel_unary.v
F_mu_ref_conc/fundamental_unary.v
F_mu_ref_conc/rules_binary.v
F_mu_ref_conc/logrel_binary.v
F_mu_ref_conc/weakestpre.v
F_mu_ref_conc/fundamental_binary.v
F_mu_ref_conc/soundness_unary.v
F_mu_ref_conc/context_refinement.v
......
......@@ -27,6 +27,7 @@ Ltac properness :=
| |- (_ _)%I (_ _)%I => apply and_proper
| |- (_ _)%I (_ _)%I => apply or_proper
| |- (_ _)%I (_ _)%I => apply impl_proper
| |- (_ - _)%I (_ - _)%I => apply wand_proper
| |- (WP _ {{ _ }})%I (WP _ {{ _ }})%I => apply wp_proper =>?
| |- ( _)%I ( _)%I => apply later_proper
| |- ( _)%I ( _)%I => apply always_proper
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment