From 3463fadd3f3ed9cee6a2b6cc8cafdb1f978933a7 Mon Sep 17 00:00:00 2001 From: "russell@unturf.com" Date: Fri, 17 Apr 2026 20:56:00 -0400 Subject: [PATCH] C --fast named-let bug: minimal repro + workaround, all 4 tiers pass now MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Hunted the C --fast compiler bug that was hanging on the EML proof. Narrowed to a specific pattern: (let loop ((t start)) (let ((next (fn t))) (if next (loop next) t))) A named-let whose body is (let ((x (...))) (if x (recurse x) base)). The recursive call inside the inner let+if branch never reaches the loop closure — hangs or segfaults. Reproducible with a 4-line test case; filed as c/TODO-named-let-bytecode.md with minimal repro, suspected cause (env-chain mismatch between PUSH_ENV and TAIL_CALL), and a known- good workaround. Workaround landed in proof/eml_proof_in_lumbda.lsp's `normalize`: replaced the named-let with an internal recursive `define`, which compiles correctly under --fast. Same logic, different surface syntax. All four Lumbda tiers now verify the proof. Benchmark refreshed (make bench-proof): cold cached Lumbda asm 46 ms 7 ms Lumbda C --fast 65 ms 9 ms Lumbda C (tree-walker) 87 ms 12 ms Lumbda Python --fast 651 ms 232 ms Lean 4 722 ms 5 ms All four tiers now green. Asm still fastest (46 ms cold vs Lean's 722 ms — ~16× faster). Cached Lumbda asm 7 ms vs Lean 5 ms (within 1.5×). The C --fast tier went from "hangs" to 65 ms cold — competitive with asm once the compiler bug is dodged. Whitepaper §8.6 table updated; prior "(hangs)" row is gone; footnote on the named-let workaround links the TODO file. --- c/TODO-named-let-bytecode.md | 60 ++++++++ proof/eml_proof_in_lumbda.lsp | 12 +- whitepaper/uncommonlisp-whitepaper.pdf | 201 ++++++++++++------------- whitepaper/uncommonlisp-whitepaper.rst | 14 +- 4 files changed, 174 insertions(+), 113 deletions(-) create mode 100644 c/TODO-named-let-bytecode.md diff --git a/c/TODO-named-let-bytecode.md b/c/TODO-named-let-bytecode.md new file mode 100644 index 0000000..5ee5f70 --- /dev/null +++ b/c/TODO-named-let-bytecode.md @@ -0,0 +1,60 @@ +# C --fast bytecode compiler: named-let + inner `let`+`if` bug + +## Reproduction (minimal) + +```scheme +(define (maybe x) (if (> x 3) #f (+ x 1))) +(define (g start) + (let loop ((t start)) + (let ((next (maybe t))) + (if next (loop next) t)))) +(display (g 0)) (newline) +``` + +Expected output: `4` + +Actual with `c/uncommonlisp --fast`: hangs or segfaults. +Tree-walker (`c/uncommonlisp` default) works correctly. +Python `--fast` and asm tree-walker both work correctly. + +## What's special + +The bug fires when: +- Outer named-let: `(let loop ((t ...)) BODY)` +- Inside BODY: `(let ((next (fn t))) ...)` — another let +- Inside inner let: `(if next (loop next) t)` — recursive call + through an if branch that was reached via an inner let-body + +The recursive tail call to `loop` through the nested let + if doesn't +reach the loop closure. Bytecode emission likely walks the wrong env +chain or targets the wrong stack slot. + +## Workaround + +Replace named-let with an internal recursive `define`: + +```scheme +(define (g start) + (define (iter t) + (let ((next (maybe t))) + (if next (iter next) t))) + (iter start)) +``` + +Compiles correctly under `--fast`. Applied to `proof/eml_proof_in_lumbda.lsp` +for the `normalize` function. + +## Where to look + +`c/vm.c:344` `SYM_LET` named-let branch emits: + `PUSH_ENV, MAKE_CLOSURE, DUP, BIND name, , CALL/TAIL_CALL`. + +Suspected: the lambda body's closure-env capture plus the inner `let` +PUSH_ENV interact badly when the tail call is behind an `if` whose +compilation path doesn't POP_ENV back to the closure's expected level. + +## Priority + +Low for now — workaround lands in every affected .lsp and the other +three tiers are unaffected. File for cleanup when the C --fast +refactor happens. diff --git a/proof/eml_proof_in_lumbda.lsp b/proof/eml_proof_in_lumbda.lsp index 2bc6064..643d4bf 100644 --- a/proof/eml_proof_in_lumbda.lsp +++ b/proof/eml_proof_in_lumbda.lsp @@ -134,13 +134,21 @@ (step-root rules term))) ;;; --- Normalize: repeat until fixed point or step limit --- +;;; +;;; Uses an internal recursive `iter` rather than a named-let because +;;; the C `--fast` bytecode compiler mis-compiles the specific pattern +;;; (let loop ((t ...)) (let ((next (fn t))) (if next (loop next) t))) +;;; — the recursive call inside an inner (let + if) branch doesn't +;;; reach `loop`. Tracked separately; asm and Python --fast are +;;; unaffected. An internal `define (iter ...)` compiles correctly. (define (normalize rules term) - (let loop ((t term) (n 0)) + (define (iter t n) (if (> n 500) t ; step limit safety (let ((next (step-any rules t))) - (if next (loop next (+ n 1)) t))))) + (if next (iter next (+ n 1)) t)))) + (iter term 0)) ;;; ═══════════════════════════════════════════════════════════════ ;;; EML axioms and derivation rules diff --git a/whitepaper/uncommonlisp-whitepaper.pdf b/whitepaper/uncommonlisp-whitepaper.pdf index b44d6a3..d33f5c5 100644 --- a/whitepaper/uncommonlisp-whitepaper.pdf +++ b/whitepaper/uncommonlisp-whitepaper.pdf @@ -270,7 +270,7 @@ endobj << /A << /S /URI /Type /Action /URI (mailto:russell@unturf.com) ->> /Border [ 0 0 0 ] /Rect [ 248.0736 753.0236 334.3536 765.0236 ] /Subtype /Link /Type /Annot +>> /Border [ 0 0 0 ] /Rect [ 248.0736 725.8236 334.3536 737.8236 ] /Subtype /Link /Type /Annot >> endobj 34 0 obj @@ -496,7 +496,7 @@ endobj endobj 59 0 obj << -/Author () /CreationDate (D:20260417204712-04'00') /Creator (\(unspecified\)) /Keywords () /ModDate (D:20260417204712-04'00') /Producer (ReportLab PDF Library - \(opensource\)) +/Author () /CreationDate (D:20260417205437-04'00') /Creator (\(unspecified\)) /Keywords () /ModDate (D:20260417205437-04'00') /Producer (ReportLab PDF Library - \(opensource\)) /Subject (\(unspecified\)) /Title () /Trapped /False >> endobj @@ -688,17 +688,17 @@ endobj endobj 96 0 obj << -/Dest [ 32 0 R /XYZ 57.02362 591.0236 0 ] /Next 97 0 R /Parent 61 0 R /Prev 89 0 R /Title (9. Language Coverage) +/Dest [ 32 0 R /XYZ 57.02362 567.0236 0 ] /Next 97 0 R /Parent 61 0 R /Prev 89 0 R /Title (9. Language Coverage) >> endobj 97 0 obj << -/Dest [ 32 0 R /XYZ 57.02362 341.8236 0 ] /Next 98 0 R /Parent 61 0 R /Prev 96 0 R /Title (10. Relationship to Companion Papers) +/Dest [ 32 0 R /XYZ 57.02362 317.8236 0 ] /Next 98 0 R /Parent 61 0 R /Prev 96 0 R /Title (10. Relationship to Companion Papers) >> endobj 98 0 obj << -/Count 6 /Dest [ 32 0 R /XYZ 57.02362 92.62362 0 ] /First 99 0 R /Last 104 0 R /Next 105 0 R /Parent 61 0 R +/Count 6 /Dest [ 36 0 R /XYZ 57.02362 765.0236 0 ] /First 99 0 R /Last 104 0 R /Next 105 0 R /Parent 61 0 R /Prev 97 0 R /Title (11. Four Implementation Tiers, One Language) >> endobj @@ -5631,7 +5631,7 @@ endstream endobj 128 0 obj << -/Length 10017 +/Length 9908 >> stream 1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET @@ -5874,14 +5874,14 @@ q 1 0 0 1 176.435 75 cm q 0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (44 ms) Tj T* ET +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (46 ms) Tj T* ET Q Q q 1 0 0 1 256.6398 75 cm q 0 0 0 rg -BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL (4 ms) Tj T* ET +BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL (7 ms) Tj T* ET Q Q q @@ -5894,69 +5894,62 @@ Q q 1 0 0 1 6 57 cm q -0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (Lumbda C \(tree-walker\)) Tj T* ET +BT 1 0 0 1 0 2 Tm 12 TL /F1 10 Tf 0 0 0 rg (Lumbda C ) Tj /F5 10 Tf (--fast) Tj T* ET Q Q q 1 0 0 1 176.435 57 cm q 0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (64 ms) Tj T* ET +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (65 ms) Tj T* ET Q Q q 1 0 0 1 256.6398 57 cm q 0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (5 ms) Tj T* ET +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (9 ms) Tj T* ET Q Q q 1 0 0 1 6 39 cm q -BT 1 0 0 1 0 2 Tm 12 TL /F1 10 Tf 0 0 0 rg (Lumbda Python ) Tj /F5 10 Tf (--fast) Tj T* ET +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (Lumbda C \(tree-walker\)) Tj T* ET Q Q q 1 0 0 1 176.435 39 cm q 0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (619 ms) Tj T* ET +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (87 ms) Tj T* ET Q Q q 1 0 0 1 256.6398 39 cm q 0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (185 ms) Tj T* ET +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (12 ms) Tj T* ET Q Q q 1 0 0 1 6 21 cm q -BT 1 0 0 1 0 2 Tm 12 TL /F1 10 Tf 0 0 0 rg (Lumbda C ) Tj /F5 10 Tf (--fast) Tj T* ET +BT 1 0 0 1 0 2 Tm 12 TL /F1 10 Tf 0 0 0 rg (Lumbda Python ) Tj /F5 10 Tf (--fast) Tj T* ET Q Q q 1 0 0 1 176.435 21 cm q 0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (\(hangs\)) Tj T* ET +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (651 ms) Tj T* ET Q Q q 1 0 0 1 256.6398 21 cm q 0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (\(hangs\)) Tj T* ET -Q -Q -q -1 0 0 1 336.8445 21 cm -q -0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (known compiler bug) Tj T* ET +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (232 ms) Tj T* ET Q Q q @@ -5970,14 +5963,14 @@ q 1 0 0 1 176.435 3 cm q 0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (726 ms) Tj T* ET +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (722 ms) Tj T* ET Q Q q 1 0 0 1 256.6398 3 cm q 0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (2 ms) Tj T* ET +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (5 ms) Tj T* ET Q Q q @@ -6013,7 +6006,7 @@ Q q 1 0 0 1 57.02362 67.02362 cm q -BT 1 0 0 1 0 26 Tm .204897 Tw 12 TL /F1 10 Tf 0 0 0 rg (Two comparisons matter. ) Tj /F3 10 Tf (Cold vs cold) Tj /F1 10 Tf ( is the honest end-to-end compare: Lumbda asm \(44 ms\) verifies the) Tj T* 0 Tw .216373 Tw (proof ) Tj /F3 10 Tf (16\327 faster than Lean's cold rebuild) Tj /F1 10 Tf ( \(726 ms\) on the same hardware, because Lumbda doesn't link a) Tj T* 0 Tw .315636 Tw (compiled binary or spin up a kernel \227 it just runs a rewriter over five small terms. ) Tj /F3 10 Tf (Cached vs cached) Tj /F1 10 Tf ( is the) Tj T* 0 Tw ET +BT 1 0 0 1 0 26 Tm .204897 Tw 12 TL /F1 10 Tf 0 0 0 rg (Two comparisons matter. ) Tj /F3 10 Tf (Cold vs cold) Tj /F1 10 Tf ( is the honest end-to-end compare: Lumbda asm \(46 ms\) verifies the) Tj T* 0 Tw -0.127156 Tw (proof ) Tj /F3 10 Tf (~16\327 faster than Lean's cold rebuild) Tj /F1 10 Tf ( \(722 ms\) on the same hardware, because Lumbda doesn't link a) Tj T* 0 Tw .315636 Tw (compiled binary or spin up a kernel \227 it just runs a rewriter over five small terms. ) Tj /F3 10 Tf (Cached vs cached) Tj /F1 10 Tf ( is the) Tj T* 0 Tw ET Q Q @@ -6021,89 +6014,89 @@ endstream endobj 129 0 obj << -/Length 9096 +/Length 9243 >> stream 1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET q 1 0 0 1 57.02362 741.0236 cm q -BT 1 0 0 1 0 14 Tm 1.589913 Tw 12 TL /F1 10 Tf 0 0 0 rg (throwaway benchmark but still interesting: Lumbda asm at 4 ms vs Lean at 2 ms, within 2\327, on what is) Tj T* 0 Tw (essentially "read a file and print five lines.") Tj T* ET +BT 1 0 0 1 0 14 Tm 1.150966 Tw 12 TL /F1 10 Tf 0 0 0 rg (throwaway benchmark but still interesting: Lumbda asm at 7 ms vs Lean at 5 ms, within 1.5\327, on what is) Tj T* 0 Tw (essentially "read a file and print five lines.") Tj T* ET Q Q q -1 0 0 1 57.02362 699.0236 cm +1 0 0 1 57.02362 675.0236 cm q -BT 1 0 0 1 0 26 Tm 2.017397 Tw 12 TL /F1 10 Tf 0 0 0 rg (Three of the four Lumbda tiers verify the proof; C ) Tj /F5 10 Tf (--fast) Tj /F1 10 Tf ( is the known cumulative-state compiler bug) Tj T* 0 Tw 3.755696 Tw (tracked separately and does not affect the other three. ) Tj /F3 10 Tf (Reproduce:) Tj /F1 10 Tf ( ) Tj /F5 10 Tf (make) Tj ( ) Tj (bench-proof) Tj /F1 10 Tf ( \(source:) Tj T* 0 Tw /F5 10 Tf (tests/bench-proof.sh) Tj /F1 10 Tf (\).) Tj T* ET +BT 1 0 0 1 0 50 Tm .526772 Tw 12 TL /F3 10 Tf 0 0 0 rg (All four Lumbda tiers verify the proof.) Tj /F1 10 Tf ( A C ) Tj /F5 10 Tf (--fast) Tj /F1 10 Tf ( bytecode-compiler bug originally caused the final tier) Tj T* 0 Tw 10.06986 Tw (to hang on the rewriter's named-let loop; narrowed to a minimal reproduction \(see) Tj T* 0 Tw 1.693196 Tw /F5 10 Tf (c/TODO-named-let-bytecode.md) Tj /F1 10 Tf (\) and worked around in the proof file by using an internal recursive) Tj T* 0 Tw .558138 Tw /F5 10 Tf (define) Tj /F1 10 Tf ( in place of the offending named-let. All four tiers now complete in under 100 ms cold. ) Tj /F3 10 Tf (Reproduce:) Tj /F1 10 Tf T* 0 Tw /F5 10 Tf (make) Tj ( ) Tj (bench-proof) Tj /F1 10 Tf ( \(source: ) Tj /F5 10 Tf (tests/bench-proof.sh) Tj /F1 10 Tf (\).) Tj T* ET Q Q q -1 0 0 1 57.02362 609.0236 cm +1 0 0 1 57.02362 585.0236 cm q BT 1 0 0 1 0 74 Tm 2.513543 Tw 12 TL /F3 10 Tf 0 0 0 rg (First machine-checked treatment.) Tj /F1 10 Tf ( The original paper \(Odrzywo) Tj /F7 10 Tf 12 TL (n) Tj /F1 10 Tf 12 TL (ek, arXiv:2603.21852v2, 2026-04-04\)) Tj T* 0 Tw .313453 Tw (presents the EML universality claim analytically \227 pure LaTeX mathematics, no formal tool. The companion) Tj T* 0 Tw .549873 Tw (Zenodo artifact is symbolic-regression / gradient-optimization code, not a verification. To our knowledge the) Tj T* 0 Tw 1.856373 Tw (Lean 4 proof shipped in this repo is the first machine-checked treatment of the EML identities, and the) Tj T* 0 Tw .247122 Tw (accompanying Lumbda-native checker is the first self-hosted machine-checked version. Five theorems, zero) Tj T* 0 Tw .234556 Tw /F5 10 Tf (sorry) Tj /F1 10 Tf (, no Mathlib dependency \227 40\327 faster than the brute-force numerical search it replaced, and carrying) Tj T* 0 Tw (the additional guarantee that no implementation quirk of floating point can ever break the conclusion.) Tj T* ET Q Q q -1 0 0 1 57.02362 577.8236 cm +1 0 0 1 57.02362 553.8236 cm q BT 1 0 0 1 0 2.2 Tm 13.2 TL /F2 11 Tf .133333 .133333 .133333 rg (9. Language Coverage) Tj T* ET Q Q q -1 0 0 1 57.02362 557.8236 cm +1 0 0 1 57.02362 533.8236 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (Lumbda implements a near-complete R7RS-small Scheme:) Tj T* ET Q Q q -1 0 0 1 57.02362 503.8236 cm +1 0 0 1 57.02362 479.8236 cm q BT 1 0 0 1 0 38 Tm 1.369223 Tw 12 TL /F3 10 Tf 0 0 0 rg (Special forms) Tj /F1 10 Tf ( \(32\): ) Tj /F5 10 Tf (define) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (set!) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (lambda) Tj /F1 10 Tf (, ) Tj /F5 10 Tf /F6 10 Tf 12 TL (l) Tj /F5 10 Tf 12 TL /F1 10 Tf (, ) Tj /F5 10 Tf (if) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (cond) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (case) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (and) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (or) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (when) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (unless) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (begin) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (let) Tj /F1 10 Tf (,) Tj T* 0 Tw 10.15262 Tw /F5 10 Tf (let*) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (letrec) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (letrec*) Tj /F1 10 Tf (, named-let, ) Tj /F5 10 Tf (do) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (quasiquote) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (define-macro) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (define-syntax) Tj /F1 10 Tf (,) Tj T* 0 Tw 3.646907 Tw /F5 10 Tf (syntax-rules) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (let-syntax) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (letrec-syntax) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (apply) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (eval) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (values) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (call/cc) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (dynamic-wind) Tj /F1 10 Tf (,) Tj T* 0 Tw /F5 10 Tf (guard) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (parameterize) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (load) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (error) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (module) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (import) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (define-record-type) Tj /F1 10 Tf (.) Tj T* ET Q Q q -1 0 0 1 57.02362 473.8236 cm +1 0 0 1 57.02362 449.8236 cm q BT 1 0 0 1 0 14 Tm .150642 Tw 12 TL /F3 10 Tf 0 0 0 rg (Built-in functions) Tj /F1 10 Tf ( \(100+\): Full arithmetic \(exact rationals, inexact reals, trigonometry\), pairs & lists \(SRFI-1\),) Tj T* 0 Tw (strings \(mutable\), characters, vectors, hash tables, I/O \(ports, file system\), system interface, Python interop.) Tj T* ET Q Q q -1 0 0 1 57.02362 443.8236 cm +1 0 0 1 57.02362 419.8236 cm q BT 1 0 0 1 0 14 Tm 2.274835 Tw 12 TL /F3 10 Tf 0 0 0 rg (Hygienic macros) Tj /F1 10 Tf (: ) Tj /F5 10 Tf (syntax-rules) Tj /F1 10 Tf ( with ellipsis \() Tj /F5 10 Tf (...) Tj /F1 10 Tf (\) support. Pattern matching, template instantiation,) Tj T* 0 Tw (proper hygiene. Also ) Tj /F5 10 Tf (define-macro) Tj /F1 10 Tf ( for procedural macros.) Tj T* ET Q Q q -1 0 0 1 57.02362 413.8236 cm +1 0 0 1 57.02362 389.8236 cm q BT 1 0 0 1 0 14 Tm 1.958835 Tw 12 TL /F3 10 Tf 0 0 0 rg (Standard library) Tj /F1 10 Tf ( \() Tj /F5 10 Tf (stdlib.lsp) Tj /F1 10 Tf (, 385 lines\): Additional macros \() Tj /F5 10 Tf (swap!) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (fluid-let) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (while) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (dotimes) Tj /F1 10 Tf (\),) Tj T* 0 Tw (utility functions, simple object system, SRFI-2/8/64 test framework.) Tj T* ET Q Q q -1 0 0 1 57.02362 359.8236 cm +1 0 0 1 57.02362 335.8236 cm q BT 1 0 0 1 0 38 Tm 1.569862 Tw 12 TL /F3 10 Tf 0 0 0 rg (Test suite) Tj /F1 10 Tf (: 974 verified assertions covering lexing, parsing, special forms, bytecode compilation, macros) Tj T* 0 Tw .214835 Tw (\(hygienic & procedural\), continuations, generators, record types, modules, arithmetic, higher-order functions,) Tj T* 0 Tw 4.238031 Tw (error handling, portal serialization, cross-implementation portal exchange, file I/O parity, & graceful) Tj T* 0 Tw (degradation on mismatched or corrupt input.) Tj T* ET Q Q q -1 0 0 1 57.02362 328.6236 cm +1 0 0 1 57.02362 304.6236 cm q BT 1 0 0 1 0 2.2 Tm 13.2 TL /F2 11 Tf .133333 .133333 .133333 rg (10. Relationship to Companion Papers) Tj T* ET Q Q q -1 0 0 1 57.02362 308.6236 cm +1 0 0 1 57.02362 284.6236 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (Lumbda forms one piece of a larger permacomputer machine learning stack:) Tj T* ET Q Q q -1 0 0 1 57.02362 302.6236 cm +1 0 0 1 57.02362 278.6236 cm Q q -1 0 0 1 57.02362 164.6236 cm +1 0 0 1 57.02362 140.6236 cm q 1 1 1 rg n 0 138 481.2283 -18 re f* @@ -6240,34 +6233,34 @@ Q Q Q q -1 0 0 1 57.02362 164.6236 cm +1 0 0 1 57.02362 140.6236 cm Q q -1 0 0 1 57.02362 110.6236 cm +1 0 0 1 57.02362 86.62362 cm q BT 1 0 0 1 0 38 Tm 1.738453 Tw 12 TL /F1 10 Tf 0 0 0 rg (Lumbda provides the runtime layer: a language that can checkpoint its own execution, migrate between) Tj T* 0 Tw 3.051529 Tw (machines, & resume from serialized state. The portal system enables distributed computation across) Tj T* 0 Tw 1.058196 Tw (permacomputer nodes. Categorization & feedback activities could run inside Lumbda's VM, with ) Tj /F5 10 Tf (call/cc) Tj /F1 10 Tf T* 0 Tw (providing the state machine transitions & portal providing persistence.) Tj T* ET Q Q -q -1 0 0 1 57.02362 79.42362 cm -q -BT 1 0 0 1 0 2.2 Tm 13.2 TL /F2 11 Tf .133333 .133333 .133333 rg (11. Four Implementation Tiers, One Language) Tj T* ET -Q -Q -q -1 0 0 1 57.02362 65.42362 cm -Q endstream endobj 130 0 obj << -/Length 2113 +/Length 2303 >> stream 1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET q -1 0 0 1 57.02362 753.0236 cm +1 0 0 1 57.02362 751.8236 cm +q +BT 1 0 0 1 0 2.2 Tm 13.2 TL /F2 11 Tf .133333 .133333 .133333 rg (11. Four Implementation Tiers, One Language) Tj T* ET +Q +Q +q +1 0 0 1 57.02362 737.8236 cm +Q +q +1 0 0 1 57.02362 725.8236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -6283,19 +6276,19 @@ Q Q Q q -1 0 0 1 57.02362 753.0236 cm +1 0 0 1 57.02362 725.8236 cm Q q -1 0 0 1 57.02362 675.0236 cm +1 0 0 1 57.02362 647.8236 cm q BT 1 0 0 1 0 62 Tm .778726 Tw 12 TL /F1 10 Tf 0 0 0 rg (Lumbda ships as four independently built tiers: a Python bytecode VM, a C tree-walker, a C bytecode VM,) Tj T* 0 Tw 2.18402 Tw (and a C x86_64 JIT \(the last three packaged in one binary, selectable by flag\), plus a pure-assembly) Tj T* 0 Tw .931492 Tw (interpreter. Each tier is MOAD-isolated from the others \227 a defect surfaced in one is fixed in that tier, not) Tj T* 0 Tw 2.098556 Tw (patched across shared infrastructure. All four run the same ) Tj /F5 10 Tf (.lsp) Tj /F1 10 Tf ( source files and exchange the same) Tj T* 0 Tw 2.266213 Tw (S-expression portal format; \24711.3-\24711.5 demonstrate this end-to-end across sockets, relays, and HTTP) Tj T* 0 Tw (portal transfers.) Tj T* ET Q Q q -1 0 0 1 57.02362 667.0236 cm +1 0 0 1 57.02362 639.8236 cm Q q -1 0 0 1 57.02362 165.1875 cm +1 0 0 1 57.02362 137.9875 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -6318,10 +6311,10 @@ Q Q Q q -1 0 0 1 57.02362 157.1875 cm +1 0 0 1 57.02362 129.9875 cm Q q -1 0 0 1 57.02362 149.1875 cm +1 0 0 1 57.02362 121.9875 cm Q endstream @@ -9547,49 +9540,49 @@ xref 0002247717 00000 n 0002257330 00000 n 0002265750 00000 n -0002275821 00000 n -0002284970 00000 n -0002287136 00000 n -0002298601 00000 n -0002314667 00000 n -0002323713 00000 n -0002332601 00000 n -0002339769 00000 n -0002347074 00000 n -0002355749 00000 n -0002363222 00000 n -0002365422 00000 n -0002367113 00000 n -0002367437 00000 n -0002367472 00000 n -0002367507 00000 n -0002367542 00000 n -0002367577 00000 n -0002367612 00000 n -0002367647 00000 n -0002367682 00000 n -0002367717 00000 n -0002367752 00000 n -0002367788 00000 n -0002367824 00000 n -0002367860 00000 n -0002367896 00000 n -0002367932 00000 n -0002367968 00000 n -0002368004 00000 n -0002368040 00000 n -0002368076 00000 n -0002368112 00000 n -0002368148 00000 n -0002368184 00000 n -0002368220 00000 n -0002368256 00000 n -0002368292 00000 n -0002368328 00000 n +0002275711 00000 n +0002285007 00000 n +0002287363 00000 n +0002298828 00000 n +0002314894 00000 n +0002323940 00000 n +0002332828 00000 n +0002339996 00000 n +0002347301 00000 n +0002355976 00000 n +0002363449 00000 n +0002365649 00000 n +0002367340 00000 n +0002367664 00000 n +0002367699 00000 n +0002367734 00000 n +0002367769 00000 n +0002367804 00000 n +0002367839 00000 n +0002367874 00000 n +0002367909 00000 n +0002367944 00000 n +0002367979 00000 n +0002368015 00000 n +0002368051 00000 n +0002368087 00000 n +0002368123 00000 n +0002368159 00000 n +0002368195 00000 n +0002368231 00000 n +0002368267 00000 n +0002368303 00000 n +0002368339 00000 n +0002368375 00000 n +0002368411 00000 n +0002368447 00000 n +0002368483 00000 n +0002368519 00000 n +0002368555 00000 n trailer << /ID -[] +[<1d1d492e26ccbe99cb4cca73ae9eecee><1d1d492e26ccbe99cb4cca73ae9eecee>] % ReportLab generated PDF document -- digest (opensource) /Info 59 0 R @@ -9597,5 +9590,5 @@ trailer /Size 168 >> startxref -2368364 +2368591 %%EOF diff --git a/whitepaper/uncommonlisp-whitepaper.rst b/whitepaper/uncommonlisp-whitepaper.rst index f6a4b85..e581140 100644 --- a/whitepaper/uncommonlisp-whitepaper.rst +++ b/whitepaper/uncommonlisp-whitepaper.rst @@ -727,16 +727,16 @@ The Lean proof operates over abstract ``exp`` & ``ln`` functions with the axioms ============================== =========== ============ ===================== Approach cold cached notes ============================== =========== ============ ===================== - Lumbda asm 44 ms **4 ms** fastest Lumbda tier - Lumbda C (tree-walker) 64 ms 5 ms - Lumbda Python ``--fast`` 619 ms 185 ms - Lumbda C ``--fast`` (hangs) (hangs) known compiler bug - Lean 4 726 ms 2 ms reference + Lumbda asm 46 ms **7 ms** fastest Lumbda tier + Lumbda C ``--fast`` 65 ms 9 ms + Lumbda C (tree-walker) 87 ms 12 ms + Lumbda Python ``--fast`` 651 ms 232 ms + Lean 4 722 ms 5 ms reference ============================== =========== ============ ===================== -Two comparisons matter. **Cold vs cold** is the honest end-to-end compare: Lumbda asm (44 ms) verifies the proof **16× faster than Lean's cold rebuild** (726 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 4 ms vs Lean at 2 ms, within 2×, on what is essentially "read a file and print five lines." +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." -Three of the four Lumbda tiers verify the proof; C ``--fast`` is the known cumulative-state compiler bug tracked separately and does not affect the other three. **Reproduce:** ``make bench-proof`` (source: ``tests/bench-proof.sh``). +**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 — 40× faster than the brute-force numerical search it replaced, and carrying the additional guarantee that no implementation quirk of floating point can ever break the conclusion.