prove declaring a continuation. it's magic.

_CoqProject

@@ -41,3 +41,4 @@ theories/typing/int.v
 theories/typing/function.v
 theories/typing/programs.v
 theories/typing/mem.v
+theories/typing/cont.v

theories/lang/derived.v

@@ -34,6 +34,12 @@ Lemma wp_let E x e1 e2 v Φ :
   ▷ WP subst' x e1 e2 @ E {{ Φ }} -∗ WP Let x e1 e2 @ E {{ Φ }}.
 Proof. eauto using wp_lam. Qed.
 
+Lemma wp_let' E x e1 e2 v Φ :
+  to_val e1 = Some v →
+  Closed (x :b: []) e2 →
+  ▷ WP subst' x (of_val v) e2 @ E {{ Φ }} -∗ WP Let x e1 e2 @ E {{ Φ }}.
+Proof. intros ?. rewrite (of_to_val e1) //. eauto using wp_let. Qed.
+
 Lemma wp_seq E e1 e2 v Φ :
   to_val e1 = Some v →
   Closed [] e2 →

theories/typing/cont.v

+From iris.base_logic Require Import big_op.
+From iris.proofmode Require Import tactics.
+From lrust.lifetime Require Import borrow.
+From lrust.typing Require Export type.
+From lrust.typing Require Import programs.
+
+Section cont_typing.
+  Context `{typeG Σ}.
+
+  (** Jumping to and defining a continuation. *)
+  (* TODO: On paper, we allow passing paths as arguments to continuations.
+     That however would require the continuation precondition to be parameterized over paths
+     instead of values -- effectively showing that the sort "val" on paper is
+     really for paths, not just for values. *)
+  Lemma typed_jump {n} E L k T' T (args : vec val n) :
+    tctx_incl E L T (T' args) →
+    typed_body E L [CCtx_iscont k L n T'] T (k (of_val <$> (args : list _))).
+  Proof.
+    (* This proofs waits for the problem in typed_call to be figured out:
+       How to best do the induction for reducing the multi-application. *)
+  Abort.
+
+  Lemma typed_cont {n} E L1 L2 C T T' kb (argsb : vec binder n) e1 econt e2 :
+    e1 = Rec kb argsb econt → Closed (kb :b: argsb +b+ []) econt → Closed (kb :b: []) e2 →
+    (∀ k args, typed_body E L1 (CCtx_iscont k L1 n T' :: C) (T' args)
+                          (subst' kb k $ subst_vec argsb (Vector.map of_val $ args) econt)) →
+    (∀ k, typed_body E (L1 ++ L2) (CCtx_iscont k L1 n T' :: C) T (subst' kb k e2)) →
+    typed_body E (L1 ++ L2) C T (let: kb := e1 in e2).
+  Proof.
+    intros -> Hc1 Hc2 Hecont He2. iIntros (tid qE) "#LFT HE HL HC HT".
+    iApply wp_let'.
+    { simpl. rewrite decide_left. done. }
+    iModIntro. iApply (He2 with "* LFT HE HL [HC] HT"). clear He2.
+    iIntros "HE". iLöb as "IH". iIntros (x) "H".
+    iDestruct "H" as %[->|?]%elem_of_cons; last by iApply ("HC" with "HE *").
+    iIntros (args) "HL HT". iApply wp_rec; try done.
+    { apply Forall_of_val_is_val. }
+    { rewrite -vec_to_list_map -subst_vec_eq. eauto. }
+    (* FIXME: iNext here unfolds things in the context. *)
+    iNext. iApply (Hecont with "* LFT HE HL [HC] HT").
+    by iApply "IH".
+  Qed.
+
+End cont_typing.

theories/typing/cont_context.v

@@ -10,7 +10,7 @@ Section cont_context_def.
   Definition cont_postcondition : iProp Σ := False%I.
 
   Record cctx_elt : Type :=
-    CctxElt { cctxe_k : val; cctxe_L : llctx;
+    CCtx_iscont { cctxe_k : val; cctxe_L : llctx;
               cctxe_n : nat; cctxe_T : vec val cctxe_n → tctx }.
   Definition cctx := list cctx_elt.
 End cont_context_def.
@@ -20,7 +20,7 @@ Section cont_context.
   Context `{typeG Σ}.
 
   Definition cctx_elt_interp (tid : thread_id) (x : cctx_elt) : iProp Σ :=
-    let 'CctxElt k L n T := x in
+    let 'CCtx_iscont k L n T := x in
     (∀ args, llctx_interp L 1 -∗ tctx_interp tid (T args) -∗
          WP k (of_val <$> (args : list _)) {{ _, cont_postcondition }})%I.
   Definition cctx_interp (tid : thread_id) (C : cctx) : iProp Σ :=
@@ -35,7 +35,7 @@ Section cont_context.
   Proof.
     rewrite /cctx_interp. iIntros "H". iIntros ([k L n T]) "%".
     iIntros (args) "HL HT". iMod "H".
-    by iApply ("H" $! (CctxElt k L n T) with "[%] * HL HT").
+    by iApply ("H" $! (CCtx_iscont k L n T) with "[%] * HL HT").
   Qed.
 
   Definition cctx_incl (E : elctx) (C1 C2 : cctx): Prop :=
@@ -58,14 +58,14 @@ Section cont_context.
 
   Lemma cctx_incl_cons E k L n T1 T2 C1 C2:
     cctx_incl E C1 C2 → (∀ args, tctx_incl E L (T2 args) (T1 args)) →
