;; Foundations — The Computational Floor
;; From scoped effects to CEK: what's beneath algebraic effects and why it's the limit.

(defcomp ()
  (~docs/page :title "Foundations \u2014 The Computational Floor"

    (p (~tw :tokens "text-stone-500 text-sm italic mb-8")
      "Scoped effects unify everything SX does. But they are not the bottom. "
      "Beneath them is a hierarchy of increasingly fundamental primitives, "
      "terminating at three irreducible things: an expression, an environment, and a continuation. "
      "This document traces that hierarchy, proves where the floor is, "
      "and maps the path from where SX stands to the deepest layer.")

    ;; -----------------------------------------------------------------------
    ;; The hierarchy
    ;; -----------------------------------------------------------------------

    (h2 (~tw :tokens "text-xl font-bold mt-12 mb-4") "The Hierarchy")

    (p "Every layer is definable in terms of the one below. "
       "No layer can be decomposed without the layer beneath it.")

    (~docs/code :src
      (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 "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 (~tw :tokens "text-xl font-bold mt-12 mb-4") "What We Built")

    (div (~tw :tokens "overflow-x-auto mb-6")
      (table (~tw :tokens "min-w-full text-sm")
        (thead (tr
          (th (~tw :tokens "text-left pr-4 pb-2 font-semibold") "Layer")
          (th (~tw :tokens "text-left pr-4 pb-2 font-semibold") "Spec files")
          (th (~tw :tokens "text-left pr-4 pb-2 font-semibold") "What it provides")
          (th (~tw :tokens "text-left pb-2 font-semibold") "Tests")))
        (tbody
          (tr (td (~tw :tokens "pr-4 py-1") "0 \u2014 CEK")
              (td (~tw :tokens "pr-4 font-mono text-xs") "cek.sx, frames.sx")
              (td (~tw :tokens "pr-4") "Explicit step function, 20+ frame types, cek-call dispatch, CEK-native HO forms")
              (td "43 CEK + 26 reactive"))
          (tr (td (~tw :tokens "pr-4 py-1") "1 \u2014 Continuations")
              (td (~tw :tokens "pr-4 font-mono text-xs") "continuations.sx, callcc.sx")
              (td (~tw :tokens "pr-4") "shift/reset (delimited), call/cc (full), ReactiveResetFrame + DerefFrame")
              (td "Continuation tests"))
          (tr (td (~tw :tokens "pr-4 py-1") "2 \u2014 Effect signatures")
              (td (~tw :tokens "pr-4 font-mono text-xs") "boundary.sx, eval.sx")
              (td (~tw :tokens "pr-4") ":effects annotations on define, boundary enforcement at startup")
              (td "Boundary validation"))
          (tr (td (~tw :tokens "pr-4 py-1") "3 \u2014 Scoped effects")
              (td (~tw :tokens "pr-4 font-mono text-xs") "eval.sx, adapters")
              (td (~tw :tokens "pr-4") "scope/provide/context/emit!/emitted, scope-push!/scope-pop!")
              (td "Scope integration"))
          (tr (td (~tw :tokens "pr-4 py-1") "4 \u2014 Patterns")
              (td (~tw :tokens "pr-4 font-mono text-xs") "signals.sx, adapter-dom.sx, engine.sx")
              (td (~tw :tokens "pr-4") "signal/deref/computed/effect/batch, island/lake, spread/collect")
              (td "20 signal + 26 CEK reactive")))))

    ;; -----------------------------------------------------------------------
    ;; Layer 0: The CEK machine
    ;; -----------------------------------------------------------------------

    (h2 (~tw :tokens "text-xl font-bold mt-12 mb-4") "Layer 0: The CEK Machine")

    (p "The CEK machine (Felleisen & Friedman, 1986) is a small-step evaluator with three registers:")

    (div (~tw :tokens "overflow-x-auto mb-6")
      (table (~tw :tokens "min-w-full text-sm")
        (thead (tr
          (th (~tw :tokens "text-left pr-4 pb-2 font-semibold") "Register")
          (th (~tw :tokens "text-left pr-4 pb-2 font-semibold") "Name")
          (th (~tw :tokens "text-left pb-2 font-semibold") "Meaning")))
        (tbody
          (tr (td (~tw :tokens "pr-4 py-1 font-mono") "C") (td (~tw :tokens "pr-4") "Control") (td "The expression being evaluated"))
          (tr (td (~tw :tokens "pr-4 py-1 font-mono") "E") (td (~tw :tokens "pr-4") "Environment") (td "The bindings in scope \u2014 names to values"))
          (tr (td (~tw :tokens "pr-4 py-1 font-mono") "K") (td (~tw :tokens "pr-4") "Kontinuation") (td "What to do with the result")))))

    (p "Every step of evaluation is a transition: take the current (C, E, K), "
       "produce a new (C\u2032, E\u2032, K\u2032). That's it. That's all computation is.")

    (p "Can you remove any register?")

    (ul (~tw :tokens "list-disc pl-6 mb-4 space-y-1")
      (li (strong "Remove C") " \u2014 nothing to evaluate. No computation.")
      (li (strong "Remove E") " \u2014 names are meaningless. Lose abstraction. "
          "Every value must be literal, every function must be closed. No variables, no closures, no reuse.")
      (li (strong "Remove K") " \u2014 no sequencing. The result of an expression goes nowhere. "
          "Lose composition \u2014 you can evaluate one thing but never connect it to the next."))

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

    (h3 (~tw :tokens "text-lg font-semibold mt-8 mb-3") "CEK in SX")

    (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 (~tw :tokens "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 (~tw :tokens "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 :src
      (str ";; map pushes a MapFrame, calls f on each element via continue-with-call\n"
           "(map (fn (x) (* 2 (deref counter))) items)\n"
           "\n"
           ";; 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 "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
    ;; -----------------------------------------------------------------------

    (h2 (~tw :tokens "text-xl font-bold mt-12 mb-4") "Layer 1: Delimited Continuations")

    (p "Delimited continuations (Felleisen 1988, Danvy & Filinski 1990) "
       "expose the K register as a first-class value:")

    (~docs/code :src
      (str ";; reset marks a point in the continuation\n"
           "(reset\n"
           "  (+ 1 (shift k        ;; k = \"the rest up to reset\"\n"
           "         (k (k 10))))  ;; invoke it twice: 1 + (1 + 10) = 12\n"
           ")"))

    (p (code "reset") " says: \"here's a boundary.\" "
       (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.")

    (h3 (~tw :tokens "text-lg font-semibold mt-8 mb-3") "Deref as shift")

    (p "The reactive payoff. " (code "deref") " inside a " (code "reactive-reset") " boundary "
       "is shift/reset applied to signals:")

    (~docs/code :src
      (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 (~tw :tokens "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, "
       "continuations themselves \u2014 all expressible as shift/reset patterns. "
       "This means layer 1 is already computationally complete for effects. "
       "Everything above is structure, not power.")

    ;; -----------------------------------------------------------------------
    ;; The floor proof
    ;; -----------------------------------------------------------------------

    (h2 (~tw :tokens "text-xl font-bold mt-12 mb-4") "Why Layer 0 Is the Floor")

    (p "Two independent arguments:")

    (h3 (~tw :tokens "text-lg font-semibold mt-8 mb-3") "1. Church\u2013Turing")

    (p "The Church\u2013Turing thesis: any effectively computable function can be computed by "
       "a Turing machine (equivalently, by the lambda calculus, equivalently, by the CEK machine). "
       "This has withstood 90 years of attempts to disprove it. "
       "No formal system has ever been shown to compute more.")

    (p "This means CEK captures " (em "all") " computation. Adding more primitives doesn't let you "
       "compute anything new. It only changes what's " (em "convenient") " to express.")

    (h3 (~tw :tokens "text-lg font-semibold mt-8 mb-3") "2. Irreducibility of C, E, K")

    (p "The three registers are independently necessary:")

    (ul (~tw :tokens "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.")
      (li (strong "C without K") " = single expression evaluation. "
          "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.")

    ;; -----------------------------------------------------------------------
    ;; Digging deeper: what's next
    ;; -----------------------------------------------------------------------

    (h2 (~tw :tokens "text-xl font-bold mt-12 mb-4") "Progress")

    (div (~tw :tokens "overflow-x-auto mb-6")
      (table (~tw :tokens "min-w-full text-sm")
        (thead (tr
          (th (~tw :tokens "text-left pr-4 pb-2 font-semibold") "Step")
          (th (~tw :tokens "text-left pr-4 pb-2 font-semibold") "What")
          (th (~tw :tokens "text-left pb-2 font-semibold") "Status")))
        (tbody
          (tr (td (~tw :tokens "pr-4 py-1") "1")
              (td (~tw :tokens "pr-4") "Serializable CEK state")
              (td (~tw :tokens "text-emerald-600 font-semibold") "\u2714 Done \u2014 freeze-scope, freeze-signal, freeze-to-sx, thaw-from-sx"))
          (tr (td (~tw :tokens "pr-4 py-1") "2")
              (td (~tw :tokens "pr-4") "CEK stepping debugger")
              (td (~tw :tokens "text-emerald-600 font-semibold") "\u2714 Done \u2014 live island with reactive code view, DOM preview"))
          (tr (td (~tw :tokens "pr-4 py-1") "3")
              (td (~tw :tokens "pr-4") "Content-addressed computation")
              (td (~tw :tokens "text-emerald-600 font-semibold") "\u2714 Done \u2014 content-hash, freeze-to-cid, thaw-from-cid"))
          (tr (td (~tw :tokens "pr-4 py-1") "3.5")
              (td (~tw :tokens "pr-4") "Data representations")
              (td (~tw :tokens "text-stone-400") "Planned — byte buffers + typed structs"))
          (tr (td (~tw :tokens "pr-4 py-1") "3.7")
              (td (~tw :tokens "pr-4") "Verified components")
              (td (~tw :tokens "text-stone-400") "Planned — content-addressed UI trust"))
          (tr (td (~tw :tokens "pr-4 py-1") "4")
              (td (~tw :tokens "pr-4") "Concurrent CEK")
              (td (~tw :tokens "text-amber-600 font-semibold") "Spec complete — implementation next"))
          (tr (td (~tw :tokens "pr-4 py-1") "5")
              (td (~tw :tokens "pr-4") "Linear effects")
              (td (~tw :tokens "text-stone-400") "Future")))))

    ;; -----------------------------------------------------------------------
    ;; Step 3.5: Data Representations
    ;; -----------------------------------------------------------------------

    (h2 (~tw :tokens "text-xl font-bold mt-12 mb-4") "Step 3.5: Data Representations")

    (p "Two primitives that sit below concurrency but above the raw CEK machine. "
       "Both are about how values are represented — enabling work that's currently host-only.")

    (h3 (~tw :tokens "text-lg font-semibold mt-8 mb-3") "3.5a Byte Buffers")

    (p "Fixed-size mutable byte arrays. A small primitive surface that unlocks "
       "binary protocol parsing, image headers, wire formats, and efficient CID computation:")

    (~docs/code :src
      (str ";; Create and write\n"
           "(let ((buf (make-buffer 256)))\n"
           "  (buffer-write-u8! buf 0 #xFF)\n"
           "  (buffer-write-u32! buf 1 magic-number)\n"
           "  (buffer-slice buf 0 5))\n"
           "\n"
           ";; Read from network/file\n"
           "(let ((header (buffer-slice packet 0 12)))\n"
           "  (case (buffer-read-u8 header 0)\n"
           "    (1 (parse-handshake header))\n"
           "    (2 (parse-data header))\n"
           "    (else (error \"unknown packet type\"))))"))

    (p "Primitives:")

    (ul (~tw :tokens "list-disc pl-6 mb-4 space-y-1")
      (li (code "make-buffer") " — allocate N zero-filled bytes")
      (li (code "buffer-read-u8/u16/u32") ", " (code "buffer-read-i8/i16/i32") " — typed reads at offset")
      (li (code "buffer-write-u8!/u16!/u32!") " — typed writes at offset (big-endian default)")
      (li (code "buffer-slice") " — zero-copy view of a region")
      (li (code "buffer-length") " — byte count")
      (li (code "buffer->list") ", " (code "list->buffer") " — conversion to/from byte lists")
      (li (code "buffer->string") ", " (code "string->buffer") " — UTF-8 encode/decode"))

    (p "Host mapping:")

    (div (~tw :tokens "overflow-x-auto mb-6")
      (table (~tw :tokens "min-w-full text-sm")
        (thead (tr
          (th (~tw :tokens "text-left pr-4 pb-2 font-semibold") "Primitive")
          (th (~tw :tokens "text-left pr-4 pb-2 font-semibold") "JavaScript")
          (th (~tw :tokens "text-left pr-4 pb-2 font-semibold") "Python")
          (th (~tw :tokens "text-left pb-2 font-semibold") "OCaml")))
        (tbody
          (tr (td (~tw :tokens "pr-4 py-1 font-mono") "make-buffer")
              (td (~tw :tokens "pr-4") "new ArrayBuffer(n)")
              (td (~tw :tokens "pr-4") "bytearray(n)")
              (td "Bytes.create n"))
          (tr (td (~tw :tokens "pr-4 py-1 font-mono") "buffer-read-u32")
              (td (~tw :tokens "pr-4") "DataView.getUint32")
              (td (~tw :tokens "pr-4") "struct.unpack_from")
              (td "Bytes.get_int32_be"))
          (tr (td (~tw :tokens "pr-4 py-1 font-mono") "buffer-slice")
              (td (~tw :tokens "pr-4") "new Uint8Array(buf, off, len)")
              (td (~tw :tokens "pr-4") "memoryview(buf)[off:off+len]")
              (td "Bytes.sub buf off len")))))

    (p "Byte buffers connect directly to content addressing (Step 3). "
       "Computing a CID currently requires host-side hashing of opaque SX text. "
       "With buffers, the hash input can be a canonical binary representation — "
       "deterministic, compact, and consistent across hosts.")

    (h3 (~tw :tokens "text-lg font-semibold mt-8 mb-3") "3.5b Typed Structs")

    (p "Named product types with fixed fields. On interpreted hosts, structs are syntactic sugar over dicts. "
       "On compiled hosts (OCaml, Rust), they compile to unboxed records — no dict overhead, "
       "no hash lookups, no string key comparisons:")

    (~docs/code :src
      (str ";; Define a struct\n"
           "(defstruct point (x : number) (y : number))\n"
           "\n"
           ";; Construct\n"
           "(let ((p (make-point 3 4)))\n"
           "  ;; Access — compiles to field offset on native hosts\n"
           "  (+ (point-x p) (point-y p)))  ;; => 7\n"
           "\n"
           ";; Pattern match\n"
           "(case p\n"
           "  ((point x y) (sqrt (+ (* x x) (* y y)))))  ;; => 5"))

    (p "What " (code "defstruct") " generates:")

    (ul (~tw :tokens "list-disc pl-6 mb-4 space-y-1")
      (li (code "make-point") " — constructor (arity-checked)")
      (li (code "point?") " — type predicate")
      (li (code "point-x") ", " (code "point-y") " — field accessors")
      (li (code "point") " — case pattern for destructuring"))

    (p "The performance difference matters for compiled hosts:")

    (div (~tw :tokens "overflow-x-auto mb-6")
      (table (~tw :tokens "min-w-full text-sm")
        (thead (tr
          (th (~tw :tokens "text-left pr-4 pb-2 font-semibold") "Operation")
          (th (~tw :tokens "text-left pr-4 pb-2 font-semibold") "Dict (current)")
          (th (~tw :tokens "text-left pb-2 font-semibold") "Struct (compiled)")))
        (tbody
          (tr (td (~tw :tokens "pr-4 py-1") "Field access")
              (td (~tw :tokens "pr-4") "Hash lookup — O(1) amortized, cache-unfriendly")
              (td "Offset load — O(1) actual, single instruction"))
          (tr (td (~tw :tokens "pr-4 py-1") "Construction")
              (td (~tw :tokens "pr-4") "Allocate hash table + insert N entries")
              (td "Allocate N words, write sequentially"))
          (tr (td (~tw :tokens "pr-4 py-1") "Pattern match")
              (td (~tw :tokens "pr-4") "N string comparisons")
              (td "Tag check + field projection")))))

    (p "Typed structs connect to the gradual type system in " (code "types.sx") ". "
       "A " (code "defstruct") " declaration is a type definition that the type checker can verify "
       "and the compiler can exploit. On interpreted hosts, the same code runs — just slower.")

    ;; -----------------------------------------------------------------------
    ;; Step 3.7: Verified Components
    ;; -----------------------------------------------------------------------

    (h2 (~tw :tokens "text-xl font-bold mt-12 mb-4") "Step 3.7: Verified Components")

    (p "Content-addressed components become a trust mechanism. "
       "HTTPS tells you the connection is authentic. "
       "Verified components tell you the " (em "UI") " is authentic — "
       "that the payment form in your browser is the exact component that was audited, "
       "not a tampered copy injected by XSS, a rogue extension, or a compromised CDN.")

    (h3 (~tw :tokens "text-lg font-semibold mt-8 mb-3") "Why SX can do this")

    (p "Most frameworks can't verify UI at the component level because there's no stable identity. "
       "A React component is compiled, bundled, minified, tree-shaken — "
       "the thing in the browser bears no relationship to the source. In SX:")

    (ul (~tw :tokens "list-disc pl-6 mb-4 space-y-1")
      (li (strong "Components are source") " — the " (code ".sx") " definition IS the component. No compilation step that could diverge.")
      (li (strong "Components are pure functions") " — same inputs, same output. Deterministic.")
      (li (strong "Content addressing is built in") " — " (code "freeze-to-cid") " gives every component a CID (Step 3).")
      (li (strong "The evaluator runs in the browser") " — the client can independently compute the CID of any component it receives."))

    (p "Because components are pure functions defined in source form, "
       "verifying the definition IS verifying the behaviour. "
       "There is no gap between \"what was audited\" and \"what runs.\" "
       "That gap is where every UI supply chain attack lives.")

    (h3 (~tw :tokens "text-lg font-semibold mt-8 mb-3") "3.7a Transitive closure CID")

    (p "A component's CID must cover its entire dependency tree. "
       "If " (code "~bank/payment-form") " calls " (code "~bank/amount-input") " calls "
       (code "~ui/text-field") ", all three definitions are part of the CID:")

    (~docs/code :src
      (str ";; Shallow CID — just this component's definition\n"
           "(freeze-to-cid ~bank/payment-form)        ;; => bafyrei..abc\n"
           "\n"
           ";; Deep CID — component + all transitive dependencies\n"
           "(freeze-to-cid-deep ~bank/payment-form)   ;; => bafyrei..xyz\n"
           "\n"
           ";; The deep CID changes if ANY dependency changes.\n"
           ";; A one-character change in ~ui/text-field\n"
           ";; produces a completely different deep CID."))

    (h3 (~tw :tokens "text-lg font-semibold mt-8 mb-3") "3.7b Canonical serialization")

    (p "For CIDs to match across hosts, the serialized form must be identical. "
       "Canonical SX: no comments, no redundant whitespace, deterministic key ordering in dicts, "
       "normalized number representation:")

    (~docs/code :src
      (str ";; These must produce the same CID on JS, Python, and OCaml:\n"
           "(canonical-sx '(div :class \"card\" (p \"hello\")))\n"
           ";; => \"(div :class \\\"card\\\" (p \\\"hello\\\"))\"\n"
           "\n"
           ";; Dict key ordering is sorted:\n"
           "(canonical-sx '{:b 2 :a 1})  ;; => \"{:a 1 :b 2}\""))

    (h3 (~tw :tokens "text-lg font-semibold mt-8 mb-3") "3.7c Browser verification")

    (p "The client-side verification flow:")

    (~docs/code :src
      (str ";; Server sends component + CID via aser wire format\n"
           ";; Browser receives, independently computes CID, compares\n"
           "\n"
           ";; Per-component verification\n"
           "(component-verify ~bank/payment-form\n"
           "  :expected-cid \"bafyrei...\"\n"
           "  :on-mismatch :refuse)    ;; or :warn, :log\n"
           "\n"
           ";; Verify entire page component tree against published manifest\n"
           "(page-verify\n"
           "  :manifest-url \"/.well-known/sx-manifest.json\"\n"
           "  :on-mismatch :refuse)\n"
           "\n"
           ";; Query verification status (for UI indicators)\n"
           "(verified? ~bank/payment-form)  ;; => true/false"))

    (p "Visual indicator — like the HTTPS lock icon, but for individual UI components. "
       "The browser knows which components have verified CIDs and can surface this to the user.")

    (h3 (~tw :tokens "text-lg font-semibold mt-8 mb-3") "3.7d Manifest and discovery")

    (p "Publishers declare expected CIDs via a well-known manifest:")

    (~docs/code :src
      (str ";; .well-known/sx-manifest.json\n"
           "{\"version\": 1,\n"
           " \"components\": {\n"
           "   \"~bank/payment-form\": {\n"
           "     \"cid\": \"bafyrei...abc\",\n"
           "     \"cid-deep\": \"bafyrei...xyz\",\n"
           "     \"audited\": \"2026-03-01\",\n"
           "     \"auditor\": \"security-firm.com\"\n"
           "   },\n"
           "   \"~bank/login\": {\n"
           "     \"cid\": \"bafyrei...def\",\n"
           "     \"cid-deep\": \"bafyrei...uvw\",\n"
           "     \"audited\": \"2026-02-15\"\n"
           "   }\n"
           " },\n"
           " \"signature\": \"...\"\n"
           "}"))

    (p "Alternative discovery mechanisms:")

    (ul (~tw :tokens "list-disc pl-6 mb-4 space-y-1")
      (li (strong "DNS TXT") " — " (code "_sx-verify.bank.com TXT \"payment-form=bafyrei...\""))
      (li (strong "Certificate transparency") " — append-only log of component CIDs, publicly auditable")
      (li (strong "IPFS") " — the CID is the address; fetching from IPFS is self-verifying")
      (li (strong "Signed manifest") " — publisher signs the manifest with their TLS key; browser verifies signature"))

    (h3 (~tw :tokens "text-lg font-semibold mt-8 mb-3") "How this differs from SRI")

    (p "Subresource Integrity (SRI) already does hash verification for " (code "<script>") " tags. "
       "But SRI has three gaps that verified components close:")

    (div (~tw :tokens "overflow-x-auto mb-6")
      (table (~tw :tokens "min-w-full text-sm")
        (thead (tr
          (th (~tw :tokens "text-left pr-4 pb-2 font-semibold") "")
          (th (~tw :tokens "text-left pr-4 pb-2 font-semibold") "SRI")
          (th (~tw :tokens "text-left pb-2 font-semibold") "SX Verified Components")))
        (tbody
          (tr (td (~tw :tokens "pr-4 py-1 font-semibold") "Granularity")
              (td (~tw :tokens "pr-4") "Whole files (a JS bundle)")
              (td "Individual components"))
          (tr (td (~tw :tokens "pr-4 py-1 font-semibold") "Who sets the hash?")
              (td (~tw :tokens "pr-4") "The server — if compromised, serves matching hashes")
              (td "Independent manifest — client verifies against external source"))
          (tr (td (~tw :tokens "pr-4 py-1 font-semibold") "What's verified?")
              (td (~tw :tokens "pr-4") "The file bytes — says nothing about runtime behaviour")
              (td "The definition — and since components are pure functions, definition = behaviour")))))

    ;; -----------------------------------------------------------------------
    ;; Step 4: Concurrent CEK — deep spec
    ;; -----------------------------------------------------------------------

    (h2 (~tw :tokens "text-xl font-bold mt-12 mb-4") "Step 4: Concurrent CEK")

    (p "Multiple CEK machines running concurrently. The machines are independent \u2014 "
       "each has its own C, E, K registers. Communication is via typed channels. "
       "The host provides the concurrency mechanism (Web Workers, forkIO, tokio::spawn). "
       "The spec defines the coordination primitives.")

    (h3 (~tw :tokens "text-lg font-semibold mt-8 mb-3") "4.1 Spawn")

    (p "The fundamental primitive. Create a new CEK machine from a thunk, "
       "run it concurrently, return a signal that resolves with the result:")

    (~docs/code :src
      (str "(let ((result (spawn (fn () (* 6 7)))))
"
           "  ;; result is a signal \u2014 nil until the computation completes
"
           "  (effect (fn ()
"
           "    (when (deref result)
"
           "      (log (str \"answer: \" (deref result))))))
"
           "  ;; => \"answer: 42\" (eventually)"))

    (p "Implementation: the host freezes the thunk\u2019s CEK state, ships it to a worker, "
       "the worker thaws and runs, posts back the result, the signal resolves. "
       "The reactive system propagates the change \u2014 any island deref\u2019ing the signal re-renders.")

    (p "The default implementation is synchronous (no actual concurrency). "
       "The host overrides " (code "spawn-impl") " for real concurrency:")

    (~docs/code :src
      (str ";; Host-provided spawn (Web Worker)
"
           "(set! spawn-impl
"
           "  (fn (thunk result-sig)
"
           "    (let ((frozen (freeze-to-sx \"spawn\")))
"
           "      (worker-post frozen)
"
           "      (worker-on-message
"
           "        (fn (val) (reset! result-sig val))))))"))

    (h3 (~tw :tokens "text-lg font-semibold mt-8 mb-3") "4.2 Channels")

    (p "Typed communication pipes between concurrent computations. "
       "Send is non-blocking. Receive suspends via " (code "shift") " until data arrives:")

    (~docs/code :src
      (str ";; Create a channel
"
           "(make-channel \"results\")
"
           "
"
           ";; Producer (in spawned computation)
"
           "(spawn (fn ()
"
           "  (channel-send \"results\" (expensive-computation))))
"
           "
"
           ";; Consumer (in main thread)
"
           "(let ((val (channel-receive \"results\")))
"
           "  ;; val is a signal if no data yet, or the value if buffered
"
           "  (when (signal? val)
"
           "    ;; Reactive: re-renders when data arrives
"
           "    (div \"Waiting...\" (deref val))))"))

    (p "Channels are named and registered globally. Multiple producers and consumers "
       "can share a channel. The buffer stores values until a consumer reads them. "
       "When a consumer arrives and the buffer is empty, a signal is returned "
       "that resolves when a producer sends.")

    (p "Channel semantics:")

    (ul (~tw :tokens "list-disc pl-6 mb-4 space-y-1")
      (li (strong "Unbuffered") " \u2014 send blocks until a receiver is ready (rendezvous)")
      (li (strong "Buffered") " \u2014 send succeeds immediately, values queue (current default)")
      (li (strong "Broadcast") " \u2014 every receiver gets every value (pub/sub)")
      (li (strong "Select") " \u2014 wait on multiple channels, take the first that has data"))

    (h3 (~tw :tokens "text-lg font-semibold mt-8 mb-3") "4.3 Fork / Join")

    (p "Spawn multiple computations, collect all results. "
       "The spec primitive, not a library pattern:")

    (~docs/code :src
      (str ";; Fork: run N computations concurrently
"
           "(let ((results (fork-join (list
"
           "  (fn () (fetch-user 1))
"
           "  (fn () (fetch-user 2))
"
           "  (fn () (fetch-user 3))))))
"
           "  ;; results is a list of signals
"
           "  ;; All resolve when all computations complete
"
           "  (div
"
           "    (map (fn (r) (div (deref r))) results)))"))

    (p "Fork/join composes with the reactive system. Each result signal drives "
       "a reactive DOM node. Results appear as they complete, not all-or-nothing.")

    (h3 (~tw :tokens "text-lg font-semibold mt-8 mb-3") "4.4 Scheduler")

    (p "The scheduler decides which CEK machine steps next. "
       "Different strategies for different use cases:")

    (ul (~tw :tokens "list-disc pl-6 mb-4 space-y-1")
      (li (strong "Round-robin") " \u2014 fair, each machine gets equal time")
      (li (strong "Priority") " \u2014 UI-facing computations step first")
      (li (strong "Work-stealing") " \u2014 idle workers steal from busy ones")
      (li (strong "Cooperative") " \u2014 machines yield explicitly via " (code "yield!"))
      (li (strong "DAG-ordered") " \u2014 step machines whose inputs are ready (Art DAG)"))

    (~docs/code :src
      (str ";; Cooperative scheduling
"
           "(spawn (fn ()
"
           "  (for-each (fn (item)
"
           "    (process item)
"
           "    (yield!)  ;; let other machines run
"
           "    ) items)))
"
           "
"
           ";; DAG scheduling
"
           "(dag-execute
"
           "  {:nodes {:a (fn () (load-image \"input.jpg\"))
"
           "           :b (fn (a) (resize a 512 512))
"
           "           :c (fn (a) (blur a 3))
"
           "           :d (fn (b c) (composite b c))}
"
           "   :edges {[:a] [:b :c]
"
           "           [:b :c] [:d]}})"))

    (h3 (~tw :tokens "text-lg font-semibold mt-8 mb-3") "4.5 Content-addressed concurrency")

    (p "Concurrent computation + content addressing = verifiable parallel execution:")

    (ul (~tw :tokens "list-disc pl-6 mb-4 space-y-1")
      (li "Each spawned computation\u2019s initial state has a CID")
      (li "Each result has a CID")
      (li "The mapping input-CID \u2192 output-CID is a proof of computation")
      (li "Memoize: if input-CID was computed before, return cached output-CID")
      (li "Distribute: send input-CID to whichever worker has the data")
      (li "Verify: any machine can re-run from input-CID and check output-CID matches"))

    (~docs/code :src
      (str ";; Content-addressed spawn
"
           "(let ((input-cid (freeze-to-cid \"job\")))
"
           "  ;; Check cache first
"
           "  (or (result-cache-get input-cid)
"
           "      ;; Not cached \u2014 compute and cache
"
           "      (let ((result (spawn (fn () (expensive-work)))))
"
           "        (effect (fn ()
"
           "          (when (deref result)
"
           "            (result-cache-put input-cid
"
           "              (freeze-to-cid \"result\")))))
"
           "        result)))"))

    (h3 (~tw :tokens "text-lg font-semibold mt-8 mb-3") "4.6 Host mapping")

    (p "Each host implements concurrency differently. The spec is the same:")

    (div (~tw :tokens "overflow-x-auto mb-6")
      (table (~tw :tokens "min-w-full text-sm")
        (thead (tr
          (th (~tw :tokens "text-left pr-4 pb-2 font-semibold") "Primitive")
          (th (~tw :tokens "text-left pr-4 pb-2 font-semibold") "JavaScript")
          (th (~tw :tokens "text-left pr-4 pb-2 font-semibold") "Python")
          (th (~tw :tokens "text-left pr-4 pb-2 font-semibold") "OCaml")
          (th (~tw :tokens "text-left pb-2 font-semibold") "Rust/WASM")))
        (tbody
          (tr (td (~tw :tokens "pr-4 py-1 font-mono") "spawn")
              (td (~tw :tokens "pr-4") "Web Worker")
              (td (~tw :tokens "pr-4") "asyncio.create_task")
              (td (~tw :tokens "pr-4") "Eio.Fiber.fork")
              (td "tokio::spawn"))
          (tr (td (~tw :tokens "pr-4 py-1 font-mono") "channel")
              (td (~tw :tokens "pr-4") "MessageChannel")
              (td (~tw :tokens "pr-4") "asyncio.Queue")
              (td (~tw :tokens "pr-4") "Eio.Stream.t")
              (td "mpsc::channel"))
          (tr (td (~tw :tokens "pr-4 py-1 font-mono") "yield!")
              (td (~tw :tokens "pr-4") "setTimeout(0)")
              (td (~tw :tokens "pr-4") "await asyncio.sleep(0)")
              (td (~tw :tokens "pr-4") "Eio.Fiber.yield")
              (td "tokio::task::yield_now"))
          (tr (td (~tw :tokens "pr-4 py-1 font-mono") "freeze/thaw")
              (td (~tw :tokens "pr-4") "postMessage + JSON")
              (td (~tw :tokens "pr-4") "pickle / SX text")
              (td (~tw :tokens "pr-4") "Marshal + SX text")
              (td "serde + SX text"))
          (tr (td (~tw :tokens "pr-4 py-1 font-mono") "select")
              (td (~tw :tokens "pr-4") "Promise.race")
              (td (~tw :tokens "pr-4") "asyncio.wait FIRST_COMPLETED")
              (td (~tw :tokens "pr-4") "Eio.Fiber.any")
              (td "tokio::select!")))))

    (h3 (~tw :tokens "text-lg font-semibold mt-8 mb-3") "4.7 Roadmap")

    (div (~tw :tokens "overflow-x-auto mb-6")
      (table (~tw :tokens "min-w-full text-sm")
        (thead (tr
          (th (~tw :tokens "text-left pr-4 pb-2 font-semibold") "Phase")
          (th (~tw :tokens "text-left pr-4 pb-2 font-semibold") "What")
          (th (~tw :tokens "text-left pr-4 pb-2 font-semibold") "Host")
          (th (~tw :tokens "text-left pb-2 font-semibold") "Validates")))
        (tbody
          (tr (td (~tw :tokens "pr-4 py-1") "4a")
              (td (~tw :tokens "pr-4") "spawn + Web Worker")
              (td (~tw :tokens "pr-4") "JavaScript")
              (td "Freeze/thaw across execution contexts"))
          (tr (td (~tw :tokens "pr-4 py-1") "4b")
              (td (~tw :tokens "pr-4") "Channels (buffered)")
              (td (~tw :tokens "pr-4") "JavaScript")
              (td "Cross-worker communication"))
          (tr (td (~tw :tokens "pr-4 py-1") "4c")
              (td (~tw :tokens "pr-4") "Fork/join + DAG scheduler")
              (td (~tw :tokens "pr-4") "JavaScript")
              (td "Art DAG integration path"))
          (tr (td (~tw :tokens "pr-4 py-1") "4d")
              (td (~tw :tokens "pr-4") "OCaml bootstrapper → native compilation")
              (td (~tw :tokens "pr-4") "OCaml")
              (td "Native performance, direct CEK-to-ML mapping"))
          (tr (td (~tw :tokens "pr-4 py-1") "4e")
              (td (~tw :tokens "pr-4") "Rust/WASM bootstrapper")
              (td (~tw :tokens "pr-4") "Rust")
              (td "Browser performance, WASM target"))
          (tr (td (~tw :tokens "pr-4 py-1") "4f")
              (td (~tw :tokens "pr-4") "Content-addressed spawn")
              (td (~tw :tokens "pr-4") "Any")
              (td "Memoization, distribution, verification"))
          (tr (td (~tw :tokens "pr-4 py-1") "4g")
              (td (~tw :tokens "pr-4") "IPFS-backed content store")
              (td (~tw :tokens "pr-4") "Any")
              (td "Global content addressing, peer-to-peer"))
          (tr (td (~tw :tokens "pr-4 py-1") "4h")
              (td (~tw :tokens "pr-4") "Select + broadcast channels")
              (td (~tw :tokens "pr-4") "Any")
              (td "Complex coordination patterns"))
          (tr (td (~tw :tokens "pr-4 py-1") "4i")
              (td (~tw :tokens "pr-4") "Linear channels")
              (td (~tw :tokens "pr-4") "Any")
              (td "Resource safety, exactly-once delivery")))))

    (p "Each phase is independently valuable. Phase 4a (Web Worker spawn) is the immediate next build. "
       "Phase 4d (OCaml) proves the spec compiles to native code — the CEK machine maps directly to ML's runtime model. "
       "Phase 4e (Rust/WASM) proves it can run in the browser at near-native speed. "
       "Phase 4g (IPFS) makes it distributed.")

    ;; -----------------------------------------------------------------------
    ;; Step 5: Linear effects (future)
    ;; -----------------------------------------------------------------------

    (h2 (~tw :tokens "text-xl font-bold mt-12 mb-4") "Step 5: Linear Effects")

    (p "Constrain the continuation: a handler " (em "must") " resume exactly once. "
       "No dropping (resource leak), no duplicating (nondeterminism). "
       "This is the linearity axis from the three-axis model.")

    (ul (~tw :tokens "list-disc pl-6 mb-4 space-y-1")
      (li (strong "Affine channels") " \u2014 send at most once. Prevents duplicate messages.")
      (li (strong "Linear scopes") " \u2014 a freeze scope that must be thawed. Prevents orphaned state.")
      (li (strong "Session types") " \u2014 a protocol that must complete. Prevents half-open connections.")
      (li (strong "Resource handles") " \u2014 a file/DB handle that must be closed. Prevents leaks."))

    (p "Linear effects connect SX to Rust\u2019s ownership model. "
       "Affine types (use at most once) are the practical sweet spot. "
       "Full linearity (use exactly once) is for protocols and resources.")

    (p "This is the furthest horizon. The infrastructure \u2014 freeze scopes, channels, "
       "content addressing \u2014 must be solid first. Linearity is a discipline on top, "
       "not a prerequisite beneath.")

        (p (~tw :tokens "text-stone-500 text-sm italic mt-12")
       "The floor is thought itself. We can't go deeper, because there's no one left to dig.")))
