add missing file

theories/typing/lib/diverging_static.v

+From iris.proofmode Require Import tactics.
+From iris.base_logic Require Import big_op.
+From lrust.typing Require Export type.
+From lrust.typing Require Import typing.
+Set Default Proof Using "Type".
+
+Section diverging_static.
+  Context `{!typeG Σ}.
+
+  (* Show that we can convert any live borrow to 'static with an infinite
+     loop. *)
+  Definition diverging_static_loop (call_once : val) : val :=
+    funrec: <> ["x"; "f"] :=
+      let: "call_once" := call_once in
+      letcall: "ret" := "call_once" ["f"; "x"]%E in
+    withcont: "loop":
+      "loop" []
+    cont: "loop" [] :=
+      "loop" [].
+
+  Lemma diverging_static_loop_type T F call_once
+        `{!TyWf T, !TyWf F} :
+    (* F : FnOnce(&'static T), as witnessed by the impl call_once *)
+    typed_val call_once (fn(∅; F, &shr{static} T) → unit) →
+    typed_val (diverging_static_loop call_once)
+              (fn(∀ α, λ ϝ, T.(ty_outlives_E) static; &shr{α} T, F) → emp).
+  Proof.
+    intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ϝ ret arg). inv_vec arg=>x f. simpl_subst.
+    iApply type_let; [apply Hf|solve_typing|]. iIntros (call); simpl_subst.
+    (* Drop to Iris *)
+    iIntros (tid) "#LFT #HE Hna HL Hk (Hcall & Hx & Hf & _)".
+    (* We need a ϝ token to show that we can call F despite it being non-'static. *)
+    iMod (lctx_lft_alive_tok ϝ with "HE HL") as (qϝ) "(Hϝ & HL & _)";
+      [solve_typing..|].
+    iMod (lctx_lft_alive_tok α with "HE HL") as (q) "(Hα & _ & _)";
+      [solve_typing..|].
+    iMod (lft_eternalize with "Hα") as "#Hα".
+    iAssert (type_incl (box (&shr{α} T)) (box (&shr{static} T))) as "#[_ [Hincl _]]".
+    { iApply box_type_incl. iNext. iApply shr_type_incl; first done.
+      iApply type_incl_refl. }
+    wp_let. rewrite tctx_hasty_val.
+    iApply (type_call_iris _ [ϝ] () [_; _] with "LFT HE Hna [Hϝ] Hcall [Hx Hf]").
+    - solve_typing.
+    - solve_to_val.
+    - by rewrite /= (right_id static).
+    - simpl. iFrame. iSplit; last done. rewrite !tctx_hasty_val.
+      iApply "Hincl". done.
+    - iClear "Hα Hincl". iIntros (r) "Htl Hϝ1 Hret". wp_rec.
+      (* Go back to the type system. *)
+      iApply (type_type _ [] _ [] with "[] LFT HE Htl [] Hk [-]"); last first.
+      { rewrite /tctx_interp /=. done. }
+      { rewrite /llctx_interp /=. done. }
+      iApply (type_cont [] [] (λ _, [])).
+      + iIntros (?). simpl_subst. iApply type_jump; solve_typing.
+      + iIntros "!#" (? args). inv_vec args. simpl_subst. iApply type_jump; solve_typing.
+  Qed.
+
+End diverging_static.