theories/typing/fixpoint.v → lambda-rust/typing/fixpoint.v

 From lrust.lang Require Import proofmode.
 From lrust.typing Require Export lft_contexts type bool.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 Import uPred.
 
 Section fixpoint_def.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
   Context (T : type → type) {HT: TypeContractive T}.
 
   Global Instance type_inhabited : Inhabited type := populate bool.
@@ -12,7 +12,7 @@ Section fixpoint_def.
   Local Instance type_2_contractive : Contractive (Nat.iter 2 T).
   Proof using Type*.
     intros n ? **. simpl.
-    by apply dist_later_dist, type_dist2_dist_later, HT, HT, type_later_dist2_later.
+    by apply dist_later_S, type_dist2_dist_later, HT, HT, type_later_dist2_later.
   Qed.
 
   Definition type_fixpoint : type := fixpointK 2 T.
@@ -28,25 +28,25 @@ Section fixpoint_def.
   Global Instance type_fixpoint_wf `{!∀ `{!TyWf ty}, TyWf (T ty)} : TyWf type_fixpoint :=
     let lfts :=
       let _ : TyWf type_fixpoint := {| ty_lfts := []; ty_wf_E := [] |} in
-      (T type_fixpoint).(ty_lfts)
+      ty_lfts (T type_fixpoint)
     in
     let wf_E :=
       let _ : TyWf type_fixpoint := {| ty_lfts := lfts; ty_wf_E := [] |} in
-      (T type_fixpoint).(ty_wf_E)
+      ty_wf_E (T type_fixpoint)
     in
     {| ty_lfts := lfts; ty_wf_E := wf_E |}.
 End fixpoint_def.
 
-Lemma type_fixpoint_ne `{!typeG Σ} (T1 T2 : type → type)
+Lemma type_fixpoint_ne `{!typeGS Σ} (T1 T2 : type → type)
     `{!TypeContractive T1, !TypeContractive T2} n :
   (∀ t, T1 t ≡{n}≡ T2 t) → type_fixpoint T1 ≡{n}≡ type_fixpoint T2.
 Proof. eapply fixpointK_ne; apply type_contractive_ne, _. Qed.
 
 Section fixpoint.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
   Context (T : type → type) {HT: TypeContractive T}.
 
-  Global Instance fixpoint_copy :
+  Global Instance type_fixpoint_copy :
     (∀ `(!Copy ty), Copy (T ty)) → Copy (type_fixpoint T).
   Proof.
     intros ?. unfold type_fixpoint. apply fixpointK_ind.
@@ -61,11 +61,11 @@ Section fixpoint.
       { split; (intros [H1 H2]; split; [apply H1|apply H2]). }
       apply limit_preserving_and; repeat (apply limit_preserving_forall=> ?).
       + apply bi.limit_preserving_Persistent; solve_proper.
-      + apply limit_preserving_impl, bi.limit_preserving_entails;
+      + apply limit_preserving_impl', bi.limit_preserving_emp_valid;
         solve_proper_core ltac:(fun _ => eapply ty_size_ne || f_equiv).
   Qed.
 
-  Global Instance fixpoint_send :
+  Global Instance type_fixpoint_send :
     (∀ `(!Send ty), Send (T ty)) → Send (type_fixpoint T).
   Proof.
     intros ?. unfold type_fixpoint. apply fixpointK_ind.
@@ -77,7 +77,7 @@ Section fixpoint.
       apply bi.limit_preserving_entails; solve_proper.
   Qed.
 
-  Global Instance fixpoint_sync :
+  Global Instance type_fixpoint_sync :
     (∀ `(!Sync ty), Sync (T ty)) → Sync (type_fixpoint T).
   Proof.
     intros ?. unfold type_fixpoint. apply fixpointK_ind.
@@ -89,16 +89,15 @@ Section fixpoint.
       apply bi.limit_preserving_entails; solve_proper.
   Qed.
 
+  Lemma type_fixpoint_unfold : type_fixpoint T ≡ T (type_fixpoint T).
+  Proof. apply fixpointK_unfold. by apply type_contractive_ne. Qed.
+
   Lemma fixpoint_unfold_eqtype E L : eqtype E L (type_fixpoint T) (T (type_fixpoint T)).
