rose-ash/sx/sx/plans/theorem-prover.sx

;; ---------------------------------------------------------------------------
;; Theorem Prover: prove.sx — Constraint Solving for SX Primitives
;; ---------------------------------------------------------------------------

;; Helper: render a Phase 1 result row
(defcomp ~plans/theorem-prover/prove-phase1-row (&key (name :as string) (status :as string))
  (tr :class "border-t border-stone-100"
    (td :class "py-1.5 px-3 font-mono text-xs text-stone-700" name)
    (td :class "py-1.5 px-3 text-xs"
      (if (= status "sat")
        (span :class "text-emerald-600 font-medium" "sat")
        (span :class "text-red-600 font-medium" status)))))

;; Helper: render a Phase 2 result row
(defcomp ~plans/theorem-prover/prove-phase2-row (&key (name :as string) (status :as string) (tested :as number) (skipped :as number) (counterexample :as string?))
  (tr :class "border-t border-stone-100"
    (td :class "py-1.5 px-3 font-mono text-xs text-stone-700" name)
    (td :class "py-1.5 px-3 text-xs"
      (if (= status "verified")
        (span :class "text-emerald-600 font-medium" "verified")
        (span :class "text-red-600 font-medium" "falsified")))
    (td :class "py-1.5 px-3 text-xs text-stone-500 text-right tabular-nums"
      (str tested))
    (td :class "py-1.5 px-3 text-xs text-stone-400 text-right tabular-nums"
      (str skipped))
    (td :class "py-1.5 px-3 text-xs font-mono text-red-600"
      (or counterexample ""))))