-    cctx_incl E (CctxElt k L n T1 :: C1) (CctxElt k L n T2 :: C2).
+    cctx_incl E (CCtx_iscont k L n T1 :: C1) (CCtx_iscont k L n T2 :: C2).
   Proof.
     iIntros (HC1C2 HT1T2 ??) "#LFT H HE". rewrite /cctx_interp.
     iIntros (x) "Hin". iDestruct "Hin" as %[->|Hin]%elem_of_cons.
     - iIntros (args) "HL HT".
       iMod (HT1T2 with "LFT HE HL HT") as "(HE & HL & HT)".
       iSpecialize ("H" with "HE").
-      iApply ("H" $! (CctxElt _ _ _ _) with "[%] * HL HT").
+      iApply ("H" $! (CCtx_iscont _ _ _ _) with "[%] * HL HT").
       constructor.
     - iApply (HC1C2 with "LFT [H] HE * [%]"); last done.
       iIntros "HE". iIntros (x') "%".

theories/typing/function.v

@@ -11,7 +11,7 @@ Section fn.
           (tys : A → vec type n) (ty : A → type) : type :=
     {| st_own tid vl := (∃ f, ⌜vl = [f]⌝ ∗ □ ∀ (x : A) (args : vec val n) (k : val),
          typed_body (E x) []
-                    [CctxElt k [] 1 (λ v, [TCtx_hasty (v!!!0) (ty x)])]
+                    [CCtx_iscont k [] 1 (λ v, [TCtx_hasty (v!!!0) (ty x)])]
                     (zip_with (TCtx_hasty ∘ of_val) args (tys x))
                     (f (of_val <$> (k :: args : list val))))%I |}.
   Next Obligation.
@@ -31,7 +31,7 @@ Section fn.
     - iIntros "HE". unfold cctx_interp. iIntros (e) "He".
       iDestruct "He" as %->%elem_of_list_singleton. iIntros (ret) "HL HT".
       iSpecialize ("HC" with "HE"). unfold cctx_elt_interp.
-      iApply ("HC" $! (CctxElt _ _ _ _) with "[%] * HL >").
+      iApply ("HC" $! (CCtx_iscont _ _ _ _) with "[%] * HL >").
         by apply elem_of_list_singleton.
       rewrite /tctx_interp !big_sepL_singleton /=.
       iDestruct "HT" as (v) "[HP Hown]". iExists v. iFrame "HP".
@@ -90,7 +90,7 @@ Section fn.
   (* TODO: Define some syntactic sugar for calling and letrec like we do on paper. *)
   Lemma typed_call {A n} E L E' T T' (tys : A → vec type n) ty k p (ps : vec path n) x :
     tctx_incl E L T (zip_with TCtx_hasty ps (tys x) ++ T') → elctx_sat E L (E' x) →
-    typed_body E L [CctxElt k L 1 (λ v, (TCtx_hasty (v!!!0) (ty x)) :: T')]
+    typed_body E L [CCtx_iscont k L 1 (λ v, (TCtx_hasty (v!!!0) (ty x)) :: T')]
                (TCtx_hasty p (fn E' tys ty) :: T) (p (of_val k :: ps)).
   Proof.
     (* FIXME: Why can't I merge these iIntros? *)
@@ -119,7 +119,7 @@ Section fn.
   Lemma typed_fn {A n m} E L E' (tys : A → vec type n) ty fb kb (argsb : vec binder n) ef e
        (cps : vec path m) (ctyl : vec type m) `{!LstCopy ctyl, !LstSend ctyl} :
     ef = Rec fb (kb :: argsb) e → Closed (fb :b: kb :b: argsb +b+ []) e →
-    (∀ x f k (args : vec val n), typed_body (E' x) [] [CctxElt k [] 1 (λ v, [TCtx_hasty (v!!!0) (ty x)])]
+    (∀ x f k (args : vec val n), typed_body (E' x) [] [CCtx_iscont k [] 1 (λ v, [TCtx_hasty (v!!!0) (ty x)])]
                  (TCtx_hasty f (fn E' tys ty) ::
                   zip_with (TCtx_hasty ∘ of_val) args (tys x) ++
                   zip_with TCtx_hasty cps ctyl)
@@ -131,13 +131,12 @@ Section fn.
     rewrite tctx_interp_singleton. iLöb as "IH". iExists _. iSplit.
     { simpl. rewrite decide_left. done. }
     iExists _. iSplit; first done. iAlways. clear qE. 
-    iIntros (x args k). iIntros (tid' qE) "_ HE HL HC HT'". 
-    move:(Forall_of_val_is_val (k :: args))=>?.
-    evar (eb:expr). assert (subst_l (kb :: argsb) (of_val <$> k :: args) e = Some eb).
-    { subst eb. rewrite -!vec_to_list_cons -vec_to_list_map -subst_vec_eq. eauto. }
-    rewrite [elctx_interp]lock [llctx_interp]lock [tctx_interp]lock.
-    wp_rec. unlock. subst eb. iApply (Hbody with "* LFT HE HL HC").
+    iIntros (x args k). iIntros (tid' qE) "_ HE HL HC HT'".
+    iApply wp_rec; try done.
+    { apply Forall_of_val_is_val. }
+    { rewrite -!vec_to_list_cons -vec_to_list_map -subst_vec_eq. eauto. }
+    iApply (Hbody with "* LFT HE HL HC").
     rewrite tctx_interp_cons tctx_interp_app. iFrame "HT' IH".
-    iApply tctx_send. done.
+    iApply tctx_send. by iNext.
   Qed.
 End fn.