From a8ddcbcd2d40c7e6582717bb2c0269ef611107ee Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 11 May 2018 11:07:37 +0200
Subject: [PATCH] Prove soundness.
---
_CoqProject | 2 +
theories/lifetime/lifetime_sig.v | 2 +-
theories/typing/programs.v | 10 ++---
theories/typing/soundness.v | 71 ++++++++++++++++++++++++++++++++
theories/typing/typing.v | 9 ++++
5 files changed, 88 insertions(+), 6 deletions(-)
create mode 100644 theories/typing/soundness.v
create mode 100644 theories/typing/typing.v
diff --git a/_CoqProject b/_CoqProject
index dc849794..e439a2af 100644
--- a/_CoqProject
+++ b/_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
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index f5c0cae9..a2b7f1b9 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/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.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 9032ff1f..7d868c27 100644
--- a/theories/typing/programs.v
+++ b/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 →
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
new file mode 100644
index 00000000..d55f339a
--- /dev/null
+++ b/theories/typing/soundness.v
@@ -0,0 +1,71 @@
+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.
diff --git a/theories/typing/typing.v b/theories/typing/typing.v
new file mode 100644
index 00000000..e6033ae3
--- /dev/null
+++ b/theories/typing/typing.v
@@ -0,0 +1,9 @@
+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.
--
GitLab