(defcomp ~plans/theorem-prover/plan-theorem-prover-content ()
  (~docs/page :title "Theorem Prover"

    ;; --- Intro ---
    (~docs/section :title "SX proves itself" :id "intro"
      (p :class "text-stone-600"
        (code "prove.sx") " is a constraint solver and property prover written in SX. It takes the SX specification (" (code "primitives.sx") "), translates it to formal logic via " (code "z3.sx") ", and proves properties about the result. Every step in the pipeline is an s-expression program operating on other s-expressions.")
      (p :class "text-stone-600"
        "Two proof modes. " (strong "Phase 1") " verifies that every primitive definition is satisfiable " (em "by construction") " — the definition is the model. " (strong "Phase 2") " goes further: it states algebraic properties (commutativity, associativity, transitivity, bounds) and verifies them by " (em "bounded model checking") " — exhaustive evaluation over integer domains, searching for counterexamples.")
      (div :class "rounded border border-violet-200 bg-violet-50 p-4 mt-4"
        (p :class "text-sm text-violet-800 font-semibold mb-2" "Everything is SX")
        (p :class "text-sm text-violet-700"
          "No external solver. No Python proof logic. " (code "prove.sx") " is 400+ lines of s-expressions that parse SMT-LIB, evaluate expressions, generate test domains, compute cartesian products, search for counterexamples, and produce verification conditions. The same code would work client-side via the bootstrapped JavaScript evaluator.")))

    ;; --- Phase 1 Results ---
    (~docs/section :title "Phase 1: Definitional satisfiability" :id "phase1"
      (p :class "text-stone-600"
        "Every " (code "define-primitive") " with a " (code ":body") " produces a " (code "forall") " assertion in SMT-LIB. For example, " (code "(define-primitive \"inc\" :params (n) :body (+ n 1))") " becomes:")
      (~docs/code :src (highlight "; inc\n(declare-fun inc (Int) Int)\n(assert (forall (((n Int)))\n  (= (inc n) (+ n 1))))\n(check-sat)" "lisp"))
      (p :class "text-stone-600"
        "This is satisfiable by construction: define " (code "inc(n) = n + 1") " and the assertion holds. " (code "prove.sx") " verifies this mechanically for every primitive — it parses the SMT-LIB, extracts the definition, builds a model, and evaluates it with test values.")

      (div :class "rounded border border-emerald-200 bg-emerald-50 p-4 my-4"
        (p :class "text-sm font-semibold"
          (if phase1-all-sat
            (span :class "text-emerald-800" (str phase1-sat "/" phase1-total " primitives: all sat"))
            (span :class "text-red-800" (str phase1-sat "/" phase1-total " sat (some failed)"))))
        (p :class "text-xs text-emerald-700 mt-1"
          "Computed live in " (str phase1-ms) "ms"))

      (~docs/subsection :title "Results"
        (div :class "overflow-x-auto rounded border border-stone-200 max-h-64 overflow-y-auto"
          (table :class "w-full text-left"
            (thead
              (tr :class "bg-stone-100 sticky top-0"
                (th :class "py-2 px-3 text-xs text-stone-500 font-medium" "Primitive")
                (th :class "py-2 px-3 text-xs text-stone-500 font-medium" "Status")))
            (tbody
              (map (fn (r)
                (~plans/theorem-prover/prove-phase1-row
                  :name (get r "name")
                  :status (get r "status")))
                phase1-results))))))

    ;; --- Phase 2 Results ---
    (~docs/section :title "Phase 2: Algebraic properties" :id "phase2"
      (p :class "text-stone-600"
        "Phase 1 proves internal consistency. Phase 2 proves " (em "external properties") " — mathematical laws that should hold across all inputs. Each property is defined as a test function evaluated over a bounded integer domain.")
      (p :class "text-stone-600"
        "For arity 1, the domain is [-50, 50] (101 values). For arity 2, [-20, 20] (1,681 pairs). For arity 3, [-8, 8] (4,913 triples). Properties with preconditions (like " (code "clamp-in-range") " requiring " (code "(<= lo hi)") ") skip value combinations that don't satisfy the precondition.")

      (div :class "rounded border border-emerald-200 bg-emerald-50 p-4 my-4"
        (p :class "text-sm font-semibold"
          (if phase2-all-verified
            (span :class "text-emerald-800" (str phase2-verified "/" phase2-total " properties: all verified"))
            (span :class "text-red-800" (str phase2-verified "/" phase2-total " verified (" phase2-falsified " falsified)"))))
        (p :class "text-xs text-emerald-700 mt-1"
          (str phase2-total-tested " constraint evaluations in " phase2-ms "ms")))

      (~docs/subsection :title "Results"
        (div :class "overflow-x-auto rounded border border-stone-200 max-h-96 overflow-y-auto"
          (table :class "w-full text-left"
            (thead
              (tr :class "bg-stone-100 sticky top-0"
                (th :class "py-2 px-3 text-xs text-stone-500 font-medium" "Property")
                (th :class "py-2 px-3 text-xs text-stone-500 font-medium" "Status")
                (th :class "py-2 px-3 text-xs text-stone-500 font-medium text-right" "Tested")
                (th :class "py-2 px-3 text-xs text-stone-500 font-medium text-right" "Skipped")
                (th :class "py-2 px-3 text-xs text-stone-500 font-medium" "Counterexample")))
            (tbody
              (map (fn (r)
                (~plans/theorem-prover/prove-phase2-row
                  :name (get r "name")
                  :status (get r "status")
                  :tested (get r "tested")
                  :skipped (get r "skipped")
                  :counterexample (get r "counterexample" "")))
                phase2-results))))))

    ;; --- What the properties prove ---
    (~docs/section :title "What the properties prove" :id "properties"
      (p :class "text-stone-600"
        "34 properties across seven categories. Each encodes a mathematical law that the SX primitives must obey.")

      (div :class "space-y-4 mt-4"
        (div :class "rounded border border-stone-200 bg-stone-50 p-4"
          (p :class "text-sm font-semibold text-stone-800 mb-2" "Arithmetic")
          (p :class "text-sm text-stone-600"
            (code "(+ a b) = (+ b a)") " commutativity. "
            (code "(+ (+ a b) c) = (+ a (+ b c))") " associativity. "
            (code "(+ a 0) = a") " identity. "
            (code "(* a (+ b c)) = (+ (* a b) (* a c))") " distributive law. "
            "Same for " (code "*") " — commutative, associative, identity, zero annihilation. "
            (code "(- a a) = 0") " subtraction inverse. Nine properties, all verified."))

        (div :class "rounded border border-stone-200 bg-stone-50 p-4"
          (p :class "text-sm font-semibold text-stone-800 mb-2" "inc / dec")
          (p :class "text-sm text-stone-600"
            (code "(inc n) = (+ n 1)") " and " (code "(dec n) = (- n 1)") " — definitional relationships. "
            (code "(dec (inc n)) = n") " and " (code "(inc (dec n)) = n") " — mutual inverses. "
            "These confirm that " (code "inc") " and " (code "dec") " are exactly " (code "+1") " and " (code "-1") ", not off-by-one."))

        (div :class "rounded border border-stone-200 bg-stone-50 p-4"
          (p :class "text-sm font-semibold text-stone-800 mb-2" "abs")
          (p :class "text-sm text-stone-600"
            (code "(abs n) >= 0") " non-negativity. "
            (code "(abs (abs n)) = (abs n)") " idempotence. "
            (code "(abs n) = (abs (- 0 n))") " symmetry. "
            "Three properties that together characterize absolute value."))

        (div :class "rounded border border-stone-200 bg-stone-50 p-4"
          (p :class "text-sm font-semibold text-stone-800 mb-2" "Predicates")
          (p :class "text-sm text-stone-600"
            (code "(odd? n) = (not (even? n))") " — " (code "odd?") " and " (code "even?") " are complementary. "
            (code "(even? n) = (= (mod n 2) 0)") " — " (code "even?") " matches modular arithmetic. "
            (code "(zero? n) = (= n 0)") " — " (code "zero?") " is exactly equality with zero. "
            (code "(not (not p)) = p") " — double negation elimination."))

        (div :class "rounded border border-stone-200 bg-stone-50 p-4"
          (p :class "text-sm font-semibold text-stone-800 mb-2" "min / max / clamp")
          (p :class "text-sm text-stone-600"
            (code "min") " and " (code "max") " are commutative and satisfy their bounds: "
            (code "(min a b) <= a") " and " (code "(max a b) >= a") ". "
            (code "(min a b) + (max a b) = a + b") " — the min-max sum identity. "
            (code "clamp") " with precondition " (code "lo <= hi") ": result is always in " (code "[lo, hi]") ", equals " (code "x") " when already in range, and is idempotent."))

        (div :class "rounded border border-stone-200 bg-stone-50 p-4"
          (p :class "text-sm font-semibold text-stone-800 mb-2" "Comparison & inequality")
          (p :class "text-sm text-stone-600"
            (code "(< a b) = (> b a)") " — flipped arguments. "
            (code "(<= a b) = (not (> a b))") " and " (code "(>= a b) = (not (< a b))") " — duality. "
            "Trichotomy: exactly one of " (code "<") ", " (code "=") ", " (code ">") " holds. "
            "Transitivity: " (code "(< a b)") " and " (code "(< b c)") " implies " (code "(< a c)") ". "
            (code "(!= a b) = (not (= a b))") "."))))

    ;; --- SMT-LIB output ---
    (~docs/section :title "SMT-LIB verification conditions" :id "smtlib"
      (p :class "text-stone-600"
        "Each property also generates SMT-LIB for unbounded verification by an external solver. The strategy: assert the " (em "negation") " of the universal property. If Z3 returns " (code "unsat") ", the property holds for " (em "all") " integers — not just the bounded domain.")
      (p :class "text-stone-600"
        (code "prove.sx") " reuses " (code "z3-expr") " from " (code "z3.sx") " to translate the property AST to SMT-LIB. Properties with preconditions use " (code "=>") " (implication). The same SX expression is both the bounded test and the formal verification condition.")
      (~docs/code :src (highlight smtlib-sample "lisp")))

    ;; --- What it tells us ---
    (~docs/section :title "What this tells us about SX" :id "implications"
      (p :class "text-stone-600"
        "Three things, at increasing depth.")

      (~docs/subsection :title "1. The spec is internally consistent"
        (p :class "text-stone-600"
          "Phase 1 proves every " (code "define-primitive") " with a " (code ":body") " is satisfiable. The definition doesn't contradict itself. This is necessary but weak — it's true by construction. The value is mechanical verification: no typo, no copy-paste error, no accidental negation in any of the 91 definitions."))

      (~docs/subsection :title "2. The primitives obey algebraic laws"
        (p :class "text-stone-600"
          "Phase 2 proves real mathematical properties hold across bounded domains. These aren't tautologies — they're constraints that " (em "could") " fail. "
          (code "(+ a b) = (+ b a)") " could fail if " (code "+") " had a subtle bug. "
          (code "clamp-in-range") " could fail if " (code "max") "/" (code "min") " were swapped. "
          "The " (str phase2-total-tested) " evaluations found zero counterexamples.")
        (p :class "text-stone-600"
          "Bounded model checking is not a mathematical proof — it verifies over a finite domain. The SMT-LIB output bridges the gap: feed it to Z3 for a universal proof over all integers."))

      (~docs/subsection :title "3. SX can reason about itself"
        (p :class "text-stone-600"
          "The deep result. The SX evaluator executes " (code "z3.sx") ", which reads SX spec files and emits formal logic. Then the SX evaluator executes " (code "prove.sx") ", which parses that logic and proves properties about it. The specification, the translator, and the prover are all written in the same language, operating on the same data structures.")
        (p :class "text-stone-600"
          "The pipeline: " (code "SX spec") " → " (code "SX translator") " → " (code "formal logic") " → " (code "SX prover") " → " (code "proof") ". At every step, SX is both the subject and the tool. The system is verifying its own foundations using its own machinery.")
        (div :class "rounded border border-amber-200 bg-amber-50 p-4 mt-3"
          (p :class "text-sm text-amber-800 font-semibold mb-2" "The strange loop")
          (p :class "text-sm text-amber-700"
            "The SX spec defines primitives. " (code "z3.sx") " (written in SX, using those primitives) translates the spec to formal logic. " (code "prove.sx") " (written in SX, using those same primitives) proves properties about the logic. The primitives being verified are the same primitives doing the verifying. This is not circular — it's a fixed point. If the primitives were wrong, the proofs would fail."))))

    ;; --- The pipeline ---
    (~docs/section :title "The full pipeline" :id "pipeline"
      (div :class "rounded border border-stone-200 bg-stone-50 p-4"
        (table :class "w-full text-sm"
          (thead (tr :class "text-left text-stone-500"
            (th :class "pb-2 pr-4" "Step")
            (th :class "pb-2 pr-4" "Input")
            (th :class "pb-2 pr-4" "Tool")
            (th :class "pb-2" "Output")))
          (tbody
            (tr :class "text-stone-700 border-t border-stone-200"
              (td :class "py-2 pr-4 font-mono text-xs" "1")
              (td :class "py-2 pr-4 font-mono text-xs" "primitives.sx")
              (td :class "py-2 pr-4 font-mono text-xs" "z3.sx")
              (td :class "py-2" "SMT-LIB (formal logic)"))
            (tr :class "text-stone-700 border-t border-stone-200"
              (td :class "py-2 pr-4 font-mono text-xs" "2a")
              (td :class "py-2 pr-4 font-mono text-xs" "SMT-LIB")
              (td :class "py-2 pr-4 font-mono text-xs" "prove.sx (Phase 1)")
              (td :class "py-2" "sat (definitional consistency)"))
            (tr :class "text-stone-700 border-t border-stone-200"
              (td :class "py-2 pr-4 font-mono text-xs" "2b")
              (td :class "py-2 pr-4 font-mono text-xs" "property defs")
              (td :class "py-2 pr-4 font-mono text-xs" "prove.sx (Phase 2)")
              (td :class "py-2" "verified (algebraic laws)"))
            (tr :class "text-stone-700 border-t border-stone-200"
              (td :class "py-2 pr-4 font-mono text-xs" "3")
              (td :class "py-2 pr-4 font-mono text-xs" "properties")
              (td :class "py-2 pr-4 font-mono text-xs" "prove.sx → z3-expr")
              (td :class "py-2" "SMT-LIB for Z3 (unbounded)"))
            (tr :class "text-stone-400 border-t border-stone-200"
              (td :class "py-2 pr-4 font-mono text-xs" "4")
              (td :class "py-2 pr-4 font-mono text-xs" "SMT-LIB")
              (td :class "py-2 pr-4 font-mono text-xs italic" "Z3 (external)")
              (td :class "py-2 italic" "unsat (universal proof)")))))
      (p :class "text-stone-600 mt-4"
        "Steps 1-3 run on this page, live, in the SX evaluator. Step 4 requires an external Z3 installation — the SMT-LIB output above is ready to feed to it."))

    ;; --- Source ---
    (~docs/section :title "The source: prove.sx" :id "source"
      (p :class "text-stone-600"
        "The entire constraint solver is a single SX file. Key sections: "
        (code "smt-eval") " evaluates SMT-LIB expressions. "
        (code "prove-tuples") " generates cartesian products for bounded checking. "
        (code "prove-search") " walks tuples looking for counterexamples. "
        (code "sx-properties") " declares 34 algebraic laws as test functions with quoted ASTs. "
        (code "prove-property-smtlib") " translates properties to SMT-LIB verification conditions via " (code "z3-expr") ".")
      (~docs/code :src (highlight prove-source "lisp")))

    (~docs/section :title "The translator: z3.sx" :id "z3-source"
      (p :class "text-stone-600"
        "The translator that " (code "prove.sx") " depends on. SX expressions that walk other SX expressions and emit SMT-LIB strings. Both files together: ~760 lines of s-expressions, no host language logic.")
      (~docs/code :src (highlight z3-source "lisp")))))