-  Proof.
-    unfold eqtype, subtype, type_incl.
-    setoid_rewrite <-fixpointK_unfold; [| by apply type_contractive_ne, _..].
-    split; iIntros (qL) "_ !# _"; (iSplit; first done); iSplit; iIntros "!#*$".
-  Qed.
+  Proof. apply type_equal_eqtype, type_equal_equiv, type_fixpoint_unfold. Qed.
 End fixpoint.
 
 Section subtyping.
-  Context `{!typeG Σ} (E : elctx) (L : llctx).
+  Context `{!typeGS Σ} (E : elctx) (L : llctx).
 
   (* TODO : is there a way to declare these as a [Proper] instances ? *)
   Lemma fixpoint_mono T1 `{!TypeContractive T1} T2 `{!TypeContractive T2} :
@@ -141,11 +140,11 @@ Section subtyping.
   Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
 End subtyping.
 
-Hint Resolve fixpoint_mono fixpoint_proper : lrust_typing.
+Global Hint Resolve fixpoint_mono fixpoint_proper : lrust_typing.
 
 (* These hints can loop if [fixpoint_mono] and [fixpoint_proper] have
    not been tried before, so we give them a high cost *)
-Hint Resolve fixpoint_unfold_subtype_l|100 : lrust_typing.
-Hint Resolve fixpoint_unfold_subtype_r|100 : lrust_typing.
-Hint Resolve fixpoint_unfold_eqtype_l|100 : lrust_typing.
-Hint Resolve fixpoint_unfold_eqtype_r|100 : lrust_typing.
+Global Hint Resolve fixpoint_unfold_subtype_l|100 : lrust_typing.
+Global Hint Resolve fixpoint_unfold_subtype_r|100 : lrust_typing.
+Global Hint Resolve fixpoint_unfold_eqtype_l|100 : lrust_typing.
+Global Hint Resolve fixpoint_unfold_eqtype_r|100 : lrust_typing.

theories/typing/int.v → lambda-rust/typing/int.v

-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Export type.
 From lrust.typing Require Import bool programs.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Section int.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Program Definition int : type :=
     {| st_own tid vl :=
@@ -22,11 +22,11 @@ Section int.
 End int.
 
 Section typing.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Lemma type_int_instr (z : Z) : typed_val #z int.
   Proof.
-    iIntros (E L tid) "_ _ $ $ _". iApply wp_value.
+    iIntros (E L tid ?) "_ _ $ $ _". iApply wp_value.
     by rewrite tctx_interp_singleton tctx_hasty_val' //.
   Qed.
 
@@ -37,9 +37,9 @@ Section typing.
   Proof. iIntros. iApply type_let; [apply type_int_instr|solve_typing|done]. Qed.
 
   Lemma type_plus_instr E L p1 p2 :
-    typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 + p2) int.
+    ⊢ typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 + p2) int.
   Proof.
-    iIntros (tid) "_ _ $ $ [Hp1 [Hp2 _]]".
+    iIntros (tid ?) "_ _ $ $ [Hp1 [Hp2 _]]".
     wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
     wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done.
     wp_op. by rewrite tctx_interp_singleton tctx_hasty_val' //.
@@ -53,9 +53,9 @@ Section typing.
   Proof. iIntros. iApply type_let; [iApply type_plus_instr|solve_typing|done]. Qed.
 
   Lemma type_minus_instr E L p1 p2 :
-    typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 - p2) int.
+    ⊢ typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 - p2) int.
   Proof.
-    iIntros (tid) "_ _ $ $ [Hp1 [Hp2 _]]".
+    iIntros (tid ?) "_ _ $ $ [Hp1 [Hp2 _]]".
     wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
     wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done.
     wp_op. by rewrite tctx_interp_singleton tctx_hasty_val' //.
@@ -69,9 +69,9 @@ Section typing.
   Proof. iIntros. iApply type_let; [apply type_minus_instr|solve_typing|done]. Qed.
 
   Lemma type_le_instr E L p1 p2 :
-    typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 ≤ p2) bool.
+    ⊢ typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 ≤ p2) bool.
   Proof.
-    iIntros (tid) "_ _ $ $ [Hp1 [Hp2 _]]".
+    iIntros (tid ?) "_ _ $ $ [Hp1 [Hp2 _]]".
     wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
     wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done.
     wp_op; case_bool_decide; by rewrite tctx_interp_singleton tctx_hasty_val' //.

