Verificação

Makoto é uma linguagem para sistemas que não podem falhar, e o jeito honesto de merecer o “não pode falhar” é deixar o programador declarar uma garantia e o compilador descarregá-la. Esta seção é o espectro de garantias: disciplinas de posse, refinamentos, protocolos de sessão, cercas de efeito e terminação, tipos dependentes e provas, e model checking. Nada disso é um modo em que você coloca a linguagem; cada peça é opt-in (seção 1), invocada por um decorador ou um tipo e invisível ao código que não pede. A espinha é uma única ideia — a escada de descarga (discharge ladder) — e todo o resto é um degrau dela.

A escada de descarga

Toda garantia em Makoto é uma obrigação sobre um predicado, e toda obrigação é descarregada no degrau mais alto que a sustenta. É o “borrow-checker que você consulta” da seção 5 generalizado: a análise é conselho com dentes, e a linguagem sempre te diz, na cara, onde uma dada garantia de fato para.

Os degraus, do mais forte ao mais fraco:

• Degrau 0 — nível-de-tipo. O tipo torna o estado ruim irrepresentável. Um handle @must_consume que é dropado é erro de compilação; um Vec[T, 0] não tem head. Nada a checar em runtime, porque o programa errado não compilou.
• Degrau 1 — dobra em comptime. O predicado é decidido pelo compilador dobrando valores conhecidos (Index[8] onde o índice é o literal 3). É o motor do degrau 0 aplicado a valores, não a formas.
• Degrau 2 — descarga invocada. Uma extensão (SMT para refinamentos aritméticos, um model checker para propriedades temporais) prova a obrigação. Opt-in atrás de flag ou use; veja @spec abaixo e a seção 20.
• Degrau 3 — checagem em runtime. A obrigação não pôde ser provada estaticamente, então vira uma checagem que trapa na violação (@requires/@ensures, um refinamento que sobreviveu até runtime).
• Degrau 4 — consultivo. O checker não decide e não insere custo; ele avisa (as camadas dica/warning do analisador de memória).
• Degrau 5 — humano. assume (seção 5): você afirma o predicado sob sua própria autoridade, por escrito, e assume a consequência.

A regra que torna a escada segura: uma obrigação que não pode ser descarregada num degrau cai para o degrau de baixo, nunca para fora da escada. Um refinamento que o SMT não prova vira checagem de runtime; uma checagem de runtime que você não pode pagar vira um assume que você assinou. A garantia nunca some em silêncio; ela degrada, visivelmente, para a forma mais fraca-porém-honesta que sobra.

Posse como disciplina de tipo: @must_consume, @consume_once

(estende a seção 5; funciona sobre a flow-analysis existente.) A seção 5 já move posse na fronteira com @transfer (um move em posição de valor) e @consume (um parâmetro que come seu argumento). Dois decoradores nível-de-tipo elevam a mesma flow-analysis do parâmetro para o tipo, de modo que um recurso carrega sua disciplina aonde quer que vá:

decl Transaction @must_consume { conn: *Connection }   // linear: toda instância DEVE ser consumida exatamente uma vez
decl Scratch      @consume_once { buf: [*]u8 }          // affine: consumida no máximo uma vez (pode simplesmente morrer)

@must_consume é linearidade (exatamente uma vez — dropar sem consumir é erro, então uma transação não pode ser esquecida em silêncio). @consume_once é afinidade (no máximo uma vez — pode ficar sem uso, mas nunca ser usada duas vezes, então um buffer liberado não pode ser liberado de novo). A checagem é a flow-analysis do @transfer rodada sobre a vida do tipo: chegar ao fim de um escopo com um valor @must_consume não consumido é o erro; um segundo uso de qualquer um dos dois é o erro. Typestate compõe com isso de graça via os value-params da seção 10 — File[Open] e File[Closed] são um tipo @must_consume indexado por um estado, e fn close(f: File[Open] @consume) -> File[Closed] o percorre. (As user-docs nomeiam a teoria: @must_consume é linear, @consume_once é affine.)

Refinamentos: @where

(delta de core novo: um tipo pode carregar um predicado.) Um refinamento é um tipo mais um predicado que seus valores satisfazem. Ele se unifica com os contratos da seção 14 — um @where num tipo é um @requires/@ensures que viaja com o tipo em vez de sentar numa função — e usa o próprio device da seção 14 para nomear o valor. Há duas formas, e a simples não carrega binder nenhum:

alias Balance         = i64   @where(i64 >= 0)              // referência-por-tipo: o valor é seu tipo, como @ensures(u8 > 0)
alias Index[n: usize] = usize @where(usize < n)             // idem, com um value-param em escopo

