define typing for instructions; int and bool now no longer import any of the outdated def.s

theories/typing/bool.v

 From iris.proofmode Require Import tactics.
 From lrust.typing Require Export type.
-From lrust.typing Require Import typing perm.
+From lrust.typing Require Import programs.
 
 Section bool.
   Context `{typeG Σ}.
@@ -9,16 +9,24 @@ Section bool.
     {| st_own tid vl := (∃ z:bool, ⌜vl = [ #z ]⌝)%I |}.
   Next Obligation. iIntros (tid vl) "H". iDestruct "H" as (z) "%". by subst. Qed.
 
-  Lemma typed_bool ρ (b:Datatypes.bool): typed_step_ty ρ #b bool.
-  Proof. iIntros (tid) "!#(_&_&_&$)". wp_value. by iExists _. Qed.
+  Lemma typed_bool (b : Datatypes.bool) E L :
+    typed_instruction_ty E L [] #b bool.
+  Proof.
+    iIntros (tid qE) "!# _ $ $ _". wp_value. rewrite tctx_interp_singleton.
+    iExists _. iSplitR; first done. iExists _. done.
+  Qed.
 
-  Lemma typed_if ρ e1 e2 ν:
-    typed_program ρ e1 → typed_program ρ e2 →
-    typed_program (ρ ∗ ν ◁ bool) (if: ν then e1 else e2).
+  Lemma typed_if E L C T e1 e2 p:
+    typed_body E L C T e1 → typed_body E L C T e2 →
+    typed_body E L C (TCtx_hasty p bool :: T) (if: p then e1 else e2).
   Proof.
-    iIntros (He1 He2 tid) "!#(#HEAP & #LFT & [Hρ H◁] & Htl)".
-    wp_bind ν. iApply (has_type_wp with "H◁"). iIntros (v) "% H◁!>".
-    rewrite has_type_value. iDestruct "H◁" as (b) "Heq". iDestruct "Heq" as %[= ->].
-    wp_if. destruct b; iNext. iApply He1; iFrame "∗#". iApply He2; iFrame "∗#".
+    (* FIXME why can't I merge these two iIntros? *)
+    iIntros (He1 He2). iIntros (tid qE) "#LFT HE HL HC".
+    rewrite tctx_interp_cons. iIntros "[Hp HT]".
+    wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "[% Hown]".
+    iDestruct "Hown" as (b) "Hv". iDestruct "Hv" as %[=->].
+    destruct b; wp_if.
+    - iApply (He1 with "LFT HE HL HC HT").
+    - iApply (He2 with "LFT HE HL HC HT").
   Qed.
-End bool.
+End bool.
\ No newline at end of file

theories/typing/int.v

 From iris.proofmode Require Import tactics.
 From lrust.typing Require Export type.
-From lrust.typing Require Import typing bool perm.
+From lrust.typing Require Import bool programs.
 
 Section int.
   Context `{typeG Σ}.
