crytic / crytic/echidna

Runs are not reproducible under --timeout even with a fixed --seed and --workers 1 (use --test-limit)

Open
#1,630 0 comments 0 reactions 0 assignees View on GitHub
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

Open the contributing 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

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.