russell@unturf.com
d88149a502
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.
349 lines
12 KiB
Text
349 lines
12 KiB
Text
;;; proof-netspace-server.lsp — a content-addressed proof cache over TCP.
|
||
;;;
|
||
;;; Clients send one of three verbs as a single S-expression:
|
||
;;;
|
||
;;; (<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.
|
||
;;;
|
||
;;; 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 (<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)
|