Lockstep: the project explained from zero

This folder explains the whole project for someone who has never touched compilers or WebAssembly. Read the files in order. Each one is short and builds on the one before.

If a word confuses you, check the glossary first.

The detailed day-by-day record (with every number and the exact run IDs) is notes/logbook.md. This guide explains the ideas; the logbook is the evidence.

1. The big picture

The problem in one paragraph

WebAssembly (Wasm for short) is a way to run fast programs inside a web browser and on servers. Games, design tools like Figma and video editors use it. The exact rules for how WebAssembly behaves are written in an official document called the specification (or "spec"). Since 2025 that spec is written in a special language called SpecTec, so a computer can read it, not just people. SpecTec can even run WebAssembly programs straight from the rules, but it does that very slowly, because it reads the rules step by step for every single instruction. Real engines (the ones in Chrome or Firefox) are fast, but people write them by hand, separately from the rules, so they can disagree with the spec and need to be updated by hand whenever the spec changes.

The board game analogy

Think of a board game with a thick rulebook.

• Option A, the referee: someone who looks up the rulebook for every single move. Always right, but painfully slow. That's SpecTec's built-in interpreter.
• Option B, the hand-made version: a programmer who read the rulebook once and wrote their own fast version of the game. Fast, but they might have misread a rule, and every time the rulebook changes they have to fix their version by hand. That's a hand-written engine.
• Option C, this project: a machine that reads the rulebook and writes the fast version automatically. It's correct because it comes straight from the rules, and when the rules change you just run the machine again.

That machine is a compiler. The project's name, Lockstep, means the engine moves in lockstep (perfectly in sync) with the rulebook.

What was built

1. A compiler: a new part added to SpecTec, called with spectec --rust. It reads all 474 algorithms in the WebAssembly 3.0 spec and writes about 22,000 lines of Rust code. The compiler itself is upstream/spectec/src/backend-rust/gen.ml (about 700 lines of OCaml).
2. A runtime: about 4,900 lines of hand-written Rust in gen-engine/src/ that the generated code runs on top of: values, numbers, the "machine" the spec describes, math helpers and the test runner. This part is general: it doesn't contain any WebAssembly instruction rules, those all come from the spec.
3. A test front end: dump.ml reuses SpecTec's own parser so the official test files can be fed to the engine.
4. Measurement tools: scripts in bench/ that time the engines fairly and count memory allocations.

The results so far

• Correct: the generated engine passes 55,861 out of 55,861 official WebAssembly tests (all 259 test files), exactly the same results as SpecTec's own interpreter, file by file.
• Fast compared to SpecTec: about 45 times faster on 8 benchmark programs (it started at 28x before the optimizations), and 6.8x faster on the whole test suite.
• Not yet as fast as a hand-written engine: about 3.5 times slower than the official hand-written OCaml "reference interpreter" (it started at 5.6x).
• Optimizations: 7 speed-ups so far, each one re-checked against all 55,861 tests. Together they made the engine about 1.7x faster and cut memory use on one test from 2.84 GB to 35 MB.

All speed numbers are preliminary because the server they ran on was busy with other jobs. See 07-measuring-speed.md.

Why it matters

• One source of truth. Today the rulebook and the engines are separate things that humans keep in sync. Here, the engine is the rulebook, translated.
• New features faster. When someone adds a feature to the spec, the engine gets it by re-running the compiler.
• A faster official reference. The people who write the standard need to run tests against the spec. A fast, faithful engine makes that practical.

Next: 02-webassembly-and-spectec.md

2. WebAssembly, the spec, SpecTec and AL

What is WebAssembly?

When you write a program in C, C++ or Rust, a compiler can turn it into WebAssembly: a list of very simple instructions like "push the number 5", "add the top two numbers", "jump back to the start of this loop". A browser then runs those instructions. It's like a tiny, safe, made-up computer that every browser agrees on.

WebAssembly is a stack machine. Instead of naming places to store numbers, most instructions work on a stack (a pile) of values:

i32.const 2     ;; pile: [2]
i32.const 3     ;; pile: [2, 3]
i32.add         ;; takes 2 and 3 off the pile, puts 5 back: [5]

i32 means "32-bit integer". Other types are i64, f32, f64 (decimal numbers), v128 (128-bit vectors for SIMD, doing math on many numbers at once) and references (pointers to functions or objects).

Programs also use: - locals: a function's own variables (local.get 0 reads variable 0) - blocks and loops: block, loop, and br ("branch", which means jump) to leave a block or restart a loop - calls: call 3 runs function 3 - memory: a big array of bytes the program can read and write (i32.load, i32.store)

What is a specification?

The specification is the official rulebook. For every instruction it says exactly what happens, including the weird cases (dividing by zero must "trap", which means stop with an error; adding two i32s wraps around at 2^32; and so on). Every engine must follow it.

What is SpecTec?

