Fix bracket highlighting: both ( and ) share open step index

When a tag's open step is evaluated, both its opening and closing brackets go big+bold together. Previously close ) had the close step index so it stayed faint until much later. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Reactive code view stepper for home page
2026-03-14 22:00:43 +00:00 · 2026-03-14 21:58:42 +00:00 · 2026-03-14 21:21:14 +00:00 · 2026-03-14 20:43:57 +00:00 · 2026-03-14 20:40:24 +00:00 · 2026-03-14 20:33:40 +00:00
17 changed files with 1747 additions and 671 deletions
--- a/shared/infrastructure/factory.py
+++ b/shared/infrastructure/factory.py
@@ -49,6 +49,7 @@ def create_base_app(
    domain_services_fn: Callable[[], None] | None = None,
    no_oauth: bool = False,
    no_db: bool = False,
+    css_extras: Sequence[str] | None = None,
 ) -> Quart:
    """
    Create a Quart app with shared infrastructure.
@@ -139,17 +140,24 @@ def create_base_app(
    _styles = BASE_DIR / "static" / "styles"
    _fa_css = BASE_DIR / "static" / "fontawesome" / "css"
    if (_styles / "tw.css").exists() and not registry_loaded():
-        load_css_registry(
-            _styles / "tw.css",
-            extra_css=[
+        if css_extras is None:
+            # Legacy default: all shared CSS for blog/market/etc apps
+            _extra = [
                _styles / "basics.css",
                _styles / "cards.css",
                _styles / "blog-content.css",
                _styles / "prism.css",
                _fa_css / "all.min.css",
                _fa_css / "v4-shims.min.css",
-            ],
-            url_rewrites={"../webfonts/": "/static/fontawesome/webfonts/"},
+            ]
+            _rewrites = {"../webfonts/": "/static/fontawesome/webfonts/"}
+        else:
+            _extra = [_styles / e if "/" not in e else e for e in css_extras]
+            _rewrites = {}
+        load_css_registry(
+            _styles / "tw.css",
+            extra_css=_extra,
+            url_rewrites=_rewrites,
        )

    # Dev-mode: auto-reload sx templates when files change on disk
--- a/shared/static/scripts/sx-browser.js
+++ b/shared/static/scripts/sx-browser.js
--- a/shared/sx/ref/adapter-dom.sx
+++ b/shared/sx/ref/adapter-dom.sx
@@ -952,7 +952,7 @@
                (dom-set-attr el k (str (dict-get attrs k))))
                extra-keys)
              ;; Flush any newly collected CSS rules to live stylesheet
-              (flush-cssx-to-dom))
+              (run-post-render-hooks))
            ;; No longer a spread — clear tracked state
            (do
              (set! prev-classes (list))
--- a/shared/sx/ref/boot.sx
+++ b/shared/sx/ref/boot.sx
@@ -88,7 +88,7 @@
          (process-elements el)
          (sx-hydrate-elements el)
          (sx-hydrate-islands el)
-          (flush-cssx-to-dom))))))
+          (run-post-render-hooks))))))


 ;; --------------------------------------------------------------------------
@@ -120,7 +120,7 @@
            (process-elements el)
            (sx-hydrate-elements el)
            (sx-hydrate-islands el)
-            (flush-cssx-to-dom)
+            (run-post-render-hooks)
            (dom-dispatch el "sx:resolved" {:id id})))
        (log-warn (str "resolveSuspense: no element for id=" id))))))

@@ -418,29 +418,34 @@


 ;; --------------------------------------------------------------------------
-;; CSSX live flush — inject collected CSS rules into the DOM
+;; Render hooks — generic pre/post callbacks for hydration, swap, mount.
+;; The spec calls these at render boundaries; the app decides what to do.
+;; Pre-render: setup before DOM changes (e.g. prepare state).
+;; Post-render: cleanup after DOM changes (e.g. flush collected CSS).
 ;; --------------------------------------------------------------------------
-;;
-;; ~cssx/tw collects CSS rules via collect!("cssx" ...) during rendering.
-;; On the server, ~cssx/flush emits a batch <style> tag. On the client,
-;; islands render independently and no batch flush runs. This function
-;; injects any unflushed rules into a persistent <style> element in <head>.
-;; Called after hydration (boot + post-swap) to cover all render paths.

-(define flush-cssx-to-dom :effects [mutation io]
+(define *pre-render-hooks* (list))
+(define *post-render-hooks* (list))
+
+(define register-pre-render-hook :effects [mutation]
+  (fn ((hook-fn :as lambda))
+    (append! *pre-render-hooks* hook-fn)))
+
+(define register-post-render-hook :effects [mutation]
+  (fn ((hook-fn :as lambda))
+    (append! *post-render-hooks* hook-fn)))
+
+(define run-pre-render-hooks :effects [mutation io]
  (fn ()
-    (let ((rules (collected "cssx")))
-      (when (not (empty? rules))
-        (let ((style (or (dom-query "#sx-cssx-live")
-                         (let ((s (dom-create-element "style" nil)))
-                           (dom-set-attr s "id" "sx-cssx-live")
-                           (dom-set-attr s "data-cssx" "")
-                           (dom-append-to-head s)
-                           s))))
-          (dom-set-prop style "textContent"
-            (str (or (dom-get-prop style "textContent") "")
-                 (join "" rules))))
-        (clear-collected! "cssx")))))
+    (for-each (fn (hook) (cek-call hook nil)) *pre-render-hooks*)))
+
+(define run-post-render-hooks :effects [mutation io]
+  (fn ()
+    (log-info "run-post-render-hooks:" (len *post-render-hooks*) "hooks")
+    (for-each (fn (hook)
+      (log-info "  hook type:" (type-of hook) "callable:" (callable? hook) "lambda:" (lambda? hook))
+      (cek-call hook nil))
+      *post-render-hooks*)))


 ;; --------------------------------------------------------------------------
@@ -464,7 +469,7 @@
      (process-sx-scripts nil)
      (sx-hydrate-elements nil)
      (sx-hydrate-islands nil)
-      (flush-cssx-to-dom)
+      (run-post-render-hooks)
      (process-elements nil))))


--- a/shared/sx/ref/js.sx
+++ b/shared/sx/ref/js.sx
@@ -618,7 +618,7 @@
      (if (not (nil? renamed))
        renamed
        ;; General mangling rules
-        (let ((result name))
+        (let ((result (replace name "*" "_")))
          ;; Handle trailing ? and !
          (let ((result (cond
                  (ends-with? result "?")
@@ -1422,23 +1422,27 @@
                             (= (keyword-name (nth expr 2)) "effects"))
                      (nth expr 4)
                      (nth expr 2))))
-      (if (nil? val-expr)
-        (str "var " (js-mangle name) " = NIL;")
-        ;; Detect zero-arg self-tail-recursive functions → while loops
-        (if (and (list? val-expr)
-                 (not (empty? val-expr))
-                 (= (type-of (first val-expr)) "symbol")
-                 (or (= (symbol-name (first val-expr)) "fn")
-                     (= (symbol-name (first val-expr)) "lambda"))
-                 (list? (nth val-expr 1))
-                 (= (len (nth val-expr 1)) 0)
-                 (js-is-self-tail-recursive? name (rest (rest val-expr))))
-          ;; While loop optimization
-          (let ((body (rest (rest val-expr)))
-                (loop-body (js-emit-loop-body name body)))
-            (str "var " (js-mangle name) " = function() { while(true) { " loop-body " } };"))
-          ;; Normal define
-          (str "var " (js-mangle name) " = " (js-expr val-expr) ";"))))))
+      (let ((mangled (js-mangle name))
+            (var-decl
+              (if (nil? val-expr)
+                (str "var " (js-mangle name) " = NIL;")
+                ;; Detect zero-arg self-tail-recursive functions → while loops
+                (if (and (list? val-expr)
+                         (not (empty? val-expr))
+                         (= (type-of (first val-expr)) "symbol")
+                         (or (= (symbol-name (first val-expr)) "fn")
+                             (= (symbol-name (first val-expr)) "lambda"))
+                         (list? (nth val-expr 1))
+                         (= (len (nth val-expr 1)) 0)
+                         (js-is-self-tail-recursive? name (rest (rest val-expr))))
+                  ;; While loop optimization
+                  (let ((body (rest (rest val-expr)))
+                        (loop-body (js-emit-loop-body name body)))
+                    (str "var " mangled " = function() { while(true) { " loop-body " } };"))
+                  ;; Normal define
+                  (str "var " mangled " = " (js-expr val-expr) ";")))))
+        ;; Self-register: every spec define is available to evaluated SX code
+        (str var-decl "\nPRIMITIVES[\"" name "\"] = " mangled ";")))))


 ;; --------------------------------------------------------------------------
--- a/shared/sx/ref/orchestration.sx
+++ b/shared/sx/ref/orchestration.sx
@@ -460,7 +460,7 @@
    (sx-process-scripts root)
    (sx-hydrate root)
    (sx-hydrate-islands root)
-    (flush-cssx-to-dom)
+    (run-post-render-hooks)
    (process-elements root)))


@@ -871,7 +871,7 @@
      (hoist-head-elements-full target)
      (process-elements target)
      (sx-hydrate-elements target)
-      (flush-cssx-to-dom)
+      (run-post-render-hooks)
      (dom-dispatch target "sx:clientRoute"
        (dict "pathname" pathname))
      (log-info (str "sx:route client " pathname)))))
--- a/shared/sx/ref/platform_js.py
+++ b/shared/sx/ref/platform_js.py
@@ -1508,6 +1508,20 @@ CEK_FIXUPS_JS = '''
    while (!cekTerminal_p(state)) { state = cekStep(state); }
    return cekValue(state);
  };
+
+  // Platform functions — defined in platform_js.py, not in .sx spec files.
+  // Spec defines self-register via js-emit-define; these are the platform interface.
+  PRIMITIVES["type-of"] = typeOf;
+  PRIMITIVES["symbol-name"] = symbolName;
+  PRIMITIVES["keyword-name"] = keywordName;
+  PRIMITIVES["callable?"] = isCallable;
+  PRIMITIVES["lambda?"] = isLambda;
+  PRIMITIVES["lambda-name"] = lambdaName;
+  PRIMITIVES["component?"] = isComponent;
+  PRIMITIVES["island?"] = isIsland;
+  PRIMITIVES["make-symbol"] = function(n) { return new Symbol(n); };
+  PRIMITIVES["is-html-tag?"] = function(n) { return HTML_TAGS.indexOf(n) >= 0; };
+  PRIMITIVES["make-env"] = function() { return merge(componentEnv, PRIMITIVES); };
 '''


@@ -1798,8 +1812,8 @@ PLATFORM_DOM_JS = """
    // If lambda takes 0 params, call without event arg (convenience for on-click handlers)
    var wrapped = isLambda(handler)
      ? (lambdaParams(handler).length === 0
-        ? function(e) { try { cekCall(handler, NIL); } catch(err) { console.error("[sx-ref] domListen handler error:", name, err); } }
-        : function(e) { try { cekCall(handler, [e]); } catch(err) { console.error("[sx-ref] domListen handler error:", name, err); } })
+        ? function(e) { try { cekCall(handler, NIL); } catch(err) { console.error("[sx-ref] domListen handler error:", name, err); } finally { runPostRenderHooks(); } }
+        : function(e) { try { cekCall(handler, [e]); } catch(err) { console.error("[sx-ref] domListen handler error:", name, err); } finally { runPostRenderHooks(); } })
      : handler;
    if (name === "click") logInfo("domListen: click on <" + (el.tagName||"?").toLowerCase() + "> text=" + (el.textContent||"").substring(0,20) + " isLambda=" + isLambda(handler));
    el.addEventListener(name, wrapped);
