Runs are not reproducible under --timeout even with a fixed --seed and --workers 1 (use --test-limit)
- Dominant language
- Haskell
- Stars
- 3.2k
- Forks
- 432
- Avg merge
- 1d 20h
- Merged PRs (30d)
- 5
Description
### Summary
With a fixed `--seed` **and `--workers 1`**, Echidna runs are still **not reproducible when the campaign is bounded by `--timeout`**: each run executes a different (machine-speed-dependent) number of test cases, so a property can be falsified in one run and reported as passing in another with identical arguments. Bounding the campaign by `--test-limit` instead is fully deterministic.
This is distinct from #1091 (non-determinism with `workers > 1`): here `--workers 1` is used, and the source of non-determinism is the wall-clock `--timeout` stop condition, not worker races.
### Impact
`--seed` is widely assumed to make a run reproducible. When a campaign uses `--timeout` (the common default in tutorials and CI), the same `--seed` explores a different number of sequences each run, so:
- falsification is flaky (a real violation is found only in some runs), and
- a saved reproducer cannot be re-derived by re-running with the same seed.
### Minimal reproducer
`Det.sol` (no RPC, deterministic work per call, property never actually fails — we only compare how much work each run does):
```solidity
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.20;
contract Det {
uint256 x;
function poke(uint256 a) public { x = uint256(keccak256(abi.encode(a, x))); }
function echidna_prop() public view returns (bool) { return x != type(uint256).max; }
}
```
Bounded by wall-clock `--timeout` — **not reproducible** (Total calls differ run to run):
```
$ echidna Det.sol --contract Det --format text --seed 1 --workers 1 --timeout 4
... Total calls: 14417
$ echidna Det.sol --contract Det --format text --seed 1 --workers 1 --timeout 4
... Total calls: 13205
```
Bounded by `--test-limit` — **reproducible** (identical):
```
$ echidna Det.sol --contract Det --format text --seed 1 --workers 1 --test-limit 20000
... Total calls: 20071
$ echidna Det.sol --contract Det --format text --seed 1 --workers 1 --test-limit 20000
... Total calls: 20071
```
On a real on-chain harness the consequence is result-level: with the same `--seed`, `--workers 1` and `--rpc-block N`, a property is falsified under `--timeout 60` in some runs and not others, but reproducibly (found or not found the same way every time) under `--test-limit`.
### Expected
Either:
1. document clearly that reproducibility requires `--test-limit` and that `--timeout` is inherently non-reproducible even with a fixed `--seed` (and, ideally, warn when both `--seed` and `--timeout` are given), or
2. make a `--seed`ed, `--timeout`-bounded run reproducible (e.g. stop after a seed-derived amount of work rather than pure wall-clock).
### Environment
- Echidna 2.3.3 (x86_64-linux release)
- Linux
Happy to provide the on-chain harness / full logs if useful.
Contributor guide
Research direction
Start with the Det.sol reproducer and run the two echidna commands using --seed 1 and --workers 1, comparing --timeout with --test-limit. Trace the handling of those stop conditions and define done as either clear reproducibility documentation and warning behavior, or deterministic results for seeded timeout runs.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- solidity
- Domain
- cli, testing
- Issue type
- Bug
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Active
- Clarity
- Mostly clear
- Newbie friendliness
- 48/100