From 126a0604a09fd8f572f688e56a1abe58278d76a6 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Fri, 6 Apr 2018 13:09:55 +0200 Subject: [PATCH 1/1] no multi-defn boxes --- personal/_posts/2018-04-05-a-formal-look-at-pinning.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/personal/_posts/2018-04-05-a-formal-look-at-pinning.md b/personal/_posts/2018-04-05-a-formal-look-at-pinning.md index 4aed608..98e0477 100644 --- a/personal/_posts/2018-04-05-a-formal-look-at-pinning.md +++ b/personal/_posts/2018-04-05-a-formal-look-at-pinning.md @@ -154,6 +154,8 @@ Formally: ``` Box.own(bytes) := exists |ptr, inner_bytes| bytes.try_into() == Ok(ptr) && ptr.points_to_owned(inner_bytes) && T.own(inner_bytes) +``` +``` (&'a mut T).own(bytes) := exists |ptr| bytes.try_into() == Ok(ptr) && borrowed('a, exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes)) @@ -166,6 +168,8 @@ This could look as follows: ``` Box.own(ptr: Pointer) := exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes) +``` +``` (&'a mut T).own(ptr: Pointer) := borrowed('a, exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes)) ``` @@ -223,6 +227,8 @@ A list of bytes makes a valid `PinBox` if those bytes form a pointer `ptr` su For `Pin<'a, T>`, `ptr` is valid if we have borrowed `T.pin(ptr)` for lifetime `'a`. ``` PinBox.own(ptr) := T.pin(ptr) +``` +``` Pin<'a, T>.own(ptr) := borrowed('a, T.pin(ptr)) ``` -- 2.30.2