Conversation
Add a minimal Echidna setup (harness + config + runner) to fuzz StakeRegistry/TestToken invariants and provide a yarn script for local execution.
Update the stake coverage property to use nodeEffectiveStake and ignore Echidna's crytic-export output directory.
Add properties for successful manageStake(add>0) post-state (potential/balance deltas and commitment recomputation) and add non-interference checks so unrelated actors' stake entries never change during actions.
Add Echidna properties for freeze/slash/migrate post-state correctness, reset actor tracking on stake deletions, and make the runner compile on-host to avoid container npx/hardhat dependency.
Expose winnerSelection in the Redistribution harness to assert phase partitioning, reveal↔commit linkage, single winner selection per round, and freezing of non-revealers. Strengthen PostageStamp fuzzing with wider non-interference checks and a pot monotonicity invariant, and document the new properties.
Introduce a fuzz-only RedistributionClaimStub that bypasses proof verification and executes claim→withdraw end-to-end. Add pot mock + invariants for single-claim-per-round, winner payout, oracle adjustPrice call, and freezing non-revealers; wire the harness into the runner and docs.
Add system-level properties for stake accounting (stake token balance covers sum of potential stake), pot accounting (pot never exceeds stamp token balance), and price floors (oracle/stamp never below minimum).
Run Prettier (with Solidity plugin) to satisfy CI formatting checks.
There was a problem hiding this comment.
Really nice initiative with really a lot of changes.
It would have been better in several different PRs.
I checked the basic setup and the PriceOrcale harness mostly, but I peeked into other harness logics as well.
I stumbled upon an issue with running the test, see below.
|
|
||
| Echidna repeatedly calls the harness “action” functions (like `act_manageStake`) with random inputs, building **stateful sequences**. After (and during) those sequences it checks `echidna_*` property functions such as: | ||
|
|
||
| - **Token properties**: total supply stays constant; decimals stay 16 |
There was a problem hiding this comment.
True, was aimed for robustness and if in some cases code changes that we check every minor detail.
Logic wise how its now this would never happen.
There was a problem hiding this comment.
these kind of tests should be chai manual tests. shouldn't echidna check only state-model correctness?
IMO this does not need detailed testing because it doesn't replace targeted tests.
There was a problem hiding this comment.
Yes you are right
The right mental model would be
Chai tests = targeted, readable, scenario-driven tests
Echidna = randomized exploration of both global invariants and per-call correctness across arbitrary state histories
| echo "==> echidna: running contract $c" >&2 | ||
|
|
||
| # Avoid stale Crytic compile artifacts causing old properties/tests to run. | ||
| rm -rf crytic-export |
There was a problem hiding this comment.
This is wrong, the docker writes the files with root, and my user permission cannot remove it.
There was a problem hiding this comment.
Current scripts/echidna.sh no longer removes anything on the host.
It runs rm -rf crytic-export inside the same docker run as Echidna (sh -c 'rm -rf crytic-export && echidna-test …')
There was a problem hiding this comment.
I don't completely understand why crytic-export generated in the first place if you automatically remove it in each iteration?
There was a problem hiding this comment.
It's generated as a side effect of echidna-test. Every invocation of Echidna triggers CryticCompile, which writes to crytic-export/. We can't prevent that; we can only clean it before the next iteration so it doesn't contaminate the next contract's run.
| uint64 minUp = oracle.minimumPriceUpscaled(); | ||
| uint64 expected = uint64(p) << 10; | ||
| if (expected < minUp) expected = minUp; |
There was a problem hiding this comment.
why do you override expected like this? seemingly, the bit overflow is surpressed like this, but it can hide other problems too.
9694920 to
351eb8c
Compare
yes you are right. I remove one part into another PR that should be separate |
- Run rm + echidna in one Docker invocation so host users need not delete root-owned crytic-export - Point root README fuzz blurb at echidna/README.md (avoid stale harness list) - PriceOracle harness: arm setPrice postconditions only after ok+returned; read expected upscaled from oracle; expand _clearPending; merge paused/revert state checks with OR - System harness: replace tautological min(pot,bal)<=bal with pot<=token balance check - Redistribution harness: clear winnerSelection pending at start of every action Made-with: Cursor
- Run rm + echidna in one Docker invocation so host users need not delete root-owned crytic-export - Point root README fuzz blurb at echidna/README.md (avoid stale harness list) - PriceOracle harness: arm setPrice postconditions only after ok+returned; read expected upscaled from oracle; expand _clearPending; merge paused/revert state checks with OR - System harness: replace tautological min(pot,bal)<=bal with pot<=token balance check - Redistribution harness: clear winnerSelection pending at start of every action
…ng scratch - Claim harness: same stale-pending pattern as redistribution winnerSelection; non-claim actions now drop pendingClaim - Postage harness: _clearPending zeros all pending snapshot fields (parity with PriceOracle harness _clearPending)
Solidity public array getters revert on out-of-bounds access (mapped to currentCommits declaration in Redistribution.sol). Echidna traces those as failures even when wrapped in staticcall. - Add RedistributionExposed.sol with currentCommitsLength/currentRevealsLength - Bound redistribution + system harness scans using real lengths (cap 25) - Simplify _scanRevealsLen to use length instead of probing past end
- Run rm + echidna in one Docker invocation so host users need not delete root-owned crytic-export - Point root README fuzz blurb at echidna/README.md (avoid stale harness list) - PriceOracle harness: arm setPrice postconditions only after ok+returned; read expected upscaled from oracle; expand _clearPending; merge paused/revert state checks with OR - System harness: replace tautological min(pot,bal)<=bal with pot<=token balance check - Redistribution harness: clear winnerSelection pending at start of every action
4dabb17 to
e0bbd29
Compare
After a new commit round, commit() clears currentCommits but currentReveals is only reset when the reveal phase for that round starts. The property echidna_reveal_entries_imply_matching_commit incorrectly failed when a new unrevealed commit coexisted with prior-round reveals (Echidna counterexample: happyCommit → reveal → wait → happyCommit).
f7f55c2 to
ae49977
Compare
Stale currentReveals persist until the first reveal() of the new round updates currentRevealRound and deletes the array. That window includes reveal phase (currentPhaseCommit false), not only commit phase.
|
Made serious cleanups per suggestions above, keeping fuzz tests that makes most sense to be in Echidna. |
nugaon
left a comment
There was a problem hiding this comment.
according the redistribution tests coverage in the corpus, the reveal and the claim function logic is not even touched by the echidna tests.
I commented some of the lines where the workflow breaks.
The testcode does not bypass the block number related checks in these functions and the runs have really low chance to hit any of the phases of the redistribution game.
maybe maxBlockDelay could be changed in the Echidna conf file to a lower number.
| # and without Hardhat artifacts CryticCompile will try (and fail) to run `npx hardhat compile`. | ||
| yarn -s hardhat compile --force >/dev/null | ||
|
|
||
| CONTRACTS_DEFAULT=( |
There was a problem hiding this comment.
it could be dynamic instead of hardcoded.
| @@ -0,0 +1,280 @@ | |||
| --- | |||
| name: Security Findings Exploitability | |||
| bool okCall = actors[idx].callWinnerSelection(); | ||
| if (!okCall) return; |
great point, this setting was wrong completely. thank you |
maxBlockDelay 1000 made it nearly impossible for Echidna to land commit, reveal, and claim within the same 152-block round. Reducing to 38 (one phase width) lets the fuzzer naturally walk through all three phases. Also adds act_tick() no-ops so Echidna can advance block.number without running guard-clause logic.
- Increase seqLen 100→200 for better commit→reveal→claim coverage - Auto-discover Echidna*Harness.sol in runner script instead of hardcoded list - Remove phantom .gitignore entries (echidna/coverage/, echidna/out/) - Update README next-steps to mention auto-discovery naming convention - Remove unrelated .cursor/plans file from branch
- Remove unused _revealFull() helper from EchidnaRedistributionHarness - Remove dead seedBatch/Batch struct/mapping from redistribution stamp mock - Remove unread withdrawCalls from EchidnaPostageStampPotMock - Remove unread lastFreezeTime and lastRedundancy from shared mocks
… harness Add a shouldRevertWithdraw toggle to the pot mock so Echidna can explore the path where claimStub succeeds but PostageStamp.withdraw() fails via the .call() error-swallowing pattern. New property asserts pot and actor balances are preserved when withdraw reverts, while the round is still consumed (documenting the known H-1 behavior).
Add an Echidna harness that exercises the real redistribution claim verifier with fixed CAC/SOC proof fixtures and targeted mutations. Isolate its corpus/config and document the workflow so it can run independently from the shared suite.
Apply formatter output to the new real-claim Echidna harness and its README updates so the fixture-based claim fuzzing changes match the repository style.
|
Fixed previous discrepancies and comments and also added some fuzzing to claim function and separate config and corpus for it. |
Introduce Echidna-based, stateful fuzz testing for this repo.
Add a Docker-based runner and documentation, plus a multi-actor harness that fuzzes all smart contracts with role modeling, cross-actor accounting invariants, non-interference checks, and post-condition properties for all contracts.
What is fuzz testing?
Fuzz testing ("fuzzing") is an automated testing technique that repeatedly calls contract functions with many randomized inputs and stateful sequences of calls. Instead of writing a single expected-output test per scenario, you write properties/invariants that must always hold, and the fuzzer tries hard to find a sequence that breaks them.
Why use it for smart contracts?
Finds edge cases humans miss: weird input combinations, unusual call ordering, boundary values, and unexpected state transitions.
Stateful bugs: catches issues that only appear after many steps (e.g. stake -> freeze -> slash -> migrate -> restake).
Property-driven: you encode "this should never happen" rules (access control, accounting conservation, deletion semantics), and the tool searches for counterexamples.
Echidna coverage of the commit -> reveal -> claim lifecycle
What we test
Commit (well covered)
act_happyCommitin the redistribution harnesses constructs valid overlays, sets staking mock data, and callscommit()through actorsechidna_tracked_commit_matches_storage,echidna_commit_overlays_unique)Reveal (covered, though hit rate is still probabilistic in the general harnesses)
act_happyRevealreplays tracked pre-images from the same roundechidna_tracked_reveal_matches_storage,echidna_revealed_commit_indices_valid,echidna_reveal_entries_imply_matching_commit)Winner selection (covered via exposed internal)
act_winnerSelectionin the base harness callsexposedWinnerSelection()which runs the realwinnerSelection()internal function - this is the core claim logic:getCurrentTruth()truth determinationOracleContract.adjustPrice()callcurrentClaimRoundbookkeepingechidna_winnerSelection_only_once_per_round,echidna_last_winnerSelection_freezes_nonrevealedPot withdrawal (covered via claim stub)
claimStub()in the claim-stub harness runs realwinnerSelection()and then callsPostageStamp.withdraw(winner)directlyechidna_claim_withdraws_pot_to_winner_when_successful,echidna_claim_triggers_oracle_adjustPrice,echidna_claim_only_once_per_roundReal
claim()proof path (now covered with fixture-based fuzzing)EchidnaRedistributionRealClaimHarnessexercises the realRedistribution.claim()verifier path with fixed valid CAC and SOC proof bundlescommit -> reveal -> claimflow, then runs the actual proof-verifyingclaim()functionechidna_unmutated_fixture_claim_succeedsechidna_mutated_fixture_claim_does_not_succeedechidna_successful_real_claim_effects_holdWhy the real
claim()path needs a fixture-based approachNaive random fuzzing is very unlikely to hit a valid proof-verifying
claim()because the inputs must satisfy multiple correlated cryptographic relationships at once:These witnesses need to be constructed, not discovered by chance. The fixture-based harness solves this by seeding Echidna with valid proof bundles and then fuzzing mutations around them while still executing the real on-chain verifier logic.
Is the current coverage sufficient?
The split is now more complete and more intentional:
claim()verifier path via fixed CAC/SOC fixtures plus targeted proof mutationsSupporting runner/config changes
Also added:
echidna/echidna-real-claim.yamlECHIDNA_CONFIGsupport inscripts/echidna.shThis lets the real-claim harness use its own isolated corpus and run independently from the shared suite when needed.
Validation
Validated both with the dedicated run: