Copy English

Why

Stateful fuzzing is becoming standard Solidity tooling, yet its main failure mode is silent: the test passes because the generator never performed meaningful work. Reachability metrics belong beside the assertion.

Foundry checks invariants after randomized sequences of calls. A campaign can remain green while accomplishing almost nothing when generated calls revert before reaching meaningful protocol states.

How it works

Write an open invariant test and a handler-based version for the same vault, compare call/revert distributions, add ghost-variable accounting, and deliberately seed a sequence-only bug.

PoC

Test the same ERC-4626-style vault twice: first by targeting the contracts directly, then through handlers that prepare balances and approvals. Track calls, reverts, deposits, withdrawals, actors, and reached states with metrics and ghost variables. Seed a bug that requires a deposit-transfer-withdraw sequence.

What it proves

The assertion is only half the test. The action distribution must reach the state space where the property could fail. Compare the open and handler-based campaigns by coverage and meaningful transitions, not merely runs and depth.

Reference: Foundry invariant testing.

Review clarification

A passing campaign has two possible meanings — the property held, or the fuzzer never got close enough to break it — and Foundry will not say which by default. With open targeting the generated calls are random functions from random senders with random arguments, and almost all of them die at the first require: a withdraw with no shares, a deposit with no balance and no approval. Thousands of runs can leave the vault in roughly the state setUp() built, so the invariant passes over a state space of about one state — the alarm was tested while nobody ever got past the front door.

The handler pattern constrains randomness into meaningful randomness: pick an actor from a managed set, deal tokens, approve, bound() the amount into a range that can succeed, then call the vault. Ghost variables then do two jobs. One is accounting — a shadow ledger (sum of deposits, sum withdrawn) the invariant can assert against. The other is the card's real thesis: measurement. Per-action call and revert counters, dumped in a call-summary, make the distribution visible — if withdraw succeeded zero times in ten thousand calls, the green campaign proved nothing about withdrawals, and now that fact is on screen. The assertion is half the test; the distribution is the other half.

The seeded bug is the empirical proof. Plant a defect only reachable via deposit → transfer the shares to someone else → that person withdraws: open targeting essentially never lines those three calls up with consistent actors, while the handler campaign finds it quickly. Same assertion, same tool — only the action distribution differs, and only one campaign catches it. Foundry's fail_on_revert = true is the blunt version of this discipline: it forces handlers by making open targeting unsurvivable — useful as a forcing function, too strict as a default.

This connects directly to jayverse-defi (2026-09-07): its fuzz test already applies the philosophy in miniature — bound() on every input is handler thinking — but it is a single-sequence test, not a stateful campaign. A real campaign there would be a handler over deposit/wrap/unwrap/requestWithdraw/claim/addRewards/slash across several actors, ghost sums for the queue, and invariants like pool balance == totalPooledETH + pendingWithdrawalETH. The withdrawal queue — request needs shares, claim needs a time warp past readyAt — is exactly a sequence-only region open fuzzing would never touch, and the natural done path for this card.

← All Dev Notes · Workspace Index · Top ↑

Copy 한국어

Invariant 테스트는 도달하는 동작만큼만 좋다

Foundry 는 무작위 호출 순서 뒤에 속성을 검증할 수 있지만, 대부분의 호출이 revert 하거나 중요한 상태에 도달하지 못하면 초록색 캠페인은 거의 아무것도 증명하지 못합니다.

같은 ERC-4626 형태의 vault 를 두 번 시험합니다 — 먼저 컨트랙트를 직접 겨냥(open)하고, 다음에는 잔액과 승인을 준비하는 handler 방식으로. 호출/revert 분포와 ghost variable 회계를 추적하고, 입금-전송-출금 순서로만 도달할 수 있는 버그를 심습니다.

왜

상태 있는 퍼징은 표준 Solidity 도구가 되어 가고 있지만, 주된 실패 모드는 조용합니다: 생성기가 의미 있는 일을 한 번도 하지 못했기 때문에 테스트가 통과하는 것. 도달성 지표는 assertion 옆에 나란히 있어야 합니다.

Foundry 는 무작위 호출 순서 뒤에 invariant 를 검사합니다. 생성된 호출이 의미 있는 프로토콜 상태에 도달하기 전에 대부분 revert 하면, 캠페인은 거의 아무것도 하지 않고도 계속 초록색일 수 있습니다.

