Garantias

Até aqui o livro tratou do que a Makoto deixa você escrever. Este capítulo trata do que ela deixa você prometer: que um handle é usado exatamente uma vez, que um saldo nunca fica negativo, que dois processos seguem o mesmo protocolo, que uma função está correta. Cada promessa é invocada por um decorator ou por um tipo, e nada disso encosta em código que não pediu.

Desenhado, ainda não implementado

A camada de verificação está totalmente desenhada (documento de design §21 e o guia de verificação), mas o compilador mk ainda não a checa. Os trechos abaixo mostram a linguagem-alvo. Use-os para aprender o modelo, não para testar o compilador.

A escada

Toda garantia tem a mesma forma: uma obrigação sobre um predicado. “Este índice está dentro do bound” é o predicado i < len. O trabalho do compilador é descarregar cada obrigação, da forma mais forte que conseguir:

Degrau	Como é descarregada	Exemplo
0	Nível-de-tipo: o estado ruim não pode ser escrito	um @must_consume dropado
1	Dobra em comptime: o compilador calcula a resposta	Index[8] com o literal 3
2	Prova invocada: uma extensão prova (SMT, model checker)	um refinamento com aritmética dinâmica
3	Checagem em runtime: um trap na violação	@requires, um refinamento que chegou a runtime
4	Consultivo: um aviso, sem custo inserido	as dicas do analisador de memória
5	Humano: você afirma, por escrito	assume "…"

Uma regra mantém tudo honesto:

Uma obrigação que não pode ser cumprida num degrau cai para o de baixo. Nunca para fora da escada.

Um refinamento que o solver não prova vira uma checagem de runtime. Uma checagem de runtime que você não pode pagar num caminho quente vira um assume com o seu nome. A garantia degrada às claras, e a linguagem te diz em qual degrau ela parou.

Usar uma coisa o número certo de vezes

Dois decorators num decl dizem quantas vezes um valor pode ser consumido:

• @must_consume: exatamente uma vez (linear). Esquecer é o bug.
• @consume_once: no máximo uma vez (afim). Pode ficar sem uso, mas nunca usado duas vezes.

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) }
    // ERRO: no caminho else, t nunca é consumida
}

É a análise de @transfer do capítulo 08, levada do parâmetro para o próprio tipo. O programa errado não compila, então não sobra nada para checar em runtime (degrau 0).

Indexe o tipo por um estado e você ganha typestate de graça:

decl File[s: FileState] @must_consume { fd: i32 }
fn open(path: string) -> File[Open]
fn close(f: File[Open] @consume) -> File[Closed]   // só um File aberto, e só uma vez

Fechar um File[Closed] não passa no typecheck. Não existe flag de “já fechado” para esquecer.

Tipos que carregam uma promessa

Um refinamento é um tipo mais um predicado que os valores dele sempre satisfazem. Ele é escrito com @where, e o valor é nomeado do mesmo jeito que o @ensures nomeia o retorno: pelo tipo, ou por um slot nomeado.

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

Um NonEmpty[T] entra em qualquer lugar que espera um List[T], mas não o contrário. Dentro de uma guarda, o checker estreita o tipo:

fn first[T](xs: NonEmpty[T]) -> T {
    return xs[0]                        // sem checagem de bound, sem Optional
}

let ys: List[int] = read_input()
// first(ys)                            // ERRO: List[int] não é NonEmpty[int]
if ys.len > 0 { first(ys) }             // OK: a guarda estreitou ys

Um literal se resolve em comptime (degrau 1). Aritmética dinâmica vai para a extensão SMT (degrau 2), e o que ninguém consegue provar vira checagem de runtime (degrau 3).

Cercas: pure e total

• @pure: sem efeitos colaterais. Mesmas entradas, mesma saída, nada de fora alterado.
• @total: definida para toda entrada e sempre termina.

As duas são inferidas por padrão. Escrever o decorator é exigir a checagem:

@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)
    }
}

O match exaustivo já impede que a função trave; o @total acrescenta a prova de terminação. Uma função comptime usada dentro de um tipo precisa ser @total, e é isso que impede um tipo de travar o compilador.

Um protocolo que o compilador percorre

O tipo de um channel diz o que pode atravessá-lo. Um tipo de sessão diz também em que ordem, então o deadlock de os dois lados esperarem vira erro de compilação. A Makoto escreve isso com palavras que você já conhece:

@protocol decl KVServer {
    loop {
        @receives match {                 // o cliente escolhe a operação a cada rodada
            Get  => { Key @receives;  Value @sends;   continue }
            Put  => { Key @receives;  Value @receives;  Ack @sends;  continue }
            Quit => _                     // sai do loop: a sessão termina
        }
    }
}

@receives match quer dizer que o outro lado escolhe o ramo; @sends match, que você escolhe. Você escreve o protocolo uma vez, de um lado só. O outro lado é o espelho, dual, e o spawn checa que as duas pontas se encaixam:

let c: Channel[Auth]        // o cliente segura Auth
spawn server(ch)            // ch: Channel[dual Auth]

Um Channel[T] comum continua um cano tipado. Só um channel tipado por um @protocol é percorrido como sessão.

Tipos que mencionam valores

Você já escreveu [N]T. Value-params num decl levam isso adiante, sem sintaxe nova:

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]

Isso já dá segurança de comprimento, de bound e unidades de medida. Atrás de @proof, a mesma maquinaria vira um assistente de provas: uma proposição é um tipo, e uma prova é um programa que tem esse tipo.

@proof @total fn zero_right(n: Nat) -> Eq[Nat, add(n, 0), n] {
    match n {
        Zero    => Refl
        Succ(k) => cong(Succ, zero_right(k))   // a indução é o match mais a chamada recursiva
    }
}

Provar um design

Provas verificam uma implementação. Model checking verifica um design: explora os estados de uma subárvore supervisionada e checa propriedades globais. Ele mora numa extensão, porque o motor muda com o estado da arte:

// safety: nunca existe mais de um líder por termo
@spec(count(nodes, |n| n.role == Leader && n.term == cur) <= 1)

// liveness: todo pedido submetido acaba commitado
@spec(spec.always(spec.implies(submitted(req), spec.eventually(committed(req)))))

Quando nada mais serve

O último degrau é você. O assume (capítulo 10) afirma sem checar, por escrito, na operação que precisa dele. Nunca é silencioso e nunca é licença para comportamento indefinido. É a garantia caindo para a forma honesta mais forte que sobrou.

O que levar daqui

Você escreve	Você ganha	Degrau usual
@must_consume / @consume_once	usado exatamente / no máximo uma vez	degrau 0
@where(pred)	um valor satisfaz um predicado	degrau 1, 2 ou 3
@pure / @total	sem efeitos / termina	degrau 0
@protocol, @sends / @receives, dual	um protocolo é seguido, sem deadlock	degrau 0
value-params, @proof	comprimentos e bounds hoje, provas completas opt-in	degrau 0 ou 1
@spec	safety e liveness globais	degrau 2

Para cada termo, cada degrau e o raciocínio por trás, leia o espectro de verificação.