prove writing to Cell; tune some notation

theories/lifetime/frac_borrow.v

@@ -11,7 +11,7 @@ Definition frac_bor `{invG Σ, lftG Σ, frac_borG Σ} κ (Φ : Qp → iProp Σ)
   (∃ γ κ', κ ⊑ κ' ∗ &shr{κ'} ∃ q, Φ q ∗ own γ q ∗
                        (⌜q = 1%Qp⌝ ∨ ∃ q', ⌜(q + q' = 1)%Qp⌝ ∗ q'.[κ']))%I.
 Notation "&frac{ κ } P" := (frac_bor κ P)
-  (format "&frac{ κ } P", at level 20, right associativity) : uPred_scope.
+  (format "&frac{ κ }  P", at level 20, right associativity) : uPred_scope.
 
 Section frac_bor.
   Context `{invG Σ, lftG Σ, frac_borG Σ}.

theories/lifetime/na_borrow.v

@@ -8,7 +8,7 @@ Definition na_bor `{invG Σ, lftG Σ, na_invG Σ}
   (∃ i, &{κ,i}P ∗ na_inv tid N (idx_bor_own 1 i))%I.
 
 Notation "&na{ κ , tid , N } P" := (na_bor κ tid N P)
-  (format "&na{ κ , tid , N } P", at level 20, right associativity) : uPred_scope.
+  (format "&na{ κ , tid , N }  P", at level 20, right associativity) : uPred_scope.
 
 Section na_bor.
   Context `{invG Σ, lftG Σ, na_invG Σ}

theories/lifetime/shr_borrow.v

@@ -7,7 +7,7 @@ Set Default Proof Using "Type".
 Definition shr_bor `{invG Σ, lftG Σ} κ (P : iProp Σ) :=
   (∃ i, &{κ,i}P ∗ inv lftN (∃ q, idx_bor_own q i))%I.
 Notation "&shr{ κ } P" := (shr_bor κ P)
-  (format "&shr{ κ } P", at level 20, right associativity) : uPred_scope.
+  (format "&shr{ κ }  P", at level 20, right associativity) : uPred_scope.
 
 Section shared_bors.
   Context `{invG Σ, lftG Σ} (P : iProp Σ).

theories/typing/own.v

@@ -151,6 +151,8 @@ Section own.
   Qed.
 End own.
 
+Notation box ty := (own ty.(ty_size) ty).
+
 Section typing.
   Context `{typeG Σ}.
 
@@ -206,7 +208,7 @@ Section typing.
     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 ((v ◁ box (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.
 
@@ -227,7 +229,7 @@ Section typing.
 
   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 (λ _, []).
+    typed_instruction E L [p ◁ box 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".

theories/typing/shr_bor.v

@@ -47,7 +47,7 @@ Section shr_bor.
 End shr_bor.
 
 Notation "&shr{ κ } ty" := (shr_bor κ ty)
-  (format "&shr{ κ } ty", at level 20, right associativity) : lrust_type_scope.
+  (format "&shr{ κ }  ty", at level 20, right associativity) : lrust_type_scope.
 
 Section typing.
   Context `{typeG Σ}.

theories/typing/tests/get_x.v

@@ -11,7 +11,7 @@ Section get_x.
     funrec: <> ["p"] :=
        let: "p'" := !"p" in
        letalloc: "r" := "p'" +ₗ #0 in
