diff --git a/.gitignore b/.gitignore index f0d92eca..61d01e91 100644 --- a/.gitignore +++ b/.gitignore @@ -38,4 +38,8 @@ contractsInfo.json gas-report.txt # Tenderly -tenderly.log \ No newline at end of file +tenderly.log + +# Echidna fuzzing +echidna/corpus/ +crytic-export/ \ No newline at end of file diff --git a/README.md b/README.md index adcda8ac..4a600352 100644 --- a/README.md +++ b/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) diff --git a/echidna/README.md b/echidna/README.md new file mode 100644 index 00000000..130bb3f0 --- /dev/null +++ b/echidna/README.md @@ -0,0 +1,137 @@ +# 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). + +## How a campaign works (newcomers) + +Echidna does **not** run all actions at once. Each **sequence** is one fresh harness deploy, then up to **`seqLen` steps** (default **320**). Each step = **one** `act_*` call with pseudo-random arguments. Between steps Echidna may advance `block.number` by up to **`maxBlockDelay`** (default **152**, one redistribution round). + +Example sequence: + +```text +deploy harness +→ act_happyCommit(0, …) +→ act_tick() +→ act_updater_adjustPrice(3) +→ act_rando_tryAdjustPrice(1, 2) +→ act_happyReveal(0) +→ … (up to 320 steps) +``` + +After **every** step, **all** `echidna_*` properties (invariants) are checked. They must return `true`. If one fails, Echidna saves that prefix as a **reproducer**: + +```text +act_A() → check all echidna_* ✓ +act_B() → check all echidna_* ✓ +act_C() → check all echidna_* ✗ → FAIL, report sequence A → B → C +``` + +Echidna then tries many such sequences (**`testLimit`**, default **60 000**). Each sequence starts from a **new deploy** (constructor runs again). Which action runs next is guided by randomness + coverage/corpus—not a fixed script. + +| Term | Meaning | +|------|---------| +| **One sequence** | Up to 320 txs on one deployment | +| **One tx** | One `act_*` (or other callable on the harness) | +| **Properties** | Invariants checked **after each tx**, not only at the end | +| **Campaign** | 60 000 sequences × up to 320 steps (per harness) | + +**Actions** = moves in a long random game. **Properties** = rules that must hold after every move. + +## 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//` (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. diff --git a/echidna/echidna.yaml b/echidna/echidna.yaml new file mode 100644 index 00000000..2f98c383 --- /dev/null +++ b/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 diff --git a/package.json b/package.json index bcaf1539..3efd28d6 100644 --- a/package.json +++ b/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", diff --git a/scripts/echidna-coverage-summary.ts b/scripts/echidna-coverage-summary.ts new file mode 100644 index 00000000..49980142 --- /dev/null +++ b/scripts/echidna-coverage-summary.ts @@ -0,0 +1,180 @@ +/** + * Summarize Echidna LCOV coverage with action-only metrics. + * + * Echidna records coverage during fuzz transactions (act_*). echidna_* property + * checks run afterward via eth_call and are omitted from this summary. + * + * Usage: + * yarn ts-node scripts/echidna-coverage-summary.ts + * yarn ts-node scripts/echidna-coverage-summary.ts EchidnaRedistributionHarness + * yarn ts-node scripts/echidna-coverage-summary.ts EchidnaRedistributionHarness --coverage-dir echidna/corpus/by-contract/EchidnaRedistributionHarness/coverage + */ + +import * as fs from 'fs'; +import * as path from 'path'; + +const ROOT = path.resolve(__dirname, '..'); +const HARNESS_DIR = path.join(ROOT, 'src', 'echidna'); + +type CoverageTriple = [pct: number, covered: number, total: number]; + +interface Summary { + harness: string; + lcov: string; + fileTotal: CoverageTriple; + actions: CoverageTriple; +} + +function discoverHarnesses(): string[] { + return fs + .readdirSync(HARNESS_DIR) + .filter((f) => /^Echidna.*Harness\.sol$/.test(f)) + .map((f) => path.basename(f, '.sol')) + .sort(); +} + +function harnessContractStart(lines: string[], harness: string): number { + const needle = `contract ${harness}`; + for (let i = 0; i < lines.length; i++) { + if (lines[i].startsWith(needle)) return i + 1; + } + throw new Error(`contract ${harness} not found in src/echidna/${harness}.sol`); +} + +function actionsSectionEnd(lines: string[], harnessStart: number): number { + for (let i = harnessStart; i <= lines.length; i++) { + const line = lines[i - 1].trim(); + if (line.startsWith('//') && line.includes('Properties')) return i; + } + for (let i = harnessStart; i <= lines.length; i++) { + if (lines[i - 1].includes('function echidna_')) return i; + } + return lines.length + 1; +} + +function latestLcov(coverageDir: string): string | null { + if (!fs.existsSync(coverageDir)) return null; + const files = fs + .readdirSync(coverageDir) + .filter((f) => /^covered\..*\.lcov$/.test(f)) + .map((f) => path.join(coverageDir, f)) + .sort((a, b) => fs.statSync(a).mtimeMs - fs.statSync(b).mtimeMs); + return files.length > 0 ? files[files.length - 1] : null; +} + +function parseLcovHits(lcovPath: string, harness: string): Map { + const text = fs.readFileSync(lcovPath, 'utf8'); + const suffix = `/${harness}.sol`; + let blockStart = -1; + for (const match of text.matchAll(/^SF:(.+)$/gm)) { + if (match[1].endsWith(suffix)) blockStart = match.index ?? -1; + } + if (blockStart < 0) { + throw new Error(`${harness}.sol not present in ${path.basename(lcovPath)}`); + } + + const rest = text.slice(blockStart); + const end = rest.indexOf('end_of_record'); + const block = end >= 0 ? rest.slice(0, end) : rest; + + const hits = new Map(); + for (const line of block.split('\n')) { + if (!line.startsWith('DA:')) continue; + const [lnS, cntS] = line.slice(3).split(',', 2); + hits.set(Number(lnS), Number(cntS)); + } + return hits; +} + +function coveragePct(hits: Map, lo: number, hi: number): CoverageTriple { + const lines: number[] = []; + for (let ln = lo; ln <= hi; ln++) { + if (hits.has(ln)) lines.push(ln); + } + if (lines.length === 0) return [0, 0, 0]; + const covered = lines.filter((ln) => (hits.get(ln) ?? 0) > 0).length; + return [(100 * covered) / lines.length, covered, lines.length]; +} + +function summarize(harness: string, coverageDir: string): Summary | null { + const srcPath = path.join(HARNESS_DIR, `${harness}.sol`); + if (!fs.existsSync(srcPath)) { + throw new Error(`missing source file ${srcPath}`); + } + + const lcovPath = latestLcov(coverageDir); + if (!lcovPath) return null; + + const lines = fs.readFileSync(srcPath, 'utf8').split('\n'); + const harnessStart = harnessContractStart(lines, harness); + const actionsEnd = actionsSectionEnd(lines, harnessStart); + const hits = parseLcovHits(lcovPath, harness); + + return { + harness, + lcov: path.basename(lcovPath), + fileTotal: coveragePct(hits, 1, lines.length), + actions: coveragePct(hits, harnessStart, actionsEnd - 1), + }; +} + +function fmtPct([pct, covered, total]: CoverageTriple): string { + return `${pct.toFixed(1).padStart(5)}% (${covered}/${total})`; +} + +function printSummary(result: Summary): void { + console.log(`==> echidna coverage: ${result.harness} (${result.lcov})`); + console.log(` harness file total: ${fmtPct(result.fileTotal)}`); + console.log(` actions only: ${fmtPct(result.actions)}`); +} + +function parseArgs(argv: string[]): { harnesses: string[]; coverageDir?: string } { + const harnesses: string[] = []; + let coverageDir: string | undefined; + + for (let i = 0; i < argv.length; i++) { + const arg = argv[i]; + if (arg === '--coverage-dir') { + coverageDir = argv[++i]; + if (!coverageDir) throw new Error('--coverage-dir requires a path'); + continue; + } + if (arg.startsWith('-')) { + throw new Error(`unknown option ${arg}`); + } + harnesses.push(arg); + } + + return { harnesses, coverageDir }; +} + +function main(): number { + const { harnesses: argHarnesses, coverageDir: globalCoverageDir } = parseArgs(process.argv.slice(2)); + const harnesses = argHarnesses.length > 0 ? argHarnesses : discoverHarnesses(); + if (harnesses.length === 0) { + console.error('no harness contracts found'); + return 1; + } + + let exitCode = 0; + for (const harness of harnesses) { + const coverageDir = globalCoverageDir ?? path.join(ROOT, 'echidna', 'corpus', 'by-contract', harness, 'coverage'); + + try { + const result = summarize(harness, coverageDir); + if (!result) { + console.error(`==> echidna coverage: ${harness}: no covered.*.lcov in ${coverageDir}`); + continue; + } + printSummary(result); + } catch (err) { + const msg = err instanceof Error ? err.message : String(err); + console.error(`==> echidna coverage: ${harness}: ${msg}`); + exitCode = 1; + } + } + + return exitCode; +} + +process.exit(main()); diff --git a/scripts/echidna.sh b/scripts/echidna.sh new file mode 100755 index 00000000..50d454b4 --- /dev/null +++ b/scripts/echidna.sh @@ -0,0 +1,76 @@ +#!/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'" + + yarn -s ts-node "${ROOT_DIR}/scripts/echidna-coverage-summary.ts" "${c}" \ + --coverage-dir "${ROOT_DIR}/${CORPUS_DIR}/coverage" || true +done diff --git a/src/echidna/EchidnaMocks.sol b/src/echidna/EchidnaMocks.sol new file mode 100644 index 00000000..bb00eff1 --- /dev/null +++ b/src/echidna/EchidnaMocks.sol @@ -0,0 +1,66 @@ +// SPDX-License-Identifier: BSD-3-Clause +pragma solidity ^0.8.19; + +import "../Redistribution.sol"; + +/// @notice Shared stake registry mock for redistribution harnesses. +contract EchidnaStakeRegistryMock is IStakeRegistry { + struct Node { + bytes32 overlay; + uint8 height; + uint256 effectiveStake; + uint256 lastUpdated; + bool exists; + } + + mapping(address => Node) internal nodes; + mapping(address => uint256) public freezeCount; + + function setNode( + address owner, + bytes32 overlay, + uint8 height, + uint256 effectiveStake, + uint256 lastUpdated + ) external { + nodes[owner] = Node({ + overlay: overlay, + height: height, + effectiveStake: effectiveStake, + lastUpdated: lastUpdated, + exists: true + }); + } + + function freezeDeposit(address _owner, uint256 _time) external { + if (!nodes[_owner].exists) return; + freezeCount[_owner] += 1; + nodes[_owner].lastUpdated = block.number + _time; + } + + function lastUpdatedBlockNumberOfAddress(address _owner) external view returns (uint256) { + return nodes[_owner].lastUpdated; + } + + function overlayOfAddress(address _owner) external view returns (bytes32) { + return nodes[_owner].overlay; + } + + function heightOfAddress(address _owner) external view returns (uint8) { + return nodes[_owner].height; + } + + function nodeEffectiveStake(address _owner) external view returns (uint256) { + return nodes[_owner].effectiveStake; + } +} + +/// @notice Shared price oracle mock for redistribution harnesses. +contract EchidnaPriceOracleMock is IPriceOracle { + uint256 public calls; + + function adjustPrice(uint16) external returns (bool) { + calls += 1; + return true; + } +} diff --git a/src/echidna/EchidnaPostageStampHarness.sol b/src/echidna/EchidnaPostageStampHarness.sol new file mode 100644 index 00000000..34a6d924 --- /dev/null +++ b/src/echidna/EchidnaPostageStampHarness.sol @@ -0,0 +1,624 @@ +// SPDX-License-Identifier: BSD-3-Clause +pragma solidity ^0.8.19; + +import "../TestToken.sol"; +import "../PostageStamp.sol"; + +contract EchidnaPostageActor { + TestToken internal immutable token; + PostageStamp internal immutable stamp; + + constructor(TestToken token_, PostageStamp stamp_) { + token = token_; + stamp = stamp_; + token.approve(address(stamp), type(uint256).max); + } + + function createBatchMutable( + uint256 initialBalancePerChunk, + uint8 depth, + uint8 bucketDepth, + bytes32 nonce + ) external returns (bool ok, bytes32 batchId) { + bytes memory data; + (ok, data) = address(stamp).call( + abi.encodeWithSelector( + stamp.createBatch.selector, + address(this), + initialBalancePerChunk, + depth, + bucketDepth, + nonce, + false + ) + ); + if (ok && data.length >= 32) batchId = abi.decode(data, (bytes32)); + } + + function createBatchImmutable( + uint256 initialBalancePerChunk, + uint8 depth, + uint8 bucketDepth, + bytes32 nonce + ) external returns (bool ok, bytes32 batchId) { + bytes memory data; + (ok, data) = address(stamp).call( + abi.encodeWithSelector( + stamp.createBatch.selector, + address(this), + initialBalancePerChunk, + depth, + bucketDepth, + nonce, + true + ) + ); + if (ok && data.length >= 32) batchId = abi.decode(data, (bytes32)); + } + + function topUp(bytes32 batchId, uint256 topupAmountPerChunk) external returns (bool ok) { + (ok, ) = address(stamp).call(abi.encodeWithSelector(stamp.topUp.selector, batchId, topupAmountPerChunk)); + } + + function increaseDepth(bytes32 batchId, uint8 newDepth) external returns (bool ok) { + (ok, ) = address(stamp).call(abi.encodeWithSelector(stamp.increaseDepth.selector, batchId, newDepth)); + } + + function trySetPrice(uint256 price) external returns (bool ok) { + (ok, ) = address(stamp).call(abi.encodeWithSelector(stamp.setPrice.selector, price)); + } + + function tryWithdraw(address beneficiary) external returns (bool ok) { + (ok, ) = address(stamp).call(abi.encodeWithSelector(stamp.withdraw.selector, beneficiary)); + } + + function tryPause() external returns (bool ok) { + (ok, ) = address(stamp).call(abi.encodeWithSelector(stamp.pause.selector)); + } + + function tryUnpause() external returns (bool ok) { + (ok, ) = address(stamp).call(abi.encodeWithSelector(stamp.unPause.selector)); + } +} + +/// @notice Echidna harness for PostageStamp state machine and invariants. +contract EchidnaPostageStampHarness { + TestToken internal immutable token; + PostageStamp internal immutable stamp; + + uint256 internal constant ACTOR_COUNT = 3; + EchidnaPostageActor[3] internal actors; + EchidnaPostageActor internal oracleActor; + EchidnaPostageActor internal redistributorActor; + EchidnaPostageActor internal pauserActor; + + // Ring buffer of observed batchIds. + uint256 internal constant MAX_TRACKED = 16; + bytes32[MAX_TRACKED] internal tracked; + uint256 internal trackedCount; + + // Forbidden-call flags. + bool internal unauthorizedPriceSetSucceeded; + bool internal unauthorizedWithdrawSucceeded; + bool internal unauthorizedPauseSucceeded; + bool internal pausedMutationSucceeded; + bool internal nonInterferenceViolated; + bool internal potDecreasedUnexpectedly; + + // Pending postconditions (cleared on each action). + bool internal pendingCreate; + bytes32 internal pendingBatchId; + uint256 internal pendingCreateTotalAmount; + uint256 internal pendingStampTokenBalanceBefore; + uint256 internal pendingCreateNormalisedExpected; + uint8 internal pendingCreateDepth; + uint8 internal pendingCreateBucketDepth; + bool internal pendingCreateImmutable; + + bool internal pendingTopUp; + bytes32 internal pendingTopUpBatchId; + uint256 internal pendingTopUpTokenBefore; + uint256 internal pendingTopUpNormalisedBefore; + uint256 internal pendingTopUpTotalAmount; + uint256 internal pendingTopUpPerChunk; + + bool internal pendingIncreaseDepth; + bytes32 internal pendingIncBatchId; + uint8 internal pendingIncOldDepth; + uint8 internal pendingIncNewDepth; + uint256 internal pendingIncValidChunkBefore; + uint256 internal pendingIncTokenBefore; + uint8 internal pendingIncBucketDepth; + uint256 internal pendingIncExpectedNormalised; + + bool internal pendingExpireAll; + + bool internal pendingSetPrice; + uint256 internal pendingSetPriceTotalOutPaymentBefore; + uint64 internal pendingSetPriceLastUpdatedExpected; + uint64 internal pendingSetPriceLastPriceExpected; + + bool internal pendingWithdraw; + address internal pendingWithdrawBeneficiary; + uint256 internal pendingWithdrawBeneficiaryBalBefore; + uint256 internal pendingWithdrawExpectedAmount; + uint256 internal pendingWithdrawStampBalBefore; + + // Temporary inputs to reduce stack pressure in helpers. + bytes32 internal tmpNonce; + bool internal tmpImmutable; + bytes32 internal tmpBatchA; + bytes32 internal tmpBatchB; + bytes32 internal tmpBatchC; + bytes32 internal tmpBatchD; + bytes32 internal tmpBatchE; + bytes32 internal tmpDigestA; + bytes32 internal tmpDigestB; + bytes32 internal tmpDigestC; + bytes32 internal tmpDigestD; + bytes32 internal tmpDigestE; + + uint256 internal lastPotObserved; + + constructor() { + token = new TestToken("TestToken", "TT", 1_000_000_000_000_000_000_000_000); // 1e24 + stamp = new PostageStamp(address(token), 2); + + for (uint256 i = 0; i < ACTOR_COUNT; i++) { + actors[i] = new EchidnaPostageActor(token, stamp); + token.transfer(address(actors[i]), 1_000_000_000_000_000_000_000_00); // 1e23 / 10 + } + + oracleActor = new EchidnaPostageActor(token, stamp); + redistributorActor = new EchidnaPostageActor(token, stamp); + pauserActor = new EchidnaPostageActor(token, stamp); + + stamp.grantRole(stamp.PRICE_ORACLE_ROLE(), address(oracleActor)); + stamp.grantRole(stamp.REDISTRIBUTOR_ROLE(), address(redistributorActor)); + stamp.grantRole(stamp.PAUSER_ROLE(), address(pauserActor)); + + lastPotObserved = stamp.pot(); + } + + // ----------------------------- + // Actions + // ----------------------------- + + function act_fundActor(uint8 actorId, uint256 amount) external { + _clearPending(); + uint256 bal = token.balanceOf(address(this)); + if (bal == 0) return; + uint256 x = amount % (bal + 1); + if (x == 0) return; + token.transfer(address(_actor(actorId)), x); + } + + function act_createBatch( + uint8 actorId, + uint256 initialPerChunk, + uint8 depthRaw, + bytes32 nonce, + bool immutableFlag + ) external { + _clearPending(); + // Normalize expiry so createBatch's internal expireLimited() doesn't unexpectedly mutate other batches. + stamp.expireLimited(type(uint256).max); + tmpNonce = nonce; + tmpImmutable = immutableFlag; + _createBatchInternal(actorId, initialPerChunk, depthRaw); + _observePot(false); + } + + function act_topUp(uint8 actorId, uint8 batchIndex, uint256 topupPerChunk) external { + _clearPending(); + EchidnaPostageActor a = _actor(actorId); + + if (stamp.paused()) { + bool okPaused = a.topUp(_batch(batchIndex), 1); + if (okPaused) pausedMutationSucceeded = true; + return; + } + + bytes32 batchId = _batch(batchIndex); + if (batchId == bytes32(0)) return; + _armNonInterference(batchIndex, batchId); + + // Only the creator can topUp (msg.sender irrelevant); topUp isn't owner gated but will revert if batch doesn't exist/expired. + uint8 depth = stamp.batchDepth(batchId); + if (depth == 0) return; + + uint256 maxPerChunk = token.balanceOf(address(a)) / (1 << depth); + if (maxPerChunk == 0) return; + uint256 perChunk = topupPerChunk % (maxPerChunk + 1); + if (perChunk == 0) return; + + uint256 tokenBefore = token.balanceOf(address(stamp)); + uint256 normBefore = stamp.batchNormalisedBalance(batchId); + uint256 totalAmount = perChunk * (1 << depth); + + bool ok = a.topUp(batchId, perChunk); + if (!ok) return; + _checkNonInterference(); + + pendingTopUp = true; + pendingTopUpBatchId = batchId; + pendingTopUpTokenBefore = tokenBefore; + pendingTopUpNormalisedBefore = normBefore; + pendingTopUpTotalAmount = totalAmount; + pendingTopUpPerChunk = perChunk; + } + + function act_increaseDepth(uint8 actorId, uint8 batchIndex, uint8 newDepthRaw) external { + _clearPending(); + EchidnaPostageActor a = _actor(actorId); + + if (stamp.paused()) { + bool okPaused = a.increaseDepth(_batch(batchIndex), 3); + if (okPaused) pausedMutationSucceeded = true; + _observePot(false); + return; + } + + bytes32 batchId = _batch(batchIndex); + if (batchId == bytes32(0)) { + _observePot(false); + return; + } + + // increaseDepth is owner-gated; we only attempt if the batch owner matches this actor. + if (stamp.batchOwner(batchId) != address(a)) { + _observePot(false); + return; + } + + // Normalize state to avoid this call also expiring unrelated batches (it calls expireLimited internally). + stamp.expireLimited(type(uint256).max); + + uint8 oldDepth = stamp.batchDepth(batchId); + if (oldDepth == 0) { + _observePot(false); + return; + } + + uint8 minBucket = stamp.minimumBucketDepth(); + uint8 newDepth = uint8(minBucket + 1 + (newDepthRaw % 12)); + if (newDepth <= oldDepth) { + _observePot(false); + return; + } + + uint256 validBefore = stamp.validChunkCount(); + uint256 tokenBefore = token.balanceOf(address(stamp)); + uint8 bucketDepthBefore = stamp.batchBucketDepth(batchId); + + uint256 ctopBefore = stamp.currentTotalOutPayment(); + uint256 remainingBefore = stamp.remainingBalance(batchId); + uint8 depthChange = newDepth - oldDepth; + uint256 expectedNormalisedAfter = ctopBefore + (remainingBefore / (1 << depthChange)); + + _armNonInterference(batchIndex, batchId); + + bool ok = a.increaseDepth(batchId, newDepth); + if (!ok) { + _observePot(false); + return; + } + _checkNonInterference(); + + pendingIncreaseDepth = true; + pendingIncBatchId = batchId; + pendingIncOldDepth = oldDepth; + pendingIncNewDepth = newDepth; + pendingIncValidChunkBefore = validBefore; + pendingIncTokenBefore = tokenBefore; + pendingIncBucketDepth = bucketDepthBefore; + pendingIncExpectedNormalised = expectedNormalisedAfter; + _observePot(false); + } + + function act_oracle_setPrice(uint256 price) external { + _clearPending(); + bool ok = oracleActor.trySetPrice(price); + if (!ok) { + _observePot(false); + return; + } + + pendingSetPrice = true; + pendingSetPriceLastUpdatedExpected = uint64(block.number); + pendingSetPriceLastPriceExpected = uint64(price); + // Capture the exact base total payout immediately after setting the price. + // At this point `lastUpdatedBlock == block.number`, so `currentTotalOutPayment()` equals `totalOutPayment`. + pendingSetPriceTotalOutPaymentBefore = stamp.currentTotalOutPayment(); + _observePot(false); + } + + function act_expireAll() external { + _clearPending(); + stamp.expireLimited(type(uint256).max); + pendingExpireAll = true; + _observePot(false); + } + + function act_redistributor_withdraw(uint8 beneficiaryActorId) external { + _clearPending(); + address beneficiary = address(_actor(beneficiaryActorId)); + if (beneficiary == address(0)) beneficiary = address(0xBEEF); + + uint256 amount = stamp.totalPot(); + uint256 balBefore = token.balanceOf(beneficiary); + uint256 stampBalBefore = token.balanceOf(address(stamp)); + + bool ok = redistributorActor.tryWithdraw(beneficiary); + if (!ok) { + _observePot(false); + return; + } + + pendingWithdraw = true; + pendingWithdrawBeneficiary = beneficiary; + pendingWithdrawBeneficiaryBalBefore = balBefore; + pendingWithdrawStampBalBefore = stampBalBefore; + pendingWithdrawExpectedAmount = amount; + _observePot(true); + } + + function act_pauser_pause() external { + _clearPending(); + pauserActor.tryPause(); + } + + function act_pauser_unpause() external { + _clearPending(); + pauserActor.tryUnpause(); + } + + function act_rando_trySetPrice(uint8 actorId, uint256 price) external { + _clearPending(); + bool ok = _actor(actorId).trySetPrice(price); + if (ok) unauthorizedPriceSetSucceeded = true; + } + + function act_rando_tryWithdraw(uint8 actorId, address beneficiary) external { + _clearPending(); + if (beneficiary == address(0)) beneficiary = address(0xBEEF); + bool ok = _actor(actorId).tryWithdraw(beneficiary); + if (ok) unauthorizedWithdrawSucceeded = true; + } + + function act_rando_tryPause(uint8 actorId) external { + _clearPending(); + bool ok = _actor(actorId).tryPause(); + if (ok) unauthorizedPauseSucceeded = true; + } + + function act_rando_tryUnpause(uint8 actorId) external { + _clearPending(); + bool ok = _actor(actorId).tryUnpause(); + if (ok) unauthorizedPauseSucceeded = true; + } + + // ----------------------------- + // Properties + // ----------------------------- + + function echidna_never_performed_forbidden_calls() external view returns (bool) { + return + !unauthorizedPriceSetSucceeded && + !unauthorizedWithdrawSucceeded && + !unauthorizedPauseSucceeded && + !pausedMutationSucceeded && + !nonInterferenceViolated && + !potDecreasedUnexpectedly; + } + + function echidna_lastExpiryBalance_never_exceeds_currentTotalOutPayment() external view returns (bool) { + return stamp.lastExpiryBalance() <= stamp.currentTotalOutPayment(); + } + + function echidna_createBatch_postconditions_hold() external view returns (bool) { + if (!pendingCreate) return true; + + if (token.balanceOf(address(stamp)) != pendingStampTokenBalanceBefore + pendingCreateTotalAmount) return false; + + if (stamp.batchOwner(pendingBatchId) == address(0)) return false; + if (stamp.batchDepth(pendingBatchId) != pendingCreateDepth) return false; + if (stamp.batchBucketDepth(pendingBatchId) != pendingCreateBucketDepth) return false; + if (stamp.batchImmutableFlag(pendingBatchId) != pendingCreateImmutable) return false; + + // Normalised balance is computed as currentTotalOutPayment + perChunk at creation time. + if (stamp.batchNormalisedBalance(pendingBatchId) != pendingCreateNormalisedExpected) return false; + return true; + } + + function echidna_topUp_postconditions_hold() external view returns (bool) { + if (!pendingTopUp) return true; + if (token.balanceOf(address(stamp)) != pendingTopUpTokenBefore + pendingTopUpTotalAmount) return false; + return stamp.batchNormalisedBalance(pendingTopUpBatchId) == pendingTopUpNormalisedBefore + pendingTopUpPerChunk; + } + + function echidna_increaseDepth_updates_validChunkCount_and_keeps_balance() external view returns (bool) { + if (!pendingIncreaseDepth) return true; + if (token.balanceOf(address(stamp)) != pendingIncTokenBefore) return false; + + uint256 expectedDelta = (1 << pendingIncNewDepth) - (1 << pendingIncOldDepth); + if (stamp.validChunkCount() != pendingIncValidChunkBefore + expectedDelta) return false; + + if (stamp.batchDepth(pendingIncBatchId) != pendingIncNewDepth) return false; + if (stamp.batchBucketDepth(pendingIncBatchId) != pendingIncBucketDepth) return false; + if (stamp.batchNormalisedBalance(pendingIncBatchId) != pendingIncExpectedNormalised) return false; + return true; + } + + function echidna_expireAll_clears_expired_batches() external view returns (bool) { + if (!pendingExpireAll) return true; + return !stamp.expiredBatchesExist(); + } + + function echidna_setPrice_postconditions_hold() external view returns (bool) { + if (!pendingSetPrice) return true; + if (stamp.lastUpdatedBlock() != pendingSetPriceLastUpdatedExpected) return false; + if (stamp.lastPrice() != pendingSetPriceLastPriceExpected) return false; + uint256 blocksSince = block.number - uint256(pendingSetPriceLastUpdatedExpected); + uint256 expected = pendingSetPriceTotalOutPaymentBefore + + uint256(pendingSetPriceLastPriceExpected) * + blocksSince; + return stamp.currentTotalOutPayment() == expected; + } + + function echidna_withdraw_postconditions_hold() external view returns (bool) { + if (!pendingWithdraw) return true; + if (stamp.pot() != 0) return false; + if ( + token.balanceOf(pendingWithdrawBeneficiary) != + pendingWithdrawBeneficiaryBalBefore + pendingWithdrawExpectedAmount + ) return false; + return token.balanceOf(address(stamp)) == pendingWithdrawStampBalBefore - pendingWithdrawExpectedAmount; + } + + // ----------------------------- + // Helpers + // ----------------------------- + + function _actor(uint8 actorId) internal view returns (EchidnaPostageActor) { + return actors[uint256(actorId) % ACTOR_COUNT]; + } + + function _batch(uint8 batchIndex) internal view returns (bytes32) { + if (trackedCount == 0) return bytes32(0); + return tracked[uint256(batchIndex) % MAX_TRACKED]; + } + + function _clearPending() internal { + pendingCreate = false; + pendingBatchId = bytes32(0); + pendingCreateTotalAmount = 0; + pendingStampTokenBalanceBefore = 0; + pendingCreateNormalisedExpected = 0; + pendingCreateDepth = 0; + pendingCreateBucketDepth = 0; + pendingCreateImmutable = false; + + pendingTopUp = false; + pendingTopUpBatchId = bytes32(0); + pendingTopUpTokenBefore = 0; + pendingTopUpNormalisedBefore = 0; + pendingTopUpTotalAmount = 0; + pendingTopUpPerChunk = 0; + + pendingIncreaseDepth = false; + pendingIncBatchId = bytes32(0); + pendingIncOldDepth = 0; + pendingIncNewDepth = 0; + pendingIncValidChunkBefore = 0; + pendingIncTokenBefore = 0; + pendingIncBucketDepth = 0; + pendingIncExpectedNormalised = 0; + + pendingExpireAll = false; + pendingSetPrice = false; + pendingSetPriceTotalOutPaymentBefore = 0; + pendingSetPriceLastUpdatedExpected = 0; + pendingSetPriceLastPriceExpected = 0; + + pendingWithdraw = false; + pendingWithdrawBeneficiary = address(0); + pendingWithdrawBeneficiaryBalBefore = 0; + pendingWithdrawExpectedAmount = 0; + pendingWithdrawStampBalBefore = 0; + } + + function _batchDigest(bytes32 batchId) internal view returns (bytes32) { + address owner = stamp.batchOwner(batchId); + if (owner == address(0)) return bytes32(0); + return + keccak256( + abi.encodePacked( + owner, + stamp.batchDepth(batchId), + stamp.batchBucketDepth(batchId), + stamp.batchImmutableFlag(batchId), + stamp.batchNormalisedBalance(batchId), + stamp.batchLastUpdatedBlockNumber(batchId) + ) + ); + } + + function _armNonInterference(uint8 batchIndex, bytes32 target) internal { + tmpBatchA = _batch(uint8(batchIndex + 1)); + tmpBatchB = _batch(uint8(batchIndex + 2)); + tmpBatchC = _batch(uint8(batchIndex + 3)); + tmpBatchD = _batch(uint8(batchIndex + 4)); + tmpBatchE = _batch(uint8(batchIndex + 5)); + if (tmpBatchA == target) tmpBatchA = bytes32(0); + if (tmpBatchB == target) tmpBatchB = bytes32(0); + if (tmpBatchC == target) tmpBatchC = bytes32(0); + if (tmpBatchD == target) tmpBatchD = bytes32(0); + if (tmpBatchE == target) tmpBatchE = bytes32(0); + tmpDigestA = tmpBatchA == bytes32(0) ? bytes32(0) : _batchDigest(tmpBatchA); + tmpDigestB = tmpBatchB == bytes32(0) ? bytes32(0) : _batchDigest(tmpBatchB); + tmpDigestC = tmpBatchC == bytes32(0) ? bytes32(0) : _batchDigest(tmpBatchC); + tmpDigestD = tmpBatchD == bytes32(0) ? bytes32(0) : _batchDigest(tmpBatchD); + tmpDigestE = tmpBatchE == bytes32(0) ? bytes32(0) : _batchDigest(tmpBatchE); + } + + function _checkNonInterference() internal { + if (tmpBatchA != bytes32(0) && _batchDigest(tmpBatchA) != tmpDigestA) nonInterferenceViolated = true; + if (tmpBatchB != bytes32(0) && _batchDigest(tmpBatchB) != tmpDigestB) nonInterferenceViolated = true; + if (tmpBatchC != bytes32(0) && _batchDigest(tmpBatchC) != tmpDigestC) nonInterferenceViolated = true; + if (tmpBatchD != bytes32(0) && _batchDigest(tmpBatchD) != tmpDigestD) nonInterferenceViolated = true; + if (tmpBatchE != bytes32(0) && _batchDigest(tmpBatchE) != tmpDigestE) nonInterferenceViolated = true; + } + + function _observePot(bool withdrew) internal { + uint256 prev = lastPotObserved; + uint256 nowPot = stamp.pot(); + if (nowPot < prev) { + if (!(withdrew && nowPot == 0 && prev > 0)) potDecreasedUnexpectedly = true; + } + lastPotObserved = nowPot; + } + + function _createBatchInternal(uint8 actorId, uint256 initialPerChunk, uint8 depthRaw) internal { + if (stamp.paused()) return; + + EchidnaPostageActor a = _actor(actorId); + + // Bound depth and bucketDepth to safe values. + uint8 depth = uint8(2 + (depthRaw % 12)); // [2..13] + uint8 minBucket = stamp.minimumBucketDepth(); + if (minBucket >= depth) return; + uint8 bucketDepth = uint8(minBucket + (uint8(uint256(tmpNonce) % uint256(depth - minBucket)))); + if (bucketDepth >= depth) return; + + // Bound initialPerChunk and ensure actor can pay. + uint256 available = token.balanceOf(address(a)); + uint256 denom = (1 << depth); + uint256 maxPerChunk = available / denom; + if (maxPerChunk == 0) return; + uint256 perChunk = (initialPerChunk % maxPerChunk) + 1; // non-zero + + // Store pre-call snapshots directly into pending fields (to reduce stack pressure). + pendingStampTokenBalanceBefore = token.balanceOf(address(stamp)); + pendingCreateTotalAmount = perChunk * denom; + pendingCreateNormalisedExpected = stamp.currentTotalOutPayment() + perChunk; + pendingCreateDepth = depth; + pendingCreateBucketDepth = bucketDepth; + pendingCreateImmutable = tmpImmutable; + + bool ok; + bytes32 batchId; + if (tmpImmutable) { + (ok, batchId) = a.createBatchImmutable(perChunk, depth, bucketDepth, tmpNonce); + } else { + (ok, batchId) = a.createBatchMutable(perChunk, depth, bucketDepth, tmpNonce); + } + if (!ok || batchId == bytes32(0)) return; + + tracked[trackedCount % MAX_TRACKED] = batchId; + trackedCount++; + + pendingBatchId = batchId; + pendingCreate = true; + } +} diff --git a/src/echidna/EchidnaPriceOracleHarness.sol b/src/echidna/EchidnaPriceOracleHarness.sol new file mode 100644 index 00000000..ff28623b --- /dev/null +++ b/src/echidna/EchidnaPriceOracleHarness.sol @@ -0,0 +1,322 @@ +// SPDX-License-Identifier: BSD-3-Clause +pragma solidity ^0.8.19; + +import "../PriceOracle.sol"; + +contract EchidnaPostageStampMock { + uint256 public lastPrice; + uint256 public setPriceCalls; + bool public shouldRevert; + + function setShouldRevert(bool v) external { + shouldRevert = v; + } + + function setPrice(uint256 price) external { + if (shouldRevert) revert("mock revert"); + lastPrice = price; + setPriceCalls += 1; + } +} + +contract EchidnaOracleActor { + PriceOracle internal immutable oracle; + + constructor(PriceOracle oracle_) { + oracle = oracle_; + } + + function callSetPrice(uint32 p) external returns (bool ok, bool returned) { + bytes memory data; + (ok, data) = address(oracle).call(abi.encodeWithSelector(oracle.setPrice.selector, p)); + returned = ok && data.length >= 32 ? abi.decode(data, (bool)) : false; + } + + function callAdjustPrice(uint16 r) external returns (bool ok, bool returned) { + bytes memory data; + (ok, data) = address(oracle).call(abi.encodeWithSelector(oracle.adjustPrice.selector, r)); + returned = ok && data.length >= 32 ? abi.decode(data, (bool)) : false; + } + + function callPause() external returns (bool ok) { + (ok, ) = address(oracle).call(abi.encodeWithSelector(oracle.pause.selector)); + } + + function callUnpause() external returns (bool ok) { + (ok, ) = address(oracle).call(abi.encodeWithSelector(oracle.unPause.selector)); + } +} + +/// @notice Echidna harness for comprehensive fuzzing of PriceOracle. +contract EchidnaPriceOracleHarness { + PriceOracle internal immutable oracle; + EchidnaPostageStampMock internal immutable stamp; + + EchidnaOracleActor internal immutable updater; + EchidnaOracleActor internal immutable rando; + + // “Must never happen” flags. + bool internal unauthorizedAdminCallSucceeded; + bool internal unauthorizedAdjustSucceeded; + bool internal pausedAdjustChangedState; + + // Pending post-conditions (cleared on each action). + bool internal pendingSetPrice; + uint64 internal pendingExpectedUpScaled; + uint256 internal pendingStampCallsBefore; + bool internal pendingStampShouldCall; + + bool internal pendingAdjust; + bool internal pendingAdjustPaused; + uint64 internal pendingPriceBefore; + uint64 internal pendingLastAdjustedBefore; + uint64 internal pendingExpectedLastAdjustedAfter; + uint64 internal pendingExpectedUpScaledAfter; + uint256 internal pendingAdjustStampCallsBefore; + bool internal pendingAdjustStampShouldCall; + bool internal adjustWouldOverflowButSucceeded; + + constructor() { + stamp = new EchidnaPostageStampMock(); + oracle = new PriceOracle(address(stamp)); + + updater = new EchidnaOracleActor(oracle); + rando = new EchidnaOracleActor(oracle); + + oracle.grantRole(oracle.PRICE_UPDATER_ROLE(), address(updater)); + } + + // ----------------------------- + // Actions + // ----------------------------- + + function act_setStampRevertMode(bool v) external { + _clearPending(); + stamp.setShouldRevert(v); + } + + function act_admin_setPrice(uint32 p) external { + _clearPending(); + + uint256 callsBefore = stamp.setPriceCalls(); + (bool ok, bool returned) = _callSetPriceAsAdmin(p); + + // Do not arm postconditions unless the call fully succeeded; otherwise + // `pendingSetPrice` would not match what the contract actually did (e.g. stamp callback failed). + if (!ok || !returned) return; + + pendingStampCallsBefore = callsBefore; + pendingExpectedUpScaled = oracle.currentPriceUpScaled(); + pendingStampShouldCall = !stamp.shouldRevert(); + pendingSetPrice = true; + } + + function act_admin_pause() external { + _clearPending(); + oracle.pause(); + } + + function act_admin_unpause() external { + _clearPending(); + oracle.unPause(); + } + + function act_updater_adjustPrice(uint16 redundancy) external { + _clearPending(); + + pendingAdjustPaused = oracle.isPaused(); + pendingPriceBefore = oracle.currentPriceUpScaled(); + pendingLastAdjustedBefore = oracle.lastAdjustedRound(); + pendingAdjustStampCallsBefore = stamp.setPriceCalls(); + + (bool ok, bool returned) = updater.callAdjustPrice(redundancy); + + if (pendingAdjustPaused) { + if ( + oracle.currentPriceUpScaled() != pendingPriceBefore || + oracle.lastAdjustedRound() != pendingLastAdjustedBefore || + stamp.setPriceCalls() != pendingAdjustStampCallsBefore + ) { + pausedAdjustChangedState = true; + } + return; + } + + // Not paused. Determine whether the call is expected to revert on basic guards. + uint64 currentRound = oracle.currentRound(); + bool wouldRevertEarly = (redundancy == 0) || (currentRound <= pendingLastAdjustedBefore); + + if (wouldRevertEarly) { + if (ok) adjustWouldOverflowButSucceeded = true; + if ( + oracle.currentPriceUpScaled() != pendingPriceBefore || + oracle.lastAdjustedRound() != pendingLastAdjustedBefore || + stamp.setPriceCalls() != pendingAdjustStampCallsBefore + ) { + pausedAdjustChangedState = true; + } + return; + } + + // Compute expected post-state. If arithmetic would overflow in the contract, we expect a revert. + (bool canCompute, uint64 expected) = _tryExpectedAdjustedPrice( + pendingPriceBefore, + redundancy, + currentRound, + pendingLastAdjustedBefore + ); + + if (!canCompute) { + if (ok && returned) adjustWouldOverflowButSucceeded = true; + return; + } + + if (!ok) { + adjustWouldOverflowButSucceeded = true; + return; + } + + pendingExpectedLastAdjustedAfter = currentRound; + pendingExpectedUpScaledAfter = expected; + pendingAdjustStampShouldCall = !stamp.shouldRevert(); + pendingAdjust = true; + } + + function act_rando_tryAdjustPrice(uint16 redundancy) external { + _clearPending(); + (bool ok, bool returned) = rando.callAdjustPrice(redundancy); + // When not paused, adjustPrice is role-gated and should not succeed for a rando. + if (!oracle.isPaused() && ok && returned) unauthorizedAdjustSucceeded = true; + } + + function act_rando_trySetPrice(uint32 p) external { + _clearPending(); + (bool ok, bool returned) = rando.callSetPrice(p); + if (ok && returned) unauthorizedAdminCallSucceeded = true; + } + + function act_rando_tryPause() external { + _clearPending(); + bool ok = rando.callPause(); + if (ok) unauthorizedAdminCallSucceeded = true; + } + + function act_rando_tryUnpause() external { + _clearPending(); + bool ok = rando.callUnpause(); + if (ok) unauthorizedAdminCallSucceeded = true; + } + + // ----------------------------- + // Properties + // ----------------------------- + + function echidna_never_performed_forbidden_calls() external view returns (bool) { + return + !unauthorizedAdminCallSucceeded && + !unauthorizedAdjustSucceeded && + !pausedAdjustChangedState && + !adjustWouldOverflowButSucceeded; + } + + function echidna_price_never_below_minimum() external view returns (bool) { + return oracle.currentPriceUpScaled() >= oracle.minimumPriceUpscaled(); + } + + function echidna_lastAdjustedRound_not_in_future() external view returns (bool) { + return oracle.lastAdjustedRound() <= oracle.currentRound(); + } + + function echidna_setPrice_updates_expected_state_and_calls_stamp() external view returns (bool) { + if (!pendingSetPrice) return true; + if (oracle.currentPriceUpScaled() != pendingExpectedUpScaled) return false; + if (oracle.currentPrice() != uint32(pendingExpectedUpScaled >> 10)) return false; + + uint256 callsAfter = stamp.setPriceCalls(); + if (pendingStampShouldCall) { + if (callsAfter != pendingStampCallsBefore + 1) return false; + if (stamp.lastPrice() != uint256(oracle.currentPrice())) return false; + } else { + if (callsAfter != pendingStampCallsBefore) return false; + } + return true; + } + + function echidna_adjustPrice_postconditions_hold_when_applicable() external view returns (bool) { + if (!pendingAdjust) return true; + + if (oracle.lastAdjustedRound() != pendingExpectedLastAdjustedAfter) return false; + if (oracle.currentPriceUpScaled() != pendingExpectedUpScaledAfter) return false; + if (oracle.currentPrice() != uint32(pendingExpectedUpScaledAfter >> 10)) return false; + + uint256 callsAfter = stamp.setPriceCalls(); + if (pendingAdjustStampShouldCall) { + if (callsAfter != pendingAdjustStampCallsBefore + 1) return false; + if (stamp.lastPrice() != uint256(oracle.currentPrice())) return false; + } else { + if (callsAfter != pendingAdjustStampCallsBefore) return false; + } + return true; + } + + // ----------------------------- + // Helpers + // ----------------------------- + + function _callSetPriceAsAdmin(uint32 p) internal returns (bool ok, bool returned) { + // This harness is the admin because it deployed PriceOracle. + bytes memory data; + (ok, data) = address(oracle).call(abi.encodeWithSelector(oracle.setPrice.selector, p)); + returned = ok && data.length >= 32 ? abi.decode(data, (bool)) : false; + } + + function _tryExpectedAdjustedPrice( + uint64 priceUpScaledBefore, + uint16 redundancy, + uint64 currentRound, + uint64 lastAdjusted + ) internal view returns (bool ok, uint64 expected) { + uint16 used = redundancy; + uint16 maxRed = uint16(4 + 4); + if (used > maxRed) used = maxRed; + + uint256 price = uint256(priceUpScaledBefore); + uint256 base = uint256(oracle.priceBase()); + + uint256 rate = uint256(oracle.changeRate(uint256(used))); + // In the real contract, this multiplication happens in uint64 space: + // uint32 * uint64 -> uint64, and would revert on overflow. + if (rate * price > type(uint64).max) return (false, 0); + price = (rate * price) / base; + + uint64 skipped = currentRound - lastAdjusted - 1; + if (skipped > 0) { + uint256 rateMax = uint256(oracle.changeRate(0)); + for (uint64 i = 0; i < skipped; i++) { + if (rateMax * price > type(uint64).max) return (false, 0); + price = (rateMax * price) / base; + } + } + + uint256 minUp = uint256(oracle.minimumPriceUpscaled()); + if (price < minUp) price = minUp; + if (price > type(uint64).max) return (false, 0); + return (true, uint64(price)); + } + + function _clearPending() internal { + pendingSetPrice = false; + pendingAdjust = false; + pendingExpectedUpScaled = 0; + pendingStampCallsBefore = 0; + pendingStampShouldCall = false; + pendingAdjustPaused = false; + pendingPriceBefore = 0; + pendingLastAdjustedBefore = 0; + pendingExpectedLastAdjustedAfter = 0; + pendingExpectedUpScaledAfter = 0; + pendingAdjustStampCallsBefore = 0; + pendingAdjustStampShouldCall = false; + adjustWouldOverflowButSucceeded = false; + } +} diff --git a/src/echidna/EchidnaRedistributionClaimHarness.sol b/src/echidna/EchidnaRedistributionClaimHarness.sol new file mode 100644 index 00000000..593abdb4 --- /dev/null +++ b/src/echidna/EchidnaRedistributionClaimHarness.sol @@ -0,0 +1,369 @@ +// SPDX-License-Identifier: BSD-3-Clause +pragma solidity ^0.8.19; + +import "../Redistribution.sol"; +import "../TestToken.sol"; +import "../interface/IPostageStamp.sol"; +import "./EchidnaMocks.sol"; + +contract EchidnaPostageStampPotMock is IPostageStamp { + TestToken internal immutable token; + + uint256 public pot; + address public lastBeneficiary; + uint256 public lastAmount; + uint256 public validChunkCountValue; + bool public shouldRevertWithdraw; + + constructor(TestToken t) { + token = t; + } + + function seedPot(uint256 amount) external { + token.mint(address(this), amount); + pot += amount; + } + + function setShouldRevertWithdraw(bool v) external { + shouldRevertWithdraw = v; + } + + function setValidChunkCount(uint256 v) external { + validChunkCountValue = v; + } + + function withdraw(address beneficiary) external { + if (shouldRevertWithdraw) revert("mock withdraw revert"); + uint256 bal = token.balanceOf(address(this)); + uint256 amt = pot < bal ? pot : bal; + lastBeneficiary = beneficiary; + lastAmount = amt; + pot = 0; + if (amt > 0) { + token.transfer(beneficiary, amt); + } + } + + // Unused in this claim-stub harness but required by the interface. + function setPrice(uint256) external {} + function validChunkCount() external view returns (uint256) { + return validChunkCountValue; + } + function batchOwner(bytes32) external pure returns (address) { + return address(0); + } + function batchDepth(bytes32) external pure returns (uint8) { + return 0; + } + function batchBucketDepth(bytes32) external pure returns (uint8) { + return 0; + } + function remainingBalance(bytes32) external pure returns (uint256) { + return 0; + } + function minimumInitialBalancePerChunk() external pure returns (uint256) { + return 0; + } + function batches( + bytes32 + ) + external + pure + returns ( + address owner, + uint8 depth, + uint8 bucketDepth, + bool immutableFlag, + uint256 normalisedBalance, + uint256 lastUpdatedBlockNumber + ) + { + return (address(0), 0, 0, false, 0, 0); + } +} + +contract RedistributionClaimStub is Redistribution { + constructor( + address staking, + address postageContract, + address oracleContract + ) Redistribution(staking, postageContract, oracleContract) {} + + /// @notice Fuzz-only claim: run real winnerSelection(), then withdraw pot to winner. + /// @dev Bypasses inclusion/SOC/stamp proof verification entirely. + function claimStub() external whenNotPaused { + winnerSelection(); + Reveal memory winnerSelected = winner; + + (bool success, ) = address(PostageContract).call( + abi.encodeWithSignature("withdraw(address)", winnerSelected.owner) + ); + if (!success) { + emit WithdrawFailed(winnerSelected.owner); + } + + emit WinnerSelected(winnerSelected); + emit ChunkCount(PostageContract.validChunkCount()); + } +} + +contract EchidnaRedistributionClaimActor { + RedistributionClaimStub internal immutable redist; + + constructor(RedistributionClaimStub r) { + redist = r; + } + + function callCommit(bytes32 obfuscatedHash, uint64 roundNumber) external returns (bool ok) { + (ok, ) = address(redist).call(abi.encodeWithSelector(redist.commit.selector, obfuscatedHash, roundNumber)); + } + + function callReveal(uint8 depth, bytes32 hash, bytes32 nonce) external returns (bool ok) { + (ok, ) = address(redist).call(abi.encodeWithSelector(redist.reveal.selector, depth, hash, nonce)); + } + + function callClaimStub() external returns (bool ok) { + (ok, ) = address(redist).call(abi.encodeWithSelector(redist.claimStub.selector)); + } +} + +/// @notice Harness to fuzz commit→reveal→claim-withdraw end-to-end (without proof verification). +contract EchidnaRedistributionClaimHarness { + uint256 internal constant ACTOR_COUNT = 3; + uint256 internal constant ROUND_LENGTH = 152; + + TestToken internal immutable token; + EchidnaStakeRegistryMock internal immutable stakeMock; + EchidnaPostageStampPotMock internal immutable stampMock; + EchidnaPriceOracleMock internal immutable oracleMock; + RedistributionClaimStub internal immutable redist; + + EchidnaRedistributionClaimActor[3] internal actors; + + // Track a "happy-path" preimage so reveal/claim can actually succeed. + bool[3] internal trackedHasCommit; + bool[3] internal trackedHasReveal; + uint64[3] internal trackedRound; + bytes32[3] internal trackedObfuscated; + bytes32[3] internal trackedHash; + bytes32[3] internal trackedNonce; + uint8[3] internal trackedDepth; + + // Pending claim postconditions. + bool internal pendingClaim; + bool internal pendingWithdrawShouldFail; + uint64 internal pendingClaimRound; + uint256 internal pendingPotBefore; + uint256 internal pendingOracleCallsBefore; + uint256[3] internal pendingActorBalBefore; + + // Flags. + bool internal claimSucceededTwiceSameRound; + uint64 internal lastClaimRound; + + constructor() { + token = new TestToken("TestToken", "TT", 0); + stakeMock = new EchidnaStakeRegistryMock(); + stampMock = new EchidnaPostageStampPotMock(token); + oracleMock = new EchidnaPriceOracleMock(); + redist = new RedistributionClaimStub(address(stakeMock), address(stampMock), address(oracleMock)); + + for (uint256 i = 0; i < ACTOR_COUNT; i++) { + actors[i] = new EchidnaRedistributionClaimActor(redist); + // Seed eligible stake; lastUpdated=1 ensures it will become "2 rounds old" later. + stakeMock.setNode(address(actors[i]), bytes32(uint256(i + 1)), 0, 1e18, 1); + } + } + + function _clearClaimPending() internal { + pendingClaim = false; + } + + // ----------------------------- + // Actions + // ----------------------------- + + /// @dev No-op that lets Echidna advance block.number without side effects, + /// helping the fuzzer walk through round phases. + function act_tick() external {} + + function act_seedPot(uint256 amount) external { + _clearClaimPending(); + uint256 x = amount % 1e24; + if (x == 0) x = 1e18; + stampMock.seedPot(x); + } + + function act_setWithdrawRevertMode(bool v) external { + _clearClaimPending(); + stampMock.setShouldRevertWithdraw(v); + } + + function act_setActorNode( + uint8 actorId, + bytes32 overlay, + uint8 height, + uint256 effectiveStake, + uint256 lastUpdated + ) external { + _clearClaimPending(); + uint256 idx = uint256(actorId) % ACTOR_COUNT; + uint8 h = uint8(height % 16); + uint256 stake = effectiveStake == 0 ? 1e18 : (effectiveStake % 1e24) + 1; + uint256 u = lastUpdated == 0 ? 1 : lastUpdated; + stakeMock.setNode(address(actors[idx]), overlay, h, stake, u); + } + + function act_happyCommit(uint8 actorId, bytes32 hash, bytes32 nonce) external { + _clearClaimPending(); + if (!redist.currentPhaseCommit()) return; + if (block.number % ROUND_LENGTH == (ROUND_LENGTH / 4) - 1) return; + + uint256 idx = uint256(actorId) % ACTOR_COUNT; + EchidnaRedistributionClaimActor a = actors[idx]; + + // Make proximity always pass by setting depth == height (depthResponsibility=0). + bytes32 overlay = keccak256(abi.encodePacked("overlay", idx, redist.currentRoundAnchor())); + uint8 height = 0; + uint8 depth = 0; + + // Ensure staking is old enough. + stakeMock.setNode(address(a), overlay, height, 1e18, _backdateLastUpdated()); + + bytes32 obf = redist.wrapCommit(overlay, depth, hash, nonce); + bool ok = a.callCommit(obf, redist.currentRound()); + if (!ok) return; + + trackedHasCommit[idx] = true; + trackedHasReveal[idx] = false; + trackedRound[idx] = redist.currentRound(); + trackedObfuscated[idx] = obf; + trackedHash[idx] = hash; + trackedNonce[idx] = nonce; + trackedDepth[idx] = depth; + } + + function act_happyReveal(uint8 actorId) external { + _clearClaimPending(); + if (!redist.currentPhaseReveal()) return; + + uint256 idx = uint256(actorId) % ACTOR_COUNT; + if (!trackedHasCommit[idx] || trackedHasReveal[idx]) return; + if (redist.currentRound() != trackedRound[idx]) return; + if (redist.currentCommitRound() != trackedRound[idx]) return; + + bool ok = actors[idx].callReveal(trackedDepth[idx], trackedHash[idx], trackedNonce[idx]); + if (!ok) return; + trackedHasReveal[idx] = true; + } + + function act_claimStub(uint8 actorId) external { + _clearClaimPending(); + uint256 idx = uint256(actorId) % ACTOR_COUNT; + pendingClaimRound = redist.currentRound(); + pendingOracleCallsBefore = oracleMock.calls(); + pendingWithdrawShouldFail = stampMock.shouldRevertWithdraw(); + + // Snapshot pot + actor balances before claim. + pendingPotBefore = stampMock.pot(); + for (uint256 i = 0; i < ACTOR_COUNT; i++) { + pendingActorBalBefore[i] = token.balanceOf(address(actors[i])); + } + + bool ok = actors[idx].callClaimStub(); + if (!ok) return; + + if (lastClaimRound == pendingClaimRound) claimSucceededTwiceSameRound = true; + lastClaimRound = pendingClaimRound; + + pendingClaim = true; + } + + // ----------------------------- + // Properties + // ----------------------------- + + function echidna_claim_only_once_per_round() external view returns (bool) { + return !claimSucceededTwiceSameRound; + } + + function echidna_claim_withdraws_pot_to_winner_when_successful() external view returns (bool) { + if (!pendingClaim) return true; + if (pendingWithdrawShouldFail) return true; + if (redist.currentClaimRound() != pendingClaimRound) return true; + + // Pot must be zeroed by our mock withdraw on success. + if (stampMock.pot() != 0) return false; + + // Beneficiary must match the winner selected by the round logic. + (, address winnerOwner, , , , ) = redist.winner(); + if (stampMock.lastBeneficiary() != winnerOwner) return false; + + // The amount transferred must match the pot snapshot (our mock mints on seedPot). + if (stampMock.lastAmount() != pendingPotBefore) return false; + + // Exactly one actor's balance should increase by lastAmount, matching the beneficiary. + uint256 increased = 0; + for (uint256 i = 0; i < ACTOR_COUNT; i++) { + uint256 afterBal = token.balanceOf(address(actors[i])); + if (afterBal != pendingActorBalBefore[i]) { + if (afterBal != pendingActorBalBefore[i] + stampMock.lastAmount()) return false; + if (address(actors[i]) != stampMock.lastBeneficiary()) return false; + increased += 1; + } + } + if (pendingPotBefore == 0) return increased == 0; + return increased == 1; + } + + /// @notice H-1 scenario: when withdraw fails, claim still succeeds (round consumed) + /// but pot is preserved and no actor balances change. + function echidna_failed_withdraw_preserves_pot_and_consumes_round() external view returns (bool) { + if (!pendingClaim) return true; + if (!pendingWithdrawShouldFail) return true; + if (redist.currentClaimRound() != pendingClaimRound) return true; + + // Round must still be marked as claimed even though withdraw failed. + // (This is the H-1 behavior: currentClaimRound is set inside winnerSelection() + // before withdraw runs, and the .call() swallows the revert.) + + // Pot must be unchanged — withdraw reverted so no transfer happened. + if (stampMock.pot() != pendingPotBefore) return false; + + // No actor balances should have changed. + for (uint256 i = 0; i < ACTOR_COUNT; i++) { + if (token.balanceOf(address(actors[i])) != pendingActorBalBefore[i]) return false; + } + return true; + } + + function echidna_claim_triggers_oracle_adjustPrice() external view returns (bool) { + if (!pendingClaim) return true; + if (oracleMock.calls() <= pendingOracleCallsBefore) return false; + return true; + } + + function echidna_nonrevealers_frozen_after_claim_selection() external view returns (bool) { + if (!pendingClaim) return true; + if (redist.currentClaimRound() != pendingClaimRound) return true; + + // Any actor that committed but did not reveal in that round should have been frozen at least once. + for (uint256 i = 0; i < ACTOR_COUNT; i++) { + if (!trackedHasCommit[i]) continue; + if (trackedRound[i] != pendingClaimRound) continue; + if (trackedHasReveal[i]) continue; + if (stakeMock.freezeCount(address(actors[i])) == 0) return false; + } + return true; + } + + // ----------------------------- + // Helpers + // ----------------------------- + + function _backdateLastUpdated() internal view returns (uint256) { + uint256 twoRounds = 2 * ROUND_LENGTH; + if (block.number > twoRounds + 1) return block.number - twoRounds - 1; + return 1; + } +} diff --git a/src/echidna/EchidnaRedistributionHarness.sol b/src/echidna/EchidnaRedistributionHarness.sol new file mode 100644 index 00000000..0631e744 --- /dev/null +++ b/src/echidna/EchidnaRedistributionHarness.sol @@ -0,0 +1,640 @@ +// SPDX-License-Identifier: BSD-3-Clause +pragma solidity ^0.8.19; + +import "../Redistribution.sol"; +import "../interface/IPostageStamp.sol"; +import "./RedistributionExposed.sol"; +import "./EchidnaMocks.sol"; + +contract EchidnaPostageStampMock is IPostageStamp { + uint256 public withdrawCalls; + address public lastBeneficiary; + uint256 public validChunkCountValue; + + function setValidChunkCount(uint256 v) external { + validChunkCountValue = v; + } + + function withdraw(address beneficiary) external { + withdrawCalls += 1; + lastBeneficiary = beneficiary; + } + + function setPrice(uint256) external {} + + function validChunkCount() external view returns (uint256) { + return validChunkCountValue; + } + + function batchOwner(bytes32) external pure returns (address) { + return address(0); + } + function batchDepth(bytes32) external pure returns (uint8) { + return 0; + } + function batchBucketDepth(bytes32) external pure returns (uint8) { + return 0; + } + function remainingBalance(bytes32) external pure returns (uint256) { + return 1; + } + function minimumInitialBalancePerChunk() external pure returns (uint256) { + return 1; + } + function batches( + bytes32 + ) + external + pure + returns ( + address owner, + uint8 depth, + uint8 bucketDepth, + bool immutableFlag, + uint256 normalisedBalance, + uint256 lastUpdatedBlockNumber + ) + { + return (address(0), 0, 0, false, 0, 0); + } +} + +contract EchidnaRedistributionActor { + RedistributionExposed internal immutable redist; + + constructor(RedistributionExposed r) { + redist = r; + } + + function callCommit(bytes32 obfuscatedHash, uint64 roundNumber) external returns (bool ok) { + (ok, ) = address(redist).call(abi.encodeWithSelector(redist.commit.selector, obfuscatedHash, roundNumber)); + } + + function callReveal(uint8 depth, bytes32 hash, bytes32 nonce) external returns (bool ok) { + (ok, ) = address(redist).call(abi.encodeWithSelector(redist.reveal.selector, depth, hash, nonce)); + } + + function callClaim() external returns (bool ok) { + // Create minimal calldata that avoids immediate out-of-bounds panics. + Redistribution.ChunkInclusionProof memory p; + p.proofSegments = new bytes32[](1); + p.proofSegments2 = new bytes32[](0); + p.proofSegments3 = new bytes32[](0); + p.socProof = new Redistribution.SOCProof[](0); + + (ok, ) = address(redist).call(abi.encodeWithSelector(redist.claim.selector, p, p, p)); + } + + function callWinnerSelection() external returns (bool ok) { + (ok, ) = address(redist).call(abi.encodeWithSelector(redist.exposedWinnerSelection.selector)); + } +} + +/// @notice Base Echidna harness for Redistribution. +/// @dev Focuses on commit/reveal state-machine consistency and winnerSelection postconditions. +contract EchidnaRedistributionHarness { + EchidnaStakeRegistryMock internal immutable stakeMock; + EchidnaPostageStampMock internal immutable stampMock; + EchidnaPriceOracleMock internal immutable oracleMock; + RedistributionExposed internal immutable redist; + + uint256 internal constant ACTOR_COUNT = 3; + /// @dev Cap scans; must match pending winnerSelection snapshot arrays (size 25). + uint256 internal constant MAX_COMMIT_REVEAL_SCAN = 25; + EchidnaRedistributionActor[3] internal actors; + + bool internal winnerSelectionSucceededTwiceSameRound; + + // Pending winnerSelection postconditions. + bool internal pendingWinnerSelection; + uint64 internal pendingWinnerSelectionRound; + uint8 internal pendingWinnerSelectionLen; + address[25] internal pendingWSOwners; + bool[25] internal pendingWSRevealed; + uint256[25] internal pendingWSFreezeCountBefore; + + uint64 internal lastWinnerSelectionRound; + + // Tracked "happy-path" state per actor (used to assert strong postconditions when we succeed). + bool[3] internal trackedHasCommit; + bool[3] internal trackedHasReveal; + uint64[3] internal trackedRound; + bytes32[3] internal trackedOverlay; + uint8[3] internal trackedHeight; + uint8[3] internal trackedDepth; + uint256[3] internal trackedStake; + bytes32[3] internal trackedReserveHash; + bytes32[3] internal trackedNonce; + bytes32[3] internal trackedObfuscated; + + struct CommitView { + bytes32 overlay; + address owner; + bool revealed; + uint8 height; + uint256 stake; + bytes32 obfuscatedHash; + uint256 revealIndex; + } + + struct RevealView { + bytes32 overlay; + address owner; + uint8 depth; + uint256 stake; + uint256 stakeDensity; + bytes32 hash; + } + + constructor() { + stakeMock = new EchidnaStakeRegistryMock(); + stampMock = new EchidnaPostageStampMock(); + oracleMock = new EchidnaPriceOracleMock(); + + redist = new RedistributionExposed(address(stakeMock), address(stampMock), address(oracleMock)); + + for (uint256 i = 0; i < ACTOR_COUNT; i++) { + actors[i] = new EchidnaRedistributionActor(redist); + // Seed a stake that will eventually satisfy commit constraints once block.number is large enough. + stakeMock.setNode(address(actors[i]), bytes32(uint256(i + 1)), 0, 1e18, 1); + } + } + + function _clearWinnerSelectionPending() internal { + pendingWinnerSelection = false; + pendingWinnerSelectionLen = 0; + } + + function _boundedCommitsLen() internal view returns (uint256) { + uint256 n = redist.currentCommitsLength(); + return n > MAX_COMMIT_REVEAL_SCAN ? MAX_COMMIT_REVEAL_SCAN : n; + } + + function _boundedRevealsLen() internal view returns (uint256) { + uint256 n = redist.currentRevealsLength(); + return n > MAX_COMMIT_REVEAL_SCAN ? MAX_COMMIT_REVEAL_SCAN : n; + } + + // ----------------------------- + // Actions + // ----------------------------- + + /// @dev No-op that lets Echidna advance block.number without side effects, + /// helping the fuzzer walk through round phases. + function act_tick() external {} + + function act_setActorStake( + uint8 actorId, + bytes32 overlay, + uint8 height, + uint256 effectiveStake, + uint256 lastUpdated + ) external { + _clearWinnerSelectionPending(); + EchidnaRedistributionActor a = actors[uint256(actorId) % ACTOR_COUNT]; + // Bound height so 2**depthResponsibility doesn't explode too hard during reveal. + uint8 h = uint8(height % 16); + // Avoid lastUpdated=0 unless we want NotStaked; keep at least 1. + uint256 u = lastUpdated == 0 ? 1 : lastUpdated; + uint256 stake = _boundStake(effectiveStake); + stakeMock.setNode(address(a), overlay, h, stake, u); + } + + function act_commit(uint8 actorId, bytes32 obfuscatedHash, int8 roundDelta) external { + _clearWinnerSelectionPending(); + EchidnaRedistributionActor a = actors[uint256(actorId) % ACTOR_COUNT]; + uint64 cr = redist.currentRound(); + uint64 rn = cr; + if (roundDelta < 0 && uint64(uint8(-roundDelta)) < cr) rn = cr - uint64(uint8(-roundDelta)); + if (roundDelta > 0) rn = cr + uint64(uint8(roundDelta)); + a.callCommit(obfuscatedHash, rn); + } + + function act_reveal(uint8 actorId, uint8 depth, bytes32 hash, bytes32 nonce) external { + _clearWinnerSelectionPending(); + EchidnaRedistributionActor a = actors[uint256(actorId) % ACTOR_COUNT]; + a.callReveal(uint8(depth % 32), hash, nonce); + } + + function act_claim(uint8 actorId) external { + _clearWinnerSelectionPending(); + EchidnaRedistributionActor a = actors[uint256(actorId) % ACTOR_COUNT]; + a.callClaim(); + } + + function act_admin_pause() external { + _clearWinnerSelectionPending(); + redist.pause(); + } + + function act_admin_unpause() external { + _clearWinnerSelectionPending(); + redist.unPause(); + } + + function act_admin_setSampleMaxValue(uint256 v) external { + _clearWinnerSelectionPending(); + redist.setSampleMaxValue(v); + } + + function act_admin_setFreezingParams(uint8 a, uint8 b, uint8 c) external { + _clearWinnerSelectionPending(); + redist.setFreezingParams(a, b, c); + } + + // ----------------------------- + // Advanced actions (aim for successful commit/reveal) + // ----------------------------- + + function act_happyCommit( + uint8 actorId, + uint8 height, + uint256 stakeAmount, + bytes32 reserveHash, + bytes32 nonce + ) external { + _clearWinnerSelectionPending(); + if (redist.paused()) return; + if (!redist.currentPhaseCommit()) return; + // Avoid the "phase last block" restriction in commit phase. + if (block.number % 152 == (152 / 4) - 1) return; + + uint256 idx = uint256(actorId) % ACTOR_COUNT; + EchidnaRedistributionActor a = actors[idx]; + + // Pick a unique overlay per actor that still has a high chance of being eligible. + // We set depthResponsibility = 0 (depth == height), which makes proximity always pass. + bytes32 anchor = redist.currentRoundAnchor(); + bytes32 overlay = keccak256(abi.encodePacked("overlay", idx, anchor)); + + uint8 h = uint8(height % 16); + uint8 d = h; + uint256 stake = _boundStake(stakeAmount); + uint256 lastUpdated = _backdateLastUpdated(); + + // Set node data so commit checks can pass. + stakeMock.setNode(address(a), overlay, h, stake, lastUpdated); + + // Avoid reverting on AlreadyCommitted for identical overlay. + if (_commitOverlayExists(overlay)) return; + + bytes32 obfuscated = redist.wrapCommit(overlay, d, reserveHash, nonce); + bool ok = a.callCommit(obfuscated, redist.currentRound()); + if (!ok) return; + + trackedHasCommit[idx] = true; + trackedHasReveal[idx] = false; + trackedRound[idx] = redist.currentRound(); + trackedOverlay[idx] = overlay; + trackedHeight[idx] = h; + trackedDepth[idx] = d; + trackedStake[idx] = stake; + trackedReserveHash[idx] = reserveHash; + trackedNonce[idx] = nonce; + trackedObfuscated[idx] = obfuscated; + } + + function act_happyReveal(uint8 actorId) external { + _clearWinnerSelectionPending(); + if (redist.paused()) return; + if (!redist.currentPhaseReveal()) return; + + uint256 idx = uint256(actorId) % ACTOR_COUNT; + if (!trackedHasCommit[idx] || trackedHasReveal[idx]) return; + + // Reveal must happen in the same round that received commits. + if (redist.currentRound() != trackedRound[idx]) return; + if (redist.currentCommitRound() != trackedRound[idx]) return; + + EchidnaRedistributionActor a = actors[idx]; + // Ensure the actor's overlay/height match the committed values. + stakeMock.setNode( + address(a), + trackedOverlay[idx], + trackedHeight[idx], + trackedStake[idx], + _backdateLastUpdated() + ); + + bool ok = a.callReveal(trackedDepth[idx], trackedReserveHash[idx], trackedNonce[idx]); + if (!ok) return; + + trackedHasReveal[idx] = true; + } + + function act_winnerSelection(uint8 actorId) external { + _clearWinnerSelectionPending(); + uint256 idx = uint256(actorId) % ACTOR_COUNT; + // Snapshot current commits (bounded) and freeze counts before selection. + pendingWinnerSelectionRound = redist.currentRound(); + + uint256 commitLim = _boundedCommitsLen(); + for (uint256 i = 0; i < commitLim; i++) { + (bool ok, bytes memory data) = address(redist).staticcall( + abi.encodeWithSignature("currentCommits(uint256)", i) + ); + if (!ok) break; + CommitView memory cv = abi.decode(data, (CommitView)); + pendingWSOwners[i] = cv.owner; + pendingWSRevealed[i] = cv.revealed; + pendingWSFreezeCountBefore[i] = stakeMock.freezeCount(cv.owner); + pendingWinnerSelectionLen++; + } + + bool okCall = actors[idx].callWinnerSelection(); + if (!okCall) return; + + // "Only once per round" should hold: a second success in the same round is forbidden. + if (lastWinnerSelectionRound == pendingWinnerSelectionRound) winnerSelectionSucceededTwiceSameRound = true; + lastWinnerSelectionRound = pendingWinnerSelectionRound; + + // Arm postconditions: non-revealers must have been frozen. + pendingWinnerSelection = true; + } + + // ----------------------------- + // Properties + // ----------------------------- + + function echidna_reveal_entries_imply_matching_commit() external view returns (bool) { + // For each reveal entry, there must exist a commit marked revealed with matching overlay/owner and revealIndex pointing here. + // + // `commit()` deletes `currentCommits` when `currentCommitRound` advances but does not clear + // `currentReveals` until the first `reveal()` of the new round (`reveal()` deletes when + // `currentRevealRound` catches up to `cr`). Until then, `currentCommitRound != currentRevealRound` + // even in **reveal phase** (currentPhaseCommit false): old `currentReveals` entries coexist with + // fresh unrevealed `currentCommits`. Skip linkage checks for that whole transitional window. + if (redist.currentCommitRound() != redist.currentRevealRound()) { + return true; + } + + uint256 rLim = _boundedRevealsLen(); + uint256 cLim = _boundedCommitsLen(); + for (uint256 i = 0; i < rLim; i++) { + (bool okR, bytes32 rOverlay, address rOwner) = _revealOverlayOwner(i); + if (!okR) return false; + + bool found = false; + for (uint256 j = 0; j < cLim; j++) { + (bool okC, bytes32 cOverlay, address cOwner, bool cRevealed, uint256 cRevealIndex) = _commitRevealLink( + j + ); + if (!okC) return false; + if (cRevealed && cRevealIndex == i && cOverlay == rOverlay && cOwner == rOwner) { + found = true; + break; + } + } + if (!found) return false; + } + return true; + } + + function echidna_winnerSelection_only_once_per_round() external view returns (bool) { + return !winnerSelectionSucceededTwiceSameRound; + } + + function echidna_last_winnerSelection_freezes_nonrevealed() external view returns (bool) { + if (!pendingWinnerSelection) return true; + // If we moved to another claim round, the commit set and expectations are stale; ignore. + if (redist.currentClaimRound() != pendingWinnerSelectionRound) return true; + + for (uint256 i = 0; i < pendingWinnerSelectionLen; i++) { + if (pendingWSRevealed[i]) continue; + address ow = pendingWSOwners[i]; + if (ow == address(0)) continue; + if (stakeMock.freezeCount(ow) <= pendingWSFreezeCountBefore[i]) return false; + // Freeze should move lastUpdated into the future in the mock. + if (stakeMock.lastUpdatedBlockNumberOfAddress(ow) <= block.number) return false; + } + return true; + } + + function echidna_commit_overlays_unique() external view returns (bool) { + (uint256 n, bytes32[25] memory overlays, , , ) = _scanCommits(); + for (uint256 i = 0; i < n; i++) { + bytes32 oi = overlays[i]; + for (uint256 j = i + 1; j < n; j++) { + bytes32 oj = overlays[j]; + if (oi != bytes32(0) && oi == oj) return false; + } + } + return true; + } + + function echidna_revealed_commit_indices_valid() external view returns (bool) { + ( + uint256 cN, + , + uint256[25] memory revealIndex, + bool[25] memory revealed, + address[25] memory owner + ) = _scanCommits(); + uint256 rN = _scanRevealsLen(); + for (uint256 i = 0; i < cN; i++) { + if (!revealed[i]) continue; + uint256 ri = revealIndex[i]; + if (ri >= rN) return false; + (bool ok, bytes32 rOverlay, address rOwner) = _revealOverlayOwner(ri); + if (!ok) return false; + // Compare against commit i overlay/owner. + (bool ok2, bytes32 cOverlay, address cOwner) = _commitOverlayOwner(i); + if (!ok2) return false; + if (rOverlay != cOverlay) return false; + if (rOwner != cOwner) return false; + if (cOwner != owner[i]) return false; + } + return true; + } + + function echidna_tracked_commit_matches_storage() external view returns (bool) { + uint64 liveCommitRound = redist.currentCommitRound(); + for (uint256 i = 0; i < ACTOR_COUNT; i++) { + if (!trackedHasCommit[i]) continue; + // `currentCommits` is deleted when a new commit round begins. + // Only assert strong postconditions for commits in the currently tracked commit round. + if (trackedRound[i] != liveCommitRound) continue; + + (bool ok, uint256 commitIdx) = _findCommit(trackedOverlay[i], trackedObfuscated[i]); + if (!ok) return false; + + (, bytes32 ov, address ow, , uint8 h, uint256 stake, bytes32 obf /* revealIndex */, ) = _commitFull( + commitIdx + ); + + if (ov != trackedOverlay[i]) return false; + if (obf != trackedObfuscated[i]) return false; + if (ow != address(actors[i])) return false; + if (h != trackedHeight[i]) return false; + if (stake != trackedStake[i]) return false; + } + return true; + } + + function echidna_tracked_reveal_matches_storage() external view returns (bool) { + uint64 liveCommitRound = redist.currentCommitRound(); + for (uint256 i = 0; i < ACTOR_COUNT; i++) { + if (!trackedHasReveal[i]) continue; + if (trackedRound[i] != liveCommitRound) continue; + if (!_checkTrackedReveal(i)) return false; + } + return true; + } + + // ----------------------------- + // View helpers (avoid needing array length getters) + // ----------------------------- + + function _scanCommits() + internal + view + returns ( + uint256 n, + bytes32[25] memory overlays, + uint256[25] memory revealIndex, + bool[25] memory revealed, + address[25] memory owner + ) + { + uint256 lim = _boundedCommitsLen(); + for (uint256 i = 0; i < lim; i++) { + (bool ok, bytes32 ov, address ow, bool rev, uint256 ri) = _commitFields(i); + if (!ok) break; + overlays[i] = ov; + owner[i] = ow; + revealed[i] = rev; + revealIndex[i] = ri; + n++; + } + } + + function _scanRevealsLen() internal view returns (uint256 n) { + n = _boundedRevealsLen(); + } + + function _commitOverlayOwner(uint256 i) internal view returns (bool ok, bytes32 ov, address ow) { + (ok, ov, ow, , ) = _commitFields(i); + } + + function _commitRevealLink( + uint256 i + ) internal view returns (bool ok, bytes32 overlay, address owner, bool revealed, uint256 revealIndex) { + bytes memory data; + (ok, data) = address(redist).staticcall(abi.encodeWithSignature("currentCommits(uint256)", i)); + if (!ok) return (false, bytes32(0), address(0), false, 0); + (overlay, owner, revealed, , , , revealIndex) = abi.decode( + data, + (bytes32, address, bool, uint8, uint256, bytes32, uint256) + ); + } + + function _commitFields(uint256 i) internal view returns (bool ok, bytes32 ov, address ow, bool rev, uint256 ri) { + bytes memory data; + (ok, data) = address(redist).staticcall(abi.encodeWithSignature("currentCommits(uint256)", i)); + if (!ok) return (false, bytes32(0), address(0), false, 0); + // Commit struct getter returns: + // (bytes32 overlay, address owner, bool revealed, uint8 height, uint256 stake, bytes32 obfuscatedHash, uint256 revealIndex) + (ov, ow, rev, , , , ri) = abi.decode(data, (bytes32, address, bool, uint8, uint256, bytes32, uint256)); + } + + function _revealOverlayOwner(uint256 i) internal view returns (bool ok, bytes32 ov, address ow) { + bytes memory data; + (ok, data) = address(redist).staticcall(abi.encodeWithSignature("currentReveals(uint256)", i)); + if (!ok) return (false, bytes32(0), address(0)); + // Reveal struct getter returns: + // (bytes32 overlay, address owner, uint8 depth, uint256 stake, uint256 stakeDensity, bytes32 hash) + (ov, ow, , , , ) = abi.decode(data, (bytes32, address, uint8, uint256, uint256, bytes32)); + } + + function _commitFull( + uint256 i + ) + internal + view + returns ( + bool ok, + bytes32 overlay, + address owner, + bool revealed, + uint8 height, + uint256 stake, + bytes32 obfuscatedHash, + uint256 revealIndex + ) + { + bytes memory data; + (ok, data) = address(redist).staticcall(abi.encodeWithSignature("currentCommits(uint256)", i)); + if (!ok) return (false, bytes32(0), address(0), false, 0, 0, bytes32(0), 0); + (overlay, owner, revealed, height, stake, obfuscatedHash, revealIndex) = abi.decode( + data, + (bytes32, address, bool, uint8, uint256, bytes32, uint256) + ); + } + + function _checkTrackedReveal(uint256 actorIdx) internal view returns (bool) { + (bool ok, uint256 commitIdx) = _findCommit(trackedOverlay[actorIdx], trackedObfuscated[actorIdx]); + if (!ok) return false; + + bytes memory cdata; + (ok, cdata) = address(redist).staticcall(abi.encodeWithSignature("currentCommits(uint256)", commitIdx)); + if (!ok) return false; + CommitView memory c = abi.decode(cdata, (CommitView)); + + if (c.owner != address(actors[actorIdx])) return false; + if (c.overlay != trackedOverlay[actorIdx]) return false; + if (c.obfuscatedHash != trackedObfuscated[actorIdx]) return false; + if (c.height != trackedHeight[actorIdx]) return false; + if (c.stake != trackedStake[actorIdx]) return false; + if (!c.revealed) return false; + + bytes memory rdata; + (ok, rdata) = address(redist).staticcall(abi.encodeWithSignature("currentReveals(uint256)", c.revealIndex)); + if (!ok) return false; + RevealView memory r = abi.decode(rdata, (RevealView)); + + if (r.overlay != trackedOverlay[actorIdx]) return false; + if (r.owner != address(actors[actorIdx])) return false; + if (r.depth != trackedDepth[actorIdx]) return false; + if (r.hash != trackedReserveHash[actorIdx]) return false; + if (r.stake != c.stake) return false; + + uint8 dr = trackedDepth[actorIdx] - c.height; + uint256 expectedDensity = c.stake * (uint256(1) << dr); + if (r.stakeDensity != expectedDensity) return false; + return true; + } + + function _findCommit(bytes32 overlay, bytes32 obfuscated) internal view returns (bool ok, uint256 idx) { + uint256 lim = _boundedCommitsLen(); + for (uint256 i = 0; i < lim; i++) { + (bool okI, bytes32 ov, , , , , bytes32 obf, ) = _commitFull(i); + if (!okI) break; + if (ov == overlay && obf == obfuscated) return (true, i); + } + return (false, 0); + } + + function _commitOverlayExists(bytes32 overlay) internal view returns (bool) { + uint256 lim = _boundedCommitsLen(); + for (uint256 i = 0; i < lim; i++) { + (bool ok, bytes32 ov, , , ) = _commitFields(i); + if (!ok) break; + if (ov == overlay) return true; + } + return false; + } + + function _backdateLastUpdated() internal view returns (uint256) { + uint256 twoRounds = 2 * 152; + if (block.number > twoRounds + 1) return block.number - twoRounds - 1; + return 1; + } + + function _boundStake(uint256 s) internal pure returns (uint256) { + // Keep stake densities well within uint256 range even if depthResponsibility grows a bit. + uint256 max = 1e24; + if (s == 0) return 1; + if (s > max) return (s % max) + 1; + return s; + } +} diff --git a/src/echidna/EchidnaStakeRegistryHarness.sol b/src/echidna/EchidnaStakeRegistryHarness.sol new file mode 100644 index 00000000..ba99631a --- /dev/null +++ b/src/echidna/EchidnaStakeRegistryHarness.sol @@ -0,0 +1,667 @@ +// SPDX-License-Identifier: BSD-3-Clause +pragma solidity ^0.8.19; + +import "../TestToken.sol"; +import "../Staking.sol"; + +contract ConstantPriceOracle is IPriceOracle { + uint32 internal immutable _price; + + constructor(uint32 price_) { + _price = price_; + } + + function currentPrice() external view returns (uint32) { + return _price; + } +} + +contract EchidnaStakeActor { + TestToken internal immutable token; + StakeRegistry internal immutable registry; + + constructor(TestToken token_, StakeRegistry registry_) { + token = token_; + registry = registry_; + token.approve(address(registry), type(uint256).max); + } + + function manageStake(bytes32 setNonce, uint256 addAmount, uint8 height) external returns (bool ok) { + (ok, ) = address(registry).call( + abi.encodeWithSelector(registry.manageStake.selector, setNonce, addAmount, height) + ); + } + + function withdrawFromStake() external returns (bool ok) { + (ok, ) = address(registry).call(abi.encodeWithSelector(registry.withdrawFromStake.selector)); + } + + function migrateStake() external returns (bool ok) { + (ok, ) = address(registry).call(abi.encodeWithSelector(registry.migrateStake.selector)); + } + + function tryPause() external returns (bool ok) { + (ok, ) = address(registry).call(abi.encodeWithSelector(registry.pause.selector)); + } + + function tryUnpause() external returns (bool ok) { + (ok, ) = address(registry).call(abi.encodeWithSelector(registry.unPause.selector)); + } + + function tryChangeNetworkId(uint64 newNetworkId) external returns (bool ok) { + (ok, ) = address(registry).call(abi.encodeWithSelector(registry.changeNetworkId.selector, newNetworkId)); + } + + function tryFreezeDeposit(address owner, uint256 time) external returns (bool ok) { + (ok, ) = address(registry).call(abi.encodeWithSelector(registry.freezeDeposit.selector, owner, time)); + } + + function trySlashDeposit(address owner, uint256 amount) external returns (bool ok) { + (ok, ) = address(registry).call(abi.encodeWithSelector(registry.slashDeposit.selector, owner, amount)); + } +} + +/// @notice Echidna harness for stateful, multi-actor fuzzing of StakeRegistry. +/// @dev Echidna calls public/external functions on this contract. +contract EchidnaStakeRegistryHarness { + TestToken internal immutable token; + StakeRegistry internal immutable registry; + ConstantPriceOracle internal immutable oracle; + + uint256 internal immutable initialSupply; + + uint256 internal constant MIN_STAKE = 100000000000000000; // 1e17 (matches StakeRegistry) + uint32 internal constant ORACLE_PRICE = 1; + + uint256 internal constant ACTOR_COUNT = 3; + EchidnaStakeActor[3] internal actors; + EchidnaStakeActor internal redistributor; + + uint64 internal trackedNetworkId; + + // Tracking per-actor last successful state. + uint256[3] internal lastCommittedStakeByActor; + bytes32[3] internal lastSetNonceByActor; + uint64[3] internal networkIdAtLastStakeByActor; + + // “Must never happen” flags (set by actions, checked by properties). + bool internal unauthorizedAdminCallSucceeded; + bool internal unauthorizedFreezeSlashSucceeded; + bool internal pausedManageStakeSucceeded; + bool internal frozenManageStakeSucceeded; + bool internal actionInvariantViolated; + + // Post-condition checks for the last *successful* manageStake(add > 0). + // We keep these checks "pending" only until the next action, so properties + // validate the immediate post-state without being invalidated by later actions. + bool internal pendingManageStakeAddCheck; + uint256 internal pendingActorIdx; + uint256 internal pendingAddAmount; + uint8 internal pendingHeight; + uint256 internal pendingPotentialBefore; + uint256 internal pendingRegistryBalanceBefore; + + // Post-condition checks for the last freeze/slash/migrate call (pending until next action). + bool internal pendingFreezeCheck; + uint256 internal pendingFreezeIdx; + bool internal pendingFreezeHadStake; + bytes32 internal pendingFreezeOverlay; + uint256 internal pendingFreezeCommitted; + uint256 internal pendingFreezePotential; + uint8 internal pendingFreezeHeight; + uint256 internal pendingFreezeExpectedLastUpdated; + + bool internal pendingSlashCheck; + uint256 internal pendingSlashIdx; + bool internal pendingSlashHadStake; + bytes32 internal pendingSlashOverlay; + uint256 internal pendingSlashCommitted; + uint256 internal pendingSlashPotential; + uint8 internal pendingSlashHeight; + uint256 internal pendingSlashLastUpdated; + uint256 internal pendingSlashAmount; + uint256 internal pendingSlashExpectedBlockNumber; + + bool internal pendingMigrateCheck; + uint256 internal pendingMigrateIdx; + bool internal pendingMigrateHadStake; + uint256 internal pendingMigratePotentialBefore; + uint256 internal pendingMigrateActorBalanceBefore; + uint256 internal pendingMigrateLastUpdatedBefore; + bool internal migrateSucceededWhileUnpaused; + + constructor() { + // Keep values modest so arithmetic in invariants stays safe. + initialSupply = 1_000_000_000_000_000_000_000_000; // 1e24 + + token = new TestToken("TestToken", "TT", initialSupply); + oracle = new ConstantPriceOracle(ORACLE_PRICE); + trackedNetworkId = 10; + registry = new StakeRegistry(address(token), trackedNetworkId, address(oracle)); + + // Create actors and fund them. + for (uint256 i = 0; i < ACTOR_COUNT; i++) { + actors[i] = new EchidnaStakeActor(token, registry); + token.transfer(address(actors[i]), initialSupply / 20); // 5% each + networkIdAtLastStakeByActor[i] = trackedNetworkId; + } + + // A dedicated redistributor actor (role granted by admin = this harness). + redistributor = new EchidnaStakeActor(token, registry); + registry.grantRole(registry.REDISTRIBUTOR_ROLE(), address(redistributor)); + } + + // ----------------------------- + // Actions (state transitions) + // ----------------------------- + + function act_fundActor(uint8 actorId, uint256 amount) external { + _clearPendingChecks(); + bytes32 d0 = _stakeDigest(address(actors[0])); + bytes32 d1 = _stakeDigest(address(actors[1])); + bytes32 d2 = _stakeDigest(address(actors[2])); + + EchidnaStakeActor a = _actor(actorId); + uint256 bal = token.balanceOf(address(this)); + if (bal == 0) return; + uint256 x = amount % (bal + 1); + if (x == 0) return; + token.transfer(address(a), x); + + if (_stakeDigest(address(actors[0])) != d0) actionInvariantViolated = true; + if (_stakeDigest(address(actors[1])) != d1) actionInvariantViolated = true; + if (_stakeDigest(address(actors[2])) != d2) actionInvariantViolated = true; + } + + function act_actor_manageStake(uint8 actorId, bytes32 setNonce, uint256 addAmount, uint8 height) external { + _clearPendingChecks(); + + uint256 idx = uint256(actorId) % ACTOR_COUNT; + EchidnaStakeActor actor = actors[idx]; + // Keep height small to avoid huge powers of two. + uint8 h = uint8(height % 16); + + uint256 available = token.balanceOf(address(actor)); + if (available == 0) return; + + uint256 add = addAmount % (available + 1); + + // If this is the first stake update, enforce the minimum stake rule + // (or skip the call when we can't satisfy it). + uint256 lastUpdated = registry.lastUpdatedBlockNumberOfAddress(address(actor)); + if (lastUpdated == 0 && add > 0) { + uint256 minStake = MIN_STAKE * (1 << h); + if (add < minStake) { + add = minStake; + if (add > available) return; + } + } + + // If paused, manageStake must not succeed. + if (registry.paused()) { + bool okPaused = actor.manageStake(setNonce, add, h); + if (okPaused) pausedManageStakeSucceeded = true; + return; + } + + // If frozen (including same-block update), manageStake must not succeed. + if (lastUpdated != 0 && lastUpdated >= block.number) { + bool okFrozen = actor.manageStake(setNonce, add, h); + if (okFrozen) frozenManageStakeSucceeded = true; + return; + } + + // Snapshot other actors so we can detect unintended writes. + (bytes32 otherDigestA, bytes32 otherDigestB) = _otherDigests(idx); + + // Prepare pending post-conditions only for add > 0. + if (add > 0) { + pendingActorIdx = idx; + pendingAddAmount = add; + pendingHeight = h; + (, , pendingPotentialBefore, , ) = registry.stakes(address(actor)); + pendingRegistryBalanceBefore = token.balanceOf(address(registry)); + } + + bool ok = actor.manageStake(setNonce, add, h); + if (!ok) return; + + _checkOtherDigestsUnchanged(idx, otherDigestA, otherDigestB); + + (, uint256 committedStake, , , ) = registry.stakes(address(actor)); + if (committedStake < lastCommittedStakeByActor[idx]) actionInvariantViolated = true; + lastCommittedStakeByActor[idx] = committedStake; + lastSetNonceByActor[idx] = setNonce; + networkIdAtLastStakeByActor[idx] = trackedNetworkId; + + // Arm post-condition properties for the immediate post-state. + if (add > 0) pendingManageStakeAddCheck = true; + } + + function act_actor_withdrawSurplus(uint8 actorId) external { + _clearPendingChecks(); + + uint256 idx = uint256(actorId) % ACTOR_COUNT; + EchidnaStakeActor a = actors[idx]; + (bytes32 otherDigestA, bytes32 otherDigestB) = _otherDigests(idx); + + (bytes32 ov, uint256 committed, uint256 potential, , uint8 h) = registry.stakes(address(a)); + uint256 beforeBal = token.balanceOf(address(a)); + + bool ok = a.withdrawFromStake(); + if (!ok) return; + + _checkOtherDigestsUnchanged(idx, otherDigestA, otherDigestB); + + (bytes32 ov2, , uint256 potentialAfter, , ) = registry.stakes(address(a)); + uint256 afterBal = token.balanceOf(address(a)); + + // No changes to overlay expected from withdraw. + if (ov2 != ov) actionInvariantViolated = true; + + // Expected surplus based on contract math. + uint256 effective = _min(potential, committed * (1 << h) * uint256(ORACLE_PRICE)); + uint256 surplus = potential - effective; + + if (surplus == 0) { + if (potentialAfter != potential) actionInvariantViolated = true; + if (afterBal != beforeBal) actionInvariantViolated = true; + return; + } + + if (potentialAfter + surplus != potential) actionInvariantViolated = true; + if (afterBal != beforeBal + surplus) actionInvariantViolated = true; + } + + function act_actor_migrateStake(uint8 actorId) external { + _clearPendingChecks(); + + uint256 idx = uint256(actorId) % ACTOR_COUNT; + EchidnaStakeActor a = actors[idx]; + (bytes32 otherDigestA, bytes32 otherDigestB) = _otherDigests(idx); + + pendingMigrateIdx = idx; + pendingMigrateActorBalanceBefore = token.balanceOf(address(a)); + (, , pendingMigratePotentialBefore, pendingMigrateLastUpdatedBefore, ) = registry.stakes(address(a)); + pendingMigrateHadStake = pendingMigrateLastUpdatedBefore != 0; + + bool ok = a.migrateStake(); + if (!ok) return; + + if (!registry.paused()) migrateSucceededWhileUnpaused = true; + _checkOtherDigestsUnchanged(idx, otherDigestA, otherDigestB); + pendingMigrateCheck = true; + + // If a stake existed, migrateStake refunds and deletes it. Reset per-actor tracking + // so future re-stakes don't incorrectly look like "commitment decreased". + if (pendingMigrateHadStake) { + lastCommittedStakeByActor[idx] = 0; + lastSetNonceByActor[idx] = bytes32(0); + networkIdAtLastStakeByActor[idx] = trackedNetworkId; + } + } + + function act_admin_pause() external { + _clearPendingChecks(); + bytes32 d0 = _stakeDigest(address(actors[0])); + bytes32 d1 = _stakeDigest(address(actors[1])); + bytes32 d2 = _stakeDigest(address(actors[2])); + registry.pause(); + if (_stakeDigest(address(actors[0])) != d0) actionInvariantViolated = true; + if (_stakeDigest(address(actors[1])) != d1) actionInvariantViolated = true; + if (_stakeDigest(address(actors[2])) != d2) actionInvariantViolated = true; + } + + function act_admin_unpause() external { + _clearPendingChecks(); + bytes32 d0 = _stakeDigest(address(actors[0])); + bytes32 d1 = _stakeDigest(address(actors[1])); + bytes32 d2 = _stakeDigest(address(actors[2])); + registry.unPause(); + if (_stakeDigest(address(actors[0])) != d0) actionInvariantViolated = true; + if (_stakeDigest(address(actors[1])) != d1) actionInvariantViolated = true; + if (_stakeDigest(address(actors[2])) != d2) actionInvariantViolated = true; + } + + function act_admin_changeNetworkId(uint64 newNetworkId) external { + _clearPendingChecks(); + bytes32 d0 = _stakeDigest(address(actors[0])); + bytes32 d1 = _stakeDigest(address(actors[1])); + bytes32 d2 = _stakeDigest(address(actors[2])); + registry.changeNetworkId(newNetworkId); + trackedNetworkId = newNetworkId; + if (_stakeDigest(address(actors[0])) != d0) actionInvariantViolated = true; + if (_stakeDigest(address(actors[1])) != d1) actionInvariantViolated = true; + if (_stakeDigest(address(actors[2])) != d2) actionInvariantViolated = true; + } + + function act_actor_tryPause(uint8 actorId) external { + _clearPendingChecks(); + bytes32 d0 = _stakeDigest(address(actors[0])); + bytes32 d1 = _stakeDigest(address(actors[1])); + bytes32 d2 = _stakeDigest(address(actors[2])); + bool ok = _actor(actorId).tryPause(); + if (ok) unauthorizedAdminCallSucceeded = true; + if (_stakeDigest(address(actors[0])) != d0) actionInvariantViolated = true; + if (_stakeDigest(address(actors[1])) != d1) actionInvariantViolated = true; + if (_stakeDigest(address(actors[2])) != d2) actionInvariantViolated = true; + } + + function act_actor_tryUnpause(uint8 actorId) external { + _clearPendingChecks(); + bytes32 d0 = _stakeDigest(address(actors[0])); + bytes32 d1 = _stakeDigest(address(actors[1])); + bytes32 d2 = _stakeDigest(address(actors[2])); + bool ok = _actor(actorId).tryUnpause(); + if (ok) unauthorizedAdminCallSucceeded = true; + if (_stakeDigest(address(actors[0])) != d0) actionInvariantViolated = true; + if (_stakeDigest(address(actors[1])) != d1) actionInvariantViolated = true; + if (_stakeDigest(address(actors[2])) != d2) actionInvariantViolated = true; + } + + function act_actor_tryChangeNetworkId(uint8 actorId, uint64 newNetworkId) external { + _clearPendingChecks(); + bytes32 d0 = _stakeDigest(address(actors[0])); + bytes32 d1 = _stakeDigest(address(actors[1])); + bytes32 d2 = _stakeDigest(address(actors[2])); + bool ok = _actor(actorId).tryChangeNetworkId(newNetworkId); + if (ok) unauthorizedAdminCallSucceeded = true; + if (_stakeDigest(address(actors[0])) != d0) actionInvariantViolated = true; + if (_stakeDigest(address(actors[1])) != d1) actionInvariantViolated = true; + if (_stakeDigest(address(actors[2])) != d2) actionInvariantViolated = true; + } + + function act_redistributor_freeze(uint8 targetActorId, uint32 time) external { + _clearPendingChecks(); + + uint256 idx = uint256(targetActorId) % ACTOR_COUNT; + EchidnaStakeActor t = actors[idx]; + (bytes32 otherDigestA, bytes32 otherDigestB) = _otherDigests(idx); + + ( + pendingFreezeOverlay, + pendingFreezeCommitted, + pendingFreezePotential, + pendingFreezeExpectedLastUpdated, + pendingFreezeHeight + ) = registry.stakes(address(t)); + pendingFreezeIdx = idx; + pendingFreezeHadStake = pendingFreezeExpectedLastUpdated != 0; + pendingFreezeExpectedLastUpdated = pendingFreezeHadStake ? block.number + uint256(time) : 0; + + bool ok = redistributor.tryFreezeDeposit(address(t), uint256(time)); + if (!ok) return; + + _checkOtherDigestsUnchanged(idx, otherDigestA, otherDigestB); + pendingFreezeCheck = true; + } + + function act_redistributor_slash(uint8 targetActorId, uint256 amount) external { + _clearPendingChecks(); + + uint256 idx = uint256(targetActorId) % ACTOR_COUNT; + EchidnaStakeActor t = actors[idx]; + (bytes32 otherDigestA, bytes32 otherDigestB) = _otherDigests(idx); + + ( + pendingSlashOverlay, + pendingSlashCommitted, + pendingSlashPotential, + pendingSlashLastUpdated, + pendingSlashHeight + ) = registry.stakes(address(t)); + pendingSlashIdx = idx; + pendingSlashHadStake = pendingSlashLastUpdated != 0; + pendingSlashAmount = amount; + pendingSlashExpectedBlockNumber = block.number; + + bool ok = redistributor.trySlashDeposit(address(t), amount); + if (!ok) return; + + _checkOtherDigestsUnchanged(idx, otherDigestA, otherDigestB); + pendingSlashCheck = true; + + // If the slash deleted the stake (amount >= potential), reset per-actor tracking + // so future re-stakes don't incorrectly look like "commitment decreased". + if (pendingSlashHadStake && pendingSlashPotential <= pendingSlashAmount) { + lastCommittedStakeByActor[idx] = 0; + lastSetNonceByActor[idx] = bytes32(0); + networkIdAtLastStakeByActor[idx] = trackedNetworkId; + } + } + + function act_actor_tryFreeze(uint8 actorId, uint8 targetActorId, uint32 time) external { + _clearPendingChecks(); + bytes32 d0 = _stakeDigest(address(actors[0])); + bytes32 d1 = _stakeDigest(address(actors[1])); + bytes32 d2 = _stakeDigest(address(actors[2])); + bool ok = _actor(actorId).tryFreezeDeposit(address(_actor(targetActorId)), uint256(time)); + if (ok) unauthorizedFreezeSlashSucceeded = true; + if (_stakeDigest(address(actors[0])) != d0) actionInvariantViolated = true; + if (_stakeDigest(address(actors[1])) != d1) actionInvariantViolated = true; + if (_stakeDigest(address(actors[2])) != d2) actionInvariantViolated = true; + } + + function act_actor_trySlash(uint8 actorId, uint8 targetActorId, uint256 amount) external { + _clearPendingChecks(); + bytes32 d0 = _stakeDigest(address(actors[0])); + bytes32 d1 = _stakeDigest(address(actors[1])); + bytes32 d2 = _stakeDigest(address(actors[2])); + bool ok = _actor(actorId).trySlashDeposit(address(_actor(targetActorId)), amount); + if (ok) unauthorizedFreezeSlashSucceeded = true; + if (_stakeDigest(address(actors[0])) != d0) actionInvariantViolated = true; + if (_stakeDigest(address(actors[1])) != d1) actionInvariantViolated = true; + if (_stakeDigest(address(actors[2])) != d2) actionInvariantViolated = true; + } + + // ----------------------------- + // Properties (checked by Echidna) + // ----------------------------- + + function echidna_never_performed_forbidden_calls() external view returns (bool) { + return + !unauthorizedAdminCallSucceeded && + !unauthorizedFreezeSlashSucceeded && + !pausedManageStakeSucceeded && + !frozenManageStakeSucceeded && + !actionInvariantViolated; + } + + function echidna_registry_balance_covers_sum_potential() external view returns (bool) { + uint256 sumPotential; + for (uint256 i = 0; i < ACTOR_COUNT; i++) { + (, , uint256 potentialStake, , ) = registry.stakes(address(actors[i])); + sumPotential += potentialStake; + } + return token.balanceOf(address(registry)) >= sumPotential; + } + + /// @notice After a successful manageStake(add > 0), potential and registry balance + /// must both increase by exactly `add`. + function echidna_last_manageStake_add_updates_potential_and_registry_balance() external view returns (bool) { + if (!pendingManageStakeAddCheck) return true; + address a = address(actors[pendingActorIdx]); + (, , uint256 potentialAfter, , ) = registry.stakes(a); + if (potentialAfter != pendingPotentialBefore + pendingAddAmount) return false; + if (token.balanceOf(address(registry)) != pendingRegistryBalanceBefore + pendingAddAmount) return false; + return true; + } + + /// @notice After a successful manageStake(add > 0), committedStake must be + /// recomputed to floor(potential / (price * 2**height)). + function echidna_last_manageStake_add_recomputes_committedStake() external view returns (bool) { + if (!pendingManageStakeAddCheck) return true; + address a = address(actors[pendingActorIdx]); + (, uint256 committedAfter, uint256 potentialAfter, , uint8 hAfter) = registry.stakes(a); + if (hAfter != pendingHeight) return false; + uint256 denom = uint256(ORACLE_PRICE) * (1 << pendingHeight); + uint256 expectedCommitted = potentialAfter / denom; + return committedAfter == expectedCommitted; + } + + function echidna_migrate_never_succeeds_while_unpaused() external view returns (bool) { + return !migrateSucceededWhileUnpaused; + } + + function echidna_last_migrate_refunds_and_deletes_when_stake_exists() external view returns (bool) { + if (!pendingMigrateCheck) return true; + address a = address(actors[pendingMigrateIdx]); + + // migrateStake has whenPaused; if the call succeeded, we must be paused. + if (!registry.paused()) return false; + + if (!pendingMigrateHadStake) { + // No stake existed; migrate is a no-op. + if (token.balanceOf(a) != pendingMigrateActorBalanceBefore) return false; + return registry.lastUpdatedBlockNumberOfAddress(a) == 0; + } + + // Stake existed; it must be deleted and balance refunded. + if (token.balanceOf(a) != pendingMigrateActorBalanceBefore + pendingMigratePotentialBefore) return false; + return registry.lastUpdatedBlockNumberOfAddress(a) == 0; + } + + function echidna_last_freeze_only_updates_lastUpdated() external view returns (bool) { + if (!pendingFreezeCheck) return true; + address a = address(actors[pendingFreezeIdx]); + (bytes32 ov, uint256 c, uint256 p, uint256 u, uint8 h) = registry.stakes(a); + + if (!pendingFreezeHadStake) { + return ov == bytes32(0) && c == 0 && p == 0 && u == 0 && h == 0; + } + + if (ov != pendingFreezeOverlay) return false; + if (c != pendingFreezeCommitted) return false; + if (p != pendingFreezePotential) return false; + if (h != pendingFreezeHeight) return false; + return u == pendingFreezeExpectedLastUpdated; + } + + function echidna_last_slash_updates_expected_fields() external view returns (bool) { + if (!pendingSlashCheck) return true; + address a = address(actors[pendingSlashIdx]); + (bytes32 ov, uint256 c, uint256 p, uint256 u, uint8 h) = registry.stakes(a); + + if (!pendingSlashHadStake) { + // No stake existed; slash does nothing. + return ov == bytes32(0) && c == 0 && p == 0 && u == 0 && h == 0; + } + + if (pendingSlashPotential > pendingSlashAmount) { + // Partial slash: only potential decreases, lastUpdated set to block.number at slash time. + if (ov != pendingSlashOverlay) return false; + if (c != pendingSlashCommitted) return false; + if (h != pendingSlashHeight) return false; + if (p != pendingSlashPotential - pendingSlashAmount) return false; + return u == pendingSlashExpectedBlockNumber; + } + + // Full slash: stake deleted. + return ov == bytes32(0) && c == 0 && p == 0 && u == 0 && h == 0; + } + + function echidna_stake_committed_never_decreases_per_actor() external view returns (bool) { + for (uint256 i = 0; i < ACTOR_COUNT; i++) { + (, uint256 committedStake, , uint256 lastUpdated, ) = registry.stakes(address(actors[i])); + if (lastUpdated == 0) continue; + if (committedStake < lastCommittedStakeByActor[i]) return false; + } + return true; + } + + function echidna_nodeEffective_matches_freeze_rule_per_actor() external view returns (bool) { + for (uint256 i = 0; i < ACTOR_COUNT; i++) { + (, uint256 committedStake, uint256 potentialStake, uint256 lastUpdated, uint8 h) = registry.stakes( + address(actors[i]) + ); + uint256 fromView = registry.nodeEffectiveStake(address(actors[i])); + if (lastUpdated == 0) { + if (fromView != 0) return false; + continue; + } + if (lastUpdated >= block.number) { + if (fromView != 0) return false; + continue; + } + uint256 expected = _min(potentialStake, committedStake * (1 << h) * uint256(ORACLE_PRICE)); + if (fromView != expected) return false; + } + return true; + } + + function echidna_empty_state_is_zeroed_for_all() external view returns (bool) { + for (uint256 i = 0; i < ACTOR_COUNT; i++) { + (bytes32 overlay, uint256 committedStake, uint256 potentialStake, uint256 lastUpdated, uint8 h) = registry + .stakes(address(actors[i])); + if (lastUpdated != 0) continue; + if (overlay != bytes32(0) || committedStake != 0 || potentialStake != 0 || h != 0) return false; + } + return true; + } + + function echidna_overlay_matches_last_manageStake_for_all() external view returns (bool) { + for (uint256 i = 0; i < ACTOR_COUNT; i++) { + (bytes32 overlay, , , uint256 lastUpdated, ) = registry.stakes(address(actors[i])); + if (lastUpdated == 0) continue; + bytes32 expected = keccak256( + abi.encodePacked(address(actors[i]), _reverse(networkIdAtLastStakeByActor[i]), lastSetNonceByActor[i]) + ); + if (overlay != expected) return false; + } + return true; + } + + function _min(uint256 a, uint256 b) internal pure returns (uint256) { + return a < b ? a : b; + } + + function _reverse(uint64 input) internal pure returns (uint64 v) { + v = input; + v = ((v & 0xFF00FF00FF00FF00) >> 8) | ((v & 0x00FF00FF00FF00FF) << 8); + v = ((v & 0xFFFF0000FFFF0000) >> 16) | ((v & 0x0000FFFF0000FFFF) << 16); + v = (v >> 32) | (v << 32); + } + + function _actor(uint8 actorId) internal view returns (EchidnaStakeActor) { + return actors[uint256(actorId) % ACTOR_COUNT]; + } + + function _stakeDigest(address who) internal view returns (bytes32) { + (bytes32 overlay, uint256 committedStake, uint256 potentialStake, uint256 lastUpdated, uint8 h) = registry + .stakes(who); + return keccak256(abi.encodePacked(overlay, committedStake, potentialStake, lastUpdated, h)); + } + + function _otherDigests(uint256 idx) internal view returns (bytes32 dA, bytes32 dB) { + if (idx == 0) { + dA = _stakeDigest(address(actors[1])); + dB = _stakeDigest(address(actors[2])); + } else if (idx == 1) { + dA = _stakeDigest(address(actors[0])); + dB = _stakeDigest(address(actors[2])); + } else { + dA = _stakeDigest(address(actors[0])); + dB = _stakeDigest(address(actors[1])); + } + } + + function _checkOtherDigestsUnchanged(uint256 idx, bytes32 dA, bytes32 dB) internal { + if (idx == 0) { + if (_stakeDigest(address(actors[1])) != dA) actionInvariantViolated = true; + if (_stakeDigest(address(actors[2])) != dB) actionInvariantViolated = true; + } else if (idx == 1) { + if (_stakeDigest(address(actors[0])) != dA) actionInvariantViolated = true; + if (_stakeDigest(address(actors[2])) != dB) actionInvariantViolated = true; + } else { + if (_stakeDigest(address(actors[0])) != dA) actionInvariantViolated = true; + if (_stakeDigest(address(actors[1])) != dB) actionInvariantViolated = true; + } + } + + function _clearPendingChecks() internal { + pendingManageStakeAddCheck = false; + pendingFreezeCheck = false; + pendingSlashCheck = false; + pendingMigrateCheck = false; + } +} diff --git a/src/echidna/EchidnaSystemHarness.sol b/src/echidna/EchidnaSystemHarness.sol new file mode 100644 index 00000000..7ee68734 --- /dev/null +++ b/src/echidna/EchidnaSystemHarness.sol @@ -0,0 +1,366 @@ +// SPDX-License-Identifier: BSD-3-Clause +pragma solidity ^0.8.19; + +import "../TestToken.sol"; +import "../PostageStamp.sol"; +import "../PriceOracle.sol"; +import "../Redistribution.sol" as RedistMod; +import "../Staking.sol" as StakingMod; +import "./RedistributionExposed.sol"; + +contract EchidnaSystemActor { + TestToken internal immutable token; + StakingMod.StakeRegistry internal immutable stake; + PostageStamp internal immutable stamp; + PriceOracle internal immutable oracle; + RedistMod.Redistribution internal immutable redist; + + constructor(TestToken t, StakingMod.StakeRegistry s, PostageStamp p, PriceOracle o, RedistMod.Redistribution r) { + token = t; + stake = s; + stamp = p; + oracle = o; + redist = r; + + token.approve(address(stake), type(uint256).max); + token.approve(address(stamp), type(uint256).max); + } + + function callManageStake(bytes32 setNonce, uint256 addAmount, uint8 height) external returns (bool ok) { + (ok, ) = address(stake).call(abi.encodeWithSelector(stake.manageStake.selector, setNonce, addAmount, height)); + } + + function callWithdrawFromStake() external returns (bool ok) { + (ok, ) = address(stake).call(abi.encodeWithSelector(stake.withdrawFromStake.selector)); + } + + function callCreateBatch( + address owner, + uint256 initialBalancePerChunk, + uint8 depth, + uint8 bucketDepth, + bytes32 nonce, + bool immutableFlag + ) external returns (bool ok) { + (ok, ) = address(stamp).call( + abi.encodeWithSelector( + stamp.createBatch.selector, + owner, + initialBalancePerChunk, + depth, + bucketDepth, + nonce, + immutableFlag + ) + ); + } + + function callTopUp(bytes32 batchId, uint256 topupAmountPerChunk) external returns (bool ok) { + (ok, ) = address(stamp).call(abi.encodeWithSignature("topUp(bytes32,uint256)", batchId, topupAmountPerChunk)); + } + + function callIncreaseDepth(bytes32 batchId, uint8 newDepth) external returns (bool ok) { + (ok, ) = address(stamp).call(abi.encodeWithSignature("increaseDepth(bytes32,uint8)", batchId, newDepth)); + } + + function callExpireAll() external returns (bool ok) { + (ok, ) = address(stamp).call(abi.encodeWithSelector(stamp.expireLimited.selector, type(uint256).max)); + } + + function callCommit(bytes32 obfuscatedHash, uint64 roundNumber) external returns (bool ok) { + (ok, ) = address(redist).call(abi.encodeWithSelector(redist.commit.selector, obfuscatedHash, roundNumber)); + } + + function callReveal(uint8 depth, bytes32 hash, bytes32 nonce) external returns (bool ok) { + (ok, ) = address(redist).call(abi.encodeWithSelector(redist.reveal.selector, depth, hash, nonce)); + } + + function callAdjustPrice(uint16 redundancy) external returns (bool ok) { + (ok, ) = address(oracle).call(abi.encodeWithSelector(oracle.adjustPrice.selector, redundancy)); + } +} + +/// @notice Integration fuzz harness: StakeRegistry + PostageStamp + PriceOracle + Redistribution wired together. +contract EchidnaSystemHarness { + uint256 internal constant ACTOR_COUNT = 3; + + TestToken internal immutable token; + PostageStamp internal immutable stamp; + PriceOracle internal immutable oracle; + StakingMod.StakeRegistry internal immutable stake; + RedistMod.Redistribution internal immutable redist; + + EchidnaSystemActor[3] internal actors; + uint256 internal constant BOOTSTRAP_HEIGHT = 16; + bytes32[3] internal bootstrapNonce; + + // Integration negative-test flags. + bool internal unauthorizedOracleAdjustSucceeded; + + // Tracked commit/reveal preimages for the integrated happy-path flow. + bool[3] internal trackedHasCommit; + bool[3] internal trackedHasReveal; + uint64[3] internal trackedRound; + bytes32[3] internal trackedObfuscated; + bytes32[3] internal trackedHash; + bytes32[3] internal trackedRevealNonce; + uint8[3] internal trackedDepth; + + constructor() { + token = new TestToken("TestToken", "TST", 0); + + // Deploy postage first; oracle depends on it. + stamp = new PostageStamp(address(token), 16); + oracle = new PriceOracle(address(stamp)); + + // Wire roles: the oracle must be able to call PostageStamp.setPrice. + stamp.grantRole(stamp.PRICE_ORACLE_ROLE(), address(oracle)); + + // Deploy stake registry (uses oracle.currentPrice()). + stake = new StakingMod.StakeRegistry(address(token), 1, address(oracle)); + + // Deploy redistribution (uses stake/stamp/oracle). Exposed wrapper adds length helpers for harness scans. + redist = RedistMod.Redistribution( + address(new RedistributionExposed(address(stake), address(stamp), address(oracle))) + ); + + // Wire roles: redistribution must be able to freeze stake and withdraw the stamp pot. + stake.grantRole(stake.REDISTRIBUTOR_ROLE(), address(redist)); + stamp.grantRole(stamp.REDISTRIBUTOR_ROLE(), address(redist)); + + // Create actor contracts and pre-fund + pre-stake them. + for (uint256 i = 0; i < ACTOR_COUNT; i++) { + actors[i] = new EchidnaSystemActor(token, stake, stamp, oracle, redist); + bootstrapNonce[i] = keccak256(abi.encodePacked("bootstrap", i)); + // Mint enough for both staking and postage operations. + token.mint(address(actors[i]), 1e28); + // Bootstrap a stake early so that after 2 rounds pass, commit() can succeed. + actors[i].callManageStake(bootstrapNonce[i], 1e24, uint8(BOOTSTRAP_HEIGHT)); + } + + // Create a dedicated price updater (actor[0]) for adjustPrice. + oracle.grantRole(oracle.PRICE_UPDATER_ROLE(), address(actors[0])); + } + + // ----------------------------- + // Integration actions + // ----------------------------- + + /// @dev No-op that lets Echidna advance block.number without side effects, + /// helping the fuzzer walk through round phases. + function act_tick() external {} + + function act_actor_manageStake(uint8 actorId, bytes32 setNonce, uint256 addAmount, uint8 height) external { + EchidnaSystemActor a = actors[uint256(actorId) % ACTOR_COUNT]; + uint8 h = uint8(height % 32); + uint256 amt = _boundStakeAdd(addAmount); + a.callManageStake(setNonce, amt, h); + } + + function act_actor_withdrawSurplus(uint8 actorId) external { + EchidnaSystemActor a = actors[uint256(actorId) % ACTOR_COUNT]; + a.callWithdrawFromStake(); + } + + function act_actor_createBatch( + uint8 actorId, + uint256 initialBalancePerChunk, + uint8 depth, + uint8 bucketDepth, + bytes32 nonce, + bool imm + ) external { + EchidnaSystemActor a = actors[uint256(actorId) % ACTOR_COUNT]; + uint8 minBucket = stamp.minimumBucketDepth(); + // depth must exceed minimumBucketDepth; allow [minBucket+1 .. minBucket+10] + uint8 d = uint8(minBucket + 1 + (depth % 10)); + // bucketDepth must be in [minBucket, d-1] + uint8 b = uint8(minBucket + (bucketDepth % (d - minBucket))); + + uint256 min = stamp.minimumInitialBalancePerChunk(); + uint256 init = initialBalancePerChunk % (min + 1e6); + if (init < min) init = min; + if (init == 0) init = 1; + + a.callCreateBatch(address(a), init, d, b, nonce, imm); + } + + function act_actor_topUp(uint8 actorId, bytes32 batchId, uint256 topupAmountPerChunk) external { + EchidnaSystemActor a = actors[uint256(actorId) % ACTOR_COUNT]; + uint256 amt = topupAmountPerChunk % 1e9; + if (amt == 0) amt = 1; + a.callTopUp(batchId, amt); + } + + function act_actor_increaseDepth(uint8 actorId, bytes32 batchId, uint8 newDepth) external { + EchidnaSystemActor a = actors[uint256(actorId) % ACTOR_COUNT]; + uint8 d = uint8((newDepth % 12) + 1); + a.callIncreaseDepth(batchId, d); + } + + function act_actor_expireAll(uint8 actorId) external { + EchidnaSystemActor a = actors[uint256(actorId) % ACTOR_COUNT]; + a.callExpireAll(); + } + + function act_admin_setOraclePrice(uint32 p) external { + // This should update both oracle state and PostageStamp.lastPrice (via setPrice()). + oracle.setPrice(p); + } + + function act_updater_adjustOraclePrice(uint16 redundancy) external { + // Only actor[0] has PRICE_UPDATER_ROLE. + actors[0].callAdjustPrice(uint16((redundancy % 8) + 1)); + } + + function act_rando_tryAdjustOraclePrice(uint8 actorId, uint16 redundancy) external { + EchidnaSystemActor a = actors[uint256(actorId) % ACTOR_COUNT]; + bool ok = a.callAdjustPrice(uint16((redundancy % 8) + 1)); + if (ok && address(a) != address(actors[0])) unauthorizedOracleAdjustSucceeded = true; + } + + function act_redist_happyCommit(uint8 actorId, bytes32 hash, bytes32 revealNonce) external { + if (redist.paused()) return; + if (!redist.currentPhaseCommit()) return; + // Avoid the commit-phase last-block restriction. + if (block.number % 152 == (152 / 4) - 1) return; + + uint256 idx = uint256(actorId) % ACTOR_COUNT; + EchidnaSystemActor a = actors[idx]; + + // Must have staked at least 2 rounds prior. + uint256 lastUpdated = stake.lastUpdatedBlockNumberOfAddress(address(a)); + if (lastUpdated == 0) return; + if (lastUpdated >= block.number - 2 * 152) return; + + // Use the actor's current staking height as the reveal depth (depthResponsibility = 0 => proximity always passes). + uint8 height = stake.heightOfAddress(address(a)); + uint8 depth = height; + + bytes32 overlay = stake.overlayOfAddress(address(a)); + bytes32 obfuscated = redist.wrapCommit(overlay, depth, hash, revealNonce); + + bool ok = a.callCommit(obfuscated, redist.currentRound()); + if (!ok) return; + + trackedHasCommit[idx] = true; + trackedHasReveal[idx] = false; + trackedRound[idx] = redist.currentRound(); + trackedObfuscated[idx] = obfuscated; + trackedHash[idx] = hash; + trackedRevealNonce[idx] = revealNonce; + trackedDepth[idx] = depth; + } + + function act_redist_happyReveal(uint8 actorId) external { + if (redist.paused()) return; + if (!redist.currentPhaseReveal()) return; + + uint256 idx = uint256(actorId) % ACTOR_COUNT; + if (!trackedHasCommit[idx] || trackedHasReveal[idx]) return; + + // Must reveal in the same round that holds commits. + if (redist.currentRound() != trackedRound[idx]) return; + if (redist.currentCommitRound() != trackedRound[idx]) return; + + EchidnaSystemActor a = actors[idx]; + bool ok = a.callReveal(trackedDepth[idx], trackedHash[idx], trackedRevealNonce[idx]); + if (!ok) return; + trackedHasReveal[idx] = true; + } + + // ----------------------------- + // Integration properties + // ----------------------------- + + function echidna_unauthorized_oracle_adjust_never_succeeds() external view returns (bool) { + return !unauthorizedOracleAdjustSucceeded; + } + + function echidna_oracle_price_matches_stamp_lastPrice_when_updated() external view returns (bool) { + // `PostageStamp.lastPrice` updates on every successful oracle `setPrice`/`adjustPrice` call. + // We don't assert it *always* equals oracle.currentPrice(), because it can lag if the stamp call failed. + // But in this integrated harness, oracle holds PRICE_ORACLE_ROLE and the stamp call should succeed. + uint64 lp = stamp.lastPrice(); + if (lp == 0) return true; // not updated yet + return uint32(lp) == oracle.currentPrice(); + } + + function echidna_stamp_internal_pot_not_above_contract_balance() external view returns (bool) { + // Raw `pot` tracks accrued liability; it must not exceed ERC20 balance held by the stamp contract. + // (`totalPot()` caps at balance but is non-view; this is the meaningful accounting check.) + return stamp.pot() <= token.balanceOf(address(stamp)); + } + + function echidna_tracked_redist_commit_reveal_consistent() external view returns (bool) { + uint64 liveCommitRound = redist.currentCommitRound(); + for (uint256 i = 0; i < ACTOR_COUNT; i++) { + if (!trackedHasCommit[i]) continue; + if (trackedRound[i] != liveCommitRound) continue; + + // Verify the commit exists in storage (scan bounded prefix). + if (!_commitExists(trackedObfuscated[i], address(actors[i]))) return false; + } + + for (uint256 i = 0; i < ACTOR_COUNT; i++) { + if (!trackedHasReveal[i]) continue; + if (trackedRound[i] != liveCommitRound) continue; + + if (!_revealMatchesCommit(address(actors[i]), trackedDepth[i], trackedHash[i])) return false; + } + return true; + } + + // ----------------------------- + // Internal helpers + // ----------------------------- + + function _boundStakeAdd(uint256 a) internal pure returns (uint256) { + if (a == 0) return 1e18; + uint256 max = 1e25; + if (a > max) return (a % max) + 1; + return a; + } + + function _commitExists(bytes32 obfuscated, address owner) internal view returns (bool) { + uint256 lim = RedistributionExposed(address(redist)).currentCommitsLength(); + if (lim > 25) lim = 25; + for (uint256 i = 0; i < lim; i++) { + (bool ok, bytes memory data) = address(redist).staticcall( + abi.encodeWithSignature("currentCommits(uint256)", i) + ); + if (!ok) break; + (bytes32 ov, address ow, bool rev, uint8 h, uint256 st, bytes32 obf, uint256 ri) = abi.decode( + data, + (bytes32, address, bool, uint8, uint256, bytes32, uint256) + ); + ov; + rev; + h; + st; + ri; + if (ow == owner && obf == obfuscated) return true; + } + return false; + } + + function _revealMatchesCommit(address owner, uint8 depth, bytes32 hash) internal view returns (bool) { + uint256 lim = RedistributionExposed(address(redist)).currentRevealsLength(); + if (lim > 25) lim = 25; + for (uint256 i = 0; i < lim; i++) { + (bool ok, bytes memory data) = address(redist).staticcall( + abi.encodeWithSignature("currentReveals(uint256)", i) + ); + if (!ok) break; + (bytes32 ov, address ow, uint8 d, uint256 st, uint256 sd, bytes32 h) = abi.decode( + data, + (bytes32, address, uint8, uint256, uint256, bytes32) + ); + ov; + st; + sd; + if (ow == owner && d == depth && h == hash) return true; + } + return false; + } +} diff --git a/src/echidna/RedistributionExposed.sol b/src/echidna/RedistributionExposed.sol new file mode 100644 index 00000000..e196c519 --- /dev/null +++ b/src/echidna/RedistributionExposed.sol @@ -0,0 +1,26 @@ +// SPDX-License-Identifier: BSD-3-Clause +pragma solidity ^0.8.19; + +import "../Redistribution.sol"; + +/// @notice Test/fuzz wrapper: exposes `winnerSelection` and array lengths so harnesses need not call +/// the auto-generated `currentCommits(i)` / `currentReveals(i)` getters out of bounds (those revert). +contract RedistributionExposed is Redistribution { + constructor( + address staking, + address postageContract, + address oracleContract + ) Redistribution(staking, postageContract, oracleContract) {} + + function exposedWinnerSelection() external { + winnerSelection(); + } + + function currentCommitsLength() external view returns (uint256) { + return currentCommits.length; + } + + function currentRevealsLength() external view returns (uint256) { + return currentReveals.length; + } +} diff --git a/test/PostageStamp.test.ts b/test/PostageStamp.test.ts index 36b9026b..4f05706b 100644 --- a/test/PostageStamp.test.ts +++ b/test/PostageStamp.test.ts @@ -1161,6 +1161,9 @@ describe('PostageStamp', function () { describe('when copyBatch creates a batch', function () { beforeEach(async function () { + postageStampStamper = await ethers.getContract('PostageStamp', stamper); + token = await ethers.getContract('TestToken', deployer); + const postageStampDeployer = await ethers.getContract('PostageStamp', deployer); const admin = await postageStampStamper.DEFAULT_ADMIN_ROLE(); await postageStampDeployer.grantRole(admin, stamper); @@ -1376,6 +1379,10 @@ describe('PostageStamp', function () { const price = 100; await setPrice(price); + const currentTotalOutPayment = parseInt(await postageStampStamper.currentTotalOutPayment()); + const lastPrice = parseInt(await postageStampStamper.lastPrice()); + const expectedNormalisedBalance = batch.initialPaymentPerChunk + currentTotalOutPayment + lastPrice; + await expect( postageStampStamper.copyBatch( stamper, @@ -1390,14 +1397,14 @@ describe('PostageStamp', function () { .withArgs( batch.id, transferAmount, - price + batch.initialPaymentPerChunk, + expectedNormalisedBalance, stamper, batch.depth, batch.bucketDepth, batch.immutable ); const stamp = await postageStampStamper.batches(batch.id); - expect(stamp[4]).to.equal(price + batch.initialPaymentPerChunk); + expect(stamp[4]).to.equal(expectedNormalisedBalance); }); it('should include pending totalOutpayment in the normalised balance', async function () {