From bc3c1ccdad664b475b5c5de5b922a37986e5da53 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 12 May 2017 09:09:15 +0200
Subject: [PATCH] Lemma to call a rust-typed function from Iris

---
 theories/typing/cont_context.v |   2 +-
 theories/typing/function.v     | 114 ++++++++++++++++++++++++---------
 theories/typing/lft_contexts.v |  41 ++++++------
 theories/typing/lib/spawn.v    |   3 +
 4 files changed, 108 insertions(+), 52 deletions(-)

diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index ae290251..0dac90df 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -25,7 +25,7 @@ Section cont_context.
 
   Definition cctx_elt_interp (tid : thread_id) (x : cctx_elt) : iProp Σ :=
     let '(k ◁cont(L, T)) := x in
-    (∀ args, na_own tid ⊤ -∗ llctx_interp L 1 -∗ tctx_interp tid (T args) -∗
+    (∀ args, na_own tid top -∗ 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 Σ :=
     (∀ (x : cctx_elt), ⌜x ∈ C⌝ -∗ cctx_elt_interp tid x)%I.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 4071d4c6..b10f2d91 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -232,59 +232,113 @@ Section typing.
     rewrite /typed_body. iNext. iIntros "*". iApply "Hf".
   Qed.
 
-  Lemma type_call' {A} E L T p (κs : list lft) (ps : list path)
-                         (fp : A → fn_params (length ps)) (k : val) x :
-    Forall (lctx_lft_alive E L) κs →
+  From iris.proofmode Require Import environments. (* FIXME: remove. *)
+
+  (* In principle, proving this hard-coded to an empty L would be sufficient --
+     but then we would have to require elctx_sat as an Iris assumption. *)
+  Lemma type_call_iris' E L (κs : list lft) {A} x qκs qL tid
+        p (ps : list path) (k : expr) (fp : A → fn_params (length ps)) :
     (∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ₑ κ) <$> κs) ++ E) L ((fp x).(fp_E) ϝ)) →
-    typed_body E L [k ◁cont(L, λ v : vec _ 1, (v!!!0 ◁ box (fp x).(fp_ty)) :: T)]
-               ((p ◁ fn fp) ::
-                zip_with TCtx_hasty ps (box <$> (vec_to_list (fp x).(fp_tys))) ++
-                T)
-               (call: p ps → k).
+    is_Some (to_val k) →
+    lft_ctx -∗ elctx_interp E -∗ na_own tid ⊤ -∗ llctx_interp L qL -∗
+    qκs.[lft_intersect_list κs] -∗
+    tctx_elt_interp tid (p ◁ fn fp) -∗
+    ([∗ list] y ∈ zip_with TCtx_hasty ps (box <$> vec_to_list (fp x).(fp_tys)), tctx_elt_interp tid y) -∗
+    (∀ ret, na_own tid top -∗ llctx_interp L qL -∗ qκs.[lft_intersect_list κs] -∗
+             (box (fp x).(fp_ty)).(ty_own) tid [ret] -∗ 
+             WP k [of_val ret] {{ _, cont_postcondition }}) -∗
+    WP (call: p ps → k) {{ _, cont_postcondition }}.
   Proof.
