-
Notifications
You must be signed in to change notification settings - Fork 1.9k
"borrow checker invariants" section of the "leveraging the type system" chapter #2867
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
base: main
Are you sure you want to change the base?
Changes from 5 commits
b771e7f
3831858
a81b55a
0b4318f
728af30
a37a272
88852f2
0aa4f21
37e69fe
595ca8e
2a88748
31284d6
e7f874b
808de4f
85b70f0
44dff2a
ebf00a2
7b72587
9f49ba5
6fcc471
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,58 @@ | ||
--- | ||
minutes: 0 | ||
--- | ||
|
||
# Using the Borrow checker to enforce Invariants | ||
|
||
The logic of the borrow checker, while tied to "memory ownership", can be abstracted away from this central use case to model other problems and prevent API misuse. | ||
|
||
```rust,editable | ||
fn main() { | ||
tall-vase marked this conversation as resolved.
Outdated
Show resolved
Hide resolved
|
||
// Doors can be open or closed, and you need the right key to lock or unlock one. | ||
// Modelled with Shared Key and Owned Door. Nothing to do with "memory safety"! | ||
pub struct DoorKey { pub key_shape: u32 } | ||
pub struct ClosedDoor { lock_shape: u32 } | ||
pub struct OpenDoor { lock_shape: u32 } | ||
|
||
fn open_door(key: &DoorKey, door: ClosedDoor) -> Result<OpenDoor, ClosedDoor> { | ||
if door.lock_shape == key.key_shape { | ||
Ok(OpenDoor{lock_shape: door.lock_shape}) | ||
} else { | ||
Err(door) | ||
} | ||
} | ||
|
||
fn close_door(key: &DoorKey, door: OpenDoor) -> Result<ClosedDoor, OpenDoor> { | ||
if door.lock_shape == key.key_shape { | ||
Ok(ClosedDoor{lock_shape: door.lock_shape}) | ||
} else { | ||
Err(door) | ||
} | ||
} | ||
|
||
let key = DoorKey{ key_shape: 7 }; | ||
let closed_door = ClosedDoor{ lock_shape: 7}; | ||
let opened_door = open_door(&key, closed_door); | ||
if let Ok(opened_door) = opened_door { | ||
println!("Opened the door with key shape '{}'", key.key_shape); | ||
} else { | ||
eprintln!("Door wasn't opened! Your key only opens locks with shape '{}'", key.key_shape); | ||
} | ||
} | ||
``` | ||
|
||
<details> | ||
|
||
- The borrow checker has been used to prevent use-after-free and multiple mutable references up until this point. | ||
tall-vase marked this conversation as resolved.
Outdated
Show resolved
Hide resolved
|
||
|
||
- This example uses the ownership & borrowing rules to model the opening and closing of a door. We can try to open a door with a key, but if it's the wrong key the door is still closed (here represented as an error.) | ||
tall-vase marked this conversation as resolved.
Outdated
Show resolved
Hide resolved
|
||
|
||
- The rules of the borrow checker fundamentally exist to prevent developers from accessing, changing, and holding onto data in memory in unpredictable ways without preventing _writing software_. The underlying logical system does not "know" what memory is. All it does is enforce a specific set of rules of how different operations affect what possible later operations are. | ||
|
||
- Those rules can apply to many other cases, so we can piggy-back onto the rules of the borrow checker to design APIs to be harder or impossible to misuse. Even when there's little or no actual "memory safety" concerns in the problem domain. | ||
|
||
- This section will walk through some of those different domains. | ||
|
||
- Interior, private mutability or reference counting in data types may let an API designer shift the meaning of ownership to a different (but analogous) set of semantics as they need to, even to the point where some API designers have managed to model self-referential types this way. | ||
|
||
</details> |
Original file line number | Diff line number | Diff line change | ||||
---|---|---|---|---|---|---|
@@ -0,0 +1,48 @@ | ||||||
--- | ||||||
minutes: 0 | ||||||
--- | ||||||
|
||||||
# Aliasing XOR Mutability | ||||||
|
||||||
We can use the mutual exclusion of `&T` and `&mut T` references for a single value to model some constraints. | ||||||
|
||||||
```rust,editable | ||||||
fn main() { | ||||||
pub struct TransactionInterface(/* some kind of interior state */); | ||||||
tall-vase marked this conversation as resolved.
Outdated
Show resolved
Hide resolved
|
||||||
|
||||||
pub struct DatabaseConnection { | ||||||
transaction: TransactionInterface, | ||||||
} | ||||||
|
||||||
impl DatabaseConnection { | ||||||
pub fn new() -> Self { Self { transaction: TransactionInterface(/* again, pretend there's some interior state */) } } | ||||||
pub fn get_transaction(&self) -> &TransactionInterface { &self.transaction } | ||||||
pub fn commit(&mut self) {} | ||||||
} | ||||||
|
||||||
pub fn do_something_with_transaction(transaction: &TransactionInterface) {} | ||||||
|
||||||
let mut db = DatabaseConnection::new(); | ||||||
let transaction = db.get_transaction(); | ||||||
do_something_with_transaction(transaction); | ||||||
db.commit(); | ||||||
do_something_with_transaction(transaction); // 🛠️❌ | ||||||
} | ||||||
``` | ||||||
|
||||||
<details> | ||||||
|
||||||
- This example shows how we can use the "Aliasing XOR Mutability" rule when it comes to shared and mutable references to model safe access to transactions for a database. This is a loose sketch of such a model, and rust database frameworks you use may not look anything like this in practice. | ||||||
tall-vase marked this conversation as resolved.
Outdated
Show resolved
Hide resolved
|
||||||
|
||||||
- As laid out in [generalizing ownership]("./generalizing-ownership.md") we can look at the ways Mutable References and Shareable References interact to see if they fit with the invariants we want to uphold for an API. | ||||||
|
- As laid out in [generalizing ownership]("./generalizing-ownership.md") we can look at the ways Mutable References and Shareable References interact to see if they fit with the invariants we want to uphold for an API. | |
- As laid out in [generalizing ownership]("./generalizing-ownership.md") we can look at the ways mutable references and shared references interact to see if they fit with the invariants we want to uphold for an API. |
tall-vase marked this conversation as resolved.
Outdated
Show resolved
Hide resolved
tall-vase marked this conversation as resolved.
Outdated
Show resolved
Hide resolved
tall-vase marked this conversation as resolved.
Outdated
Show resolved
Hide resolved
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,46 @@ | ||
--- | ||
minutes: 0 | ||
--- | ||
tall-vase marked this conversation as resolved.
Show resolved
Hide resolved
|
||
|
||
The logic of the borrow checker, while modelled off "memory ownership", can be abstracted away from that use case to model other problems where we want to prevent API misuse. | ||
|
||
```rust,editable | ||
pub struct InternalData; | ||
pub struct Value(InternalData); | ||
|
||
fn shared_use(value: &Value) -> &InternalData { | ||
&value.0 | ||
} | ||
|
||
fn exclusive_use(value: &mut Value) -> &mut InternalData { | ||
&mut value.0 | ||
} | ||
|
||
fn deny_future_use(value: Value) {} | ||
|
||
let mut value = Value(InternalData); | ||
let deny_mut = shared_use(&value); | ||
let try_to_deny_immutable = exclusive_use(&mut value); // ❌🔨 | ||
let more_mut_denial = &deny_mut; | ||
deny_future_use(value); | ||
let even_more_mut_denial = shared_use(&value); // ❌🔨 | ||
tall-vase marked this conversation as resolved.
Outdated
Show resolved
Hide resolved
|
||
``` | ||
|
||
<details> | ||
|
||
- To use the borrow checker as a problem solving tool, we will need to "forget" that the original purpose of it is to prevent mutable aliasing in the context of concurrency, instead imagining and working within situations where the rules are the same but the meaning is slightly different. | ||
tall-vase marked this conversation as resolved.
Outdated
Show resolved
Hide resolved
|
||
|
||
- In rust's borrow checker we have access to three different ways of "taking" a value: | ||
|
||
<!-- TODO: actually link to the RAII section when it has been merged. --> | ||
tall-vase marked this conversation as resolved.
Outdated
Show resolved
Hide resolved
|
||
- Owned value. Very permissive case of what you can do with it, but demands that nothing else is using it in any context and "drops" the value when scope ends (unless that scope returns this value) (see: RAII.) | ||
|
||
- Mutable Reference, while holding onto a mutable reference we can still "dispatch" to methods and functions that take an immutable, shared reference of the value but only as long as we're not aliasing immutable, sharable references to related data "after" that dispatch. | ||
|
||
- Shareable Reference, allows aliasing but prevents mutable access while any of these exist. We can't "dispatch" to methods and functions that take mutable reference when all we have is a shared reference. | ||
|
||
- Important to note that every `&T` and `&mut T` has an _implicit lifetime._ We get to avoid annotating a lot of lifetimes because the rust compiler can infer the majority of them. See: [Lifetime Elision]("../../../../../lifetimes/lifetime-elision.md") | ||
|
||
- Potentially relevant: show how we can replace a lot of the `&` and `&mut` here with `&'a` and `&'a mut`. | ||
tall-vase marked this conversation as resolved.
Outdated
Show resolved
Hide resolved
|
||
|
||
</details> |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,59 @@ | ||
--- | ||
minutes: 0 | ||
--- | ||
|
||
# Lifetime "Connections" & External Resources | ||
|
||
Using `PhantomData` in conjunction with lifetimes lets us say "this value may own its data, but it can only live as long as the value that generated it" in rust's type system. | ||
|
||
```rust,editable | ||
fn main() { | ||
use std::marker::PhantomData; | ||
pub struct Tag; | ||
pub struct ErasedData<'a>{data: String, _phantom: PhantomData<&'a ()>}; | ||
tall-vase marked this conversation as resolved.
Outdated
Show resolved
Hide resolved
|
||
impl <'a> ErasedData<'a> { | ||
pub fn get(&self) -> &str { | ||
&self.data | ||
} | ||
} | ||
pub struct TaggedData<T>{data: String, _phantom: PhantomData<T>}; | ||
tall-vase marked this conversation as resolved.
Outdated
Show resolved
Hide resolved
|
||
impl <T> TaggedData<T> { | ||
pub fn new(data: String) -> Self {Self {data, _phantom: PhantomData} } | ||
pub fn consume(self) {} | ||
pub fn get_erased(&self) -> ErasedData<'_> { | ||
// has an owned String, but _phantom holds onto the lifetime of the TaggedData | ||
// that created it. | ||
ErasedData { data: self.data.clone(), _phantom: PhantomData } | ||
} | ||
} | ||
|
||
let tagged_data: TaggedData<Tag> = TaggedData::new("Real Data".to_owned()); | ||
// Get the erased-but-still-linked data. | ||
let erased_owned_and_linked = tagged_data.get_erased(); | ||
tagged_data.consume(); | ||
// The data is owned by `erased_owned_and_linked` but still connected to `tagged_data`. | ||
println!("{}", erased_owned_and_linked.get()); // ❌🔨 | ||
} | ||
``` | ||
|
||
<details> | ||
|
||
- PhantomData lets developers "tag" types with type and lifetime parameters that are not "really" present in the struct or enum. | ||
tall-vase marked this conversation as resolved.
Outdated
Show resolved
Hide resolved
|
||
|
||
- PhantomData can be used with the Typestate pattern to have data with the same structure i.e. `TaggedData<Start>` can have methods or trait implementations that `TaggedData<End>` doesn't. | ||
|
||
- But it can also be used to encode a connection between the lifetime of one value and another, while both values still maintain separate owned data within them. | ||
|
||
- This is really useful for modelling a bunch of relationships between data, where we want to establish that while a type has owned values within it is still connected to another piece of data and can only live as long as it. | ||
|
||
- Consider a case where you want to return owned data from a method, but you don't want that data to live longer than the value that created it. | ||
|
||
- [`BorrowedFd`](https://rust-lang.github.io/rfcs/3128-io-safety.html#ownedfd-and-borrowedfdfd) uses these captured lifetimes to enforce the invariant that "if this file descriptor exists, the OS file descriptor is still open" because a `BorrowedFd`'s lifetime parameter demands that there exists another value in your program that has the same lifetime as it, and this has been encoded by the API designer to mean _that value is what keeps the access to the file open_. Its counterpart `OwnedFd` is instead a file descriptor that closes that file on drop. | ||
|
||
- Lifetimes need to come from somewhere! We can't build functions of the form `fn lifetime_shenanigans<'a>(owned: OwnedData) -> &'b Data` (without tying `'b` to `'a` in some way). Lifetime elision hides where a lot of lifetimes come from, but that doesn't mean the explicitly named lifetimes "come from nowhere." | ||
tall-vase marked this conversation as resolved.
Outdated
Show resolved
Hide resolved
|
||
|
||
- This way of encoding information in types is _exceptionally powerful_ when combined with unsafe, as the ways one can manipulate lifetimes becomes almost arbitrary. This is also dangerous, but when combined with tools like external, mechanically-verified proofs _we can safely encode cyclic/self-referential types while encoding lifetime & safety expectations in the relevant data types._ | ||
|
||
- The [GhostCell (2021)](https://plv.mpi-sws.org/rustbelt/ghostcell/) paper and its [relevant implementation](https://gitlab.mpi-sws.org/FP/ghostcell) show this kind of work off. While the borrow checker is restrictive, there are still ways to use escape hatches and then _show that the ways you used those escape hatches are consistent and safe._ | ||
|
||
</details> |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,49 @@ | ||
--- | ||
minutes: 0 | ||
--- | ||
|
||
# Single-use values | ||
|
||
In some circumstances we want values that can be used _exactly once_. One critical example of this is in cryptography: "Nonces." | ||
|
||
```rust,editable | ||
fn main() { | ||
pub struct Key; | ||
|
||
// Pretend this is a cryptographically unique, use-once number. | ||
pub struct Nonce(u32); | ||
|
||
// It's unsafe to declare a nonce directly! In practice, | ||
// this would be done with an RNG source, and potentially | ||
// a timestamp. | ||
unsafe fn new_nonce_from_raw(nonce: u32) -> Nonce { | ||
Nonce(nonce) | ||
} | ||
|
||
let nonce = unsafe { new_nonce_from_raw(1337) }; | ||
let data_1: [u8; 4] = [1, 2, 3, 4]; | ||
let data_2: [u8; 4] = [4, 3, 2, 1]; | ||
let key = Key; | ||
|
||
// The key and data can be re-used, copied, etc. but the nonce cannot. | ||
fn encrypt(nonce: Nonce, key: &Key, data: &[u8]) {} | ||
|
||
encrypt(nonce, &key, &data_1); | ||
encrypt(nonce, &key, &data_2); // 🛠️❌ | ||
} | ||
``` | ||
tall-vase marked this conversation as resolved.
Show resolved
Hide resolved
|
||
<details> | ||
|
||
- Owned "consumption" lets us model single-once values. | ||
tall-vase marked this conversation as resolved.
Outdated
Show resolved
Hide resolved
|
||
|
||
- Not implementing clone/copy here and making the interior type opaque (as per the newtype pattern) is _intentional_, as it prevents multiple uses of the same, API-controlled value. | ||
|
||
- I.e. A Nonce is a additional piece of random, unique data during an encryption process that helps prevent "replay attacks". | ||
|
||
|
||
- In practice people have ended up re-using nonces in circumstances where security is important, making it possible for private key information to be derived by attackers. | ||
|
||
- By tying nonce creation and consumption up in rust's ownership model, and by not implementing clone/copy on sensitive single-use data, we can prevent this kind of dangerous misuse. | ||
|
||
- Cryptography Nuance: There is still the case where a nonce may be used twice if it's created through purely a pseudo-random process with no additional metadata, and that circumstance can't be avoided through this particular method. This kind of API prevents one kind of misuse, but not all kinds. | ||
|
||
|
||
</details> |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Please add the timing information.