simple ffi examples

simple ffi examples

- store effect is now more general (can be polymorphic in ctx dep bit)
- delimlang embedded into a language with higher-order heap
- type system + interpretation + safety wrt GITree eq. th.
- an example without glue code, which is well-typed, but
  unguarded shift captures heap lang ctx, which results in a wrong computation

missing build instruction

_CoqProject

@@ -46,6 +46,7 @@ theories/examples/delim_lang/hom.v
 theories/examples/delim_lang/example.v
 theories/examples/delim_lang/logpred.v
 theories/examples/delim_lang/logrel.v
+theories/examples/delim_lang/glue.v
 
 theories/examples/input_lang_callcc/lang.v
 theories/examples/input_lang_callcc/interp.v

theories/effects/store.v

@@ -128,10 +128,10 @@ End constructors.
 
 Section wp.
   Context {n : nat}.
-  Variable (rs : gReifiers NotCtxDep n).
-  Context {R} `{!Cofe R}.
-  Context `{!SubOfe unitO R}.
-
+  Context {a : is_ctx_dep}.
+  Variable (rs : gReifiers a n).
+  Context {R} {CR : Cofe R}.
+  Context {SO : SubOfe unitO R}.
   Notation F := (gReifiers_ops rs).
   Notation IT := (IT F R).
   Notation ITV := (ITV F R).
@@ -157,7 +157,7 @@ Section wp.
     iModIntro. iExists sg. by iFrame.
   Qed.
 
-  Context `{!subReifier reify_store rs}.
+  Context `{!subReifier (sReifier_NotCtxDep_min reify_store a) rs}.
   Context `{!invGS_gen HasLc Σ, !stateG rs R Σ}.
   Notation iProp := (iProp Σ).
 
@@ -169,6 +169,10 @@ Section wp.
                         (∃ σ, £ 1 ∗ has_substate σ ∗ own heapG_name (●V σ))%I.
   Definition pointsto (l : loc) (α : IT) : iProp :=
     own heapG_name $ gmap_view_frag l (DfracOwn 1) (Next α).
+  Global Instance pointsto_proper l : Proper ((≡) ==> (≡)) (pointsto l).
+  Proof. solve_proper. Qed.
+  Global Instance pointsto_ne l : NonExpansive (pointsto l).
+  Proof. solve_proper. Qed.
 
   Lemma istate_alloc α l σ :
     σ !! l = None →
@@ -225,7 +229,7 @@ Section wp.
   Proof.
     iIntros (Hee) "#Hcxt H".
     unfold READ. simpl.
-    iApply wp_subreify_ctx_indep'. simpl.
+    iApply wp_subreify_ctx_indep_lift''.
     iInv (nroot.@"storeE") as (σ) "[>Hlc [Hs Hh]]" "Hcl".
     iApply (fupd_mask_weaken E1).
     { set_solver. }
@@ -281,7 +285,7 @@ Section wp.
     WP@{rs} WRITE l β @ s {{ Φ }}.
   Proof.
     iIntros (Hee) "#Hcxt H".
-    iApply wp_subreify_ctx_indep'. simpl.
+    iApply wp_subreify_ctx_indep_lift''. simpl.
     iInv (nroot.@"storeE") as (σ) "[>Hlc [Hs Hh]]" "Hcl".
     iApply (fupd_mask_weaken E1).
     { set_solver. }
@@ -327,7 +331,7 @@ Section wp.
     WP@{rs} ALLOC α k @ s {{ Φ }}.
   Proof.
     iIntros "Hh H".
-    iApply wp_subreify_ctx_indep'. simpl.
+    iApply wp_subreify_ctx_indep_lift''. simpl.
     iInv (nroot.@"storeE") as (σ) "[>Hlc [Hs Hh]]" "Hcl".
     iApply (lc_fupd_elim_later with "Hlc").
     iModIntro.
@@ -355,7 +359,7 @@ Section wp.
     WP@{rs} DEALLOC l @ s {{ Φ }}.
   Proof.
     iIntros (Hee) "#Hcxt H".
-    iApply wp_subreify_ctx_indep'. simpl.
+    iApply wp_subreify_ctx_indep_lift''. simpl.
     iInv (nroot.@"storeE") as (σ) "[>Hlc [Hs Hh]]" "Hcl".
     iApply (fupd_mask_weaken E1).
     { set_solver. }
@@ -395,9 +399,9 @@ Section wp.
 
 End wp.
 
-Arguments heapG {_} rs R {_} Σ.
-Arguments heapPreG {_} rs R {_} Σ.
-Arguments heapΣ {_} rs R {_}.
-Arguments heap_ctx {_ _ _ _ _ _ _ _ _}.
-Arguments pointsto {_ _ _ _ _ _} _ _.
+Arguments heapG {_} {_} rs R {_} Σ.
+Arguments heapPreG {_} {_} rs R {_} Σ.
+Arguments heapΣ {_} {_} rs R {_}.
+Arguments heap_ctx {_ _} rs {_ _ _ _ _ _ _}.
+Arguments pointsto {_ _ _ _ _ _ _} _ _.
 #[global]  Opaque ALLOC READ WRITE DEALLOC.

theories/examples/affine_lang/lang.v

@@ -213,7 +213,7 @@ Section affine.
     end.
 
   Lemma wp_Thunk (β:IT) s (Φ:ITV → iProp) `{!NonExpansive Φ} :
