From: Ralf Jung Date: Fri, 6 Apr 2018 11:09:55 +0000 (+0200) Subject: no multi-defn boxes X-Git-Url: https://git.ralfj.de/web.git/commitdiff_plain/71836ba461dbfa77bee7d1eae2c9173b0996c53e?hp=a0f981ab2c59f712725083ca43af6f3ce05e4804 no multi-defn boxes --- diff --git a/ralf/_posts/2018-04-05-a-formal-look-at-pinning.md b/ralf/_posts/2018-04-05-a-formal-look-at-pinning.md index 4aed608..98e0477 100644 --- a/ralf/_posts/2018-04-05-a-formal-look-at-pinning.md +++ b/ralf/_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)) ```