From 4e8ad785ea14fd46005e3c5e09b1d6c2b172177f Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org>
Date: Wed, 11 Jan 2017 18:27:52 +0100
Subject: [PATCH] Soundness of the type system. Also, added a file typing.v
 that reexports all the type system.

---
 _CoqProject                           |  2 +
 opam.pins                             |  2 +-
 theories/lang/tactics.v               |  2 +-
 theories/lifetime/lifetime_sig.v      |  2 +-
 theories/lifetime/model/definitions.v |  2 +-
 theories/typing/borrow.v              | 20 +++----
 theories/typing/fixpoint.v            |  1 +
 theories/typing/own.v                 | 36 ++++++-------
 theories/typing/product_split.v       | 26 ++++-----
 theories/typing/programs.v            |  1 -
 theories/typing/soundness.v           | 78 +++++++++++++++++++++++++++
 theories/typing/tests/get_x.v         |  5 +-
 theories/typing/tests/init_prod.v     |  7 +--
 theories/typing/tests/lazy_lft.v      |  5 +-
 theories/typing/tests/option_as_mut.v |  5 +-
 theories/typing/tests/rebor.v         |  5 +-
 theories/typing/tests/unbox.v         |  5 +-
 theories/typing/tests/unwrap_or.v     |  5 +-
 theories/typing/type.v                |  2 +-
 theories/typing/type_context.v        |  1 -
 theories/typing/type_sum.v            | 20 +++----
 theories/typing/unsafe/cell.v         |  2 +-
 22 files changed, 146 insertions(+), 88 deletions(-)
 create mode 100644 theories/typing/soundness.v

diff --git a/_CoqProject b/_CoqProject
index d25c14ab..4de595c5 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -43,6 +43,8 @@ theories/typing/borrow.v
 theories/typing/cont.v
 theories/typing/fixpoint.v
 theories/typing/type_sum.v
+theories/typing/typing.v
+theories/typing/soundness.v
 theories/typing/tests/get_x.v
 theories/typing/tests/rebor.v
 theories/typing/tests/unbox.v
diff --git a/opam.pins b/opam.pins
index cbfb3aa0..57ff8356 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq be81fb92a76f31ca656f8dad37122843f58884cf
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 9fa0b57d44cbba40d7bb272b45cc0875bc68940d
diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
index 5767645f..99dc7464 100644
--- a/theories/lang/tactics.v
+++ b/theories/lang/tactics.v
@@ -240,7 +240,7 @@ Ltac reshape_val e tac :=
   | of_val ?v => v
   | Lit ?l => constr:(LitV l)
   | Rec ?f ?xl ?e => constr:(RecV f xl e)
-  end in let v := go e in first [tac v | fail 2].
+  end in let v := go e in tac v.
 
 Ltac reshape_expr e tac :=
   let rec go_fun K f vs es :=
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 52fdd1f3..d9f55c4d 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -151,7 +151,7 @@ Module Type lifetime_sig.
   End properties.
 
   Parameter lftΣ : gFunctors.
-  Global Declare Instance subG_lftΣ Σ : subG lftΣ Σ → lftPreG Σ.
+  Global Declare Instance subG_lftPreG Σ : subG lftΣ Σ → lftPreG Σ.
 
   Parameter lft_init : ∀ `{invG Σ, !lftPreG Σ} E, ↑lftN ⊆ E →
     True ={E}=∗ ∃ _ : lftG Σ, lft_ctx.
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index a84788de..d5677a85 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -54,7 +54,7 @@ Definition lftPreG' := lftPreG.
 Definition lftΣ : gFunctors :=
   #[ boxΣ; GFunctor (authR alftUR); GFunctor (authR ilftUR);
      GFunctor (authR borUR); GFunctor (authR natUR); GFunctor (authR inhUR) ].
-Instance subG_lftΣ Σ :
+Instance subG_lftPreG Σ :
   subG lftΣ Σ → lftPreG Σ.
 Proof. solve_inG. Qed.
 
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 76a658d4..3f114dc3 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
-From lrust.lang Require Import heap.
+From lrust.lang Require Import proofmode.
 From lrust.typing Require Export uniq_bor shr_bor own.
 From lrust.typing Require Import lft_contexts type_context programs.
 Set Default Proof Using "Type".
@@ -13,7 +13,7 @@ Section borrow.
   Context `{typeG Σ}.
 
   Lemma tctx_borrow E L p n ty κ :
