Decouple core evaluator from web platform, extract libraries
The core evaluator (spec/evaluator.sx) is now the irreducible computational core with zero web, rendering, or type-system knowledge. 2531 → 2313 lines. - Add extensible special form registry (*custom-special-forms* + register-special-form!) - Add render dispatch hooks (*render-check* / *render-fn*) replacing hardcoded render-active?/is-render-expr?/render-expr - Extract freeze scopes → spec/freeze.sx (library, not core) - Extract content addressing → spec/content.sx (library, not core) - Move sf-deftype/sf-defeffect → spec/types.sx (self-registering) - Move sf-defstyle → web/forms.sx (self-registering with all web forms) - Move web tests (defpage, streaming) → web/tests/test-forms.sx - Add is-else-clause? helper (replaces 5 inline patterns) - Make escape-html/escape-attr library functions in render.sx (pure SX, not platform-provided) - Add foundations plan: Step 3.5 (data representations), Step 3.7 (verified components), OCaml for Step 4d - Update all three bootstrappers (JS 957/957, Python 744/744, OCaml 952/952) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This commit is contained in:
@@ -234,6 +234,9 @@
|
||||
(tr (td :class "pr-4 py-1" "3.5")
|
||||
(td :class "pr-4" "Data representations")
|
||||
(td :class "text-stone-400" "Planned — byte buffers + typed structs"))
|
||||
(tr (td :class "pr-4 py-1" "3.7")
|
||||
(td :class "pr-4" "Verified components")
|
||||
(td :class "text-stone-400" "Planned — content-addressed UI trust"))
|
||||
(tr (td :class "pr-4 py-1" "4")
|
||||
(td :class "pr-4" "Concurrent CEK")
|
||||
(td :class "text-amber-600 font-semibold" "Spec complete — implementation next"))
|
||||
@@ -358,6 +361,143 @@
|
||||
"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 :class "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 :class "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 :class "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 :class "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 :code
|
||||
(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 :class "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 :code
|
||||
(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 :class "text-lg font-semibold mt-8 mb-3" "3.7c Browser verification")
|
||||
|
||||
(p "The client-side verification flow:")
|
||||
|
||||
(~docs/code :code
|
||||
(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 :class "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 :code
|
||||
(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 :class "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 :class "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 :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" "")
|
||||
(th :class "text-left pr-4 pb-2 font-semibold" "SRI")
|
||||
(th :class "text-left pb-2 font-semibold" "SX Verified Components")))
|
||||
(tbody
|
||||
(tr (td :class "pr-4 py-1 font-semibold" "Granularity")
|
||||
(td :class "pr-4" "Whole files (a JS bundle)")
|
||||
(td "Individual components"))
|
||||
(tr (td :class "pr-4 py-1 font-semibold" "Who sets the hash?")
|
||||
(td :class "pr-4" "The server — if compromised, serves matching hashes")
|
||||
(td "Independent manifest — client verifies against external source"))
|
||||
(tr (td :class "pr-4 py-1 font-semibold" "What's verified?")
|
||||
(td :class "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
|
||||
;; -----------------------------------------------------------------------
|
||||
|
||||
Reference in New Issue
Block a user