Merge branch 'master' of https://gitlab.mpi-sws.org/FP/LambdaRust-coq

opam.pins

-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 53fe9f4028ceeb7346a528ad0748fd0f3de3edd5
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 05b530001f48a4544a9aaee7b8ff1a2abbe14e14

theories/typing/bool.v

@@ -18,13 +18,21 @@ End bool.
 Section typing.
   Context `{typeG Σ}.
 
-  Lemma type_bool (b : Datatypes.bool) E L :
+  Lemma type_bool_instr (b : Datatypes.bool) E L :
     typed_instruction_ty E L [] #b bool.
   Proof.
     iAlways. iIntros (tid qE) "_ _ $ $ $ _". wp_value.
     rewrite tctx_interp_singleton tctx_hasty_val. iExists _. done.
   Qed.
 
+  Lemma typed_bool (b : Datatypes.bool) E L C T x e :
+    Closed (x :b: []) e →
+    (∀ (v : val), typed_body E L C ((v ◁ bool) :: T) (subst' x v e)) →
+    typed_body E L C T (let: x := #b in e).
+  Proof.
+    intros. eapply type_let; [done|apply type_bool_instr|solve_typing|done].
+  Qed.
+
   Lemma type_if E L C T e1 e2 p:
     (p ◁ bool)%TC ∈ T →
     typed_body E L C T e1 → typed_body E L C T e2 →

theories/typing/borrow.v

@@ -28,7 +28,10 @@ Section borrow.
   Lemma tctx_extract_hasty_borrow E L p n ty κ T :
     tctx_extract_hasty E L p (&uniq{κ}ty) ((p ◁ own n ty)::T)
                        ((p ◁{κ} own n ty)::T).
-  Proof. apply (tctx_incl_frame_r _ [_] [_;_]), tctx_borrow. Qed.
+  Proof.
+    rewrite tctx_extract_hasty_unfold.
+    apply (tctx_incl_frame_r _ [_] [_;_]), tctx_borrow.
+  Qed.
 
   (* 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 :
@@ -36,7 +39,8 @@ Section borrow.
     tctx_extract_hasty E L p (&shr{κ}ty) ((p ◁ own n ty')::T)
                        ((p ◁ &shr{κ}ty')::(p ◁{κ} own n ty')::T).
   Proof.
-    intros. apply (tctx_incl_frame_r _ [_] [_;_;_]). rewrite ->tctx_borrow.
+    rewrite tctx_extract_hasty_unfold=>??.
+    apply (tctx_incl_frame_r _ [_] [_;_;_]). rewrite ->tctx_borrow.
     apply (tctx_incl_frame_r _ [_] [_;_]). rewrite ->tctx_share; solve_typing.
   Qed.
 

theories/typing/function.v

@@ -156,7 +156,7 @@ Section typing.
   Qed.
 
   (* TODO: Define some syntactic sugar for calling and letrec like we do on paper. *)
-  Lemma type_call {A} E L E' T p (ps : list path)
+  Lemma type_call' {A} E L E' T p (ps : list path)
                          (tys : A → vec type (length ps)) ty k x :
     elctx_sat E L (E' x) →
     typed_body E L [k ◁cont(L, λ v : vec _ 1, (v!!!0 ◁ ty x) :: T)]
@@ -197,7 +197,7 @@ Section typing.
         iApply (big_sepL_mono' with "Hvl"). by iIntros (i [v ty']).
   Qed.
 
-  Lemma type_call' {A} x E L E' C T T' T'' p (ps : list path)
+  Lemma type_call {A} x E L E' C T T' T'' p (ps : list path)
                         (tys : A → vec type (length ps)) ty k :
     (p ◁ fn E' tys ty)%TC ∈ T →
     elctx_sat E L (E' x) →
@@ -207,10 +207,11 @@ Section typing.
     typed_body E L C T (call: p ps → k).
   Proof.
     intros Hfn HE HTT' HC HT'T''.
-    rewrite -typed_body_mono /flip; last done; first by eapply type_call.
+    rewrite -typed_body_mono /flip; last done; first by eapply type_call'.
     - etrans. eapply (incl_cctx_incl _ [_]); first by intros ? ->%elem_of_list_singleton.
-      apply cctx_incl_cons_match; first done. intros args. inv_vec args=>ret q. inv_vec q. done.
-    - etrans; last by apply (tctx_incl_frame_l [_]).
+      apply cctx_incl_cons_match; first done. intros args. by inv_vec args.
+    - rewrite tctx_extract_ctx_unfold in HTT'.
+      etrans; last by apply (tctx_incl_frame_l [_]).
       apply copy_elem_of_tctx_incl; last done. apply _.
   Qed.
 
@@ -231,7 +232,7 @@ Section typing.
       + by eapply is_closed_weaken, list_subseteq_nil.
       + eapply Is_true_eq_left, forallb_forall, List.Forall_forall, Forall_impl=>//.
         intros. eapply Is_true_eq_true, is_closed_weaken=>//. set_solver+.
-    - intros k ret. inv_vec ret=>ret v0. inv_vec v0. rewrite /subst_v /=.
+    - intros k ret. inv_vec ret=>ret. rewrite /subst_v /=.
       rewrite ->(is_closed_subst []), incl_cctx_incl; first done; try set_solver+.
       apply subst'_is_closed; last done. apply is_closed_of_val.
     - intros.
@@ -241,7 +242,7 @@ Section typing.
       rewrite is_closed_nil_subst //.
       assert (map (subst "_k" k) ps = ps) as ->.
       { clear -Hpsc. induction Hpsc=>//=. rewrite is_closed_nil_subst //. congruence. }
-      eapply type_call'; try done. constructor. done.
+      eapply type_call; try done. constructor. done.
   Qed.
 
   Lemma type_rec {A} E L E' fb kb (argsb : list binder) e

theories/typing/int.v

@@ -17,14 +17,22 @@ End int.
 Section typing.
   Context `{typeG Σ}.
 
-  Lemma type_int (z : Z) E L :
+  Lemma type_int_instr (z : Z) E L :
     typed_instruction_ty E L [] #z int.
   Proof.
     iAlways. iIntros (tid qE) "_ _ $ $ $ _". wp_value.
     rewrite tctx_interp_singleton tctx_hasty_val. iExists _. done.
   Qed.
 
-  Lemma type_plus E L p1 p2 :
+  Lemma typed_int (z : Z) E L C T x e :
+    Closed (x :b: []) e →
+    (∀ (v : val), typed_body E L C ((v ◁ int) :: T) (subst' x v e)) →
+    typed_body E L C T (let: x := #z in e).
+  Proof.
+    intros. eapply type_let; [done|apply type_int_instr|solve_typing|done].
+  Qed.
+
+  Lemma type_plus_instr E L p1 p2 :
     typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 + p2) int.
   Proof.
     iAlways. iIntros (tid qE) "_ _ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
@@ -37,7 +45,16 @@ Section typing.
     iExists _. done.
   Qed.
 
-  Lemma type_minus E L p1 p2 :
+  Lemma typed_plus E L C T T' p1 p2 x e :
+    Closed (x :b: []) e →
+    tctx_extract_ctx E L [p1 ◁ int; p2 ◁ int] T T' →
+    (∀ (v : val), typed_body E L C ((v ◁ int) :: T') (subst' x v e)) →
+    typed_body E L C T (let: x := p1 + p2 in e).
+  Proof.
+    intros. eapply type_let; [done|apply type_plus_instr|solve_typing|done].
+  Qed.
+
+  Lemma type_minus_instr E L p1 p2 :
     typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 - p2) int.
   Proof.
     iAlways. iIntros (tid qE) "_ _ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
@@ -50,7 +67,16 @@ Section typing.
     iExists _. done.
   Qed.
 
-  Lemma type_le E L p1 p2 :
+  Lemma typed_minus E L C T T' p1 p2 x e :
+    Closed (x :b: []) e →
+    tctx_extract_ctx E L [p1 ◁ int; p2 ◁ int] T T' →
+    (∀ (v : val), typed_body E L C ((v ◁ int) :: T') (subst' x v e)) →
+    typed_body E L C T (let: x := p1 - p2 in e).
+  Proof.
+    intros. eapply type_let; [done|apply type_minus_instr|solve_typing|done].
+  Qed.
+
+  Lemma type_le_instr E L p1 p2 :
     typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 ≤ p2) bool.
   Proof.
     iAlways. iIntros (tid qE) "_ _ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
@@ -63,4 +89,12 @@ Section typing.
       iExists _; done.
   Qed.
 
+  Lemma typed_le E L C T T' p1 p2 x e :
+    Closed (x :b: []) e →
+    tctx_extract_ctx E L [p1 ◁ int; p2 ◁ int] T T' →
+    (∀ (v : val), typed_body E L C ((v ◁ bool) :: T') (subst' x v e)) →
+    typed_body E L C T (let: x := p1 ≤ p2 in e).
+  Proof.
+    intros. eapply type_let; [done|apply type_le_instr|solve_typing|done].
+  Qed.
 End typing.

theories/typing/own.v

@@ -190,23 +190,29 @@ Section typing.
     iApply uninit_own. auto.
   Qed.
 
