rose-ash

coop/rose-ash

Fork 0

Commit Graph

Author	SHA1	Message	Date
giles	b99e69d1bb	Add (param :as type) annotations to all fn/lambda params across SX spec 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>	2026-03-11 20:27:36 +00:00
giles	00e7ba4650	Add theorem prover docs page with Phase 2 constraint solving Some checks failed Build and Deploy / build-and-deploy (push) Has been cancelled Details - 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>	2026-03-08 23:17:09 +00:00
giles	3ca89ef765	Self-hosted z3.sx translator, prove.sx prover, parser unicode, auto reader macros - z3.sx: SX-to-SMT-LIB translator written in SX (359 lines), replaces Python translation logic - prove.sx: SMT-LIB satisfiability checker in SX — proves all 91 primitives sat by construction - Parser: support unicode characters (em-dash, accented letters) in symbols - Auto-resolve reader macros: #name finds name-translate in component env, no Python registration - Platform primitives: type-of, symbol-name, keyword-name, sx-parse registered in primitives.py - Cond heuristic: predicates ending in ? recognized as Clojure-style tests - Library loading: z3.sx loaded at startup with reload callbacks for hot-reload ordering - reader_z3.py: rewritten as thin shell delegating to z3.sx - Split monolithic .sx files: essays (22), plans (13), reactive-islands (6) into separate files Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>	2026-03-08 22:47:53 +00:00

Author

SHA1

Message

Date

giles

b99e69d1bb

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

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>

2026-03-11 20:27:36 +00:00

giles

00e7ba4650

Add theorem prover docs page with Phase 2 constraint solving

Build and Deploy / build-and-deploy (push) Has been cancelled

Details

- 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>

2026-03-08 23:17:09 +00:00

giles

3ca89ef765

Self-hosted z3.sx translator, prove.sx prover, parser unicode, auto reader macros

- z3.sx: SX-to-SMT-LIB translator written in SX (359 lines), replaces Python translation logic
- prove.sx: SMT-LIB satisfiability checker in SX — proves all 91 primitives sat by construction
- Parser: support unicode characters (em-dash, accented letters) in symbols
- Auto-resolve reader macros: #name finds name-translate in component env, no Python registration
- Platform primitives: type-of, symbol-name, keyword-name, sx-parse registered in primitives.py
- Cond heuristic: predicates ending in ? recognized as Clojure-style tests
- Library loading: z3.sx loaded at startup with reload callbacks for hot-reload ordering
- reader_z3.py: rewritten as thin shell delegating to z3.sx
- Split monolithic .sx files: essays (22), plans (13), reactive-islands (6) into separate files

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

2026-03-08 22:47:53 +00:00

3 Commits