From d88149a5022d17aced8941995d5da3dcd54e42e8 Mon Sep 17 00:00:00 2001 From: "russell@unturf.com" Date: Fri, 17 Apr 2026 21:36:26 -0400 Subject: [PATCH] proof netspace: envelope teleport + portable hash-table on vectors MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Extends proof-netspace RPC with two verbs that let peers exchange the full solution space in one round-trip: (envelope) → reply (envelope (h1 h2 ...)) (merge (h1 h2 ...)) → fold hashes into local DB, reply (merged N) Any node can now bootstrap from a peer's cache instead of re-verifying every theorem locally. Two nodes that swap envelopes both become supersets of what either knew — the primitive for mesh-wide spiral. *proof-db* swapped from linear alist to a hash-set. O(N·M) merge drops to O(M). The hash-table is a ~20-line pure-Lumbda library over make-vector / vector-ref / vector-set! — runs unmodified in all three tiers. No asm hash-table primitive needed. Also fixes a pre-existing asm defect: bi_makevec clobbered %rax via the GETARG macro's internal scratch use, causing SIGSEGV on every (make-vector N fill) call. The bug shipped because asm/test.sh only covered the variadic (vector ...) constructor; tests/functional.lsp had one make-vector assert but was never wired into asm's harness. Added five make-vector assertions to asm/test.sh (132 → 137). Portal snapshot rewritten to emit (set! *proof-db* ...) so the top-level binding is actually mutated on restart — previous (define ...) form bound locally on some code paths, leaving the in-memory DB empty after load. Verified: make test-all green (137 asm + 189 functional + Python/C tests), 3-tier matrix cold+warm+restart all clean. --- asm/test.sh | 5 + asm/uncommonlisp | Bin 46544 -> 46544 bytes asm/uncommonlisp.o | Bin 45872 -> 45872 bytes asm/uncommonlisp.s | 22 +- examples/proof-netspace-client.lsp | 123 ++++++++++ examples/proof-netspace-server.lsp | 349 +++++++++++++++++++++++++++++ 6 files changed, 489 insertions(+), 10 deletions(-) create mode 100644 examples/proof-netspace-client.lsp create mode 100644 examples/proof-netspace-server.lsp diff --git a/asm/test.sh b/asm/test.sh index 03cc01f..63dd214 100644 --- a/asm/test.sh +++ b/asm/test.sh @@ -160,6 +160,11 @@ check "vec-len" "(vector-length (vector 1 2 3))" "3" check "vec?" "(vector? (vector 1))" "#t" check "vec?-f" "(vector? 42)" "#f" check "vec-set" "(let ((v (vector 1 2 3))) (vector-set! v 1 99) (vector-ref v 1))" "99" +check "makevec" "(vector-ref (make-vector 3 0) 1)" "0" +check "makevec-len" "(vector-length (make-vector 5 42))" "5" +check "makevec-fill" "(vector-ref (make-vector 4 7) 2)" "7" +check "makevec-mut" "(let ((v (make-vector 3 0))) (vector-set! v 1 99) (vector-ref v 1))" "99" +check "makevec-big" "(vector-length (make-vector 1021 0))" "1021" # ─── FUNCTIONAL TESTS: real programs ───────────────────── diff --git a/asm/uncommonlisp b/asm/uncommonlisp index 812b609a48bb9dda8a36bab11ba62a5d92aab3ed..9c535263ed8a618c7265c66a69e2b2b9517c4581 100755 GIT binary patch delta 88 zcmV-e0H^=Z>jKd00jKd00py*1Z4JbEiQJUXv=w0!9IDRwD4wTjidgOGt?PSK&%vq%gC^D^TTp~YXB{3AgTZW diff --git a/asm/uncommonlisp.s b/asm/uncommonlisp.s index 6c8001b..99d86b7 100644 --- a/asm/uncommonlisp.s +++ b/asm/uncommonlisp.s @@ -3738,15 +3738,18 @@ bi_vector: RET_VAL bi_makevec: + # (make-vector n fill) — allocate n-slot vector filled with `fill`. + # GETARG uses %rax as scratch, so we MUST stash the length in a + # callee-safe register before consuming the second arg. GETARG %rax - sarq $3, %rax # n - GETARG %rcx # fill value (or default 0) - movq %r15, %rdx # vector obj - movq %rax, (%r15) # length - leaq 8(%r15,%rax,8), %r15 - # Fill - leaq 8(%rdx), %rdi - movq (%rdx), %rsi # count + sarq $3, %rax # n (untagged) + movq %rax, %rdx # save n in %rdx — survives next GETARG + GETARG %rcx # fill value (tagged) + movq %r15, %rax # vector obj pointer + movq %rdx, (%r15) # store length + leaq 8(%r15,%rdx,8), %r15 # advance heap past length + n*8 bytes + leaq 8(%rax), %rdi # elements start + movq %rdx, %rsi # count = n .bmv_fill: testq %rsi, %rsi jz .bmv_done @@ -3755,8 +3758,7 @@ bi_makevec: decq %rsi jmp .bmv_fill .bmv_done: - movq %rdx, %rax - orq $7, %rax + orq $7, %rax # tag as vector RET_VAL bi_vecref: diff --git a/examples/proof-netspace-client.lsp b/examples/proof-netspace-client.lsp new file mode 100644 index 0000000..b3974ad --- /dev/null +++ b/examples/proof-netspace-client.lsp @@ -0,0 +1,123 @@ +;;; proof-netspace-client.lsp — query the proof netspace server. +;;; +;;; Three passes: +;;; +;;; 1. Verify each of five EML theorems per-proof (PROVEN / UNKNOWN). +;;; 2. Fetch the whole envelope — the server's full solution space +;;; ships back in one round-trip as (envelope (h1 h2 ...)). +;;; 3. Merge our own envelope back + one synthetic hash. Server +;;; reports (merged 1) proving the synthetic was the only new +;;; entry and the rest were already known. +;;; +;;; Two nodes can chain (envelope) + (merge ...) in either direction +;;; until both hold the union of what either knew. +;;; +;;; Usage (start the server first): +;;; python3 uncommonlisp.py --fast examples/proof-netspace-client.lsp +;;; ./c/uncommonlisp examples/proof-netspace-client.lsp +;;; ./asm/uncommonlisp < examples/proof-netspace-client.lsp + +(define *host* "127.0.0.1") +(define *port* 9086) + +;;; ─── Canonical serializer (matches server) ───────────────── + +(define (atom->string v) + (cond + ((number? v) (number->string v)) + ((symbol? v) (symbol->string v)) + ((null? v) "()") + ((pair? v) (string-append "(" (list->str v) ")")) + (else "?"))) + +(define (list->str lst) + (cond + ((null? lst) "") + ((null? (cdr lst)) (atom->string (car lst))) + (else (string-append (atom->string (car lst)) " " + (list->str (cdr lst)))))) + +;;; ─── One-shot TCP round-trip ─────────────────────────────── + +(define (request str) + (let ((sock (tcp-connect *host* *port*))) + (if sock + (begin + (tcp-send sock str) + (let ((resp (tcp-recv sock 65536))) + (tcp-close sock) + (if resp resp "NO-RESPONSE"))) + "NO-CONNECT"))) + +;;; ─── Per-proof verification ──────────────────────────────── + +(define (ask lhs rhs) + (request (string-append "(" (atom->string lhs) " " + (atom->string rhs) ")"))) + +(define (probe name lhs rhs) + (let ((t0 (current-time-ms))) + (let ((resp (ask lhs rhs))) + (let ((t1 (current-time-ms))) + (display name) (display ": ") + (display (- t1 t0)) (display " ms ") + (display resp))))) + +;;; ─── Envelope teleport ───────────────────────────────────── + +(define (count-items form n) + ;; Return length of a list form; used to count hashes in envelope. + (if (pair? form) (count-items (cdr form) (+ n 1)) n)) + +(define (parse-envelope resp) + ;; resp = "(envelope (h1 h2 ...))\n" — return the inner list. + (let ((form (read-from-string resp))) + (if (and (pair? form) (eqv? (car form) 'envelope) (pair? (cdr form))) + (car (cdr form)) + '()))) + +(define (hashes->string lst acc) + (if (null? lst) acc + (hashes->string (cdr lst) + (string-append acc (number->string (car lst)) " ")))) + +(define (fetch-envelope) + (let ((t0 (current-time-ms))) + (let ((resp (request "(envelope)"))) + (let ((t1 (current-time-ms))) + (display "envelope : ") (display (- t1 t0)) (display " ms ") + (let ((hashes (parse-envelope resp))) + (display (count-items hashes 0)) + (display " hashes teleported") (newline) + hashes))))) + +(define (merge-envelope hashes synthetic) + ;; Send the server its own envelope back plus one synthetic hash. + ;; Expected reply: (merged 1) — only the synthetic was new. + (let ((t0 (current-time-ms))) + (let ((payload (string-append "(merge (" + (hashes->string hashes "") + (number->string synthetic) "))"))) + (let ((resp (request payload))) + (let ((t1 (current-time-ms))) + (display "merge : ") (display (- t1 t0)) (display " ms ") + (display resp)))))) + +;;; ─── Run ─────────────────────────────────────────────────── + +(display "querying proof netspace at ") (display *host*) (display ":") +(display *port*) (newline) +(newline) + +(probe "eml_is_exp " '(eml ?x 1) '(exp ?x)) +(probe "eml_is_e " '(eml 1 1) '(exp 1)) +(probe "eml_is_ln " '(eml 1 (eml (eml 1 ?x) 1)) '(ln ?x)) +(probe "eml_is_zero " '(eml 1 (eml (eml 1 1) 1)) 0) +(probe "eml_is_sub " '(eml (ln ?a) (exp ?b)) '(- ?a ?b)) +(newline) + +(define env (fetch-envelope)) +(merge-envelope env 999999999) +(newline) + +(display "done") (newline) diff --git a/examples/proof-netspace-server.lsp b/examples/proof-netspace-server.lsp new file mode 100644 index 0000000..a976664 --- /dev/null +++ b/examples/proof-netspace-server.lsp @@ -0,0 +1,349 @@ +;;; proof-netspace-server.lsp — a content-addressed proof cache over TCP. +;;; +;;; Clients send one of three verbs as a single S-expression: +;;; +;;; ( ) — verify a theorem, reply PROVEN/UNKNOWN/ERROR +;;; (envelope) — reply with whole DB as (envelope (h1 h2 ...)) +;;; (merge (h1 h2 ...)) — fold hashes into local DB, reply (merged ) +;;; +;;; Three layers of cache before falling through to local verification: +;;; +;;; 1. in-memory alist — fastest +;;; 2. per-proof file — survives restart, /tmp/lumbda-proofs/.proof +;;; 3. portal snapshot — /tmp/lumbda-proof-db.sexp, bulk load on startup +;;; +;;; Two peers can teleport whole solution spaces by chaining envelope + +;;; merge in either direction. Both become supersets of what either knew. +;;; +;;; Portable across Python, C, and asm. Example: +;;; +;;; python3 uncommonlisp.py --fast examples/proof-netspace-server.lsp +;;; ./c/uncommonlisp --fast examples/proof-netspace-server.lsp +;;; ./asm/uncommonlisp < examples/proof-netspace-server.lsp + +(define *port* 9086) +(define *max-requests* 10000) +(define *snapshot-path* "/tmp/lumbda-proof-db.sexp") +(define *proofs-dir* "/tmp/lumbda-proofs/") + +;;; ─── Tiny content hash (djb2, 31-bit) ────────────────────── + +(define (hash-string s) + (define len (string-length s)) + (define (iter i h) + (if (= i len) + h + (iter (+ i 1) + (modulo (+ (* h 33) (char->integer (string-ref s i))) + 2147483647)))) + (iter 0 5381)) + +;;; ─── Serialize a theorem to a canonical string ───────────── + +(define (atom->string v) + (cond + ((number? v) (number->string v)) + ((symbol? v) (symbol->string v)) + ((null? v) "()") + ((pair? v) (string-append "(" (list->str v) ")")) + ((string? v) (string-append "\"" v "\"")) + (else "?"))) + +(define (list->str lst) + (cond + ((null? lst) "") + ((null? (cdr lst)) (atom->string (car lst))) + (else (string-append (atom->string (car lst)) " " + (list->str (cdr lst)))))) + +(define (theorem->string lhs rhs) + (string-append (atom->string lhs) "=" (atom->string rhs))) + +;;; ─── Term-rewriting engine (same axioms as EML proof) ────── + +(define (pattern-var? x) + (if (symbol? x) + (let ((s (symbol->string x))) + (if (> (string-length s) 0) + (= (char->integer (string-ref s 0)) 63) ; '?' = 63 + #f)) + #f)) + +(define (sub-lookup var subs) + (if (null? subs) #f + (if (eqv? (car (car subs)) var) (car subs) + (sub-lookup var (cdr subs))))) + +(define (term-equal? a b) + (cond + ((and (pair? a) (pair? b)) + (if (term-equal? (car a) (car b)) (term-equal? (cdr a) (cdr b)) #f)) + ((and (null? a) (null? b)) #t) + (else (equal? a b)))) + +(define (match-pat pat term subs) + (cond + ((eqv? subs 'no-match) 'no-match) + ((pattern-var? pat) + (let ((existing (sub-lookup pat subs))) + (if existing + (if (term-equal? (cdr existing) term) subs 'no-match) + (cons (cons pat term) subs)))) + ((and (pair? pat) (pair? term)) + (match-pat (cdr pat) (cdr term) + (match-pat (car pat) (car term) subs))) + ((and (null? pat) (null? term)) subs) + ((term-equal? pat term) subs) + (else 'no-match))) + +(define (subst template subs) + (cond + ((pattern-var? template) + (let ((found (sub-lookup template subs))) + (if found (cdr found) template))) + ((pair? template) + (cons (subst (car template) subs) (subst (cdr template) subs))) + (else template))) + +(define (try-rule rule term) + (let ((pat (car rule)) (rhs (car (cdr (cdr rule))))) + (let ((subs (match-pat pat term '()))) + (if (eqv? subs 'no-match) #f (subst rhs subs))))) + +(define (step-root rules term) + (cond + ((null? rules) #f) + ((try-rule (car rules) term) (try-rule (car rules) term)) + (else (step-root (cdr rules) term)))) + +(define (step-any rules term) + (if (pair? term) + (let ((car-step (step-any rules (car term)))) + (if car-step + (cons car-step (cdr term)) + (let ((cdr-step (step-any rules (cdr term)))) + (if cdr-step (cons (car term) cdr-step) + (step-root rules term))))) + (step-root rules term))) + +(define (normalize rules term) + (define (iter t n) + (if (> n 500) t + (let ((next (step-any rules t))) + (if next (iter next (+ n 1)) t)))) + (iter term 0)) + +(define eml-rules + (list + '((eml ?x ?y) -> (- (exp ?x) (ln ?y))) + '((exp (ln ?x)) -> ?x) + '((ln (exp ?x)) -> ?x) + '((ln 1) -> 0) + '((- ?x 0) -> ?x) + '((- 0 ?x) -> (neg ?x)) + '((neg (neg ?x)) -> ?x) + '((- ?x ?x) -> 0) + '((- ?a (- ?a ?b)) -> ?b))) + +(define (verify lhs rhs) + (term-equal? (normalize eml-rules lhs) (normalize eml-rules rhs))) + +;;; ─── Hash-table library (pure Lumbda, portable) ─────────── +;;; +;;; Asm has no native hash-table primitive, but exposes make-vector, +;;; vector-ref, and vector-set! — the substrate a hash-table needs. +;;; This library builds a hash-SET keyed by integer on top of vectors: +;;; +;;; slot 0 = bucket count N +;;; slots 1..N = bucket list (chained alist of raw integer keys) +;;; +;;; Lookup and insert are O(1) expected. No resize: pick a bucket +;;; count large enough to keep load factor below ~10 at target scale. +;;; 1021 buckets keeps lookups fast through 10k entries. +;;; +;;; All operations use only primitives available on every tier: +;;; make-vector, vector-ref, vector-set!, modulo, cons, car, cdr. + +(define *ht-buckets* 1021) + +(define (ht-make n) + (let ((v (make-vector (+ n 1) '()))) + (vector-set! v 0 n) + v)) + +(define (ht-bucket t k) + (+ 1 (modulo (if (< k 0) (- 0 k) k) (vector-ref t 0)))) + +(define (ht-in-bucket? bucket k) + (cond + ((null? bucket) #f) + ((= (car bucket) k) #t) + (else (ht-in-bucket? (cdr bucket) k)))) + +(define (ht-has? t k) + (ht-in-bucket? (vector-ref t (ht-bucket t k)) k)) + +(define (ht-add! t k) + ;; returns #t if new, #f if already present + (let ((idx (ht-bucket t k))) + (let ((bucket (vector-ref t idx))) + (if (ht-in-bucket? bucket k) #f + (begin (vector-set! t idx (cons k bucket)) #t))))) + +(define (ht-size t) + (define n (vector-ref t 0)) + (define (blen lst) + (if (null? lst) 0 (+ 1 (blen (cdr lst))))) + (define (walk i acc) + (if (> i n) acc + (walk (+ i 1) (+ acc (blen (vector-ref t i)))))) + (walk 1 0)) + +(define (ht-fold-keys t acc fn) + (define n (vector-ref t 0)) + (define (bfold lst acc) + (if (null? lst) acc + (bfold (cdr lst) (fn (car lst) acc)))) + (define (walk i acc) + (if (> i n) acc + (walk (+ i 1) (bfold (vector-ref t i) acc)))) + (walk 1 acc)) + +;;; ─── Proof DB (hash-set backed by ht-*) ──────────────────── + +(define *proof-db* (ht-make *ht-buckets*)) + +(define (db-has? h) (ht-has? *proof-db* h)) +(define (db-add! h) (ht-add! *proof-db* h)) +(define (db-size) (ht-size *proof-db*)) + +(define (rebuild-db-from-list hashes) + ;; Used by portal-restore — builds a fresh table from a flat hash list. + (let ((t (ht-make *ht-buckets*))) + (define (walk lst) + (if (null? lst) t + (begin (ht-add! t (car lst)) (walk (cdr lst))))) + (walk hashes))) + +;;; ─── Per-proof file ──────────────────────────────────────── + +(define (proof-file-path h) + (string-append *proofs-dir* (number->string h) ".proof")) + +(define (file-has? h) + (if (file->string (proof-file-path h)) #t #f)) + +(define (file-add! h canon) + (write-file (proof-file-path h) + (string-append ";; proof artifact for hash " (number->string h) "\n" + ";; " canon "\n" "PROVEN\n"))) + +;;; ─── Portal snapshot of the DB (bulk transfer) ───────────── +;;; +;;; Snapshot emits a `set!` form (not `define`). When the loader calls +;;; (load ...), the top-level *proof-db* binding gets mutated in place +;;; regardless of whether `load` executes in a nested scope. `define` in +;;; a loaded file may introduce a local binding; `set!` always touches +;;; the lexically-enclosing top-level one. + +(define (portal-snapshot!) + (let ((hashes-str + (ht-fold-keys *proof-db* "" + (lambda (h acc) + (string-append acc (number->string h) " "))))) + (write-file *snapshot-path* + (string-append ";; lumbda proof netspace snapshot\n" + "(set! *proof-db* (rebuild-db-from-list '(" + hashes-str ")))\n")))) + +(define (portal-restore!) + (if (file->string *snapshot-path*) + (load *snapshot-path*) + #f)) + +;;; ─── Envelope teleport ───────────────────────────────────── +;;; +;;; Envelope = the full solution space as a list of hashes. Two nodes +;;; can exchange envelopes and each merges what it didn't know. After +;;; one round-trip, both hold the union. After N rounds across M nodes, +;;; the entire mesh converges on the same solution space. + +(define (envelope-reply) + (let ((hashes-str + (ht-fold-keys *proof-db* "" + (lambda (h acc) + (string-append acc (number->string h) " "))))) + (string-append "(envelope (" hashes-str "))\n"))) + +(define (merge-hashes lst added) + ;; Fold a flat list of hashes into *proof-db*; return count newly added. + ;; O(M) expected — each ht-add! is O(1) with well-distributed keys. + (if (null? lst) added + (if (ht-add! *proof-db* (car lst)) + (merge-hashes (cdr lst) (+ added 1)) + (merge-hashes (cdr lst) added)))) + +(define (merge-reply lst) + (let ((added (merge-hashes lst 0))) + (string-append "(merged " (number->string added) ")\n"))) + +;;; ─── Request handling ────────────────────────────────────── + +(define (verify-reply lhs rhs) + (let ((h (hash-string (theorem->string lhs rhs)))) + (cond + ((db-has? h) "PROVEN\n") + ((file-has? h) + (db-add! h) + "PROVEN\n") + ((verify lhs rhs) + (db-add! h) + (file-add! h (theorem->string lhs rhs)) + "PROVEN\n") + (else "UNKNOWN\n")))) + +(define (handle-request raw) + (let ((form (read-from-string raw))) + (cond + ;; (envelope) — return entire DB + ((and (pair? form) (eqv? (car form) 'envelope) (null? (cdr form))) + (envelope-reply)) + ;; (merge ( ...)) — fold hashes into DB + ((and (pair? form) (eqv? (car form) 'merge) (pair? (cdr form))) + (merge-reply (car (cdr form)))) + ;; ( ) — verify a theorem + ((and (pair? form) (pair? (cdr form))) + (verify-reply (car form) (car (cdr form)))) + (else "ERROR\n")))) + +;;; ─── Main loop ───────────────────────────────────────────── + +(portal-restore!) + +(define server (tcp-listen *port*)) + +;; No heap-snapshot here — this server mutates *proof-db* via set! and +;; writes cons cells that must outlive a request. Rewinding the heap +;; would invalidate the DB. Rely on *max-requests* + per-request +;; allocations being small. 10k requests × ~4 KB = ~40 MB, well inside +;; the 64 MB asm heap before heap_grow fires. + +(define (serve-loop n) + (if (>= n *max-requests*) + (begin (portal-snapshot!) + (display "request cap reached, snapshot saved\n") + (tcp-close server)) + (begin + (let ((client (tcp-accept server))) + (let ((req (tcp-recv client 8192))) + (if (and req (> (string-length req) 0)) + (tcp-send client (handle-request req)) + #f)) + (tcp-close client)) + ;; Portal-snapshot every 20 requests so crashes don't lose much + (if (= (modulo n 20) 0) (portal-snapshot!) #f) + (serve-loop (+ n 1))))) + +(display "proof-netspace-server on :") (display *port*) +(display " (") (display (db-size)) (display " proofs preloaded)") (newline) +(serve-loop 0)