-    tctx_incl E L [p ◁ own n ty] [p ◁ &uniq{κ}ty; p ◁{κ} own n ty].
+    tctx_incl E L [p ◁ own_ptr n ty] [p ◁ &uniq{κ}ty; p ◁{κ} own_ptr n ty].
   Proof.
     iIntros (tid ??) "#LFT $ $ H".
     rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
@@ -27,8 +27,8 @@ Section borrow.
 
   Lemma tctx_extract_hasty_borrow E L p n ty ty' κ T :
     subtype E L ty' ty →
-    tctx_extract_hasty E L p (&uniq{κ}ty) ((p ◁ own n ty')::T)
-                       ((p ◁{κ} own n ty)::T).
+    tctx_extract_hasty E L p (&uniq{κ}ty) ((p ◁ own_ptr n ty')::T)
+                       ((p ◁{κ} own_ptr n ty)::T).
   Proof.
     intros. apply (tctx_incl_frame_r _ [_] [_;_]). rewrite subtype_tctx_incl.
     by apply tctx_borrow. by f_equiv.
@@ -37,8 +37,8 @@ Section borrow.
   (* See the comment above [tctx_extract_hasty_share] in [uniq_bor.v]. *)
   Lemma tctx_extract_hasty_borrow_share E L p ty ty' κ n T :
     lctx_lft_alive E L κ → subtype E L ty' ty →
-    tctx_extract_hasty E L p (&shr{κ}ty) ((p ◁ own n ty')::T)
-                       ((p ◁ &shr{κ}ty')::(p ◁{κ} own n ty')::T).
+    tctx_extract_hasty E L p (&shr{κ}ty) ((p ◁ own_ptr n ty')::T)
+                       ((p ◁ &shr{κ}ty')::(p ◁{κ} own_ptr n ty')::T).
   Proof.
     intros. apply (tctx_incl_frame_r _ [_] [_;_;_]). rewrite ->tctx_borrow.
     apply (tctx_incl_frame_r _ [_] [_;_]). rewrite ->tctx_share; solve_typing.
@@ -46,7 +46,7 @@ Section borrow.
 
   Lemma type_deref_uniq_own_instr {E L} κ p n ty :
     lctx_lft_alive E L κ →
-    typed_instruction_ty E L [p ◁ &uniq{κ} own n ty] (!p) (&uniq{κ} ty).
+    typed_instruction_ty E L [p ◁ &uniq{κ} own_ptr n ty] (!p) (&uniq{κ} ty).
   Proof.
     iIntros (Hκ) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp".
     rewrite tctx_interp_singleton.
@@ -70,7 +70,7 @@ Section borrow.
 
   Lemma type_deref_uniq_own {E L} κ x p e n ty C T T' :
     Closed (x :b: []) e →
-    tctx_extract_hasty E L p (&uniq{κ} own n ty) T T' →
+    tctx_extract_hasty E L p (&uniq{κ} own_ptr n ty) T T' →
     lctx_lft_alive E L κ →
     (∀ (v:val), typed_body E L C ((v ◁ &uniq{κ} ty) :: T') (subst' x v e)) →
     typed_body E L C T (let: x := !p in e).
@@ -80,7 +80,7 @@ Section borrow.
 
   Lemma type_deref_shr_own_instr {E L} κ p n ty :
     lctx_lft_alive E L κ →
-    typed_instruction_ty E L [p ◁ &shr{κ} own n ty] (!p) (&shr{κ} ty).
+    typed_instruction_ty E L [p ◁ &shr{κ} own_ptr n ty] (!p) (&shr{κ} ty).
   Proof.
     iIntros (Hκ) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp".
     rewrite tctx_interp_singleton.
@@ -99,7 +99,7 @@ Section borrow.
 
   Lemma type_deref_shr_own {E L} κ x p e n ty C T T' :
     Closed (x :b: []) e →
-    tctx_extract_hasty E L p (&shr{κ} own n ty) T T' →
+    tctx_extract_hasty E L p (&shr{κ} own_ptr n ty) T T' →
     lctx_lft_alive E L κ →
     (∀ (v:val), typed_body E L C ((v ◁ &shr{κ} ty) :: T') (subst' x v e)) →
     typed_body E L C T (let: x := !p in e).
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index 140ad5f1..c13c52b5 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -1,3 +1,4 @@
+From lrust.lang Require Import proofmode.
 From lrust.typing Require Export lft_contexts type bool.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 8f64431d..7bb2b40c 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -41,7 +41,7 @@ Section own.
       rewrite /= -Qcmult_plus_distr_l -Z2Qc_inj_add /Z.add. do 3 f_equal. lia.
   Qed.
 
-  Program Definition own (n : nat) (ty : type) :=
+  Program Definition own_ptr (n : nat) (ty : type) :=
     {| ty_size := 1;
        ty_own tid vl :=
          (* We put a later in front of the †{q}, because we cannot use
@@ -96,7 +96,7 @@ Section own.
   Qed.
 
   Global Instance own_mono E L n :
-    Proper (subtype E L ==> subtype E L) (own n).
+    Proper (subtype E L ==> subtype E L) (own_ptr n).
   Proof.
     intros ty1 ty2 Hincl. iIntros. iSplit; first done.
     iDestruct (Hincl with "* [] [] []") as "(_ & #Ho & #Hs)"; [done..|clear Hincl].
@@ -113,27 +113,27 @@ Section own.
       iMod "Hvs'" as "[Hshr $]". iApply ("Hs" with "Hshr").
   Qed.
   Lemma own_mono' E L n ty1 ty2 :
-    subtype E L ty1 ty2 → subtype E L (own n ty1) (own n ty2).
+    subtype E L ty1 ty2 → subtype E L (own_ptr n ty1) (own_ptr n ty2).
   Proof. apply own_mono. Qed.
   Global Instance own_proper E L n :
-    Proper (eqtype E L ==> eqtype E L) (own n).
+    Proper (eqtype E L ==> eqtype E L) (own_ptr n).
   Proof. intros ?? Heq. split; f_equiv; apply Heq. Qed.
   Lemma own_proper' E L n ty1 ty2 :
-    eqtype E L ty1 ty2 → eqtype E L (own n ty1) (own n ty2).
+    eqtype E L ty1 ty2 → eqtype E L (own_ptr n ty1) (own_ptr n ty2).
   Proof. apply own_proper. Qed.
 
-  Global Instance own_contractive n : Contractive (own n).
+  Global Instance own_contractive n : Contractive (own_ptr n).
   Proof.
     intros m ?? EQ. split; [split|]; simpl.
     - done.
     - destruct m=>// tid vl /=. repeat (apply EQ || f_contractive || f_equiv).
     - intros κ tid l. repeat (apply EQ || f_contractive || f_equiv).
   Qed.
-  Global Instance own_ne n m : Proper (dist m ==> dist m) (own n).
+  Global Instance own_ne n m : Proper (dist m ==> dist m) (own_ptr n).
   Proof. apply contractive_ne, _. Qed.
 
   Global Instance own_send n ty :
-    Send ty → Send (own n ty).
+    Send ty → Send (own_ptr n ty).
   Proof.
     iIntros (Hsend tid1 tid2 vl) "H". iDestruct "H" as (l) "[% [Hm H†]]". subst vl.
     iExists _. iSplit; first done. iFrame "H†". iNext.
@@ -141,7 +141,7 @@ Section own.
   Qed.
 
   Global Instance own_sync n ty :
-    Sync ty → Sync (own n ty).
+    Sync ty → Sync (own_ptr n ty).
   Proof.
     iIntros (Hsync κ tid1 tid2 l) "H". iDestruct "H" as (l') "[Hm #Hshr]".
     iExists _. iFrame "Hm". iAlways. iIntros (F q) "% Htok".
@@ -151,14 +151,14 @@ Section own.
   Qed.
 End own.
 
-Notation box ty := (own ty.(ty_size) ty).
+Notation box ty := (own_ptr ty.(ty_size) ty).
 
 Section typing.
   Context `{typeG Σ}.
 
   (** Typing *)
   Lemma write_own {E L} ty ty' n :
-    ty.(ty_size) = ty'.(ty_size) → typed_write E L (own n ty') ty (own n ty).
+    ty.(ty_size) = ty'.(ty_size) → typed_write E L (own_ptr n ty') ty (own_ptr n ty).
   Proof.
     iIntros (Hsz) "!#". iIntros (p tid F qE qL ?) "_ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
     iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
@@ -169,7 +169,7 @@ Section typing.
   Qed.
 
   Lemma read_own_copy E L ty n :
-    Copy ty → typed_read E L (own n ty) ty (own n ty).
+    Copy ty → typed_read E L (own_ptr n ty) ty (own_ptr n ty).
   Proof.
     iIntros (Hsz) "!#". iIntros (p tid F qE qL ?) "_ $ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
     iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ #Hown]". iModIntro.
@@ -178,7 +178,7 @@ Section typing.
   Qed.
 
   Lemma read_own_move E L ty n :
-    typed_read E L (own n ty) ty (own n $ uninit ty.(ty_size)).
+    typed_read E L (own_ptr n ty) ty (own_ptr n $ uninit ty.(ty_size)).
   Proof.
     iAlways. iIntros (p tid F qE qL ?) "_ $ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
     iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
@@ -191,7 +191,7 @@ Section typing.
   Lemma type_new_instr {E L} (n : Z) :
     0 ≤ n →
     let n' := Z.to_nat n in
-    typed_instruction_ty E L [] (new [ #n ]%E) (own n' (uninit n')).
+    typed_instruction_ty E L [] (new [ #n ]%E) (own_ptr n' (uninit n')).
   Proof.
     intros. iAlways. iIntros (tid q) "#HEAP #LFT $ $ $ _".
     iApply (wp_new with "HEAP"); try done. iModIntro.
@@ -213,7 +213,7 @@ Section typing.
     0 ≤ n →
     let n' := Z.to_nat n in
     subtype E L (uninit n') ty →
-    (∀ (v : val), typed_body E L C ((v ◁ own n' ty) :: T) (subst' x v e)) →
+    (∀ (v : val), typed_body E L C ((v ◁ own_ptr n' ty) :: T) (subst' x v e)) →
     typed_body E L C T (let: x := new [ #n ] in e).
   Proof.
     intros ???? Htyp. eapply type_let. done. by apply type_new_instr. solve_typing.
@@ -238,7 +238,7 @@ Section typing.
 
   Lemma type_delete {E L} ty C T T' (n' : nat) (n : Z)  p e :
     Closed [] e →
-    tctx_extract_hasty E L p (own n' ty) T T' →
+    tctx_extract_hasty E L p (own_ptr n' ty) T T' →
     n = n' → Z.of_nat (ty.(ty_size)) = n →
     typed_body E L C T' e →
     typed_body E L C T (delete [ #n; p ] ;; e).
@@ -251,7 +251,7 @@ Section typing.
     Closed [] p → Closed (x :b: []) e →
     tctx_extract_hasty E L p ty T T' →
     ty.(ty_size) = 1%nat →
-    (∀ (v : val), typed_body E L C ((v ◁ own 1 ty)::T') (subst x v e)) →
+    (∀ (v : val), typed_body E L C ((v ◁ own_ptr 1 ty)::T') (subst x v e)) →
     typed_body E L C T (letalloc: x <- p in e).
   Proof.
     intros. eapply type_new.
@@ -273,7 +273,7 @@ Section typing.
     typed_read E L ty1 ty ty2 →
     tctx_extract_hasty E L p ty1 T T' →
     (∀ (v : val),
-        typed_body E L C ((v ◁ own (ty.(ty_size)) ty)::(p ◁ ty2)::T') (subst x v e)) →
+        typed_body E L C ((v ◁ own_ptr (ty.(ty_size)) ty)::(p ◁ ty2)::T') (subst x v e)) →
     typed_body E L C T (letalloc: x <⋯ !{ty.(ty_size)}p in e).
   Proof.
     intros. eapply type_new.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index e06f82a5..80b4f865 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -85,8 +85,8 @@ Section product_split.
 
   (** Owned pointers *)
   Lemma tctx_split_own_prod2 E L p n ty1 ty2 :
-    tctx_incl E L [p ◁ own n $ product2 ty1 ty2]
-                  [p ◁ own n ty1; p +ₗ #ty1.(ty_size) ◁ own n ty2].
+    tctx_incl E L [p ◁ own_ptr n $ product2 ty1 ty2]
+                  [p ◁ own_ptr n ty1; p +ₗ #ty1.(ty_size) ◁ own_ptr n ty2].
   Proof.
     iIntros (tid q1 q2) "#LFT $ $ H".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
@@ -104,8 +104,8 @@ Section product_split.
   Qed.
 
   Lemma tctx_merge_own_prod2 E L p n ty1 ty2 :
-    tctx_incl E L [p ◁ own n ty1; p +ₗ #ty1.(ty_size) ◁ own n ty2]
-                  [p ◁ own n $ product2 ty1 ty2].
+    tctx_incl E L [p ◁ own_ptr n ty1; p +ₗ #ty1.(ty_size) ◁ own_ptr n ty2]
+                  [p ◁ own_ptr n $ product2 ty1 ty2].
   Proof.
     iIntros (tid q1 q2) "#LFT $ $ H".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
@@ -122,13 +122,13 @@ Section product_split.
   Qed.
 
   Lemma own_is_ptr n ty tid (vl : list val) :
-    ty_own (own n ty) tid vl -∗ ⌜∃ l : loc, vl = [(#l) : val]⌝.
+    ty_own (own_ptr n ty) tid vl -∗ ⌜∃ l : loc, vl = [(#l) : val]⌝.
   Proof.
     iIntros "H". iDestruct "H" as (l) "[% _]". iExists l. done.
   Qed.
 
   Lemma tctx_split_own_prod E L n tyl p :
-    tctx_incl E L [p ◁ own n $ product tyl] (hasty_ptr_offsets p (own n) tyl 0).
+    tctx_incl E L [p ◁ own_ptr n $ product tyl] (hasty_ptr_offsets p (own_ptr n) tyl 0).
   Proof.
     apply tctx_split_ptr_prod.
     - intros. apply tctx_split_own_prod2.
@@ -137,8 +137,8 @@ Section product_split.
 
   Lemma tctx_merge_own_prod E L n tyl :
     tyl ≠ [] →
-    ∀ p, tctx_incl E L (hasty_ptr_offsets p (own n) tyl 0)
-                   [p ◁ own n $ product tyl].
+    ∀ p, tctx_incl E L (hasty_ptr_offsets p (own_ptr n) tyl 0)
+                   [p ◁ own_ptr n $ product tyl].
   Proof.
     intros. apply tctx_merge_ptr_prod; try done.
     - apply _.
@@ -266,8 +266,8 @@ Section product_split.
      automation system to be able to perform e.g., borrowing or splitting after
      splitting. *)
   Lemma tctx_extract_split_own_prod E L p p' n ty tyl T T' :
-    tctx_extract_hasty E L p' ty (hasty_ptr_offsets p (own n) tyl 0) T' →
-    tctx_extract_hasty E L p' ty ((p ◁ own n $ Π tyl) :: T) (T' ++ T).
+    tctx_extract_hasty E L p' ty (hasty_ptr_offsets p (own_ptr n) tyl 0) T' →
+    tctx_extract_hasty E L p' ty ((p ◁ own_ptr n $ Π tyl) :: T) (T' ++ T).
   Proof.
     intros. apply (tctx_incl_frame_r T [_] (_::_)). by rewrite tctx_split_own_prod.
   Qed.
@@ -311,8 +311,8 @@ Section product_split.
 
   Lemma tctx_extract_merge_own_prod E L p n tyl T T' :
     tyl ≠ [] →
-    extract_tyl E L p (own n) tyl 0 T T' →
-    tctx_extract_hasty E L p (own n (Π tyl)) T T'.
+    extract_tyl E L p (own_ptr n) tyl 0 T T' →
+    tctx_extract_hasty E L p (own_ptr n (Π tyl)) T T'.
   Proof. auto using tctx_extract_merge_ptr_prod, tctx_merge_own_prod. Qed.
 
   Lemma tctx_extract_merge_uniq_prod E L p κ tyl T T' :
@@ -330,7 +330,7 @@ End product_split.
 
 (* We do not want unification to try to unify the definition of these
    types with anything in order to try splitting or merging. *)
-Hint Opaque own uniq_bor shr_bor tctx_extract_hasty : lrust_typing lrust_typing_merge.
+Hint Opaque own_ptr uniq_bor shr_bor tctx_extract_hasty : lrust_typing lrust_typing_merge.
 
 (* We make sure that splitting is tried before borrowing, so that not
    the entire product is borrowed when only a part is needed. *)
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 05fff696..ebff0b3d 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -1,5 +1,4 @@
 From iris.base_logic Require Import big_op.
-From lrust.lang Require Export notation.
 From lrust.lang Require Import proofmode memcpy.
 From lrust.typing Require Export type lft_contexts type_context cont_context.
 Set Default Proof Using "Type".
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
new file mode 100644
index 00000000..6f2f7f04
--- /dev/null
+++ b/theories/typing/soundness.v
@@ -0,0 +1,78 @@
+From iris.algebra Require Import frac.
+From iris.base_logic Require Import big_op.
+From iris.base_logic.lib Require Import na_invariants.
+From iris.proofmode Require Import tactics.
+From lrust.lang Require Import races adequacy proofmode notation.
+From lrust.lifetime Require Import lifetime frac_borrow.
+From lrust.typing Require Import typing.
+
+Set Default Proof Using "Type".
+
+Class typePreG Σ := PreTypeG {
+  type_heapG :> heapPreG Σ;
+  type_lftG :> lftPreG Σ;
+  type_preG_na_invG :> na_invG Σ;
+  type_frac_borrowG :> frac_borG Σ
+}.
+
+Definition typeΣ : gFunctors :=
+  #[heapΣ; lftΣ; na_invΣ; GFunctor (constRF fracR)].
+Instance subG_typePreG {Σ} : subG typeΣ Σ → typePreG Σ.
+Proof.
+  split.
+  - apply subG_heapPreG. solve_inG.
+  - apply subG_lftPreG. solve_inG.
+  - solve_inG.
+  - solve_inG.
+Qed.
+
+Section type_soundness.
+  Definition exit_cont : val := λ: [<>], #().
+
+  Definition main_type `{typeG Σ} :=
+    fn (λ _, []) (λ _, [# ]) (λ _:(), box unit).
+
+  Theorem type_soundness `{typePreG Σ} (main : val) σ t :
+    (∀ `{typeG Σ}, typed_instruction_ty [] [] [] main main_type) →
+    rtc step ([main [exit_cont]%E], ∅) (t, σ) →
+    nonracing_threadpool t σ ∧
+    (∀ e, e ∈ t → is_Some (to_val e) ∨ reducible e σ).
+  Proof.
+    intros Hmain Hrtc.
+    cut (adequate (main [exit_cont]%E) ∅ (λ _, True)).
+    { split. by eapply adequate_nonracing.
+      intros. by eapply (adequate_safe (main [exit_cont]%E)). }
+    apply: heap_adequacy=>?.
+    iIntros "!# #HEAP". iMod lft_init as (?) "#LFT". done.
+    iMod na_alloc as (tid) "Htl". set (Htype := TypeG _ _ _ _ _).
+    wp_bind (of_val main). iApply (wp_wand with "[Htl]").
+    iApply (Hmain _ $! tid 1%Qp with "* HEAP LFT Htl [] [] []").
+    { by rewrite /elctx_interp big_sepL_nil. }
+    { by rewrite /llctx_interp big_sepL_nil. }
+    { by rewrite tctx_interp_nil. }
+    clear Hrtc Hmain main. iIntros (main) "(Htl & _ & _ & Hmain)".
+    rewrite tctx_interp_singleton. iDestruct "Hmain" as (?) "[EQ Hmain]".
+    rewrite eval_path_of_val. iDestruct "EQ" as %[= <-].
+    iDestruct "Hmain" as (f k x e ?) "(EQ & % & Hmain)". iDestruct "EQ" as %[= ->].
+    destruct x; try done.
+    iApply (wp_rec _ _ _ _ _ _ [exit_cont]%E); [done| |by simpl_subst|iNext].
+    { repeat econstructor. apply to_of_val. }
+    iApply ("Hmain" $! () exit_cont [#] tid 1%Qp with "HEAP LFT Htl [] [] []");
+      last by rewrite tctx_interp_nil.
+    { by rewrite /elctx_interp big_sepL_nil. }
+    { by rewrite /llctx_interp big_sepL_nil. }
+    iIntros "_". rewrite cctx_interp_singleton. simpl. iIntros (args) "_ _".
+    inv_vec args. iIntros (x) "_". by wp_seq.
+  Qed.
+End type_soundness.
+
+(* Soundness theorem when no other CMRA is needed. *)
+
+Theorem type_soundness_closed (main : val) σ t :
+  (∀ `{typeG typeΣ}, typed_instruction_ty [] [] [] main main_type) →
+  rtc step ([main [exit_cont]%E], ∅) (t, σ) →
+  nonracing_threadpool t σ ∧
+  (∀ e, e ∈ t → is_Some (to_val e) ∨ reducible e σ).
+Proof.
+  intros. eapply @type_soundness; try done. apply _.
+Qed.
diff --git a/theories/typing/tests/get_x.v b/theories/typing/tests/get_x.v
index c75329e4..54577cbf 100644
--- a/theories/typing/tests/get_x.v
+++ b/theories/typing/tests/get_x.v
@@ -1,7 +1,4 @@
-From lrust.lifetime Require Import definitions.
-From lrust.lang Require Import new_delete.
-From lrust.typing Require Import programs product product_split own uniq_bor
-                    shr_bor int function lft_contexts uninit cont.
+From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section get_x.
diff --git a/theories/typing/tests/init_prod.v b/theories/typing/tests/init_prod.v
index 145c9471..8893096a 100644
--- a/theories/typing/tests/init_prod.v
+++ b/theories/typing/tests/init_prod.v
@@ -1,7 +1,4 @@
-From lrust.lifetime Require Import definitions.
-From lrust.lang Require Import new_delete.
-From lrust.typing Require Import programs product product_split own uniq_bor
-                    shr_bor int function lft_contexts uninit cont borrow.
+From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section init_prod.
@@ -23,7 +20,7 @@ Section init_prod.
     eapply type_deref; [solve_typing..|apply read_own_move|done|]=>y'. simpl_subst.
     eapply (type_new_subtype (Π[uninit 1; uninit 1])); [solve_typing..|].
       intros r. simpl_subst. unfold Z.to_nat, Pos.to_nat; simpl.
-    eapply (type_assign (own 2 (uninit 1))); [solve_typing..|by apply write_own|].
+    eapply (type_assign (own_ptr 2 (uninit 1))); [solve_typing..|by apply write_own|].
     eapply type_assign; [solve_typing..|by apply write_own|].
     eapply type_delete; [solve_typing..|].
     eapply type_delete; [solve_typing..|].
diff --git a/theories/typing/tests/lazy_lft.v b/theories/typing/tests/lazy_lft.v
index 4e5da308..aa147026 100644
--- a/theories/typing/tests/lazy_lft.v
+++ b/theories/typing/tests/lazy_lft.v
@@ -1,7 +1,4 @@
-From lrust.lifetime Require Import definitions.
-From lrust.lang Require Import new_delete.
-From lrust.typing Require Import programs product product_split own uniq_bor
-                    shr_bor int function lft_contexts uninit cont borrow type_sum.
+From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section lazy_lft.
diff --git a/theories/typing/tests/option_as_mut.v b/theories/typing/tests/option_as_mut.v
index 1c57578d..114f89f1 100644
--- a/theories/typing/tests/option_as_mut.v
+++ b/theories/typing/tests/option_as_mut.v
@@ -1,7 +1,4 @@
-From lrust.lifetime Require Import definitions.
-From lrust.lang Require Import new_delete.
-From lrust.typing Require Import programs product product_split own uniq_bor
-                    shr_bor int function lft_contexts uninit cont borrow type_sum.
+From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section option_as_mut.
diff --git a/theories/typing/tests/rebor.v b/theories/typing/tests/rebor.v
index 67cd5cde..a30f43cb 100644
--- a/theories/typing/tests/rebor.v
+++ b/theories/typing/tests/rebor.v
@@ -1,7 +1,4 @@
-From lrust.lifetime Require Import definitions.
-From lrust.lang Require Import new_delete.
-From lrust.typing Require Import programs product product_split own uniq_bor
-                    shr_bor int function lft_contexts uninit cont borrow.
+From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section rebor.
diff --git a/theories/typing/tests/unbox.v b/theories/typing/tests/unbox.v
index 77f66614..3f9b02b4 100644
--- a/theories/typing/tests/unbox.v
+++ b/theories/typing/tests/unbox.v
@@ -1,7 +1,4 @@
-From lrust.lifetime Require Import definitions.
-From lrust.lang Require Import new_delete.
-From lrust.typing Require Import programs product product_split own uniq_bor
-                    shr_bor int function lft_contexts uninit cont borrow.
+From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section unbox.
diff --git a/theories/typing/tests/unwrap_or.v b/theories/typing/tests/unwrap_or.v
index b1c2724c..72a29785 100644
--- a/theories/typing/tests/unwrap_or.v
+++ b/theories/typing/tests/unwrap_or.v
@@ -1,7 +1,4 @@
-From lrust.lifetime Require Import definitions.
-From lrust.lang Require Import new_delete.
-From lrust.typing Require Import programs product product_split own uniq_bor
-                    shr_bor int function lft_contexts uninit cont borrow type_sum.
+From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section unwrap_or.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index bf270f5b..979af897 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -9,7 +9,7 @@ Class typeG Σ := TypeG {
   type_heapG :> heapG Σ;
   type_lftG :> lftG Σ;
   type_na_invG :> na_invG Σ;
-  type_frac_borrowG Σ :> frac_borG Σ
+  type_frac_borrowG :> frac_borG Σ
 }.
 
 Definition lftE := ↑lftN.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 1d1535f1..824d0bde 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -1,6 +1,5 @@
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
-From lrust.lang Require Import notation.
 From lrust.typing Require Import type lft_contexts.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 037176e2..e1017869 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import tactics.
-From lrust.lang Require Import heap memcpy.
-From lrust.typing Require Export uninit uniq_bor shr_bor own sum.
+From lrust.lang Require Import memcpy.
+From lrust.typing Require Import uninit uniq_bor shr_bor own sum.
 From lrust.typing Require Import lft_contexts type_context programs product.
 Set Default Proof Using "Type".
 
@@ -9,11 +9,11 @@ Section case.
 
   Lemma type_case_own' E L C T p n tyl el :
     Forall2 (λ ty e,
-      typed_body E L C ((p +ₗ #0 ◁ own n (uninit 1)) :: (p +ₗ #1 ◁ own n ty) ::
+      typed_body E L C ((p +ₗ #0 ◁ own_ptr n (uninit 1)) :: (p +ₗ #1 ◁ own_ptr n ty) ::
          (p +ₗ #(S (ty.(ty_size))) ◁
-            own n (uninit (list_max (map ty_size tyl) - ty_size ty))) :: T) e ∨
-      typed_body E L C ((p ◁ own n (sum tyl)) :: T) e) tyl el →
-    typed_body E L C ((p ◁ own n (sum tyl)) :: T) (case: !p of el).
+            own_ptr n (uninit (list_max (map ty_size tyl) - ty_size ty))) :: T) e ∨
+      typed_body E L C ((p ◁ own_ptr n (sum tyl)) :: T) e) tyl el →
+    typed_body E L C ((p ◁ own_ptr n (sum tyl)) :: T) (case: !p of el).
   Proof.
     iIntros (Hel) "!#". iIntros (tid qE) "#HEAP #LFT Hna HE HL HC HT". wp_bind p.
     rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
@@ -49,12 +49,12 @@ Section case.
   Qed.
 
   Lemma type_case_own E L C T T' p n tyl el :
-    tctx_extract_hasty E L p (own n (sum tyl)) T T' →
+    tctx_extract_hasty E L p (own_ptr n (sum tyl)) T T' →
     Forall2 (λ ty e,
-      typed_body E L C ((p +ₗ #0 ◁ own n (uninit 1)) :: (p +ₗ #1 ◁ own n ty) ::
+      typed_body E L C ((p +ₗ #0 ◁ own_ptr n (uninit 1)) :: (p +ₗ #1 ◁ own_ptr n ty) ::
          (p +ₗ #(S (ty.(ty_size))) ◁
-            own n (uninit (list_max (map ty_size tyl) - ty_size ty))) :: T') e ∨
-      typed_body E L C ((p ◁ own n (sum tyl)) :: T') e) tyl el →
+            own_ptr n (uninit (list_max (map ty_size tyl) - ty_size ty))) :: T') e ∨
+      typed_body E L C ((p ◁ own_ptr n (sum tyl)) :: T') e) tyl el →
     typed_body E L C T (case: !p of el).
   Proof. unfold tctx_extract_hasty=>->. apply type_case_own'. Qed.
 
diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index 62195526..1c7c8c5c 100644
--- a/theories/typing/unsafe/cell.v
+++ b/theories/typing/unsafe/cell.v
@@ -3,7 +3,7 @@ From iris.base_logic Require Import big_op.
 From lrust.lang Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Export type.
-From lrust.typing Require Import type_context programs shr_bor own function product uninit cont.
+From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section cell.
-- 
GitLab