coop/rose-ash
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Add (param :as type) annotations to all fn/lambda params across SX spec

Browse Source 
Extend the type annotation system from defcomp-only to fn/lambda params:
- Infrastructure: sf-lambda, py/js-collect-params-loop, and bootstrap_py.py
  now recognize (name :as type) in param lists, extracting just the name
- bootstrap_py.py: add _extract_param_name() helper, fix _emit_for_each_stmt
- 521 type annotations across 22 .sx spec files (eval, types, adapters,
  transpilers, engine, orchestration, deps, signals, router, prove, etc.)
- Zero behavioral change: annotations are metadata for static analysis only
- All bootstrappers (Python, JS, G1) pass, 81/81 spec tests pass

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
This commit is contained in:
giles
2026-03-11 20:27:36 +00:00
parent c82941d93c
commit b99e69d1bb
23 changed files with 532 additions and 498 deletions
Download Patch File Download Diff File Expand all files Collapse all files

60
shared/sx/ref/prove.sx
View File

@@ -25,7 +25,7 @@
;; Evaluate an SMT-LIB expression in a variable environment
(define smt-eval
(fn (expr env)
(fn (expr (env :as dict))
(cond
;; Numbers
(number? expr) expr
@@ -136,11 +136,11 @@
;; Bind parameter names to values
(define smt-bind-params
(fn (params vals)
(fn ((params :as list) (vals :as list))
(smt-bind-loop params vals {})))
(define smt-bind-loop
(fn (params vals acc)
(fn ((params :as list) (vals :as list) (acc :as dict))
(if (or (empty? params) (empty? vals))
acc
(smt-bind-loop (rest params) (rest vals)
@@ -153,11 +153,11 @@
;; Extract declarations and assertions from parsed SMT-LIB
(define smt-extract-statements
(fn (exprs)
(fn ((exprs :as list))
(smt-extract-loop exprs {} (list))))
(define smt-extract-loop
(fn (exprs decls assertions)
(fn ((exprs :as list) (decls :as dict) (assertions :as list))
(if (empty? exprs)
{:decls decls :assertions assertions}
(let ((expr (first exprs))
@@ -286,7 +286,7 @@
;; Verify a single definitional assertion by construction + evaluation
(define smt-verify-definition
(fn (def-info decls)
(fn ((def-info :as dict) (decls :as dict))
(let ((name (get def-info "name"))
(params (get def-info "params"))
(body (get def-info "body"))
@@ -295,10 +295,10 @@
;; 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))
(tests (filter (fn ((tv :as list)) (= (len tv) n-params)) smt-test-values))
;; Run tests
(results (map
(fn (test-vals)
(fn ((test-vals :as list))
(let ((env (merge model (smt-bind-params params test-vals)))
;; Evaluate body directly
(body-result (smt-eval body env))
@@ -311,9 +311,9 @@
:equal (= body-result call-result)}))
tests)))
{:name name
:status (if (every? (fn (r) (get r "equal")) results) "sat" "FAIL")
: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) (get r "equal")) results))
:tests-passed (len (filter (fn ((r :as dict)) (get r "equal")) results))
:tests-total (len results)
:sample (if (empty? results) nil (first results))}))))
@@ -325,16 +325,16 @@
;; Strip SMT-LIB comment lines (starting with ;) and return only actual forms.
;; Handles comments that contain ( characters.
(define smt-strip-comments
(fn (s)
(fn ((s :as string))
(let ((lines (split s "\n"))
(non-comment (filter
(fn (line) (not (starts-with? (trim line) ";")))
(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)
(fn ((smtlib-str :as string))
(let ((parsed (sx-parse (smt-strip-comments smtlib-str)))
(stmts (smt-extract-statements parsed))
(decls (get stmts "decls"))
@@ -351,7 +351,7 @@
{:status "unknown"
:reason "non-definitional assertion (needs full SMT solver)"}))
assertions)))
{:status (if (every? (fn (r) (= (get r "status") "sat")) results)
{:status (if (every? (fn ((r :as dict)) (= (get r "status") "sat")) results)
"sat" "unknown")
:assertions (len assertions)
:results results})))))
@@ -377,7 +377,7 @@
;; Batch verify: translate and prove all define-* forms
(define prove-file
(fn (exprs)
(fn ((exprs :as list))
(let ((translatable
(filter
(fn (expr)
@@ -396,7 +396,7 @@
(name (nth expr 1)))
(assoc proof "name" name)))
translatable))
(sat-count (len (filter (fn (r) (= (get r "status") "sat")) results)))
(sat-count (len (filter (fn ((r :as dict)) (= (get r "status") "sat")) results)))
(total (len results)))
{:total total
:sat sat-count
@@ -424,7 +424,7 @@
;; Default domain bounds by arity — balance coverage vs. combinatorics
(define prove-domain-for
(fn (arity)
(fn ((arity :as number))
(cond
(<= arity 1) (range -50 51) ;; 101 values
(= arity 2) (range -20 21) ;; 41^2 = 1,681 pairs
@@ -433,7 +433,7 @@
;; Cartesian product: all n-tuples from a domain
(define prove-tuples
(fn (domain arity)
(fn ((domain :as list) (arity :as number))
(if (<= arity 0) (list (list))
(if (= arity 1)
(map (fn (x) (list x)) domain)
@@ -441,12 +441,12 @@
(prove-tuples-expand domain sub (list)))))))
(define prove-tuples-expand
(fn (domain sub acc)
(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) (cons (first domain) t)) sub))))))
(map (fn ((t :as list)) (cons (first domain) t)) sub))))))
;; --------------------------------------------------------------------------
@@ -454,7 +454,7 @@
;; --------------------------------------------------------------------------
(define prove-call
(fn (f vals)
(fn ((f :as lambda) (vals :as list))
(let ((n (len vals)))
(cond
(= n 0) (f)
@@ -472,13 +472,13 @@
;; 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)
(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 given-fn tuples tested skipped)
(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))
@@ -505,7 +505,7 @@
;; Verify a single property via bounded model checking
(define prove-property
(fn (prop)
(fn ((prop :as dict))
(let ((name (get prop "name"))
(vars (get prop "vars"))
(test-fn (get prop "test"))
@@ -519,10 +519,10 @@
;; Batch verify a list of properties
(define prove-properties
(fn (props)
(fn ((props :as list))
(let ((results (map prove-property props))
(verified (filter (fn (r) (= (get r "status") "verified")) results))
(falsified (filter (fn (r) (= (get r "status") "falsified")) results)))
(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)
@@ -537,13 +537,13 @@
;; 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)
(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) (str "(" v " Int)")) vars)))
(map (fn ((v :as string)) (str "(" v " Int)")) vars)))
(holds-smt (z3-expr holds))
(body (if (nil? given-e)
holds-smt
@@ -556,7 +556,7 @@
;; Generate SMT-LIB for all properties, including necessary definitions
(define prove-properties-smtlib
(fn (props primitives-exprs)
(fn ((props :as list) (primitives-exprs :as list))
(let ((defs (z3-translate-file primitives-exprs))
(prop-smts (map prove-property-smtlib props)))
(str ";; ================================================================\n"