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/ca01c873f12fa26f5bbe11310b392cd855e7caf9?hp=e33e1041ec91bb5a9f538631b578c6bcfb78c73a no multi-defn boxes --- 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)) ```