alias NonEmpty[T]     = (xs: List[T]) @where(xs.len > 0)    // slot nomeado: (xs: List[T]) declara xs, exatamente como um retorno nomeado

A forma referência-por-tipo é o default e espelha @ensures(u8 > 0), onde a pós-condição nomeia o retorno pelo tipo porque o tipo é o slot. A forma slot-nomeado é o mesmo movimento de um retorno nomeado -> (lo: u8) da seção 14: quando o tipo-base é genérico ou verboso, (xs: List[T]) introduz o nome xs cujo tipo está escrito ali mesmo — sem variável mágica, sem it. Não há terceiro sentido para :; é binding de campo-e-parâmetro como sempre.

O predicado é uma expressão comptime que o checker consome (como o @requires), não um valor-função guardado. A subtipagem segue a implicação — T @where(P) é subtipo de T @where(Q) exatamente quando P ⟹ Q — e dentro de um guard o checker estreita: depois de if xs.len > 0, um xs flui como NonEmpty. A descarga anda na escada: um refinamento decidido por dobra em comptime é degrau 1; um que precisa de aritmética dinâmica cai para a extensão SMT (degrau 2) ou para uma checagem de runtime (degrau 3). O ganho é que bounds-checks e Optional somem onde o tipo já provou.

Cercas: @pure, @total

(delta de core novo: duas análises do checker.) Dois decoradores declaram promessas sobre como uma função computa, no mesmo slot de @requires/@ensures, checadas pelo compilador e invisíveis a quem não as lê:

• @pure — análise de efeito: sem @mm(alloc/free), sem spawn ou canal, sem FFI, sem IO, sem mutação externa, sem runtime.panic. O corpo é uma função matemática das suas entradas.
• @total — terminação e totalidade. A seção 14 já força o match a ser exaustivo, então a metade “definida em toda entrada” é de graça; @total adiciona a outra metade, a terminação (recursão estrutural ou uma medida bem-fundada decrescente), e recusa um loop sem medida decrescente.

Ambos são inferidos por default e demandados pelo decorador: o compilador já sabe se um corpo toca efeito e se uma recursão é estrutural, então escrever @pure/@total é você declarar a obrigação (degrau 0) para o compilador verificar, exatamente como o @requires declara uma pré-condição. Eles são obrigatórios em qualquer função comptime usada em posição de tipo: um tipo como Vec[T, factorial(n)] só é sound se factorial terminar em tempo de compilação, então a cerca é o que impede uma função comptime de travar o compilador e, ao mesmo tempo, o que torna a camada dependente abaixo sound.

Tipos de sessão: @protocol, @sends, @receives, dual

(delta de core novo; completa a seção 4.) Um canal conecta dois processos, e a seção 4 já checa um contrato no spawn. Um protocolo promove o endpoint de um canal a um typestate linear: um roteiro de envios e recebimentos que o checker percorre e te obriga a completar. Ele é escrito com palavras, nunca os !/?/&/+ dos papers de cálculo de processos, e reusa match, loop, continue e _ do core:

@protocol decl Auth {                    // descreve UM endpoint; o peer recebe o espelho automaticamente
    Credentials @sends                   // eu envio Credentials, então...
    @receives match {                     // ...eu RECEBO o tag → o PEER escolhe; eu trato cada arm (escolha externa)
        Ok   => Token  @receives
        Deny => Reason @receives
    }
}

@protocol decl KVServer {
    loop {
        @receives match {                 // o cliente escolhe a operação (escolha externa para o servidor)
            Get  => { Key @receives;  Value @sends;   continue }
            Put  => { Key @receives;  Value @receives;  Ack @sends;  continue }
            Quit => _                     // sem continue → cai fora do loop → fim
        }
    }
}

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

dual Auth é um operador-de-tipo comptime que produz o endpoint espelhado — todo @sends vira @receives e vice-versa, inclusive @sends match @receives match. Você escreve o protocolo uma vez; o outro lado é derivado:

let c: Channel[Auth]        // o cliente vê Auth
spawn server(ch)            // ch: Channel[dual Auth] — o compilador gera e checa o espelho

dual é um operador e não um decorador porque dual produz um tipo diferente (um decorador só anota o que a coisa já é; dual a transforma), a mesma distinção que mantém computação-de-tipo como List[T] fora do espaço dos decoradores. E crucialmente, a disciplina é opt-in dentro do core: um Channel[T] puro continua um cano comum sem obrigação de sessão; só um canal tipado por um protocolo (Channel[Auth]) é percorrido como sessão. O caso simples fica simples.

Tipos dependentes: @proof e a camada prática

Tipos dependentes — tipos que mencionam valores — são teoria antiga e estável (Martin-Löf, anos 1970; Coq, Agda, Lean, Idris em produção), e por isso, pela régua “o estável fica, o volátil vira extensão” da seção 20, eles pertencem ao core, opt-in-por-uso como @supervisor. Makoto os divide numa camada prática que quase nada precisa de novo, e uma camada de prova cercada por uma cerca.

