engineering/lumbda
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

whitepaper: add bend chapter, fifth scope of feedback, source link

Browse source 
Folds 76 commits of substance since 2026-04-24 into the whitepaper
without losing any of the novel cross-domain glue the language earns
its keep on.

Additions
- §4.3 extended from four scopes to five, with bend as feedback across
  heterogeneous compute (host ↔ GPU). New diagram
  diagrams/five-scopes-feedback.png stacks the boundaries.
- §11.8 Bend: cross-tier GPU dispatch. Wire modes (S-exp text, BSHK
  binary), worker hosting per tier, spawn-process-stdio + flush-port
  cross-tier IPC, worker health heartbeat with VRAM-ranked pick,
  6-row catalog of live forms (cuda-shake-fanout, cuda-secp256k1-mul,
  cuda-bignum-cgbn, cuda-radix-sort, cuda-blake3-tree,
  cuda-sim-ops-bin). New diagram diagrams/bend-dispatch.png.
- §2.1 C-tier bignum: arbitrary-precision integers (Boehm-GC managed),
  which unblocked the secp256k1 widths the GPU forms need on the host
  side.
- §12.1 post-cycle audit: recv-exact O(n²)→O(n), asm scheme_read
  overflow, asm gc_sweep page-fault, C-tier JIT cur_code restore
  across CALL/RETURN.
- §13 GPU Phase 1 moved from future to shipped; Phase 2 trampolining
  and Phase 3 interaction combinators sharpened.
- Source repo link (git.unturf.com/engineering/unturf/lumbda) added
  to the cover page band and the Citation block.

