comments

theories/affine_lang/logrel1.v

@@ -3,6 +3,7 @@ From Equations Require Import Equations.
 From gitrees Require Export lang_generic gitree program_logic.
 From gitrees.affine_lang Require Import lang.
 From gitrees.examples Require Import store pairs.
+Require Import iris.algebra.gmap.
 
 Local Notation tyctx := (tyctx ty).
 
@@ -69,9 +70,9 @@ Section logrel.
   Variable (P : A → iProp).
   Context `{!NonExpansive P}.
   Local Notation expr_pred := (expr_pred s rs P).
-  Context {HCI : ∀ o : opid (sReifier_ops (gReifiers_sReifier rs)),
-             CtxIndep (gReifiers_sReifier rs)
-               (ITF_solution.IT (sReifier_ops (gReifiers_sReifier rs)) R) o}.
+  Context {HCI :
+      ∀ o : opid (sReifier_ops (gReifiers_sReifier rs)),
+             CtxIndep (gReifiers_sReifier rs) IT o}.
 
   (* interpreting tys *)
   Program Definition protected (Φ : ITV -n> iProp) : ITV -n> iProp := λne αv,
@@ -421,11 +422,8 @@ Arguments interp_ty {_ _ _ _ _ _ _ _ _ _ _ _ _ _ _} τ.
 
 Local Definition rs : gReifiers 2 := gReifiers_cons reify_store (gReifiers_cons input_lang.interp.reify_io gReifiers_nil).
 
-Require Import iris.algebra.gmap.
-
 Local Instance CtxIndepInputLang R `{!Cofe R} (o : opid (sReifier_ops (gReifiers_sReifier rs))) :
-  CtxIndep (gReifiers_sReifier rs)
-    (ITF_solution.IT (sReifier_ops (gReifiers_sReifier rs)) R) o.
+  CtxIndep (gReifiers_sReifier rs) (IT (gReifiers_ops rs) R) o.
 Proof.
   destruct o as [x o].
   inv_fin x.
@@ -616,6 +614,7 @@ Proof.
 Qed.
 
 Definition R := sumO locO (sumO unitO natO).
+
 Lemma logrel1_safety e τ (β : IT (gReifiers_ops rs) R) st st' k :
   typed empC e τ →
   ssteps (gReifiers_sReifier rs) (interp_expr rs e ()) st β st' k →

theories/affine_lang/logrel2.v

@@ -4,6 +4,7 @@ From gitrees Require Export lang_generic gitree program_logic.
 From gitrees.input_lang Require Import lang interp logpred.
 From gitrees.affine_lang Require Import lang logrel1.
 From gitrees.examples Require Import store pairs.
+Require Import iris.algebra.gmap.
 
 Local Notation tyctx := (tyctx ty).
 
@@ -69,9 +70,9 @@ Section glue.
   Context `{!invGS Σ, !stateG rs R Σ, !heapG rs R Σ, !na_invG Σ}.
   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}.
+  Context {HCI :
+      ∀ o : opid (sReifier_ops (gReifiers_sReifier rs)),
+             CtxIndep (gReifiers_sReifier rs) IT o}.
 
   Definition s : stuckness := λ e, e = OtherError.
   Variable p : na_inv_pool_name.
@@ -460,11 +461,9 @@ End glue.
 
 Local Definition rs : gReifiers 2 := gReifiers_cons reify_store (gReifiers_cons input_lang.interp.reify_io gReifiers_nil).
 
-Require Import iris.algebra.gmap.
-
 Local Instance CtxIndepInputLang R `{!Cofe R} (o : opid (sReifier_ops (gReifiers_sReifier rs))) :
   CtxIndep (gReifiers_sReifier rs)
-    (ITF_solution.IT (sReifier_ops (gReifiers_sReifier rs)) R) o.
+    (IT (sReifier_ops (gReifiers_sReifier rs)) R) o.
 Proof.
   destruct o as [x o].
   inv_fin x.

theories/gitree/greifiers.v

@@ -168,22 +168,10 @@ Section greifiers.
         (k : (Outs (sReifier_ops r op) ♯ X -n> laterO X)) :
       sReifier_re r op (x, s1, k) ≡{m}≡ Some (y, s2) →
       sReifier_re (rs !!! sR_idx) (subEff_opid op)
-        (subEff_ins x, sR_state s1, ccompose k (subEff_outs ^-1)) ≡{m}≡
+        (subEff_ins x, sR_state s1, k ◎ (subEff_outs ^-1)) ≡{m}≡
         Some (y, sR_state s2)
     }.
 
-  Lemma ccompose_id_l {A B : ofe} (f : A -n> B) :
-    cid ◎ f ≡ f.
-  Proof.
-    intros x; reflexivity.
-  Qed.
-
-  Lemma ccompose_id_r {A B : ofe} (f : A -n> B) :
-    f ◎ cid ≡ f.
-  Proof.
-    intros x; reflexivity.
-  Qed.
-
   #[global] Instance subReifier_here {n} (r : sReifier) (rs : gReifiers n) :
     subReifier r (gReifiers_cons r rs).
   Proof.
@@ -233,7 +221,7 @@ Section greifiers.
     (s1 s2 : sReifier_state r ♯ X) :
     sReifier_re r op (x, s1, k) ≡ Some (y, s2) →
       sReifier_re (rs !!! sR_idx) (subEff_opid op)
-        (subEff_ins x, sR_state s1, ccompose k (subEff_outs ^-1)) ≡
+        (subEff_ins x, sR_state s1, k ◎ (subEff_outs ^-1)) ≡
         Some (y, sR_state s2).
   Proof.
     intros Hx. apply equiv_dist=>m.