동작 방식

같은 vault 에 대해 open invariant 테스트와 handler 기반 버전을 작성하고, 호출/revert 분포를 비교하고, ghost variable 회계를 더하고, 순서로만 드러나는 버그를 의도적으로 심습니다.

PoC

같은 ERC-4626 형태의 vault 를 두 번 시험합니다: 먼저 컨트랙트를 직접 대상으로 삼고, 다음에는 잔액과 승인을 준비하는 handler 를 통해서. 메트릭과 ghost variable 로 호출, revert, 입금, 출금, 행위자, 도달 상태를 추적합니다. 입금-전송-출금 순서가 있어야 드러나는 버그를 심습니다.

무엇을 증명하나

Assertion 은 테스트의 절반뿐입니다. 동작 분포가 속성이 깨질 수 있는 상태 공간에 도달해야 합니다. open 방식과 handler 방식의 캠페인을 runs 와 depth 만이 아니라 coverage 와 의미 있는 상태 전이로 비교합니다.

참고: Foundry invariant testing.

검토 후 보완

통과한 캠페인의 의미는 둘 중 하나입니다 — 속성이 지켜졌다, 또는 깨뜨릴 만큼 가까이 가 본 적이 없다 — 그리고 Foundry 는 기본 설정으로는 어느 쪽인지 말해 주지 않습니다. open 타기팅에서는 무작위 호출자가 무작위 인자로 무작위 함수를 부르고, 거의 전부가 첫 require 에서 죽습니다: 셰어 없는 withdraw, 잔액도 승인도 없는 deposit. 수천 runs 뒤에도 vault 는 setUp() 이 만든 상태에서 거의 벗어나지 못해, invariant 는 사실상 상태 하나짜리 공간 위에서 통과합니다 — 정문을 한 번도 못 지나갔는데 경보기만 시험한 격입니다.

handler 패턴은 무작위성을 의미 있는 무작위성으로 제약합니다: 관리되는 액터 집합에서 하나 고르고, 토큰을 deal 하고, approve 하고, bound() 로 성공 가능한 범위로 묶은 뒤 vault 를 호출합니다. ghost variable 은 두 가지 일을 합니다. 하나는 회계 — invariant 가 대조할 그림자 장부(입금 합, 출금 합). 다른 하나가 이 카드의 진짜 논지인 측정입니다: 액션별 호출/revert 카운터를 콜 서머리로 출력하면 분포가 눈에 보입니다 — 1만 호출 중 withdraw 성공이 0회라면 그 초록 캠페인은 출금에 대해 아무것도 증명하지 않은 것이고, 이제 그 사실이 화면에 있습니다. assertion 은 테스트의 절반, 분포가 나머지 절반입니다.

심어 둔 버그가 실증입니다. 입금 → 셰어를 타인에게 전송 → 그 사람이 출금해야만 닿는 결함을 심으면: open 타기팅은 그 세 호출을 일관된 액터로 줄 세우는 일이 사실상 없고, handler 캠페인은 금방 찾습니다. 같은 assertion, 같은 도구 — 액션 분포만 다른데 한쪽만 잡습니다. Foundry 의 fail_on_revert = true 는 이 규율의 무딘 버전입니다: open 타기팅이 살아남을 수 없게 만들어 handler 작성을 강제합니다 — 강제 장치로는 유용하고, 기본값으로는 과합니다.

jayverse-defi(2026-09-07)와 직접 연결됩니다: 그 퍼즈 테스트는 이미 이 철학의 축소판이고 — 모든 입력의 bound() 가 곧 handler 식 사고 — 다만 단일 시퀀스 테스트이지 상태형 캠페인은 아닙니다. 진짜 캠페인이라면 여러 액터에 걸친 deposit/wrap/unwrap/requestWithdraw/claim/addRewards/slash handler, 큐를 위한 ghost 합계, 그리고 pool balance == totalPooledETH + pendingWithdrawalETH 같은 invariant 가 됩니다. 출금 큐 — 요청엔 셰어가, 클레임엔 readyAt 을 지나는 시간 워프가 필요 — 는 open 퍼징이 절대 못 건드리는 시퀀스 전용 영역이고, 이 카드의 자연스러운 done 경로입니다.

← 전체 개발 노트 · 워크스페이스 인덱스 · 맨 위 ↑