Compressions (no novel glue dropped — audited per fox's constraint)
- §8.2-§8.5 EML derivation prose collapsed into a single §8.2
  derivation chain code block; §8.6 renumbered to §8.3.
- §6.6.3 adaptive-meta-GC narrative compressed; result table kept.
- §7.4.1 GC-build S-expression portal tightened to two paragraphs;
  "language is its own wire format" insight kept.

Preserved in full per audit
- §7.5 portable RNG state across tiers
- §7.5.1 one-side kernel entropy + portable bit-identical continuation
- §11.7 sendfile + adaptive preload (27 KB asm-gc within 2% of Caddy)
- §6.6.1 collaborative arena + mark verifier
- §6.6.5 precise block typing
- §8.1 + §8.3 Lumbda hosts its own EML proof checker, ~16× faster
  than Lean cold

Net RST: 1622 → 1655 lines.
This commit is contained in:
russell@unturf.com 2026-06-07 10:49:48 -04:00
parent d9f4e38222
commit 661f9a01ec
No known key found for this signature in database
9 changed files with 2990 additions and 2478 deletions
Download patch file Download diff file Expand all files Collapse all files

97
docs/bend-dispatch.dot Normal file
View file

@ -0,0 +1,97 @@
// Bend cross-tier GPU dispatch — 2026-06-07
// "A diagram is worth 10,000 words." — russell@unturf.com
//
// One (bend …) form. The dispatcher picks local vs worker per call.
// When it goes remote, the wire frame is either S-expression text
// (small payloads, parser cost dominates) or a 4-byte magic + raw
// bytes (huge payloads). Workers spawn a leaf CUDA binary via each
// tier's native process-spawn primitive. CUDA kernel returns bytes
// back through the same wire frame.
digraph bend_dispatch {
rankdir=LR
splines=true
nodesep=0.45
ranksep=0.7
node [shape=box, style="filled,rounded", fontname="Helvetica", fontsize=11, margin="0.18,0.10"]
edge [fontname="Helvetica", fontsize=9, arrowsize=0.85]
label="Bend — one (bend …) form across host, wire, worker, and GPU"
labelloc=t
fontsize=14
fontname="Helvetica Bold"
// ─── Caller side ────────────────────────────────────────────────
subgraph cluster_caller {
label="Caller tier (any of Python / C / asm)"
labelloc=t
style="rounded,filled"
fillcolor="#e8f4f8"
color="#0984e3"
fontname="Helvetica Bold"
fontsize=11
fontcolor="#0984e3"
call [label="(bend! …) form\nin user code" fillcolor="#b3d9e8"]
cost [label="cost estimator\n(local vs wire)" fillcolor="#d6eaf8"]
local [label="evaluate locally\n(small payloads)" fillcolor="#aed6f1"]
call -> cost
cost -> local [label="cheap" fontcolor="#1f618d"]
}
// ─── Wire ──────────────────────────────────────────────────────
subgraph cluster_wire {
label="Wire — port 8320 (BEND)"
labelloc=t
style="rounded,filled"
fillcolor="#fff8e1"
color="#f57f17"
fontname="Helvetica Bold"
fontsize=11
fontcolor="#f57f17"
sexp [label="S-expression\n(text)\n— small payloads" fillcolor="#ffe082"]
bin [label="binary frame\nmagic + raw bytes\n— huge payloads\n(BSHK, BCGB, BSCP,\n BSRT, BSB3, …)" fillcolor="#ffd54f"]
}
cost -> sexp [label="≤ ~1k inputs" fontcolor="#f57f17"]
cost -> bin [label="≥ ~1k inputs\n(150× over S-exp\n at 1 M)" fontcolor="#f57f17"]
// ─── Worker side ───────────────────────────────────────────────
subgraph cluster_worker {
label="Worker tier (any of Python / C / asm — listens on :8320)"
labelloc=t
style="rounded,filled"
fillcolor="#e8f5e9"
color="#2e7d32"
fontname="Helvetica Bold"
fontsize=11
fontcolor="#2e7d32"
recv [label="gpu-worker\nrecv + dispatch\n+ health" fillcolor="#a5d6a7"]
spawn [label="spawn-process-stdio\n— Py: subprocess.Popen\n— C: fork + execve\n— asm: pipe2+fork+execve\n (raw syscall, no libc)" fillcolor="#c8e6c9"]
recv -> spawn
}
sexp -> recv
bin -> recv
// ─── Leaf CUDA binary + GPU ────────────────────────────────────
subgraph cluster_gpu {
label="Leaf CUDA binary + RTX 3090"
labelloc=t
style="rounded,filled"
fillcolor="#f3e5f5"
color="#7b1fa2"
fontname="Helvetica Bold"
fontsize=11
fontcolor="#7b1fa2"
leaf [label="shake256-fanout /\nsecp256k1-batch-mul /\ncgbn-batch-worker /\nblake3-fanout /\nradix-sort /\ndemo_ops …" fillcolor="#ce93d8"]
kernel [label="CUDA kernel\n(byte-identical\n vs host reference)" fillcolor="#ba68c8"]
leaf -> kernel
}
spawn -> leaf [label="stdin / stdout" fontcolor="#7b1fa2"]
// ─── Return path ───────────────────────────────────────────────
kernel -> leaf [label="bytes back" fontcolor="#7b1fa2" style=dashed]
leaf -> spawn [style=invis]
spawn -> recv [label="result" style=dashed fontcolor="#2e7d32"]
recv -> cost [label="wire frame back" style=dashed fontcolor="#f57f17" constraint=false]
local -> call [label="value" style=dashed fontcolor="#1f618d" constraint=false]
}

BIN
docs/bend-dispatch.png Normal file
View file

Binary file not shown.
Side by side

After

Width:  |  Height:  |  Size: 126 KiB

105
docs/five-scopes-feedback.dot Normal file
View file

@ -0,0 +1,105 @@
// Five scopes of feedback — 2026-06-07
// "A diagram is worth 10,000 words." — russell@unturf.com
//
// One primitive (feedback) at five nested boundaries. Each row shows what
// crosses, the mechanism that lets it cross, and the implementation
// primitive that makes the mechanism real. The rows stack so a reader
// can run their eye top-to-bottom and see the abstraction widen.
digraph five_scopes {
rankdir=TB
splines=true
nodesep=0.4
ranksep=0.35
node [shape=box, style="filled,rounded", fontname="Helvetica", fontsize=11, margin="0.15,0.08"]
edge [fontname="Helvetica", fontsize=10, arrowsize=0.8]
label="Five scopes of feedback — one primitive, five boundaries"
labelloc=t
fontsize=14
fontname="Helvetica Bold"
// Row 1 — within process
subgraph cluster_1 {
label="① Within process — call/cc continuation (live)"
labelloc=b
style="rounded,filled"
fillcolor="#e8f4f8"
color="#0984e3"
fontname="Helvetica Bold"
fontsize=11
fontcolor="#0984e3"
rank=same
n1a [label="frame stack" fillcolor="#b3d9e8" color="#0984e3"]
n1b [label="frame stack" fillcolor="#b3d9e8" color="#0984e3"]
n1a -> n1b [color="#0984e3" penwidth=1.8]
}
// Row 2 — across process
subgraph cluster_2 {
label="② Across process — portal (VM state + continuation)"
labelloc=b
style="rounded,filled"
fillcolor="#e8f5e9"
color="#2e7d32"
fontname="Helvetica Bold"
fontsize=11
fontcolor="#2e7d32"
rank=same
n2a [label="process A (any tier)" fillcolor="#a5d6a7" color="#2e7d32"]
n2b [label="process B (any tier)" fillcolor="#a5d6a7" color="#2e7d32"]
n2a -> n2b [color="#2e7d32" penwidth=1.8]
}
// Row 3 — across impl
subgraph cluster_3 {
label="③ Across impl — source-as-data (the reader)"
labelloc=b
style="rounded,filled"
fillcolor="#fff8e1"
color="#f57f17"
fontname="Helvetica Bold"
fontsize=11
fontcolor="#f57f17"
rank=same
n3a [label="Python tier" fillcolor="#ffe082" color="#f57f17"]
n3b [label="C / asm tier" fillcolor="#ffe082" color="#f57f17"]
n3a -> n3b [color="#f57f17" penwidth=1.8]
}
// Row 4 — across machine
subgraph cluster_4 {
label="④ Across machine — TCP socket (request / response bytes)"
labelloc=b
style="rounded,filled"
fillcolor="#fce4ec"
color="#c2185b"
fontname="Helvetica Bold"
fontsize=11
fontcolor="#c2185b"
rank=same
n4a [label="machine M1" fillcolor="#f8bbd0" color="#c2185b"]
n4b [label="machine M2" fillcolor="#f8bbd0" color="#c2185b"]
n4a -> n4b [color="#c2185b" penwidth=1.8]
}
// Row 5 — across compute
subgraph cluster_5 {
label="⑤ Across compute — (bend …) form (S-exp or BSHK binary)"
labelloc=b
style="rounded,filled"
fillcolor="#f3e5f5"
color="#7b1fa2"
fontname="Helvetica Bold"
fontsize=11
fontcolor="#7b1fa2"
rank=same
n5a [label="host CPU (any tier)" fillcolor="#ce93d8" color="#7b1fa2"]
n5b [label="CUDA worker + kernel" fillcolor="#ce93d8" color="#7b1fa2"]
n5a -> n5b [color="#7b1fa2" penwidth=1.8]
}
// Invisible chain forces vertical stacking of clusters.
n1a -> n2a [style=invis]
n2a -> n3a [style=invis]
n3a -> n4a [style=invis]
n4a -> n5a [style=invis]
}

BIN
docs/five-scopes-feedback.png Normal file
View file

Binary file not shown.
Side by side

After

Width:  |  Height:  |  Size: 80 KiB

BIN
whitepaper/diagrams/bend-dispatch.png Normal file
View file

Binary file not shown.
Side by side

After

Width:  |  Height:  |  Size: 126 KiB

BIN
whitepaper/diagrams/five-scopes-feedback.png Normal file
View file

Binary file not shown.
Side by side

After

Width:  |  Height:  |  Size: 80 KiB

190
whitepaper/lumbda-whitepaper.html
View file

File diff suppressed because one or more lines are too long

4852
whitepaper/lumbda-whitepaper.pdf
View file

File diff suppressed because one or more lines are too long

224
whitepaper/lumbda-whitepaper.rst
View file

@ -49,6 +49,10 @@ lumbda.
.. class:: center
Source: `git.unturf.com/engineering/unturf/lumbda <https://git.unturf.com/engineering/unturf/lumbda>`_
.. class:: center
*April 2026*
----
@ -129,7 +133,7 @@ Core types stay minimal:
- **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.
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. The C tier carries the matching integer story through a runtime-promoted bignum: small integers stay tagged 63-bit ``int64_t`` on the fast path, and any operation that would overflow promotes to an arbitrary-precision representation (Boehm-GC-managed). The promotion is invisible to Scheme code — ``(expt 2 1024)`` returns the exact value across all three tiers. This is what unblocked the secp256k1 widths used by the §11.8 GPU forms; the bend dispatcher would not have been honest with cropped 64-bit arithmetic on the host side.
2.2 The Bytecode
^^^^^^^^^^^^^^^^
@ -284,26 +288,33 @@ Every control flow pattern reduces to a continuation operation:
One primitive. Every pattern.
4.3 Four Scopes of Feedback
4.3 Five Scopes of Feedback
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
The single word "feedback" covers four nested scopes, each giving rise to one of our core abstractions:
The single word "feedback" covers five nested scopes, each giving rise to one of our core abstractions:
.. table::
:widths: 18 26 26 26
=============== ========================= ========================= ==========================
Scope Mechanism Unit of travel Implementation
=============== ========================= ========================= ==========================
Within process ``call/cc``, tail-call continuation (live) explicit frame stack
Across process portal (JSON or binary) VM state + continuation graph serializer
Across impl source-as-interchange bindings (as data) the reader
Across machine TCP sockets request / response bytes six tcp-* primitives
=============== ========================= ========================= ==========================
================ ========================= ========================= ==========================
Scope Mechanism Unit of travel Implementation
================ ========================= ========================= ==========================
Within process ``call/cc``, tail-call continuation (live) explicit frame stack
Across process portal (JSON or binary) VM state + continuation graph serializer
Across impl source-as-interchange bindings (as data) the reader
Across machine TCP sockets request / response bytes six tcp-* primitives
Across compute ``(bend ...)`` call shipped to worker wire protocol + spawn
================ ========================= ========================= ==========================
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.
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. Across heterogeneous compute (CPU ↔ GPU), a single ``(bend ...)`` call is the unit — the runtime decides per call whether the form evaluates locally or ships to a CUDA worker, and the answer feeds back through the same protocol the cross-machine and cross-impl scopes already use. The HTTP handler is 70 lines of portable Scheme that runs byte-identical in all three runtimes; the bend dispatcher is built on the same socket and portal primitives.
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.
The same abstraction, at five scopes. No new primitive at any level — each scope adds one implementation primitive (``call/cc`` / portal / reader / socket / bend dispatcher) and keeps the semantics. This is what "feedback is all you need" actually means once you extend it past the process boundary, past the implementation boundary, past the machine boundary, and now past the host-vs-accelerator boundary. §11.8 covers the wire protocol and the catalog of GPU forms surfaced through bend; this section just plants it as the fifth scope.
.. figure:: diagrams/five-scopes-feedback.png
:width: 95%
:align: center
*Five scopes of feedback as concentric crossings. Each row names what travels, the mechanism that lets it travel, and the cluster colour follows through the rest of the paper — blue for within-process (§3-§5), green for across-process portal (§7), amber for across-impl source-as-data (§11.1-§11.4), pink for across-machine sockets (§11.3-§11.5), purple for across-compute bend (§11.8).*
5. Optimizations
@ -570,37 +581,11 @@ On an arena-friendly workload (transient allocation, scoped lifetime) the arena
6.6.3 Collaborative Meta-GC: From Greedy to Adaptive
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The policy described in §6.6.1 is **greedy** — at every ``(with-arena)`` exit, unconditionally run the verifier, then decide reset-vs-sweep based on what it found. That works, but it pays the mark-phase cost even for arenas that are almost certainly going to escape. On a workload where most arenas escape, the verifier's work is wasted: the answer was going to be "escape" regardless.
The §6.6.1 policy is **greedy** — every ``(with-arena)`` exit runs the verifier first, then decides reset-vs-sweep. An **adaptive** dispatcher (``arena-set-mode 1``, the default) tracks recent escape rate as a scaled EMA — ``rate = (rate * 7 + sample * 256) / 8`` where ``sample = 0`` on reset, ``1`` on escape — and when ``rate > 128`` (50% escape) it **skips the verifier entirely**, letting the natural bump-overflow GC reclaim anything truly dead. Every 16 skipped arenas, a probe forces one verify so the policy can recover if the workload shifts back to arena-friendly.
The next layer replaces that with an **adaptive** policy driven by a scaled exponential moving average of recent escape rate::
Four pieces collaborate through one piece of shared state (the EMA + probe countdown): allocator reads ``arena_active`` to skip free-list reuse; ``gc_collect`` clears it on implicit trigger; verifier returns 0/1 for the EMA update; dispatcher reads rate + countdown to decide verify|skip|probe. No component queries another's internals.
rate = (rate * 7 + sample * 256) / 8 # sample = 0 (reset) | 1 (escape)
When ``rate > 128`` (50% escape rate) the dispatcher **skips the verifier entirely** and lets the arena's allocations survive in place. The heap keeps growing until a natural bump-overflow triggers ``gc_collect``, which reclaims anything truly dead with a proper mark pass. Every 16 skipped arenas, a probe forces one verify so the policy can re-evaluate and recover if the workload shifts back to arena-friendly.
Four co-operating pieces — allocator, mark phase, arena verifier, and the policy dispatcher — share exactly one piece of state (the EMA plus a probe countdown) and make local decisions:
.. code-block::
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
No component queries another's internals. This is "collaborative" in the structural sense — shared state, no direct coupling — while each decision remains local.
**Control toggles:**
.. code-block:: scheme
(arena-set-mode 0) ; greedy baseline (always verify)
(arena-set-mode 1) ; adaptive (default)
**Stats** now include skipped-verifier count and the current EMA, for observability::
(arena-stats) -> (calls resets escapes skipped bytes-reclaimed rate)
**Three-workload benchmark** (``make bench-gc-adaptive``, i5-8350U, ``N=1000`` iterations per phase, each phase in a fresh asm-gc process to isolate state):
**Three-workload benchmark** (``make bench-gc-adaptive``, i5-8350U, N=1000 iterations per phase, fresh asm-gc process per phase):
.. table::
:widths: 20 16 12 12 12 14 14
@ -616,17 +601,7 @@ No component queries another's internals. This is "collaborative" in the structu
mixed adaptive 858 14 1986 2 1970
========== ========== ========== ======== ========= ========== ===========
Reading the numbers:
- **Friendly** workload: adaptive and greedy are within ~1%. EMA stays at 0 (every arena resets), so the skip path never fires — a null result for the adaptive policy, which is exactly what we want on workloads that are already arena-scoped cleanly.
- **Hostile** workload: also within ~1%. Both modes trigger implicit ``gc_collect`` 982 times out of 1000 arenas — heap overflow during the thunk clears ``arena_active`` before the dispatcher sees it, so the adaptive skip path only activates 11 times. The policy's signal is drowned out by pressure-driven GC on this shape. Adaptive isn't helping, but it's not hurting either.
- **Mixed** workload: adaptive and greedy within ~1%. Earlier measurements (before the precise-type-byte fix) had shown a 17% adaptive win here; after the fix the numbers converged. The fix both accelerated the common paths (fewer redundant checks) and closed one correctness hole, so whatever advantage adaptive was extracting from the specific crash pattern it had tolerated is now available to greedy too. Honest result is that adaptive is neutral here, not a win.
**Honest read.** The adaptive policy is currently a null experiment on these three workloads — within measurement noise of greedy in all three cases. It may still win on workloads we haven't probed (long-running servers with occasional large bursts, mixed short/long transactions), but nothing in the three-way benchmark tells us to prefer it. Shipping it as default (``arena_adaptive_mode=1`` at ``_start``) costs nothing and keeps the counters (``arena-stats`` fifth field = ``skipped``, sixth field = EMA rate ×256) available for observability. The benchmark also drove the original precise-type-byte work (§6.6.5) that eliminated the latent class of conservative-scan bugs — so even the null result paid for itself in correctness progress.
**Reproduce:** ``make bench-gc-adaptive`` (source: ``tests/bench-gc-adaptive.sh``, ``examples/bench-gc-adaptive.lsp``). Each (workload × mode) pair runs in a fresh asm-gc process so results don't contaminate each other across phases.
**Honest read.** Adaptive is a null experiment on these three workloads — within measurement noise of greedy everywhere. It may still win on long-running mixed workloads we haven't probed, but nothing here demands it. Shipping at default costs nothing and the ``arena-stats`` counters (``skipped`` count, EMA rate ×256) give observability for future tuning. The benchmark drove the precise-type-byte work in §6.6.5 — so even the null result paid for itself in correctness progress.
6.6.4 Validation: HTTP Server Under Sustained Load
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@ -781,7 +756,7 @@ Constraints: same architecture, same binary layout, same process model. An asm b
7.4.1 The GC Build Uses S-Expressions
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The **GC** asm build can't use the binary heap dump because the heap is a linked list of chunks with typed block headers and a free list — raw-byte serialization would lose the structure. Rather than inventing portal v2 with chunk tables and pointer-relocation metadata, the GC build's ``portal-save`` walks the global env chain from ``%r14`` and emits one ``(define <sym> (quote <val>))`` form per binding. ``portal-resume`` is equivalent to ``(load "<filename>")`` — read every form and eval it.
The GC asm build can't use the binary heap dump — its heap is a linked list of chunks with typed block headers and a free list, so raw-byte serialization would lose the structure. Rather than inventing portal v2 with chunk tables and pointer-relocation metadata, the GC build's ``portal-save`` walks the global env chain from ``%r14`` and emits one ``(define <sym> (quote <val>))`` per binding; ``portal-resume`` is equivalent to ``(load "<filename>")``. **The language is its own wire format.**
::
@ -790,11 +765,7 @@ The **GC** asm build can't use the binary heap dump because the heap is a linked
(define greeting (quote "hello"))
(define x (quote 42))
Every non-builtin, non-closure binding round-trips. Closures and builtins are skipped — closures can't be faithfully re-read from their printed form, builtins get re-created from the target interpreter's prelude. This is the same treatment the JSON portal already gives to builtins (§7.3).
**Trade-off.** The GC build's portal is slower than the binary dump (walks each binding through the printer) and stricter about what it can preserve (data only, no closures or continuations). In exchange: **every portal produced by the GC build resumes on every other tier**, with no MAP_FIXED trick, no architecture constraint, no "same binary" requirement. A GC-asm producer can hand a portal to a Python consumer — we added the asm-gc column to the §7.2 matrix and all 16 cells are green.
**Version tag.** Every v1 portal starts with a single comment line — ``;; lumbda-portal v1`` — that Scheme readers already skip but the resume path actively parses. The matching policy: a file beginning with ``;;`` is required to match the v1 prefix exactly, or ``portal-resume`` returns ``#f`` instead of trying to evaluate forms that may use syntax the current reader doesn't understand. A file that doesn't begin with ``;;`` at all is accepted as legacy (pre-v1) for back-compat. The S-expression portal is a **migration format**, not an archive format — it exists to hand live data across a process boundary at handoff time, not to carry state across years of language evolution. When we need the latter, it earns its own format with proper schema evolution and a builtin-rename mapping table; the current portal stays simple and the version tag is the hook that lets v2 happen cleanly when someone actually needs it.
The trade is portability for capacity: every non-builtin, non-closure binding round-trips (closures can't be faithfully re-read; builtins get re-created from the target's prelude — same policy as §7.3 JSON), and in exchange **every GC-build portal resumes on every other tier** with no MAP_FIXED, no architecture constraint, no "same binary" requirement. The §7.2 matrix gains an asm-gc column and all 16 cells stay green. A v1 prefix line — ``;; lumbda-portal v1`` — gates the format so future schema changes can break cleanly; the S-expression portal is a **migration format** for live handoff, not an archive format.
7.5 Portal Preserves RNG State
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
@ -927,53 +898,39 @@ Reference: "All elementary functions from a single operator" (arXiv:2603.21852v2
With this operator & the constant ``1``, the following derivation chain constructs every elementary function:
8.2 Stage 1: Core Functions (Depth 1--3)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
8.2 Derivation Chain
^^^^^^^^^^^^^^^^^^^^^
Four stages climb from one operator to every elementary function. The full per-step proof lives in the cited arXiv paper; this is the chain in code form, as the Lumbda checker actually runs it:
::
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
; Stage 1 — core (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 eml 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)``.
; Stage 2 — arithmetic, from exp & ln
0 = ln(1)
a - b = eml(ln(a), exp(b)) ; subtraction
a * b = exp(ln(a) + ln(b)) ; multiplication
1/x = exp(-ln(x)) ; division
x^y = exp(y * ln(x)) ; exponentiation
sqrt(x)= exp(ln(x) / 2) ; roots
8.3 Stage 2: Arithmetic
^^^^^^^^^^^^^^^^^^^^^^^^^
; Stage 3 — complex plane via ln(-1)
ln(-1) = iπ ; complex logarithm of -1
π = imag(ln(-1)) ; π from imaginary part
i = exp(iπ/2) ; i from Euler
::
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
; Stage 4 — trigonometry via Euler
sin(x) = (exp(ix) - exp(-ix)) / 2i
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``.
Each line is one rewrite step the symbolic checker in ``proof/eml_proof_in_lumbda.lsp`` actually exercises. The key insight at Stage 3 is that ``ln`` of a negative number enters the complex plane: once we can construct ``-1`` from eml via the subtraction chain, ``ln(-1) = iπ`` follows, and ``π``, ``i``, and every trigonometric function fall out of Euler.
8.6 Verification & Friction Analysis
8.3 Verification & Friction Analysis
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
The proof has been verified at six distinct levels. Times are best-of-3 on the i5-8350U:
@ -1052,7 +1009,7 @@ Two comparisons matter. **Cold vs cold** is the honest end-to-end compare: Lumbd
**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.
**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.3 for the full six-row comparison), and carrying the additional guarantee that no implementation quirk of floating point can ever break the conclusion.
9. Language Coverage
@ -1414,6 +1371,74 @@ All four servers return the PDF byte-identical against the on-disk master. The s
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.
11.8 Bend: Cross-Tier GPU Dispatch
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
§11.3 showed lumbda serving HTTP from any tier. §11.4 showed s-expressions over sockets as RPC. §11.5 moved live bindings between machines through portal-over-HTTP. The last scope §4.3 planted — *across heterogeneous compute* — needs one more primitive: a way for Scheme code to dispatch hot inner loops to a CUDA-backed worker without pulling the toolchain into the lumbda build.
``examples/cuda-fanout/`` ships that primitive. ``(bend ...)`` is a special form that takes one ordinary lambda invocation and, at call time, decides whether to evaluate it locally or ship it to a worker over a wire protocol. The decision is cost-driven — a per-form estimator compares the wire round-trip against the expected local cost and picks the cheaper path. The same ``(bend ...)`` form runs unmodified across the Python, C, and asm tiers; the dispatcher reuses the same socket + portal primitives the other §11 sections built.
.. figure:: diagrams/bend-dispatch.png
:width: 96%
:align: center
*One ``(bend …)`` form across host, wire, worker, and GPU. The cost estimator picks local vs wire per call; small payloads ride the S-expression text frame, huge payloads ride the binary ``BSHK`` / ``BCGB`` / ``BSCP`` / ``BSRT`` / ``BSB3`` magic. The worker tier — Python, C, or asm — spawns a leaf CUDA binary via its native process-spawn primitive (``subprocess.Popen`` / ``fork`` + ``execve`` / raw ``pipe2`` + ``fork`` + ``execve``). Dashed arrows are the return path; results travel the same wire frame backwards.*
**Two wire modes, one form.** Bend's wire protocol carries either S-expressions (text) or a binary frame whose first four bytes are a magic that names the payload shape (``BSHK`` for shake fan-out, ``BCGB`` for CGBN ops, ``BSCP`` for secp256k1 scalar-mul, ``BSRT``/``BSRR`` for radix sort, ``BSB3``/``BSR3`` for BLAKE3-tree):
.. code-block:: scheme
;; small payloads — readable, every tier already has the parser
(bend! '(cuda-shake-fanout ("00" "01" "deadbeef") 32))
;; huge payloads — binary frame, parser cost drops out
(bend! '(cuda-radix-sort n u64-vec))
S-expression mode wins on small calls because no new code path runs — the existing portal reader handles the round-trip. Binary mode wins at scale: at 1 M × 16 B SHAKE-256 inputs the BSHK path is **150× faster than s-exp** (parser cost dominates above ~1 k inputs) and **12× faster than the host's own hashlib loop**. The crossover is the same shape we saw with the JSON portal vs the binary heap dump in §7.4: portability wins until the parser is the bottleneck, then the typed binary frame takes over.
**Workers run on any tier.** ``make gpu-worker LUMBDA={c,python,asm}`` boots a Scheme-resident gpu-worker that listens on port 8320 (BEND mnemonic) and spawns a leaf CUDA binary per call via ``spawn-process-stdio`` — a new cross-tier primitive (Python ``subprocess.Popen``, C ``fork`` + ``execve``, asm raw ``pipe2`` + ``fork`` + ``execve`` syscalls — no libc) that lands the same ``(spawn-process-stdio path argv)`` form in all three tiers. The C-tier worker host is **~9× faster than Python** on small calls (dispatcher overhead drops with the interpreter); at huge calls the binary wire mode equalizes everything because the worker is now spending all its time in the CUDA kernel. The asm-tier worker host is ~70 KB statically linked.
**Worker health.** Every worker exposes a ``(health)`` op that returns ``(vram-free-bytes pid uptime-ms)``. The dispatcher caches the response for 5 s and ranks workers by free VRAM — a 3090 with 24 GB free always picks over a 4090 already running qwen. ``cluster.lsp`` reuses the same protocol across a 3-node fleet (3× RTX 3090, see ``lumbda.com/bend.html``).
**Catalog of live forms.** Each form ships a self-contained CUDA binary plus a one-line lumbda wrapper. Headline numbers on RTX 3090:
.. list-table::
:widths: 26 38 22 14
:header-rows: 1
* - Form
- Throughput
- vs baseline
- Wire
* - ``cuda-shake-fanout``
- 1 M × 16 B in ~12 ms
- 12× hashlib
- BSHK
* - ``cuda-secp256k1-mul`` v3
- 13.83 Mkeys/s @ n=1M
- 1.76× v1 (~309× coincurve)
- BSCP
* - ``cuda-bignum-cgbn``
- 1.28 Gops/s mod-mul (256-bit)
- ~256× GMP CPU
- BCGB
* - ``cuda-radix-sort``
- 5.50 Gkeys/s @ n=10M (CUB ``DeviceRadixSort`` u64)
- ~4× Titan baseline
- BSRT
* - ``cuda-blake3-tree``
- 32.5 GB/s @ 1M × 64 B (kernel 1.97 ms)
- single-GPU reference
- BSB3
* - ``cuda-sim-ops-bin``
- 1.27× host @ 141 batches (9024 shots); SHAKE-RNG mode bit-identical to upstream ``eval_circuit``
- matches upstream Pareto
- ``ops.bin``
Every form's output is byte-identical against a host reference: ``hashlib.shake_256`` for SHAKE, ``coincurve`` for secp256k1, ``hashlib.blake3`` for BLAKE3, Python ``sorted()`` for radix, and the upstream ``eval_circuit`` walker on the same ``ops.bin`` for circuit simulation. The catalog is open at ``examples/cuda-fanout/CATALOG.md`` — currently 27 surveyed forms across cryptography, sort/search, graph, sparse linear algebra, and signal processing. Companion page: ``lumbda.com/bend.html`` carries the live fleet status and the published speedup table.
**Why this matters past the speedups.** A 22 KB asm interpreter that drives a 24 GB GPU through a 4-byte magic + raw bytes is the same pattern the other §11 sections demonstrate: the language sits on top of the kernel boundary, not under it. No CUDA toolchain links into lumbda. No libcudart in asm's address space. Every cross-compute call is one ``(bend ...)`` form, one spawn, one wire frame. The wire format and the language are the same artifact, again — and now the artifact crosses the host/accelerator boundary too.
12. MOAD Audit: Fixing What We Built
--------------------------------------
@ -1460,6 +1485,8 @@ The Python implementation had a similar defect: ``_define_record_type`` used ``l
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.
**Post-cycle audit (since 2026-04-24).** Bend's wire protocol surfaced another sedimentary defect: ``wire.lsp``'s ``recv-exact`` accumulated bytes by repeatedly appending to a growing string, O(n²) over the whole receive. The 1 M-input binary benchmark exposed it — Python tier Scheme-level scaling went non-linear above ~100 k bytes. Fix: collect into a list and ``string-concat`` once at end, O(n). The same benchmark also forced honest huge-workload numbers across all three tiers: C-tier worker host ~9× faster than Python, binary mode 12× faster than host hashlib at 1 M inputs. Two correctness fixes landed alongside: asm ``scheme_read`` had a 256-byte input buffer that overflowed on long strings (#GP fault past 272 chars; fix raised the buffer and added a bounds check), and asm ``gc_sweep`` had a page-fault on chunk-abandonment when the bump pointer landed exactly at a chunk-end boundary (fix walks the chunk chain explicitly). A JIT correctness fix on the C tier — the bytecode VM had been clobbering ``cur_code`` across ``CALL``/``RETURN`` in named-let bodies, hanging the EML proof checker on the rewriter loop — restored the cross-tier proof timings in §8.3.
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
@ -1491,7 +1518,7 @@ This is the permacomputer obligation: infrastructure that renews itself. Code th
- **WebSocket / bidirectional**: HTTP/1.0 is request-response; a persistent socket loop with framing brings full-duplex feedback.
- **Continuation-passing over HTTP**: §11.5 moves *bindings* over HTTP. The next step is moving a live *continuation* — serialize it via ``call/cc`` + JSON portal, transmit, resume on the remote VM. Makes any TCP endpoint a trampoline target.
- **DAG-of-hot-paths predictive preload**: §11.7's adaptive server ranks by raw frequency, which pins the top URLs but cannot predict *which* assets co-occur. A navigation DAG (edge weights = ``P(next = v | prev = u)``) learned from referrer headers or session logs would let the boot-time preloader walk forward from seed nodes and warm everything within a predicted session depth. For deployments with > 1000 resources where the flat top-N is too narrow and full hot-caching is too wide, the DAG is the middle path. The frequency-only version in the repo today is designed to be the single-node degenerate case — a DAG with no edges.
- **GPU lambda execution**: Map/reduce on CUDA for data-parallel Scheme (Phase 1), trampolining for recursive lambdas (Phase 2), interaction combinators for massive parallelism (Phase 3)
- **GPU lambda execution — Phase 1 shipped**: Map/reduce on CUDA via ``(bend ...)`` is now in production (§4.3 fifth scope, §11.8 catalog of 27 forms — cuda-secp256k1, cuda-blake3-tree, cuda-radix-sort, cuda-bignum-cgbn, etc.). Phase 2 is trampolining for recursive lambdas — turning a ``(bend (lambda (n) ...))`` into successive worker round-trips driven by ``call/cc``, so a Scheme recursion can run entirely on the GPU side of the wire. Phase 3 is interaction combinators for massive parallelism — the same lambda calculus reductions implemented as GPU-resident graph rewrites, removing the host-side dispatcher from the inner loop.
- **Copying GC in asm**: ``heap-snapshot`` is an escape hatch. A mark-and-copy collector would remove the sharp edge for general programs without forcing the programmer to reason about lifetimes.
- **Concurrent accept loop (asm)**: Currently single-threaded. A pre-forked worker model or ``SO_REUSEPORT`` pool would multiply throughput without changing the Scheme code.
- **Complex number arithmetic**: Extending the numeric tower for the full EML derivation chain
@ -1552,6 +1579,7 @@ Citation
russell@unturf, TimeHexOn, foxhop, Zoë Trout. "Feedback Is All You Need."
permacomputer.com, 2026.
https://lumbda.com/lumbda-whitepaper.pdf
Source: https://git.unturf.com/engineering/unturf/lumbda
References