diff --git a/.gitignore b/.gitignore
index 7844feb..baa823a 100644
--- a/.gitignore
+++ b/.gitignore
@@ -6,3 +6,7 @@ target/
node_modules/
test-results/
playwright-report/
+
+# Bundled single-file talk (632 KB of inlined fonts) — rebuild with tools/bundle-talk.py
+dist/
+static/talk.html
diff --git a/content/preprints/_index.md b/content/preprints/_index.md
deleted file mode 100644
index 49b28dc..0000000
--- a/content/preprints/_index.md
+++ /dev/null
@@ -1,6 +0,0 @@
-+++
-title = "Preprints"
-description = "Working preprints and positioning notes on PulseEngine's verification methodology — draft, honesty-scoped, and pre-review."
-template = "preprints.html"
-sort_by = "date"
-+++
diff --git a/content/publications/_index.md b/content/publications/_index.md
new file mode 100644
index 0000000..2effdc3
--- /dev/null
+++ b/content/publications/_index.md
@@ -0,0 +1,6 @@
++++
+title = "Publications"
+description = "Talks and preprints from PulseEngine — conference decks as delivered, and working notes on the verification methodology. Draft, honesty-scoped, and pre-review unless stated otherwise."
+template = "publications.html"
+sort_by = "date"
++++
diff --git a/content/preprints/oracle-gated-agent-loops.md b/content/publications/oracle-gated-agent-loops.md
similarity index 99%
rename from content/preprints/oracle-gated-agent-loops.md
rename to content/publications/oracle-gated-agent-loops.md
index 1d10721..66f17e9 100644
--- a/content/preprints/oracle-gated-agent-loops.md
+++ b/content/publications/oracle-gated-agent-loops.md
@@ -4,6 +4,7 @@ description = "Treat the AI agent as an untrusted producer whose every output is
date = 2026-07-16
draft = false
template = "paper.html"
+aliases = ["/preprints/oracle-gated-agent-loops/"]
[taxonomies]
tags = ["verification", "ai-agents", "how-it-works"]
authors = ["Ralf Anton Beier"]
diff --git a/content/publications/wasm-research-day-2026.md b/content/publications/wasm-research-day-2026.md
new file mode 100644
index 0000000..7af1242
--- /dev/null
+++ b/content/publications/wasm-research-day-2026.md
@@ -0,0 +1,756 @@
++++
+title = "Change the Tires, Not the Car"
+description = "Wasm Research Day 2026. The Component Model as the integration step for an operating system, the same components lowered ahead of time onto three architectures, and an honest account of what is still missing."
+date = 2026-08-06
+aliases = ["/talks/wasm-research-day-2026/"]
+template = "talk.html"
+
+[extra]
+event = "Wasm Research Day 2026"
+slot = "25 + 5, remote"
++++
+
+
+
Wasm Research Day 2026 · 25 + 5
+
Change the Tires, Not the Car
+
The Component Model as the integration step for an OS
+ written in WebAssembly.
+
Ralf Anton Beier · avrabe
+
I work in automotive, so to me everything is a car —
+ declaring the bias up front.
+ pulseengine.eu · every number on these slides says where it came from
+
+
+
+
Wasm Research Day 2026the promise
+
In twenty-five minutes
+
By the end of this, you will be able to:
+
+
explain which parts of the Component Model survive being
+ compiled away entirely — and which do not
+
describe how one tool hands a machine-checked fact
+ to the next, and why it is keyed to a value rather than a position
+
quote what an operating system made of components costs on
+ a part with 8 KB of RAM
+
+
If any of those is still unclear at the end, I have
+ failed — ask me.
+
+
+
+
Act I · the inversion
+
How embedded actually builds software
+
+
+
what you do today
+
Take the vendor's HAL and board-support package for that part. Take an
+ RTOS with a port layer per architecture and a board file per board. Take
+ register headers generated from the chip's own description file. Select
+ variants with #ifdef. Statically link one image.
+
+
+
and it is the right answer
+
No MMU. Kilobytes of RAM. Hard deadlines. Cents per unit. Every
+ abstraction costs bytes and cycles that are not there, and the vendor knows
+ the silicon better than you do. This ships in billions of units, and it
+ works.
+
+
+
The consequence is the part worth arguing about: the OS is
+ the layer that gets rewritten per target, and the application's
+ portability is a convention, not a contract.
+
+
+
+
Act I · the inversion
+
So invert it
+
In embedded the hardware defines the software: pick the part
+ and you have picked the OS, the drivers, the toolchain. Reverse that
+ dependency — software becomes the durable artifact, silicon a
+ parameter.
+
Write the OS itself as WebAssembly components and make the Component Model the
+ integration step. Not a runtime on the device — a build step that
+ joins typed pieces and then gets compiled away.
+
The OS and everything above it is the car. The few native functions that touch
+ hardware are the tires. New chip, new board —
+ change the tires, not the car.
+
What software-defined means down here: not features
+ shipped over the air onto hardware chosen years ago, but software portable across
+ silicon that stays verified across the move.
A driver sits below the OS: it may import gust:hal and
+ must not depend upward on gust:os. That is not a convention — it is
+ a gate that fails the build.
+
+
+
+
Act II · the carthe whole chain
+
Integration step, not a build step
+
Five components in, one native object out — and every
+ arrow happens on a build machine, not on the device.
+ lower to ARMsynth
+ module + facts
+ →
+ gustos.o · 4 812 B text · .bss 0
+
+
+ linkld
+ .o + 3 native functions
+ →
+ firmware no engine, no interpreter, no JIT
+
+
+
+
+
+
Act II · the carthe whole chain
+
The same chain, actually run
+
Five components in, one relocatable object out —
+ and at the end, the two questions that matter: what does it still need from the
+ world, and what does it cost?
+
+
+
+
+
+
+
+
Act II · the cargust on the STM32F100RB
+
The part that sets the rules is a failsafe
+
We build flight software for a drone — a car in the air,
+ four rotors instead of four tires. This is its emergency motor controller: if the main
+ flight computer stops, it is what is still driving the motors.
+
+
the partSTM32F100RB — geometry generated from the architecture model128 KB flash · 8 KB RAM
+
+
Its one safety property is byte-exact pass-through.
+ When a rotor fails and the controller asymmetrically zeros motors, re-mixing
+ reintroduces the parasitic moment that caused a real failure. The failsafe must
+ not be clever.
+
A typed requirement, WIT generated from the model, and an
+ oracle — 46 rows × 4 motors, byte-exact, negative control must fail.
+ Status: draft.
+
+
+
+
Act II · the cargust on the STM32F100RB
+
What it costs on that part
+
a whole flashed image — the watchdog silicon test
+
text data bss
+ 6028 0 8
+flash 6 028 B of 131 072 4.6%
+SRAM 8 B of 8 192 0.1% — 8 184 free
+
No MMU. No engine. Eight bytes of RAM. That is why the
+ drivers are 0 SRAM, the interfaces are scalar, and the allocator traps instead of
+ growing — none of those are taste.
+
Scope: one dissolved driver plus the minimum to boot and
+ report. A floor, not a system footprint — no scheduler, no tenants.
A driver's capability is checked against a typed contract at composition
+ time. Before this it was an untyped env extern that only had to
+ match by name at native link.
+
+
+
+
Act II · the carone driver
+
A contract that cannot express the bug
+
A watchdog you can accidentally switch off is worthless. So the interface offers
+ no way to switch it off:
Behind it the driver is a small state machine — Idle →
+ Configured → Running — and a bounded proof
+ shows no edge leaves Running: refresh keeps
+ it there, unlock is rejected.
+
The contract cannot express the one transition the proof
+ forbids. That is the argument for putting a seam in a type system rather
+ than in a comment.
+
+
+
+
Act II · the cargust:hal · dma
+
The seam is not only scalars
+
Everything so far has been u32 in, u32 out. DMA is
+ where that stops — and the Component Model already has the vocabulary:
It consumes own<dma-buffer>: while the engine holds it the buffer
+ is statically inaccessible to wasm — a transfer,
+ not a copy.
+
+
seamthe ownership state machine, dissolved220 B · 0 SRAM · 6 Kani proofs
+
+
Outlook. “Does the Component Model require
+ extra copying?” (Luke Wagner) is not academic at 8 KB. Shared memory as a
+ canonical-ABI option is the general answer; this is the verified embedded instance of
+ it — and its awkward case, a host answering zero with a fixed address (MPU, not
+ MMU), is our default. Design reference: Christof Petig's wasm-shm-test.
Cortex-M3 · STM32F100RB — the same .o
+IWDG reset CONFIRMED IWDGRSTF=1
+
RISC-V · ESP32-C3 rev v0.4
+native 271 dissolved 499 milliticks/call ratio 1.839× slower
+correctness IDENTICAL over [0,2047] mismatch=0
+
+
Captured 2026-08-04, all three probes attached at once.
+ The watchdog legs are one happy path on two dies — they do not evidence
+ cannot-un-start; the firmware never attempts one.
+
+
+
+
Act III · the tiresgust, three hosts
+
Same bytes. Three different answerers.
+
+
+
in a browser tab
+
gust:hal/mmio answered by a JS array. Pulled from the
+ registry, signature verified, transpiled — 10 / 10
+ behavioural checks pass.
+
+
+
on a host
+
Answered by a Rust array under a component runtime. Same script, same
+ assertions.
+
+
+
on silicon
+
Answered by real registers. The composite is lowered first; nothing
+ interprets it.
+
+
+
The published artifact is the same one in all three:
+ ghcr.io/pulseengine/gale-nano:0.6.0, signed, pulled — not rebuilt
+ per target.
+
+
+
+
Act III · the tiresone driver
+
The whole of a tire
+
A component that imports gust:hal/mmio does not care who answers
+ it. In a browser tab, this is the answer — the whole of it:
+
web/shim-mmio.js
+
const REGS = new Uint32Array(64);
+// the one clock register the OS reads
+const TIM2_CNT = 0x40000024;
+export function read32(addr) {
+ const a = addr >>> 0;
+ return a === TIM2_CNT ? clock : REGS[(a >>> 2) & 63];
+}
Most of this code was written by AI, under review. That is
+ the premise, not a footnote.
+
An assistant will write a plausible driver, a plausible proof, and a plausible
+ green test, faster than anyone can read them. So the question stopped being
+ can it write the code and became what would have to be
+ true for me to believe it.
+
Qualify the pipeline once and the argument amortizes across every
+ product built on it. That is why the factory matters more than the car.
+
It is also why the failures later in this act are the
+ interesting part — they are what a plausible green check costs when nobody
+ can read everything.
+
+
+
+
Act IV · the factorymeld
+
Is this the Component Model, or our dialect?
+
The fuser does essentially what RFC 46 proposes, for
+ the sync subset — flatten the composition DAG, merge the index spaces,
+ generate adapter trampolines, re-wrap as a component.
declinedasync / fibers — no stack switching on these parts, and compiling the runtime in is a TCB problem
+
rejectedmultiply-instantiated modules — we refuse them rather than ship an unproved transform
+
the twoboth are the same shape — a middle component that forwards a resource it does not define, and the adapter cannot tell the two apartA → B → CC defines it · B only passes it on
+
+
+
+
+
Act IV · the factoryeverything below the seam
+
What you still have to trust
+
+
beforerustc + the LLVM wasm backend — every component starts here
+
composewac · the WIT generator · wit-bindgen's canonical glue
+
modelsour encodings of Wasm and of four ISAs
+
checkersthe LRAT checker's Lean proof, its kernel, the model↔code gap
+
belowld · the linker script · the native functions · hand-written unsafe
+
+
"Three native functions" is the seam, not the trusted base.
+ The base is this list, and none of the gates in this talk cover the first row.
+
+
+
+
Act IV · the factoryfour tools
+
Four tools, one spine
+
+
+
+
+
+
+
meld welds many components, joined at their interfaces, into a single module — so the boundaries stop existing at run time.
+
loom rewrites the code to be smaller and faster, and reverts any rewrite it cannot prove keeps the same behaviour.
+
synth turns the wasm into real machine instructions for a real chip, and re-proves the translation on every compilation.
+
scry is sound abstract interpretation — it reads the code without running it and over-approximates, so what it proves holds on every run. It records every place it had to give up as data.
+ Translation validationvalue equivalence · QF_BV
+ Behavioral differentialexecuted vs baseline
+ Total-operation modelthe verifier does not see traps
+
+
out
+ Optimized Wasmbyte-identical if nothing proven
+ wsc.factsvalue-range invariants
+
+
+
+
in
+ One core module.wasm or .wat — already fused
+ wsc.facts ingestbad section ⇒ no facts
+ cabi arena binddangling realloc → defined fn
+
+ Trap verdictsPROVEN-SAFE | POTENTIAL-TRAP
+ Shadow-stack boundconsumed by synth
+ Gap reportevery ⊤, as data
+
+
+
+
cyan a machine checks it
+ amber the hazard still openSame five rows — and every tool's hazard
+ is one defect: its model is more total than Wasm.
+
+
+
+
Act IV · the factoryloom → synth
+
No stage trusts the one above it
+
It is not running a separate pass to hunt for facts. To
+ delete a bounds check it must already have established the index is in
+ range — every optimizer does that. What is unusual is what happens
+ next: normally the code is emitted and the reasoning that justified it
+ evaporates.
+
Here it is written into a custom section instead — and the whole
+ channel is nine bytes:
+
custom section "wsc.facts"
+01 schema v1
+01 one fact
+ 01 kind = value-range
+ 03 func_index 3
+ 07 value_id 7 ← a VALUE, not a position
+ 03 00 ff 0f body: 0 ≤ v ≤ 2047 (sleb128)
+
+
+
+
Act IV · the factoryloom → synth
+
Why a value, not a position
+
An optimizer renumbers everything. Key a fact to an instruction index,
+ and the next pass deletes three instructions above it.
+
The fact is still true of something — and is now asserted about something
+ else. A downstream consumer then reasons about the wrong operand, with a valid
+ module and a machine-checked implication.
+
So a fact whose value did not survive the pipeline is
+ dropped, never re-pointed. An absent fact costs
+ performance; a mis-keyed one costs correctness.
+
+
+
+
Act IV · the factoryloom → synth
+
What the channel is worth
+
+
measuredone guarded memory access, lowered with and without the fact232 → 104 B
+
+
Honest scope: emitter, schema and wire format are done and
+ byte-verified against the consumer. The source that would populate this
+ at volume is not wired — so that is what the channel does when it carries a
+ fact, not evidence that we produce many yet.
The OS primitives above carry a proven bound —
+ ch ∈ [524, 1524] — so ch + 476 is
+ provably inside [1000, 2000] and
+ both clamp branches are dead code:
+
push {r7, lr}
+add.w r0, r0, #476
+uxth r0, r0
+pop {r7, pc} — the whole function, 12 B
+
+
+
+
Act IV · the factorysynth
+
What that is worth, measured
+
+
native LLVMfull clamp — what LLVM ships0.50 ticks/call
+
dissolved todayclamp still emitted0.70 — 1.4× slower
+
with the proofclamp elided0.23 — 2.2× faster
+
+
The output clamp stays; this is the intermediate range
+ check. The bound comes from a verified primitive, not off the wire.
+
+
+
+
Act IV · the factorysynth vs LLVM
+
… and no, LLVM is not the problem
+
tell it the same thing and it folds it too
+
assert_unchecked(524 <= ch && ch <= 1524);
+ → add.w r0, r0, #476 stock LLVM, 30 B → 12 B
+
So the codegen is not the result. Both emit the same
+ instruction — only one of them checked.
+
You can tell a compiler anything and it will believe you.
+ Get that range wrong and it is undefined behaviour, silently, with no
+ diagnostic. The question was never can the compiler fold it — it
+ is how would you know the premise is true.
+
+
+
+
Act V · what is missinggust drivers
+
What componentizing actually costs
+
driver object .text, core module → component
+
gpio 502 → 1196 B spi 454 → 1450 B
+timer 204 → 828 B wdg 638 → 1718 B
+.data / .bss, all of them 0 → 0
+flash is cheap here; SRAM is the binding constraint
+
+
+
+
Act V · what is missingwit-bindgen
+
So we patched the generator
+
measured for this talk
+
wdg, rebuilt both ways — feature off is the control
+(not the 1718 B shipped object; this is a newer bindgen)
+canonical glue on a growing allocator 1746 B
+backed by a bounded arena instead 1428 B−318
+
cabi_realloc now delegates to an embedder arena that traps rather
+ than growing. 29% of the overhead back — and the
+ drivers do not use it yet.
+
+
+
+
Act V · what is nextthe outlook
+
What we are building next, and what would change our minds
+
+
nowDissolve the whole OS. Its size today is a wasm number. Until a native object exists there is nothing to verify, and nothing to bound.next
+
thenA stack bound proven, not asserted. The compiler's own contract calls this reservation trusted rather than proven.2048 / 8192
+
thenIsolation enforced, not modelled. Partitions exist in the model, not yet as MPU regions on silicon — and fusing into one address space is where that gets sharp.
+
openThe dissolve is still a trusted step. Source proofs do not cross the lowering. Translation validation is the shape of an answer, not one.
+
+
What would change our minds: a verified translation we could
+ adopt instead of ours; a part whose registers defeat the seam; an assessor who
+ disagrees.
+
+
+
+
Act V · what is missingthe takeaway
+
Three things to take with you
+
+
oneThe Component Model can be a build step. Fuse the graph into one core module and the boundary is gone — 43 of 45 canonical-ABI fixtures then behave identically.
+
twoA proof can cross a tool boundary in nine bytes — keyed to a value, dropped rather than re-pointed when the value dies.
+
threeOn a part with 8 KB of RAM the seam costs nothing at run time, because by then it is not there.
+
+
The two that do not are resource chains through a
+ re-exporting middle component. The schema is open, and that ledger is a claim
+ rather than a result — if it is wrong I would rather hear it than not.
+
+
+
+
Change the tires, not the car
+
The OS as components is the demonstration. The factory
+ that lowers it — and can say why each stage is believed — is the part that
+ generalizes.
+
Ralf Anton Beier · github.com/avrabe
+ · pulseengine.eu · every tool named here is open source
+
+
+
+
backup not in the talk
+
Qualify the checker, not the prover
+
Certification asks why you believe the solver. "Qualify Z3" is not a
+ tractable answer.
+
So the solver stays untrusted and emits a certificate. Only a small
+ checker is trusted — and its soundness is machine-checked in Lean 4, with no
+ sorry in its kernel.
+
+
shippedbit-vector obligations re-discharged with re-checkable certificates62 / 62
+
scope62 of the bit-vector obligations. The rest of each proof still rests on the solver.
+
+
Don't trust the tool — check its output.
+
+
+
+
backup not in the talk
+
Exactly how far this goes — and no further
+
+
shippingtheorem proving · SMT · bounded MC · translation validation
+
partialrefinement to Lean · mutation · abstract interpretation
+
not yetAn authority audit. We have not been audited.
+
+
Bounded model checking is bounded. Verus, Rocq and Kani are gated on
+ pull requests — but path-filtered, so a commit outside those paths triggers
+ nothing. Lean runs in no workflow at all.
+
+
+
+
backup not in the talk
+
Every one of these gates was green for the wrong reason
+
+
scrya proof that never ran
+
synthtwo validators, one blind spot
+
looma gate with zero callers
+
melda test on a path the shipped code skipped
+
galea count that cannot see instances
+
+
One of them, concretely: a requirement said the fuser
+ rejects a component that instantiates a module twice. The test called the reject
+ function directly and passed. The shipped path accepted those modules and
+ duplicated them.
+
The failure produced the same observable as
+ success.
+
+
+
+
backup not in the talk
+
Two things building this talk taught us
+
+
+
the runner broke on success
+
Plugging in the third board made the first unreachable. The
+ all-three-at-once case was the one nothing had run.
+
+
+
a reproducible number that isn't
+
A byte-reproducible command whose wasm input is not in the repo — it
+ lived in a scratch directory that no longer exists.
+
+
+
A bench whose input is not committed is not
+ reproducible, however precisely its output is recorded.
+
+
+
+
Act V · what is missingall of it
+
Before the rest of the vision holds
+
+
A proven stack bound. An OS node reserves 2 048 of
+ those 8 192 bytes for its shadow stack — and the compiler's own contract
+ says that budget is asserted, not proven. scry computes the depth;
+ wiring it to the reservation is the named next step, and until it lands the
+ number is our word.
+
Multi-tenant isolation on real MPU regions — modelled, not yet enforced on silicon.
+
Drivers beyond the ones that port cleanly. A verified state machine for one
+ bus does not transfer to the next revision of it — that needs a fresh proof.
+
The canonical-ABI overhead above, reduced rather than accepted.
+
Certificates on every obligation, not the subset that has them today.
+
Someone outside this project auditing the dossier.
+
+
+
+
+
Act V · what is missing
+
When not to dissolve
+
+
+
dissolve
+
One closed tenant graph · no MMU · a narrow, hardware-shaped interface ·
+ footprint and determinism dominate · re-qualification is per product anyway.
+
+
+
link a shared system-interface binary
+
Several runtimes on one OS and ISA · a wide, dynamic, POSIX-shaped
+ interface · third parties ship binaries · the fleet needs a driver updated
+ without re-qualifying the image.
+
+
+
Both positions want the interface specified as WIT and typed. We differ only
+ in when it binds — and my side of that line is the
+ narrow one.
+
+
+
+
Act II · the carone driver
+
The bounded proof behind that contract
+
fn p2_cannot_un_start() {
+ let w = Iwdg { phase: Running, .. };
+ if let Ok(n) = refresh(w) { assert_eq!(n.phase, Running); }
+ // no escape from Running:
+ assert!(unlock(w).is_err());
+}
+
The contract cannot express the one transition the proof
+ forbids. That is the argument for putting a seam in a type system rather
+ than in a comment.
+
diff --git a/content/talks/wasm-research-day-2026-notes.md b/content/talks/wasm-research-day-2026-notes.md
new file mode 100644
index 0000000..8784c50
--- /dev/null
+++ b/content/talks/wasm-research-day-2026-notes.md
@@ -0,0 +1,222 @@
++++
+title = "Speaker notes — every number in the deck"
+description = "What each figure in the Wasm Research Day 2026 talk measures, what it does not mean, and where it came from."
+date = 2026-08-06
+draft = true # deck published, speaker notes deliberately not
+template = "page.html"
++++
+
+The title slide promises *every number on these slides says where it came from*.
+This is that promise, written down. Open it on a second screen during Q&A.
+
+Each entry is: **what the slide says** → what it actually measures → **what it
+does not mean** → where it comes from.
+
+---
+
+## 43 of 45 — slides 19 and 32
+
+**Slide 19** ("Is this the Component Model, or our dialect?") — *43 / 45
+canonical-ABI fixtures pass at runtime.*
+**Slide 32** (takeaway) — *fuse the graph into one core module and the boundary is
+gone; 43 of 45 canonical-ABI fixtures then behave identically.*
+
+**What it measures.** 45 wit-bindgen test fixtures. Each one is a *component
+graph* exercising a canonical-ABI feature — strings, lists, records, variants,
+options, results, resources, multi-return, flags, enums, type aliases — across
+**both directions** of cross-component calls. For each: compose the graph, fuse it
+into a single core module, **run it**, and compare the observed behaviour against
+the unfused original. 43 behave identically.
+
+This is a **differential execution oracle**, not a validation check. That
+distinction matters and is worth saying: a fused module can type-check, pass
+`wasm-tools validate`, and still be wrong. Only running it catches that class.
+
+**What it does not mean.**
+- Not 43/45 of the Component Model *specification* — it is a fixture pass rate.
+- Not "lowered to native and still correct". This is the **fusion** step, run
+ under a host. The lowering to a native object is a separate stage.
+- Not a claim about async, which is rejected rather than tested.
+
+**The two failures.** Three-component resource forwarding chains where the
+*intermediate* component re-exports a resource it does not itself define. A known
+hard corner of the canonical ABI, not a general weakness.
+
+**Source.** meld's RFC-46 response, and its fixture suite.
+
+---
+
+## The composition figures — slide 6
+
+*5 components → 1 component, 20 741 B → meld fuse → 1 core module, 9 874 B (−52.4%)
+→ gustos.o, 4 812 B text, .bss 0 → 3 native functions.*
+
+**What it measures.** The five `gust:os` provider components, composed with `wac`,
+fused with `meld fuse --memory shared`, optimized with `loom optimize --passes
+inline`, lowered with `synth compile --target cortex-m3 --all-exports
+--relocatable`. Sizes by `wc -c` and `arm-zephyr-eabi-size`. The three undefined
+symbols are `poll-task`, `read32`, `write32`, by `nm -u`.
+
+**What it does not mean.**
+- `.bss 0` is **zero static RAM in the object** — not "this OS needs no RAM".
+ Stacks and any linear-memory arena are provided by the embedder.
+- "3 native functions" is the **seam**, not the trusted base. See slide 20.
+- The 52.4% includes deleted component metadata, not only memory merging.
+
+**Correction on the record.** An earlier version of the flow slide said *11 linear
+memories*. The composed component has **5**. The 11 came from a grep that also
+matched five `(export "memory")` lines and a `canon lift`; meld's own stdout says
+"Fusing 11 components", which made the wrong number look right.
+
+---
+
+## 8 bytes of SRAM — slide 9
+
+*A whole flashed image: 6 028 B flash of 131 072 (4.6%), 8 B SRAM of 8 192 (0.1%),
+8 184 free.*
+
+**What it measures.** `gust_wdg_silicon` — the firmware flashed for the Cortex-M3 leg (STM32F100RB) — by `arm-zephyr-eabi-size`.
+
+**What it does not mean.** This is the **watchdog silicon test image**: one
+dissolved driver plus the minimum to boot and report. It is a **floor, not a
+system footprint** — no scheduler, no task set, no application. Say this before
+someone asks; the slide says it too.
+
+---
+
+## 2 048 of 8 192 — slide 33 (gaps)
+
+*An OS node reserves 2 048 bytes for its shadow stack, and the budget is asserted
+rather than proven.*
+
+**Why it is in the deck.** gale's OS-node builds pass `synth --shadow-stack-size
+2048`, and synth's own flag contract says: *"The footprint is ASSERTED (the budget
+is trusted), not proven — synth does not yet prove the program's max shadow-stack
+depth fits the budget."* scry computes the depth; wiring it is the named next
+step. If asked "do you have a stack bound" the answer is **no, and here is exactly
+what would give us one**.
+
+---
+
+## The driver seams — slides 17 and 18
+
+*USART: 254 B · 0 SRAM · 3 relocations. DMA: 220 B · 0 SRAM · 6 Kani proofs.*
+
+**What it measures.** `arm-zephyr-eabi-size` on the committed dissolved objects;
+`nm -u` for the relocation count; `kani::proof` harness count for the DMA
+ownership FSM.
+
+**Correction on the record.** The USART figure was **326 B** in an earlier draft.
+That number comes from a results file attributed to a two-year-old toolchain and
+no current build reproduces it; the committed object measures 254. The DMA object
+is **220 B**, not the 218 that had been circulating.
+
+---
+
+## Three dies — slide 14
+
+*Cortex-M4 and Cortex-M3: IWDG reset CONFIRMED, `RCC_CSR 0x14000000 → 0x34000000`,
+`IWDGRSTF=1`. RISC-V: native 271 vs dissolved 499 milliticks/call, 1.839× slower,
+correctness IDENTICAL over [0,2047], mismatch 0.*
+
+**What it does not mean.** The two watchdog legs are **one happy path on two
+dies**. They do not evidence the cannot-un-start property — the firmware never
+attempts an un-start. That property is a source-level Kani proof and stays one.
+
+The ESP32-C3 figure **reproduces** a July measurement using the committed synth
+0.40 object; the current toolchain pin is newer, so it is not a measurement of
+what we ship today. The re-dissolve is blocked because the `gust_mix` wasm input
+is not in the repository.
+
+---
+
+## The fact channel — slides 21 to 23
+
+*Nine bytes: `01 01 01 03 07 03 00 ff 0f`. A guarded memory access: 232 → 104 B.*
+
+**What it measures.** The nine bytes are computed from loom's own emitter
+(`build_wsc_facts_payload`): schema version, fact count, kind, function index,
+value id, body length, then `lo`/`hi` as signed LEB128. One value-range fact,
+function 3, value 7, range [0, 2047].
+
+**What it does not mean.** The 232 → 104 figure is **what the channel does when it
+carries a fact** — not evidence that we produce many. The emitter, schema and wire
+format are done and byte-verified against the consumer; the *source* that would
+populate it at volume is not wired. loom emits **no** `wsc.facts` section by
+default.
+
+---
+
+## The clamp — slides 26 to 28
+
+*native LLVM 0.50 ticks/call · dissolved today 0.70 (1.4× slower) · with the proof
+0.23 (2.2× faster). And `assert_unchecked` → stock LLVM 30 B → 12 B.*
+
+**What it measures.** `gust_floor_bench`, same harness for all three. The
+`assert_unchecked` comparison is rustc → thumbv7m, `opt-level="s"`, lto,
+panic=abort.
+
+**The honest headline, volunteered before anyone asks.** The shipping
+configuration is **1.4×–1.84× slower than native LLVM**. The 0.23 row is the
+proof-carrying path, and it depends on a fact channel whose producer is not wired.
+
+**Correction on the record.** The deck used to claim *"a compiler with no verifier
+cannot reach it"*. That is **false** — told the same premise, stock LLVM folds the
+clamp identically. What is ours is the *provenance* of the premise:
+`assert_unchecked` is unchecked, so a wrong range is undefined behaviour with no
+diagnostic. Both emit the same instruction; only one of them checked.
+
+---
+
+## Componentization cost — slides 30 and 31
+
+*gpio 502 → 1196 · timer 204 → 828 · spi 454 → 1450 · wdg 638 → 1718 B. And
+1746 → 1428 B, −318, with a bounded arena.*
+
+**What it does not mean.** The **1746** control is a *rebuild* against the
+wit-bindgen fork with the feature off — not the shipped 1718 object. The −318 is
+attributable to the feature alone; the version bump between them costs +20 B on
+its own. Measuring against the shipped object would have credited the feature with
+−298 and been wrong.
+
+**Correction on the record.** The spi figure was **1244** in an earlier draft.
+That number appears nowhere in the repository or its history; the measured and
+recorded figure is 1450.
+
+---
+
+## What synth actually eats — slide 21 (synth tab)
+
+**Correction on the record.** The synth tab's `in` row used to read *WIT / ABI —
+lift · lower*, and did not name the actual input at all. On gale's path synth is
+handed **one core module** — `loom.wasm`, `fused.stripped.wasm`, or a `.wat`; every
+`build-*.sh` in `benches/gust/` calls `synth compile `. It is never
+handed a WIT file or a component, and its CLI has no `--wit` flag.
+
+synth *does* carry a WIT parser (`synth-wit`) and a canonical-ABI lift/lower
+implementation (`synth-abi`) — but on this pipeline they are not on the path,
+because **meld already did the lifting and lowering upstream and erased the
+boundary**. Claiming them as synth inputs credited synth with meld's work.
+
+If asked "so what does synth do with WIT?" — on this pipeline, nothing. It is a
+core-module compiler here. The Component Model work happens one stage earlier.
+
+---
+
+## 50 rules · 50 Rocq Qed — slide 20 (synth tab)
+
+Say the denominator if asked: 50 *selection* rules proved, against synth's own ISA
+model. It is not 50 of all rules in all backends, and the model is ours rather than
+an external mechanization.
+
+---
+
+## Things to say before being asked
+
+- **Proofs are gated on pull requests, path-filtered** — Verus, Rocq and Kani run
+ on push and PR to main for proof-relevant paths. A commit outside those paths
+ triggers nothing. **Lean runs in no workflow at all.**
+- **We have not been audited** by any certification authority. The project says so
+ in its own posture statement.
+- **Bounded model checking is bounded.** If asked for the bound on a specific
+ property, say you will follow up rather than guess.
diff --git a/sass/_talk.scss b/sass/_talk.scss
new file mode 100644
index 0000000..1f7cbf5
--- /dev/null
+++ b/sass/_talk.scss
@@ -0,0 +1,818 @@
+// Slide deck — a presentation surface built on the site's own tokens.
+// Deliberately NOT a generic deck theme: it inherits --bg / --accent / the
+// Atkinson pair from _variables.scss, so a slide looks like the site rather
+// than like a template. Self-hosted fonts (see _fonts.scss) mean it presents
+// with no network at all.
+
+.deck {
+ --slide-pad: clamp(1.25rem, 5vw, 5rem);
+ // Chrome sits above the home indicator / rounded corners on an iPad.
+ --safe-b: max(env(safe-area-inset-bottom), .55rem);
+ --safe-l: max(env(safe-area-inset-left), 1.1rem);
+ --safe-r: max(env(safe-area-inset-right), 1.1rem);
+
+ position: fixed;
+ inset: 0;
+ // iOS Safari's `100vh` counts the area behind the toolbars, so the last line
+ // of a slide hides under them. `dvh` tracks the live viewport; the `inset`
+ // above is the fallback where dvh is unsupported.
+ height: 100dvh;
+ background: $bg;
+ color: $text;
+ font-family: $font-sans;
+ overflow: hidden;
+ z-index: 200;
+
+ // One lever for the whole type scale. Slides are sized in vmin, which tracks
+ // height; on a short screen the same words need proportionally more of it, so
+ // the scale steps down rather than every slide being re-trimmed per device.
+ --fs: 1;
+
+ // Stop iOS from inflating text in the landscape orientation it will be
+ // presented in, which would otherwise break the fitted type scale.
+ -webkit-text-size-adjust: 100%;
+ // No rubber-band bounce dragging the whole deck around.
+ overscroll-behavior: none;
+}
+
+.deck__stage {
+ position: absolute;
+ inset: 0;
+ display: grid;
+}
+
+// Every slide occupies the same grid cell; only the current one is visible.
+.slide {
+ grid-area: 1 / 1;
+ display: flex;
+ flex-direction: column;
+ justify-content: center;
+ gap: 1.1rem;
+ padding: var(--slide-pad);
+ // Clear the on-screen controls and the home indicator.
+ padding-bottom: calc(var(--slide-pad) + 3.6rem + var(--safe-b));
+ overflow-y: auto;
+ visibility: hidden;
+ opacity: 0;
+ transition: opacity .28s ease;
+
+ &.is-current { visibility: visible; opacity: 1; }
+
+ // A slide's own scroll must never move the page behind it.
+ overscroll-behavior: contain;
+ -webkit-overflow-scrolling: touch;
+ // Let the browser own vertical panning and leave horizontal gestures to the
+ // swipe handler — without this iOS may claim the swipe as a back-navigation.
+ touch-action: pan-y;
+}
+
+@media (prefers-reduced-motion: reduce) {
+ .slide { transition: none; }
+}
+
+// ─── Type scale ───────────────────────────────────────────────────────
+// Sized in vmin so a slide reads the same projected, shared, or in a tab.
+
+.slide h1 {
+ font-size: clamp(2.8rem, min(calc(8.4vmin * var(--fs)), calc(6.64vh * var(--fs))), 6rem);
+ line-height: 1.1;
+ font-weight: 700;
+ letter-spacing: -0.02em;
+ text-wrap: balance;
+ margin: 0;
+}
+
+.slide h2 {
+ font-size: clamp(2.1rem, min(calc(6.0vmin * var(--fs)), calc(4.74vh * var(--fs))), 4.2rem);
+ line-height: 1.15;
+ font-weight: 600;
+ letter-spacing: -0.015em;
+ text-wrap: balance;
+ margin: 0;
+}
+
+.slide p,
+.slide li {
+ font-size: clamp(1.45rem, min(calc(4.2vmin * var(--fs)), calc(3.32vh * var(--fs))), 2.9rem);
+ line-height: 1.55;
+ // Wide enough to sit against a full-width evidence block without reading as
+ // a narrow column pinned to the left edge.
+ max-width: min(100%, 62ch);
+ margin: 0;
+}
+
+.slide ul { display: flex; flex-direction: column; gap: .38rem; padding-left: 1.1rem; margin: 0; }
+
+// The eyebrow says which act we are in — it is structural, not decorative:
+// the deck has five acts and the label is how the audience keeps its place.
+.slide p.slide__act,
+.slide__act {
+ font-family: $font-mono;
+ font-size: clamp(1rem, min(calc(2.3vmin * var(--fs)), calc(1.82vh * var(--fs))), 1.5rem);
+ letter-spacing: .14em;
+ text-transform: uppercase;
+ color: $text-faint;
+ margin: 0;
+}
+
+.slide__lead {
+ font-size: clamp(1.7rem, min(calc(5.0vmin * var(--fs)), calc(3.95vh * var(--fs))), 3.4rem) !important;
+ color: $text-dim;
+ max-width: min(100%, 44ch);
+}
+
+// A pull-quote slide: the project's own words, attributed.
+.slide__quote {
+ font-size: clamp(2.1rem, min(calc(5.6vmin * var(--fs)), calc(4.42vh * var(--fs))), 4rem);
+ line-height: 1.3;
+ font-weight: 500;
+ max-width: 26ch;
+ text-wrap: balance;
+ border-left: 3px solid $accent;
+ padding-left: 1.2rem;
+}
+
+.slide p.slide__cite,
+.slide__cite {
+ max-width: min(100%, 92ch); // mono runs ~0.6em/char — needs more ch to match
+ font-family: $font-mono;
+
+ // A long closing note reads better across the full slide than as a tall column
+ // in the left two-thirds — fewer lines, and it stops competing with the body
+ // block above it for the same measure.
+ &.is-wide { max-width: 100%; }
+ font-size: clamp(1.05rem, min(calc(2.5vmin * var(--fs)), calc(1.98vh * var(--fs))), 1.6rem);
+ color: $text-faint;
+}
+
+// ─── Evidence blocks ──────────────────────────────────────────────────
+// Real captured output. Monospace, bordered, and horizontally scrollable in
+// its own container so a long line never scrolls the slide sideways.
+
+.evidence {
+ font-family: $font-mono;
+ font-size: clamp(1.15rem, min(calc(3.2vmin * var(--fs)), calc(2.53vh * var(--fs))), 2rem);
+ line-height: 1.5;
+ background: $bg-subtle;
+ border: 1px solid $border-subtle;
+ border-radius: 10px;
+ padding: .9rem 1.1rem;
+ overflow-x: auto;
+ white-space: pre;
+ margin: 0;
+ max-width: 100%;
+}
+
+// Several evidence blocks read as one exhibit. Separate
elements rather
+// than one with blank lines in it: a blank line inside a raw-HTML block ends
+// the block, and the markdown parser resumes *inside* the evidence.
+.stack {
+ display: flex;
+ flex-direction: column;
+ gap: .5rem;
+ width: 100%;
+}
+
+.slide p.evidence__label,
+.evidence__label {
+ font-family: $font-mono;
+ font-size: clamp(.95rem, min(calc(2.2vmin * var(--fs)), calc(1.74vh * var(--fs))), 1.4rem);
+ letter-spacing: .06em;
+ text-transform: uppercase;
+ color: $text-faint;
+ margin: 0 0 -.5rem;
+}
+
+.ok { color: $green; }
+.bad { color: $red; }
+.warn { color: $amber; }
+.dim { color: $text-faint; }
+.hi { color: $accent; }
+
+// ─── Terminal recording ───────────────────────────────────────────────
+// A real capture replayed inline. Text, not video: selectable, crisp at any
+// projection size, ~2 KB on disk, and it degrades to a disabled button rather
+// than a broken embed if the file cannot be read.
+
+.cast {
+ display: flex;
+ flex-direction: column;
+ gap: .5rem;
+ width: 100%;
+ min-height: 0;
+}
+
+.cast__play {
+ align-self: flex-start;
+ font-family: $font-mono;
+ font-size: clamp(.85rem, min(calc(1.85vmin * var(--fs)), calc(1.46vh * var(--fs))), 1.1rem);
+ padding: .45rem 1rem;
+ min-height: 44px; // same touch target as the deck controls
+ color: $text;
+ background: $surface;
+ border: 1px solid $border;
+ border-radius: 8px;
+ cursor: pointer;
+ -webkit-tap-highlight-color: transparent;
+ touch-action: manipulation;
+
+ &::before { content: '▶ '; color: $green; }
+ &:hover:not(:disabled) { border-color: $accent; }
+ &:disabled { color: $text-faint; cursor: default; &::before { content: ''; } }
+ &:focus-visible { outline: 2px solid $accent; outline-offset: 2px; }
+}
+
+.cast__screen {
+ font-family: $font-mono;
+ font-size: clamp(1.05rem, min(calc(2.9vmin * var(--fs)), calc(2.29vh * var(--fs))), 1.8rem);
+ line-height: 1.45;
+ white-space: pre-wrap;
+ word-break: break-word;
+ background: #0b0d13; // a terminal is a terminal in both themes
+ color: #d7dae3;
+ border: 1px solid $border-subtle;
+ border-radius: 10px;
+ padding: .8rem 1rem;
+ margin: 0;
+ overflow-y: auto;
+ display: none;
+ // In a flex column a
with min-height:0 is squashed to nothing by its
+ // siblings — the recording played into a box a few pixels tall. Claim the
+ // room explicitly instead.
+ flex: 1 1 auto;
+ min-height: 46vmin;
+}
+
+.cast.is-open {
+ flex: 1 1 auto;
+ min-height: 0;
+ .cast__screen { display: block; }
+}
+
+// Running the recording hands the slide over to it: the diagram has made its
+// point by then, and the terminal is the evidence for the same claim.
+.slide.cast-open {
+ justify-content: flex-start;
+ .flow { display: none; }
+}
+
+// ─── Claim ledger ─────────────────────────────────────────────────────
+// The provenance marker is the point of this deck: every number says whether
+// it was measured for this talk or is a standing project claim.
+
+.ledger {
+ display: grid;
+ gap: .5rem;
+ width: 100%;
+ max-width: min(100%, 64ch);
+}
+
+.ledger__row {
+ display: grid;
+ grid-template-columns: auto 1fr auto;
+ align-items: baseline;
+ gap: .9rem;
+ padding: .55rem .8rem;
+ background: $surface;
+ border: 1px solid $border-subtle;
+ border-radius: 8px;
+ font-size: clamp(1.15rem, min(calc(3.0vmin * var(--fs)), calc(2.37vh * var(--fs))), 1.9rem);
+}
+
+.ledger__tag {
+ font-family: $font-mono;
+ font-size: .78em;
+ letter-spacing: .05em;
+ text-transform: uppercase;
+ white-space: nowrap;
+}
+
+.ledger__val {
+ font-family: $font-mono;
+ font-variant-numeric: tabular-nums;
+ white-space: nowrap;
+ color: $text;
+}
+
+// A worked example in the value column: the shape of the failure, not a number.
+.ledger.is-wide { max-width: min(100%, 92ch); }
+.ledger__fig {
+ text-align: right;
+ white-space: normal; // the sub-label must be allowed to wrap; nowrap
+ max-width: 26ch; // is inherited from .ledger__val and clips it at
+ b { color: $amber; } // narrow widths instead of shrinking.
+ .fig__line { white-space: nowrap; }
+ small {
+ display: block;
+ font-size: .68em;
+ line-height: 1.25;
+ color: $text-dim;
+ letter-spacing: .01em;
+ }
+}
+
+// ─── Flow: what each stage eats and what it emits ─────────────────────
+// The tool sites answer "what goes in, what comes out" for every stage; a
+// pipeline drawn as bare arrows does not. Each row names both sides.
+
+.flow {
+ display: grid;
+ gap: .24rem;
+ width: 100%;
+}
+
+.flow__row {
+ display: grid;
+ grid-template-columns: minmax(6rem, auto) 1fr auto 1fr;
+ align-items: center;
+ gap: .5rem .9rem;
+ padding: .38rem .8rem;
+ background: $surface;
+ border: 1px solid $border-subtle;
+ border-radius: 8px;
+}
+
+.flow__stage {
+ font-family: $font-mono;
+ font-size: clamp(1.2rem, min(calc(3.0vmin * var(--fs)), calc(2.37vh * var(--fs))), 1.9rem);
+ font-weight: 600;
+ color: $accent;
+
+ // The action is what the audience needs to follow; the tool name goes on its
+ // own line underneath, for whoever wants to look it up afterwards. Without
+ // `display: block` these run together as "composewac".
+ small {
+ display: block;
+ font-size: .72em;
+ font-weight: 400;
+ color: $text-faint;
+ margin-top: .1rem;
+ }
+}
+
+.flow__in,
+.flow__out {
+ font-family: $font-mono;
+ font-size: clamp(1.05rem, min(calc(2.7vmin * var(--fs)), calc(2.13vh * var(--fs))), 1.7rem);
+ line-height: 1.35;
+}
+
+.flow__in { color: $text-dim; }
+.flow__out { color: $text; }
+
+.flow__arrow {
+ font-family: $font-mono;
+ color: $text-faint;
+ font-size: clamp(1.2rem, min(calc(2.9vmin * var(--fs)), calc(2.29vh * var(--fs))), 1.8rem);
+}
+
+// Stack the row on a narrow screen rather than crushing four columns.
+@media (max-width: 720px) {
+ .flow__row { grid-template-columns: 1fr; gap: .15rem; }
+ .flow__arrow { display: none; }
+ .flow__in::before { content: 'in '; color: var(--text-faint); }
+ .flow__out::before { content: 'out '; color: var(--text-faint); }
+}
+
+// Code inside a two-column split has roughly half the width, so it takes one
+// step down — still well above the 11.6px it used to be, and it stops the
+// WIT block scrolling sideways inside its column.
+.split .evidence { font-size: clamp(1rem, min(calc(2.7vmin * var(--fs)), calc(2.13vh * var(--fs))), 1.7rem); padding: .7rem .85rem; }
+
+// ─── Two-column split ─────────────────────────────────────────────────
+
+.split {
+ display: grid;
+ grid-template-columns: repeat(auto-fit, minmax(15rem, 1fr));
+ gap: 1.2rem;
+ width: 100%;
+}
+
+.split__col h3 {
+ font-family: $font-mono;
+ font-size: clamp(1rem, min(calc(2.4vmin * var(--fs)), calc(1.9vh * var(--fs))), 1.5rem);
+ letter-spacing: .1em;
+ text-transform: uppercase;
+ color: $text-faint;
+ margin: 0 0 .55rem;
+ font-weight: 500;
+}
+
+// ─── Chrome: progress, counter, help ──────────────────────────────────
+
+.deck__progress {
+ position: absolute;
+ left: 0; bottom: 0;
+ height: 2px;
+ background: $accent;
+ transition: width .28s ease;
+ z-index: 2;
+}
+
+.deck__counter {
+ position: absolute;
+ right: var(--safe-r);
+ bottom: calc(var(--safe-b) + 3.1rem);
+ font-family: $font-mono;
+ font-variant-numeric: tabular-nums;
+ font-size: .8rem;
+ color: $text-faint;
+ z-index: 2;
+}
+
+.deck__hint {
+ position: absolute;
+ left: var(--safe-l);
+ bottom: calc(var(--safe-b) + .9rem);
+ font-family: $font-mono;
+ font-size: .8rem;
+ color: $text-faint;
+ z-index: 2;
+}
+
+// ─── On-screen controls ───────────────────────────────────────────────
+// The only way to drive the deck on a tablet.
+
+.deck__nav {
+ position: absolute;
+ right: var(--safe-r);
+ bottom: var(--safe-b);
+ display: flex;
+ gap: .4rem;
+ z-index: 3;
+}
+
+.deck__btn {
+ // 44px is Apple's minimum comfortable touch target.
+ min-width: 44px;
+ min-height: 44px;
+ display: grid;
+ place-items: center;
+ font-family: $font-mono;
+ font-size: 1.05rem;
+ line-height: 1;
+ color: $text-dim;
+ background: $surface;
+ border: 1px solid $border-subtle;
+ border-radius: 10px;
+ cursor: pointer;
+ // Suppress the iOS tap flash and the double-tap-to-zoom delay.
+ -webkit-tap-highlight-color: transparent;
+ touch-action: manipulation;
+ transition: color .15s ease, border-color .15s ease;
+
+ &:hover { color: $text; border-color: $border; }
+ &:active { background: $surface-raised; }
+
+ &:focus-visible {
+ outline: 2px solid $accent;
+ outline-offset: 2px;
+ }
+}
+
+@media (prefers-reduced-motion: reduce) {
+ .deck__btn { transition: none; }
+}
+
+// Previously these were dimmed to .35 under `(hover: hover)` and restored on
+// hover. An iPad with a keyboard or trackpad attached MATCHES that query while
+// the person is still touching the screen — so the controls went nearly
+// invisible with no way to bring them back. A presenter always needs the
+// controls; they stay visible.
+.deck__nav { opacity: .8; transition: opacity .2s ease; }
+.deck:hover .deck__nav,
+.deck__nav:focus-within { opacity: 1; }
+
+// ─── Overview (press o) ───────────────────────────────────────────────
+
+.deck.is-overview {
+ .deck__stage {
+ display: grid;
+ grid-template-columns: repeat(auto-fill, minmax(13rem, 1fr));
+ gap: .8rem;
+ padding: 1.2rem;
+ padding-bottom: calc(3.6rem + var(--safe-b));
+ overflow-y: auto;
+ -webkit-overflow-scrolling: touch;
+ align-content: start;
+ }
+
+ counter-reset: slideno;
+
+ // A thumbnail shows the act, the heading and the number — not a shrunken
+ // render of the whole slide. Scaling every element by hand was fragile: at
+ // tablet width every one of the nineteen thumbnails overflowed its box by up
+ // to 2x and got clipped mid-line, which reads as slides overlapping. Title
+ // cards cannot spill, stay legible at any width, and are what you actually
+ // need mid-talk — which slide is which.
+ .slide {
+ counter-increment: slideno;
+ grid-area: auto;
+ visibility: visible;
+ opacity: .6;
+ aspect-ratio: 16 / 10;
+ justify-content: flex-start;
+ padding: .7rem .8rem;
+ border: 1px solid $border-subtle;
+ border-radius: 8px;
+ background: $bg-subtle;
+ cursor: pointer;
+ overflow: hidden;
+ gap: .3rem;
+ transition: opacity .15s ease, border-color .15s ease;
+
+ &.is-current { opacity: 1; border-color: $accent; }
+ &:hover { opacity: .85; }
+
+ // Everything that is not the act label or the heading is suppressed.
+ > *:not(.slide__act):not(h1):not(h2) { display: none; }
+
+ &::after {
+ content: counter(slideno);
+ position: absolute;
+ right: .55rem;
+ bottom: .4rem;
+ font-family: $font-mono;
+ font-variant-numeric: tabular-nums;
+ font-size: .72rem;
+ color: $text-faint;
+ }
+
+ position: relative;
+
+ .slide__act { font-size: .62rem; letter-spacing: .1em; }
+ h1 { font-size: 1rem; line-height: 1.2; }
+ h2 { font-size: .92rem; line-height: 1.25; }
+ }
+}
+
+// Presenter notes never render on the slide; they are for the speaker's
+// source file only.
+.notes { display: none; }
+
+@media print {
+ .deck { position: static; }
+ .deck__stage { display: block; }
+ .slide { visibility: visible; opacity: 1; page-break-after: always; min-height: 100vh; }
+ .deck__progress, .deck__counter, .deck__hint { display: none; }
+}
+
+// On a narrow screen (a tablet held in portrait) a long code line has nowhere
+// to go: it stays inside the block's own scroll, but the reader has to swipe a
+//
to finish a sentence. Wrap instead — landscape keeps `pre`.
+@media (max-width: 900px) {
+ .evidence { white-space: pre-wrap; word-break: break-word; }
+}
+
+// ─── Very short viewports ────────────────────────────────────────────
+// The vh cap above handles aspect; this is only a floor for laptop screens
+// short enough that even a height-proportional scale crowds the dense slides.
+@media (max-height: 620px) { .deck { --fs: .9; } }
+
+// ─── Architecture diagram ─────────────────────────────────────────────
+// Stages read top-to-bottom with the stage name in a left gutter. The source
+// diagrams are left-to-right columns, but six columns on a slide put the block
+// labels at 11px and the reading order stopped being obvious once they wrapped.
+// A vertical sequence has one unambiguous order and gives every block real width.
+
+.archtabs { display: flex; gap: .4rem; }
+
+.archtab {
+ font-family: $font-mono;
+ font-size: clamp(.85rem, min(2vmin, 1.7vh), 1.15rem);
+ padding: .3rem .8rem;
+ min-height: 38px;
+ color: $text-dim;
+ background: transparent;
+ border: 1px solid $border-subtle;
+ border-radius: 7px;
+ cursor: pointer;
+ -webkit-tap-highlight-color: transparent;
+ touch-action: manipulation;
+
+ &.is-on { color: $bg; background: $accent; border-color: $accent; font-weight: 600; }
+ &:focus-visible { outline: 2px solid $accent; outline-offset: 2px; }
+}
+
+// One plain-language line per tool, swapped with the tab. The tab labels are
+// tool names this room has no reason to know; the rows below are structure, not
+// purpose. Without this the slide says how, and never what.
+.archwhat {
+ display: none;
+ font-size: clamp(.95rem, min(calc(2.5vmin * var(--fs)), calc(1.98vh * var(--fs))), 1.5rem);
+ line-height: 1.4;
+ color: $text-dim;
+ max-width: min(100%, 78ch);
+ margin: 0;
+
+ &.is-on { display: block; }
+ b { color: $text; font-weight: 600; }
+}
+
+.archset { display: grid; width: 100%; }
+.archr { grid-area: 1 / 1; display: none; flex-direction: column; gap: .1rem; }
+.archr.is-on { display: flex; }
+
+.archr__row {
+ display: grid;
+ grid-template-columns: 10ch 1fr;
+ gap: .45rem;
+ align-items: start;
+}
+
+.archr__st {
+ font-family: $font-mono;
+ font-size: clamp(.8rem, min(2.3vmin, 1.9vh), 1.15rem);
+ letter-spacing: .08em;
+ text-transform: uppercase;
+ color: $accent;
+ padding-top: .35rem;
+ text-align: right;
+}
+
+.archr__bs { display: flex; flex-wrap: wrap; gap: .3rem; }
+
+// The colour coding is only information if the room is told what it codes.
+// The key rides on the same line as the closing note — a colour code needs a
+// legend, but not a line of its own.
+.archfoot {
+ display: flex;
+ flex-wrap: wrap;
+ align-items: baseline;
+ gap: .3rem 1.4rem;
+ margin-top: .45rem;
+}
+.archkey {
+ display: inline-flex;
+ flex-wrap: wrap;
+ align-items: baseline;
+ gap: .2rem .55rem;
+ white-space: nowrap;
+ .ab { font-size: .92em; padding: .02rem .38rem; border-radius: 4px; }
+}
+
+.ab {
+ flex: 1 1 auto;
+ background: $surface;
+ border: 1px solid $border-subtle;
+ border-radius: 6px;
+ padding: .24rem .5rem;
+ font-size: clamp(.9rem, min(2.9vmin, 2.35vh), 1.4rem);
+ font-weight: 600;
+ line-height: 1.2;
+
+ small {
+ display: block;
+ font-family: $font-mono;
+ font-size: .84em;
+ font-weight: 400;
+ color: $text-dim;
+ margin-top: 0;
+ }
+
+ // Produces or checks evidence.
+ &.ev { border-color: rgba(14,116,144,.55); background: rgba(34,211,238,.20); color: $cyan; }
+ // The hazard class specific to this translation.
+ &.hz { border-color: rgba(161,98,7,.6); background: rgba(251,191,36,.30); color: $amber; }
+ &.ev small, &.hz small { color: $text-dim; }
+}
+
+// On a narrow screen (a tablet held in portrait) a long code line has nowhere
+// to go: it stays inside the block's own scroll, but the reader has to swipe a
+//
to finish a sentence. Wrap instead — landscape keeps `pre`.
+@media (max-width: 900px) {
+ .evidence { white-space: pre-wrap; word-break: break-word; }
+}
+
+// ─── Very short viewports ────────────────────────────────────────────
+// The vh cap above handles aspect; this is only a floor for laptop screens
+// short enough that even a height-proportional scale crowds the dense slides.
+@media (max-height: 620px) { .deck { --fs: .9; } }
+
+// ─── Architecture diagram ─────────────────────────────────────────────
+// A diagram is read, not spoken word-by-word, so it gets its own smaller
+// scale rather than the prose one. Evidence-producing blocks are tinted;
+// the hazard block is the one thing on the slide that is not reassuring.
+
+.arch {
+ display: grid;
+ // Six columns across 1180px left the block labels at 11px. Three columns
+ // flowing into two rows triples the width per column and lets the diagram
+ // carry readable type.
+ grid-template-columns: repeat(3, 1fr);
+ gap: .4rem .7rem;
+ width: 100%;
+ align-items: start;
+}
+
+.arch__col { display: flex; flex-direction: column; gap: .28rem; min-width: 0; }
+
+.arch__stage {
+ font-family: $font-mono;
+ font-size: clamp(.72rem, min(2vmin, 1.6vh), 1.1rem);
+ letter-spacing: .1em;
+ text-transform: uppercase;
+ color: $text-faint;
+ white-space: nowrap;
+}
+
+.arch__b {
+ background: $surface;
+ border: 1px solid $border-subtle;
+ border-radius: 6px;
+ padding: .28rem .42rem;
+ font-size: clamp(.85rem, min(2.7vmin, 2.2vh), 1.35rem);
+ font-weight: 600;
+ line-height: 1.25;
+ min-width: 0;
+
+ small {
+ display: block;
+ font-family: $font-mono;
+ font-size: .82em;
+ font-weight: 400;
+ color: $text-dim;
+ margin-top: .1rem;
+ overflow-wrap: anywhere;
+ }
+}
+
+// Teal: this block produces or checks evidence.
+.arch__b.is-ev {
+ border-color: rgba(34, 211, 238, .5);
+ background: rgba(34, 211, 238, .07);
+ color: $cyan;
+ small { color: $text-dim; }
+}
+
+// Amber: the hazard class specific to this translation.
+.arch__b.is-hz {
+ border-color: rgba(251, 191, 36, .55);
+ background: rgba(251, 191, 36, .08);
+ color: $amber;
+ small { color: $text-dim; }
+}
+
+@media (max-width: 900px) {
+ .arch { grid-template-columns: repeat(2, 1fr); }
+}
+
+// A diagram slide is read, not declaimed: it can carry a smaller heading and
+// tighter stacking than a prose slide, which buys the blocks their legibility.
+.slide:has(.archset) {
+ gap: .55rem;
+ h2 { font-size: clamp(1.5rem, min(4vmin, 3.2vh), 2.5rem); }
+}
+
+// ─── Syntax highlighting ──────────────────────────────────────────────
+// Only source blocks carry `data-lang`; captured output, hexdumps and
+// measurement tables stay plain, because colouring evidence like code
+// misrepresents what it is.
+.tok-kw { color: $purple; }
+.tok-ty { color: $cyan; }
+.tok-str { color: $green; }
+.tok-num { color: $amber; }
+.tok-fn { color: $accent; }
+.tok-com { color: $text-faint; font-style: italic; }
+
+// ─── Scope chip ───────────────────────────────────────────────────────
+// Says what a slide is ABOUT — one tool, or the whole chain. With tool names
+// running through the deck, "is this meld specifically or everything?" is a
+// question the audience should never have to hold.
+.slide__scope {
+ display: inline-block;
+ margin-left: .7rem;
+ padding: .05em .5em;
+ border: 1px solid currentColor;
+ border-radius: 99px;
+ font-size: .82em;
+ letter-spacing: .05em;
+ text-transform: none;
+ vertical-align: baseline;
+
+ &.is-one { color: $accent; } // a single tool or component
+ &.is-many { color: $cyan; } // a set, or the whole chain
+}
+
+// ─── Backup section ───────────────────────────────────────────────────
+// Slides after the close: not in the talk, reachable from the overview when a
+// question needs them. Marked so the speaker never wonders whether they have
+// run past the ending.
+.slide.is-backup {
+ border-top: 2px solid $amber;
+}
+
+.slide__act .is-backup-tag {
+ color: $amber;
+ border-color: $amber;
+}
+
+// The speaker. On the title slide it sits between the subtitle and the
+// declarations — larger than a citation, quieter than the lead.
+.slide p.slide__byline,
+.slide__byline {
+ font-family: $font-mono;
+ font-size: clamp(1.1rem, min(calc(2.8vmin * var(--fs)), calc(2.2vh * var(--fs))), 1.7rem);
+ color: $text-dim;
+ margin: 0;
+}
diff --git a/sass/main.scss b/sass/main.scss
index 191d8e9..1a5b13b 100644
--- a/sass/main.scss
+++ b/sass/main.scss
@@ -1,4 +1,5 @@
@import "variables";
+@import "fonts"; // self-hosted Atkinson — see _fonts.scss
@import "base";
@import "background";
@import "nav";
@@ -7,3 +8,4 @@
@import "pipeline";
@import "tree";
@import "responsive";
+@import "talk";
diff --git a/static/casts/dissolve.cast b/static/casts/dissolve.cast
new file mode 100644
index 0000000..990ef93
--- /dev/null
+++ b/static/casts/dissolve.cast
@@ -0,0 +1,26 @@
+{"version":3,"term":{"cols":80,"rows":24},"timestamp":1785872149,"command":"bash demo.sh","env":{"SHELL":"/bin/zsh"}}
+[0.006, "o", "\u001b[38;5;245m# five OS components, joined by the Component Model\u001b[0m\r\n\r\n"]
+[0.813, "o", "\u001b[38;5;68m$\u001b[0m wac compose fused-gustos.wac --dep ... -o os.wasm\r\n"]
+[0.532, "o", "20741 bytes\r\n"]
+[0.001, "o", "\r\n"]
+[0.612, "o", "\u001b[38;5;68m$\u001b[0m wasm-tools component wit os.wasm | grep -E 'import|export'\r\n"]
+[0.520, "o", " import gust:os/taskdisp@0.1.0;\r\n import gust:hal/mmio@0.1.0;\r\n export gust:os/time@0.1.0;\r\n export gust:os/log@0.1.0;\r\n export gust:os/spawn@0.1.0;\r\n export gust:os/exec@0.1.0;\r\n export gust:os/timer@0.1.0;\r\n"]
+[0.000, "o", "\r\n"]
+[0.614, "o", "\u001b[38;5;245m# fuse them: many linear memories become one\u001b[0m\r\n\r\n"]
+[0.816, "o", "\u001b[38;5;68m$\u001b[0m meld fuse os.wasm --memory shared -o core.wasm\r\n"]
+[0.496, "o", "Output: core.wasm (9874 bytes)\r\n Size reduction: 52.4%\r\n"]
+[0.001, "o", "\r\n"]
+[0.614, "o", "\u001b[38;5;245m# optimize, then lower the whole OS to a Cortex-M3 object\u001b[0m\r\n\r\n"]
+[0.816, "o", "\u001b[38;5;68m$\u001b[0m loom optimize --passes inline core.wasm -o opt.wasm\r\n"]
+[0.649, "o", "ok\r\n\r\n"]
+[0.612, "o", "\u001b[38;5;68m$\u001b[0m synth compile opt.wasm --target cortex-m3 --relocatable -o gustos.o\r\n"]
+[0.506, "o", "wrote gustos.o\r\n\r\n"]
+[0.614, "o", "\u001b[38;5;245m# what does the whole OS still need from the outside world?\u001b[0m\r\n\r\n"]
+[0.806, "o", "\u001b[38;5;68m$\u001b[0m arm-zephyr-eabi-nm -u gustos.o\r\n"]
+[0.496, "o", " U poll-task\r\n U read32\r\n U write32\r\n"]
+[0.000, "o", "\r\n"]
+[0.614, "o", "\u001b[38;5;68m$\u001b[0m arm-zephyr-eabi-size gustos.o\r\n"]
+[0.491, "o", " text\t data\t bss\t dec\t hex\tfilename\r\n 4812\t 0\t 0\t 4812\t 12cc\tgustos.o\r\n"]
+[0.000, "o", "\r\n"]
+[0.610, "o", "\u001b[38;5;114m# the whole OS. three symbols. zero SRAM. no engine.\u001b[0m\r\n"]
+[2.516, "x", "0"]
diff --git a/templates/base.html b/templates/base.html
index adc74ec..8e769ec 100644
--- a/templates/base.html
+++ b/templates/base.html
@@ -101,7 +101,7 @@
{# Docs nav hidden during revamp — restore when content is ready #}
{# Docs #}
Reports
- Preprints
+ PublicationsGitHubYouTube