-       delete [ #1; "p"] ;; "return" ["r":expr].
+       delete [ #1; "p"] ;; "return" ["r"].
 
   Lemma get_x_type :
     typed_instruction_ty [] [] [] get_x

theories/typing/tests/init_prod.v

@@ -12,7 +12,7 @@ Section rebor.
        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].
+       delete [ #1; "x"] ;; delete [ #1; "y"] ;; "return" ["r"].
 
   Lemma init_prod_type :
     typed_instruction_ty [] [] [] init_prod

theories/typing/tests/rebor.v

@@ -16,7 +16,7 @@ Section rebor.
        let: "y'" := !"y" in
        letalloc: "r" := "y'" in
        Endlft ;; delete [ #2; "t1"] ;; delete [ #2; "t2"] ;;
-                 delete [ #1; "x"] ;; "return" ["r":expr].
+                 delete [ #1; "x"] ;; "return" ["r"].
 
   Lemma rebor_type :
     typed_instruction_ty [] [] [] rebor

theories/typing/tests/unbox.v

@@ -11,7 +11,7 @@ Section unbox.
     funrec: <> ["b"] :=
        let: "b'" := !"b" in let: "bx" := !"b'" in
        letalloc: "r" := "bx" +ₗ #0 in
-       delete [ #1; "b"] ;; "return" ["r":expr].
+       delete [ #1; "b"] ;; "return" ["r"].
 
   Lemma ubox_type :
     typed_instruction_ty [] [] [] unbox
@@ -20,7 +20,7 @@ Section unbox.
   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.
+    intros b'; simpl_subst.
     eapply type_deref_uniq_own; (try solve_typing)=>bx; simpl_subst.
     eapply type_letalloc_1; (try solve_typing)=>r. simpl_subst.
     eapply type_delete; try solve_typing.

theories/typing/uninit.v

@@ -64,6 +64,10 @@ Section uninit.
     subtype E L (Π(uninit <$> ns)) (uninit (foldr plus 0%nat ns)).
   Proof. apply uninit_product_eqtype. Qed.
 
+  Lemma uninit_unit E L :
+    eqtype E L unit (uninit 0%nat).
+  Proof. apply (uninit_product_eqtype _ _ []). Qed.
+
   Lemma uninit_own n tid vl :
     (uninit n).(ty_own) tid vl ⊣⊢ ⌜length vl = n⌝.
   Proof.

theories/typing/uniq_bor.v

@@ -136,7 +136,7 @@ Section uniq_bor.
 End uniq_bor.
 
 Notation "&uniq{ κ } ty" := (uniq_bor κ ty)
-  (format "&uniq{ κ } ty", at level 20, right associativity) : lrust_type_scope.
+  (format "&uniq{ κ }  ty", at level 20, right associativity) : lrust_type_scope.
 
 Section typing.
   Context `{typeG Σ}.

theories/typing/unsafe/cell.v

 From iris.proofmode Require Import tactics.
+From iris.base_logic Require Import big_op.
+From lrust.lang Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Export type.
-From lrust.typing Require Import type_context programs.
+From lrust.typing Require Import type_context programs shr_bor own function product uninit cont.
 Set Default Proof Using "Type".
 
 Section cell.
@@ -56,6 +58,8 @@ End cell.
 Section typing.
   Context `{typeG Σ}.
 
+  (* All of these are of course actual code in Rust, but somehow this is more fun. *)
+
   (* Constructing a cell is a coercion. *)
   Lemma tctx_mk_cell E L ty p :
     tctx_incl E L [p ◁ ty] [p ◁ cell ty].
@@ -69,6 +73,61 @@ Section typing.
   Proof.
     iIntros (???) "#LFT $ $ Hty". rewrite !tctx_interp_singleton /=. done.
   Qed.
-  
-  (* TODO: get, set; potentially more operations? *)
+
+  Lemma read_cell E L κ ty :
+    Copy ty → lctx_lft_alive E L κ →
+    typed_read E L (&shr{κ} cell ty) ty (&shr{κ} cell ty).
+  Proof. intros ??. exact: read_shr. Qed. 
+
+  (* Writing actually needs code; typed_write can't have thread tokens. *)
+  Definition cell_write ty : val :=
+    funrec: <> ["c"; "x"] :=
+       let: "c'" := !"c" in
+       "c'" <⋯ !{ty.(ty_size)} "x";;
+       let: "r" := new [ #0 ] in
+       delete [ #1; "c"] ;; delete [ #ty.(ty_size); "x"] ;; "return" ["r"].
+
+  Lemma cell_write_type ty :
+    typed_instruction_ty [] [] [] (cell_write ty)
+        (fn (λ α, [☀α])%EL (λ α, [# box (&shr{α} cell ty); box ty])
+            (λ α, box unit)).
+  Proof.
+    apply type_fn; try apply _. move=> /= α ret arg. inv_vec arg=>c x. simpl_subst.
+    eapply type_deref; try solve_typing. by apply read_own_move. done.
+    intros c'. simpl_subst.
+    eapply type_let with (T1 := [c' ◁ _; x ◁ _]%TC)
+                         (T2 := λ _, [c' ◁ &shr{α} cell ty;
+                                      x ◁ box (uninit ty.(ty_size))]%TC); try solve_typing; [|].
+    { (* The core of the proof: Showing that the assignment is safe. *)
+      iAlways. iIntros (tid qE) "#HEAP #LFT Htl HE $".
+      rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+      iIntros "[Hc' Hx]". rewrite {1}/elctx_interp big_opL_singleton /=.
+      iDestruct "Hc'" as (l) "[EQ #Hshr]". iDestruct "EQ" as %[=->].
+      iDestruct "Hx" as (l') "[EQ [Hown >H†]]". iDestruct "EQ" as %[=->].
+      iDestruct "Hown" as (vl') "[>H↦' Hown']".
+      iMod (na_bor_acc with "LFT Hshr HE Htl") as "(Hown & Htl & Hclose)"; [solve_ndisj..|].
+      iDestruct "Hown" as (vl) "[>H↦ Hown]".
+      iAssert (▷ ⌜length vl = ty_size ty⌝)%I with "[#]" as ">%".
+      { iNext. by iApply ty_size_eq. }
+      iAssert (▷ ⌜length vl' = ty_size ty⌝)%I with "[#]" as ">%".
+      { iNext. by iApply ty_size_eq. }
+      iApply wp_fupd. iApply (wp_memcpy with "[$HEAP $H↦ $H↦']"); [done..|].
+      iNext. iIntros "[H↦ H↦']". rewrite {1}/elctx_interp big_opL_singleton /=.
+      iMod ("Hclose" with "[H↦ Hown'] Htl") as "[$ $]".
+      { iExists vl'. by iFrame. }
+      rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //.
+      iSplitR; iModIntro.
+      - iExists _. iSplit; done.
+      - iExists _. iSplit; first done. iFrame. iExists _. iFrame.
+        rewrite uninit_own. auto. }
+    intros v. simpl_subst. clear v.
+    eapply (type_new_subtype unit); try solve_typing. try done.
+    { apply uninit_unit. }
+    intros r. simpl_subst.
+    eapply type_delete; [solve_typing..|].
+    eapply type_delete; [solve_typing..|].
+    eapply (type_jump [_]); solve_typing.
+  Qed.
+
+  (* TODO: potentially more operations? *)
 End typing.