Typechecking Ralf's example.

theories/typing/examples/foo.v

+From iris.proofmode Require Import tactics.
+From lrust.typing Require Import typing.
+Set Default Proof Using "Type".
+
+Section foo.
+  Context `{typeG Σ}.
+
+  Definition foo : val :=
+    (* fn foo(mut x: u32, mut y: u32) { *)
+    funrec: <> ["x"; "y"] :=
+      let: "one" := #1 in
+      Newlft;;
+        (* let mut p = Box::new(&mut x); *)
+        letalloc: "p" <- "x" in
+        (* { *)
+        Newlft;;
+          (* let q = &mut **p; *)
+          let: "q" := !"p" in
+          (* *q += 1; *)
+          let: "u" := !"q" in let: "u" := "u" + "one" in "q" <- "u";;
+        (* } *)
+        Endlft;;
+        (* **p += 1; *)
+        Newlft;; let: "p'" := !"p" in let: "u" := !"p'" in
+                 let: "u" := "u" + "one" in "p'" <- "u";; Endlft;;
+        (* *p = &mut y; *)
+        "p" <- "y";;
+        (* **p += 1; *)
+        Newlft;; let: "p'" := !"p" in let: "u" := !"p'" in
+                 let: "u" := "u" + "one" in "p'" <- "u";; Endlft;;
+      (* } *)
+      Endlft;;
+      let: "r" := new [ #0] in
+      delete [ #1; "p"] ;; delete [ #1; "x"] ;; delete [ #1; "y"] ;; "return" ["r"].
+
+  Lemma foo_type :
+    typed_val foo (fn(∅; int, int) → unit).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([] ϝ ret p).
+    inv_vec p=>x y. simpl_subst.
+    iApply type_int. iIntros (one). simpl_subst.
+    iApply (type_newlft []). iIntros (α).
+    iApply (type_letalloc_1 (&uniq{α}int)); [solve_typing..|]. iIntros (p). simpl_subst.
+    iApply (type_newlft [α]). iIntros (β).
+    iApply (type_deref_uniq_uniq β α); [solve_typing..|]. iIntros (q). simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (?). simpl_subst.
+    iApply type_plus; [solve_typing..|]. iIntros (?). simpl_subst.
+    iApply type_assign; [solve_typing..|].
+    iApply type_endlft.
+    iApply (type_newlft [α]). iIntros (γ).
+    iApply type_deref_uniq_uniq; [solve_typing..|]. iIntros (p'). simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (?). simpl_subst.
+    iApply type_plus; [solve_typing..|]. iIntros (?). simpl_subst.
+    iApply type_assign; [solve_typing..|].
+    iApply type_endlft.
+    iApply (type_assign _ (&uniq{α}_)); [solve_typing..|].
+    iApply (type_newlft [α]). iIntros (δ).
+    iApply type_deref; [solve_typing..|]. iIntros (p'2). simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (?). simpl_subst.
+    iApply type_plus; [solve_typing..|]. iIntros (?). simpl_subst.
+    iApply type_assign; [solve_typing..|].
+    iApply type_endlft.
+    iApply type_endlft.
+    iApply type_new; first done. iIntros (r). simpl_subst.
+    iApply type_delete; [solve_typing..|].
+    iApply type_delete; [solve_typing..|].
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+End foo.