O espectro de verificação

O companheiro da seção 21 do documento de design. Aquela seção especifica a camada de verificação; esta a explica — cada termo, por que existe, e como você de fato usa, com exemplos trabalhados. É um guia, não uma spec: onde os dois divergirem, o documento de design vence.

Makoto é feita para sistemas que não podem falhar. “Não pode falhar” é uma promessa, e uma promessa só é honesta se algo pode checá-la. Este documento é sobre a maquinaria que deixa você declarar uma garantia e o compilador descarregá-la — de “este handle é usado exatamente uma vez” até “este kernel está provado correto” — sem que nada disso vaze para o código de quem nunca pediu.

Tudo aqui obedece ao teste opt-in (seção 1 do design): você só paga pelo que invoca. Não existe um modo de verificação. Existe um espectro de garantias, cada uma invocada por um decorador ou um tipo, cada uma invisível até você buscá-la. Um programa que não quer nada disso não escreve nada disso e não lê nada disso.

---

1. A ideia única: a escada de descarga

Uma garantia em Makoto tem sempre a mesma forma: uma obrigação sobre um predicado. “Este índice está dentro do bound” é o predicado i < len; “esta transação está commitada ou revertida” é um predicado sobre um protocolo; “reverter uma lista duas vezes dá a original” é um predicado sobre uma função. O trabalho do compilador é descarregar cada obrigação — torná-la verdadeira, prová-la, checá-la ou, na falta de tudo isso, te fazer assinar por ela.

Há uma escada de jeitos de descarregar uma obrigação, do mais forte ao mais fraco:

Degrau	Como a obrigação é descarregada	Exemplo
0	Nível-de-tipo — o estado ruim não pode ser escrito	um @must_consume dropado; Vec[T, 0].head
1	Dobra em comptime — o compilador calcula a resposta	Index[8] com o índice literal 3
2	Prova invocada — uma extensão prova (SMT, model checker)	refinamento com aritmética dinâmica, uma propriedade de liveness
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 "…" (seção 5)

A única regra que torna isso seguro:

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 SMT não prova não desaparece; vira uma checagem de runtime. Uma checagem de runtime que você não pode pagar num caminho quente não desaparece; vira um assume com seu nome. A garantia sempre degrada para a forma honesta mais forte ainda disponível, e a linguagem te diz, na cara, em qual degrau você parou. Essa honestidade é o ponto todo — o nome Makoto (誠, “verdade”) é a recusa a esconder onde uma garantia para.

O resto deste documento são os degraus, uma família por vez.

---

2. Posse: usar uma coisa o número certo de vezes

Os termos. Duas palavras da teoria de tipos, e são mais simples do que parecem:

• Linear — deve ser usada exatamente uma vez. Nem zero (esquecê-la é um bug), nem duas.
• Affine — deve ser usada no máximo uma vez. Pode ficar sem uso, mas nunca duas vezes.

Makoto as nomeia pelo que fazem, e guarda a palavra da teoria para a doc:

• @must_consume = linear. Você tem que consumir isto. Uma transação de banco que você tem que commitar ou reverter — sair de um escopo com ela ainda aberta é o erro.
• @consume_once = affine. Você pode consumir isto uma vez. Um buffer de rascunho que você pode ou não usar, mas nunca liberar duas vezes.

Por que existe. A seção 5 já move posse numa fronteira: @transfer move um valor para fora, e um parâmetro @consume come seu argumento. Mas esses moram no ponto de uso — um parâmetro, uma expressão. Às vezes a disciplina pertence à própria coisa, aonde quer que ela vá. Um handle de conexão deveria carregar “use-me exatamente uma vez” no seu tipo, de modo que nenhuma função em lugar nenhum possa esquecê-lo. É isso que os decoradores nível-de-tipo adicionam: a mesma flow-analysis, elevada do parâmetro para o decl.

Como você usa.

decl Transaction @must_consume { conn: *Connection }   // toda Transaction DEVE ser consumida exatamente uma vez
decl Scratch      @consume_once { buf: [*]u8 }          // um Scratch pode morrer sem uso, mas nunca ser usado duas vezes

fn commit(t: Transaction @consume)   { … }              // consome (degrau 0: o tipo agora está gasto)
fn rollback(t: Transaction @consume) { … }