theories/typing/lib/diverging_static.v → lambda-rust/typing/lib/diverging_static.v

-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Export type.
 From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Section diverging_static.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   (* 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"] :=
+    fn: ["x"; "f"] :=
       let: "call_once" := call_once in
       letcall: "ret" := "call_once" ["f"; "x"]%E in
     withcont: "loop":
@@ -24,15 +24,15 @@ Section diverging_static.
     typed_val (diverging_static_loop call_once)
               (fn(∀ α, λ ϝ, ty_outlives_E T static; &shr{α} T, F) → ∅).
   Proof.
-    intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    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 & _)".
+    iIntros (tid qmax) "#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α & _ & _)";
+    iMod (lctx_lft_alive_tok_noend α 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 _]]".
@@ -51,6 +51,48 @@ Section diverging_static.
       { 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.
+      + iIntros "!>" (? args). inv_vec args. simpl_subst. iApply type_jump; solve_typing.
+  Qed.
+
+
+  (** With the right typing rule, we can prove a variant of the above where the
+      lifetime is in an arbitrary invariant position, without even leaving the
+      type system.  This is incompatible with branding!
+
+      Our [TyWf] is not working well for type constructors (we have no way of
+      representing the fact that well-formedness is somewhat "uniform"), so we
+      instead work with a constant [Euser] of lifetime inclusion assumptions (in
+      general it could change with the type parameter but only in monotone ways)
+      and a single [κuser] of lifetimes that have to be alive (making κuser a
+      list would require some induction-based reasoning principles that we do
+      not have, but showing that it works for one lifetime is enough to
+      demonstrate the principle). *)
+  Lemma diverging_static_loop_type_bad (T : lft → type) F κuser Euser call_once
+        `{!TyWf F} :
+    (* The "bad" type_equivalize_lft_static rule *)
+    (∀ E L C T κ e,
+      (⊢ typed_body ((static ⊑ₑ κ) :: E) L C T e) →
+      ⊢ typed_body E ((κ ⊑ₗ []) :: L) C T e) →
+    (* Typing of this function *)
+    let _ : (∀ κ, TyWf (T κ)) := λ κ, {| ty_lfts := [κ; κuser]; ty_wf_E := Euser |} in
+    (∀ κ1 κ2, (T κ1).(ty_size) = (T κ2).(ty_size)) →
+    (∀ E L κ1 κ2, lctx_lft_eq E L κ1 κ2 → subtype E L (T κ1) (T κ2)) →
+    typed_val call_once (fn(∅; F, T static) → unit) →
+    typed_val (diverging_static_loop call_once)
+              (fn(∀ α, ∅; T α, F) → ∅).
+  Proof.
+    intros type_equivalize_lft_static_bad HWf HTsz HTsub 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.
+    iApply (type_cont [_] [] (λ r, [(r!!!0%fin:val) ◁ box (unit)])).
+    { iIntros (k). simpl_subst.
+      iApply type_equivalize_lft_static_bad.
+      iApply (type_call [ϝ] ()); solve_typing. }
+    iIntros "!> %k %args". inv_vec args=>r. simpl_subst.
+    iApply (type_cont [] [] (λ r, [])).
+    { iIntros (kloop). simpl_subst. iApply type_jump; solve_typing. }
+    iIntros "!> %k' %args". inv_vec args. simpl_subst.
+    iApply type_jump; solve_typing.
   Qed.
 End diverging_static.

theories/typing/lib/fake_shared.v → lambda-rust/typing/lib/fake_shared.v

-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Section fake_shared.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Definition fake_shared_box : val :=
-    funrec: <> ["x"] := Skip ;; return: ["x"].
+    fn: ["x"] := Skip ;; return: ["x"].
 
   Lemma fake_shared_box_type ty `{!TyWf ty} :
     typed_val fake_shared_box
       (fn(∀ '(α, β), ∅; &shr{α}(&shr{β} ty)) → &shr{α}(box ty)).
   Proof.
-    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk HT".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk HT".
     rewrite tctx_interp_singleton tctx_hasty_val.
-    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
+    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "%"; [solve_typing..|].
     iAssert (▷ ty_own (own_ptr 1 (&shr{α}(box ty))) tid [x])%I with "[HT]" as "HT".
     { destruct x as [[|l|]|]=>//=. iDestruct "HT" as "[H $]".
       iNext. iDestruct "H" as ([|[[]|][]]) "[H↦ H]"; try done.
       iExists _. iFrame. iDestruct "H" as (vl) "[#Hf H]".
       iNext. destruct vl as [|[[|l'|]|][]]; try done. iExists l'. iSplit.
-      { iApply frac_bor_iff; last done. iIntros "!>!# *".
-        rewrite heap_mapsto_vec_singleton. iSplit; auto. }
-      iDestruct "H" as "#H". iIntros "!# * % $". iApply step_fupd_intro. set_solver.
-      simpl. by iApply ty_shr_mono. }
+      { iApply frac_bor_iff; last done. iIntros "!>!> *".
+        rewrite heap_pointsto_vec_singleton. iSplit; auto. }
+      iDestruct "H" as "#H". iIntros "!> * % $". iApply step_fupd_intro; first set_solver.
+      simpl. iApply ty_shr_mono; last done.
+      by iApply lft_incl_syn_sem. }
     do 2 wp_seq.
     iApply (type_type [] _ _ [ x ◁ box (&shr{α}(box ty)) ]
             with "[] LFT [] Hna HL Hk [HT]"); last first.
@@ -35,27 +36,29 @@ Section fake_shared.
   Qed.
 
   Definition fake_shared_uniq : val :=
-    funrec: <> ["x"] := Skip ;; return: ["x"].
+    fn: ["x"] := Skip ;; return: ["x"].
 
   Lemma fake_shared_uniq_type ty `{!TyWf ty} :
     typed_val fake_shared_box
       (fn(∀ '(α, β), ∅; &shr{α}(&shr{β} ty)) → &shr{α}(&uniq{β} ty)).
   Proof.
-    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk HT".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk HT".
     rewrite tctx_interp_singleton tctx_hasty_val.
-    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
+    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "%"; [solve_typing..|].
     (* FIXME: WTF, using &uniq{β} here does not work. *)
     iAssert (▷ ty_own (own_ptr 1 (&shr{α} (uniq_bor β ty))) tid [x])%I with "[HT]" as "HT".
     { destruct x as [[|l|]|]=>//=. iDestruct "HT" as "[H $]".
       iNext. iDestruct "H" as ([|[[]|][]]) "[H↦ H]"; try done.
       iExists _. iFrame. iDestruct "H" as (vl) "[#Hf H]".
       iNext. destruct vl as [|[[|l'|]|][]]; try done. iExists l'. iSplit.
-      { iApply frac_bor_iff; last done. iIntros "!>!# *".
-        rewrite heap_mapsto_vec_singleton. iSplit; auto. }
-      iDestruct "H" as "#H". iIntros "!# * % $". iApply step_fupd_intro. set_solver.
-      simpl. iApply ty_shr_mono; last done. iApply lft_intersect_incl_l. }
+      { iApply frac_bor_iff; last done. iIntros "!>!> *".
+        rewrite heap_pointsto_vec_singleton. iSplit; auto. }
+      iDestruct "H" as "#H". iIntros "!> * % $". iApply step_fupd_intro; first set_solver.
+      simpl. iApply ty_shr_mono; last done.
+      by iApply lft_intersect_incl_l.
+    }
     do 2 wp_seq.
     iApply (type_type [] _ _ [ x ◁ box (&shr{α}(&uniq{β} ty)) ]
             with "[] LFT [] Hna HL Hk [HT]"); last first.

theories/typing/lib/panic.v → lambda-rust/typing/lib/panic.v

-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 (* Minimal support for panic. Lambdarust does not support unwinding the
    stack. Instead, we just end the current thread by not calling any
@@ -11,15 +11,15 @@ Set Default Proof Using "Type".
    [take_mut]. *)
 
 Section panic.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Definition panic : val :=
-    funrec: <> [] := #☠.
+    fn: [] := #☠.
 
   Lemma panic_type : typed_val panic (fn(∅) → ∅).
   Proof.
-    intros E L. iApply type_fn; [done|]. iIntros "!# *".
-    inv_vec args.  iIntros (tid) "LFT HE Hna HL Hk HT /=". simpl_subst.
+    intros E L. iApply type_fn; [done|]. iIntros "!> _ %κ %ret %args".
+    inv_vec args. iIntros (tid qmax) "LFT HE Hna HL Hk HT /=". simpl_subst.
     by iApply wp_value.
   Qed.
 End panic.