1.1 A first program🔗ℹ

#lang evm-redex/asm

PUSH1 0x05

PUSH1 0x03

ADD

STOP

Running it prints:

outcome is the halt reason (stop, return, revert, out-of-gas, invalid-opcode, …); stack is the final stack, top element first, each a 256-bit word in hex; returndata is the bytes of a RETURN / REVERT.

1.2 The assembly dialect🔗ℹ

One instruction per token, one or more per line; mnemonics are case-insensitive. A ; begins a comment that runs to the end of the line.

Opcodes. Every opcode the interpreter implements is a mnemonic: ADD, MUL, SSTORE, JUMPI, KECCAK256, CALLDATALOAD, DUP1…DUP16, SWAP1…SWAP16, LOG0…LOG4, RETURN, REVERT, and so on. An unknown mnemonic is a compile error.

PUSH. Three forms:

• Explicit — PUSH1 0x05 … PUSH32 0x..: the operand is padded to exactly k bytes; an operand too wide for k is an error.

• Auto-sized — a bare PUSH with a literal chooses the minimal width: PUSH 0x1234 becomes PUSH2. (PUSH 0 is PUSH1 0x00; the zero-byte PUSH0 opcode is written PUSH0.)

• Label — PUSH name references a label (below) and is always emitted as PUSH2.

Operands are hexadecimal (0x..) or decimal.

Labels. A token name: defines a label at the current position; a bare name as a PUSH operand references it, and the assembler resolves it to that position’s program counter. This is how jumps are written without counting bytes:

#lang evm-redex/asm

.gas 100000

PUSH1 0x00        ; counter = 0

loop: JUMPDEST

PUSH1 0x01

ADD               ; counter += 1

DUP1              ; [counter, counter]

PUSH1 0x0a        ; [10, counter, counter]

GT                ; 10 > counter ?

PUSH loop         ; the JUMPDEST's pc, resolved for you

JUMPI             ; if so, loop

STOP              ; leaves 10 on the stack

Directives configure the run; they must come before any instruction:

• .gas N — the gas budget (default 30,000,000).

• .calldata 0x.. — the transaction calldata, for CALLDATALOAD / CALLDATASIZE / CALLDATACOPY.

#lang evm-redex/asm

.calldata 0x00000000000000000000000000000000000000000000000000000000000000ff

PUSH1 0x00

CALLDATALOAD      ; the first 32-byte word of calldata

PUSH1 0x00

MSTORE

PUSH1 0x20

PUSH1 0x00

RETURN            ; return memory[0..32)

Raw bytecode. If the source begins with 0x, the whole thing is taken as a hex bytecode blob — handy for pasting solc output and disassembling or running it as-is. (A mnemonic program never starts with 0x, so there is no ambiguity.)

#lang evm-redex/asm

0x6005600301

1.3 Using the result from other modules🔗ℹ

A #lang evm-redex/asm module provides three bindings, so another module can require it and inspect what the program did — this is how the example programs are tested:

• program-bytes — the assembled bytecode, a list of bytes.

• result — an evm-result (outcome, gas, stack, return data, and the final machine).

• final-machine — the final machine term, for reading anything else (memory, logs, world) with machine-field.

(require "arithmetic.rkt")

(evm-result-stack result)     ; => '(8)

program-bytes                 ; => '(96 5 96 3 1 0)

1.4 The programmatic API🔗ℹ

The same assembler, disassembler, and runner are available as ordinary functions through (require evm-redex/asm) — no #lang needed. This is what the language is built on, and what the unit tests exercise directly.

(define-values (code cfg) (assemble "PUSH1 0x05\nPUSH1 0x03\nADD\nSTOP"))

; code => '(96 5 96 3 1 0)

(disassemble (list 97 0 86 0))

; => "PUSH2 0x0056\nSTOP"