lumbda.

2.1 Type System

Core types stay minimal:

• Symbol: Interned strings with identity comparison (Symbol._t cache)

• Pair: (car . cdr) cons cells with optional line tracking for error reporting

• Nil: Singleton () for list termination

• Proc: Interpreted procedure (params, rest, body, env, name)

• CompiledProc: Bytecode procedure (CodeObj, params, rest, env, name)

• FullCont: First-class continuation (frames, stack, ip, instrs, env, vm_id)

• Macro: Wraps a transformer (Proc or _SyntaxTransformer)

• Env: Lexical environment chain (bindings dict, parent pointer, global pointer)

Exact rational arithmetic uses Python's Fraction type. (/ 1 3) evaluates to 1/3, not 0.333.... Literal 1/3 syntax parses directly to rationals.

2.2 The Bytecode

The compiler emits instructions as (opcode, operand) tuples into a CodeObj:

Core opcodes (20):

OP_CONST        push a constant value
OP_LOOKUP       look up a variable in the environment chain
OP_SET          set! a variable
OP_DEFINE       define a new binding
OP_POP          discard top of stack
OP_DUP          duplicate top of stack
OP_VOID         push #<void>
OP_JUMP         unconditional jump
OP_JUMP_IF_FALSE        conditional jump
OP_JUMP_IF_FALSE_KEEP   conditional jump, keep value on stack
OP_JUMP_IF_TRUE_KEEP    conditional jump, keep value on stack
OP_CALL         call a procedure (push frame)
OP_TAIL_CALL    call in tail position (replace frame)
OP_RETURN       return from procedure (pop frame)
OP_MAKE_CLOSURE create a closure from a CodeObj + environment
OP_PUSH_ENV     push a child environment
OP_POP_ENV      restore parent environment
OP_BIND         bind a name in the current environment
OP_EVAL         fall back to tree-walking interpreter
OP_CALL_CC      capture the current continuation

Specialized opcodes (20):

OP_ADD OP_SUB OP_MUL OP_NEG
OP_ADD1 OP_SUB1
OP_NUM_EQ OP_LT OP_GT OP_LE OP_GE
OP_CAR OP_CDR OP_CONS
OP_NULL_P OP_PAIR_P OP_NOT OP_ZERO_P
OP_VEC_REF OP_VEC_SET

Specialized opcodes avoid function call overhead for hot builtins. (+ x 1) compiles to OP_ADD1 instead of OP_LOOKUP '+' / OP_CONST 1 / OP_CALL.

4.1 Generators from Continuations

A generator in Lumbda uses call/cc to yield values & resume later:

(auto-compile! #t)
(define (make-gen thunk)
  (let ((k #f) (done #f))
    (lambda ()
      (if done 'done
          (call/cc (lambda (return)
            (if k (k return)
                (begin (thunk (lambda (val)
                         (call/cc (lambda (next)
                           (set! k next) (return val)))))
                       (set! done #t) (return 'done)))))))))

(define counter (make-gen (lambda (yield)
  (let loop ((i 0)) (yield i) (loop (+ i 1))))))
(counter) ; => 0
(counter) ; => 1
(counter) ; => 2

No special generator syntax. No coroutine framework. The same call/cc that handles escape continuations also handles cooperative multitasking, because feedback is feedback.

4.2 Why "Feedback Is All You Need"

Every control flow pattern reduces to a continuation operation:

• Loop: tail-call feeds the function back to itself

• Generator: call/cc feeds a value out, saves a resumption point, feeds control back in on next call

• Exception: call/cc feeds control to a handler registered via dynamic-wind

• Checkpoint: portal serializes the continuation, feeds the machine state to storage

• Migration: portal deserializes on another machine, feeds the continuation back to a new VM

• Cross-impl exchange: S-expression serialization feeds bindings across implementations that share no memory layout

• Network request: a socket tcp-send feeds bytes to a peer; tcp-recv feeds the response back

One primitive. Every pattern.

4.3 Four Scopes of Feedback

The single word "feedback" covers four nested scopes, each giving rise to one of our core abstractions:

Within a single VM, a continuation is the unit — the whole call stack, captured & passed. Across processes on the same machine, a portal is the unit — the whole heap or VM state, serialized to a file, resumed elsewhere. Across implementations that share no binary compatibility, Scheme source itself is the unit: (define x 42) travels because every parser already knows how to receive it. Across machines, bytes over a socket are the unit — an HTTP request is feedback to a peer, a response is feedback back. The HTTP handler is 70 lines of portable Scheme that runs byte-identical in all three runtimes.

The same abstraction, at four scopes. No new primitive at any level — each scope adds one implementation primitive (call/cc / portal / reader / socket) and keeps the semantics. This is what "feedback is all you need" actually means once you extend it past the process boundary.

5.1 Peephole Optimizer

The _peephole function runs over every compiled procedure after bytecode generation:

• Dead code elimination: OP_VOID followed by OP_POP → remove both instructions

• Redundant jump elimination: OP_JUMP to the next instruction → remove the jump

• Jump target adjustment: After removing instructions, all jump offsets update to maintain correctness

• Source map preservation: The parallel source map (line numbers per instruction) stays synchronized after removals

5.2 Inline Cache

Variable lookup in a chain of lexical environments requires walking from the current environment to the global. For frequently accessed global variables (builtins like +, car, null?), this traversal dominates execution time.

The inline cache tracks instruction_index → (cached_env, cached_value) pairs. On OP_LOOKUP:

1. Check if a cached entry exists for this instruction index

2. Verify the symbol is not shadowed in the local environment

3. If valid, use the cached value (skip the environment chain walk)

4. If invalid or absent, perform the full lookup & update the cache

This optimization targets the common case: inner loops that reference global functions thousands of times. The cache stays valid as long as the binding is not shadowed locally.

5.3 Constant Folding

The compiler evaluates pure expressions at compile time:

(+ 1 2)        ; => OP_CONST 3 (not OP_CONST 1 / OP_CONST 2 / OP_ADD)
(> 5 3)        ; => OP_CONST #t
(string-length "hello")  ; => OP_CONST 5

Supported foldable operations: +, -, *, =, <, >, <=, >=, not, zero?, positive?, negative?, abs, min, max, string-length, string-append.

Folding only applies when all operands are compile-time constants & the function name is not shadowed in the compilation environment.

6.1 Raw Results

BC Speedup = interpreter time / bytecode time. This measures the gain from compilation within Lumbda itself.

6.2 Analysis

The bytecode compiler delivers 7--12x speedups on recursive & iterative workloads compared to the tree-walking interpreter. The largest gains appear in tight loops (sum-to: 11.4x) & deep recursion (fib(20) tree: 9.2x, mergesort: 11.0x), where the explicit frame stack & specialized opcodes eliminate the overhead of AST traversal.

Hash table operations show a smaller speedup (1.6x) because the bottleneck sits in Python's dictionary operations, not in Scheme evaluation overhead.

CPython remains 50--150x faster than the bytecode VM on most benchmarks. This is expected: CPython compiles to native bytecode with a C runtime, while Lumbda's bytecode VM is itself written in Python. The comparison establishes that Lumbda pays a known, bounded overhead for running a complete Scheme (with full call/cc, exact rationals, & hygienic macros) inside a host language.

The important comparison is not Lumbda vs CPython (different languages), but Lumbda interpreter vs Lumbda bytecode (same language, same semantics, different execution strategy). The bytecode compiler proves that feedback-based architecture does not preclude efficient execution.

6.3 What the Benchmarks Test

• fib(35) iterative: Named-let tail recursion. Tests OP_TAIL_CALL & OP_ADD1

• fib(20) tree-recursive: Exponential call tree. Tests OP_CALL / OP_RETURN throughput

• tak(15,10,6): Takeuchi function. Deep mutual recursion with 3 arguments

• sum-to(50000): 50,000 tail-recursive iterations. Tests frame stack performance at scale

• ackermann(3,4): Deeply nested recursion (125 result, many thousands of calls)

• list ops: iota / reverse / filter / map / fold-left chain on 5,000 elements

• mergesort: Recursive divide-and-conquer on 200 elements. Tests cons allocation throughput

• hash-table: 1,000 set! + ref operations. Tests Python dict interop overhead

6.4 Three Implementations Head-to-Head (i5-8350U)

Same hardware, same workloads, in-process timing via current-time-ms. Best of two runs. Each implementation is run in its high-performance configuration: Python with --fast (bytecode VM), C with --fast (bytecode VM, also its mode for deep recursion), asm in its native tree-walker mode (asm has no bytecode layer — it doesn't need one).

(C fast is the fastest cell in every row — best of the three on this hardware.)

Reproduce: make bench-3way (source: tests/bench-3way.sh). Prints the same table on your hardware with best-of-two timings.

C wins every workload on this hardware. Its bytecode compiler + explicit frame stack (and optional --jit for pattern-matched call forms) gives a ~3× margin over asm on tail-recursive loops and deep recursion alike. asm's tree-walker is the narrowest Scheme of the three — no bytecode layer, no JIT — but still beats Python's bytecode VM by ~7–8× because it pays no Python overhead (no dict lookups, no object allocation per VM op, no interpreter dispatch thunk).

None of the three segfault on ackermann in their recommended mode. Python --fast uses OP_TAIL_CALL with explicit frames. C --fast uses its bytecode VM, also with explicit frames. asm's jmp-based TCO reuses the same host stack slot for tail calls. Only C's default tree-walker mode would exhaust the host C stack on deep recursion — by design; it uses the C call stack for each Scheme call. Either pass -f/--fast or ulimit -s unlimited when using the C tree-walker on deeply recursive code. The C binary's help text spells this out explicitly. (A future refactor could spawn a worker pthread with a 64 MB stack and run eval there, making the tree-walker safe under any configuration — tracked as an optional improvement, low priority given --fast is strictly faster anyway.)

asm's remaining bottleneck is allocation, not lookup. Profiling sum-to(1M) shows ~170 MB RSS — each tail call through apply_closure + env_define allocates 24 bytes per parameter (sym / val / parent), twice per loop iteration, for 48 MB total before the three heap_grow events that follow. A future optimization candidate is per-frame batched allocation (8 + 16N bytes once per call instead of 24N), or env-cell in-place reuse for self-tail-calls. An inline cache for env lookups (ported from Python's VM) turns out to help less than anticipated because asm's env chains are typically only 2 deep and each step is a pointer dereference; measured upper bound is ~5%. The ~3× gap to C is mostly the absence of a bytecode layer and the per-call env allocation — not a lookup-path problem.

6.5 Native Container Primitives: Moving Hot Loops Into Asm

The proof-netspace server (§7) needs a hash-set to dedupe proof hashes. asm had no native hash-set, so d88149a shipped a portable one in Lumbda itself: a fixed-size vector of alists, with the bucket walk written in Scheme. It works in every tier and matches the usual chained-hash-table algorithm. But the entire inner loop — modulo for bucket index, car / cdr / = to walk the chain, cons to insert — runs through asm's tree-walker, one Scheme AST node at a time.

A native hash-set moves the same algorithm into asm: bi_hash_set_add is one hash_value call, one AND mask, one bucket-slot load, one hs_chain_find loop over raw tagged pairs, and one make_pair on miss. No environment lookups, no frame allocation, no tree-walk dispatch — the entire hot path is straight-line machine code.

Same hash function (key value for ints, djb2 for strings, identity for everything else), same 64-bucket chaining, same load factor. The ~15–20× factor is purely the cost of interpretation on the bucket walk: each Scheme-level car pays a tag check plus an eval dispatch, while the asm-level loop is two memory loads and a compare per step. Run-to-run variance on a shared laptop sits at a few percent — the ratio is stable to first order.

This matters beyond one data structure. Every container that lives in Lumbda-the-language-on-asm-the-interpreter pays the same overhead. For a server that processes thousands of proofs per minute, pulling the hash-set into the asm primitive layer erases a dominant cost. The same pattern applies to any structure with a tight inner loop: vector sort, string search, rolling checksum. Asm's tree-walker is slow on user code; asm's builtins run at the speed of the host CPU.

The layout reuses vector tag 7 with a negative sentinel at offset 0 (hash-table: -1, hash-set: -2). vector? and the printer check the sentinel to stay disjoint from real vectors. No additional tag bits were consumed — the seven-way tag mask (TAG_MASK = 7) still has room for only heap-level containers, and nothing new needs tagging because the sentinel carries the discrimination.

Reproduce: make bench-hashset (source: tests/bench-hashset.sh). Asm-only: C and Python tiers supply hash-table but not hash-set — the speedup shown here is intra-asm, native primitive vs Scheme-level implementation, not cross-tier.

6.6 Memory Management and the Meta-GC

The asm tier's default allocator is a bump pointer: every allocation advances %r15 monotonically, and nothing is ever freed. Python and C tiers have garbage collection (Python's host GC, Boehm GC_MALLOC in C); asm doesn't, by design, to keep the 6,645-line auditable surface small. Short programs finish without paying. Long-running asm servers leak until the kernel caps them — a real hazard that crashed this laptop twice during HTTP benchmarks before we wrote the six-layer safety envelope into CLAUDE.md.

To measure what a collector would actually cost, we built a second asm binary behind an assemble-time flag:

as --64 --defsym GC_NAIVE=1 lumbda.s  # collecting build
as --64                     lumbda.s  # default, bump-only

Same source, same tests (137/137 pass on both). The GC build adds an 8-byte (size << 1 | mark) header on every heap block, a stop-the-world mark-sweep triggered by bump overflow, and a free-list allocator that first-fits reclaimed space.

Control-group numbers (workload: 2,000 iterations of build-sum-discard over 200-element lists, i5-8350U, 512 MB ulimit -v):

122× less memory at a ~26% throughput cost. That is the honest GC tax at the naive end of the spectrum — the number we had been guessing at before building the control group. Every future memory-management proposal (generational, incremental, region-based) now has a concrete floor to beat.

6.6.1 Meta-GC: Arena Fast Path with Mark-Phase Verifier

On top of the naive sweep, the GC build exposes a Lumbda primitive (with-arena thunk) that takes a zero-argument procedure, runs it, and attempts an O(1) bulk reclaim of every allocation the thunk made. The decision logic is a three-way policy:

1. If an implicit GC fired inside the thunk (heap overflow forced a full sweep mid-execution), the snapshot is stale — skip the reset attempt and return.

2. Otherwise, run the existing mark phase with the thunk's return value added as an extra root, then walk the arena range [snapshot_r15, %r15) block by block. If no header in that range has the mark bit set, nothing survives — bulk-reset %r15 to the snapshot (one store) and return.

3. If any block in the arena range is marked, the thunk's return value or some other root reaches into the arena. Abort the reset, fall through to the naive sweep on the full heap, and return.

Free-list reuse is disabled while an arena is active so the chain stays pristine for a verbatim restore; heap_alloc enforces this via a global arena_active flag. One critical correctness detail: after apply_proc_raw returns from the thunk, volatile registers contain stale tagged pointers into the arena. The conservative stack scan would otherwise treat those residuals as live roots and trigger a false escape on every call. Zero-ing %rax, %rcx, %rdx, %rsi, %rdi, %rbp, %r8-%r12 before the verifier runs removes this hazard.

Meta-GC benchmark (same workload, same binary, both phases in one process):

Strategy	Wall time	Peak RSS	Full GCs	Arena outcomes
Phase A: naive sweep only	945 ms	1.2 MB	200	(unused)
Phase B: arena-wrapped body	1030 ms	1.2 MB	1	2,000 resets / 0 escapes

Phase B reclaims 205 MB via O(1) bulk resets — the work that would otherwise drive the mark-sweep path. Only one full GC fires (initial warm-up); the other 199 pressure events are replaced by arena exits. Wall time is within 1.4% of naive-only on this workload because the arena verifier's mark cost is comparable to the sweep cost it replaces. The advantage is not raw throughput but bounded per-iteration latency (no pressure-driven jitter) and the observability to prove which path actually ran.

Escape detection. When the thunk returns a heap-allocated value that the outer scope captures:

(set! escaped (with-arena (lambda () (build-list 50 '()))))

…the verifier finds the returned pair's chain marked inside the arena range, correctly aborts, and the naive sweep keeps the data live. Tested at 20 consecutive escapes: 20 escapes reported, 0 resets, (length escaped) = 50 after completion. The fall-through path is correct under load.

rate = (rate * 7 + sample * 256) / 8    # sample = 0 (reset) | 1 (escape)

allocator: reads arena_active to skip free-list reuse
gc_collect: clears arena_active on implicit trigger (snapshot stale)
verifier: returns 0 (reset) / 1 (escape) for EMA update
dispatcher: reads rate+countdown, decides verify|skip|probe

(arena-set-mode 0)   ; greedy baseline (always verify)
(arena-set-mode 1)   ; adaptive (default)

(arena-stats) -> (calls resets escapes skipped bytes-reclaimed rate)

# Old:  [size:63 | mark:1]
# New:  [size:48 | type:8 | flags:8 (mark at bit 0)]

7.1 S-Expression Portal — the Portable One

The most boring format is the most portable. An S-expression portal is a sequence of define forms:

;; Lumbda portable state
(define my-int 42)
(define my-list '(1 2 3 4 5 6 7 8 9 10))
(define my-str "hello world")
(define my-result 832040)

Every Scheme implementation in the world can already read this. No schema, no decoder, no version field. The file is a Scheme program; loading it is evaluating it.

The key insight: the language IS the interchange format. We did not design this. R. Kent Dybvig didn't. John McCarthy didn't. It is a structural consequence of homoiconicity: if the syntax of the language is the syntax of its data structures, then data serialization is language serialization. Portability across implementations is free — it arrives with the parser.

Producer side: assemble the file with (display ...) & (write ...) to an output port. Consumer side: (load "file.sexp"). Both sides exist in every implementation, giving us a 3×3 matrix of valid exchanges.

7.2 Cross-Implementation Exchange Matrix

16 of 16. Verified by tests/portal-cross-test.sh (make bench-portal-cross). The asm-gc column expands the matrix from 9 to 16 cells — the GC build's portal-save emits the same S-expression format, so it exchanges with every other tier (§7.4.1 below).

This matters because it defeats the "version lock-in" trap. If the JSON portal were the only option, a Python 3.15 producer could emit structures a C consumer couldn't parse. With S-expression portals, the only dependency is a parser that handles the subset of forms in the file. Every implementation already has one.

7.3 JSON Portal — Graph-Aware, Continuation-Preserving

When you need to preserve shared references, cycles, closures, or a live continuation, S-expressions aren't enough. The JSON portal (Python & C) performs graph-aware serialization:

• Tracks id(obj) → ref_id for object identity (handles shared refs & cycles)

• Serializes environments as chains of binding dictionaries with parent pointers

• Serializes compiled procedures as CodeObj + captured environment

• Serializes continuations as the full frame stack + machine state

• Skips builtins (reconstructed from the prelude on resume)

Deserialization is two-pass: shell pass creates empty object shells & assigns reference IDs, fill pass populates pointers & values. This handles the closure-that-captures-itself pattern cleanly.

During VM execution, portal-checkpoint! triggers at OP_JUMP & OP_TAIL_CALL instructions, capturing the current continuation, serializing it to a .portal file, & continuing. Resumption restores the saved state & continues execution from the exact instruction where the checkpoint occurred.

python3 lumbda.py --portal-resume state.portal

The computation does not need to restart from the beginning.

7.4 Binary Heap Dump — the Fast One

The no-GC asm implementation ships a direct-dump portal: write the raw heap bytes, the r14 (env) & r15 (bump pointer) registers, the heap base address, & a magic header. No parsing, no encoding.

bi_portal_save:
    # Magic | heap_size | heap_base | r14 | r15 | reserved | heap_bytes

bi_portal_resume:
    # Read 48-byte header, verify magic + sanity,
    # mmap MAP_FIXED at saved heap_base so pointers stay valid,
    # read heap bytes into fixed-address region,
    # restore r14/r15.

Sub-millisecond save & resume. The MAP_FIXED trick is why it works across processes: because every pointer inside the heap is an absolute address, resuming at a different address would require relocation. Mapping at the same address keeps pointers live.

Constraints: same architecture, same binary layout, same process model. An asm binary portal written on one box resumes on another x86_64 Linux box running the same asm binary. It does not resume on a rebuilt binary — the BSS-resident symbol table sym_table is not in the heap dump, so interned symbols would need to be reinterned. That's the price of trivial serialization.

# GC-build portal file is just Scheme source:
(define nums (quote (1 2 3 4 5)))
(define greeting (quote "hello"))
(define x (quote 42))

7.5 Cross-Process Benchmarks

Producer process A saves state to a file; consumer process B starts fresh, loads the file, continues. Wall-clock time for both processes end-to-end, 50 iterations, same-laptop. Reproduce: make bench-portal (source: tests/portal-benchmark.sh).

The asm→asm cross-process is ~160× faster than Python→Python. The binary & S-expression portals are within 10% of each other on this workload — the bottleneck is process startup, not serialization. For larger heaps the binary format pulls further ahead; for portability, S-expression always wins.

7.6 Mismatch Cases: Graceful Degradation

A usable persistence layer fails well. What happens when the consumer meets unexpected input?

All defects surfaced & fixed during benchmark development: an asm segfault on (define x) without a value (now binds to VOID), an asm portal-resume that accepted short headers (now verifies sys_read returned a full 48 bytes & sanity-checks heap metadata), a Python file not found error reporting the outer script path instead of the inner missing file (now uses FileNotFoundError.filename). Graceful degradation is not free; it is tested.

7.7 Use Case: Distributed Primality Testing

(define (prime? n)
  (let loop ((i 2) (checks 0))
    (cond
      ((> (* i i) n) #t)
      ((= (remainder n i) 0) #f)
      (else
       (when (= (remainder i 10000) 0)
         (portal-checkpoint! "prime-state.portal"))
       (loop (+ i 1) (+ checks 1))))))

(define result (prime? 1000000007))

Machine A starts the computation. Every 10,000 iterations, it writes a checkpoint. Machine B picks up the .portal file & continues from the last checkpoint. The computation migrates without either machine needing to know about the other. Feedback — the continuation — carries the entire execution context.

8.1 The Operator

(define (eml x y) (- (exp x) (log y)))

With this operator & the constant 1, the following derivation chain constructs every elementary function:

8.2 Stage 1: Core Functions (Depth 1--3)

exp(x) = eml(x, 1)                        ; ln(1) = 0, so eml(x,1) = exp(x) - 0
e      = eml(1, 1)                         ; exp(1) = e
ln(x)  = eml(1, eml(eml(1,x), 1))         ; nested application recovers ln

Proof of ln recovery: Let a = eml(1,x) = e - ln(x). Then eml(a, 1) = exp(e - ln(x)) = exp(e)/x. Then eml(1, exp(e)/x) = e - ln(exp(e)/x) = e - e + ln(x) = ln(x).

8.3 Stage 2: Arithmetic

0          = ln(1) = eml(1, eml(eml(1,1), 1))
a - b      = eml(ln(a), exp(b))            ; exp(ln(a)) - ln(exp(b)) = a - b
-1         = (e-1) - e                      ; via eml subtraction chain
a * b      = exp(ln(a) + ln(b))            ; multiplication from exp & ln
1/x        = exp(-ln(x))                   ; division from exp & ln
x^y        = exp(y * ln(x))                ; exponentiation
sqrt(x)    = exp(ln(x) / 2)               ; roots

8.4 Stage 3: Complex Plane Access

ln(-1) = iπ                                ; standard complex logarithm
π = imag(ln(-1))
i = exp(iπ/2)

The key insight: ln of a negative number enters the complex plane. Since we can construct -1 from eml via the subtraction chain, ln(-1) yields iπ, from which π & i follow.

8.5 Stage 4: Trigonometry via Euler

sin(x) = (exp(ix) - exp(-ix)) / 2i        ; Euler's formula
cos(x) = (exp(ix) + exp(-ix)) / 2
tan(x) = sin(x) / cos(x)

All trigonometric functions follow from complex exponentials, which follow from exp, which follows from eml.

8.6 Verification & Friction Analysis

The proof has been verified at six distinct levels. Times are best-of-3 on the i5-8350U:

Three separate wins compound here.

1. Algorithmic: symbolic vs numerical — the Lumbda symbolic rewriter is ~1,280× faster than the Lumbda brute-force search (46 ms vs 59 s). This is the MOAD-0001 defect at the proof-methodology layer: O(N²) enumerate-and-compare where O(1) algebraic reasoning suffices. The brute-force version enumerates every pairwise EML composition at each depth, comparing results against target functions; the symbolic checker applies 5 rewrites using 3 axioms (exp(ln(x)) = x, ln(exp(x)) = x, ln(1) = 0) and terminates. Understanding beats search by three orders of magnitude.

2. Runtime: asm vs compiled-Lean-binary — with the same symbolic strategy on both sides, Lumbda asm at 46 ms is ~16× faster than Lean 4's cold rebuild (722 ms). The asm interpreter is already a binary; Lean has to go through lake build, link the kernel, and spin up before verifying. No algorithmic advantage — just the startup tax Lean pays to guarantee a smaller trusted computing base.

3. Caching: artifact replay — both checkers now write a small success-artifact on pass and short-circuit on subsequent runs if the magic header matches. Cached Lumbda (7 ms) and cached Lean (5 ms) are essentially "read one file and print five lines." The 16× cold gap collapses to ~1.5×. rm -f /tmp/lumbda-eml.cache (analogous to lake clean) forces a cold re-check and the full numbers return.

Symmetric honesty. Lean's kernel guarantees remain stronger even when the timings equalize: the Lean TCB is ~3 KLOC of audited elaborator/kernel, while Lumbda's asm interpreter is ~6.6 KLOC of hand-written assembly. For proofs where the cost of a bug in the checker itself matters, Lean is the right tool; for small symbolic-rewrite proofs where the language hosting the proof should be able to host the checker too, Lumbda does the job in under 50 ms cold without external dependencies.

Lesson: The fastest path to truth is not computation — it is understanding. When you know why eml(1, eml(eml(1,x), 1)) = ln(x), you verify it in microseconds. When you don't, you search for hours. Symbolic reasoning eliminates the quadratic friction of numerical verification; caching eliminates the startup friction of every verifier. Both layers stack.

Reproduce: make bench-proof runs the cold and cached paths for both Lumbda (across all three tiers) and Lean. Source: proof/benchmark.sh.

1. Numerical verification (proof/eml_proof.py): Python script using cmath at high precision. Verifies every derivation step with tolerance 1e-10. Includes brute-force tree search at depth ≤ 4 confirming that eml compositions reach the expected targets.

2. Self-hosted verification (proof/eml_proof.lsp): The same proof runs in Lumbda's bytecode VM (python3 lumbda.py --fast proof/eml_proof.lsp). The language verifies its own mathematical foundations.

3. Formal proof (proof/lean/EmlProof/Basic.lean): Lean 4 proof with zero sorry. Five theorems:

eml_is_exp  : eml(x, 1) = exp(x)
eml_is_e    : eml(1, 1) = exp(1) = e
eml_is_ln   : eml(1, eml(eml(1,x), 1)) = ln(x)
eml_is_zero : eml(1, eml(eml(1,1), 1)) = 0
eml_is_sub  : eml(ln(a), exp(b)) = a - b

The Lean proof operates over abstract exp & ln functions with the axioms exp(ln(x)) = x, ln(exp(x)) = x, & ln(1) = 0. This makes the result independent of any particular real number implementation.

4. Native Lumbda proof checker (proof/eml_proof_in_lumbda.lsp): a ~150-line term-rewriting engine written in portable Scheme that verifies the five theorems by symbolic rewriting — no external Lean binary, no numerical evaluation. Same abstract axioms, same five theorems, same pass/fail oracle. Runs byte-identically in Python, C, and asm. This is not a replacement for Lean on real proof work — it is a demonstration that when the proofs you need are simple symbolic rewrites, the language hosting the proof can host the checker too. Lumbda runs its own proof of a mathematical claim it cares about, with no external verifier in the loop.

PASS: eml_is_exp
PASS: eml_is_e
PASS: eml_is_ln
PASS: eml_is_zero
PASS: eml_is_sub
ALL EML THEOREMS VERIFIED IN LUMBDA

Verification speed: Lean vs Lumbda tiers, both cold and cached. Same five theorems, same symbolic-rewrite strategy. The Lumbda checker now implements its own cached-replay path that mirrors Lean's: write a small artifact after a successful run; on subsequent runs, trust the artifact if the magic header matches and skip re-verification. rm -f /tmp/lumbda-eml.cache forces a cold re-check (analogous to lake clean). Best of 3 on the i5-8350U:

Two comparisons matter. Cold vs cold is the honest end-to-end compare: Lumbda asm (46 ms) verifies the proof ~16× faster than Lean's cold rebuild (722 ms) on the same hardware, because Lumbda doesn't link a compiled binary or spin up a kernel — it just runs a rewriter over five small terms. Cached vs cached is the throwaway benchmark but still interesting: Lumbda asm at 7 ms vs Lean at 5 ms, within 1.5×, on what is essentially "read a file and print five lines."

All four Lumbda tiers verify the proof. A C --fast bytecode-compiler bug originally caused the final tier to hang on the rewriter's named-let loop; narrowed to a minimal reproduction (see c/TODO-named-let-bytecode.md) and worked around in the proof file by using an internal recursive define in place of the offending named-let. All four tiers now complete in under 100 ms cold. Reproduce: make bench-proof (source: tests/bench-proof.sh).

First machine-checked treatment. The original paper (Odrzywołek, arXiv:2603.21852v2, 2026-04-04) presents the EML universality claim analytically — pure LaTeX mathematics, no formal tool. The companion Zenodo artifact is symbolic-regression / gradient-optimization code, not a verification. To our knowledge the Lean 4 proof shipped in this repo is the first machine-checked treatment of the EML identities, and the accompanying Lumbda-native checker is the first self-hosted machine-checked version. Five theorems, zero sorry, no Mathlib dependency — ~1,280× faster than the brute-force numerical search it replaced once the symbolic rewriter was written (see §8.6 for the full six-row comparison), and carrying the additional guarantee that no implementation quirk of floating point can ever break the conclusion.

11.1 Test Coverage

980 verified assertions across all implementations, all green under make test-all:

• Python unit + integration: 571 tests (tests.py)

• C unit + integration + JIT + continuations + portal: 83 tests (c/test.c)

• Assembly unit + integration + functional: 137 tests (asm/test.sh), passing identically under both the bump-only and GC_NAIVE builds

• Shared functional (same .lsp in Python + C): 189 tests (tests/functional.lsp)

The shared functional suite matters: it runs byte-identical Scheme source through two different runtimes & compares output. Python & C agree 189 times per run. When they disagree, that tells us something specific & actionable.

Cross-implementation portal exchange is verified separately: tests/portal-cross-test.sh runs 9 producer×consumer combinations. All 9 green.

11.2 File I/O Parity

All three implementations share the same minimal file I/O vocabulary — discovered necessary while building the cross-impl portal:

The asm port representation deserves a note. Because all three tag bits are consumed by the existing value types (int/pair/sym/closure/builtin/special/string/vector), we encode ports as SPECIAL values ≥ 1000: port_val = ((PORT_SPECIAL_BASE + fd) << 3) | TAG_SPECIAL. Extraction is fd = (val >> 3) - PORT_SPECIAL_BASE. port? is a range check. No tag expansion, no heap object, no allocator pressure — the port is the file descriptor, wrapped.

11.3 Sockets: One HTTP Server, Three Runtimes

Six primitives extend the file-I/O vocabulary to TCP:

Sockets share the same port representation as files — in asm the fd is packed into SPECIAL values ≥ 1000, in Python + C the fd lives inside an existing ULPort struct. read/write unify because to Linux a socket is just an fd.

examples/http-server.lsp is a 90-line HTTP/1.0 server. It parses a request line, dispatches by path, and returns 200/404 with Content-Length. The same file runs unmodified in all three impls:

python3 lumbda.py --fast examples/http-server.lsp
./c/lumbda examples/http-server.lsp
./asm/lumbda < examples/http-server.lsp

The companion examples/http-client-bench.lsp is a 45-line load generator using only the six tcp-* primitives plus current-time-ms. In-process client eliminates the ~2 ms/request fork overhead that curl-based benchmarks suffer, so real server throughput shows through. Reproduce: make bench-web (source: tests/web-benchmark.sh).

(The asm-server / asm-client pair is the fastest cell here — 2,994 req/s from a 22 KB binary, served & driven by the same 22 KB binary.)

For external comparison: python3 -m http.server and busybox httpd both land around 382 req/s under a curl client on the same machine. When driven by an in-process client they hit the same ceiling as our servers — the bottleneck has always been the client fork/exec, not the server.

What's remarkable is not the speed. It is that a 22 KB binary with zero libc dependency and seven canonical Linux syscalls plus the socket family runs HTTP as fast as anything else on the machine, with a protocol handler written in portable Scheme that runs byte-for-byte in all three runtimes. The asm binary is 96× smaller than busybox httpd (2.1 MB) and 360× smaller than the Python interpreter alone (8 MB).

11.4 S-expressions over Sockets: RPC, REPL, and Chains

The HTTP example sends request-line bytes and response-line bytes. Those bytes don't have to be HTTP. If both sides of the wire speak Scheme, the wire protocol can be Scheme source itself — the reader is already the parser you need. Two new builtins close the loop in all three impls:

• (read-from-string s) — parse one S-expression from a string, return the value

• (eval expr) — evaluate a Scheme value in the global env (Python and C already had this as a special form; asm gains it as an 89-byte builtin)

Two server patterns emerge:

Whitelisted RPC (examples/rpc-server.lsp, 90 lines). The server reads a request sexp, dispatches by car on a closed set (ping, add, mul, fib, echo), never calls eval on client input. Safe by construction. Uses heap-snapshot/heap-restore for O(1) memory on asm.

Full remote REPL (examples/repl-server.lsp, 70 lines). The server reads a request sexp and passes it straight to eval. Persistent global env across connections; (define x 42) from one call is visible from the next. DANGER: any reachable client can run arbitrary Scheme in-process. Deliberately does not use heap-snapshot because remote define adds bindings past any snapshot point; the ulimit -v safety cap (512 MB) backstops the leak.

Both patterns run byte-identically in Python, C, and asm. The 3×3 server×client matrix is 9/9 green — any runtime can host either side.

Chains: relays across runtimes. A transparent relay (examples/rpc-relay.lsp, 50 lines) accepts a connection, forwards the request bytes to a backend without parsing, relays the reply back. Because the envelope is Scheme source and the relay never opens it, chains of arbitrary runtimes compose naturally:

Each relay hop costs ~650 µs (one full TCP round-trip + context switches on the same host, no actual parsing work). The relay never allocates anything beyond a transient buffer; on asm it uses heap-snapshot/heap-restore to keep memory flat under load. Four runtimes strung together through two relay machines, the same .lsp on every hop. Reproduce: make bench-rpc-chain (source: tests/rpc-chain-bench.sh).

The result is not a performance story — it is a composition story. S-expressions are the envelope and the payload. A 22 KB binary can be a backend, a relay, a client, or any point in a chain; the protocol needs no separate definition because the protocol IS the language.

11.5 Portal over HTTP: State Transfer Between Machines

The HTTP server carries request bytes. The portal serializes machine state to bytes. Combine them: a node exposes its state as an HTTP endpoint, another node pulls that endpoint down and resumes. This was the first item in §13 Future Work — it is now a running demo.

examples/portal-http-server.lsp holds some state (integer counter, list, string, the result of fib(30)) and answers GET /portal with an S-expression portal body — literally a sequence of (define ...) forms.

examples/portal-http-client.lsp dials the endpoint, strips the HTTP headers, splits the body by newline, and for each non-empty, non-comment line calls (eval (read-from-string line)). The remote bindings become local.

;; server-side (excerpt)
(define (portal-body)
  (string-append
    "(define counter " (number->string counter) ")\n"
    "(define my-fib " (number->string my-fib) ")\n" ...))

;; client-side (excerpt)
(define resp (tcp-recv sock 65536))
(define body (body-of resp))
(eval-all-lines body)       ; iterates, calls (eval (read-from-string line))
(display counter)           ; => the server's counter value
(display my-fib)            ; => 832040

3×3 matrix green: Python/C/asm in any role — server or client or both — exchange state correctly. All nine combinations verified. examples/portal-http-client.lsp is 90 lines of portable Scheme; the full round-trip uses only the six tcp-* primitives plus read-from-string, eval, and standard string manipulation.

The client needs eval semantics that install define-bindings in the global env regardless of the dynamic scope of the eval call. Python and C originally evaluated the eval result in the caller's env, which worked at top level but silently failed inside a helper function. A two-line fix in each (env = env.g in Python's leval, env = env->global in C's SYM_EVAL branch) aligns both with asm's long-standing bi_eval behavior.

This is the closing demonstration of "feedback is all you need" extended across all four scopes. A continuation-style value — here, a set of bindings — travels:

• within a process via call/cc

• across processes on the same host via portal files

• across implementations that share no binary compatibility via S-expression serialization

• across machines via sockets (HTTP, RPC, raw TCP)

The wire protocol and the language are the same artifact. A 22 KB binary can be any node in any chain of any scope.

11.6 heap-snapshot: The Arena Escape Hatch

The asm bump allocator has no GC. Every string-append, tcp-recv, make-pair, or similar per-request allocation grows r15. Over a long-running server that is an unbounded leak — an incident on 2026-04-16 drove an asm server to 19.3 GB RSS before being killed.

Two new builtins fix this without introducing a collector:

(heap-snapshot)           ; => opaque int (current r15)
(heap-restore snap)       ; => void (rewinds r15 to snap)

Python + C expose the same names as no-ops (their real GCs already handle this). Portable Scheme can call them unconditionally.

The pattern is narrow by design:

(define *snap* (heap-snapshot))   ; captured AFTER top-level binds
(define (loop n snap)
  ...
  (heap-restore snap)             ; every allocation since snap is now garbage
  (loop (+ n 1) snap))

The snapshot is dangerously precise: anything allocated after the snap and still reachable after the restore becomes a dangling pointer. The canonical pattern (HTTP request scope) allocates per-request and discards per-request — nothing escapes. Measured asm RSS with this pattern: 88 KB initial, 100 KB after 1,100 requests. Flat.

This is not a general-purpose allocator. It is an escape hatch the programmer uses when they can prove the scope boundary. For general programs on asm, the heap still grows. For the HTTP server pattern, O(1) memory costs two lines of code.

11.7 Static File Serving: Cache, Sendfile, and Adaptive Preload

The HTTP demo in §11.3 served synthesized responses. To host lumbda.com we needed a real static-file path — something that hands a 2.67 MiB PDF (this whitepaper) off the disk without bouncing it through the Scheme heap. Three variants now ship in examples/, each ~100–200 lines of portable Scheme, each running on asm/lumbda-gc (the GC build, 27 KB stripped).

• http-static-server.lsp — read the file per request via file->string, build a response, send. Baseline. Correct and portable across all four tiers; every 2.67 MiB PDF round-trip allocates 2.67 MiB of Scheme string.

• http-static-server-cached.lsp — on startup, build a hash-table keyed by URL path to the full pre-composed HTTP response (headers + body). Per-request handler is one hash-table-ref/default. No file->string, no string-append, no MIME lookup in the hot path.

• http-static-server-sendfile.lsp — small assets (≤ 16 KB) stay inline-cached as full responses; large assets cache only the headers and stream the body via a new tcp-sendfile primitive that issues the Linux SYS_SENDFILE (40) syscall directly. Zero-copy kernel → socket, no userspace bounce.

tcp-sendfile is a 90-line asm-gc builtin. It opens the path, lseek's to find the size, then loops sendfile(2) until the full body is written, and close()'s. The body never enters the Lumbda heap — headers are composed in Scheme and flushed via tcp-send, then the kernel DMAs the file directly into the socket buffer.

Four-way race (tests/bench-www-race.sh, i5-8350U, 1000 small requests, 100 large requests, concurrency 8, xargs -P 8 curl, adjacent runs):

All four servers return the PDF byte-identical against the on-disk master. The sendfile path lands within 2% of Caddy on throughput while holding 9× less peak RSS in a binary 1,400× smaller (27 KB stripped vs 38 MB). Small-request throughput (GET /) is essentially flat across the three lumbda variants — the cached path already removed per-request work, so sendfile's win is entirely on large bodies.

Adaptive preload: ``http-static-server-adaptive.lsp``. A hit-counter hash-table (URL → integer) is updated every request. Every N requests the counter is flushed to www.hits as newline-delimited path count records. On startup the file is loaded, sorted descending, and the top cache-max URLs are preloaded — so each boot reflects what the previous run actually served. Cold start falls back to a seed list (/ and /404.html). Cold requests beyond the seed set are promoted into the cache on first hit until the cap is reached. Because this server mutates persistent state (the counter and the cache) on every request, the arena-pattern heap-restore is dropped and the GC build's mark-sweep reclaims transients instead.

For small deployments (≤ ~1000 resources) this is ~95% of the win of a full predictive-preload system: the top few URLs dominate traffic and get pinned at boot. Anything rarer warms on demand. The remaining 5% — predicting which URLs will be needed from co-occurrence rather than raw frequency — is §13 Future Work.

12.1 MOAD-0001: The Sedimentary Defect in Our Own Code

The assembly interpreter's intern_symbol used a linear scan through all interned symbols — O(N) per lookup, O(N²) over a program's lifetime. For a program defining 34 builtins plus user symbols, every define, every lambda parameter, every variable reference walked the entire table.

Before (linear scan):

.isym_search:
    cmpq %rcx, %r8        # compare lengths
    jne .isym_next
    rep cmpsb              # compare bytes
    je .isym_found
.isym_next:
    addq $24, %rax         # next entry
    jmp .isym_search       # O(N) per intern

After (djb2 hash table, 1024 buckets):

.intern_hash:
    imulq $33, %rax        # djb2: hash = hash * 33 + c
    addq %rcx, %rax
    loop .intern_hash
    andq $1023, %rax       # bucket = hash & (1024-1)
    # O(1) average lookup

The fix: 99 lines changed, 1024-bucket hash table with chaining. 2.9x faster on a 2000-symbol stress test. On benchmarks with fewer symbols (ack, fib), the improvement is modest (15% on sum-to(50k)), because the linear scan was already fast at small N. The fix pays off at scale — the same pattern as MOAD-0001 everywhere: invisible at small inputs, catastrophic at large ones.

The Python implementation had a similar defect: _define_record_type used list.index() for field lookup. Replaced with a dict. O(N) → O(1).

Two more MOAD-0001 defects surfaced during the HTTP server work and were fixed in the same pass:

• c/builtins.c's bi_string_replace scanned the source byte-by-byte, calling strncmp(src, from, from_len) at every position. O(N·k). Replaced with strstr (libc-tuned, typically Boyer-Moore-Horspool) called in a loop that skips to the next match. O(N + matches·k).

• lumbda.py's _tokenize_lines called src.count('\\n', 0, m.start()) per token to compute line numbers. O(N·M). Replaced with a single pass that builds a line_starts array, then bisects per token. O(M + N log M).

A third correctness fix landed after the portal-over-HTTP demo exposed it: lumbda.py's Env.lookup used to short-cut from the local frame directly to the global frame before walking intermediate parents. That was fast but wrong — a let-loop parameter named the same as a global builtin (count, a SRFI-1 procedure) got shadowed in reverse, the shortcut returned the global builtin instead of walking up to the loop's parameter frame. Fix: walk self → self.p → ... → global in order, without any shortcut. The inline cache at OP_LOOKUP was correspondingly tightened to validate the full chain before firing. 980 tests remained green.

Every release audit surfaces more. Writing new code is writing new sediment, unless the audit runs.

12.2 MOAD-0002: The Intertangle in Our Own Design

All three implementations share mutable global state between subsystems:

• Assembly: The global environment lives in register %r14. Every define, set!, and eval mutates it directly. This works because the assembly interpreter is single-threaded & sequential, but it means the evaluator, the environment manager, & the builtin system are inseparable. You cannot test one without the others.

• C: Thread-local g_error_ctx, cc_escape_val, & cc_active_jmp couple error handling & call/cc across all modules. These are necessary for setjmp/longjmp but they mean the JIT, the evaluator, & the continuation system cannot be reasoned about independently.

• Python: _portal_checkpoint, _call_stack, _modules, _record_types, _auto_compile — five module-level mutable globals that different subsystems read & write. The portal system, the error reporter, the module loader, & the compilation strategy are all coupled through shared state.

We documented these rather than refactoring them. In each case, the coupling exists for performance (the globals are on hot paths) or necessity (setjmp requires thread-local state). The documentation makes the coupling visible so future work can decouple selectively.

12.3 Our Shared Infrastructure

Every MOAD we fixed in our own code is a MOAD we understand better when we find it in others. The sedimentary defect in intern_symbol is the same pattern as the sedimentary defect in Lean 4's check_duplicated_univ_params. The intertangle in our global environment register is the same pattern as the intertangle in any system that routes state through implicit globals instead of explicit parameters.

Our infrastructure does not extract rent from workaholics to feed gluttons. A symbol table that does O(N) work per lookup is a workaholic node — it does more work than necessary on every operation, and that cost compounds through every downstream consumer. Fixing it reduces stress on our shared computational heart. The CPU cycles saved are cycles available for the next lambda, the next continuation, the next portal resume.

This is the permacomputer obligation: infrastructure that renews itself. Code that gets faster as we understand it better. A hash table is not an optimization — it is the removal of unnecessary suffering from a system that deserves better.