fn handle(t: Transaction) {
    if ok { commit(t) }
    // ERRO: no caminho else, t nunca é consumida — @must_consume quebrado
}

A checagem é a análise do @transfer da seção 5 rodada sobre a vida inteira do valor: chegar ao fim de um escopo com um @must_consume não consumido é erro, e um segundo uso de qualquer tipo é erro. Isso é uma garantia de degrau 0: o programa errado não compila, então não há nada a checar em runtime.

Typestate de graça. Uma “máquina de estados no tipo” — um arquivo que é Open e depois Closed, um socket Unbound e depois Listening — é só um tipo @must_consume indexado por um valor de estado (os value-params da seção 10), com funções que o percorrem:

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

Chamar close num File[Closed] não compila. Sem flag em runtime, sem exceção “já fechado” — o erro é irrepresentável.

---

3. Refinamentos: um tipo que carrega uma promessa

O termo. Um tipo refinado é um tipo mais um predicado que seus valores garantidamente satisfazem. Um NonEmpty[T] é um List[T] que além disso nunca é vazio. Um Balance é um i64 que nunca é negativo. O predicado é parte do tipo, então uma vez que um valor tem o tipo, a promessa já está mantida.

Por que existe. Dois motivos. Primeiro, ele deleta categorias inteiras de checagem em runtime e de Optional: uma função que recebe um NonEmpty[T] nunca precisa perguntar “e se for vazio?”, porque não pode ser. Segundo, ele unifica com os contratos que você já tem — um @where num tipo é um @requires/@ensures (seção 14) que viaja com o tipo em vez de ficar preso a uma função.

O binder — e de onde ele vem. É a parte que as pessoas erram, então vale ser exato. O predicado precisa nomear o valor que restringe. Makoto não inventa uma variável mágica para isso (nada de it). Ele reusa os dois devices que a seção 14 já tem para nomear valores:

• Referência-por-tipo (o default, sem binder). Exatamente como @ensures(u8 > 0), onde a pós-condição nomeia o retorno pelo tipo porque o tipo é o slot:

  alias Balance         = i64   @where(i64 >= 0)
  alias Index[n: usize] = usize @where(usize < n)

• Slot nomeado (quando o tipo-base é genérico ou longo). Exatamente como um retorno nomeado -> (lo: u8) na seção 14, o slot (xs: List[T]) introduz o nome xs, cujo tipo está escrito ali:

  alias NonEmpty[T] = (xs: List[T]) @where(xs.len > 0)

Então xs não é mágico e não é não-declarado — ele é ligado em (xs: List[T]), do mesmo jeito que lo é ligado em -> (lo: u8). O caso simples não precisa de binder nenhum; só o caso genérico paga por um.

Como descarrega. O predicado é uma expressão comptime que o checker consome (não é uma função guardada). A subtipagem segue a implicação: T @where(P) é subtipo de T @where(Q) exatamente quando P ⟹ Q, então um NonEmpty[T] flui aonde um List[T] é esperado, mas não o contrário. Dentro de um guard o checker estreita — depois de if xs.len > 0 { … }, o xs no braço tem tipo NonEmpty[T]. E a obrigação anda na escada: decidida por dobra em comptime é degrau 1; precisando de aritmética dinâmica cai para a extensão SMT (degrau 2, seção 7) ou para uma checagem de runtime (degrau 3).

fn first[T](xs: NonEmpty[T]) -> T {
    return xs[0]                        // sem bounds-check, sem Optional: o tipo já provou não-vazio
}

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

---

4. Cercas: pure e total

Os termos.

• Uma função pura não tem efeitos colaterais: dadas as mesmas entradas, sempre retorna a mesma saída e não muda nada fora de si.
• Uma função total é definida em toda entrada (nunca trava) e sempre termina (nunca loopa para sempre).

Por que existem. Por si só são promessas úteis. Mas o trabalho de verdade delas é ser a cerca em volta da camada de tipos dependentes (seção 6). Um tipo que menciona um valor computado — Vec[T, factorial(n)] — só faz sentido se factorial de fato termina de computar em tempo de compilação. Uma “prova” que secretamente loopa para sempre não prova nada. Então pureza e totalidade são as condições que tornam computação-de-tipo e provas sound, e a cerca é onde o compilador insiste nelas.

