O Bug Que Não Compilou: Portando um Erro de Reordenação para o Hydro

Marc Brooker dedicou um post de abril — "It's time to be right." — a argumentar que o que limita o desenvolvimento de software agêntico não é a capacidade dos modelos, mas a cauda de defeitos: os erros raros e graves, não a saída média. A direção que ele propõe é ferramental que torna classes inteiras de defeitos impossíveis de escrever, e ele nomeia dois sistemas dessa família: Cedar para autorização e Hydro para sistemas distribuídos.

Já li versões do discurso de "correto por construção" há anos, normalmente acopladas a protótipos de pesquisa que nunca consegui ter em mãos. O Hydro é diferente em um aspecto: ele existe de verdade. A crate hydro_lang vem publicando releases alpha 0.17 ao longo de junho de 2026, e o repositório carrega os testes de compilação que sustentam suas afirmações. Então rodei o experimento que o discurso implica. Peguei uma pequena agregação do tipo que já escrevi à mão muitas vezes, plantei o bug de reordenação que essa classe de código sempre desenvolve, reproduzi o bug deterministicamente — e então portei para o Hydro para ver exatamente qual linha o verificador de tipos recusaria.

A versão curta: o bug não sobreviveu ao port. Não porque o Hydro o encontrou, mas porque a linha com o bug precisa de uma suposição de ordenação que os tipos não me deixariam sustentar silenciosamente. A versão longa é mais interessante, porque o que o Hydro garante e o que ele apenas faz você assinar embaixo são coisas diferentes, e essa diferença é onde eu basearia uma decisão de adoção.

Uma agregação de 600 mensagens que responde 291

O cenário é a menor forma possível de um padrão que encontro sempre: N workers, cada um mantendo um contador local, reportam periodicamente (worker_id, contagem_cumulativa) a um agregador, que combina os relatos em um total global. Relatos cumulativos são a escolha de manual aqui — eles se auto-recuperam depois de uma mensagem perdida, já que o próximo relato carrega o valor completo.

O agregador escrito à mão aplica cada relato com uma atribuição: state[worker] = value. Essa linha embute um invariante que ninguém escreveu: relatos de um mesmo worker chegam na ordem em que foram enviados. Em uma única conexão TCP isso vale. Adicione um caminho de retry, um segundo hop, um load balancer ou um transporte UDP, e isso silenciosamente deixa de valer.

Aqui está o experimento inteiro em um arquivo — a ordem de envio, uma reordenação determinística fazendo o papel da rede, o fold com bug e o corrigido:

use std::collections::BTreeMap;

const WORKERS: u64 = 3;
const REPORTS: u64 = 200; // cumulative reports per worker: 1, 2, ..., 200

// One report: (worker id, that worker's cumulative processed count).
type Report = (u64, u64);

fn produced_order() -> Vec<Report> {
    // Round-robin interleave: the order the workers actually sent.
    (1..=REPORTS)
        .flat_map(|n| (0..WORKERS).map(move |w| (w, n)))
        .collect()
}

// Deterministic Fisher-Yates driven by a tiny LCG: models a fan-in where
// per-message delays (retries, multiple hops) can reorder anything.
fn network_reorder(mut msgs: Vec<Report>, mut seed: u64) -> Vec<Report> {
    for i in (1..msgs.len()).rev() {
        seed = seed.wrapping_mul(6364136223846793005).wrapping_add(1442695040888963407);
        msgs.swap(i, (seed >> 33) as usize % (i + 1));
    }
    msgs
}

// Aggregator 1: "the report I received last is the newest" (assignment).
// Correct only if arrival order matches send order.
fn last_arrival_wins(msgs: &[Report]) -> u64 {
    let mut state = BTreeMap::new();
    for &(w, n) in msgs {
        state.insert(w, n); // <- the latent bug: overwrite trusts arrival order
    }
    state.values().sum()
}

// Aggregator 2: merge with max. Cumulative counters only grow, so the
// newest value is the largest one -- no matter when it arrives.
fn max_merge(msgs: &[Report]) -> u64 {
    let mut state = BTreeMap::new();
    for &(w, n) in msgs {
        let slot = state.entry(w).or_insert(0);
        *slot = n.max(*slot); // commutative + idempotent merge
    }
    state.values().sum()
}