SpecTec is a language made for writing specs like this one. The WebAssembly spec is written in SpecTec files (upstream/specification/wasm-latest/*.spectec). From those files, SpecTec can produce:

• the human-readable spec document (the website and PDF)
• AL, which stands for "algorithmic language"
• other outputs for proof tools

What is AL?

AL turns the spec's math-style rules into step-by-step algorithms, like a recipe. Here's the real AL for br_if ("branch if"):

Step_pure/br_if l {
  Assert (top_value(I32))          -- check there's an i32 on the stack
  Pop (I32.CONST c)                -- take it off, call it c
  If ((c =/= 0)) {                 -- if c is not zero...
    Execute (BR l)                 -- ...do the instruction "br l"
  }
  Else { Nop }                     -- otherwise do nothing
}

There are 474 of these algorithms: one per instruction, plus helpers like $binop_ (the math for binary operators) and $local (read a local variable), plus the algorithms for setting up a module (instantiate) and calling a function (invoke).

AL has about 13 kinds of statements (Assert, Let, Pop, Push, If, Execute, Enter, Exit, Trap, Return, ...). That small number is what makes translating it to another language possible.

What is the meta-interpreter, and why is it slow?

SpecTec includes an interpreter for AL written in OCaml (upstream/spectec/src/backend-interpreter/). It reads the AL algorithms as data and walks through them one statement at a time. It's called a "meta-interpreter" because it interprets the spec, which itself describes an interpreter. It's two layers of interpretation.

Why it's slow: 1. Every step is looked up. To run br_if it finds the br_if algorithm, then for every statement inside it, it looks at what kind of statement it is and what expression it contains, every time. 2. Every value is a generic tree. The number 5 isn't stored as a plain number; it's a tree like CONST(I32, 5), made of general-purpose pieces. 3. It follows the spec's abstract machine literally. For example, every time a loop repeats, the spec says "copy the loop's body into a new label". The meta-interpreter really copies it. 4. Loading the spec takes 31 to 34 seconds before it can run anything.

On a simple counting loop, the meta-interpreter takes about 440 microseconds per loop iteration (about 11 instructions). Production engines are expected to be thousands of times faster than that, though this project hasn't measured them yet.

The other engine you'll hear about: the reference interpreter

The WebAssembly team also keeps a hand-written interpreter in OCaml, called the reference interpreter (upstream/interpreter/, shortened to "refint" in this project). It's written for clarity, not speed, but it's still far faster than the meta-interpreter. It's the main speed target: the project's stretch goal is to get within 2x of it.

Important detail: this project uses the reference interpreter's parser and validator to read test files (the "front end"), but never to execute anything. All execution is done by the generated code.

Next: 03-kill-test.md

3. The kill test (deciding if the project was worth it)

Before spending months on a project, it's smart to spend one week trying to "kill" it: test the riskiest assumptions first, and stop if they fail. The plan is in KILLTEST.md, and the results are in notes/logbook.md.

The two questions

1. Can the AL be translated to Rust mechanically? That means by following fixed rules for each statement kind, without inventing new logic per instruction. If every instruction needed special hand-written tricks, a compiler couldn't do it automatically.
2. Is a naive translation at least 10 times faster than the meta-interpreter? If not, the whole idea isn't worth it.

The decision rule (written before running anything)

• Kill if more than about 3 of the ~15 instructions needed logic that isn't in the AL, or the speedup was under 10x.
• Proceed if the translation was mechanical and the speedup was at least 10x.

Writing the rule before the experiment matters: it stops you from moving the goalposts after seeing the results.

What was done

• A benchmark (bench/kill.wast) with count(n) (a loop that counts to n) and fib(n) (recursive Fibonacci), plus a few extra functions so all ~15 instructions are used: i32 add/sub/mul, eqz, lt_s, local.get/set/tee, block, loop, br, br_if, call, return and drop.
• A hand translation (engine/, written in Rust): the 16 AL algorithms those instructions need, translated statement by statement. The rules used for each statement kind are in notes/translation.md.
• Timing of both on the same inputs, 5 runs each.

Results

• Logic not in the AL: 0 of ~15 instructions. Everything that had to be written by hand was shared runtime (the stack of contexts, the run loop, how big integers are stored), and all of that comes from the meta-interpreter's own OCaml code, not invented.
• Speed:

Decision: proceed. Both conditions passed easily.

What this did and didn't show

It showed that most of the meta-interpreter's slowness comes from interpreting the AL, not from the AL's abstract machine itself. But this hand translation was small and hand-written. The real project had to:

• write a compiler that produces the translation automatically for all 474 algorithms, not 16
• support the whole language: floats, SIMD, memory, tables, garbage-collected structs and arrays, exceptions
• pass the official test suite

Note that the full generated engine is slower per instruction than this small hand translation. The generated engine uses one general value type for everything (to handle the whole language), while the kill test's hand translation used plain Rust integers. That's why the full engine is "only" ~45x faster than the meta-interpreter instead of ~600-1000x. Closing that gap is the optimization work in 08-optimizations.md.

Next: 04-the-compiler.md

4. The compiler (gen.ml)

Where it lives and how it runs

The compiler is one OCaml file inside SpecTec: upstream/spectec/src/backend-rust/gen.ml. SpecTec already had several "backends" (things that take the spec and produce some output, like the document or the interpreter). This project adds a new one. You run it with:

./spectec ../specification/wasm-latest/*.spectec --rust OUT.rs

gen-engine/regen.sh does this for you: it rebuilds SpecTec and writes gen-engine/src/spec.rs. Never edit spec.rs by hand. It's regenerated every time, so any change must be made in gen.ml.

The main idea: one Rust function per AL algorithm

Each of the 474 algorithms becomes one Rust function: - instruction algorithms (like BR_IF) become r_BR_IF ("r" for rule) - helper functions (like $binop_) become a_binop_ ("a" for algorithm)

Every function has the same shape:

pub fn r_BR_IF(cx: &mut Cx, args: &[Value]) -> Res<Option<Value>>

• cx is the machine state (the stack of contexts and the store; see 05-the-runtime.md)
• args are the algorithm's arguments
• the result is either a returned value (Some), nothing (None), or an error/trap (Err)

A real example: br_if

The AL (from the spec):

Step_pure/br_if l {
  Assert (top_value(I32))
  Pop (I32.CONST c)
  If ((c =/= 0)) { Execute (BR l) }
  Else { Nop }
}

The generated Rust (from spec.rs, with comments added here):

pub fn r_BR_IF(cx: &mut Cx, args: &[Value]) -> Res<Option<Value>> {
  let mut v_c: Value = Value::Bool(false);        // every AL variable gets a Rust variable
  let mut v_l: Value = Value::Bool(false);
  if args.len() != 1 { return err(...); }          // same check the meta-interpreter does
  let __p444 = args[0].clone();
  v_l = __p444.clone();                            // the parameter l

  // Assert (top_value(I32))
  if !rt::is_true(&Value::Bool(cx.value_stack_len() > 0)) { return err("assertion fail: top_value(I32)"); }

  // Pop (I32.CONST c): pop a value and check it really is CONST(I32, c)
  let __x445 = cx.pop_value()?;
  let __a446: Rc<[Value]> = match &__x445 { Value::Case(t, a) if *t == Tag(2) && a.len() == 2 => a.clone(), _ => { return err(...); } };
  let __x447 = __a446[0].clone();
  let __a448: Rc<[Value]> = match &__x447 { Value::Case(t, a) if *t == Tag(3) && a.len() == 0 => a.clone(), _ => { return err(...); } };
  let __x449 = __a446[1].clone();
  v_c = __x449.clone();                            // c

  // If ((c =/= 0)) { Execute (BR l) } Else { Nop }
  if rt::is_true(&rt::ne(&v_c.clone(), &Value::Num(Num::Nat(Z::S(0i128))))?) {
    let __v450 = Value::Case(Tag(21), Rc::new([v_l.clone()]));   // build the instruction BR l
    cx.execute(__v450)?;                                           // run it
  } else {
  }
  Ok(None)
}

Things to notice: - Statement for statement. Each AL line becomes a few Rust lines in the same order. That's the "mechanical" translation the kill test checked. - Tags. Constructor names like CONST, I32 and BR become numbers (Tag(2), Tag(3), Tag(21)) so comparing them is fast. The list of names is at the top of spec.rs (TAGS). - Names like __x445 are temporary variables the compiler makes up. The numbers just keep them unique. - It's not pretty, and that's fine. Nobody reads spec.rs day to day. What matters is that it's faithful and the Rust compiler can optimize it.

The parts of gen.ml

Reading the file top to bottom:

1. Output helpers (emit, nest): write lines of Rust with the right indentation.
2. Names (mangle, var, func_name, rule_name, tag): turn AL names into valid Rust names. AL allows names like instr'*; Rust doesn't, so ' becomes _Q and * becomes _S (so instr* is v_instr_S).
3. Deciding what a call means (builtin_of, inverse_of, numerics_fn): when the AL calls $f(...), the meta-interpreter decides at run time whether f is another AL algorithm, a built-in math function (numerics), or a special "relation" (like validation). The compiler makes that decision once, ahead of time, and emits a direct call. This is part of why the compiled code is faster.
4. Expressions (ce, "compile expression"): turns an AL expression into a Rust expression that produces a Value. Examples: a + b becomes rt::add(&a, &b)?, a list [a, b] becomes Value::list(vec![a, b]), a record field e.FIELD becomes rt::access(&e, &rt::P::Dot(Tag(..)))?.
5. Calls (call): emits a_f(cx, &[args]) for AL functions, crate::numerics::f::name(&[args]) for math built-ins, and crate::relation::call(...) for relations.
6. Patterns (assign): AL's Let and Pop can unpack values, like Pop (I32.CONST c) above. assign emits the Rust that checks the shape and pulls out the parts, or fails with "invalid assignment" (the same error the meta-interpreter gives).
7. Statements (stmt): one case per AL statement kind (If, Assert, Push, Pop, Let, Trap, Return, Execute, Enter, Exit, Replace, Append, ...).
8. The tail rule (instrs and enters_contexts): the trickiest part. When an AL algorithm says Execute (some instruction) and that's not its last statement, the instruction (and everything it starts) has to finish before the next statement. The compiler emits let d = cx.depth(); ...; cx.run(d)?; around it. When it is the last statement, the work is left for the main loop instead, which keeps the Rust stack from growing on every loop iteration. This rule comes from how the meta-interpreter works (its "Wasm n" counter).
9. Purity analysis and reuse (effects_of, compute_effects, bind_counts, plan_memos): added for optimization v5. It finds functions whose result depends only on their arguments, and reuses their results inside one algorithm. See 08-optimizations.md.
10. Putting it together (gen_algo, gen_file): writes every algorithm, then two dispatch functions:
    • run_algo(cx, tag, args): "run the algorithm for this instruction", used when the machine executes an instruction
    • call_func(cx, name, args): "call a function by its name", used for calls that can't be resolved ahead of time (functions passed as arguments)

The other OCaml file: dump.ml (the test front end)

The official tests are .wast files: WebAssembly modules plus commands like "call function fib with 10 and check the answer is 55". The engine doesn't parse .wast itself. Instead, dump.ml uses SpecTec's existing code (which uses the reference interpreter's parser and validator) to convert each .wast file into a .al file: one AL value per line, in a simple text format described in gen-engine/FORMAT.md. The engine then reads those .al files.

Why do it this way? Parsing and validation aren't what this project is about, and reusing SpecTec's own front end guarantees both engines see exactly the same modules. Validation (checking a module is well-formed, $Module_ok) is computed ahead of time by the reference validator and stored in the dump.

Next: 05-the-runtime.md

5. The runtime (gen-engine/src/)

The generated code (spec.rs) can't run alone. It needs a library of basic pieces: what a value is, how numbers work, what the machine looks like, how to read test files. That's the runtime. It's hand-written, but it's general: none of it describes a WebAssembly instruction. All the instruction rules come from the spec through spec.rs.

Total: about 4,900 hand-written lines plus about 22,000 generated lines.

value.rs: what a value is

In AL, everything is a value: a number, a list, a record, a constructor like CONST(I32, 5), and so on. In Rust that's one big type, Value, with one variant per kind:

Sharing (Rc). Copying a big list every time it's passed around would be slow, so values use Rc ("reference counted"): copying a value just copies a pointer and adds 1 to a counter. The memory is freed when the counter reaches 0. This mirrors OCaml, where values are shared by default.

Changing in place (RefCell). Some lists and record fields are updated in place by the spec (for example, writing to a local variable or to memory). RefCell allows that safely. This matches the meta-interpreter, where lists are OCaml arrays that can be modified.

Tags. Constructor names (CONST, I32, ...) are stored as small numbers (Tag). value.rs has the table that maps numbers back to names (tag_name), used for error messages.

Errors (Exn, Res). Trap (the Wasm program did something illegal, like dividing by zero), Fail (an AL branch didn't apply, used for "try this, otherwise that"), Throw (Wasm exceptions), OutOfMemory, Exhaustion, Invalid, and Error (a bug or something unsupported).

num.rs: numbers

The spec does math with ideal numbers: natural numbers (0, 1, 2, ...), integers (..., -1, 0, 1, ...), fractions and real numbers, all with no size limit. A 64-bit multiplication can produce a 128-bit intermediate result, and the spec then wraps it.

• Z is an integer: stored as a fast 128-bit number (i128) when it fits, and switched to an unlimited "big integer" (BigInt) only when it doesn't. Almost every number fits, so this is fast.
• Num is Nat, Int, Rat (fraction) or Real, with the same rules as SpecTec's xl/num.ml (for example, subtracting two Nats that would go negative is an error).

ctx.rs: the machine

The spec describes an abstract machine. The runtime keeps its state in Cx:

• store: everything a running program owns (functions, memories, tables, globals, ...), as one big record
• ctxs: a stack of contexts. A context is one of:
  • a frame (FRAME_): one per function call, holding its locals
  • a label (LABEL_): one per block or loop you're inside
  • a handler (HANDLER_): for exception handling

Each context has its own value stack (the pile of numbers) and its own list of instructions still to run.

Key operations: - push_value, pop_value: put values on and take them off the pile - push_context, pop_context: enter and exit a block, loop or function - current_context(FRAME_): find the nearest frame, used by $local to find local variables - execute(instr): run one instruction. A CONST just gets pushed; anything else calls its algorithm through run_algo. - run(depth): the main loop. It keeps taking the next instruction from the top context and executing it, until the stack of contexts is back down to depth.

Since v3, a context doesn't copy its instruction list. It keeps a pointer to the shared list plus a position (seq + pc). See 08-optimizations.md.

rt.rs: expression operations

Everything the generated code needs to compute expressions: - arithmetic and comparisons on Values (add, sub, lt, eq, ...) - lists (cat joins two lists, len, make_list builds n copies) - reading inside values (access: list index, list slice, record field) - updating inside values (upd, ext, replace_idx, replace_slice, replace_dot, append) - AL-specific operations: choose (pick from a set), is_case_of, has_type ("is this value an i32 type?"), is_valid

These are ports of the meta-interpreter's eval_expr, so they behave the same way, including the same error cases.

numerics.rs: the math built-ins

Some spec functions aren't written as AL algorithms but as built-ins: floating-point math (fadd, fsqrt, fmin with all the NaN rules), bit operations (iand, ishl, ipopcnt), conversions (trunc, convert, reinterpret), and converting numbers to and from bytes (ibytes, nbytes). This file is a port of SpecTec's OCaml numerics.ml and fxx.ml (about 2,200 lines). Since v2, a macro table lets the generated code call each one directly.

relation.rs: the few hand-written rules

The meta-interpreter also handles a few "relations" by hand rather than from the AL. This file does the same: - Module_ok (is the module valid?): precomputed when the test was dumped - Expand (unfold a recursive type): uses the spec's own $unrolldt function - Ref_ok, Val_ok, Externaddr_ok and the subtyping checks: ported from the reference interpreter's valid/match.ml

host.rs: the test host

The official tests import a few functions from a fake module called spectest (like print_i32). This file implements them.

reader.rs: reading .al dump files

Parses the text format from gen-engine/FORMAT.md back into Values.

runner.rs: running the tests

Goes through a dump file line by line and does what each command says: define a module, register it under a name, call a function and check the result (assert_return), check that something traps (assert_trap), and so on. It compares results the same way SpecTec's runner does (including special cases like "any NaN is fine here"). It measures the CPU time of each command and prints the total (FILE took X ms.).

main.rs

Starts everything. It runs the engine on a thread with a 4 GB stack, because the generated code uses one Rust function call per Wasm call, so deeply recursive Wasm programs need a deep Rust stack.

allocs.rs (only in measurement builds)

A counting memory allocator. It counts every time the engine asks for new memory. It's only compiled in when you build with --features count-allocs, so it never slows down the normal build. See 07-measuring-speed.md.

spec.rs

The generated code. About 22,000 lines. Regenerate it with gen-engine/regen.sh; don't edit it by hand.

Next: 06-testing.md

6. Testing: how we know the engine is correct

A fast engine is worthless if it gives wrong answers. Correctness is checked first, and re-checked after every single optimization.

The official test suite

The WebAssembly project publishes an official test suite: upstream/test/core, 259 .wast files. Each file defines some WebAssembly modules and then gives commands, for example:

(assert_return (invoke "fib" (i32.const 10)) (i32.const 55))   ;; calling fib(10) must return 55
(assert_trap (invoke "div" (i32.const 1) (i32.const 0)) "integer divide by zero")

The suite covers everything in WebAssembly 3.0: integer and float math, memory, tables, SIMD, garbage-collected structs and arrays, exceptions, tail calls and so on.

The correctness rule

The engine must get exactly the same result as SpecTec's own meta-interpreter on every test file. Not "about the same", not "most files". Every file must have the same number of passed tests out of the same total.

Since the meta-interpreter is the spec running, matching it file by file is the strongest check available.

What counts as a test (read this carefully)

To be honest about the number 55,861:

• It counts every command that SpecTec's own test runner executes. Our runner (gen-engine/src/runner.rs) follows SpecTec's runner (backend-interpreter/runner.ml) exactly.
• SpecTec's runner skips 11 long-running files: memory_copy, memory_copy64, memory_fill, memory_fill64, memory_grow, memory_grow64, call_indirect, call_indirect64, return_call, return_call_indirect and return_call_ref. They're too slow for the meta-interpreter, so they count as 0 tests in both engines. Running them is a good next step now that the engine is faster.
• Some command kinds are skipped by both, like assert_malformed (checking the parser rejects broken text), assert_unlinkable and assert_exhaustion (checking the program runs out of stack).

So the precise claim is: "Lockstep passes all 55,861 commands that SpecTec's reference runner executes on the 259 files of the official core test suite, with identical results per file." Say it like that to experts. For non-experts, "100% of the official tests SpecTec runs" is fine.

How a test run works, step by step

1. Dump (gen-engine/dump-all.sh, about 47 seconds for all files): SpecTec reads each .wast file and writes a .al file into gen-engine/target/dumps/. One spec load for all files.
2. Run (gen-engine/run-all.sh): runs the engine once per .al file, so if one file crashes it only loses that file. It saves each file's output and writes target/results/summary.csv (file, passed, total, CPU time, status). It also catches crashes and timeouts (10 minutes per file).
3. Compare (gen-engine/compare.py): joins our results with the saved output of SpecTec running the same files (target/baseline/stderr.txt) into one table.
4. Check (gen-engine/check.sh): does steps 2 and 3, then prints how many files differ. The answer has to be 0.

For the optimization versions, bench/check-variants.sh NAME... runs check.sh on each saved version and keeps the results in gen-engine/target/variants/NAME-check.txt.

Results

(v3's first run had call.wast killed because the server ran out of memory; that was the memory problem v7 later fixed. Run alone, it passed 90/90.)

Why this level of testing matters for the optimizations

Every optimization changes how the engine works internally. The claim is that they are meaning-preserving: the engine computes exactly the same results, just faster. Each rewrite comes with a reason why it's safe (see 08-optimizations.md), and then the full test suite checks it. Two independent checks are better than one.

Next: 07-measuring-speed.md

7. Measuring speed fairly

Measuring speed sounds easy ("just time it"), but it's full of traps. This file explains each choice and why it was made.

The three engines being compared

Trap 1: wall-clock time lies on a busy computer

"Wall-clock time" is what a stopwatch measures. If other programs are using the processor, your program waits, and the stopwatch counts the waiting too.

Fix: CPU time. The operating system can report how much processor time your process actually used (clock_gettime(CLOCK_PROCESS_CPUTIME_ID) in runner.rs; SpecTec uses OCaml's Sys.time, which is the same idea). Waiting doesn't count.

CPU time still isn't perfect on a busy machine: other programs fill the processor's caches and compete for memory, which slows yours down a little. So we also do the things below.

Trap 2: startup costs hide the real speed

SpecTec takes 31 to 34 seconds just to load the spec. Every engine also spends time setting up a module before running it. If you just time "run fib(15)", you mostly measure setup, not the actual work.

Fix: the slope method. Run the same program with different amounts of work (for example sieve with n = 1,000, 5,000 and 20,000). Plot time against work. The result is roughly a straight line:

time = setup + (cost per unit of work) × work

The slope of the line is the cost per unit of work, and the setup cost (where the line crosses zero) drops out. All speed numbers in this project are slopes: "µs per loop iteration", "µs per call", and so on. bench/kernels.py and bench/ablate.py compute them with a least-squares line fit.

Trap 3: one run is luck

Any single run can be unlucky (another job started at that moment).

Fix: repeat and take the median. Each input is run several times (5 for the main comparisons, 3 for the optimization comparisons), and we use the median (the middle value), which ignores the occasional very slow run.

Also: interleave and shuffle. Within each round, all engines (or all versions) run one after another, in a random order. So if the machine gets busier halfway through, every engine is affected equally instead of one engine getting all the bad luck.

Trap 4: averaging speedups the wrong way

If one benchmark is 2x faster and another is 0.5x, the "average speedup" isn't 1.25x. For ratios you use the geometric mean (multiply them and take the n-th root), which gives 1x here, the right answer. All "on average" speedups in this project are geometric means.

The benchmark programs (kernels)

bench/progs/kernels.wast has 8 small programs, each stressing different things:

bench/time-kernels.sh times all three engines on these. bench/progs/expect.py computes the correct answer for each input, and every run checks it, so a wrong answer stops the measurement.

The allocation counter: a measurement that the busy server can't spoil

The server used for this project was shared with other heavy jobs all day (load average 5 to 11 on 4 cores), which makes timing noisy. Some optimizations change timing by only 5-10%, smaller than the noise.

So there's a second measurement: counting allocations. Every time the engine asks the system for a new piece of memory, that's one allocation. Allocations are slow-ish (and freeing them later costs too), and most of the engine's overhead turned out to be creating and destroying values. The count is exact and the same every run, no matter how busy the machine is.

It's done with a special build (cargo build --features count-allocs, code in gen-engine/src/allocs.rs) that wraps the memory allocator with a counter. The timed builds don't include it, so it never affects timing.

How the optimization versions are compared

1. After each optimization, bench/snapshot.sh NAME saves:
   • the release binary (for timing)
   • a count-allocs build (for counting)
   • a .tgz of the exact source code, so every version can be rebuilt later

All of this goes into gen-engine/target/variants/. 2. bench/ablate.sh RUNS NAME... times all the saved versions on the kernels, interleaved and shuffled, then runs each counting build once. 3. bench/ablate.py prints µs per unit, allocations per unit and speedup versus the first version.

This is called an ablation study: measuring the effect of each change separately, so you know which ideas actually helped.

Honest limitations

• The server is a shared cloud machine (4-core Intel Xeon, Hetzner), not a quiet dedicated one, and it has no hardware performance counters or perf profiler. Final numbers must be redone on a quiet machine.
• The comparison with SpecTec and refint for the newest version mixes two timing runs taken at different times (v7's numbers from one run, SpecTec's and refint's from an earlier one). A same-session rerun will fix that.
• Benchmarks are small hand-written programs. The research plan also lists bigger real-world benchmarks (CoreMark, PolyBench, a Lua interpreter) for later.

Next: 08-optimizations.md

8. The optimizations (v1 to v7)

The rule: meaning-preserving rewrites

Every optimization must keep the engine doing exactly the same thing, just faster. There are two checks for each one: 1. An argument for why it can't change any result (written below for each). 2. The full test suite: all 55,861 tests, identical per file to SpecTec.

Most changes are in the compiler (gen.ml, so they change the generated code), and some are in the runtime. None of them adds hand-written instruction logic: the engine still comes entirely from the spec.

Where the time was going

The first generated engine (v0) spent most of its time creating and destroying values: allocating memory for every little value, copying lists, and freeing them again. For example, on the sieve benchmark it made 415 allocations per step of work. So most optimizations attack allocations.

v1: pass arguments as slices

Before: every function call built a fresh Vec (a growable list in the heap) to hold its arguments, then threw it away. After: arguments go in a small fixed array on the stack (&[Value]), which costs no allocation. Running an instruction also passes the instruction's own argument list instead of copying it. Analogy: handing someone the papers directly instead of buying a new folder for every handoff. Why it's safe: the callee reads the same values in the same order; only the container changed. Effect: 24-39% fewer allocations.

v2: call math functions directly

Before: a math built-in like fadd was found by comparing its name, as a string, against a list of 83 names, on every call. After: the compiler knows which built-in each call means, so it emits a direct call (numerics::f::fadd(..)). One macro table in numerics.rs creates both the direct functions and the by-name lookup, so the two can never disagree. Analogy: calling someone's direct number instead of asking the receptionist to look them up every time. Why it's safe: it's the same function, found earlier. Effect: no allocation change, small CPU saving (too small to measure on the busy server).

v3: share instruction lists instead of copying them

Before: the spec says entering a block or loop means "push a new label with the body's instructions". The engine copied the whole list of instructions, then reversed it, every time. In a loop that's every single iteration. After: the new context keeps a pointer to the original list plus a position (seq + pc in ctx.rs). The small extra end marker goes in a separate little list. Analogy: using a bookmark in the recipe book instead of photocopying the recipe every time you cook. Why it's safe: sharing is only wrong if someone changes the list while it's being used. Checking every place in the generated code that changes something in place (Replace and Append statements) shows they only ever change the store, a frame's locals or a module instance, never an instruction list. Effect: fewer allocations (sieve: 253 to 230 per unit), less copying.

v4: cheaper constructors

Before: two waste problems with constructors like CONST(I32, 5) and ADD: - a constructor with no arguments (like I32 or ADD) still allocated an empty argument list, even when it was only built to compare with something - a constructor with arguments allocated twice: once for a Vec, then again to copy it into its final shared form

After: - every no-argument constructor shares one empty argument list (no allocation) - constructors with arguments are built in one step (one allocation)

Analogy: instead of printing a new blank form every time, everyone points to the same blank form on the wall. Why it's safe: an empty list has no contents to change, so sharing it is invisible. The one-step build produces the identical value. Effect: the biggest single drop. Allocations per unit on xorshift went from 194 to 72.

v5: don't compute the same pure thing twice

Before: the spec's BINOP algorithm (for i32.add and friends) says:

If (|$binop_(nt, binop, c_1, c_2)| <= 0) { Trap }        -- if there's no result, trap
Let c = choose($binop_(nt, binop, c_1, c_2))              -- otherwise pick the result

So $binop_ (the actual math) ran twice for every arithmetic instruction. After: the compiler notices the second call is identical and reuses the first result. How the compiler knows it's safe (the purity analysis): a function is pure if its result depends only on its arguments: - it doesn't read the machine state (store, contexts, value stack) - it doesn't change anything in place - every function it calls is also pure

The compiler checks this for all 474 algorithms, repeating until nothing changes (a "fixpoint", because a function's purity depends on the functions it calls). A call is reused only when: - the function is pure - every variable in its arguments is set exactly once (so the arguments can't have changed between the two calls) - the algorithm itself can't change anything in place

30 algorithms get this. Analogy: writing down the answer to a calculation instead of redoing it when you need it again. Why it's safe: same function plus same arguments gives the same answer, and those conditions guarantee the arguments are the same. Effect: floats: 157 to 95 allocations per unit; xorshift time improved about 30%.

v6: cheaper type checks and comparisons

Before: - has_type(x, "Inn") ("is this an integer type?") turned the tag back into its name and compared strings, on every call - comparisons like binop = ADD built an ADD value just to compare against it

After: - each tag is classified once (integer type, float type, reference, ...) and remembered - comparing with a no-argument constructor is a direct tag check (161 places in the generated code)

Why it's safe: it gives the same true/false answer for every value; it just gets there faster. Effect: too small to see in timing on the busy server; no allocation change.

v7: compact memory

Before: a WebAssembly memory is a big array of bytes, but the engine stored it as a list of general Values: a full value (dozens of bytes) for every single byte of memory. One test (call.wast) grows memory by 306 pages (about 20 million bytes), which made the engine use 2.84 GB of RAM. On the shared server that was enough to get the process killed once. After: memories are stored as plain bytes (Value::Bytes, a Vec<u8>). Only the five operations that ever touch a whole memory support it: length, read one byte or a slice, write a slice, join two lists (growing memory), and make n copies (creating memory). Anything else that receives one fails loudly instead of quietly doing something wrong. Two careful details: - growing memory must build a new buffer, not extend the old one in place, because the memory.grow algorithm reads the old size after growing - writing checks every byte first, so a bad value can't leave memory half-written

Why it's safe: a list of small numbers and a byte array hold the same information; the five operations give the same results for both. Effect: call.wast peak memory went from 2.84 GB to 35 MB (81x less). No speed change on the kernels, which barely use memory.

All together

Allocations per unit of work fell 47% to 83%, depending on the kernel. The full per-kernel table is in notes/logbook.md and 09-results-and-next-steps.md.

Next: 09-results-and-next-steps.md

9. Results, what they mean, and what's next

All the main numbers in one place

Correctness - 55,861 / 55,861 commands passed (every command SpecTec's runner executes on the 259 official core test files), identical per file to SpecTec, for every version v0 to v7.

Feasibility (kill test, hand translation of ~15 instructions) - 0 of ~15 instructions needed logic that isn't in the spec's AL - 1,059x faster per loop iteration, 607x faster per call than SpecTec

Whole test suite (v0) - SpecTec: 108.4 s of CPU time; engine: 16.0 s, so 6.8x faster. This is less than on the benchmarks because the suite is mostly tiny modules where setup dominates.

Benchmarks (µs per unit of work, run ablate-20261029T054035Z, 3 runs, busy server)

Against the other engines (v7, approximate) - about 45x faster than SpecTec (v0 was 28x) - about 3.5x slower than the hand-written reference interpreter (v0 was 5.6x). Closest: fib at 1.2x. Furthest: indirect at 9.2x.

Memory - call.wast peak memory: 2.84 GB (v6) down to 35 MB (v7)

What the numbers mean

• The main claim holds: a compiler can turn the official spec into an engine that is fully correct (same results as the spec on every test) and much faster than running the spec directly. The goal from the research plan ("at least 10x faster") is passed by a wide margin.
• Interpretation, not the spec's design, was the main cost. Removing the interpretation layer gave the first big jump (28x).
• After that, allocation was the main cost. The optimizations that removed allocations gave the biggest gains, and kernels with the biggest allocation drops (xorshift, matmul, floats) got the biggest speedups.
• Not every idea paid off. v2 and v6 made no measurable difference on these benchmarks, and that's a real result too: it shows where the time isn't going.
• The stretch goal (within 2x of the reference interpreter) isn't reached yet. We're at about 3.5x.

Limitations (say these before a judge asks)

1. Busy server. All timings ran on a shared machine with other heavy jobs. Allocation counts are exact; times are preliminary and need a quiet machine.
2. Mixed runs. The 45x and 3.5x figures combine v7's run with SpecTec's and refint's from an earlier run.
3. Small benchmarks. The 8 kernels are short hand-written programs. Real-world programs may behave differently.
4. 11 long test files are skipped, exactly like SpecTec's own runner does.
5. Front end reused. Parsing and validation come from the reference interpreter (through SpecTec). The project's contribution is execution.
6. The runtime is hand-written, about 4,900 lines. It contains no instruction rules, but it's still code that has to be correct (the test suite checks it).
7. AI tools helped build it. The logbook records that Claude Code (with helper agents) and Gemini were used. Be ready to explain every part in your own words.

What's next

1. Profile v7 to see what dominates now. Likely suspects:
   • the step-by-step context machine itself (every instruction goes through the run loop)
   • looking up local variables (local.get searches the context stack for the current frame every time)
   • call_indirect (the slowest kernel compared with refint, 9.2x)
2. More rewrites. The research plan's ideas still to do:
   • native machine integers for small math (instead of 128-bit general numbers)
   • a separate control stack instead of labels mixed into contexts
   • faster br that exits several labels at once (today it exits one label at a time)
3. Re-measure on a quiet machine, with all engines in the same session, 10 runs each.
4. Run the 11 long test files that SpecTec skips. The faster engine may be able to.
5. Stretch experiments from the research plan:
   • feature latency: take a WebAssembly proposal already written in SpecTec, regenerate the engine and count how many lines of engine code had to change (expected: zero)
   • module specialization: compile the engine for one specific program (partial evaluation, the idea behind Futamura's projections) for more speed
6. Bigger benchmarks: CoreMark, PolyBench, a Lua interpreter, and comparing with wasmi and wasm3.

Next: 10-commands.md

10. Commands and scripts

First, how running things works here

The project lives on your laptop, but anything heavy (building, testing, timing) runs on your server, because your internet is metered and the server has the tools. This folder is a Magic Box: it syncs automatically to the server, and you run commands there with magic run.

cd ~/Projects/spectec-engine
magic run bash gen-engine/check.sh

• magic run CMD runs CMD on the server, in the synced copy of this folder.
• magic flush makes sure your latest edits have reached the server (do this right after editing, before magic run).
• Files the server creates sync back to the laptop, except big build output: gen-engine/target/ (binaries, dumps, results, variants) and upstream/test stay on the server only.
• Rust's cargo needs source ~/.cargo/env first in a magic run shell, for example: magic run bash -c 'source ~/.cargo/env; cd gen-engine && cargo build --release'.

Building

After changing gen.ml, run both, in that order. After changing only runtime files (gen-engine/src/*.rs except spec.rs), just build.

Testing

Saving and comparing versions

Comparing with SpecTec and the reference interpreter

Profiling

Running one test file by hand

magic run bash -c 'cd gen-engine/target/dumps && ../release/gen-engine block.al'

It prints failures to stdout and the summary (- 52/52 (100.00%) and block.wast took X ms.) to stderr.

Next: 11-glossary.md

11. Glossary

Ablation study. Measuring each improvement separately (turning them on one at a time) to see which ones actually helped.

AL (algorithmic language). SpecTec's step-by-step version of the spec's rules. Each instruction becomes a short algorithm made of statements like Pop, Push, If and Execute.

Allocation. Asking the system for a new piece of memory to store something. Each one costs time, and so does freeing it later.

Backend. The part of a tool that produces output. SpecTec has backends for the document, the interpreter and others; this project adds a Rust backend.

Benchmark / kernel. A small program used to measure speed.

br (branch). WebAssembly's jump instruction. It leaves a block or restarts a loop.

Compiler. A program that translates code from one language into another. Here it translates the spec's AL into Rust.

Context. One entry in the abstract machine's stack: a frame (function call), a label (block or loop) or a handler (exceptions). Each has its own value stack and remaining instructions.

CPU time. How much processor time a program actually used, not counting time spent waiting.

Dump (.al file). A test file converted by SpecTec into AL values, one per line, so the engine can read it.

Fixpoint. Repeating a calculation until the answer stops changing. Used to decide which functions are pure, because a function's purity depends on the functions it calls.

Frame. The context for one function call. It holds the function's local variables and its module.

Geometric mean. The right way to average ratios like speedups: multiply them all and take the n-th root.

Interpreter. A program that runs code by reading it step by step, as opposed to translating it first.

Kill test. A short experiment designed to stop a project early if its riskiest assumption is wrong.

Label. The context for a block or loop. br jumps relative to labels.

Lockstep. Moving in perfect sync. The project's name: the engine stays in sync with the spec because it's generated from it.

Median. The middle value when you sort the measurements. It isn't fooled by one unusually slow run.

Meta-interpreter. SpecTec's interpreter for AL. "Meta" because it interprets the spec, which itself describes an interpreter.

Module. A WebAssembly program: functions, memory, tables, globals, imports and exports.

Nullary constructor. A constructor with no arguments, like I32 or ADD.

Partial evaluation. Specializing a program for some of its inputs ahead of time. For example, specializing the engine for one particular Wasm program. Futamura's projections are the classic theory behind it.

Pure function. A function whose result depends only on its arguments: no reading or changing of anything else.

Rc / RefCell. Rust tools for sharing a value between several owners (Rc, with a reference count) and for changing a shared value safely (RefCell).

Reference interpreter (refint). The official hand-written WebAssembly interpreter in OCaml. Written for clarity, but much faster than the meta-interpreter.

Runtime. The hand-written library the generated code runs on: values, numbers, the context machine, math built-ins and the test runner.

Rust. A fast, memory-safe programming language. The generated engine is written in Rust.

SIMD. "Single instruction, multiple data": doing the same math on many numbers at once (WebAssembly's v128 type).

Slope method. Timing a program at several amounts of work and fitting a line. The slope is the cost per unit of work, and startup cost drops out.

Spec (specification). The official rulebook that defines exactly how WebAssembly behaves.

SpecTec. The language (and tool) the WebAssembly spec is written in. It can produce documents, AL and an interpreter from the same source.

Stack machine. A computer design where instructions take their inputs from a pile (stack) of values and push their results back.

Store. Everything a running WebAssembly program owns: functions, memories, tables, globals, structs, arrays and exceptions.

Tag. A small number standing for a constructor name (like CONST or I32), so comparisons are fast.

Tail rule. When an AL algorithm runs an instruction that isn't its last statement, that instruction must finish before the next statement starts. The compiler emits cx.run(depth) for this.

Trap. WebAssembly's way of stopping with an error, for example dividing by zero or reading outside memory.

WebAssembly (Wasm). A portable, safe instruction format that browsers and servers run. C, C++, Rust and many other languages can compile to it.

Next: 12-judge-answer-speed.md

12. If a judge asks: "How did you make it faster?"

The 30-second answer

"SpecTec runs WebAssembly by reading the spec's rules one by one for every instruction, like a referee checking the rulebook on every move. We built a compiler that reads those same rules once and turns them into Rust code. That alone made it about 28x faster. Then we profiled it and found most of the remaining time went into creating and throwing away small pieces of memory, so we made seven safe rewrites to remove that waste, which gave another 1.7x. In total it's about 45x faster than SpecTec, and it still passes all 55,861 official tests with exactly the same results."

If they ask for more detail

Step 1: compile instead of interpret (the big win, about 28x)

• The rules don't change between instructions, so looking them up every time is wasted work.
• We translate each rule into real code once, ahead of time. Then the computer just runs that code.

Step 2: remove wasted memory work (about 1.7x more)

• After step 1 we measured where the time went. The engine was allocating memory constantly: on sieve it made 415 allocations per unit of work.
• The best examples to give:
  • Bookmarks instead of photocopies (v3): every loop iteration used to copy the whole list of instructions. Now it keeps a pointer plus a position, like a bookmark in a recipe book.
  • One shared blank form (v4): every simple value like ADD used to get its own empty list. Now they all share one. This was the biggest single drop: 194 to 72 allocations per unit on xorshift.
  • Don't do the math twice (v5): the spec's rule for add computes the result twice, once to check it exists and once to use it. The compiler proves the function is "pure" (same inputs always give the same answer) and reuses the first result. xorshift got about 30% faster.
  • Store memory as plain bytes (v7): this one saves memory, not speed. Peak RAM on call.wast went from 2.84 GB to 35 MB.

If they ask "How do you know you didn't break anything?"

"Every optimization has two checks: a written argument for why it can't change any result, and a rerun of all 55,861 official tests, which must match SpecTec exactly, file by file. All seven versions pass."

Honest limits (say these before they find them)

• The timings were measured on a shared, busy server, so they're preliminary. The allocation counts are exact.
• It's still about 3.5x slower than the hand-written reference interpreter. The goal is to get within 2x.
• v2 (direct math calls) and v6 (faster type checks) made no measurable difference. That's still useful: it shows where the time isn't going.
• The 8 benchmarks are short hand-written programs. Real programs may behave differently.

The full details are in 08-optimizations.md and 09-results-and-next-steps.md. The exact run IDs are in notes/logbook.md if a judge asks for evidence.

Next: 13-explaining-the-paper.md

13. How to explain every figure, table and code block in the paper

This chapter goes through paper/paper.pdf in the order things appear. For each figure, table or code block you get:

• Script: a short paragraph you can say out loud while presenting it
• What it shows: the point of it, in one or two sentences
• How to read it: what the axes, colors, rows or lines mean
• What to say: a one-sentence version, for when there's no time for the script
• If they ask: the questions a judge is most likely to ask about it, with answers

One idea comes up again and again, so learn it once:

Log scale. Several charts use a log scale: each grid line is 10 times the one before (1, 10, 100, 1,000). This lets tiny and huge numbers fit on one chart. The useful trick: on a log scale, the distance between two dots shows how many times faster one is, not how many microseconds apart they are. Two dots one grid line apart means 10x.

Figure 1. Architecture (the box diagram)

Script (about 20 seconds):

This is how the whole system fits together. At the top, the official WebAssembly spec goes into SpecTec, which turns it into 474 small algorithms. My compiler, the blue box, turns those algorithms into about 22,000 lines of Rust. In the middle, each official test file is turned into data the engine can read, using SpecTec's own parser, so both sides read the tests the same way. At the bottom, I compare my results with SpecTec's, file by file.

What it shows: how the whole system fits together. Blue boxes are the parts built in this project; gray boxes already existed.

How to read it: there are two rows that meet at the Lockstep engine.

• Top row, the specification side (runs once per version of the spec): the official Wasm 3.0 spec goes into SpecTec, which turns it into AL, 474 small step-by-step algorithms. Before this project, AL could only become prose, LaTeX, or be run slowly by the meta-interpreter. The new blue box, spectec --rust (gen.ml, about 700 lines), writes those 474 algorithms out as Rust code: spec.rs, about 22,000 lines.
• Middle row, the test side (runs once per test file): each official .wast test file goes through dump.ml, which uses SpecTec's own parser and checker to write the test as AL values, one per command.
• The engine (one Rust program) = the generated spec.rs + a hand-written runtime (values, the context stack, numeric math, the test runner).
• Bottom row: the engine produces "passed / total" and CPU time for each file, and these are compared with SpecTec's own run of the same file.

What to say: "The spec goes in at the top, our compiler turns it into Rust, the tests go in at the middle, and at the bottom we compare our results with SpecTec's, file by file."

If they ask:

• "Which parts did you write?" The blue ones: the compiler gen.ml, the test dumper dump.ml, and the engine (the generated part is written by the compiler; the runtime is written by hand).
• "Isn't the hand-written runtime cheating?" No. It contains no rules for any instruction. It's the same kind of support code that SpecTec's own meta-interpreter writes by hand in OCaml (the context stack, the step loop, number math). All instruction behavior comes from the spec.
• "Why reuse SpecTec's parser?" Parsing and checking test files aren't part of the spec's execution algorithms. The meta-interpreter reuses the same code, so both sides read the tests identically and the comparison is fair.

Table 1. How Lockstep differs from previous approaches

Script (about 20 seconds):

This table shows where Lockstep fits. The key column is the last one: does it follow the official spec automatically? Hand-written engines and separate formal versions all need someone to update them by hand when the spec changes. Only SpecTec's own interpreter and Lockstep follow the spec automatically, and Lockstep compiles the spec instead of interpreting it, so it's much faster.

What it shows: where this project sits compared with other ways of running WebAssembly.

How to read it: the most important column is the last one, "Follows the official spec automatically". Only two rows say yes: SpecTec's meta-interpreter (slow, because it interprets) and Lockstep (compiled, so faster). Every other project either has its own separate math version of Wasm (WasmCert, KWasm) or is written by hand (reference interpreter, Wasmtime, wasmi, wasm3), so someone must update it by hand when the spec changes.

What to say: "Everyone else either runs the spec slowly or rewrites it by hand. We're the only one that compiles the official spec itself."

If they ask:

• "Why not just use Wasmtime? It's much faster." Wasmtime is a hand translation of the spec, so it can disagree with it. Our goal is an engine that agrees with the spec by construction, useful as a trusted reference for testing other engines.

Table 2. Translation of AL statements (the compiler's rulebook)

Script (about 20 seconds):

This table is basically my whole compiler. The spec's algorithms use only about ten kinds of statement, like Assert, Pop, Push, If and Trap. Each kind is always translated into Rust the same way. That's why the compiler is only about 700 lines, and why nothing in the engine is special-cased for a single instruction.

What it shows: the whole compiler in one table. The AL has only about ten kinds of statement, and each one is turned into Rust in a fixed way.

How to read it: left column is the AL statement, right column is the Rust the compiler writes. cx is the engine's state (the stack and the store). A few examples:

• Assert e becomes if !is_true(e) { return err(..) }: check a condition, stop with an error if it's false
• Pop becomes cx.pop_value(): take a value off the stack
• Push e becomes cx.push(e): put a value on the stack
• Trap becomes return Err(Exn::Trap): stop the program with a WebAssembly error

What to say: "Because there are only about ten kinds of statement, the compiler is small, about 700 lines. Every one of the 474 algorithms is translated by these same rules, with nothing special-cased per instruction."

If they ask:

• "What's the tricky one?" Execute when it's not the last statement. The spec expects everything it starts to finish before the next line runs. The meta-interpreter gets that from its step counter; our code remembers the stack depth and runs until it's back there (cx.run(depth)).

Listing 1. The br_if algorithm and the Rust generated for it (the code block)

Script (about 20 seconds):

Here's a real example: the spec's rule for br_if, "branch if", and the Rust my compiler generated for it. On top is the spec: check there's a value, pop it, and if it isn't zero, branch. Below, each gray comment is one line of the spec, and the code under it is its translation, so anyone can check the engine against the spec line by line. It's wordy on purpose: this first version is a literal translation, and the speed came later from separate, tested rewrites.

What it shows: a real side-by-side example. Top: the spec's algorithm for br_if ("branch if"). Bottom: the exact Rust our compiler wrote for it. The point is that the Rust follows the spec line by line, so anyone can check it.

The AL on top, in plain words:

Step_pure/br_if l {
 Assert (top_value(I32))           -- there must be a number on the stack
 Pop (I32.CONST c)                 -- take it off; call it c
 If ((c =/= 0)) { Execute (BR l) } -- if c is not zero, jump to label l
 Else { Nop }                      -- otherwise do nothing
}

The Rust, walked through in blocks:

1. pub fn r_BR_IF(cx, args): one Rust function per spec algorithm. cx is the engine state; args holds l, the label to jump to.
2. let mut v_c ... let mut v_l ...: one Rust variable for each spec variable (c and l). This replaces the meta-interpreter's lookup table of variables, which is one reason it's faster.
3. if args.len() != 1 { return err(..) }: a safety check that exactly one argument came in.
4. v_l = __p444.clone(): store the argument as l.
5. // Assert (top_value(I32)) then if !... cx.value_stack_len() > 0 ...: the spec's Assert line. It checks the stack isn't empty.
6. // Pop (I32.CONST c) then cx.pop_value() and two match blocks: take the value off the stack and check its shape. The first match checks it's a CONST (tag 2) with two parts; the second checks the first part is I32 (tag 3). Then the number inside becomes v_c. If the shape is wrong, it stops with an error instead of guessing.
7. // If ((c =/= 0)) ... then if rt::is_true(&rt::ne(&v_c, ... 0 ...)): the spec's If. If c is not 0, build the instruction BR l (tag 21) and execute it.
8. Ok(None): done, return nothing.

What to say: "Each gray comment is a line of the spec, and the code under it is the translation. You can check it line by line. Names like CONST and I32 became small numbers (tags) when the code was generated, so at run time comparing them is just comparing two integers, not two words."

If they ask:

• "Why does it look so wordy, with all the .clone()s?" On purpose. The first version is a literal translation so it's easy to check against the spec. Speed came afterwards, from separate rewrites, each tested on the full suite (Table 3).
• "Why __p444, __x445?" They're temporary names the compiler invents; the number just keeps them unique.
• "The spec says top value must be an I32, but the code only checks the stack isn't empty." Correct, and that's deliberate: SpecTec's own meta-interpreter does exactly the same (its source has a "TODO: type check" there), and we mirror it. The very next line's match would still catch a wrong type and stop with an error, and WebAssembly's validation guarantees the type anyway.
• "What's Z::S(0i128)?" The number 0 as the spec's "mathematical integer" type. The spec uses unbounded numbers; we store small ones in a 128-bit integer.

Table 3. The rewrites (v0 to v7)

Script (about 20 seconds):

These are the seven speed-ups. The last column gives the reason each one can't change any result, and after each one I re-ran all 55,861 tests. Most of them remove wasted memory work: for example, using a bookmark instead of copying a list of instructions, or not computing the same pure result twice.

What it shows: the seven speed-ups, what each one changed, and why each can't change any result. Each version includes all the ones before it.

How to read it: each row is one rewrite. The last column, "Why the meaning is unchanged", is the important one: it's the safety argument.

What to say: "Every rewrite has a reason it can't change behavior, and on top of that every version was re-run on all 55,861 tests."

If they ask:

• "Which one is the cleverest?" v5. The compiler checks all 474 algorithms to find the "pure" ones (same input always gives same output, no side effects), then reuses results instead of recomputing. For example, the spec's arithmetic rule computes the answer twice; now it's computed once.
• "Which one was riskiest?" v3, because its safety depends on a fact about the whole spec: nothing ever changes an instruction list in place. We checked every place the generated code changes something, and none of them touch an instruction list.

Table 4. Official core test suite results

Script (about 20 seconds):

This is the correctness result. SpecTec passes 55,861 commands on the official test suite, and so does my engine. And it's not just the same total: it's the same result in every one of the 259 files, for the first version and for each of the seven optimized versions.

What it shows: correctness. Lockstep passes every command SpecTec passes, in every file, for every version.

How to read it: three rows. SpecTec 55,861 / 55,861. Lockstep v0 the same, with identical counts in 259 / 259 files. Each of v1 to v7 also the same.

What to say: "Not just the same total: the same result in every single file, for all eight versions."

If they ask:

• "Why not every command in the suite?" We use SpecTec's own runner rules so the comparison is fair. Those rules skip 11 very slow test names (12 files, because one name exists twice) and some command types like assert_malformed that test the parser, not execution.
• "Does passing the tests prove it's correct?" It's strong evidence, not a proof. And because we mirror the meta-interpreter, a bug both share wouldn't show up. That's in the paper's limitations.

Figure 2. Kill test (two rows of dots)

Script (about 20 seconds):

Before building the full compiler, I ran a one-week test to decide if the project was worth doing. I translated about 15 instructions by hand, following the spec exactly. I set two rules in advance: stop if more than 3 instructions need logic that isn't in the spec, or if it's less than 10 times faster. Zero instructions needed extra logic, and it was 600 to 1,000 times faster, so I went ahead.

What it shows: the one-week feasibility test that decided whether the project was worth doing. A quick hand translation of about 15 instructions vs SpecTec.

How to read it: log scale, time per unit of work. Each row has two dots: orange is SpecTec, the other is the hand translation. The further apart, the bigger the speedup.

• count (one loop iteration, about 11 instructions): 440 µs vs 0.416 µs, 1,059x faster
• fib (one recursive call): 578 µs vs 0.953 µs, 607x faster

What to say: "Before building anything big, I set a rule: stop if more than 3 instructions need logic that isn't in the spec, or if it's under 10x faster. Zero needed extra logic, and it was 600 to 1,000 times faster, so the project went ahead."

If they ask:

• "If the kill test was 1,000x faster, why is the real engine only 28 to 45x?" The hand translation used plain Rust integers for just 15 instructions. The real engine has to handle the whole language, so it uses one general value type for everything, which costs much more. Closing that gap is exactly what the rewrites (Table 3) work on.

Figure 4. Whole test suite, file by file (scatter plot + bar chart)

Script (about 20 seconds):

This shows the whole official test suite, file by file. On the left, each dot is a file, and dots below the diagonal line ran faster on my engine. On the right, you can see how many files fall in each speedup range: most are 4 to 16 times faster, and the median is 7.2 times. The 23 gray files that were slower are mostly memory tests, and that's exactly what my last optimization fixed.

What it shows: how much faster Lockstep v0 is on each of the official test files.

How to read (a), the scatter plot:

• Each dot is one test file. Across (x) is SpecTec's time, up (y) is Lockstep's time, both log scale.
• The diagonal line marked "same speed": a dot on it means both took the same time. Below the line = Lockstep faster (blue). Above = Lockstep slower (gray). The second, lower diagonal marks 10x faster.
• Most dots are blue and below the line. The gray ones above it are mostly memory tests. call.wast (top right) is labelled because it's the one that used 2.84 GB of RAM.

How to read (b), the bar chart:

• Each bar counts how many files had a speedup in that range. The ranges double each step (1/8 to 1/4, ..., 16 to 32).
• Gray bars (left of 1) are files where Lockstep was slower: 4 + 7 + 12 = 23 files.
• Blue bars are faster files. The tallest bar, 84 files, is 8 to 16x faster. The median is 7.2x.

What to say: "Most files are 4 to 16 times faster. The suite is mostly tiny tests where setup time dominates, so the gain is smaller than on real loops. The 23 slower files are almost all memory tests, which is what rewrite v7 fixed later."

If they ask:

• "Why are 23 files slower?" In v0, memory was stored as one big general value per byte, so tests that grow memory were slow and memory-hungry. v7 stores plain bytes; call.wast went from 2.84 GB to 35 MB. (Honest note: the suite timings in this figure are v0; it hasn't been re-timed with v7 yet.)
• "Why only 6.8x here but 28x on kernels?" Test files are tiny, so loading and setting up each module takes most of the time. Kernels are loops that run real work, which is where compiling helps most.

Figure 3. Compute kernels (dot plot with three engines)

Script (about 20 seconds):

This is the main speed result, on eight benchmark programs. Orange is SpecTec, blue is my engine, green is the hand-written reference interpreter, and further left means faster. In every row my engine is in the middle: 15 to 42 times faster than SpecTec, 28 times on average, but still slower than the hand-written interpreter. And this is the first version, before any optimization.

What it shows: the main speed result. Eight small benchmark programs, three engines.

How to read it:

• Each row is one benchmark ("kernel"), with its unit of work under the name (per call, per iteration...).
• Three markers per row, on a log scale of time per unit (left = faster): orange square = SpecTec, blue circle = Lockstep v0, green diamond = the hand-written OCaml reference interpreter.
• The blue dot sits between the other two in every row: much faster than SpecTec, still slower than the hand-written interpreter.
• The two columns on the right give the ratios. Bottom line: 28x faster than SpecTec, 5.6x slower than the reference (geometric mean).

What to say: "On every benchmark, our engine is between the two: 15 to 42 times faster than running the spec directly, and still 2 to 13 times slower than the hand-written interpreter. That's v0, before any optimization."

If they ask:

• "What's a geometric mean?" The right kind of average for ratios. If one thing is 2x and another 8x, the geometric mean is 4x (multiply, then take the root), which treats "twice as fast" and "half as fast" fairly.
• "Why is indirect the worst (12.6x slower)?" Indirect calls go through a type check and table lookup that the spec describes in many small steps. It's on the list of next optimizations.
• "How did you measure fairly?" CPU time measured inside each program, SpecTec's 31-second spec loading excluded, and the slope method (next question).
• "What's the slope method?" Run each benchmark at several sizes, plot time against amount of work, and fit a straight line. The slope is the cost of one unit of work; fixed costs like startup go into the starting point of the line and drop out.

Table 5. Kernels in numbers

Script (about 20 seconds):

These are the exact numbers behind that chart, plus the final version, v7. After the seven optimizations, my engine went from 28 to about 45 times faster than SpecTec, and from 5.6 to about 3.5 times behind the hand-written interpreter. On fib it's almost there, only 1.2 times slower. These final numbers are approximate, because they combine two measuring sessions.

What it shows: the exact numbers behind Figure 3, plus a column for the final version v7.

How to read it: µs of CPU time per unit of work. The first five columns come from one session (SpecTec, Lockstep v0, reference interpreter, and the two ratios). The last three columns add v7: about 45x faster than SpecTec and 3.5x slower than the reference (geometric mean). Closest: fib at 1.2x slower. Furthest: indirect at 9.2x.

What to say: "After the seven rewrites we went from 28x to about 45x faster than SpecTec, and from 5.6x to 3.5x behind the hand-written interpreter."

If they ask:

• "Why the '~' on 45x and 3.5x?" v7 was timed in a different session from SpecTec and the reference interpreter, and the server was busy. So those two numbers are approximate. The paper says so in the caption.

Figure 5. Ablation: what each rewrite contributes (two line charts)

Script (about 20 seconds):

This chart shows what each optimization did, one at a time. The right side counts memory allocations, which are exact: they fell to 31% of the start. The left side is time, which is noisier because the server was busy, but it follows the same shape and ends at 59%, which means 1.69 times faster. The biggest gains came from v4 and v5, and the benchmarks that lost the most allocations sped up the most.

What it shows: "ablation" means adding one change at a time to see what each one does. Left: time. Right: memory allocations (creating and freeing small pieces of memory).

How to read it:

• Across (x): the versions in order: v0 baseline, v3 shared seq, v4 constructors, v5 pure reuse, v6 tag tests, v7 byte memory. (v1 and v2 were measured in an earlier run.)
• Up (y): percent of v0. 100% = same as the start; lower is better.
• Thin light lines = the eight kernels. Big dark dots = their geometric mean.
• (a) Time ends at 59% of v0, which is the 1.69x speedup. It's bumpy because the server was busy (one thin line jumps up at v6; that's noise).
• (b) Allocations ends at 31% of v0: about two thirds of all allocations removed. It's smooth because allocation counts are exact, not affected by the busy server.
• The two big drops are v4 (constructors) and v5 (pure reuse). After v5 both charts go flat: v6 and v7 didn't help these kernels.

What to say: "The right chart is the reliable one: allocations are counted exactly, and they fell to 31% of the start. The left chart follows the same shape, ending at 59% of the original time. The kernels with the biggest allocation drops got the biggest speedups, which shows allocation was the main cost."

If they ask:

• "Why measure allocations at all?" Because the timings were noisy on a shared server. Allocation counts don't change with machine load, so they're solid evidence even when time isn't.
• "So v6 and v7 were useless?" Not useless: v6 shows string comparisons weren't the bottleneck (a real finding), and v7 was about memory, not speed: call.wast went from 2.84 GB to 35 MB. The kernels barely use memory, so it can't show here.

Table 6. Ablation in numbers

Script (about 20 seconds):

These are the numbers behind that chart. Each cell is the time, with the allocations in brackets. For example, xorshift went from 304 allocations per step to 51, and its time dropped by more than half. Overall, the seven rewrites made the engine 1.69 times faster: from 1.34 times on sieve up to 2.36 times on matmul.

What it shows: the exact numbers behind Figure 5.

How to read it: each cell is time (allocations): µs per unit, with allocations per unit in brackets. For example, xorshift v0 is 36.5 (304): 36.5 µs and 304 allocations per iteration. By v7 it's 15.9 (51). The last column is v7's speedup over v0, from 1.34x (sieve) to 2.36x (matmul). The bottom row is the geometric mean: 1.00x, 1.31x, 1.40x, 1.68x, 1.67x, 1.69x.

What to say: "Look at xorshift: allocations went from 304 to 51 per iteration and time dropped by more than half. The allocation numbers are exact; the times are preliminary."

If they ask:

• "Why does v6 sometimes look slower than v5 (like fib 23.5 to 27.8)?" Noise from the busy server. The allocation count is identical (115 both times), so nothing changed in the work done.

The one-minute version, if a judge asks you to walk through the paper

1. Figure 1: spec goes into our compiler, out comes a Rust engine; tests are compared file by file.
2. Listing 1: the generated code follows the spec line by line, so it's easy to check.
3. Figure 2: a small test first proved it was worth doing (600 to 1,000x).
4. Table 4: correctness: same result as SpecTec in all 259 files, 55,861 commands, every version.
5. Figures 4 and 3: speed: 6.8x on the test suite, 28x on loops.
6. Figure 5: seven safe rewrites removed about 70% of allocations and gave another 1.69x, to about 45x total.

Back to the start: README.md