Poprzedni post przeprowadził przez implementację end-to-end: minimalny kontrakt tokenów, rekonstrukcję stanu off-chain i frontend React — od `mint()` do MetaMask. Ten post kontynuuje tam, gdzie tamten się skończył: jak przeprowadzić QA czegoś takiego?
Nie jestem (jeszcze) inżynierem blockchain, ale wzorce QA dobrze przenoszą się między domenami, a pożyczanie tego, co już działa gdzie indziej, to sposób, w jaki uczę się najszybciej.
Kontrakt robi tylko trzy rzeczy: `mint`, `transfer` i `burn`, ale nawet to wystarczy, by przećwiczyć pełny łańcuch narzędzi QA: analizę statyczną, testowanie mutacji, profilowanie gazu, weryfikację formalną.
Kod znajduje się w `egpivo/ethereum-account-state`.
Piramida QA Blockchain: od analizy statycznej u podstawy do weryfikacji formalnej na szczycieZanim dodano cokolwiek nowego, projekt już miał:
Wszystkie testy przeszły. Pokrycie wyglądało dobrze. Więc po co się więcej starać?
Ponieważ "wszystkie testy przeszły" nie oznacza "wszystkie błędy zostały wykryte". 100% pokrycia linii nadal może przeoczyć prawdziwy błąd, jeśli żadne asercje nie sprawdzają właściwej rzeczy.
Slither(Trail of Bits) wychwytuje problemy niewidoczne dla testów: reentrancy, niesprawdzone wartości zwracane, niedopasowania interfejsów.
./scripts/run-qa.sh slither
Wynik: 1 znalezisko średnie: `erc20-interface`: `transfer()` nie zwraca `bool`.
To jest oczekiwane. Kontrakt celowo nie jest pełnym ERC20: jest edukacyjną maszyną stanów. Ale znalezisko nie jest akademickie:
Jeśli ktoś później zaimportuje ten token do protokołu oczekującego ERC20, niedopasowanie interfejsu zawiodłoby po cichu. Slither flaguje to teraz, więc decyzja jest świadoma.
./scripts/run-qa.sh coverageWynik pokrycia.
Jedna nieobsłużona funkcja: `BalanceLib.gt()`. Wrócimy do tego.
wynik forge coverage: 24 testy przeszły, tabela pokrycia Token.sol./scripts/run-qa.sh gas
Bazowe koszty gazu dla trzech operacji:
Gaz w kontekście operacjiPrzy kolejnych uruchomieniach `forge snapshot — diff` porównuje z bazą. 20% regresja gazu w `transfer()` to realny koszt dla każdego użytkownika — wykrycie tego przed merge jest tanie.
Tu sprawy stały się interesujące. Gambit(Certora) generuje mutanty: kopie `Token.sol` z małymi celowymi błędami (`+=` na `-=`, `>=` na `>`, negowane warunki). Pipeline uruchamia pełny zestaw testów przeciwko każdemu mutantowi. Jeśli mutant przeżyje (wszystkie testy nadal przechodzą), to jest konkretna luka testowa.
./scripts/run-qa.sh mutation
Wynik: 97,0% wynik mutacji — 32 zabite, 1 przeżył z 33 mutantów.
Log wyjściowy Gambit pokazuje każdego mutanta i co zmienił. Kilka przykładów:
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 ← żaden test tego nie wykryłTestowanie mutacji Gambit: 32 zabite, 1 przeżył, wynik mutacji 97,0%
Przeżywający mutant zamienił `a > b` na `b > a` w `BalanceLib.gt()`. Żaden test tego nie wykrył, ponieważ `gt()` jest martwym kodem. Nigdy nie jest wywoływany nigdzie w `Token.sol`.
Pokrycie zaflagowało 91,67% funkcji, ale nie mogło wyjaśnić luki. Testowanie mutacji tak: `gt()` jest martwym kodem, nic go nie wywołuje i nikt nie zauważyłby, gdyby był błędny.
Martwy lub niechroniony kod w inteligentnych kontraktach ma realne precedensy.
Funkcja nie była przeznaczona do wywołania, ale nikt nie przetestował tego założenia. Nasz `gt()` jest nieszkodliwy w porównaniu, ale wzorzec jest ten sam: kod, który istnieje, ale nigdy nie jest wykonywany, to kod, którego nikt nie obserwuje.
Halmos(a16z) rozumuje o wszystkich możliwych wejściach symbolicznie. Tam gdzie testy fuzz próbkują losowe wartości i mają nadzieję trafić na przypadki brzegowe, Halmos dowodzi właściwości wyczerpująco.
./scripts/run-qa.sh halmos
Wynik: 9/9 testów symbolicznych przeszło — wszystkie właściwości udowodnione dla wszystkich wejść.
Zweryfikowane właściwości:
Zweryfikowane właściwościJedna praktyczna uwaga: Halmos 0.3.3 nie obsługuje `vm.expectRevert()`, więc nie mogłem napisać testów revert w normalny sposób Foundry. Obejście to wzorzec try/catch — jeśli wywołanie się powiedzie, gdy powinno się cofnąć, `assert(false)` zawodzi dowód:
function check_mint_reverts_on_zero_address(uint256 amount) public {
vm.assume(amount > 0);
try token.mint(address(0), amount) {
assert(false); // nie powinno tutaj dotrzeć
} catch {
// oczekiwane cofnięcie - Halmos dowodzi, że ta ścieżka jest zawsze brana
}
}
Nie najładniejsze, ale działa — Halmos nadal dowodzi właściwości dla wszystkich wejść. To jest rodzaj rzeczy, o której dowiadujesz się tylko faktycznie uruchamiając narzędzie.
Dla kontekstu, dlaczego weryfikacja formalna ma znaczenie:
Podatność była w kodzie, do przejrzenia przez każdego, ale żadne narzędzie ani test nie wykrył jej przed wdrożeniem. Symboliczne dowodziarze jak Halmos istnieją właśnie po to, by zamknąć tę lukę — nie próbkują; wyczerpują przestrzeń wejściową.
Wynik Halmos: 9 testów przeszło, 0 nieudanych, wyniki testów symbolicznychPlik testowy to `contracts/test/Token.halmos.t.sol`.
Architektura pierwszego posta ma warstwę domenową TypeScript, która odzwierciedla maszynę stanów on-chain. Ta faza testuje, czy obie faktycznie się zgadzają.
Dodałem testy właściwości fast-check dla warstwy domenowej TypeScript, odzwierciedlające to, co robi fuzzer Foundry dla Solidity:
npm test - tests/unit/property.test.ts
Wynik: 9/9 testów właściwości przeszło po naprawieniu prawdziwego błędu.
Testowane właściwości:
fast-check znalazł prawdziwy błąd spójności między warstwami w `Token.ts` `transfer()`. Skurczony kontrprzykład był natychmiast jasny:
Property failed after 3 tests
Shrunk 2 time(s)
Counterexample: transfer(from=0xaaa…, to=0xaaa…, amount=1n)
→ from == to (transfer do siebie)
→ verifyInvariant() zwrócił false
Transfer do siebie (`from == to`) złamał niezmiennik `sum(balances) == totalSupply`. `toBalance` był odczytany przed aktualizacją `fromBalance`, więc gdy `from == to`, nieaktualna wartość nadpisała odliczenie:
// Przed (błędne)
const fromBalance = this.getBalance(from);
const toBalance = this.getBalance(to); // ← nieaktualne gdy from == to
this.accounts.set(from.getValue(), fromBalance.subtract(amount));
this.accounts.set(to.getValue(), toBalance.add(amount)); // ← nadpisuje odejmowanie
Poprawka: odczytaj `toBalance` po zapisaniu `fromBalance`, dopasowując semantykę pamięci Solidity:
// Po (naprawione)
const fromBalance = this.getBalance(from);
this.accounts.set(from.getValue(), fromBalance.subtract(amount));
const toBalance = this.getBalance(to); // ← teraz odczytuje zaktualizowaną wartość
this.accounts.set(to.getValue(), toBalance.add(amount));
Kontrakt Solidity nie był dotknięty: ponownie odczytuje pamięć po każdym zapisie. Ale lustro TypeScript miało subtelną zależność kolejności, której nie obejmował żaden istniejący test jednostkowy.
Niedopasowania między warstwami w większej skali były katastrofalne.
Nasz błąd transferu do siebie nie spowodowałby utraty niczyich pieniędzy, ale tryb awarii jest strukturalnie taki sam: dwie warstwy, które powinny się zgadzać, nie zgadzają się.
Uruchamianie narzędzi QA w istniejącym projekcie nigdy nie jest tylko "zainstaluj i uruchom". Kilka rzeczy pękło, zanim zadziałały:
Wszystko działa przez dwa skrypty:
./scripts/run-qa.sh slither gas # tylko analiza statyczna + gaz
./scripts/run-qa.sh mutation # tylko testowanie mutacji
./scripts/run-qa.sh all # wszystko
Nie każde sprawdzenie jest szybkie. Slither i pokrycie działają przy każdym commit. Testowanie mutacji i Halmos są wolniejsze — lepiej nadają się do cotygodniowych uruchomień lub przed wydaniem.
Pięć warstw QA, z których każda wychwytuje inną klasę problemów.
Wyjaśnienie warstwGambit i fast-check dały najbardziej przydatne wyniki w tej rundzie.
Sprawdzenia QA są teraz podłączone do GitHub Actions jako sześciostopniowy pipeline:
Pipeline CI: Build & Lint rozchodzi się do etapów Test, Coverage, Gas, Slither i AuditPipeline GitHub Actions: Build & Lint bramkuje wszystkie etapy niższego rzędu.
Wyjaśnienie etapówEthereum Account State: QA Pipeline for a Minimal Token zostało pierwotnie opublikowane w Coinmonks na Medium, gdzie ludzie kontynuują rozmowę, podkreślając i odpowiadając na tę historię.