@@ -1807,7 +1821,7 @@ PLATFORM_DOM_JS = """
  }

  function eventDetail(e) {
-    return (e && e.detail != null) ? e.detail : nil;
+    return (e && e.detail != null) ? e.detail : NIL;
  }

  function domQuery(sel) {
@@ -1852,7 +1866,7 @@ PLATFORM_DOM_JS = """
    if (el) { if (!el._sxData) el._sxData = {}; el._sxData[key] = val; }
  }
  function domGetData(el, key) {
-    return (el && el._sxData) ? (el._sxData[key] != null ? el._sxData[key] : nil) : nil;
+    return (el && el._sxData) ? (el._sxData[key] != null ? el._sxData[key] : NIL) : NIL;
  }
  function domInnerHtml(el) {
    return (el && el.innerHTML != null) ? el.innerHTML : "";
@@ -3033,6 +3047,9 @@ def fixups_js(has_html, has_sx, has_dom, has_signals=False, has_deps=False, has_
  if (typeof domOuterHtml === "function") PRIMITIVES["dom-outer-html"] = domOuterHtml;
  if (typeof domInnerHtml === "function") PRIMITIVES["dom-inner-html"] = domInnerHtml;
  if (typeof domTextContent === "function") PRIMITIVES["dom-text-content"] = domTextContent;
+  if (typeof domCreateElement === "function") PRIMITIVES["dom-create-element"] = domCreateElement;
+  if (typeof domAppend === "function") PRIMITIVES["dom-append"] = domAppend;
+  if (typeof domAppendToHead === "function") PRIMITIVES["dom-append-to-head"] = domAppendToHead;
  if (typeof jsonParse === "function") PRIMITIVES["json-parse"] = jsonParse;
  if (typeof nowMs === "function") PRIMITIVES["now-ms"] = nowMs;
  PRIMITIVES["sx-parse"] = sxParse;
--- a/shared/sx/ref/run_js_sx.py
+++ b/shared/sx/ref/run_js_sx.py
@@ -216,13 +216,15 @@ def compile_ref_to_js(
    # Platform JS for selected adapters
    if not has_dom:
        parts.append("\n  var _hasDom = false;\n")
-    for name in ("dom", "engine", "orchestration", "boot"):
-        if name in adapter_set and name in adapter_platform:
-            parts.append(adapter_platform[name])

+    # CEK fixups + general fixups BEFORE boot (boot hydrates islands that need these)
    parts.append(fixups_js(has_html, has_sx, has_dom, has_signals, has_deps, has_page_helpers))
    if has_cek:
        parts.append(CEK_FIXUPS_JS)
+
+    for name in ("dom", "engine", "orchestration", "boot"):
+        if name in adapter_set and name in adapter_platform:
+            parts.append(adapter_platform[name])
    if has_continuations:
        parts.append(CONTINUATIONS_JS)
    if has_dom:
--- a/sx/app.py
+++ b/sx/app.py
@@ -64,6 +64,7 @@ def create_app() -> "Quart":
        "sx",
        context_fn=sx_standalone_context if SX_STANDALONE else sx_docs_context,
        domain_services_fn=register_domain_services,
+        css_extras=[],  # No legacy CSS — SX uses CSSX + custom highlighting
        **extra_kw,
    )

--- a/sx/sx/docs-content.sx
+++ b/sx/sx/docs-content.sx
@@ -2,7 +2,7 @@

 (defcomp ~docs-content/home-content ()
  (div :id "main-content" :class "max-w-3xl mx-auto px-4 py-6"
-    (~docs/code :code (highlight (component-source "~layouts/header") "lisp"))))
+    (~home/stepper)))

 (defcomp ~docs-content/docs-introduction-content ()
  (~docs/page :title "Introduction"
--- a/sx/sx/essays/platonic-sx.sx
+++ b/sx/sx/essays/platonic-sx.sx
@@ -0,0 +1,274 @@
+(defcomp ~essays/platonic-sx/essay-platonic-sx ()
+  (~docs/page :title "Platonic SX"
+
+    (p :class "text-stone-500 text-sm italic mb-8"
+      "The allegory of the cave, the theory of Forms, and why a hypermedium "
+      "that defines itself participates in something Plato would have recognized.")
+
+    (~docs/section :title "The cave" :id "the-cave"
+      (p :class "text-stone-600"
+        "In Book VII of the " (a :href "https://en.wikipedia.org/wiki/Allegory_of_the_cave" :class "text-violet-600 hover:underline" "Republic")
+        ", Plato describes prisoners chained in a cave, facing a wall. "
+        "Behind them burns a fire; between the fire and the prisoners, figures move, "
+        "casting shadows on the wall. The prisoners have never seen the figures directly. "
+        "They take the shadows for reality.")
+
+      (p :class "text-stone-600"
+        "The allegory is about representation. The shadows are not the things themselves "
+        "but projections \u2014 reduced, flattened, stripped of depth and colour. "
+        "The prisoners mistake the representation for the thing represented. "
+        "They build entire theories about the behaviour of shadows, never suspecting "
+        "that the shadows are derived from something more real.")
+
+      (p :class "text-stone-600"
+        "The web is a cave."))
+
+    (~docs/section :title "Shadows on the wall" :id "shadows"
+      (p :class "text-stone-600"
+        "An HTML page is a shadow. It is a projection of the thing the author intended \u2014 "
+        "a structure, a meaning, a behaviour \u2014 flattened into a string of angle brackets. "
+        "The structure is lost in the serialization. The meaning is implicit in class names "
+        "and data attributes. The behaviour is bolted on in a separate language (JavaScript) "
+        "that has no formal relationship to the markup it manipulates.")
+
+      (p :class "text-stone-600"
+        "CSS is another shadow \u2014 a projection of visual intention into a cascade of "
+        "property-value pairs, separated from the structure it describes. "
+        "JSON is a shadow of data, stripped of type, context, and behaviour. "
+        "REST is a shadow of computation, reduced to verbs and resource paths.")
+
+      (p :class "text-stone-600"
+        "Each format is a lossy projection. And crucially, each projects into a "
+        (em "different") " medium. HTML for structure. CSS for style. JavaScript for behaviour. "
+        "JSON for data. The original unity \u2014 the " (em "thing itself") " \u2014 is scattered "
+        "across four representations that cannot reference each other "
+        "without external convention.")
+
+      (p :class "text-stone-600"
+        "Plato would have recognized this immediately. The Forms are one. "
+        "The shadows are many. The task of philosophy is to see past the shadows."))
+
+    (~docs/section :title "The theory of Forms" :id "forms"
+      (p :class "text-stone-600"
+        "Plato's " (a :href "https://en.wikipedia.org/wiki/Theory_of_forms" :class "text-violet-600 hover:underline" "theory of Forms")
+        " holds that behind every particular instance \u2014 every chair, every circle, "
+        "every act of justice \u2014 there exists an ideal Form: the perfect Chair, "
+        "the perfect Circle, Justice itself. Particular instances participate in their Form "
+        "but are always imperfect copies. The Form is eternal, immutable, and more real "
+        "than any instance.")
+
+      (p :class "text-stone-600"
+        "A " (code "defcomp") " definition is a Form:")
+
+      (~docs/code :code
+        (str "(defcomp ~card (&key title subtitle &rest children)\n"
+             "  (div :class \"rounded-lg shadow-sm p-4\"\n"
+             "    (h2 :class \"font-bold\" title)\n"
+             "    (when subtitle (p :class \"text-stone-500\" subtitle))\n"
+             "    children))"))
+
+      (p :class "text-stone-600"
+        "This is not a card. It is the " (em "idea") " of a card \u2014 the structure that every "
+        "particular card participates in. When the server evaluates "
+        (code "(~card :title \"Plato\" :subtitle \"428 BC\")") ", it produces a particular instance: "
+        "an HTML fragment, a shadow on a specific wall. The Form persists. "
+        "The shadow is consumed and replaced on the next render.")
+
+      (p :class "text-stone-600"
+        "In Plato's ontology, Forms are more real than particulars because they are "
+        "what particulars " (em "depend on") ". The HTML output depends on the component definition. "
+        "The component definition does not depend on any particular output. "
+        "It is prior, in the way that axioms are prior to theorems."))
+
+    (~docs/section :title "The divided line" :id "divided-line"
+      (p :class "text-stone-600"
+        "In the Republic, Plato describes " (a :href "https://en.wikipedia.org/wiki/Analogy_of_the_divided_line" :class "text-violet-600 hover:underline" "a line divided into four segments")
+        ", representing degrees of reality and knowledge:")
+
+      (div :class "overflow-x-auto mb-6"
+        (table :class "min-w-full text-sm"
+          (thead (tr
+            (th :class "text-left pr-4 pb-2 font-semibold" "Segment")
+            (th :class "text-left pr-4 pb-2 font-semibold" "Plato")
+            (th :class "text-left pb-2 font-semibold" "SX")))
+          (tbody
+            (tr (td :class "pr-4 py-1" "Images")
+                (td :class "pr-4" "Shadows, reflections")
+                (td "The rendered HTML in the browser \u2014 a momentary projection"))
+            (tr (td :class "pr-4 py-1" "Sensible objects")
+                (td :class "pr-4" "Physical things")
+                (td "The SX wire format \u2014 structured but still particular"))
+            (tr (td :class "pr-4 py-1" "Mathematical objects")
+                (td :class "pr-4" "Numbers, geometric shapes")
+                (td "Component definitions, the CEK machine, continuation frames"))
+            (tr (td :class "pr-4 py-1" "The Good / Forms")
+                (td :class "pr-4" "The Form of Forms")
+                (td "The s-expression itself \u2014 the representation that represents")))))
+
+      (p :class "text-stone-600"
+        "The bottom of the line is images \u2014 the DOM, pixels on screen. "
+        "Moving up: the SX wire format preserves more structure than HTML "
+        "(it retains the component calls, the s-expression nesting). "
+        "Above that: the component definitions and the CEK machine \u2014 "
+        "abstract structures that generate all possible instances. "
+        "At the top: the s-expression itself, which is both the medium of definition "
+        "and the thing defined.")
+
+      (p :class "text-stone-600"
+        "Plato's line is a hierarchy of " (em "participation") ". "
+        "Each level participates in the one above. "
+        "The rendered HTML participates in the component definition. "
+        "The component participates in the evaluator semantics. "
+        "The evaluator participates in the s-expression form. "
+        "The s-expression form participates in \u2014 what? "
+        "In computation itself. In the CEK machine. In logic."))
+
+    (~docs/section :title "Anamnesis: the evaluator remembers" :id "anamnesis"
+      (p :class "text-stone-600"
+        "Plato believed that learning is " (a :href "https://en.wikipedia.org/wiki/Anamnesis_(philosophy)" :class "text-violet-600 hover:underline" "recollection")
+        " \u2014 " (em "anamnesis") ". The soul has seen the Forms before birth; "
+        "education is not acquiring new knowledge but remembering what is already known. "
+        "The particular reminds us of the universal.")
+
+      (p :class "text-stone-600"
+        "The SX evaluator does something structurally similar. "
+        "When the browser receives SX wire format \u2014 ")
+
+      (~docs/code :code
+        "(~card :title \"Plato\" :subtitle \"428 BC\")")
+
+      (p :class "text-stone-600"
+        " \u2014 it does not receive instructions for rendering. It receives a " (em "name") " "
+        "and a set of arguments. The evaluator already knows " (code "~card") ". "
+        "It has the Form in its component environment. "
+        "The wire format is a reminder: " (em "produce the instance you already know how to produce") ". "
+        "The particular prompts the evaluator to recollect the universal.")
+
+      (p :class "text-stone-600"
+        "This is why the SX wire format is so small. It doesn't transmit the " (em "what") " "
+        "\u2014 the full HTML, the complete structure. It transmits the " (em "which") " "
+        "\u2014 which Form, which arguments. The evaluator supplies the rest from memory. "
+        "Bandwidth is the cost of forgetting. SX's wire format is efficient "
+        "because the client " (em "remembers") "."))
+
+    (~docs/section :title "Platonic aesthetics" :id "aesthetics"
+      (p :class "text-stone-600"
+        "For Plato, beauty is not subjective. A thing is beautiful to the degree "
+        "that it participates in the " (a :href "https://en.wikipedia.org/wiki/Platonic_beauty" :class "text-violet-600 hover:underline" "Form of Beauty")
+        " \u2014 which is to say, to the degree that it exhibits "
+        (em "order") ", " (em "proportion") ", and " (em "unity") ". "
+        "The " (a :href "https://en.wikipedia.org/wiki/Symposium_(Plato)" :class "text-violet-600 hover:underline" "Symposium")
+        " describes an ascent from beautiful bodies to beautiful souls to beautiful ideas, "
+        "culminating in Beauty itself \u2014 the Form that makes all beautiful things beautiful.")
+
+      (p :class "text-stone-600"
+        "There is a beauty in s-expressions that is Platonic in this precise sense. "
+        "Not decorative beauty \u2014 no one finds parentheses pretty. "
+        "But structural beauty: the kind Plato meant.")
+
+      (ul :class "list-disc pl-6 mb-4 space-y-2 text-stone-600"
+        (li (strong "Unity") " \u2014 one representation for everything. "
+            "Code, data, markup, wire format, component definitions, the evaluator itself. "
+            "No seams, no translation boundaries, no format negotiation. "
+            "The s-expression is a universal solvent.")
+        (li (strong "Proportion") " \u2014 the means are proportional to the ends. "
+            "A component is as complex as the thing it describes and no more. "
+            "The evaluator is 900 lines of SX. The parser is 400. "
+            "There is no hidden machinery, no framework overhead, no build step. "
+            "The ratio of essential to accidental complexity approaches one.")
+        (li (strong "Order") " \u2014 the hierarchy is strict and explicit. "
+            "CEK at the bottom, continuations above, scoped effects above, patterns at the top. "
+            "Each layer is definable in terms of the one below. "
+            "No circular dependencies, no ad hoc escape hatches, no exceptions to the rules."))
+
+      (p :class "text-stone-600"
+        "Plato would say that these properties are not incidental but necessary \u2014 "
+        "they follow from the proximity of s-expressions to the Forms themselves. "
+        "A representation that can represent itself has fewer impediments "
+        "between it and the abstract structure it encodes. "
+        "It is more " (em "real") ", in the Platonic sense, than a representation "
+        "that requires a separate meta-representation to describe it."))
+
+    (~docs/section :title "The escape from the cave" :id "escape"
+      (p :class "text-stone-600"
+        "In the allegory, one prisoner is freed and dragged up into the sunlight. "
+        "At first the light is blinding. He can only look at reflections in water, "
+        "then at objects, then at the sun itself. He returns to the cave "
+        "and tries to tell the others what he saw. They think he is mad.")
+
+      (p :class "text-stone-600"
+        "The web's cave is comfortable. Developers have built elaborate theories "
+        "of the shadows \u2014 virtual DOMs, hydration strategies, build tool chains, "
+        "CSS-in-JS, state management libraries. Each theory explains how shadows behave. "
+        "None asks why we are working with shadows at all.")
+
+      (p :class "text-stone-600"
+        "The escape is not a technology. It is a shift in perspective: "
+        (em "stop working with projections and work with the thing itself") ". "
+        "An s-expression is not a projection of structure into text \u2014 "
+        "it IS the structure. A " (code "defcomp") " is not a description of a component "
+        "in a host language \u2014 it IS the component. "
+        "The SX evaluator is not described by a specification \u2014 "
+        "it IS the specification, executing.")
+
+      (p :class "text-stone-600"
+        "This is what it means for a representation to be homoiconic. "
+        "The map is the territory. The shadow and the figure are the same thing. "
+        "The cave and the sunlit world collapse into one."))
+
+    (~docs/section :title "The demiurge" :id "demiurge"
+      (p :class "text-stone-600"
+        "In the " (a :href "https://en.wikipedia.org/wiki/Timaeus_(dialogue)" :class "text-violet-600 hover:underline" "Timaeus")
+        ", Plato introduces the " (a :href "https://en.wikipedia.org/wiki/Demiurge" :class "text-violet-600 hover:underline" "demiurge")
+        " \u2014 the divine craftsman who looks at the eternal Forms and fashions "
+        "the physical world in their image. The demiurge does not create the Forms. "
+        "He creates " (em "instances") " of them, in a medium (matter) that is less perfect "
+        "than the Forms themselves.")
+
+      (p :class "text-stone-600"
+        "The bootstrapper is a demiurge. It looks at the Forms (" (code "eval.sx") ", "
+        (code "parser.sx") ", " (code "cek.sx") ") and fashions instances in a material medium: "
+        "Python, JavaScript. The instances are less perfect than the Forms \u2014 "
+        "they have platform-specific quirks, performance characteristics, "
+        "memory layouts. But they " (em "participate") " in the Forms. "
+        "They are correct to the degree that they faithfully instantiate the spec.")
+
+      (p :class "text-stone-600"
+        "The demiurge is not omnipotent. He works with what the medium allows. "
+        "The Python bootstrapper emits " (code "def") " and " (code "lambda") "; "
+        "the JavaScript bootstrapper emits " (code "var") " and " (code "function") ". "
+        "Each medium has its own constraints. But the Form \u2014 the " (code ".sx") " spec \u2014 "
+        "is the same. Multiple demiurges, one set of Forms, many material instances."))
+
+    (~docs/section :title "The good" :id "the-good"
+      (p :class "text-stone-600"
+        "At the apex of Plato's hierarchy is the " (a :href "https://en.wikipedia.org/wiki/Form_of_the_Good" :class "text-violet-600 hover:underline" "Form of the Good")
+        " \u2014 the Form that makes all other Forms intelligible. "
+        "It is not itself a thing but the condition for all things being knowable. "
+        "It is the sun in the allegory: the source of light that reveals everything else.")
+
+      (p :class "text-stone-600"
+        "If we take the analogy seriously, what is SX's Form of the Good? "
+        "What makes the hierarchy \u2014 CEK, continuations, scoped effects, patterns \u2014 intelligible as a whole?")
+
+      (p :class "text-stone-600"
+        "It is the principle that " (strong "the representation and the thing represented should be identical") ". "
+        "Code is data. The specification is the implementation. The wire format is the source syntax. "
+        "The evaluator evaluates itself. Every level of the hierarchy obeys this principle, "
+        "and it is what makes each level intelligible from the one below.")
+
+      (p :class "text-stone-600"
+        "This is not a design principle in the engineering sense \u2014 a guideline to be followed or violated. "
+        "It is the structural " (em "reason") " the hierarchy exists at all. "
+        "Remove it and the layers collapse. Restore it and they reconstitute. "
+        "It is prior to the hierarchy, in the way the Good is prior to the Forms.")
+
+      (p :class "text-stone-600"
+        "Plato would have understood this. He spent his life searching for the thing "
+        "that is most itself, least dependent on anything else, most fully real. "
+        "An s-expression that defines its own evaluator, parsed by its own parser, "
+        "bootstrapped to every medium, generating instances of itself in perpetuity \u2014 "
+        "this is as close to a Platonic Form as computation gets."))
+
+    (p :class "text-stone-500 text-sm italic mt-12"
+       "The unexamined code is not worth running.")))
--- a/sx/sx/geography/cek.sx
+++ b/sx/sx/geography/cek.sx
@@ -148,6 +148,331 @@
        "lisp")))))