fn main() {
    let expected = WORKERS * REPORTS; // 600
    let in_order = produced_order();
    let reordered = network_reorder(in_order.clone(), 42);

    println!("expected total:                 {expected}");
    println!("last-arrival-wins, in order:    {}", last_arrival_wins(&in_order));
    println!("last-arrival-wins, reordered:   {}", last_arrival_wins(&reordered));
    println!("max-merge, in order:            {}", max_merge(&in_order));
    println!("max-merge, reordered:           {}", max_merge(&reordered));

    // The tests this post is really about:
    assert_eq!(last_arrival_wins(&in_order), expected); // passes CI forever
    assert_ne!(last_arrival_wins(&reordered), expected); // the planted bug, reproduced
    assert_eq!(max_merge(&in_order), expected);
    assert_eq!(max_merge(&reordered), expected); // order-free merge stays right
    println!("assertions passed: the bug is arrival-order dependence, not math");
}

Rode com rustc reorder.rs && ./reorder.

No Rust 1.95.0 a saída é: esperado 600, last-arrival-wins responde 600 em ordem e 291 reordenado, max-merge responde 600 nas duas vezes. A resposta errada não está ligeiramente errada; é uma subcontagem de 51%, porque para cada worker o relato que por acaso chegou por último — digamos o 97º de 200 — sobrescreveu todos os posteriores.

Dois detalhes nesse arquivo carregam o argumento. Primeiro, a assertion em ordem sobre o fold com bug passa. Esse bug vai para produção. Qualquer teste que alimente mensagens por um canal in-process vai aprová-lo, e é por isso que eu o chamo de bug latente em vez de build quebrado. Segundo, quando ampliei a verificação para 1.000 sementes de reordenação diferentes nos meus próprios testes, last_arrival_wins errou em todas as 1.000 e max_merge acertou em todas as 1.000 — incluindo uma execução em que entreguei cada mensagem duas vezes. A correção não é esperteza; é escolher uma função de merge onde ordem de chegada e duplicação deixam de importar. Essa é a mesma lição que os CRDTs ensinam, reduzida a uma entrada de BTreeMap.

O problema é que nada em Rust, ou em qualquer linguagem mainstream, conecta a linha state.insert(w, n) ao contrato de entrega do canal que a alimenta. O invariante mora na minha cabeça. O verificador de tipos vê uma escrita em mapa perfeitamente aceitável.

O port: onde o verificador de tipos me barrou

O Hydro é um framework Rust vindo da linhagem de pesquisa em dataflow da UC Berkeley. Você escreve um programa só descrevendo computação através de localizações — um Process aqui, um Cluster de workers ali — em estilo coreográfico, e um compilador em estágios o divide em binários por máquina. Essa arquitetura não é o assunto de hoje; o tipo de um valor é.

No Hydro, a caixa de entrada do agregador não é um iterador de mensagens. É um Stream com cinco parâmetros de tipo:

Stream<Type, Loc, Bound = Unbounded, Order = TotalOrder, Retry = ExactlyOnce>

Order e Retry são os dois que mataram meu bug. Um stream é marcado como TotalOrder apenas quando nenhum não determinismo pode afetar a ordem dos elementos; um fan-in mesclado é marcado como NoOrder. Duplicação funciona da mesma forma: ExactlyOnce versus AtLeastOnce. Esses marcadores não são documentação. Os operadores os consomem, e os operadores de rede os degradam para corresponder ao que o cabo pode prometer.

O port do meu hop de workers para agregador fica assim:

let totals = workers
    .source_iter(q!(local_reports()))   // Stream<(u32, u64), Cluster<Worker>, ...>
    .send_bincode(&aggregator)          // KeyedStream<MemberId<Worker>, (u32, u64), ...>
    .values();                          // Stream<(u32, u64), _, Unbounded, NoOrder>

let state = totals.fold(
    q!(|| BTreeMap::<u32, u64>::new()),
    q!(|m, (w, v)| { m.insert(w, v); }), // the same buggy line, ported
);

