3 Library reference: the property-based testing DSL

9.3

Racket

3 Library reference: the property-based testing DSL🔗ℹ

The evm-redex/pbt library lets you validate properties of a fixed EVM program — a routine of opcodes or a whole contract/transaction — by running it through the semantics on many generated concrete inputs. You write the property as a Hoare-style contract (pre/post conditions), optionally with per-step invariants and revert/success obligations, and the engine searches for a counterexample, shrinking it to a minimal failing input.

This is property-based testing, so it is incomplete: it finds counterexamples, it does not prove their absence. In exchange it runs on concrete inputs and so places no restriction on the program — cryptographic precompiles, non-linear arithmetic and loops all simply execute. It builds on rackcheck (generation and shrinking) and Redex’s own redex-check.

This chapter documents every exported binding. For a hands-on, step-by-step walkthrough that applies the library to real Solidity contracts, read the tutorial in The evm-redex test suite: tutorial, tests, and examples first; this reference explains each piece it uses.

(require evm-redex/pbt)

3.1 Defining properties🔗ℹ

syntax
(define-evm-property name clause ...)

clause = #:code bytes
| #:call tx
| #:contract bytes
| #:address addr
| #:given ([x gen] ...)
| #:world world
| #:block block
| #:stack stack
| #:gas gas
| #:memory memory
| #:msg msg
| #:orig-storage store
| #:pre expr
| #:post proc
| #:invariant proc
| #:revert-when expr
| #:succeed-when expr
| #:fuel n
| #:trials n
| #:seed n

Binds name to an evm-property. The clauses fall into four groups.

Program (choose exactly one). #:code gives fragment mode: bytes is a list of opcode bytes, run from a fresh machine with run. #:call gives transaction mode: tx is built with make-tx and run with the full transaction machinery; pair it with #:world (a pre-state), or with #:contract and #:address to install a contract’s runtime code in a minimal world.

Inputs and setup. #:given lists the generated inputs; each x is bound (to a concrete value) in every other clause. In fragment mode the initial machine is configured with #:stack (top first), #:gas, #:memory, #:world, #:msg and #:orig-storage; in transaction mode the environment is #:world and #:block.

Obligations (any subset). #:pre is the Hoare antecedent over the inputs — when it is false the trial passes vacuously, so it gates the other obligations. #:post is (lambda (m0 m1) ....) in fragment mode or (lambda (w0 w1 result) ....) in transaction mode, where m0 / w0 is the pre-state (this is how you refer to “old” values) and result is a txn-run. #:invariant is a predicate checked at every step in fragment mode (via run-trace) and at the start/end boundary in transaction mode. #:revert-when / #:succeed-when demand that, under the given condition, the run reverts / succeeds.

Budget. #:fuel caps steps; #:trials sets the number of generated cases (default 1000); #:seed fixes the RNG for reproducibility.