A camada prática (válida hoje). Um tipo indexado-por-valor é um struct comum sobre os value-params que a seção 10 já tem:

decl Vec[T, n: usize] { data: [n]T }                                  // vetor indexado-por-comprimento; n é um value-param comptime
fn concat[T, n: usize, m: usize](a: Vec[T, n], b: Vec[T, m]) -> Vec[T, n + m]   // n + m é um Expr em posição de type-arg

Isso não é um GADT e não precisa de gramática nova: Vec[int, 3] é uma chamada comptime que produz um struct concreto (um decl[…] é açúcar para um comptime fn(…) -> type, seção 10). Segurança-de-comprimento, segurança-de-bounds e unidades-de-medida já são expressáveis; “não-vazio” nessa camada é um refinamento @where, não um índice.

A camada de prova (cinco deltas, todos cercados por @proof). Tipos dependentes plenos adicionam, sobre a camada prática:

• D1 — value-param dependente [x: A]. Um value-param pode ser tipado por um type-param anterior do mesmo […], não só por um tipo concreto. Generaliza o value-param existente e é simétrico ao HKT C[_]; ambos são só formas de parâmetro genérico. Um value-param dependente puro é sound sem @proof (é um valor comptime monomorfizado, como [n: usize]).
• D2 — um kind no cabeçalho da declaração, via -> Kind. decl Vec[T, n: usize] -> type { … } (o -> type é o default e pode ser omitido); @proof decl Eq[A, x: A, y: A] -> prop { … }. O -> reusa “produz” (um type-former produz um type ou um prop, o -> type da seção 10); : não ganha terceiro sentido. prop é um universo novo ao lado de type (uma proposição cujo habitante é uma prova).
• D3 — uma variante com tipo-de-resultado explícito (famílias indexadas / GADTs). Dentro de um decl dependente, uma variante pode declarar o índice que produz, escrita com as formas de campo e de tipo-função que já existem — uma nulária Nome: TipoResultado, ou um construtor Nome: fn[…](…) -> TipoResultado:

  @proof decl Vec[T, n: usize] -> type {
      Nil:  Vec[T, 0]
      Cons: fn[m: usize](head: T, tail: Vec[T, m]) -> Vec[T, m + 1]
  }

  Não é uma quarta forma de decl; são as formas campo-de-struct e tipo-função relidas como variantes-que-refinam-índice quando o head é dependente.
• D4 — normalização comptime simbólica (definitional equality). O checker normaliza expressões comptime sobre value-params ligados — não apenas dobrando literais — e compara tipos a-menos-de-computação, de modo que Vec[T, add(n, 0)] e Vec[T, n] são o mesmo tipo. Isso não tem sintaxe de superfície; é o kernel que faz D1–D3 significarem algo, e é a única peça grau-de-pesquisa, tornada sound pelas cercas.
• D5 — campos dependentes (Σ) e parâmetros runtime dependentes (Π). O tipo de um campo posterior pode mencionar o valor de um campo anterior, e o tipo de um parâmetro posterior pode mencionar um parâmetro anterior, reusando a gramática de struct e de parâmetro por inteiro:

  decl Sized { n: usize; data: [n]int }      // Σ: o tipo de data depende de n
  fn take(n: usize, xs: [n]int) -> [n]int    // Π: o tipo de xs depende de n

@proof é a cerca, e implica @total, @pure e positividade-estrita. A distinção que ela traça é entre dado e lógica: uma família indexada usada como dado é sound no core sem cerca nenhuma, exatamente como qualquer tipo recursivo; ela precisa de consistência lógica (total, pura, estritamente-positiva) só quando é confiada como lógica — uma proposição cujo habitante você acredita. Sob @proof, o compilador força essa disciplina; sem ela, a mesma família é só dado rico.

Igualdade e sua prova são então uma família indexada comum, não uma primitiva — elas caem de D1–D4:

@proof decl Eq[A, x: A, y: A] -> prop {
    Refl: fn[a: A]() -> Eq[A, a, a]
}

@proof @total fn zero_right(n: Nat) -> Eq[Nat, add(n, 0), n] {
    match n {
        Zero    => Refl                        // add(0, 0) normaliza para 0 (D4) ⇒ Eq[Nat, 0, 0], que Refl habita
        Succ(k) => cong(Succ, zero_right(k))   // a indução É o match mais a recursão; @total a torna bem-fundada
    }
}

Uma prova é um programa (Curry-Howard): uma @proof @total fn que retorna uma proposição, construída com match (arms são =>) e recursão. cong é ela mesma uma @proof fn numa pequena proof-stdlib — um valor de library, não sintaxe. Não há keyword theorem e não há linguagem de táticas no core.

