diff --git a/README.md b/README.md index 819d1b8..20a96ee 100644 --- a/README.md +++ b/README.md @@ -1,10 +1,11 @@ # Guarded Interaction Trees This is the Coq formalization of guarded interaction trees, associated examples and case studies. +Read the [GITrees POPL paper](https://iris-project.org/pdfs/2024-popl-gitrees.pdf) describing our work. ## Installation instructions -To install the formalization you will need the Iris, std++, and Equations packages. +To install the formalization you will need Iris and std++ libraries. The dependencies can be easily installed using [Opam](https://opam.ocaml.org/) with the following commands: ``` @@ -24,16 +25,20 @@ All the code lives in the `theories` folder. Below is the quick guide to the code structure. - `gitree/` -- contains the core definitions related to guarded interaction trees -- `input_lang/` -- formalization of the language with io, the soundness and adequacy -- `input_lang_callcc/` -- formalization of the language with io, throw and call/cc, the soundness and adequacy -- `affine_lang/` -- formalization of the affine language, type safety of the language interoperability -- `examples/` -- some other smaller examples -- `lang_generic.v` -- generic facts about languages with binders and their interpretations, shared by `input_lang` and `affine_lang` -- `lang_generic_sem.v` -- generic facts about languages with a different representation of binders and their interpretations, used for `input_lang_callcc` +- `lib/` -- derived combinators for gitrees +- `examples/input_lang/` -- formalization of the language with io, the soundness and adequacy +- `examples/input_lang_callcc/` -- formalization of the language with io, throw and call/cc, the soundness and adequacy +- `examples/affine_lang/` -- formalization of the affine language, type safety of the language interoperability +- `effects/` -- concrete effects, their interpretaions, and logics - `prelude.v` -- some stuff that is missing from Iris +- `lang_generic.v` -- generic facts about languages with binders and their interpretations, shared by `input_lang` and `affine_lang` +- `vendor/Binding/` -- the functorial syntax library used for ### References from the paper to the code +The version of the formalization that corresponds to the paper can be found under the [tag `popl24`](https://github.com/logsem/gitrees/releases/tag/popl24). +Below we describe the correspondence per-section. + - **Section 3** + Definition of guarded interaction trees, constructors, the recursion principle, and the destructors are in `gitree/core.v` diff --git a/_CoqProject b/_CoqProject index 4d1ffbf..ee4ddbc 100644 --- a/_CoqProject +++ b/_CoqProject @@ -31,6 +31,7 @@ theories/program_logic.v theories/examples/input_lang_delim/lang.v theories/examples/input_lang_delim/interp.v +theories/examples/input_lang_delim/example.v theories/examples/input_lang_callcc/lang.v theories/examples/input_lang_callcc/interp.v @@ -53,4 +54,4 @@ theories/lib/while.v theories/lib/factorial.v theories/lib/iter.v -theories/utils/finite_sets.v \ No newline at end of file +theories/utils/finite_sets.v diff --git a/coq-gitrees.opam b/coq-gitrees.opam index 8a0f678..3056b98 100644 --- a/coq-gitrees.opam +++ b/coq-gitrees.opam @@ -2,14 +2,13 @@ opam-version: "2.0" name: "coq-gitrees" synopsis: "Guarded Interaction Trees" version: "dev" -maintainer: "..." -authors: "..." +maintainer: "Logsem" +authors: "Logsem" license: "BSD" build: [make "-j%{jobs}%"] install: [make "install"] remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/gitrees"] depends: [ - "coq-equations" { (= "1.3+8.17") } "coq-iris" { (= "4.1.0") } "coq-iris-heap-lang" { (= "4.1.0") } "coq-stdpp" { (= "1.9.0") } diff --git a/theories/effects/store.v b/theories/effects/store.v index 7027cba..a7deb17 100644 --- a/theories/effects/store.v +++ b/theories/effects/store.v @@ -224,10 +224,7 @@ Section wp. Proof. iIntros (Hee) "#Hcxt H". unfold READ. simpl. - match goal with - | |- context G [Vis ?a ?b ?c] => assert (c ≡ idfun ◎ (subEff_outs ^-1)) as -> - end; first solve_proper. - iApply wp_subreify_ctx_indep'. + iApply wp_subreify_ctx_indep'. simpl. iInv (nroot.@"storeE") as (σ) "[>Hlc [Hs Hh]]" "Hcl". iApply (fupd_mask_weaken E1). { set_solver. } @@ -249,16 +246,9 @@ Section wp. iFrame "Hs". repeat iSplit. - assert ((option_bind _ _ (λ x, Some (x, σ)) (σ !! l)) ≡ - (option_bind _ _ (λ x, Some (x, σ)) (Some (Next β')))) as H. - + f_equiv. - * solve_proper. - * by rewrite Hx Hb'. - + simpl in H. - rewrite <-H. - unfold mbind. - simpl. - iPureIntro. - f_equiv; last done. + (option_bind _ _ (λ x, Some (x, σ)) (Some (Next β')))) as <-. + { rewrite Hx /= ; solve_proper. } + simpl. iPureIntro. by f_equiv. - iPureIntro. apply ofe_iso_21. - iNext. iIntros "Hlc Hs". iMod ("Hback" with "Hp") as "Hback". @@ -290,8 +280,7 @@ Section wp. WP@{rs} WRITE l β @ s {{ Φ }}. Proof. iIntros (Hee) "#Hcxt H". - unfold READ. simpl. - iApply wp_subreify_ctx_indep'. + iApply wp_subreify_ctx_indep'. simpl. iInv (nroot.@"storeE") as (σ) "[>Hlc [Hs Hh]]" "Hcl". iApply (fupd_mask_weaken E1). { set_solver. } @@ -337,7 +326,7 @@ Section wp. WP@{rs} ALLOC α k @ s {{ Φ }}. Proof. iIntros "Hh H". - iApply wp_subreify_ctx_indep'. + iApply wp_subreify_ctx_indep'. simpl. iInv (nroot.@"storeE") as (σ) "[>Hlc [Hs Hh]]" "Hcl". iApply (lc_fupd_elim_later with "Hlc"). iModIntro. @@ -365,8 +354,7 @@ Section wp. WP@{rs} DEALLOC l @ s {{ Φ }}. Proof. iIntros (Hee) "#Hcxt H". - unfold DEALLOC. simpl. - iApply wp_subreify_ctx_indep'. + iApply wp_subreify_ctx_indep'. simpl. iInv (nroot.@"storeE") as (σ) "[>Hlc [Hs Hh]]" "Hcl". iApply (fupd_mask_weaken E1). { set_solver. } @@ -404,105 +392,6 @@ Section wp. iModIntro. done. Qed. - (** * The logical relation TODO *) - (* Definition N := nroot.@"heh". *) - (* Definition logrel_expr V (α : IT) : iProp := *) - (* (heap_ctx -∗ WP@{rs} α {{ V }})%I. *) - - (* Context `{!SubOfe natO R, !Inhabited R}. *) - - (* Definition logrel_nat (βv : ITV) : iProp := *) - (* (∃ n : nat, βv ≡ RetV n)%I. *) - (* Definition logrel_arr V1 V2 (βv : ITV) : iProp := *) - (* (∃ f, IT_of_V βv ≡ Fun f ∧ □ ∀ αv, V1 αv -∗ *) - (* logrel_expr V2 (APP' (Fun f) (IT_of_V αv)))%I. *) - (* Definition logrel_ref V (l : loc) : iProp := *) - (* (inv (N.@l) (∃ βv, pointsto l (IT_of_V βv) ∗ V βv))%I. *) - - (* Lemma logrel_alloc V V2 (αv :ITV) (k : locO -n> IT) `{!forall v, Persistent (V v)} *) - (* `{NonExpansive V2} : *) - (* V αv -∗ *) - (* (∀ l, logrel_ref V l -∗ logrel_expr V2 (k l)) -∗ *) - (* logrel_expr V2 (ALLOC (IT_of_V αv) k). *) - (* Proof. *) - (* iIntros "#HV H". *) - (* iIntros "#Hh". *) - (* iApply (wp_alloc with "Hh"). *) - (* iNext. iNext. *) - (* iIntros (l) "Hl". *) - (* iMod (inv_alloc (N.@l) _ (∃ βv, pointsto l (IT_of_V βv) ∗ V βv)%I with "[Hl]") *) - (* as "#Hinv". *) - (* { eauto with iFrame. } *) - (* iSpecialize ("H" with "Hinv"). *) - (* by iApply "H". *) - (* Qed. *) - - (* Opaque Ret. (*TODO*) *) - (* Lemma logrel_write V αv l `{!forall v, Persistent (V v)} : *) - (* logrel_ref V l -∗ *) - (* V αv -∗ *) - (* logrel_expr logrel_nat (WRITE l (IT_of_V αv)). *) - (* Proof. *) - (* iIntros "#Hl #Hav #Hctx". *) - (* iApply wp_subreify'. *) - (* iInv (nroot.@"storeE") as (σ) "[>Hlc [Hs Hh]]" "Hcl1". *) - (* iInv (N.@l) as "HH" "Hcl2". *) - (* iDestruct "HH" as (βv) "[Hbv #HV]". *) - (* iApply (lc_fupd_elim_later with "Hlc"). *) - (* iNext. *) - (* iAssert (⌜is_Some (σ !! l)⌝)%I as "%Hdom". *) - (* { iApply (istate_loc_dom with "Hh Hbv"). } *) - (* iExists σ, (),(<[l:=Next (IT_of_V αv)]>σ),(Ret ()). *) - (* iFrame "Hs". *) - (* iSimpl. repeat iSplit; [ done | done | ]. *) - (* iNext. iIntros "Hlc Hs". *) - (* iMod (istate_write _ _ (IT_of_V αv) with "Hh Hbv") as "[Hh Hlav]". *) - (* iMod ("Hcl2" with "[Hlav]") as "_". *) - (* { iNext. iExists _; by iFrame. } *) - (* iMod ("Hcl1" with "[Hlc Hh Hs]") as "_". *) - (* { iNext. iExists _; by iFrame. } *) - (* iModIntro. *) - (* iApply wp_val. iModIntro. *) - (* iExists (). unfold RetV. done. *) - (* Qed. *) - - (* Lemma logrel_read V l `{!forall v, Persistent (V v)} : *) - (* logrel_ref V l -∗ *) - (* logrel_expr V (READ l). *) - (* Proof. *) - (* iIntros "#Hr #Hctx". *) - (* iApply wp_subreify'. *) - (* iInv (nroot.@"storeE") as (σ) "[>Hlc [Hs Hh]]" "Hcl1". *) - (* iInv (N.@l) as "HH" "Hcl2". *) - (* iDestruct "HH" as (βv) "[Hbv #HV]". *) - (* iAssert (▷ (σ !! l ≡ Some (Next (IT_of_V βv))))%I as "#Hlookup". *) - (* { iNext. iApply (istate_read with "Hh Hbv"). } *) - (* iAssert (▷ ⌜is_Some (σ !! l)⌝)%I as "#Hdom". *) - (* { iNext. iApply (istate_loc_dom with "Hh Hbv"). } *) - (* iDestruct "Hdom" as ">%Hdom". *) - (* destruct Hdom as [x Hx]. *) - (* destruct (Next_uninj x) as [β' Hb']. *) - (* iAssert (▷ ▷ (β' ≡ IT_of_V βv))%I as "#Hbv'". *) - (* { iNext. rewrite Hx. rewrite option_equivI. *) - (* rewrite Hb'. by iNext. } *) - (* iClear "Hlookup". *) - (* iApply (lc_fupd_elim_later with "Hlc"). *) - (* iNext. iSimpl. *) - (* iExists σ,(Next β'),σ,β'. iFrame "Hs". *) - (* repeat iSplit. *) - (* { iPureIntro. rewrite Hx/= Hb'. done. } *) - (* { rewrite ofe_iso_21//. } *) - (* iNext. iIntros "Hlc Hs". *) - (* iMod ("Hcl2" with "[Hbv]") as "_". *) - (* { iNext. eauto with iFrame. } *) - (* iMod ("Hcl1" with "[Hlc Hh Hs]") as "_". *) - (* { iNext. eauto with iFrame. } *) - (* iModIntro. *) - (* iRewrite "Hbv'". *) - (* iApply wp_val. *) - (* iModIntro. done. *) - (* Qed. *) - End wp. Arguments heapG {_} rs R {_} Σ. diff --git a/theories/examples/affine_lang/lang.v b/theories/examples/affine_lang/lang.v index 628d2e9..14cdcb9 100644 --- a/theories/examples/affine_lang/lang.v +++ b/theories/examples/affine_lang/lang.v @@ -3,6 +3,8 @@ From gitrees.examples.input_lang Require Import lang interp. From gitrees.effects Require Import store. From gitrees.lib Require Import pairs. +Require Import Binding.Resolver Binding.Lib Binding.Set Binding.Auto Binding.Env. + (* for namespace sake *) Module io_lang. Definition state := input_lang.lang.state. @@ -14,8 +16,6 @@ Module io_lang. input_lang.interp.interp_expr rs e ı_scope. End io_lang. -Require Import Binding.Resolver Binding.Lib Binding.Set Binding.Auto Binding.Env. - Inductive ty := tBool | tInt | tUnit | tArr (τ1 τ2 : ty) | tPair (τ1 τ2 : ty) @@ -42,7 +42,7 @@ Inductive expr : ∀ (S : Set), Type := | Alloc {S : Set} : expr S → expr S | Replace {S1 S2 : Set} : expr S1 → expr S2 → expr (sum S1 S2) | Dealloc {S : Set} : expr S → expr S -| EEmbed {S : Set} {τ1 τ1'} : io_lang.expr Empty_set → ty_conv τ1 τ1' → expr S +| EEmbed {S : Set} {τ1 τ1'} : io_lang.expr ∅ → ty_conv τ1 τ1' → expr S . Section affine. diff --git a/theories/examples/affine_lang/logrel1.v b/theories/examples/affine_lang/logrel1.v index d26e888..c9c38b5 100644 --- a/theories/examples/affine_lang/logrel1.v +++ b/theories/examples/affine_lang/logrel1.v @@ -1,11 +1,11 @@ (** Unary (Kripke) logical relation for the affine lang *) -Require Import iris.algebra.gmap. From gitrees Require Export gitree program_logic greifiers. From gitrees.examples.affine_lang Require Import lang. From gitrees.effects Require Import store. From gitrees.lib Require Import pairs. From gitrees.utils Require Import finite_sets. + Inductive typed : forall {S : Set}, (S → ty) → expr S → ty → Prop := (** functions *) | typed_Var {S : Set} (Ω : S → ty) (v : S) : @@ -525,15 +525,15 @@ Lemma logrel1_adequacy cr Σ R `{!Cofe R, !SubOfe natO R, !SubOfe unitO R, !SubO (α : interp_scope ∅ -n> IT (gReifiers_ops rs) R) (β : IT (gReifiers_ops rs) R) st st' k : (∀ `{H1 : !invGS Σ} `{H2: !stateG rs R Σ} `{H3: !heapG rs R Σ}, (£ cr ⊢ valid1 rs notStuck (λne _: unitO, True)%I □ α τ)%I) → - ssteps (gReifiers_sReifier NotCtxDep rs) (α ı_scope) st β st' k → - (∃ β1 st1, sstep (gReifiers_sReifier NotCtxDep rs) β st' β1 st1) + ssteps (gReifiers_sReifier rs) (α ı_scope) st β st' k → + (∃ β1 st1, sstep (gReifiers_sReifier rs) β st' β1 st1) ∨ (∃ βv, (IT_of_V βv ≡ β)%stdpp). Proof. intros Hlog Hst. destruct (IT_to_V β) as [βv|] eqn:Hb. { right. exists βv. apply IT_of_to_V'. rewrite Hb; eauto. } left. - cut ((∃ β1 st1, sstep (gReifiers_sReifier NotCtxDep rs) β st' β1 st1) + cut ((∃ β1 st1, sstep (gReifiers_sReifier rs) β st' β1 st1) ∨ (∃ e, (β ≡ Err e)%stdpp ∧ notStuck e)). { intros [?|He]; first done. destruct He as [? [? []]]. } @@ -549,9 +549,9 @@ Proof. iMod (new_heapG rs σ) as (H3) "H". iAssert (has_substate σ ∗ has_substate ios)%I with "[Hst]" as "[Hs Hio]". { unfold has_substate, has_full_state. - assert (of_state NotCtxDep rs (IT (gReifiers_ops rs) _) st ≡ - of_idx NotCtxDep rs (IT (gReifiers_ops rs) _) sR_idx (sR_state σ) - ⋅ of_idx NotCtxDep rs (IT (gReifiers_ops rs) _) sR_idx (sR_state ios))%stdpp as ->; last first. + assert (of_state rs (IT (gReifiers_ops rs) _) st ≡ + of_idx rs (IT (gReifiers_ops rs) _) sR_idx (sR_state σ) + ⋅ of_idx rs (IT (gReifiers_ops rs) _) sR_idx (sR_state ios))%stdpp as ->; last first. { rewrite -own_op. done. } unfold sR_idx. simpl. intro j. @@ -580,8 +580,8 @@ Definition R := sumO locO (sumO unitO natO). Lemma logrel1_safety e τ (β : IT (gReifiers_ops rs) R) st st' k : typed □ e τ → - ssteps (gReifiers_sReifier NotCtxDep rs) (interp_expr rs e ı_scope) st β st' k → - (∃ β1 st1, sstep (gReifiers_sReifier NotCtxDep rs) β st' β1 st1) + ssteps (gReifiers_sReifier rs) (interp_expr rs e ı_scope) st β st' k → + (∃ β1 st1, sstep (gReifiers_sReifier rs) β st' β1 st1) ∨ (∃ βv, (IT_of_V βv ≡ β)%stdpp). Proof. intros Hty Hst. diff --git a/theories/examples/affine_lang/logrel2.v b/theories/examples/affine_lang/logrel2.v index 3db5de0..865580c 100644 --- a/theories/examples/affine_lang/logrel2.v +++ b/theories/examples/affine_lang/logrel2.v @@ -1,6 +1,4 @@ -From stdpp Require Import finite. From iris.base_logic.lib Require Import na_invariants. -From iris.algebra Require Import gmap. From gitrees Require Export gitree program_logic greifiers. From gitrees.examples.input_lang Require Import lang interp logpred. From gitrees.examples.affine_lang Require Import lang logrel1. @@ -478,15 +476,15 @@ Lemma logrel2_adequacy (cr : nat) R `{!Cofe R, !SubOfe locO R, !SubOfe natO R, ! (τ : ty) (α : interp_scope Empty_set -n> IT (gReifiers_ops rs) R) (β : IT (gReifiers_ops rs) R) st st' k : (∀ `{H1 : !invGS Σ} `{H2: !stateG rs R Σ} `{H3: !heapG rs R Σ} p, (£ cr ⊢ valid2 rs p □ α τ)%I) → - ssteps (gReifiers_sReifier NotCtxDep rs) (α ı_scope) st β st' k → - (∃ β1 st1, sstep (gReifiers_sReifier NotCtxDep rs) β st' β1 st1) + ssteps (gReifiers_sReifier rs) (α ı_scope) st β st' k → + (∃ β1 st1, sstep (gReifiers_sReifier rs) β st' β1 st1) ∨ (β ≡ Err OtherError)%stdpp ∨ (∃ βv, (IT_of_V βv ≡ β)%stdpp). Proof. intros Hlog Hst. destruct (IT_to_V β) as [βv|] eqn:Hb. { right. right. exists βv. apply IT_of_to_V'. rewrite Hb; eauto. } - cut ((∃ β1 st1, sstep (gReifiers_sReifier NotCtxDep rs) β st' β1 st1) + cut ((∃ β1 st1, sstep (gReifiers_sReifier rs) β st' β1 st1) ∨ (∃ e, (β ≡ Err e)%stdpp ∧ s e)). { intros [?|He]; first eauto. right. left. destruct He as [? [? ->]]. done. } @@ -502,9 +500,9 @@ Proof. iMod (new_heapG rs σ) as (H3) "H". iAssert (has_substate σ ∗ has_substate ios)%I with "[Hst]" as "[Hs Hio]". { unfold has_substate, has_full_state. - assert (of_state NotCtxDep rs (IT (gReifiers_ops rs) _) st ≡ - of_idx NotCtxDep rs (IT (gReifiers_ops rs) _) sR_idx (sR_state σ) - ⋅ of_idx NotCtxDep rs (IT (gReifiers_ops rs) _) sR_idx (sR_state ios))%stdpp as ->; last first. + assert (of_state rs (IT (gReifiers_ops rs) _) st ≡ + of_idx rs (IT (gReifiers_ops rs) _) sR_idx (sR_state σ) + ⋅ of_idx rs (IT (gReifiers_ops rs) _) sR_idx (sR_state ios))%stdpp as ->; last first. { rewrite -own_op. done. } unfold sR_idx. simpl. intro j. @@ -535,8 +533,8 @@ Definition R := sumO locO (sumO natO unitO). Lemma logrel2_safety e τ (β : IT (gReifiers_ops rs) R) st st' k : typed_glued □ e τ → - ssteps (gReifiers_sReifier NotCtxDep rs) (interp_expr rs e ı_scope) st β st' k → - (∃ β1 st1, sstep (gReifiers_sReifier NotCtxDep rs) β st' β1 st1) + ssteps (gReifiers_sReifier rs) (interp_expr rs e ı_scope) st β st' k → + (∃ β1 st1, sstep (gReifiers_sReifier rs) β st' β1 st1) ∨ (β ≡ Err OtherError)%stdpp ∨ (∃ βv, (IT_of_V βv ≡ β)%stdpp). Proof. diff --git a/theories/examples/input_lang/interp.v b/theories/examples/input_lang/interp.v index 0f8c135..806f55a 100644 --- a/theories/examples/input_lang/interp.v +++ b/theories/examples/input_lang/interp.v @@ -443,9 +443,9 @@ Section interp. + repeat f_equiv; [by apply interp_ectx_subst | by apply interp_val_subst]. Qed. - (** ** Interpretation is a homomorphism (for some constructors) *) + (** ** Interpretation of evaluation contexts induces homomorphism *) - #[global] Instance interp_ectx_hom_emp {S} env : + #[local] Instance interp_ectx_hom_emp {S} env : IT_hom (interp_ectx (EmptyK : ectx S) env). Proof. simple refine (IT_HOM _ _ _ _ _); intros; auto. @@ -453,7 +453,7 @@ Section interp. by rewrite laterO_map_id. Qed. - #[global] Instance interp_ectx_hom_output {S} (K : ectx S) env : + #[local] Instance interp_ectx_hom_output {S} (K : ectx S) env : IT_hom (interp_ectx K env) -> IT_hom (interp_ectx (OutputK K) env). Proof. @@ -465,7 +465,7 @@ Section interp. - by rewrite !hom_err. Qed. - #[global] Instance interp_ectx_hom_if {S} + #[local] Instance interp_ectx_hom_if {S} (K : ectx S) (e1 e2 : expr S) env : IT_hom (interp_ectx K env) -> IT_hom (interp_ectx (IfK K e1 e2) env). @@ -485,7 +485,7 @@ Section interp. apply IF_Err. Qed. - #[global] Instance interp_ectx_hom_appr {S} (K : ectx S) + #[local] Instance interp_ectx_hom_appr {S} (K : ectx S) (e : expr S) env : IT_hom (interp_ectx K env) -> IT_hom (interp_ectx (AppRK e K) env). @@ -497,7 +497,7 @@ Section interp. - by rewrite !hom_err. Qed. - #[global] Instance interp_ectx_hom_appl {S} (K : ectx S) + #[local] Instance interp_ectx_hom_appl {S} (K : ectx S) (v : val S) (env : interp_scope S) : IT_hom (interp_ectx K env) -> IT_hom (interp_ectx (AppLK K v) env). @@ -514,7 +514,7 @@ Section interp. apply APP'_Err_l, interp_val_asval. Qed. - #[global] Instance interp_ectx_hom_natopr {S} (K : ectx S) + #[local] Instance interp_ectx_hom_natopr {S} (K : ectx S) (e : expr S) op env : IT_hom (interp_ectx K env) -> IT_hom (interp_ectx (NatOpRK op e K) env). @@ -526,7 +526,7 @@ Section interp. - by rewrite !hom_err. Qed. - #[global] Instance interp_ectx_hom_natopl {S} (K : ectx S) + #[local] Instance interp_ectx_hom_natopl {S} (K : ectx S) (v : val S) op (env : interp_scope S) : IT_hom (interp_ectx K env) -> IT_hom (interp_ectx (NatOpLK op K v) env). @@ -544,14 +544,7 @@ Section interp. + by apply NATOP_Err_l, interp_val_asval. Qed. - Lemma get_fun_ret' E A `{Cofe A} n : (∀ f, @get_fun E A _ f (core.Ret n) ≡ Err RuntimeErr). - Proof. - intros. - by rewrite IT_rec1_ret. - Qed. - - #[global] Instance interp_ectx_hom {S} - (K : ectx S) env : + #[global] Instance interp_ectx_hom {S} (K : ectx S) env : IT_hom (interp_ectx K env). Proof. induction K; apply _. @@ -607,18 +600,18 @@ Section interp. Opaque Ret. Lemma interp_expr_fill_yes_reify {S} K env (e e' : expr S) - (σ σ' : stateO) (σr : gState_rest NotCtxDep sR_idx rs ♯ IT) n : + (σ σ' : stateO) (σr : gState_rest sR_idx rs ♯ IT) n : head_step e σ e' σ' (n, 1) → - reify (gReifiers_sReifier NotCtxDep rs) - (interp_expr (fill K e) env) (gState_recomp NotCtxDep σr (sR_state σ)) - ≡ (gState_recomp NotCtxDep σr (sR_state σ'), Tick_n n $ interp_expr (fill K e') env). + reify (gReifiers_sReifier rs) + (interp_expr (fill K e) env) (gState_recomp σr (sR_state σ)) + ≡ (gState_recomp σr (sR_state σ'), Tick_n n $ interp_expr (fill K e') env). Proof. intros Hst. - trans (reify (gReifiers_sReifier NotCtxDep rs) (interp_ectx K env (interp_expr e env)) - (gState_recomp NotCtxDep σr (sR_state σ))). + trans (reify (gReifiers_sReifier rs) (interp_ectx K env (interp_expr e env)) + (gState_recomp σr (sR_state σ))). { f_equiv. by rewrite interp_comp. } inversion Hst; simplify_eq; cbn-[gState_recomp]. - - trans (reify (gReifiers_sReifier NotCtxDep rs) (INPUT (interp_ectx K env ◎ Ret)) (gState_recomp NotCtxDep σr (sR_state σ))). + - trans (reify (gReifiers_sReifier rs) (INPUT (interp_ectx K env ◎ Ret)) (gState_recomp σr (sR_state σ))). { repeat f_equiv; eauto. rewrite hom_INPUT. @@ -639,19 +632,19 @@ Section interp. rewrite ofe_iso_21. simpl. reflexivity. - - trans (reify (gReifiers_sReifier NotCtxDep rs) (interp_ectx K env (OUTPUT n0)) (gState_recomp NotCtxDep σr (sR_state σ))). + - trans (reify (gReifiers_sReifier rs) (interp_ectx K env (OUTPUT n0)) (gState_recomp σr (sR_state σ))). { do 3 f_equiv; eauto. rewrite get_ret_ret//. } - trans (reify (gReifiers_sReifier NotCtxDep rs) (OUTPUT_ n0 (interp_ectx K env (Ret 0))) (gState_recomp NotCtxDep σr (sR_state σ))). + trans (reify (gReifiers_sReifier rs) (OUTPUT_ n0 (interp_ectx K env (Ret 0))) (gState_recomp σr (sR_state σ))). { do 2 f_equiv; eauto. by rewrite hom_OUTPUT_. } rewrite reify_vis_eq_ctx_indep //; last first. { - epose proof (@subReifier_reify sz NotCtxDep reify_io rs _ IT _ (inr (inl ())) n0 _ σ (update_output n0 σ) σr) as H. + epose proof (@subReifier_reify sz _ reify_io rs _ IT _ (inr (inl ())) n0 _ σ (update_output n0 σ) σr) as H. simpl in H. simpl. erewrite <-H; last reflexivity. @@ -663,11 +656,11 @@ Section interp. reflexivity. Qed. - Lemma soundness {S} (e1 e2 : expr S) σ1 σ2 (σr : gState_rest NotCtxDep sR_idx rs ♯ IT) n m (env : interp_scope S) : + Lemma soundness {S} (e1 e2 : expr S) σ1 σ2 (σr : gState_rest sR_idx rs ♯ IT) n m (env : interp_scope S) : prim_step e1 σ1 e2 σ2 (n,m) → - ssteps (gReifiers_sReifier NotCtxDep rs) - (interp_expr e1 env) (gState_recomp NotCtxDep σr (sR_state σ1)) - (interp_expr e2 env) (gState_recomp NotCtxDep σr (sR_state σ2)) n. + ssteps (gReifiers_sReifier rs) + (interp_expr e1 env) (gState_recomp σr (sR_state σ1)) + (interp_expr e2 env) (gState_recomp σr (sR_state σ2)) n. Proof. Opaque gState_decomp gState_recomp. inversion 1; simplify_eq/=. diff --git a/theories/examples/input_lang/lang.v b/theories/examples/input_lang/lang.v index bd6939f..a9d15f4 100644 --- a/theories/examples/input_lang/lang.v +++ b/theories/examples/input_lang/lang.v @@ -1,9 +1,7 @@ From gitrees Require Export prelude. -Require Import List. -Import ListNotations. - Require Import Binding.Resolver Binding.Lib Binding.Set Binding.Auto Binding.Env. + Inductive nat_op := Add | Sub | Mult. Inductive expr {X : Set} : Type := @@ -509,6 +507,10 @@ Coercion App : expr >-> Funclass. Coercion AppLK : ectx >-> Funclass. Coercion AppRK : expr >-> Funclass. +(* XXX: We use these typeclasses to share the notaiton between the +expressions and the evaluation contexts, for readability. It will be +good to also share the notation between different languages. *) + Class AsSynExpr (F : Set -> Type) := { __asSynExpr : ∀ S, F S -> expr S }. Arguments __asSynExpr {_} {_} {_}. diff --git a/theories/examples/input_lang/logpred.v b/theories/examples/input_lang/logpred.v index 303d9d4..6f1471b 100644 --- a/theories/examples/input_lang/logpred.v +++ b/theories/examples/input_lang/logpred.v @@ -256,15 +256,15 @@ Lemma logpred_adequacy cr Σ R `{!Cofe R, SubOfe natO R} (β : IT (gReifiers_ops rs) R) st st' k : (∀ `{H1 : !invGS Σ} `{H2: !stateG rs R Σ}, (£ cr ⊢ valid1 rs notStuck (λne _ : unitO, True)%I □ α τ)%I) → - ssteps (gReifiers_sReifier NotCtxDep rs) (α ı_scope) st β st' k → - (∃ β1 st1, sstep (gReifiers_sReifier NotCtxDep rs) β st' β1 st1) + ssteps (gReifiers_sReifier rs) (α ı_scope) st β st' k → + (∃ β1 st1, sstep (gReifiers_sReifier rs) β st' β1 st1) ∨ (∃ βv, IT_of_V βv ≡ β). Proof. intros Hlog Hst. destruct (IT_to_V β) as [βv|] eqn:Hb. { right. exists βv. apply IT_of_to_V'. rewrite Hb; eauto. } left. - cut ((∃ β1 st1, sstep (gReifiers_sReifier NotCtxDep rs) β st' β1 st1) + cut ((∃ β1 st1, sstep (gReifiers_sReifier rs) β st' β1 st1) ∨ (∃ e, β ≡ Err e ∧ notStuck e)). { intros [?|He]; first done. destruct He as [? [? []]]. } @@ -279,8 +279,8 @@ Proof. destruct st as [σ []]. iAssert (has_substate σ) with "[Hst]" as "Hs". { unfold has_substate, has_full_state. - assert (of_state NotCtxDep rs (IT (gReifiers_ops rs) _) (σ,()) ≡ - of_idx NotCtxDep rs (IT (gReifiers_ops rs) _) sR_idx (sR_state σ)) as ->; last done. + assert (of_state rs (IT (gReifiers_ops rs) _) (σ,()) ≡ + of_idx rs (IT (gReifiers_ops rs) _) sR_idx (sR_state σ)) as ->; last done. intro j. unfold sR_idx. simpl. unfold of_state, of_idx. destruct decide as [Heq|]; last first. @@ -302,10 +302,10 @@ Proof. done. Qed. -Lemma io_lang_safety e τ σ st' (β : IT (sReifier_ops (gReifiers_sReifier NotCtxDep rs)) natO) k : +Lemma io_lang_safety e τ σ st' (β : IT (sReifier_ops (gReifiers_sReifier rs)) natO) k : typed □ e τ → - ssteps (gReifiers_sReifier NotCtxDep rs) (interp_expr rs e ı_scope) (σ, ()) β st' k → - (∃ β1 st1, sstep (gReifiers_sReifier NotCtxDep rs) β st' β1 st1) + ssteps (gReifiers_sReifier rs) (interp_expr rs e ı_scope) (σ, ()) β st' k → + (∃ β1 st1, sstep (gReifiers_sReifier rs) β st' β1 st1) ∨ (∃ βv, IT_of_V βv ≡ β). Proof. intros Htyped Hsteps. diff --git a/theories/examples/input_lang/logrel.v b/theories/examples/input_lang/logrel.v index c058fd2..30b1a2d 100644 --- a/theories/examples/input_lang/logrel.v +++ b/theories/examples/input_lang/logrel.v @@ -359,7 +359,7 @@ Definition rs : gReifiers NotCtxDep 1 := gReifiers_cons reify_io gReifiers_nil. Lemma logrel_nat_adequacy Σ `{!invGpreS Σ}`{!statePreG rs natO Σ} {S} (α : IT (gReifiers_ops rs) natO) (e : expr S) n σ σ' k : (∀ `{H1 : !invGS Σ} `{H2: !stateG rs natO Σ}, (True ⊢ logrel rs Tnat α e)%I) → - ssteps (gReifiers_sReifier NotCtxDep rs) α (σ,()) (Ret n) σ' k → ∃ m σ', prim_steps e σ (Val $ LitV n) σ' m. + ssteps (gReifiers_sReifier rs) α (σ,()) (Ret n) σ' k → ∃ m σ', prim_steps e σ (Val $ LitV n) σ' m. Proof. intros Hlog Hst. pose (ϕ := λ (βv : ITV (gReifiers_ops rs) natO), @@ -391,8 +391,8 @@ Proof. iPoseProof (Hlog with "[//]") as "Hlog". iAssert (has_substate σ) with "[Hs]" as "Hs". { unfold has_substate, has_full_state. - assert (of_state NotCtxDep rs (IT (gReifiers_ops rs) natO) (σ, ()) ≡ - of_idx NotCtxDep rs (IT (gReifiers_ops rs) natO) 0 σ)%stdpp as ->; last done. + assert (of_state rs (IT (gReifiers_ops rs) natO) (σ, ()) ≡ + of_idx rs (IT (gReifiers_ops rs) natO) 0 σ)%stdpp as ->; last done. intro j. unfold sR_idx. simpl. unfold of_state, of_idx. destruct decide as [Heq|]; last first. @@ -413,7 +413,7 @@ Qed. Theorem adequacy (e : expr ∅) (k : nat) σ σ' n : typed □ e Tnat → - ssteps (gReifiers_sReifier NotCtxDep rs) (interp_expr rs e ı_scope) (σ,()) (Ret k : IT _ natO) σ' n → + ssteps (gReifiers_sReifier rs) (interp_expr rs e ı_scope) (σ,()) (Ret k : IT _ natO) σ' n → ∃ mm σ', prim_steps e σ (Val $ LitV k) σ' mm. Proof. intros Hty Hst. @@ -424,8 +424,7 @@ Proof. { apply Hty. } unfold logrel_valid. iIntros "_". - unshelve iSpecialize ("H" $! ı_scope _ with "[]"). - { apply ı%bind. } + iSpecialize ("H" $! ı_scope ı%bind with "[]"). { iIntros (x); destruct x. } rewrite ebind_id; first last. { intros ?; reflexivity. } diff --git a/theories/examples/input_lang_callcc/hom.v b/theories/examples/input_lang_callcc/hom.v index 661374b..66f3f2d 100644 --- a/theories/examples/input_lang_callcc/hom.v +++ b/theories/examples/input_lang_callcc/hom.v @@ -1,6 +1,7 @@ -From gitrees Require Import gitree. +(** In this module, we package up IT homomorphism in a sigma type, and +we will use it as a domain for logical relations on continuations *) +From gitrees Require Import gitree lang_generic. From gitrees.examples.input_lang_callcc Require Import lang interp. -Require Import gitrees.lang_generic. Require Import Binding.Lib Binding.Set Binding.Env. Open Scope stdpp_scope. @@ -42,6 +43,7 @@ Section hom. `f ◎ `g = `h. Proof. intros ->. done. Qed. + (** Specific packaged homomorphisms *) Program Definition IFSCtx_HOM α β : HOM := exist _ (λne x, IFSCtx α β x) _. Next Obligation. intros; simpl. diff --git a/theories/examples/input_lang_callcc/interp.v b/theories/examples/input_lang_callcc/interp.v index 5daeec3..e9e94ec 100644 --- a/theories/examples/input_lang_callcc/interp.v +++ b/theories/examples/input_lang_callcc/interp.v @@ -1,9 +1,6 @@ -From gitrees Require Import gitree. +From gitrees Require Import gitree lang_generic. From gitrees.examples.input_lang_callcc Require Import lang. -Require Import gitrees.lang_generic. - -Require Import Binding.Lib. -Require Import Binding.Set. +Require Import Binding.Lib Binding.Set. Notation stateO := (leibnizO state). @@ -512,14 +509,6 @@ Section interp. end. Solve All Obligations with first [ solve_proper | solve_proper_please ]. - (* Open Scope syn_scope. *) - - (* Example callcc_ex : expr ∅ := *) - (* NatOp + (# 1) (Callcc (NatOp + (# 1) (Throw (# 2) ($ 0)))). *) - (* Eval cbn in callcc_ex. *) - (* Eval cbn in interp_expr callcc_ex *) - (* (λne (x : leibnizO ∅), match x with end). *) - Global Instance interp_val_asval {S} {D : interp_scope S} (v : val S) : AsVal (interp_val v D). Proof. @@ -712,9 +701,9 @@ Section interp. intros ?; simpl; repeat f_equiv; first by apply interp_ectx_subst. Qed. - (** ** Interpretation is a homomorphism (for some constructors) *) + (** ** Interpretation of evaluation contexts induces homomorphism *) - #[global] Instance interp_ectx_hom_emp {S} env : + #[local] Instance interp_ectx_hom_emp {S} env : IT_hom (interp_ectx (EmptyK : ectx S) env). Proof. simple refine (IT_HOM _ _ _ _ _); intros; auto. @@ -722,7 +711,7 @@ Section interp. by rewrite laterO_map_id. Qed. - #[global] Instance interp_ectx_hom_output {S} (K : ectx S) env : + #[local] Instance interp_ectx_hom_output {S} (K : ectx S) env : IT_hom (interp_ectx K env) -> IT_hom (interp_ectx (OutputK K) env). Proof. @@ -734,7 +723,7 @@ Section interp. - by rewrite !hom_err. Qed. - #[global] Instance interp_ectx_hom_if {S} + #[local] Instance interp_ectx_hom_if {S} (K : ectx S) (e1 e2 : expr S) env : IT_hom (interp_ectx K env) -> IT_hom (interp_ectx (IfK K e1 e2) env). @@ -754,7 +743,7 @@ Section interp. apply IF_Err. Qed. - #[global] Instance interp_ectx_hom_appr {S} (K : ectx S) + #[local] Instance interp_ectx_hom_appr {S} (K : ectx S) (e : expr S) env : IT_hom (interp_ectx K env) -> IT_hom (interp_ectx (AppRK e K) env). @@ -766,7 +755,7 @@ Section interp. - by rewrite !hom_err. Qed. - #[global] Instance interp_ectx_hom_appl {S} (K : ectx S) + #[local] Instance interp_ectx_hom_appl {S} (K : ectx S) (v : val S) (env : interp_scope S) : IT_hom (interp_ectx K env) -> IT_hom (interp_ectx (AppLK K v) env). @@ -783,7 +772,7 @@ Section interp. apply APP'_Err_l, interp_val_asval. Qed. - #[global] Instance interp_ectx_hom_natopr {S} (K : ectx S) + #[local] Instance interp_ectx_hom_natopr {S} (K : ectx S) (e : expr S) op env : IT_hom (interp_ectx K env) -> IT_hom (interp_ectx (NatOpRK op e K) env). @@ -795,7 +784,7 @@ Section interp. - by rewrite !hom_err. Qed. - #[global] Instance interp_ectx_hom_natopl {S} (K : ectx S) + #[local] Instance interp_ectx_hom_natopl {S} (K : ectx S) (v : val S) op (env : interp_scope S) : IT_hom (interp_ectx K env) -> IT_hom (interp_ectx (NatOpLK op K v) env). @@ -813,13 +802,7 @@ Section interp. + by apply NATOP_Err_l, interp_val_asval. Qed. - Lemma get_fun_ret' E A `{Cofe A} n : (∀ f, @get_fun E A _ f (core.Ret n) ≡ Err RuntimeErr). - Proof. - intros. - by rewrite IT_rec1_ret. - Qed. - - #[global] Instance interp_ectx_hom_throwr {S} + #[local] Instance interp_ectx_hom_throwr {S} (K : ectx S) (v : val S) env : IT_hom (interp_ectx K env) -> IT_hom (interp_ectx (ThrowRK v K) env). @@ -832,7 +815,7 @@ Section interp. destruct (IT_dont_confuse ((interp_ectx K env α))) as [(e' & HEQ) |[(n & HEQ) |[(f & HEQ) |[(β & HEQ) | (op & i & k & HEQ)]]]]. + rewrite HEQ !get_fun_tick !get_fun_err. reflexivity. - + rewrite HEQ !get_fun_tick !get_fun_ret'. + + rewrite HEQ !get_fun_tick. reflexivity. + rewrite HEQ !get_fun_tick !get_fun_fun//=. + rewrite HEQ !get_fun_tick. @@ -860,7 +843,7 @@ Section interp. reflexivity. Qed. - #[global] Instance interp_ectx_hom_throwl {S} + #[local] Instance interp_ectx_hom_throwl {S} (K : ectx S) (e : expr S) env : IT_hom (interp_ectx K env) -> IT_hom (interp_ectx (ThrowLK K e) env). @@ -930,18 +913,18 @@ Section interp. Opaque Ret. Lemma interp_expr_fill_yes_reify {S} K env (e e' : expr S) - (σ σ' : stateO) (σr : gState_rest CtxDep sR_idx rs ♯ IT) n : + (σ σ' : stateO) (σr : gState_rest sR_idx rs ♯ IT) n : head_step e σ e' σ' K (n, 1) → - reify (gReifiers_sReifier CtxDep rs) - (interp_expr (fill K e) env) (gState_recomp CtxDep σr (sR_state σ)) - ≡ (gState_recomp CtxDep σr (sR_state σ'), Tick_n n $ interp_expr (fill K e') env). + reify (gReifiers_sReifier rs) + (interp_expr (fill K e) env) (gState_recomp σr (sR_state σ)) + ≡ (gState_recomp σr (sR_state σ'), Tick_n n $ interp_expr (fill K e') env). Proof. intros Hst. - trans (reify (gReifiers_sReifier CtxDep rs) (interp_ectx K env (interp_expr e env)) - (gState_recomp CtxDep σr (sR_state σ))). + trans (reify (gReifiers_sReifier rs) (interp_ectx K env (interp_expr e env)) + (gState_recomp σr (sR_state σ))). { f_equiv. by rewrite interp_comp. } inversion Hst; simplify_eq; cbn-[gState_recomp]. - - trans (reify (gReifiers_sReifier CtxDep rs) (INPUT (interp_ectx K env ◎ Ret)) (gState_recomp CtxDep σr (sR_state σ))). + - trans (reify (gReifiers_sReifier rs) (INPUT (interp_ectx K env ◎ Ret)) (gState_recomp σr (sR_state σ))). { repeat f_equiv; eauto. rewrite hom_INPUT. @@ -960,12 +943,12 @@ Section interp. repeat f_equiv. rewrite Tick_eq/=. repeat f_equiv. rewrite interp_comp. reflexivity. - - trans (reify (gReifiers_sReifier CtxDep rs) (interp_ectx K env (OUTPUT n0)) (gState_recomp CtxDep σr (sR_state σ))). + - trans (reify (gReifiers_sReifier rs) (interp_ectx K env (OUTPUT n0)) (gState_recomp σr (sR_state σ))). { do 3 f_equiv; eauto. rewrite get_ret_ret//. } - trans (reify (gReifiers_sReifier CtxDep rs) (OUTPUT_ n0 (interp_ectx K env (Ret 0))) (gState_recomp CtxDep σr (sR_state σ))). + trans (reify (gReifiers_sReifier rs) (OUTPUT_ n0 (interp_ectx K env (Ret 0))) (gState_recomp σr (sR_state σ))). { do 2 f_equiv; eauto. by rewrite hom_OUTPUT_. @@ -992,7 +975,7 @@ Section interp. unfold CALLCC. simpl. set (subEff1 := @subReifier_subEff sz CtxDep reify_io rs subR). - trans (reify (gReifiers_sReifier CtxDep rs) (CALLCC_ f (laterO_map (interp_ectx K env))) gσ). + trans (reify (gReifiers_sReifier rs) (CALLCC_ f (laterO_map (interp_ectx K env))) gσ). { do 2 f_equiv. rewrite hom_CALLCC_. @@ -1021,11 +1004,11 @@ Section interp. do 2 f_equiv. by intro. Qed. - Lemma soundness {S} (e1 e2 : expr S) σ1 σ2 (σr : gState_rest CtxDep sR_idx rs ♯ IT) n m (env : interp_scope S) : + Lemma soundness {S} (e1 e2 : expr S) σ1 σ2 (σr : gState_rest sR_idx rs ♯ IT) n m (env : interp_scope S) : prim_step e1 σ1 e2 σ2 (n,m) → - ssteps (gReifiers_sReifier CtxDep rs) - (interp_expr e1 env) (gState_recomp CtxDep σr (sR_state σ1)) - (interp_expr e2 env) (gState_recomp CtxDep σr (sR_state σ2)) n. + ssteps (gReifiers_sReifier rs) + (interp_expr e1 env) (gState_recomp σr (sR_state σ1)) + (interp_expr e2 env) (gState_recomp σr (sR_state σ2)) n. Proof. Opaque gState_decomp gState_recomp. inversion 1; simplify_eq/=. @@ -1097,7 +1080,7 @@ Section interp. match goal with | |- context G [ofe_mor_car _ _ _ (Next ?f)] => set (f' := f) end. - trans (reify (gReifiers_sReifier CtxDep rs) (THROW (interp_val v env) (Next f')) (gState_recomp CtxDep σr (sR_state σ2))). + trans (reify (gReifiers_sReifier rs) (THROW (interp_val v env) (Next f')) (gState_recomp σr (sR_state σ2))). { f_equiv; last done. f_equiv. diff --git a/theories/examples/input_lang_callcc/lang.v b/theories/examples/input_lang_callcc/lang.v index e7cb712..65eabcb 100644 --- a/theories/examples/input_lang_callcc/lang.v +++ b/theories/examples/input_lang_callcc/lang.v @@ -1,12 +1,9 @@ From gitrees Require Export prelude. -Require Import List. -Import ListNotations. - Require Import Binding.Resolver Binding.Lib Binding.Set Binding.Auto Binding.Env. Inductive nat_op := Add | Sub | Mult. -Inductive expr {X : Set} := +Inductive expr {X : Set} : Type := (* Values *) | Val (v : val) : expr | Var (x : X) : expr diff --git a/theories/examples/input_lang_callcc/logrel.v b/theories/examples/input_lang_callcc/logrel.v index cbfd44f..717256c 100644 --- a/theories/examples/input_lang_callcc/logrel.v +++ b/theories/examples/input_lang_callcc/logrel.v @@ -1,8 +1,6 @@ (** Logical relation for adequacy for the IO lang *) -From gitrees Require Import gitree. +From gitrees Require Import gitree lang_generic. From gitrees.examples.input_lang_callcc Require Import lang interp hom. -Require Import gitrees.lang_generic. -Require Import gitrees.gitree.greifiers. Require Import Binding.Lib Binding.Set Binding.Env. Open Scope stdpp_scope. @@ -692,7 +690,7 @@ Lemma logrel_nat_adequacy Σ `{!invGpreS Σ} `{!statePreG rs natO Σ} {S} (α : IT (gReifiers_ops rs) natO) (e : expr S) n σ σ' k : (∀ `{H1 : !invGS Σ} `{H2: !stateG rs natO Σ}, (⊢ logrel rs Tnat α e)%I) → - ssteps (gReifiers_sReifier CtxDep rs) α (σ, ()) (Ret n) σ' k → + ssteps (gReifiers_sReifier rs) α (σ, ()) (Ret n) σ' k → ∃ m σ', prim_steps e σ (Val $ LitV n) σ' m. Proof. intros Hlog Hst. @@ -731,8 +729,8 @@ Proof. iAssert (has_substate σ) with "[Hs]" as "Hs". { unfold has_substate, has_full_state. - assert ((of_state CtxDep rs (IT (sReifier_ops (gReifiers_sReifier CtxDep rs)) natO) (σ, ())) ≡ - (of_idx CtxDep rs (IT (sReifier_ops (gReifiers_sReifier CtxDep rs)) natO) sR_idx (sR_state σ))) + assert ((of_state rs (IT (sReifier_ops (gReifiers_sReifier rs)) natO) (σ, ())) ≡ + (of_idx rs (IT (sReifier_ops (gReifiers_sReifier rs)) natO) sR_idx (sR_state σ))) as -> ; last done. intros j. unfold sR_idx. simpl. unfold of_state, of_idx. @@ -767,7 +765,7 @@ Qed. Theorem adequacy (e : expr ∅) (k : nat) σ σ' n : typed □ e Tnat → - ssteps (gReifiers_sReifier CtxDep rs) (interp_expr rs e ı_scope) (σ, ()) (Ret k : IT _ natO) σ' n → + ssteps (gReifiers_sReifier rs) (interp_expr rs e ı_scope) (σ, ()) (Ret k : IT _ natO) σ' n → ∃ mm σ', prim_steps e σ (Val $ LitV k) σ' mm. Proof. intros Hty Hst. diff --git a/theories/examples/input_lang_delim/example.v b/theories/examples/input_lang_delim/example.v index 0110269..9389c3e 100644 --- a/theories/examples/input_lang_delim/example.v +++ b/theories/examples/input_lang_delim/example.v @@ -1,7 +1,5 @@ -From gitrees Require Import gitree. +From gitrees Require Import gitree lang_generic. From gitrees.examples.input_lang_delim Require Import lang interp. -Require Import gitrees.lang_generic. -From iris.algebra Require Import gmap excl auth gmap_view. From iris.proofmode Require Import base classes tactics environments. From iris.base_logic Require Import algebra. @@ -63,6 +61,7 @@ Proof. (* then, shift *) do 2 shift_hom. iApply (wp_shift with "Hσ"). + { rewrite laterO_map_Next. done. } iIntros "!>_ Hσ". simpl. @@ -70,7 +69,7 @@ Proof. rewrite -(IT_of_V_Ret 6) get_val_ITV'. simpl. rewrite get_fun_fun. simpl. do 2 shift_hom. - iApply (wp_app_cont with "Hσ"). + iApply (wp_app_cont with "Hσ"); first done. iIntros "!> _ Hσ". simpl. rewrite later_map_Next -Tick_eq. iApply wp_tick. iNext. @@ -86,7 +85,7 @@ Proof. shift_hom. shift_natop_l. rewrite get_fun_fun. simpl. shift_hom. shift_natop_l. - iApply (wp_app_cont with "Hσ"). + iApply (wp_app_cont with "Hσ"); first done. iIntros "!> _ Hσ". simpl. rewrite later_map_Next -Tick_eq. iApply wp_tick. iNext. diff --git a/theories/examples/input_lang_delim/interp.v b/theories/examples/input_lang_delim/interp.v index c82d255..3f0b2db 100644 --- a/theories/examples/input_lang_delim/interp.v +++ b/theories/examples/input_lang_delim/interp.v @@ -1,25 +1,14 @@ (* From Equations Require Import Equations. *) -From gitrees Require Import gitree. +From gitrees Require Import gitree lang_generic. From gitrees.examples.input_lang_delim Require Import lang. -Require Import gitrees.lang_generic. -From iris.algebra Require Import gmap excl auth gmap_view. +From iris.algebra Require Import list. From iris.proofmode Require Import classes tactics. From iris.base_logic Require Import algebra. -From iris.heap_lang Require Export locations. -Require Import Binding.Lib. -Require Import Binding.Set. +Require Import Binding.Lib Binding.Set. -(** * State *) - -(* Definition stateF : oFunctor := (gmapOF unitO (▶ ∙))%OF. *) - -(* #[local] Instance state_inhabited : Inhabited (stateF ♯ unitO). *) -(* Proof. apply _. Qed. *) -(* #[local] Instance state_cofe X `{!Cofe X} : Cofe (stateF ♯ X). *) -(* Proof. apply _. Qed. *) - +(** * State, corresponding to a meta-continuation *) Definition stateF : oFunctor := (listOF (▶ ∙ -n> ▶ ∙))%OF. #[local] Instance state_inhabited : Inhabited (stateF ♯ unitO). @@ -237,38 +226,35 @@ Section weakestpre. (** ** SHIFT *) Lemma wp_shift (σ : state) (f : (laterO IT -n> laterO IT) -n> laterO IT) - (k : IT -n> IT) {Hk : IT_hom k} Φ s : + (k : IT -n> IT) β {Hk : IT_hom k} Φ s : + laterO_map 𝒫 (f (laterO_map k)) ≡ Next β → has_substate σ -∗ - ▷ (£ 1 -∗ has_substate σ -∗ WP@{rs} 𝒫 (later_car ( f (laterO_map k))) @ s {{ Φ }}) -∗ + ▷ (£ 1 -∗ has_substate σ -∗ WP@{rs} β @ s {{ Φ }}) -∗ WP@{rs} (k (SHIFT f)) @ s {{ Φ }}. Proof. - iIntros "Hs Ha". + iIntros (Hp) "Hs Ha". unfold SHIFT. simpl. rewrite hom_vis. - iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ (later_map 𝒫 $ f (laterO_map k)) with "Hs"). + iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ (laterO_map 𝒫 $ f (laterO_map k)) with "Hs"). { - simpl. - repeat f_equiv. - - rewrite ccompose_id_l. intro. simpl. by rewrite ofe_iso_21. - - reflexivity. + simpl. do 2 f_equiv; last done. do 2 f_equiv. + rewrite ccompose_id_l. intro. simpl. by rewrite ofe_iso_21. } - { by rewrite later_map_Next. } + { exact Hp. } iModIntro. iApply "Ha". Qed. - - - Lemma wp_reset (σ : state) (e : laterO IT) (k : IT -n> IT) {Hk : IT_hom k} + Lemma wp_reset (σ : state) (e : IT) (k : IT -n> IT) {Hk : IT_hom k} Φ s : has_substate σ -∗ ▷ (£ 1 -∗ has_substate ((laterO_map k) :: σ) -∗ - WP@{rs} 𝒫 (later_car e) @ s {{ Φ }}) -∗ - WP@{rs} k $ (RESET e) @ s {{ Φ }}. + WP@{rs} 𝒫 e @ s {{ Φ }}) -∗ + WP@{rs} k $ (RESET (Next e)) @ s {{ Φ }}. Proof. iIntros "Hs Ha". unfold RESET. simpl. rewrite hom_vis. - iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ (laterO_map 𝒫 e) with "Hs"). + iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ (Next $ 𝒫 e) with "Hs"). - simpl. repeat f_equiv. rewrite ccompose_id_l. trans ((laterO_map k) :: σ); last reflexivity. f_equiv. intro. simpl. by rewrite ofe_iso_21. @@ -276,7 +262,7 @@ Section weakestpre. - iApply "Ha". Qed. - + (** XXX: Formulate the rules using AsVal *) Lemma wp_pop_end (v : ITV) Φ s : has_substate [] -∗ @@ -306,24 +292,24 @@ Section weakestpre. Qed. Lemma wp_app_cont (σ : state) (e : laterO IT) (k' : laterO (IT -n> IT)) - (k : IT -n> IT) {Hk : IT_hom k} + (k : IT -n> IT) β {Hk : IT_hom k} Φ s : + laterO_ap k' e ≡ Next β → has_substate σ -∗ ▷ (£ 1 -∗ has_substate ((laterO_map k) :: σ) -∗ - WP@{rs} later_car (laterO_ap k' e) @ s {{ Φ }}) -∗ + WP@{rs} β @ s {{ Φ }}) -∗ WP@{rs} k (APP_CONT e k') @ s {{ Φ }}. Proof. - iIntros "Hs Ha". + iIntros (Hb) "Hs Ha". unfold APP_CONT. simpl. rewrite hom_vis. - iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ (laterO_ap k' e) with "Hs"). - - simpl. do 2 f_equiv. + iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ (Next β) with "Hs"). + - cbn-[laterO_ap]. rewrite Hb. do 2 f_equiv. trans (laterO_map k :: σ); last reflexivity. rewrite ccompose_id_l. f_equiv. intro. simpl. by rewrite ofe_iso_21. - reflexivity. - iApply "Ha". Qed. - End weakestpre. Section interp. @@ -359,15 +345,13 @@ Section interp. Program Definition interp_shift {S} (e : @interp_scope F R _ (inc S) -n> IT) : interp_scope S -n> IT := λne env, SHIFT (λne (k : laterO IT -n> laterO IT), - Next (e (@extend_scope F R _ _ env (λit x, Tau (k (Next x)))))). + Next (e (extend_scope env (λit x, Tau (k (Next x)))))). Next Obligation. solve_proper. Qed. Next Obligation. solve_proper_prepare. repeat f_equiv. intros [| a]; simpl; last solve_proper. - repeat f_equiv. - intros ?; simpl. - by repeat f_equiv. + repeat f_equiv. solve_proper. Qed. Next Obligation. solve_proper_prepare. @@ -391,49 +375,42 @@ Section interp. (** ** REC *) Opaque laterO_map. - Program Definition interp_rec_pre {S : Set} (body : @interp_scope F R _ (inc (inc S)) -n> IT) - : laterO (@interp_scope F R _ S -n> IT) -n> @interp_scope F R _ S -n> IT := - λne self env, Fun $ laterO_map (λne (self : @interp_scope F R _ S -n> IT) (a : IT), - body (@extend_scope F R _ _ (@extend_scope F R _ _ env (self env)) a)) self. + Program Definition interp_rec_pre {S : Set} (body : interp_scope (inc (inc S)) -n> IT) + : laterO (interp_scope S -n> IT) -n> interp_scope S -n> IT := + λne self env, Fun $ laterO_map (λne (self : interp_scope S -n> IT) (a : IT), + body (extend_scope (extend_scope env (self env)) a)) self. Next Obligation. - intros. solve_proper_prepare. f_equiv; intros [| [| y']]; simpl; solve_proper. Qed. Next Obligation. - intros. solve_proper_prepare. f_equiv; intros [| [| y']]; simpl; solve_proper. Qed. Next Obligation. - intros. solve_proper_prepare. do 3 f_equiv; intros ??; simpl; f_equiv; intros [| [| y']]; simpl; solve_proper. Qed. Next Obligation. - intros. solve_proper_prepare. by do 2 f_equiv. Qed. Program Definition interp_rec {S : Set} - (body : @interp_scope F R _ (inc (inc S)) -n> IT) : - @interp_scope F R _ S -n> IT := + (body : interp_scope (inc (inc S)) -n> IT) : interp_scope S -n> IT := mmuu (interp_rec_pre body). Program Definition ir_unf {S : Set} - (body : @interp_scope F R _ (inc (inc S)) -n> IT) env : IT -n> IT := - λne a, body (@extend_scope F R _ _ - (@extend_scope F R _ _ env (interp_rec body env)) - a). + (body : interp_scope (inc (inc S)) -n> IT) env : IT -n> IT := + λne a, body (extend_scope + (extend_scope env (interp_rec body env)) a). Next Obligation. - intros. solve_proper_prepare. f_equiv. intros [| [| y']]; simpl; solve_proper. Qed. - Lemma interp_rec_unfold {S : Set} (body : @interp_scope F R _ (inc (inc S)) -n> IT) env : + Lemma interp_rec_unfold {S : Set} (body : interp_scope (inc (inc S)) -n> IT) env : interp_rec body env ≡ Fun $ Next $ ir_unf body env. Proof. trans (interp_rec_pre body (Next (interp_rec body)) env). @@ -480,28 +457,11 @@ Section interp. λne env, Ret n. (** ** CONT *) + (** XXX DF: why do we need a tick here? Seems to be necessary for soundness *) Program Definition interp_cont_val {S} (K : S -n> (IT -n> IT)) : S -n> IT := - λne env, (λit x, Tau (laterO_map (𝒫 ◎ K env) (Next x))). + λne env, (λit x, Tick $ 𝒫 (K env x)). Solve All Obligations with solve_proper_please. - (* Program Definition interp_cont {S} (e : @interp_scope F R _ (inc S) -n> IT) : *) - (* interp_scope S -n> IT := *) - (* λne env, (Fun (Next (λne x, Tick $ e (@extend_scope F R _ _ env x)))). *) - (* Next Obligation. *) - (* solve_proper_prepare. repeat f_equiv. *) - (* intros [|a]; eauto. *) - (* Qed. *) - (* Next Obligation. *) - (* solve_proper_prepare. *) - (* repeat f_equiv. *) - (* intro. simpl. repeat f_equiv. *) - (* intros [|z]; eauto. *) - (* Qed. *) - - (* #[local] Instance interp_reset_full_ne {S} (f : @interp_scope F R _ S -n> IT): *) - (* NonExpansive (λ env, interp_reset (f env)). *) - (* Proof. solve_proper. Qed. *) - Program Definition interp_ifk {A} (e1 e2 : A -n> IT) (K : A -n> IT -n> IT) : A -n> (IT -n> IT) := λne env b, (K env) $ interp_if (λne env, b) e1 e2 env. @@ -692,16 +652,6 @@ Section interp. intro. simpl. by repeat f_equiv. Qed. - - (* Lemma interp_ectx_ren {S S'} env (δ : S [→] S') (K : ectx S) : *) - (* interp_ectx (fmap δ K) env ≡ interp_ectx K (ren_scope δ env). *) - (* Proof. *) - (* induction K; intros ?; simpl; eauto. *) - (* destruct a; simpl; try (etrans; first by apply IHK); repeat f_equiv; *) - (* try solve [by apply interp_expr_ren | by apply interp_val_ren]. *) - (* Qed. *) - - Lemma interp_comp {S} (e : expr S) (env : interp_scope S) (K : cont S): interp_expr (fill K e) env ≡ (interp_cont K) env ((interp_expr e) env). Proof. elim : K e env; eauto. @@ -772,9 +722,9 @@ Section interp. - (** ** Interpretation is a homomorphism (for some constructors) *) + (** ** Interpretation of continuations is a homormophism *) - #[global] Instance interp_cont_hom_emp {S} env : + #[local] Instance interp_cont_hom_emp {S} env : IT_hom (interp_cont (END : cont S) env). Proof. simple refine (IT_HOM _ _ _ _ _); intros; auto. @@ -782,8 +732,7 @@ Section interp. by rewrite laterO_map_id. Qed. - - #[global] Instance interp_cont_hom_if {S} + #[local] Instance interp_cont_hom_if {S} (K : cont S) (e1 e2 : expr S) env : IT_hom (interp_cont K env) -> IT_hom (interp_cont (IfK e1 e2 K) env). @@ -800,7 +749,7 @@ Section interp. Qed. - #[global] Instance interp_cont_hom_appr {S} (K : cont S) + #[local] Instance interp_cont_hom_appr {S} (K : cont S) (e : expr S) env : IT_hom (interp_cont K env) -> IT_hom (interp_cont (AppRK e K) env). @@ -812,7 +761,7 @@ Section interp. - by rewrite !hom_err. Qed. - #[global] Instance interp_cont_hom_appl {S} (K : cont S) + #[local] Instance interp_cont_hom_appl {S} (K : cont S) (v : val S) (env : interp_scope S) : IT_hom (interp_cont K env) -> IT_hom (interp_cont (AppLK v K) env). @@ -830,19 +779,19 @@ Section interp. Qed. - #[global] Instance interp_cont_hom_app_contr {S} (K : cont S) + #[local] Instance interp_cont_hom_app_contr {S} (K : cont S) (e : expr S) env : IT_hom (interp_cont K env) -> IT_hom (interp_cont (AppContRK e K) env). Proof. intros. simple refine (IT_HOM _ _ _ _ _); intros; simpl. - - by rewrite -!hom_tick. + - by rewrite -!hom_tick. - rewrite !hom_vis. f_equiv. intro x. simpl. by rewrite -laterO_map_compose. - by rewrite !hom_err. Qed. - #[global] Instance interp_cont_hom_app_contl {S} (K : cont S) + #[local] Instance interp_cont_hom_app_contl {S} (K : cont S) (v : val S) (env : interp_scope S) : IT_hom (interp_cont K env) -> IT_hom (interp_cont (AppContLK v K) env). @@ -859,7 +808,7 @@ Section interp. Qed. - #[global] Instance interp_cont_hom_natopr {S} (K : cont S) + #[local] Instance interp_cont_hom_natopr {S} (K : cont S) (e : expr S) op env : IT_hom (interp_cont K env) -> IT_hom (interp_cont (NatOpRK op e K) env). @@ -871,7 +820,7 @@ Section interp. - by rewrite !hom_err. Qed. - #[global] Instance interp_cont_hom_natopl {S} (K : cont S) + #[local] Instance interp_cont_hom_natopl {S} (K : cont S) (v : val S) op (env : interp_scope S) : IT_hom (interp_cont K env) -> IT_hom (interp_cont (NatOpLK op v K) env). @@ -888,14 +837,6 @@ Section interp. + apply hom_err. Qed. - - Lemma get_fun_ret' E A `{Cofe A} n : (∀ f, @get_fun E A _ f (core.Ret n) ≡ Err RuntimeErr). - Proof. - intros. - by rewrite IT_rec1_ret. - Qed. - - #[global] Instance interp_cont_hom {S} (K : cont S) env : IT_hom (interp_cont K env). @@ -903,8 +844,6 @@ Section interp. induction K; simpl; apply _. Qed. - - (** ** Finally, preservation of reductions *) Lemma interp_cred_no_reify {S : Set} (env : interp_scope S) (C C' : config S) (t t' : IT) (σ σ' : state) n : @@ -943,28 +882,27 @@ Section interp. (interp_config C env) = (t, σ) -> (interp_config C' env) = (t', σ') -> σ = σ'. - Proof. + Proof. inversion 1; cbn; intros Ht Ht'; inversion Ht; inversion Ht'; subst; reflexivity. Qed. Opaque map_meta_cont. Opaque extend_scope. - Opaque Ret. Lemma interp_cred_yes_reify {S : Set} (env : interp_scope S) (C C' : config S) - (t t' : IT) (σ σ' : state) (σr : gState_rest CtxDep sR_idx rs ♯ IT) n : + (t t' : IT) (σ σ' : state) (σr : gState_rest sR_idx rs ♯ IT) n : C ===> C' / (n, 1) -> (interp_config C env) = (t, σ) -> (interp_config C' env) = (t', σ') -> - reify (gReifiers_sReifier CtxDep rs) t (gState_recomp CtxDep σr (sR_state σ)) - ≡ (gState_recomp CtxDep σr (sR_state σ'), Tick_n n $ t'). + reify (gReifiers_sReifier rs) t (gState_recomp σr (sR_state σ)) + ≡ (gState_recomp σr (sR_state σ'), Tick_n n $ t'). Proof. inversion 1; cbn-[IF APP' Tick get_ret2 gState_recomp]; intros Ht Ht'; inversion Ht; inversion Ht'; subst; try rewrite !map_meta_cont_cons in Ht, Ht'|-*. - - trans (reify (gReifiers_sReifier CtxDep rs) + - trans (reify (gReifiers_sReifier rs) (RESET_ (laterO_map (𝒫 ◎ (interp_cont k env))) (Next (interp_expr e env))) - (gState_recomp CtxDep σr (sR_state (map_meta_cont mk env)))). + (gState_recomp σr (sR_state (map_meta_cont mk env)))). { repeat f_equiv. rewrite !hom_vis. simpl. f_equiv. rewrite ccompose_id_l. by intro. @@ -984,9 +922,9 @@ Section interp. match goal with | |- context G [Vis ?o ?f ?κ] => set (fin := f); set (op := o); set (kout := κ) end. - trans (reify (gReifiers_sReifier CtxDep rs) + trans (reify (gReifiers_sReifier rs) (Vis op fin ((laterO_map (𝒫 ◎ interp_cont k env)) ◎ kout)) - (gState_recomp CtxDep σr (sR_state σ))). + (gState_recomp σr (sR_state σ))). { repeat f_equiv. rewrite !hom_vis. f_equiv. by intro. } @@ -1002,6 +940,7 @@ Section interp. - subst fin. reflexivity. - solve_proper. } + simpl. rewrite -Tick_eq. do 3 f_equiv. rewrite interp_expr_subst. simpl. f_equiv. @@ -1015,10 +954,10 @@ Section interp. | |- context G [ofe_mor_car _ _ (get_fun _) (ofe_mor_car _ _ Fun ?f)] => set (fin := f) end. - trans (reify (gReifiers_sReifier CtxDep rs) + trans (reify (gReifiers_sReifier rs) (APP_CONT_ (Next (interp_val v env)) fin kk) - (gState_recomp CtxDep σr (sR_state (σ)))). + (gState_recomp σr (sR_state (σ)))). { repeat f_equiv. rewrite get_val_ITV. simpl. rewrite get_fun_fun. simpl. rewrite !hom_vis. f_equiv. subst kk. rewrite ccompose_id_l. intro. simpl. @@ -1035,8 +974,8 @@ Section interp. } f_equiv. by rewrite -!Tick_eq. - remember (map_meta_cont mk env) as σ. - trans (reify (gReifiers_sReifier CtxDep rs) (POP (interp_val v env)) - (gState_recomp CtxDep σr (sR_state (laterO_map (𝒫 ◎ interp_cont k env) :: σ)))). + trans (reify (gReifiers_sReifier rs) (POP (interp_val v env)) + (gState_recomp σr (sR_state (laterO_map (𝒫 ◎ interp_cont k env) :: σ)))). { do 2 f_equiv; last repeat f_equiv. apply get_val_ITV. @@ -1054,8 +993,8 @@ Section interp. } f_equiv. rewrite laterO_map_Next -Tick_eq. by f_equiv. - - trans (reify (gReifiers_sReifier CtxDep rs) (POP (interp_val v env)) - (gState_recomp CtxDep σr (sR_state []))). + - trans (reify (gReifiers_sReifier rs) (POP (interp_val v env)) + (gState_recomp σr (sR_state []))). { do 2 f_equiv; last first. { f_equiv. by rewrite map_meta_cont_nil. } @@ -1078,14 +1017,14 @@ Section interp. (** * SOUNDNESS *) Lemma soundness {S : Set} (env : interp_scope S) (C C' : config S) - (t t' : IT) (σ σ' : state) (σr : gState_rest CtxDep sR_idx rs ♯ IT) n nm : + (t t' : IT) (σ σ' : state) (σr : gState_rest sR_idx rs ♯ IT) n nm : steps C C' nm -> fst nm = n -> (interp_config C env) = (t, σ) -> (interp_config C' env) = (t', σ') -> - ssteps (gReifiers_sReifier CtxDep rs) - t (gState_recomp CtxDep σr (sR_state σ)) - t' (gState_recomp CtxDep σr (sR_state σ')) n. + ssteps (gReifiers_sReifier rs) + t (gState_recomp σr (sR_state σ)) + t' (gState_recomp σr (sR_state σ')) n. Proof. intros H. revert n t t' σ σ'. @@ -1100,11 +1039,11 @@ Section interp. specialize (interp_cred_no_reify_state env _ _ _ _ _ _ _ H0 Ht Heqc2) as <-; simpl in Heq|-*; rewrite Heq; eapply IHs]; try solve - [eapply ssteps_many with t2 (gState_recomp CtxDep σr (sR_state σ2)); last done; + [eapply ssteps_many with t2 (gState_recomp σr (sR_state σ2)); last done; specialize (interp_cred_yes_reify env _ _ _ _ _ _ σr _ H0 Ht Heqc2) as Heq; cbn in Ht; eapply sstep_reify; last done; inversion Ht; rewrite !hom_vis; done]. - + eapply ssteps_many with t2 (gState_recomp CtxDep σr (sR_state σ2)); last done. + + eapply ssteps_many with t2 (gState_recomp σr (sR_state σ2)); last done. specialize (interp_cred_no_reify env _ _ _ _ _ _ _ H0 Ht Heqc2) as Heq. specialize (interp_cred_no_reify_state env _ _ _ _ _ _ _ H0 Ht Heqc2) as <-. simpl in Heq|-*; rewrite Heq. constructor; eauto. @@ -1112,19 +1051,19 @@ Section interp. simpl in Heq|-*. change (2+n') with (1+(1+n')). eapply ssteps_many; last first. - * eapply ssteps_many with t2 (gState_recomp CtxDep σr (sR_state σ2)); last done. + * eapply ssteps_many with t2 (gState_recomp σr (sR_state σ2)); last done. eapply sstep_tick; reflexivity. * eapply sstep_reify; last apply Heq. cbn in Ht. inversion Ht. rewrite get_val_ITV. simpl. rewrite get_fun_fun. simpl. rewrite !hom_vis. done. - + eapply ssteps_many with t2 (gState_recomp CtxDep σr (sR_state σ2)); last done. + + eapply ssteps_many with t2 (gState_recomp σr (sR_state σ2)); last done. specialize (interp_cred_yes_reify env _ _ _ _ _ _ σr _ H0 Ht Heqc2) as Heq. cbn in Ht; inversion Ht. subst. rewrite get_val_ITV. simpl. eapply sstep_reify; simpl in Heq; last first. * rewrite -Heq. f_equiv. f_equiv. rewrite get_val_ITV. simpl. done. * f_equiv. reflexivity. - + eapply ssteps_many with t2 (gState_recomp CtxDep σr (sR_state σ2)); last done. + + eapply ssteps_many with t2 (gState_recomp σr (sR_state σ2)); last done. specialize (interp_cred_yes_reify env _ _ _ _ _ _ σr _ H0 Ht Heqc2) as Heq. cbn in Ht; inversion Ht. subst. rewrite get_val_ITV. simpl. eapply sstep_reify; simpl in Heq; last first. diff --git a/theories/examples/input_lang_delim/lang.v b/theories/examples/input_lang_delim/lang.v index 66aadb3..dbd9688 100644 --- a/theories/examples/input_lang_delim/lang.v +++ b/theories/examples/input_lang_delim/lang.v @@ -1,13 +1,7 @@ -From stdpp Require Export strings. From gitrees Require Export prelude. -(* From Equations Require Import Equations. *) -Require Import List. -Import ListNotations. Require Import Binding.Resolver Binding.Lib Binding.Set Binding.Auto Binding.Env. - -Require Import FunctionalExtensionality. - +(* Require Import FunctionalExtensionality. *) Variant nat_op := Add | Sub | Mult. @@ -23,8 +17,6 @@ Inductive expr {X : Set} := | NatOp (op : nat_op) (e₁ : expr) (e₂ : expr) : expr | If (e₁ : expr) (e₂ : expr) (e₃ : expr) : expr (* The effects *) -(* | Input : expr *) -(* | Output (e : expr) : expr *) | Shift (e : @expr (inc X)) : expr | Reset (e : expr) : expr with val {X : Set} := @@ -49,12 +41,8 @@ Arguments val X%bind : clear implicits. Arguments expr X%bind : clear implicits. Arguments cont X%bind : clear implicits. - - - Local Open Scope bind_scope. - Fixpoint emap {A B : Set} (f : A [→] B) (e : expr A) : expr B := match e with | Val v => Val (vmap f v) @@ -63,8 +51,6 @@ Fixpoint emap {A B : Set} (f : A [→] B) (e : expr A) : expr B := | AppCont e₁ e₂ => AppCont (emap f e₁) (emap f e₂) | NatOp o e₁ e₂ => NatOp o (emap f e₁) (emap f e₂) | If e₁ e₂ e₃ => If (emap f e₁) (emap f e₂) (emap f e₃) - (* | Input => Input *) - (* | Output e => Output (emap f e) *) | Shift e => Shift (emap (f ↑) e) | Reset e => Reset (emap f e) end @@ -102,8 +88,6 @@ Fixpoint ebind {A B : Set} (f : A [⇒] B) (e : expr A) : expr B := | AppCont e₁ e₂ => AppCont (ebind f e₁) (ebind f e₂) | NatOp o e₁ e₂ => NatOp o (ebind f e₁) (ebind f e₂) | If e₁ e₂ e₃ => If (ebind f e₁) (ebind f e₂) (ebind f e₃) - (* | Input => Input *) - (* | Output e => Output (ebind f e) *) | Shift e => Shift (ebind (f ↑) e) | Reset e => Reset (ebind f e) end @@ -306,27 +290,12 @@ Fixpoint fill {X : Set} (K : cont X) (e : expr X) : expr X := end. - -(* Lemma fill_emap {X Y : Set} (f : X [→] Y) (K : ectx X) (e : expr X) *) -(* : fmap f (fill K e) = fill (fmap f K) (fmap f e). *) -(* Proof. *) -(* revert f. *) -(* induction K as *) -(* [ | ?? IH | ?? IH | ?? IH | ??? IH | ???? IH *) -(* | ??? IH | ?? IH ]; *) -(* intros f; term_simpl; first done; rewrite IH; reflexivity. *) -(* Qed. *) - -(*** Operational semantics *) +(*** Continuation operations *) Global Instance fill_inj {S} (Ki : cont S) : Inj (=) (=) (fill Ki). Proof. induction Ki; intros ???; simplify_eq/=; auto with f_equal. Qed. -(* Lemma ctx_el_to_expr_val {S} C (e : expr S) : *) -(* is_Some (to_val (ctx_el_to_expr C e)) → is_Some (to_val e). *) -(* Proof. case : C => [] > H; simpl in H; try by apply is_Some_None in H. Qed. *) - Lemma fill_val {S} Ki (e : expr S) : is_Some (to_val (fill Ki e)) → is_Some (to_val e). Proof. @@ -334,12 +303,6 @@ Proof. apply H in H0; simpl in H0; contradiction (is_Some_None H0). Qed. -(* (* CHECK *) *) -(* Lemma val_head_stuck {S} (e1 : expr S) e2 K K' Ko m : *) -(* head_step e1 K e2 K' Ko m → to_val e1 = None. *) -(* Proof. destruct 1; naive_solver. Qed. *) - - (* K1 ∘ K2 *) Fixpoint cont_compose {S} (K1 K2 : cont S) : cont S := match K2 with @@ -353,7 +316,6 @@ Fixpoint cont_compose {S} (K1 K2 : cont S) : cont S := | NatOpRK op e K => NatOpRK op e (cont_compose K1 K) end. - Lemma fill_comp {S} (K1 K2 : cont S) e : fill (cont_compose K1 K2) e = fill K1 (fill K2 e). Proof. elim: K2 K1 e =>>; eauto; @@ -458,13 +420,6 @@ where "c ===> c' / nm" := (Cred c c' nm). Arguments Mcont S%bind : clear implicits. Arguments config S%bind : clear implicits. -(** ** On configs & meta-contexts *) - -Definition meta_fill {S} (mk : Mcont S) e := - fold_left (λ e k, fill k e) mk e. - - - Inductive steps {S} : config S -> config S -> (nat * nat) -> Prop := | steps_zero : forall c, steps c c (0,0) @@ -473,15 +428,8 @@ Inductive steps {S} : config S -> config S -> (nat * nat) -> Prop := steps c2 c3 (n',m') -> steps c1 c3 (n+n',m+m'). - -(* Lemma ceval_expr_to_val {S} : *) -(* forall (e : expr S) k mk, exists v nm, steps (Ceval e k mk) (Ceval v k mk) nm. *) -(* Proof. *) -(* intros. *) -(* induction 1; intros. *) -(* - exists (Val v), (0,0). constructor. *) -(* - *) - +Definition meta_fill {S} (mk : Mcont S) e := + fold_left (λ e k, fill k e) mk e. (*** Type system *) (* Type system from [Filinski, Danvy 89] : A Functional Abstraction of Typed Contexts *) @@ -564,6 +512,8 @@ Inductive ty := (* typed_val Γ (RecV e) (Tarr τ1 τ2) *) (* . *) +(*** Notations *) + Declare Scope syn_scope. Delimit Scope syn_scope with syn. diff --git a/theories/examples/input_lang_delim/logrel.v b/theories/examples/input_lang_delim/logrel.v index 6b03fa6..eb41879 100644 --- a/theories/examples/input_lang_delim/logrel.v +++ b/theories/examples/input_lang_delim/logrel.v @@ -1,5 +1,4 @@ (** Logical relation for adequacy for the IO lang *) -From Equations Require Import Equations. From gitrees Require Import gitree. From gitrees.examples.input_lang_callcc Require Import lang interp hom. Require Import gitrees.lang_generic. diff --git a/theories/gitree/greifiers.v b/theories/gitree/greifiers.v index 1e549a4..e1847c8 100644 --- a/theories/gitree/greifiers.v +++ b/theories/gitree/greifiers.v @@ -566,7 +566,12 @@ Arguments gReifiers_cons {_ _}. Arguments gReifiers_nil {_}. Arguments gReifiers_ops {_ _}. Arguments gReifiers_re {_ _}. +Arguments gState_rest {_ _}. +Arguments gState_recomp {_ _ _ _ _ _}. +Arguments gState_decomp {_ _} _ {_ _ _}. +Arguments gState_decomp' {_ _} _ {_ _ _}. Arguments gReifiers_state {_ _}. Arguments gReifiers_re_idx {_ _}. Arguments gReifiers_re_idx_type {_ _}. Arguments gReifiers_re_type {_ _}. +Arguments gReifiers_sReifier {_ _}. diff --git a/theories/gitree/weakestpre.v b/theories/gitree/weakestpre.v index 45d4d16..e6e343f 100644 --- a/theories/gitree/weakestpre.v +++ b/theories/gitree/weakestpre.v @@ -6,32 +6,32 @@ From gitrees.gitree Require Import core reify greifiers reductions. (** * Ghost state from gReifiers *) -Definition gReifiers_ucmra {n} (a : is_ctx_dep) (rs : gReifiers a n) +Definition gReifiers_ucmra {n} {a : is_ctx_dep} (rs : gReifiers a n) (X : ofe) `{!Cofe X} : ucmra := discrete_funUR (λ (i : fin n), optionUR (exclR (sReifier_state (rs !!! i) ♯ X))). (** The resource corresponding to the whole global state *) -Definition of_state {n} (a : is_ctx_dep) (rs : gReifiers a n) +Definition of_state {n} {a : is_ctx_dep} (rs : gReifiers a n) (X : ofe) `{!Cofe X} (st : gReifiers_state rs ♯ X) - : gReifiers_ucmra a rs X := - λ i, Excl' (fstO (gState_decomp a i st)). + : gReifiers_ucmra rs X := + λ i, Excl' (fstO (gState_decomp i st)). (** The resource corresponding to a speicific projection out of the global state *) -Definition of_idx {n} (a : is_ctx_dep) (rs : gReifiers a n) +Definition of_idx {n} {a : is_ctx_dep} (rs : gReifiers a n) (X : ofe) `{!Cofe X} (i : fin n) - (st : sReifier_state (rs !!! i) ♯ X) : gReifiers_ucmra a rs X. + (st : sReifier_state (rs !!! i) ♯ X) : gReifiers_ucmra rs X. Proof. simple refine (λ j, if (decide (j = i)) then _ else None). simpl. induction e. exact (Excl' st). Defined. -Lemma of_state_recomp_lookup_ne {n} (a : is_ctx_dep) (rs : gReifiers a n) +Lemma of_state_recomp_lookup_ne {n} {a : is_ctx_dep} (rs : gReifiers a n) (X : ofe) `{!Cofe X} i j (σ1 σ2 : sReifier_state (rs !!! i) ♯ X) rest : i ≠ j → - of_state a rs X (gState_recomp a rest σ1) j - ≡ of_state a rs X (gState_recomp a rest σ2) j. + of_state rs X (gState_recomp rest σ1) j + ≡ of_state rs X (gState_recomp rest σ2) j. Proof. intros Hij. revert σ1 σ2 rest. unfold of_state. @@ -50,11 +50,11 @@ Proof. Qed. Section ucmra. - Context {n : nat} (a : is_ctx_dep) (rs : gReifiers a n). + Context {n : nat} {a : is_ctx_dep} (rs : gReifiers a n). Context (X : ofe) `{!Cofe X}. - Notation gReifiers_ucmra := (gReifiers_ucmra a rs X). - Notation of_state := (of_state a rs X). - Notation of_idx := (of_idx a rs X). + Notation gReifiers_ucmra := (gReifiers_ucmra rs X). + Notation of_state := (of_state rs X). + Notation of_idx := (of_idx rs X). #[export] Instance of_state_ne : NonExpansive of_state. Proof. solve_proper. Qed. @@ -65,14 +65,14 @@ Section ucmra. Proof. intro; done. Qed. Lemma of_state_recomp_lookup i (σ : sReifier_state (rs !!! i) ♯ X) rest : - of_state (gState_recomp a rest σ) i ≡ Excl' σ. + of_state (gState_recomp rest σ) i ≡ Excl' σ. Proof. unfold of_state. rewrite gState_decomp_recomp. done. Qed. Lemma of_state_decomp_local_update i (σ σ1 σ2 : sReifier_state (rs !!! i) ♯ X) rest : - (of_state (gState_recomp a rest σ1), of_idx i σ2) - ~l~> (of_state (gState_recomp a rest σ), of_idx i σ). + (of_state (gState_recomp rest σ1), of_idx i σ2) + ~l~> (of_state (gState_recomp rest σ), of_idx i σ). Proof. apply discrete_fun_local_update. intros j. @@ -88,7 +88,7 @@ Section ucmra. Qed. Lemma of_state_of_idx_agree i σ1 σ2 rest f Σ : - of_state (gState_recomp a rest σ1) ≡ of_idx i σ2 ⋅ f ⊢@{iProp Σ} σ1 ≡ σ2. + of_state (gState_recomp rest σ1) ≡ of_idx i σ2 ⋅ f ⊢@{iProp Σ} σ1 ≡ σ2. Proof. iIntros "Hs". rewrite discrete_fun_equivI. @@ -106,16 +106,16 @@ Section ucmra. End ucmra. Section weakestpre. - Context {n : nat} (a : is_ctx_dep) (rs : gReifiers a n) {A} `{!Cofe A}. - Notation rG := (gReifiers_sReifier a rs). + Context {n : nat} {a : is_ctx_dep} (rs : gReifiers a n) {A} `{!Cofe A}. + Notation rG := (gReifiers_sReifier rs). Notation F := (sReifier_ops rG). Notation IT := (IT F A). Notation ITV := (ITV F A). Notation stateF := (gReifiers_state rs). Notation stateO := (stateF ♯ IT). - Notation stateR := (gReifiers_ucmra a rs IT). - Let of_state := (of_state a rs IT). - Let of_idx := (of_idx a rs IT). + Notation stateR := (gReifiers_ucmra rs IT). + Let of_state := (of_state rs IT). + Let of_idx := (of_idx rs IT). Notation reify := (reify rG). Notation istep := (istep rG). Notation isteps := (isteps rG). @@ -164,8 +164,8 @@ Section weakestpre. Lemma state_interp_has_state_idx_agree (i : fin n) (σ1 σ2 : sReifier_state (rs !!! i) ♯ IT) - (rest : gState_rest a i rs ♯ IT) `{!stateG Σ} : - state_interp (gState_recomp a rest σ1) -∗ has_state_idx i σ2 -∗ σ1 ≡ σ2. + (rest : gState_rest i rs ♯ IT) `{!stateG Σ} : + state_interp (gState_recomp rest σ1) -∗ has_state_idx i σ2 -∗ σ1 ≡ σ2. Proof. iIntros "H1 H2". iDestruct (own_valid_2 with "H1 H2") as "Hs". @@ -177,14 +177,14 @@ Section weakestpre. Lemma state_interp_has_state_idx_update (i : fin n) (σ σ1 σ2 : sReifier_state (rs !!! i) ♯ IT) - (rest : gState_rest a i rs ♯ IT) `{!stateG Σ} : - state_interp (gState_recomp a rest σ1) -∗ has_state_idx i σ2 ==∗ - state_interp (gState_recomp a rest σ) ∗ has_state_idx i σ. + (rest : gState_rest i rs ♯ IT) `{!stateG Σ} : + state_interp (gState_recomp rest σ1) -∗ has_state_idx i σ2 ==∗ + state_interp (gState_recomp rest σ) ∗ has_state_idx i σ. Proof. iIntros "H1 H2". iMod (own_update_2 with "H1 H2") as "H". { apply auth_update. - apply (of_state_decomp_local_update a _ _ _ σ). } + apply (of_state_decomp_local_update _ _ _ σ). } iDestruct "H" as "[$ $]". done. Qed. @@ -407,8 +407,8 @@ Section weakestpre. forall (x : Ins (F op) ♯ IT) (k : Outs (F op) ♯ IT -n> laterO IT), (|={E1,E2}=> ∃ σ σ' β, has_state_idx i σ ∗ - ∀ rest, reify (Vis op x k) (gState_recomp a rest σ) - ≡ (gState_recomp a rest σ', Tick β) ∗ + ∀ rest, reify (Vis op x k) (gState_recomp rest σ) + ≡ (gState_recomp rest σ', Tick β) ∗ ▷ (£ 1 -∗ has_state_idx i σ' -∗ |={E2,E1}=> WP β @ s;E1 {{ Φ }})) -∗ WP (Vis op x k) @ s;E1 {{ Φ }}. Proof. @@ -418,8 +418,8 @@ Section weakestpre. iRight. iSplit. { iPureIntro. apply IT_to_V_Vis. } iIntros (fs) "Hgst". - destruct (gState_decomp a i fs) as [σ0 rest] eqn:Hdecomp. - assert (fs ≡ gState_recomp a rest σ0) as Hfs. + destruct (gState_decomp i fs) as [σ0 rest] eqn:Hdecomp. + assert (fs ≡ gState_recomp rest σ0) as Hfs. { symmetry. apply gState_recomp_decomp. by rewrite Hdecomp. } iMod "H" as (σ σ' β) "[Hlst H]". @@ -434,10 +434,10 @@ Section weakestpre. iSplit. { (* it is safe *) iLeft. - iExists β,(gState_recomp a rest σ'). iRight. - iExists op,x,k; eauto. } + iExists β, (gState_recomp rest σ'). iRight. + iExists op, x, k; eauto. } iIntros (fs' α0) "Hst Hlc". rewrite istep_vis. - iAssert (gState_recomp a rest σ' ≡ fs' ∧ Tick β ≡ Tick α0)%I + iAssert (gState_recomp rest σ' ≡ fs' ∧ Tick β ≡ Tick α0)%I with "[Hreify Hst]" as "[Hst Hb]". { iRewrite "Hreify" in "Hst". by rewrite prod_equivI. } @@ -453,7 +453,7 @@ Section weakestpre. Lemma wp_reify E1 s Φ i (lop : opid (sReifier_ops (rs !!! i))) x k σ σ' β : let op : opid F := (existT i lop) in - (∀ rest, reify (Vis op x k) (gState_recomp a rest σ) ≡ (gState_recomp a rest σ', Tick β)) → + (∀ rest, reify (Vis op x k) (gState_recomp rest σ) ≡ (gState_recomp rest σ', Tick β)) → has_state_idx i σ -∗ ▷ (£ 1 -∗ has_state_idx i σ' -∗ WP β @ s;E1 {{ Φ }}) -∗ WP (Vis op x k) @ s;E1 {{ Φ }}. @@ -667,21 +667,20 @@ End weakestpre. Section weakestpre_specific. Context {n : nat} {A} `{!Cofe A}. - Notation rG a rs := (gReifiers_sReifier (n := n) a rs). - Notation F a rs := (sReifier_ops (rG a rs)). - Notation IT a rs := (IT (F a rs) A). - Notation ITV a rs := (ITV (F a rs) A). - Notation stateF a rs := (gReifiers_state a rs). - Notation stateO a rs := (stateF a rs ♯ IT a rs). - Notation stateR a rs := (gReifiers_ucmra a rs (IT a rs)). - Let of_state a rs := (of_state a rs (IT a rs)). - Let of_idx a rs := (of_idx a rs (IT a rs)). - Notation reify a rs := (reify (rG a rs)). - Notation istep a rs := (istep (rG a rs)). - Notation isteps a rs := (isteps (rG a rs)). - Notation sstep a rs := (sstep (rG a rs)). - Notation ssteps a rs := (ssteps (rG a rs)). - Notation wp a rs := (wp a rs). + Notation rG rs := (gReifiers_sReifier (n := n) rs). + Notation F rs := (sReifier_ops (rG rs)). + Notation IT rs := (IT (F rs) A). + Notation ITV rs := (ITV (F rs) A). + Notation stateF rs := (gReifiers_state rs). + Notation stateO rs := (stateF rs ♯ IT rs). + Notation stateR rs := (gReifiers_ucmra rs (IT rs)). + Let of_state {a} rs := (of_state (a:=a) rs (IT rs)). + Let of_idx {a} rs := (of_idx (a:=a) rs (IT rs)). + Notation reify rs := (reify (rG rs)). + Notation istep rs := (istep (rG rs)). + Notation isteps rs := (isteps (rG rs)). + Notation sstep rs := (sstep (rG rs)). + Notation ssteps rs := (ssteps (rG rs)). Context `{!invGS Σ}. Notation iProp := (iProp Σ). @@ -690,15 +689,15 @@ Section weakestpre_specific. Lemma wp_reify_idx_ctx_dep (rs : gReifiers CtxDep n) `{!@stateG _ CtxDep rs A _ Σ} E1 E2 s Φ i (lop : opid (sReifier_ops (rs !!! i))) : - let op : opid (F CtxDep rs) := (existT i lop) in - forall (x : Ins (F CtxDep rs op) ♯ IT CtxDep rs) - (k : Outs (F CtxDep rs op) ♯ IT CtxDep rs -n> laterO (IT CtxDep rs)), + let op : opid (F rs) := (existT i lop) in + forall (x : Ins (F rs op) ♯ IT rs) + (k : Outs (F rs op) ♯ IT rs -n> laterO (IT rs)), (|={E1,E2}=> - ∃ σ y σ' β, has_state_idx CtxDep rs i σ + ∃ σ y σ' β, has_state_idx rs i σ ∗ sReifier_re (rs !!! i) lop (x, σ, k) ≡ Some (y, σ') ∗ y ≡ Next β - ∗ ▷ (£ 1 -∗ has_state_idx CtxDep rs i σ' ={E2,E1}=∗ wp CtxDep rs β s E1 Φ)) - -∗ wp CtxDep rs (Vis op x k) s E1 Φ. + ∗ ▷ (£ 1 -∗ has_state_idx rs i σ' ={E2,E1}=∗ wp rs β s E1 Φ)) + -∗ wp rs (Vis op x k) s E1 Φ. Proof. intros op x k. iIntros "H". @@ -708,13 +707,13 @@ Section weakestpre_specific. iFrame "Hlst". iIntros (rest). iFrame "H". - iAssert (gReifiers_re rs _ _ op (x, gState_recomp CtxDep rest σ, _) - ≡ Some (y, gState_recomp CtxDep rest σ'))%I + iAssert (gReifiers_re rs _ _ op (x, gState_recomp rest σ, _) + ≡ Some (y, gState_recomp rest σ'))%I with "[Hreify]" as "Hgreify". { rewrite (@gReifiers_re_idx _ CtxDep). - iAssert (optionO_map (prodO_map idfun (gState_recomp CtxDep rest)) + iAssert (optionO_map (prodO_map idfun (gState_recomp rest)) (sReifier_re (rs !!! i) lop (x, σ, k)) - ≡ optionO_map (prodO_map idfun (gState_recomp CtxDep rest)) + ≡ optionO_map (prodO_map idfun (gState_recomp rest)) (Some (y, σ')))%I with "[Hreify]" as "H". - iApply (f_equivI with "Hreify"). - simpl. iExact "H". @@ -727,14 +726,14 @@ Section weakestpre_specific. Lemma wp_reify_idx_ctx_indep (rs : gReifiers NotCtxDep n) `{!@stateG _ NotCtxDep rs A _ Σ} E1 E2 s Φ i (lop : opid (sReifier_ops (rs !!! i))) : - let op : opid (F NotCtxDep rs) := (existT i lop) in - forall (x : Ins (F NotCtxDep rs op) ♯ IT NotCtxDep rs) - (k : Outs (F NotCtxDep rs op) ♯ IT NotCtxDep rs -n> laterO (IT NotCtxDep rs)), - (|={E1,E2}=> ∃ σ y σ' β, has_state_idx NotCtxDep rs i σ + let op : opid (F rs) := (existT i lop) in + forall (x : Ins (F rs op) ♯ IT rs) + (k : Outs (F rs op) ♯ IT rs -n> laterO (IT rs)), + (|={E1,E2}=> ∃ σ y σ' β, has_state_idx rs i σ ∗ sReifier_re (rs !!! i) lop (x, σ) ≡ Some (y, σ') ∗ k y ≡ Next β - ∗ ▷ (£ 1 -∗ has_state_idx NotCtxDep rs i σ' ={E2,E1}=∗ wp NotCtxDep rs β s E1 Φ)) - -∗ wp NotCtxDep rs (Vis op x k) s E1 Φ. + ∗ ▷ (£ 1 -∗ has_state_idx rs i σ' ={E2,E1}=∗ wp rs β s E1 Φ)) + -∗ wp rs (Vis op x k) s E1 Φ. Proof. intros op x k. iIntros "H". @@ -744,16 +743,16 @@ Section weakestpre_specific. iFrame "Hlst". iIntros (rest). iFrame "H". - iAssert (@gReifiers_re _ NotCtxDep rs _ _ op (x, gState_recomp NotCtxDep rest σ) - ≡ Some (y, gState_recomp NotCtxDep rest σ'))%I + iAssert (@gReifiers_re _ NotCtxDep rs _ _ op (x, gState_recomp rest σ) + ≡ Some (y, gState_recomp rest σ'))%I with "[Hreify]" as "Hgreify". - { pose proof (@gReifiers_re_idx n NotCtxDep i rs (IT NotCtxDep rs)) as J. + { pose proof (@gReifiers_re_idx n NotCtxDep i rs (IT rs)) as J. simpl in J. simpl. rewrite J; clear J. - iAssert (optionO_map (prodO_map idfun (gState_recomp NotCtxDep rest)) + iAssert (optionO_map (prodO_map idfun (gState_recomp rest)) (sReifier_re (rs !!! i) lop (x, σ)) - ≡ optionO_map (prodO_map idfun (gState_recomp NotCtxDep rest)) + ≡ optionO_map (prodO_map idfun (gState_recomp rest)) (Some (y, σ')))%I with "[Hreify]" as "H". - iApply (f_equivI with "Hreify"). - simpl. iExact "H". @@ -765,13 +764,13 @@ Section weakestpre_specific. Lemma wp_subreify_ctx_dep' (rs : gReifiers CtxDep n) `{!@stateG _ CtxDep rs A _ Σ} E1 E2 s Φ sR `{!subReifier sR rs} - (op : opid (sReifier_ops sR)) (x : Ins (sReifier_ops sR op) ♯ (IT CtxDep rs)) - (k : Outs (F CtxDep rs (subEff_opid op)) ♯ IT CtxDep rs -n> laterO (IT CtxDep rs)) : - (|={E1,E2}=> ∃ σ y σ' β, has_substate CtxDep rs σ ∗ + (op : opid (sReifier_ops sR)) (x : Ins (sReifier_ops sR op) ♯ (IT rs)) + (k : Outs (F rs (subEff_opid op)) ♯ IT rs -n> laterO (IT rs)) : + (|={E1,E2}=> ∃ σ y σ' β, has_substate rs σ ∗ sReifier_re sR op (x, σ, (k ◎ subEff_outs)) ≡ Some (y, σ') ∗ y ≡ Next β - ∗ ▷ (£ 1 -∗ has_substate CtxDep rs σ' ={E2,E1}=∗ wp CtxDep rs β s E1 Φ)) - -∗ wp CtxDep rs (Vis (subEff_opid op) (subEff_ins x) k) s E1 Φ. + ∗ ▷ (£ 1 -∗ has_substate rs σ' ={E2,E1}=∗ wp rs β s E1 Φ)) + -∗ wp rs (Vis (subEff_opid op) (subEff_ins x) k) s E1 Φ. Proof. iIntros "H". iApply wp_reify_idx_ctx_dep. @@ -791,13 +790,13 @@ Section weakestpre_specific. Lemma wp_subreify_ctx_indep' (rs : gReifiers NotCtxDep n) `{!@stateG _ NotCtxDep rs A _ Σ} E1 E2 s Φ sR `{!subReifier sR rs} - (op : opid (sReifier_ops sR)) (x : Ins (sReifier_ops sR op) ♯ (IT NotCtxDep rs)) - (k : Outs (F NotCtxDep rs (subEff_opid op)) ♯ IT NotCtxDep rs -n> laterO (IT NotCtxDep rs)) : - (|={E1,E2}=> ∃ σ y σ' β, has_substate NotCtxDep rs σ ∗ + (op : opid (sReifier_ops sR)) (x : Ins (sReifier_ops sR op) ♯ (IT rs)) + (k : Outs (F rs (subEff_opid op)) ♯ IT rs -n> laterO (IT rs)) : + (|={E1,E2}=> ∃ σ y σ' β, has_substate rs σ ∗ sReifier_re sR op (x, σ) ≡ Some (y, σ') ∗ k (subEff_outs y) ≡ Next β - ∗ ▷ (£ 1 -∗ has_substate NotCtxDep rs σ' ={E2,E1}=∗ wp NotCtxDep rs β s E1 Φ)) - -∗ wp NotCtxDep rs (Vis (subEff_opid op) (subEff_ins x) k) s E1 Φ. + ∗ ▷ (£ 1 -∗ has_substate rs σ' ={E2,E1}=∗ wp rs β s E1 Φ)) + -∗ wp rs (Vis (subEff_opid op) (subEff_ins x) k) s E1 Φ. Proof. iIntros "H". iApply wp_reify_idx_ctx_indep. @@ -811,15 +810,15 @@ Section weakestpre_specific. Lemma wp_subreify_ctx_dep (rs : gReifiers CtxDep n) `{!@stateG _ CtxDep rs A _ Σ} E1 s Φ sR `{!subReifier sR rs} (op : opid (sReifier_ops sR)) - (x : Ins (sReifier_ops sR op) ♯ IT CtxDep rs) (y : laterO (IT CtxDep rs)) - (k : Outs (F CtxDep rs (subEff_opid op)) ♯ IT CtxDep rs -n> laterO (IT CtxDep rs)) - (σ σ' : sReifier_state sR ♯ IT CtxDep rs) β : + (x : Ins (sReifier_ops sR op) ♯ IT rs) (y : laterO (IT rs)) + (k : Outs (F rs (subEff_opid op)) ♯ IT rs -n> laterO (IT rs)) + (σ σ' : sReifier_state sR ♯ IT rs) β : sReifier_re sR op (x, σ, (k ◎ subEff_outs)) ≡ Some (y, σ') → y ≡ Next β → - has_substate CtxDep rs σ -∗ - ▷ (£ 1 -∗ has_substate CtxDep rs σ' -∗ wp CtxDep rs β s E1 Φ) + has_substate rs σ -∗ + ▷ (£ 1 -∗ has_substate rs σ' -∗ wp rs β s E1 Φ) -∗ - wp CtxDep rs (Vis (subEff_opid op) (subEff_ins x) k) s E1 Φ. + wp rs (Vis (subEff_opid op) (subEff_ins x) k) s E1 Φ. Proof. intros HSR Hk. iIntros "Hlst H". @@ -828,7 +827,7 @@ Section weakestpre_specific. rewrite Tick_eq. rewrite -Hk. rewrite reify_vis_eq_ctx_dep //. pose proof (@subReifier_reify n CtxDep sR rs _ - (IT CtxDep rs) _ op x y (k ◎ subEff_outs) σ σ' rest) as H'. + (IT rs) _ op x y (k ◎ subEff_outs) σ σ' rest) as H'. simpl in H'. rewrite <-H'. - simpl. @@ -845,16 +844,16 @@ Section weakestpre_specific. Lemma wp_subreify_ctx_indep (rs : gReifiers NotCtxDep n) `{!@stateG _ NotCtxDep rs A _ Σ} E1 s Φ sR `{!subReifier sR rs} (op : opid (sReifier_ops sR)) - (x : Ins (sReifier_ops sR op) ♯ IT NotCtxDep rs) - (y : Outs (sReifier_ops sR op) ♯ IT NotCtxDep rs) - (k : Outs (F NotCtxDep rs (subEff_opid op)) ♯ IT NotCtxDep rs -n> laterO (IT NotCtxDep rs)) - (σ σ' : sReifier_state sR ♯ IT NotCtxDep rs) β : + (x : Ins (sReifier_ops sR op) ♯ IT rs) + (y : Outs (sReifier_ops sR op) ♯ IT rs) + (k : Outs (F rs (subEff_opid op)) ♯ IT rs -n> laterO (IT rs)) + (σ σ' : sReifier_state sR ♯ IT rs) β : sReifier_re sR op (x, σ) ≡ Some (y, σ') → k (subEff_outs y) ≡ Next β → - has_substate NotCtxDep rs σ -∗ - ▷ (£ 1 -∗ has_substate NotCtxDep rs σ' -∗ wp NotCtxDep rs β s E1 Φ) + has_substate rs σ -∗ + ▷ (£ 1 -∗ has_substate rs σ' -∗ wp rs β s E1 Φ) -∗ - wp NotCtxDep rs (Vis (subEff_opid op) (subEff_ins x) k) s E1 Φ. + wp rs (Vis (subEff_opid op) (subEff_ins x) k) s E1 Φ. Proof. intros HSR Hk. iIntros "Hlst H". @@ -869,26 +868,26 @@ End weakestpre_specific. Section weakestpre_bind. Context {n : nat} (rs : gReifiers NotCtxDep n) {A} `{!Cofe A}. - Notation rG := (gReifiers_sReifier NotCtxDep rs). + Notation rG := (gReifiers_sReifier rs). Notation F := (sReifier_ops rG). Notation IT := (IT F A). Notation ITV := (ITV F A). - Notation stateF := (gReifiers_state NotCtxDep rs). + Notation stateF := (gReifiers_state rs). Notation stateO := (stateF ♯ IT). - Notation stateR := (gReifiers_ucmra NotCtxDep rs IT). - Let of_state := (of_state NotCtxDep rs IT). - Let of_idx := (of_idx NotCtxDep rs IT). + Notation stateR := (gReifiers_ucmra rs IT). + Let of_state := (of_state rs IT). + Let of_idx := (of_idx rs IT). Notation reify := (reify rG). Notation istep := (istep rG). Notation isteps := (isteps rG). Notation sstep := (sstep rG). Notation ssteps := (ssteps rG). - Notation wp := (wp NotCtxDep rs). + Notation wp := (wp rs). Implicit Type op : opid F. Implicit Type α β : IT. - Context `{!invGS Σ} `{!@stateG _ NotCtxDep rs A _ Σ}. + Context `{!invGS Σ} `{!stateG rs (A:=A) Σ}. Notation iProp := (iProp Σ). Notation coPsetO := (leibnizO coPset). @@ -905,7 +904,7 @@ Section weakestpre_bind. assert (NonExpansive (λ βv0, WP f (IT_of_V βv0) @ s;E1 {{ βv1, Φ βv1 }})%I). { solve_proper. } iIntros "H". iLöb as "IH" forall (α). - rewrite (wp_unfold _ _ (f _)). + rewrite (wp_unfold _ (f _)). destruct (IT_to_V (f α)) as [βv|] eqn:Hfa. - iLeft. iExists βv. iSplit; first done. assert (is_Some (IT_to_V α)) as [αv Ha]. @@ -999,7 +998,7 @@ Notation "'WP@{' re } α {{ Φ } }" := Lemma wp_adequacy cr Σ `{!invGpreS Σ} n a (rs : gReifiers a n) {A} `{!Cofe A} `{!statePreG rs A Σ} (α : IT _ A) σ βv σ' s k (ψ : (ITV (gReifiers_ops rs) A) → Prop) : - ssteps (gReifiers_sReifier a rs) α σ (IT_of_V βv) σ' k → + ssteps (gReifiers_sReifier rs) α σ (IT_of_V βv) σ' k → (∀ `{H1 : !invGS Σ} `{H2: !stateG rs A Σ}, ∃ Φ, NonExpansive Φ ∧ (∀ βv, Φ βv ⊢ ⌜ψ βv⌝) ∧ (£ cr ∗ has_full_state σ ⊢ WP@{rs} α @ s {{ Φ }})%I) → @@ -1010,7 +1009,7 @@ Proof. { intros HH. eapply uPred.pure_soundness; eauto. } eapply (step_fupdN_soundness_lc _ 0 (cr + 3*k)). intros Hinv. iIntros "[Hcr Hlc]". - iMod (new_state_interp a rs σ) as (sg) "[Hs Hs2]". + iMod (new_state_interp rs σ) as (sg) "[Hs Hs2]". destruct (Hprf Hinv sg) as (Φ & HΦ & HΦψ & Hprf'). iPoseProof (Hprf' with "[$Hcr $Hs2]") as "Hic". iPoseProof (wp_ssteps with "[$Hs $Hic]") as "Hphi". @@ -1026,16 +1025,16 @@ Lemma wp_safety cr Σ `{!invGpreS Σ} n a (rs : gReifiers a n) {A} `{!Cofe A} `{!statePreG rs A Σ} s k (α β : IT (gReifiers_ops rs) A) (σ σ' : gReifiers_state rs ♯ IT (gReifiers_ops rs) A) : (∀ Σ P Q, @disjunction_property Σ P Q) → - ssteps (gReifiers_sReifier a rs) α σ β σ' k → + ssteps (gReifiers_sReifier rs) α σ β σ' k → IT_to_V β ≡ None → (∀ `{H1 : !invGS_gen HasLc Σ} `{H2: !stateG rs A Σ}, ∃ Φ, NonExpansive Φ ∧ (£ cr ∗ has_full_state σ ⊢ WP@{rs} α @ s {{ Φ }})%I) → - ((∃ β1 σ1, sstep (gReifiers_sReifier a rs) β σ' β1 σ1) + ((∃ β1 σ1, sstep (gReifiers_sReifier rs) β σ' β1 σ1) ∨ (∃ e, β ≡ Err e ∧ s e)). Proof. Opaque istep. intros Hdisj Hstep Hbv Hwp. - cut (⊢@{iProp Σ} (∃ β1 σ1, istep (gReifiers_sReifier a rs) β σ' β1 σ1) + cut (⊢@{iProp Σ} (∃ β1 σ1, istep (gReifiers_sReifier rs) β σ' β1 σ1) ∨ (∃ e, β ≡ Err e ∧ ⌜s e⌝))%I. { intros [Hprf | Hprf]%Hdisj. - left. @@ -1069,7 +1068,7 @@ Proof. iApply (IT_vis_err_ne with "Ha"). } eapply (step_fupdN_soundness_lc _ 0 (cr + (3*k+2))). intros Hinv. iIntros "[Hcr Hlc]". - iMod (new_state_interp a rs σ) as (sg) "[Hs Hs2]". + iMod (new_state_interp rs σ) as (sg) "[Hs Hs2]". destruct (Hwp Hinv sg) as (Φ & HΦ & Hprf'). iPoseProof (Hprf' with "[$Hs2 $Hcr]") as "Hic". iPoseProof (wp_ssteps_isafe with "[$Hs $Hic]") as "H". diff --git a/theories/lib/factorial.v b/theories/lib/factorial.v index 3d8b324..c85c4be 100644 --- a/theories/lib/factorial.v +++ b/theories/lib/factorial.v @@ -111,7 +111,7 @@ Section fact. iIntros (ℓ) "Hl". simpl. iApply wp_seq. { solve_proper. } - iApply (wp_wand _ _ (λ _, pointsto acc (Ret $ fact n)) with "[-]"); last first. + iApply (wp_wand _ (λ _, pointsto acc (Ret $ fact n)) with "[-]"); last first. { simpl. iIntros (_) "Hacc". iModIntro. iApply (wp_read with "Hctx Hacc"). iNext. iNext. iIntros "Hacc".