-    ⊢ heap_ctx -∗
+    ⊢ heap_ctx rs -∗
       ▷ (∀ l, pointsto l (Ret 0) -∗ Φ (thunkedV β l)) -∗
       WP@{rs} Thunk β @ s {{ Φ }}.
   Proof.

theories/examples/affine_lang/logrel1.v

@@ -105,9 +105,9 @@ Section logrel.
 
   Notation ssubst_valid := (ssubst_valid_fin1 rs ty (λ x, protected (interp_ty x)) expr_pred).
 
-  Definition valid1 {S : Set} `{!EqDecision S} `{!Finite S} (Ω : S → ty)
+  Program Definition valid1 {S : Set} `{!EqDecision S} `{!Finite S} (Ω : S → ty)
     (α : interp_scope S -n> IT) (τ : ty) : iProp :=
-    ∀ ss, heap_ctx
+    ∀ ss, heap_ctx rs
           -∗ (ssubst_valid Ω ss)
           -∗ expr_pred (α ss) (interp_ty τ).
 

theories/examples/affine_lang/logrel2.v

@@ -127,7 +127,7 @@ Section glue.
 
   Lemma compat_glue_from_affine_bool α :
     valid2 □ α tBool ⊢
-      heap_ctx -∗ io_valid □ α Tnat.
+      heap_ctx rs -∗ io_valid □ α Tnat.
   Proof.
     iIntros "H #Hctx".
     iIntros (σ ss) "Hs Hss".
@@ -143,7 +143,7 @@ Section glue.
 
   Lemma compat_glue_from_affine_nat α :
     valid2 □ α tInt ⊢
-      heap_ctx -∗ io_valid □ α Tnat.
+      heap_ctx rs -∗ io_valid □ α Tnat.
   Proof.
     iIntros "H #Hctx".
     iIntros (σ ss) "Hs Hss".
@@ -157,7 +157,7 @@ Section glue.
 
   Lemma compat_glue_from_affine_unit α :
     valid2 □ α tUnit ⊢
-      heap_ctx -∗ io_valid □ (constO (glue_from_affine _ ty_conv_unit (α ı_scope))) Tnat.
+      heap_ctx rs -∗ io_valid □ (constO (glue_from_affine _ ty_conv_unit (α ı_scope))) Tnat.
   Proof.
     iIntros "H #Hctx".
     iIntros (σ ss) "Hs Hss".
