russell@unturf.com
5ea687a888
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.
315 lines
10 KiB
Text
315 lines
10 KiB
Text
;;; 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)
|