Merge branch 'callcc-non-cps' of github.com:logsem/gitrees into callc…

…c-non-cps

.github/workflows/build.yml

@@ -19,6 +19,7 @@ jobs:
       matrix:
         image:
           - 'coqorg/coq:8.17'
+          - 'coqorg/coq:8.18'
       max-parallel: 4
       fail-fast: false
 

README.md

@@ -26,13 +26,17 @@ to the code structure.
 
 - `gitree/` -- contains the core definitions related to guarded interaction trees
 - `lib/` -- derived combinators for gitrees
+- `effects/` -- concrete effects, their semantics, and program logic rules
 - `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
+- `examples/input_lang_callcc/` -- formalization of the language with io, throw and call/cc, the soundness and adequacy
+- `examples/delim_lang/` -- formalization shift/reset effects, of a language with delimited continuations and its soundness
 - `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
+
+For the representation of binders we use a library implemented by
+Filip Sieczkowski and Piotr Polesiuk, located in the `vendor/Binding/`
+folder.
 
 ### References from the paper to the code
 
@@ -76,15 +80,6 @@ Below we describe the correspondence per-section.
 
 ## Notes
 
-### Representations of binders 1
-For the representation of languages with binders, we follow the
-approach of (Benton, Hur, Kennedy, McBride, JAR 2012) with well-scoped
-terms and substitutions/renamings. (`input_lang`, `affine_lang`)
-
-### Representations of binders 2
-For `input_lang_callcc` we use a binder library, implemented by Filip
-Sieczkowski and Piotr Polesiuk.
-
 ### Disjunction property
 Some results in the formalization make use of the disjunction property
 of Iris: if (P ∨ Q) is provable, then either P or Q are provable on

_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

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.

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.

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.

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.
 

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.