@@ -9,46 +9,50 @@ Section int.
     {| st_own tid vl := (∃ z:Z, ⌜vl = [ #z ]⌝)%I |}.
   Next Obligation. iIntros (tid vl) "H". iDestruct "H" as (z) "%". by subst. Qed.
 
-  Lemma typed_int ρ (z:Datatypes.nat) :
-    typed_step_ty ρ #z int.
-  Proof. iIntros (tid) "!#(_&_&_&$)". wp_value. by iExists _. Qed.
+  Lemma typed_int (z : Z) E L :
+    typed_instruction_ty E L [] #z int.
+  Proof.
+    iIntros (tid qE) "!# _ $ $ _". wp_value. rewrite tctx_interp_singleton.
+    iExists _. iSplitR; first done. iExists _. done.
+  Qed.
 
-  Lemma typed_plus e1 e2 ρ1 ρ2:
-    typed_step_ty ρ1 e1 int → typed_step_ty ρ2 e2 int →
-    typed_step_ty (ρ1 ∗ ρ2) (e1 + e2) int.
+  Lemma typed_plus E L p1 p2 :
+    typed_instruction_ty E L [TCtx_hasty p1 int; TCtx_hasty p2 int] (p1 + p2) int.
   Proof.
-    unfold typed_step_ty, typed_step. setoid_rewrite has_type_value.
-    iIntros (He1 He2 tid) "!#(#HEAP&#ĽFT&[H1 H2]&?)".
-    wp_bind e1. iApply wp_wand_r. iSplitR "H2". iApply He1; iFrame "∗#".
-    iIntros (v1) "[Hv1?]". iDestruct "Hv1" as (z1) "Hz1". iDestruct "Hz1" as %[=->].
-    wp_bind e2. iApply wp_wand_r. iSplitL. iApply He2; iFrame "∗#".
-    iIntros (v2) "[Hv2$]". iDestruct "Hv2" as (z2) "Hz2". iDestruct "Hz2" as %[=->].
-    wp_op. by iExists _.
+    iIntros (tid qE) "!# _ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
+    iIntros "[Hp1 Hp2]".
+    wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "[% Hown1]".
+    wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "[% Hown2]".
+    iDestruct "Hown1" as (z1) "EQ". iDestruct "EQ" as %[=->].
+    iDestruct "Hown2" as (z2) "EQ". iDestruct "EQ" as %[=->].
+    wp_op. rewrite tctx_interp_singleton. iExists _. iSplitR; first done.
+    iExists _. done.
   Qed.
 
-  Lemma typed_minus e1 e2 ρ1 ρ2:
-    typed_step_ty ρ1 e1 int → typed_step_ty ρ2 e2 int →
-    typed_step_ty (ρ1 ∗ ρ2) (e1 - e2) int.
+  Lemma typed_minus E L p1 p2 :
+    typed_instruction_ty E L [TCtx_hasty p1 int; TCtx_hasty p2 int] (p1 - p2) int.
   Proof.
-    unfold typed_step_ty, typed_step. setoid_rewrite has_type_value.
-    iIntros (He1 He2 tid) "!#(#HEAP&#LFT&[H1 H2]&?)".
-    wp_bind e1. iApply wp_wand_r. iSplitR "H2". iApply He1; iFrame "∗#".
-    iIntros (v1) "[Hv1?]". iDestruct "Hv1" as (z1) "Hz1". iDestruct "Hz1" as %[=->].
-    wp_bind e2. iApply wp_wand_r. iSplitL. iApply He2; iFrame "∗#".
-    iIntros (v2) "[Hv2$]". iDestruct "Hv2" as (z2) "Hz2". iDestruct "Hz2" as %[=->].
-    wp_op. by iExists _.
+    iIntros (tid qE) "!# _ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
+    iIntros "[Hp1 Hp2]".
+    wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "[% Hown1]".
+    wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "[% Hown2]".
+    iDestruct "Hown1" as (z1) "EQ". iDestruct "EQ" as %[=->].
+    iDestruct "Hown2" as (z2) "EQ". iDestruct "EQ" as %[=->].
+    wp_op. rewrite tctx_interp_singleton. iExists _. iSplitR; first done.
+    iExists _. done.
   Qed.
 
-  Lemma typed_le e1 e2 ρ1 ρ2:
-    typed_step_ty ρ1 e1 int → typed_step_ty ρ2 e2 int →
-    typed_step_ty (ρ1 ∗ ρ2) (e1 ≤ e2) bool.
+  Lemma typed_le E L p1 p2 :
+    typed_instruction_ty E L [TCtx_hasty p1 int; TCtx_hasty p2 int] (p1 ≤ p2) bool.
   Proof.
-    unfold typed_step_ty, typed_step. setoid_rewrite has_type_value.
-    iIntros (He1 He2 tid) "!#(#HEAP&#LFT&[H1 H2]&?)".
-    wp_bind e1. iApply wp_wand_r. iSplitR "H2". iApply He1; iFrame "∗#".
-    iIntros (v1) "[Hv1?]". iDestruct "Hv1" as (z1) "Hz1". iDestruct "Hz1" as %[=->].
-    wp_bind e2. iApply wp_wand_r. iSplitL. iApply He2; iFrame "∗#".
-    iIntros (v2) "[Hv2$]". iDestruct "Hv2" as (z2) "Hz2". iDestruct "Hz2" as %[=->].
-    wp_op; intros _; by iExists _.
+    iIntros (tid qE) "!# _ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
+    iIntros "[Hp1 Hp2]".
+    wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "[% Hown1]".
+    wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "[% Hown2]".
+    iDestruct "Hown1" as (z1) "EQ". iDestruct "EQ" as %[=->].
+    iDestruct "Hown2" as (z2) "EQ". iDestruct "EQ" as %[=->].
+    wp_op; intros _; rewrite tctx_interp_singleton; iExists _; (iSplitR; first done);
+      iExists _; done.
   Qed.
+  
 End int.

theories/typing/product_split.v

@@ -163,7 +163,8 @@ Section product_split.
     iDestruct "H" as (l P) "[[EQ #HPiff] HP]". iDestruct "EQ" as %[=->]. 
     iMod (bor_iff with "LFT [] HP") as "Hown". set_solver. by eauto.
     rewrite /= split_prod_mt. iMod (bor_sep with "LFT Hown") as "[H1 H2]".
-    set_solver. iSplitL "H1"; iExists _; (iSplitR; first by rewrite Hp);
+    set_solver. rewrite /tctx_elt_interp /=.
+    iSplitL "H1"; iExists _; (iSplitR; first by rewrite Hp);
                   iExists _, _; erewrite <-uPred.iff_refl; auto.
   Qed.
 

theories/typing/programs.v

-From iris.program_logic Require Import hoare.
 From iris.base_logic Require Import big_op.
 From lrust.lang Require Export notation memcpy.
-From lrust.typing Require Export type.
-From lrust.typing Require Import perm lft_contexts type_context cont_context.
 From lrust.lang Require Import proofmode.
 From lrust.lifetime Require Import frac_borrow reborrow borrow creation.
+From lrust.typing Require Export type lft_contexts type_context cont_context.
 
 Section typing.
   Context `{typeG Σ}.
 
+  (** Function Body *)
   Definition typed_body (E : elctx) (L : llctx) (C : cctx) (T : tctx)
                         (e : expr) : iProp Σ :=
     (∀ tid qE, lft_ctx -∗ elctx_interp E qE -∗ llctx_interp L 1 -∗
                (elctx_interp E qE -∗ cctx_interp tid C) -∗ tctx_interp tid T -∗
                WP e {{ _, cont_postcondition }})%I.
+  Global Arguments typed_body _ _ _ _ _%E.
 
   Instance typed_body_llctx_permut E :
     Proper ((≡ₚ) ==> eq ==> eq ==> eq ==> (⊢)) (typed_body E).
@@ -21,6 +21,12 @@ Section typing.
     intros L1 L2 HL C ? <- T ? <- e ? <-. rewrite /typed_body. by setoid_rewrite HL.
   Qed.
 
+  Instance typed_body_elctx_permut :
+    Proper ((≡ₚ) ==> eq ==> eq ==> eq ==> eq ==> (⊢)) typed_body.
+  Proof.
+    intros E1 E2 HE L ? <- C ? <- T ? <- e ? <-. rewrite /typed_body. by setoid_rewrite HE.
+  Qed.
+
   Instance typed_body_mono E L:
     Proper (flip (cctx_incl E) ==> flip (tctx_incl E L) ==> eq ==> (⊢)) (typed_body E L).
   Proof.
@@ -31,4 +37,12 @@ Section typing.
     iIntros "HE". by iApply (HC with "LFT HC").
   Qed.
 
+  (** Instruction *)
+  Definition typed_instruction (E : elctx) (L : llctx)
+             (T1 : tctx) (e : expr) (T2 : val → tctx) : iProp Σ :=
+    (∀ tid qE, □ (lft_ctx -∗ elctx_interp E qE -∗ llctx_interp L 1 -∗ tctx_interp tid T1 -∗
+                   WP e {{ v, elctx_interp E qE ∗ llctx_interp L 1 ∗ tctx_interp tid (T2 v) }}))%I.
+  Global Arguments typed_instruction _ _ _ _%E _.
 End typing.
+
+Notation typed_instruction_ty E L T1 e ty := (typed_instruction E L T1 e (λ v : val, [TCtx_hasty v ty])).

theories/typing/shr_bor.v

@@ -52,7 +52,8 @@ Section typing.
     iDestruct "EQ" as %[=->]. simpl. iModIntro. iSplit.
     - iExists _. iSplit. done. iExists _. iSplit. done.
       by iApply (ty_shr_mono with "LFT Hκκ' Hshr").
-    - iExists _. iSplit. done. iIntros "_". eauto.
+    - iExists _. iSplit. done. iIntros "_". iIntros "!> !>".
+      iExists _. auto.
   Qed.
 
 End typing.

theories/typing/type_context.v

@@ -10,8 +10,8 @@ Bind Scope expr_scope with path.
 Section type_context.
   Context `{typeG Σ}.
 
-  Fixpoint eval_path (ν : path) : option val :=
-    match ν with
+  Fixpoint eval_path (p : path) : option val :=
+    match p with
     | BinOp OffsetOp e (Lit (LitInt n)) =>
       match eval_path e with
       | Some (#(LitLoc l)) => Some (#(shift_loc l n))
@@ -33,6 +33,8 @@ Section type_context.
     | TCtx_blocked p κ ty => ∃ v, ⌜eval_path p = Some v⌝ ∗
                              ([†κ] ={⊤}=∗ ▷ ty.(ty_own) tid [v])
     end%I.
+  (* Block tctx_elt_interp from reducing with simpl when x is a constructor. *)
+  Global Arguments tctx_elt_interp : simpl never.
   Definition tctx_interp (tid : thread_id) (T : tctx) : iProp Σ :=
     ([∗ list] x ∈ T, tctx_elt_interp tid x)%I.
 
@@ -69,7 +71,35 @@ Section type_context.
     eval_path p1 = eval_path p2 →
     tctx_elt_interp tid (TCtx_hasty p1 ty) ≡
     tctx_elt_interp tid (TCtx_hasty p2 ty).
-  Proof. intros Hp. simpl. setoid_rewrite Hp. done. Qed.
+  Proof. intros Hp. rewrite /tctx_elt_interp /=. setoid_rewrite Hp. done. Qed.
+
+  Lemma wp_eval_path p v :
+    eval_path p = Some v → (WP p {{ v', ⌜v' = v⌝ }})%I.
+  Proof.
+    revert v; induction p; intros v; cbn -[to_val];
+      try (intros ?; by iApply wp_value); [].
+    destruct op; try discriminate; [].
+    destruct p2; try (intros ?; by iApply wp_value); [].
+    destruct l; try (intros ?; by iApply wp_value); [].
+    destruct (eval_path p1); try (intros ?; by iApply wp_value); [].
+    destruct v0; try discriminate; [].
+    destruct l; try discriminate; [].
+    intros [=<-]. iStartProof. wp_bind p1.
+    iApply (wp_wand with "[]").
+    { iApply IHp1. done. }
+    iIntros (v) "%". subst v. wp_op. done.
+  Qed.
+
+  Lemma wp_hasty tid p ty Φ :
+    tctx_elt_interp tid (TCtx_hasty p ty) -∗
+    (∀ v, ⌜eval_path p = Some v⌝ ∗ ty.(ty_own) tid [v] -∗ Φ v) -∗
+    WP p {{ Φ }}.
+  Proof.
+    iIntros "Hty HΦ". iDestruct "Hty" as (v) "[% Hown]".
+    iApply (wp_wand with "[]").
+    { iApply wp_eval_path. done. }
+    iIntros (v') "%". subst v'. iApply "HΦ". by auto.
+  Qed.
 
   Lemma contains_tctx_incl E L T1 T2 : T1 `contains` T2 → tctx_incl E L T2 T1.
   Proof.