-    iIntros (Hκs HE tid) "#LFT #HE Htl HL HC (Hf & Hargs & HT)".
-    wp_apply (wp_hasty with "Hf"). iIntros (v) "% Hf".
-    iApply (wp_app_vec _ _ (_::_) ((λ v, ⌜v = (λ: ["_r"], (#() ;; #()) ;; k ["_r"])%V⌝):::
+    iIntros (HE [k' Hk']) "#LFT #HE Htl HL Hκs Hf Hargs Hk". rewrite -(of_to_val k k') //.
+    clear dependent k. wp_apply (wp_hasty with "Hf"). iIntros (v) "% Hf".
+    iApply (wp_app_vec _ _ (_::_) ((λ v, ⌜v = (λ: ["_r"], (#() ;; #()) ;; k' ["_r"])%V⌝):::
                vmap (λ ty (v : val), tctx_elt_interp tid (v ◁ box ty)) (fp x).(fp_tys))%I
             with "[Hargs]"); first wp_done.
     - rewrite /=. iSplitR "Hargs".
       { simpl. iApply wp_value; last done. solve_to_val. }
-      clear dependent k p.
-      rewrite /tctx_interp vec_to_list_map !zip_with_fmap_r
-              (zip_with_zip (λ e ty, (e, _))) zip_with_zip !big_sepL_fmap.
-      iApply (big_sepL_mono' with "Hargs"); last done. iIntros (i [p ty]) "HT/=".
-      iApply (wp_hasty with "HT"). setoid_rewrite tctx_hasty_val. iIntros (?) "? $".
+      remember (fp_tys (fp x)) as tys. clear dependent k' p HE fp x.
+      iInduction ps as [|p ps] "IH" forall (tys); first by simpl.
+      simpl in tys. inv_vec tys=>ty tys. simpl.
+      iDestruct "Hargs" as "[HT Hargs]". iSplitL "HT".
+      + iApply (wp_hasty with "HT"). iIntros (?). rewrite tctx_hasty_val. iIntros "? $".
+      + iApply "IH". done.
     - simpl. change (@length expr ps) with (length ps).
       iIntros (vl'). inv_vec vl'=>kv vl.
       iIntros "/= [% Hvl]". subst kv. iDestruct "Hf" as (fb kb xb e ?) "[EQ [EQl #Hf]]".
-      iDestruct "EQ" as %[=->]. iDestruct "EQl" as %EQl. revert vl fp HE.
-      rewrite <-EQl=>vl fp HE. iApply wp_rec; try done.
+      iDestruct "EQ" as %[=->]. iDestruct "EQl" as %EQl.
+      revert vl fp HE. rewrite <-EQl=>vl fp HE. iApply wp_rec; try done.
       { rewrite -fmap_cons Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. }
       { rewrite -fmap_cons -(subst_v_eq (fb::kb::xb) (_:::_:::vl)) //. }
       iNext. iMod (lft_create with "LFT") as (ϝ) "[Htk #Hinh]"; first done.
-      iSpecialize ("Hf" $! x ϝ _ vl).
-      iDestruct (HE ϝ with "HL") as "#HE'".
-      iMod (lctx_lft_alive_list with "LFT [# $HE //] HL") as "[#HEE Hclose]"; [done..|].
-      iApply ("Hf" with "LFT [>] Htl [Htk] [HC HT Hclose]").
-      + iApply "HE'". iFrame "#". auto.
+      iSpecialize ("Hf" $! x ϝ _ vl). iDestruct (HE ϝ with "HL") as "#HE'".
+      iMod (bor_create _ ϝ with "LFT Hκs") as "[Hκs HκsI]"; first done.
+      iDestruct (frac_bor_lft_incl with "LFT [>Hκs]") as "#Hκs".
+      { iApply (bor_fracture with "LFT"); first done. by rewrite Qp_mult_1_r. }
+      iApply ("Hf" with "LFT [] Htl [Htk] [Hk HκsI HL]").
+      + iApply "HE'". iFrame "#". iClear "Hf Hinh HE' LFT HE". clear.
+        (* FIXME: iInduction κs as [|κ κs] "IH". fails. *)
+        iRevert "Hκs". rewrite /coq_tactics.of_envs /=.
+        rewrite uPred.sep_elim_r. induction κs; iIntros "_ #Hκs"; simpl; first done.
+        iSplitL.
+        { iApply lft_incl_trans; first done. iApply lft_intersect_incl_l. }
+        iApply IHκs; first by auto. iAlways.
+        iApply lft_incl_trans; first done. iApply lft_intersect_incl_r.
       + iSplitL; last done. iExists ϝ. iSplit; first by rewrite /= left_id.
         iFrame "#∗".
       + iIntros (y) "IN". iDestruct "IN" as %->%elem_of_list_singleton.
-        iIntros (args) "Htl [HL _] Hret". inv_vec args=>r.
-        iDestruct "HL" as  (κ') "(EQ & Htk & _)". iDestruct "EQ" as %EQ.
+        iIntros (args) "Htl [Hϝ _] [Hret _]". inv_vec args=>r.
+        iDestruct "Hϝ" as  (κ') "(EQ & Htk & _)". iDestruct "EQ" as %EQ.
         rewrite /= left_id in EQ. subst κ'. simpl. wp_rec. wp_bind Endlft.
-        iSpecialize ("Hinh" with "Htk").
+        iSpecialize ("Hinh" with "Htk"). iClear "Hκs".
         iApply (wp_mask_mono (↑lftN)); first done.
         iApply (wp_step_fupd with "Hinh"); [solve_ndisj..|]. wp_seq.
-        iIntros "#Htok !>". wp_seq. iMod ("Hclose" with "Htok") as "HL".
-        iSpecialize ("HC" with "[]"); first by (iPureIntro; apply elem_of_list_singleton).
-        iApply ("HC" $! [#r] with "Htl HL").
-        rewrite tctx_interp_singleton tctx_interp_cons. iFrame.
+        iIntros "#Htok !>". wp_seq. iMod ("HκsI" with "Htok") as ">Hκs".
+        iApply ("Hk" with "Htl HL Hκs"). rewrite tctx_hasty_val. done.
       + rewrite /tctx_interp vec_to_list_map !zip_with_fmap_r
                 (zip_with_zip (λ v ty, (v, _))) zip_with_zip !big_sepL_fmap.
         iApply (big_sepL_mono' with "Hvl"); last done. by iIntros (i [v ty']).
   Qed.
 
+  Lemma type_call_iris E (κs : list lft) {A} x qκs tid
+        p (ps : list path) (k : expr) (fp : A → fn_params (length ps)) :
+    (∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ₑ κ) <$> κs) ++ E) [] ((fp x).(fp_E) ϝ)) →
+    is_Some (to_val k) →
+    lft_ctx -∗ elctx_interp E -∗ na_own tid ⊤ -∗
+    qκs.[lft_intersect_list κs] -∗
+    tctx_elt_interp tid (p ◁ fn fp) -∗
+    ([∗ list] y ∈ zip_with TCtx_hasty ps (box <$> vec_to_list (fp x).(fp_tys)), tctx_elt_interp tid y) -∗
+    (∀ ret, na_own tid top -∗ qκs.[lft_intersect_list κs] -∗
+             (box (fp x).(fp_ty)).(ty_own) tid [ret] -∗ 
+             WP k [of_val ret] {{ _, cont_postcondition }}) -∗
+    WP (call: p ps → k) {{ _, cont_postcondition }}.
+  Proof.
+    iIntros (HE Hk') "#LFT #HE Htl Hκs Hf Hargs Hk".
+    iApply (type_call_iris' with "LFT HE Htl [] Hκs Hf Hargs [Hk]"); [done..| |].
+    - instantiate (1 := 1%Qp). by rewrite /llctx_interp.
+    - iIntros "* Htl _". iApply "Hk". done.
+  Qed.
+
+  Lemma type_call' E L (κs : list lft) T p (ps : list path)
+                   {A} (fp : A → fn_params (length ps)) (k : val) x :
+    Forall (lctx_lft_alive E L) κs →
+    (∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ₑ κ) <$> κs) ++ E) L ((fp x).(fp_E) ϝ)) →
+    typed_body E L [k ◁cont(L, λ v : vec _ 1, (v!!!0 ◁ box (fp x).(fp_ty)) :: T)]
+               ((p ◁ fn fp) ::
+                zip_with TCtx_hasty ps (box <$> vec_to_list (fp x).(fp_tys)) ++
+                T)
+               (call: p ps → k).
+  Proof.
+    iIntros (Hκs HE tid) "#LFT #HE Htl HL HC (Hf & Hargs & HT)".
+    iMod (lctx_lft_alive_tok_list _ _ κs with "HE HL") as (q) "(Hκs & HL & Hclose)"; [done..|].
+    iApply (type_call_iris' with "LFT HE Htl HL Hκs Hf Hargs"); [done|solve_to_val|].
+    iIntros (r) "Htl HL Hκs Hret". iMod ("Hclose" with "Hκs HL") as "HL".
+    iSpecialize ("HC" with "[]"); first by (iPureIntro; apply elem_of_list_singleton).
+    iApply ("HC" $! [#r] with "Htl HL").
+    rewrite tctx_interp_cons tctx_hasty_val. iFrame.
+  Qed.
+
+  (* Specialized type_call':  Adapted for use by solve_typing; fixed "list of
+     alive lifetimes" to be the local ones. *)
   Lemma type_call {A} x E L C T T' T'' p (ps : list path)
                         (fp : A → fn_params (length ps)) k :
     p ◁ fn fp ∈ T →
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index d41c2925..26a448f7 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -171,6 +171,26 @@ Section lft_contexts.
     iApply "Hclose". iFrame.
   Qed.
 
+  Lemma lctx_lft_alive_tok_list κs F q :
+    ↑lftN ⊆ F → Forall lctx_lft_alive κs →
+      elctx_interp E -∗ llctx_interp L q ={F}=∗
+         ∃ q', q'.[lft_intersect_list κs] ∗ llctx_interp L q' ∗
+                   (q'.[lft_intersect_list κs] -∗ llctx_interp L q' ={F}=∗ llctx_interp L q).
+  Proof.
+    iIntros (? Hκs) "#HE". iInduction κs as [|κ κs] "IH" forall (q Hκs).
+    { iIntros "HL !>". iExists _. iFrame "HL". iSplitL; first iApply lft_tok_static.
+      iIntros "_ $". done. }
+    inversion_clear Hκs.
+    iIntros "HL". iMod (lctx_lft_alive_tok κ with "HE HL") as (q') "(Hκ & HL & Hclose1)"; [solve_typing..|].
+    iMod ("IH" with "* [//] HL") as (q'') "(Hκs & HL & Hclose2)".
+    destruct (Qp_lower_bound q' q'') as (qq & q0  & q'0 & -> & ->).
+    iExists qq. iDestruct "HL" as "[$ HL2]". iDestruct "Hκ" as "[Hκ1 Hκ2]".
+    iDestruct "Hκs" as "[Hκs1 Hκs2]". iModIntro. simpl. rewrite -lft_tok_sep. iSplitL "Hκ1 Hκs1".
+    { by iFrame. }
+    iIntros "[Hκ1 Hκs1] HL1". iMod ("Hclose2" with "[$Hκs1 $Hκs2] [$HL1 $HL2]") as "HL".
+    iMod ("Hclose1" with "[$Hκ1 $Hκ2] HL") as "HL". done.
+  Qed.
+
   Lemma lctx_lft_alive_static : lctx_lft_alive static.
   Proof.
     iIntros (F qL ?) "_ $". iExists 1%Qp. iSplitL. by iApply lft_tok_static. auto.
@@ -221,27 +241,6 @@ Section lft_contexts.
     intros. by eapply lctx_lft_alive_incl, lctx_lft_incl_external.
   Qed.
 
-  Lemma lctx_lft_alive_list κs ϝ `{!frac_borG Σ} :
-    Forall lctx_lft_alive κs →
-    ∀ (F : coPset) (qL : Qp),
-      ↑lftN ⊆ F → lft_ctx -∗ elctx_interp E -∗
-         llctx_interp L qL ={F}=∗ elctx_interp ((λ κ, ϝ ⊑ₑ κ) <$> κs) ∗
-                                   ([†ϝ] ={F}=∗ llctx_interp L qL).
-  Proof.
-    iIntros (Hκs F qL ?) "#LFT #HE". iInduction κs as [|κ κs] "IH" forall (qL Hκs).
-    { iIntros "$ !>". rewrite /elctx_interp /=; auto. }
-    iIntros "[HL1 HL2]". inversion Hκs as [|?? Hκ Hκs']. clear Hκs. subst.
-    iMod ("IH" with "[% //] HL2") as "[#Hκs Hclose1] {IH}".
-    iMod (Hκ with "HE HL1") as (q) "[Hκ Hclose2]"; first done.
-    iMod (bor_create with "LFT [Hκ]") as "[Hκ H†]"; first done. iApply "Hκ".
-    iDestruct (frac_bor_lft_incl _ _ q with "LFT [> Hκ]") as "#Hincl".
-    { iApply (bor_fracture with "LFT [>-]"); first done. simpl.
-      rewrite Qp_mult_1_r. done. (* FIXME: right_id? *) }
-    iModIntro. iFrame "#". iIntros "#Hϝ†".
-    iMod ("H†" with "Hϝ†") as ">Hκ". iMod ("Hclose2" with "Hκ") as "$".
-    by iApply "Hclose1".
-  Qed.
-
   (* External lifetime context satisfiability *)
 
   Definition elctx_sat E' : Prop :=
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index a7f02d57..ba16d840 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -105,6 +105,9 @@ Section spawn.
       { iIntros "!> *". rewrite tctx_interp_singleton tctx_hasty_val.
         iIntros "?". by iFrame. }
       iIntros (c) "Hfin". iMod na_alloc as (tid') "Htl". wp_let. wp_let.
+      iApply (type_call_iris _ [] [] tt with "HE [] [] [Hf']"). 5: iExact "Hf'". (* FIXME: Removing the [ ] around Hf' in the spec pattern diverges. *)
+      solve_typing. solve_to_val. rewrite /llctx_interp. done. iApply lft_tok_static.
+      iFrame. done.
       (* FIXME this is horrible. *)
       refine (let Hcall := type_call' _ [] [] f' [] [env:expr]
                 (λ _:(), FP_wf ∅ [# fty] retty) in _).
-- 
GitLab