diff --git a/asm/uncommonlisp-gc b/asm/uncommonlisp-gc index b8ea325..5e1689a 100755 Binary files a/asm/uncommonlisp-gc and b/asm/uncommonlisp-gc differ diff --git a/asm/uncommonlisp-gc.o b/asm/uncommonlisp-gc.o index b1504f8..a16cb14 100644 Binary files a/asm/uncommonlisp-gc.o and b/asm/uncommonlisp-gc.o differ diff --git a/asm/uncommonlisp.s b/asm/uncommonlisp.s index 636613b..17f01f8 100644 --- a/asm/uncommonlisp.s +++ b/asm/uncommonlisp.s @@ -416,6 +416,14 @@ s_rparen_nl: .ascii ")\n" s_dotsp: .ascii " . " s_minus: .ascii "-" s_hashparen: .ascii "#(" +# Portal v1 header. GC-build portal-save emits this as the first +# line of every output file; portal-resume reads the first bytes +# and verifies the prefix before loading. A file starting with ";;" +# that does NOT match is rejected as an unsupported version. A file +# that does not start with ";;" at all is accepted as legacy +# (pre-v1) and loaded normally for back-compat. +s_portal_v1: .ascii ";; lumbda-portal v1\n" +.equ s_portal_v1_len, 20 # Interned special form symbols (filled at init) .align 8 @@ -4992,6 +5000,14 @@ bi_portal_save: js .ps_gc_fail movq %rax, %rbx # fd + # Emit v1 header. resume() will read this first line and bail + # if it doesn't match, letting us evolve the format cleanly. + movq $SYS_WRITE, %rax + movq %rbx, %rdi + leaq s_portal_v1(%rip), %rsi + movq $s_portal_v1_len, %rdx + syscall + # Redirect printer to the portal file. movq output_fd(%rip), %r12 # save caller's fd movq %rbx, output_fd(%rip) @@ -5052,11 +5068,103 @@ bi_portal_save: .endif .ifdef GC_NAIVE -# GC build: portal-resume is equivalent to (load "filename") since -# the GC portal format is S-expressions. No magic header, no binary -# heap dump to splice back in — just read+eval every form. +# GC build: portal-resume reads the v1 header, then delegates to +# bi_load for the actual form-by-form evaluation. Header check +# lets us reject unknown future versions cleanly instead of +# getting a mysterious parse error on new syntax. +# +# Policy: +# file starts with ";; lumbda-portal v1\n" -> load +# file starts with ";;" but different -> VAL_FALSE (reject) +# file does not start with ";;" at all -> load as legacy bi_portal_resume: + # Peek at arg without consuming %r12 — bi_load needs its own + # GETARG to re-read the filename after we've validated the + # header. + movq %r12, %rax + andq $-8, %rax + movq (%rax), %rbx # filename (tagged string) + andq $-8, %rbx + movq (%rbx), %rcx # string length + leaq 8(%rbx), %rsi # bytes + + # Null-terminate on stack (256-byte slot). + subq $256, %rsp + movq %rsp, %rdi + movq %rcx, %rdx +.prg_cp: + testq %rdx, %rdx + jz .prg_cp_done + movb (%rsi), %al + movb %al, (%rdi) + incq %rsi + incq %rdi + decq %rdx + jmp .prg_cp +.prg_cp_done: + movb $0, (%rdi) + + # Open read-only. + movq $SYS_OPEN, %rax + movq %rsp, %rdi + movq $O_RDONLY, %rsi + xorq %rdx, %rdx + syscall + addq $256, %rsp + testq %rax, %rax + js .prg_fail + movq %rax, %rbx # fd + + # Read up to 32 bytes to inspect the header. + subq $32, %rsp + movq $SYS_READ, %rax + movq %rbx, %rdi + movq %rsp, %rsi + movq $32, %rdx + syscall + # rax = bytes actually read. If <2 we can't tell what it is — accept. + cmpq $2, %rax + jl .prg_close_accept + # Is this a comment line (starts with ";;")? + movzwl (%rsp), %eax + cmpl $0x3b3b, %eax # ";;" + jne .prg_close_accept # no header marker — legacy file, accept + # Header present. Must match s_portal_v1 exactly for the first + # s_portal_v1_len bytes. + leaq s_portal_v1(%rip), %rdi + movq %rsp, %rsi + movq $s_portal_v1_len, %rcx +.prg_match: + movb (%rdi), %al + cmpb (%rsi), %al + jne .prg_bad_version + incq %rdi + incq %rsi + decq %rcx + jnz .prg_match + # Fall through — header matches. + +.prg_close_accept: + addq $32, %rsp + movq $SYS_CLOSE, %rax + movq %rbx, %rdi + syscall + # Delegate to bi_load, which re-opens the file and reads every + # form. The v1 header itself is a ";; comment" line the reader + # already skips. jmp bi_load + +.prg_bad_version: + addq $32, %rsp + movq $SYS_CLOSE, %rax + movq %rbx, %rdi + syscall + movq $VAL_FALSE, %rax + RET_VAL + +.prg_fail: + movq $VAL_FALSE, %rax + RET_VAL .endif .ifndef GC_NAIVE diff --git a/whitepaper/uncommonlisp-whitepaper.pdf b/whitepaper/uncommonlisp-whitepaper.pdf index 214fcfe..d5b6246 100644 --- a/whitepaper/uncommonlisp-whitepaper.pdf +++ b/whitepaper/uncommonlisp-whitepaper.pdf @@ -358,7 +358,7 @@ endobj << /A << /S /URI /Type /Action /URI (mailto:russell@unturf.com) ->> /Border [ 0 0 0 ] /Rect [ 248.0736 476.6236 334.3536 488.6236 ] /Subtype /Link /Type /Annot +>> /Border [ 0 0 0 ] /Rect [ 248.0736 320.6236 334.3536 332.6236 ] /Subtype /Link /Type /Annot >> endobj 44 0 obj @@ -584,7 +584,7 @@ endobj endobj 69 0 obj << -/Author () /CreationDate (D:20260418202758-04'00') /Creator (\(unspecified\)) /Keywords () /ModDate (D:20260418202758-04'00') /Producer (ReportLab PDF Library - \(opensource\)) +/Author () /CreationDate (D:20260419094254-04'00') /Creator (\(unspecified\)) /Keywords () /ModDate (D:20260419094254-04'00') /Producer (ReportLab PDF Library - \(opensource\)) /Subject (\(unspecified\)) /Title () /Trapped /False >> endobj @@ -767,68 +767,68 @@ endobj endobj 104 0 obj << -/Dest [ 38 0 R /XYZ 57.02362 303.4236 0 ] /Next 105 0 R /Parent 98 0 R /Prev 102 0 R /Title (7.5 Cross-Process Benchmarks) +/Dest [ 38 0 R /XYZ 57.02362 189.4236 0 ] /Next 105 0 R /Parent 98 0 R /Prev 102 0 R /Title (7.5 Cross-Process Benchmarks) >> endobj 105 0 obj << -/Dest [ 39 0 R /XYZ 57.02362 691.0236 0 ] /Next 106 0 R /Parent 98 0 R /Prev 104 0 R /Title (7.6 Mismatch Cases: Graceful Degradation) +/Dest [ 39 0 R /XYZ 57.02362 565.0236 0 ] /Next 106 0 R /Parent 98 0 R /Prev 104 0 R /Title (7.6 Mismatch Cases: Graceful Degradation) >> endobj 106 0 obj << -/Dest [ 39 0 R /XYZ 57.02362 425.0236 0 ] /Parent 98 0 R /Prev 105 0 R /Title (7.7 Use Case: Distributed Primality Testing) +/Dest [ 39 0 R /XYZ 57.02362 299.0236 0 ] /Parent 98 0 R /Prev 105 0 R /Title (7.7 Use Case: Distributed Primality Testing) >> endobj 107 0 obj << -/Count 6 /Dest [ 39 0 R /XYZ 57.02362 224.2236 0 ] /First 108 0 R /Last 113 0 R /Next 114 0 R /Parent 71 0 R +/Count 6 /Dest [ 40 0 R /XYZ 57.02362 765.0236 0 ] /First 108 0 R /Last 113 0 R /Next 114 0 R /Parent 71 0 R /Prev 98 0 R /Title (8. The EML Universality Proof) >> endobj 108 0 obj << -/Dest [ 39 0 R /XYZ 57.02362 147.0236 0 ] /Next 109 0 R /Parent 107 0 R /Title (8.1 The Operator) +/Dest [ 40 0 R /XYZ 57.02362 687.8236 0 ] /Next 109 0 R /Parent 107 0 R /Title (8.1 The Operator) >> endobj 109 0 obj << -/Dest [ 40 0 R /XYZ 57.02362 765.0236 0 ] /Next 110 0 R /Parent 107 0 R /Prev 108 0 R /Title (8.2 Stage 1: Core Functions \(Depth 1--3\)) +/Dest [ 40 0 R /XYZ 57.02362 611.0236 0 ] /Next 110 0 R /Parent 107 0 R /Prev 108 0 R /Title (8.2 Stage 1: Core Functions \(Depth 1--3\)) >> endobj 110 0 obj << -/Dest [ 40 0 R /XYZ 57.02362 645.0236 0 ] /Next 111 0 R /Parent 107 0 R /Prev 109 0 R /Title (8.3 Stage 2: Arithmetic) +/Dest [ 40 0 R /XYZ 57.02362 491.0236 0 ] /Next 111 0 R /Parent 107 0 R /Prev 109 0 R /Title (8.3 Stage 2: Arithmetic) >> endobj 111 0 obj << -/Dest [ 40 0 R /XYZ 57.02362 530.6236 0 ] /Next 112 0 R /Parent 107 0 R /Prev 110 0 R /Title (8.4 Stage 3: Complex Plane Access) +/Dest [ 40 0 R /XYZ 57.02362 376.6236 0 ] /Next 112 0 R /Parent 107 0 R /Prev 110 0 R /Title (8.4 Stage 3: Complex Plane Access) >> endobj 112 0 obj << -/Dest [ 40 0 R /XYZ 57.02362 422.6236 0 ] /Next 113 0 R /Parent 107 0 R /Prev 111 0 R /Title (8.5 Stage 4: Trigonometry via Euler) +/Dest [ 40 0 R /XYZ 57.02362 268.6236 0 ] /Next 113 0 R /Parent 107 0 R /Prev 111 0 R /Title (8.5 Stage 4: Trigonometry via Euler) >> endobj 113 0 obj << -/Dest [ 40 0 R /XYZ 57.02362 326.6236 0 ] /Parent 107 0 R /Prev 112 0 R /Title (8.6 Verification & Friction Analysis) +/Dest [ 40 0 R /XYZ 57.02362 172.6236 0 ] /Parent 107 0 R /Prev 112 0 R /Title (8.6 Verification & Friction Analysis) >> endobj 114 0 obj << -/Dest [ 42 0 R /XYZ 57.02362 339.0236 0 ] /Next 115 0 R /Parent 71 0 R /Prev 107 0 R /Title (9. Language Coverage) +/Dest [ 42 0 R /XYZ 57.02362 168.2236 0 ] /Next 115 0 R /Parent 71 0 R /Prev 107 0 R /Title (9. Language Coverage) >> endobj 115 0 obj << -/Dest [ 44 0 R /XYZ 57.02362 765.0236 0 ] /Next 116 0 R /Parent 71 0 R /Prev 114 0 R /Title (10. Relationship to Companion Papers) +/Dest [ 44 0 R /XYZ 57.02362 609.0236 0 ] /Next 116 0 R /Parent 71 0 R /Prev 114 0 R /Title (10. Relationship to Companion Papers) >> endobj 116 0 obj << -/Count 6 /Dest [ 44 0 R /XYZ 57.02362 515.8236 0 ] /First 117 0 R /Last 122 0 R /Next 123 0 R /Parent 71 0 R +/Count 6 /Dest [ 44 0 R /XYZ 57.02362 359.8236 0 ] /First 117 0 R /Last 122 0 R /Next 123 0 R /Parent 71 0 R /Prev 115 0 R /Title (11. Four Implementation Tiers, One Language) >> endobj @@ -6950,7 +6950,7 @@ endstream endobj 149 0 obj << -/Length 8326 +/Length 7564 >> stream 1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET @@ -7034,27 +7034,108 @@ BT 1 0 0 1 0 50 Tm .145197 Tw 12 TL /F3 10 Tf 0 0 0 rg (Trade-off.) Tj /F1 10 Tf Q Q q -1 0 0 1 57.02362 291.4236 cm +1 0 0 1 57.02362 203.4236 cm +q +BT 1 0 0 1 0 98 Tm .352256 Tw 12 TL /F3 10 Tf 0 0 0 rg (Version tag.) Tj /F1 10 Tf ( Every v1 portal starts with a single comment line \227 ) Tj /F5 10 Tf (;;) Tj ( ) Tj (lumbda-portal) Tj ( ) Tj (v1) Tj /F1 10 Tf ( \227 that Scheme) Tj T* 0 Tw 1.054609 Tw (readers already skip but the resume path actively parses. The matching policy: a file beginning with ) Tj /F5 10 Tf (;;) Tj /F1 10 Tf ( is) Tj T* 0 Tw .969272 Tw (required to match the v1 prefix exactly, or ) Tj /F5 10 Tf (portal-resume) Tj /F1 10 Tf ( returns ) Tj /F5 10 Tf (#f) Tj /F1 10 Tf ( instead of trying to evaluate forms) Tj T* 0 Tw .037808 Tw (that may use syntax the current reader doesn't understand. A file that doesn't begin with ) Tj /F5 10 Tf (;;) Tj /F1 10 Tf ( at all is accepted) Tj T* 0 Tw .136772 Tw (as legacy \(pre-v1\) for back-compat. The S-expression portal is a ) Tj /F3 10 Tf (migration format) Tj /F1 10 Tf (, not an archive format \227) Tj T* 0 Tw 1.54465 Tw (it exists to hand live data across a process boundary at handoff time, not to carry state across years of) Tj T* 0 Tw 1.13755 Tw (language evolution. When we need the latter, it earns its own format with proper schema evolution and a) Tj T* 0 Tw 1.366962 Tw (builtin-rename mapping table; the current portal stays simple and the version tag is the hook that lets v2) Tj T* 0 Tw (happen cleanly when someone actually needs it.) Tj T* ET +Q +Q +q +1 0 0 1 57.02362 177.4236 cm q BT 1 0 0 1 0 2 Tm 12 TL /F2 10 Tf .133333 .133333 .133333 rg (7.5 Cross-Process Benchmarks) Tj T* ET Q Q q -1 0 0 1 57.02362 249.4236 cm +1 0 0 1 57.02362 135.4236 cm q BT 1 0 0 1 0 26 Tm 2.703647 Tw 12 TL /F1 10 Tf 0 0 0 rg (Producer process A saves state to a file; consumer process B starts fresh, loads the file, continues.) Tj T* 0 Tw 10.67759 Tw (Wall-clock time for both processes end-to-end, 50 iterations, same-laptop. ) Tj /F3 10 Tf (Reproduce:) Tj /F1 10 Tf T* 0 Tw /F5 10 Tf (make) Tj ( ) Tj (bench-portal) Tj /F1 10 Tf ( \(source: ) Tj /F5 10 Tf (tests/portal-benchmark.sh) Tj /F1 10 Tf (\).) Tj T* ET Q Q q -1 0 0 1 57.02362 243.4236 cm +1 0 0 1 57.02362 129.4236 cm Q q -1 0 0 1 57.02362 63.42362 cm +1 0 0 1 57.02362 75.42362 cm q 1 1 1 rg -n 0 180 481.2283 -18 re f* +n 0 54 481.2283 -18 re f* .878431 .878431 .878431 rg -n 0 162 481.2283 -18 re f* +n 0 36 481.2283 -18 re f* +1 1 1 rg +n 0 18 481.2283 -18 re f* +0 0 0 rg +BT /F3 10 Tf 12 TL ET +q +1 0 0 1 6 39 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 93.12904 0 Td (Pair \(producer ) Tj /F6 10 Tf 12 TL (\256) Tj /F3 10 Tf 12 TL ( consumer\)) Tj T* -93.12904 0 Td ET +Q +Q +q +1 0 0 1 339.1581 39 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 47.19513 0 Td (Time/iter) Tj T* -47.19513 0 Td ET +Q +Q +0 0 0 rg +BT /F1 10 Tf 12 TL ET +q +1 0 0 1 6 21 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (Python ) Tj /F6 10 Tf 12 TL (\256) Tj /F1 10 Tf 12 TL ( Python \(sexp\)) Tj T* ET +Q +Q +q +1 0 0 1 339.1581 21 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (260 ms) Tj T* ET +Q +Q +q +1 0 0 1 6 3 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (C ) Tj /F6 10 Tf 12 TL (\256) Tj /F1 10 Tf 12 TL ( C \(sexp\)) Tj T* ET +Q +Q +q +1 0 0 1 339.1581 3 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (6 ms) Tj T* ET +Q +Q +q +1 J +1 j +0 0 0 RG +.25 w +n 0 0 m 481.2283 0 l S +n 0 36 m 481.2283 36 l S +n 0 18 m 481.2283 18 l S +n 333.1581 0 m 333.1581 54 l S +n 0 54 m 481.2283 54 l S +n 0 0 m 0 54 l S +n 481.2283 0 m 481.2283 54 l S +Q +Q +Q + +endstream +endobj +150 0 obj +<< +/Length 9535 +>> +stream +1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET +q +1 0 0 1 57.02362 621.0236 cm +q 1 1 1 rg n 0 144 481.2283 -18 re f* .878431 .878431 .878431 rg @@ -7072,188 +7153,106 @@ n 0 36 481.2283 -18 re f* .878431 .878431 .878431 rg n 0 18 481.2283 -18 re f* 0 0 0 rg -BT /F3 10 Tf 12 TL ET -q -1 0 0 1 6 165 cm -q -0 0 0 rg -BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 93.12904 0 Td (Pair \(producer ) Tj /F6 10 Tf 12 TL (\256) Tj /F3 10 Tf 12 TL ( consumer\)) Tj T* -93.12904 0 Td ET -Q -Q -q -1 0 0 1 339.1581 165 cm -q -0 0 0 rg -BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 47.19513 0 Td (Time/iter) Tj T* -47.19513 0 Td ET -Q -Q -0 0 0 rg BT /F1 10 Tf 12 TL ET q -1 0 0 1 6 147 cm -q -0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (Python ) Tj /F6 10 Tf 12 TL (\256) Tj /F1 10 Tf 12 TL ( Python \(sexp\)) Tj T* ET -Q -Q -q -1 0 0 1 339.1581 147 cm -q -0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (260 ms) Tj T* ET -Q -Q -q 1 0 0 1 6 129 cm q 0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (C ) Tj /F6 10 Tf 12 TL (\256) Tj /F1 10 Tf 12 TL ( C \(sexp\)) Tj T* ET -Q -Q -q -1 0 0 1 339.1581 129 cm -q -0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (6 ms) Tj T* ET -Q -Q -q -1 0 0 1 6 111 cm -q -0 0 0 rg BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL (asm ) Tj /F6 10 Tf 12 TL (\256) Tj /F3 10 Tf 12 TL ( asm \(sexp\)) Tj T* ET Q Q q -1 0 0 1 339.1581 111 cm +1 0 0 1 339.1581 129 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL (1.6 ms) Tj T* ET Q Q q -1 0 0 1 6 93 cm +1 0 0 1 6 111 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL (asm ) Tj /F6 10 Tf 12 TL (\256) Tj /F3 10 Tf 12 TL ( asm \(binary portal\)) Tj T* ET Q Q q -1 0 0 1 339.1581 93 cm +1 0 0 1 339.1581 111 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL (1.5 ms) Tj T* ET Q Q q -1 0 0 1 6 75 cm +1 0 0 1 6 93 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (Python ) Tj /F6 10 Tf 12 TL (\256) Tj /F1 10 Tf 12 TL ( C \(sexp\)) Tj T* ET Q Q q -1 0 0 1 339.1581 75 cm +1 0 0 1 339.1581 93 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (133 ms) Tj T* ET Q Q q -1 0 0 1 6 57 cm +1 0 0 1 6 75 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (Python ) Tj /F6 10 Tf 12 TL (\256) Tj /F1 10 Tf 12 TL ( asm \(sexp\)) Tj T* ET Q Q q -1 0 0 1 339.1581 57 cm +1 0 0 1 339.1581 75 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (145 ms) Tj T* ET Q Q q -1 0 0 1 6 39 cm +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 (C ) Tj /F6 10 Tf 12 TL (\256) Tj /F1 10 Tf 12 TL ( Python \(sexp\)) Tj T* ET Q Q q -1 0 0 1 339.1581 39 cm +1 0 0 1 339.1581 57 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (154 ms) Tj T* ET Q Q q -1 0 0 1 6 21 cm +1 0 0 1 6 39 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (C ) Tj /F6 10 Tf 12 TL (\256) Tj /F1 10 Tf 12 TL ( asm \(sexp\)) Tj T* ET Q Q q -1 0 0 1 339.1581 21 cm +1 0 0 1 339.1581 39 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (4.1 ms) Tj T* ET Q Q q -1 0 0 1 6 3 cm +1 0 0 1 6 21 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (asm ) Tj /F6 10 Tf 12 TL (\256) Tj /F1 10 Tf 12 TL ( Python \(sexp\)) Tj T* ET Q Q q -1 0 0 1 339.1581 3 cm +1 0 0 1 339.1581 21 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (167 ms) Tj T* ET Q Q q -1 J -1 j -0 0 0 RG -.25 w -n 0 0 m 481.2283 0 l S -n 0 162 m 481.2283 162 l S -n 0 144 m 481.2283 144 l S -n 0 126 m 481.2283 126 l S -n 0 108 m 481.2283 108 l S -n 0 90 m 481.2283 90 l S -n 0 72 m 481.2283 72 l S -n 0 54 m 481.2283 54 l S -n 0 36 m 481.2283 36 l S -n 0 18 m 481.2283 18 l S -n 333.1581 0 m 333.1581 180 l S -n 0 180 m 481.2283 180 l S -n 0 0 m 0 180 l S -n 481.2283 0 m 481.2283 180 l S -Q -Q -Q - -endstream -endobj -150 0 obj -<< -/Length 8648 ->> -stream -1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET -q -1 0 0 1 57.02362 747.0236 cm -q -1 1 1 rg -n 0 18 481.2283 -18 re f* -0 0 0 rg -BT /F1 10 Tf 12 TL ET -q 1 0 0 1 6 3 cm q 0 0 0 rg @@ -7272,41 +7271,48 @@ q 1 j 0 0 0 RG .25 w +n 0 144 m 481.2283 144 l S +n 0 126 m 481.2283 126 l S +n 0 108 m 481.2283 108 l S +n 0 90 m 481.2283 90 l S +n 0 72 m 481.2283 72 l S +n 0 54 m 481.2283 54 l S +n 0 36 m 481.2283 36 l S n 0 18 m 481.2283 18 l S -n 333.1581 0 m 333.1581 18 l S -n 0 0 m 0 18 l S -n 481.2283 0 m 481.2283 18 l S +n 333.1581 0 m 333.1581 144 l S +n 0 0 m 0 144 l S +n 481.2283 0 m 481.2283 144 l S n 0 0 m 481.2283 0 l S Q Q Q q -1 0 0 1 57.02362 747.0236 cm +1 0 0 1 57.02362 621.0236 cm Q q -1 0 0 1 57.02362 705.0236 cm +1 0 0 1 57.02362 579.0236 cm q BT 1 0 0 1 0 26 Tm .698334 Tw 12 TL /F1 10 Tf 0 0 0 rg (The asm) Tj /F6 10 Tf 12 TL (\256) Tj /F1 10 Tf 12 TL (asm cross-process is ~160\327 faster than Python) Tj /F6 10 Tf 12 TL (\256) Tj /F1 10 Tf 12 TL (Python. The binary & S-expression portals are) Tj T* 0 Tw .812256 Tw (within 10% of each other on this workload \227 the bottleneck is process startup, not serialization. For larger) Tj T* 0 Tw (heaps the binary format pulls further ahead; for portability, S-expression always wins.) Tj T* ET Q Q q -1 0 0 1 57.02362 679.0236 cm +1 0 0 1 57.02362 553.0236 cm q BT 1 0 0 1 0 2 Tm 12 TL /F2 10 Tf .133333 .133333 .133333 rg (7.6 Mismatch Cases: Graceful Degradation) Tj T* ET Q Q q -1 0 0 1 57.02362 661.0236 cm +1 0 0 1 57.02362 535.0236 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (A usable persistence layer fails well. What happens when the consumer meets unexpected input?) Tj T* ET Q Q q -1 0 0 1 57.02362 655.0236 cm +1 0 0 1 57.02362 529.0236 cm Q q -1 0 0 1 57.02362 505.0236 cm +1 0 0 1 57.02362 379.0236 cm q 1 1 1 rg n 0 150 481.2283 -18 re f* @@ -7539,22 +7545,22 @@ Q Q Q q -1 0 0 1 57.02362 505.0236 cm +1 0 0 1 57.02362 379.0236 cm Q q -1 0 0 1 57.02362 439.0236 cm +1 0 0 1 57.02362 313.0236 cm q BT 1 0 0 1 0 50 Tm 1.476556 Tw 12 TL /F1 10 Tf 0 0 0 rg (All defects surfaced & fixed during benchmark development: an asm segfault on ) Tj /F5 10 Tf (\(define) Tj ( ) Tj (x\)) Tj /F1 10 Tf ( without a) Tj T* 0 Tw 1.838453 Tw (value \(now binds to ) Tj /F5 10 Tf (VOID) Tj /F1 10 Tf (\), an asm portal-resume that accepted short headers \(now verifies ) Tj /F5 10 Tf (sys_read) Tj /F1 10 Tf T* 0 Tw 1.204272 Tw (returned a full 48 bytes & sanity-checks heap metadata\), a Python ) Tj /F5 10 Tf (file) Tj ( ) Tj (not) Tj ( ) Tj (found) Tj /F1 10 Tf ( error reporting the) Tj T* 0 Tw 1.304862 Tw (outer script path instead of the inner missing file \(now uses ) Tj /F5 10 Tf (FileNotFoundError.filename) Tj /F1 10 Tf (\). Graceful) Tj T* 0 Tw (degradation is not free; it is tested.) Tj T* ET Q Q q -1 0 0 1 57.02362 413.0236 cm +1 0 0 1 57.02362 287.0236 cm q BT 1 0 0 1 0 2 Tm 12 TL /F2 10 Tf .133333 .133333 .133333 rg (7.7 Use Case: Distributed Primality Testing) Tj T* ET Q Q q -1 0 0 1 57.02362 286.2236 cm +1 0 0 1 57.02362 160.2236 cm q q 1 0 0 1 0 0 cm @@ -7574,38 +7580,47 @@ Q Q Q q -1 0 0 1 57.02362 242.2236 cm +1 0 0 1 57.02362 116.2236 cm q BT 1 0 0 1 0 26 Tm 1.105522 Tw 12 TL /F1 10 Tf 0 0 0 rg (Machine A starts the computation. Every 10,000 iterations, it writes a checkpoint. Machine B picks up the) Tj T* 0 Tw 2.790642 Tw /F5 10 Tf (.portal) Tj /F1 10 Tf ( file & continues from the last checkpoint. The computation migrates without either machine) Tj T* 0 Tw (needing to know about the other. Feedback \227 the continuation \227 carries the entire execution context.) Tj T* ET Q Q + +endstream +endobj +151 0 obj +<< +/Length 7783 +>> +stream +1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET q -1 0 0 1 57.02362 211.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 (8. The EML Universality Proof) Tj T* ET Q Q q -1 0 0 1 57.02362 179.0236 cm +1 0 0 1 57.02362 719.8236 cm q BT 1 0 0 1 0 14 Tm 3.669104 Tw 12 TL /F1 10 Tf 0 0 0 rg (Lumbda ships with a mathematical proof that a single operator generates all elementary functions:) Tj T* 0 Tw /F5 10 Tf (eml\(x,) Tj ( ) Tj (y\)) Tj ( ) Tj (=) Tj ( ) Tj (exp\(x\)) Tj ( ) Tj (-) Tj ( ) Tj (ln\(y\)) Tj /F1 10 Tf (.) Tj T* ET Q Q q -1 0 0 1 57.02362 161.0236 cm +1 0 0 1 57.02362 701.8236 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (Reference: "All elementary functions from a single operator" \(arXiv:2603.21852v2\).) Tj T* ET Q Q q -1 0 0 1 57.02362 135.0236 cm +1 0 0 1 57.02362 675.8236 cm q BT 1 0 0 1 0 2 Tm 12 TL /F2 10 Tf .133333 .133333 .133333 rg (8.1 The Operator) Tj T* ET Q Q q -1 0 0 1 57.02362 104.2236 cm +1 0 0 1 57.02362 645.0236 cm q q 1 0 0 1 0 0 cm @@ -7626,28 +7641,19 @@ Q Q Q q -1 0 0 1 57.02362 84.22362 cm +1 0 0 1 57.02362 625.0236 cm q BT 1 0 0 1 0 2 Tm 12 TL /F1 10 Tf 0 0 0 rg (With this operator & the constant ) Tj /F5 10 Tf (1) Tj /F1 10 Tf (, the following derivation chain constructs every elementary function:) Tj T* ET Q Q - -endstream -endobj -151 0 obj -<< -/Length 9423 ->> -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 599.0236 cm q BT 1 0 0 1 0 2 Tm 12 TL /F2 10 Tf .133333 .133333 .133333 rg (8.2 Stage 1: Core Functions \(Depth 1--3\)) Tj T* ET Q Q q -1 0 0 1 57.02362 703.0236 cm +1 0 0 1 57.02362 549.0236 cm q q 1 0 0 1 0 0 cm @@ -7668,19 +7674,19 @@ Q Q Q q -1 0 0 1 57.02362 659.0236 cm +1 0 0 1 57.02362 505.0236 cm q BT 1 0 0 1 0 26 Tm 16.01403 Tw 12 TL /F3 10 Tf 0 0 0 rg (Proof of ln recovery) Tj /F1 10 Tf (: Let ) Tj /F5 10 Tf (a) Tj ( ) Tj (=) Tj ( ) Tj (eml\(1,x\)) Tj ( ) Tj (=) Tj ( ) Tj (e) Tj ( ) Tj (-) Tj ( ) Tj (ln\(x\)) Tj /F1 10 Tf (. Then) Tj T* 0 Tw 28.85979 Tw /F5 10 Tf (eml\(a,) Tj ( ) Tj (1\)) Tj ( ) Tj (=) Tj ( ) Tj (exp\(e) Tj ( ) Tj (-) Tj ( ) Tj (ln\(x\)\)) Tj ( ) Tj (=) Tj ( ) Tj (exp\(e\)/x) Tj /F1 10 Tf (. Then) Tj T* 0 Tw /F5 10 Tf (eml\(1,) Tj ( ) Tj (exp\(e\)/x\)) Tj ( ) Tj (=) Tj ( ) Tj (e) Tj ( ) Tj (-) Tj ( ) Tj (ln\(exp\(e\)/x\)) Tj ( ) Tj (=) Tj ( ) Tj (e) Tj ( ) Tj (-) Tj ( ) Tj (e) Tj ( ) Tj (+) Tj ( ) Tj (ln\(x\)) Tj ( ) Tj (=) Tj ( ) Tj (ln\(x\)) Tj /F1 10 Tf (.) Tj T* ET Q Q q -1 0 0 1 57.02362 633.0236 cm +1 0 0 1 57.02362 479.0236 cm q BT 1 0 0 1 0 2 Tm 12 TL /F2 10 Tf .133333 .133333 .133333 rg (8.3 Stage 2: Arithmetic) Tj T* ET Q Q q -1 0 0 1 57.02362 544.6236 cm +1 0 0 1 57.02362 390.6236 cm q q 1 0 0 1 0 0 cm @@ -7700,13 +7706,13 @@ Q Q Q q -1 0 0 1 57.02362 518.6236 cm +1 0 0 1 57.02362 364.6236 cm q BT 1 0 0 1 0 2 Tm 12 TL /F2 10 Tf .133333 .133333 .133333 rg (8.4 Stage 3: Complex Plane Access) Tj T* ET Q Q q -1 0 0 1 57.02362 468.6236 cm +1 0 0 1 57.02362 314.6236 cm q q 1 0 0 1 0 0 cm @@ -7727,19 +7733,19 @@ Q Q Q q -1 0 0 1 57.02362 436.6236 cm +1 0 0 1 57.02362 282.6236 cm q BT 1 0 0 1 0 14 Tm .253071 Tw 12 TL /F1 10 Tf 0 0 0 rg (The key insight: ) Tj /F5 10 Tf (ln) Tj /F1 10 Tf ( of a negative number enters the complex plane. Since we can construct ) Tj /F5 10 Tf (-1) Tj /F1 10 Tf ( from eml via) Tj T* 0 Tw (the subtraction chain, ) Tj /F5 10 Tf (ln\(-1\)) Tj /F1 10 Tf ( yields ) Tj /F5 10 Tf (i) Tj /F6 10 Tf 12 TL (p) Tj /F5 10 Tf 12 TL /F1 10 Tf (, from which ) Tj /F5 10 Tf /F6 10 Tf 12 TL (p) Tj /F5 10 Tf 12 TL /F1 10 Tf ( & ) Tj /F5 10 Tf (i) Tj /F1 10 Tf ( follow.) Tj T* ET Q Q q -1 0 0 1 57.02362 410.6236 cm +1 0 0 1 57.02362 256.6236 cm q BT 1 0 0 1 0 2 Tm 12 TL /F2 10 Tf .133333 .133333 .133333 rg (8.5 Stage 4: Trigonometry via Euler) Tj T* ET Q Q q -1 0 0 1 57.02362 360.6236 cm +1 0 0 1 57.02362 206.6236 cm q q 1 0 0 1 0 0 cm @@ -7760,69 +7766,61 @@ Q Q Q q -1 0 0 1 57.02362 340.6236 cm +1 0 0 1 57.02362 186.6236 cm q BT 1 0 0 1 0 2 Tm 12 TL /F1 10 Tf 0 0 0 rg (All trigonometric functions follow from complex exponentials, which follow from ) Tj /F5 10 Tf (exp) Tj /F1 10 Tf (, which follows from ) Tj /F5 10 Tf (eml) Tj /F1 10 Tf (.) Tj T* ET Q Q q -1 0 0 1 57.02362 314.6236 cm +1 0 0 1 57.02362 160.6236 cm q BT 1 0 0 1 0 2 Tm 12 TL /F2 10 Tf .133333 .133333 .133333 rg (8.6 Verification & Friction Analysis) Tj T* ET Q Q q -1 0 0 1 57.02362 296.6236 cm +1 0 0 1 57.02362 142.6236 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (The proof has been verified at six distinct levels. Times are best-of-3 on the i5-8350U:) Tj T* ET Q Q q -1 0 0 1 57.02362 290.6236 cm +1 0 0 1 57.02362 136.6236 cm Q q -1 0 0 1 57.02362 140.6236 cm +1 0 0 1 57.02362 70.62362 cm q 1 1 1 rg -n 0 150 481.2283 -18 re f* +n 0 66 481.2283 -18 re f* .878431 .878431 .878431 rg -n 0 132 481.2283 -18 re f* +n 0 48 481.2283 -18 re f* 1 1 1 rg -n 0 114 481.2283 -30 re f* -.878431 .878431 .878431 rg -n 0 84 481.2283 -30 re f* -1 1 1 rg -n 0 54 481.2283 -18 re f* -.878431 .878431 .878431 rg -n 0 36 481.2283 -18 re f* -1 1 1 rg -n 0 18 481.2283 -18 re f* +n 0 30 481.2283 -30 re f* 0 0 0 rg BT /F3 10 Tf 12 TL ET q -1 0 0 1 6 135 cm +1 0 0 1 6 51 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 57.2861 0 Td (Approach) Tj T* -57.2861 0 Td ET Q Q q -1 0 0 1 179.2422 135 cm +1 0 0 1 179.2422 51 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 11.2037 0 Td (Time) Tj T* -11.2037 0 Td ET Q Q q -1 0 0 1 236.9896 135 cm +1 0 0 1 236.9896 51 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 27.0174 0 Td (Guarantee) Tj T* -27.0174 0 Td ET Q Q q -1 0 0 1 352.4844 135 cm +1 0 0 1 352.4844 51 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 43.03697 0 Td (Friction) Tj T* -43.03697 0 Td ET @@ -7831,61 +7829,100 @@ Q 0 0 0 rg BT /F1 10 Tf 12 TL ET q -1 0 0 1 6 117 cm +1 0 0 1 6 33 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (Python \(numerical evaluation\)) Tj T* ET Q Q q -1 0 0 1 179.2422 117 cm +1 0 0 1 179.2422 33 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (0.04 s) Tj T* ET Q Q q -1 0 0 1 236.9896 117 cm +1 0 0 1 236.9896 33 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (1e-10 tolerance) Tj T* ET Q Q q -1 0 0 1 352.4844 117 cm +1 0 0 1 352.4844 33 cm q BT 1 0 0 1 0 2 Tm 12 TL /F1 10 Tf 0 0 0 rg (Low: evaluate & compare) Tj T* ET Q Q q -1 0 0 1 6 87 cm +1 0 0 1 6 3 cm q 0 0 0 rg BT 1 0 0 1 0 14 Tm /F1 10 Tf 12 TL (Lumbda \(numerical brute-force) Tj T* (search\)) Tj T* ET Q Q q -1 0 0 1 179.2422 99 cm +1 0 0 1 179.2422 15 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (59 s) Tj T* ET Q Q q -1 0 0 1 236.9896 99 cm +1 0 0 1 236.9896 15 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (1e-10 tolerance) Tj T* ET Q Q q -1 0 0 1 352.4844 87 cm +1 0 0 1 352.4844 3 cm q 0 0 0 rg BT 1 0 0 1 0 14 Tm /F1 10 Tf 12 TL (High: O\(N\262\) pairwise) Tj T* (search) Tj T* ET Q Q q +1 J +1 j +0 0 0 RG +.25 w +n 0 0 m 481.2283 0 l S +n 0 48 m 481.2283 48 l S +n 0 30 m 481.2283 30 l S +n 173.2422 0 m 173.2422 66 l S +n 230.9896 0 m 230.9896 66 l S +n 346.4844 0 m 346.4844 66 l S +n 0 66 m 481.2283 66 l S +n 0 0 m 0 66 l S +n 481.2283 0 m 481.2283 66 l S +Q +Q +Q + +endstream +endobj +152 0 obj +<< +/Length 10223 +>> +stream +1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET +q +1 0 0 1 57.02362 681.0236 cm +q +1 1 1 rg +n 0 84 481.2283 -30 re f* +.878431 .878431 .878431 rg +n 0 54 481.2283 -18 re f* +1 1 1 rg +n 0 36 481.2283 -18 re f* +.878431 .878431 .878431 rg +n 0 18 481.2283 -18 re f* +0 0 0 rg +BT /F1 10 Tf 12 TL ET +q 1 0 0 1 6 69 cm q 0 0 0 rg @@ -8001,79 +8038,51 @@ q 1 j 0 0 0 RG .25 w -n 0 132 m 481.2283 132 l S -n 0 114 m 481.2283 114 l S n 0 84 m 481.2283 84 l S n 0 54 m 481.2283 54 l S n 0 36 m 481.2283 36 l S n 0 18 m 481.2283 18 l S -n 173.2422 0 m 173.2422 150 l S -n 230.9896 0 m 230.9896 150 l S -n 346.4844 0 m 346.4844 150 l S -n 0 150 m 481.2283 150 l S +n 173.2422 0 m 173.2422 84 l S +n 230.9896 0 m 230.9896 84 l S +n 346.4844 0 m 346.4844 84 l S +n 0 0 m 0 84 l S +n 481.2283 0 m 481.2283 84 l S n 0 0 m 481.2283 0 l S -n 0 0 m 0 150 l S -n 481.2283 0 m 481.2283 150 l S Q Q Q q -1 0 0 1 57.02362 140.6236 cm +1 0 0 1 57.02362 681.0236 cm Q q -1 0 0 1 57.02362 122.6236 cm +1 0 0 1 57.02362 663.0236 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL (Three separate wins compound here.) Tj T* ET Q Q q -1 0 0 1 57.02362 116.6236 cm +1 0 0 1 57.02362 657.0236 cm Q q -1 0 0 1 57.02362 116.6236 cm +1 0 0 1 57.02362 657.0236 cm Q q -1 0 0 1 57.02362 62.69291 cm +1 0 0 1 57.02362 585.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET q -1 0 0 1 6 38.93071 cm +1 0 0 1 6 57 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F5 10 Tf 12 TL 2 0 Td (1.) Tj T* -2 0 Td ET Q Q q -1 0 0 1 23 14.93071 cm -q -BT 1 0 0 1 0 26 Tm 1.90218 Tw 12 TL /F3 10 Tf 0 0 0 rg (Algorithmic: symbolic vs numerical) Tj /F1 10 Tf ( \227 the Lumbda symbolic rewriter is ) Tj /F3 10 Tf (~1,280\327 faster) Tj /F1 10 Tf ( than the) Tj T* 0 Tw .906556 Tw (Lumbda brute-force search \(46 ms vs 59 s\). This is the MOAD-0001 defect at the proof-methodology) Tj T* 0 Tw .474835 Tw (layer: O\(N\262\) enumerate-and-compare where O\(1\) algebraic reasoning suffices. The brute-force version) Tj T* 0 Tw ET -Q -Q -q -Q -Q -Q - -endstream -endobj -152 0 obj -<< -/Length 8752 ->> -stream -1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET -q -1 0 0 1 57.02362 729.0236 cm -q -0 0 0 rg -BT /F1 10 Tf 12 TL ET -BT 1 0 0 1 6 23 Tm T* ET -q 1 0 0 1 23 -3 cm q -BT 1 0 0 1 0 26 Tm .206529 Tw 12 TL /F1 10 Tf 0 0 0 rg (enumerates every pairwise EML composition at each depth, comparing results against target functions;) Tj T* 0 Tw 2.312025 Tw (the symbolic checker applies 5 rewrites using 3 axioms \() Tj /F5 10 Tf (exp\(ln\(x\)\)) Tj ( ) Tj (=) Tj ( ) Tj (x) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (ln\(exp\(x\)\)) Tj ( ) Tj (=) Tj ( ) Tj (x) Tj /F1 10 Tf (,) Tj T* 0 Tw /F5 10 Tf (ln\(1\)) Tj ( ) Tj (=) Tj ( ) Tj (0) Tj /F1 10 Tf (\) and terminates. Understanding beats search by three orders of magnitude.) Tj T* ET +BT 1 0 0 1 0 62 Tm 1.90218 Tw 12 TL /F3 10 Tf 0 0 0 rg (Algorithmic: symbolic vs numerical) Tj /F1 10 Tf ( \227 the Lumbda symbolic rewriter is ) Tj /F3 10 Tf (~1,280\327 faster) Tj /F1 10 Tf ( than the) Tj T* 0 Tw .906556 Tw (Lumbda brute-force search \(46 ms vs 59 s\). This is the MOAD-0001 defect at the proof-methodology) Tj T* 0 Tw .474835 Tw (layer: O\(N\262\) enumerate-and-compare where O\(1\) algebraic reasoning suffices. The brute-force version) Tj T* 0 Tw .206529 Tw (enumerates every pairwise EML composition at each depth, comparing results against target functions;) Tj T* 0 Tw 2.312025 Tw (the symbolic checker applies 5 rewrites using 3 axioms \() Tj /F5 10 Tf (exp\(ln\(x\)\)) Tj ( ) Tj (=) Tj ( ) Tj (x) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (ln\(exp\(x\)\)) Tj ( ) Tj (=) Tj ( ) Tj (x) Tj /F1 10 Tf (,) Tj T* 0 Tw /F5 10 Tf (ln\(1\)) Tj ( ) Tj (=) Tj ( ) Tj (0) Tj /F1 10 Tf (\) and terminates. Understanding beats search by three orders of magnitude.) Tj T* ET Q Q q @@ -8081,10 +8090,10 @@ Q Q Q q -1 0 0 1 57.02362 723.0236 cm +1 0 0 1 57.02362 579.0236 cm Q q -1 0 0 1 57.02362 675.0236 cm +1 0 0 1 57.02362 531.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -8106,10 +8115,10 @@ Q Q Q q -1 0 0 1 57.02362 669.0236 cm +1 0 0 1 57.02362 525.0236 cm Q q -1 0 0 1 57.02362 609.0236 cm +1 0 0 1 57.02362 465.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -8131,34 +8140,34 @@ Q Q Q q -1 0 0 1 57.02362 609.0236 cm +1 0 0 1 57.02362 465.0236 cm Q q -1 0 0 1 57.02362 543.0236 cm +1 0 0 1 57.02362 399.0236 cm q BT 1 0 0 1 0 50 Tm .913719 Tw 12 TL /F3 10 Tf 0 0 0 rg (Symmetric honesty.) Tj /F1 10 Tf ( Lean's kernel guarantees remain stronger even when the timings equalize: the Lean) Tj T* 0 Tw .45989 Tw (TCB is ~3 KLOC of audited elaborator/kernel, while Lumbda's asm interpreter is ~6.6 KLOC of hand-written) Tj T* 0 Tw .884917 Tw (assembly. For proofs where the cost of a bug in the checker itself matters, Lean is the right tool; for small) Tj T* 0 Tw 2.400556 Tw (symbolic-rewrite proofs where the language hosting the proof should be able to host the checker too,) Tj T* 0 Tw (Lumbda does the job in under 50 ms cold without external dependencies.) Tj T* ET Q Q q -1 0 0 1 57.02362 489.0236 cm +1 0 0 1 57.02362 345.0236 cm q BT 1 0 0 1 0 38 Tm 3.571147 Tw 12 TL /F3 10 Tf 0 0 0 rg (Lesson) Tj /F1 10 Tf (: The fastest path to truth is not computation \227 it is understanding. When you know ) Tj /F4 10 Tf (why) Tj /F1 10 Tf T* 0 Tw .96189 Tw /F5 10 Tf (eml\(1,) Tj ( ) Tj (eml\(eml\(1,x\),) Tj ( ) Tj (1\)\)) Tj ( ) Tj (=) Tj ( ) Tj (ln\(x\)) Tj /F1 10 Tf (, you verify it in microseconds. When you don't, you search for) Tj T* 0 Tw .874862 Tw (hours. Symbolic reasoning eliminates the quadratic friction of numerical verification; caching eliminates the) Tj T* 0 Tw (startup friction of every verifier. Both layers stack.) Tj T* ET Q Q q -1 0 0 1 57.02362 459.0236 cm +1 0 0 1 57.02362 315.0236 cm q BT 1 0 0 1 0 14 Tm .708556 Tw 12 TL /F3 10 Tf 0 0 0 rg (Reproduce:) Tj /F1 10 Tf ( ) Tj /F5 10 Tf (make) Tj ( ) Tj (bench-proof) Tj /F1 10 Tf ( runs the cold and cached paths for both Lumbda \(across all three tiers\)) Tj T* 0 Tw (and Lean. Source: ) Tj /F5 10 Tf (proof/benchmark.sh) Tj /F1 10 Tf (.) Tj T* ET Q Q q -1 0 0 1 57.02362 453.0236 cm +1 0 0 1 57.02362 309.0236 cm Q q -1 0 0 1 57.02362 453.0236 cm +1 0 0 1 57.02362 309.0236 cm Q q -1 0 0 1 57.02362 417.0236 cm +1 0 0 1 57.02362 273.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -8180,10 +8189,10 @@ Q Q Q q -1 0 0 1 57.02362 411.0236 cm +1 0 0 1 57.02362 267.0236 cm Q q -1 0 0 1 57.02362 375.0236 cm +1 0 0 1 57.02362 231.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -8205,10 +8214,10 @@ Q Q Q q -1 0 0 1 57.02362 369.0236 cm +1 0 0 1 57.02362 225.0236 cm Q q -1 0 0 1 57.02362 345.0236 cm +1 0 0 1 57.02362 201.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -8230,10 +8239,10 @@ Q Q Q q -1 0 0 1 57.02362 345.0236 cm +1 0 0 1 57.02362 201.0236 cm Q q -1 0 0 1 57.02362 275.8236 cm +1 0 0 1 57.02362 131.8236 cm q q 1 0 0 1 0 0 cm @@ -8254,19 +8263,28 @@ Q Q Q q -1 0 0 1 57.02362 231.8236 cm +1 0 0 1 57.02362 87.82362 cm q BT 1 0 0 1 0 26 Tm 4.138556 Tw 12 TL /F1 10 Tf 0 0 0 rg (The Lean proof operates over abstract ) Tj /F5 10 Tf (exp) Tj /F1 10 Tf ( & ) Tj /F5 10 Tf (ln) Tj /F1 10 Tf ( functions with the axioms ) Tj /F5 10 Tf (exp\(ln\(x\)\)) Tj ( ) Tj (=) Tj ( ) Tj (x) Tj /F1 10 Tf (,) Tj T* 0 Tw 2.484897 Tw /F5 10 Tf (ln\(exp\(x\)\)) Tj ( ) Tj (=) Tj ( ) Tj (x) Tj /F1 10 Tf (, & ) Tj /F5 10 Tf (ln\(1\)) Tj ( ) Tj (=) Tj ( ) Tj (0) Tj /F1 10 Tf (. This makes the result independent of any particular real number) Tj T* 0 Tw (implementation.) Tj T* ET Q Q q -1 0 0 1 57.02362 225.8236 cm +1 0 0 1 57.02362 81.82362 cm Q q -1 0 0 1 57.02362 225.8236 cm +1 0 0 1 57.02362 81.82362 cm Q + +endstream +endobj +153 0 obj +<< +/Length 9888 +>> +stream +1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET q -1 0 0 1 57.02362 141.8236 cm +1 0 0 1 57.02362 681.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -8288,10 +8306,10 @@ Q Q Q q -1 0 0 1 57.02362 141.8236 cm +1 0 0 1 57.02362 681.0236 cm Q q -1 0 0 1 57.02362 63.02362 cm +1 0 0 1 57.02362 602.2236 cm q q 1 0 0 1 0 0 cm @@ -8311,26 +8329,17 @@ Q Q Q Q - -endstream -endobj -153 0 obj -<< -/Length 10148 ->> -stream -1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET q -1 0 0 1 57.02362 705.0236 cm +1 0 0 1 57.02362 534.2236 cm q BT 1 0 0 1 0 50 Tm 4.101411 Tw 12 TL /F3 10 Tf 0 0 0 rg (Verification speed: Lean vs Lumbda tiers, both cold and cached.) Tj /F1 10 Tf ( Same five theorems, same) Tj T* 0 Tw 1.757362 Tw (symbolic-rewrite strategy. The Lumbda checker now implements its own cached-replay path that mirrors) Tj T* 0 Tw .258797 Tw (Lean's: write a small artifact after a successful run; on subsequent runs, trust the artifact if the magic header) Tj T* 0 Tw .759029 Tw (matches and skip re-verification. ) Tj /F5 10 Tf (rm) Tj ( ) Tj (-f) Tj ( ) Tj (/tmp/lumbda-eml.cache) Tj /F1 10 Tf ( forces a cold re-check \(analogous to) Tj T* 0 Tw /F5 10 Tf (lake) Tj ( ) Tj (clean) Tj /F1 10 Tf (\). Best of 3 on the i5-8350U:) Tj T* ET Q Q q -1 0 0 1 57.02362 699.0236 cm +1 0 0 1 57.02362 528.2236 cm Q q -1 0 0 1 57.02362 591.0236 cm +1 0 0 1 57.02362 420.2236 cm q 1 1 1 rg n 0 108 481.2283 -18 re f* @@ -8514,96 +8523,96 @@ Q Q Q q -1 0 0 1 57.02362 591.0236 cm +1 0 0 1 57.02362 420.2236 cm Q q -1 0 0 1 57.02362 525.0236 cm +1 0 0 1 57.02362 354.2236 cm q BT 1 0 0 1 0 50 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 1.150966 Tw (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 459.0236 cm +1 0 0 1 57.02362 288.2236 cm q 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 357.0236 cm +1 0 0 1 57.02362 186.2236 cm q BT 1 0 0 1 0 86 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 /F9 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 .312025 Tw /F5 10 Tf (sorry) Tj /F1 10 Tf (, no Mathlib dependency \227 ) Tj /F3 10 Tf (~1,280\327 faster than the brute-force numerical search) Tj /F1 10 Tf ( it replaced once) Tj T* 0 Tw 2.035223 Tw (the symbolic rewriter was written \(see \2478.6 for the full six-row comparison\), and carrying the additional) Tj T* 0 Tw (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 325.8236 cm +1 0 0 1 57.02362 155.0236 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 305.8236 cm +1 0 0 1 57.02362 135.0236 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 251.8236 cm +1 0 0 1 57.02362 81.02362 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 221.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 191.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 161.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 107.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 endstream endobj 154 0 obj << -/Length 4694 +/Length 6464 >> stream 1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET q -1 0 0 1 57.02362 751.8236 cm +1 0 0 1 57.02362 741.0236 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 711.0236 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 681.0236 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 627.0236 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 595.8236 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 731.8236 cm +1 0 0 1 57.02362 575.8236 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 725.8236 cm +1 0 0 1 57.02362 569.8236 cm Q q -1 0 0 1 57.02362 587.8236 cm +1 0 0 1 57.02362 431.8236 cm q 1 1 1 rg n 0 138 481.2283 -18 re f* @@ -8740,25 +8749,25 @@ Q Q Q q -1 0 0 1 57.02362 587.8236 cm +1 0 0 1 57.02362 431.8236 cm Q q -1 0 0 1 57.02362 533.8236 cm +1 0 0 1 57.02362 377.8236 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 502.6236 cm +1 0 0 1 57.02362 346.6236 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 488.6236 cm +1 0 0 1 57.02362 332.6236 cm Q q -1 0 0 1 57.02362 476.6236 cm +1 0 0 1 57.02362 320.6236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -8774,16 +8783,16 @@ Q Q Q q -1 0 0 1 57.02362 476.6236 cm +1 0 0 1 57.02362 320.6236 cm Q q -1 0 0 1 57.02362 398.6236 cm +1 0 0 1 57.02362 242.6236 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 390.6236 cm +1 0 0 1 57.02362 234.6236 cm Q endstream @@ -12143,60 +12152,60 @@ xref 0002509558 00000 n 0002518581 00000 n 0002529268 00000 n -0002537647 00000 n -0002546348 00000 n -0002555824 00000 n -0002564629 00000 n -0002574831 00000 n -0002579578 00000 n -0002581413 00000 n -0002594869 00000 n -0002611528 00000 n -0002622036 00000 n -0002629495 00000 n -0002636169 00000 n -0002644231 00000 n -0002652167 00000 n -0002658635 00000 n -0002660791 00000 n -0002661869 00000 n -0002662273 00000 n -0002662308 00000 n -0002662343 00000 n -0002662378 00000 n -0002662413 00000 n -0002662448 00000 n -0002662483 00000 n -0002662518 00000 n -0002662553 00000 n -0002662588 00000 n -0002662624 00000 n -0002662660 00000 n -0002662696 00000 n -0002662732 00000 n -0002662768 00000 n -0002662804 00000 n -0002662840 00000 n -0002662876 00000 n -0002662912 00000 n -0002662948 00000 n -0002662984 00000 n -0002663020 00000 n -0002663056 00000 n -0002663092 00000 n -0002663128 00000 n -0002663164 00000 n -0002663200 00000 n -0002663236 00000 n -0002663272 00000 n -0002663308 00000 n -0002663344 00000 n -0002663380 00000 n -0002663416 00000 n +0002536885 00000 n +0002546473 00000 n +0002554309 00000 n +0002564586 00000 n +0002574527 00000 n +0002581044 00000 n +0002582879 00000 n +0002596335 00000 n +0002612994 00000 n +0002623502 00000 n +0002630961 00000 n +0002637635 00000 n +0002645697 00000 n +0002653633 00000 n +0002660101 00000 n +0002662257 00000 n +0002663335 00000 n +0002663739 00000 n +0002663774 00000 n +0002663809 00000 n +0002663844 00000 n +0002663879 00000 n +0002663914 00000 n +0002663949 00000 n +0002663984 00000 n +0002664019 00000 n +0002664054 00000 n +0002664090 00000 n +0002664126 00000 n +0002664162 00000 n +0002664198 00000 n +0002664234 00000 n +0002664270 00000 n +0002664306 00000 n +0002664342 00000 n +0002664378 00000 n +0002664414 00000 n +0002664450 00000 n +0002664486 00000 n +0002664522 00000 n +0002664558 00000 n +0002664594 00000 n +0002664630 00000 n +0002664666 00000 n +0002664702 00000 n +0002664738 00000 n +0002664774 00000 n +0002664810 00000 n +0002664846 00000 n +0002664882 00000 n trailer << /ID -[] +[<1d446ae1004a02d6f40b0a19c1f8b013><1d446ae1004a02d6f40b0a19c1f8b013>] % ReportLab generated PDF document -- digest (opensource) /Info 69 0 R @@ -12204,5 +12213,5 @@ trailer /Size 200 >> startxref -2663452 +2664918 %%EOF diff --git a/whitepaper/uncommonlisp-whitepaper.rst b/whitepaper/uncommonlisp-whitepaper.rst index 018a005..b2ae75f 100644 --- a/whitepaper/uncommonlisp-whitepaper.rst +++ b/whitepaper/uncommonlisp-whitepaper.rst @@ -786,6 +786,8 @@ Every non-builtin, non-closure binding round-trips. Closures and builtins are sk **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. + 7.5 Cross-Process Benchmarks ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^