update student ad to match email
[web.git] / personal / _posts / 2017-07-17-types-as-contracts.md
1 ---
2 title: "Types as Contracts"
3 categories: internship rust
4 forum: https://internals.rust-lang.org/t/types-as-contracts/5562
5 ---
6
7 Over the last couple of weeks of my [internship]({% post_url
8 2017-05-23-internship-starting %}), I have been working on a proposal for the "Unsafe Code Guidelines".
9 I got some very encouraging feedback at the [Mozilla All-Hands](https://internals.rust-lang.org/t/recapping-this-weeks-mozilla-all-hands/5465),
10 and now I'd like to put this proposal out there and start having a discussion.
11 <!-- MORE -->
12 Warning: Long post is long.  You have been warned.
13
14 If you need more context on this topic, I suggest you read my post on [unsafe code guidelines and undefined behavior]({% post_url 2017-07-14-undefined-behavior %}) first.
15
16 ## 1 It's in the Types
17
18 Consider the following simple function:
19 {% highlight rust %}
20 fn simple(x: &mut i32, y: &mut f32) -> i32 {
21     *x = 3;
22     *y = 4.0;
23     *x
24 }
25 {% endhighlight %}
26
27 As discussed in my previous post, we would like an unsafe Rust program that calls this function with aliasing pointers to be UB.
28 I'd like to propose that the fundamental reason this is UB is the *type* of the function and, in particular, its arguments: `&mut` expresses uniqueness, so the memory pointed to by an `&mut` must not alias with anything else.
29 Borrowing some terminology from related fields, we can see the function type as stating a *contract*:  The `&mut` say that `simple` expects to be called with non-aliasing pointers.
30 If we violate the contract, all bets are off.
31
32 To realize this idea, we need to define, for every type, what is the contract associated with that type. When is some piece of storage *valid* at any given type?
33 For some types, that's simple: `i32` is any fully initialized four-byte value. `bool` is one byte, either `0` (representing `false`) or `1` (representing `true`).
34 Compound types like `(T, U)` are defined in terms of their constituent types:  The first component must be a valid `T`, the second component a valid `U`.
35
36 Where it gets interesting is the reference types: `&mut T` says that we have a (non-null, properly aligned) pointer.
37 Whatever the pointer points to must be a valid `T`.
38 *Moreover*, the memory range covered by this pointer (whose extent is given by the size of `T`) is exclusively accessed by this function -- no concurrent thread performs any access, and when we call unknown code and do *not* pass on the reference, we can rely on that unknown code not accessing this memory either.
39
40 Similarly, for `&T`, we can rely on no-one performing any write access to this memory.
41 At the same time, the contract for `&T` also says that we ourselves will not write to this memory either.
42 This is a nice example showing that contracts go both ways:  The function can rely on the other party (the caller) having done their part by providing valid arguments, but the function also has to make guarantees itself.
43 Another example of a guarantee provided by functions is their promise to provide a valid return value when they are done.
44
45 My proposal for the unsafe code guidelines then is to validate the contract described by a function's types at the function boundaries, and to make it UB for the contract to be violated.
46 In particular, `simple` would validate `x` and `y` immediately after being called, and it would be UB for them to alias.
47
48
49 ## 2 Specification Framework
50
51 I have [previously written about my thoughts on undefined behavior]({% post_url 2017-07-14-undefined-behavior %}):
52
53 > I also think that tooling to *detect* UB is of paramount importance [...].
54 In fact, specifying a dynamic UB checker is a very good way to specify UB!
55 Such a specification would describe the additional state that is needed at run-time to then *check* at every operation whether we are running into UB.
56
57 Following this, I will in the following describe how we could check the contracts expressed by Rust's types for violations.
58 I am considering a MIR program; if a Rust program is supposed to be checked, it has to be translated to MIR first.
59 (You can [read up on my explanation]({% post_url 2017-05-23-internship-starting %}) of why I think this is a good way to proceed.)
60 The validation of reference types (in particular, their exclusive / read-only nature) will need some extra "instrumented" state -- also see [this previous post on the topic]({% post_url 2017-06-06-MIR-semantics %}).[^1]
61 The extra state in my proposal consists of something akin to a reader-writer lock for every memory location.
62 I am first going to describe these locks and how they affect program behavior, before explaining contract validation.
63
64 [^1]: If at this point you are under the impression that all these previous posts have been collectively building up towards this proposal, you are not entirely wrong.
65
66 This is not (yet) a proper specification in that some important details are still left open.
67 The goal is to lay down a framework as the basis for discussion.
68 Many things already work as expected, and hopefully the remaining issues can be sorted out by tuning some of the details.
69
70 ### 2.1 Memory Locks
71
72 Every location comes with an additional reader-writer "lock".
73 These locks have nothing to do with concurrency, in fact they are more like `RefCell`.
74 Locks are used to verify the guarantees provided by references:
75 Shared references point to memory that is not mutated by anyone, and mutable references point to memory that is not *accessed* (read from or written to) by anyone *else*.
76 Notably, however, unlocked memory is free to be accessed by anyone -- nobody is making any particular assumptions about this memory.
77
78 To track these locks, we store a `locks: Vec<LockInfo>` for every location, with `LockInfo` defined as:
79 {% highlight rust %}
80 struct LockInfo {
81     write_lock: bool,
82     frame: usize,
83     lft: Option<Lifetime>,
84 }
85 {% endhighlight %}
86 (Notice that an implementation of this specification is free to track locks in a different way, as long as the effective behavior is the same.
87 The reason I am giving concrete types here is just to make the specification more precise.)
88
89 When a lock is acquired, we record which stack frame is the owner of this lock (starting at 0 for `main`, and counting up).
90 Now, on every read access, we check whether there is a write lock of this location held *by another function*.
91 If yes, the access is UB.
92 Furthermore, write accesses are UB if there is a read lock held *or* if there is a write lock held by another function.
93 Finally, acquiring a lock makes sure that the new lock is not in conflict with existing locks:
94 Acquiring a read lock is UB if there is a write lock held by anyone, including the function requesting a read lock; and acquiring a write lock is UB is there is any lock held by anyone.
95
96 Locks are typically released automatically when they expire.
97 To this end, the function acquiring a lock can optionally specify the *lifetime* of the lock.
98 Not specifying a lifetime implies that the lock is held until the function returns.
99 For the purpose of this specification, it does not matter what exactly a lifetime is; it is only relevant at which point it *ends*.
100 Lucky enough, MIR recently gained [`EndRegion` statements](https://github.com/rust-lang/rust/pull/39409) that we can use for this purpose:
101 When `EndRegion(lft)` is executed, all locks with lifetime `lft` are released.
102 Beyond this, a write lock can also be explicitly released by the function that acquired it, even before the lock's lifetime ends.
103 (It does not turn out to ever be necessary to do this for read locks in my proposal.)
104
105 There is one more mechanism we need to introduce:  Acquired write locks can be *suspended* for a lifetime.
106 This means the lock is temporarily released, but meant to be reacquired later.
107 To this end, the `LockInfo` is removed from the location's `locks` and put into a `HashMap<Lifetime, (Location, LockInfo)>` which is stored somewhere separately from the program's memory.
108 When the `EndRegion` corresponding to the given lifetime is reached, the lock is reacquired and put back into the `locks` of the given location.
109
110 ### 2.2 Examples
111
112 With the lock mechanism established, we can now perform type validation in MIR.
113 To this end, we add a new `Validate` statement to the language.
114 This statement takes a list of `(Lvalue, Ty)` pairs to be validated, and a *validation operation*.
115 The operation can be *acquire*, *suspend (for a lifetime)* or *release*, indicating whether memory locks are acquired, suspended, or released.
116 Before explaining type validation in general, let us look at some examples.
117
118 #### Validating function arguments
119
120 Here's the sample code from above with validation annotated explicitly:
121 {% highlight rust %}
122 fn simple(x: &mut i32, y: &mut f32) -> i32 {
123     Validate(Acquire, [x, y]);
124     *x = 3;
125     *y = 4.0;
126     *x
127 }
128 {% endhighlight %}
129 For simplicity's sake, I just pretend that validation commands were present not just in MIR, but also in the Rust surface language. Also, while validation takes *pairs* of lvalues and types, the types can be inferred, so I am only listing lvalues here.
130
131 Let us now see what happens when `x` and `y` alias.
132 I mentioned above that we want this case to be UB, because we want to be able to reorder the two stores.
133 Indeed, it will turn out that the validation describes above triggers UB here.
134
135 We perform acquire validation of the arguments immediately after a function is called.
136 This validates the function's contract with the caller.
137 `x` is of reference type, so validation will follow the reference and recursively validate whatever `*x` is valid at type `i32`.
138 The recursive call then acquires the write lock for `*x` and checks that memory is initialized.
139 The lock is acquired for the entire duration of the function call, based on the fact that the lifetime of the reference outlives the function.
140 This completes validating `x`.
141 Validation of `y` proceeds exactly the same way.
142 In particular, validation will acquire a write lock for `*y`.
143 However, since `x` and `y` alias, this will overlap the write lock that was acquired for `*x`!
144 This is how we get the UB that we were looking for.
145
146 In other words, acquiring locks for everything we can reach through references implicitly checks for aliasing, making sure that mutable references do not overlap with anything else.
147
148 #### Validating function calls
149
150 The second example demonstrates how validation, and memory locks in particular, let us reason about the actions of unknown external functions:
151 {% highlight rust %}
152 // Defined elsewhere: fn fun(x: &i32, z: &mut (i32, i32)) { ... }
153
154 fn example(x: &i32, y: &mut i32, z: &mut (i32, i32)) {
155     Validate(Acquire, [x, y, z]);
156     let x_val = *x;
157     let y_val = *y;
158
159     Validate(Release, [x, z]);
160     fun(x, {z});
161
162     let x_val_2 = *x;
163     *y = y_val;
164 }
165 {% endhighlight %}
166 We would like to optimize this code and eliminate the write to `y` at the end of the function, arguing that we are just writing back the value that's already stored there.
167 The reason we think we can do that is that we hold an exclusive reference to `*y`.
168 We do not pass `y` to `fun`, and there most not be any other reference to this memory, so `fun` cannot touch `y`.
169 And indeed, the validation rules make it so that it is UB for `fun` to access `y`.
170
171 Furthermore, we want to eliminate the load from `x` at the end, and instead re-use `x_val`, arguing that since `x` is a shared reference, it is UB for `nop` to change its value.
172
173 In the beginning of `example`, during acquire validation, we acquire the read lock for `*x` and the write lock for `*y` and `*z`.
174 When we pass a mutable reference to `fun`, we explicitly acknowledge that `fun` has the right to modify this memory.
175 This means that we have to *release* any write locks that we may hold on `x` or `z`, which is done by performing release validation on all function arguments.
176 For `x`, this doesn't actually do anything as we only hold a read lock, but the write lock on `z` is released here.
177 (We assume there is no implicit reborrowing of `z` going on here. The curly braces make it so that `z` is moved, not borrowed, to `fun`.)
178 So, when `fun` is called, we still hold the read lock for `x` and the write lock for `y`.
179 Consequently, if `fun` were to access `y` or write to `x`, we know that's UB -- so we can rely on this not to happen and perform our desired optimizations.
180
181 Notice that this optimization is extremely hard to perform e.g. in C, because to know that `fun` cannot access `y`, the compiler needs to do whole-program alias analysis -- a notoriously hard problem.
182 In contrast, Rust's type system allows us to perform such optimizations intra-procedurally, without looking at other functions' code at all.
183
184 #### Validating taking a reference
185
186 In the last example, we deliberately *moved* `z` to `fun` to side-step any discussions about borrowing.
187 However, typically, you would actually *reborrow* `z`.
188 As we will see in this example, to properly model transferring ownership of (re)borrowed memory to other functions, we will perform suspend and acquired validation around the operation that takes a reference.
189 To better demonstrate this, let us also say that `fun` actually returns a reference with the same lifetime as `z`.
190 Overall, our code now looks like this (with all reborrowing being explicit):
191 {% highlight rust %}
192 // Defined elsewhere: fn fun<'z>(x: &i32, z: &'z mut (i32, i32)) -> &'z mut i32  { ... }
193
194 fn example(x: &i32, y: &mut i32, z: &mut (i32, i32)) {
195     Validate(Acquire, [x, y, z]);
196     let x_val = *x;
197     let y_val = *y;
198
199     {   // 'inner begins here
200         Validate(Suspend('inner), [z]);
201         let z_for_fun = &'inner mut z;
202         Validate(Acquire, [z_for_fun]);
203
204         Validate(Release, [x, z_for_fun]);
205         let z_inner : &'inner mut i32 = fun(x, {z_for_fun});
206         Validate(Acquire, [z_inner]);
207
208         *z_inner = 42;
209     }   // 'inner ends here
210
211     let x_val_2 = *x;
212     *y = y_val;
213 }
214 {% endhighlight %}
215 Again we would like to eliminate the write to `y` and the read from `x`.
216 To eliminate the write to `y` as being redundant, we have to prove, in particular, that the write to `z_inner` cannot affect `*y`.
217
218 As usual, we start by acquiring the read lock for `*x` and the write lock for `*y` and `*z`.
219 When `z` gets reborrowed to be passed to `fun` with lifetime `'inner`, we *suspend* our lock of `*z` for this lifetime.
220 This models the fact that, no matter what we do with the newly created reference, we know that when `'inner` ends, we get our exclusive access back.
221 After the suspension, we don't hold a lock any more for what is now `*z_for_fun`, so we immediately acquire a write lock again.
222 However, following the type of `z_for_fun`, we will acquire this lock only for lifetime `'inner`.
223 For this to work, validation needs to know the *non-erased type* of the lvalues -- all the lifetime information must be present, so we can acquire the lock for the right lifetime.
224 (Suspending and then acquiring the write lock may sound somewhat redundant.
225 However, notice that, if we were to take a shared reference, we would now acquire a read lock rather than a write lock.
226 Furthermore, even here, the overall effect is far from a no-op: The suspended lock will stay around even if the reacquired lock is released.  In fact, this is exactly what happens next.)
227
228 Next, we call `fun`.
229 At this point, we release our write lock on `*z_for_fun` again, as usual when passing a mutable reference to a function.
230 (The acquire-release of `z_for_fun` is indeed redundant here, but notice that the two validation statements arise from two separate MIR operations:  taking a reference and calling a function.
231 These operations just happen to occur immediately after one another here.)
232 However, the suspended lock of `*z` stays around -- so while we gave up control of `z` (aka `z_for_fun`) for lifetime `'inner`, we still know that we will get control back when `'inner` ends!
233 `fun` is now free to do whatever it wants, as long as it does not violate our still-existing write lock of `*y` and the read lock of `*x`.
234
235 When `fun` returns, we obtain a new mutable reference.
236 At this point, we again run acquire validation.
237 In this case, we want to ensure that `z_inner` does not alias `y`.
238 The locks ensure that `fun` cannot possibly change `y`, but we (`example`) can -- and if writing to `z_inner` were to change `*y`, that access would come from the stack frame holding the lock on `y`, so it would be permitted!
239 However, we do want to still optimize away the write to `y` at the end of `example` as being redundant.
240 To this end, we acquire-validate all data returned to us from other functions, making sure that references we obtain this way to not conflict with other references we already hold.
241 Following the type of `z_inner`, we only acquire this lock for `'inner`.
242
243 Another way to look at acquiring the return value is that we are validating the contract we have with `fun`: The contract says that `fun` should return a reference to us that comes with the uniqueness guarantees of `&mut`, so we better make sure that `fun` actually delivered what it said it would.
244
245 Finally, `'inner` ends.
246 Multiple things happen now:
247 First, our lock of `z_inner` expires and is hence released.
248 (We already released the lock of `z_for_fun` ourselves, so nothing is to be done there.)
249 Next, remember that we suspended our lock of `z` for `'inner`; so now is the time that this lock gets reacquired.
250 In other words, as the lifetime of the reborrow from `z` expires, we release all locks of memory that is tied to that lifetime, and then re-gain full exclusive access to `z`.
251
252 When we come to the write to `*y`, we know that this write is redundant because (a) we held the write lock for `*y` all the time, so nobody else could have written to it without triggering UB, and (b) we know `z_inner` does not alias with `y` (or else we would already have UB), so we ourselves have not written to `*y` either.
253 Hence, we may optimize away the write.
254
255 ### 2.3 Validation
256
257 The examples should already give you a good idea of what `Validate` does.
258 It is time to look at this statement in some more depth.
259 Remember that it takes a validation operation and a list of lvalue-type pairs as arguments.
260 The most important validation operation is *acquire validation*.
261 As the name indicates, this is about acquiring the appropriate locks.
262 It also otherwise makes sure that values are valid at the given type, e.g., references have to be non-NULL and aligned.
263
264 The core of acquire validation is an operation with a signature roughly like this:
265 {% highlight rust %}
266 fn acquire_validate(lval: Lvalue, ty: Ty, mutbl: Mutability, lft: Option<Lifetime>)
267 {% endhighlight %}
268 Why are mutability and lifetime showing up here?
269 The reason is that reference types have a "transitive" effect down the type hierarchy: `&T` makes everything reachable through this reference read-only, even if `T` involves `&mut`.
270 Similarly, in case of nested references, it is the *outermost* reference that defines the lifetime for which access through this pointer is granted.
271 (The compiler makes sure that inner references always have longer lifetimes than outer references.)
272
273 As we have seen in the examples, `acquire_validate` recursively traverses the type hierarchy.
274 When it encounters a primitive type like `i32`, it acquires a lock of `size_of::<ty>` many locations starting at `lval` for lifetime `lft` -- this will be a write or read lock depending on whether `mutbl` says this data is mutable or not.[^2]
275 In other words, memory is locked "at the leaves" of the type structure, rather than locking immediately when we see a reference type.
276 We will come back later to why this is necessary.
277 Validation also makes sure that the value stored in memory is valid at the given type.
278 For a `u32`, this just amounts to checking that the memory is properly initialized.
279
280 [^2]: For simplicity, we pretend lvalues are just locations in memory.  Actually, lvalues can also refer to variables not in memory (like non-addressable stack locals), but these do not need to be locked.  Furthermore, lvalues for unsized types carry the additional information stored in a fat pointer, i.e., a length (for slices) or a vtable (for trait objects); this is handled appropriately when validating the respective types.
281
282 For compound types like tuples, `struct` or `enum`, validation proceeds recursively on the fields.
283 In particular, the enum discriminant is checked to be in-range (in particular, nothing can pass validation at an empty enum type).
284 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.
285
286 Finally, when encountering a box or reference type, two things happen.
287 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.
288 The pointer is also checked to be non-NULL and properly aligned for the type it points to.
289 Furthermore, validation proceeds recursively after *dereferencing* the pointer.
290 Crucially, for the case of validating a reference, the `mutbl` and `lft` for this recursive call are taking the type into account:
291 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.
292 If `mutbl` was mutable, it becomes immutable when following a shared reference.
293
294 Acquire validation is performed at the beginning of every function (acquiring the function arguments) and upon returning from another function (acquiring the return value).
295 These are the places when we rely on other functions providing valid data to us.
296
297 There are two other validation operations besides acquire validation: release validation, and suspend validation.
298 Both operations recursively follow the type just like acquire validation, and for all memory they visit, they release/suspend *write* locks.
299 Read locks are not touched, which corresponds to the fact that shared references are `Copy` and hence never "given up":
300 Shared references always remain usable until their lifetime expires, at which point the read lock is released automatically.
301
302 Release validation occurs before calling a function, when the function arguments are released.
303 This grants the functions write access to memory that we are explicitly passing along.
304
305 Suspend validation occurs before taking a reference, using the lifetime of the new reference.
306 This encodes the fact that when the lifetime ends (and hence the lock is being reacquired), we are the exclusive owner of this memory again.
307
308 **Update:** It has been pointed out to me that another way for values to flow back into a function is through mutable references. Good catch! I will need to extend the validation machinery to also perform acquire validation when a write lock is reacquired. **/Update**
309
310 To summarize, validation statements are emitted during MIR construction in the following places:
311 - At the beginning of the function, we perform acquire validation of the arguments.
312 - When taking a reference, we suspend the referee for the reference lifetime and acquire the referent.
313 - When calling another function, we release the arguments and acquire the return value.
314
315
316 ### 2.4 `UnsafeCell`
317
318 I hope you now have an idea of how memory locks and validation enforce the assumptions that are encoded in Rust's types.
319 One topic that needs special treatment in this context is interior mutability.
320 If a function takes an `x: &Cell<i32>`, following the rules above, it will acquire a read lock of `*x` for the duration of the function call, making `*x` immutable.
321 Clearly, we do not want to do that -- calling `x.set` *will* actually mutate `*x`, and mutating through a shared reference is exactly the point of using `Cell`!
322
323 Lucky enough, the compiler *already* says that interior mutability is only allowed via [`UnsafeCell`](https://doc.rust-lang.org/stable/core/cell/struct.UnsafeCell.html).
324 We can use this for our purposes: To adjust validation for interior mutability, we *stop* our recursive descent and do not do anything when reaching an `UnsafeCell` *while `mutbl` indicates we are in immutable mode* -- `&mut UnsafeCell` is not affected.
325 In particular, no locks are acquired.
326 This justifies calling `set` on a shared reference and having the value changed.
327 Of course, it also means we cannot do some of the optimizations we discussed above -- but that's actually exactly what we want!
328 These optimizations are unsound in the presence of interior mutability.
329
330 Notice that for this to work, it is crucial that we acquire locks "at the leaves" of the type structure, and not just when we encounter a reference.
331 For example, if we validate something at type `&(i32, Cell<i32>)`, we *do* want to acquire a read lock for the first component, but not for the second.
332
333 ### 2.5 Unsafe Code
334
335 There's one last issue that I want to cover before (finally) concluding this post: Unsafe code.
336 So far, we have only considered entirely safe code, and we have seen how validation and memory locks enforce the guarantees associated with reference type.
337 The type checker already ensures that safe code will never trigger a lock failure -- actually, you can see the validation statements as some form of "dynamic borrow checking", enforcing the same rules as the borrow checker does statically.
338 The only way that these checks could ever fail is for unsafe code to feed "bad" values into safe code, and that is exactly the point:
339 These proposed "unsafe code guidelines" restrict what unsafe code can do when interfacing with safe code.
340
341 However, *within* unsafe code, we have to give programmers a little more leeway.
342 We cannot always make as strong assumptions as we did in safe code:
343 For example, let us look at `mem::swap` (somewhat desugared):
344 {% highlight rust %}
345 // Defined elsewhere: unsafe fn ptr::swap_nonoverlapping<T>(x: *mut T, y: *mut T) { ... }
346
347 pub fn swap<T>(x: &mut T, y: &mut T) {
348     Validate(Acquire, [x, y]);
349     let x = x as *mut T;
350     let y = y as *mut T;
351     unsafe {
352         Validate(Release, [x, y]);
353         ptr::swap_nonoverlapping(x, y, 1);
354     }
355 }
356 {% endhighlight %}
357 In the beginning, we acquire the write lock for `x` and `y`, establishing that the two pointers do not alias -- this is exactly as expected.
358 However, when we release the arguments to `ptr::swap_nonoverlaping`, nothing actually happens:
359 We are only passing raw pointers that do not come with any guarantees.
360 In particular, we keep the write locks on `x` and `y`!
361 Now, that's a problem -- `ptr::swap_nonoverlaping` will of course write to both of them when it swaps their content, triggering UB.
362
363 First of all, let me note that this example actually demonstrates that we are validating the borrow checking gurantees correctly.
364 As far as the borrow checker is concerned, `x` and `y` have never been borrowed or moved to anyone else, they were fully owned by `swap` all the time.
365
366 The trouble is that the ownership transfer to `ptr::swap_nonoverlaping` is not described by its type, and hence cannot be known to the compiler.
367 This is possible because `ptr::swap_nonoverlapping` is an *unsafe* function that can make more assumptions than its type says, and rely on the caller to uphold these assumptions.
368 The compiler has no way to know what these assumptions are.
369
370 To accommodate such code, I suggest that we emit fewer validation instruction when building MIR for functions containing unsafe blocks.
371 For example, we could imagine that if a function contains an unsafe block, instead of the usual validation, we only perform an acquire in the beginning of the function, immediately followed by a release.
372 This would verify that our arguments are well-formed, but would otherwise acknowledge that we just do not know how ownership is flowing inside such a function.
373 Of course, this also disables some optimizations -- but maybe these are optimizations that we do not want to perform anyway in unsafe code, because they could end up breaking the program.
374
375 Anyway, this part of my proposal is certainly not yet final.
376 This topic needs input from many people so as to safely cover the unsafe code people write while still (hopefully) permitting the optimizations people expect to happen.
377 One potential middle-ground here is having a function attribute that controls which validation statements are emitted, or even providing some form of intrinsics for programmers to explicitly perform validation.
378
379 ## 3 Conclusion
380
381 I have described a mechanism to validate the contract expressed by Rust's types, in particular, the uniqueness and read-only guarantees provided by reference types.
382 This validation describes what (safe) code can assume about its variables at run-time, and it enables some code motion optimizations that would otherwise require whole-program alias analysis.
383
384 I said before that I think providing a way to *detect* UB is crucial, and the framework laid out above is designed with this in mind.
385 In fact, I have been working on a miri-based implementation of this mechanism:
386 [This rustc branch](https://github.com/RalfJung/rust/tree/mir-validate) adds the new `Validate` statement to MIR and adds a MIR pass to insert validation statements as described above, while [this miri branch](https://github.com/RalfJung/miri/tree/mir-validate) adds memory locks to miri and implements type-based validation.
387 (Both of these branches are subject to frequent rebasing, so expect force pushes if you track them.)
388 The implementation is not yet complete, and some of the terminology changed (it turns out writing things down helps you find good names :), so don't be confused if it looks a little different.
389 Other than that though, feel free to play around and provide feedback.
390 I hope the implementation can help us check whether unsafe code follows the rules I laid down here, and whether these rules match programmer intuition.
391 (In fact, this is how I figured out that `mem::swap` violates the most strict interpretation of the rules -- I did expect a violation somewhere in libstd's unsafe code, but had no idea where it would show up.) 
392 We could even have a test suite to aid in fine-tuning the rules.
393
394 I also said that "we should strive for programmers' intuition agreeing with the [...] compiler".
395 This is of course hard to measure, but one property that I think goes a long way here is that in this proposal, pointers can remain "thin".
396 I probably should write a whole separate blog post on this topic, but the short version is that in my proposal, if a function has permission to access certain region of memory, then it does not matter how it performs the access -- if there are multiple pointers to this region around, they are all equally valid to use.
397 This is in contrast to e.g. C's `restrict` or type-based alias analysis, which make a distinction based on *which pointer* is used to access certain regions of memory.
398 Such models are fairly hard to write checkers for, as witness by there being no sanitizer.
399 Moreover, they typically (from what I have seen so far) have some trouble supporting integer-pointer casts.
400 If pointers have an "identity" beyond the address they point to, then which "identity" does a pointer that's casted from an integer obtain?
401 I am not saying it is impossible to solve this issue, but it is a source of complication.
402 It is also quickly a source of programmer confusion.
403 In my experience, programmers that use pointers casted from integers typically like to think of pointers as being "just integers" and not having any "identity" beyond the address they point to (and indeed, the fact that such casts work seems to indicate that they are right).
404 I would be much less worried about unsafe Rust code being broken by optimizations if we can make it so that this mental model is actually right.
405 Wouldn't it be great if we could add "Has the simple model of pointers that everybody incorrectly *thinks* C has" to the list of Rust selling points?
406 I think this aligns well with Rust's slogan "Hacking without fear" -- and without compromise; remember we still get all the optimizations!
407
408 Congratulations!
409 You have reached the end of this blog post.
410 Thanks a lot for reading.
411 If you have any comments, please raise them -- the entire purpose of this post is to get the proposal out there so that we can see if this approach can suit the needs of Rust programmers and compiler writers alike.
412 If there are explanations you think are missing or confusing, please bring that up as well; I may then update this post accordingly or add a note in the [forum](https://internals.rust-lang.org/t/types-as-contracts/5562) for any ammendments that turned out to be necessary.
413 The concrete proposal will sure need some fixing here and there.
414 It is also not complete yet.
415 I already mentioned that there are open questions around unsafe code.
416 Other areas of future work include `static` variables and the `NonZero` type.
417 Nevertheless, my hope is that the general approach of a contract-like, type-driven validation mechanism ends up being useful.
418 So, keep the comments flowing -- and safe hacking.
419
420 **Update**: I did some refactoring of the post, reordering sections 2.2 and 2.3 to hopefully make it all flow better. Thanks for all the helpful feedback!
421
422 #### Footnotes