lumbda/examples/proof-netspace-server.lsp
russell@unturf.com 5ea687a888 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.
2026-04-18 05:29:23 -04:00

26 lines
1.1 KiB
Text

;;; proof-netspace-server.lsp — default-config wrapper for the netspace server.
;;;
;;; 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 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/")
(load "examples/proof-netspace-server-lib.lsp")