Стан облікового запису Ethereum: конвеєр QA для мінімального токена

QA-панель моніторингу стану смартконтракту

У попередній публікації була розглянута наскрізна реалізація: мінімальний контракт токена, реконструкція офчейн-стану та React-фронтенд — від `mint()` до MetaMask. Ця публікація продовжує розпочате: як здійснити QA чогось подібного?

Я ще не блокчейн-інженер, але QA-патерни добре переносяться між різними доменами, і запозичення того, що вже працює в інших місцях, — найшвидший спосіб навчання.

Контракт виконує лише три дії: `mint`, `transfer` та `burn`, але навіть цього достатньо для практики повного QA-інструментарію: статичний аналіз, мутаційне тестування, профілювання газу, формальна верифікація.

Код знаходиться в `egpivo/ethereum-account-state`.

Піраміда QA блокчейну: від статичного аналізу в основі до формальної верифікації на вершині

З чого ми почали

Перед додаванням чогось нового проєкт вже мав:

• 21 модульний тест Foundry, що охоплюють кожний перехід стану (успіх, відміна при некоректному введенні, випромінювання подій)
• 3 інваріантні тести через `TokenHandler`, який виконує випадкові послідовності `mint`/`transfer`/`burn` на 10 акторах (по 128 тисяч викликів)
• Фаз-тести, що перевіряють `sum(balances) == totalSupply` для випадкових сум
• Доменні тести TypeScript (Vitest), що відображають ончейн-машину станів
• CI: компіляція, тестування, лінтинг (Prettier + solhint)

Усі тести пройдено. Покриття виглядало нормально. Навіщо тоді більше?

Тому що "всі тести пройдено" не означає "всі баги виявлено". 100% покриття рядків все одно може пропустити реальний баг, якщо жодна перевірка не перевіряє потрібне.

Фаза 1: статичний аналіз смартконтракту та покриття

Slither

Slither (Trail of Bits) виявляє проблеми, невидимі для тестів: повторний вхід, неперевірені значення повернення, невідповідності інтерфейсів.

./scripts/run-qa.sh slither

Результат: 1 середня знахідка: `erc20-interface`: `transfer()` не повертає `bool`.

Це очікувано. Контракт навмисно не є повним ERC20: це навчальна машина станів. Але знахідка не академічна:

Якщо хтось пізніше імпортує цей токен у протокол, що очікує ERC20, невідповідність інтерфейсу призведе до тихого збою. Slither позначає це зараз, щоб рішення було свідомим.

Покриття

./scripts/run-qa.sh coverage Результат покриття.

Одна неохоплена функція: `BalanceLib.gt()`. Ми повернемося до цього.

вивід forge coverage: 24 тести пройдено, таблиця покриття Token.sol

Знімки газу

./scripts/run-qa.sh gas

Базові витрати газу для трьох операцій:

Газ у вираженні операцій

При наступних запусках `forge snapshot — diff` порівнює з базовою лінією. 20% регресія газу в `transfer()` — це реальна вартість для кожного користувача — виявити це до злиття дешево.

Фаза 2: мутаційне тестування та формальна верифікація

Мутаційне тестування (Gambit)

Тут стало цікаво. Gambit (Certora) генерує мутантів: копії `Token.sol` з невеликими навмисними багами (`+=` на `-=`, `>=` на `>`, умови інвертовано). Конвеєр запускає повний набір тестів проти кожного мутанта. Якщо мутант виживає (усі тести все ще проходять), це конкретна прогалина в тестах.

./scripts/run-qa.sh mutation

Результат: 97,0% оцінка мутацій — 32 вбито, 1 вижив із 33 мутантів.

Вихідний лог Gambit показує кожного мутанта та що він змінив. Кілька прикладів:

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 ← жоден тест це не виявив Мутаційне тестування Gambit: 32 вбито, 1 вижив, оцінка мутацій 97,0%

Мутант, що вижив, поміняв `a > b` на `b > a` у `BalanceLib.gt()`. Жоден тест це не виявив, тому що `gt()` — це мертвий код. Він ніколи не викликається ніде в `Token.sol`.

Покриття позначило 91,67% функцій, але не змогло пояснити прогалину. Мутаційне тестування зробило це: `gt()` — мертвий код, ніщо його не викликає, і ніхто не помітив би, якби він був неправильним.

Мертвий або незахищений код у смартконтрактах має реальні прецеденти.

Функція не була призначена для виклику, але ніхто не перевіряв це припущення. Наш `gt()` нешкідливий у порівнянні, але патерн той самий: код, що існує, але ніколи не виконується, — це код, за яким ніхто не стежить.

Формальна верифікація (Halmos)

Halmos (a16z) міркує про всі можливі вхідні дані символічно. Там, де фаз-тести вибірково тестують випадкові значення та сподіваються потрапити в крайні випадки, Halmos доводить властивості вичерпно.

./scripts/run-qa.sh halmos

Результат: 9/9 символічних тестів пройдено — усі властивості доведено для всіх вхідних даних.

Верифіковані властивості:

Верифіковані властивості

Одна практична примітка: Halmos 0.3.3 не підтримує `vm.expectRevert()`, тому я не міг написати тести на відміну звичайним способом Foundry. Обхідний шлях — це патерн try/catch — якщо виклик успішний, коли має відмінитися, `assert(false)` провалює доказ:

function check_mint_reverts_on_zero_address(uint256 amount) public {
vm.assume(amount > 0);
try token.mint(address(0), amount) {
assert(false); // не повинно досягти цього місця
} catch {
// очікувана відміна - Halmos доводить, що цей шлях завжди береться
}
}

Не найкрасивіше, але працює — Halmos все одно доводить властивість для всіх вхідних даних. Це те, що можна дізнатися, лише фактично запустивши інструмент.

Для контексту про те, чому формальна верифікація важлива:

Уразливість була в коді, доступному для перегляду будь-кому, але жоден інструмент чи тест не виявив її до розгортання. Символічні доказувачі, як Halmos, існують саме для закриття цієї прогалини — вони не беруть вибірку; вони вичерпують простір вхідних даних.

Вивід Halmos: 9 тестів пройдено, 0 провалено, результати символічних тестів

Тестовий файл — `contracts/test/Token.halmos.t.sol`.

Фаза 3: міжрівневе тестування властивостей

Архітектура першої публікації має доменний рівень TypeScript, що відображає ончейн-машину станів. Ця фаза перевіряє, чи дійсно вони погоджуються.

Тестування на основі властивостей з fast-check

Я додав тести властивостей fast-check для доменного рівня TypeScript, відображаючи те, що робить фазер Foundry для Solidity:

npm test - tests/unit/property.test.ts

Результат: 9/9 тестів властивостей пройдено після виправлення реального бага.

Протестовані властивості:

• `Balance`: комутативність, асоціативність, ідентичність, інверсія, узгодженість порівняння
• `Token`: інваріант `sum(balances) == totalSupply` при випадкових послідовностях операцій (200 запусків, по 50 операцій)
• `Token`: `totalSupply` невід'ємний після випадкових послідовностей
• `mint` завжди успішний для дійсних вхідних даних
• `transfer` зберігає `totalSupply`

Баг, знайдений fast-check

fast-check знайшов реальний баг міжрівневої узгодженості в `Token.ts` `transfer()`. Скорочений контрприклад був одразу зрозумілий:

Property failed after 3 tests
Shrunk 2 time(s)
Counterexample: transfer(from=0xaaa…, to=0xaaa…, amount=1n)
→ from == to (самопереказ)
→ verifyInvariant() повернув false

Самопереказ (`from == to`) порушив інваріант `sum(balances) == totalSupply`. `toBalance` було прочитано до оновлення `fromBalance`, тому коли `from == to`, застаріле значення перезаписало відрахування:

// До (з багом)
const fromBalance = this.getBalance(from);
const toBalance = this.getBalance(to); // ← застаріле, коли from == to
this.accounts.set(from.getValue(), fromBalance.subtract(amount));
this.accounts.set(to.getValue(), toBalance.add(amount)); // ← перезаписує віднімання

Виправлення: читати `toBalance` після запису `fromBalance`, відповідно до семантики сховища Solidity:

// Після (виправлено)
const fromBalance = this.getBalance(from);
this.accounts.set(from.getValue(), fromBalance.subtract(amount));
const toBalance = this.getBalance(to); // ← тепер читає оновлене значення
this.accounts.set(to.getValue(), toBalance.add(amount));

Контракт Solidity не був уражений: він перечитує сховище після кожного запису. Але дзеркало TypeScript мало тонку залежність від порядку, яку не охоплював жоден існуючий модульний тест.

Міжрівневі невідповідності в більшому масштабі були катастрофічними.

Наш баг самопереказу не призвів би до втрати чиїхось грошей, але режим збою структурно той самий: два рівні, які повинні погоджуватися, не погоджуються.

Підводні камені на шляху

Запуск QA-інструментів на існуючому проєкті ніколи не буває просто "встановити та запустити". Кілька речей зламалося, перш ніж запрацювало:

• 0% покриття, тому що `foundry.toml` не мав тестового шляху: перший запуск `forge coverage` повернув 0% по всій лінії. Виявляється, `foundry.toml` не вказував `test = "contracts/test"` або `script = "contracts/script"`, тому Forge не виявляв жодних тестів. Команда покриття успішно завершилася мовчки — просто нічого було покривати. Це був найбільш оманливий збій: зелений запуск без корисного виводу.
• імпорт `InvariantTest` зник у forge-std v1.14.0: `Invariant.t.sol` імпортував `InvariantTest` з `forge-std`, який був видалений у недавньому релізі. Компіляція провалилася з непрозорою помилкою "символ не знайдено". Виправлення полягало в видаленні імпорту — `Test` сам по собі достатній для інваріантного тестування Foundry зараз.
• `uint256(token.totalSupply())` проти `Balance.unwrap()`: тести використовували явне приведення для витягу базового `uint256` з визначеного користувачем типу `Balance`. Це компілювалося, але це неправильна ідіома — `Balance.unwrap(token.totalSupply())` — це те, для чого розроблена система UDVT. Застосовано в `Token.t.sol`, `Invariant.t.sol` та `DeploySepolia.s.sol`.

Дизайн конвеєра

Все запускається через два скрипти:

• scripts/setup-qa-tools.sh`: встановлює Slither, Halmos, Gambit (ідемпотентно)
• `scripts/run-qa.sh`: виконує перевірки, зберігає результати з позначкою часу в `qa-results/`

./scripts/run-qa.sh slither gas # тільки статичний аналіз + газ
./scripts/run-qa.sh mutation # тільки мутаційне тестування
./scripts/run-qa.sh all # все

Не кожна перевірка швидка. Slither та покриття запускаються при кожному коміті. Мутаційне тестування та Halmos повільніші — краще підходять для щотижневих або передвипускних запусків.

Підсумок

Інструментарій QA блокчейну: що виявляє кожен рівень — від статичного аналізу до міжрівневого тестування властивостей

П'ять рівнів QA, кожен виявляє різний клас проблем.

Пояснення рівнів

Gambit та fast-check дали найбільш дієві результати в цьому раунді.

CI-конвеєр

QA-перевірки тепер підключені до GitHub Actions як шестиетапний конвеєр:

CI-конвеєр: Build & Lint розгалужується на Test, Coverage, Gas, Slither та Audit етапи

Конвеєр GitHub Actions: Build & Lint керує всіма подальшими етапами.

Пояснення етапів

Посилання

• Джерело Ethereum Account State: [github.com/egpivo/ethereum-account-state](https://github.com/egpivo/ethereum-account-state)
• Попередня публікація: Ethereum Account State
• Slither: github.com/crytic/slither
• Gambit: github.com/Certora/gambit
• Halmos: github.com/a16z/halmos
• fast-check: github.com/dubzzz/fast-check
• Foundry: getfoundry.sh

Примітки

• Ця публікація адаптована з мого оригінального допису в блозі.

---

Ethereum Account State: QA Pipeline for a Minimal Token було спочатку опубліковано в Coinmonks на Medium, де люди продовжують розмову, виділяючи та реагуючи на цю історію.