From 082e4f07b419cfb881a5d45a3733618aa608933b Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 26 Oct 2016 00:28:43 +0200
Subject: [PATCH] Typing steps : non-memory operations.

---
 _CoqProject |   2 +
 derived.v   |   2 +-
 lifetime.v  |   2 +-
 perm.v      |   9 +---
 perm_incl.v |   6 +--
 typing.v    | 150 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 valuable.v  |  30 +++++++++++
 7 files changed, 189 insertions(+), 12 deletions(-)
 create mode 100644 typing.v
 create mode 100644 valuable.v

diff --git a/_CoqProject b/_CoqProject
index 1136854b..6ef94ecd 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -13,5 +13,7 @@ wp_tactics.v
 lifetime.v
 type.v
 type_incl.v
+valuable.v
 perm.v
 perm_incl.v
+typing.v
diff --git a/derived.v b/derived.v
index 6b691080..8d4507f1 100644
--- a/derived.v
+++ b/derived.v
@@ -13,7 +13,7 @@ Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
 Coercion lit_of_bool : bool >-> base_lit.
 Notation If e0 e1 e2 := (Case e0 [e2;e1]).
 Notation Newlft := (Lit LitUnit) (only parsing).
-Notation Endlft := (Seq Skip Skip) (only parsing).
+Notation Endlft := (Seq Skip (Lit LitUnit)) (only parsing).
 
 Section derived.
 Context `{irisG lrust_lang Σ}.
diff --git a/lifetime.v b/lifetime.v
index ae6e905a..04c4812c 100644
--- a/lifetime.v
+++ b/lifetime.v
@@ -88,7 +88,7 @@ Section lft.
   (** Basic rules about lifetimes  *)
   Axiom lft_begin : ∀ `(nclose lftN ⊆ E), True ={E}=> ∃ κ, [κ]{1} ★ lft κ.
   (* TODO : Do we really need a full mask here ? *)
-  Axiom lft_end : ∀ κ, lft κ ⊢ [κ]{1} ={⊤,∅}=★ ▷ |={∅,⊤}=> [†κ].
+  Axiom lft_end : ∀ κ, lft κ ⊢ [κ]{1} -★ |={⊤,∅}▷=> [†κ].
   Axiom lft_own_op : ∀ κ q1 q2, [κ]{q1} ★ [κ]{q2} ⊣⊢ [κ]{q1+q2}.
 
   (** Creating borrows and using them  *)
diff --git a/perm.v b/perm.v
index 758d79ca..10d84185 100644
--- a/perm.v
+++ b/perm.v
@@ -1,22 +1,17 @@
 From iris.program_logic Require Import thread_local.
 From iris.proofmode Require Import tactics.
-From lrust Require Export type.
+From lrust Require Export type valuable.
 
 Delimit Scope perm_scope with P.
 Bind Scope perm_scope with perm.
 
-(* TODO : find a better place for this. *)
-Definition valuable := option val.
-Definition proj_valuable (n : Z) : valuable → valuable :=
-  (≫= λ v, match v with LitV (LitLoc l) => Some (#(shift_loc l n)) | _ => None end).
-
 Module Perm.
 
 Section perm.
 
   Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
 
-  Definition has_type (v : valuable) (ty : type) : perm :=
+  Definition has_type (v : Valuable.t) (ty : type) : perm :=
     λ tid, from_option (λ v, ty.(ty_own) tid [v]) False%I v.
 
   Definition extract (κ : lifetime) (ρ : perm) : perm :=
diff --git a/perm_incl.v b/perm_incl.v
index 4d5dd845..28eb5a24 100644
--- a/perm_incl.v
+++ b/perm_incl.v
@@ -145,7 +145,7 @@ Section props.
     foldr (λ (q : Qp) acc, q + acc)%Qc 0%Qc ql = q →
     v ◁ own q (Π tyl) ⇔
       foldr (λ qtyoffs acc,
-             proj_valuable (Z.of_nat (qtyoffs.2.2)) v ◁
+             Valuable.proj (Z.of_nat (qtyoffs.2.2)) v ◁
                            own (qtyoffs.1) (qtyoffs.2.1) ★ acc)
             ⊤ (combine ql (combine_offs tyl 0)).
   Proof.
@@ -179,7 +179,7 @@ Section props.
   Lemma perm_split_uniq_borrow_prod tyl κ v :
     v ◁ &uniq{κ} (Π tyl) ⇒
       foldr (λ tyoffs acc,
-             proj_valuable (Z.of_nat (tyoffs.2)) v ◁ &uniq{κ} (tyoffs.1) ★ acc)%P
+             Valuable.proj (Z.of_nat (tyoffs.2)) v ◁ &uniq{κ} (tyoffs.1) ★ acc)%P
             ⊤ (combine_offs tyl 0).
   Proof.
     intros tid.
@@ -196,7 +196,7 @@ Section props.
   Lemma perm_split_shr_borrow_prod tyl κ v :
     v ◁ &shr{κ} (Π tyl) ⇒
       foldr (λ tyoffs acc,
-             proj_valuable (Z.of_nat (tyoffs.2)) v ◁ &shr{κ} (tyoffs.1) ★ acc)%P
+             Valuable.proj (Z.of_nat (tyoffs.2)) v ◁ &shr{κ} (tyoffs.1) ★ acc)%P
             ⊤ (combine_offs tyl 0).
   Proof.
     intros tid.
