Enforcing resource invariants in Move

Introduction

Parsing bytes

struct Foo {
a: u8,
b: u8,
}
public fun parse_foo(bytes: vector<u8>): Foo {
let a = *vector::borrow(&bytes, 0);
let b = *vector::borrow(&bytes, 1);
Foo { a, b }
}
public fun parse_foo(bytes: vector<u8>): Foo {
assert!(vector::length(&bytes) == 2, 0);
let foo = *vector::borrow(&bytes, 0);
let bar = *vector::borrow(&bytes, 1);
Foo { foo, bar }
}
struct Foo {
a: u8,
b: u64,
}
public fun parse_u64(bytes: vector<u8>): u64 {
// read 8 bytes from the vector and construct a u64
...
}
public fun parse_u64(bytes: &vector<u8>, offset: u64): u64 {
// read 8 bytes from the vector starting at 'offset' and construct a u64
...
}
public fun parse_foo(bytes: vector<u8>): Foo {
assert!(vector::length(&bytes) == 9, 0);
let a = *vector::borrow(&bytes, 0);
let b = parse_u64(&bytes, 1);
Foo { a, b }
}

A safe interface for parsing

struct Cursor<T> {
data: vector<T>,
}
public fun poke<T>(cur: &mut Cursor<T>): T {
vector::pop_back(&mut cur.data)
}
public fun init<T>(data: vector<T>): Cursor<T> {
vector::reverse(&mut data);
Cursor { data }
}
public fun parse_u64(cursor: &mut Cursor<u8>): u64 {
...
}
public fun parse_foo(bytes: vector<u8>): Foo {
let cur = cursor::init(bytes);
let a = cursor::poke(&mut cur);
let b = parse_u64(&mut cur);
Foo { a, b }
}
57 │         let cur = cursor::init(bytes);
│ --- The local variable 'cur' still contains a value. The value does not have the 'drop' ability and must be consumed before the function returns
·
60 │ Foo { a, b }
│ ^^^^^^^^^^^^ Invalid return
public fun destroy_empty<T>(cur: Cursor<T>) {
let Cursor { data } = cur;
vector::destroy_empty(data);
}
public fun parse_foo(bytes: vector<u8>): Foo {
let cur = cursor::init(bytes);
let a = cursor::poke(&mut cur);
let b = parse_u64(&mut cur);
cursor::destroy_empty(cur);
Foo { a, b }
}

Parametricity

public fun destroy_empty<T>(cur: Cursor<T>) {
let Cursor { data } = cur;
}
    25 │     public fun destroy_empty<T>(cur: Cursor<T>) {
│ - The type 'vector<T>' can have the ability 'drop' but the type argument 'T' does not have the required ability 'drop'
26 │ let Cursor { data } = cur;
│ ---- ^ Invalid return
│ │
│ The local variable 'data' still contains a value. The value does not have the 'drop' ability and must be consumed before the function returns
public fun destroy_empty(cur: Cursor) {
let Cursor { data } = cur;
}

Can Rust do this?

Conclusion

--

--

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store
Wormhole

Cross-chain interoperability protocol connecting high value blockchains