blog(draft): the architecture no single repo owns — cross-repo checks - #122
Merged
Conversation
New draft grounded in a parallel cross-repo ingestion audit. Thesis: the toolchain became a graph this month (loom→synth proof-carrying wsc.facts; ordeal as the shared default solver, Z3 demoted; agora coordination mirrored into rivet; gust composing 5 repos bit-identical on 3 chips; kiln-builtins now real) — those edges span repos, so no single repo's CI owns them, and that's where drift hides (ordeal#53 README vs shipped proof, scry#97 README undersells code, sigil#186 missing attribution). draft=true, held. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
… kiln no_std-interpreter direction - sigil: the attestation sink meant to ingest from loom/synth/witness/scry and feed rivet, but most edges are designed-not-wired and #164 (can't sign wasip2) blocks the org-wide rollout + keeps agora's sigs stubbed — a perfect cross-repo-architecture point. - kiln: this week's direction to give the interpreter a no_std on-board mode (a 2nd runtime path beside synth AOT; keeps a compiler out of the embedded cert TCB) — the graph is still growing edges. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
- Grounding: one-line 'what PulseEngine is' up top; noun-glosses for synth/loom. - Diagram honesty (the drift the post warns about): kiln→gale was factually wrong today (interpret-on-target is roadmap) → dashed 'on-target planned'; sigil edges marked 'designed' (not wired); loom→ordeal 'slated'; colour legend added. - Composition made legible AS components: new CM section + diagram showing app imports gale:kernel, gale-kiln exports it, drivers import gust:hal/mmio → meld resolves imports↔exports + flattens to one core module → loom/synth → native. (Real interface names verified against the gale repo.) - Foreshadow the drift examples so they read as evidence, not housekeeping. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…deal machinery
You were right: the overview echoed how-it-works. Now it goes under the hood of two
edges, with real detail (verified against the repos):
- Edge one — the OS composed: the full gust component table (gale-app-demo, gale-kiln
provides gale:kernel, 7 thin-seam drivers importing only gust:hal/mmio, each Kani-
proven with harness counts), the ~77-line / 5-atom TCB ('0 new atoms per driver'),
the exact meld→loom→synth fusion command-chain with sizes (fused.o 668 B → 3.5 KB
image, fits F100 8 KB), run-demo()=53 as a differential equivalence check (honest:
tested not proven), and the silicon ratios.
- Edge two — proofs that flow: loom translation-validates each pass and emits wsc.facts
(value-range/divisor-nonzero/shift-bound); synth ingests them to elide guards LLVM
must keep (0.45× floor, flag-gated) and selects via 40 Rocq-verified rules; synth-
verify checks WASM≡ARM per-rule via ordeal; ordeal emits an LRAT certificate a Lean-
verified checker validates (accept ⇒ UNSAT); Z3 kept as differential oracle (141/141).
Honest edges named (Charon/Aeneas trusted; 64-bit mul/div Kani at width 8).
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…acked component model - Fix: the 'follow one function' Mermaid crashed (mermaid 11.16) on unquoted <, [], ≠ in edge labels — all special-char labels now quoted. - Add: a stacked component-model diagram (verified-wasm layers above the trust line; the thin gust:hal/mmio seam; the ~77-line native TCB; silicon below). - Reframe as an architecture document: replaced the drift-issues section (ordeal#53/ scry#97/sigil#186) and the fleet-review narrative with a clean 'Status quo, and where it's heading' (live / deepening / next / being-wired), describing the architecture and its direction rather than the issue findings. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…nned bits) Per feedback (overloaded). Now a single concrete piece: how gust composes from ~10 verified WebAssembly components into a ~3.5 KB native image on 3 real chips, over a ~77-line trusted base. One diagram (the stack), the component table, the fusion chain, run-demo()=53 differential check, silicon ratios. Dropped: the loom/synth/ordeal pipeline, the 'no single repo owns' meta-thesis, and the planned/aspirational (kiln interpreter, sigil, agora). Renamed slug → verified-os-on-silicon. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…kiln/sigil issues) Read the gale gust_os_roadmap.yaml + REQ-OS-* artifacts and the gale/kiln/sigil issues to ground the PLANNED architecture, not just today's snapshot. Added 'The architecture, and where it's headed': the North Star (general multi-tenant verified OS, MPU-isolated over one thin TCB), the honest release ladder v0.1→v1.0 (driver breadth → the gust:os capability seam with an io_uring-shaped submit/complete queue composed from gale::msgq + kiln + the driver seam + dma-own's own<buffer> → MPU multi-tenancy, blocked on synth multi-memory → v1.0 cut), the 0-new-trusted-atoms invariant (nm atom-count kill-check), and the scry→sigil→kiln reject-at-load trust chain for on-target loading. Kept focused on the OS; still honest (v0.3–v1.0 not built; dissolve tested not proven). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
- New diagram: the v1.0 target stack with shipped-vs-planned marked (green = running today at v0.2: composition, uart+dma, semaphore, on silicon; dashed = planned: the gust:os syscall seam v0.4, mutually-distrusting tenants under MPU v0.5). Shows the 1.0 architecture and how far it is at a glance. - Tightened throughout (drivers, compose tail, run-demo notes, the close). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The 'fuse→optimize→compile' code block read awkwardly. Now a boxed flowchart: the two typed components (gale-app-demo, gale-kiln) fuse via meld into one core module, then loom (240 B) → synth (668 B .text) → link+TCB (~3.5 KB, fits F100 8 KB). Sizes on each box; native artifacts marked distinct from the wasm ones. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…-options diagram - Stack (layers) diagram split more: the lumped 'OS' → kiln scheduler + gale primitives (sem/msgq/mutex/event); drivers → serial buses (uart/spi/i2c) + digital&timing (gpio/timer/dma/adc). Five verified-wasm layers instead of three. - Added 'Two ways to run it, both signed': the compile-to-native (synth, today) vs on-target interpreter (kiln no_std, planned) options, with sigil signing + scry-bounds reject-at-load, as a diagram. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…dictions - credit flattening to loom/synth (meld yields a composed component), and justify the 1.8KB→240B drop (canonical-ABI adapters strip once seam is internal) - fix gale:kernel bare-package identifier → gale:kernel/* interfaces throughout (incl. gale::msgq Rust-syntax → gale:kernel/msgq WIT-syntax) - resolve the 5-atoms vs 'fourth atom' contradiction (→ 'a new atom') - align reject-at-load prose to future tense (diagram already marks it planned) - group kiln+primitives as one gale-kiln component in the stack (keeps the layer split but fixes the one-vs-two-component ambiguity) - glosses: HAL, MPU, own<buffer>, Kani; qualify 'shared memory' as single-memory - compress 'What it buys' (third thesis restatement) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The idealized stack (D1) portrayed the full app+scheduler+primitives+drivers composition as shipped, but only the semaphore demo composes and runs today. The v1.0 diagram already carries the trusted-base shape with honest shipped(green)/planned(dashed) coloring, so nothing is lost. Reworked the section intro so it no longer references 'the line'. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…acts Read the actual gale/kiln/sigil issues, rivet artifacts, and gale src/mpu.rs. Corrections: - TCB is a 4-atom base (mmio r/w, irq, dma), not 5; breadth node is 3-atom (source: gale gust_os_roadmap.yaml 4-item TCB shim) - New "Isolation, honestly" scene: real Verus-verified validate_region from gale src/mpu.rs, with the honest line that it is a proven region *model*, not hardware programming/fault-trapping (that is v0.5, blocked on synth#404) - Fix the interpreter motivation: NOT "keep compiler out of cert base" (gust rejects that framing — dissolve keeps both compiler AND interpreter off the device); the real driver is migratable/dynamically-loaded tenants - Ground reject-at-load in the real mechanism: scry bounds host-side -> kiln.resource_limits section -> sigil signs whole module -> kiln no_std loader verifies as one admission step (kiln#415, kiln#421, sigil#187) - v0.3 drivers are proven (Kani 4/4,3/3,6/6; 4 fused to ~2.4KB @ 3 atoms), not merely "next"; name the real rivet release-status query Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…omponent kiln the interpreter is a no_std wasm component that synth dissolves to native via the same one pipeline as everything else (kiln#415 / PR #416: wasm is the universal IR, synth the single build-time compiler in the TCB). The on-device kiln then loads and interprets the migratable tenant components at runtime. Not two parallel routes to silicon — one compiler pipeline; the difference is only dissolve-ahead-of-time vs load-and-interpret-on-device. Reworked prose + diagram accordingly. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Not ready to ship; keep it held (draft + explicit ready=false) while the architecture content is still being reviewed. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
A 4th blog draft (standalone, after the Sat/Sun/Mon drip), grounded in a parallel cross-repo ingestion audit of the actual repos.
Thesis
The toolchain became a graph this month — those new edges span repositories, so no single repo's CI owns them:
wsc.factsinvariants ingested as codegen premises).coordination-factartifacts.That graph creates a drift class per-repo CI structurally can't catch — and this week's sweep found it: ordeal#53 (README vs shipped proof), scry#97 (README undersells working code), sigil#186 (missing MIT attribution). Cross-repo architecture checks by an agent fleet are the answer.
Grounded, honest (agora spike, loom not yet migrated to ordeal, some invariant edges design-phase).
draft = true, held for review. ~1,200 words.🤖 Generated with Claude Code