From 639fc76bce5e52e16f4bb4cff04add804940eed7 Mon Sep 17 00:00:00 2001 From: William Weishuhn Date: Sun, 6 Sep 2026 03:09:54 -0400 Subject: [PATCH 1/3] Verify original Foundry assertions and concrete exported properties --- .github/workflows/ci.yml | 26 +- CHANGELOG.md | 7 + README.md | 37 +- package.json | 7 +- src/cli.js | 113 +++--- src/cvl-export.js | 380 ++++++++---------- src/echidna-gen.js | 123 ++++-- src/forge-symb.js | 291 +++++--------- src/halmos-runner.js | 149 ++++--- src/solparse.js | 84 ++++ test/cvl-compile.js | 26 ++ test/e2e.js | 39 +- test/exporters.test.js | 56 +++ test/fixtures/fuzz-project/foundry.toml | 10 + .../fuzz-project/test/Accounting.t.sol | 33 ++ test/symbolic.test.js | 134 ++++++ 16 files changed, 938 insertions(+), 577 deletions(-) create mode 100644 src/solparse.js create mode 100644 test/cvl-compile.js create mode 100644 test/exporters.test.js create mode 100644 test/fixtures/fuzz-project/foundry.toml create mode 100644 test/fixtures/fuzz-project/test/Accounting.t.sol create mode 100644 test/symbolic.test.js diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index ab4be4a..6ee5c43 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -33,16 +33,40 @@ jobs: - uses: foundry-rs/foundry-toolchain@v1 - uses: actions/setup-python@v5 with: - python-version: '3.x' + python-version: '3.12' - run: pip install halmos==0.3.3 z3-solver - uses: actions/setup-node@v4 with: node-version: '20.x' - run: npm install + - name: Require real Forge, Halmos and generated-harness regressions + run: node --test test/*.test.js + env: + COUNTERFLOW_REQUIRE_SYMBOLIC: '1' # Expectations gate: safe references must PASS, known exploits must FAIL # with a counterexample. Any regression or lost trophy fails the job. - run: node src/cli.js bytecode --expect + certora-local-compile: + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@v4 + - uses: actions/setup-python@v5 + with: + python-version: '3.12' + - uses: actions/setup-node@v4 + with: + node-version: '20.x' + - uses: actions/setup-java@v4 + with: + distribution: temurin + java-version: '21' + - run: pip install certora-cli==8.19.1 solc-select + - run: solc-select install 0.8.24 && solc-select use 0.8.24 + # --compilation_steps_only never submits a remote proof or uses a service key. + - run: npm run test:cvl + action-smoke: runs-on: ubuntu-latest steps: diff --git a/CHANGELOG.md b/CHANGELOG.md index b47655a..9550222 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2,6 +2,13 @@ All notable changes to Counterflow will be documented in this file. +## Unreleased + +- Run original Foundry tests under Halmos instead of generating assertions from counterexamples; preserve exact signatures, setup, failure evidence and full-width witnesses. +- Fail closed on empty/malformed reports, missing tests, operational failures, timeouts, bounded loops and unsupported invariant sequences. JSON output and CLI exit codes distinguish violations from incomplete checks. +- Repair concrete Echidna actor tracking and CVL storage-hook exports; report partial coverage and reject vacuous unsigned non-negativity properties. +- Add real Forge/Halmos and generated-harness regressions, including typed counterexamples, multiple callers and deliberately corrupt accounting. + ## [0.6.1] — 2026-07-23 ### Added diff --git a/README.md b/README.md index 301b807..b70a2b6 100644 --- a/README.md +++ b/README.md @@ -32,7 +32,7 @@ Solidity + English invariants │ ▼ [Halmos bytecode] TRUSTED — EVM symbolic exec (9 scenarios, 3 PASS / 6 FAIL confirming exploits) - [Foundry fuzz+symb] fuzz → cex → halmos symbolic proof + [Foundry fuzz+symb] fuzz → original test under Halmos (bounded checks) [Echidna validation] harness generation from binding ``` @@ -154,3 +154,38 @@ CLI, translation prompts, validation, trusted Z3 core, Halmos tests, benchmark b - Richer Z3 models: compound interest - VS Code extension with inline binding review - Public leaderboard on GitHub Pages + +## Original-test fuzz and symbolic checks + +Run `counterflow fuzz-symb AccountingTest --test '^testFuzz_' --root /path/to/foundry-project --json`. +Forge runs the selected original tests. Each failed ordinary/fuzz test is then run +under Halmos with its original setup, argument types, operations and assertions. +No replacement Solidity assertion is fabricated from a counterexample. + +Exit codes: **0** for completed fuzzing with no failure (not a symbolic proof), +**3** whenever Forge observed a violation, **2** for operational or incomplete +results without a concrete violation. A Halmos pass cannot erase a Forge failure. +Stateful invariant sequences require a dedicated replay harness and are reported +unsupported. Empty results, skipped tests, solver timeouts, stuck paths, all-revert +execution and truncated loops cannot count as symbolic passes. Halmos passes are +scoped to its configured input/execution bounds. + +`gen-echidna` and `export-cvl` require `--contract Contract.sol`. Both report +covered and unsupported invariants and exit 2 on partial coverage. Unsigned +`>= 0` checks are deliberately unsupported: they cannot witness arithmetic wrap. +Echidna supports simple contracts without constructor/inheritance setup, scalar +ABI inputs and concrete solvency/share/backing/cap properties. Use the generated +wrapper allowlist; delegatecalls preserve caller/storage and track callers plus +address arguments. Actor-sum checks need manual review if other addresses are +credited or external callbacks change balances. CVL uses concrete storage hooks +and getter methods; it omits abstract transition shells without assertions. + +Validation: `npm test`, `npm run bench`, `npm run bytecode:expect`. +Set `COUNTERFLOW_REQUIRE_SYMBOLIC=1` to require installed Forge and Halmos for the +integration tests instead of allowing their absence to skip those tests. + +`npm run test:cvl` compiles and typechecks the generated TokenPool solvency +specification with Certora CLI 8.19.1, Java 21 and Solidity 0.8.24. Set +`COUNTERFLOW_SOLC` to the desired compiler executable if it is not `solc` on PATH. +This check uses `--compilation_steps_only`, needs no service credential and +submits no remote proof. Remote proof results remain a separate verification step. diff --git a/package.json b/package.json index 72844a7..1e3dda8 100644 --- a/package.json +++ b/package.json @@ -1,14 +1,15 @@ { "name": "@kryptosai/counterflow", "version": "0.6.1", - "description": "Prove the contract, or reveal the exploit — formal verification for Solidity and DeFi smart contracts. AI-translated invariants proved or refuted by Z3 SMT, with Halmos bytecode backstop and Foundry/Echidna export.", + "description": "Prove the contract, or reveal the exploit \u2014 formal verification for Solidity and DeFi smart contracts. AI-translated invariants proved or refuted by Z3 SMT, with Halmos bytecode backstop and Foundry/Echidna export.", "main": "src/verify.js", "bin": { "counterflow": "src/cli.js" }, "scripts": { "postinstall": "node -e 'if(process.env.CI||process.env.COUNTERFLOW_SKIP_POSTINSTALL||!process.stdout.isTTY)process.exit(0);console.log(\"Counterflow installed. Run counterflow doctor to check Python 3 + z3-solver setup.\")'", - "test": "node test/e2e.js", + "test": "node test/e2e.js && node --test test/*.test.js", + "test:cvl": "node test/cvl-compile.js", "bench": "node bench/run.js", "bytecode": "node src/cli.js bytecode HalmosTest", "bytecode:expect": "node src/cli.js bytecode --expect", @@ -27,7 +28,7 @@ "completeness": "node src/cli.js completeness", "mutate": "node src/cli.js mutate", "real-contracts": "node src/cli.js check examples/UniswapV2Swap.binding.json && node src/cli.js check examples/AaveLending.binding.json && node src/cli.js check examples/CompoundCToken.binding.json", - "cvl-export": "node src/cli.js export-cvl examples/TokenPool.binding.json -o examples/TokenPool.spec" + "cvl-export": "node src/cli.js export-cvl examples/TokenPool.binding.json --contract examples/TokenPool.sol -o examples/TokenPool.spec" }, "repository": { "type": "git", diff --git a/src/cli.js b/src/cli.js index 0f04e8d..de20332 100644 --- a/src/cli.js +++ b/src/cli.js @@ -37,10 +37,10 @@ USAGE counterflow bench [--json] counterflow audit counterflow audit-binding [--binding binding.json] [--json] - counterflow gen-echidna [--contract-name Name] [--output-dir path] + counterflow gen-echidna --contract Contract.sol [--contract-name Name] [--output-dir path] counterflow gen-foundry [--contract-name Name] [--output-dir path] - counterflow fuzz-symb [--test TestGlob] - counterflow export-cvl [-o output.spec] + counterflow fuzz-symb [--test TestRegex] [--root path] [--json] + counterflow export-cvl --contract Contract.sol [-o output.spec] counterflow kontrol [--test TestGlob] counterflow doctor counterflow leaderboard [--json] [--markdown] @@ -79,8 +79,13 @@ WHAT A VERDICT MEANS UNKNOWN = solver could not decide within limits.`; function arg(flag) { + // Returns the flag's value, or null when absent OR when the next token is + // another flag (missing value) — prevents `--test --json` swallowing --json. const i = process.argv.indexOf(flag); - return i === -1 ? null : process.argv[i + 1]; + if (i === -1) return null; + const value = process.argv[i + 1]; + if (value === undefined || value.startsWith('--')) return null; + return value; } async function main() { @@ -244,21 +249,45 @@ async function main() { const bindingPath = process.argv[3]; if (!bindingPath) { console.log(USAGE); process.exit(1); } const binding = JSON.parse(fs.readFileSync(bindingPath, 'utf-8')); - const contractName = arg('--contract-name') || binding.model || 'Contract'; + const contractPath = arg('--contract'); + if (!contractPath) { + console.error(`${C.red}gen-echidna requires --contract — the old default generated${C.reset}`); + console.error(`${C.red}uncompilable harnesses (contract name fell back to the model id).${C.reset}`); + process.exit(2); + } + const resolvedContract = path.resolve(contractPath); + if (!fs.existsSync(resolvedContract)) { + console.error(`${C.red}contract not found: ${contractPath}${C.reset}`); + process.exit(2); + } + const contractName = arg('--contract-name') || (() => { + const { parseContractInfo } = require('./solparse'); + const names = parseContractInfo(fs.readFileSync(resolvedContract, 'utf-8')).contractNames; + return names[0]; + })(); const outputDir = path.resolve(arg('--output-dir') || './echidna-output'); fs.mkdirSync(outputDir, { recursive: true }); const echidna = require('./echidna-gen'); - const sol = echidna.generateEchidnaTest(binding, contractName); - const yaml = echidna.generateEchidnaConfig(binding); - const solFile = path.join(outputDir, `Echidna${contractName}.sol`); + const importPath = path.relative(outputDir, resolvedContract).replace(/\\/g, '/'); + let out; + try { + out = echidna.generateEchidnaTest(binding, resolvedContract, contractName, importPath); + } catch (e) { + console.error(`${C.red}${e.message}${C.reset}`); + process.exit(2); + } + const yaml = echidna.generateEchidnaConfig(binding, out.filterFunctions || []); + const solFile = path.join(outputDir, out.fileName); const cfgFile = path.join(outputDir, 'echidna.yaml'); - fs.writeFileSync(solFile, sol); + fs.writeFileSync(solFile, out.sol); fs.writeFileSync(cfgFile, yaml); console.log(`${C.green}Echidna files generated:${C.reset}`); console.log(` ${solFile}`); console.log(` ${cfgFile}`); - process.exit(0); + for (const n of out.notes || []) console.log(` ${C.yellow}${n}${C.reset}`); + console.log(`Executable properties: ${out.covered.join(', ')}. Uncovered: ${out.skipped.length}.`); + process.exit(out.complete ? 0 : 2); } if (cmd === 'gen-foundry') { @@ -282,56 +311,40 @@ async function main() { } if (cmd === 'fuzz-symb') { - const { spawnSync } = require('child_process'); const contractName = process.argv[3]; - if (!contractName) { console.log(USAGE); process.exit(1); } - const testGlob = arg('--test') || '*'; - - const hasForge = spawnSync('forge', ['--version'], { encoding: 'utf-8' }).status === 0; - if (!hasForge) { - console.log(`${C.red}forge not installed: install Foundry (https://book.getfoundry.sh)${C.reset}`); - process.exit(2); - } - - const results = runFuzzThenSymbolic(contractName, testGlob); - if (!results.ok) { - console.log(`${C.red}${results.error}${C.reset}`); - process.exit(2); - } - - console.log(`${C.bold}Fuzz + Symbolic Results — ${contractName}${C.reset}`); - console.log(`\n${results.combinedSummary}`); - console.log(`\n${C.bold}Forge Fuzz:${C.reset}`); - console.log(` exit code: ${results.fuzzResults.exitCode}`); - console.log(` failures: ${results.fuzzResults.failures}`); - if (results.fuzzResults.failures > 0) { - for (const cex of results.fuzzResults.counterexamples) { - console.log(` ${C.red}${cex.testName}${C.reset}: ${cex.reason}`); + if (!contractName || contractName.startsWith('-')) { console.log(USAGE); process.exit(2); } + for (const flag of ['--test', '--root']) { + if (process.argv.includes(flag) && !arg(flag)) { + const error = `${flag} requires a value`; + console.log(json ? JSON.stringify({ ok: false, verdict: 'unknown', error }) : error); + process.exit(2); } } - - if (results.symbolicResults.length > 0) { - console.log(`\n${C.bold}Halmos Symbolic:${C.reset}`); - for (const sr of results.symbolicResults) { - const allPassed = sr.halmos.ok && sr.halmos.results.every(r => r.passed); - const mark = allPassed ? `${C.green}✓${C.reset}` : `${C.red}✗${C.reset}`; - console.log(` ${mark} ${sr.testName}`); - if (!allPassed) { - console.log(bytecodeReport(sr.halmos.results)); - } + const result = runFuzzThenSymbolic(contractName, arg('--test'), { + cwd: path.resolve(arg('--root') || process.cwd()), + }); + if (json) { + console.log(JSON.stringify(result, null, 2)); + } else if (!result.ok) { + console.error(`${C.red}${result.error}${C.reset}`); + } else { + console.log(result.combinedSummary); + for (const sr of result.symbolicResults) { + console.log(` ${sr.status.toUpperCase()} ${sr.cex.contractId}:${sr.cex.signature}`); + if (sr.halmos.error) console.log(` ${sr.halmos.error}`); + if (sr.halmos.results.length) console.log(bytecodeReport(sr.halmos.results)); } } - - if (json) console.log(JSON.stringify(results, null, 2)); - process.exit(results.fuzzResults.failures > 0 ? 3 : 0); + process.exit(result.verdict === 'violated' ? 3 : result.ok && result.complete ? 0 : 2); } if (cmd === 'export-cvl') { const bindingPath = process.argv[3]; if (!bindingPath) { console.log(USAGE); process.exit(1); } const out = arg('-o') || bindingPath.replace(/\.json$/, '.spec'); + const contractPath = arg('--contract'); const cvl = require('./cvl-export'); - const result = cvl.exportCvl(path.resolve(bindingPath)); + const result = cvl.exportCvl(path.resolve(bindingPath), contractPath ? path.resolve(contractPath) : null); if (!result.ok) { console.error(`${C.red}CVL export failed:${C.reset} ${result.error}`); process.exit(2); @@ -339,7 +352,9 @@ async function main() { fs.writeFileSync(out, result.cvl); console.log(`${C.green}CVL spec written to ${out}${C.reset}`); console.log(`${C.dim}Model: ${result.model}${C.reset}`); - process.exit(0); + console.log(`Exported: ${result.covered.join(', ')}. Uncovered: ${result.skipped.length}.`); + for (const item of result.skipped) console.log(` UNSUPPORTED ${item.invariant}: ${item.reason}`); + process.exit(result.complete ? 0 : 2); } if (cmd === 'kontrol') { diff --git a/src/cvl-export.js b/src/cvl-export.js index 71c245a..0799ec0 100644 --- a/src/cvl-export.js +++ b/src/cvl-export.js @@ -1,87 +1,16 @@ -const { GUARDS, EFFECTS, INVARIANTS } = require('./translate'); const { validateBinding } = require('./validate'); - -const EFFECT_TO_GHOST_UPDATE = { - bal_add_amt: 'ghost_sumBalances = ghost_sumBalances + amt;', - bal_sub_amt: 'ghost_sumBalances = ghost_sumBalances - amt;', - bal_add_amt_to: 'ghost_sumBalances = ghost_sumBalances + amt;', - bal_sub_amt_src: 'ghost_sumBalances = ghost_sumBalances - amt;', - set_bal_zero: 'ghost_sumBalances = ghost_sumBalances - balances[e.msg.sender];', - total_add_amt: 'ghost_sumTotal = ghost_sumTotal + amt;', - total_sub_amt: 'ghost_sumTotal = ghost_sumTotal - amt;', - shares_add_amt: 'ghost_sumShares = ghost_sumShares + amt;', - shares_sub_amt: 'ghost_sumShares = ghost_sumShares - amt;', - total_shares_add_amt: 'ghost_sumTotalShares = ghost_sumTotalShares + amt;', - total_shares_sub_amt: 'ghost_sumTotalShares = ghost_sumTotalShares - amt;', - allowance_sub_amt: 'ghost_sumAllowances = ghost_sumAllowances - amt;', -}; - -const GHOST_DECLARATIONS = [ - 'ghost mathint ghost_sumBalances { init_state assert ghost_sumBalances == 0; }', - 'ghost mathint ghost_sumTotal { init_state assert ghost_sumTotal == 0; }', - 'ghost mathint ghost_sumShares { init_state assert ghost_sumShares == 0; }', - 'ghost mathint ghost_sumTotalShares { init_state assert ghost_sumTotalShares == 0; }', - 'ghost mathint ghost_sumAllowances { init_state assert ghost_sumAllowances == 0; }', - 'ghost bool ghost_locked;', -]; - -const INVARIANT_CONDITIONS = { - nonneg_balance: 'ghost_sumBalances >= 0', - nonneg_shares: 'ghost_sumShares >= 0', - nonneg_allowance: 'ghost_sumAllowances >= 0', - nonneg_total: 'ghost_sumTotal >= 0', - nonneg_total_shares: 'ghost_sumTotalShares >= 0', - solvency: 'ghost_sumBalances == ghost_sumTotal', - shares_integrity: 'ghost_sumShares == ghost_sumTotalShares', - backing: 'ghost_sumTotal >= ghost_sumTotalShares', - supply_cap: 'ghost_sumTotal <= to_mathint(CAP())', - reentrancy_safe: 'ghost_locked == false', - nonneg_reserves: 'true', - nonneg_lp: 'true', - constant_product: 'true', - lp_integrity: 'true', - backing_amm: 'true', - nonneg_collateral: 'true', - nonneg_debt: 'true', - nonneg_total_collateral: 'true', - nonneg_total_debt: 'true', - collateral_integrity: 'true', - debt_integrity: 'true', - overcollateralized: 'true', - lending_solvency: 'true', - nonneg_staked: 'true', - nonneg_rewards: 'true', - stake_integrity: 'true', - reward_integrity: 'true', - staking_backing: 'true', - cross_contract_safe: 'ghost_locked == false', -}; - -const GUARD_TO_REQUIRE = { - amt_gt_0: 'amt > 0', - bal_ge_amt: 'balances[e.msg.sender] >= amt', - bal_gt_0: 'balances[e.msg.sender] > 0', - total_ge_amt: 'totalAssets >= amt', - sender_is_owner: 'e.msg.sender == owner', - bal_src_ge_amt: 'balances[src] >= amt', - allowance_ge_amt: 'allowances[src][e.msg.sender] >= amt', - shares_ge_amt: 'shares[e.msg.sender] >= amt', - total_shares_ge_amt: 'totalShares >= amt', - not_locked: 'ghost_locked == false', - balance_unchanged_before_call: 'true', - dx_gt_0: 'dx > 0', - dy_gt_0: 'dy > 0', - reserveX_ge_dx: 'reserveX >= dx', - reserveY_ge_dy: 'reserveY >= dy', - lp_ge_amt: 'lp >= amt', - collateral_ge_amt: 'collateral >= amt', - debt_ge_amt: 'debt >= amt', - healthy_position: 'true', - staked_ge_amt: 'staked >= amt', - rewards_ge_amt: 'rewards >= amt', - cross_not_in_progress: 'true', - cross_snapshot_match: 'true', -}; +const { parseContractInfo } = require('./solparse'); + +// ── Contract-aware CVL export ──────────────────────────────────────────── +// +// Previous versions of this exporter emitted `filtered { f -> true }` / +// `satisfy true` rules — tautologies that Certora "proves" vacuously. A +// generator that emits false assurance is worse than none: CVL now resolves +// the binding's abstract state against REAL contract identifiers (parsed from +// the Solidity source via --contract) and emits genuine Certora conditions +// using the documented patterns (storage hooks + ghosts for sums, parameterized +// direct-read invariants). Anything unresolvable is SKIPPED with a loud +// TODO comment — never silently satisfied. const INVARIANT_LABELS = { nonneg_balance: 'balances never negative', @@ -113,176 +42,207 @@ const INVARIANT_LABELS = { reward_integrity: 'reward integrity', staking_backing: 'staking backing', cross_contract_safe: 'cross-contract call safety', + nonneg_deposits: 'channel deposits never negative', + nonneg_spent: 'channel claims never negative', + nonneg_released: 'channel refunds never negative', + nonneg_remaining: 'channel unspent balance never negative', + channel_integrity: 'escrow holds deposits minus claims minus refunds', + channel_conservation: 'deposits equal claims + refunds + unspent', }; -function usesEffect(binding, prefixes) { - return (binding.functions || []).some((fn) => - (fn.effects || []).some((e) => prefixes.some((p) => e.startsWith(p))) - ); -} - -function computeRelevantGhosts(binding) { - const ghosts = []; +// ── Identifier resolution against parsed contract info ────────────────── - if (usesEffect(binding, ['bal_', 'set_bal_zero'])) { - ghosts.push('ghost mathint ghost_sumBalances { init_state assert ghost_sumBalances == 0; }'); - } - if (usesEffect(binding, ['total_'])) { - ghosts.push('ghost mathint ghost_sumTotal { init_state assert ghost_sumTotal == 0; }'); - } - if (usesEffect(binding, ['shares_'])) { - ghosts.push('ghost mathint ghost_sumShares { init_state assert ghost_sumShares == 0; }'); - } - if (usesEffect(binding, ['total_shares_'])) { - ghosts.push('ghost mathint ghost_sumTotalShares { init_state assert ghost_sumTotalShares == 0; }'); - } - if (usesEffect(binding, ['allowance_'])) { - ghosts.push('ghost mathint ghost_sumAllowances { init_state assert ghost_sumAllowances == 0; }'); - } - - const needsLocked = - (binding.functions || []).some((fn) => - (fn.guards || []).includes('not_locked') || - (fn.effects || []).includes('reentrancy_lock_acquire') - ); - if (needsLocked) { - ghosts.push('ghost bool ghost_locked { init_state assert ghost_locked == false; }'); - } - - return ghosts; +function pickUint(info, names) { + for (const n of names) if (info.uints.includes(n)) return n; + return null; } -function generateCvlRule(fn, idx) { - const name = fn.name || `function_${idx}`; - const guards = fn.guards || []; - const effects = fn.effects || []; - - const lines = []; - lines.push(` /// @notice Counterflow rule for function: ${name}`); - lines.push(` rule ${name}(method f) {`); - lines.push(' env e;'); - lines.push(' calldataarg args;'); - - if (guards.length > 0) { - lines.push(''); - lines.push(' // ---- pre-conditions (guards) ----'); - for (const g of guards) { - const req = GUARD_TO_REQUIRE[g]; - if (req && req !== 'true') { - lines.push(` require ${req};`); - } - } +function pickMap(info, keywords) { + for (const name of info.maps) { + if (keywords.some((k) => name.toLowerCase().includes(k))) return name; } + return null; +} - lines.push(''); - lines.push(` f(e, args);`); +function channelMap(info) { + const sm = info.structMaps.find((s) => + (info.structs[s.struct] || []).some((f) => f === 'remaining') || + (info.structs[s.struct] || []).some((f) => f === 'deposit')); + return sm || null; +} - if (effects.length > 0) { - lines.push(''); - lines.push(' // ---- post-conditions (effects) ----'); - for (const e of effects) { - const upd = EFFECT_TO_GHOST_UPDATE[e]; - if (upd) { - lines.push(` ${upd}`); - } - } +/** + * Resolve binding abstraction -> contract expression fragment. + * Returns { expr, ghostHooks } where expr uses real identifiers, or throws + * { unresolvable: [...] } when the contract cannot support the invariant. + */ +function resolveInvariant(binding, info, inv) { + const u = { balance: pickMap(info, ['balance']), allowance: pickMap(info, ['allow']), share: pickMap(info, ['share']) }; + const total = pickUint(info, ['totalAssets', 'totalSupply', 'total']); + const totalShares = pickUint(info, ['totalShares', 'shareSupply', 'shareTotal']); + const chanMap = channelMap(info); + const chanFields = chanMap ? (info.structs[chanMap.struct] || []) : []; + const field = (f) => chanMap && chanFields.includes(f) ? `${chanMap.name}[a].${f}` : null; + + if (inv.startsWith('nonneg_')) return { skipped: true, reason: 'Unsigned storage >= 0 cannot witness model-level underflow; use the original assertion/bytecode check' }; + switch (inv) { + case 'solvency': + if (!u.balance) throw new Error('balance mapping not found for sum hook'); + if (!total) throw new Error('uint total not found'); + return { + expr: null, + ghost: `ghost mathint ghost_sumBalances { init_state axiom ghost_sumBalances == 0; }`, + hook: `hook Sstore ${u.balance}[KEY address user] uint256 newBalance (uint256 oldBalance) {\n ghost_sumBalances = ghost_sumBalances + to_mathint(newBalance) - to_mathint(oldBalance);\n}`, + invariant: `invariant solvency() to_mathint(${total}()) == ghost_sumBalances;`, + getters: [total], + }; + case 'shares_integrity': + if (!u.share) throw new Error('shares mapping not found for sum hook'); + if (!totalShares) throw new Error('uint totalShares not found'); + return { + expr: null, + ghost: `ghost mathint ghost_sumShares { init_state axiom ghost_sumShares == 0; }`, + hook: `hook Sstore ${u.share}[KEY address user] uint256 newBalance (uint256 oldBalance) {\n ghost_sumShares = ghost_sumShares + to_mathint(newBalance) - to_mathint(oldBalance);\n}`, + invariant: `invariant shares_integrity() to_mathint(${totalShares}()) == ghost_sumShares;`, + getters: [totalShares], + }; + case 'backing': + if (!total || !totalShares) throw new Error('total/totalShares not found'); + return { expr: `to_mathint(${total}()) >= to_mathint(${totalShares}())`, params: '()', getters: [total, totalShares] }; + case 'supply_cap': + if (!total) throw new Error('uint total not found'); + return { expr: `to_mathint(${total}()) <= 1000000000`, params: '()', getters: [total] }; + case 'channel_integrity': + case 'channel_conservation': + return { + expr: null, + ghost: null, + hook: null, + invariant: null, + skipped: true, + reason: 'channel ghost sums require Certora hooks on struct fields — see README (Certora interop)', + }; + case 'reentrancy_safe': + return { expr: null, invariant: null, skipped: true, reason: 'reentrancy is modeled as ghost locks in the Z3 core, not in contract storage' }; + default: + return { + expr: null, invariant: null, skipped: true, + reason: `invariant '${inv}' has no Z3↔CVL mapping yet (see invariant_mapping for semantics)`, + }; } - - lines.push(' }'); - return lines.join('\n'); } -function generateCvlInvariant(inv) { - const cond = INVARIANT_CONDITIONS[inv]; - if (!cond) return null; - +function emitInvariantBlock(binding, info, inv) { const label = INVARIANT_LABELS[inv] || inv; - - const lines = []; - lines.push(` /// @notice Invariant: ${label}`); - lines.push(` invariant ${inv}(method f)`); - lines.push(' filtered { f -> true }'); - lines.push(' {'); - lines.push(' preserve {'); - if (cond === 'true') { - lines.push(` // ${inv}: placeholder — extend with model-specific condition`); - lines.push(' satisfy true;'); - } else { - lines.push(` satisfy ${cond};`); + try { + const r = resolveInvariant(binding, info, inv); + if (r.skipped) { + return `// TODO [${inv}]: ${r.reason}`; + } + if (r.invariant) { + return `/// ${label}\n${r.invariant}`; + } + if (r.expr) { + return `/// ${label}\ninvariant ${inv}${r.params} ${r.expr};`; + } + return null; + } catch (e) { + return `// TODO [${inv}]: could not resolve against contract source — ${e.message}`; } - lines.push(' }'); - lines.push(' }'); - - return lines.join('\n'); } -function generateCvl(binding) { +function generateCvl(binding, contractSource) { + if (!contractSource) throw new Error('CVL export requires the concrete contract source'); const model = binding.model || 'unknown'; - const functions = binding.functions || []; const invariants = binding.invariants || []; - - const ghosts = computeRelevantGhosts(binding); + const info = contractSource != null ? parseContractInfo(contractSource) : { uints: [], maps: [], structMaps: [], structs: {} }; const timestamp = new Date().toISOString(); const out = []; - out.push(`/// CVL specification generated from Counterflow binding`); + out.push(`/// CVL specification generated from a Counterflow binding`); out.push(`/// Model: ${model}`); out.push(`/// Generated: ${timestamp}`); - out.push(`/// Source: Counterflow v0.3.0 — https://github.com/KryptosAI/counterflow`); + out.push(`/// NOTE: abstract identifiers are resolved against the contract source`); + out.push(`/// (counterflow export-cvl --contract ) so the`); + out.push(`/// emitted rules are real properties. Unresolvable invariants are emitted as`); + out.push(`/// TODO comments, never as tautologies.`); out.push(''); - out.push('// ---- ghost variable declarations ----'); - if (ghosts.length > 0) { - for (const g of ghosts) { - out.push(g); - } - } else { - out.push('// (no ghost variables needed — binding has no tracked effects)'); + const getters = new Set(); + for (const inv of invariants) { + try { for (const getter of resolveInvariant(binding, info, inv).getters || []) getters.add(getter); } catch {} + } + if (getters.size) { + out.push('methods {'); + for (const getter of getters) out.push(` function ${getter}() external returns (uint256) envfree;`); + out.push('}', ''); + } + const blocks = invariants.map((inv) => emitInvariantBlock(binding, info, inv)).filter(Boolean); + const ghostLines = new Set(); + const hookLines = []; + for (const inv of invariants) { + try { + const r = resolveInvariant(binding, info, inv); + if (r.ghost) ghostLines.add(r.ghost); + if (r.hook) hookLines.push(r.hook); + } catch { /* skipped */ } } - out.push(''); - if (functions.length > 0) { - out.push('// ---- function transition rules ----'); + if (ghostLines.size > 0) { + out.push('// ---- ghost variables (sum tracking, Certora storage hooks) ----'); + for (const g of ghostLines) out.push(g); out.push(''); - for (let i = 0; i < functions.length; i++) { - out.push(generateCvlRule(functions[i], i)); - if (i < functions.length - 1) out.push(''); - } + } + if (hookLines.length > 0) { + out.push('// ---- storage hooks ----'); + for (const h of hookLines) out.push(h); out.push(''); } - if (invariants.length > 0) { - out.push('// ---- invariant rules ----'); - out.push(''); - for (const inv of invariants) { - const block = generateCvlInvariant(inv); - if (block) { - out.push(block); - out.push(''); - } - } + const emitted = blocks.filter((b) => !b.startsWith('// TODO')); + out.push('// ---- invariant rules ----'); + out.push(''); + if (emitted.length === 0) { + out.push('// No invariants could be resolved against the contract source.'); + out.push('// Run with --contract so the exporter can map the'); + out.push('// binding abstraction (balances, totalAssets, channel fields, ...)'); + out.push('// to the contract\'s real identifiers.'); } + for (const b of blocks) out.push(b + '\n'); return out.join('\n') + '\n'; } -function exportCvl(bindingPath) { +function exportCvl(bindingPath, contractPath) { const fs = require('fs'); const raw = fs.readFileSync(bindingPath, 'utf-8'); let binding; try { binding = JSON.parse(raw); - } catch { - return { ok: false, error: `invalid JSON in binding file: ${bindingPath}` }; + } catch (e) { + return { ok: false, error: `binding is not valid JSON: ${e.message}` }; } - const v = validateBinding(binding); if (!v.valid) { - return { ok: false, error: `binding validation failed: ${v.errors.join(', ')}` }; + return { ok: false, error: 'binding failed validation: ' + v.errors.join('; ') }; } - - const cvl = generateCvl(binding); - return { ok: true, cvl, model: binding.model }; + if (!contractPath) return { ok: false, error: 'export-cvl requires --contract ' }; + try { + const source = fs.readFileSync(contractPath, 'utf8'); + const info = parseContractInfo(source); + if (info.contractNames.length !== 1) return { ok: false, error: 'Provide one concrete contract for identifier resolution' }; + const covered = [], skipped = []; + for (const invariant of binding.invariants) { + try { + const r = resolveInvariant(binding, info, invariant); + if (r.skipped) skipped.push({ invariant, reason: r.reason }); + else covered.push(invariant); + } catch (e) { skipped.push({ invariant, reason: e.message }); } + } + if (!covered.length) return { ok: false, error: 'No concrete invariants could be exported', covered, skipped }; + return { ok: true, cvl: generateCvl(binding, source), model: binding.model, + complete: skipped.length === 0, covered, skipped }; + } catch (e) { return { ok: false, error: e.message }; } } -module.exports = { generateCvl, exportCvl, computeRelevantGhosts }; +module.exports = { exportCvl, generateCvl, parseContractInfo, resolveInvariant }; diff --git a/src/echidna-gen.js b/src/echidna-gen.js index e8d8cd0..cb98c89 100644 --- a/src/echidna-gen.js +++ b/src/echidna-gen.js @@ -1,48 +1,95 @@ -const INVARIANT_PROPS = { - nonneg_balance: `return balances[address(this)] <= totalAssets || balances[address(this)] == 0; // uint cannot be negative; check solvency per-actor`, - nonneg_total: `return totalAssets >= 0; // always true for uint256; placeholder`, - solvency: `return balances[address(this)] <= totalAssets; // per-actor solvency check`, - backing: `return totalAssets >= totalShares; // every share backed`, - supply_cap: `return totalAssets <= 1000000000; // supply cap`, - nonneg_shares: `return shares[address(this)] <= totalShares || shares[address(this)] == 0;`, - nonneg_allowance: `return true; // allowance checked via transferFrom guard; static here`, - nonneg_total_shares: `return totalShares >= 0; // always true for uint256; placeholder`, - shares_integrity: `return true; // requires ghost-var tracking (not in contract); placeholder`, - reentrancy_safe: `return true; // cannot test reentrancy with fuzzing; placeholder`, -}; +const fs = require('fs'); +const { parseContractInfo, parseFunctions, codeOnly } = require('./solparse'); +const { validateBinding } = require('./validate'); -function generateEchidnaTest(binding, contractName) { - const name = contractName || binding.model || 'Contract'; - const invs = binding.invariants || []; - const fns = (binding.functions || []).map(f => f.name); - - const props = invs.map((inv, i) => { - const body = INVARIANT_PROPS[inv] || `return true; // invariant ${inv} not instrumented`; - return ` function echidna_${inv}_${i}() public view returns (bool) { ${body} }`; - }).join('\n\n'); - - const filterComment = fns.length - ? `// filterFunctions: [${fns.map(f => `"${f}(uint256)"`).join(', ')}]` - : ''; - - return `// SPDX-License-Identifier: MIT +// Concrete observed-storage checks. Delegatecalls preserve the original caller +// and storage; a wrapper allowlist ensures actor tracking cannot be bypassed. +function generateEchidnaTest(binding, contractPath, contractName, importPath) { + const valid = validateBinding(binding); + if (!valid.valid) throw new Error(valid.errors.join('; ')); + if (!contractPath || !contractName) throw new Error('gen-echidna requires --contract '); + const source = fs.readFileSync(contractPath, 'utf8'), code = codeOnly(source); + const info = parseContractInfo(source); + if (info.contractNames.length !== 1 || info.contractNames[0] !== contractName) throw new Error('Provide one concrete contract; multiple-contract sources need an explicit harness'); + if (/\bconstructor\s*\(/.test(code) || /\bcontract\s+\w+\s+is\b/.test(code)) throw new Error('Constructor/inheritance setup needs an explicit harness'); + if (!importPath || /["\n\r]/.test(importPath)) throw new Error('Invalid Solidity import path'); + const functions = parseFunctions(source); + const wrappers = [], filterFunctions = [], notes = [], skipped = [], covered = [], properties = []; + const pick = names => names.find(n => info.uints.includes(n)); + const pickMap = names => names.find(n => info.publicMaps.includes(n)); + const total = pick(['totalAssets', 'totalSupply', 'total']), shares = pick(['totalShares', 'shareSupply']); + const balances = pickMap(['balances', 'balance']), shareMap = pickMap(['shares', 'shareBalances']); + for (const fn of binding.functions) { + const matches = functions.filter(f => f.name === fn.name); + if (matches.length !== 1) throw new Error(`Cannot resolve unique function ${fn.name}; overloads need an explicit harness`); + const target = matches[0]; + if (!['public', 'external'].includes(target.visibility)) throw new Error(`Function ${fn.name} must be public or external`); + const params = target.args ? target.args.split(',').map((part, i) => { + const m = part.trim().match(/^(address|bool|u?int(?:8|16|24|32|40|48|56|64|72|80|88|96|104|112|120|128|136|144|152|160|168|176|184|192|200|208|216|224|232|240|248|256)?|bytes(?:[1-9]|[12]\d|3[0-2]))(?:\s+(\w+))?$/); + if (!m) throw new Error(`Unsupported ABI parameter in ${fn.name}: ${part}`); + return { type: m[1] === 'uint' ? 'uint256' : m[1] === 'int' ? 'int256' : m[1], name: m[2] || `arg${i}` }; + }) : []; + const types = params.map(p => p.type).join(','), names = params.map(p => p.name).join(', '); + filterFunctions.push(`Echidna${contractName}.cf_${fn.name}(${types})`); + wrappers.push(` function cf_${fn.name}(${params.map(p => `${p.type} ${p.name}`).join(', ')}) public { + _cf_track(msg.sender); +${params.filter(p => p.type === 'address').map(p => ` _cf_track(${p.name});`).join('\n')} + (bool success, bytes memory reason) = address(this).delegatecall( + abi.encodeWithSignature("${fn.name}(${types})"${names ? ', ' + names : ''})); + if (!success) { assembly { revert(add(reason, 32), mload(reason)) } } + }`); + } + for (const inv of binding.invariants) { + let body; + if (inv === 'solvency' && balances && total) body = sumProperty(balances, total); + else if (inv === 'shares_integrity' && shareMap && shares) body = sumProperty(shareMap, shares); + else if (inv === 'backing' && total && shares) body = ` return ${total} >= ${shares};`; + else if (inv === 'supply_cap' && total) body = ` return ${total} <= 1000000000;`; + if (body) { + covered.push(inv); + properties.push(` function echidna_${inv}() public view returns (bool) {\n${body}\n }`); + } else { + const reason = inv.startsWith('nonneg_') ? 'Unsigned storage >= 0 is tautological and does not test arithmetic underflow' : 'No concrete storage mapping is implemented for this invariant'; + skipped.push({ invariant: inv, reason }); notes.push(`UNSUPPORTED ${inv}: ${reason}`); + } + } + if (!covered.length) throw new Error(`No executable properties could be generated. ${notes.join('; ')}`); + notes.push('Actor-sum scope: caller and address arguments observed in wrapped calls; review contracts that credit other addresses or use external callbacks'); + return { fileName: `Echidna${contractName}.sol`, filterFunctions, covered, skipped, complete: skipped.length === 0, notes, + sol: `// SPDX-License-Identifier: MIT pragma solidity ^0.8.20; - -import "../src/${name}.sol"; - -contract Echidna${name} is ${name} { -${props} +import "${importPath}"; +// Use the accompanying wrapper allowlist. Actor sums cover callers and address arguments. +// This harness does not prove the binding's complete vocabulary. +${skipped.map(s => `// UNSUPPORTED ${s.invariant}: ${s.reason}`).join('\n')} +contract Echidna${contractName} is ${contractName} { + address[] internal _cf_actors; + mapping(address => bool) internal _cf_seen; + function _cf_track(address who) internal { + if (!_cf_seen[who]) { _cf_seen[who] = true; _cf_actors.push(who); } + } +${wrappers.join('\n\n')} +${properties.join('\n\n')} } -${filterComment}`; +` }; } - -function generateEchidnaConfig(binding) { - const fns = (binding.functions || []).map(f => f.name); +function sumProperty(mapping, total) { + return ` uint256 sum; + for (uint256 i; i < _cf_actors.length; i++) { + uint256 balance = this.${mapping}(_cf_actors[i]); + if (balance > type(uint256).max - sum) return false; + sum += balance; + } + return sum == ${total};`; +} +function generateEchidnaConfig(binding, filterFunctions) { + if (!filterFunctions?.length) throw new Error('An explicit wrapper allowlist is required'); return `testLimit: 50000 seqLen: 100 deployer: "0x10000" sender: ["0x10000", "0x20000", "0x30000"] -${fns.length ? 'filterFunctions: [' + fns.map(f => `"${f}(uint256)"`).join(', ') + ']' : ''}`; +filterBlacklist: false +filterFunctions: ${JSON.stringify(filterFunctions)} +`; } - module.exports = { generateEchidnaTest, generateEchidnaConfig }; diff --git a/src/forge-symb.js b/src/forge-symb.js index 0d91f95..939d016 100644 --- a/src/forge-symb.js +++ b/src/forge-symb.js @@ -1,38 +1,7 @@ const { spawnSync } = require('child_process'); -const fs = require('fs'); const path = require('path'); const { runHalmos } = require('./halmos-runner'); -const HALMOS_DIR = path.join(__dirname, '..', 'halmos'); -const HALMOS_TEST_DIR = path.join(HALMOS_DIR, 'test'); - -function isForgeInstalled() { - try { - const r = spawnSync('forge', ['--version'], { encoding: 'utf-8', timeout: 10000 }); - return r.status === 0; - } catch { - return false; - } -} - -function sanitizeName(name) { - return name - .replace(/[^a-zA-Z0-9_]/g, '_') - .replace(/^_+/, '') - .replace(/_+/g, '_') - .replace(/(?:^|_)([a-z])/g, (_, c) => c.toUpperCase()); -} - -function extractContractName(contractSource) { - if (!contractSource || contractSource.trim().length === 0) { - return null; - } - if (contractSource.indexOf('\n') === -1 && contractSource.indexOf(' ') === -1) { - return contractSource; - } - const m = contractSource.match(/contract\s+(\w+)/); - return m ? m[1] : null; -} /** * Parse forge -vvv test output and extract counterexamples from failing tests. @@ -164,195 +133,119 @@ function parseArgs(argStr) { } /** - * Generate a Halmos symbolic test Solidity file that starts from the concrete - * counterexample values and lets Halmos symbolically explore all branches from there. + * Foundry JSON is the authority for the test identity and outcome. Counterexample + * arguments stay opaque: decoding them into invented uint256 parameters loses + * signed/address/tuple types, and cannot reconstruct the original test setup. */ -function generateSymbolicFromCex(testName, cex, contractSource) { - const basename = sanitizeName(testName || 'test'); - const contractName = extractContractName(contractSource) || 'ContractUnderTest'; - const safeName = `Symbolic${basename}Test`; - const args = cex && cex.args ? cex.args : []; - - const isNamed = args && typeof args === 'object' && !Array.isArray(args) && args.named; - const argEntries = isNamed ? Object.entries(args.named) : (Array.isArray(args) ? args : []); - - const paramDecls = []; - const assumeStmts = []; - const knownParams = []; - - if (isNamed) { - for (const [name, val] of argEntries) { - paramDecls.push(`uint256 ${name}`); - assumeStmts.push(` vm.assume(${name} == ${val});`); - knownParams.push(name); - } - } else { - for (let i = 0; i < argEntries.length; i++) { - const pname = `arg${i}`; - paramDecls.push(`uint256 ${pname}`); - assumeStmts.push(` vm.assume(${pname} == ${argEntries[i]});`); - knownParams.push(pname); - } +function parseForgeResults(output) { + const suites = JSON.parse(output); + if (!suites || Array.isArray(suites) || typeof suites !== 'object') { + throw new Error('Forge did not return a test-suite object'); } - - const paramsStr = paramDecls.join(', '); - - return `// SPDX-License-Identifier: MIT -// Auto-generated by Counterflow: fuzz-to-symbolic bridge. -// Counterexample from forge fuzz: ${testName} -pragma solidity ^0.8.20; - -import {${contractName}} from "../src/${contractName}.sol"; - -contract ${safeName} { - function check_${basename}_symbolic(${paramsStr}) public { -${assumeStmts.join('\n')} - - ${contractName} instance = new ${contractName}(); - - // --- Replay the operation that triggered the violation --- - // FIXME: apply the sequence of calls that led to the counterexample, - // using the pinned parameter values above. - // - // Example: - // instance.deposit(arg0); - // instance.withdraw(arg1); - - // --- Assert the property under test --- - // FIXME: replace the line below with the actual invariant assertion. - // Halmos will symbolically explore all execution branches from this point. - assert(true); + const tests = []; + for (const [contractId, suite] of Object.entries(suites)) { + if (!suite || !suite.test_results || typeof suite.test_results !== 'object') { + throw new Error(`Missing test results for ${contractId}`); } - - function vm_assume(bool c) internal pure { - if (!c) { - assembly { - revert(0, 0) - } - } + const separator = contractId.lastIndexOf(':'); + if (separator < 0) throw new Error(`Invalid Forge contract identity: ${contractId}`); + for (const [signature, result] of Object.entries(suite.test_results)) { + if (!['Success', 'Failure', 'Skipped'].includes(result.status)) { + throw new Error(`Unknown Forge status for ${signature}: ${result.status}`); + } + tests.push({ + contractId, + contractName: contractId.slice(separator + 1), + testName: signature.split('(')[0], + signature, + status: result.status, + reason: result.reason, + counterexample: result.counterexample, + kind: result.kind, + }); } -} -`; -} - -/** - * Write a generated symbolic test file into the halmos test directory and - * invoke Halmos on it. Uses runHalmos from halmos-runner.js — no duplication. - */ -function runHalmosSymbolic(testFile) { - const content = fs.readFileSync(testFile, 'utf-8'); - const basename = path.basename(testFile); - - const contractMatch = content.match(/contract\s+(\w+)\s*(?:is|\{)/); - if (!contractMatch) { - return { ok: false, error: `Could not extract contract name from ${testFile}` }; } - const contractName = contractMatch[1]; - - const dest = path.join(HALMOS_TEST_DIR, basename); - fs.writeFileSync(dest, content, 'utf-8'); + return tests; +} - return runHalmos(contractName); +function escapeRegex(value) { + return value.replace(/[.*+?^${}()|[\]\\]/g, '\\$&'); } /** - * Fuzz-to-symbolic bridge entry point. - * - * 1. Runs forge fuzz tests. - * 2. Parses output for failed tests and extracts counterexamples. - * 3. For each failure, generates a Halmos symbolic test pinning the cex values. - * 4. Runs Halmos on each generated test. - * 5. Returns combined results. + * The original compiled Foundry test IS the symbolic harness. Halmos invokes + * its constructor/setUp and explores its real test function with symbolic ABI + * inputs. No replacement Solidity or guessed assertion is generated. * - * @param {string} contractName - The test contract name for --match-contract - * @param {string} testGlob - The test glob for --match-test - * @param {object} [options] - { contractSource, cwd } - * @returns Combined fuzz + symbolic results. + * Stateful invariant sequences and lifecycle failures require different replay + * semantics; they are retained as failures and reported as unsupported. */ function runFuzzThenSymbolic(contractName, testGlob, options = {}) { - if (!isForgeInstalled()) { - return { - ok: false, - error: 'forge is not installed. Install Foundry from https://getfoundry.sh', - fuzzResults: [], - symbolicResults: [], - }; + const cwd = path.resolve(options.cwd || process.cwd()); + const run = options.spawnSync || spawnSync; + const symbolic = options.runHalmos || runHalmos; + const empty = { fuzzResults: null, symbolicResults: [], complete: false, verdict: 'unknown' }; + if (!contractName || !/^[A-Za-z_$][\w$]*$/.test(contractName)) { + return { ...empty, ok: false, error: 'Provide an exact Foundry test contract name' }; } - - const cwd = options.cwd || HALMOS_DIR; - - const forgeArgs = [ - 'test', - '--match-contract', contractName, - '--match-test', testGlob, - '-vvv', - ]; - - const fuzzRun = spawnSync('forge', forgeArgs, { - cwd, - encoding: 'utf-8', - maxBuffer: 50 * 1024 * 1024, - timeout: 300000, + const forgeArgs = ['test', '--json', '--match-contract', `^${escapeRegex(contractName)}$`]; + if (testGlob && testGlob !== '*') forgeArgs.push('--match-test', testGlob); + const fuzzRun = run('forge', forgeArgs, { + cwd, encoding: 'utf-8', maxBuffer: 50 * 1024 * 1024, + timeout: options.timeoutMs || 300000, }); - - const output = (fuzzRun.stdout || '') + '\n' + (fuzzRun.stderr || ''); - const counterexamples = extractCounterexampleFromForge(output); - + if (fuzzRun.error || fuzzRun.signal || ![0, 1].includes(fuzzRun.status)) { + return { ...empty, ok: false, error: `Forge execution failed: ${fuzzRun.error?.message || fuzzRun.signal || fuzzRun.stderr || fuzzRun.status}` }; + } + let tests; + try { tests = parseForgeResults(fuzzRun.stdout || ''); } + catch (e) { + return { ...empty, ok: false, error: `Forge results unavailable: ${e.message}. ${(fuzzRun.stderr || '').slice(-2000)}` }; + } + const executed = tests.filter(t => t.status !== 'Skipped'); + const failures = tests.filter(t => t.status === 'Failure'); const fuzzResults = { - exitCode: fuzzRun.status, - passing: fuzzRun.status === 0 && counterexamples.length === 0, - failures: counterexamples.length, - counterexamples, - rawOutput: output, + exitCode: fuzzRun.status, passing: fuzzRun.status === 0 && failures.length === 0 && executed.length > 0, + tests: tests.length, executed: executed.length, skipped: tests.length - executed.length, + failures: failures.length, counterexamples: failures, }; - - const symbolicResults = []; - for (const cex of counterexamples) { - const source = options.contractSource || ''; - const genSrc = generateSymbolicFromCex(cex.testName, cex, source); - const filename = `Symbolic${sanitizeName(cex.testName)}Test.t.sol`; - const tmpFile = path.join(HALMOS_TEST_DIR, filename); - fs.writeFileSync(tmpFile, genSrc, 'utf-8'); - - const halmosResult = runHalmosSymbolic(tmpFile); - symbolicResults.push({ - testName: cex.testName, - cex, - halmos: halmosResult, - }); - - // Clean up generated file to avoid polluting the test directory - try { fs.unlinkSync(tmpFile); } catch (_) { /* best effort */ } + if (!executed.length || (fuzzRun.status !== 0 && !failures.length) || (fuzzRun.status === 0 && failures.length)) { + return { ...empty, fuzzResults, ok: false, error: 'Forge returned no executed tests or inconsistent failure/exit status' }; } - const allSymbolicPassed = symbolicResults.length > 0 && - symbolicResults.every(sr => sr.halmos.ok && sr.halmos.results.every(r => r.passed)); - - let combinedSummary; - if (!counterexamples.length) { - combinedSummary = `Fuzz: all tests passed — no counterexamples to promote.`; - } else if (allSymbolicPassed) { - combinedSummary = `Fuzz: ${counterexamples.length} failure(s) found and promoted to symbolic. ` + - `Symbolic: all passed (no deeper violations found).`; - } else { - const symFailCount = symbolicResults.filter( - sr => !sr.halmos.ok || sr.halmos.results.some(r => !r.passed) - ).length; - combinedSummary = `Fuzz: ${counterexamples.length} failure(s) promoted to symbolic. ` + - `Symbolic: ${symFailCount} test(s) found additional violations.`; - } + const symbolicResults = failures.map(cex => { + const unsupported = cex.counterexample?.Sequence || cex.kind?.Invariant || + cex.testName.startsWith('invariant') || ['setUp', 'afterInvariant', 'beforeTestSetup'].includes(cex.testName); + if (unsupported) { + return { testName: cex.testName, cex, status: 'unsupported', + halmos: { ok: false, results: [], error: 'Stateful sequences and lifecycle failures need an explicit replay harness; the Forge failure remains valid' } }; + } + const halmos = symbolic(cex.contractName, { + cwd, matchTest: `^${escapeRegex(cex.signature)}$`, + expectedTests: [{ contractId: cex.contractId, signature: cex.signature }], + timeoutMs: options.timeoutMs || 300000, + panicErrorCodes: '*', + }); + const reproduced = halmos.ok && halmos.results.length === 1 && halmos.results[0].status === 'violated'; + return { testName: cex.testName, cex, halmos, + status: reproduced ? 'reproduced' : halmos.ok ? 'inconsistent' : 'unknown' }; + }); + const complete = symbolicResults.every(r => r.status === 'reproduced'); + const reproduced = symbolicResults.filter(r => r.status === 'reproduced').length; + const combinedSummary = failures.length + ? `Forge found ${failures.length} failure(s). Halmos reproduced ${reproduced} using the original tests; ${failures.length - reproduced} remain inconclusive or unsupported. Fuzz failures are never cleared by a symbolic pass.` + : `Forge passed ${executed.length} test(s), with ${tests.length - executed.length} skipped. No counterexamples to promote; this is not a symbolic proof.`; + return { ok: true, complete, verdict: failures.length ? 'violated' : 'fuzz_passed', + fuzzResults, symbolicResults, combinedSummary }; +} - return { - ok: true, - fuzzResults, - symbolicResults, - combinedSummary, - }; +// A concrete argument list alone is insufficient to reconstruct a property. +// Retain an explicit diagnostic for callers of the old, unsound generator API. +function generateSymbolicFromCex() { + throw new Error('Use runFuzzThenSymbolic with the original Foundry project; a counterexample alone cannot reconstruct its test or assertion'); } module.exports = { - runFuzzThenSymbolic, - extractCounterexampleFromForge, + runFuzzThenSymbolic, parseForgeResults, extractCounterexampleFromForge, generateSymbolicFromCex, - runHalmosSymbolic, }; diff --git a/src/halmos-runner.js b/src/halmos-runner.js index 3814032..6b2414b 100644 --- a/src/halmos-runner.js +++ b/src/halmos-runner.js @@ -1,6 +1,7 @@ const { spawnSync } = require('child_process'); const fs = require('fs'); const path = require('path'); +const os = require('os'); const HALMOS_DIR = path.join(__dirname, '..', 'halmos'); @@ -40,19 +41,6 @@ function pickPythonWithHalmos() { return null; } -function pickPythonInner() { - const candidates = [ - process.env.COUNTERFLOW_PYTHON, - path.join(__dirname, '..', '.venv', 'bin', 'python'), - 'python3', - ].filter(Boolean); - for (const p of candidates) { - const r = spawnSync(p, ['-c', 'import z3'], { encoding: 'utf-8' }); - if (r.status === 0) return p; - } - return null; -} - function formatHalmosError() { const venvPath = path.join(__dirname, '..', '.venv', 'bin', 'halmos'); const venvExists = fs.existsSync(venvPath); @@ -71,55 +59,97 @@ function formatHalmosError() { return lines.join('\n'); } +/** Interpret the structured Halmos result, including incomplete explorations. */ +function parseHalmosJson(raw, output = '') { + const report = JSON.parse(raw); + if (!report || !report.test_results || Array.isArray(report.test_results)) { + throw new Error('Halmos returned no structured test results'); + } + const printed = parseHalmosOutput(output); + const results = []; + for (const [contractId, tests] of Object.entries(report.test_results)) { + if (!Array.isArray(tests)) throw new Error(`Invalid Halmos tests for ${contractId}`); + for (const t of tests) { + if (typeof t.name !== 'string' || !Number.isInteger(t.exitcode)) { + throw new Error('Malformed Halmos test result'); + } + const hasWitness = Number.isInteger(t.num_models) && t.num_models > 0 && Array.isArray(t.models) && + t.models.some(m => m?.is_valid === true); + const validPaths = Array.isArray(t.num_paths) && t.num_paths.length === 3 && + t.num_paths.every(n => Number.isInteger(n) && n >= 0) && + t.num_paths[0] >= t.num_paths[1] + t.num_paths[2]; + const fullyExplored = validPaths && t.num_paths[1] > 0 && + t.num_paths[2] === 0 && t.num_bounded_loops === 0; + const status = t.exitcode === 1 && hasWitness ? 'violated' : + t.exitcode === 0 && fullyExplored ? 'passed' : 'unknown'; + const textResult = printed.find(r => r.name === t.name && r.contractId === contractId); + results.push({ name: t.name, contractId, status, passed: status === 'passed', + counterexample: status === 'violated' + ? textResult?.counterexample || { raw } : null, + exitCode: t.exitcode, paths: t.num_paths, boundedLoops: t.num_bounded_loops, + }); + } + } + if (!results.length) throw new Error('Halmos executed zero tests'); + return { report, results }; +} + /** - * Run Halmos symbolic tests for a specific test contract (or all if '*'). - * Returns { ok, results: [{ name, passed, counterexample }] }. + * Run the original compiled tests. JSON and process status are both required; + * empty results, all-reverting paths, truncated loops, timeouts and unsupported + * execution are never accepted as passing verification. */ -function runHalmos(testGlob) { - // '*' (or empty) means "all test contracts" — halmos's --contract filter is a - // regex, so a literal '*' is an invalid pattern and yields zero results. - // Omit the flag entirely instead (also picks up future test contracts). - const contractArgs = (testGlob && testGlob !== '*') ? ['--contract', testGlob] : []; - +function runHalmos(testContract, options = {}) { + const cwd = path.resolve(options.cwd || HALMOS_DIR); const halmosBin = pickHalmos(); - if (halmosBin) { - const build = spawnSync('forge', ['build'], { cwd: HALMOS_DIR, encoding: 'utf-8' }); - if (build.status !== 0) { - return { ok: false, error: `forge build failed:\n${build.stderr}` }; - } - - const res = spawnSync(halmosBin, ['--root', HALMOS_DIR, ...contractArgs], { - cwd: HALMOS_DIR, - encoding: 'utf-8', + const python = halmosBin ? null : pickPythonWithHalmos(); + if (!halmosBin && !python) return { ok: false, results: [], error: formatHalmosError() }; + const temp = fs.mkdtempSync(path.join(os.tmpdir(), 'counterflow-halmos-')); + const resultFile = path.join(temp, 'result.json'); + const args = halmosBin ? [] : ['-m', 'halmos']; + args.push('--root', cwd, '--json-output', resultFile, '--solver', 'z3', + '--solver-timeout-assertion', '30s', '--solver-threads', '2'); + if (testContract && testContract !== '*') args.push('--contract', testContract); + if (options.matchTest) args.push('--match-test', options.matchTest); + if (options.panicErrorCodes) args.push('--panic-error-codes', options.panicErrorCodes); + try { + const proc = spawnSync(halmosBin || python, args, { + cwd, encoding: 'utf-8', timeout: options.timeoutMs || 300000, maxBuffer: 50 * 1024 * 1024, }); - - const combined = (res.stdout || '') + '\n' + (res.stderr || ''); - const results = parseHalmosOutput(combined); - - return { ok: true, results }; - } - - const python = pickPythonWithHalmos(); - if (python) { - const build = spawnSync('forge', ['build'], { cwd: HALMOS_DIR, encoding: 'utf-8' }); - if (build.status !== 0) { - return { ok: false, error: `forge build failed:\n${build.stderr}` }; + const output = (proc.stdout || '') + '\n' + (proc.stderr || ''); + if (proc.error || proc.signal || ![0, 1].includes(proc.status)) { + return { ok: false, results: [], error: `Halmos execution failed: ${proc.error?.message || proc.signal || proc.status}`, output }; } - - const res = spawnSync(python, ['-m', 'halmos', '--root', HALMOS_DIR, ...contractArgs], { - cwd: HALMOS_DIR, - encoding: 'utf-8', - maxBuffer: 50 * 1024 * 1024, - }); - - const combined = (res.stdout || '') + '\n' + (res.stderr || ''); - const results = parseHalmosOutput(combined); - - return { ok: true, results }; + if (!fs.existsSync(resultFile)) return { ok: false, results: [], error: 'Halmos produced no result file (build or execution failure)', output }; + const { report, results } = parseHalmosJson(fs.readFileSync(resultFile, 'utf8'), output); + if (report.exitcode !== proc.status || + (proc.status === 0 && results.some(r => r.exitCode !== 0)) || + (proc.status === 1 && results.every(r => r.exitCode === 0))) { + return { ok: false, results, error: 'Inconsistent Halmos process and test exit status', output }; + } + const normalizeId = id => { + const colon = id.lastIndexOf(':'); + const source = path.relative(cwd, path.resolve(cwd, id.slice(0, colon))).replace(/\\/g, '/'); + return source + id.slice(colon); + }; + if (options.expectedTests) { + const actual = results.map(r => normalizeId(r.contractId) + ':' + r.name).sort(); + const expected = options.expectedTests.map(r => normalizeId(r.contractId) + ':' + r.signature).sort(); + if (JSON.stringify(actual) !== JSON.stringify(expected)) { + return { ok: false, results, error: 'Halmos did not execute exactly the requested Foundry tests', output }; + } + } + const incomplete = results.filter(r => r.status === 'unknown'); + return { ok: incomplete.length === 0, results, exitCode: proc.status, + scope: 'Original test setup and assertions, within configured Halmos input and execution bounds', + ...(incomplete.length ? { error: `${incomplete.length} symbolic test(s) were incomplete or inconclusive` } : {}), + }; + } catch (e) { + return { ok: false, results: [], error: `Halmos result error: ${e.message}` }; + } finally { + fs.rmSync(temp, { recursive: true, force: true }); } - - return { ok: false, error: formatHalmosError() }; } function parseHalmosOutput(text) { @@ -130,16 +160,19 @@ function parseHalmosOutput(text) { // halmos prints the counterexample block BEFORE the [FAIL] summary line, // so buffer cex vars and attach them to the next [FAIL] (cleared on [PASS]). let pendingCex = {}; + let contractId = null; for (const line of lines) { + const suite = line.match(/^Running \d+ tests for (.+)$/); + if (suite) { contractId = suite[1]; pendingCex = {}; continue; } const passMatch = line.match(/\[PASS\]\s+(\S+)/); const failMatch = line.match(/\[FAIL\]\s+(\S+)/); if (passMatch) { - results.push({ name: passMatch[1], passed: true, counterexample: null }); + results.push({ contractId, name: passMatch[1], passed: true, counterexample: null }); pendingCex = {}; } else if (failMatch) { - results.push({ name: failMatch[1], passed: false, counterexample: pendingCex }); + results.push({ contractId, name: failMatch[1], passed: false, counterexample: pendingCex }); pendingCex = {}; } else if (line.includes('Counterexample')) { // header line — variable assignments follow @@ -157,4 +190,4 @@ function parseHalmosOutput(text) { return results; } -module.exports = { runHalmos }; +module.exports = { runHalmos, parseHalmosJson }; diff --git a/src/solparse.js b/src/solparse.js new file mode 100644 index 0000000..8fa9197 --- /dev/null +++ b/src/solparse.js @@ -0,0 +1,84 @@ +// Shared Solidity source introspection: identifier + function-signature +// resolution used by the CVL exporter and the Echidna/Foundry generators. +// Regex-based and best-effort by design: generators must fail LOUDLY (TODO +// comments, skipped blocks) rather than emit fabricated identifiers. + +function codeOnly(source) { + return source.replace(/("(?:\\.|[^"\\])*"|'(?:\\.|[^'\\])*')|\/\*[\s\S]*?\*\/|\/\/[^\n]*/g, + match => match.replace(/[^\n]/g, ' ')); +} + +function parseContractInfo(source) { + source = codeOnly(source); + const info = { + uints: [], + maps: [], + publicMaps: [], + structMaps: [], + structs: {}, + contractNames: [], + }; + let m; + const mUint = /(?\s*uint256\s*\)\s*(?:public|internal|private)?\s+(\w+)/g; + while ((m = mMap.exec(source)) !== null) { + if (!info.maps.includes(m[1])) info.maps.push(m[1]); + } + const publicMap = /mapping\s*\(\s*address\s*=>\s*(?:uint256|uint)\s*\)\s*public\s+(\w+)/g; + while ((m = publicMap.exec(source)) !== null) info.publicMaps.push(m[1]); + const mStructMap = /mapping\s*\(\s*address\s*=>\s*(\w+)\s*\)\s*(?:public|internal|private)?\s+(\w+)/g; + while ((m = mStructMap.exec(source)) !== null) { + info.structMaps.push({ struct: m[1], name: m[2] }); + } + const mStruct = /struct\s+(\w+)\s*\{([^}]*)\}/g; + while ((m = mStruct.exec(source)) !== null) { + const fields = []; + let fm; + const mField = /(uint256|uint|address|bool)\s+(\w+)/g; + while ((fm = mField.exec(m[2])) !== null) fields.push(fm[2]); + info.structs[m[1]] = fields; + } + const mContract = /contract\s+(\w+)/g; + while ((m = mContract.exec(source)) !== null) info.contractNames.push(m[1]); + return info; +} + +// Returns [{ name, sig, args }] where sig is the solidity signature +// (e.g. "deposit(uint256,address)") and args the comma-joined `type name` list. +function parseFunctions(source) { + source = codeOnly(source); + const functions = []; + const mFn = /function\s+(\w+)\s*\(([^)]*)\)([^;{]*)/g; + let m; + const typeOf = (raw) => raw + .replace(/mapping[^,()]*/, 'mapping') + .trim(); + while ((m = mFn.exec(source)) !== null) { + const name = m[1]; + const visibility = (m[3].match(/\b(public|external|internal|private)\b/) || [])[1]; + const params = []; + const body = m[2]; + if (body.trim() === '') { + functions.push({ name, sig: `${name}()`, args: '', visibility }); + continue; + } + // split top-level commas (no nested parens in our supported signatures) + for (const part of body.split(',')) { + const p = part.trim(); + const tok = p.split(/\s+/); + if (tok.length >= 2) { + const type = typeOf(tok.slice(0, -1).join(' ')); + const argName = tok[tok.length - 1]; + params.push(`${type} ${argName}`); + } else if (p) { + params.push(p); + } + } + const sig = `${name}(${params.map((p) => p.split(/\s+/)[0]).join(',')})`; + functions.push({ name, sig, args: params.join(', '), visibility }); + } + return functions; +} + +module.exports = { parseContractInfo, parseFunctions, codeOnly }; diff --git a/test/cvl-compile.js b/test/cvl-compile.js new file mode 100644 index 0000000..5944d02 --- /dev/null +++ b/test/cvl-compile.js @@ -0,0 +1,26 @@ +// Compile and typecheck an actually generated CVL spec. This submits no proof. +const assert = require('node:assert/strict'); +const fs = require('node:fs'); +const os = require('node:os'); +const path = require('node:path'); +const { spawnSync } = require('node:child_process'); +const { exportCvl } = require('../src/cvl-export'); + +const fixture = path.join(__dirname, '../examples'); +const root = fs.mkdtempSync(path.join(os.tmpdir(), 'counterflow-cvl-compile-')); +try { + const generated = exportCvl(path.join(fixture, 'TokenPool.binding.json'), path.join(fixture, 'TokenPool.sol')); + assert.equal(generated.ok, true, generated.error); + assert.deepEqual(generated.covered, ['solvency']); + assert.equal(generated.complete, false, 'Unsigned nonnegativity checks remain unsupported'); + fs.copyFileSync(path.join(fixture, 'TokenPool.sol'), path.join(root, 'TokenPool.sol')); + fs.writeFileSync(path.join(root, 'TokenPool.spec'), generated.cvl); + const result = spawnSync('certoraRun', ['TokenPool.sol', '--verify', 'TokenPool:TokenPool.spec', + '--solc', process.env.COUNTERFLOW_SOLC || 'solc', '--compilation_steps_only'], { + cwd: root, encoding: 'utf8', timeout: 180000, maxBuffer: 10 * 1024 * 1024, + }); + assert.equal(result.status, 0, [result.error?.message, result.stdout, result.stderr].filter(Boolean).join('\n')); + console.log('Generated solvency CVL compiled and typechecked. No remote proof submitted.'); +} finally { + fs.rmSync(root, { recursive: true, force: true }); +} diff --git a/test/e2e.js b/test/e2e.js index ea9db17..70db38c 100644 --- a/test/e2e.js +++ b/test/e2e.js @@ -103,12 +103,15 @@ function run() { }); console.log('echidna gen'); - t('generateEchidnaTest produces valid output', () => { + t('Echidna resolves concrete storage and reports unsupported invariants', () => { const { generateEchidnaTest } = require('../src/echidna-gen'); - const out = generateEchidnaTest(correct); - assert.ok(typeof out === 'string', 'output should be a string'); - assert.ok(out.includes('echidna_'), 'output should contain echidna_ properties'); - assert.ok(out.includes('contract Echidna'), 'output should contain contract Echidna'); + const out = generateEchidnaTest(correct, path.join(__dirname, '../examples/TokenPool.sol'), 'TokenPool', './TokenPool.sol'); + assert.deepStrictEqual(out.covered, ['solvency']); + assert.strictEqual(out.complete, false); + assert.ok(out.sol.includes('return sum == totalAssets;')); + assert.ok(out.sol.includes('delegatecall')); + assert.ok(!out.sol.includes('return true;')); + assert.throws(() => generateEchidnaTest(correct), /requires --contract/); }); console.log('foundry export'); @@ -124,19 +127,16 @@ function run() { }); console.log('CVL export'); - t('generateCvl produces valid CVL with ghost variables', () => { + t('CVL exports concrete storage hooks and getters without empty rules', () => { const { generateCvl } = require('../src/cvl-export'); - const cvl = generateCvl(correct); - assert.ok(typeof cvl === 'string', 'output should be a string'); - assert.ok(cvl.length > 0, 'output should not be empty'); - assert.ok(cvl.includes('ghost'), 'output should contain ghost declarations'); - assert.ok(cvl.includes('rule deposit'), 'output should contain rule for deposit'); - assert.ok(cvl.includes('rule withdraw'), 'output should contain rule for withdraw'); - assert.ok(cvl.includes('require amt > 0'), 'output should contain require amt > 0'); - assert.ok(cvl.includes('invariant nonneg_balance'), 'output should contain invariant nonneg_balance'); - assert.ok(cvl.includes('invariant nonneg_total'), 'output should contain invariant nonneg_total'); - assert.ok(cvl.includes('invariant solvency'), 'output should contain invariant solvency'); - assert.ok(cvl.includes('preserve'), 'output should contain preserve block'); + const cvl = generateCvl(correct, fs.readFileSync(path.join(__dirname, '../examples/TokenPool.sol'), 'utf8')); + assert.ok(cvl.includes('hook Sstore balances[KEY address user]')); + assert.ok(cvl.includes('to_mathint(newBalance) - to_mathint(oldBalance)')); + assert.ok(cvl.includes('function totalAssets() external returns (uint256) envfree;')); + assert.ok(cvl.includes('invariant solvency() to_mathint(totalAssets()) == ghost_sumBalances;')); + assert.ok(!cvl.includes('rule deposit')); + assert.ok(!cvl.includes('invariant nonneg_balance')); + assert.throws(() => generateCvl(correct), /concrete contract source/); }); t('exportCvl rejects invalid binding', () => { const { exportCvl } = require('../src/cvl-export'); @@ -155,9 +155,12 @@ function run() { const path = require('path'); const tmp = path.join(__dirname, '..', 'tmp_valid.json'); fs.writeFileSync(tmp, JSON.stringify(correct)); - const result = exportCvl(tmp); + assert.strictEqual(exportCvl(tmp).ok, false); + const result = exportCvl(tmp, path.join(__dirname, '../examples/TokenPool.sol')); fs.unlinkSync(tmp); assert.strictEqual(result.ok, true); + assert.strictEqual(result.complete, false); + assert.deepStrictEqual(result.covered, ['solvency']); assert.ok(result.cvl, 'should return CVL output'); assert.strictEqual(result.model, 'erc20_pool'); }); diff --git a/test/exporters.test.js b/test/exporters.test.js new file mode 100644 index 0000000..7c09511 --- /dev/null +++ b/test/exporters.test.js @@ -0,0 +1,56 @@ +const test = require('node:test'); +const assert = require('node:assert/strict'); +const fs = require('node:fs'); +const path = require('node:path'); +const os = require('node:os'); +const { spawnSync } = require('node:child_process'); +const { generateEchidnaTest, generateEchidnaConfig } = require('../src/echidna-gen'); +const binding = require('../examples/TokenPool.binding.json'); +const hasForge = spawnSync('forge', ['--version']).status === 0; + +test('generated concrete properties preserve callers and distinguish corrupt accounting', { skip: !hasForge }, () => { + const dir = fs.mkdtempSync(path.join(os.tmpdir(), 'counterflow-export-')); + try { + fs.mkdirSync(path.join(dir, 'test')); + fs.writeFileSync(path.join(dir, 'foundry.toml'), '[profile.default]\nsolc = "0.8.24"\nlibs = []\n'); + const source = fs.readFileSync(path.join(__dirname, '../examples/TokenPool.sol'), 'utf8'); + for (const [name, code] of [['TokenPool', source], ['CorruptPool', source.replace(/TokenPool/g, 'CorruptPool').replace('totalAssets += amt;', 'totalAssets += amt + 1;')]]) { + const file = path.join(dir, `${name}.sol`); + fs.writeFileSync(file, code); + const generated = generateEchidnaTest(binding, file, name, `../${name}.sol`); + fs.writeFileSync(path.join(dir, 'test', generated.fileName), generated.sol); + assert.equal(generated.complete, false); + assert.match(generateEchidnaConfig(binding, generated.filterFunctions), /filterBlacklist: false/); + assert.ok(generated.filterFunctions.includes(`Echidna${name}.cf_deposit(uint256)`)); + } + fs.writeFileSync(path.join(dir, 'test/Generated.t.sol'), `pragma solidity ^0.8.20; +import "./EchidnaTokenPool.sol"; +import "./EchidnaCorruptPool.sol"; +interface Vm { function prank(address) external; } +contract GeneratedTest { + Vm constant vm = Vm(address(uint160(uint256(keccak256("hevm cheat code"))))); + function test_correct_twoCallers() public { + EchidnaTokenPool p = new EchidnaTokenPool(); + vm.prank(address(11)); p.cf_deposit(17); + vm.prank(address(22)); p.cf_deposit(9); + assert(p.balances(address(11)) == 17 && p.balances(address(22)) == 9); + assert(p.balances(address(p)) == 0 && p.echidna_solvency()); + vm.prank(address(11)); p.cf_withdraw(7); + assert(p.balances(address(11)) == 10 && p.echidna_solvency()); + } + function test_detects_corruption() public { + EchidnaCorruptPool p = new EchidnaCorruptPool(); + vm.prank(address(11)); p.cf_deposit(17); + assert(!p.echidna_solvency()); + } +}`); + const result = spawnSync('forge', ['test', '--root', dir, '--json'], { encoding: 'utf8', timeout: 90000 }); + assert.equal(result.status, 0, result.stdout + result.stderr); + const tests = Object.values(JSON.parse(result.stdout)).flatMap(s => Object.values(s.test_results)); + assert.equal(tests.length, 2); + assert.ok(tests.every(t => t.status === 'Success')); + const privateFile = path.join(dir, 'Private.sol'); + fs.writeFileSync(privateFile, source.replaceAll('external {', 'internal {')); + assert.throws(() => generateEchidnaTest(binding, privateFile, 'TokenPool', './Private.sol'), /public or external/); + } finally { fs.rmSync(dir, { recursive: true, force: true }); } +}); diff --git a/test/fixtures/fuzz-project/foundry.toml b/test/fixtures/fuzz-project/foundry.toml new file mode 100644 index 0000000..0e094ba --- /dev/null +++ b/test/fixtures/fuzz-project/foundry.toml @@ -0,0 +1,10 @@ +[profile.default] +src = "src" +test = "test" +out = "out" +libs = [] +solc = "0.8.24" + +[profile.default.fuzz] +runs = 256 +seed = "0x42" diff --git a/test/fixtures/fuzz-project/test/Accounting.t.sol b/test/fixtures/fuzz-project/test/Accounting.t.sol new file mode 100644 index 0000000..461e4d4 --- /dev/null +++ b/test/fixtures/fuzz-project/test/Accounting.t.sol @@ -0,0 +1,33 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.20; + +contract AccountingTest { + uint256 internal opening; + + function setUp() public { + opening = 17; + } + + function testFuzz_safe(uint8 amount) external { + assert(opening == 17); + uint256 expected = opening + amount; + opening += amount; + assert(opening == expected); + } + + function testFuzz_bug(uint8 amount) external { + assert(opening == 17); + uint256 expected = opening + amount; + opening += amount; + if (amount == 7) opening++; + assert(opening == expected); + } + + function test_nonFuzz_failure() external pure { + assert(false); + } + + function testFuzz_reverts(uint8 amount) external pure { + require(amount == 0, "unsupported amount"); + } +} diff --git a/test/symbolic.test.js b/test/symbolic.test.js new file mode 100644 index 0000000..28a5010 --- /dev/null +++ b/test/symbolic.test.js @@ -0,0 +1,134 @@ +const test = require('node:test'); +const assert = require('node:assert/strict'); +const fs = require('node:fs'); +const os = require('node:os'); +const path = require('node:path'); +const { spawnSync } = require('node:child_process'); +const { parseForgeResults, runFuzzThenSymbolic, generateSymbolicFromCex } = require('../src/forge-symb'); +const { parseHalmosJson, runHalmos } = require('../src/halmos-runner'); + +const contractId = 'test/Accounting.t.sol:AccountingTest'; +const signature = 'testFuzz_bug(uint8)'; +const forgeReport = (extra = {}) => JSON.stringify({ [contractId]: { test_results: { + [signature]: { status: 'Failure', reason: 'assertion failed', counterexample: { Single: { calldata: '0x1234', args: '7' } }, ...extra }, +} } }); +const symbolicReport = (extra = {}) => JSON.stringify({ exitcode: 0, test_results: { [contractId]: [ + { name: signature, exitcode: 0, num_paths: [1, 1, 0], num_bounded_loops: 0, ...extra }, +] } }); + +test('a counterexample alone cannot fabricate a new symbolic assertion', () => { + assert.throws(() => generateSymbolicFromCex('testBug', { args: ['7'] }, 'TokenPool'), /original Foundry project/); +}); + +test('Forge parsing keeps exact signatures, calldata, and suite identity', () => { + const [result] = parseForgeResults(forgeReport()); + assert.equal(result.signature, signature); + assert.equal(result.contractId, contractId); + assert.equal(result.counterexample.Single.calldata, '0x1234'); +}); + +test('zero tests, malformed output, compilation failure and killed Forge never pass', () => { + for (const result of [ + { status: 0, stdout: '{}' }, { status: 0, stdout: 'not JSON' }, + { status: 1, stdout: '{}' }, { status: null, error: new Error('ETIMEDOUT') }, + { status: 0, stdout: forgeReport({ status: 'Skipped' }) }, + { status: 0, stdout: forgeReport() }, + ]) { + const r = runFuzzThenSymbolic('AccountingTest', '*', { spawnSync: () => result }); + assert.equal(r.ok, false); + assert.equal(r.complete, false); + } +}); + +test('symbolic success never erases a concrete fuzz failure', () => { + let options; + const result = runFuzzThenSymbolic('AccountingTest', '*', { + spawnSync: () => ({ status: 1, stdout: forgeReport() }), + runHalmos: (_, args) => { options = args; return { ok: true, results: [{ passed: true, status: 'passed' }] }; }, + }); + assert.equal(result.verdict, 'violated'); + assert.equal(result.complete, false); + assert.equal(result.symbolicResults[0].status, 'inconsistent'); + assert.equal(options.matchTest, '^testFuzz_bug\\(uint8\\)$'); + assert.deepEqual(options.expectedTests, [{ contractId, signature }]); +}); + +test('empty symbolic results and unsupported stateful sequences remain inconclusive', () => { + const empty = runFuzzThenSymbolic('AccountingTest', '*', { + spawnSync: () => ({ status: 1, stdout: forgeReport() }), + runHalmos: () => ({ ok: true, results: [] }), + }); + assert.equal(empty.complete, false); + const sequence = runFuzzThenSymbolic('AccountingTest', '*', { + spawnSync: () => ({ status: 1, stdout: forgeReport({ counterexample: { Sequence: [] } }) }), + runHalmos: () => { throw new Error('must not discard the sequence'); }, + }); + assert.equal(sequence.verdict, 'violated'); + assert.equal(sequence.symbolicResults[0].status, 'unsupported'); +}); + +test('Halmos needs nonempty structured evidence, with no truncated or stuck paths', () => { + assert.throws(() => parseHalmosJson('{"test_results":{}}'), /zero tests/); + for (const extra of [ + { exitcode: 2 }, { exitcode: 3 }, { exitcode: 4 }, { exitcode: 5 }, + { num_bounded_loops: 1 }, { num_paths: [2, 1, 1] }, { num_paths: [1, 0, 0] }, + { num_paths: [0, 1, 0] }, { num_paths: [1, '1', 0] }, { num_paths: [1, 1, 0, 0] }, + { exitcode: 1, num_models: '1', models: [{ is_valid: true }] }, + { exitcode: 1, num_models: 1, models: [{ is_valid: false }] }, + ]) { + const r = parseHalmosJson(symbolicReport(extra)).results[0]; + assert.equal(r.passed, false); + assert.equal(r.status, 'unknown'); + } + assert.equal(parseHalmosJson(symbolicReport()).results[0].status, 'passed'); +}); + +test('Halmos concrete witnesses retain full-width values from its hex transcript', () => { + const hex = '0x' + 'f'.repeat(64); + const raw = symbolicReport({ exitcode: 1, num_models: 1, models: [{ is_valid: true }] }); + const text = `Running 1 tests for ${contractId}\nCounterexample:\n amount = ${hex}\n[FAIL] ${signature}`; + assert.equal(parseHalmosJson(raw, text).results[0].counterexample.amount, hex); +}); + +const hasForge = spawnSync('forge', ['--version'], { encoding: 'utf8' }).status === 0; +const localHalmos = path.join(__dirname, '..', '.venv', 'bin', 'halmos'); +const hasHalmos = fs.existsSync(localHalmos) || spawnSync('halmos', ['--version'], { encoding: 'utf8' }).status === 0; +if (process.env.COUNTERFLOW_REQUIRE_SYMBOLIC === '1') { + assert.ok(hasForge && hasHalmos, 'Required integration tools: forge and halmos'); +} + +test('real Forge and Halmos preserve setup, typed inputs, assertions, and CLI exit codes', { + skip: !(hasForge && hasHalmos), timeout: 180000, +}, () => { + const root = fs.mkdtempSync(path.join(os.tmpdir(), 'counterflow-symbolic-e2e-')); + try { + fs.cpSync(path.join(__dirname, 'fixtures/fuzz-project'), root, { recursive: true }); + const source = path.join(root, 'test/Accounting.t.sol'); + const before = fs.readFileSync(source, 'utf8'); + const bug = runFuzzThenSymbolic('AccountingTest', '^testFuzz_bug', { cwd: root }); + assert.equal(bug.verdict, 'violated'); + assert.equal(bug.complete, true, JSON.stringify(bug)); + assert.equal(bug.symbolicResults[0].status, 'reproduced'); + assert.ok(Object.values(bug.symbolicResults[0].halmos.results[0].counterexample).includes('0x07')); + const safe = runFuzzThenSymbolic('AccountingTest', '^testFuzz_safe', { cwd: root }); + assert.equal(safe.verdict, 'fuzz_passed'); + assert.equal(safe.symbolicResults.length, 0); + const safeSymbolic = runHalmos('AccountingTest', { cwd: root, matchTest: '^testFuzz_safe\\(uint8\\)$' }); + assert.equal(safeSymbolic.ok, true, safeSymbolic.error); + assert.equal(safeSymbolic.results[0].status, 'passed'); + const missing = runHalmos('AccountingTest', { cwd: root, matchTest: '^doesNotExist$' }); + assert.equal(missing.ok, false); + const nonFuzz = runFuzzThenSymbolic('AccountingTest', '^test_nonFuzz', { cwd: root }); + assert.equal(nonFuzz.symbolicResults[0].status, 'reproduced'); + const revert = runFuzzThenSymbolic('AccountingTest', '^testFuzz_reverts', { cwd: root }); + assert.equal(revert.verdict, 'violated'); + assert.equal(revert.complete, false); // Halmos treats ordinary require as an assumption. + for (const [regex, code] of [['^testFuzz_bug', 3], ['^testFuzz_safe', 0], ['^absent$', 2]]) { + const cli = spawnSync(process.execPath, [path.join(__dirname, '../src/cli.js'), 'fuzz-symb', 'AccountingTest', '--root', root, '--test', regex, '--json'], { encoding: 'utf8', timeout: 60000 }); + assert.equal(cli.status, code, cli.stdout + cli.stderr); + assert.equal(typeof JSON.parse(cli.stdout).ok, 'boolean'); + } + assert.equal(fs.readFileSync(source, 'utf8'), before); + assert.deepEqual(fs.readdirSync(path.join(root, 'test')), ['Accounting.t.sol']); + } finally { fs.rmSync(root, { recursive: true, force: true }); } +}); From 5072d60f4709ba2a27497f465c8bbc92615f5091 Mon Sep 17 00:00:00 2001 From: William Weishuhn Date: Sun, 6 Sep 2026 03:14:12 -0400 Subject: [PATCH 2/3] Retain diagnostics for inconclusive bytecode checks --- bench/halmos-check.js | 5 +++++ src/halmos-runner.js | 5 ++++- 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/bench/halmos-check.js b/bench/halmos-check.js index 94de256..dd0194a 100644 --- a/bench/halmos-check.js +++ b/bench/halmos-check.js @@ -24,6 +24,11 @@ console.log(''); const r = runHalmos('*'); if (!r.ok) { console.error(`${C.red}halmos error: ${r.error}${C.reset}`); + for (const result of r.results) { + console.error(JSON.stringify({ name: result.name, status: result.status, + exitCode: result.exitCode, paths: result.paths, boundedLoops: result.boundedLoops })); + } + if (r.output) console.error(r.output); process.exit(2); } diff --git a/src/halmos-runner.js b/src/halmos-runner.js index 6b2414b..e479e78 100644 --- a/src/halmos-runner.js +++ b/src/halmos-runner.js @@ -143,7 +143,10 @@ function runHalmos(testContract, options = {}) { const incomplete = results.filter(r => r.status === 'unknown'); return { ok: incomplete.length === 0, results, exitCode: proc.status, scope: 'Original test setup and assertions, within configured Halmos input and execution bounds', - ...(incomplete.length ? { error: `${incomplete.length} symbolic test(s) were incomplete or inconclusive` } : {}), + ...(incomplete.length ? { + error: `${incomplete.length} symbolic test(s) were incomplete or inconclusive`, + output, + } : {}), }; } catch (e) { return { ok: false, results: [], error: `Halmos result error: ${e.message}` }; From af7cf07bd0f496b670516598152a3572ad6710ab Mon Sep 17 00:00:00 2001 From: William Weishuhn Date: Sun, 6 Sep 2026 03:17:11 -0400 Subject: [PATCH 3/3] Preserve native contract creation when running Foundry with Halmos --- README.md | 5 +++++ src/forge-symb.js | 3 +++ src/halmos-runner.js | 3 +++ 3 files changed, 11 insertions(+) diff --git a/README.md b/README.md index b70a2b6..0e045bc 100644 --- a/README.md +++ b/README.md @@ -170,6 +170,11 @@ unsupported. Empty results, skipped tests, solver timeouts, stuck paths, all-rev execution and truncated loops cannot count as symbolic passes. Halmos passes are scoped to its configured input/execution bounds. +Both engines use `FOUNDRY_DYNAMIC_TEST_LINKING=false` to preserve native contract +creation. [Foundry 1.8 enables dynamic test linking by default](https://github.com/foundry-rs/foundry/releases/tag/v1.8.0); +its injected `deployCode(string)` cheatcode is unsupported by Halmos 0.3.3. +The runner sets this per process and leaves the project's configuration file intact. + `gen-echidna` and `export-cvl` require `--contract Contract.sol`. Both report covered and unsupported invariants and exit 2 on partial coverage. Unsigned `>= 0` checks are deliberately unsupported: they cannot witness arithmetic wrap. diff --git a/src/forge-symb.js b/src/forge-symb.js index 939d016..2a8fad3 100644 --- a/src/forge-symb.js +++ b/src/forge-symb.js @@ -193,6 +193,9 @@ function runFuzzThenSymbolic(contractName, testGlob, options = {}) { const fuzzRun = run('forge', forgeArgs, { cwd, encoding: 'utf-8', maxBuffer: 50 * 1024 * 1024, timeout: options.timeoutMs || 300000, + // Foundry 1.8 defaults to deployCode instrumentation unsupported by Halmos + // 0.3.3. Both engines must compile the original native CREATE operations. + env: { ...process.env, FOUNDRY_DYNAMIC_TEST_LINKING: 'false' }, }); if (fuzzRun.error || fuzzRun.signal || ![0, 1].includes(fuzzRun.status)) { return { ...empty, ok: false, error: `Forge execution failed: ${fuzzRun.error?.message || fuzzRun.signal || fuzzRun.stderr || fuzzRun.status}` }; diff --git a/src/halmos-runner.js b/src/halmos-runner.js index e479e78..5c42086 100644 --- a/src/halmos-runner.js +++ b/src/halmos-runner.js @@ -116,6 +116,9 @@ function runHalmos(testContract, options = {}) { const proc = spawnSync(halmosBin || python, args, { cwd, encoding: 'utf-8', timeout: options.timeoutMs || 300000, maxBuffer: 50 * 1024 * 1024, + // Keep Foundry's new deployCode instrumentation out of the bytecode; + // Halmos 0.3.3 supports the underlying native CREATE instructions. + env: { ...process.env, FOUNDRY_DYNAMIC_TEST_LINKING: 'false' }, }); const output = (proc.stdout || '') + '\n' + (proc.stderr || ''); if (proc.error || proc.signal || ![0, 1].includes(proc.status)) {