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

_CoqProject

@@ -45,3 +45,5 @@ theories/typing/fixpoint.v
 theories/typing/type_sum.v
 theories/typing/tests/get_x.v
 theories/typing/tests/rebor.v
+theories/typing/tests/unbox.v
+theories/typing/tests/init_prod.v

theories/typing/borrow.v

@@ -46,11 +46,12 @@ Section borrow.
     apply (tctx_incl_frame_r _ [_] [_;_]). rewrite ->tctx_share; solve_typing.
   Qed.
 
-  Lemma type_deref_uniq_own {E L} κ p n ty :
+  Lemma type_deref_uniq_own_instr {E L} κ p n ty :
     lctx_lft_alive E L κ →
     typed_instruction_ty E L [p ◁ &uniq{κ} own n ty] (!p) (&uniq{κ} ty).
   Proof.
-    iIntros (Hκ) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
+    iIntros (Hκ) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp".
+    rewrite tctx_interp_singleton.
     iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
     wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
     iDestruct "Hown" as (l P) "[[Heq #HPiff] HP]". iDestruct "Heq" as %[=->].
@@ -69,11 +70,22 @@ Section borrow.
       rewrite -heap_mapsto_vec_singleton. iFrame. iExists _. by iFrame.
   Qed.
 
-  Lemma type_deref_shr_own {E L} κ p n ty :
+  Lemma type_deref_uniq_own {E L} κ x p e n ty C T T' :
+    Closed (x :b: []) e →
+    tctx_extract_hasty E L p (&uniq{κ} own n ty) T T' →
+    lctx_lft_alive E L κ →
+    (∀ (v:val), typed_body E L C ((v ◁ &uniq{κ} 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_uniq_own_instr|solve_typing|done].
+  Qed.
+
+  Lemma type_deref_shr_own_instr {E L} κ p n ty :
     lctx_lft_alive E L κ →
     typed_instruction_ty E L [p ◁ &shr{κ} own n ty] (!p) (&shr{κ} ty).
   Proof.
-    iIntros (Hκ) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
+    iIntros (Hκ) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp".
+    rewrite tctx_interp_singleton.
     iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first set_solver.
     wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
     iDestruct "Hown" as (l) "[Heq #H↦]". iDestruct "Heq" as %[=->].
@@ -81,16 +93,28 @@ Section borrow.
     iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
     iApply (wp_fupd_step _ (_∖_) with "[Hown Htok2]"); try done.
     - iApply ("Hown" with "* [%] Htok2"). set_solver+.
-    - wp_read. iIntros "!>[#Hshr Htok2]". iMod ("Hclose'" with "[H↦]") as "Htok1"; first by auto.
+    - wp_read. iIntros "!>[#Hshr Htok2]".
+      iMod ("Hclose'" with "[H↦]") as "Htok1"; first by auto.
       iMod ("Hclose" with "[Htok1 Htok2]") as "($ & $)"; first by iFrame.
       rewrite tctx_interp_singleton tctx_hasty_val' //. iExists _. auto.
   Qed.
 
-  Lemma type_deref_uniq_uniq {E L} κ κ' p ty :
+  Lemma type_deref_shr_own {E L} κ x p e n ty C T T' :
+    Closed (x :b: []) e →
+    tctx_extract_hasty E L p (&shr{κ} own n ty) T T' →
+    lctx_lft_alive E L κ →
+    (∀ (v:val), typed_body E L C ((v ◁ &shr{κ} 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_shr_own_instr|solve_typing|done].
+  Qed.
+
+  Lemma type_deref_uniq_uniq_instr {E L} κ κ' p ty :
     lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
     typed_instruction_ty E L [p ◁ &uniq{κ} &uniq{κ'} ty] (!p) (&uniq{κ} ty).
   Proof.
-    iIntros (Hκ Hincl) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
+    iIntros (Hκ Hincl) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp".
+    rewrite tctx_interp_singleton.
     iPoseProof (Hincl with "[#] [#]") as "Hincl".
     { by iApply elctx_interp_persist. } { by iApply llctx_interp_persist. }
     iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
@@ -116,7 +140,17 @@ Section borrow.
     iApply (lft_incl_glb with "Hincl"). iApply lft_incl_refl.
   Qed.
 
-  Lemma type_deref_shr_uniq {E L} κ κ' p ty :
+  Lemma type_deref_uniq_uniq {E L} κ κ' x p e ty C T T' :
+    Closed (x :b: []) e →
+    tctx_extract_hasty E L p (&uniq{κ} &uniq{κ'} ty) T T' →
+    lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
+    (∀ (v:val), typed_body E L C ((v ◁ &uniq{κ} 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_uniq_uniq_instr|solve_typing|done].
+  Qed.
+
+  Lemma type_deref_shr_uniq_instr {E L} κ κ' p ty :
     lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
     typed_instruction_ty E L [p ◁ &shr{κ} &uniq{κ'} ty] (!p) (&shr{κ} ty).
   Proof.
@@ -139,6 +173,16 @@ Section borrow.
       rewrite tctx_interp_singleton tctx_hasty_val' //.
       iExists _. iSplitR. done. by iApply (ty_shr_mono with "LFT Hincl' Hshr").
   Qed.
+
+  Lemma type_deref_shr_uniq {E L} κ κ' x p e ty C T T' :
+    Closed (x :b: []) e →
+    tctx_extract_hasty E L p (&shr{κ} &uniq{κ'} ty) T T' →
+    lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
+    (∀ (v:val), typed_body E L C ((v ◁ &shr{κ} 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_shr_uniq_instr|solve_typing|done].
+  Qed.
 End borrow.
 
 Hint Resolve tctx_extract_hasty_borrow tctx_extract_hasty_borrow_share

theories/typing/own.v

@@ -210,6 +210,21 @@ Section typing.
     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_new_subtype ty E L C T x (n : Z) e :
+    Closed (x :b: []) e →
+    0 ≤ n →
+    let n' := Z.to_nat n in
+    subtype E L (uninit n') ty →
+    (∀ (v : val), typed_body E L C ((v ◁ own n' ty) :: T) (subst' x v e)) →
+    typed_body E L C T (let: x := new [ #n ] in e).
+  Proof.
+    intros ???? Htyp. eapply type_let. done. by apply type_new_instr. solve_typing.
+    iIntros (v). iApply typed_body_mono; [done| |done|].
+    (* FIXME : why can't we iApply Htyp? *)
+    2:by iDestruct (Htyp v) as "$".
+    by apply (tctx_incl_frame_r _ [_] [_]), subtype_tctx_incl, own_mono.
+  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 (λ _, []).

theories/typing/product_split.v

@@ -401,4 +401,6 @@ Hint Extern 0
      (tctx_extract_hasty _ _ _ _ (hasty_ptr_offsets _ _ _ _) _) =>
         cbn[hasty_ptr_offsets].
 
+Hint Extern 0 (tctx_extract_hasty _ _ _ _ (_ ++ _) _) => cbn[app].
+
 Hint Unfold extract_tyl : lrust_typing.

theories/typing/tests/init_prod.v

+From lrust.lifetime Require Import definitions.
+From lrust.lang Require Import new_delete.
+From lrust.typing Require Import programs product product_split own uniq_bor
+                    shr_bor int function lft_contexts uninit cont borrow.
+Set Default Proof Using "Type".
+
+Section rebor.
+  Context `{typeG Σ}.
+
+  Definition init_prod :=
+    (funrec: <> ["x"; "y"] :=
+       let: "x'" := !"x" in let: "y'" := !"y" in
+       let: "r" := new [ #2] in
+       "r" +ₗ #0 <- "x'";; "r" +ₗ #1 <- "y'";;
+       delete [ #1; "x"] ;; delete [ #1; "y"] ;; "return" ["r":expr])%E.
+
+  Lemma init_prod_type :
+    typed_instruction_ty [] [] [] init_prod
+        (fn (λ _, []) (λ _, [# own 1 int; own 1 int])
+            (λ (_ : ()), own 2 (Π[int;int]))).
+  Proof.
+    apply type_fn; try apply _. move=> /= [] ret p. inv_vec p=>x y. simpl_subst.
+    eapply type_deref; try solve_typing; [apply read_own_move|done|]=>x'. simpl_subst.
+    eapply type_deref; try solve_typing; [apply read_own_move|done|]=>y'. simpl_subst.
+    eapply (type_new_subtype (Π[uninit 1; uninit 1])); [apply _|done| |].
+      { apply (uninit_product_subtype [] [] [1;1]%nat). }
+      intros r. simpl_subst. unfold Z.to_nat, Pos.to_nat; simpl.
+    eapply (type_assign (own 2 (uninit 1))); try solve_typing. by apply write_own.
+    eapply type_assign; try solve_typing. by apply write_own.
+    eapply type_delete; try solve_typing.
+    eapply type_delete; try solve_typing.
+    eapply (type_jump [_]); solve_typing.
+  Qed.
+End rebor.

theories/typing/tests/unbox.v

+From lrust.lifetime Require Import definitions.
+From lrust.lang Require Import new_delete.
+From lrust.typing Require Import programs product product_split own uniq_bor
+                    shr_bor int function lft_contexts uninit cont borrow.
+Set Default Proof Using "Type".
+
+Section unbox.
+  Context `{typeG Σ}.
+
+  Definition unbox :=
+    (funrec: <> ["b"] :=
+       let: "b'" := !"b" in let: "bx" := !"b'" in
+       letalloc: "r" := "bx" +ₗ #0 in
+       delete [ #1; "b"] ;; "return" ["r":expr])%E.
+
+  Lemma ubox_type :
+    typed_instruction_ty [] [] [] unbox
+        (fn (λ α, [☀α])%EL (λ α, [# own 1 (&uniq{α}own 2 (Π[int; int]))])
+            (λ α, own 1 (&uniq{α} int))).
+  Proof.
+    apply type_fn; try apply _. move=> /= α ret b. inv_vec b=>b. simpl_subst.
+    eapply type_deref; try solve_typing. by apply read_own_move. done.
+      intros b'; simpl_subst.
+    eapply type_deref_uniq_own; (try solve_typing)=>bx; simpl_subst.
+    eapply (type_letalloc_1 (&uniq{α}int)); (try solve_typing)=>r. simpl_subst.
+    eapply type_delete; try solve_typing.
+    eapply (type_jump [_]); solve_typing.
+  Qed.
+End unbox.

theories/typing/type_context.v

@@ -363,5 +363,5 @@ Hint Resolve tctx_extract_blocked_here tctx_extract_blocked_cons
    the environment if the type is copy. But due to a bug in Coq, we
    cannot enforce this using [Hint Resolve]. Cf:
        https://coq.inria.fr/bugs/show_bug.cgi?id=5299 *)
-Hint Extern 2 (tctx_extract_hasty _ _ ?p _ ((?p ◁ _) :: _) _) =>
+Hint Extern 2 (tctx_extract_hasty _ _ _ _ ((_ ◁ _) :: _) _) =>
   eapply tctx_extract_hasty_here_eq.