C --fast named-let bug: minimal repro + workaround, all 4 tiers pass now
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.
This commit is contained in:
parent
3f51a6b31b
commit
3463fadd3f
4 changed files with 174 additions and 113 deletions
60
c/TODO-named-let-bytecode.md
Normal file
60
c/TODO-named-let-bytecode.md
Normal file
|
|
@ -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, <args...>, 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.
|
||||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
[<c02adde799653294dc72d7b8e3e793c4><c02adde799653294dc72d7b8e3e793c4>]
|
||||
[<1d1d492e26ccbe99cb4cca73ae9eecee><1d1d492e26ccbe99cb4cca73ae9eecee>]
|
||||
% ReportLab generated PDF document -- digest (opensource)
|
||||
|
||||
/Info 59 0 R
|
||||
|
|
@ -9597,5 +9590,5 @@ trailer
|
|||
/Size 168
|
||||
>>
|
||||
startxref
|
||||
2368364
|
||||
2368591
|
||||
%%EOF
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue