Tutorial: testing Solidity contracts with evm-redex🔗ℹ

2.1 Compile it🔗ℹ

Ask solc for the bytecode and the ABI, as one JSON file:

  solc --combined-json bin,bin-runtime,abi contracts/Counter.sol > Counter.json

2.2 Load and deploy🔗ℹ

read-artifact pulls the creation and runtime bytecode (and the ABI) out of the JSON; deploy runs the constructor and gives you the deployed address and the resulting world.

(require evm-redex/pbt)

(define ART (read-artifact "Counter.json" #:contract "Counter"))

(define DEPLOYER 2703024129)

(define DEP     (deploy (artifact-creation ART) #:from DEPLOYER))

(define COUNTER (deploy-result-address DEP))

(define BASE    (deploy-result-world DEP))   ; the world just after deployment

2.3 Read state🔗ℹ

count is a public variable, so Solidity generates a count() getter. A call runs a message; call-result-return is its return data, which abi-decode turns back into a number:

(define (count-of world)

(car (abi-decode (list "uint256")

(call-result-return

(call world COUNTER #:data (encode-call "count()"))))))

(count-of BASE)   ; => 0

2.4 Send transactions🔗ℹ

encode-call builds the calldata for a function; call returns a call-result, and call-result-world is the world after the call. Thread that world through a couple of calls and read the count back:

(define CALLER 2964324353)

(define (send world sig . args)

(call-result-world

(call world COUNTER #:from CALLER #:data (apply encode-call sig args))))

(let* ([w (send BASE "increment()")]

[w (send w "add(uint256)" 5)])

(count-of w))    ; => 6

2.5 State a property🔗ℹ

Concrete calls are fine for a sanity check, but the point of the library is to test a property over many generated inputs. define-evm-property in transaction mode (the #:call clause) runs a real transaction; #:given lists the generated inputs, and #:post receives the world before (w0) and after (w1) plus the transaction result:

(define (tx sig . args)

(make-tx #:sender CALLER #:to COUNTER #:gas-limit 200000 #:gas-price 0

#:data (apply encode-call sig args)))

(define-evm-property add-raises-count-by-n

#:given ([n (gen-word-in 0 (expt 2 200))])

#:world BASE

#:call  (tx "add(uint256)" n)

#:post  (lambda (w0 w1 r) (= (count-of w1) (+ (count-of w0) n))))

(check-evm-property add-raises-count-by-n #:trials 50)

Running it prints:

A property can also assert that a call reverts. #:revert-when says "under this condition, the transaction must revert"; from a count of zero, decrement() always does:

(define-evm-property decrement-reverts-at-zero

#:given ()                     ; no generated inputs — a plain assertion

#:world BASE                   ; count is 0 here

#:call  (tx "decrement()")

#:revert-when #t)

(check-evm-property decrement-reverts-at-zero #:trials 1)

3.1 The property that matters: conservation🔗ℹ

The invariant a token must never break is that a transfer moves value without creating or destroying any. This one property captures both the success and the revert paths, over amounts that straddle ALICE’s balance:

(define (tx from sig . args)

(make-tx #:sender from #:to TOKEN #:gas-limit 200000 #:gas-price 0

#:data (apply encode-call sig args)))

(define-evm-property transfer-conserves-supply

#:given ([amount (gen-word-in 0 2000)])       ; straddles the 1000 balance

#:world MINTED

#:call  (tx ALICE "transfer(address,uint256)" BOB amount)

#:post  (lambda (w0 w1 r)

(and (= (total w1) (total w0))       ; supply never changes

(if (eq? (txn-run-outcome r) 'revert)

(= (bal w1 ALICE) (bal w0 ALICE))          ; rolled back

(and (= (bal w1 ALICE) (- (bal w0 ALICE) amount))

(= (bal w1 BOB)   (+ (bal w0 BOB) amount)))))))

(check-evm-property transfer-conserves-supply #:trials 100)

And a focused revert property — a transfer of more than you own must fail:

(define-evm-property transfer-reverts-when-insufficient

#:given ([amount (gen-word-in 1001 100000)])  ; always more than ALICE has

#:world MINTED

#:call  (tx ALICE "transfer(address,uint256)" BOB amount)

#:revert-when #t)

(check-evm-property transfer-reverts-when-insufficient #:trials 50)

When a property fails, the engine shrinks the random inputs to a minimal counterexample and prints it — that shrunk case is the payoff of property-based testing. Try weakening transfer’s require in the contract and re-running: the conservation property falsifies with a tiny transfer.

4.1 Voting🔗ℹ

"tutorial/ballot.rkt" tests Ballot, the delegated-voting contract. Two things are new here: the constructor takes arguments (an array of bytes32 proposal names), which you ABI-encode and append to the creation bytecode; and a getter can return a struct, which you decode as a tuple.

(define ART (read-artifact "Ballot.json" #:contract "Ballot"))

(define CHAIR 3298922497)

; proposal names are bytes32 — pad each to 32 bytes

(define NAMES (list (name->b32 "alpha") (name->b32 "beta") (name->b32 "gamma")))

; constructor args are ABI-encoded and appended to the creation code

(define DEP    (deploy (append (artifact-creation ART)

(abi-encode (list "bytes32[]") (list NAMES)))

#:from CHAIR))

(define BALLOT (deploy-result-address DEP))

The chairperson (the deployer) grants a right to vote, the voter casts it, and the tally updates — and the rule worth checking is that only the chairperson may grant voting rights, so a call from anyone else must revert:

(define OUTSIDER 50157932545)

(define-evm-property only-chair-grants-rights

#:given ([who gen-address])

#:world BASE

#:call  (make-tx #:sender OUTSIDER #:nonce 0 #:to BALLOT #:gas-limit 300000 #:gas-price 0

#:data (encode-call "giveRightToVote(address)" who))

#:revert-when #t)                 ; a non-chairperson caller always reverts

(check-evm-property only-chair-grants-rights #:trials 30)

4.2 An open auction🔗ℹ

"tutorial/auction.rkt" tests SimpleAuction. Its calls carry ether: make-tx’s #:value funds the bid. Accounts that bid need a balance, so we top a couple up by hand — the same thing deploy does for the deployer:

(require (only-in evm-redex world-ref world-set acct-balance acct-with-balance))

(define (fund w a wei)

(world-set w a (acct-with-balance (world-ref w a) (+ (acct-balance (world-ref w a)) wei))))

The auction’s central rule is that a bid is accepted exactly when it beats the current highest, and then becomes the new highest — one property captures both the accept and the reject path:

(define-evm-property bid-raises-the-highest

#:given ([v (gen-word-in 0 500)])

#:world W1                          ; highest bid is 100 here

#:call  (make-tx #:sender BOB #:nonce (nonce-of W1 BOB) #:to AUCTION #:value v

#:gas-limit 300000 #:gas-price 0 #:data (encode-call "bid()"))

#:post  (lambda (w0 w1 r)

(if (> v (highest-bid w0))

(and (eq? (txn-run-outcome r) 'success) (= (highest-bid w1) v))

(eq? (txn-run-outcome r) 'revert))))

(check-evm-property bid-raises-the-highest #:trials 60)

4.3 Safe remote purchase🔗ℹ

"tutorial/purchase.rkt" tests Purchase, a four-state escrow (Created → Locked → Release → Inactive). The constructor is payable — the seller locks twice the item value — so you deploy it with #:value:

(define DEP (deploy (artifact-creation ART) #:from SELLER #:value 200))  ; value = 100

The happy path is buyer confirmPurchase (matching the deposit) then confirmReceived. The rule worth pinning is that from the Locked state only the buyer can confirm receipt:

(define-evm-property only-buyer-confirms-receipt

#:given ()

#:world LOCKED-W

#:call  (make-tx #:sender OUTSIDER #:nonce 0 #:to PURCHASE #:gas-limit 300000 #:gas-price 0

#:data (encode-call "confirmReceived()"))

#:revert-when #t)

(check-evm-property only-buyer-confirms-receipt #:trials 1)

The fourth Solidity by Example contract, the Micropayment Channel, is not included: it verifies an off-chain ECDSA signature with ecrecover, and producing that signature happens outside the EVM this library models — so testing it would need an off-chain signer, beyond the scope of this tutorial.