@@ -248,7 +236,7 @@ Section greifiers.
     (σ σ' : sReifier_state r ♯ X) (rest : gState_rest sR_idx rs ♯ X) :
     sReifier_re r op (x, σ, k) ≡ Some (y, σ') →
     gReifiers_re rs (subEff_opid op)
-      (subEff_ins x, gState_recomp rest (sR_state σ), ccompose k (subEff_outs ^-1))
+      (subEff_ins x, gState_recomp rest (sR_state σ), k ◎ (subEff_outs ^-1))
       ≡ Some (y, gState_recomp rest (sR_state σ')).
   Proof.
     intros Hre.
@@ -280,7 +268,7 @@ Section greifiers.
     (s1 s2 : sReifier_state r ♯ X) :
         sReifier_re r op (x, s1, k) ≡ Some (y, s2) ⊢@{iProp}
         sReifier_re (rs !!! sR_idx) (subEff_opid op)
-          (subEff_ins x, sR_state s1, ccompose k (subEff_outs ^-1)) ≡
+          (subEff_ins x, sR_state s1, k ◎ (subEff_outs ^-1)) ≡
           Some (y, sR_state s2).
   Proof.
     apply uPred.internal_eq_entails=>m.
@@ -299,7 +287,7 @@ Section greifiers.
     (σ σ' : sReifier_state r ♯ X) (rest : gState_rest sR_idx rs ♯ X) :
     sReifier_re r op (x,σ, k) ≡ Some (y, σ') ⊢@{iProp}
     gReifiers_re rs (subEff_opid op)
-      (subEff_ins x, gState_recomp rest (sR_state σ), ccompose k (subEff_outs ^-1))
+      (subEff_ins x, gState_recomp rest (sR_state σ), k ◎ (subEff_outs ^-1))
       ≡ Some (y, gState_recomp rest (sR_state σ')).
   Proof.
     apply uPred.internal_eq_entails=>m.

theories/input_lang/interp.v

@@ -169,7 +169,7 @@ Section weakestpre.
   Proof.
     intros Hs. iIntros "Hs Ha".
     unfold OUTPUT. simpl.
-    iApply (wp_subreify rs _ _ _ _ _ _ _ with "Hs").
+    iApply (wp_subreify rs with "Hs").
     { simpl. by rewrite Hs. }
     { simpl. done. }
     iModIntro. iIntros "H1 H2".

theories/input_lang_callcc/interp.v

@@ -237,7 +237,7 @@ Section weakestpre.
     + done.
     + done.
   Qed.
-  
+
 
   Lemma wp_output (σ σ' : stateO) (n : nat) Φ s :
     update_output n σ = σ' →
@@ -251,16 +251,6 @@ Section weakestpre.
     iApply wp_val. iApply ("Ha" with "Hcl Hs").
   Qed.
 
-  (* Proof. *)
-  (*   intros Hs. iIntros "Hs Ha". *)
-  (*   unfold OUTPUT. simpl. *)
-  (*   iApply (wp_subreify with "Hs"). *)
-  (*   { simpl. by rewrite Hs. } *)
-  (*   { simpl. done. } *)
-  (*   iModIntro. iIntros "H1 H2". *)
-  (*   iApply wp_val. by iApply ("Ha" with "H1 H2"). *)
-  (* Qed. *)
-
   Lemma wp_throw' (σ : stateO) (f : laterO (IT -n> IT)) (x : IT)
     (κ : IT -n> IT) `{!IT_hom κ} Φ s :
     has_substate σ -∗
@@ -272,7 +262,6 @@ Section weakestpre.
     iApply (wp_subreify with "Hs"); simpl; done.
   Qed.
 
-
   Lemma wp_throw (σ : stateO) (f : laterO (IT -n> IT)) (x : IT) Φ s :
     has_substate σ -∗
     ▷ (£ 1 -∗ has_substate σ -∗ WP@{rs} later_car f x @ s {{ Φ }}) -∗

theories/lang_generic.v

@@ -196,8 +196,7 @@ Section kripke_logrel.
 
   Lemma expr_pred_bind f `{!IT_hom f} α Φ Ψ `{!NonExpansive Φ}
     {G : ∀ o : opid (sReifier_ops (gReifiers_sReifier rs)),
-       CtxIndep (gReifiers_sReifier rs)
-         (ITF_solution.IT (sReifier_ops (gReifiers_sReifier rs)) R) o} :
+       CtxIndep (gReifiers_sReifier rs) IT o} :
     expr_pred α Ψ ⊢
     (∀ αv, Ψ αv -∗ expr_pred (f (IT_of_V αv)) Φ) -∗
     expr_pred (f α) Φ.

theories/prelude.v

@@ -12,6 +12,18 @@ Program Definition idfun {A : ofe} : A -n> A := λne x, x.
 (** OFEs stuff *)
 Notation "F ♯ E" := (oFunctor_apply F E) (at level 20, right associativity).
 
+Lemma ccompose_id_l {A B : ofe} (f : A -n> B) :
+  cid ◎ f ≡ f.
+Proof.
+  intros x; reflexivity.
+Qed.
+
+Lemma ccompose_id_r {A B : ofe} (f : A -n> B) :
+  f ◎ cid ≡ f.
+Proof.
+  intros x; reflexivity.
+Qed.
+
 Infix "≃" := (ofe_iso) (at level 50).
 
 Definition ofe_iso_1' {A B : ofe} (p : A ≃ B) : A → B := ofe_iso_1 p.