Como você usa. Elas ficam no mesmo slot de @requires/@ensures, e são inferidas por default — o compilador já sabe se seu corpo toca um efeito e se sua recursão encolhe seu argumento. Escrever o decorador é você demandar a checagem (degrau 0), do mesmo jeito que o @requires declara uma pré-condição:

@pure  fn area(r: f64) -> f64 { return 3.14159 * r * r }        // sem IO, sem alocação, sem spawn
@total fn len[T](xs: List[T]) -> usize {                         // recursão estrutural → termina
    match xs {
        Nil        => 0
        Cons(_, t) => 1 + len(t)
    }
}

A metade exaustividade da totalidade já é de graça: a seção 14 força o match a cobrir todo caso, então uma função @total não pode travar; o decorador só adiciona a terminação (recursão estrutural, ou uma medida que provadamente decresce). Uma função comptime usada num tipo precisa ser @total — é a regra que impede um tipo de travar o compilador, e a razão de a camada dependente poder ser confiada.

---

5. Tipos de sessão: um protocolo que o compilador percorre

O termo. Um tipo de sessão é o roteiro de uma conversa sobre um canal: quem envia o quê, em que ordem, quem decide em cada bifurcação, e quando ela acaba. Um endpoint de canal tipado por uma sessão é um typestate linear — você é obrigado a seguir o roteiro até o fim, e o compilador checa que você segue.

Por que existe. A seção 4 já tipa o payload de um canal e checa um contrato no spawn. Mas um tipo de payload diz o quê pode cruzar, não em que ordem — e errar a ordem (os dois lados esperando receber) é um deadlock. Um protocolo torna a ordem parte do tipo, então um descompasso é erro de compilação em vez de um processo travado.

Sem símbolos crípticos. Tipos de sessão vêm de papers de cálculo de processos cheios de !, ?, &, +. Makoto usa palavras, e reusa construções que você já conhece — match para uma escolha, loop/continue para recursão, _ para o fim:

@protocol decl Auth {                    // descreve UM endpoint (aqui, a visão do cliente)
    Credentials @sends                   // eu envio Credentials, então…
    @receives match {                     // …um tag CHEGA, então o PEER escolhe; eu trato cada arm
        Ok   => Token  @receives
        Deny => Reason @receives
    }
}

• @sends / @receives são postfix num tipo (consistente com *T @consume): Token @receives significa “eu recebo um Token aqui.”
• A direção num match diz quem escolhe o braço:
  • @receives match — o tag chega, então o peer decide e eu trato cada arm (escolha externa: eu reajo ao que ele escolheu).
  • @sends match — eu emito o tag, então eu decido qual arm dirigir (escolha interna).
• Recursão é loop + continue; o fim do protocolo é cair fora do bloco (ou um _ puro):

@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 => _                     // sem continue → sai do loop → a sessão acaba
        }
    }
}

O outro lado, de graça. Você escreve o protocolo uma vez, do ponto de vista de um endpoint. O outro endpoint é o seu dual — todo @sends vira @receives e vice-versa (inclusive @sends match @receives match). dual é um operador-de-tipo comptime (não um decorador — ele produz um tipo diferente, não anota um), e o contrato-no-spawn da seção 4 checa que os dois lados batem:

let c: Channel[Auth]        // o cliente segura Auth
spawn server(ch)            // ch: Channel[dual Auth] — o compilador deriva o espelho e checa que alinha

Endpoints descompassados simplesmente não compilam, então essa classe de deadlock é uma garantia de degrau 0.

Opt-in, mesmo aqui. Um Channel[T] puro continua só um cano tipado sem obrigação de sessão. Só um canal tipado por um @protocol — Channel[Auth] — é percorrido como sessão. O caso simples fica simples; você invoca a disciplina exatamente onde uma conversa vale ser fixada.

---

6. Tipos dependentes: tipos que mencionam valores

O termo. Um tipo dependente é um tipo que depende de um valor. Vec[T, 3] (um vetor de exatamente três Ts) é um tipo que menciona o número 3. Eq[Nat, x, y] (uma prova de que x é igual a y) é um tipo que menciona dois números. Uma vez que tipos podem mencionar valores, o type checker pode forçar fatos sobre valores — “estes dois vetores têm o mesmo comprimento”, “este índice está abaixo do bound” — em tempo de compilação.

