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

Add spec explorer plan to sx-docs plans section

Browse Source 
New plan page at /etc/plans/spec-explorer describing the "fifth ring"
architecture: SX exploring itself through per-function cards showing
source, Python/JS/Z3 translations, platform deps, tests, proofs, and
usage examples.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
This commit is contained in:
giles
2026-03-12 00:05:45 +00:00
parent 4e96997e09
commit e046542aa0
4 changed files with 225 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
sx/sx/nav-data.sx
View File

@@ -204,7 +204,9 @@
(dict :label "Generative SX" :href "/etc/plans/generative-sx"
:summary "Programs that write themselves as they run — self-compiling specs, runtime self-extension, generative testing, seed networks.")
(dict :label "Art DAG on SX" :href "/etc/plans/art-dag-sx"
:summary "SX endpoints as portals into media processing environments — recipes as programs, split execution across GPU/cache/live boundaries, streaming AV output.")))
:summary "SX endpoints as portals into media processing environments — recipes as programs, split execution across GPU/cache/live boundaries, streaming AV output.")
(dict :label "Spec Explorer" :href "/etc/plans/spec-explorer"
:summary "The fifth ring — SX exploring itself. Per-function cards showing source, Python/JS/Z3 translations, platform dependencies, tests, proofs, and usage examples.")))
(define reactive-islands-nav-items (list
(dict :label "Overview" :href "/geography/reactive/"

213
sx/sx/plans/spec-explorer.sx Normal file
View File

@@ -0,0 +1,213 @@
;; ---------------------------------------------------------------------------
;; Spec Explorer — The Fifth Ring
;; ---------------------------------------------------------------------------
(defcomp ~plan-spec-explorer-content ()
(~doc-page :title "Spec Explorer"
(~doc-section :title "The Five Rings" :id "five-rings"
(p "SX has a peculiar architecture. At its centre sits a specification — a set of s-expression files that define the language. Not a description of the language. Not documentation about the language. The specification " (em "is") " the language. It is simultaneously a formal definition and executable code. You can read it as a document or run it as a program. It does not describe how to build an SX evaluator; it " (em "is") " an SX evaluator, expressed in the language it defines.")
(p "This is the nucleus. Everything else radiates outward from it.")
(div :class "space-y-3 my-4"
(div :class "rounded border border-violet-200 bg-violet-50/50 p-4"
(div :class "flex items-center gap-2 mb-1"
(span :class "inline-block px-2 py-0.5 rounded text-xs font-bold bg-violet-600 text-white" "1")
(span :class "font-semibold text-stone-800" "The Nucleus"))
(p :class "text-sm text-stone-600" "The spec itself — " (code "shared/sx/ref/*.sx") ". Fourteen files, 180+ functions with type and effect annotations. Each function is simultaneously a formal definition and executable code."))
(div :class "rounded border border-sky-200 bg-sky-50/50 p-4"
(div :class "flex items-center gap-2 mb-1"
(span :class "inline-block px-2 py-0.5 rounded text-xs font-bold bg-sky-600 text-white" "2")
(span :class "font-semibold text-stone-800" "The Bootstrapper Ring"))
(p :class "text-sm text-stone-600" "Translators that read the spec and emit native implementations. " (code "bootstrap_py.py") " emits Python. " (code "js.sx") " emits JavaScript. " (code "z3.sx") " emits SMT-LIB verification conditions. The spec's knowledge is preserved in every translation. Nothing is added, nothing is lost."))
(div :class "rounded border border-rose-200 bg-rose-50/50 p-4"
(div :class "flex items-center gap-2 mb-1"
(span :class "inline-block px-2 py-0.5 rounded text-xs font-bold bg-rose-500 text-white" "3")
(span :class "font-semibold text-stone-800" "The Bridge Ring"))
(p :class "text-sm text-stone-600" "The platform boundary — " (code "boundary.sx") " is literally the membrane between the made world (the spec) and the found world (the host environment). It declares what the host must provide so the spec can function. Each spec function's dependencies trace back to either other spec functions or platform primitives."))
(div :class "rounded border border-amber-200 bg-amber-50/50 p-4"
(div :class "flex items-center gap-2 mb-1"
(span :class "inline-block px-2 py-0.5 rounded text-xs font-bold bg-amber-500 text-white" "4")
(span :class "font-semibold text-stone-800" "The Runtime Ring"))
(p :class "text-sm text-stone-600" "Bootstrapped spec + platform bridge = working system. Tests verify behaviour. " (code "prove.sx") " verifies algebraic properties by bounded model checking. " (code "z3.sx") " translates to SMT-LIB for unbounded proofs. The spec doesn't just claim to work — it proves it."))
(div :class "rounded border border-green-200 bg-green-50/50 p-4"
(div :class "flex items-center gap-2 mb-1"
(span :class "inline-block px-2 py-0.5 rounded text-xs font-bold bg-green-600 text-white" "5")
(span :class "font-semibold text-stone-800" "The Application Ring"))
(p :class "text-sm text-stone-600" "This website — rendering the spec's source code using the runtime the spec produced, displayed in components written in the language the spec defines, navigated by an engine the spec specifies. The documentation is the thing documenting itself.")))
(p "The spec explorer makes all five rings visible for every function."))
;; -----------------------------------------------------------------------
;; What the explorer shows
;; -----------------------------------------------------------------------
(~doc-section :title "Per-Function Cards" :id "cards"
(p "Each function in the spec gets a card showing all five rings:")
(div :class "overflow-x-auto rounded border border-stone-200 mb-4"
(table :class "w-full text-left text-sm"
(thead (tr :class "border-b border-stone-200 bg-stone-100"
(th :class "px-3 py-2 font-medium text-stone-600" "Ring")
(th :class "px-3 py-2 font-medium text-stone-600" "Panel")
(th :class "px-3 py-2 font-medium text-stone-600" "Content")))
(tbody
(tr :class "border-b border-stone-100"
(td :class "px-3 py-2"
(span :class "inline-block px-2 py-0.5 rounded text-xs font-bold bg-violet-600 text-white" "1"))
(td :class "px-3 py-2 font-semibold text-stone-700" "Nucleus")
(td :class "px-3 py-2 text-stone-600" "SX source with syntax highlighting. Effect badges (pure/mutation/io/render). Typed parameter list."))
(tr :class "border-b border-stone-100"
(td :class "px-3 py-2"
(span :class "inline-block px-2 py-0.5 rounded text-xs font-bold bg-sky-600 text-white" "2"))
(td :class "px-3 py-2 font-semibold text-stone-700" "Translations")
(td :class "px-3 py-2 text-stone-600" "Collapsible panels showing the same function in Python, JavaScript, and Z3/SMT-LIB. Each generated by the actual bootstrappers — not hand-written."))
(tr :class "border-b border-stone-100"
(td :class "px-3 py-2"
(span :class "inline-block px-2 py-0.5 rounded text-xs font-bold bg-rose-500 text-white" "3"))
(td :class "px-3 py-2 font-semibold text-stone-700" "Bridge")
(td :class "px-3 py-2 text-stone-600" "Cross-references: which spec functions and platform primitives this function depends on. Platform deps marked with " (code "\u2B21") "."))
(tr :class "border-b border-stone-100"
(td :class "px-3 py-2"
(span :class "inline-block px-2 py-0.5 rounded text-xs font-bold bg-amber-500 text-white" "4"))
(td :class "px-3 py-2 font-semibold text-stone-700" "Runtime")
(td :class "px-3 py-2 text-stone-600" "Tests matched from " (code "test-*.sx") " files. Proof status from " (code "prove.sx") " — sat/unknown/n/a. Algebraic properties that reference this function."))
(tr :class "border-b border-stone-100"
(td :class "px-3 py-2"
(span :class "inline-block px-2 py-0.5 rounded text-xs font-bold bg-green-600 text-white" "5"))
(td :class "px-3 py-2 font-semibold text-stone-700" "Examples")
(td :class "px-3 py-2 text-stone-600" "Usage examples extracted from comments, test assertions, and curated examples. Living documentation."))))))
;; -----------------------------------------------------------------------
;; Effect system
;; -----------------------------------------------------------------------
(~doc-section :title "Effect Annotations" :id "effects"
(p "Every function in the spec now carries an " (code ":effects") " annotation declaring what kind of side effects it performs:")
(div :class "flex flex-wrap gap-3 my-4"
(span :class "inline-flex items-center gap-1 px-3 py-1 rounded bg-green-100 text-green-700 text-sm font-medium" "pure " (code ":effects []"))
(span :class "inline-flex items-center gap-1 px-3 py-1 rounded bg-amber-100 text-amber-700 text-sm font-medium" "mutation " (code ":effects [mutation]"))
(span :class "inline-flex items-center gap-1 px-3 py-1 rounded bg-orange-100 text-orange-700 text-sm font-medium" "io " (code ":effects [io]"))
(span :class "inline-flex items-center gap-1 px-3 py-1 rounded bg-sky-100 text-sky-700 text-sm font-medium" "render " (code ":effects [render]")))
(p "The explorer shows effect badges on each function card, and the stats bar aggregates them across the whole file. Pure functions (green) are the nucleus — no side effects, fully deterministic, safe to cache, reorder, or parallelise.")
(~doc-code :code (highlight "(define signal :effects []\n (fn ((initial-value :as any))\n (make-signal initial-value)))\n\n(define reset! :effects [mutation]\n (fn ((s :as signal) value)\n (when (signal? s)\n (let ((old (signal-value s)))\n (when (not (identical? old value))\n (signal-set-value! s value)\n (notify-subscribers s))))))" "sx")))
;; -----------------------------------------------------------------------
;; Bootstrapper translations
;; -----------------------------------------------------------------------
(~doc-section :title "Bootstrapper Translations" :id "translations"
(p "Each function is translated by the actual bootstrappers that build the production runtime. The same " (code "signal") " function shown in three target languages:")
(~doc-subsection :title "Python (via bootstrap_py.py)"
(~doc-code :code (highlight "def signal(initial_value):\n return make_signal(initial_value)" "python"))
(p :class "text-sm text-stone-500" (code "PyEmitter._emit_define()") " — the exact same code path that generates " (code "sx_ref.py") "."))
(~doc-subsection :title "JavaScript (via js.sx)"
(~doc-code :code (highlight "var signal = function(initial_value) {\n return make_signal(initial_value);\n};" "javascript"))
(p :class "text-sm text-stone-500" (code "js-emit-define") " — the self-hosting JS bootstrapper, written in SX, evaluated by the Python evaluator."))
(~doc-subsection :title "Z3 / SMT-LIB (via z3.sx)"
(~doc-code :code (highlight "; signal — Create a reactive signal container with an initial value.\n(declare-fun signal (Value) Value)" "lisp"))
(p :class "text-sm text-stone-500" (code "z3-translate") " — the first self-hosted bootstrapper, translating spec declarations to verification conditions for theorem provers.")))
;; -----------------------------------------------------------------------
;; Testing and proving
;; -----------------------------------------------------------------------
(~doc-section :title "Tests and Proofs" :id "runtime"
(p "Ring 4 shows that the spec does what it claims.")
(~doc-subsection :title "Tests"
(p "Test files (" (code "test-signals.sx") ", " (code "test-eval.sx") ", etc.) use the " (code "defsuite") "/" (code "deftest") " framework. The explorer matches tests to functions by suite name and shows them on the function card.")
(~doc-code :code (highlight "(defsuite \"signal basics\"\n (deftest \"creates signal with value\"\n (let ((s (signal 42)))\n (assert-equal (deref s) 42)))\n (deftest \"reset changes value\"\n (let ((s (signal 0)))\n (reset! s 99)\n (assert-equal (deref s) 99))))" "sx")))
(~doc-subsection :title "Proofs"
(p (code "prove.sx") " verifies algebraic properties of SX primitives by bounded model checking. For each " (code "define-primitive") " with a " (code ":body") ", " (code "prove-translate") " translates to SMT-LIB and verifies satisfiability by construction.")
(p "Properties from the " (code "sx-properties") " library are matched to functions and shown on their cards:")
(~doc-code :code (highlight ";; prove.sx property: +-commutative\n{:name \"+-commutative\"\n :vars (list \"a\" \"b\")\n :test (fn (a b) (= (+ a b) (+ b a)))\n :holds '(= (+ a b) (+ b a))}\n\n;; Result: verified — 1,681 ground instances tested" "sx"))))
;; -----------------------------------------------------------------------
;; Architecture
;; -----------------------------------------------------------------------
(~doc-section :title "Implementation" :id "implementation"
(p "Three layers, three increments.")
(~doc-subsection :title "Layer 1: Python helper"
(p (code "spec-explorer-data(slug)") " in " (code "helpers.py") " — parses a " (code ".sx") " spec file via " (code "parse_all()") ", extracts sections/defines/effects/params, calls each bootstrapper for per-function translations, matches tests, runs proofs.")
(p "This is the only new Python code. Everything else is SX components."))
(~doc-subsection :title "Layer 2: SX components"
(p (code "specs-explorer.sx") " — 12-15 " (code "defcomp") " components rendering the structured data:")
(div :class "overflow-x-auto"
(pre :class "text-xs bg-stone-100 rounded p-3"
(code "~spec-explorer-content top-level, receives parsed data\n ~spec-explorer-header filename, title, source link\n ~spec-explorer-stats aggregate badges: effects, tests, proofs\n ~spec-explorer-toc section table of contents\n ~spec-explorer-section one section with its defines\n ~spec-explorer-define one function card (all five rings)\n ~spec-effect-badge colored effect badge\n ~spec-param-list typed parameter list\n ~spec-ring-translations SX / Python / JS / Z3 panels\n ~spec-ring-bridge cross-references + platform deps\n ~spec-ring-runtime tests + proofs\n ~spec-ring-examples usage examples\n ~spec-platform-interface platform primitives table"))))
(~doc-subsection :title "Layer 3: Routing"
(p "New route at " (code "/language/specs/explore/<slug>") " — parallel to existing raw source at " (code "/language/specs/<slug>") ". Each spec page gets an \"Explore\" link; the explorer gets a \"Source\" link.")))
;; -----------------------------------------------------------------------
;; Increments
;; -----------------------------------------------------------------------
(~doc-section :title "Incremental Delivery" :id "increments"
(div :class "space-y-4"
(div :class "rounded border border-stone-200 p-4"
(div :class "flex items-center gap-2 mb-2"
(span :class "inline-block px-2 py-0.5 rounded text-xs font-bold bg-violet-600 text-white uppercase" "Inc 1")
(span :class "font-semibold text-stone-800" "Core + Translations (Ring 1-2)"))
(ul :class "list-disc pl-5 text-sm text-stone-600 space-y-1"
(li (code "_spec_explorer_data()") " — sections, defines, effects, params, source extraction")
(li "Python translation via " (code "PyEmitter._emit_define()"))
(li "JavaScript translation via " (code "js-emit-define") " (from " (code "run_js_sx.py") ")")
(li "Z3 translation via " (code "z3-translate") " (from " (code "z3.sx") ")")
(li "Explorer components + translation panels + routing")
(li "Test with " (code "signals.sx"))))
(div :class "rounded border border-stone-200 p-4"
(div :class "flex items-center gap-2 mb-2"
(span :class "inline-block px-2 py-0.5 rounded text-xs font-bold bg-sky-600 text-white uppercase" "Inc 2")
(span :class "font-semibold text-stone-800" "Bridge + Runtime (Ring 3-4)"))
(ul :class "list-disc pl-5 text-sm text-stone-600 space-y-1"
(li "Cross-reference index: function\u2192slug mapping across all spec files")
(li "Platform dependency detection (ref not in index = platform primitive)")
(li "Test file parsing: " (code "defsuite") "/" (code "deftest") " structure extraction")
(li "Test-to-function matching")
(li "Proof generation via " (code "prove-translate"))
(li "Property matching from " (code "sx-properties"))))
(div :class "rounded border border-stone-200 p-4"
(div :class "flex items-center gap-2 mb-2"
(span :class "inline-block px-2 py-0.5 rounded text-xs font-bold bg-green-600 text-white uppercase" "Inc 3")
(span :class "font-semibold text-stone-800" "Examples + Polish (Ring 5)"))
(ul :class "list-disc pl-5 text-sm text-stone-600 space-y-1"
(li "Example extraction from comments + test assertions")
(li "Curated examples for key functions")
(li "Stats bar with aggregate counts")
(li "Table of contents with anchor links")
(li "Platform interface table")
(li "View switcher links between source and explorer")))))
;; -----------------------------------------------------------------------
;; The strange loop
;; -----------------------------------------------------------------------
(~doc-section :title "The Strange Loop" :id "strange-loop"
(p "When you view " (code "/language/specs/explore/eval") ", what happens is this:")
(ol :class "list-decimal pl-5 text-stone-700 space-y-2"
(li "The SX evaluator — bootstrapped from " (code "eval.sx") " — evaluates the page definition.")
(li "The page calls " (code "spec-explorer-data(\"eval\")") ", which parses " (code "eval.sx") " using " (code "parse_all()") " — itself bootstrapped from " (code "parser.sx") ".")
(li "The parsed AST is fed to " (code "PyEmitter") " and " (code "js-emit-define") " — the same bootstrappers that produced the running evaluator.")
(li "The resulting data is rendered by SX components, written in the language " (code "eval.sx") " defines, evaluated by the runtime " (code "eval.sx") " produced.")
(li "The components use " (code "highlight") " to syntax-highlight the SX source — which is the source of the evaluator that's currently running the highlight function."))
(p "The evaluator evaluates its own definition. The parser parses its own grammar. The bootstrapper translates its own translator. The documentation documents the thing doing the documenting.")
(p "This is not a metaphor. It is the literal execution path."))))

9
sx/sx/plans/status.sx
View File

@@ -132,7 +132,14 @@
(span :class "inline-block px-2 py-0.5 rounded text-xs font-bold bg-green-600 text-white uppercase" "Complete")
(a :href "/geography/isomorphism/" :class "font-semibold text-stone-800 underline" "Isomorphic Phase 7: Full Isomorphism"))
(p :class "text-sm text-stone-600" "Affinity annotations, render plans, optimistic data updates, offline mutation queue, isomorphic testing harness, universal page descriptor.")
(p :class "text-sm text-stone-500 mt-1" "All 6 sub-phases (7a–7f) complete."))))))
(p :class "text-sm text-stone-500 mt-1" "All 6 sub-phases (7a–7f) complete."))
(div :class "rounded border border-stone-200 bg-stone-50 p-4"
(div :class "flex items-center gap-2 mb-1"
(span :class "inline-block px-2 py-0.5 rounded text-xs font-bold bg-stone-500 text-white uppercase" "Not Started")
(a :href "/etc/plans/spec-explorer" :class "font-semibold text-stone-800 underline" "Spec Explorer — The Fifth Ring"))
(p :class "text-sm text-stone-600" "SX exploring itself. Per-function cards showing all five rings: SX source (nucleus), Python/JS/Z3 translations (bootstrapper), platform dependencies (bridge), tests and proofs (runtime), and usage examples (application). The documentation is the thing documenting itself.")
(p :class "text-sm text-stone-500 mt-1" "Prerequisite complete: 180+ functions annotated with :effects across all 14 spec files. Three increments: core + translations, bridge + runtime, examples + polish."))))))
;; ---------------------------------------------------------------------------
;; Fragment Protocol

1
sx/sxc/pages/docs.sx
View File

@@ -557,6 +557,7 @@
"wasm-bytecode-vm" (~plan-wasm-bytecode-vm-content)
"generative-sx" (~plan-generative-sx-content)
"art-dag-sx" (~plan-art-dag-sx-content)
"spec-explorer" (~plan-spec-explorer-content)
:else (~plans-index-content))))
;; ---------------------------------------------------------------------------