Prove soundness.

_CoqProject

@@ -39,3 +39,5 @@ theories/typing/type_sum.v
 theories/typing/fixpoint.v
 theories/typing/cont.v
 theories/typing/function.v
+theories/typing/typing.v
+theories/typing/soundness.v

theories/lifetime/lifetime_sig.v

@@ -194,5 +194,5 @@ Module Type lifetime_sig.
   Global Declare Instance subG_lftPreG Lat Σ : subG (lftΣ Lat) Σ → lftPreG Lat Σ.
 
   Parameter lft_init : ∀ `{invG Σ, !lftPreG Lat Σ} E, ↑lftN ⊆ E →
-    True ={E}=∗ ∃ _ : lftG Lat Σ, lft_ctx.
+    (|={E}=> ∃ _ : lftG Lat Σ, lft_ctx)%I.
 End lifetime_sig.

theories/typing/programs.v

@@ -226,11 +226,11 @@ Section typing_rules.
         (l vl q [= ->]) "(Hl & Hown & Hclose)"; first done.
     iDestruct (ty_size_eq with "Hown") as "#>%". rewrite ->Hsz in *.
     destruct vl as [|v [|]]; try done.
-    rewrite own_loc_na_vec_singleton. iApply wp_fupd. (*  wp_read. *)
-    (* iMod ("Hclose" with "Hl") as "($ & $ & Hown2)". *)
-    (* rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //. *)
-    (* by iFrame. *)
-  Admitted.
+    rewrite own_loc_na_vec_singleton. iApply wp_fupd. wp_read.
+    iMod ("Hclose" with "Hl") as "($ & $ & Hown2)".
+    rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
+    by iFrame.
+  Qed.
 
   Lemma type_deref {E L} ty1 C T T' ty ty1' x p e:
     Closed (x :b: []) e →

theories/typing/soundness.v

+From iris.bi Require Import big_op.
+From iris.algebra Require Import frac.
+From iris.program_logic Require Import adequacy.
+From gpfsl.lang Require Import na_invariants adequacy.
+From lrust.lang Require Import 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 :> noprolPreG Σ;
+  type_lftG :> lftPreG view_Lat Σ;
+  type_preG_na_invG :> na_invG view_Lat Σ;
+  type_frac_borrowG :> frac_borG Σ
+}.
+
+Definition typeΣ : gFunctors :=
+  #[noprolΣ; lftΣ view_Lat; na_invΣ view_Lat; GFunctor (constRF fracR)].
+Instance subG_typePreG {Σ} : subG typeΣ Σ → typePreG Σ.
+Proof. solve_inG. Qed.
+
+Section type_soundness.
+  Definition exit_cont : val := λ: [<>], #☠.
+
+  Definition main_type `{typeG Σ} := (fn(∅) → unit)%T.
+
+  Theorem type_soundness `{typePreG Σ} (main : val) t σ :
+    (∀ `{typeG Σ}, typed_val main main_type) →
+    rtc step ([(main [exit_cont] at init_tview)%E], mkGB ∅ ∅ ∅) (t, σ) →
+    (* nonracing_threadpool t σ ∧ *)   (* TODO : prove DRF theorem *)
+    (∀ e 𝓥, (e at 𝓥)%E ∈ t → is_Some (to_val e) ∨ reducible (e at 𝓥) σ).
+  Proof.
+    intros Hmain Hrtc.
+    cut (adequate NotStuck (main [exit_cont]%E at init_tview) (mkGB ∅ ∅ ∅) (λ _, True)).
+    { (* split. by eapply adequate_nonracing. *)
+      intros.
+      edestruct (adequate_not_stuck NotStuck (main [exit_cont]%E at init_tview))
+         as [toval|red]=>//.
+      - destruct toval as [v ?%nopro_lang.to_base_val]. eauto.
+      - eauto. }
+    apply: (noprol_adequacy' _ _ (λ x, True))=>? tid1.
+    iMod lft_init as (?) "#LFT". done.
+    iMod na_alloc as (tid2) "Htl". set (Htype := TypeG _ _ _ _ _).
+    set (tid := {| tid_na_inv_pool := tid2; tid_tid := tid1 |}).
+    wp_bind (of_val main). iApply (wp_wand with "[Htl]").
+    { iApply (Hmain _ [] [] $! tid with "LFT [] Htl [] []");
+        by rewrite /elctx_interp /llctx_interp ?tctx_interp_nil. }
+    clear Hrtc Hmain main. iIntros (main) "(Htl & _ & Hmain & _)".
+    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. wp_rec.
+    iMod (lft_create with "LFT") as (ϝ) "Hϝ"; first done.
+    iApply ("Hmain" $! () ϝ exit_cont [#] tid with "LFT [] Htl [Hϝ] []");
+      last by rewrite tctx_interp_nil.
+    { by rewrite /elctx_interp /=. }
+    { rewrite /llctx_interp /=. iSplit; last done. iExists ϝ. iFrame. by rewrite /= left_id. }
+    rewrite cctx_interp_singleton. simpl. iIntros (args) "_ _".
+    inv_vec args. iIntros (x) "_ /=". by wp_lam.
+  Qed.
+End type_soundness.
+
+(* Soundness theorem when no other CMRA is needed. *)
+
+Theorem type_soundness_closed (main : val) σ t :
+  (∀ `{typeG typeΣ}, typed_val main main_type) →
+  rtc step ([(main [exit_cont] at init_tview)%E], mkGB ∅ ∅ ∅) (t, σ) →
+  (* nonracing_threadpool t σ ∧ *)   (* TODO : prove DRF theorem *)
+  (∀ e 𝓥, (e at 𝓥)%E ∈ t → is_Some (to_val e) ∨ reducible (e at 𝓥) σ).
+Proof. intros. eapply @type_soundness; try done. apply _. Qed.

theories/typing/typing.v

+From lrust.lang Require Export memcpy notation.
+From lrust.typing Require Export
+  lft_contexts type_context cont_context programs cont type
+  int bool own uniq_bor shr_bor uninit product sum fixpoint function
+  product_split borrow type_sum.
+
+(* Last, so that we make sure we shadow the defintion of delete for
+   collections coming from the prelude. *)
+From lrust.lang Require Export new_delete.