Model checking: @spec (extensão)

(extensão, seção 20.) Onde a camada de prova verifica uma implementação, o model checking verifica um design: propriedades globais e temporais de um sistema de processos (sem split-brain, entrega eventual). É o único membro desta seção que é uma extensão, e pela razão da seção 20 — o engine é volátil (bounded model checking, heurísticas de state-explosion, uma ponte que emite P ou TLA⁺ como alvo de codegen), mesmo que a teoria que ele checa seja estável. Ele adiciona um decorador, uma library comptime, um pass e um alvo de codegen, e não muda nada no core.

@spec(count(nodes, |n| n.role == Leader && n.term == cur) <= 1)                       // safety: um predicado puro, "always" implícito
@spec(spec.always(spec.implies(submitted(req), spec.eventually(committed(req)))))     // liveness: uma fórmula temporal

Safety é um predicado booleano comum no vocabulário de @requires/@where; liveness usa spec.always/spec.eventually/spec.implies/spec.leads_to, que são palavras 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 já limita o sistema a checar; o pass extrai o sistema-de-transições do grafo de spawn-e-canais. (@spec é o guarda-chuva para safety e liveness; o nome @property está indisponível — é o decorador de property-based-testing da extensão de testes.)

Táticas: prova-como-termo agora, @by depois

O termo de prova de um teorema real pode ser grande, e scripts de tática o constroem transformando um goal. Makoto chega lá em tiers:

• Tier 0 — prova-como-termo (hoje). Com D1–D5, você escreve a prova direto como uma função recursiva total, como o zero_right acima. É o chão e não precisa de táticas.
• Tier 1 — táticas como library. Táticas são funções comptime sobre um Goal de 1ª classe (como o reflect expõe type-data, 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.
• Tier 2 — @by (diferido, um delta de core). A forma ergonômica é um bloco cujos statements threadam o goal:

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

  @by é um decorador, não uma keyword — uma keyword reservaria o identificador by em todo programa; um decorador vive no namespace do @ e deixa by livre para nomes de usuário. É prefixado como @mm(arena) { … } (o modo tem que ser conhecido antes de o bloco ser lido), e é um delta de core genuíno porque um bloco com goal-threading é semântica de bloco nova — não algo que uma library possa adicionar, já que uma library não estende gramática (seção 20).

O compromisso de core que @by precisa é deliberadamente 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, e todo o vocabulário de táticas — Goal, Stack, as táticas, os combinadores — é uma library comum. Quando o compilador for self-hosted e importável (use compiler), o AST é ele mesmo um tipo de library, 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 — então ele compra ergonomia de tática sem o decorator/DSL hell que a linguagem rejeita. Três problemas vêm com essa era e são nomeados aqui para não serem descobertos tarde: higiene (um binding introduzido por macro não pode capturar um nome do usuário), estabilidade da API de AST (o tipo de AST refletido é um contrato público), e atribuição de erro (um erro dentro do código expandido tem que apontar para a fonte do usuário). Até lá a linguagem entrega Tier 0 e Tier 1, com a library de Tier 1 escrita no formato final para que @by depois a embrulhe sem retrabalho.

Core, delta, extensão

Feature	Forma	Onde	Gramática nova?
Disciplina de posse	@must_consume / @consume_once no decl	core (estende seção 5)	não — decorador
Refinamento	@where num tipo	core	pequena — um tipo carrega um predicado
Tipos de sessão	@protocol decl + @sends/@receives + dual	core (completa seção 4)	sim — corpo de protocolo, dual
Cercas	@pure / @total	core	não — análises do checker
Dependente, prático	value-params + @where	core	não — válido hoje
Dependente, prova	@proof + D1–D5	core, opt-in-por-uso	sim — gramática D1–D3, semântica D4–D5
Model checking	@spec + spec.* + pass + P/TLA⁺	extensão (seção 20)	não — o engine é volátil
Táticas @by	decorador de bloco com goal-threading	delta de core, diferido	sim — quando invocado

O modelo mental. Uma garantia é uma obrigação sobre um predicado, e o compilador a descarrega no degrau mais alto possível — irrepresentável se puder, provada se precisar, checada se não puder ser provada e, no último caso, assinada por você. Posse, refinamentos, sessões, cercas e tipos dependentes são degraus dessa única escada, cada um invocado por um decorador ou um tipo e cada um invisível até você buscá-lo. O proof-assistant mora no core porque sua teoria tem décadas; o model checker mora numa extensão porque seu engine não; e nenhuma obrigação jamais cai para fora da escada — ela só degrada, na cara, para a forma honesta mais forte que sobra. 誠.