+;; ---------------------------------------------------------------------------
+;; CEK stepper: interactive stepping debugger
+;; ---------------------------------------------------------------------------
+
+(defisland ~geography/cek/demo-stepper (&key initial-expr)
+  (let ((source (signal (or initial-expr "(+ 1 (* 2 3))")))
+        (state (signal nil))
+        (steps (signal 0))
+        (history (signal (list)))
+        (error-msg (signal nil)))
+
+    ;; Parse and create initial CEK state
+    (define start-eval
+      (fn ()
+        (reset! error-msg nil)
+        (reset! history (list))
+        (reset! steps 0)
+        (let ((parsed (sx-parse (deref source))))
+          (if (empty? parsed)
+            (reset! error-msg "Parse error: empty expression")
+            (reset! state (make-cek-state (first parsed) (make-env) (list)))))))
+
+    ;; Single step
+    (define do-step
+      (fn ()
+        (when (and (deref state) (not (cek-terminal? (deref state))))
+          (let ((prev (deref state)))
+            (swap! history (fn (h) (append h (list prev))))
+            (swap! steps inc)
+            (reset! state (cek-step prev))))))
+
+    ;; Run to completion
+    (define do-run
+      (fn ()
+        (when (deref state)
+          (let run-loop ((n 0))
+            (when (and (not (cek-terminal? (deref state))) (< n 200))
+              (do-step)
+              (run-loop (+ n 1)))))))
+
+    ;; Reset
+    (define do-reset
+      (fn ()
+        (reset! state nil)
+        (reset! steps 0)
+        (reset! history (list))
+        (reset! error-msg nil)))
+
+    ;; Format control for display
+    (define fmt-control
+      (fn (s)
+        (if (nil? s) "\u2014"
+          (let ((c (get s "control")))
+            (if (nil? c) "\u2014"
+              (sx-serialize c))))))
+
+    ;; Format value
+    (define fmt-value
+      (fn (s)
+        (if (nil? s) "\u2014"
+          (let ((v (get s "value")))
+            (cond
+              (nil? v) "nil"
+              (callable? v) (str "\u03bb:" (or (lambda-name v) "fn"))
+              :else (sx-serialize v))))))
+
+    ;; Format kont
+    (define fmt-kont
+      (fn (s)
+        (if (nil? s) "\u2014"
+          (let ((k (get s "kont")))
+            (if (empty? k) "[]"
+              (str "[" (join " " (map (fn (f) (get f "type")) k)) "]"))))))
+
+    ;; Initialize on first render
+    (start-eval)
+
+    (div :class "space-y-4"
+      ;; Input
+      (div :class "flex gap-2 items-end"
+        (div :class "flex-1"
+          (label :class "text-xs text-stone-400 block mb-1" "Expression")
+          (input :type "text" :bind source
+                 :class "w-full px-3 py-1.5 rounded border border-stone-300 font-mono text-sm focus:outline-none focus:border-violet-400"
+                 :on-change (fn (e) (start-eval))))
+        (div :class "flex gap-1"
+          (button :on-click (fn (e) (start-eval))
+                  :class "px-3 py-1.5 rounded bg-stone-200 text-stone-700 text-sm hover:bg-stone-300" "Reset")
+          (button :on-click (fn (e) (do-step))
+                  :class "px-3 py-1.5 rounded bg-violet-500 text-white text-sm hover:bg-violet-600" "Step")
+          (button :on-click (fn (e) (do-run))
+                  :class "px-3 py-1.5 rounded bg-violet-700 text-white text-sm hover:bg-violet-800" "Run")))
+
+      ;; Error
+      (when (deref error-msg)
+        (div :class "text-red-600 text-sm" (deref error-msg)))
+
+      ;; Current state
+      (when (deref state)
+        (div :class "rounded border border-stone-200 bg-white p-3 font-mono text-sm space-y-1"
+          (div :class "flex gap-4"
+            (span :class "text-stone-400 w-16" "Step")
+            (span :class "font-bold" (deref steps)))
+          (div :class "flex gap-4"
+            (span :class "text-stone-400 w-16" "Phase")
+            (span :class (str "font-bold " (if (= (get (deref state) "phase") "eval") "text-blue-600" "text-green-600"))
+              (get (deref state) "phase")))
+          (div :class "flex gap-4"
+            (span :class "text-violet-500 w-16" "C")
+            (span (fmt-control (deref state))))
+          (div :class "flex gap-4"
+            (span :class "text-amber-600 w-16" "V")
+            (span (fmt-value (deref state))))
+          (div :class "flex gap-4"
+            (span :class "text-emerald-600 w-16" "K")
+            (span (fmt-kont (deref state))))
+          (when (cek-terminal? (deref state))
+            (div :class "mt-2 pt-2 border-t border-stone-200 text-stone-800 font-bold"
+              (str "Result: " (sx-serialize (cek-value (deref state))))))))
+
+      ;; Step history
+      (when (not (empty? (deref history)))
+        (div :class "rounded border border-stone-100 bg-stone-50 p-2"
+          (div :class "text-xs text-stone-400 mb-1" "History")
+          (div :class "space-y-0.5 font-mono text-xs max-h-48 overflow-y-auto"
+            (map-indexed (fn (i s)
+              (div :class "flex gap-2 text-stone-500"
+                (span :class "text-stone-300 w-6 text-right" (+ i 1))
+                (span :class (if (= (get s "phase") "eval") "text-blue-400" "text-green-400") (get s "phase"))
+                (span :class "text-violet-400 truncate" (fmt-control s))
+                (span :class "text-amber-400" (fmt-value s))
+                (span :class "text-emerald-400" (fmt-kont s))))
+              (deref history))))))))
+
+
+;; ---------------------------------------------------------------------------
+;; Render stepper: watch a component render itself, tag by tag
+;;
+;; Walks the SX AST depth-first. At each step, renders ONE subtree
+;; via render-to-html and appends to the accumulating output.
+;; The preview pane shows partial HTML building up.
+;; ---------------------------------------------------------------------------
+
+(defisland ~geography/cek/demo-render-stepper (&key initial-expr)
+  (let ((source (signal (or initial-expr
+          "(div (~cssx/tw :tokens \"p-6 rounded-lg border border-stone-200 bg-white text-center\")\n  (h1 (~cssx/tw :tokens \"text-3xl font-bold mb-2\")\n    (span (~cssx/tw :tokens \"text-rose-500\") \"the \")\n    (span (~cssx/tw :tokens \"text-amber-500\") \"joy \")\n    (span (~cssx/tw :tokens \"text-emerald-500\") \"of \")\n    (span (~cssx/tw :tokens \"text-violet-600 text-4xl\") \"sx\")))")))
+        (steps (signal (list)))
+        (step-idx (signal 0))
+        (parsed-ok (signal false))
+        (error-msg (signal nil))
+        (dom-stack-sig (signal (list))))
+    (letrec
+      ((split-tag (fn (expr result)
+         (cond
+           (not (list? expr))
+             (append! result {"type" "leaf" "expr" expr})
+           (empty? expr) nil
+           (not (= (type-of (first expr)) "symbol"))
+             (append! result {"type" "leaf" "expr" expr})
+           (is-html-tag? (symbol-name (first expr)))
+             (let ((ctag (symbol-name (first expr)))
+                   (cargs (rest expr))
+                   (cch (list))
+                   (cat (list))
+                   (spreads (list))
+                   (ckw false))
+               (for-each (fn (a)
+                 (cond
+                   (= (type-of a) "keyword") (do (set! ckw true) (append! cat a))
+                   ckw (do (set! ckw false) (append! cat a))
+                   (and (list? a) (not (empty? a))
+                        (= (type-of (first a)) "symbol")
+                        (starts-with? (symbol-name (first a)) "~"))
+                     (do (set! ckw false) (append! spreads a))
+                   :else (do (set! ckw false) (append! cch a))))
+                 cargs)
+               (append! result {"type" "open" "tag" ctag "attrs" cat "spreads" spreads})
+               (for-each (fn (c) (split-tag c result)) cch)
+               (append! result {"type" "close" "tag" ctag}))
+           :else
+             (append! result {"type" "expr" "expr" expr}))))
+       (get-preview (fn () (dom-query "[data-sx-lake=\"preview\"]")))
+       (get-stack (fn () (deref dom-stack-sig)))
+       (set-stack (fn (v) (reset! dom-stack-sig v)))
+       (push-stack (fn (el) (reset! dom-stack-sig (append (deref dom-stack-sig) (list el)))))
+       (pop-stack (fn ()
+         (let ((s (deref dom-stack-sig)))
+           (when (> (len s) 1)
+             (reset! dom-stack-sig (slice s 0 (- (len s) 1)))))))
+       (do-parse (fn ()
+         (reset! error-msg nil)
+         (reset! step-idx 0)
+         (reset! parsed-ok false)
+         (set-stack (list))
+         (let ((container (get-preview)))
+           (when container (dom-set-prop container "innerHTML" "")))
+         (let ((parsed (sx-parse (deref source))))
+           (if (empty? parsed)
+             (do (reset! error-msg "Parse error") (reset! steps (list)))
+             (let ((result (list)))
+               (split-tag (first parsed) result)
+               (reset! steps result)
+               (reset! parsed-ok true)
+               (set-stack (list (get-preview))))))))
+       (do-step (fn ()
+         (when (and (deref parsed-ok) (< (deref step-idx) (len (deref steps))))
+           (let ((step (nth (deref steps) (deref step-idx)))
+                 (step-type (get step "type"))
+                 (stack (get-stack))
+                 (parent (if (empty? (get-stack)) (get-preview) (last (get-stack)))))
+             (cond
+               (= step-type "open")
+                 (let ((el (dom-create-element (get step "tag") nil))
+                       (attrs (get step "attrs"))
+                       (spreads (or (get step "spreads") (list))))
+                   (let loop ((i 0))
+                     (when (< i (len attrs))
+                       (dom-set-attr el (keyword-name (nth attrs i)) (nth attrs (+ i 1)))
+                       (loop (+ i 2))))
+                   (for-each (fn (sp)
+                     (let ((result (eval-expr sp (make-env))))
+                       (when (and result (spread? result))
+                         (let ((sattrs (spread-attrs result)))
+                           (for-each (fn (k)
+                             (if (= k "class")
+                               (dom-set-attr el "class"
+                                 (str (or (dom-get-attr el "class") "") " " (get sattrs k)))
+                               (dom-set-attr el k (get sattrs k))))
+                             (keys sattrs))))))
+                     spreads)
+                   (when parent (dom-append parent el))
+                   (push-stack el))
+               (= step-type "close")
+                 (pop-stack)
+               (= step-type "leaf")
+                 (when parent
+                   (let ((val (get step "expr")))
+                     (dom-append parent (create-text-node (if (string? val) val (str val))))))
+               (= step-type "expr")
+                 (let ((rendered (render-to-dom (get step "expr") (make-env) nil)))
+                   (when (and parent rendered)
+                     (dom-append parent rendered)))))
+           (swap! step-idx inc))))
+       (do-run (fn ()
+         (let loop ()
+           (when (< (deref step-idx) (len (deref steps)))
+             (do-step)
+             (loop)))))
+       (do-back (fn ()
+         (when (and (deref parsed-ok) (> (deref step-idx) 0))
+           (let ((target (- (deref step-idx) 1))
+                 (container (get-preview)))
+             (when container (dom-set-prop container "innerHTML" ""))
+             (set-stack (list (get-preview)))
+             (reset! step-idx 0)
+             (for-each (fn (_) (do-step)) (slice (deref steps) 0 target)))))))
+      (div :class "space-y-4"
+        (div
+          (label :class "text-xs text-stone-400 block mb-1" "Component expression")
+          (textarea :bind source :rows 4
+            :class "w-full px-3 py-2 rounded border border-stone-300 font-mono text-xs focus:outline-none focus:border-violet-400"))
+        (div :class "flex gap-1"
+          (button :on-click (fn (e) (do-parse))
+            :class "px-3 py-1.5 rounded bg-stone-700 text-white text-sm hover:bg-stone-800" "Parse")
+          (button :on-click (fn (e) (do-back))
+            :class (str "px-3 py-1.5 rounded text-sm "
+                     (if (and (deref parsed-ok) (> (deref step-idx) 0))
+                       "bg-stone-200 text-stone-700 hover:bg-stone-300"
+                       "bg-stone-100 text-stone-300 cursor-not-allowed"))
+            "\u25c0")
+          (button :on-click (fn (e) (do-step))
+            :class (str "px-3 py-1.5 rounded text-sm "
+                     (if (and (deref parsed-ok) (< (deref step-idx) (len (deref steps))))
+                       "bg-violet-500 text-white hover:bg-violet-600"
+                       "bg-violet-200 text-violet-400 cursor-not-allowed"))
+            "Step \u25b6")
+          (button :on-click (fn (e) (do-run))
+            :class (str "px-3 py-1.5 rounded text-sm "
+                     (if (deref parsed-ok)
+                       "bg-violet-700 text-white hover:bg-violet-800"
+                       "bg-violet-200 text-violet-400 cursor-not-allowed"))
+            "Run \u25b6\u25b6"))
+        (when (deref error-msg)
+          (div :class "text-red-600 text-sm" (deref error-msg)))
+        (when (and (deref parsed-ok) (= (deref step-idx) 0))
+          (div :class "text-sm text-stone-500 bg-stone-50 rounded p-2"
+            (str "Parsed " (len (deref steps)) " render steps. Click Step to begin.")))
+        (div :class "grid grid-cols-1 md:grid-cols-2 gap-4"
+          (when (deref parsed-ok)
+            (div :class "rounded border border-stone-200 bg-white p-3 min-h-24"
+              (div :class "text-xs text-stone-400 mb-2"
+                (str (deref step-idx) " / " (len (deref steps))
+                     (if (= (deref step-idx) (len (deref steps))) " \u2014 complete" "")))
+              (div :class "space-y-0.5 font-mono text-xs max-h-64 overflow-y-auto"
+                (map-indexed (fn (i step)
+                  (div :class (str "flex gap-2 px-1 rounded "
+                               (cond
+                                 (= i (deref step-idx)) "bg-violet-100 text-violet-700 font-bold"
+                                 (< i (deref step-idx)) "text-stone-400"
+                                 :else "text-stone-300"))
+                    (span :class "w-4 text-right"
+                      (if (< i (deref step-idx)) "\u2713" (str (+ i 1))))
+                    (span :class "truncate"
+                      (let ((lbl (get step "label")))
+                        (if lbl
+                          (if (> (len lbl) 60) (str (slice lbl 0 57) "...") lbl)
+                          (let ((tp (get step "type")))
+                            (cond
+                              (= tp "open") (str "<" (get step "tag") ">")
+                              (= tp "close") (str "</" (get step "tag") ">")
+                              :else (sx-serialize (get step "expr")))))))))
+                  (deref steps)))))
+          (div :class "rounded border border-stone-200 p-3 min-h-24"
+            (div :class "text-xs text-stone-400 mb-2" "Live DOM")
+            (lake :id "preview")))))))
+
+
+
+
+
+
+
+
+
+
 ;; ---------------------------------------------------------------------------
 ;; Demo page content
 ;; ---------------------------------------------------------------------------