Tipos dependentes não são novos nem experimentais. São teoria de décadas, bem-entendida (Martin-Löf nos anos 1970; Coq, Agda, Lean e Idris os entregam em produção). Pela própria régua do design doc — o estável fica no core, o volátil vira extensão (seção 20) — eles pertencem ao core, opt-in-por-uso, como @supervisor. Makoto os divide em dois tiers.

6.1 A camada prática (disponível hoje)

Um tipo indexado-por-valor é só um struct sobre os value-params que a seção 10 já tem:

decl Vec[T, n: usize] { data: [n]T }                                             // um vetor cujo comprimento n está no seu tipo
fn concat[T, n: usize, m: usize](a: Vec[T, n], b: Vec[T, m]) -> Vec[T, n + m]    // o comprimento do resultado é n + m, checado

Não há sintaxe nova aqui e não há “GADT”: um decl[…] já é açúcar para um comptime fn(…) -> type (seção 10), então Vec[int, 3] é uma chamada em tempo de compilação que produz um struct concreto. Este tier já compra segurança-de-comprimento, segurança-de-bounds, e unidades-de-medida (um Meters e um Seconds que não podem ser somados). “Não-vazio” neste tier é um refinamento @where (seção 3), não um índice.

6.2 A camada de prova (cinco adições ao core, cercadas por @proof)

Para ir de “dado indexado” a “lógica provada”, o core ganha cinco coisas — três de gramática, duas do checker — todas que só ligam sob @proof:

• D1 — value-param dependente [x: A]. Hoje um value-param é tipado por um tipo concreto ([n: usize]). D1 deixa ele ser tipado por um type-param anterior ([A, x: A]). É o mesmo […] que você já escreve, um passo mais geral, e fica ao lado do higher-kinded C[_] — ambos são só formas de parâmetro genérico. É isso que deixa um tipo mencionar um valor de um tipo arbitrário.
• D2 — um kind no cabeçalho, -> Kind. Uma declaração pode dizer o que produz: decl Vec[T, n: usize] -> type (o -> type é o default e costuma ser omitido), ou @proof decl Eq[…] -> prop. O -> reusa “produz” (um type-former produz um type, o -> type da seção 10); : continua significando binding de campo-e-parâmetro e nada mais. prop é um universo novo ao lado de type: uma proposição, um tipo cujo habitante é uma prova.
• D3 — variantes com um tipo-de-resultado (famílias indexadas / GADTs). Num decl dependente, uma variante pode dizer qual índice produz, escrita com as formas de campo e de tipo-função que já existem:

  @proof decl Vec[T, n: usize] -> type {
      Nil:  Vec[T, 0]                                        // o vetor vazio tem comprimento 0
      Cons: fn[m: usize](head: T, tail: Vec[T, m]) -> Vec[T, m + 1]   // adicionar um faz virar m + 1
  }

  Não é uma quarta forma de decl; é a forma campo-de-struct (Nome: Tipo) e a forma tipo-função (fn[…](…) -> …) relidas como variantes-que-refinam-índice quando o head é dependente.
• D4 — definitional equality (um poder do checker, sem sintaxe nova). Para qualquer coisa acima significar algo, o checker precisa decidir quando dois índices computados são o mesmo tipo: ele normaliza expressões comptime sobre value-params ligados (não só dobrando literais) e compara a-menos-de-computação, de modo que Vec[T, add(n, 0)] e Vec[T, n] são um tipo só. Este é o verdadeiro kernel da tipagem dependente, e a única peça grau-de-pesquisa — tornada sound pelas cercas @total/@pure da seção 4.
• D5 — campos dependentes (Σ) e parâmetros dependentes (Π). Um campo posterior pode mencionar o valor de um campo anterior, e um parâmetro posterior um parâmetro anterior, reusando a gramática de struct e de parâmetro sem tocar:

  decl Sized { n: usize; data: [n]int }      // um "par dependente / Σ": o tipo de data depende de n
  fn take(n: usize, xs: [n]int) -> [n]int    // uma "função dependente / Π": o tipo de xs depende de n

