From 62785d6153fbd3790de06383bebbe7cde8094419 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 10 Jan 2017 16:42:53 +0100
Subject: [PATCH] prove writing to Cell; tune some notation
---
theories/lifetime/frac_borrow.v | 2 +-
theories/lifetime/na_borrow.v | 2 +-
theories/lifetime/shr_borrow.v | 2 +-
theories/typing/own.v | 6 ++-
theories/typing/shr_bor.v | 2 +-
theories/typing/tests/get_x.v | 2 +-
theories/typing/tests/init_prod.v | 2 +-
theories/typing/tests/rebor.v | 2 +-
theories/typing/tests/unbox.v | 4 +-
theories/typing/uninit.v | 4 ++
theories/typing/uniq_bor.v | 2 +-
theories/typing/unsafe/cell.v | 65 +++++++++++++++++++++++++++++--
12 files changed, 80 insertions(+), 15 deletions(-)
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index e491ea98..c07510ec 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/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 Σ}.
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index 4be5c06e..b3f1168e 100644
--- a/theories/lifetime/na_borrow.v
+++ b/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 Σ}
diff --git a/theories/lifetime/shr_borrow.v b/theories/lifetime/shr_borrow.v
index 2e197577..56a23e07 100644
--- a/theories/lifetime/shr_borrow.v
+++ b/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 Σ).
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 8ce49d9d..c63a3aa6 100644
--- a/theories/typing/own.v
+++ b/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".
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 9aef143a..aa617b18 100644
--- a/theories/typing/shr_bor.v
+++ b/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 Σ}.
diff --git a/theories/typing/tests/get_x.v b/theories/typing/tests/get_x.v
index 4973fd2e..80f507e3 100644
--- a/theories/typing/tests/get_x.v
+++ b/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
diff --git a/theories/typing/tests/init_prod.v b/theories/typing/tests/init_prod.v
index 827d3397..d22af19c 100644
--- a/theories/typing/tests/init_prod.v
+++ b/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
diff --git a/theories/typing/tests/rebor.v b/theories/typing/tests/rebor.v
index bdb8cd0a..6a8c4a73 100644
--- a/theories/typing/tests/rebor.v
+++ b/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
diff --git a/theories/typing/tests/unbox.v b/theories/typing/tests/unbox.v
index b807b8c3..f2af4f94 100644
--- a/theories/typing/tests/unbox.v
+++ b/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.
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index 0dbfa1ea..132c55f0 100644
--- a/theories/typing/uninit.v
+++ b/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.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index c07ed71e..0a515948 100644
--- a/theories/typing/uniq_bor.v
+++ b/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 Σ}.
diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index bfd5dcbb..26bc7df7 100644
--- a/theories/typing/unsafe/cell.v
+++ b/theories/typing/unsafe/cell.v
@@ -1,7 +1,9 @@
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.
--
GitLab