@@ -157,39 +482,42 @@

    (~docs/section :title "What this demonstrates" :id "what"
      (p "These are " (strong "live islands") " evaluated by the CEK machine. Every " (code "eval-expr") " goes through " (code "cek-run") ". Every " (code "(deref sig)") " in an island creates a reactive DOM binding via continuation frames.")
-      (p "The CEK machine is defined in " (code "cek.sx") " (160 lines) and " (code "frames.sx") " (100 lines) — pure s-expressions, bootstrapped to both JavaScript and Python."))
+      (p "The CEK machine is defined in " (code "cek.sx") " and " (code "frames.sx") " — pure s-expressions, bootstrapped to both JavaScript and Python."))
+
+    (~docs/section :title "Stepper" :id "stepper"
+      (p "The CEK machine is pure data\u2192data. Each step takes a state dict and returns a new one. "
+         "Type an expression, click Step to advance one CEK transition.")
+      (~geography/cek/demo-stepper :initial-expr "(let ((x 10)) (+ x (* 2 3)))")
+      (~docs/code :code (highlight (component-source "~geography/cek/demo-stepper") "lisp")))
+
+    (~docs/section :title "Render stepper" :id "render-stepper"
+      (p "Watch a component render itself. The CEK evaluates the expression — "
+         "when it encounters " (code "(div ...)") ", the render adapter produces HTML in one step. "
+         "Click Run to see the rendered output appear in the preview.")
+      (~geography/cek/demo-render-stepper)
+      (~docs/code :code (highlight (component-source "~geography/cek/demo-render-stepper") "lisp")))

    (~docs/section :title "1. Counter" :id "demo-counter"
      (p (code "(deref count)") " in text position creates a reactive text node. " (code "(deref doubled)") " is a computed that updates when count changes.")
      (~geography/cek/demo-counter :initial 0)
-      (~docs/code :code (highlight
-        "(defisland ~demo-counter (&key initial)\n  (let ((count (signal (or initial 0)))\n        (doubled (computed (fn () (* 2 (deref count))))))\n    (div\n      (button :on-click (fn (e) (swap! count dec)) \"-\")\n      (span (deref count))\n      (button :on-click (fn (e) (swap! count inc)) \"+\")\n      (p (str \"doubled: \" (deref doubled))))))"
-        "lisp")))
+      (~docs/code :code (highlight (component-source "~geography/cek/demo-counter") "lisp")))

    (~docs/section :title "2. Computed chain" :id "demo-chain"
      (p "Three levels of computed: base -> doubled -> quadrupled. Change base, all propagate.")
      (~geography/cek/demo-chain)
-      (~docs/code :code (highlight
-        "(let ((base (signal 1))\n      (doubled (computed (fn () (* (deref base) 2))))\n      (quadrupled (computed (fn () (* (deref doubled) 2)))))\n  (span (deref base))\n  (p (str \"doubled: \" (deref doubled)\n         \"  |  quadrupled: \" (deref quadrupled))))"
-        "lisp")))
+      (~docs/code :code (highlight (component-source "~geography/cek/demo-chain") "lisp")))

    (~docs/section :title "3. Reactive attributes" :id "demo-attr"
      (p (code "(deref sig)") " in " (code ":class") " position. The CEK evaluates the " (code "str") " expression, and when the signal changes, the continuation re-evaluates and updates the attribute.")
      (~geography/cek/demo-reactive-attr)
-      (~docs/code :code (highlight
-        "(div :class (str \"p-3 rounded font-medium \"\n             (if (deref danger)\n               \"bg-red-100 text-red-800\"\n               \"bg-green-100 text-green-800\"))\n  (if (deref danger) \"DANGER\" \"SAFE\"))"
-        "lisp")))
+      (~docs/code :code (highlight (component-source "~geography/cek/demo-reactive-attr") "lisp")))

    (~docs/section :title "4. Effect + cleanup" :id "demo-stopwatch"
      (p "Effects still work through CEK. This stopwatch uses " (code "effect") " with cleanup — toggling the signal clears the interval.")
      (~geography/cek/demo-stopwatch)
-      (~docs/code :code (highlight
-        "(effect (fn ()\n  (when (deref running)\n    (let ((id (set-interval (fn () (swap! elapsed inc)) 100)))\n      (fn () (clear-interval id))))))"
-        "lisp")))
+      (~docs/code :code (highlight (component-source "~geography/cek/demo-stopwatch") "lisp")))

    (~docs/section :title "5. Batch coalescing" :id "demo-batch"
      (p "Two signals updated in " (code "batch") " — one notification cycle. Compare render counts between batch and no-batch.")
      (~geography/cek/demo-batch)
-      (~docs/code :code (highlight
-        "(batch (fn ()\n  (swap! first-sig inc)\n  (swap! second-sig inc)))\n;; One render pass, not two."
-        "lisp")))))
+      (~docs/code :code (highlight (component-source "~geography/cek/demo-batch") "lisp")))))
--- a/sx/sx/home-stepper.sx
+++ b/sx/sx/home-stepper.sx
@@ -0,0 +1,230 @@
+(defisland ~home/stepper ()
+  (let ((source "(div (~cssx/tw :tokens \"text-center\")\n  (h1 (~cssx/tw :tokens \"text-3xl font-bold mb-2\")\n    (span (~cssx/tw :tokens \"text-rose-500\") \"the \")\n    (span (~cssx/tw :tokens \"text-amber-500\") \"joy \")\n    (span (~cssx/tw :tokens \"text-emerald-500\") \"of \")\n    (span (~cssx/tw :tokens \"text-violet-600 text-4xl\") \"sx\")))")
+        (steps (signal (list)))
+        (step-idx (signal 9))
+        (dom-stack-sig (signal (list)))
+        (code-tokens (signal (list)))
+        (code-spans (list)))
+    (letrec
+      ((split-tag (fn (expr result)
+         (cond
+           (not (list? expr))
+             (append! result {"type" "leaf" "expr" expr})
+           (empty? expr) nil
+           (not (= (type-of (first expr)) "symbol"))
+             (append! result {"type" "leaf" "expr" expr})
+           (is-html-tag? (symbol-name (first expr)))
+             (let ((ctag (symbol-name (first expr)))
+                   (cargs (rest expr))
+                   (cch (list))
+                   (cat (list))
+                   (spreads (list))
+                   (ckw false))
+               (for-each (fn (a)
+                 (cond
+                   (= (type-of a) "keyword") (do (set! ckw true) (append! cat a))
+                   ckw (do (set! ckw false) (append! cat a))
+                   (and (list? a) (not (empty? a))
+                        (= (type-of (first a)) "symbol")
+                        (starts-with? (symbol-name (first a)) "~"))
+                     (do (set! ckw false) (append! spreads a))
+                   :else (do (set! ckw false) (append! cch a))))
+                 cargs)
+               (append! result {"type" "open" "tag" ctag "attrs" cat "spreads" spreads})
+               (for-each (fn (c) (split-tag c result)) cch)
+               (append! result {"type" "close" "tag" ctag}))
+           :else
+             (append! result {"type" "expr" "expr" expr}))))
+       (build-code-tokens (fn (expr tokens step-ref indent)
+         (cond
+           (string? expr)
+             (do (append! tokens {"text" (str "\"" expr "\"") "cls" "text-emerald-700" "step" (get step-ref "v")})
+                 (dict-set! step-ref "v" (+ (get step-ref "v") 1)))
+           (number? expr)
+             (do (append! tokens {"text" (str expr) "cls" "text-amber-700" "step" (get step-ref "v")})
+                 (dict-set! step-ref "v" (+ (get step-ref "v") 1)))
+           (= (type-of expr) "keyword")
+             (append! tokens {"text" (str ":" (keyword-name expr)) "cls" "text-violet-600" "step" (get step-ref "v")})
+           (= (type-of expr) "symbol")
+             (let ((name (symbol-name expr)))
+               (append! tokens {"text" name "cls"
+                 (cond
+                   (is-html-tag? name) "text-sky-700 font-semibold"
+                   (starts-with? name "~") "text-rose-600 font-semibold"
+                   :else "text-stone-700")
+                 "step" (get step-ref "v")}))
+           (list? expr)
+             (when (not (empty? expr))
+               (let ((head (first expr))
+                     (is-tag (and (= (type-of head) "symbol") (is-html-tag? (symbol-name head))))
+                     (is-comp (and (= (type-of head) "symbol") (starts-with? (symbol-name head) "~")))
+                     (open-step (get step-ref "v")))
+                 (append! tokens {"text" "(" "cls" "text-stone-400" "step" open-step})
+                 (build-code-tokens head tokens step-ref indent)
+                 (when is-tag
+                   (dict-set! step-ref "v" (+ (get step-ref "v") 1)))
+                 (for-each (fn (a)
+                   (let ((is-child (and (list? a) (not (empty? a))
+                                        (= (type-of (first a)) "symbol")
+                                        (or (is-html-tag? (symbol-name (first a)))
+                                            (starts-with? (symbol-name (first a)) "~"))))
+                         (is-spread (and (list? a) (not (empty? a))
+                                         (= (type-of (first a)) "symbol")
+                                         (starts-with? (symbol-name (first a)) "~"))))
+                     (if is-spread
+                       ;; Component spread: save counter, process, restore
+                       ;; All tokens inside share parent open-step
+                       (let ((saved (get step-ref "v"))
+                               (saved-tokens-len (len tokens)))
+                         (append! tokens {"text" " " "cls" "" "step" -1})
+                         (build-code-tokens a tokens step-ref indent)
+                         ;; Mark all tokens added during spread as spread tokens
+                         (let mark-loop ((j saved-tokens-len))
+                           (when (< j (len tokens))
+                             (dict-set! (nth tokens j) "spread" true)
+                             (mark-loop (+ j 1))))
+                         (dict-set! step-ref "v" saved))
+                       (if (and is-tag is-child)
+                         (do (append! tokens {"text" (str "\n" (join "" (map (fn (_) "  ") (range 0 (+ indent 1))))) "cls" "" "step" -1})
+                             (build-code-tokens a tokens step-ref (+ indent 1)))
+                         (do (append! tokens {"text" " " "cls" "" "step" -1})
+                             (build-code-tokens a tokens step-ref indent))))))
+                   (rest expr))
+                 (append! tokens {"text" ")" "cls" "text-stone-400" "step" open-step})
+                 (when is-tag
+                   (dict-set! step-ref "v" (+ (get step-ref "v") 1)))))
+           :else nil)))
+       (get-preview (fn () (dom-query "[data-sx-lake=\"home-preview\"]")))
+       (get-code-view (fn () (dom-query "[data-sx-lake=\"code-view\"]")))
+       (get-stack (fn () (deref dom-stack-sig)))
+       (set-stack (fn (v) (reset! dom-stack-sig v)))
+       (push-stack (fn (el) (reset! dom-stack-sig (append (deref dom-stack-sig) (list el)))))
+       (pop-stack (fn ()
+         (let ((s (deref dom-stack-sig)))
+           (when (> (len s) 1)
+             (reset! dom-stack-sig (slice s 0 (- (len s) 1)))))))
+       (build-code-dom (fn ()
+         (when (and (empty? code-spans) (not (empty? (deref code-tokens))))
+           (let ((code-el (get-code-view)))
+             (when code-el
+               (dom-set-prop code-el "innerHTML" "")
+               (for-each (fn (tok)
+                 (let ((sp (dom-create-element "span" nil)))
+                   (dom-set-attr sp "class" (get tok "cls"))
+                   (dom-set-prop sp "textContent" (get tok "text"))
+                   (dom-append code-el sp)
+                   (append! code-spans (dict "el" sp "step" (get tok "step") "cls" (get tok "cls") "spread" (get tok "spread")))))
+                 (deref code-tokens)))))))
+       (update-code-highlight (fn ()
+         (let ((cur (deref step-idx)))
+           (for-each (fn (s)
+             (let ((step-num (get s "step"))
+                   (el (get s "el"))
+                   (base (get s "cls")))
+               (when (not (= step-num -1))
+                 (dom-set-attr el "class"
+                   (str base
+                     (let ((is-spread (get s "spread")))
+                     (cond
+                       (and (= step-num cur) is-spread) " opacity-60"
+                       (= step-num cur) " bg-amber-100 rounded px-0.5 font-bold text-sm"
+                       (and (< step-num cur) is-spread) " opacity-60"
+                       (< step-num cur) " font-bold text-xs"
+                       :else " opacity-40")))))))
+             code-spans))))
+       (do-step (fn ()
+         (build-code-dom)
+         (when (< (deref step-idx) (len (deref steps)))
+           (when (empty? (get-stack))
+             (let ((p (get-preview)))
+               (when p (set-stack (list p)))))
+           (let ((step (nth (deref steps) (deref step-idx)))
+                 (step-type (get step "type"))
+                 (parent (if (empty? (get-stack)) (get-preview) (last (get-stack)))))
+             (cond
+               (= step-type "open")
+                 (let ((el (dom-create-element (get step "tag") nil))
+                       (attrs (get step "attrs"))
+                       (spreads (or (get step "spreads") (list))))
+                   (let loop ((i 0))
+                     (when (< i (len attrs))
+                       (dom-set-attr el (keyword-name (nth attrs i)) (nth attrs (+ i 1)))
+                       (loop (+ i 2))))
+                   (for-each (fn (sp)
+                     (let ((result (eval-expr sp (make-env))))
+                       (when (and result (spread? result))
+                         (let ((sattrs (spread-attrs result)))
+                           (for-each (fn (k)
+                             (if (= k "class")
+                               (dom-set-attr el "class"
+                                 (str (or (dom-get-attr el "class") "") " " (get sattrs k)))
+                               (dom-set-attr el k (get sattrs k))))
+                             (keys sattrs))))))
+                     spreads)
+                   (when parent (dom-append parent el))
+                   (push-stack el))
+               (= step-type "close")
+                 (pop-stack)
+               (= step-type "leaf")
+                 (when parent
+                   (let ((val (get step "expr")))
+                     (dom-append parent (create-text-node (if (string? val) val (str val))))))
+               (= step-type "expr")
+                 (let ((rendered (render-to-dom (get step "expr") (make-env) nil)))
+                   (when (and parent rendered)
+                     (dom-append parent rendered)))))
+           (swap! step-idx inc)
+           (update-code-highlight))))
+       (do-back (fn ()
+         (when (> (deref step-idx) 0)
+           (let ((target (- (deref step-idx) 1))
+                 (container (get-preview)))
+             (when container (dom-set-prop container "innerHTML" ""))
+             (set-stack (list (get-preview)))
+             (reset! step-idx 0)
+             (for-each (fn (_) (do-step)) (slice (deref steps) 0 target)))))))
+      ;; Auto-parse via effect
+      (effect (fn ()
+        (let ((parsed (sx-parse source)))
+          (when (not (empty? parsed))
+            (let ((result (list))
+                  (step-ref (dict "v" 0)))
+              (split-tag (first parsed) result)
+              (reset! steps result)
+              (let ((tokens (list)))
+                (dict-set! step-ref "v" 0)
+                (build-code-tokens (first parsed) tokens step-ref 0)
+                (reset! code-tokens tokens))
+              ;; Defer code DOM build until lake exists
+              (schedule-idle (fn ()
+                (build-code-dom)
+                ;; Replay to initial step-idx
+                (let ((target (deref step-idx)))
+                  (reset! step-idx 0)
+                  (set-stack (list (get-preview)))
+                  (for-each (fn (_) (do-step)) (slice (deref steps) 0 target)))
+                (update-code-highlight)
+                (run-post-render-hooks))))))))
+      (div :class "space-y-4"
+        ;; Code view lake — spans built imperatively, classes updated on step
+        (div (~cssx/tw :tokens "font-mono bg-stone-50 rounded p-2 overflow-x-auto leading-relaxed whitespace-pre-wrap")
+          :style "font-size:0.5rem"
+          (lake :id "code-view"))
+        ;; Controls
+        (div :class "flex items-center justify-center gap-2 md:gap-3"
+          (button :on-click (fn (e) (do-back))
+            :class (str "px-2 py-1 rounded text-lg "
+                     (if (> (deref step-idx) 0)
+                       "text-stone-600 hover:text-stone-800 hover:bg-stone-100"
+                       "text-stone-300 cursor-not-allowed"))
+            "\u25c0")
+          (span :class "text-sm text-stone-500 font-mono tabular-nums"
+            (deref step-idx) " / " (len (deref steps)))
+          (button :on-click (fn (e) (do-step))
+            :class (str "px-2 py-1 rounded text-lg "
+                     (if (< (deref step-idx) (len (deref steps)))
+                       "text-violet-600 hover:text-violet-800 hover:bg-violet-50"
+                       "text-violet-300 cursor-not-allowed"))
+            "\u25b6"))
+        ;; Live preview lake
+        (lake :id "home-preview")))))
--- a/sx/sx/nav-data.sx
+++ b/sx/sx/nav-data.sx
@@ -113,7 +113,9 @@
  (dict :label "SX and Dennett" :href "/sx/(etc.(philosophy.dennett))"
        :summary "Real patterns, intentional stance, and multiple drafts — Dennett's philosophy of mind as a framework for understanding SX.")
  (dict :label "S-Existentialism" :href "/sx/(etc.(philosophy.existentialism))"
-        :summary "Existence precedes essence — Sartre, Camus, and the absurd freedom of writing a Lisp for the web.")))
+        :summary "Existence precedes essence — Sartre, Camus, and the absurd freedom of writing a Lisp for the web.")
+  (dict :label "Platonic SX" :href "/sx/(etc.(philosophy.platonic-sx))"
+        :summary "The allegory of the cave, the theory of Forms, and why a self-defining hypermedium participates in something Plato would have recognized.")))

 (define specs-nav-items (list
  {:label "Core" :href "/sx/(language.(spec.core))" :children (list
--- a/sx/sx/page-functions.sx
+++ b/sx/sx/page-functions.sx
@@ -506,6 +506,7 @@
        "wittgenstein" '(~essays/sx-and-wittgenstein/essay-sx-and-wittgenstein)
        "dennett" '(~essays/sx-and-dennett/essay-sx-and-dennett)
        "existentialism" '(~essays/s-existentialism/essay-s-existentialism)
+        "platonic-sx" '(~essays/platonic-sx/essay-platonic-sx)
        :else '(~essays/philosophy-index/content)))))

 ;; Plans (under etc)
--- a/sx/sx/plans/foundations.sx
+++ b/sx/sx/plans/foundations.sx
@@ -21,16 +21,50 @@
       "No layer can be decomposed without the layer beneath it.")

    (~docs/code :code
-      (str "Layer 0: CEK machine      (expression + environment + continuation)\n"
-           "Layer 1: Continuations     (shift / reset \u2014 delimited capture)\n"
-           "Layer 2: Algebraic effects (operations + handlers)\n"
-           "Layer 3: Scoped effects    (+ region delimitation)\n"
-           "Layer 4: SX patterns       (spread, provide, island, lake, signal, collect)"))
+      (str "Layer 0: CEK machine      (expression + environment + continuation)   \u2714 DONE\n"
+           "Layer 1: Continuations     (shift / reset \u2014 delimited capture)         \u2714 DONE\n"
+           "Layer 2: Algebraic effects (operations + handlers)                     \u2714 DONE\n"
+           "Layer 3: Scoped effects    (+ region delimitation)                     \u2714 DONE\n"
+           "Layer 4: SX patterns       (spread, provide, island, lake, signal)     \u2714 DONE"))

-    (p "SX currently has layers 0, 1, and 4. "
-       "Layer 3 is the scoped-effects plan (provide/context/emit!). "
-       "Layer 2 falls out of layers 1 and 3 and doesn't need its own representation. "
-       "This document is about layers 0 through 2 \u2014 the machinery beneath scoped effects.")
+    (p "All five layers are implemented. The entire hierarchy from patterns down to raw CEK "
+       "is specced in " (code ".sx") " files and bootstrapped to Python and JavaScript. "
+       "No hand-written evaluation logic remains.")
+
+    ;; -----------------------------------------------------------------------
+    ;; What we built (status)
+    ;; -----------------------------------------------------------------------
+
+    (h2 :class "text-xl font-bold mt-12 mb-4" "What We Built")
+
+    (div :class "overflow-x-auto mb-6"
+      (table :class "min-w-full text-sm"
+        (thead (tr
+          (th :class "text-left pr-4 pb-2 font-semibold" "Layer")
+          (th :class "text-left pr-4 pb-2 font-semibold" "Spec files")
+          (th :class "text-left pr-4 pb-2 font-semibold" "What it provides")
+          (th :class "text-left pb-2 font-semibold" "Tests")))
+        (tbody
+          (tr (td :class "pr-4 py-1" "0 \u2014 CEK")
+              (td :class "pr-4 font-mono text-xs" "cek.sx, frames.sx")
+              (td :class "pr-4" "Explicit step function, 20+ frame types, cek-call dispatch, CEK-native HO forms")
+              (td "43 CEK + 26 reactive"))
+          (tr (td :class "pr-4 py-1" "1 \u2014 Continuations")
+              (td :class "pr-4 font-mono text-xs" "continuations.sx, callcc.sx")
+              (td :class "pr-4" "shift/reset (delimited), call/cc (full), ReactiveResetFrame + DerefFrame")
+              (td "Continuation tests"))
+          (tr (td :class "pr-4 py-1" "2 \u2014 Effect signatures")
+              (td :class "pr-4 font-mono text-xs" "boundary.sx, eval.sx")
+              (td :class "pr-4" ":effects annotations on define, boundary enforcement at startup")
+              (td "Boundary validation"))
+          (tr (td :class "pr-4 py-1" "3 \u2014 Scoped effects")
+              (td :class "pr-4 font-mono text-xs" "eval.sx, adapters")
+              (td :class "pr-4" "scope/provide/context/emit!/emitted, scope-push!/scope-pop!")
+              (td "Scope integration"))
+          (tr (td :class "pr-4 py-1" "4 \u2014 Patterns")
+              (td :class "pr-4 font-mono text-xs" "signals.sx, adapter-dom.sx, engine.sx")
+              (td :class "pr-4" "signal/deref/computed/effect/batch, island/lake, spread/collect")
+              (td "20 signal + 26 CEK reactive")))))

    ;; -----------------------------------------------------------------------
    ;; Layer 0: The CEK machine
@@ -65,36 +99,35 @@

    (p "Three things, all necessary, none decomposable further.")

-    (h3 :class "text-lg font-semibold mt-8 mb-3" "CEK in eval.sx")
+    (h3 :class "text-lg font-semibold mt-8 mb-3" "CEK in SX")

-    (p "SX already implements CEK. It just doesn't name it:")
+    (p "The CEK machine is the default evaluator on both client (JS) and server (Python). "
+       "Every " (code "eval-expr") " call goes through " (code "cek-run") ". "
+       "The spec lives in two files:")
+
+    (ul :class "list-disc pl-6 mb-4 space-y-1"
+      (li (code "frames.sx") " \u2014 20+ frame types (IfFrame, ArgFrame, MapFrame, ReactiveResetFrame, ...)")
+      (li (code "cek.sx") " \u2014 step function, run loop, special form handlers, HO form handlers, cek-call"))
+
+    (p (code "cek-call") " is the universal function dispatch. "
+       "It replaces the old " (code "invoke") " shim \u2014 SX lambdas go through " (code "cek-run") ", "
+       "native callables through " (code "apply") ". One calling convention, bootstrapped identically to every host.")
+
+    (h3 :class "text-lg font-semibold mt-8 mb-3" "CEK-native higher-order forms")
+
+    (p "All higher-order forms step element-by-element through the CEK machine:")

    (~docs/code :code
-      (str ";; eval-expr IS the CEK transition function\n"
-           ";; C = expr, E = env, K = implicit (call stack / trampoline)\n"
-           "(define eval-expr\n"
-           "  (fn (expr env)\n"
-           "    (cond\n"
-           "      (number? expr) expr          ;; literal: C \u2192 value, K unchanged\n"
-           "      (string? expr) expr\n"
-           "      (symbol? expr) (env-get env expr)  ;; variable: C + E \u2192 value\n"
-           "      (list? expr)                       ;; compound: modify K (push frame)\n"
-           "        (let ((head (first expr)))\n"
-           "          ...))))\n"
+      (str ";; map pushes a MapFrame, calls f on each element via continue-with-call\n"
+           "(map (fn (x) (* 2 (deref counter))) items)\n"
           "\n"
-           ";; The trampoline IS the K register made explicit:\n"
-           ";; instead of growing the call stack, thunks are continuations\n"
-           "(define trampoline\n"
-           "  (fn (val)\n"
-           "    (let loop ((v val))\n"
-           "      (if (thunk? v)\n"
-           "        (loop (eval-expr (thunk-expr v) (thunk-env v)))\n"
-           "        v))))"))
+           ";; deref inside the callback goes through CEK's DerefFrame\n"
+           ";; \u2192 reactive-shift-deref fires if inside a reactive-reset boundary\n"
+           ";; \u2192 the continuation from deref to the MapFrame is captured as a subscriber"))

-    (p "The trampoline is the K register. Thunks are suspended continuations. "
-       "Tail-call optimization is replacing K instead of extending it. "
-       "SX's evaluation model is already a CEK machine \u2014 the plan is to make this explicit, "
-       "not to build something new.")
+    (p "This means " (code "deref") " works inside " (code "map") ", " (code "filter") ", "
+       (code "reduce") ", " (code "for-each") ", " (code "some") ", " (code "every?") " callbacks. "
+       "The HO forms don't escape to tree-walk \u2014 the CEK machine processes every step.")

    ;; -----------------------------------------------------------------------
    ;; Layer 1: Delimited continuations
@@ -116,15 +149,25 @@
       (code "shift") " says: \"give me everything between here and that boundary as a callable function.\" "
       "The captured continuation " (em "is") " a slice of the K register.")

