From 15dc2a2a569306f80383caeb3f68e6f091efce32 Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Tue, 27 Feb 2024 14:12:00 +0100 Subject: [PATCH] factor out the IO tape effects --- _CoqProject | 14 +- theories/effects/io_tape.v | 144 +++++++++ theories/effects/store.v | 1 + theories/examples/affine_lang/lang.v | 2 +- theories/examples/affine_lang/logrel1.v | 6 +- theories/examples/affine_lang/logrel2.v | 2 +- theories/examples/input_lang/interp.v | 127 +------- theories/examples/input_lang/lang.v | 17 +- theories/examples/input_lang_callcc/hom.v | 3 +- theories/examples/input_lang_callcc/interp.v | 299 ++++++++----------- theories/examples/input_lang_callcc/lang.v | 18 +- theories/examples/input_lang_callcc/logrel.v | 96 +++--- theories/gitree/greifiers.v | 11 + 13 files changed, 344 insertions(+), 396 deletions(-) create mode 100644 theories/effects/io_tape.v diff --git a/_CoqProject b/_CoqProject index f470788..2337a45 100644 --- a/_CoqProject +++ b/_CoqProject @@ -28,6 +28,13 @@ theories/gitree.v theories/program_logic.v +theories/effects/store.v +theories/effects/io_tape.v + +theories/lib/pairs.v +theories/lib/while.v +theories/lib/factorial.v +theories/lib/iter.v theories/examples/delim_lang/lang.v theories/examples/delim_lang/interp.v @@ -47,11 +54,4 @@ theories/examples/affine_lang/lang.v theories/examples/affine_lang/logrel1.v theories/examples/affine_lang/logrel2.v -theories/effects/store.v - -theories/lib/pairs.v -theories/lib/while.v -theories/lib/factorial.v -theories/lib/iter.v - theories/utils/finite_sets.v diff --git a/theories/effects/io_tape.v b/theories/effects/io_tape.v new file mode 100644 index 0000000..fd34746 --- /dev/null +++ b/theories/effects/io_tape.v @@ -0,0 +1,144 @@ +(** I/O on a tape effect *) +From gitrees Require Import prelude gitree. + +Record state := State { + inputs : list nat; + outputs : list nat; + }. +#[export] Instance state_inhabited : Inhabited state := populate (State [] []). + +Definition update_input (s : state) : nat * state := + match s.(inputs) with + | [] => (0, s) + | n::ns => + (n, {| inputs := ns; outputs := s.(outputs) |}) + end. +Definition update_output (n:nat) (s : state) : state := + {| inputs := s.(inputs); outputs := n::s.(outputs) |}. + +Notation stateO := (leibnizO state). + +Program Definition inputE : opInterp := + {| + Ins := unitO; + Outs := natO; + |}. + +Program Definition outputE : opInterp := + {| + Ins := natO; + Outs := unitO; + |}. + +Definition ioE := @[inputE;outputE]. + +(* INPUT *) +Definition reify_input X `{Cofe X} : unitO * stateO → + option (natO * stateO) := + λ '(o, σ), Some (update_input σ : prodO natO stateO). +#[export] Instance reify_input_ne X `{Cofe X} : + NonExpansive (reify_input X). +Proof. + intros ?[[]][[]][_?]. simpl in *. f_equiv. + repeat f_equiv. done. +Qed. + +(* OUTPUT *) +Definition reify_output X `{Cofe X} : (natO * stateO) → + option (unitO * stateO) := + λ '(n, σ), Some((), update_output n σ : stateO). +#[export] Instance reify_output_ne X `{Cofe X} : + NonExpansive (reify_output X). +Proof. + intros ?[][][]. simpl in *. + repeat f_equiv; done. +Qed. + +Canonical Structure reify_io : sReifier NotCtxDep. +Proof. + simple refine {| sReifier_ops := ioE; + sReifier_state := stateO + |}. + intros X HX op. + destruct op as [[] | [ | []]]; simpl. + - simple refine (OfeMor (reify_input X)). + - simple refine (OfeMor (reify_output X)). +Defined. + +Section constructors. + Context {E : opsInterp} {A} `{!Cofe A}. + Context {subEff0 : subEff ioE E}. + Context {subOfe0 : SubOfe natO A}. + Notation IT := (IT E A). + Notation ITV := (ITV E A). + + Program Definition INPUT : (nat -n> IT) -n> IT := λne k, Vis (E:=E) (subEff_opid (inl ())) + (subEff_ins (F:=ioE) (op:=(inl ())) ()) + (NextO ◎ k ◎ (subEff_outs (F:=ioE) (op:=(inl ())))^-1). + Solve Obligations with solve_proper. + Program Definition OUTPUT_ : nat -n> IT -n> IT := + λne m α, Vis (E:=E) (subEff_opid (inr (inl ()))) + (subEff_ins (F:=ioE) (op:=(inr (inl ()))) m) + (λne _, NextO α). + Solve All Obligations with solve_proper_please. + Program Definition OUTPUT : nat -n> IT := λne m, OUTPUT_ m (Ret 0). + + Lemma hom_INPUT k f `{!IT_hom f} : f (INPUT k) ≡ INPUT (OfeMor f ◎ k). + Proof. + unfold INPUT. + rewrite hom_vis/=. repeat f_equiv. + intro x. cbn-[laterO_map]. rewrite laterO_map_Next. + done. + Qed. + Lemma hom_OUTPUT_ m α f `{!IT_hom f} : f (OUTPUT_ m α) ≡ OUTPUT_ m (f α). + Proof. + unfold OUTPUT. + rewrite hom_vis/=. repeat f_equiv. + intro x. cbn-[laterO_map]. rewrite laterO_map_Next. + done. + Qed. + +End constructors. + +Section weakestpre. + Context {sz : nat}. + Variable (rs : gReifiers NotCtxDep sz). + Context {subR : subReifier reify_io rs}. + Notation F := (gReifiers_ops rs). + Context {R} `{!Cofe R}. + Context `{!SubOfe natO R}. + Notation IT := (IT F R). + Notation ITV := (ITV F R). + Context `{!invGS Σ, !stateG rs R Σ}. + Notation iProp := (iProp Σ). + + Lemma wp_input (σ σ' : stateO) (n : nat) (k : natO -n> IT) Φ s : + update_input σ = (n, σ') → + has_substate σ -∗ + ▷ (£ 1 -∗ has_substate σ' -∗ WP@{rs} (k n) @ s {{ Φ }}) -∗ + WP@{rs} (INPUT k) @ s {{ Φ }}. + Proof. + intros Hs. iIntros "Hs Ha". + unfold INPUT. simpl. + iApply (wp_subreify_ctx_indep with "Hs"). + { simpl. rewrite Hs//=. } + { simpl. by rewrite ofe_iso_21. } + iModIntro. done. + Qed. + + Lemma wp_output (σ σ' : stateO) (n : nat) Φ s : + update_output n σ = σ' → + has_substate σ -∗ + ▷ (£ 1 -∗ has_substate σ' -∗ Φ (RetV 0)) -∗ + WP@{rs} (OUTPUT n) @ s {{ Φ }}. + Proof. + intros Hs. iIntros "Hs Ha". + unfold OUTPUT. simpl. + iApply (wp_subreify_ctx_indep rs with "Hs"). + { simpl. by rewrite Hs. } + { simpl. done. } + iModIntro. iIntros "H1 H2". + iApply wp_val. by iApply ("Ha" with "H1 H2"). + Qed. + +End weakestpre. diff --git a/theories/effects/store.v b/theories/effects/store.v index a7deb17..f11e23e 100644 --- a/theories/effects/store.v +++ b/theories/effects/store.v @@ -1,3 +1,4 @@ +(** Higher-order store effect *) From iris.algebra Require Import gmap excl auth gmap_view. From iris.proofmode Require Import classes tactics. From iris.base_logic Require Import algebra. diff --git a/theories/examples/affine_lang/lang.v b/theories/examples/affine_lang/lang.v index 14cdcb9..6076ca1 100644 --- a/theories/examples/affine_lang/lang.v +++ b/theories/examples/affine_lang/lang.v @@ -7,7 +7,7 @@ Require Import Binding.Resolver Binding.Lib Binding.Set Binding.Auto Binding.Env (* for namespace sake *) Module io_lang. - Definition state := input_lang.lang.state. + Definition state := io_tape.state. Definition ty := input_lang.lang.ty. Definition expr := input_lang.lang.expr. Definition tyctx {S : Set} := S → ty. diff --git a/theories/examples/affine_lang/logrel1.v b/theories/examples/affine_lang/logrel1.v index c9c38b5..c5d68af 100644 --- a/theories/examples/affine_lang/logrel1.v +++ b/theories/examples/affine_lang/logrel1.v @@ -1,7 +1,7 @@ (** Unary (Kripke) logical relation for the affine lang *) From gitrees Require Export gitree program_logic greifiers. From gitrees.examples.affine_lang Require Import lang. -From gitrees.effects Require Import store. +From gitrees.effects Require Import io_tape store. From gitrees.lib Require Import pairs. From gitrees.utils Require Import finite_sets. @@ -51,7 +51,7 @@ Section logrel. Context {sz : nat}. Variable rs : gReifiers NotCtxDep sz. Context `{!subReifier reify_store rs}. - Context `{!subReifier input_lang.interp.reify_io rs}. + Context `{!subReifier reify_io rs}. Notation F := (gReifiers_ops rs). Context {R} `{!Cofe R}. Context `{!SubOfe natO R}. @@ -516,7 +516,7 @@ Arguments compat_destruct {_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _}. Arguments compat_replace {_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _}. Local Definition rs : gReifiers NotCtxDep 2 := - gReifiers_cons reify_store (gReifiers_cons input_lang.interp.reify_io gReifiers_nil). + gReifiers_cons reify_store (gReifiers_cons reify_io gReifiers_nil). Variable Hdisj : ∀ (Σ : gFunctors) (P Q : iProp Σ), disjunction_property P Q. diff --git a/theories/examples/affine_lang/logrel2.v b/theories/examples/affine_lang/logrel2.v index 865580c..3eaeb0c 100644 --- a/theories/examples/affine_lang/logrel2.v +++ b/theories/examples/affine_lang/logrel2.v @@ -467,7 +467,7 @@ End glue. Local Definition rs : gReifiers NotCtxDep 2 := gReifiers_cons reify_store - (gReifiers_cons input_lang.interp.reify_io gReifiers_nil). + (gReifiers_cons reify_io gReifiers_nil). Variable Hdisj : ∀ (Σ : gFunctors) (P Q : iProp Σ), disjunction_property P Q. diff --git a/theories/examples/input_lang/interp.v b/theories/examples/input_lang/interp.v index 806f55a..202bc12 100644 --- a/theories/examples/input_lang/interp.v +++ b/theories/examples/input_lang/interp.v @@ -1,134 +1,9 @@ From gitrees Require Import gitree lang_generic. +From gitrees.effects Require Export io_tape. From gitrees.examples.input_lang Require Import lang. Require Import Binding.Lib Binding.Set. -Notation stateO := (leibnizO state). - -Program Definition inputE : opInterp := - {| - Ins := unitO; - Outs := natO; - |}. - -Program Definition outputE : opInterp := - {| - Ins := natO; - Outs := unitO; - |}. - -Definition ioE := @[inputE;outputE]. - -(* INPUT *) -Definition reify_input X `{Cofe X} : unitO * stateO → - option (natO * stateO) := - λ '(o, σ), Some (update_input σ : prodO natO stateO). -#[export] Instance reify_input_ne X `{Cofe X} : - NonExpansive (reify_input X). -Proof. - intros ?[[]][[]][_?]. simpl in *. f_equiv. - repeat f_equiv. done. -Qed. - -(* OUTPUT *) -Definition reify_output X `{Cofe X} : (natO * stateO) → - option (unitO * stateO) := - λ '(n, σ), Some((), update_output n σ : stateO). -#[export] Instance reify_output_ne X `{Cofe X} : - NonExpansive (reify_output X). -Proof. - intros ?[][][]. simpl in *. - repeat f_equiv; done. -Qed. - -Canonical Structure reify_io : sReifier NotCtxDep. -Proof. - simple refine {| sReifier_ops := ioE; - sReifier_state := stateO - |}. - intros X HX op. - destruct op as [[] | [ | []]]; simpl. - - simple refine (OfeMor (reify_input X)). - - simple refine (OfeMor (reify_output X)). -Defined. - -Section constructors. - Context {E : opsInterp} {A} `{!Cofe A}. - Context {subEff0 : subEff ioE E}. - Context {subOfe0 : SubOfe natO A}. - Notation IT := (IT E A). - Notation ITV := (ITV E A). - - Program Definition INPUT : (nat -n> IT) -n> IT := λne k, Vis (E:=E) (subEff_opid (inl ())) - (subEff_ins (F:=ioE) (op:=(inl ())) ()) - (NextO ◎ k ◎ (subEff_outs (F:=ioE) (op:=(inl ())))^-1). - Solve Obligations with solve_proper. - Program Definition OUTPUT_ : nat -n> IT -n> IT := - λne m α, Vis (E:=E) (subEff_opid (inr (inl ()))) - (subEff_ins (F:=ioE) (op:=(inr (inl ()))) m) - (λne _, NextO α). - Solve All Obligations with solve_proper_please. - Program Definition OUTPUT : nat -n> IT := λne m, OUTPUT_ m (Ret 0). - - Lemma hom_INPUT k f `{!IT_hom f} : f (INPUT k) ≡ INPUT (OfeMor f ◎ k). - Proof. - unfold INPUT. - rewrite hom_vis/=. repeat f_equiv. - intro x. cbn-[laterO_map]. rewrite laterO_map_Next. - done. - Qed. - Lemma hom_OUTPUT_ m α f `{!IT_hom f} : f (OUTPUT_ m α) ≡ OUTPUT_ m (f α). - Proof. - unfold OUTPUT. - rewrite hom_vis/=. repeat f_equiv. - intro x. cbn-[laterO_map]. rewrite laterO_map_Next. - done. - Qed. - -End constructors. - -Section weakestpre. - Context {sz : nat}. - Variable (rs : gReifiers NotCtxDep sz). - Context {subR : subReifier reify_io rs}. - Notation F := (gReifiers_ops rs). - Context {R} `{!Cofe R}. - Context `{!SubOfe natO R}. - Notation IT := (IT F R). - Notation ITV := (ITV F R). - Context `{!invGS Σ, !stateG rs R Σ}. - Notation iProp := (iProp Σ). - - Lemma wp_input (σ σ' : stateO) (n : nat) (k : natO -n> IT) Φ s : - update_input σ = (n, σ') → - has_substate σ -∗ - ▷ (£ 1 -∗ has_substate σ' -∗ WP@{rs} (k n) @ s {{ Φ }}) -∗ - WP@{rs} (INPUT k) @ s {{ Φ }}. - Proof. - intros Hs. iIntros "Hs Ha". - unfold INPUT. simpl. - iApply (wp_subreify_ctx_indep with "Hs"). - { simpl. rewrite Hs//=. } - { simpl. by rewrite ofe_iso_21. } - iModIntro. done. - Qed. - - Lemma wp_output (σ σ' : stateO) (n : nat) Φ s : - update_output n σ = σ' → - has_substate σ -∗ - ▷ (£ 1 -∗ has_substate σ' -∗ Φ (RetV 0)) -∗ - WP@{rs} (OUTPUT n) @ s {{ Φ }}. - Proof. - intros Hs. iIntros "Hs Ha". - unfold OUTPUT. simpl. - iApply (wp_subreify_ctx_indep rs with "Hs"). - { simpl. by rewrite Hs. } - { simpl. done. } - iModIntro. iIntros "H1 H2". - iApply wp_val. by iApply ("Ha" with "H1 H2"). - Qed. - -End weakestpre. Section interp. Context {sz : nat}. diff --git a/theories/examples/input_lang/lang.v b/theories/examples/input_lang/lang.v index a9d15f4..0afca04 100644 --- a/theories/examples/input_lang/lang.v +++ b/theories/examples/input_lang/lang.v @@ -1,4 +1,4 @@ -From gitrees Require Export prelude. +From gitrees Require Export prelude effects.io_tape. Require Import Binding.Resolver Binding.Lib Binding.Set Binding.Auto Binding.Env. @@ -281,21 +281,6 @@ Qed. (*** Operational semantics *) -Record state := State { - inputs : list nat; - outputs : list nat; - }. -#[export] Instance state_inhabited : Inhabited state := populate (State [] []). - -Definition update_input (s : state) : nat * state := - match s.(inputs) with - | [] => (0, s) - | n::ns => - (n, {| inputs := ns; outputs := s.(outputs) |}) - end. -Definition update_output (n:nat) (s : state) : state := - {| inputs := s.(inputs); outputs := n::s.(outputs) |}. - Inductive head_step {S} : expr S → state → expr S → state → nat*nat → Prop := | BetaS e1 v2 σ : head_step (App (Val $ RecV e1) (Val v2)) σ (subst (Inc := inc) ((subst (F := expr) (Inc := inc) e1) (Val (shift (Inc := inc) v2))) (Val (RecV e1))) σ (1,0) diff --git a/theories/examples/input_lang_callcc/hom.v b/theories/examples/input_lang_callcc/hom.v index 66f3f2d..17d197e 100644 --- a/theories/examples/input_lang_callcc/hom.v +++ b/theories/examples/input_lang_callcc/hom.v @@ -9,7 +9,8 @@ Open Scope stdpp_scope. Section hom. Context {sz : nat}. Context {rs : gReifiers CtxDep sz}. - Context {subR : subReifier reify_io rs}. + Context `{!subReifier reify_cont rs}. + Context `{!subReifier (sReifier_NotCtxDep_CtxDep reify_io) rs}. Notation F := (gReifiers_ops rs). Notation IT := (IT F natO). Notation ITV := (ITV F natO). diff --git a/theories/examples/input_lang_callcc/interp.v b/theories/examples/input_lang_callcc/interp.v index 4262221..e87f55d 100644 --- a/theories/examples/input_lang_callcc/interp.v +++ b/theories/examples/input_lang_callcc/interp.v @@ -1,20 +1,7 @@ -From gitrees Require Import gitree lang_generic. +From gitrees Require Import gitree lang_generic effects.io_tape. From gitrees.examples.input_lang_callcc Require Import lang. Require Import Binding.Lib Binding.Set. -Notation stateO := (leibnizO state). - -Program Definition inputE : opInterp := - {| - Ins := unitO; - Outs := natO; - |}. -Program Definition outputE : opInterp := - {| - Ins := natO; - Outs := unitO; - |}. - Program Definition callccE : opInterp := {| Ins := ((▶ ∙ -n> ▶ ∙) -n> ▶ ∙); @@ -26,115 +13,57 @@ Program Definition throwE : opInterp := Outs := Empty_setO; |}. -Definition ioE := @[inputE;outputE;callccE;throwE]. - -Definition reify_input X `{Cofe X} : unitO * stateO * (natO -n> laterO X) → - option (laterO X * stateO) := - λ '(_, σ, k), let '(n, σ') := (update_input σ : prodO natO stateO) in - Some (k n, σ'). -#[export] Instance reify_input_ne X `{Cofe X} : - NonExpansive (reify_input X : prodO (prodO unitO stateO) - (natO -n> laterO X) → - optionO (prodO (laterO X) stateO)). -Proof. - intros n [[? σ1] k1] [[? σ2] k2]. simpl. - intros [[_ ->] Hk]. simpl in *. - repeat f_equiv. assumption. -Qed. - -Definition reify_output X `{Cofe X} : (natO * stateO * (unitO -n> laterO X)) → - optionO (prodO (laterO X) stateO) := - λ '(n, σ, k), Some (k (), ((update_output n σ) : stateO)). -#[export] Instance reify_output_ne X `{Cofe X} : - NonExpansive (reify_output X : prodO (prodO natO stateO) - (unitO -n> laterO X) → - optionO (prodO (laterO X) stateO)). -Proof. - intros ? [[]] [[]] []; simpl in *. - repeat f_equiv; first assumption; apply H0. -Qed. +Definition contE := @[callccE;throwE]. Definition reify_callcc X `{Cofe X} : ((laterO X -n> laterO X) -n> laterO X) * - stateO * (laterO X -n> laterO X) → - option (laterO X * stateO) := - λ '(f, σ, k), Some ((k (f k): laterO X), σ : stateO). + unitO * (laterO X -n> laterO X) → + option (laterO X * unitO) := + λ '(f, σ, k), Some ((k (f k): laterO X), σ : unitO). #[export] Instance reify_callcc_ne X `{Cofe X} : NonExpansive (reify_callcc X : - prodO (prodO ((laterO X -n> laterO X) -n> laterO X) stateO) + prodO (prodO ((laterO X -n> laterO X) -n> laterO X) unitO) (laterO X -n> laterO X) → - optionO (prodO (laterO X) stateO)). + optionO (prodO (laterO X) unitO)). Proof. intros ?[[]][[]][[]]. simpl in *. repeat f_equiv; auto. Qed. Definition reify_throw X `{Cofe X} : - ((laterO X * (laterO (X -n> X))) * stateO * (Empty_setO -n> laterO X)) → - option (laterO X * stateO) := + ((laterO X * (laterO (X -n> X))) * unitO * (Empty_setO -n> laterO X)) → + option (laterO X * unitO) := λ '((e, k'), σ, _), - Some (((laterO_ap k' : laterO X -n> laterO X) e : laterO X), σ : stateO). + Some (((laterO_ap k' : laterO X -n> laterO X) e : laterO X), σ : unitO). #[export] Instance reify_throw_ne X `{Cofe X} : NonExpansive (reify_throw X : - prodO (prodO (prodO (laterO X) (laterO (X -n> X))) stateO) + prodO (prodO (prodO (laterO X) (laterO (X -n> X))) unitO) (Empty_setO -n> laterO X) → - optionO (prodO (laterO X) (stateO))). + optionO (prodO (laterO X) (unitO))). Proof. intros ?[[[]]][[[]]]?. rewrite /reify_throw. repeat f_equiv; apply H0. Qed. -Canonical Structure reify_io : sReifier CtxDep. +Canonical Structure reify_cont : sReifier CtxDep. Proof. - simple refine {| sReifier_ops := ioE; - sReifier_state := stateO + simple refine {| sReifier_ops := contE; + sReifier_state := unitO |}. intros X HX op. - destruct op as [ | [ | [ | [| []]]]]; simpl. - - simple refine (OfeMor (reify_input X)). - - simple refine (OfeMor (reify_output X)). + destruct op as [|[|[]]]; simpl. - simple refine (OfeMor (reify_callcc X)). - simple refine (OfeMor (reify_throw X)). Defined. Section constructors. Context {E : opsInterp} {A} `{!Cofe A}. - Context {subEff0 : subEff ioE E}. - Context {subOfe0 : SubOfe natO A}. + Context {subEff0 : subEff contE E}. Notation IT := (IT E A). Notation ITV := (ITV E A). - Program Definition INPUT : (nat -n> IT) -n> IT := - λne k, Vis (E:=E) (subEff_opid (inl ())) - (subEff_ins (F:=ioE) (op:=(inl ())) ()) - (NextO ◎ k ◎ (subEff_outs (F:=ioE) (op:=(inl ())))^-1). - Solve Obligations with solve_proper. - - Program Definition OUTPUT_ : nat -n> IT -n> IT := - λne m α, Vis (E:=E) (subEff_opid (inr (inl ()))) - (subEff_ins (F:=ioE) (op:=(inr (inl ()))) m) - (λne _, NextO α). - Solve All Obligations with solve_proper_please. - Program Definition OUTPUT : nat -n> IT := λne m, OUTPUT_ m (Ret 0). - - Lemma hom_INPUT k f `{!IT_hom f} : f (INPUT k) ≡ INPUT (OfeMor f ◎ k). - Proof. - unfold INPUT. - rewrite hom_vis/=. repeat f_equiv. - intro x. cbn-[laterO_map]. rewrite laterO_map_Next. - done. - Qed. - Lemma hom_OUTPUT_ m α f `{!IT_hom f} : f (OUTPUT_ m α) ≡ OUTPUT_ m (f α). - Proof. - unfold OUTPUT. - rewrite hom_vis/=. repeat f_equiv. - intro x. cbn-[laterO_map]. rewrite laterO_map_Next. - done. - Qed. - - Program Definition CALLCC_ : ((laterO IT -n> laterO IT) -n> laterO IT) -n> (laterO IT -n> laterO IT) -n> IT := - λne f k, Vis (E:=E) (subEff_opid (inr (inr (inl ())))) - (subEff_ins (F:=ioE) (op:=(inr (inr (inl ())))) f) - (k ◎ (subEff_outs (F:=ioE) (op:=(inr (inr (inl ())))))^-1). + λne f k, Vis (E:=E) (subEff_opid (inl ())) + (subEff_ins (F:=contE) (op:=(inl ())) f) + (k ◎ (subEff_outs (F:=contE) (op:=(inl ())))^-1). Solve All Obligations with solve_proper. Program Definition CALLCC : ((laterO IT -n> laterO IT) -n> laterO IT) -n> IT := @@ -150,10 +79,10 @@ Section constructors. Qed. Program Definition THROW : IT -n> (laterO (IT -n> IT)) -n> IT := - λne e k, Vis (E:=E) (subEff_opid (inr (inr (inr (inl ()))))) - (subEff_ins (F:=ioE) (op:=(inr (inr (inr (inl ()))))) + λne e k, Vis (E:=E) (subEff_opid (inr (inl ()))) + (subEff_ins (F:=contE) (op:=(inr (inl ()))) (NextO e, k)) - (λne x, Empty_setO_rec _ ((subEff_outs (F:=ioE) (op:=(inr (inr (inr (inl ()))))))^-1 x)). + (λne x, Empty_setO_rec _ ((subEff_outs (F:=contE) (op:=(inr (inl ()))))^-1 x)). Next Obligation. solve_proper_prepare. destruct ((subEff_outs ^-1) x). @@ -172,68 +101,20 @@ End constructors. Section weakestpre. Context {sz : nat}. Variable (rs : gReifiers CtxDep sz). - Context {subR : subReifier reify_io rs}. + Context {subR : subReifier reify_cont rs}. Notation F := (gReifiers_ops rs). Context {R} `{!Cofe R}. - Context `{!SubOfe natO R}. Notation IT := (IT F R). Notation ITV := (ITV F R). Context `{!invGS Σ, !stateG rs R Σ}. Notation iProp := (iProp Σ). - Lemma wp_input' (σ σ' : stateO) (n : nat) (k : natO -n> IT) (κ : IT -n> IT) - `{!IT_hom κ} Φ s : - update_input σ = (n, σ') -> - has_substate σ -∗ - ▷ (£ 1 -∗ has_substate σ' -∗ WP@{rs} (κ ◎ k $ n) @ s {{ Φ }}) -∗ - WP@{rs} κ (INPUT k) @ s {{ Φ }}. - Proof. - iIntros (Hσ) "Hs Ha". - rewrite hom_INPUT. simpl. - iApply (wp_subreify_ctx_dep with "Hs"). - + simpl. by rewrite Hσ. - + by rewrite ofe_iso_21. - + done. - Qed. - - Lemma wp_input (σ σ' : stateO) (n : nat) (k : natO -n> IT) Φ s : - update_input σ = (n, σ') → - has_substate σ -∗ - ▷ (£ 1 -∗ has_substate σ' -∗ WP@{rs} (k n) @ s {{ Φ }}) -∗ - WP@{rs} (INPUT k) @ s {{ Φ }}. - Proof. - eapply (wp_input' σ σ' n k idfun). - Qed. + Implicit Type σ : unitO. + Implicit Type κ : IT -n> IT. + Implicit Type x : IT. - Lemma wp_output' (σ σ' : stateO) (n : nat) (κ : IT -n> IT) + Lemma wp_throw' σ κ (f : IT -n> IT) (x : IT) `{!IT_hom κ} Φ s : - update_output n σ = σ' → - has_substate σ -∗ - ▷ (£ 1 -∗ has_substate σ' -∗ WP@{rs} (κ (Ret 0)) @ s {{ Φ }}) -∗ - WP@{rs} κ (OUTPUT n) @ s {{ Φ }}. - Proof. - iIntros (Hσ) "Hs Ha". - rewrite /OUTPUT hom_OUTPUT_. - iApply (wp_subreify_ctx_dep with "Hs"). - + simpl. by rewrite Hσ. - + done. - + done. - Qed. - - Lemma wp_output (σ σ' : stateO) (n : nat) Φ s : - update_output n σ = σ' → - has_substate σ -∗ - ▷ (£ 1 -∗ has_substate σ' -∗ Φ (RetV 0)) -∗ - WP@{rs} (OUTPUT n) @ s {{ Φ }}. - Proof. - iIntros (Hσ) "Hs Ha". - iApply (wp_output' _ _ _ idfun with "Hs [Ha]"); first done. - simpl. iNext. iIntros "Hcl Hs". - iApply wp_val. iApply ("Ha" with "Hcl Hs"). - Qed. - - Lemma wp_throw' (σ : stateO) (f : IT -n> IT) (x : IT) - (κ : IT -n> IT) `{!IT_hom κ} Φ s : has_substate σ -∗ ▷ (£ 1 -∗ has_substate σ -∗ WP@{rs} f x @ s {{ Φ }}) -∗ WP@{rs} κ (THROW x (Next f)) @ s {{ Φ }}. @@ -243,15 +124,15 @@ Section weakestpre. iApply (wp_subreify_ctx_dep with "Hs"); simpl; done. Qed. - Lemma wp_throw (σ : stateO) (f : IT -n> IT) (x : IT) Φ s : + Lemma wp_throw σ (f : IT -n> IT) (x : IT) Φ s : has_substate σ -∗ ▷ (£ 1 -∗ has_substate σ -∗ WP@{rs} f x @ s {{ Φ }}) -∗ WP@{rs} (THROW x (Next f)) @ s {{ Φ }}. Proof. - iApply (wp_throw' _ _ _ idfun). + iApply (wp_throw' _ idfun). Qed. - Lemma wp_callcc (σ : stateO) (f : (laterO IT -n> laterO IT) -n> laterO IT) (k : IT -n> IT) {Hk : IT_hom k} β Φ s : + Lemma wp_callcc σ (f : (laterO IT -n> laterO IT) -n> laterO IT) (k : IT -n> IT) {Hk : IT_hom k} β Φ s : f (laterO_map k) ≡ Next β → has_substate σ -∗ ▷ (£ 1 -∗ has_substate σ -∗ WP@{rs} k β @ s {{ Φ }}) -∗ @@ -275,12 +156,45 @@ Section weakestpre. iApply "Ha". Qed. + (* XXX TODO: this duplicates wp_input and wp_output *) + Context `{!subReifier (sReifier_NotCtxDep_CtxDep reify_io) rs}. + Context `{!SubOfe natO R}. + Lemma wp_input' (σ σ' : stateO) (n : nat) (k : natO -n> IT) (κ : IT -n> IT) + `{!IT_hom κ} Φ s : + update_input σ = (n, σ') -> + has_substate σ -∗ + ▷ (£ 1 -∗ has_substate σ' -∗ WP@{rs} (κ ◎ k $ n) @ s {{ Φ }}) -∗ + WP@{rs} κ (INPUT k) @ s {{ Φ }}. + Proof. + iIntros (Hσ) "Hs Ha". + rewrite hom_INPUT. + iApply (wp_subreify_ctx_dep with "Hs"). + + simpl. rewrite Hσ. simpl. done. + + by rewrite ofe_iso_21. + + done. + Qed. + Lemma wp_output' (σ σ' : stateO) (n : nat) (κ : IT -n> IT) + `{!IT_hom κ} Φ s : + update_output n σ = σ' → + has_substate σ -∗ + ▷ (£ 1 -∗ has_substate σ' -∗ WP@{rs} (κ (Ret 0)) @ s {{ Φ }}) -∗ + WP@{rs} κ (OUTPUT n) @ s {{ Φ }}. + Proof. + iIntros (Hσ) "Hs Ha". + rewrite /OUTPUT hom_OUTPUT_. + iApply (wp_subreify_ctx_dep with "Hs"). + + simpl. by rewrite Hσ. + + done. + + done. + Qed. + End weakestpre. Section interp. Context {sz : nat}. Variable (rs : gReifiers CtxDep sz). - Context {subR : subReifier reify_io rs}. + Context {subR1 : subReifier reify_cont rs}. + Context {subR2 : subReifier (sReifier_NotCtxDep_CtxDep reify_io) rs}. Context {R} `{CR : !Cofe R}. Context `{!SubOfe natO R}. Notation F := (gReifiers_ops rs). @@ -929,13 +843,11 @@ Section interp. } rewrite reify_vis_eq_ctx_dep //; first last. { - epose proof (@subReifier_reify sz CtxDep reify_io rs _ IT _ (inl ()) () (Next (interp_ectx K env (Ret n0))) (NextO ◎ (interp_ectx K env ◎ Ret)) σ σ' σr) as H. - simpl in H. - simpl. - erewrite <-H; last first. - - rewrite H5. reflexivity. - - f_equiv; - solve_proper. + apply (subReifier_reify + (sReifier_NotCtxDep_CtxDep reify_io) rs (inl ()) + () (Next (interp_ectx K env (Ret n0))) + (NextO ◎ (interp_ectx K env ◎ Ret)) σ σ' σr). + simpl. rewrite H5. reflexivity. } repeat f_equiv. rewrite Tick_eq/=. repeat f_equiv. rewrite interp_comp. @@ -952,12 +864,14 @@ Section interp. } rewrite reify_vis_eq_ctx_dep //; last first. { - epose proof (@subReifier_reify sz CtxDep reify_io rs _ IT _ (inr (inl ())) n0 (Next (interp_ectx K env ((Ret 0)))) (constO (Next (interp_ectx K env ((Ret 0))))) σ (update_output n0 σ) σr) as H. - simpl in H. simpl. - erewrite <-H; last reflexivity. + pose proof (subReifier_reify + (sReifier_NotCtxDep_CtxDep reify_io) rs (inr (inl ())) + n0 (Next (interp_ectx K env (Ret 0))) + (constO (Next (interp_ectx K env ((Ret 0))))) σ (update_output n0 σ) σr) as H. + simpl in H. erewrite <-H; last reflexivity. f_equiv. - + intros ???. by rewrite /prod_map H0. + + do 3 intro. by rewrite /prod_map H0. + do 2 f_equiv. by intro. } repeat f_equiv. rewrite Tick_eq/=. repeat f_equiv. @@ -971,7 +885,6 @@ Section interp. Transparent CALLCC. unfold CALLCC. simpl. - set (subEff1 := @subReifier_subEff sz CtxDep reify_io rs subR). trans (reify (gReifiers_sReifier rs) (CALLCC_ f (laterO_map (interp_ectx K env))) gσ). { do 2 f_equiv. @@ -981,17 +894,28 @@ Section interp. rewrite reify_vis_eq_ctx_dep//; last first. { simpl. - epose proof (@subReifier_reify sz CtxDep reify_io rs subR IT _ - (inr (inr (inl ()))) f _ - (laterO_map (interp_ectx K env)) σ' σ' σr) as H. + set (ss := gState_decomp (@sR_idx _ _ _ _ subR1) gσ). + pose (s1 := (sR_state^-1 ss.1)). simpl in s1. + epose proof (subReifier_reify reify_cont rs (inl ()) f _ + (laterO_map (interp_ectx K env)) + s1 s1 (ss.2)) as H. simpl in H. erewrite <-H; last reflexivity. - f_equiv; last done. - intros ???. by rewrite /prod_map H0. + f_equiv. + + intros ???. rewrite /prod_map H0. repeat f_equiv. + rewrite ofe_iso_12. + destruct ss; f_equiv; eauto. simpl. + symmetry. apply ofe_iso_12. + + repeat f_equiv; eauto. + rewrite ofe_iso_12. + destruct ss; f_equiv; eauto. + symmetry. apply ofe_iso_12. } rewrite interp_comp. rewrite interp_expr_subst. f_equiv. + { setoid_rewrite ofe_iso_12. + by apply gState_recomp_decomp. } rewrite Tick_eq. f_equiv. rewrite laterO_map_Next. @@ -1094,19 +1018,36 @@ Section interp. match goal with | |- context G [(_, _, ?a)] => set (κ := a) end. - epose proof (@subReifier_reify sz CtxDep reify_io rs subR IT _ - (inr (inr (inr (inl ())))) (Next (interp_val v env), Next f') + set (gσ := (gState_recomp σr (sR_state (σ2 : sReifier_state (sReifier_NotCtxDep_CtxDep reify_io) ♯ IT)))). + (* set (gσ := (gState_recomp σr (sR_state σ2))). *) + set (ss := gState_decomp (@sR_idx _ _ _ _ subR1) gσ). + pose (s1 := (sR_state^-1 ss.1)). simpl in gσ, s1. + epose proof (subReifier_reify reify_cont rs (inr (inl ())) + (Next (interp_val v env), Next f') (Next (Tau (Next ((interp_ectx K' env) (interp_val v env))))) - (Empty_setO_rec _) σ2 σ2 σr) as H'. - subst κ. + (Empty_setO_rec _) s1 s1 ss.2) as H'. simpl in H'. - erewrite <-H'; last reflexivity. - rewrite /prod_map. - f_equiv; first solve_proper. - do 2 f_equiv; first reflexivity. - intro; simpl. - f_equiv. - } + subst κ. + simpl. trans (Some + (Next (Tau (Next (interp_ectx K' env (interp_val v env)))), + gState_recomp ss.2 (sR_state (s1 : sReifier_state reify_cont ♯ IT)))). + - erewrite <-H'; last reflexivity. + rewrite /prod_map. + f_equiv. + + repeat intro. repeat f_equiv; eauto. + unfold s1. + setoid_rewrite ofe_iso_12. + symmetry. by apply gState_recomp_decomp. + + do 2 f_equiv. + * repeat f_equiv. unfold s1. + setoid_rewrite ofe_iso_12. + symmetry. by apply gState_recomp_decomp. + * intro; simpl. + f_equiv. done. + - rewrite Tick_eq. repeat f_equiv. + unfold s1. + setoid_rewrite ofe_iso_12. + by apply gState_recomp_decomp. } Qed. End interp. diff --git a/theories/examples/input_lang_callcc/lang.v b/theories/examples/input_lang_callcc/lang.v index 65eabcb..8f5cb94 100644 --- a/theories/examples/input_lang_callcc/lang.v +++ b/theories/examples/input_lang_callcc/lang.v @@ -1,4 +1,4 @@ -From gitrees Require Export prelude. +From gitrees Require Export prelude effects.io_tape. Require Import Binding.Resolver Binding.Lib Binding.Set Binding.Auto Binding.Env. Inductive nat_op := Add | Sub | Mult. @@ -299,22 +299,6 @@ Qed. (*** Operational semantics *) -Record state := State { - inputs : list nat; - outputs : list nat; - }. -#[export] Instance state_inhabited : Inhabited state := populate (State [] []). - -Definition update_input (s : state) : nat * state := - match s.(inputs) with - | [] => (0, s) - | n::ns => - (n, {| inputs := ns; outputs := s.(outputs) |}) - end. -Definition update_output (n:nat) (s : state) : state := - {| inputs := s.(inputs); outputs := n::s.(outputs) |}. - - Inductive head_step {S} : expr S → state → expr S → state → ectx S → nat * nat → Prop := | BetaS e1 v2 σ K : head_step (App (Val $ RecV e1) (Val v2)) σ (subst (Inc := inc) ((subst (F := expr) (Inc := inc) e1) (Val (shift (Inc := inc) v2))) (Val (RecV e1))) σ K (1,0) diff --git a/theories/examples/input_lang_callcc/logrel.v b/theories/examples/input_lang_callcc/logrel.v index 8d2891a..677579a 100644 --- a/theories/examples/input_lang_callcc/logrel.v +++ b/theories/examples/input_lang_callcc/logrel.v @@ -1,5 +1,5 @@ (** Logical relation for adequacy for the IO lang *) -From gitrees Require Import gitree lang_generic. +From gitrees Require Import gitree lang_generic effects.io_tape. From gitrees.examples.input_lang_callcc Require Import lang interp hom. Require Import Binding.Lib Binding.Set Binding.Env. @@ -8,13 +8,14 @@ Open Scope stdpp_scope. Section logrel. Context {sz : nat}. Variable (rs : gReifiers CtxDep sz). - Context {subR : subReifier reify_io rs}. + Context `{!subReifier reify_cont rs}. + Context `{!subReifier (sReifier_NotCtxDep_CtxDep reify_io) rs}. Notation F := (gReifiers_ops rs). Notation IT := (IT F natO). Notation ITV := (ITV F natO). Context `{!invGS Σ, !stateG rs natO Σ}. Notation iProp := (iProp Σ). - Notation restO := (gState_rest sR_idx rs ♯ IT). + Notation restO := (gState_rest (@sR_idx _ _ (sReifier_NotCtxDep_CtxDep reify_io)) rs ♯ IT). Canonical Structure exprO S := leibnizO (expr S). Canonical Structure valO S := leibnizO (val S). @@ -31,11 +32,13 @@ Section logrel. Definition logrel_nat {S} (βv : ITV) (v : val S) : iProp := (∃ n, βv ≡ RetV n ∧ ⌜v = LitV n⌝)%I. + Definition cont_ctx : iProp := has_substate (() : sReifier_state reify_cont ♯ IT). + Definition obs_ref {S} (α : IT) (e : expr S) : iProp := (∀ (σ : stateO), - has_substate σ -∗ + has_substate σ -∗ cont_ctx -∗ WP α {{ βv, ∃ m v σ', ⌜prim_steps e σ (Val v) σ' m⌝ - ∗ logrel_nat βv v ∗ has_substate σ' }})%I. + ∗ logrel_nat βv v ∗ has_substate σ' ∗ cont_ctx }})%I. Definition logrel_ectx {S} V (κ : HOM) (K : ectx S) : iProp := (□ ∀ (βv : ITV) (v : val S), V βv v -∗ obs_ref (`κ (IT_of_V βv)) (fill K (Val v)))%I. @@ -181,9 +184,8 @@ Section logrel. intros Hpure. iIntros "H". iIntros (κ' K') "#HK'". - iIntros (σ) "Hs". - iSpecialize ("H" with "HK'"). - iSpecialize ("H" with "Hs"). + iIntros (σ) "Hs Hcont". + iSpecialize ("H" with "HK' Hs Hcont"). iApply (wp_wand with "H"). iIntros (βv). iDestruct 1 as ([m m'] v σ' Hsteps) "[H2 Hs]". iExists ((Nat.add n m),m'),v,σ'. iFrame "H2 Hs". @@ -200,8 +202,8 @@ Section logrel. obs_ref (`f α) (fill K e). Proof. iIntros "H1 #H2". - iIntros (σ) "Hs". - iApply (wp_wand with "[H1 H2 Hs] []"); first iApply ("H1" with "[H2] [$Hs]"). + iIntros (σ) "Hs Hcont". + iApply (wp_wand with "[H1 H2 Hs Hcont] []"); first iApply ("H1" with "[H2] [$Hs] Hcont"). - iIntros (βv v). iModIntro. iIntros "#Hv". by iApply "H2". @@ -260,9 +262,9 @@ Section logrel. (Tick (f (IT_of_V αv))) (logrel_val τ2) with "[]"); last first. + rewrite {2}/ss'. rewrite /f. - iIntros (κ K) "#HK". iIntros (σ) "Hs". + iIntros (κ K) "#HK". iIntros (σ) "Hs Hcont". rewrite hom_tick. iApply wp_tick. iNext. - iApply "H"; eauto. + iApply ("H" with "[] [] Hs Hcont"); eauto. rewrite /ss' /γ'. iIntros (x'); destruct x' as [| [| x']]; term_simpl; iModIntro. * by iApply logrel_of_val. @@ -338,12 +340,12 @@ Section logrel. iIntros (κ K) "#HK". unfold interp_input. term_simpl. - iIntros (σ) "Hs". + iIntros (σ) "Hs Hcont". destruct (update_input σ) as [n σ'] eqn:Hinp. - iApply (wp_input' with "Hs []"); first done. + iApply (wp_input' with "Hs [-]"); first done. iNext. iIntros "Hlc Hs". term_simpl. iSpecialize ("HK" $! (RetV n) (LitV n) with "[]"); first by iExists n. - iSpecialize ("HK" $! σ' with "Hs"). + iSpecialize ("HK" $! σ' with "Hs Hcont"). rewrite IT_of_V_Ret. iApply (wp_wand with "[$HK] []"). iIntros (v') "(%m & %v'' & %σ'' & %Hstep & H)". @@ -449,12 +451,12 @@ Section logrel. iRewrite "HEQ". rewrite get_fun_fun. simpl. - iIntros (σ) "Hs". - iApply (wp_throw' with "Hs []"). - iNext. iIntros "Hcl Hs". term_simpl. + iIntros (σ) "Hs Hcont". + iApply (wp_throw' with "Hcont"). + iNext. iIntros "Hcl Hcont". term_simpl. rewrite later_map_Next. iApply wp_tick. iNext. iSpecialize ("H" $! βv v with "[]"); first done. - iSpecialize ("H" $! σ with "Hs"). + iSpecialize ("H" $! σ with "Hs Hcont"). iApply (wp_wand with "[$H] []"). iIntros (w) "(%m & %v'' & %σ'' & %Hstep & H)". destruct m as [m m']. @@ -479,11 +481,11 @@ Section logrel. unfold interp_callcc. Opaque extend_scope. term_simpl. - iIntros (σ) "Hs". + iIntros (σ) "Hs Hcont". - iApply (wp_callcc with "Hs []"). + iApply (wp_callcc with "Hcont"). { simpl. done. } - iNext. iIntros "Hcl Hs". term_simpl. + iNext. iIntros "Hcl Hcont". term_simpl. pose (ff := (λit x : IT, Tick ((`κ) x))). match goal with @@ -519,7 +521,7 @@ Section logrel. iSpecialize ("H" $! κ K with "HK"). Opaque extend_scope. term_simpl. - iSpecialize ("H" $! σ with "Hs"). + iSpecialize ("H" $! σ with "Hs Hcont"). subst ss' γ'. iApply (wp_wand with "[$H] []"). iIntros (v') "(%m & %v'' & %σ'' & %Hstep & H)". @@ -555,12 +557,12 @@ Section logrel. iIntros (βv v). iModIntro. iIntros "#Hv". iDestruct "Hv" as (n) "[Hb ->]". iRewrite "Hb". simpl. - iIntros (σ) "Hs". + iIntros (σ) "Hs Hcont". rewrite get_ret_ret. - iApply (wp_output' with "Hs []"); first done. + iApply (wp_output' with "Hs"); first done. iNext. iIntros "Hlc Hs". iSpecialize ("HK" $! (RetV 0) (LitV 0) with "[]"); first by iExists 0. - iSpecialize ("HK" $! (update_output n σ) with "Hs"). + iSpecialize ("HK" $! (update_output n σ) with "Hs Hcont"). iApply (wp_wand with "[$HK] []"). iIntros (v') "(%m & %v'' & %σ'' & %Hstep & H')". destruct m as [m m']. @@ -685,13 +687,15 @@ Lemma κ_Ret {S} {E} n : κ ((RetV n) : ITV E natO) = (LitV n : val S). Proof. Transparent RetV. unfold RetV. simpl. done. Opaque RetV. Qed. -Definition rs : gReifiers CtxDep 1 := gReifiers_cons reify_io gReifiers_nil. +Definition rs : gReifiers CtxDep 2 := + gReifiers_cons (sReifier_NotCtxDep_CtxDep reify_io) + (gReifiers_cons reify_cont 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 Σ}, (⊢ logrel rs Tnat α e)%I) → - ssteps (gReifiers_sReifier rs) α (σ, ()) (Ret n) σ' k → + ssteps (gReifiers_sReifier rs) α (σ, ((), ())) (Ret n) σ' k → ∃ m σ', prim_steps e σ (Val $ LitV n) σ' m. Proof. intros Hlog Hst. @@ -727,26 +731,28 @@ Proof. eauto. - iIntros "[_ Hs]". iPoseProof (Hlog) as "Hlog". - iAssert (has_substate σ) with "[Hs]" as "Hs". + iAssert (has_substate σ ∗ cont_ctx rs)%I with "[Hs]" as "[Hs Hcont]". { unfold has_substate, has_full_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. - destruct decide as [Heq|]; last first. - { - inv_fin j; first done. - intros i. inversion i. - } - inv_fin j; last done. - intros Heq. - rewrite (eq_pi _ _ Heq eq_refl)//. + 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 σ)) + ⋅ of_idx rs (IT (gReifiers_ops rs) _) sR_idx (sR_state (() : sReifier_state reify_cont ♯ IT _ _))) + as -> ; last first. + { rewrite -own_op. done. } + unfold sR_idx. simpl. + intro j. + rewrite discrete_fun_lookup_op. + inv_fin j. + { unfold of_state, of_idx. simpl. + erewrite (eq_pi _ _ _ (@eq_refl _ 0%fin)). done. } + intros j. inv_fin j. + { unfold of_state, of_idx. simpl. + erewrite (eq_pi _ _ _ (@eq_refl _ 1%fin)). done. } + intros i. inversion i. } iSpecialize ("Hlog" $! HOM_id EmptyK with "[]"). { - iIntros (βv v); iModIntro. iIntros "Hv". iIntros (σ'') "HS". + iIntros (βv v); iModIntro. iIntros "Hv". iIntros (σ'') "HS Hcont". iApply wp_val. iModIntro. iExists (0, 0), v, σ''. @@ -755,7 +761,7 @@ Proof. - by iFrame. } simpl. - iSpecialize ("Hlog" $! σ with "Hs"). + iSpecialize ("Hlog" $! σ with "Hs Hcont"). iApply (wp_wand with"Hlog"). iIntros ( βv). iIntros "H". iDestruct "H" as (m' v σ1' Hsts) "[Hi Hsts]". @@ -766,7 +772,7 @@ Qed. Theorem adequacy (e : expr ∅) (k : nat) σ σ' n : typed □ e Tnat → - ssteps (gReifiers_sReifier 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/gitree/greifiers.v b/theories/gitree/greifiers.v index e1847c8..db4d41c 100644 --- a/theories/gitree/greifiers.v +++ b/theories/gitree/greifiers.v @@ -346,6 +346,17 @@ Section greifiers. apply subEff_outs. Defined. + #[export] Instance reifier_coercion_subEff {sz} r (rs : gReifiers CtxDep sz) + `{H : !subReifier (sReifier_NotCtxDep_CtxDep r) rs} : + subEff (sReifier_ops r) (gReifiers_ops _ rs) | 100. + Proof. + simple refine + {| subEff_opid (op : opid (sReifier_ops (sReifier_NotCtxDep_CtxDep r))) + := subEff_opid op |}. + - intros. apply subEff_ins. + - intros. apply subEff_outs. + Defined. + Program Definition subReifier_reify_idx_type {n} (a : is_ctx_dep) (r : sReifier a) (rs : gReifiers a n) `{!subReifier r rs} X `{!Cofe X} (op : opid (sReifier_ops r)) : Type.