diff --git a/typing.v b/typing.v
new file mode 100644
index 00000000..86c9fcb3
--- /dev/null
+++ b/typing.v
@@ -0,0 +1,150 @@
+From iris.program_logic Require Import thread_local hoare.
+From lrust Require Export type perm notation.
+From lrust Require Import type_incl perm_incl proofmode.
+
+Import Types Perm.
+
+Section typing.
+
+  Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
+
+  (* TODO : good notations for [typed_step] and [typed_step_ty] ? *)
+  Definition typed_step (ρ : perm) e (θ : Valuable.t → perm) :=
+    ∀ tid, {{ ρ tid ★ tl_own tid ⊤ }} e {{ v, θ (Some v) tid ★ tl_own tid ⊤ }}.
+
+  (* FIXME : why isn't the notation context on the last parameter not
+     taken into account? *)
+  Arguments typed_step _%P _%E _%P.
+
+  Definition typed_step_ty (ρ : perm) e ty :=
+    typed_step ρ e (λ ν, ν ◁ ty)%P.
+
+  Definition typed_program (ρ : perm) e :=
+    ∀ tid, {{ ρ tid ★ tl_own tid ⊤ }} e {{ v, False }}.
+
+  Lemma typed_step_frame ρ e θ ξ:
+    typed_step ρ e θ → typed_step (ρ ★ ξ) e (λ ν, θ ν ★ ξ)%P.
+  Proof. iIntros (Hwt tid) "!#[[?$]?]". iApply Hwt. by iFrame. Qed.
+
+  Lemma typed_step_exists {A} ρ θ e ξ:
+    (∀ x:A, typed_step (ρ ★ θ x) e ξ) →
+    typed_step (ρ ★ ∃ x, θ x) e ξ.
+  Proof.
+    iIntros (Hwt tid) "!#[[Hρ Hθ]?]". iDestruct "Hθ" as (x) "Hθ".
+    iApply Hwt. by iFrame.
+  Qed.
+
+  Lemma typed_step_bool ρ (b:Datatypes.bool) :
+    typed_step_ty ρ #b bool.
+  Proof. iIntros (tid) "!#[_$]". wp_value. simpl. eauto. Qed.
+
+  Lemma typed_step_int ρ (z:Datatypes.nat) :
+    typed_step_ty ρ #z int.
+  Proof. iIntros (tid) "!#[_$]". wp_value. simpl. eauto. Qed.
+
+  Lemma typed_step_fn {A n} `{Duplicable _ ρ, Closed (f :b: xl +b+ []) e} θ :
+    length xl = n →
+    (∀ (a : A) (vl : vec val n) (fv : val) e',
+        subst_l xl (map of_val vl) e = Some e' →
+        typed_program (Some fv ◁ fn θ ★ (θ a vl) ★ ρ) (subst' f fv e')) →
+    typed_step_ty ρ (Rec f xl e) (fn θ).
+  Proof.
+    iIntros (Hn He tid) "!# [#Hρ $]". iApply (wp_value _ _ _ (RecV f xl e)).
+    { simpl. destruct decide as [CL|?]. repeat f_equal. apply proof_irrel. done. }
+    iLöb as "IH". iExists _. iSplit. done. iIntros (a vl) "!#[Hθ?]".
+    assert (is_Some (subst_l xl (map of_val vl) e)) as [e' He'].
+    { clear -Hn. revert xl Hn e. induction vl=>-[|x xl] //=. by eauto.
+      intros ? e. edestruct IHvl as [e' ->]. congruence. eauto. }
+    iApply wp_rec; try done.
+    { apply List.Forall_forall=>?. rewrite in_map_iff=>-[?[<- _]].
+      rewrite to_of_val. eauto. }
+    iNext. iApply He. done. by iFrame "★#".
+  Qed.
+
+  Lemma typed_step_cont {n} `{Closed (f :b: xl +b+ []) e} ρ θ :
+    length xl = n →
+    (∀ (vl : vec val n) (fv : val) e',
+        subst_l xl (map of_val vl) e = Some e' →
+        typed_program (Some fv ◁ cont (λ vl, ρ ★ θ vl)%P ★ (θ vl) ★ ρ) (subst' f fv e')) →
+    typed_step_ty ρ (Rec f xl e) (cont θ).
+  Proof.
+    iIntros (Hn He tid) "!# [Hρ $]". iApply (wp_value _ _ _ (RecV f xl e)).
+    { simpl. destruct decide as [CL|?]. repeat f_equal. apply proof_irrel. done. }
+    iLöb as "IH". iExists _. iSplit. done. iIntros (vl) "Hθ ?".
+    assert (is_Some (subst_l xl (map of_val vl) e)) as [e' He'].
+    { clear -Hn. revert xl Hn e. induction vl=>-[|x xl] //=. by eauto.
+      intros ? e. edestruct IHvl as [e' ->]. congruence. eauto. }
+    iApply wp_rec; try done.
+    { apply List.Forall_forall=>?. rewrite in_map_iff=>-[?[<- _]].
+      rewrite to_of_val. eauto. }
+    iNext. iApply He. done. iFrame. simpl.
+    iExists _. iSplit. done. iIntros (vl') "[Hρ Hθ] Htl".
+    iDestruct ("IH" with "Hρ") as (f') "[Hf' IH']".
+    iDestruct "Hf'" as %[=<-]. iApply ("IH'" with "Hθ Htl").
+  Qed.
+
+  Lemma typed_step_valuable e ty:
+    typed_step_ty (Valuable.of_expr e ◁ ty) e ty.
+  Proof.
+    iIntros (tid) "!#[H$]".
+    destruct (Valuable.of_expr e) as [v|] eqn:Hv. 2:by iDestruct "H" as "[]".
+    by iApply Valuable.of_expr_wp.
+  Qed.
+
+  Lemma typed_step_plus e1 e2 ρ1 ρ2:
+    typed_step_ty ρ1 e1 int → typed_step_ty ρ2 e2 int →
+    typed_step_ty (ρ1 ★ ρ2) (BinOp PlusOp e1 e2) int.
+  Proof.
+    iIntros (He1 He2 tid) "!#[[H1 H2]?]".
+    wp_bind e1. iApply wp_wand_r. iSplitR "H2". iApply He1; by iFrame.
+    iIntros (v1) "[Hv1?]". iDestruct "Hv1" as (z1) "Hz1". iDestruct "Hz1" as %[=->].
+    wp_bind e2. iApply wp_wand_r. iSplitL. iApply He2; by iFrame.
+    iIntros (v2) "[Hv2?]". iDestruct "Hv2" as (z2) "Hz2". iDestruct "Hz2" as %[=->].
+    wp_op. iFrame. by iExists _.
+  Qed.
+
+  Lemma typed_step_minus e1 e2 ρ1 ρ2:
+    typed_step_ty ρ1 e1 int → typed_step_ty ρ2 e2 int →
+    typed_step_ty (ρ1 ★ ρ2) (BinOp MinusOp e1 e2) int.
+  Proof.
+    iIntros (He1 He2 tid) "!#[[H1 H2]?]".
+    wp_bind e1. iApply wp_wand_r. iSplitR "H2". iApply He1; by iFrame.
+    iIntros (v1) "[Hv1?]". iDestruct "Hv1" as (z1) "Hz1". iDestruct "Hz1" as %[=->].
+    wp_bind e2. iApply wp_wand_r. iSplitL. iApply He2; by iFrame.
+    iIntros (v2) "[Hv2?]". iDestruct "Hv2" as (z2) "Hz2". iDestruct "Hz2" as %[=->].
+    wp_op. iFrame. by iExists _.
+  Qed.
+
+  Lemma typed_step_le e1 e2 ρ1 ρ2:
+    typed_step_ty ρ1 e1 int → typed_step_ty ρ2 e2 int →
+    typed_step_ty (ρ1 ★ ρ2) (BinOp LeOp e1 e2) bool.
+  Proof.
+    iIntros (He1 He2 tid) "!#[[H1 H2]?]".
+    wp_bind e1. iApply wp_wand_r. iSplitR "H2". iApply He1; by iFrame.
+    iIntros (v1) "[Hv1?]". iDestruct "Hv1" as (z1) "Hz1". iDestruct "Hz1" as %[=->].
+    wp_bind e2. iApply wp_wand_r. iSplitL. iApply He2; by iFrame.
+    iIntros (v2) "[Hv2?]". iDestruct "Hv2" as (z2) "Hz2". iDestruct "Hz2" as %[=->].
+    iFrame. wp_op; intros _; by iExists _.
+  Qed.
+
+  Lemma typed_step_newlft ρ:
+    typed_step ρ Newlft (λ _, ∃ α, [α]{1} ★ α ∋ top)%P.
+  Proof.
+    iIntros (tid) "!#[_$]". wp_value. iVs lft_begin as (α) "[?#?]". done.
+    iVs (lft_borrow_create with "[][]") as "[_?]". done. done.
+    2:by iVsIntro; iExists α; iFrame. eauto.
+  Qed.
+
+  Lemma typed_step_endlft κ ρ:
+    typed_step (κ ∋ ρ ★ [κ]{1}) Endlft (λ _, ρ)%P.
+  Proof.
+    iIntros (tid) "!#[[Hextr [Htok #Hlft]]$]".
+    wp_bind (#() ;; #())%E.
+    iApply (wp_wand_r _ _ (λ _, _ ★ True)%I). iSplitR "Hextr".
+    iApply (wp_frame_step_l with "[-]"); try done.
+    iDestruct (lft_end with "Hlft Htok") as "$". by wp_seq.
+    iIntros (v) "[#Hκ _]". iVs (lft_extract_out with "Hκ Hextr"). done.
+    by wp_seq.
+  Qed.
+
+End typing.
\ No newline at end of file
diff --git a/valuable.v b/valuable.v
new file mode 100644
index 00000000..47cc322f
--- /dev/null
+++ b/valuable.v
@@ -0,0 +1,30 @@
+From lrust Require Export lang notation proofmode wp_tactics.
+
+Module Valuable.
+
+Definition t := option val.
+Definition proj (n : Z) : t → t :=
+  (≫= λ v, match v with LitV (LitLoc l) => Some (#(shift_loc l n)) | _ => None end).
+
+Fixpoint of_expr (e : expr) : t :=
+  match e with
+  | BinOp ProjOp e (Lit (LitInt n)) => proj n (of_expr e)
+  | e => to_val e
+  end.
+
+Lemma of_expr_wp `{irisG lrust_lang Σ} e v Φ :
+  of_expr e = Some v → Φ v ⊢ WP e {{ Φ }}.
+Proof.
+  revert v Φ. induction e=>v Φ Hv; iIntros; try done.
+  - inversion Hv; subst. by wp_value.
+  - by wp_value.
+  - destruct op; try done.
+    destruct e2; try done.
+    destruct l; try done.
+    wp_bind e1. simpl in Hv.
+    destruct (of_expr e1) as [v1|]; last done.
+    iApply IHe1. done. destruct v1; try done. destruct l; try done.
+    inversion Hv. subst. wp_op. eauto.
+Qed.
+
+End Valuable.
\ No newline at end of file
-- 
GitLab