Σ e Π, em bom português. Um tipo Σ (sigma) é um par onde o tipo da segunda coisa depende do valor da primeira — “um número n, junto com um vetor daquele comprimento n”. Um tipo Π (pi) é uma função cujo tipo de retorno depende do valor do argumento — “me dá um n, eu retorno um array de tamanho n”. Você já vem escrevendo um Π restrito toda vez que escreveu fn zeros[N: usize]() -> [N]int; D5 só deixa a dependência cruzar parâmetros de runtime também.

@proof é a cerca, e traça a linha entre dado e lógica. Uma família indexada usada como dado é sound no core sem cerca nenhuma — não é mais perigosa que qualquer tipo recursivo. Ela precisa de consistência lógica (total, pura, estritamente-positiva) só quando você pretende confiar nela como prova. Essa intenção é @proof, que implica @total, @pure e positividade-estrita. Sem @proof, Vec é dado rico; com ela, Eq é lógica confiável.

6.3 Uma prova é um programa

Igualdade não é built-in; é uma família indexada comum (D1–D3), e uma prova dela é uma função recursiva comum. Isto é a correspondência de Curry–Howard, dita direto: uma proposição é um tipo, e uma prova dela é um valor daquele tipo; provar um teorema é escrever um programa que tem o tipo dele.

@proof decl Eq[A, x: A, y: A] -> prop {
    Refl: fn[a: A]() -> Eq[A, a, a]        // o único jeito de construir uma igualdade é reflexividade: a igual a a
}

@proof @total fn zero_right(n: Nat) -> Eq[Nat, add(n, 0), n] {
    match n {
        Zero    => Refl                        // caso base: add(0, 0) normaliza para 0 (D4), então Eq[Nat, 0, 0], e Refl serve
        Succ(k) => cong(Succ, zero_right(k))   // passo: assume que vale para k, conclui para k + 1
    }
}

Leia o passo como indução, porque é exatamente isso: a indução é o match mais a chamada recursiva, e @total é o que garante que a recursão é bem-fundada — que é precisamente o que torna a indução válida. cong (“congruência”: se a = b então f(a) = f(b)) é ela mesma uma pequena @proof fn numa proof-stdlib — um valor de library, não sintaxe. Não há keyword theorem e não há linguagem de táticas no core; uma prova é uma função, os arms são =>, e é só isso.

---

7. Model checking: provar coisas sobre um design

O termo. Onde uma prova (seção 6) verifica uma implementação, o model checking verifica um design: ele explora os estados alcançáveis de um sistema de processos comunicantes e checa propriedades globais e temporais — safety (“algo ruim nunca acontece”: nunca dois líderes ao mesmo tempo) e liveness (“algo bom acontece no fim”: toda requisição é eventualmente respondida).

Por que é uma extensão, não core. Este é o único membro do espectro que mora numa extensão (seção 20), e pela razão exata da régua de extensão: o engine é volátil. Bounded model checking, heurísticas de state-explosion, e pontes para checkers externos (emitir P ou TLA⁺ como alvo de codegen) mudam com o estado da arte — diferente da teoria de tipos dependentes, que é estável. Então o model checking adiciona um decorador, uma library comptime, um pass e um alvo de codegen, e não toca em nada no core.

Como você usa.

// safety: um predicado booleano comum, "always" é implícito
@spec(count(nodes, |n| n.role == Leader && n.term == cur) <= 1)

// liveness: uma fórmula temporal feita de palavras de library, não símbolos □/◇
@spec(spec.always(spec.implies(submitted(req), spec.eventually(committed(req)))))

Safety lê no vocabulário de @requires/@where. Liveness usa spec.always / spec.eventually / spec.implies / spec.leads_to, que são funções de library comptime (metaprogramming is a library, seção 10) em vez dos □/◇ da lógica temporal. Um @spec ancora num @supervisor (seção 8), cuja subárvore de processos já limita o que checar; o pass lê o grafo de spawn-e-canais daquela subárvore e o explora.

(O nome guarda-chuva é @spec, cobrindo safety e liveness. O óbvio @property está tomado — é o decorador de property-based-testing da extensão de testes.)

---

8. Táticas: escrever provas sem escrever cada termo

A prova de um teorema real pode ser um termo grande. Uma tática é um comando que constrói esse termo transformando o goal atual (a proposição que falta provar, mais as hipóteses em escopo): induction n quebra o goal num caso base e num caso passo; simp fecha goals que valem por computação; rewrite h usa uma equação que você já tem. Makoto chega às táticas em tiers, e é cuidadosa sobre o que, se algo, elas custam ao core.

