5 Repository layout🔗ℹ

private/            the specification

  lang.rkt          Redex grammar (machine, world, block, tx)

  interpreter.rkt   opcode semantics (step), CALL/CREATE/SELFDESTRUCT, run loop

  transaction.rkt   tx validation, intrinsic gas, refunds, tx-type parsing

  gas.rkt           gas schedule (EIP-2929 warm/cold, SSTORE, memory)

  state.rkt mem.rkt words.rkt   world/account, memory, 256-bit words

  forks.rkt         multi-fork config: fork order, EIP gates, opcode gating

  keccak.rkt hashes.rkt rlp.rkt mpt.rkt   crypto + encoding + Merkle-Patricia trie

  ec.rkt fields.rkt pairing.rkt bls.rkt   secp256k1 / bn254 / BLS12-381 / KZG

  precompiles.rkt   0x01-0x11 precompiled contracts

  native.rkt        optional native crypto accelerators (FFI) w/ pure fallback

                    (the run loop also carries current-frame-tracer, the hook

                     coverage tools are built on)

 

pbt/                property-based testing DSL (require evm-redex/pbt)

  property.rkt      define-evm-property / check- / run-

  vocab.rkt gen.rkt observation vocabulary + EVM-tuned generators

  execute.rkt deploy.rkt solc.rkt   deploy/run/call, artifact reader

 

asm/                the #lang evm-redex/asm language + programmatic API

  opcodes.rkt       canonical mnemonic <-> byte table

  parse.rkt assemble.rkt   assembler (labels, auto-PUSH) + disassembler

  execute.rkt       run assembled bytecode -> evm-result

  runtime.rkt lang/reader.rkt   the module language and its reader

 

sim/                the #lang evm-redex/sim transaction simulator + engine

  engine.rkt        the stateful chain (deploy / send / view / mine / diff)

  state-root.rkt block.rkt   state commitments; block-boundary processing

  abi.rkt receipt.rkt trace.rkt   revert/event decode, receipts, call/step traces

  parse.rkt runtime.rkt lang/reader.rkt   the scenario language and its reader

main.rkt            the whole specification (require evm-redex)

asm.rkt             assembler / runner as functions (require evm-redex/asm)

sim.rkt             the simulator engine as functions (require evm-redex/sim)

crypto.rkt          curve/field primitives (require evm-redex/crypto)

 

tests/              the whole test suite (raco test tests)

  unit/             focused rackunit suites (words, mpt, interp, precompiles, …)

  conformance/      state_test + blockchain_test harnesses, runner, and fixtures

  erc20/ erc721/ open-zeppelin/ …   worked property-based-testing examples

  web3bugs/         reproduction of real Code4rena bugs

  equivalence/ coverage/   differential-testing and coverage harnesses

  asm/examples/ sim/examples/   example #lang programs

  scribblings/      the test-suite documentation (testing.scrbl)

 

tutorial/           the step-by-step tutorial (EN + PT) and its runnable examples

  contracts/*.sol   Counter and Token, with their compiled *.json artifacts

  counter.rkt token.rkt explore.rkt   the tutorial's runnable code

  tutorial-en.scrbl tutorial-pt.scrbl  the two-language documents

 

flake.nix flake.lock  reproducible dev environment (Racket + all native libs)

shell.nix mcl.nix     non-flake dev shell / herumi-mcl build recipe

The test suites, worked examples, bundled conformance corpora, and the Web3Bugs reproduction benchmark live under "tests/" and are documented in The evm-redex test suite: tutorial, tests, and examples. }