giles
00e7ba4650
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>
783 lines
27 KiB
Plaintext
783 lines
27 KiB
Plaintext
;; ==========================================================================
|
|
;; prove.sx — SMT-LIB satisfiability checker, written in SX
|
|
;;
|
|
;; Verifies the SMT-LIB output from z3.sx. For the class of assertions
|
|
;; z3.sx produces (definitional equalities), satisfiability is provable
|
|
;; by construction: the definition IS the model.
|
|
;;
|
|
;; This closes the loop:
|
|
;; primitives.sx → z3.sx → SMT-LIB → prove.sx → sat
|
|
;; SX spec → SX translator → s-expressions → SX prover → proof
|
|
;;
|
|
;; The prover also evaluates each definition with concrete test values
|
|
;; to demonstrate consistency.
|
|
;;
|
|
;; Usage:
|
|
;; (prove-check smtlib-string) — verify a single check-sat block
|
|
;; (prove-translate expr) — translate + verify a define-* form
|
|
;; (prove-file exprs) — verify all define-* forms
|
|
;; ==========================================================================
|
|
|
|
|
|
;; --------------------------------------------------------------------------
|
|
;; SMT-LIB expression evaluator
|
|
;; --------------------------------------------------------------------------
|
|
|
|
;; Evaluate an SMT-LIB expression in a variable environment
|
|
(define smt-eval
|
|
(fn (expr env)
|
|
(cond
|
|
;; Numbers
|
|
(number? expr) expr
|
|
|
|
;; String literals
|
|
(string? expr)
|
|
(cond
|
|
(= expr "true") true
|
|
(= expr "false") false
|
|
:else expr)
|
|
|
|
;; Booleans
|
|
(= expr true) true
|
|
(= expr false) false
|
|
|
|
;; Symbols — look up in env
|
|
(= (type-of expr) "symbol")
|
|
(let ((name (symbol-name expr)))
|
|
(cond
|
|
(= name "true") true
|
|
(= name "false") false
|
|
:else (get env name expr)))
|
|
|
|
;; Lists — function application
|
|
(list? expr)
|
|
(if (empty? expr) nil
|
|
(let ((head (first expr))
|
|
(args (rest expr)))
|
|
(if (not (= (type-of head) "symbol"))
|
|
expr
|
|
(let ((op (symbol-name head)))
|
|
(cond
|
|
;; Arithmetic
|
|
(= op "+")
|
|
(reduce (fn (a b) (+ a b)) 0
|
|
(map (fn (a) (smt-eval a env)) args))
|
|
(= op "-")
|
|
(if (= (len args) 1)
|
|
(- 0 (smt-eval (first args) env))
|
|
(- (smt-eval (nth args 0) env)
|
|
(smt-eval (nth args 1) env)))
|
|
(= op "*")
|
|
(reduce (fn (a b) (* a b)) 1
|
|
(map (fn (a) (smt-eval a env)) args))
|
|
(= op "/")
|
|
(let ((a (smt-eval (nth args 0) env))
|
|
(b (smt-eval (nth args 1) env)))
|
|
(if (= b 0) 0 (/ a b)))
|
|
(= op "div")
|
|
(let ((a (smt-eval (nth args 0) env))
|
|
(b (smt-eval (nth args 1) env)))
|
|
(if (= b 0) 0 (/ a b)))
|
|
(= op "mod")
|
|
(let ((a (smt-eval (nth args 0) env))
|
|
(b (smt-eval (nth args 1) env)))
|
|
(if (= b 0) 0 (mod a b)))
|
|
|
|
;; Comparison
|
|
(= op "=")
|
|
(= (smt-eval (nth args 0) env)
|
|
(smt-eval (nth args 1) env))
|
|
(= op "<")
|
|
(< (smt-eval (nth args 0) env)
|
|
(smt-eval (nth args 1) env))
|
|
(= op ">")
|
|
(> (smt-eval (nth args 0) env)
|
|
(smt-eval (nth args 1) env))
|
|
(= op "<=")
|
|
(<= (smt-eval (nth args 0) env)
|
|
(smt-eval (nth args 1) env))
|
|
(= op ">=")
|
|
(>= (smt-eval (nth args 0) env)
|
|
(smt-eval (nth args 1) env))
|
|
|
|
;; Logic
|
|
(= op "and")
|
|
(every? (fn (a) (smt-eval a env)) args)
|
|
(= op "or")
|
|
(some (fn (a) (smt-eval a env)) args)
|
|
(= op "not")
|
|
(not (smt-eval (first args) env))
|
|
|
|
;; ite (if-then-else)
|
|
(= op "ite")
|
|
(if (smt-eval (nth args 0) env)
|
|
(smt-eval (nth args 1) env)
|
|
(smt-eval (nth args 2) env))
|
|
|
|
;; Function call — look up in env
|
|
:else
|
|
(let ((fn-def (get env op nil)))
|
|
(if (nil? fn-def)
|
|
(list op (map (fn (a) (smt-eval a env)) args))
|
|
;; fn-def is {:params [...] :body expr}
|
|
(let ((params (get fn-def "params" (list)))
|
|
(body (get fn-def "body" nil))
|
|
(evals (map (fn (a) (smt-eval a env)) args)))
|
|
(if (nil? body)
|
|
;; Uninterpreted — return symbolic
|
|
(list op evals)
|
|
;; Evaluate body with params bound
|
|
(smt-eval body
|
|
(merge env
|
|
(smt-bind-params params evals))))))))))))
|
|
|
|
:else expr)))
|
|
|
|
|
|
;; Bind parameter names to values
|
|
(define smt-bind-params
|
|
(fn (params vals)
|
|
(smt-bind-loop params vals {})))
|
|
|
|
(define smt-bind-loop
|
|
(fn (params vals acc)
|
|
(if (or (empty? params) (empty? vals))
|
|
acc
|
|
(smt-bind-loop (rest params) (rest vals)
|
|
(assoc acc (first params) (first vals))))))
|
|
|
|
|
|
;; --------------------------------------------------------------------------
|
|
;; SMT-LIB statement parser
|
|
;; --------------------------------------------------------------------------
|
|
|
|
;; Extract declarations and assertions from parsed SMT-LIB
|
|
(define smt-extract-statements
|
|
(fn (exprs)
|
|
(smt-extract-loop exprs {} (list))))
|
|
|
|
(define smt-extract-loop
|
|
(fn (exprs decls assertions)
|
|
(if (empty? exprs)
|
|
{:decls decls :assertions assertions}
|
|
(let ((expr (first exprs))
|
|
(rest-e (rest exprs)))
|
|
(if (not (list? expr))
|
|
(smt-extract-loop rest-e decls assertions)
|
|
(if (empty? expr)
|
|
(smt-extract-loop rest-e decls assertions)
|
|
(let ((head (symbol-name (first expr))))
|
|
(cond
|
|
;; (declare-fun name (sorts) sort)
|
|
(= head "declare-fun")
|
|
(let ((name (nth expr 1))
|
|
(param-sorts (nth expr 2))
|
|
(ret-sort (nth expr 3)))
|
|
(smt-extract-loop rest-e
|
|
(assoc decls (if (= (type-of name) "symbol")
|
|
(symbol-name name) name)
|
|
{:params (if (list? param-sorts)
|
|
(map (fn (s) (if (= (type-of s) "symbol")
|
|
(symbol-name s) (str s)))
|
|
param-sorts)
|
|
(list))
|
|
:ret (if (= (type-of ret-sort) "symbol")
|
|
(symbol-name ret-sort) (str ret-sort))})
|
|
assertions))
|
|
|
|
;; (assert ...)
|
|
(= head "assert")
|
|
(smt-extract-loop rest-e decls
|
|
(append assertions (list (nth expr 1))))
|
|
|
|
;; (check-sat) — skip
|
|
(= head "check-sat")
|
|
(smt-extract-loop rest-e decls assertions)
|
|
|
|
;; comments (strings starting with ;) — skip
|
|
:else
|
|
(smt-extract-loop rest-e decls assertions)))))))))
|
|
|
|
|
|
;; --------------------------------------------------------------------------
|
|
;; Assertion classifier
|
|
;; --------------------------------------------------------------------------
|
|
|
|
;; Check if an assertion is definitional: (forall (...) (= (f ...) body))
|
|
;; or (= (f) body) for nullary
|
|
(define smt-definitional?
|
|
(fn (assertion)
|
|
(if (not (list? assertion)) false
|
|
(let ((head (symbol-name (first assertion))))
|
|
(cond
|
|
;; (forall ((bindings)) (= (f ...) body))
|
|
(= head "forall")
|
|
(let ((body (nth assertion 2)))
|
|
(and (list? body)
|
|
(= (symbol-name (first body)) "=")))
|
|
;; (= (f ...) body)
|
|
(= head "=")
|
|
true
|
|
:else false)))))
|
|
|
|
|
|
;; Extract the function name, parameters, and body from a definitional assertion
|
|
(define smt-extract-definition
|
|
(fn (assertion)
|
|
(let ((head (symbol-name (first assertion))))
|
|
(cond
|
|
;; (forall (((x Int) (y Int))) (= (f x y) body))
|
|
(= head "forall")
|
|
(let ((bindings (first (nth assertion 1)))
|
|
(eq-expr (nth assertion 2))
|
|
(call (nth eq-expr 1))
|
|
(body (nth eq-expr 2)))
|
|
{:name (if (= (type-of (first call)) "symbol")
|
|
(symbol-name (first call)) (str (first call)))
|
|
:params (map (fn (b)
|
|
(if (list? b)
|
|
(if (= (type-of (first b)) "symbol")
|
|
(symbol-name (first b)) (str (first b)))
|
|
(if (= (type-of b) "symbol")
|
|
(symbol-name b) (str b))))
|
|
(if (list? bindings) bindings (list bindings)))
|
|
:body body})
|
|
|
|
;; (= (f) body)
|
|
(= head "=")
|
|
(let ((call (nth assertion 1))
|
|
(body (nth assertion 2)))
|
|
{:name (if (list? call)
|
|
(if (= (type-of (first call)) "symbol")
|
|
(symbol-name (first call)) (str (first call)))
|
|
(str call))
|
|
:params (list)
|
|
:body body})
|
|
|
|
:else nil))))
|
|
|
|
|
|
;; --------------------------------------------------------------------------
|
|
;; Test value generation
|
|
;; --------------------------------------------------------------------------
|
|
|
|
(define smt-test-values
|
|
(list
|
|
(list 0)
|
|
(list 1)
|
|
(list -1)
|
|
(list 5)
|
|
(list 42)
|
|
(list 1 2)
|
|
(list -3 7)
|
|
(list 5 5)
|
|
(list 100 -50)
|
|
(list 3 1)
|
|
(list 1 1 10)
|
|
(list 5 1 3)
|
|
(list -5 1 10)
|
|
(list 3 3 3)
|
|
(list 7 2 9)))
|
|
|
|
|
|
;; --------------------------------------------------------------------------
|
|
;; Proof engine
|
|
;; --------------------------------------------------------------------------
|
|
|
|
;; Verify a single definitional assertion by construction + evaluation
|
|
(define smt-verify-definition
|
|
(fn (def-info decls)
|
|
(let ((name (get def-info "name"))
|
|
(params (get def-info "params"))
|
|
(body (get def-info "body"))
|
|
(n-params (len params)))
|
|
|
|
;; Build the model: define f = λparams.body
|
|
(let ((model (assoc decls name {:params params :body body}))
|
|
;; Select test values matching arity
|
|
(tests (filter (fn (tv) (= (len tv) n-params)) smt-test-values))
|
|
;; Run tests
|
|
(results (map
|
|
(fn (test-vals)
|
|
(let ((env (merge model (smt-bind-params params test-vals)))
|
|
;; Evaluate body directly
|
|
(body-result (smt-eval body env))
|
|
;; Evaluate via function call
|
|
(call-expr (cons (first (sx-parse name)) test-vals))
|
|
(call-result (smt-eval call-expr env)))
|
|
{:vals test-vals
|
|
:body-result body-result
|
|
:call-result call-result
|
|
:equal (= body-result call-result)}))
|
|
tests)))
|
|
{:name name
|
|
:status (if (every? (fn (r) (get r "equal")) results) "sat" "FAIL")
|
|
:proof "by construction (definition is the model)"
|
|
:tests-passed (len (filter (fn (r) (get r "equal")) results))
|
|
:tests-total (len results)
|
|
:sample (if (empty? results) nil (first results))}))))
|
|
|
|
|
|
;; --------------------------------------------------------------------------
|
|
;; Public API
|
|
;; --------------------------------------------------------------------------
|
|
|
|
;; Strip SMT-LIB comment lines (starting with ;) and return only actual forms.
|
|
;; Handles comments that contain ( characters.
|
|
(define smt-strip-comments
|
|
(fn (s)
|
|
(let ((lines (split s "\n"))
|
|
(non-comment (filter
|
|
(fn (line) (not (starts-with? (trim line) ";")))
|
|
lines)))
|
|
(join "\n" non-comment))))
|
|
|
|
;; Verify SMT-LIB output (string) — parse, classify, prove
|
|
(define prove-check
|
|
(fn (smtlib-str)
|
|
(let ((parsed (sx-parse (smt-strip-comments smtlib-str)))
|
|
(stmts (smt-extract-statements parsed))
|
|
(decls (get stmts "decls"))
|
|
(assertions (get stmts "assertions")))
|
|
(if (empty? assertions)
|
|
{:status "sat" :reason "no assertions (declaration only)"}
|
|
(let ((results (map
|
|
(fn (assertion)
|
|
(if (smt-definitional? assertion)
|
|
(let ((def-info (smt-extract-definition assertion)))
|
|
(if (nil? def-info)
|
|
{:status "unknown" :reason "could not parse definition"}
|
|
(smt-verify-definition def-info decls)))
|
|
{:status "unknown"
|
|
:reason "non-definitional assertion (needs full SMT solver)"}))
|
|
assertions)))
|
|
{:status (if (every? (fn (r) (= (get r "status") "sat")) results)
|
|
"sat" "unknown")
|
|
:assertions (len assertions)
|
|
:results results})))))
|
|
|
|
|
|
;; Translate a define-* form AND verify it — the full pipeline
|
|
(define prove-translate
|
|
(fn (expr)
|
|
(let ((smtlib (z3-translate expr))
|
|
(proof (prove-check smtlib))
|
|
(status (get proof "status"))
|
|
(results (get proof "results" (list))))
|
|
(str smtlib "\n"
|
|
";; ─── prove.sx ───\n"
|
|
";; status: " status "\n"
|
|
(if (empty? results) ""
|
|
(let ((r (first results)))
|
|
(str ";; proof: " (get r "proof" "") "\n"
|
|
";; tested: " (str (get r "tests-passed" 0))
|
|
"/" (str (get r "tests-total" 0))
|
|
" ground instances\n")))))))
|
|
|
|
|
|
;; Batch verify: translate and prove all define-* forms
|
|
(define prove-file
|
|
(fn (exprs)
|
|
(let ((translatable
|
|
(filter
|
|
(fn (expr)
|
|
(and (list? expr)
|
|
(>= (len expr) 2)
|
|
(= (type-of (first expr)) "symbol")
|
|
(let ((name (symbol-name (first expr))))
|
|
(or (= name "define-primitive")
|
|
(= name "define-io-primitive")
|
|
(= name "define-special-form")))))
|
|
exprs))
|
|
(results (map
|
|
(fn (expr)
|
|
(let ((smtlib (z3-translate expr))
|
|
(proof (prove-check smtlib))
|
|
(name (nth expr 1)))
|
|
(assoc proof "name" name)))
|
|
translatable))
|
|
(sat-count (len (filter (fn (r) (= (get r "status") "sat")) results)))
|
|
(total (len results)))
|
|
{:total total
|
|
: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)))
|