personal/_drafts/types-as-contracts.md

   1 ---
   2 title: "Types as Contracts"
   3 categories: internship rust
   4 ---
   5
   6 Over the last couple of weeks of my [internship]({{ site.baseurl }}{% post_url
   7 2017-05-23-internship-starting %}), I have been working on a proposal for the "Unsafe Code Guidelines".
   8 I got some very encouraging feedback at the [Mozilla All-Hands](https://internals.rust-lang.org/t/recapping-this-weeks-mozilla-all-hands/5465),
   9 and now I'd like to put this proposal out there and start having a discussion.
  10 <!-- MORE -->
  11 Warning: Long post is long.  You have been warned.
  12
  13 If you need more context on unsafe code guidelines, I suggest you read my post on [undefined behavior]({{ site.baseurl }}{% post_url 2017-07-14-undefined-behavior %}) first.
  14
  15 ## It's in the Types
  16
  17 Consider the following simple function:
  18 {% highlight rust %}
  19 fn simple(x: &mut i32, y: &mut f32) -> i32 {
  20     *x = 3;
  21     *y = 4.0;
  22     *x
  23 }
  24 {% endhighlight %}
  25
  26 As discussed in my previous post, we would like an unsafe Rust program that calls this function with aliasing pointers to be UB.
  27 In my view, the reason this is UB is given by 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.
  28 Borrowing some terminology from related fields, we can see the function type as stating a *contract*:  We can call `simple` with non-aliasing pointers, and the function will behave.
  29 If we violate the contract, all bets are off.
  30
  31 To realize this idea, we need to define, for every type, what is the contract associated with that type -- when are elements of this type *valid*?
  32 For some types, that's simple: `i32` is any four-byte value. `bool` is one byte, either `0` or `1`.
  33 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`.
  34
  35 Where it gets interesting is the reference types: `&mut T` says that we have a (non-null, properly aligned) pointer.
  36 Whatever the pointer points to, must be a valid `T`.
  37 *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.
  38
  39 Similarly, for `&T`, we can rely on no-one performing any write access to this memory.
  40 At the same time, the contract for `&T` also says that we ourselves will not write to this memory either.
  41 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.
  42 Another example of a guarantee provided by functions is their promise to provide a valid return value when they are done.
  43
  44 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.
  45 In particular, `simple` would validate `x` and `y` immediately after being called, and it would be UB for them to alias.
  46
  47
  48 ## Specification
  49
  50 I have [previously written]({{ site.baseurl }}{% post_url 2017-07-14-undefined-behavior %}):
  51
  52 > I also think that tooling to *detect* UB is of paramount importance [...].
  53 In fact, specifying a dynamic UB checker is a very good way to specify UB!
  54 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.
  55
  56 Following this, I will in the following describe how to check for contract violations.
  57 I am considering a MIR program; if a Rust program is supposed to be checked, it has to be translated to MIR first.
  58 (You can [read up on my explanation]({{ site.baseurl }}{% post_url 2017-05-23-internship-starting %}) of why I think this is a good way to proceed.)
  59 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]({{ site.baseurl }}{% post_url 2017-06-06-MIR-semantics %}).[^1]
  60 The extra state in my proposal consists of something akin to a reader-writer lock for every memory location.
  61 I am first going to describe these locks and how they affect program behavior, before explaining contract validation.
  62
  63 [^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.
  64
  65 ### Memory locks
  66
  67 ### Validation
  68