Add Freeze/Thaw page under CEK Machine with live demo

Documents and demonstrates serializable CEK state. Type an expression,
step to any point, click Freeze to see the frozen SX. Click Thaw to
resume from the frozen state and get the result.

- New page at /sx/(geography.(cek.freeze))
- Nav entry under CEK Machine
- Interactive island demo with step/run/freeze/thaw buttons
- Documentation: the idea, freeze format, thaw/resume, what it enables

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

sx/sx/geography/cek.sx

@@ -473,6 +473,150 @@
 
 
 
+
+;; ---------------------------------------------------------------------------
+;; CEK Freeze / Thaw — serializable computation
+;; ---------------------------------------------------------------------------
+
+(defcomp ~geography/cek/cek-freeze-content ()
+  (~docs/page :title "Freeze / Thaw"
+
+    (p :class "text-stone-500 text-sm italic mb-8"
+      "A computation is a value. Freeze it to an s-expression. "
+      "Store it, transmit it, content-address it. Thaw and resume anywhere.")
+
+    (~docs/section :title "The idea" :id "idea"
+      (p "The CEK machine makes evaluation explicit: every step is a pure function from state to state. "
+         "The state is a dict with four fields:")
+      (ul :class "list-disc pl-6 mb-4 space-y-1 text-stone-600"
+        (li (code "control") " \u2014 the expression being evaluated")
+        (li (code "env") " \u2014 the bindings in scope")
+        (li (code "kont") " \u2014 the continuation (what to do with the result)")
+        (li (code "phase") " \u2014 eval or continue"))
+      (p "Since the state is data, it can be serialized. "
+         (code "cek-freeze") " converts a live CEK state to pure s-expressions. "
+         (code "cek-thaw") " reconstructs a live state from frozen SX. "
+         (code "cek-run") " resumes from where it left off."))
+
+    (~docs/section :title "Freeze" :id "freeze"
+      (p "Take a computation mid-flight and freeze it:")
+      (~docs/code :code (highlight
+        "(let ((expr (sx-parse \"(+ 1 (* 2 3))\"))\n      (state (make-cek-state (first expr) (make-env) (list))))\n  ;; Step 4 times\n  (set! state (cek-step (cek-step (cek-step (cek-step state)))))\n  ;; Freeze to SX\n  (cek-freeze state))"
+        "lisp"))
+      (p "The frozen state is pure SX:")
+      (~docs/code :code (highlight
+        "{:phase \"continue\"\n :control nil\n :value 1\n :env {}\n :kont ({:type \"arg\"\n         :f (primitive \"+\")\n         :evaled ()\n         :remaining ((* 2 3))\n         :env {}})}"
+        "lisp"))
+      (p "Everything is data. The continuation frame says: \u201cI was adding 1 to something, "
+         "and I still need to evaluate " (code "(* 2 3)") ".\u201d"))
+
+    (~docs/section :title "Thaw and resume" :id "thaw"
+      (p "Parse the frozen SX back. Thaw it. Resume:")
+      (~docs/code :code (highlight
+        "(let ((frozen (sx-parse frozen-text))\n      (state (cek-thaw (first frozen))))\n  (cek-run state))\n;; => 7"
+        "lisp"))
+      (p "Native functions like " (code "+") " serialize as " (code "(primitive \"+\")") 
+         " and are looked up in the primitive registry on thaw. "
+         "Lambdas serialize as their source AST \u2014 " (code "(lambda (x) (* x 2))") 
+         " \u2014 and reconstruct as callable functions."))
+
+    (~docs/section :title "Live demo" :id "demo"
+      (p "Type an expression, step to any point, freeze the state. "
+         "The frozen SX appears below. Click Thaw to resume from the frozen state.")
+      (~geography/cek/freeze-demo))
+
+    (~docs/section :title "What this enables" :id "enables"
+      (ul :class "list-disc pl-6 mb-4 space-y-2 text-stone-600"
+        (li (strong "Persistence") " \u2014 save reactive island state to localStorage, "
+            "resume on page reload")
+        (li (strong "Migration") " \u2014 freeze a computation on one machine, "
+            "thaw on another. Same result, deterministically.")
+        (li (strong "Content addressing") " \u2014 hash the frozen SX \u2192 CID. "
+            "A pointer to a computation in progress, not just a value.")
+        (li (strong "Time travel") " \u2014 freeze at each step, store the history. "
+            "Jump to any point. Undo. Branch.")
+        (li (strong "Verification") " \u2014 re-run from a frozen state, "
+            "check the result matches. Reproducible computation."))
+      (p "The Platonic argument made concrete: a computation IS a value. "
+         "The Form persists. The instance resumes."))))
+
+
+(defisland ~geography/cek/freeze-demo ()
+  (let ((source (signal "(+ 1 (* 2 3))"))
+        (state-sig (signal nil))
+        (step-count (signal 0))
+        (frozen-sx (signal ""))
+        (thaw-result (signal "")))
+    (letrec
+      ((do-parse (fn ()
+         (reset! frozen-sx "")
+         (reset! thaw-result "")
+         (reset! step-count 0)
+         (let ((parsed (sx-parse (deref source))))
+           (when (not (empty? parsed))
+             (reset! state-sig (make-cek-state (first parsed) (make-env) (list)))))))
+       (do-step (fn ()
+         (when (and (deref state-sig) (not (cek-terminal? (deref state-sig))))
+           (reset! state-sig (cek-step (deref state-sig)))
+           (swap! step-count inc))))
+       (do-freeze (fn ()
+         (when (deref state-sig)
+           (let ((frozen (cek-freeze (deref state-sig))))
+             (reset! frozen-sx (sx-serialize frozen))))))
+       (do-thaw (fn ()
+         (when (not (empty? (deref frozen-sx)))
+           (let ((parsed (sx-parse (deref frozen-sx))))
+             (when (not (empty? parsed))
+               (let ((thawed (cek-thaw (first parsed))))
+                 (reset! thaw-result
+                   (str "Resumed from step " (deref step-count) ": "
+                        (cek-run thawed)))))))))
+       (do-run (fn ()
+         (when (deref state-sig)
+           (let run-loop ()
+             (when (not (cek-terminal? (deref state-sig)))
+               (do-step)
+               (run-loop)))))))
+      ;; Auto-parse
+      (effect (fn () (do-parse)))
+      (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) (do-parse))))
+          (div :class "flex gap-1"
+            (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")))
+        ;; Step count + freeze button
+        (div :class "flex items-center gap-3"
+          (span :class "text-sm text-stone-500 font-mono"
+            "Step " (deref step-count))
+          (when (deref state-sig)
+            (button :on-click (fn (e) (do-freeze))
+              :class "px-3 py-1.5 rounded bg-amber-500 text-white text-sm hover:bg-amber-600"
+              "Freeze")))
+        ;; Frozen SX output
+        (when (not (empty? (deref frozen-sx)))
+          (div :class "space-y-2"
+            (label :class "text-xs text-stone-400 block" "Frozen CEK state")
+            (pre :class "text-xs font-mono bg-stone-50 rounded p-3 overflow-x-auto whitespace-pre-wrap text-stone-700"
+              (deref frozen-sx))
+            (button :on-click (fn (e) (do-thaw))
+              :class "px-3 py-1.5 rounded bg-emerald-600 text-white text-sm hover:bg-emerald-700"
+              "Thaw \u2192 Resume")))
+        ;; Thaw result
+        (when (not (empty? (deref thaw-result)))
+          (div :class "rounded bg-emerald-50 border border-emerald-200 p-3 text-emerald-800 font-mono text-sm"
+            (deref thaw-result)))))))
+
+
 ;; ---------------------------------------------------------------------------
 ;; Demo page content
 ;; ---------------------------------------------------------------------------

sx/sx/nav-data.sx

@@ -174,7 +174,9 @@
   (dict :label "Overview" :href "/sx/(geography.(cek))"
         :summary "The CEK machine — explicit evaluator with Control, Environment, Kontinuation. Three registers, pure step function.")
   (dict :label "Demo" :href "/sx/(geography.(cek.demo))"
-        :summary "Live islands evaluated by the CEK machine. Counter, computed chains, reactive attributes — all through explicit continuation frames.")))
+        :summary "Live islands evaluated by the CEK machine. Counter, computed chains, reactive attributes — all through explicit continuation frames.")
+  (dict :label "Freeze / Thaw" :href "/sx/(geography.(cek.freeze))"
+        :summary "Serialize a CEK state to s-expressions. Ship it, store it, content-address it. Thaw and resume anywhere.")))
 
 (define plans-nav-items (list
   (dict :label "Status" :href "/sx/(etc.(plan.status))"

sx/sx/page-functions.sx

@@ -66,6 +66,7 @@
       '(~geography/cek/cek-content)
       (case slug
         "demo" '(~geography/cek/cek-demo-content)
+        "freeze" '(~geography/cek/cek-freeze-content)
         :else '(~geography/cek/cek-content)))))
 
 (define provide