• Tier 0 — prova-como-termo (hoje). Você escreve a prova direto, como o zero_right na seção 6.3. Para reflexividade e provas estruturais isso é curto e não precisa de nada novo.
• Tier 1 — táticas como library. Táticas são funções comptime sobre um Goal de 1ª classe (assim como reflect expõe estrutura de tipo, seção 10): induction, simp, rewrite, e os combinadores first/try/repeat, cada um fn(Stack) -> Result[Stack, TacticError]. Compostas à mão, não precisam de gramática nova — são Makoto comum.
• Tier 2 — @by (diferido). A forma ergonômica é um bloco cujos statements threadam o goal:

  return @by { induction(xs); simp; rewrite(ih) }

Por que @by é um decorador, não uma keyword. Uma keyword by reservaria o identificador em todo programa — ninguém poderia nomear uma variável ou função by de novo. Um decorador vive no namespace do @, então by continua um identificador livre; só @by é especial. É escrito prefixo, como @mm(arena) { … } (seção 5), porque você tem que saber que um bloco está em modo-tática antes de ler seus statements.

Por que é um delta de core mesmo assim (não uma library). Um bloco cujos statements threadam um goal implícito é semântica de bloco nova, e uma library não pode adicionar gramática ou semântica (seção 20). Então @by é ou core ou uma extensão de compilador — nunca uma library pura. O compromisso é mantido mínimo: @by { s1; s2; … } desugara para threadar um valor Stack definido por library através dos statements, semeado pelo tipo esperado e curto-circuitando no erro. Todo o resto — Goal, Stack, cada tática, cada combinador — é uma library comum, então a parte volátil (quais táticas existem, como compõem) churna livremente sem tocar no core.

Onde ele aterrissa: self-hosting. Quando o compilador for escrito em Makoto e importável (use compiler), o AST vira um tipo de library normal, e @by vira um macro preso-a-bloco: um decorador que recebe seu próprio bloco governado como AST comptime e devolve um valor. Essa restrição é o trilho de segurança — um macro assim reinterpreta um bloco ao qual está preso; nunca inventa sintaxe top-level nova — que é o que o impede de virar o “decorator/DSL hell” que a linguagem rejeita. Três problemas difíceis vêm com essa era, e são nomeados de antemão para não serem descobertos tarde:

1. Higiene — um binding que um macro introduz nunca pode capturar ou colidir com um nome do usuário.
2. Estabilidade da API de AST — o tipo de AST refletido agora é um contrato público; mudá-lo quebra todo macro.
3. Atribuição de erro — um erro dentro do código expandido tem que apontar para a fonte do usuário, não a do macro.

Até o self-hosting, Makoto entrega Tier 0 e Tier 1, com a library de Tier 1 escrita no formato final (Goal, Stack, induction/simp/rewrite, first/try/repeat) para que @by depois simplesmente a embrulhe, sem retrabalho.

---

9. O espectro inteiro numa página

Família	Você escreve	Garante	Casa	Degrau usual
Posse	@must_consume / @consume_once	usado exatamente / no máximo uma vez	core (estende §5)	0
Refinamento	@where(pred) num tipo	um valor satisfaz um predicado	core	1 2 3
Cercas	@pure / @total	sem efeitos / termina	core	0
Sessões	@protocol + @sends/@receives + dual	um protocolo é seguido, sem deadlock	core (completa §4)	0
Dependente (prático)	value-params + @where	comprimentos, bounds, unidades	core (hoje)	0–1
Dependente (prova)	@proof + D1–D5	correção funcional plena	core, opt-in	0
Model checking	@spec + spec.*	safety / liveness global	extensão (§20)	2
Táticas	@by { … } (depois)	ergonomia de prova	delta de core, diferido	—

A linha que costura tudo: uma escada, obrigações descarregadas o mais alto que dá, e nada jamais forçado sobre código que não invocou. O proof-assistant está no core porque sua teoria é antiga e assentada; o model checker é uma extensão porque seu engine não é; e nenhuma garantia jamais cai para fora da escada — ela degrada, na cara, para a forma honesta mais forte que sobra. 誠.