Enviar de um cluster para um processo retorna um KeyedStream chaveado pelo remetente: os substreams por membro mantêm sua ordem sobre o transporte TCP fail-stop padrão, porque uma conexão TCP realmente entrega em ordem. Mas no momento em que chamo .values() para mesclar tudo em um único barramento — que é exatamente o que meu fan-in mpsc escrito à mão fazia implicitamente — o resultado é tipado como NoOrder. O entrelaçamento entre remetentes é não determinístico, e agora o tipo do valor admite isso.

E em um stream NoOrder, aquele fold não compila. O erro, abreviado a partir da própria suíte de testes compile-fail do repositório, diz:

error[E0277]: Because the input stream has ordering `NoOrder`, the closure
              must demonstrate commutativity with a `commutative = ...` annotation.
   = note: To intentionally process the stream by observing a non-deterministic
           (shuffled) order of elements, use `.assume_ordering`. This introduces
           non-determinism so avoid unless necessary.

Este é o momento pelo qual o experimento existia. O compilador não está dizendo que minha closure está errada. Está dizendo que a correção da minha closure depende de uma ordenação que este stream não tem, e ele se recusa a prosseguir até que essa dependência seja resolvida. Inserção em mapa com sobrescrita não é comutativa — insert(w, 97) seguido de insert(w, 200) difere do inverso — então nenhuma anotação verdadeira deixa o bug passar intacto.

O diagrama abaixo é a imagem que vale guardar: as faixas por remetente mantêm sua ordem, o merge a descarta, e o portão do fold se recusa a abrir sem uma anotação de comutatividade. Desse beco sem saída o sistema de tipos deixa exatamente três saídas, e cada uma delas é uma decisão de design legível onde o código original tinha uma suposição invisível.

​

A primeira saída é reestruturar: pule o .values(), permaneça no KeyedStream e faça o fold por remetente, onde a ordem por chave ainda é TotalOrder e a atribuição é legal. Essa é uma correção real — ela codifica "a ordem vale dentro de um remetente, não entre remetentes" na forma do programa. Ela também deixa de estar disponível no momento em que o próprio transporte pode reordenar: troque a configuração TCP fail-stop por um dos transportes com perda e atrasos arbitrários presentes nos testes de rede do repositório e a garantia enfraquece nos tipos, porque o contrato de entrega do transporte é parte do tipo do stream.

A segunda saída é a que minha correção max_merge tomou: torne o combinador comutativo e diga isso.

let state = totals.fold(
    q!(|| BTreeMap::<u32, u64>::new()),
    q!(
        |m, (w, v)| {
            let slot = m.entry(w).or_insert(0);
            *slot = v.max(*slot);
        },
        commutative = manual_proof!(/** max-merge of monotone counters is commutative */)
    ),
);

A terceira saída é .assume_ordering, a escotilha explícita e insegura, que a própria mensagem de erro desencoraja. Ela existe, e deve existir: às vezes você conhece um fato de ordenação que os tipos não conseguem ver. Mas ela exige um marcador nondet! com uma justificativa escrita, o que significa que a suposição é encontrável por grep em revisão. Meu bug original era a versão silenciosa exatamente dessa anotação.

O que a garantia é — e o que ela apenas atesta

Aqui está a taxonomia pela qual eu vim. Na versão escrita à mão, "atribuição sobre um merge não ordenado" era representável, não testada e foi para produção. Na versão Hydro ela é irrepresentável por acidente: você só chega lá escrevendo uma anotação que nomeia o risco. Essa distinção — impossível versus impossível de fazer silenciosamente — é o que "correto por construção" realmente entrega aqui, e vale dizer isso sem verniz de marketing.

Como a anotação é a parte que sustenta a carga, fui ao código-fonte ver o que o manual_proof! verifica. Hoje: nada. Ele recebe um doc comment explicando por que a propriedade vale, e seu hook de registro é um no-op — a justificativa é para humanos. Um comentário na implementação do fold diz que o não determinismo de ordenação é, em vez disso, exercitado pelo simulador embutido, e que uma versão futura pretende tornar o mecanismo de prova dinâmico. Os testes de simulação do repositório sustentam a primeira metade: eles rodam flows sobre transportes com perda e atrasos arbitrários e exploram exaustivamente os agendamentos de entrega, verificando que as reordenações realmente ocorrem e que a consistência se mantém ao longo delas. Portanto, se eu mentir em um manual_proof!, o verificador de tipos não vai me pegar — o simulador é a camada projetada para isso.

