### 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!
{"ft_lang_label":"__label__en","ft_lang_prob":0.5369212,"math_prob":0.9409672,"size":382,"snap":"2020-10-2020-16","text_gpt3_token_len":138,"char_repetition_ratio":0.105820104,"word_repetition_ratio":0.0,"special_character_ratio":0.32984293,"punctuation_ratio":0.1369863,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.98418456,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2020-02-20T13:51:59Z\",\"WARC-Record-ID\":\"<urn:uuid:ce0186e6-35bf-465d-b1b2-539bf01c22a6>\",\"Content-Length\":\"972738\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:1ba7e749-c16a-40f9-b1ae-891d4d4d545e>\",\"WARC-Concurrent-To\":\"<urn:uuid:f5277146-6f07-4feb-be5c-992589a261de>\",\"WARC-IP-Address\":\"139.19.205.205\",\"WARC-Target-URI\":\"https://gitlab.mpi-sws.org/dfrumin/logrel-conc/commit/775d1b06118bec6b3e9752ce2573e18855a4e8d6\",\"WARC-Payload-Digest\":\"sha1:7TF65QLYVM646T6VYKPJBOVFYJTSSPD2\",\"WARC-Block-Digest\":\"sha1:IJIJMSTHZJAJH55LA6NXZXADDYVQ6CGY\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2020/CC-MAIN-2020-10/CC-MAIN-2020-10_segments_1581875144979.91_warc_CC-MAIN-20200220131529-20200220161529-00440.warc.gz\"}"}