(define-evm-property add-wraps
  #:code   (list 1)                     ; ADD
  #:given  ([a gen-word] [b gen-word])
  #:stack  (list a b)                   ; initial stack, top first
  #:gas    100
  #:post   (lambda (m0 m1) (= (stack-top m1) (u-add a b))))

struct
(struct evm-property (prop trials seed)
    #:transparent)
  prop : any/c
  trials : exact-nonnegative-integer?
  seed : (or/c #f exact-integer?)

The compiled property produced by define-evm-property. You normally pass it straight to a runner rather than inspecting its fields.

3.2 Running properties🔗ℹ

procedure
(check-evm-property p
[ #:trials trials
#:seed seed
#:deadline deadline]) → void?
  p : evm-property?
  trials : (or/c #f exact-nonnegative-integer?) = #f
  seed : (or/c #f exact-integer?) = #f
  deadline : (or/c #f real?) = #f

Runs p as a rackunit check, registering a pass or failure with the enclosing test suite. Use it inside a rackunit test module. The keyword arguments override the property’s own #:trials / #:seed; #:deadline is a wall-clock budget in seconds (default 60) — a contract-level check runs the full semantics per trial, so raise it when running many trials. Hitting the deadline yields an inconclusive 'timed-out, not a failure.

procedure
(run-evm-property p
[ #:trials trials
#:seed seed
#:deadline deadline]) → evm-result?
  p : evm-property?
  trials : (or/c #f exact-nonnegative-integer?) = #f
  seed : (or/c #f exact-integer?) = #f
  deadline : (or/c #f real?) = #f

The functional runner: instead of registering a rackunit check it returns an evm-result you can inspect programmatically. Use it to test the tester, or to react to a counterexample in code.

procedure
(evm-property-holds? p
[ #:trials trials
#:seed seed
#:deadline deadline]) → boolean?
  p : evm-property?
  trials : (or/c #f exact-nonnegative-integer?) = #f
  seed : (or/c #f exact-integer?) = #f
  deadline : (or/c #f real?) = #f

The boolean shortcut: #t when p passed all trials.

struct
(struct evm-result (status counterexample tests)
    #:transparent)
  status : (or/c 'passed 'falsified 'timed-out)
  counterexample : (or/c #f list?)
  tests : exact-nonnegative-integer?

The outcome of run-evm-property. counterexample is the shrunk list of generated argument values (in #:given order) when status is 'falsified, else #f. Because the seed and the shrunk inputs are recorded, a falsifying case is reproducible: feed the same inputs back through run-fragment / run-txn to re-observe the failure.

3.3 Worlds, accounts, and transactions🔗ℹ

A world is an association of addresses to accounts; an account is (list 'account nonce balance code storage transient), where code is a byte list and storage is an association of slot to value. Most of the time you obtain a world from deploy rather than writing one by hand.

procedure
(make-tx #:sender sender
#:gas-limit gas-limit
[ #:nonce nonce
#:to to
#:value value
#:data data
#:gas-price gas-price
#:max-fee max-fee
#:max-priority max-priority
#:access-list access-list
#:auth-list auth-list
#:blob-hashes blob-hashes
#:max-blob-fee max-blob-fee]) → any/c
  sender : exact-nonnegative-integer?
  gas-limit : exact-nonnegative-integer?
  nonce : exact-nonnegative-integer? = 0
  to : (or/c #f exact-nonnegative-integer?) = #f
  value : exact-nonnegative-integer? = 0
  data : (listof byte?) = '()
  gas-price : (or/c #f exact-nonnegative-integer?) = #f
  max-fee : exact-nonnegative-integer? = 0
  max-priority : exact-nonnegative-integer? = 0
  access-list : list? = '()
  auth-list : list? = '()
  blob-hashes : list? = '()
  max-blob-fee : exact-nonnegative-integer? = 0

Builds a transaction for #:call. #:to is the callee, or #f for a contract-creation transaction (with the init code in #:data). Set #:gas-price to 0 to avoid deducting a fee from the sender’s balance, which keeps value-conservation properties simple. The EIP-1559 (#:max-fee / #:max-priority), access-list, EIP-7702 authorization, and blob fields default to empty/zero.

procedure
(install-contract code addr [balance]) → list?
  code : (listof byte?)
  addr : exact-nonnegative-integer?
  balance : exact-nonnegative-integer? = 0

A one-line world holding a single account at addr with the given runtime code and balance. Handy for #:world when you want to skip deployment and test a known runtime directly.

value
DEFAULT-BLOCK : list?

The default block environment (number/timestamp 0, 30M gas limit, chain id 1, Prague fork) used when a property omits #:block.

3.4 Deploying contracts🔗ℹ

A Solidity contract compiles to two bytecodes: the creation (init) code, which runs the constructor and returns the runtime code, and the runtime (deployed) code that is stored at the address. Running the creation code is the faithful path — it applies constructor storage writes and patches immutables — whereas installing the runtime directly with #:contract skips the constructor.

procedure
(deploy creation
[ #:from from
#:value value
#:gas gas
#:nonce nonce
#:world world
#:block block]) → deploy-result?
  creation : (listof byte?)
  from : exact-nonnegative-integer? = DEFAULT-DEPLOYER
  value : exact-nonnegative-integer? = 0
  gas : exact-nonnegative-integer? = 30000000
  nonce : (or/c #f exact-nonnegative-integer?) = #f
  world : list? = '()
  block : list? = DEFAULT-BLOCK

Runs creation as a real contract-creation transaction and returns the post-deployment world with the runtime installed and all constructor effects applied. The created address is derived from #:from and the deployer’s #:nonce; deploy ensures the deployer exists with enough balance to cover #:value. Append ABI-encoded constructor arguments to creation before calling (see abi-encode).

(define art (read-artifact "storage/storage.json" #:contract "SimpleStorage"))
(define dep (deploy (artifact-creation art)))
(deploy-result-ok? dep) ; #t
(sload (deploy-result-world dep) (deploy-result-address dep) 0)

struct
(struct deploy-result (world address code ok? gas-used err)
    #:transparent)
  world : list?
  address : exact-nonnegative-integer?
  code : (or/c #f (listof byte?))
  ok? : boolean?
  gas-used : exact-nonnegative-integer?
  err : (or/c #f string?)

The result of deploy. On success ok? is #t and code is the installed runtime; on failure ok? is #f, code is #f and err carries a message. world is always the resulting world (unchanged from the input on failure).

3.5 Solidity artifacts and the ABI🔗ℹ

struct
(struct artifact (name creation runtime abi raw srcmap sources)
    #:transparent)
  name : (or/c #f string?)
  creation : (or/c #f (listof byte?))
  runtime : (or/c #f (listof byte?))
  abi : any/c
  raw : any/c
  srcmap : (or/c #f string?)
  sources : (or/c #f (listof string?))

The two bytecodes (and the parsed ABI) pulled from a build artifact. creation feeds deploy; runtime feeds #:contract.

srcmap is the runtime source map, verbatim, and sources the file list its indices refer to; both are #f unless the artifact was built with them. They are what lifts bytecode coverage to Solidity lines (see the coverage harness under "tests/coverage/"); nothing in the library itself reads them.

procedure
(read-artifact path [#:contract name]) → artifact?
  path : path-string?
  name : (or/c #f string?) = #f
procedure
(read-artifact/string str [#:contract name]) → artifact?
  str : string?
  name : (or/c #f string?) = #f

Read an artifact from a solc / Foundry / Hardhat JSON file (or string). Recognises Foundry (out/C.sol/C.json), Hardhat, solc –combined-json bin,bin-runtime,abi and solc –standard-json shapes. When the file holds several contracts, pass #:contract to select one by name (the part after the last : or /, or the whole key). Build the artifacts with the dev-shell toolchain, e.g. solc –combined-json bin,bin-runtime,abi Token.sol.

Add srcmap-runtime to that list if you want line-level coverage: solc –combined-json bin,bin-runtime,abi,srcmap-runtime Token.sol. It leaves the bytecode byte-for-byte identical — nothing else in a suite moves — and simply adds the map (and solc’s sourceList) to the JSON.

procedure
(function-selector sig) → exact-nonnegative-integer?
sig : string?

The 4-byte Contract-ABI selector for a function signature, i.e. the first four bytes of the Keccak-256 of sig, as an integer. (function-selector "transfer(address,uint256)") is 2835717307.

procedure
(encode-call sig arg ...) → (listof byte?)
sig : string?
arg : any/c

Full calldata for a call: the 4-byte function-selector of sig followed by abi-encode of the arguments. Use it for #:data.

(encode-call "transfer(address,uint256)" recipient amount)
; dynamic types too, matching the canonical Solidity vector:
(encode-call "sam(bytes,bool,uint256[])" (list 100 97 118 101) #t (list 1 2 3))

procedure
(abi-encode types values) → (listof byte?)
  types : (listof string?)
  values : list?
procedure
(abi-decode types bs) → list?
  types : (listof string?)
  bs : (listof byte?)

Encode / decode an argument tuple by ABI type strings, without a selector. abi-decode is the inverse of abi-encode and is what you use to read a getter’s return bytes. The supported types and the Racket values they map to:

uint<M> / int<M> (bare uint/int = 256), address — an integer (signed for int); bool — #t/#f (or 1/0).
bytes<M> (fixed, 1–32) and bytes (dynamic) — a byte list or a Racket bytes; string — a Racket string (or byte list).
T[] (dynamic) and T[k] (fixed) arrays — a list of element values; tuples (T1,...) — a list of the tuple’s element values.

procedure
(parse-arg-types sig) → (listof string?)
sig : string?

The argument type strings of a function signature — e.g. (parse-arg-types "transfer(address,uint256)") is '("address" "uint256"). Used internally by encode-call; exposed for building abi-encode / abi-decode type lists from a signature.

procedure
(hex->bytes s) → (or/c #f (listof byte?))
s : string?

Parse a hex string (with or without a 0x prefix, odd length tolerated) into a byte list; #f on a non-string.

3.6 Calling into a world🔗ℹ

A transaction discards a function’s return value, so transaction-mode #:post sees the world, outcome and logs but not the returned bytes. To read a getter or view function, use call, a raw frame execution that exposes the output.

procedure
(call world
addr
[ #:from from
#:value value
#:data data
#:gas gas
#:block block
#:static static?]) → call-result?
  world : list?
  addr : exact-nonnegative-integer?
  from : exact-nonnegative-integer? = DEFAULT-CALLER
  value : exact-nonnegative-integer? = 0
  data : (listof byte?) = '()
  gas : exact-nonnegative-integer? = 30000000
  block : list? = CALL-BLOCK
  static? : boolean? = #f

Runs a message call to addr at the frame level, with no transaction validation or gas charging, and returns the call’s outcome and return data. Set #:static to forbid state changes (a staticcall).

(define r (call world addr #:data (encode-call "total()")))
(call-result-outcome r) ; 'return | 'revert | ...
(car (abi-decode (list "uint256") (call-result-return r)))

struct
(struct call-result (outcome return world gas-left err logs)
    #:transparent)
  outcome : symbol?
  return : (listof byte?)
  world : list?
  gas-left : exact-nonnegative-integer?
  err : (or/c #f string?)
  logs : list?

outcome is 'return, 'stop, 'revert, 'out-of-gas, another exception tag, or 'error. return is the returned or reverted bytes (empty for 'stop); world is the post-call world (unchanged on a static call or revert); logs holds the events the call emitted, and is empty unless it succeeded — a reverted call emits none.

3.7 Lower-level execution🔗ℹ

define-evm-property builds on two run functions and their result structs. You can call them directly to reproduce a counterexample or to script an ad-hoc run.

procedure
(run-fragment code
[ #:stack stack
#:gas gas
#:memory memory
#:world world
#:msg msg
#:block block
#:tx tx
#:orig-storage orig
#:fuel fuel
#:trace? trace?]) → frag-run?
  code : (listof byte?)
  stack : list? = '()
  gas : exact-nonnegative-integer? = 1000000
  memory : list? = '()
  world : list? = '()
  msg : any/c = #f
  block : any/c = #f
  tx : any/c = #f
  orig : list? = '()
  fuel : exact-nonnegative-integer? = 1000000
  trace? : boolean? = #f

Runs a fixed opcode code fragment from a generated initial state (the engine behind fragment mode). With #:trace? it uses run-trace so per-step #:invariants can be checked.

procedure
(run-txn tx world block) → txn-run?
  tx : any/c
  world : list?
  block : list?

Runs a whole transaction against world (the engine behind transaction mode), wrapping process-transaction and catching an invalid-transaction error into a clean 'error outcome.

struct
(struct frag-run (pre post trace outcome err)
    #:transparent)
  pre : any/c
  post : any/c
  trace : (or/c #f list?)
  outcome : symbol?
  err : (or/c #f string?)

A fragment run. pre / post are the machine terms before and after; trace is the list of every intermediate machine (when #:trace? was set) else #f; outcome is the halt tag ('stop, 'return, 'revert, an exception tag, or 'error).

struct
(struct txn-run (world0 world1 ok? gas-used logs outcome err)
    #:transparent)
  world0 : list?
  world1 : list?
  ok? : boolean?
  gas-used : exact-nonnegative-integer?
  logs : list?
  outcome : (or/c 'success 'revert 'error)
  err : (or/c #f string?)

A transaction run. world0 / world1 are the pre- and post-states; ok? and outcome classify the result; gas-used and logs are the consumed gas and emitted logs. This is the result passed to a transaction-mode #:post.

procedure
(machine-with-field m tag arg ...) → any/c
  m : any/c
  tag : symbol?
  arg : any/c
value
CALL-BLOCK : list?

machine-with-field functionally overrides one field (by its tag, e.g. 'stack) of a machine term. CALL-BLOCK is the default block environment used by call.

3.8 Observation vocabulary🔗ℹ

Pure readers for #:pre / #:post / #:invariant bodies. All are total on well-formed machines / worlds.

3.8.1 Machine fields🔗ℹ

procedure
(pc m) → exact-nonnegative-integer?
  m : any/c
procedure
(gas m) → exact-nonnegative-integer?
  m : any/c
procedure
(the-stack m) → list?
  m : any/c
procedure
(mem-of m) → any/c
  m : any/c
procedure
(code-of m) → list?
  m : any/c
procedure
(world-of m) → list?
  m : any/c
procedure
(return-data m) → list?
  m : any/c
procedure
(logs-of m) → list?
  m : any/c
procedure
(refund-of m) → exact-integer?
  m : any/c
procedure
(halt-of m) → any/c
  m : any/c

Read the corresponding field of a machine m: program counter, remaining gas, the stack (top first), memory, code, world, return data, logs, gas-refund counter, and the raw halt value.

3.8.2 Stack🔗ℹ

procedure
(stack m i) → exact-nonnegative-integer?
  m : any/c
  i : exact-nonnegative-integer?
procedure
(stack-top m) → exact-nonnegative-integer?
  m : any/c
procedure
(stack-depth m) → exact-nonnegative-integer?
  m : any/c
procedure
(stack-empty? m) → boolean?
  m : any/c

(stack m i) is the ith word from the top ((stack-top m) = (stack m 0)).

3.8.3 Outcome🔗ℹ

procedure
(running? m) → boolean?
  m : any/c
procedure
(halted? m) → boolean?
  m : any/c
procedure
(stopped? m) → boolean?
  m : any/c
procedure
(returned? m) → boolean?
  m : any/c
procedure
(reverted? m) → boolean?
  m : any/c
procedure
(out-of-gas? m) → boolean?
  m : any/c
procedure
(exception? m) → boolean?
  m : any/c
procedure
(halt-tag m) → symbol?
  m : any/c

Classify a machine’s halt status. halt-tag returns the leading symbol of the halt value ('running, 'stop, 'return, 'revert, or an exception tag); exception? is true for any tag in EXN-TAGS.

value
EXN-TAGS : (listof symbol?)

The exceptional halt tags: 'out-of-gas, 'stack-underflow, 'stack-overflow, 'invalid-opcode, 'invalid-jump, 'out-of-bounds, 'stack-depth-limit, 'write-in-static.

3.8.4 Return data and memory🔗ℹ

procedure
(return-bytes m) → (listof byte?)
  m : any/c
procedure
(return-word m) → exact-nonnegative-integer?
  m : any/c
procedure
(return-size m) → exact-nonnegative-integer?
  m : any/c
procedure
(mem-word m off) → exact-nonnegative-integer?
  m : any/c
  off : exact-nonnegative-integer?
procedure
(mem-byte m off) → byte?
  m : any/c
  off : exact-nonnegative-integer?
procedure
(mem-bytes m off len) → (listof byte?)
  m : any/c
  off : exact-nonnegative-integer?
  len : exact-nonnegative-integer?
procedure
(memory-size m) → exact-nonnegative-integer?
  m : any/c

return-word reads the (first 32 bytes of the) return data as a word; mem-word reads 32 bytes at off as a word. The mem-* readers zero-extend past the current memory size.

3.8.5 World, accounts, and storage🔗ℹ

procedure
(account-of world addr) → list?
  world : list?
  addr : exact-nonnegative-integer?
procedure
(exists? world addr) → boolean?
  world : list?
  addr : exact-nonnegative-integer?
procedure
(balance-of world addr) → exact-nonnegative-integer?
  world : list?
  addr : exact-nonnegative-integer?
procedure
(nonce-of world addr) → exact-nonnegative-integer?
  world : list?
  addr : exact-nonnegative-integer?
procedure
(code-at world addr) → (listof byte?)
  world : list?
  addr : exact-nonnegative-integer?
procedure
(storage-at world addr) → list?
  world : list?
  addr : exact-nonnegative-integer?
procedure
(empty-account? world addr) → boolean?
  world : list?
  addr : exact-nonnegative-integer?
procedure
(sload world addr key) → exact-nonnegative-integer?
  world : list?
  addr : exact-nonnegative-integer?
  key : exact-nonnegative-integer?

Read an account and its fields out of a world. sload reads storage slot key of addr (0 when unset) — the workhorse for asserting on contract state without going through a getter.

procedure
(m-balance m addr) → exact-nonnegative-integer?
  m : any/c
  addr : exact-nonnegative-integer?
procedure
(m-nonce m addr) → exact-nonnegative-integer?
  m : any/c
  addr : exact-nonnegative-integer?
procedure
(m-sload m addr key) → exact-nonnegative-integer?
  m : any/c
  addr : exact-nonnegative-integer?
  key : exact-nonnegative-integer?
procedure
(m-storage-at m addr) → list?
  m : any/c
  addr : exact-nonnegative-integer?

The same world readers relative to a machine’s current world — convenient inside a fragment-mode #:invariant or #:post.

3.8.6 Constants🔗ℹ

value
UINT256-MAX : exact-nonnegative-integer?
value
WORD-MOD : exact-nonnegative-integer?

2^256 - 1 and 2^256 — the maximum word and the wrap-around modulus.

3.9 Generators🔗ℹ

EVM-tuned, edge-biased, shrinkable rackcheck generators for #:given. Edge bias matters: bugs cluster at 0, 1, 2^255, MAX-U256 and byte/word boundaries, so the defaults sample those heavily while still covering the uniform range.

value
gen-word : gen?
value
gen-word-edge : gen?
value
gen-word-small : gen?
value
gen-word-uniform : gen?
procedure
(gen-word-in lo hi) → gen?
lo : exact-nonnegative-integer?
hi : exact-nonnegative-integer?

256-bit word generators. gen-word is the balanced default (edges + small + a uniform tail); gen-word-edge draws only boundary values, gen-word-small only 0–255, gen-word-uniform uniformly over the whole range. gen-word-in draws uniformly from an inclusive range — the idiom for satisfying a precondition by construction (e.g. an amount in (gen-word-in 0 balance)) instead of a strict #:pre that discards samples.

value
gen-byte : gen?
procedure
(gen-bytes [#:max-length n]) → gen?
n : exact-nonnegative-integer? = 64
value
gen-address : gen?

A byte, a variable-length byte list, and a 160-bit address (edge-biased).

procedure
(gen-stack [#:max-depth depth]) → gen?
depth : exact-nonnegative-integer? = 8
procedure
(gen-stack-of k) → gen?
k : exact-nonnegative-integer?
value
gen-gas : gen?

gen-stack draws up to depth words; gen-stack-of exactly k. gen-gas is biased toward small/tight budgets so runs actually reach out-of-gas.

procedure
(gen-store [#:max-entries n]) → gen?
  n : exact-nonnegative-integer? = 6
procedure
(gen-account [#:code code]) → gen?
  code : (listof byte?) = '()
procedure
(gen-world-with contract
addr
[ #:storage storage
#:caller caller
#:caller-balance caller-balance]) → gen?
  contract : (listof byte?)
  addr : exact-nonnegative-integer?
  storage : gen? = (gen-store)
  caller : exact-nonnegative-integer? = 0
  caller-balance : gen? = gen-word

Storage, account, and world generators. gen-store uses a small key space so collisions are likely; gen-world-with generates a world holding contract at addr (with generated storage) plus a funded caller — useful for exercising a runtime directly without deployment.

value
gen-selector : gen?
procedure
(gen-calldata [#:max-args max-args]) → gen?
  max-args : exact-nonnegative-integer? = 3
procedure
(abi selector arg ...) → (listof byte?)
  selector : (listof byte?)
  arg : any/c

Calldata generators: a random 4-byte gen-selector and gen-calldata (selector + word-args). abi assembles calldata from an explicit selector and word arguments (each padded to 32 bytes).

All of rackcheck’s combinators (gen:integer-in, gen:one-of, gen:map, gen:frequency, gen:tuple, …) are re-exported, so you can build custom generators inline.

3.10 Running the DSL’s own tests🔗ℹ

The DSL’s tests — correct properties passing, buggy ones falsified and shrunk, each clause form, a transaction property, reproducibility by seed — live under "tests/pbt/":

; raco test tests/pbt/

1	#lang evm-redex/ asm — writing and running EVM assembly
2	#lang evm-redex/ sim — simulating transactions
3	Library reference: the property-based testing DSL
4	Tracing hook
5	Repository layout

3.1	Defining properties
3.2	Running properties
3.3	Worlds, accounts, and transactions
3.4	Deploying contracts
3.5	Solidity artifacts and the ABI
3.6	Calling into a world
3.7	Lower-level execution
3.8	Observation vocabulary
3.9	Generators
3.10	Running the DSL’s own tests