Guarantees

Everything so far was about what Makoto lets you write. This chapter is about what it lets you promise: that a handle is used exactly once, that a balance is never negative, that two processes follow the same protocol, that a function is correct. Each promise is summoned by a decorator or a type, and none of it touches code that does not ask for it.

Designed, not yet implemented

The verification layer is fully designed (design document §21, and the verification guide) but the mk compiler does not check it yet. The snippets below show the target language. Use them to learn the model, not to test the compiler.

The ladder

Every guarantee has the same shape: an obligation on a predicate. “This index is in bounds” is the predicate i < len. The compiler’s job is to discharge each obligation, as strongly as it can:

Rung	How it is discharged	Example
0	Type-level: the bad state cannot be written	a dropped @must_consume
1	Comptime fold: the compiler computes the answer	Index[8] with the literal 3
2	Summoned proof: an extension proves it (SMT, model checker)	a refinement over dynamic arithmetic
3	Runtime check: a trap on violation	@requires, a refinement that reached runtime
4	Advisory: a warning, no inserted cost	the memory analyzer’s hints
5	Human: you assert it, in writing	assume "…"

One rule keeps it honest:

An obligation that cannot be met at one rung falls to the next one down. Never off the ladder.

A refinement the solver cannot prove becomes a runtime check. A runtime check you cannot afford on a hot path becomes an assume with your name on it. The guarantee degrades in the open, and the language tells you which rung it landed on.

Use a thing the right number of times

Two decorators on a decl say how many times a value may be consumed:

• @must_consume: exactly once (linear). Forgetting it is the bug.
• @consume_once: at most once (affine). It may go unused, but never twice.

decl Transaction @must_consume { conn: *Connection }
decl Scratch      @consume_once { buf: [*]u8 }

fn commit(t: Transaction @consume)   { … }
fn rollback(t: Transaction @consume) { … }

fn handle(t: Transaction) {
    if ok { commit(t) }
    // ERROR: on the else path, t is never consumed
}

This is the @transfer analysis from chapter 08, lifted from a parameter to the type itself. The wrong program does not compile, so there is nothing to check at runtime (rung 0).

Index the type by a state and you get typestate for free:

decl File[s: FileState] @must_consume { fd: i32 }
fn open(path: string) -> File[Open]
fn close(f: File[Open] @consume) -> File[Closed]   // only an Open file, and only once

Closing a File[Closed] does not typecheck. There is no “already closed” flag to forget.

Types that carry a promise

A refinement is a type plus a predicate its values always satisfy. It is written with @where, and the value is named the same way @ensures names a return: by its type, or by a named slot.

alias Balance         = i64   @where(i64 >= 0)
alias Index[n: usize] = usize @where(usize < n)
alias NonEmpty[T]     = (xs: List[T]) @where(xs.len > 0)

A NonEmpty[T] flows anywhere a List[T] is wanted, but not the other way around. Inside a guard, the checker narrows:

fn first[T](xs: NonEmpty[T]) -> T {
    return xs[0]                        // no bounds check, no Optional
}

let ys: List[int] = read_input()
// first(ys)                            // ERROR: List[int] is not NonEmpty[int]
if ys.len > 0 { first(ys) }             // OK: the guard narrowed ys

A literal decides at comptime (rung 1). Dynamic arithmetic goes to the SMT extension (rung 2), and what nobody can prove becomes a runtime check (rung 3).

Fences: pure and total

• @pure: no side effects. Same inputs, same output, nothing outside changed.
• @total: defined for every input and always terminates.

Both are inferred by default. Writing the decorator is demanding the check:

@pure  fn area(r: f64) -> f64 { return 3.14159 * r * r }
@total fn len[T](xs: List[T]) -> usize {
    match xs {
        Nil        => 0
        Cons(_, t) => 1 + len(t)
    }
}

Exhaustive match already rules out getting stuck; @total adds the termination proof. A comptime function used inside a type must be @total, which is what keeps a type from hanging the compiler.

A protocol the compiler walks

A channel’s type says what can cross it. A session type also says in what order, so a deadlock from both sides waiting becomes a compile error. Makoto spells it with words you already know:

@protocol decl KVServer {
    loop {
        @receives match {                 // the client picks the operation each round
            Get  => { Key @receives;  Value @sends;   continue }
            Put  => { Key @receives;  Value @receives;  Ack @sends;  continue }
            Quit => _                     // out of the loop: the session ends
        }
    }
}

@receives match means the peer chooses the branch; @sends match means you do. You write the protocol once, from one side. The other side is its mirror, dual, and spawn checks that both ends line up:

let c: Channel[Auth]        // the client holds Auth
spawn server(ch)            // ch: Channel[dual Auth]

A plain Channel[T] stays a typed pipe. Only a channel typed by a @protocol is walked as a session.

Types that mention values

You already wrote [N]T. Value-parameters on a decl take it further, with no new syntax:

decl Vec[T, n: usize] { data: [n]T }
fn concat[T, n: usize, m: usize](a: Vec[T, n], b: Vec[T, m]) -> Vec[T, n + m]

That buys length safety, bounds safety and units of measure today. Behind @proof, the same machinery becomes a proof assistant: a proposition is a type, and a proof is a program that has that type.

@proof @total fn zero_right(n: Nat) -> Eq[Nat, add(n, 0), n] {
    match n {
        Zero    => Refl
        Succ(k) => cong(Succ, zero_right(k))   // induction is match plus the recursive call
    }
}

Proving a design

Proofs verify an implementation. Model checking verifies a design: it explores the states of a supervised subtree and checks global properties. It lives in an extension, because its engine changes with the state of the art:

// safety: there is never more than one leader per term
@spec(count(nodes, |n| n.role == Leader && n.term == cur) <= 1)

// liveness: every submitted request is eventually committed
@spec(spec.always(spec.implies(submitted(req), spec.eventually(committed(req)))))

When nothing else fits

The last rung is you. assume (chapter 10) asserts without checking, in writing, at the operation that needs it. It is never silent and never a license for undefined behavior. It is the guarantee falling to the strongest honest form left.

What to remember

You write	You get	Usually lands on
@must_consume / @consume_once	used exactly once / at most once	rung 0
@where(pred)	a value satisfies a predicate	rung 1, 2 or 3
@pure / @total	no effects / terminates	rung 0
@protocol, @sends / @receives, dual	a protocol is followed, no deadlock	rung 0
value-params, @proof	lengths and bounds today, full proofs opt-in	rung 0 or 1
@spec	global safety and liveness	rung 2

For every term, every rung and the reasoning behind them, read the verification spectrum.