;;; proof-netspace-server.lsp — default-config wrapper for the netspace server. ;;; ;;; Serves a content-addressed proof cache over TCP. Three verbs: ;;; ;;; ( ) — 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 ) ;;; ;;; 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 lumbda.py --fast examples/proof-netspace-server.lsp ;;; ./c/lumbda --fast examples/proof-netspace-server.lsp ;;; ./asm/lumbda < 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")