giles
c72a5af04d
Accumulated changes from WASM browser development sessions: - sx_runtime.ml: signal subscription + notify, env unwrap tolerance - sx_browser.bc.js: rebuilt js_of_ocaml browser kernel - sx_browser.bc.wasm.js + assets: WASM browser kernel build - sx-platform.js browser tests (test_js, test_platform, test_wasm) - Playwright sx-inspect.js: interactive page inspector tool - harness-web.sx: DOM assertion updates - deploy.sh, Dockerfile, dune-project: build config updates - test-stepper.sx: stepper unit tests - reader-macro-demo plan update Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
151 lines
13 KiB
Plaintext
151 lines
13 KiB
Plaintext
;; ---------------------------------------------------------------------------
|
|
;; Reader Macro Demo: #z3 — SX Spec to SMT-LIB (live translation via z3.sx)
|
|
;; ---------------------------------------------------------------------------
|
|
|
|
(defcomp ~plans/reader-macro-demo/z3-example (&key (sx-source :as string) (smt-output :as string))
|
|
(div :class "grid grid-cols-1 md:grid-cols-2 gap-4"
|
|
(div
|
|
(p :class "text-xs text-stone-500 uppercase tracking-wider mb-1" "SX Source")
|
|
(~docs/code :src (highlight sx-source "lisp")))
|
|
(div
|
|
(p :class "text-xs text-stone-500 uppercase tracking-wider mb-1" "SMT-LIB Output (live from z3.sx)")
|
|
(~docs/code :src (highlight smt-output "lisp")))))
|
|
|
|
(defcomp ~plans/reader-macro-demo/plan-reader-macro-demo-content ()
|
|
(~docs/page :title "Reader Macro Demo: #z3"
|
|
|
|
(~docs/section :title "The idea" :id "idea"
|
|
(p :class "text-stone-600"
|
|
"SX spec files (" (code "primitives.sx") ", " (code "eval.sx") ") are machine-readable declarations. Reader macros transform these at parse time. " (code "#z3") " reads a " (code "define-primitive") " declaration and emits " (a :href "https://smtlib.cs.uiowa.edu/" :class "text-violet-600 hover:underline" "SMT-LIB") " — the standard input language for " (a :href "https://github.com/Z3Prover/z3" :class "text-violet-600 hover:underline" "Z3") " and other theorem provers.")
|
|
(p :class "text-stone-600"
|
|
"Same source, two interpretations. The bootstrappers read " (code "define-primitive") " and emit executable code. " (code "#z3") " reads the same form and emits verification conditions. The specification is simultaneously a program and a proof obligation.")
|
|
(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" "Self-hosted")
|
|
(p :class "text-sm text-violet-700"
|
|
"The translator is written in SX itself (" (code "z3.sx") "). The SX evaluator executes " (code "z3.sx") " against the spec to produce SMT-LIB. Same pattern as " (code "bootstrap_js.py") " and " (code "bootstrap_py.py") ", but the transformation logic is an s-expression program transforming other s-expressions. All examples on this page are " (em "live output") " — not hardcoded strings.")))
|
|
|
|
(~docs/section :title "Arithmetic primitives" :id "arithmetic"
|
|
(p :class "text-stone-600"
|
|
"Primitives with " (code ":body") " generate " (code "forall") " assertions. Z3 can verify the definition is satisfiable.")
|
|
|
|
(~docs/subsection :title "inc"
|
|
(~plans/reader-macro-demo/z3-example
|
|
:sx-source "(define-primitive \"inc\"\n :params (n)\n :returns \"number\"\n :doc \"Increment by 1.\"\n :body (+ n 1))"
|
|
:smt-output #z3(define-primitive "inc" :params (n) :returns "number" :doc "Increment by 1." :body (+ n 1))))
|
|
|
|
(~docs/subsection :title "clamp"
|
|
(p :class "text-stone-600 mb-2"
|
|
(code "max") " and " (code "min") " have no SMT-LIB equivalent — translated to " (code "ite") " (if-then-else).")
|
|
(~plans/reader-macro-demo/z3-example
|
|
:sx-source "(define-primitive \"clamp\"\n :params (x lo hi)\n :returns \"number\"\n :doc \"Clamp x to range [lo, hi].\"\n :body (max lo (min hi x)))"
|
|
:smt-output #z3(define-primitive "clamp" :params (x lo hi) :returns "number" :doc "Clamp x to range [lo, hi]." :body (max lo (min hi x))))))
|
|
|
|
(~docs/section :title "Predicates" :id "predicates"
|
|
(p :class "text-stone-600"
|
|
"Predicates return " (code "Bool") " in SMT-LIB. " (code "mod") " and " (code "=") " are identity translations — same syntax in both languages.")
|
|
|
|
(~docs/subsection :title "odd?"
|
|
(~plans/reader-macro-demo/z3-example
|
|
:sx-source "(define-primitive \"odd?\"\n :params (n)\n :returns \"boolean\"\n :doc \"True if n is odd.\"\n :body (= (mod n 2) 1))"
|
|
:smt-output #z3(define-primitive "odd?" :params (n) :returns "boolean" :doc "True if n is odd." :body (= (mod n 2) 1))))
|
|
|
|
(~docs/subsection :title "!= (inequality)"
|
|
(~plans/reader-macro-demo/z3-example
|
|
:sx-source "(define-primitive \"!=\"\n :params (a b)\n :returns \"boolean\"\n :doc \"Inequality.\"\n :body (not (= a b)))"
|
|
:smt-output #z3(define-primitive "!=" :params (a b) :returns "boolean" :doc "Inequality." :body (not (= a b))))))
|
|
|
|
(~docs/section :title "Variadics and bodyless" :id "variadics"
|
|
(p :class "text-stone-600"
|
|
"Variadic primitives (" (code "&rest") ") are declared as uninterpreted functions — Z3 can reason about their properties but not their implementation. Primitives without " (code ":body") " get only a declaration.")
|
|
|
|
(~docs/subsection :title "+ (variadic)"
|
|
(~plans/reader-macro-demo/z3-example
|
|
:sx-source "(define-primitive \"+\"\n :params (&rest args)\n :returns \"number\"\n :doc \"Sum all arguments.\")"
|
|
:smt-output #z3(define-primitive "+" :params (&rest args) :returns "number" :doc "Sum all arguments.")))
|
|
|
|
(~docs/subsection :title "nil? (no body)"
|
|
(~plans/reader-macro-demo/z3-example
|
|
:sx-source "(define-primitive \"nil?\"\n :params (x)\n :returns \"boolean\"\n :doc \"True if x is nil/null/None.\")"
|
|
:smt-output #z3(define-primitive "nil?" :params (x) :returns "boolean" :doc "True if x is nil/null/None."))))
|
|
|
|
(~docs/section :title "Translate entire spec files" :id "full-specs"
|
|
(p :class "text-stone-600"
|
|
"The translator can process entire spec files. " (code "z3-translate-file") " in " (code "z3.sx") " filters for " (code "define-primitive") ", " (code "define-io-primitive") ", and " (code "define-special-form") " declarations, translates each, and concatenates the output.")
|
|
(p :class "text-stone-600"
|
|
"Below is the live SMT-LIB output from translating the full " (code "primitives.sx") " — all 87 primitive declarations. The composition is pure SX: " (code "(z3-translate-file (sx-parse (read-spec-file \"primitives.sx\")))") " — read the file, parse it, translate it. No Python glue.")
|
|
|
|
(~docs/subsection :title "primitives.sx (87 primitives)"
|
|
(~docs/code :src (highlight (z3-translate-file (sx-parse (read-spec-file "primitives.sx"))) "lisp"))))
|
|
|
|
(~docs/section :title "The translator: z3.sx" :id "z3-source"
|
|
(p :class "text-stone-600"
|
|
"The entire translator is a single SX file — s-expressions that walk other s-expressions and emit strings. No host language logic. The same file runs in Python (server) and could run in JavaScript (browser) via the bootstrapped evaluator.")
|
|
(~docs/code :src (highlight (read-spec-file "z3.sx") "lisp"))
|
|
(p :class "text-stone-600 mt-4"
|
|
"359 lines. The key functions: " (code "z3-sort") " maps SX types to SMT-LIB sorts. " (code "z3-expr") " recursively translates expressions — identity ops pass through unchanged, " (code "max") "/" (code "min") " become " (code "ite") ", predicates get renamed. " (code "z3-translate") " dispatches on form type. " (code "z3-translate-file") " filters and batch-translates."))
|
|
|
|
(~docs/section :title "The pattern: SX → anything" :id "sx-to-anything"
|
|
(p :class "text-stone-600"
|
|
"z3.sx proves the pattern: an SX program that transforms SX ASTs into a target language. The same pattern works for any target.")
|
|
(div :class "rounded border border-stone-200 bg-stone-50 p-4 mt-2 mb-4"
|
|
(table :class "w-full text-sm"
|
|
(thead (tr :class "text-left text-stone-500"
|
|
(th :class "pb-2 pr-4" "File")
|
|
(th :class "pb-2 pr-4" "Defines")
|
|
(th :class "pb-2 pr-4" "Reader macro")
|
|
(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" "z3.sx")
|
|
(td :class "py-2 pr-4 font-mono text-xs" "z3-translate")
|
|
(td :class "py-2 pr-4 font-mono text-xs" "#z3")
|
|
(td :class "py-2" "SMT-LIB (theorem prover)"))
|
|
(tr :class "text-stone-400 border-t border-stone-200"
|
|
(td :class "py-2 pr-4 font-mono text-xs" "py.sx")
|
|
(td :class "py-2 pr-4 font-mono text-xs" "py-translate")
|
|
(td :class "py-2 pr-4 font-mono text-xs" "#py")
|
|
(td :class "py-2" "Python source"))
|
|
(tr :class "text-stone-400 border-t border-stone-200"
|
|
(td :class "py-2 pr-4 font-mono text-xs" "js.sx")
|
|
(td :class "py-2 pr-4 font-mono text-xs" "js-translate")
|
|
(td :class "py-2 pr-4 font-mono text-xs" "#js")
|
|
(td :class "py-2" "JavaScript source"))
|
|
(tr :class "text-stone-400 border-t border-stone-200"
|
|
(td :class "py-2 pr-4 font-mono text-xs" "dot.sx")
|
|
(td :class "py-2 pr-4 font-mono text-xs" "dot-translate")
|
|
(td :class "py-2 pr-4 font-mono text-xs" "#dot")
|
|
(td :class "py-2" "Graphviz dot (dependency graphs)")))))
|
|
(p :class "text-stone-600"
|
|
"Each translator is a pure SX function from AST to string. Drop the " (code ".sx") " file in the ref directory, define " (code "name-translate") ", and " (code "#name") " works everywhere — server and client. No Python. No registration. No glue.")
|
|
(p :class "text-stone-600"
|
|
"A " (code "py.sx") " wouldn't be limited to the spec. Any SX expression could be translated: " (code "#py(map (fn (x) (* x x)) items)") " → " (code "list(map(lambda x: x * x, items))") ". The bootstrappers (" (code "bootstrap_js.py") ", " (code "bootstrap_py.py") ") are Python programs that do this for the full spec. " (code "py.sx") " would be the same thing, written in SX — a self-hosting bootstrapper."))
|
|
|
|
(~docs/section :title "How it works" :id "how-it-works"
|
|
(p :class "text-stone-600"
|
|
"The " (code "#z3") " reader macro is registered before parsing. When the parser hits " (code "#z3(define-primitive ...)") ", it:")
|
|
(ol :class "list-decimal pl-6 space-y-2 text-stone-600"
|
|
(li "Reads the identifier " (code "z3") " after " (code "#") ".")
|
|
(li "Looks for " (code "z3-translate") " in the component environment — found, because " (code "z3.sx") " was loaded at startup.")
|
|
(li "Reads the next expression — the full " (code "define-primitive") " form — into an AST node.")
|
|
(li "Calls the " (code "z3-translate") " Lambda with the AST.")
|
|
(li (code "z3.sx") " walks the AST, extracts " (code ":params") ", " (code ":returns") ", " (code ":body") ", and emits SMT-LIB.")
|
|
(li "The resulting string replaces " (code "#z3(...)") " in the parse output."))
|
|
(p :class "text-stone-600"
|
|
"No Python glue. The parser auto-resolves " (code "#name") " by looking for " (code "name-translate") " in the component env. Any " (code ".sx") " file that defines a " (code "name-translate") " function becomes a reader macro. A future " (code "py.sx") " defining " (code "py-translate") " would make " (code "#py") " work the same way — SX to Python.")
|
|
(p :class "text-stone-600"
|
|
"The handler is a pure function from AST to value. No side effects. No mutation. Reader macros are " (em "syntax transformations") " — they happen before evaluation, before rendering, before anything else. They are the earliest possible extension point."))
|
|
|
|
(~docs/section :title "The strange loop" :id "strange-loop"
|
|
(p :class "text-stone-600"
|
|
"The SX specification files are simultaneously:")
|
|
(ul :class "list-disc pl-6 space-y-2 text-stone-600"
|
|
(li (span :class "font-semibold" "Executable code") " — bootstrappers compile them to JavaScript and Python.")
|
|
(li (span :class "font-semibold" "Documentation") " — this docs site renders them with syntax highlighting and prose.")
|
|
(li (span :class "font-semibold" "Formal specifications") " — " (code "#z3") " extracts verification conditions that a theorem prover can check."))
|
|
(p :class "text-stone-600"
|
|
"One file. Three readings. No information lost. The " (code "define-primitive") " form in " (code "primitives.sx") " does not need to be translated, annotated, or re-expressed for any of these uses. The s-expression " (em "is") " the program, the documentation, and the proof obligation.")
|
|
(p :class "text-stone-600"
|
|
"And the reader macro that extracts proofs? It is itself written in SX — " (code "z3.sx") ", 359 lines of s-expressions that transform other s-expressions. The SX evaluator (bootstrapped from " (code "eval.sx") ") executes " (code "z3.sx") " against " (code "primitives.sx") " to produce SMT-LIB. The transformation tools are made of the same material as the things they transform.")
|
|
(p :class "text-stone-600"
|
|
"There is no " (code "reader_z3.py") ". No Python translation logic. The parser sees " (code "#z3") ", finds " (code "z3-translate") " in the component env (loaded from " (code "z3.sx") " at startup), and calls it. The full spec translation calls " (code "(z3-translate-file (sx-parse (read-spec-file ...)))") " — three SX functions composed together. Same evaluator. Same translator. Same source. Different reader."))))
|