The evm-redex test suite: tutorial, tests, and examples🔗ℹ

1.1 A storage contract🔗ℹ

We start from the Storage example in the Solidity documentation’s introduction to smart contracts. It is the smallest contract that still has interesting behaviour: one state variable, a setter and a getter.

The source, the compiled artifact, and the finished property file are bundled in "storage/" ("Storage.sol", "storage.json", "storage-props.rkt"); this section reconstructs that file step by step.

1.2 A voting contract🔗ℹ

The Storage example above is deliberately trivial. This section applies the same pipeline to the Ballot contract from the Solidity documentation’s Solidity by Example (voting with delegation), which has real correctness obligations: access control, one-person-one-vote, and a tally that must return the winner. The bundled version is "voting/" ("Ballot.sol", "ballot.json", "ballot-props.rkt").

1.3 A blind auction with time and Ether🔗ℹ

The BlindAuction contract (same Solidity by Example page) is the most demanding of the three: it depends on block.timestamp, moves Ether, and uses a hash commitment. It shows the two features that separate property-based testing from single-scenario tests, namely generating over time and over the secret. The bundled version is "blind-auction/".

1.4 Further worked examples🔗ℹ

The same pipeline scales from these toy contracts to production Solidity. This project bundles several more worked examples, each with its .sol, a solc artifact, and a property file:

• "storage/", "voting/" and "blind-auction/" — the three examples above (the Solidity documentation’s Storage, Ballot and BlindAuction).

• "erc20/" and "erc721/" — the minimal ERC-20 / ERC-721 from solidity-by-example.

• "open-zeppelin/" — property specifications for a curated set of OpenZeppelin contracts (ERC20, Ownable, AccessControl, ERC721, ERC1155), built from the verbatim OZ sources plus one concrete instance (*Mock.sol) per contract. Each "properties/<Contract>.rkt" attests the invariant classes the OZ audits emphasise: supply / ownership conservation, allowance and access-control semantics, no unauthorized mint, ERC-conformant reverts, and OZ specifics such as the infinite-allowance optimisation not decrementing.

Every trial executes the contract through the fast Racket executor, so hundreds of trials per property run quickly. Running the ERC-721 example even surfaced a genuine interpreter bug (a LOG that failed to pop its stack operands, masked by the conformance fixtures): property-based testing over real contracts exercises paths the reference vectors do not. It finds counterexamples; it does not prove their absence.

3.1 Twins🔗ℹ

3.2 Calls and generated sequences🔗ℹ

(define SCHEMAS

(list (list "transfer(address,uint256)"             (gen:one-of ACTORS) gen-amount)

(list "approve(address,uint256)"              (gen:one-of ACTORS) gen-amount)

(list "transferFrom(address,address,uint256)" (gen:one-of ACTORS)

(gen:one-of ACTORS) gen-amount)))

3.3 The engine🔗ℹ

The comparison kinds:

3.4 The macro🔗ℹ

Give either #:twin (a twin you built yourself) or #:contracts (two creation codes, deployed once at definition time — not per trial). Prefer #:twin when you want to hand the shrunk counterexample to explain-equivalence, which needs the twin.

