;;; 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)