-  Lemma type_new {E L} (n : nat) :
-    typed_instruction_ty E L [] (new [ #n ]%E) (own n (uninit n)).
+  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')).
   Proof.
-    iAlways. iIntros (tid eq) "#HEAP #LFT $ $ $ _".
-    iApply (wp_new with "HEAP"); try done; first omega. iModIntro.
-    iIntros (l vl) "(% & H† & Hlft)". rewrite tctx_interp_singleton tctx_hasty_val.
-    iExists _. iSplit; first done. iNext. rewrite Nat2Z.id freeable_sz_full. iFrame.
-    iExists vl. iFrame.
-    match goal with H : Z.of_nat n = Z.of_nat (length vl) |- _ => rename H into Hlen end.
-    apply (inj Z.of_nat) in Hlen. subst.
-    iInduction vl as [|v vl] "IH". done.
-    iExists [v], vl. iSplit. done. by iSplit.
+    intros. iAlways. iIntros (tid q) "#HEAP #LFT $ $ $ _".
+    iApply (wp_new with "HEAP"); try done. iModIntro.
+    iIntros (l vl) "(% & H† & Hlft)". subst. rewrite tctx_interp_singleton tctx_hasty_val.
+    iExists _. iSplit; first done. iNext. rewrite freeable_sz_full Z2Nat.id //. iFrame.
+    iExists vl. iFrame. by rewrite Nat2Z.id uninit_own.
   Qed.
 
-  Lemma type_delete {E L} ty n p :
-    ty.(ty_size) = n →
-    typed_instruction E L [p ◁ own n ty] (delete [ #n; p])%E (λ _, []).
+  Lemma type_new E L C T x (n : Z) e :
+    Closed (x :b: []) e →
+    0 ≤ n →
+    (∀ (v : val) (n' := Z.to_nat n),
+        typed_body E L C ((v ◁ own n' (uninit n')) :: T) (subst' x v e)) →
+    typed_body E L C T (let: x := new [ #n ] in e).
+  Proof. intros. eapply type_let. done. by apply type_new_instr. solve_typing. done. Qed.
+
+  Lemma type_delete_instr {E L} ty (n : Z) p :
+    Z.of_nat (ty.(ty_size)) = n →
+    typed_instruction E L [p ◁ own (ty.(ty_size)) ty] (delete [ #n; p])%E (λ _, []).
   Proof.
     iIntros (<-) "!#". iIntros (tid eq) "#HEAP #LFT $ $ $ Hp". rewrite tctx_interp_singleton.
     wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
@@ -217,6 +223,17 @@ Section typing.
     rewrite freeable_sz_full. by iFrame.
   Qed.
 
+  Lemma type_delete E L C T T' (n' : nat) ty (n : Z)  p e :
+    Closed [] e →
+    tctx_extract_hasty E L p (own 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).
+  Proof.
+    intros ?? -> Hlen ?. eapply type_seq; [done|by apply type_delete_instr| |done].
+    by rewrite (inj _ _ _ Hlen).
+  Qed.
+
   Lemma type_letalloc_1 {E L} ty C T T' (x : string) p e :
     ty.(ty_size) = 1%nat →
     Closed [] p → Closed (x :b: []) e →
@@ -224,22 +241,18 @@ Section typing.
     (∀ (v : val), typed_body E L C ((v ◁ own 1 ty)::T') (subst x v e)) →
     typed_body E L C T (letalloc: x := p in e).
   Proof.
-    intros. eapply type_let'.
+    intros. eapply type_new.
     - rewrite /Closed /=. rewrite !andb_True.
       eauto 10 using is_closed_weaken with set_solver.
-    - apply (type_new 1).
-    - solve_typing.
+    - done.
     - move=>xv /=.
       assert (subst x xv (x <- p ;; e)%E = (xv <- p ;; subst x xv e)%E) as ->.
       { (* TODO : simpl_subst should be able to do this. *)
         unfold subst=>/=. repeat f_equal.
         - by rewrite bool_decide_true.
         - eapply is_closed_subst. done. set_solver. }
-      eapply type_let'.
-      + apply subst_is_closed; last done. apply is_closed_of_val.
-      + by apply (type_assign ty (own 1 (uninit 1))), write_own.
-      + solve_typing.
-      + move=>//=.
+      eapply type_assign; [|solve_typing|by eapply write_own|done].
+      apply subst_is_closed; last done. apply is_closed_of_val.
   Qed.
 
   Lemma type_letalloc_n {E L} ty ty1 ty2 C T T' (x : string) p e :
@@ -250,11 +263,10 @@ Section typing.
         typed_body E L C ((v ◁ own (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_let'.
+    intros. eapply type_new.
     - rewrite /Closed /=. rewrite !andb_True.
       eauto 100 using is_closed_weaken with set_solver.
-    - apply type_new.
-    - solve_typing.
+    - lia.
     - move=>xv /=.
       assert (subst x xv (x <⋯ !{ty.(ty_size)}p ;; e)%E =
               (xv <⋯ !{ty.(ty_size)}p ;; subst x xv e)%E) as ->.
@@ -263,16 +275,17 @@ Section typing.
         - eapply (is_closed_subst []). done. set_solver.
         - by rewrite bool_decide_true.
         - eapply is_closed_subst. done. set_solver. }
-      eapply type_let'.
+      rewrite Nat2Z.id. eapply type_memcpy.
       + apply subst_is_closed; last done. apply is_closed_of_val.
-      + eapply type_memcpy; first done; last done.
-        (* TODO: Doing "eassumption" here shows that unification takes *forever* to fail.
+      + solve_typing.
+      + (* TODO: Doing "eassumption" here shows that unification takes *forever* to fail.
            I guess that's caused by it trying to unify typed_read and typed_write,
            but considering that the Iris connectives are all sealed, why does
            that take so long? *)
-        by eapply (write_own _ (uninit _)).
+        by eapply (write_own ty (uninit _)).
       + solve_typing.
-      + move=>//=.
+      + done.
+      + done.
   Qed.
 End typing.
 

theories/typing/product_split.v

@@ -62,8 +62,8 @@ Section product_split.
     iIntros (Hptr Htyl Hmerge Hloc p tid q1 q2) "#LFT HE HL H".
     iInduction tyl as [|ty tyl IH] "IH" forall (p Htyl); first done.
     rewrite product_cons. rewrite /= tctx_interp_singleton tctx_interp_cons.
-    iDestruct "H" as "[Hty Htyl]". iDestruct "Hty" as (v) "[Hp Hty]". iDestruct "Hp" as %Hp. 
-    iDestruct (Hloc with "Hty") as %[l [=->]].
+    iDestruct "H" as "[Hty Htyl]". iDestruct "Hty" as (v) "[Hp Hty]".
+    iDestruct "Hp" as %Hp. iDestruct (Hloc with "Hty") as %[l [=->]].
     assert (eval_path p = Some #l) as Hp'.
     { move:Hp. simpl. clear. destruct (eval_path p); last done.
       destruct v; try done. destruct l0; try done. rewrite shift_loc_0. done. }
@@ -114,8 +114,8 @@ Section product_split.
     iDestruct "Hp1" as %Hp1. iDestruct "H1" as (l) "(EQ & H↦1 & H†1)".
     iDestruct "EQ" as %[=->]. iDestruct "H2" as (v2) "(Hp2 & H2)".
     rewrite /= Hp1. iDestruct "Hp2" as %[=<-]. iDestruct "H2" as (l') "(EQ & H↦2 & H†2)".
-    iDestruct "EQ" as %[=<-]. iExists #l. iSplitR; first done. iExists l. iSplitR; first done.
-    rewrite -freeable_sz_split. iFrame.
+    iDestruct "EQ" as %[=<-]. iExists #l. iSplitR; first done. iExists l.
+    iSplitR; first done. rewrite -freeable_sz_split. iFrame.
     iDestruct "H↦1" as (vl1) "[H↦1 H1]". iDestruct "H↦2" as (vl2) "[H↦2 H2]".
     iExists (vl1 ++ vl2). rewrite heap_mapsto_vec_app. iFrame.
     iAssert (▷ ⌜length vl1 = ty_size ty1⌝)%I with "[#]" as ">EQ".
@@ -271,7 +271,7 @@ Section product_split.
     tctx_extract_hasty E L p' ty [p ◁ own n ty1; p +ₗ #ty1.(ty_size) ◁ own n ty2] T' →
     tctx_extract_hasty E L p' ty ((p ◁ own n $ product2 ty1 ty2) :: T) (T' ++ T) .
   Proof.
-    unfold tctx_extract_hasty. intros ?. apply (tctx_incl_frame_r T [_] (_::_)).
+    rewrite !tctx_extract_hasty_unfold. intros ?. apply (tctx_incl_frame_r T [_] (_::_)).
     by rewrite tctx_split_own_prod2.
   Qed.
 
@@ -280,7 +280,7 @@ Section product_split.
             [p ◁ &uniq{κ}ty1; p +ₗ #ty1.(ty_size) ◁ &uniq{κ}ty2] T' →
     tctx_extract_hasty E L p' ty ((p ◁ &uniq{κ} product2 ty1 ty2) :: T) (T' ++ T) .
   Proof.
-    unfold tctx_extract_hasty=>?. apply (tctx_incl_frame_r T [_] (_::_)).
+    rewrite !tctx_extract_hasty_unfold=>?. apply (tctx_incl_frame_r T [_] (_::_)).
     by rewrite tctx_split_uniq_prod2.
   Qed.
 
@@ -290,7 +290,7 @@ Section product_split.
     tctx_extract_hasty E L p' ty ((p ◁ &shr{κ} product2 ty1 ty2) :: T)
                                  ((p ◁ &shr{κ} product2 ty1 ty2) :: T).
   Proof.
-    unfold tctx_extract_hasty=>?. apply (tctx_incl_frame_r _ [_] [_;_]).
+    rewrite !tctx_extract_hasty_unfold=>?. apply (tctx_incl_frame_r _ [_] [_;_]).
     rewrite {1}copy_tctx_incl. apply (tctx_incl_frame_r _ [_] [_]).
     rewrite tctx_split_shr_prod2 -(contains_tctx_incl _ _ [p' ◁ ty]%TC) //.
     apply contains_skip, contains_nil_l.
@@ -300,7 +300,7 @@ Section product_split.
     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).
   Proof.
-    unfold tctx_extract_hasty=>?. apply (tctx_incl_frame_r T [_] (_::_)).
+    rewrite !tctx_extract_hasty_unfold=>?. apply (tctx_incl_frame_r T [_] (_::_)).
     by rewrite tctx_split_own_prod.
   Qed.
 
@@ -308,7 +308,7 @@ Section product_split.
     tctx_extract_hasty E L p' ty (hasty_ptr_offsets p (uniq_bor κ) tyl 0) T' →
     tctx_extract_hasty E L p' ty ((p ◁ &uniq{κ} Π tyl) :: T) (T' ++ T).
   Proof.
-    unfold tctx_extract_hasty=>?. apply (tctx_incl_frame_r T [_] (_::_)).
+    rewrite !tctx_extract_hasty_unfold=>?. apply (tctx_incl_frame_r T [_] (_::_)).
     by rewrite tctx_split_uniq_prod.
   Qed.
 
@@ -316,7 +316,7 @@ Section product_split.
     tctx_extract_hasty E L p' ty (hasty_ptr_offsets p (shr_bor κ) tyl 0) T' →
     tctx_extract_hasty E L p' ty ((p ◁ &shr{κ} Π tyl) :: T) ((p ◁ &shr{κ} Π tyl) :: T).
   Proof.
-    unfold tctx_extract_hasty=>?. apply (tctx_incl_frame_r _ [_] [_;_]).
+    rewrite !tctx_extract_hasty_unfold=>?. apply (tctx_incl_frame_r _ [_] [_;_]).
     rewrite {1}copy_tctx_incl. apply (tctx_incl_frame_r _ [_] [_]).
     rewrite tctx_split_shr_prod -(contains_tctx_incl _ _ [p' ◁ ty]%TC) //.
     apply contains_skip, contains_nil_l.
@@ -329,7 +329,7 @@ Section product_split.
     tctx_extract_hasty E L (p +ₗ #ty1.(ty_size)) (own n ty2) T2 T3 →
     tctx_extract_hasty E L p (own n (product2 ty1 ty2)) T1 T3.
   Proof.
-    unfold tctx_extract_hasty=>->->.
+    rewrite !tctx_extract_hasty_unfold=>->->.
     apply (tctx_incl_frame_r _ [_;_] [_]), tctx_merge_own_prod2.
   Qed.
 
@@ -338,7 +338,7 @@ Section product_split.
     tctx_extract_hasty E L (p +ₗ #ty1.(ty_size)) (&uniq{κ}ty2) T2 T3 →
     tctx_extract_hasty E L p (&uniq{κ}product2 ty1 ty2) T1 T3.
   Proof.
-    unfold tctx_extract_hasty=>->->.
+    rewrite !tctx_extract_hasty_unfold=>->->.
     apply (tctx_incl_frame_r _ [_;_] [_]), tctx_merge_uniq_prod2.
   Qed.
 
@@ -347,7 +347,7 @@ Section product_split.
     tctx_extract_hasty E L (p +ₗ #ty1.(ty_size)) (&shr{κ}ty2) T2 T3 →
     tctx_extract_hasty E L p (&shr{κ}product2 ty1 ty2) T1 T3.
   Proof.
-    unfold tctx_extract_hasty=>->->.
+    rewrite !tctx_extract_hasty_unfold=>->->.
     apply (tctx_incl_frame_r _ [_;_] [_]), tctx_merge_shr_prod2.
   Qed.
 
@@ -364,10 +364,9 @@ Section product_split.
     extract_tyl E L p ptr tyl 0 T T' →
     tctx_extract_hasty E L p (ptr (Π tyl)) T T'.
   Proof.
-    unfold tctx_extract_hasty=>Hi Htyl.
+    rewrite /extract_tyl !tctx_extract_hasty_unfold=>Hi Htyl.
     etrans. 2:by eapply (tctx_incl_frame_r T' _ [_]). revert T Htyl. clear.
-    generalize 0%nat. induction tyl=>[T n /= -> //|T n /=].
-    unfold tctx_extract_hasty=>-[T'' [-> Htyl]]. f_equiv. auto.
+    generalize 0%nat. induction tyl=>[T n /= -> //|T n /= [T'' [-> Htyl]]]. f_equiv. auto.
   Qed.
 
   Lemma tctx_extract_merge_own_prod E L p n tyl T T' :

theories/typing/programs.v

@@ -102,7 +102,7 @@ Section typing_rules.
       iApply "HC". done.
   Qed.
 
-  Lemma type_let E L T1 T2 (T : tctx) C xb e e' :
+  Lemma type_let' E L T1 T2 (T : tctx) C xb e e' :
     Closed (xb :b: []) e' →
     typed_instruction E L T1 e T2 →
     (∀ v : val, typed_body E L C (T2 v ++ T) (subst' xb v e')) →
@@ -116,16 +116,21 @@ Section typing_rules.
     rewrite tctx_interp_app. by iFrame.
   Qed.
 
-  Lemma type_let' E L T T' T1 T2 C xb e e' :
+  Lemma type_let E L T T' T1 T2 C xb e e' :
     Closed (xb :b: []) e' →
     typed_instruction E L T1 e T2 →
     tctx_extract_ctx E L T1 T T' →
     (∀ v : val, typed_body E L C (T2 v ++ T') (subst' xb v e')) →
     typed_body E L C T (let: xb := e in e').
-  Proof.
-    intros ?? HT ?. unfold tctx_extract_ctx in HT. rewrite ->HT.
-    by eapply type_let.
-  Qed.
+  Proof. rewrite tctx_extract_ctx_unfold. intros ?? -> ?. by eapply type_let'. Qed.
+
+  Lemma type_seq E L T T' T1 T2 C e e' :
+    Closed [] e' →
+    typed_instruction E L T1 e (λ _, T2) →
+    tctx_extract_ctx E L T1 T T' →
+    (typed_body E L C (T2 ++ T') e') →
+    typed_body E L C T (e ;; e').
+  Proof. intros. by eapply type_let. Qed.
 
   Lemma typed_newlft E L C T κs e :
     Closed [] e →
@@ -154,7 +159,7 @@ Section typing_rules.
     iApply (Hub with "[] HT"). simpl in *. subst κ. rewrite -lft_dead_or. auto.
   Qed.
 
-  Lemma type_assign {E L} ty ty1 ty1' p1 p2 :
+  Lemma type_assign_instr {E L} ty ty1 ty1' p1 p2 :
     typed_write E L ty1 ty ty1' →
     typed_instruction E L [p1 ◁ ty1; p2 ◁ ty] (p1 <- p2) (λ _, [p1 ◁ ty1']%TC).
   Proof.
@@ -173,7 +178,15 @@ Section typing_rules.
     rewrite tctx_interp_singleton tctx_hasty_val' //.
   Qed.
 
-  Lemma type_deref {E L} ty ty1 ty1' p :
+  Lemma type_assign {E L} ty1 C T T' ty ty1' p1 p2 e:
+    Closed [] e →
+    tctx_extract_ctx E L [p1 ◁ ty1; p2 ◁ ty] T T' →
+    typed_write E L ty1 ty ty1' →
+    typed_body E L C ((p1 ◁ ty1') :: T') e →
+    typed_body E L C T (p1 <- p2 ;; e).
+  Proof. intros. eapply type_seq; [done |by apply type_assign_instr|done|done]. Qed.
+
+  Lemma type_deref_instr {E L} ty ty1 ty1' p :
     ty.(ty_size) = 1%nat → typed_read E L ty1 ty ty1' →
     typed_instruction E L [p ◁ ty1] (!p) (λ v, [p ◁ ty1'; v ◁ ty]%TC).
   Proof.
@@ -191,8 +204,19 @@ Section typing_rules.
     by iFrame.
   Qed.
 
-  Lemma type_memcpy_iris E qE L qL tid ty ty1 ty1' ty2 ty2' n p1 p2 :
-    ty.(ty_size) = n →
+  Lemma type_deref {E L} ty1 C T T' ty ty1' x p e:
+    Closed (x :b: []) e →
+    tctx_extract_hasty E L p ty1 T T' →
+    typed_read E L ty1 ty ty1' →
+    ty.(ty_size) = 1%nat →
+    (∀ (v : val), typed_body E L C ((p ◁ ty1') :: (v ◁ ty) :: T') (subst' x v e)) →
+    typed_body E L C T (let: x := !p in e).
+  Proof.
+    intros. eapply type_let; [done|by apply type_deref_instr|solve_typing|by simpl].
+  Qed.
+
+  Lemma type_memcpy_iris E qE L qL tid ty ty1 ty1' ty2 ty2' (n : Z) p1 p2 :
+    Z.of_nat (ty.(ty_size)) = n →
     typed_write E L ty1 ty ty1' -∗ typed_read E L ty2 ty ty2' -∗
     {{{ heap_ctx ∗ lft_ctx ∗ na_own tid ⊤ ∗ elctx_interp E qE ∗ llctx_interp L qL ∗
         tctx_elt_interp tid (p1 ◁ ty1) ∗ tctx_elt_interp tid (p2 ◁ ty2) }}}
@@ -200,7 +224,8 @@ Section typing_rules.
     {{{ RET #(); na_own tid ⊤ ∗ elctx_interp E qE ∗ llctx_interp L qL ∗
                  tctx_elt_interp tid (p1 ◁ ty1') ∗ tctx_elt_interp tid (p2 ◁ ty2') }}}.
   Proof.
-    iIntros (Hsz) "#Hwrt #Hread !#". iIntros (Φ) "(#HEAP & #LFT & Htl & [HE1 HE2] & [HL1 HL2] & [Hp1 Hp2]) HΦ".
+    iIntros (<-) "#Hwrt #Hread !#".
+    iIntros (Φ) "(#HEAP & #LFT & Htl & [HE1 HE2] & [HL1 HL2] & [Hp1 Hp2]) HΦ".
     wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "% Hown1".
     wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "% Hown2".
     iMod ("Hwrt" with "* [] LFT HE1 HL1 Hown1")
@@ -216,8 +241,9 @@ Section typing_rules.
     iMod ("Hcl2" with "Hl2") as "($ & $ & $ & $)". done.
   Qed.
 
-  Lemma type_memcpy {E L} ty ty1 ty1' ty2 ty2' n p1 p2 :
-    ty.(ty_size) = n → typed_write E L ty1 ty ty1' → typed_read E L ty2 ty ty2' →
+  Lemma type_memcpy_instr {E L} ty ty1 ty1' ty2 ty2' (n : Z) p1 p2 :
+    Z.of_nat (ty.(ty_size)) = n →
+    typed_write E L ty1 ty ty1' → typed_read E L ty2 ty ty2' →
     typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2] (p1 <⋯ !{n}p2)
                       (λ _, [p1 ◁ ty1'; p2 ◁ ty2']%TC).
   Proof.
@@ -229,4 +255,16 @@ Section typing_rules.
     { by rewrite tctx_interp_cons tctx_interp_singleton. }
     rewrite tctx_interp_cons tctx_interp_singleton. auto.
   Qed.
+
+  Lemma type_memcpy {E L} ty1 ty2 (n : Z) C T T' ty ty1' ty2' p1 p2 e:
+    Closed [] e →
+    tctx_extract_ctx E L [p1 ◁ ty1; p2 ◁ ty2] T T' →
+    typed_write E L ty1 ty ty1' →
+    typed_read E L ty2 ty ty2' →
+    Z.of_nat (ty.(ty_size)) = n →
+    typed_body E L C ((p1 ◁ ty1') :: (p2 ◁ ty2') :: T') e →
+    typed_body E L C T (p1 <⋯ !{n}p2;; e).
+  Proof.
+    intros. eapply type_seq; [done|by eapply type_memcpy_instr|done|by simpl].
+  Qed.
 End typing_rules.

theories/typing/tests/get_x.v

@@ -17,22 +17,14 @@ Section get_x.
         (fn (λ α, [☀α])%EL (λ α, [# own 1 (&uniq{α}Π[int; int])])
             (λ α, own 1 (&shr{α} int))).
   Proof.
-    apply type_fn; try apply _. move=> /= α ret args. inv_vec args=>p args.
-    inv_vec args. simpl_subst.
+    apply type_fn; try apply _. move=> /= α ret p. inv_vec p=>p. simpl_subst.
 
-    eapply type_let'.
-    { apply _. }
-    { by eapply (type_deref (&uniq{α} _)), read_own_move. }
-    { solve_typing. }
-    intros p'. simpl_subst.
+    eapply type_deref; try solve_typing. by apply read_own_move. done.
+    intros p'; simpl_subst.
 
     eapply (type_letalloc_1 (&shr{α}int)); (try solve_typing)=>r. simpl_subst.
 
-    eapply type_let'.
-    { apply _. }
-    { by eapply (type_delete (uninit 1) 1). }
-    { solve_typing. }
-    move=> /= _.
+    eapply type_delete; try solve_typing.
 
     eapply type_jump with (args := [r]); solve_typing.
   Qed.

theories/typing/type_context.v

@@ -253,6 +253,8 @@ Section type_context.
   Definition tctx_extract_hasty E L p ty T T' : Prop :=
     tctx_incl E L T ((p ◁ ty)::T').
   Global Arguments tctx_extract_hasty _%EL _%LL _%E _%T _%TC _%TC.
+  Definition tctx_extract_hasty_unfold :
+    tctx_extract_hasty = λ E L p ty T T', tctx_incl E L T ((p ◁ ty)::T') := eq_refl.
   Lemma tctx_extract_hasty_cons E L p ty T T' x :
     tctx_extract_hasty E L p ty T T' →
     tctx_extract_hasty E L p ty (x::T) (x::T').
@@ -287,6 +289,8 @@ Section type_context.
 
   Definition tctx_extract_ctx E L T T1 T2 : Prop :=
     tctx_incl E L T1 (T++T2).
+  Definition tctx_extract_ctx_unfold :
+    tctx_extract_ctx = λ E L T T1 T2, tctx_incl E L T1 (T++T2) := eq_refl.
   Global Arguments tctx_extract_ctx _%EL _%LL _%TC _%TC _%TC.
   Lemma tctx_extract_ctx_nil E L T:
     tctx_extract_ctx E L [] T T.
@@ -338,6 +342,7 @@ Section type_context.
   Qed.
 End type_context.
 
+Global Opaque tctx_extract_ctx tctx_extract_hasty tctx_extract_blocked.
 Hint Resolve tctx_extract_hasty_here_copy : lrust_typing.
 Hint Resolve tctx_extract_hasty_here | 50 : lrust_typing.
 Hint Resolve tctx_extract_hasty_cons | 100 : lrust_typing.

theories/typing/type_sum.v

@@ -7,8 +7,7 @@ Set Default Proof Using "Type".
 Section case.
   Context `{typeG Σ}.
 
-  (* FIXME : the doc does not give [p +ₗ #(S (ty.(ty_size))) ◁ ...]. *)
-  Lemma type_case_own E L C T p n tyl el :
+  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) ::
          (p +ₗ #(S (ty.(ty_size))) ◁
@@ -49,7 +48,7 @@ Section case.
       iFrame. iExists i, vl', vl''. rewrite /= app_length nth_lookup EQty. auto.
   Qed.
 
-  Lemma type_case_own' E L C T T' p n tyl el :
+  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' →
     Forall2 (λ ty e,
       typed_body E L C ((p +ₗ #0 ◁ own n (uninit 1)) :: (p +ₗ #1 ◁ own n ty) ::
@@ -57,9 +56,9 @@ Section case.
             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 T (case: !p of el).
-  Proof. unfold tctx_extract_hasty. intros ->. apply type_case_own. Qed.
+  Proof. rewrite tctx_extract_hasty_unfold=>->. apply type_case_own'. Qed.
 
-  Lemma type_case_uniq E L C T p κ tyl el :
+  Lemma type_case_uniq' E L C T p κ tyl el :
     lctx_lft_alive E L κ →
     Forall2 (λ ty e,
       typed_body E L C ((p +ₗ #1 ◁ &uniq{κ}ty) :: T) e ∨
@@ -107,16 +106,16 @@ Section case.
       iExists _, _. iFrame. iSplit. done. iSplit; iIntros "!>!#$".
   Qed.
 
-  Lemma type_case_uniq' E L C T T' p κ tyl el :
+  Lemma type_case_uniq E L C T T' p κ tyl el :
     tctx_extract_hasty E L p (&uniq{κ}sum tyl) T T' →
     lctx_lft_alive E L κ →
     Forall2 (λ ty e,
       typed_body E L C ((p +ₗ #1 ◁ &uniq{κ}ty) :: T') e ∨
       typed_body E L C ((p ◁ &uniq{κ}sum tyl) :: T') e) tyl el →
     typed_body E L C T (case: !p of el).
-  Proof. unfold tctx_extract_hasty. intros ->. apply type_case_uniq. Qed.
+  Proof. rewrite tctx_extract_hasty_unfold=>->. apply type_case_uniq'. Qed.
 
-  Lemma type_case_shr E L C T p κ tyl el:
+  Lemma type_case_shr' E L C T p κ tyl el:
     lctx_lft_alive E L κ →
     Forall2 (λ ty e,
       typed_body E L C ((p +ₗ #1 ◁ &shr{κ}ty) :: T) e ∨
@@ -142,14 +141,14 @@ Section case.
     - iExists _. iSplit. done. iExists i. rewrite nth_lookup EQty /=. auto.
   Qed.
 
-  Lemma type_case_shr' E L C T p κ tyl el :
+  Lemma type_case_shr E L C T p κ tyl el :
     (p ◁ &shr{κ}sum tyl)%TC ∈ T →
     lctx_lft_alive E L κ →
     Forall2 (λ ty e, typed_body E L C ((p +ₗ #1 ◁ &shr{κ}ty) :: T) e) tyl el →
     typed_body E L C T (case: !p of el).
   Proof.
     intros. rewrite ->copy_elem_of_tctx_incl; last done; last apply _.
-    apply type_case_shr; first done. eapply Forall2_impl; first done. auto.
+    apply type_case_shr'; first done. eapply Forall2_impl; first done. auto.
   Qed.
 
   Lemma type_sum_assign {E L} (i : nat) tyl ty1 ty2 ty p1 p2 :

theories/typing/uniq_bor.v

@@ -195,7 +195,7 @@ Section typing.
     tctx_extract_hasty E L p (&shr{κ}ty) ((p ◁ &uniq{κ'}ty')::T)
                        ((p ◁ &shr{κ}ty')::(p ◁{κ} &uniq{κ'}ty')::T).
   Proof.
-    intros. apply (tctx_incl_frame_r _ [_] [_;_;_]).
+    rewrite tctx_extract_hasty_unfold=>???. apply (tctx_incl_frame_r _ [_] [_;_;_]).
     rewrite tctx_reborrow_uniq //. apply (tctx_incl_frame_r _ [_] [_;_]).
     rewrite tctx_share // {1}copy_tctx_incl.
     by apply (tctx_incl_frame_r _ [_] [_]), subtype_tctx_incl, shr_mono'.
@@ -206,7 +206,7 @@ Section typing.
     tctx_extract_hasty E L p (&shr{κ}ty) ((p ◁ &uniq{κ}ty')::T)
                                          ((p ◁ &shr{κ}ty')::T).
   Proof.
-    intros. apply (tctx_incl_frame_r _ [_] [_;_]).
+    rewrite tctx_extract_hasty_unfold=>??. apply (tctx_incl_frame_r _ [_] [_;_]).
     rewrite tctx_share // {1}copy_tctx_incl.
     by apply (tctx_incl_frame_r _ [_] [_]), subtype_tctx_incl, shr_mono'.
   Qed.
@@ -216,7 +216,8 @@ Section typing.
     tctx_extract_hasty E L p (&uniq{κ'}ty) ((p ◁ &uniq{κ}ty')::T)
                        ((p ◁{κ'} &uniq{κ}ty')::T).
   Proof.
-    intros. apply (tctx_incl_frame_r _ [_] [_;_]). rewrite tctx_reborrow_uniq //.
+    rewrite tctx_extract_hasty_unfold=>??.
+    apply (tctx_incl_frame_r _ [_] [_;_]). rewrite tctx_reborrow_uniq //.
     by apply (tctx_incl_frame_r _ [_] [_]), subtype_tctx_incl, uniq_mono'.
   Qed.