O post anterior percorreu uma implementação de ponta a ponta: um contrato de token mínimo, reconstrução de estado off-chain e um frontend React — desde `mint()` até MetaMask. Este post continua de onde paramos: como fazer QA de algo assim?
Não sou um engenheiro de blockchain (ainda), mas os padrões de QA são bem transferíveis entre domínios, e emprestar o que já funciona noutros lugares é como aprendo mais rápido.
O contrato faz apenas três coisas: `mint`, `transfer` e `burn`, mas mesmo isso é suficiente para praticar a cadeia de ferramentas QA completa: análise estática, teste de mutação, perfil de gas, verificação formal.
O código está em `egpivo/ethereum-account-state`.
Pirâmide de QA Blockchain: da análise estática na base à verificação formal no topoAntes de adicionar algo novo, o projeto já tinha:
Todos os testes passaram. A cobertura parecia boa. Então, por que incomodar com mais?
Porque "todos os testes passam" não significa "todos os bugs são capturados". 100% de cobertura de linha ainda pode perder um bug real se nenhuma asserção verificar a coisa certa.
Slither(Trail of Bits) captura problemas que são invisíveis aos testes: reentrância, valores de retorno não verificados, incompatibilidades de interface.
./scripts/run-qa.sh slither
Resultado: 1 descoberta Média: `erc20-interface`: `transfer()` não retorna `bool`.
Isto era esperado. O contrato intencionalmente não é um ERC20 completo: é uma máquina de estado educacional. Mas a descoberta não é académica:
Se alguém posteriormente importar este token num protocolo que espera ERC20, a incompatibilidade de interface falharia silenciosamente. O Slither sinaliza-o agora para que a decisão seja consciente.
./scripts/run-qa.sh coverageResultado da cobertura.
Uma função não coberta: `BalanceLib.gt()`. Voltaremos a isto.
saída da cobertura forge: 24 testes passaram, tabela de cobertura Token.sol./scripts/run-qa.sh gas
Custos de gas base para as três operações:
Gas em termos de operaçõesEm execuções subsequentes, `forge snapshot — diff` compara com a linha de base. Uma regressão de gas de 20% em `transfer()` é um custo real para cada utilizador — capturá-la antes do merge é barato.
Foi aqui que as coisas ficaram interessantes. Gambit(Certora) gera mutantes: cópias de `Token.sol` com pequenos bugs deliberados (`+=` para `-=`, `>=` para `>`, condições negadas). O pipeline executa o conjunto completo de testes contra cada mutante. Se um mutante sobrevive (todos os testes ainda passam), essa é uma lacuna de teste concreta.
./scripts/run-qa.sh mutation
Resultado: pontuação de mutação de 97,0% — 32 mortos, 1 sobreviveu de 33 mutantes.
O log de saída do Gambit mostra cada mutante e o que mudou. Alguns exemplos:
Generated mutant #7: BinaryOpMutation — Token.sol:168
totalSupply = totalSupply.add(amountBalance) → totalSupply = totalSupply.sub(amountBalance)
KILLED by test_Mint_Success
Generated mutant #19: RelationalOpMutation — Token.sol:196
if (!fromBalance.gte(amountBalance)) → if (fromBalance.gte(amountBalance))
KILLED by test_Transfer_Success
Generated mutant #28: SwapArgumentsMutation — Token.sol:81
return Balance.unwrap(a) > Balance.unwrap(b) → return Balance.unwrap(b) > Balance.unwrap(a)
SURVIVED ← nenhum teste capturou istoTeste de mutação Gambit: 32 mortos, 1 sobreviveu, pontuação de mutação 97,0%
O mutante sobrevivente trocou `a > b` para `b > a` em `BalanceLib.gt()`. Nenhum teste o capturou porque `gt()` é código morto. Nunca é chamado em qualquer lugar em `Token.sol`.
A cobertura sinalizou 91,67% de funções, mas não conseguiu explicar a lacuna. O teste de mutação conseguiu: `gt()` é código morto, nada o chama, e ninguém notaria se estivesse errado.
Código morto ou desprotegido em contratos inteligentes tem precedentes reais.
A função não pretendia ser chamável, mas ninguém testou essa suposição. O nosso `gt()` é inofensivo em comparação, mas o padrão é o mesmo: código que existe mas nunca é exercitado é código que ninguém está a observar.
Halmos(a16z) raciocina sobre todas as entradas possíveis simbolicamente. Onde os testes fuzz amostragem valores aleatórios e esperam atingir casos extremos, Halmos prova propriedades exaustivamente.
./scripts/run-qa.sh halmos
Resultado: 9/9 testes simbólicos passam — todas as propriedades provadas para todas as entradas.
Propriedades verificadas:
Propriedades verificadasUma nota prática: Halmos 0.3.3 não suporta `vm.expectRevert()`, então não consegui escrever testes de reversão da maneira normal do Foundry. A solução é um padrão try/catch — se a chamada for bem-sucedida quando deveria reverter, `assert(false)` falha a prova:
function check_mint_reverts_on_zero_address(uint256 amount) public {
vm.assume(amount > 0);
try token.mint(address(0), amount) {
assert(false); // não deveria chegar aqui
} catch {
// reversão esperada - Halmos prova que este caminho é sempre tomado
}
}
Não é o mais bonito, mas funciona — Halmos ainda prova a propriedade para todas as entradas. Este é o tipo de coisa que só se descobre ao executar realmente a ferramenta.
Para contexto sobre por que a verificação formal importa:
A vulnerabilidade estava no código, revisável por qualquer pessoa, mas nenhuma ferramenta ou teste a capturou antes da implementação. Provadores simbólicos como Halmos existem precisamente para fechar essa lacuna — eles não amostragem; esgotam o espaço de entrada.
Saída Halmos: 9 testes passaram, 0 falharam, resultados de teste simbólicoO arquivo de teste é `contracts/test/Token.halmos.t.sol`.
A arquitetura do primeiro post tem uma camada de domínio TypeScript que espelha a máquina de estado on-chain. Esta fase testa se os dois realmente concordam.
Adicionei testes de propriedade fast-check para a camada de domínio TypeScript, espelhando o que o fuzzer do Foundry faz para Solidity:
npm test - tests/unit/property.test.ts
Resultado: 9/9 testes de propriedade passam após corrigir um bug real.
Propriedades testadas:
fast-check encontrou um bug real de consistência cross-layer em `Token.ts` `transfer()`. O contraexemplo reduzido foi imediatamente claro:
Property failed after 3 tests
Shrunk 2 time(s)
Counterexample: transfer(from=0xaaa…, to=0xaaa…, amount=1n)
→ from == to (auto-transferência)
→ verifyInvariant() returned false
Auto-transferência (`from == to`) quebrou a invariante `sum(balances) == totalSupply`. `toBalance` foi lido antes de `fromBalance` ser atualizado, então quando `from == to`, o valor obsoleto sobrescreveu a dedução:
// Antes (com bug)
const fromBalance = this.getBalance(from);
const toBalance = this.getBalance(to); // ← obsoleto quando from == to
this.accounts.set(from.getValue(), fromBalance.subtract(amount));
this.accounts.set(to.getValue(), toBalance.add(amount)); // ← sobrescreve a subtração
Correção: ler `toBalance` após escrever `fromBalance`, correspondendo à semântica de armazenamento do Solidity:
// Depois (corrigido)
const fromBalance = this.getBalance(from);
this.accounts.set(from.getValue(), fromBalance.subtract(amount));
const toBalance = this.getBalance(to); // ← agora lê o valor atualizado
this.accounts.set(to.getValue(), toBalance.add(amount));
O contrato Solidity não foi afetado: ele relê o armazenamento após cada escrita. Mas o espelho TypeScript tinha uma dependência de ordenação subtil que nenhum teste unitário existente cobria.
Incompatibilidades cross-layer em maior escala foram catastróficas.
O nosso bug de auto-transferência não teria feito ninguém perder dinheiro, mas o modo de falha é estruturalmente o mesmo: duas camadas que deveriam concordar, não concordam.
Executar ferramentas QA num projeto existente nunca é apenas "instalar e executar". Algumas coisas quebraram antes de funcionarem:
Tudo é executado através de dois scripts:
./scripts/run-qa.sh slither gas # apenas análise estática + gas
./scripts/run-qa.sh mutation # apenas teste de mutação
./scripts/run-qa.sh all # tudo
Nem todas as verificações são rápidas. Slither e cobertura são executados em cada commit. Teste de mutação e Halmos são mais lentos — mais adequados para execuções semanais ou pré-lançamento.
Cinco camadas QA, cada uma capturando uma classe diferente de problema.
Explicação da camadaGambit e fast-check deram os resultados mais acionáveis nesta ronda.
As verificações QA estão agora conectadas ao GitHub Actions como um pipeline de seis fases:
Pipeline CI: Build & Lint distribui para as fases Test, Coverage, Gas, Slither e AuditPipeline GitHub Actions: Build & Lint controla todas as fases downstream.
Explicação da faseEthereum Account State: QA Pipeline for a Minimal Token foi originalmente publicado em Coinmonks no Medium, onde as pessoas estão a continuar a conversa ao destacar e responder a esta história.