@@ -174,9 +174,9 @@ Section glue.
     (∀ α, io_valid □ α τ1'
             ⊢ valid2 □ (constO (glue_to_affine (α ı_scope))) τ1) →
     (∀ α,  valid2 □ (constO α) τ2
-             ⊢ heap_ctx -∗ io_valid □ (constO (glue_from_affine α)) τ2') →
+             ⊢ heap_ctx rs -∗ io_valid □ (constO (glue_from_affine α)) τ2') →
     valid2 □ (constO α) (tArr τ1 τ2)
-    ⊢ heap_ctx -∗
+    ⊢ heap_ctx rs -∗
       io_valid □
          (constO (glue_from_affine_fun _ glue_from_affine glue_to_affine α))
          (Tarr (Tarr Tnat τ1') τ2').
@@ -288,7 +288,7 @@ Section glue.
     (∀ α, io_valid □ α τ2'
             ⊢ valid2 Ω (constO (glue_to_affine (α ı_scope))) τ2) →
     (∀ α,  valid2 □ (constO α) τ1
-             ⊢ heap_ctx -∗ io_valid □ (constO (glue_from_affine α)) τ1') →
+             ⊢ heap_ctx rs -∗ io_valid □ (constO (glue_from_affine α)) τ1') →
     io_valid □ α (Tarr (Tarr Tnat τ1') τ2')
       ⊢ valid2 Ω
       (constO (glue_to_affine_fun _ glue_from_affine glue_to_affine (α ı_scope)))
@@ -422,7 +422,7 @@ Section glue.
     io_valid □ α τ1' ⊢ valid2 Ω (constO (glue_to_affine _ Hconv (α ı_scope))) τ1
   with glue_from_affine_compatibility (τ1 : ty) (τ1' : io_lang.ty)
     (Hconv : ty_conv τ1 τ1') (α : IT) :
-    valid2 □ (constO α) τ1 ⊢ heap_ctx -∗ io_valid □ (constO (glue_from_affine _ Hconv α)) τ1'.
+    valid2 □ (constO α) τ1 ⊢ heap_ctx rs -∗ io_valid □ (constO (glue_from_affine _ Hconv α)) τ1'.
   Proof.
     - destruct Hconv.
       + by iApply compat_glue_to_affine_bool.

theories/examples/delim_lang/example.v

@@ -12,46 +12,44 @@ Open Scope syn_scope.
 Example p : expr Empty_set :=
   ((#1) + (reset ((#3) + (shift/cc ((($0) @k #5) + (($0) @k #6)))))).
 
+Global Ltac shift_hom :=
+  match goal with
+  | |- envs_entails _ (wp _ (ofe_mor_car _ _ (λne x, ?k1 x) (?k2 ?t)) _ _ _) =>
+      assert ((ofe_mor_car _ _ (λne x, k1 x) (k2 t)) ≡ (λne x, k1 (k2 x)) t) as -> by done
+  | |- envs_entails _ (wp _ (?k ?t) _ _ _) =>
+      assert (k t ≡ (λne x, k x) t) as -> by done
+  end.
+
+Global Ltac shift_natop_l :=
+  match goal with
+  | |- envs_entails _ (wp _ (ofe_mor_car _ _ (λne x, ?k1 x)
+                              (ofe_mor_car _ _
+                                 (ofe_mor_car _ _
+                                    (NATOP (do_natop lang.Add)) ?t) (IT_of_V ?e))) _ _ _) =>
+      assert ((ofe_mor_car _ _ (λne x, k1 x) (NATOP (do_natop lang.Add) t (IT_of_V e))) ≡
+                (λne x, k1 (NATOP (do_natop lang.Add) x (IT_of_V e))) t) as -> by done
+  end.
+
+Section proof.
+
+  Context {sz : nat}.
+  Variable rs : gReifiers CtxDep sz.
+  Context `{!subReifier reify_delim rs}.
 
-Section example.
-  Local Definition rs : gReifiers _ _ := gReifiers_cons reify_delim gReifiers_nil.
   Notation F := (gReifiers_ops rs).
   Context {R} `{!Cofe R}.
-  Context `{!SubOfe natO R, !SubOfe unitO R}.
+  Context `{!SubOfe natO R}.
   Notation IT := (IT F R).
   Notation ITV := (ITV F R).
-  Context (env : @interp_scope F R _ Empty_set).
-
-  Definition ts := interp_config rs (Cexpr p) env.
-  Definition t := fst ts.
-  Definition σ := snd ts.
-
 
-  Context `{!invGS Σ, !stateG rs R Σ, !heapG rs R Σ}.
+  Context `{!invGS Σ, !stateG rs R Σ}.
   Notation iProp := (iProp Σ).
 
-
-  Ltac shift_hom :=
-    match goal with
-    | |- envs_entails _ (wp _ (ofe_mor_car _ _ (λne x, ?k1 x) (?k2 ?t)) _ _ _) =>
-        assert ((ofe_mor_car _ _ (λne x, k1 x) (k2 t)) ≡ (λne x, k1 (k2 x)) t) as -> by done
-    | |- envs_entails _ (wp _ (?k ?t) _ _ _) =>
-        assert (k t ≡ (λne x, k x) t) as -> by done
-    end.
-
-  Ltac shift_natop_l :=
-    match goal with
-    | |- envs_entails _ (wp _ (ofe_mor_car _ _ (λne x, ?k1 x)
-                                 (ofe_mor_car _ _
-                                    (ofe_mor_car _ _
-                                       (NATOP (do_natop lang.Add)) ?t) (IT_of_V ?e))) _ _ _) =>
-        assert ((ofe_mor_car _ _ (λne x, k1 x) (NATOP (do_natop lang.Add) t (IT_of_V e))) ≡
-                  (λne x, k1 (NATOP (do_natop lang.Add) x (IT_of_V e))) t) as -> by done
-    end.
-
-  Lemma wp_t (s : gitree.weakestpre.stuckness) :
-    has_substate σ -∗
-                      WP@{rs} t @ s {{βv, βv ≡ RetV 18}}.
+  Lemma wp_t σ (s : gitree.weakestpre.stuckness) :
+    (⊢ has_substate σ
+       -∗ WP@{rs} (interp_expr _ p ı_scope) @ s
+            {{ βv, βv ≡ RetV 18
+                   ∗ has_substate σ }})%I.
   Proof.
     Opaque SHIFT APP_CONT.
     iIntros "Hσ".
@@ -106,8 +104,10 @@ Section example.
     iIntros "!> _ Hσ". simpl.
     rewrite IT_of_V_Ret NATOP_Ret.
     simpl. rewrite -(IT_of_V_Ret 18).
-    iApply (wp_pop_end with "Hσ").
-    iIntros "!> _ _".
-    iApply wp_val. done.
+    iApply wp_val.
+    iModIntro.
+    iFrame "Hσ".
+    done.
   Qed.
-End example.
+
+End proof.