Add Echidna fuzz testing harness + runner

.gitignore

@@ -38,4 +38,8 @@ contractsInfo.json
 gas-report.txt
 
 # Tenderly
-tenderly.log
+tenderly.log
+
+# Echidna fuzzing
+echidna/corpus/
+crytic-export/

README.md

@@ -101,6 +101,14 @@ To get started with this project, follow these steps:
 2. Run `yarn install` at the root of the repo to install all dependencies.
 3. Add a `.env` file in your root directory, where you'll store your sensitive information for deployment. An example file [`.env.example`](./.env.example) is provided for reference.
 
+## Fuzz testing (Echidna)
+
+Harness layout, properties, and troubleshooting are documented in [echidna/README.md](./echidna/README.md). Run (Docker required):
+
+```bash
+yarn echidna
+```
+
 ## Run
 
 ### [Tests](./test)

echidna/README.md

@@ -0,0 +1,102 @@
+# Echidna fuzzing in this repo
+
+Stateful fuzzing with [Echidna](https://github.com/crytic/echidna): deploy a **harness**, call its `act_*` functions in random **sequences**, and check that `echidna_*` **properties** stay `true`. A failing property prints a **reproducer** (call sequence + inputs).
+
+Source: `src/echidna/` (harnesses), `echidna/echidna.yaml` (defaults), `scripts/echidna.sh` (Docker runner).
+
+## Concepts
+
+| Piece | Role |
+|-------|------|
+| `act_*` | Fuzz actions — drive state on deployed contracts. |
+| `echidna_*` | Invariants — must always return `true`. |
+| `Echidna*Actor` | Separate `msg.sender` for role tests; usually `.call()` so expected reverts don’t abort the `act_*` step. |
+| `act_happy*` | Pre-conditioned inputs (tracked preimages, mock stake, phase/round) so commit/reveal are **likely** to succeed. |
+| Harness stack | `act_claimStub` → actor `callClaimStub` → `RedistributionClaimStub.claimStub()`. |
+
+**Mocks** trim dependencies to what the unit under test needs (e.g. oracle harness: postage `setPrice` + optional revert only). **System harness** uses real cross-contract wiring.
+
+**If a property fails:** real on-chain bug, too-strong property, or bad harness setup (roles/assumptions). Continuing after an expected revert only means the **next** fuzz step runs on unchanged storage — not that the protocol ignored the revert.
+
+## Harnesses
+
+| Harness | File | Under test | Focus |
+|---------|------|------------|--------|
+| Staking | `EchidnaStakeRegistryHarness.sol` | `StakeRegistry` | stake, freeze, slash, migrate, roles |
+| Oracle | `EchidnaPriceOracleHarness.sol` | `PriceOracle` | price, pause, `adjustPrice`, postage callback fail/revert |
+| Postage | `EchidnaPostageStampHarness.sol` | `PostageStamp` | batches, pot, expiry, roles |
+| Redistribution (base) | `EchidnaRedistributionHarness.sol` | `RedistributionExposed` | commit/reveal ledger, `winnerSelection`, dummy `claim()` |
+| Redistribution (claim) | `EchidnaRedistributionClaimHarness.sol` | `RedistributionClaimStub` | claim-phase pot, withdraw, rounds, H-1 |
+| System | `EchidnaSystemHarness.sol` | full wired stack | cross-contract invariants only |
+
+**Support (not Echidna targets):** `RedistributionExposed.sol` (`winnerSelection`, safe array lengths); `EchidnaMocks.sol` (stake + oracle mocks for redistribution harnesses).
+
+**Proof verification:** real `claim()` with Merkle/SOC/postage proofs → Hardhat `test/Redistribution.test.ts`. Echidna cannot generate valid proofs; base harness uses dummy calldata (`act_claim`) only to stress panics/guards.
+
+### Redistribution: base vs claim-stub
+
+| | Base | Claim-stub |
+|--|------|------------|
+| Deploy | `RedistributionExposed` + mocks (withdraw counter, no token pot) | `RedistributionClaimStub` + `TestToken` + pot mock (balance, optional withdraw revert) |
+| Claim | `act_claim` → real `claim()`, proofs almost always revert | `act_claimStub` → `claimStub()` = `winnerSelection()` + `withdraw` (no proof checks) |
+| Winner | `act_winnerSelection` | inside `claimStub()` |
+| Happy path | `act_happyCommit` → `act_happyReveal` | + `act_claimStub` |
+| Also | random commit/reveal, admin tuning | `act_seedPot`, `act_setWithdrawRevertMode` |
+
+```text
+Base:   commit ─ reveal ─ [winnerSelection] ─ act_claim(dummy → revert)
+Claim:  happy commit ─ happy reveal ─ claimStub (winner + pot)
+System: real contracts; happy commit/reveal only
+```
+
+## Actions (by harness)
+
+Written to be **mostly non-reverting** (bounded inputs, low-level calls) so sequences stay long.
+
+- **Staking:** `act_actor_manageStake`, `withdrawSurplus`, `migrateStake`; admin pause/unpause/networkId; redistributor freeze/slash; `act_actor_try*`; `act_fundActor`
+- **Oracle:** `act_admin_setPrice`, pause/unpause; `act_updater_adjustPrice`; `act_rando_try*`; `act_setStampRevertMode`
+- **Postage:** `act_createBatch`, `topUp`, `increaseDepth`, `expireAll`; `act_oracle_setPrice`; `act_redistributor_withdraw`; pauser pause/unpause; `act_rando_try*`; `act_fundActor`
+- **Redistribution (base):** `act_commit`, `reveal`, `claim`; `act_happyCommit`, `happyReveal`; `act_winnerSelection`; `act_setActorStake`; admin pause/unpause/sample/freezing
+- **Redistribution (claim):** `act_happyCommit`, `happyReveal`, `claimStub`; `act_seedPot`, `setWithdrawRevertMode`, `setActorNode`; `act_tick`
+- **System:** stake/postage/oracle actions above + `act_redist_happyCommit`, `happyReveal`
+
+## Properties (by harness)
+
+Patterns: **must-never-happen** (auth), **global invariants**, **post-conditions** on last successful action (`pending*` flags).
+
+- **Staking:** `echidna_never_performed_forbidden_calls`; registry balance vs potential stake; per-actor stake/overlay/freeze; post-conditions for manageStake/freeze/slash/migrate
+- **Oracle:** forbidden calls; price ≥ minimum; `lastAdjustedRound` not in future; post-conditions for `setPrice` / `adjustPrice`
+- **Postage:** forbidden calls; batch post-conditions; `expireAll`; withdraw/pot; `echidna_pot_never_decreases_except_withdraw`
+- **Redistribution (base):** `echidna_commit_overlays_unique`, `revealed_commit_indices_valid`, `reveal_entries_imply_matching_commit`, `winnerSelection_only_once_per_round`, `last_winnerSelection_freezes_nonrevealed`, `tracked_commit_matches_storage`, `tracked_reveal_matches_storage`  
+  _(AccessControl/Pausable/phase math: Hardhat, not fuzzed here.)_
+- **Redistribution (claim):** `echidna_claim_only_once_per_round`, `claim_withdraws_pot_to_winner_when_successful`, `failed_withdraw_preserves_pot_and_consumes_round`, `claim_triggers_oracle_adjustPrice`, `nonrevealers_frozen_after_claim_selection`
+- **System:** oracle price ↔ stamp `lastPrice`; stamp pot ≤ balance; unauthorized oracle adjust fails; tracked commit/reveal in storage
+
+## Triage example
+
+`manageStake` with `_addAmount == 0` can change `height` without recomputing `committedStake` — so \( committedStake \cdot 2^{height} \le potentialStake \) is **not** a valid invariant (property failed correctly during bring-up).
+
+Other false-positive sources: harness grants roles it shouldn’t; property assumes unreachable state; too many action reverts (weak exploration).
+
+## How to run
+
+```bash
+yarn echidna   # all harnesses; needs Docker
+```
+
+| Setting | Default | Override env |
+|---------|---------|----------------|
+| `testLimit` | 60000 | `ECHIDNA_TEST_LIMIT` |
+| `seqLen` | 320 | `ECHIDNA_SEQ_LEN` |
+| `maxBlockDelay` | 152 | — |
+| workers | yaml | `ECHIDNA_WORKERS` |
+
+Single harness: `ECHIDNA_CONTRACT=EchidnaRedistributionHarness yarn echidna` (also: `EchidnaStakeRegistryHarness`, `EchidnaPriceOracleHarness`, `EchidnaPostageStampHarness`, `EchidnaRedistributionClaimHarness`, `EchidnaSystemHarness`).
+
+Config: `echidna/echidna.yaml` (`ECHIDNA_CONFIG` to override). Corpus/coverage: `echidna/corpus/by-contract/<HarnessName>/` (gitignored). Crytic: `crytic-export/`.
+
+## Extend
+
+1. Add `src/echidna/Echidna*Harness.sol` — auto-discovered by `scripts/echidna.sh`.
+2. Prefer non-reverting `act_*`, explicit roles, a few solid properties first.
+3. On counterexample: bug vs property vs harness — then fix code or narrow the invariant.

echidna/echidna.yaml

@@ -0,0 +1,30 @@
+testMode: property
+
+# Longer sequences help (a) reach high `block.number` / `currentRound()` for redistribution,
+# and (b) walk commit → reveal → claim in one campaign. Tuned with real-claim fixture harness in mind.
+seqLen: 320
+
+# Default budget per harness (one sequence = up to seqLen txs). Override with ECHIDNA_TEST_LIMIT.
+testLimit: 60000
+
+# Shrinking a counterexample can be *much* slower than fuzzing.
+# Keep this modest; increase locally if you want a smaller reproducer.
+shrinkLimit: 1000
+
+# Bound random block jumps between transactions.
+# Up to a full round (ROUND_LENGTH) helps reach later `currentRound()` values with fewer txs;
+# sub-round delays still let the same sequence walk commit → reveal → claim.
+maxTimeDelay: 0
+maxBlockDelay: 152
+
+# Persist interesting inputs between runs (scripts/echidna.sh uses a per-harness subdir).
+corpusDir: echidna/corpus
+
+# Useful while iterating on invariants.
+coverage: true
+
+# Explicit parallelism inside Docker (host CPU may allow more).
+workers: 4
+
+# Keep output readable in CI.
+format: text

package.json

@@ -61,6 +61,7 @@
     "test:coverage": "hardhat coverage",
     "dev": "hardhat node --reset --watch --export contractsInfo.json",
     "compile": "hardhat compile",
+    "echidna": "bash scripts/echidna.sh",
     "local:deploy": "hardhat --network localhost deploy",
     "local:run": "cross-env HARDHAT_NETWORK=localhost ts-node --files",
     "local:export": "hardhat --network localhost export",

scripts/echidna.sh

@@ -0,0 +1,73 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+ROOT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
+
+if ! command -v docker >/dev/null 2>&1; then
+  echo "docker not found. Install Docker Desktop (or another docker runtime) to run Echidna." >&2
+  exit 127
+fi
+
+cd "$ROOT_DIR"
+
+IMAGE="${ECHIDNA_IMAGE:-ghcr.io/crytic/echidna/echidna:latest}"
+CONTRACT="${ECHIDNA_CONTRACT:-}"
+CONFIG="${ECHIDNA_CONFIG:-echidna/echidna.yaml}"
+
+# Crytic-compile reads artifacts/build-info when using --hardhat-ignore-compile inside Docker (no Node/npx).
+# Stale build-info from deleted Solidity sources causes "Unknown file" failures.
+rm -rf artifacts/build-info
+
+# Compile on the host. The Echidna container image doesn't ship with Node/npx,
+# and without Hardhat artifacts CryticCompile will try (and fail) to run `npx hardhat compile`.
+yarn -s hardhat compile --force >/dev/null
+
+# Auto-discover harness contracts from src/echidna/Echidna*Harness.sol.
+CONTRACTS_DEFAULT=()
+for f in src/echidna/Echidna*Harness.sol; do
+  [[ -f "$f" ]] || continue
+  name="$(basename "$f" .sol)"
+  CONTRACTS_DEFAULT+=("$name")
+done
+
+if [[ -n "$CONTRACT" ]]; then
+  CONTRACTS_TO_RUN=("$CONTRACT")
+else
+  CONTRACTS_TO_RUN=("${CONTRACTS_DEFAULT[@]}")
+fi
+
+# Optional CLI overrides (see `echidna-test --help`). Defaults live in ECHIDNA_CONFIG (typically
+# echidna/echidna.yaml: testLimit 60000, seqLen 320). Examples:
+#   ECHIDNA_TEST_LIMIT=20000 ECHIDNA_SEQ_LEN=200 yarn echidna   # faster smoke
+#   ECHIDNA_WORKERS=8 ECHIDNA_CONTRACT=EchidnaSystemHarness yarn echidna
+# Use a string (not an array) so `set -u` never trips on empty `${arr[*]}` on older Bash.
+ECHIDNA_EXTRA_CLI=""
+if [[ -n "${ECHIDNA_TEST_LIMIT:-}" ]]; then
+  ECHIDNA_EXTRA_CLI+=" --test-limit ${ECHIDNA_TEST_LIMIT}"
+fi
+if [[ -n "${ECHIDNA_SEQ_LEN:-}" ]]; then
+  ECHIDNA_EXTRA_CLI+=" --seq-len ${ECHIDNA_SEQ_LEN}"
+fi
+if [[ -n "${ECHIDNA_WORKERS:-}" ]]; then
+  ECHIDNA_EXTRA_CLI+=" --workers ${ECHIDNA_WORKERS}"
+fi
+
+for c in "${CONTRACTS_TO_RUN[@]}"; do
+  echo "==> echidna: running contract $c" >&2
+
+  # One corpus + coverage tree per harness so saved sequences stay relevant to
+  # that contract (shared corpus mixed unrelated call shapes and diluted learning).
+  CORPUS_DIR="echidna/corpus/by-contract/${c}"
+  mkdir -p "${ROOT_DIR}/${CORPUS_DIR}"
+
+  # Drop stale Crytic output inside Docker (same uid as container root). A host
+  # `rm -rf crytic-export` often fails after Docker created the dir as root.
+  docker run --rm \
+    --entrypoint sh \
+    -v "$ROOT_DIR":/src \
+    -w /src \
+    "$IMAGE" \
+    -c "rm -rf crytic-export && echidna-test . --contract ${c} --config ${CONFIG} \
+      --corpus-dir ${CORPUS_DIR} --coverage-dir ${CORPUS_DIR}/coverage${ECHIDNA_EXTRA_CLI} \
+      --crytic-args '--hardhat-ignore-compile'"
+done

src/PostageStamp.sol

@@ -566,7 +566,8 @@ contract PostageStamp is AccessControl, Pausable {
     }
 
     function minimumInitialBalancePerChunk() public view returns (uint256) {
-        return minimumValidityBlocks * lastPrice;
+        // Cast to uint256 before multiplying to avoid uint64 overflow.
+        return uint256(minimumValidityBlocks) * uint256(lastPrice);
     }
 
     /**

src/PriceOracle.sol

@@ -41,6 +41,11 @@ contract PriceOracle is AccessControl {
     // The length of a round in blocks.
     uint8 private constant ROUND_LENGTH = 152;
 
+    /// @dev Upper bound for upscaled price so `(currentPriceUpScaled >> 10)` fits in `uint32`.
+    /// Without this, `currentPrice()`'s `uint32(... >> 10)` truncates and can disagree with
+    /// `currentPriceUpScaled` and under-report vs `minimumPrice()`.
+    uint64 public constant MAX_CURRENT_PRICE_UPSCALED = uint64(uint256(type(uint32).max) << 10);
+
     // ----------------------------- Events ------------------------------
 
     /**
@@ -78,13 +83,9 @@ contract PriceOracle is AccessControl {
             revert CallerNotAdmin();
         }
 
-        uint64 _currentPriceUpScaled = _price << 10;
-        uint64 _minimumPriceUpscaled = minimumPriceUpscaled;
-
-        // Enforce minimum price
-        if (_currentPriceUpScaled < _minimumPriceUpscaled) {
-            _currentPriceUpScaled = _minimumPriceUpscaled;
-        }
+        // Cast before shifting to avoid uint32 overflow/truncation.
+        uint64 _currentPriceUpScaled = uint64(_price) << 10;
+        _currentPriceUpScaled = _clampPriceUpscaled(_currentPriceUpScaled);
         currentPriceUpScaled = _currentPriceUpScaled;
 
         // Check if the setting of price in postagestamp succeded
@@ -124,7 +125,6 @@ contract PriceOracle is AccessControl {
             }
 
             uint64 _currentPriceUpScaled = currentPriceUpScaled;
-            uint64 _minimumPriceUpscaled = minimumPriceUpscaled;
             uint32 _priceBase = priceBase;
 
             // Set the number of rounds that were skipped, we substract 1 as lastAdjustedRound is set below and default result is 1
@@ -142,10 +142,7 @@ contract PriceOracle is AccessControl {
                 }
             }
 
-            // Enforce minimum price
-            if (_currentPriceUpScaled < _minimumPriceUpscaled) {
-                _currentPriceUpScaled = _minimumPriceUpscaled;
-            }
+            _currentPriceUpScaled = _clampPriceUpscaled(_currentPriceUpScaled);
 
             currentPriceUpScaled = _currentPriceUpScaled;
             lastAdjustedRound = currentRoundNumber;
@@ -182,6 +179,18 @@ contract PriceOracle is AccessControl {
     //            STATE READING           //
     ////////////////////////////////////////
 
+    /// @notice Clamp upscaled price to [minimumPriceUpscaled, MAX_CURRENT_PRICE_UPSCALED].
+    function _clampPriceUpscaled(uint64 priceUpScaled) private view returns (uint64) {
+        uint64 minU = uint64(minimumPriceUpscaled);
+        if (priceUpScaled < minU) {
+            priceUpScaled = minU;
+        }
+        if (priceUpScaled > MAX_CURRENT_PRICE_UPSCALED) {
+            priceUpScaled = MAX_CURRENT_PRICE_UPSCALED;
+        }
+        return priceUpScaled;
+    }
+
     /**
      * @notice Return the number of the current round.
      */

src/Redistribution.sol

@@ -671,8 +671,13 @@ contract Redistribution is AccessControl, Pausable {
      * @notice Updates the source of randomness. Uses block.difficulty in pre-merge chains, this is substituted
      * to block.prevrandao in post merge chains.
      */
-    function updateRandomness() private {
-        seed = keccak256(abi.encode(seed, block.prevrandao));
+    function updateRandomness() internal virtual {
+        seed = _nextSeedValue();
+    }
+
+    /// @dev Extracted for fuzz harnesses that must pin post-reveal randomness to fixture data.
+    function _nextSeedValue() internal view virtual returns (bytes32) {
+        return keccak256(abi.encode(seed, block.prevrandao));
     }
 
     /**