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.
113 lines
3.9 KiB
Text
113 lines
3.9 KiB
Text
;;; 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)
|