-    (p "This is already specced in SX (continuations.sx). What it gives us beyond CEK:")
+    (h3 :class "text-lg font-semibold mt-8 mb-3" "Deref as shift")

-    (ul :class "list-disc pl-6 mb-4 space-y-1"
-      (li (strong "Suspendable computation") " \u2014 capture where you are, resume later")
-      (li (strong "Backtracking") " \u2014 capture a choice point, try alternatives")
-      (li (strong "Coroutines") " \u2014 two computations yielding to each other")
-      (li (strong "Async as a library") " \u2014 async/await is shift/reset with a scheduler"))
+    (p "The reactive payoff. " (code "deref") " inside a " (code "reactive-reset") " boundary "
+       "is shift/reset applied to signals:")

-    (h3 :class "text-lg font-semibold mt-8 mb-3" "The Filinski Embedding")
+    (~docs/code :code
+      (str ";; User writes:\n"
+           "(div :class (str \"count-\" (deref counter))\n"
+           "  (str \"Value: \" (deref counter)))\n"
+           "\n"
+           ";; CEK sees (deref counter) \u2192 signal? \u2192 reactive-reset on stack?\n"
+           ";; Yes: capture (str \"count-\" [HOLE]) as continuation\n"
+           ";; Register as subscriber. Return current value.\n"
+           ";; When counter changes: re-invoke continuation \u2192 update DOM."))
+
+    (p "No explicit " (code "effect()") " wrapping needed. "
+       "The continuation capture IS the subscription mechanism.")
+
+    (h3 :class "text-lg font-semibold mt-8 mb-3" "The Filinski embedding")

    (p "Filinski (1994) proved that " (code "shift/reset") " can encode "
       (em "any") " monadic effect. State, exceptions, nondeterminism, I/O, "
@@ -132,78 +175,6 @@
       "This means layer 1 is already computationally complete for effects. "
       "Everything above is structure, not power.")

