;; ==========================================================================
;; 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 :as dict))
    (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 :as list) (vals :as list))
    (smt-bind-loop params vals {})))

(define smt-bind-loop
  (fn ((params :as list) (vals :as list) (acc :as dict))
    (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 :as list))
    (smt-extract-loop exprs {} (list))))

(define smt-extract-loop
  (fn ((exprs :as list) (decls :as dict) (assertions :as list))
    (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 :as dict) (decls :as dict))
    (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 :as list)) (= (len tv) n-params)) smt-test-values))
            ;; Run tests
            (results (map
              (fn ((test-vals :as list))
                (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 :as dict)) (get r "equal")) results) "sat" "FAIL")
         :proof "by construction (definition is the model)"
         :tests-passed (len (filter (fn ((r :as dict)) (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 :as string))
    (let ((lines (split s "\n"))
          (non-comment (filter
            (fn ((line :as string)) (not (starts-with? (trim line) ";")))
            lines)))
      (join "\n" non-comment))))

;; Verify SMT-LIB output (string) — parse, classify, prove
(define prove-check
  (fn ((smtlib-str :as string))
    (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 :as dict)) (= (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 :as list))
    (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 :as dict)) (= (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 :as number))
    (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 :as list) (arity :as number))
    (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 :as list) (sub :as list) (acc :as list))
    (if (empty? domain) acc
      (prove-tuples-expand
        (rest domain) sub
        (append acc
          (map (fn ((t :as list)) (cons (first domain) t)) sub))))))


;; --------------------------------------------------------------------------
;; Function application by arity (no apply primitive available)
;; --------------------------------------------------------------------------

(define prove-call
  (fn ((f :as lambda) (vals :as list))
    (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 :as lambda) given-fn (domain :as list) (vars :as list))
    (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 :as lambda) given-fn (tuples :as list) (tested :as number) (skipped :as number))
    (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 :as dict))
    (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 :as list))
    (let ((results (map prove-property props))
          (verified (filter (fn ((r :as dict)) (= (get r "status") "verified")) results))
          (falsified (filter (fn ((r :as dict)) (= (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 :as dict))
    (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 :as string)) (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 :as list) (primitives-exprs :as list))
    (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)))