(define TW (deploy-twin REF MUTANT #:actors ACTORS))

(define-evm-equivalence mutant-is-distinguished

#:twin      TW

#:given     ([seq (gen-call-sequence SCHEMAS #:length 8 #:actors ACTORS)])

#:sequence  (append SETUP seq)

#:observe   GETTERS

#:compare   '(outcome return logs state)

#:trials 100 #:seed 20260712)

#:sequence is any expression producing a list of evm-call — the example above prepends a fixed SETUP prefix (mints that fund the actors) to the generated part, so the generated calls can get straight to the behaviour under test instead of having to stumble on a valid state by luck. That trick, and a small actor pool, are usually what stands between a property that finds the bug and one that passes vacuously.

3.5 How the harness is validated🔗ℹ

A harness that only ever reports equivalent is worthless, so "equivalence/erc20-equivalence.rkt" pins down all three outcomes it must be able to produce. The contracts ("equivalence/contracts/ERC20Ref.sol" and "ERC20Mutant.sol") are compiled and committed alongside it.

• Self-equivalence — ERC20Ref against itself: must pass. If this ever falsifies, the harness itself is nondeterministic.

• Optimiser — ERC20Ref against its own solc –optimize build (same source, 2652 vs 5486 bytes of bytecode): must pass. This is what proves the comparison is behavioural and not a bytecode diff.

• Mutant — ERC20Ref against ERC20Mutant, which carries one seeded bug (transferFrom checks the allowance but never debits it): must falsify. The counterexample shrinks to two calls, approve followed by transferFrom, and the divergence is reported on the allowance getter.

"pbt/equivalence-test.rkt" pins the pieces underneath: twins land at the same address in two separate worlds, equivalence-report-effective counts only the calls that actually succeeded, gas is enforced as a bound rather than an equality, and a reverted call emits no logs.

The mutant case is also a lesson about generators. With three actors and a six-call sequence the seeded bug was not caught in 40 trials — the engine was fine, the generator’s reach was not. A two-actor pool and a fixed setup prefix (mints that fund the actors) are what make the property find it.

4.1 The two measures🔗ℹ

• Instructions — the instruction starts of the runtime code that were executed. The denominator is the walk that steps over PUSH immediates (a byte inside PUSH data is not an instruction and can never be covered), minus solc’s non-executable metadata trailer, which would otherwise cap coverage at an arbitrary ceiling.

• JUMPI branches — for each JUMPI, whether both sides were taken. This is the measure that catches a weak property: instruction coverage saturates early, while a require the generators never falsify leaves its JUMPI one-sided forever.

Coverage is necessary, not sufficient. 100% of the instructions with a vacuous #:post still proves nothing — it says the code ran, not that anything was checked. Read it as a lower bound on the property’s reach, never as evidence of correctness.

4.2 Collecting🔗ℹ

4.3 Reading the result🔗ℹ

4.4 Solidity lines🔗ℹ

When the artifact carries a runtime source map, the same hits lift to source lines. solc’s map has one entry per instruction, in order, so the i-th entry belongs to the i-th instruction start — and the two counts agreeing is an independent check that the instruction walk is right.

An instruction is attributed to the line of its start offset only, not to its whole source range: solc maps the dispatcher to the entire contract, and honouring the range would paint every line green. And under –optimize the attribution is approximate — the optimiser merges and moves instructions, so a line reported as missed may be one whose code was folded elsewhere.

Build an artifact with the map by adding srcmap-runtime to solc’s –combined-json list; it leaves the bytecode byte-for-byte identical, so it can be added to any existing artifact without moving anything else in a suite.

4.5 Validation: separating a weak property from a strong one🔗ℹ

The house rule: a measure you have never seen distinguish anything is not evidence. "coverage/coverage-demo.rkt" states two properties over the same contract ("coverage/contracts/Token.sol", a plain token). Both are true, and both pass. They differ only in reach:

• The weak one calls a single function, transfer, and only ever with amounts the sender can afford. Every require in the contract succeeds on every trial.

• The strong one drives all four entry points and lets the generators produce amounts that overshoot the balance and the allowance, and a zero recipient — so the failing side of each check is exercised too.

A green suite cannot tell these apart. Coverage can, and the module asserts that it does: the weak property covers strictly fewer instructions and fewer lines, never enters approve / transferFrom / burn (checked at the level of specific source lines), and leaves strictly more branches one-sided.

Run racket coverage/coverage-demo.rkt to also print the annotated Solidity listing of what the weak property never executed.

"pbt/coverage-test.rkt" pins the mechanism underneath. Two checks carry most of the weight. First, the instruction walk (which steps over PUSH immediates) is compared against the number of entries in solc’s runtime source map — two independent computations of "how many instructions does this code have", which must agree, or every pc → line attribution would be off by some amount. Second, the covered instructions and the uncovered ones must partition the instruction set exactly, which is what says no byte inside a PUSH immediate was ever reported as executed. The rest: constructor coverage is kept apart from runtime coverage, coverage-merge is a union, and the numbers are identical under the Redex reference backend — which they must be, since the tracing hook lives in the driver loop rather than in either executor.

The artifact for this demo is built with the runtime source map and without the optimiser: solc –combined-json bin,bin-runtime,abi,srcmap-runtime contracts/Token.sol. The optimiser makes the line attribution approximate, since it merges and moves instructions.