From 5ea687a888c2c7d3d1e9f1410eab149cc8323142 Mon Sep 17 00:00:00 2001 From: "russell@unturf.com" Date: Sat, 18 Apr 2026 05:29:23 -0400 Subject: [PATCH] =?UTF-8?q?proof=20netspace:=202-node=20spiral=20demo=20?= =?UTF-8?q?=E2=80=94=20independent=20caches=20converge?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Extracts the 300-line server body into proof-netspace-server-lib.lsp so multi-node demos can share it without duplication. The existing proof-netspace-server.lsp entry point stays stable — now a 25-line config wrapper that sets defaults and loads the lib. New 2-node scaffolding: proof-netspace-node-a.lsp — port 9086, cache /tmp/lumbda-A-* proof-netspace-node-b.lsp — port 9087, cache /tmp/lumbda-B-* spiral-client.lsp — drives both nodes, seeds them with partially-overlapping theorem sets, runs one A→B and one B→A envelope round-trip, reports sizes spiral-demo.sh — orchestrator: starts both nodes, runs client, tears down cleanly. Accepts python|c|asm — all three converge identically (A=3 B=3 → A=5 B=5). Proves the envelope primitive at use-case scale: N independent caches mesh-converge in O(N) spiral passes. Foundation for the "looping and spiraling across time and space of manifolds" runtime topology. --- examples/proof-netspace-node-a.lsp | 12 + examples/proof-netspace-node-b.lsp | 10 + examples/proof-netspace-server-lib.lsp | 315 +++++++++++++++++++++++ examples/proof-netspace-server.lsp | 339 +------------------------ examples/spiral-client.lsp | 113 +++++++++ examples/spiral-demo.sh | 75 ++++++ 6 files changed, 533 insertions(+), 331 deletions(-) create mode 100644 examples/proof-netspace-node-a.lsp create mode 100644 examples/proof-netspace-node-b.lsp create mode 100644 examples/proof-netspace-server-lib.lsp create mode 100644 examples/spiral-client.lsp create mode 100755 examples/spiral-demo.sh diff --git a/examples/proof-netspace-node-a.lsp b/examples/proof-netspace-node-a.lsp new file mode 100644 index 0000000..31df07a --- /dev/null +++ b/examples/proof-netspace-node-a.lsp @@ -0,0 +1,12 @@ +;;; proof-netspace-node-a.lsp — node A of the 2-node spiral demo. +;;; +;;; Port 9086, cache paths under /tmp/lumbda-A-*. Run in parallel with +;;; proof-netspace-node-b.lsp (port 9087) and drive both via the +;;; spiral-client.lsp to watch independent caches converge. + +(define *port* 9086) +(define *max-requests* 10000) +(define *snapshot-path* "/tmp/lumbda-A-db.sexp") +(define *proofs-dir* "/tmp/lumbda-A-proofs/") + +(load "examples/proof-netspace-server-lib.lsp") diff --git a/examples/proof-netspace-node-b.lsp b/examples/proof-netspace-node-b.lsp new file mode 100644 index 0000000..a06abd2 --- /dev/null +++ b/examples/proof-netspace-node-b.lsp @@ -0,0 +1,10 @@ +;;; proof-netspace-node-b.lsp — node B of the 2-node spiral demo. +;;; +;;; Port 9087, cache paths under /tmp/lumbda-B-*. See node-a for context. + +(define *port* 9087) +(define *max-requests* 10000) +(define *snapshot-path* "/tmp/lumbda-B-db.sexp") +(define *proofs-dir* "/tmp/lumbda-B-proofs/") + +(load "examples/proof-netspace-server-lib.lsp") diff --git a/examples/proof-netspace-server-lib.lsp b/examples/proof-netspace-server-lib.lsp new file mode 100644 index 0000000..cefb66b --- /dev/null +++ b/examples/proof-netspace-server-lib.lsp @@ -0,0 +1,315 @@ +;;; proof-netspace-server-lib.lsp — shared server body. +;;; +;;; Expected pre-bound top-level variables (set by the wrapper script +;;; that loads this file): +;;; +;;; *port* — TCP port to listen on +;;; *max-requests* — request cap before clean shutdown +;;; *snapshot-path* — filesystem path for the bulk-load snapshot +;;; *proofs-dir* — directory for per-proof cache artifacts +;;; +;;; Wrappers: proof-netspace-server.lsp (defaults), proof-netspace-node-a.lsp, +;;; proof-netspace-node-b.lsp. + +;;; ─── 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. + +(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) + (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) + (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 ─────────────────────────────────────── +;;; +;;; 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 (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) + (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 + ((and (pair? form) (eqv? (car form) 'envelope) (null? (cdr form))) + (envelope-reply)) + ((and (pair? form) (eqv? (car form) 'merge) (pair? (cdr form))) + (merge-reply (car (cdr form)))) + ((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*)) + +(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)) + (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) diff --git a/examples/proof-netspace-server.lsp b/examples/proof-netspace-server.lsp index a976664..9e15ee2 100644 --- a/examples/proof-netspace-server.lsp +++ b/examples/proof-netspace-server.lsp @@ -1,349 +1,26 @@ -;;; proof-netspace-server.lsp — a content-addressed proof cache over TCP. +;;; proof-netspace-server.lsp — default-config wrapper for the netspace server. ;;; -;;; Clients send one of three verbs as a single S-expression: +;;; Serves a content-addressed proof cache over TCP. Three verbs: ;;; ;;; ( ) — 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. +;;; Three cache layers: in-memory hash-set → per-proof file → portal snapshot. +;;; 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 +;;; +;;; For multi-node demos see proof-netspace-node-{a,b}.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) +(load "examples/proof-netspace-server-lib.lsp") diff --git a/examples/spiral-client.lsp b/examples/spiral-client.lsp new file mode 100644 index 0000000..99e9a10 --- /dev/null +++ b/examples/spiral-client.lsp @@ -0,0 +1,113 @@ +;;; spiral-client.lsp — demonstrate envelope teleport across two nodes. +;;; +;;; Flow: +;;; 1. Seed node A with EML theorems 1..3 +;;; 2. Seed node B with EML theorems 3..5 (theorem 3 overlaps) +;;; 3. Pre-spiral: A has 3 hashes, B has 3 hashes, 1 in common +;;; 4. Spiral A→B: B pulls A's envelope and merges +;;; 5. Spiral B→A: A pulls B's envelope and merges +;;; 6. Post-spiral: both nodes hold the union (5 unique hashes each) +;;; +;;; Proves that independent caches converge with one round-trip per +;;; direction. N nodes in a mesh converge after N-1 spiral passes. +;;; +;;; Usage (start both nodes first): +;;; python3 uncommonlisp.py --fast examples/spiral-client.lsp + +(define *host* "127.0.0.1") +(define *port-a* 9086) +(define *port-b* 9087) + +;;; ─── Canonical serializer ────────────────────────────────── + +(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)))))) + +;;; ─── Wire helpers ────────────────────────────────────────── + +(define (request port 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"))) + +(define (prove port lhs rhs) + (request port + (string-append "(" (atom->string lhs) " " (atom->string rhs) ")"))) + +(define (parse-envelope resp) + (let ((form (read-from-string resp))) + (if (and (pair? form) (eqv? (car form) 'envelope) (pair? (cdr form))) + (car (cdr form)) + '()))) + +(define (count-list form n) + (if (pair? form) (count-list (cdr form) (+ n 1)) n)) + +(define (envelope-of port) + (parse-envelope (request port "(envelope)"))) + +(define (hashes->string lst acc) + (if (null? lst) acc + (hashes->string (cdr lst) + (string-append acc (number->string (car lst)) " ")))) + +(define (merge-into port hashes) + (request port + (string-append "(merge (" (hashes->string hashes "") "))"))) + +;;; ─── Report helpers ──────────────────────────────────────── + +(define (report-sizes label) + (let ((a (envelope-of *port-a*)) + (b (envelope-of *port-b*))) + (display label) + (display " A=") (display (count-list a 0)) + (display " B=") (display (count-list b 0)) (newline))) + +;;; ─── Run ─────────────────────────────────────────────────── + +(display "spiral demo across nodes A:") (display *port-a*) +(display " and B:") (display *port-b*) (newline) +(newline) + +(display "seeding node A (theorems 1..3)") (newline) +(prove *port-a* '(eml ?x 1) '(exp ?x)) +(prove *port-a* '(eml 1 1) '(exp 1)) +(prove *port-a* '(eml 1 (eml (eml 1 ?x) 1)) '(ln ?x)) + +(display "seeding node B (theorems 3..5 — overlap on #3)") (newline) +(prove *port-b* '(eml 1 (eml (eml 1 ?x) 1)) '(ln ?x)) +(prove *port-b* '(eml 1 (eml (eml 1 1) 1)) 0) +(prove *port-b* '(eml (ln ?a) (exp ?b)) '(- ?a ?b)) +(newline) + +(report-sizes "pre-spiral ") + +(display "spiral A → B (B pulls A's envelope and merges)") (newline) +(display " B: ") (display (merge-into *port-b* (envelope-of *port-a*))) + +(display "spiral B → A (A pulls B's envelope and merges)") (newline) +(display " A: ") (display (merge-into *port-a* (envelope-of *port-b*))) +(newline) + +(report-sizes "post-spiral ") +(newline) + +(display "done") (newline) diff --git a/examples/spiral-demo.sh b/examples/spiral-demo.sh new file mode 100755 index 0000000..591ebc3 --- /dev/null +++ b/examples/spiral-demo.sh @@ -0,0 +1,75 @@ +#!/bin/bash +# spiral-demo.sh — 2-node envelope teleport demonstration. +# +# Launches two independent netspace servers on ports 9086 and 9087 with +# independent cache directories, runs the spiral client to drive one +# round-trip of envelope exchange in each direction, and tears down. +# +# Usage: bash examples/spiral-demo.sh [impl] +# impl: python (default) | c | asm +# +# The implementation choice governs BOTH servers and the client. +# Any combination works at the protocol level; the script uses the +# same binary to keep the demo self-consistent. + +set -e +ulimit -v 524288 +trap 'pkill -9 -u "$USER" -f "proof-netspace-node|spiral-client" 2>/dev/null || true' EXIT INT TERM + +IMPL="${1:-python}" + +case "$IMPL" in + python) BIN="python3 uncommonlisp.py --fast" ;; + c) BIN="./c/uncommonlisp --fast" ;; + asm) BIN="asm/uncommonlisp" ;; + *) echo "unknown impl: $IMPL (expected python|c|asm)"; exit 1 ;; +esac + +# Fresh state — no preloaded caches from prior runs +rm -rf /tmp/lumbda-A-db.sexp /tmp/lumbda-A-proofs +rm -rf /tmp/lumbda-B-db.sexp /tmp/lumbda-B-proofs +mkdir -p /tmp/lumbda-A-proofs /tmp/lumbda-B-proofs + +echo "=== spiral demo ($IMPL) ===" + +# Start both nodes +if [ "$IMPL" = "asm" ]; then + timeout 25 $BIN < examples/proof-netspace-node-a.lsp > /tmp/spiral-a.log 2>&1 & + SPID_A=$! + timeout 25 $BIN < examples/proof-netspace-node-b.lsp > /tmp/spiral-b.log 2>&1 & + SPID_B=$! +else + timeout 25 $BIN examples/proof-netspace-node-a.lsp > /tmp/spiral-a.log 2>&1 & + SPID_A=$! + timeout 25 $BIN examples/proof-netspace-node-b.lsp > /tmp/spiral-b.log 2>&1 & + SPID_B=$! +fi + +sleep 3 + +# Run spiral client +if [ "$IMPL" = "asm" ]; then + timeout 15 $BIN < examples/spiral-client.lsp +else + timeout 15 $BIN examples/spiral-client.lsp +fi + +# Tear down +kill -TERM $SPID_A $SPID_B 2>/dev/null || true +sleep 1 +kill -9 $SPID_A $SPID_B 2>/dev/null || true +wait $SPID_A 2>/dev/null || true +wait $SPID_B 2>/dev/null || true + +echo +echo "=== node A log ===" +head -1 /tmp/spiral-a.log +echo "=== node B log ===" +head -1 /tmp/spiral-b.log + +# Verify no stragglers +if pgrep -u "$USER" -f 'proof-netspace-node|spiral-client' > /dev/null; then + echo "STRAGGLER — check pgrep manually" + exit 1 +fi +echo "clean"