mention boxes

diff --git a/ralf/_posts/2017-07-17-types-as-contracts.md b/ralf/_posts/2017-07-17-types-as-contracts.md
index 6bcaea00e2aaa8a212ff32801d0d4cc4a592dbde..bb867e78bcd9060690bafd94b568d903a397ce3a 100644 (file)
--- a/ralf/_posts/2017-07-17-types-as-contracts.md
+++ b/ralf/_posts/2017-07-17-types-as-contracts.md
@@ -283,11 +283,11 @@ For compound types like tuples, `struct` or `enum`, validation proceeds recursiv
 In particular, the enum discriminant is checked to be in-range (in particular, nothing can pass validation at an empty enum type).
 However, because the recursive validation will only lock memory that's actually covered by a field, we also have to acquire the appropriate lock for padding bytes and the enum discriminant here.
 
 In particular, the enum discriminant is checked to be in-range (in particular, nothing can pass validation at an empty enum type).
 However, because the recursive validation will only lock memory that's actually covered by a field, we also have to acquire the appropriate lock for padding bytes and the enum discriminant here.
 

-Finally, at a reference type, two things happen.
-First, the reference itself is stored in memory somewhere; this memory has to be locked just like the validation of `i32` locks the memory used to store the integer.
-The reference is also checked to be non-NULL and properly aligned for the type it points to.
-Furthermore, validation proceeds recursively after *dereferencing* the reference.
-Crucially, the `mutbl` and `lft` for this recursive call are taking the reference type into account:
+Finally, when encountering a box or reference type, two things happen.
+First, the pointer itself is stored in memory somewhere; this memory has to be locked just like the validation of `i32` locks the memory used to store the integer.
+The pointer is also checked to be non-NULL and properly aligned for the type it points to.
+Furthermore, validation proceeds recursively after *dereferencing* the pointer.
+Crucially, for the case of validating a reference, the `mutbl` and `lft` for this recursive call are taking the type into account:

 If `lft` was `None` and this reference's lifetime ends within the function (i.e., there is a corresponding `EndRegion` somewhere), it is now set to the reference's lifetime.
 If `mutbl` was mutable, it becomes immutable when following a shared reference.
 
 If `lft` was `None` and this reference's lifetime ends within the function (i.e., there is a corresponding `EndRegion` somewhere), it is now set to the reference's lifetime.
 If `mutbl` was mutable, it becomes immutable when following a shared reference.