Add theorem prover docs page with Phase 2 constraint solving
Some checks failed
Build and Deploy / build-and-deploy (push) Has been cancelled
Some checks failed
Build and Deploy / build-and-deploy (push) Has been cancelled
- prove.sx Phase 2: bounded model checking with 34 algebraic properties (commutativity, associativity, distributivity, inverses, bounds, transitivity) - prove.sx generates SMT-LIB for unbounded Z3 verification via z3-expr - New docs page /plans/theorem-prover with live results (91/91 sat, 34/34 verified) - Page helper runs both proof phases and returns structured data - Parser: re-add ' quote syntax (removed by prior edit) - Load prove.sx alongside z3.sx at startup Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
This commit is contained in:
@@ -28,7 +28,7 @@ def _load_sx_libraries() -> None:
|
||||
"""Load self-hosted SX libraries from the ref directory."""
|
||||
from .jinja_bridge import register_components
|
||||
ref_dir = os.path.join(os.path.dirname(__file__), "ref")
|
||||
for name in ("z3.sx",):
|
||||
for name in ("z3.sx", "prove.sx"):
|
||||
path = os.path.join(ref_dir, name)
|
||||
if os.path.exists(path):
|
||||
with open(path, encoding="utf-8") as f:
|
||||
|
||||
@@ -309,7 +309,11 @@ def _parse_expr(tok: Tokenizer) -> Any:
|
||||
if raw == "{":
|
||||
tok.next_token() # consume the '{'
|
||||
return _parse_map(tok)
|
||||
# Quasiquote syntax: ` , ,@
|
||||
# Quote / quasiquote syntax: ' ` , ,@
|
||||
if raw == "'":
|
||||
tok._advance(1) # consume the quote
|
||||
inner = _parse_expr(tok)
|
||||
return [Symbol("quote"), inner]
|
||||
if raw == "`":
|
||||
tok._advance(1) # consume the backtick
|
||||
inner = _parse_expr(tok)
|
||||
|
||||
@@ -402,3 +402,381 @@
|
||||
:sat sat-count
|
||||
:all-sat (= sat-count total)
|
||||
:results results})))
|
||||
|
||||
|
||||
;; ==========================================================================
|
||||
;; Phase 2: Property-based constraint solving
|
||||
;; ==========================================================================
|
||||
;;
|
||||
;; Properties are dicts:
|
||||
;; {:name "+-commutative"
|
||||
;; :vars ("a" "b")
|
||||
;; :test (fn (a b) (= (+ a b) (+ b a))) — for bounded checking
|
||||
;; :holds (= (+ a b) (+ b a)) — quoted AST for SMT-LIB
|
||||
;; :given (fn (lo hi) (<= lo hi)) — optional precondition
|
||||
;; :given-expr (<= lo hi) — quoted AST of precondition
|
||||
;; :domain (-20 21)} — optional custom range
|
||||
|
||||
|
||||
;; --------------------------------------------------------------------------
|
||||
;; Domain generation
|
||||
;; --------------------------------------------------------------------------
|
||||
|
||||
;; Default domain bounds by arity — balance coverage vs. combinatorics
|
||||
(define prove-domain-for
|
||||
(fn (arity)
|
||||
(cond
|
||||
(<= arity 1) (range -50 51) ;; 101 values
|
||||
(= arity 2) (range -20 21) ;; 41^2 = 1,681 pairs
|
||||
(= arity 3) (range -8 9) ;; 17^3 = 4,913 triples
|
||||
:else (range -5 6)))) ;; 11^n for n >= 4
|
||||
|
||||
;; Cartesian product: all n-tuples from a domain
|
||||
(define prove-tuples
|
||||
(fn (domain arity)
|
||||
(if (<= arity 0) (list (list))
|
||||
(if (= arity 1)
|
||||
(map (fn (x) (list x)) domain)
|
||||
(let ((sub (prove-tuples domain (- arity 1))))
|
||||
(prove-tuples-expand domain sub (list)))))))
|
||||
|
||||
(define prove-tuples-expand
|
||||
(fn (domain sub acc)
|
||||
(if (empty? domain) acc
|
||||
(prove-tuples-expand
|
||||
(rest domain) sub
|
||||
(append acc
|
||||
(map (fn (t) (cons (first domain) t)) sub))))))
|
||||
|
||||
|
||||
;; --------------------------------------------------------------------------
|
||||
;; Function application by arity (no apply primitive available)
|
||||
;; --------------------------------------------------------------------------
|
||||
|
||||
(define prove-call
|
||||
(fn (f vals)
|
||||
(let ((n (len vals)))
|
||||
(cond
|
||||
(= n 0) (f)
|
||||
(= n 1) (f (nth vals 0))
|
||||
(= n 2) (f (nth vals 0) (nth vals 1))
|
||||
(= n 3) (f (nth vals 0) (nth vals 1) (nth vals 2))
|
||||
(= n 4) (f (nth vals 0) (nth vals 1) (nth vals 2) (nth vals 3))
|
||||
:else nil))))
|
||||
|
||||
|
||||
;; --------------------------------------------------------------------------
|
||||
;; Bounded model checker
|
||||
;; --------------------------------------------------------------------------
|
||||
|
||||
;; Search for a counterexample. Returns nil if property holds for all tested
|
||||
;; values, or the first counterexample found.
|
||||
(define prove-search
|
||||
(fn (test-fn given-fn domain vars)
|
||||
(let ((arity (len vars))
|
||||
(tuples (prove-tuples domain arity)))
|
||||
(prove-search-loop test-fn given-fn tuples 0 0))))
|
||||
|
||||
(define prove-search-loop
|
||||
(fn (test-fn given-fn tuples tested skipped)
|
||||
(if (empty? tuples)
|
||||
{:status "verified" :tested tested :skipped skipped}
|
||||
(let ((vals (first tuples))
|
||||
(rest-t (rest tuples)))
|
||||
;; Check precondition (if any)
|
||||
(if (and (not (nil? given-fn))
|
||||
(not (prove-call given-fn vals)))
|
||||
;; Precondition not met — skip this combination
|
||||
(prove-search-loop test-fn given-fn rest-t tested (+ skipped 1))
|
||||
;; Evaluate the property
|
||||
(if (prove-call test-fn vals)
|
||||
;; Passed — continue
|
||||
(prove-search-loop test-fn given-fn rest-t (+ tested 1) skipped)
|
||||
;; Failed — counterexample found
|
||||
{:status "falsified"
|
||||
:tested tested
|
||||
:skipped skipped
|
||||
:counterexample vals}))))))
|
||||
|
||||
|
||||
;; --------------------------------------------------------------------------
|
||||
;; Property verification (public API)
|
||||
;; --------------------------------------------------------------------------
|
||||
|
||||
;; Verify a single property via bounded model checking
|
||||
(define prove-property
|
||||
(fn (prop)
|
||||
(let ((name (get prop "name"))
|
||||
(vars (get prop "vars"))
|
||||
(test-fn (get prop "test"))
|
||||
(given-fn (get prop "given" nil))
|
||||
(custom (get prop "domain" nil))
|
||||
(domain (if (nil? custom)
|
||||
(prove-domain-for (len vars))
|
||||
(range (nth custom 0) (nth custom 1)))))
|
||||
(let ((result (prove-search test-fn given-fn domain vars)))
|
||||
(assoc result "name" name)))))
|
||||
|
||||
;; Batch verify a list of properties
|
||||
(define prove-properties
|
||||
(fn (props)
|
||||
(let ((results (map prove-property props))
|
||||
(verified (filter (fn (r) (= (get r "status") "verified")) results))
|
||||
(falsified (filter (fn (r) (= (get r "status") "falsified")) results)))
|
||||
{:total (len results)
|
||||
:verified (len verified)
|
||||
:falsified (len falsified)
|
||||
:all-verified (= (len falsified) 0)
|
||||
:results results})))
|
||||
|
||||
|
||||
;; --------------------------------------------------------------------------
|
||||
;; SMT-LIB generation for properties
|
||||
;; --------------------------------------------------------------------------
|
||||
|
||||
;; Generate SMT-LIB for a property — asserts (not (forall ...)) so that
|
||||
;; Z3 returning "unsat" proves the property holds universally.
|
||||
(define prove-property-smtlib
|
||||
(fn (prop)
|
||||
(let ((name (get prop "name"))
|
||||
(vars (get prop "vars"))
|
||||
(holds (get prop "holds"))
|
||||
(given-e (get prop "given-expr" nil))
|
||||
(bindings (join " "
|
||||
(map (fn (v) (str "(" v " Int)")) vars)))
|
||||
(holds-smt (z3-expr holds))
|
||||
(body (if (nil? given-e)
|
||||
holds-smt
|
||||
(str "(=> " (z3-expr given-e) " " holds-smt ")"))))
|
||||
(str "; Property: " name "\n"
|
||||
"; Strategy: assert negation, check for unsat\n"
|
||||
"(assert (not (forall ((" bindings "))\n"
|
||||
" " body ")))\n"
|
||||
"(check-sat) ; expect unsat\n"))))
|
||||
|
||||
;; Generate SMT-LIB for all properties, including necessary definitions
|
||||
(define prove-properties-smtlib
|
||||
(fn (props primitives-exprs)
|
||||
(let ((defs (z3-translate-file primitives-exprs))
|
||||
(prop-smts (map prove-property-smtlib props)))
|
||||
(str ";; ================================================================\n"
|
||||
";; Auto-generated by prove.sx — property verification conditions\n"
|
||||
";; Feed to Z3 for unbounded proofs\n"
|
||||
";; ================================================================\n\n"
|
||||
";; --- Primitive definitions ---\n"
|
||||
defs "\n\n"
|
||||
";; --- Properties ---\n"
|
||||
(join "\n" prop-smts)))))
|
||||
|
||||
|
||||
;; ==========================================================================
|
||||
;; Property library: algebraic laws of SX primitives
|
||||
;; ==========================================================================
|
||||
|
||||
(define sx-properties
|
||||
(list
|
||||
|
||||
;; ----- Arithmetic identities -----
|
||||
|
||||
{:name "+-commutative"
|
||||
:vars (list "a" "b")
|
||||
:test (fn (a b) (= (+ a b) (+ b a)))
|
||||
:holds '(= (+ a b) (+ b a))}
|
||||
|
||||
{:name "+-associative"
|
||||
:vars (list "a" "b" "c")
|
||||
:test (fn (a b c) (= (+ (+ a b) c) (+ a (+ b c))))
|
||||
:holds '(= (+ (+ a b) c) (+ a (+ b c)))}
|
||||
|
||||
{:name "+-identity"
|
||||
:vars (list "a")
|
||||
:test (fn (a) (= (+ a 0) a))
|
||||
:holds '(= (+ a 0) a)}
|
||||
|
||||
{:name "*-commutative"
|
||||
:vars (list "a" "b")
|
||||
:test (fn (a b) (= (* a b) (* b a)))
|
||||
:holds '(= (* a b) (* b a))}
|
||||
|
||||
{:name "*-associative"
|
||||
:vars (list "a" "b" "c")
|
||||
:test (fn (a b c) (= (* (* a b) c) (* a (* b c))))
|
||||
:holds '(= (* (* a b) c) (* a (* b c)))}
|
||||
|
||||
{:name "*-identity"
|
||||
:vars (list "a")
|
||||
:test (fn (a) (= (* a 1) a))
|
||||
:holds '(= (* a 1) a)}
|
||||
|
||||
{:name "*-zero"
|
||||
:vars (list "a")
|
||||
:test (fn (a) (= (* a 0) 0))
|
||||
:holds '(= (* a 0) 0)}
|
||||
|
||||
{:name "distributive"
|
||||
:vars (list "a" "b" "c")
|
||||
:test (fn (a b c) (= (* a (+ b c)) (+ (* a b) (* a c))))
|
||||
:holds '(= (* a (+ b c)) (+ (* a b) (* a c)))}
|
||||
|
||||
{:name "--inverse"
|
||||
:vars (list "a")
|
||||
:test (fn (a) (= (- a a) 0))
|
||||
:holds '(= (- a a) 0)}
|
||||
|
||||
;; ----- inc / dec -----
|
||||
|
||||
{:name "inc-is-plus-1"
|
||||
:vars (list "n")
|
||||
:test (fn (n) (= (inc n) (+ n 1)))
|
||||
:holds '(= (inc n) (+ n 1))}
|
||||
|
||||
{:name "dec-is-minus-1"
|
||||
:vars (list "n")
|
||||
:test (fn (n) (= (dec n) (- n 1)))
|
||||
:holds '(= (dec n) (- n 1))}
|
||||
|
||||
{:name "inc-dec-inverse"
|
||||
:vars (list "n")
|
||||
:test (fn (n) (= (dec (inc n)) n))
|
||||
:holds '(= (dec (inc n)) n)}
|
||||
|
||||
{:name "dec-inc-inverse"
|
||||
:vars (list "n")
|
||||
:test (fn (n) (= (inc (dec n)) n))
|
||||
:holds '(= (inc (dec n)) n)}
|
||||
|
||||
;; ----- abs -----
|
||||
|
||||
{:name "abs-non-negative"
|
||||
:vars (list "n")
|
||||
:test (fn (n) (>= (abs n) 0))
|
||||
:holds '(>= (abs n) 0)}
|
||||
|
||||
{:name "abs-idempotent"
|
||||
:vars (list "n")
|
||||
:test (fn (n) (= (abs (abs n)) (abs n)))
|
||||
:holds '(= (abs (abs n)) (abs n))}
|
||||
|
||||
{:name "abs-symmetric"
|
||||
:vars (list "n")
|
||||
:test (fn (n) (= (abs n) (abs (- 0 n))))
|
||||
:holds '(= (abs n) (abs (- 0 n)))}
|
||||
|
||||
;; ----- Predicates -----
|
||||
|
||||
{:name "odd-not-even"
|
||||
:vars (list "n")
|
||||
:test (fn (n) (= (odd? n) (not (even? n))))
|
||||
:holds '(= (odd? n) (not (even? n)))}
|
||||
|
||||
{:name "even-mod-2"
|
||||
:vars (list "n")
|
||||
:test (fn (n) (= (even? n) (= (mod n 2) 0)))
|
||||
:holds '(= (even? n) (= (mod n 2) 0))}
|
||||
|
||||
{:name "zero-is-zero"
|
||||
:vars (list "n")
|
||||
:test (fn (n) (= (zero? n) (= n 0)))
|
||||
:holds '(= (zero? n) (= n 0))}
|
||||
|
||||
{:name "not-involution"
|
||||
:vars (list "n")
|
||||
:test (fn (n) (= (not (not (zero? n))) (zero? n)))
|
||||
:holds '(= (not (not (zero? n))) (zero? n))}
|
||||
|
||||
;; ----- min / max -----
|
||||
|
||||
{:name "min-commutative"
|
||||
:vars (list "a" "b")
|
||||
:test (fn (a b) (= (min a b) (min b a)))
|
||||
:holds '(= (min a b) (min b a))}
|
||||
|
||||
{:name "max-commutative"
|
||||
:vars (list "a" "b")
|
||||
:test (fn (a b) (= (max a b) (max b a)))
|
||||
:holds '(= (max a b) (max b a))}
|
||||
|
||||
{:name "min-le-both"
|
||||
:vars (list "a" "b")
|
||||
:test (fn (a b) (and (<= (min a b) a) (<= (min a b) b)))
|
||||
:holds '(and (<= (min a b) a) (<= (min a b) b))}
|
||||
|
||||
{:name "max-ge-both"
|
||||
:vars (list "a" "b")
|
||||
:test (fn (a b) (and (>= (max a b) a) (>= (max a b) b)))
|
||||
:holds '(and (>= (max a b) a) (>= (max a b) b))}
|
||||
|
||||
{:name "min-max-identity"
|
||||
:vars (list "a" "b")
|
||||
:test (fn (a b) (= (+ (min a b) (max a b)) (+ a b)))
|
||||
:holds '(= (+ (min a b) (max a b)) (+ a b))}
|
||||
|
||||
;; ----- clamp -----
|
||||
|
||||
{:name "clamp-in-range"
|
||||
:vars (list "x" "lo" "hi")
|
||||
:test (fn (x lo hi) (and (<= lo (clamp x lo hi))
|
||||
(<= (clamp x lo hi) hi)))
|
||||
:given (fn (x lo hi) (<= lo hi))
|
||||
:holds '(and (<= lo (clamp x lo hi)) (<= (clamp x lo hi) hi))
|
||||
:given-expr '(<= lo hi)}
|
||||
|
||||
{:name "clamp-identity-in-range"
|
||||
:vars (list "x" "lo" "hi")
|
||||
:test (fn (x lo hi) (= (clamp x lo hi) x))
|
||||
:given (fn (x lo hi) (and (<= lo hi) (<= lo x) (<= x hi)))
|
||||
:holds '(= (clamp x lo hi) x)
|
||||
:given-expr '(and (<= lo hi) (<= lo x) (<= x hi))}
|
||||
|
||||
{:name "clamp-idempotent"
|
||||
:vars (list "x" "lo" "hi")
|
||||
:test (fn (x lo hi) (= (clamp (clamp x lo hi) lo hi)
|
||||
(clamp x lo hi)))
|
||||
:given (fn (x lo hi) (<= lo hi))
|
||||
:holds '(= (clamp (clamp x lo hi) lo hi) (clamp x lo hi))
|
||||
:given-expr '(<= lo hi)}
|
||||
|
||||
;; ----- Comparison -----
|
||||
|
||||
{:name "lt-gt-flip"
|
||||
:vars (list "a" "b")
|
||||
:test (fn (a b) (= (< a b) (> b a)))
|
||||
:holds '(= (< a b) (> b a))}
|
||||
|
||||
{:name "le-not-gt"
|
||||
:vars (list "a" "b")
|
||||
:test (fn (a b) (= (<= a b) (not (> a b))))
|
||||
:holds '(= (<= a b) (not (> a b)))}
|
||||
|
||||
{:name "ge-not-lt"
|
||||
:vars (list "a" "b")
|
||||
:test (fn (a b) (= (>= a b) (not (< a b))))
|
||||
:holds '(= (>= a b) (not (< a b)))}
|
||||
|
||||
{:name "trichotomy"
|
||||
:vars (list "a" "b")
|
||||
:test (fn (a b) (or (< a b) (= a b) (> a b)))
|
||||
:holds '(or (< a b) (= a b) (> a b))}
|
||||
|
||||
{:name "lt-transitive"
|
||||
:vars (list "a" "b" "c")
|
||||
:test (fn (a b c) (if (and (< a b) (< b c)) (< a c) true))
|
||||
:given (fn (a b c) (and (< a b) (< b c)))
|
||||
:holds '(< a c)
|
||||
:given-expr '(and (< a b) (< b c))}
|
||||
|
||||
;; ----- Inequality -----
|
||||
|
||||
{:name "neq-is-not-eq"
|
||||
:vars (list "a" "b")
|
||||
:test (fn (a b) (= (!= a b) (not (= a b))))
|
||||
:holds '(= (!= a b) (not (= a b)))}))
|
||||
|
||||
|
||||
;; --------------------------------------------------------------------------
|
||||
;; Run all built-in properties
|
||||
;; --------------------------------------------------------------------------
|
||||
|
||||
(define prove-all-properties
|
||||
(fn ()
|
||||
(prove-properties sx-properties)))
|
||||
|
||||
@@ -157,6 +157,8 @@
|
||||
:summary "Extensible parse-time transformations via # dispatch — datum comments, raw strings, and quote shorthand.")
|
||||
(dict :label "Reader Macro Demo" :href "/plans/reader-macro-demo"
|
||||
:summary "Live demo: #z3 translates SX spec declarations to SMT-LIB verification conditions.")
|
||||
(dict :label "Theorem Prover" :href "/plans/theorem-prover"
|
||||
:summary "prove.sx — constraint solver and property prover for SX primitives, written in SX.")
|
||||
(dict :label "SX-Activity" :href "/plans/sx-activity"
|
||||
:summary "A new web built on SX — executable content, shared components, parsers, and logic on IPFS, provenance on Bitcoin, all running within your own security context.")
|
||||
(dict :label "Predictive Prefetching" :href "/plans/predictive-prefetch"
|
||||
|
||||
253
sx/sx/plans/theorem-prover.sx
Normal file
253
sx/sx/plans/theorem-prover.sx
Normal file
@@ -0,0 +1,253 @@
|
||||
;; ---------------------------------------------------------------------------
|
||||
;; Theorem Prover: prove.sx — Constraint Solving for SX Primitives
|
||||
;; ---------------------------------------------------------------------------
|
||||
|
||||
;; Helper: render a Phase 1 result row
|
||||
(defcomp ~prove-phase1-row (&key name status)
|
||||
(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 ~prove-phase2-row (&key name status tested skipped counterexample)
|
||||
(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 ~plan-theorem-prover-content ()
|
||||
(~doc-page :title "Theorem Prover"
|
||||
|
||||
;; --- Intro ---
|
||||
(~doc-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 ---
|
||||
(~doc-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:")
|
||||
(~doc-code :code (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"))
|
||||
|
||||
(~doc-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)
|
||||
(~prove-phase1-row
|
||||
:name (get r "name")
|
||||
:status (get r "status")))
|
||||
phase1-results))))))
|
||||
|
||||
;; --- Phase 2 Results ---
|
||||
(~doc-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")))
|
||||
|
||||
(~doc-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)
|
||||
(~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 ---
|
||||
(~doc-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 ---
|
||||
(~doc-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.")
|
||||
(~doc-code :code (highlight smtlib-sample "lisp")))
|
||||
|
||||
;; --- What it tells us ---
|
||||
(~doc-section :title "What this tells us about SX" :id "implications"
|
||||
(p :class "text-stone-600"
|
||||
"Three things, at increasing depth.")
|
||||
|
||||
(~doc-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."))
|
||||
|
||||
(~doc-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."))
|
||||
|
||||
(~doc-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") " \u2192 " (code "SX translator") " \u2192 " (code "formal logic") " \u2192 " (code "SX prover") " \u2192 " (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 ---
|
||||
(~doc-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 \u2192 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 ---
|
||||
(~doc-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") ".")
|
||||
(~doc-code :code (highlight prove-source "lisp")))
|
||||
|
||||
(~doc-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.")
|
||||
(~doc-code :code (highlight z3-source "lisp")))))
|
||||
@@ -626,10 +626,14 @@
|
||||
:sub-nav (~section-nav :items plans-nav-items
|
||||
:current (find-current plans-nav-items slug))
|
||||
:selected (or (find-current plans-nav-items slug) ""))
|
||||
:data (case slug
|
||||
"theorem-prover" (prove-data)
|
||||
:else nil)
|
||||
:content (case slug
|
||||
"status" (~plan-status-content)
|
||||
"reader-macros" (~plan-reader-macros-content)
|
||||
"reader-macro-demo" (~plan-reader-macro-demo-content)
|
||||
"theorem-prover" (~plan-theorem-prover-content)
|
||||
"sx-activity" (~plan-sx-activity-content)
|
||||
"predictive-prefetch" (~plan-predictive-prefetch-content)
|
||||
"content-addressed-components" (~plan-content-addressed-components-content)
|
||||
|
||||
@@ -31,6 +31,7 @@ def _register_sx_helpers() -> None:
|
||||
"optimistic-demo-data": _optimistic_demo_data,
|
||||
"action:add-demo-item": _add_demo_item,
|
||||
"offline-demo-data": _offline_demo_data,
|
||||
"prove-data": _prove_data,
|
||||
})
|
||||
|
||||
|
||||
@@ -1000,6 +1001,109 @@ def _add_demo_item(**kwargs) -> dict:
|
||||
}
|
||||
|
||||
|
||||
def _prove_data() -> dict:
|
||||
"""Run prove.sx against the SX spec — both phases.
|
||||
|
||||
Phase 1: Translate all define-* forms via z3.sx, verify satisfiability.
|
||||
Phase 2: Evaluate algebraic properties via bounded model checking.
|
||||
Returns results for the docs page to render.
|
||||
"""
|
||||
import time
|
||||
from shared.sx.parser import parse_all
|
||||
from shared.sx.evaluator import evaluate
|
||||
from shared.sx.primitives import all_primitives
|
||||
from shared.sx.evaluator import _trampoline, _call_lambda
|
||||
|
||||
env = all_primitives()
|
||||
|
||||
ref_dir = _ref_dir()
|
||||
for lib in ("z3.sx", "prove.sx"):
|
||||
path = __import__("os").path.join(ref_dir, lib)
|
||||
with open(path, encoding="utf-8") as f:
|
||||
for expr in parse_all(f.read()):
|
||||
evaluate(expr, env)
|
||||
|
||||
# Phase 1: definitional satisfiability
|
||||
with open(__import__("os").path.join(ref_dir, "primitives.sx"), encoding="utf-8") as f:
|
||||
prim_exprs = parse_all(f.read())
|
||||
|
||||
t0 = time.monotonic()
|
||||
phase1 = _trampoline(_call_lambda(env["prove-file"], [prim_exprs], env))
|
||||
phase1_ms = round((time.monotonic() - t0) * 1000)
|
||||
|
||||
# Phase 2: property-based constraint solving
|
||||
t1 = time.monotonic()
|
||||
phase2 = _trampoline(_call_lambda(env["prove-all-properties"], [], env))
|
||||
phase2_ms = round((time.monotonic() - t1) * 1000)
|
||||
|
||||
# Flatten Phase 1 results for rendering
|
||||
phase1_results = []
|
||||
for r in phase1.get("results", []):
|
||||
phase1_results.append({
|
||||
"name": r.get("name", "?"),
|
||||
"status": r.get("status", "?"),
|
||||
})
|
||||
|
||||
# Flatten Phase 2 results for rendering
|
||||
phase2_results = []
|
||||
total_tested = 0
|
||||
for r in phase2.get("results", []):
|
||||
tested = r.get("tested", 0)
|
||||
skipped = r.get("skipped", 0)
|
||||
total_tested += tested
|
||||
entry = {
|
||||
"name": r.get("name", "?"),
|
||||
"status": r.get("status", "?"),
|
||||
"tested": tested,
|
||||
"skipped": skipped,
|
||||
}
|
||||
ce = r.get("counterexample")
|
||||
if ce:
|
||||
entry["counterexample"] = str(ce)
|
||||
phase2_results.append(entry)
|
||||
|
||||
# Generate SMT-LIB sample for a few properties
|
||||
props = env["sx-properties"]
|
||||
smtlib_samples = []
|
||||
for p in props[:3]:
|
||||
smt = _trampoline(_call_lambda(env["prove-property-smtlib"], [p], env))
|
||||
smtlib_samples.append(smt)
|
||||
# One with precondition
|
||||
for p in props:
|
||||
if p.get("given-expr"):
|
||||
smt = _trampoline(_call_lambda(env["prove-property-smtlib"], [p], env))
|
||||
smtlib_samples.append(smt)
|
||||
break
|
||||
|
||||
return {
|
||||
"phase1-total": phase1.get("total", 0),
|
||||
"phase1-sat": phase1.get("sat", 0),
|
||||
"phase1-all-sat": phase1.get("all-sat", False),
|
||||
"phase1-ms": phase1_ms,
|
||||
"phase1-results": phase1_results,
|
||||
"phase2-total": phase2.get("total", 0),
|
||||
"phase2-verified": phase2.get("verified", 0),
|
||||
"phase2-falsified": phase2.get("falsified", 0),
|
||||
"phase2-all-verified": phase2.get("all-verified", False),
|
||||
"phase2-ms": phase2_ms,
|
||||
"phase2-results": phase2_results,
|
||||
"phase2-total-tested": total_tested,
|
||||
"smtlib-sample": "\n".join(smtlib_samples),
|
||||
"prove-source": _read_spec_file("prove.sx"),
|
||||
"z3-source": _read_spec_file("z3.sx"),
|
||||
}
|
||||
|
||||
|
||||
def _ref_dir() -> str:
|
||||
"""Return the path to the SX ref directory."""
|
||||
import os
|
||||
# Same resolution as _read_spec_file
|
||||
ref_dir = os.path.join(os.path.dirname(__file__), "..", "..", "shared", "sx", "ref")
|
||||
if not os.path.isdir(ref_dir):
|
||||
ref_dir = "/app/shared/sx/ref"
|
||||
return ref_dir
|
||||
|
||||
|
||||
def _offline_demo_data() -> dict:
|
||||
"""Return demo data for the offline data layer test page."""
|
||||
from datetime import datetime, timezone
|
||||
|
||||
Reference in New Issue
Block a user