-    (p "This is the key insight: "
-       (strong "layers 2\u20134 add no computational power. ") "They add " (em "structure") " \u2014 "
-       "they make effects composable, nameable, handleable. "
-       "But anything you can do with scoped effects, "
-       "you can do with raw shift/reset. You'd just hate writing it.")
-
-    ;; -----------------------------------------------------------------------
-    ;; Layer 2: Algebraic effects
-    ;; -----------------------------------------------------------------------
-
-    (h2 :class "text-xl font-bold mt-12 mb-4" "Layer 2: Algebraic Effects")
-
-    (p "Plotkin & Pretnar (2009) observed that most effects have algebraic structure: "
-       "an operation (\"perform this effect\") and a handler (\"here's what that effect means\"). "
-       "The handler receives the operation's argument and a continuation to resume the program.")
-
-    (~docs/code :code
-      (str ";; Pseudocode \u2014 algebraic effect style\n"
-           "(handle\n"
-           "  (fn () (+ 1 (perform :ask \"what number?\")))\n"
-           "  {:ask (fn (prompt resume)\n"
-           "          (resume 41))})\n"
-           ";; => 42"))
-
-    (p (code "perform") " is shift. " (code "handle") " is reset. "
-       "But with names and types. The handler pattern gives you:")
-
-    (ul :class "list-disc pl-6 mb-4 space-y-1"
-      (li (strong "Named effects") " \u2014 not just \"capture here\" but \"I need state / logging / auth\"")
-      (li (strong "Composable handlers") " \u2014 stack handlers, each handling different effects")
-      (li (strong "Effect signatures") " \u2014 a function declares what effects it needs; "
-          "the type system ensures all effects are handled"))
-
-    (p "Plotkin & Power (2003) proved that this captures: "
-       "state, exceptions, nondeterminism, I/O, cooperative concurrency, "
-       "probability, and backtracking. All as instances of one algebraic structure.")
-
-    (h3 :class "text-lg font-semibold mt-8 mb-3" "What algebraic effects cannot express")
-
-    (p "Standard algebraic effects have a limitation: their operations are " (em "first-order") ". "
-       "An operation takes a value and produces a value. But some effects need operations that "
-       "take " (em "computations") " as arguments:")
-
-    (ul :class "list-disc pl-6 mb-4 space-y-1"
-      (li (code "catch") " \u2014 takes a computation that might throw, runs it with a handler")
-      (li (code "local") " \u2014 takes a computation, runs it with modified state")
-      (li (code "once") " \u2014 takes a nondeterministic computation, commits to its first result")
-      (li (code "scope") " \u2014 takes a computation, runs it within a delimited region"))
-
-    (p "These are " (strong "higher-order effects") ". They need computations as arguments, "
-       "not just values. This is precisely what the scoped-effects plan addresses.")
-
-    ;; -----------------------------------------------------------------------
-    ;; Layer 3: Scoped effects (the bridge)
-    ;; -----------------------------------------------------------------------
-
-    (h2 :class "text-xl font-bold mt-12 mb-4" "Layer 3: Scoped and Higher-Order Effects")
-
-    (p "Wu, Schrijvers, and Hinze (2014) introduced " (em "scoped effects") " \u2014 "
-       "algebraic effects extended with operations that delimit regions. "
-       "Pirog, Polesiuk, and Sieczkowski (2018) proved these are "
-       (strong "strictly more expressive") " than standard algebraic effects.")
-
-    (p "Bach Poulsen and van der Rest (2023) generalized further with "
-       (em "hefty algebras") " \u2014 a framework that captures " (em "all") " known higher-order effects, "
-       "with scoped effects as a special case. This is the current state of the art.")
-
-    (p "SX's " (code "provide") " is a scoped effect. It creates a region (the body), "
-       "makes a value available within it (context), and collects contributions from within it (emit/emitted). "
-       "This is why it can express things that plain algebraic effects can't: "
-       "the region boundary is part of the effect, not an accident of the call stack.")
-
    ;; -----------------------------------------------------------------------
    ;; The floor proof
    ;; -----------------------------------------------------------------------
@@ -228,85 +199,96 @@

    (ul :class "list-disc pl-6 mb-4 space-y-1"
      (li (strong "C without E") " = combinatory logic. Turing-complete but inhumane. "
-          "No named bindings \u2014 everything via S, K, I combinators. "
-          "Proves you can drop E in theory, but the resulting system "
-          "can't express abstraction (which is what E provides).")
+          "No named bindings \u2014 everything via S, K, I combinators.")
      (li (strong "C without K") " = single expression evaluation. "
-          "You can compute one thing but can't compose it with anything. "
-          "Technically you can encode K into C (CPS transform), "
-          "but this transforms the expression to include the continuation explicitly \u2014 "
-          "K hasn't been removed, just moved into C.")
+          "You can compute one thing but can't compose it with anything.")
      (li (strong "E without C") " = a phone book with no one to call.")
      (li (strong "K without C") " = a to-do list with nothing on it."))

    (p "You can " (em "encode") " any register into another (CPS eliminates K, "
       "De Bruijn indices eliminate E), but encoding isn't elimination. "
-       "The information is still there, just hidden in a different representation. "
-       "Three independent concerns; three registers.")
+       "The information is still there, just hidden in a different representation.")

    ;; -----------------------------------------------------------------------
-    ;; Open questions
+    ;; Digging deeper: what's next
    ;; -----------------------------------------------------------------------

-    (h2 :class "text-xl font-bold mt-12 mb-4" "Open Questions")
+    (h2 :class "text-xl font-bold mt-12 mb-4" "Digging Deeper")

-    (p "The hierarchy above is well-established for " (em "sequential") " computation. "
-       "But there are orthogonal axes where the story is incomplete:")
+    (p "The hierarchy is built. Now we test whether the floor is solid. "
+       "Each step below validates the foundation before superstructure is added.")

-    (h3 :class "text-lg font-semibold mt-8 mb-3" "Concurrency")
+    (h3 :class "text-lg font-semibold mt-8 mb-3" "Step 1: Serializable CEK state")

-    (p "Scoped effects assume tree-shaped execution: one thing happens, then the next. "
-       "But real computation forks:")
+    (p (code "make-cek-state") " already returns a plain dict. Can we serialize it, "
+       "ship it to another machine, and resume?")
+
+    (~docs/code :code
+      (str ";; Freeze a computation mid-flight\n"
+           "(let ((state (make-cek-state expr env (list))))\n"
+           "  ;; Step a few times\n"
+           "  (let ((state2 (cek-step (cek-step state))))\n"
+           "    ;; Serialize to JSON\n"
+           "    (json-serialize state2)\n"
+           "    ;; Ship to worker, persist to disk, or content-address as CID\n"
+           "    ))"))
+
+    (p "If this works, every SX computation is a value. "
+       "If it breaks, the state representation needs fixing " (em "before") " we build channels and fork/join on top.")

    (ul :class "list-disc pl-6 mb-4 space-y-1"
-      (li "Video processing \u2014 pipeline stages run in parallel, frames are processed concurrently")
-      (li "CI/CD \u2014 test suites fork, builds parallelize, deployment is staged")
-      (li "Web rendering \u2014 async I/O, streaming SSE, suspense boundaries")
-      (li "Art DAG \u2014 the entire engine is a DAG of dependent transforms"))
+      (li "Can environments serialize? (They're dicts with parent chains \u2014 cycles?)")
+      (li "Can continuations serialize? (Frames are dicts, but closures inside them?)")
+      (li "Can native functions serialize? (No \u2014 need a registry mapping names to functions)")
+      (li "What about signals? (Dict with mutable subscribers list \u2014 serialize the value, not the graph)"))

-    (p "The \u03c0-calculus (Milner 1999) handles concurrency well but not effects. "
-       "Effect systems handle effects well but not concurrency. "
-       "Combining them is an open problem. "
-       "Brachth\u00e4user, Schuster, and Ostermann (2020) have partial results for "
-       "algebraic effects with multi-shot handlers (where the continuation can be invoked "
-       "on multiple concurrent threads), but a full synthesis doesn't exist yet.")
+    (h3 :class "text-lg font-semibold mt-8 mb-3" "Step 2: CEK stepping debugger")

-    (p "For SX, this matters because the Art DAG is fundamentally a concurrent execution engine. "
-       "If SX ever specifies DAG execution natively, it'll need something beyond scoped effects.")
+    (p (code "cek-step") " is pure data\u2192data. A debugger is just a UI over it:")

-    (h3 :class "text-lg font-semibold mt-8 mb-3" "Linearity")
+    (~docs/code :code
+      (str ";; The debugger is an island that renders CEK state\n"
+           "(defisland ~debugger (&key expr)\n"
+           "  (let ((state (signal (make-cek-state (parse expr) env (list)))))\n"
+           "    (div\n"
+           "      (button :on-click (fn () (swap! state cek-step)) \"Step\")\n"
+           "      (pre (str \"C: \" (inspect (get (deref state) \"control\"))))\n"
+           "      (pre (str \"K: \" (len (get (deref state) \"kont\")) \" frames\")))))"))

