proof netspace: 2-node spiral demo — independent caches converge
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.
This commit is contained in:
parent
d88149a502
commit
5ea687a888
6 changed files with 533 additions and 331 deletions
12
examples/proof-netspace-node-a.lsp
Normal file
12
examples/proof-netspace-node-a.lsp
Normal file
|
|
@ -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")
|
||||
10
examples/proof-netspace-node-b.lsp
Normal file
10
examples/proof-netspace-node-b.lsp
Normal file
|
|
@ -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")
|
||||
315
examples/proof-netspace-server-lib.lsp
Normal file
315
examples/proof-netspace-server-lib.lsp
Normal file
|
|
@ -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)
|
||||
|
|
@ -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:
|
||||
;;;
|
||||
;;; (<lhs> <rhs>) — 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 <n>)
|
||||
;;;
|
||||
;;; Three layers of cache before falling through to local verification:
|
||||
;;;
|
||||
;;; 1. in-memory alist — fastest
|
||||
;;; 2. per-proof file — survives restart, /tmp/lumbda-proofs/<hash>.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 (<hash> <hash> ...)) — fold hashes into DB
|
||||
((and (pair? form) (eqv? (car form) 'merge) (pair? (cdr form)))
|
||||
(merge-reply (car (cdr form))))
|
||||
;; (<lhs> <rhs>) — 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")
|
||||
|
|
|
|||
113
examples/spiral-client.lsp
Normal file
113
examples/spiral-client.lsp
Normal file
|
|
@ -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)
|
||||
75
examples/spiral-demo.sh
Executable file
75
examples/spiral-demo.sh
Executable file
|
|
@ -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"
|
||||
Loading…
Add table
Add a link
Reference in a new issue