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

…c-non-cps

README.md

@@ -5,9 +5,10 @@ This is the Coq formalization of guarded interaction trees, associated examples
 ## Installation instructions
 
 To install the formalization you will need the Iris, std++, and Equations packages.
-The dependencies can be easily installed with the following commands:
+The dependencies can be easily installed using [Opam](https://opam.ocaml.org/) with the following commands:
 
 ```
+opam repo add coq-released https://coq.inria.fr/opam/released
 opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
 opam update
 opam install . --deps-only
@@ -53,6 +54,7 @@ to the code structure.
     in `gitree/weakestpre.v`
   + The additional weakest precondition rules are in `program_logic.v`
     and `examples/store.v`
+  + The `iter` example is in `examples/iter.v`
 - **Section 7**
   + The logical relation and the adequacy proof are in `input_lang/logrel.v`
 - **Section 8**
@@ -68,7 +70,41 @@ to the code structure.
 
 ## Notes
 
+### Representations of binders
 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. 
 
+
+### 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
+their own. This propery is used to show safety of the weakest
+precondition, and it is related to the difference between internal and
+external reductions.
+
+The internal reductions of GITrees is the relation `istep`, as defined
+in the paper, and it has type `iProp` as it is an internal relatin.
+There is also a similar *external* reduction relation `sstep` which
+lives in Coq's `Prop`. We use the `istep` relation in our definitions
+(since it is an internal relation), but we want to state the safety
+result w.r.t. the external relation `sstep`, which we take to be the
+'proper definition' of the reductions for GITrees.
+
+Showing that `istep`-safety implies `sstep`-safety (i.e. that if a
+GITree can do an `istep` then it can also do a `sstep`) requires the
+disjunction propety. The disjunction property for Iris can be shown
+assuming classical axioms (e.g. LEM) on the `Prop`-level.
+
+In order not to introduce classical axioms into the whole
+formalization, we added the disjunction propety as an assumption to
+the safety theorem (`wp_safety`) and all of its instances (e.g. in
+logical relations).
+
+### Ground type of errors
+
+One other difference with the paper worth mentioning, is that in the
+formalization we "hardcode" the type `Err` of errors, whereas in the
+paper we leave it parameterized. That is why in the `affine_lang` case
+study we use `OtherError` to represent linearity violations, instead
+of `Err(Lin)`.

_CoqProject

@@ -46,3 +46,4 @@ theories/examples/store.v
 theories/examples/pairs.v
 theories/examples/while.v
 theories/examples/factorial.v
+theories/examples/iter.v

theories/examples/iter.v

@@ -0,0 +1,103 @@
+From gitrees Require Import prelude gitree.
+
+Section iter.
+  Context {E : opsInterp}.
+  Context {R} `{!Cofe R}.
+  Context `{!SubOfe natO R}.
+  Notation IT := (IT E R).
+  Notation ITV := (ITV E R).
+
+  Program Definition pre_iter_1 (itr : IT) : IT -n> IT -n> IT :=
+    λne f α, λit β, IF α (f ⊙ (itr ⊙ f ⊙ (NATOP Nat.sub α (Ret 1)) ⊙ β)) β.
+  Solve All Obligations with solve_proper_please.
+  Program Definition pre_iter_2 (itr : IT) : IT -n> IT :=
+    λne f, λit α, pre_iter_1 itr f α.
+  Solve All Obligations with solve_proper_please.
+  Program Definition pre_iter (itr : IT) : IT :=
+    λit f, pre_iter_2 itr f.
+    (* λit f α β, IF α (f ⊙ (itr ⊙ f ⊙ (NATOP Nat.sub α (Ret 1)) ⊙ β)) β. *)
+  Solve All Obligations with solve_proper_please.
+
+  #[local] Instance pre_iter_contractive : Contractive pre_iter.
+  Proof.
+    intro n.
+    repeat intro. unfold pre_iter.
+    repeat f_equiv. intro. simpl.
+    repeat f_equiv. intro. simpl.
+    f_equiv. apply Next_contractive.
+    destruct n.
+    { apply dist_later_0. }
+    apply dist_later_S.
+    apply dist_later_S in H. intro.
+    simpl. solve_proper.
+  Qed.
+  Definition ITER : IT := fixpoint pre_iter.
+
+  Lemma ITER_eq f α β `{!AsVal f, !AsVal α, !AsVal β}:
+    ITER ⊙ f ⊙ α ⊙ β ≡ Tick_n 3 $ IF α (f ⊙ (ITER ⊙ f ⊙ (NATOP Nat.sub α (Ret 1)) ⊙ β)) β.
+  Proof.
+    trans (pre_iter ITER ⊙ f ⊙ α ⊙ β).
+    - repeat f_equiv. apply (fixpoint_unfold pre_iter).
+    - trans (Tick (pre_iter_2 ITER f ⊙ α ⊙ β)).
+      { unfold pre_iter.
+        rewrite -APP'_Tick_l. do 2 f_equiv.
+        rewrite -APP'_Tick_l. do 2 f_equiv.
+        rewrite APP'_Fun_l. cbn-[pre_iter_2].
+        by rewrite Tick_eq. }
+      rewrite Tick_n_S. f_equiv.
+      trans (Tick (pre_iter_1 ITER f α ⊙ β)).
+      { unfold pre_iter_2.
+        rewrite -APP'_Tick_l. do 2 f_equiv.
+        rewrite APP'_Fun_l. cbn-[pre_iter_2].
+        by rewrite Tick_eq. }
+      rewrite Tick_n_S. f_equiv.
+      rewrite APP'_Fun_l. cbn.
+      by rewrite Tick_eq.
+  Qed.
+
+End iter.
+
+Section iter_wp.
+  Context {sz : nat}.
+  Variable (rs : gReifiers sz).
+  Context {R} `{!Cofe R}.
+  Context `{!SubOfe natO R}.
+  Notation F := (gReifiers_ops rs).
+  Notation IT := (IT F R).
+  Notation ITV := (ITV F R).
+  Context `{!invGS Σ, !stateG rs R Σ}.
+  Notation iProp := (iProp Σ).
+  Context {HCI : ∀ o : opid (sReifier_ops (gReifiers_sReifier rs)),
+             CtxIndep (gReifiers_sReifier rs)
+               (ITF_solution.IT (sReifier_ops (gReifiers_sReifier rs)) R) o}.
+
+  Lemma wp_iter f (m : nat) β Ψ `{!AsVal f} `{!NonExpansive Ψ} :
+    ⊢ WP@{rs} β {{ Ψ }} -∗
+      □ (∀ βv, Ψ βv -∗ WP@{rs} (f ⊙ (IT_of_V βv)) {{ Ψ }}) -∗
+      WP@{rs} (ITER ⊙ f ⊙ (Ret m) ⊙ β) {{ Ψ }}.
+  Proof using HCI.
+    iIntros "Hb #H".
+    iApply (wp_bind _ (AppRSCtx (ITER ⊙ f ⊙ (Ret m)))).
+    iApply (wp_wand with "Hb").
+    iIntros (βv) "Hb". iModIntro.
+    iLöb as "IH" forall (m βv).
+    unfold AppRSCtx. simpl.
+    rewrite ITER_eq. iApply wp_tick. iNext.
+    iApply wp_tick. iNext. iApply wp_tick. iNext.
+    destruct m as [|m].
+    { rewrite IF_False; last lia.
+      by iApply wp_val. }
+    rewrite IF_True; last lia.
+    iApply (wp_bind _ (AppRSCtx f)).
+    iAssert ((NATOP Nat.sub (Ret (S m)) (Ret 1)) ≡ (Ret m : IT))%I as "Heq".
+    { iPureIntro. rewrite (NATOP_Ret (S m) 1 Nat.sub). f_equiv.
+      rewrite Nat.sub_1_r. done. }
+    iRewrite "Heq".
+    iSpecialize ("IH" with "Hb").
+    iApply (wp_wand with "IH").
+    iIntros (β'v) "Hb". iModIntro.
+    unfold AppRSCtx.
+    by iApply "H".
+  Qed.
+
+End iter_wp.

theories/input_lang_callcc/hom.v

@@ -0,0 +1,130 @@
+From Equations Require Import Equations.
+From gitrees Require Import gitree.
+From gitrees.input_lang_callcc Require Import lang interp.
+Require Import gitrees.lang_generic_sem.
+Require Import Binding.Lib Binding.Set Binding.Env.
+
+Open Scope stdpp_scope.
+
+Section hom.
+  Context {sz : nat}.
+  Context {rs : gReifiers sz}.
+  Context {subR : subReifier reify_io rs}.
+  Notation F := (gReifiers_ops rs).
+  Notation IT := (IT F natO).
+  Notation ITV := (ITV F natO).
+
+  Definition HOM : ofe := @sigO (IT -n> IT) IT_hom.
+
+  Global Instance HOM_hom (κ : HOM) : IT_hom (`κ).
+  Proof.
+    apply (proj2_sig κ).
+  Qed.
+
+  Program Definition HOM_id : HOM := exist _ idfun _.
+  Next Obligation.
+    apply _.
+  Qed.
+
+  Lemma HOM_ccompose (f g : HOM) :
+    ∀ α, `f (`g α) = (`f ◎ `g) α.
+  Proof.
+    intro; reflexivity.
+  Qed.
+
+  Program Definition HOM_compose (f g : HOM) : HOM := exist _ (`f ◎ `g) _.
+  Next Obligation.
+    intros f g; simpl.
+    apply _.
+  Qed.
+
+  Lemma HOM_compose_ccompose (f g h : HOM) :
+    h = HOM_compose f g ->
+    `f ◎ `g = `h.
+  Proof. intros ->. done. Qed.
+
+  Program Definition IFSCtx_HOM α β : HOM := exist _ (λne x, IFSCtx α β x) _.
+  Next Obligation.
+    intros; simpl.
+    apply _.
+  Qed.
+
+  Program Definition NatOpRSCtx_HOM {S : Set} (op : nat_op)
+    (α : @interp_scope F natO _ S -n> IT) (env : @interp_scope F natO _ S)
+    : HOM := exist _ (interp_natoprk rs op α (λne env, idfun) env) _.
+  Next Obligation.
+    intros; simpl.
+    apply _.
+  Qed.
+
+  Program Definition NatOpLSCtx_HOM {S : Set} (op : nat_op)
+    (α : IT) (env : @interp_scope F natO _ S)
+    (Hv : AsVal α)
+    : HOM := exist _ (interp_natoplk rs op (λne env, idfun) (constO α) env) _.
+  Next Obligation.
+    intros; simpl.
+    apply _.
+  Qed.
+
+  Program Definition ThrowLSCtx_HOM {S : Set}
+    (α : @interp_scope F natO _ S -n> IT)
+    (env : @interp_scope F natO _ S)
+    : HOM := exist _ ((interp_throwlk rs (λne env, idfun) α env)) _.
+  Next Obligation.
+    intros; simpl.
+    apply _.
+  Qed.
+
+  Program Definition ThrowRSCtx_HOM {S : Set}
+    (β : IT) (env : @interp_scope F natO _ S)
+    (Hv : AsVal β)
+    : HOM := exist _ (interp_throwrk rs (constO β) (λne env, idfun) env) _.
+  Next Obligation.
+    intros; simpl.
+    simple refine (IT_HOM _ _ _ _ _); intros; simpl.
+    - solve_proper_please.
+    - destruct Hv as [? <-].
+      rewrite ->2 get_val_ITV.
+      simpl. by rewrite get_fun_tick.
+    - destruct Hv as [x Hv].
+      rewrite <- Hv.
+      rewrite -> get_val_ITV.
+      simpl.
+      rewrite get_fun_vis.
+      repeat f_equiv.
+      intro; simpl.
+      rewrite <- Hv.
+      by rewrite -> get_val_ITV.
+    - destruct Hv as [? <-].
+      rewrite get_val_ITV.
+      simpl.
+      by rewrite get_fun_err.
+  Qed.
+
+  Program Definition OutputSCtx_HOM {S : Set}
+    (env : @interp_scope F natO _ S)
+    : HOM := exist _ ((interp_outputk rs (λne env, idfun) env)) _.
+  Next Obligation.
+    intros; simpl.
+    apply _.
+  Qed.
+
+  Program Definition AppRSCtx_HOM {S : Set}
+    (α : @interp_scope F natO _ S -n> IT)
+    (env : @interp_scope F natO _ S)
+    : HOM := exist _ (interp_apprk rs α (λne env, idfun) env) _.
+  Next Obligation.
+    intros; simpl.
+    apply _.
+  Qed.
+
+  Program Definition AppLSCtx_HOM {S : Set}
+    (β : IT) (env : @interp_scope F natO _ S)
+    (Hv : AsVal β)
+    : HOM := exist _ (interp_applk rs (λne env, idfun) (constO β) env) _.
+  Next Obligation.
+    intros; simpl.
+    apply _.
+  Qed.
+
+End hom.