-    (p "Can an effect handler be invoked more than once? Must a scope be entered? "
-       "Must every emitted value be consumed?")
+    (p "This is a live island. Each click of Step calls " (code "cek-step") " on the state signal. "
+       "The deref-as-shift mechanism updates the DOM. No framework, no virtual DOM, no diffing.")
+
+    (h3 :class "text-lg font-semibold mt-8 mb-3" "Step 3: Content-addressed computation")
+
+    (p "Hash a CEK state \u2192 CID. This is where SX meets the Art DAG:")

    (ul :class "list-disc pl-6 mb-4 space-y-1"
-      (li (strong "Unrestricted") " \u2014 use as many times as you want (current SX)")
-      (li (strong "Affine") " \u2014 use at most once (Rust's ownership model)")
-      (li (strong "Linear") " \u2014 use exactly once (quantum no-cloning, exactly-once delivery)"))
+      (li "A CID identifies a computation in progress, not just a value")
+      (li "Two machines given the same CID produce the same result (deterministic)")
+      (li "Memoize: if you've already run this state, return the cached result")
+      (li "Distribute: ship the CID to whichever machine has the data it needs")
+      (li "Verify: re-run from the CID, check the result matches"))

-    (p "Linear types constrain the continuation: if a handler is linear, "
-       "it " (em "must") " resume the computation exactly once. No dropping (resource leak), "
-       "no duplicating (nondeterminism). This connects to:")
+    (p "This requires solving Step 1 (serialization) first. "
+       "Content-addressing is serialization + hashing.")

-    (ul :class "list-disc pl-6 mb-4 space-y-1"
-      (li "Resource management \u2014 file handles that " (em "must") " be closed")
-      (li "Protocol correctness \u2014 a session type that must complete")
-      (li "Transaction semantics \u2014 exactly-once commit/rollback")
-      (li "Quantum computing \u2014 no-cloning theorem as a type constraint"))
+    (h3 :class "text-lg font-semibold mt-8 mb-3" "Step 4: Concurrent CEK")

-    (p "Benton (1994) established the connection between linear logic and computation. "
-       "Adding linear effects to SX would constrain what handlers can do, "
-       "enabling stronger guarantees about resource safety. "
-       "This is orthogonal to depth \u2014 it's about " (em "discipline") ", not " (em "power") ".")
+    (p "Multiple CEK machines running in parallel, communicating via channels:")

-    (h3 :class "text-lg font-semibold mt-8 mb-3" "Higher-order effects beyond hefty algebras")
+    (~docs/code :code
+      (str ";; Fork: two CEK states from one\n"
+           "(let ((left  (make-cek-state expr-a env (list)))\n"
+           "      (right (make-cek-state expr-b env (list))))\n"
+           "  ;; Interleave steps\n"
+           "  (scheduler (list left right)))"))

-    (p "Nobody has proved that hefty algebras capture " (em "all possible") " higher-order effects. "
-       "The hierarchy might continue. This is active research with no clear terminus. "
-       "The question \"is there a structured effect that no framework can express?\" "
-       "is analogous to G\u00f6del's incompleteness \u2014 it may be that every effect framework "
-       "has blind spots, and the only \"complete\" system is raw continuations (layer 1), "
-       "which are universal but unstructured.")
+    (p "The Art DAG is the natural first consumer. Its execution model is already "
+       "a DAG of dependent computations. CEK states as DAG nodes. "
+       "Channels as edges. The scheduler is the DAG executor.")
+
+    (p "This is where scoped effects meet the \u03c0-calculus. "
+       "But it depends on Steps 1\u20133 being solid.")

    ;; -----------------------------------------------------------------------
    ;; The three-axis model
@@ -318,242 +300,29 @@
       "It's a point in a three-dimensional space:")

    (~docs/code :code
-      (str "depth:     CEK \u2192 continuations \u2192 algebraic effects \u2192 scoped effects\n"
-           "topology:  sequential \u2192 concurrent \u2192 distributed\n"
-           "linearity: unrestricted \u2192 affine \u2192 linear"))
+      (str "depth:     CEK \u2192 continuations \u2192 algebraic effects \u2192 scoped effects    [all done]\n"
+           "topology:  sequential \u2192 concurrent \u2192 distributed                        [sequential done]\n"
+           "linearity: unrestricted \u2192 affine \u2192 linear                               [unrestricted done]"))

-    (p "Each axis is independent. You can have:")
-
-    (ul :class "list-disc pl-6 mb-4 space-y-1"
-      (li "Scoped effects + sequential + unrestricted \u2014 " (strong "SX today"))
-      (li "Scoped effects + concurrent + unrestricted \u2014 the Art DAG integration")
-      (li "Scoped effects + sequential + linear \u2014 resource-safe SX")
-      (li "Algebraic effects + concurrent + linear \u2014 something like Rust + Tokio + effect handlers")
-      (li "CEK + distributed + unrestricted \u2014 raw Erlang/BEAM"))
-
-    (p "SX's current position and trajectory:")
+    (p "Each axis is independent. SX's current position:")

    (div :class "overflow-x-auto mb-6"
      (table :class "min-w-full text-sm"
        (thead (tr
          (th :class "text-left pr-4 pb-2 font-semibold" "Axis")
          (th :class "text-left pr-4 pb-2 font-semibold" "Current")
-          (th :class "text-left pr-4 pb-2 font-semibold" "Next")
-          (th :class "text-left pb-2 font-semibold" "Eventual")))
+          (th :class "text-left pb-2 font-semibold" "Next")))
        (tbody
          (tr (td :class "pr-4 py-1" "Depth")
-              (td :class "pr-4" "Layer 4 (patterns) + Layer 1 (continuations)")
-              (td :class "pr-4" "Layer 3 (scoped effects)")
-              (td "Layer 0 (explicit CEK)"))
+              (td :class "pr-4" "All layers (0\u20134) implemented")
+              (td "Validate via serialization + stepping"))
          (tr (td :class "pr-4 py-1" "Topology")
-              (td :class "pr-4" "Sequential")
-              (td :class "pr-4" "Async I/O (partial concurrency)")
-              (td "DAG execution (Art DAG)"))
+              (td :class "pr-4" "Sequential (+ async I/O)")
+              (td "Concurrent CEK (Art DAG integration)"))
          (tr (td :class "pr-4 py-1" "Linearity")
-              (td :class "pr-4" "Unrestricted")
              (td :class "pr-4" "Unrestricted")
              (td "Affine (resource safety)")))))

-    ;; -----------------------------------------------------------------------
-    ;; What explicit CEK gives SX
-    ;; -----------------------------------------------------------------------
-
-    (h2 :class "text-xl font-bold mt-12 mb-4" "What Explicit CEK Gives SX")
-
-    (p "Making the CEK machine explicit in the spec (rather than implicit in eval-expr) enables:")
-
-    (h3 :class "text-lg font-semibold mt-8 mb-3" "Stepping")
-
-    (p "A CEK machine transitions one step at a time. "
-       "If the transition function is explicit, you can:")
-
-    (ul :class "list-disc pl-6 mb-4 space-y-1"
-      (li "Single-step through evaluation (debugger)")
-      (li "Pause and serialize mid-evaluation (suspend to disk, resume on another machine)")
-      (li "Instrument each step (profiling, tracing, time-travel debugging)")
-      (li "Interleave steps from multiple computations (cooperative scheduling without OS threads)"))
-
-    (h3 :class "text-lg font-semibold mt-8 mb-3" "Serializable computation")
-
-    (p "If C, E, and K are all data structures (not host stack frames), "
-       "the entire computation state is serializable:")
-
-    (~docs/code :code
-      (str ";; Freeze a computation mid-flight\n"
-           "(let ((state (capture-cek)))\n"
-           "  (send-to-worker state)  ;; ship to another machine\n"
-           "  ;; or: (store state)    ;; persist to disk\n"
-           "  ;; or: (fork state)     ;; run the same computation twice\n"
-           "  )"))
-
-    (p "This connects to content-addressed computation: "
-       "a CID identifying a CEK state is a pointer to a computation in progress. "
-       "Resume it anywhere. Verify it. Cache it. Share it.")
-
-    (h3 :class "text-lg font-semibold mt-8 mb-3" "Formal verification")
-
-    (p "An explicit CEK machine is a state machine. State machines are verifiable. "
-       "You can prove properties about all possible execution paths: "
-       "termination, resource bounds, effect safety. "
-       "The theorem prover (prove.sx) could verify CEK transitions directly.")
-
-    ;; -----------------------------------------------------------------------
-    ;; SX's existing layers
-    ;; -----------------------------------------------------------------------
-
-    (h2 :class "text-xl font-bold mt-12 mb-4" "SX's Existing Layers")
-
-    (p "SX already has most of the hierarchy, specced or planned:")
-
-    (div :class "overflow-x-auto mb-6"
-      (table :class "min-w-full text-sm"
-        (thead (tr
-          (th :class "text-left pr-4 pb-2 font-semibold" "Layer")
-          (th :class "text-left pr-4 pb-2 font-semibold" "SX has")
-          (th :class "text-left pr-4 pb-2 font-semibold" "Where")
-          (th :class "text-left pb-2 font-semibold" "Status")))
-        (tbody
-          (tr (td :class "pr-4 py-1" "0 \u2014 CEK")
-              (td :class "pr-4" "eval-expr + trampoline")
-              (td :class "pr-4" "eval.sx")
-              (td "Implicit. Works, but CEK is hidden in the host call stack."))
-          (tr (td :class "pr-4 py-1" "1 \u2014 Continuations")
-              (td :class "pr-4" "shift / reset")
-              (td :class "pr-4" "continuations.sx")
-              (td "Specced. Bootstraps to Python and JavaScript."))
-          (tr (td :class "pr-4 py-1" "2 \u2014 Algebraic effects")
-              (td :class "pr-4" "\u2014")
-              (td :class "pr-4" "\u2014")
-              (td "Falls out of layers 1 + 3. No dedicated spec needed."))
-          (tr (td :class "pr-4 py-1" "3 \u2014 Scoped effects")
-              (td :class "pr-4" "provide / context / emit!")
-              (td :class "pr-4" "scoped-effects plan")
-              (td "Planned. Implements over eval.sx + adapters."))
-          (tr (td :class "pr-4 py-1" "4 \u2014 Patterns")
-              (td :class "pr-4" "spread, collect, island, lake, signal, store")
-              (td :class "pr-4" "various .sx files")
-              (td "Implemented. Will be redefined in terms of layer 3.")))))
-
-    ;; -----------------------------------------------------------------------
-    ;; Implementation path
-    ;; -----------------------------------------------------------------------
-
-    (h2 :class "text-xl font-bold mt-12 mb-4" "Implementation Path")
-
-    (h3 :class "text-lg font-semibold mt-8 mb-3" "Phase 1: Scoped effects (Layer 3)")
-
-    (p "This is the scoped-effects plan. Immediate next step.")
-
-    (ul :class "list-disc pl-6 mb-4 space-y-1"
-      (li "Spec " (code "provide") ", " (code "context") ", " (code "emit!") ", " (code "emitted") " in eval.sx")
-      (li "Implement in all adapters (HTML, DOM, SX wire, async)")
-      (li "Redefine spread, collect, and reactive-spread as instances")
-      (li "Prove existing tests still pass"))
-
-    (h3 :class "text-lg font-semibold mt-8 mb-3" "Phase 2: Effect signatures (Layer 2)")
-
-    (p "Add optional effect annotations to function definitions:")
-
-    (~docs/code :code
-      (str ";; Declare what effects a function uses\n"
-           "(define fetch-user :effects [io auth]\n"
-           "  (fn (id) ...))\n"
-           "\n"
-           ";; Pure function \u2014 no effects\n"
-           "(define add :effects []\n"
-           "  (fn (a b) (+ a b)))\n"
-           "\n"
-           ";; Scoped effect \u2014 uses context + emit\n"
-           "(define themed-heading :effects [context]\n"
-           "  (fn (text)\n"
-           "    (h1 :style (str \"color:\" (get (context \"theme\") :primary))\n"
-           "      text)))"))
-
-    (p "Effect signatures are checked at registration time. "
-       "A function that declares " (code ":effects []") " cannot call " (code "emit!") " or " (code "context") ". "
-       "This is layer 2 \u2014 algebraic effect structure \u2014 applied as a type discipline.")
-
-    (h3 :class "text-lg font-semibold mt-8 mb-3" "Phase 3: Explicit CEK (Layer 0)")
-
-    (p "Refactor eval.sx to expose the CEK registers as data:")
-
-    (~docs/code :code
-      (str ";; The CEK state is a value\n"
-           "(define-record CEK\n"
-           "  :control  expr       ;; the expression\n"
-           "  :env      env        ;; the bindings\n"
-           "  :kont     kont)      ;; the continuation stack\n"
-           "\n"
-           ";; One step\n"
-           "(define step :effects []\n"
-           "  (fn (cek)\n"
-           "    (case (type-of (get cek :control))\n"
-           "      :literal  (apply-kont (get cek :kont) (get cek :control))\n"
-           "      :symbol   (apply-kont (get cek :kont)\n"
-           "                            (env-get (get cek :env) (get cek :control)))\n"
-           "      :list     (let ((head (first (get cek :control))))\n"
-           "                  ...))))\n"
-           "\n"
-           ";; Run to completion\n"
-           "(define run :effects []\n"
-           "  (fn (cek)\n"
-           "    (if (final? cek)\n"
-           "      (get cek :control)\n"
-           "      (run (step cek)))))"))
-
-    (p "This makes computation " (em "inspectable") ". A CEK state can be:")
-
-    (ul :class "list-disc pl-6 mb-4 space-y-1"
-      (li "Serialized to a CID (content-addressed frozen computation)")
-      (li "Single-stepped by a debugger")
-      (li "Forked (run the same state with different inputs)")
-      (li "Migrated (ship to another machine, resume there)")
-      (li "Verified (prove properties about all reachable states)"))
-
-    (h3 :class "text-lg font-semibold mt-8 mb-3" "Phase 4: Concurrent effects (topology axis)")
-
-    (p "Extend the CEK machine to support multiple concurrent computations:")
-
-    (~docs/code :code
-      (str ";; Fork: create two CEK states from one\n"
-           "(define fork :effects [concurrency]\n"
-           "  (fn (cek)\n"
-           "    (list (step cek) (step cek))))\n"
-           "\n"
-           ";; Join: merge results from two computations\n"
-           "(define join :effects [concurrency]\n"
-           "  (fn (cek-a cek-b combine)\n"
-           "    (combine (run cek-a) (run cek-b))))\n"
-           "\n"
-           ";; Channel: typed communication between concurrent computations\n"
-           "(define channel :effects [concurrency]\n"
-           "  (fn (name)\n"
-           "    {:send (fn (v) (emit! name v))\n"
-           "     :recv (fn () (shift k (handle-recv name k)))}))"))
-
-    (p "This is where scoped effects meet the \u03c0-calculus. "
-       "The Art DAG is the natural first consumer \u2014 "
-       "its execution model is already a DAG of dependent computations.")
-
-    (h3 :class "text-lg font-semibold mt-8 mb-3" "Phase 5: Linear effects (linearity axis)")
-
-    (p "Add resource-safety constraints:")
-
-    (~docs/code :code
-      (str ";; Linear scope: must be entered, must complete\n"
-           "(define-linear open-file :effects [io linear]\n"
-           "  (fn (path)\n"
-           "    (provide \"file\" (fs-open path)\n"
-           "      ;; body MUST consume the file handle exactly once\n"
-           "      ;; compiler error if handle is dropped or duplicated\n"
-           "      (yield (file-read (context \"file\")))\n"
-           "      ;; cleanup runs unconditionally\n"
-           "      )))"))
-
-    (p "This is the furthest horizon. "
-       "Linear effects connect SX to session types, protocol verification, "
-       "and the kind of safety guarantees that Rust provides at the type level.")
-
    ;; -----------------------------------------------------------------------
    ;; The Curry-Howard correspondence
    ;; -----------------------------------------------------------------------
@@ -584,21 +353,9 @@
          (tr (td :class "pr-4 py-1" "Implication (A \u2192 B)")
              (td :class "pr-4" "Function type")
              (td "Lambda"))
-          (tr (td :class "pr-4 py-1" "Conjunction (A \u2227 B)")
-              (td :class "pr-4" "Product type")
-              (td "Dict / record"))
-          (tr (td :class "pr-4 py-1" "Disjunction (A \u2228 B)")
-              (td :class "pr-4" "Sum type / union")
-              (td "Case dispatch"))
-          (tr (td :class "pr-4 py-1" "Universal (\u2200x.P)")
-              (td :class "pr-4" "Polymorphism")
-              (td "Generic components"))
-          (tr (td :class "pr-4 py-1" "Existential (\u2203x.P)")
-              (td :class "pr-4" "Abstract type")
-              (td "Opaque scope"))
          (tr (td :class "pr-4 py-1" "Double negation (\u00ac\u00acA)")
              (td :class "pr-4" "Continuation")
-              (td "shift/reset")))))
+              (td "shift/reset, deref-as-shift")))))

    (p "A program is a proof that a computation is possible. "
       "An effect signature is a proposition about what the program does to the world. "
@@ -607,8 +364,7 @@

    (p "This is why CEK is the floor: it " (em "is") " logic. "
       "Expression = proposition, environment = hypotheses, continuation = proof context. "
-       "You can't go beneath logic and still be doing computation. "
-       "The Curry\u2013Howard correspondence is not a metaphor. It's an isomorphism.")
+       "You can't go beneath logic and still be doing computation.")

    ;; -----------------------------------------------------------------------
    ;; Summary
@@ -616,46 +372,19 @@

    (h2 :class "text-xl font-bold mt-12 mb-4" "Summary")

-    (p "The path from where SX stands to the computational floor:")
+    (p "The depth axis is complete. Every layer from patterns down to raw CEK "
+       "is specced, bootstrapped, and tested. 89 tests across three suites.")

-    (div :class "overflow-x-auto mb-6"
-      (table :class "min-w-full text-sm"
-        (thead (tr
-          (th :class "text-left pr-4 pb-2 font-semibold" "Step")
-          (th :class "text-left pr-4 pb-2 font-semibold" "What")
-          (th :class "text-left pr-4 pb-2 font-semibold" "Enables")
-          (th :class "text-left pb-2 font-semibold" "Depends on")))
-        (tbody
-          (tr (td :class "pr-4 py-1" "1")
-              (td :class "pr-4" "Scoped effects")
-              (td :class "pr-4" "Unify spread/collect/island/lake/context")
-              (td "eval.sx + adapters"))
-          (tr (td :class "pr-4 py-1" "2")
-              (td :class "pr-4" "Effect signatures")
-              (td :class "pr-4" "Static effect checking, pure/IO boundary")
-              (td "types.sx + scoped effects"))
-          (tr (td :class "pr-4 py-1" "3")
-              (td :class "pr-4" "Explicit CEK")
-              (td :class "pr-4" "Stepping, serialization, migration, verification")
-              (td "eval.sx refactor"))
-          (tr (td :class "pr-4 py-1" "4")
-              (td :class "pr-4" "Concurrent effects")
-              (td :class "pr-4" "DAG execution, parallel pipelines")
-              (td "CEK + channels"))
-          (tr (td :class "pr-4 py-1" "5")
-              (td :class "pr-4" "Linear effects")
-              (td :class "pr-4" "Resource safety, protocol verification")
-              (td "Effect signatures + linear types")))))
+    (p "The next moves are lateral, not downward:")

-    (p "Each step is independently valuable. The first is immediate. "
-       "The last may be years out or may never arrive. "
-       "The hierarchy exists whether we traverse it or not \u2014 "
-       "it's the structure of computation itself, "
-       "and SX is better for knowing where it sits within it.")
+    (ul :class "list-disc pl-6 mb-4 space-y-1"
+      (li (strong "Validate the floor") " \u2014 serialize CEK state, build a stepping debugger, "
+          "content-address computations. These test whether the foundation holds weight.")
+      (li (strong "Topology") " \u2014 concurrent CEK for the Art DAG. Multiple machines, channels, scheduling.")
+      (li (strong "Linearity") " \u2014 resource safety. Affine continuations that must be resumed exactly once."))
+
+    (p "Each step is independently valuable. The foundation is built. "
+       "Now we find out what it can carry.")

    (p :class "text-stone-500 text-sm italic mt-12"
-       "The true foundation of any language is not its syntax or its runtime "
-       "but the mathematical structure it participates in. "
-       "SX is an s-expression language, which makes it a notation for the lambda calculus, "
-       "which is a notation for logic, which is the structure of thought. "
       "The floor is thought itself. We can't go deeper, because there's no one left to dig.")))
--- a/sx/sxc/init-client.sx.txt
+++ b/sx/sxc/init-client.sx.txt
@@ -1,5 +1,5 @@
 ;; ---------------------------------------------------------------------------
-;; SX app boot — styles and behaviors injected on page load
+;; SX app boot — styles, behaviors, and post-render hooks
 ;;
 ;; Replaces inline_css and init_sx from Python app config.
 ;; Called as a data-init script on every page.
@@ -11,6 +11,25 @@
 (collect! "cssx" "@keyframes sxJiggle{0%,100%{transform:translateX(0)}25%{transform:translateX(-.5px)}75%{transform:translateX(.5px)}}")
 (collect! "cssx" "a.sx-request{animation:sxJiggle .3s ease-in-out infinite}")

+;; CSSX flush hook — inject collected CSS rules into a <style> tag.
+;; The spec calls (run-post-render-hooks) after hydration/swap/mount.
+;; This is the application's CSS injection strategy.
+(console-log "init-client: registering cssx flush hook, type:" (type-of (fn () nil)))
+(register-post-render-hook
+  (fn ()
+    (console-log "cssx flush: running, rules:" (len (collected "cssx")))
+    (let ((rules (collected "cssx")))
+      (when (not (empty? rules))
+        (let ((style (or (dom-query "[data-cssx]")
+                         (let ((s (dom-create-element "style" nil)))
+                           (dom-set-attr s "data-cssx" "")
+                           (dom-append-to-head s)
+                           s))))
+          (dom-set-prop style "textContent"
+            (str (or (dom-get-prop style "textContent") "")
+                 (join "" rules))))
+        (clear-collected! "cssx")))))
+
 ;; Nav link aria-selected update on client-side routing
 (dom-listen (dom-body) "sx:clientRoute"
  (fn (e)
Author	SHA1	Message	Date
giles	4dd9968264	Fix bracket highlighting: both ( and ) share open step index All checks were successful Build and Deploy / build-and-deploy (push) Successful in 7m59s Details When a tag's open step is evaluated, both its opening and closing brackets go big+bold together. Previously close ) had the close step index so it stayed faint until much later. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>	2026-03-14 22:00:43 +00:00
giles	7cc1bffc23	Reactive code view stepper for home page All checks were successful Build and Deploy / build-and-deploy (push) Successful in 25s Details - Imperative code view with syntax colouring matching highlight.py - Token step indices aligned with split-tag (16 steps) - Component spreads (~cssx/tw) dimmed, not highlighted - Evaluated tokens bold+larger, current amber bg+largest, future faint - Lakes for DOM preview and code view (survive reactive re-renders) - dom-stack as signal (persists across re-renders) - schedule-idle for initial code DOM build + step replay - post-render hooks flush CSSX after each event handler - Self-registering spec defines (js-emit-define emits PRIMITIVES[]) - Generic render hooks replace flush-cssx-to-dom in spec - Fix nil→NIL in platform JS, fix append semantics Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>	2026-03-14 21:58:42 +00:00
giles	169097097c	Imperative code view: spans built once, classes updated on each step All checks were successful Build and Deploy / build-and-deploy (push) Successful in 27s Details Code view uses a lake with imperative DOM spans. Each token has its base syntax colour class stored. On each step, update-code-highlight iterates all spans and sets class based on step-idx: evaluated tokens go bold, current step gets violet bg, future stays normal. No reactive re-rendering of the code view — direct DOM class updates. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>	2026-03-14 21:21:14 +00:00
giles	a7638e48d5	Reactive code view with syntax colouring, fix indenting and nil refs All checks were successful Build and Deploy / build-and-deploy (push) Successful in 1m3s Details - Each token span independently reacts to step-idx via deref-as-shift - Colours match highlight.py: sky for HTML tags, rose for components, emerald for strings, violet for keywords, amber for numbers - Current step bold+violet bg, completed steps dimmed - No closing paren on separate line - Fix bare nil → NIL in eventDetail and domGetData Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>	2026-03-14 20:43:57 +00:00
giles	93e140280b	Add reactive render stepper to home page, fix nil→NIL in platform JS All checks were successful Build and Deploy / build-and-deploy (push) Successful in 3m13s Details Home page stepper: reactive code view with syntax colouring where tokens highlight as you step through DOM construction. Each token is a span with signal-driven classes — current step bold+violet, completed steps dimmed, upcoming normal. CSSX styling via ~cssx/tw spreads. Lake preserves imperative DOM across reactive re-renders. Also fixes: bare lowercase 'nil' in platform_js.py eventDetail and domGetData — should be NIL (the SX sentinel object). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>	2026-03-14 20:40:24 +00:00
giles	07bf5a1142	Add render stepper to home page All checks were successful Build and Deploy / build-and-deploy (push) Successful in 10s Details Replace header source view with interactive CEK render stepper. Auto-parses on mount, step forward/back through DOM construction with CSSX styling. Uses lake for preview persistence. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>	2026-03-14 20:33:40 +00:00
giles	623f947b52	Fix duplicate sx-cssx-live style tags All checks were successful Build and Deploy / build-and-deploy (push) Successful in 21s Details Cache the style element reference in _cssx-style-el so flush-cssx-to-dom never creates more than one. Previous code called dom-query on every flush, which could miss the element during rapid successive calls, creating duplicates. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>	2026-03-14 20:08:36 +00:00
giles	41f4772ba7	Strip legacy CSS from SX app: no Prism, Ghost, FontAwesome extras All checks were successful Build and Deploy / build-and-deploy (push) Successful in 5m10s Details Add css_extras parameter to create_base_app. Legacy apps (blog, market etc) get the default extras (basics.css, cards.css, blog-content.css, prism.css, FontAwesome). SX app passes css_extras=[] — it uses CSSX for styling and custom highlighting, not Prism/FA/Ghost. Reduces <style id="sx-css"> from ~100KB+ of irrelevant CSS to ~5KB of Tailwind resets + only the utility rules the page actually uses. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>	2026-03-14 16:17:27 +00:00
giles	ae1ba46b44	Add live CEK stepper island — interactive stepping debugger All checks were successful Build and Deploy / build-and-deploy (push) Successful in 33s Details A defisland that lets users type an SX expression, step through CEK evaluation one transition at a time, and see C/E/K registers update live. Demonstrates that cek-step is pure data->data. - cek.sx geography: add ~geography/cek/demo-stepper island with source input, step/run/reset buttons, state display, step history - platform_js.py: register CEK stepping primitives (make-cek-state, cek-step, cek-terminal?, cek-value, make-env, sx-serialize) so island code can access them Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>	2026-03-14 16:02:41 +00:00
giles	0047757af8	Add Platonic SX essay to philosophy section Plato's allegory of the cave applied to web development: HTML/CSS/JS as shadows on the wall, s-expressions as Forms, the bootstrapper as demiurge, anamnesis as the wire format's efficiency, the divided line as SX's rendering hierarchy, and the Form of the Good as the principle that representation and thing represented should be identical. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>	2026-03-14 13:25:10 +00:00
giles	b3cba5e281	Update foundations plan: all five layers complete, reframe next steps The depth axis is done — CEK (Layer 0) through patterns (Layer 4) are all specced, bootstrapped, and tested. Rewrite the plan to reflect reality and reframe the next steps as validation (serialization, stepping debugger, content-addressed computation) before building superstructure (concurrent CEK, linear effects). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>	2026-03-14 13:20:07 +00:00