Acho isso honesto e ligeiramente decepcionante ao mesmo tempo. O sistema de tipos tira a suposição de ordenação da minha cabeça e a coloca em uma interface verificada; a veracidade da minha alegação de comutatividade continua dependendo de mim, de um teste ou de um provador futuro. O erro de compilação me disse onde pensar. Não pensou por mim.

Os custos de emenda também são reais, e eu não os descartaria. Tudo dentro de q!(...) é código em estágios — o modelo de duas fases do Hydro roda seu programa uma vez para planejar o deployment e então gera binários por máquina — e closures em estágios são onde o suporte da IDE, os stack traces e os erros do borrow checker ficam sensivelmente piores do que em Rust puro. A crate está na linha 0.17.0-alpha; eu li a API em um commit de fim de julho de 2026, não a partir de uma promessa de estabilidade. E o port é uma reescrita, não um wrapper: o framework é dono da sua topologia e do seu main loop, então a unidade de adoção é um serviço, não uma função.

Vale traçar mais um limite, já que recentemente passei um tempo fazendo model checking de um design em Quint: aquela ferramenta verifica um modelo do seu protocolo e deixa a implementação livre para divergir; o Hydro tipa a própria implementação, mas apenas para as propriedades que seus marcadores conseguem expressar — ordenação, duplicação, limitação. Eles atacam metades diferentes da mesma lacuna. Nenhum dos dois vai notar que sua lógica de negócio calcula o número errado de uma forma perfeitamente comutativa.

Então o port se paga em pequena escala? Para este serviço, isoladamente, uma regra de code review — "faça merge, nunca atribua, em um fan-in" — mais o teste de propriedade com 1.000 sementes teria pegado o mesmo bug por uma fração da curva de aprendizado. O que a regra de revisão não consegue fazer é escalar para código que eu não revisei, que é o ponto real de Brooker sobre agentes: quando mais do código é escrito por algo que não participa de design reviews, garantias acopladas ao artefato ganham de garantias acopladas à cultura. Esse argumento fica mais forte a cada trimestre, e é a razão pela qual este experimento entra nas minhas anotações como uma capacidade genuína, com todas as arestas de alpha, em vez de teatro de pesquisa.

O que eu estou guardando

• A classe de bug a temer em código de fan-in é a dependência de ordem de chegada: minha versão plantada passou em todos os testes em ordem e subcontou em 51% sob uma reordenação. Reproduza reordenações deterministicamente; um shuffle com semente é suficiente.
• Relatos cumulativos mais um merge com max tornam ordem e duplicatas irrelevantes. Se seus contadores são monótonos, você nunca precisou de "última chegada" — você precisava de "maior valor".
• A contribuição do Hydro não é verificação mágica. São cinco parâmetros de tipo em Stream que tornam os contratos de entrega parte do tipo do valor, de modo que merges não ordenados recusam folds não comutativos até você reestruturar, corrigir o merge ou assinar uma suposição explícita.
• manual_proof! é atestação, não prova — a verificação de honestidade hoje é o simulador que explora agendamentos de entrega, não o verificador de tipos. Calibre sua confiança de acordo.
• Recorra a isso quando a superfície sensível a ordenação estiver crescendo mais rápido que sua capacidade de revisão — muitos serviços, muitas mãos ou código escrito por agentes. Pule quando um único serviço revisado com um teste de propriedade cobre o mesmo risco; os custos de emenda em estágio alpha são o preço todo, e em uma base de código pequena eles excedem o custo esperado do bug.

Use quando a correção depender da semântica de entrega através de muitos fan-ins e muitos autores. Evite quando você precisar de estabilidade de API neste ano, sua equipe não estiver pronta para depurar Rust em estágios, ou uma convenção de função de merge mais um teste de reordenação já fecharem a lacuna.