From 25ae5d0384592110b98807b7dfc0efc6aaffa029 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Tue, 4 Aug 2026 20:58:22 +0200 Subject: [PATCH 01/56] talk: Wasm Research Day 2026 deck, presentable from a tablet MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A Zola section rendering slides through templates/talk.html — no slide framework, no CDN, self-hosted Atkinson faces, so the deck presents with the network unplugged. Nineteen slides across five acts, weighted to the factory (six slides) rather than the demo, per the "the pipeline is qualified once" framing the site already carries. Styles derive from the existing tokens in _variables.scss rather than a deck theme, so a slide looks like the site. Touch, because it is presented from an iPad: - swipe left/right, gated on the gesture being decisively horizontal (SWIPE_MIN 45px, 1.4x bias) so scrolling a long evidence block does not skip slides; disabled in overview, which is itself a scrolling grid - on-screen prev/next/overview/fullscreen at Apple's 44pt minimum target, quiet on pointer devices, always present on touch - touch-action: pan-y on slides so iOS does not claim horizontal swipes as back-navigation; manipulation on buttons to drop the double-tap zoom delay - 100dvh, since iOS Safari's 100vh hides the last line under the toolbars - safe-area insets so the chrome clears the home indicator - webkitRequestFullscreen fallback — iPad Safari has no unprefixed form - the hint line says "swipe to move" on a device with no hover One authoring trap worth recording: a blank line inside a raw-HTML block ends the block, so markdown resumed INSIDE a 
 and turned a "# correctness:"
log line into an 
. Evidence is now several 
 blocks in a .stack
rather than one with blank lines in it.

Branch only. Not for merge or deploy before the talk.

Co-Authored-By: Claude Opus 5 
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
---
 content/talks/_index.md                 |   9 +
 content/talks/wasm-research-day-2026.md | 303 ++++++++++++++++++
 sass/_talk.scss                         | 406 ++++++++++++++++++++++++
 sass/main.scss                          |   1 +
 templates/talk.html                     | 145 +++++++++
 5 files changed, 864 insertions(+)
 create mode 100644 content/talks/_index.md
 create mode 100644 content/talks/wasm-research-day-2026.md
 create mode 100644 sass/_talk.scss
 create mode 100644 templates/talk.html

diff --git a/content/talks/_index.md b/content/talks/_index.md
new file mode 100644
index 0000000..c8c6cce
--- /dev/null
+++ b/content/talks/_index.md
@@ -0,0 +1,9 @@
++++
+title = "Talks"
+sort_by = "date"
+render = false
++++
+
+Conference decks. Each one is a Zola page rendered through `talk.html` — no
+slide framework, no CDN, self-hosted fonts, so a deck presents with the network
+unplugged. Arrow keys move, `o` opens the overview, `f` goes full screen.
diff --git a/content/talks/wasm-research-day-2026.md b/content/talks/wasm-research-day-2026.md
new file mode 100644
index 0000000..0859a7c
--- /dev/null
+++ b/content/talks/wasm-research-day-2026.md
@@ -0,0 +1,303 @@
++++
+title = "The OS as components — and the factory that lowers it"
+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
+template = "talk.html"
+
+[extra]
+event = "Wasm Research Day 2026"
+slot = "30 minutes, remote"
++++
+
+

+  
Wasm Research Day 2026 · 30 minutes

+  
The OS as components,
and the factory that lowers it

+  
Most embedded stacks make the operating system platform-specific
+  and hope the application is portable. We are inverting that.

+  
pulseengine.eu · every number on these slides says where it came from

+

+
+

+  
Act I · the inversion

+  
Portability is usually asked of the wrong layer

+  

+    

+      
the usual arrangement

+      
The OS is written for the chip. The application is written against the OS
+      and hoped to be portable. Every new board re-opens the OS.

+    

+    

+      
what we are trying

+      
The OS itself is WebAssembly components. The Component Model is the
+      integration step — between OS components, between the OS and its drivers,
+      and between the OS and the tenants above it.

+    

+  

+

+
+

+  
Act I · the inversion

+  
The car and the tires

+  
Think of the OS and everything above it as the car, and the
+  handful of native functions that actually touch the hardware as the tires.

+  
For new terrain — another chip, another board — you change the
+  tires, not the car.

+  
This talk spends most of its time on the factory that
+  builds the car, because that is the part that has to be qualified once.

+

+
+

+  
Act II · the car

+  
Two seams, and everything hangs off them

+  

+    

+      
gust:os — what tenants see

+      
time · log · spawn
+exec · timer · taskdisp
+channel · io

+    

+    

+      
gust:hal — what touches metal

+      
mmio · irq · gpio
+spi · timer · uart · dma

+    

+  

+  
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 car

+  
Integration step, not a build step

+  

+    
waccompose the components into one

+    
meldfuse — one shared memory

+    
loomoptimize, and emit what it proved

+    
synthlower to ARM / RISC-V

+    
.oone relocatable object · no runtime on the device

+  

+  
Wasm is where the pieces are joined and checked. It is not present at run
+  time — there is no interpreter, no JIT, and no engine resident on the chip.

+

+
+

+  
Act II · the car

+  
Three dies, one session

+  
captured 2026-08-04, all three probes attached at once

+  

+    
Cortex-M4 · NUCLEO-G474RE
+gust-wdg-silicon OK: IWDG watchdog reset CONFIRMED on real STM32G474
+silicon (RCC_CSR=0x34000000, IWDGRSTF=1)

+    
Cortex-M3 · STM32F100 VLDISCOVERY — the same .o, a second die
+gust-wdg-silicon OK: IWDG watchdog reset CONFIRMED on real STM32F100
+silicon (RCC_CSR=0x34000000, IWDGRSTF=1)

+    
RISC-V · ESP32-C3 rev v0.4
+correctness: IDENTICAL ok over [0,2047]
+gust_mix_native     271 milliticks/call
+gust_mix_dissolved  499 milliticks/call
+ratio_x1000        1839   (mismatch=0)

+  

+  
The 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 stays a source-level proof.

+

+
+

+  
Act II · the car

+  
The tires are smaller than you would guess

+  

+    
seamA whole STM32 USART driver, dissolved326 B flash · 0 SRAM

+    
seamIts entire trusted surface3 relocations

+    
seamDMA modelled as an ownership round-trip218 B · 6 Kani proofs

+  

+  
The three relocations are mmio_read32, mmio_write32,
+  irq_poll. Everything above them — the protocol, the state machine,
+  the error handling — is wasm that got lowered.

+

+
+

+  
Act III · the tires

+  
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 IV · the factory

+  
The pipeline is qualified once; every product
+  that uses it inherits that qualification.

+  
— our own words, from a post two years before this talk

+  
This is why the factory matters more than the car. A car you qualify once is
+  one car. A factory you qualify once is every car it will ever build.

+

+
+

+  
Act IV · the factory

+  
Six faces, not four tools

+  

+    

+      
architect
spar — AADL / SysML. The WIT is generated from the model, not hand-written.

+    

+    

+      
build
meld fuse · loom optimize · synth lower · sigil attesting across all of it.

+    

+    

+      
verify
witness MC/DC on the shipped wasm · scry abstract interpretation · Verus, Rocq, Lean, Kani as build rules.

+    

+    

+      
trace
rivet — typed requirements, decisions and tests. Broken links fail the build.

+    

+    

+      
run
kiln runtime · gale verified kernel primitives · the applications above them.

+    

+    

+      
agent
The loop that files findings between repos — and the governance that keeps 30+ repos to the same rules.

+    

+  

+

+
+

+  
Act IV · the factory

+  
No stage trusts the one above it

+  
When loom proves a value range, it does not just use it and
+  discard it. It writes it into a custom section — wsc.facts — keyed
+  to values, not positions, so renumbering cannot silently re-point a fact.

+  
synth never re-derives that fact and never takes it on faith. It
+  proves its own specialization correct given the fact, per site, and
+  emits a certificate.

+  

+    
measuredA bounds-guard sequence, with the fact forwarded232 → 104 B

+  

+

+
+

+  
Act IV · the factory

+  
Faster because it is proven

+  

+    
baselinenative LLVM, full clamp0.50 cyc/call · 1.00×

+    
todaydissolved, as shipped0.83 cyc/call · 1.65×

+    
measured floorclamp elided because a proof allows it0.23 cyc/call · 0.45×

+  

+  
Not a model — a measured floor, soundness-gated. The elision is only legal
+  because something upstream proved the bound. A compiler with no
+  verifier in its pipeline structurally cannot reach it.

+

+
+

+  
Act IV · the factory

+  
Qualify the checker, not the prover

+  
Certification asks: why do you believe the solver? "Qualify Z3" is not a
+  tractable answer.

+  
So the solver stays untrusted and emits a certificate. Only a small,
+  dependency-free checker is trusted — and that checker's soundness is
+  machine-checked in Lean 4, with no sorry anywhere in its kernel.

+  

+    
shippedbit-vector obligations re-discharged with re-checkable certificates62 / 62

+  

+  
This turns unchecked-solver evidence into the argument
+  a verified compiler makes: don't trust the tool, check its output.

+

+
+

+  
Act IV · the factory

+  
Every one of these gates was green for the wrong reason

+  

+    
scrya proof that never ran — the theorem was false when it did 

+    
synthtwo validators, same direction, same blind spot 

+    
looma gate with passing tests and zero callers 

+    
meldverified by a test on a path the shipped code didn't take 

+    
galea count over modules that cannot see instances 

+  

+  
The failure produced the same observable as
+  success.

+  
The remedy is not more gates. It is that every check must be able to go red
+  for a reason you can state in advance.

+

+
+

+  
Act V · what is missing

+  
What componentizing actually costs

+  
driver object .text, core module → component

+  
gpio    502 → 1196 B      spi    454 → 1244 B
+timer   204 →  828 B      wdg    638 → 1718 B
+.data / .bss, every one of them       0 → 0

+  
Roughly +700 B fixed per driver for canonical-ABI glue
+  — a constant, not a proportion. On a chip with 8 KB of SRAM that is a real
+  number, and it is filed upstream rather than absorbed quietly.

+

+
+

+  
Act V · what is missing

+  
Where the verification story actually stands

+  

+    
shippingTheorem proving · SMT contracts · bounded model checking · translation validation 

+    
partialRefinement to Lean · mutation testing · abstract interpretation 

+    
not yetAn authority audit. We have not been audited. 

+  

+  
Proofs run on a verification schedule, not on every commit. Our own docs say
+  this out loud: closer to "well-specified and comprehensively tested with
+  local formal verification" than "continuously formally verified."

+

+
+

+  
Act V · what is missing

+  
Two things building this talk taught us

+  

+    

+      
the runner broke on success

+      
Plugging in the third board made the first one unreachable — two probes,
+      an interactive prompt, and a harness with no terminal. The all-three-at-once
+      case was exactly the case nothing had run.

+    

+    

+      
a reproducible number that isn't

+      
The RISC-V figure is recorded with a byte-reproducible command. The wasm
+      input to that command is not in the repository — 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 missing

+  
Before the rest of the vision holds

+  
    
+    
  • Multi-tenant isolation on real MPU regions — modelled, not yet enforced on silicon.
    • 
+    
  • Drivers beyond the ones that port cleanly. Register maps differ; a verified
+    state machine for one bus does not transfer to the next revision of that bus —
+    it needs a fresh proof, not a port.
    • 
+    
  • 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.
    • 
+  

+

+
+

+  
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.

+  
pulseengine.eu · every tool named here is open source

+

diff --git a/sass/_talk.scss b/sass/_talk.scss
new file mode 100644
index 0000000..71d3616
--- /dev/null
+++ b/sass/_talk.scss
@@ -0,0 +1,406 @@
+// 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;
+
+  // 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.2rem, 5.6vmin, 4rem);
+  line-height: 1.1;
+  font-weight: 700;
+  letter-spacing: -0.02em;
+  text-wrap: balance;
+  margin: 0;
+}
+
+.slide h2 {
+  font-size: clamp(1.6rem, 3.9vmin, 2.6rem);
+  line-height: 1.15;
+  font-weight: 600;
+  letter-spacing: -0.015em;
+  text-wrap: balance;
+  margin: 0;
+}
+
+.slide p,
+.slide li {
+  font-size: clamp(1rem, 2.05vmin, 1.4rem);
+  line-height: 1.55;
+  max-width: 46ch;
+  margin: 0;
+}
+
+.slide ul { display: flex; flex-direction: column; gap: .6rem; 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__act {
+  font-family: $font-mono;
+  font-size: clamp(.7rem, 1.35vmin, .88rem);
+  letter-spacing: .14em;
+  text-transform: uppercase;
+  color: $text-faint;
+  margin: 0;
+}
+
+.slide__lead {
+  font-size: clamp(1.15rem, 2.5vmin, 1.65rem) !important;
+  color: $text-dim;
+  max-width: 40ch;
+}
+
+// A pull-quote slide: the project's own words, attributed.
+.slide__quote {
+  font-size: clamp(1.5rem, 3.6vmin, 2.5rem);
+  line-height: 1.3;
+  font-weight: 500;
+  max-width: 26ch;
+  text-wrap: balance;
+  border-left: 3px solid $accent;
+  padding-left: 1.2rem;
+}
+
+.slide__cite {
+  font-family: $font-mono;
+  font-size: clamp(.72rem, 1.5vmin, .95rem);
+  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(.62rem, 1.42vmin, .95rem);
+  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%;
+}
+
+.evidence__label {
+  font-family: $font-mono;
+  font-size: clamp(.66rem, 1.32vmin, .84rem);
+  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; }
+
+// ─── 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: 60ch;
+}
+
+.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(.8rem, 1.75vmin, 1.05rem);
+}
+
+.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;
+}
+
+// ─── Stage chain (the pipeline, as a row of stages) ───────────────────
+
+.chain {
+  display: flex;
+  flex-wrap: wrap;
+  align-items: stretch;
+  gap: .5rem;
+  width: 100%;
+}
+
+.chain__stage {
+  flex: 1 1 8rem;
+  min-width: 7rem;
+  background: $surface;
+  border: 1px solid $border-subtle;
+  border-radius: 10px;
+  padding: .75rem .85rem;
+  display: flex;
+  flex-direction: column;
+  gap: .3rem;
+}
+
+.chain__name {
+  font-family: $font-mono;
+  font-size: clamp(.85rem, 1.9vmin, 1.15rem);
+  font-weight: 600;
+  color: $accent;
+}
+
+.chain__what {
+  font-size: clamp(.7rem, 1.45vmin, .92rem);
+  color: $text-dim;
+  line-height: 1.35;
+}
+
+// ─── 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(.72rem, 1.45vmin, .9rem);
+  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; }
+}
+
+// On a pointer device the deck is driven from the keyboard; keep the buttons
+// available but quiet until approached.
+@media (hover: hover) {
+  .deck__nav { opacity: .35; 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;
+  }
+
+  .slide {
+    grid-area: auto;
+    visibility: visible;
+    opacity: .55;
+    aspect-ratio: 16 / 10;
+    padding: .8rem;
+    border: 1px solid $border-subtle;
+    border-radius: 8px;
+    background: $bg-subtle;
+    cursor: pointer;
+    overflow: hidden;
+    gap: .35rem;
+    transition: opacity .15s ease, border-color .15s ease;
+
+    &.is-current { opacity: 1; border-color: $accent; }
+    &:hover { opacity: .9; }
+
+    // Shrink everything so a whole slide fits the thumbnail.
+    h1 { font-size: 1.05rem; }
+    h2 { font-size: .88rem; }
+    p, li { font-size: .62rem; max-width: none; }
+    .slide__quote { font-size: .8rem; padding-left: .5rem; max-width: none; }
+    .slide__lead { font-size: .68rem !important; }
+    .evidence { font-size: .5rem; padding: .35rem .45rem; }
+    .ledger__row { padding: .2rem .35rem; font-size: .55rem; gap: .35rem; }
+    .chain__stage { padding: .3rem .35rem; }
+    .chain__name { font-size: .6rem; }
+    .chain__what { font-size: .48rem; }
+  }
+}
+
+// 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; }
+}
diff --git a/sass/main.scss b/sass/main.scss
index 191d8e9..b7a9f40 100644
--- a/sass/main.scss
+++ b/sass/main.scss
@@ -7,3 +7,4 @@
 @import "pipeline";
 @import "tree";
 @import "responsive";
+@import "talk";
diff --git a/templates/talk.html b/templates/talk.html
new file mode 100644
index 0000000..5834ae5
--- /dev/null
+++ b/templates/talk.html
@@ -0,0 +1,145 @@
+{# Slide deck. Deliberately does NOT extend base.html: a deck wants the whole
+   viewport with no nav, no footer, no background canvas. It reuses main.css
+   so the tokens, fonts and colours are the site's. #}
+
+
+
+  
+  {# viewport-fit=cover so the deck reaches under an iPad's rounded corners;
+     the safe-area insets in _talk.scss keep the chrome clear of them. #}
+  
+  
+  {{ page.title }}
+  
+  
+  
+
+
+  

+    

+      {{ page.content | safe }}
+    

+    

+    
← → move · o overview · f full screen

+    

+
+    {# On-screen controls. Present for everyone, but they are the only way to
+       drive the deck from a tablet — a keyboard hint is useless there. Sized to
+       Apple's 44pt minimum touch target. #}
+    
+  

+
+
+
+

From 1d6a24ff10c3e4c5329b2f0f8b902b37199f6dd0 Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier 
Date: Tue, 4 Aug 2026 21:07:02 +0200
Subject: [PATCH 02/56] talk: fix the overview, add the code, and calibrate to
 the published slot
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Overview was unusable on a tablet. Diagnosed rather than guessed: at 1180px
every one of the thumbnails overflowed its clipped box by up to 2x and got cut
mid-line, which is what "overlapping" looked like. Hand-shrinking each element
type was never going to hold as slides were added. Thumbnails are now title
cards — act label, heading, number, everything else suppressed — which cannot
spill, stay legible at any width, and are more useful mid-talk anyway. Verified
at iPad landscape: 0 spilled, 0 overlapping pairs, no slide needs scrolling,
no evidence block overflows horizontally.

The pipeline slide answered "what are the stages" but not "what goes in and
what comes out", which is what the tool sites do well. Rebuilt as a flow with
both sides named per stage, down to `ld` taking the .o plus three native
functions and emitting firmware with no engine in it.

Added the code that was missing, all of it lifted from the repo rather than
written to look plausible: the real mmio interface and wdg-driver world, the
actual compose/fuse/optimize/compile commands, the wdg contract that offers no
stop next to the Kani property that proves no escape from Running, and
shim-mmio.js beside the silicon read32 so the substitution is on one slide.

Calibrated against the published schedule for the event:
- the slot is 25+5, not 30 — merged two overlapping slide pairs, 23 -> 21
- the title is already published; the deck now uses it verbatim
- added an opening slide crediting the four adjacent talks (one of them two
  hours earlier the same day) so the work positions against them instead of
  appearing to ignore them
- moved the verification-scope slide out of the closing act into the factory
  act: it and "no runtime resident" are the two claims this venue has not
  heard, and both now land before minute 20

Co-Authored-By: Claude Opus 5 
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
---
 content/talks/wasm-research-day-2026.md | 189 +++++++++++++++++-------
 sass/_talk.scss                         | 105 ++++++++-----
 2 files changed, 208 insertions(+), 86 deletions(-)

diff --git a/content/talks/wasm-research-day-2026.md b/content/talks/wasm-research-day-2026.md
index 0859a7c..6400a62 100644
--- a/content/talks/wasm-research-day-2026.md
+++ b/content/talks/wasm-research-day-2026.md
@@ -1,22 +1,36 @@
 +++
-title = "The OS as components — and the factory that lowers it"
+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
 template = "talk.html"
 
 [extra]
 event = "Wasm Research Day 2026"
-slot = "30 minutes, remote"
+slot = "25 + 5, remote"
 +++
 
 

-  
Wasm Research Day 2026 · 30 minutes

-  
The OS as components,
and the factory that lowers it

-  
Most embedded stacks make the operating system platform-specific
-  and hope the application is portable. We are inverting that.

+  
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.

   
pulseengine.eu · every number on these slides says where it came from

 

 
+

+  
Act I · the inversion

+  
What this room has already established

+  

+    
2022Fixpoint: Computation-Centric Networking — wasm lowered ahead of time to native, invoked without an engineserver, x86-64

+    
2023Bringing orchestration to the edge with the WebAssembly Component Model — pluggable HALs via the Component Modelpreliminary

+    
2025WASI performance on IoT and embedded — the overhead of a runtime on a constrained deviceruntime present

+    
todayWasmBounds — eliminating bounds checks by abstract interpretationtwo hours ago

+  

+  
Each of these is one ingredient. This talk is what happens
+  when you need all four at once — on a chip where the runtime the third
+  one measures does not fit at all.

+

+
 

   
Act I · the inversion

   
Portability is usually asked of the wrong layer

@@ -33,17 +47,9 @@ slot = "30 minutes, remote"
       and between the OS and the tenants above it.

     
   
-

-
-

-  
Act I · the inversion

-  
The car and the tires

-  
Think of the OS and everything above it as the car, and the
-  handful of native functions that actually touch the hardware as the tires.

-  
For new terrain — another chip, another board — you change the
-  tires, not the car.

-  
This talk spends most of its time on the factory that
-  builds the car, because that is the part that has to be qualified once.

+  
The OS and everything above it is the car. The handful of native functions
+  that actually touch the hardware are the tires. For new terrain — another chip,
+  another board — you change the tires, not the car.

 

 
 

@@ -70,15 +76,86 @@ spi · timer · uart · dma

 

   
Act II · the car

   
Integration step, not a build step

-  

-    
waccompose the components into one

-    
meldfuse — one shared memory

-    
loomoptimize, and emit what it proved

-    
synthlower to ARM / RISC-V

-    
.oone relocatable object · no runtime on the device

+  

+    

+      wac compose
+      5 components
+      →
+      1 component
exports gust:os · imports gust:hal
+    

+    

+      meld fuse
+      1 component
5 linear memories
+      →
+      1 core module
one shared memory
+    

+    

+      loom optimize
+      core module
+      →
+      core module + wsc.facts
what it proved, forwarded
+    

+    

+      synth compile
+      module + facts
+      →
+      one relocatable .o + certificates
+    

+    

+      ld
+      .o + 3 native functions
+      →
+      firmware
no engine, no interpreter, no JIT
+    

   

-  
Wasm is where the pieces are joined and checked. It is not present at run
-  time — there is no interpreter, no JIT, and no engine resident on the chip.

+

+
+

+  
Act II · the car

+  
The seam, as it is actually written

+  

+    

+      
wit/gust-hal.wit

+      
interface mmio {
+    read32:  func(addr: u32) -> u32;
+    write32: func(addr: u32, val: u32);
+    read8:   func(addr: u32) -> u8;
+    write8:  func(addr: u32, val: u8);
+}
+world wdg-driver { import mmio; export wdg; }

+    

+    

+      
and the composition

+      
wac compose fused-gustos.wac -o fused.wasm
+meld fuse --memory shared
+loom optimize --passes inline
+synth compile --target cortex-m3 \
+      --all-exports --relocatable

+    

+  

+  
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 car

+  
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:

+  
interface wdg {
+    unlock · configure · lock · start · refresh · is-running
+    — there is no stop, and no disable
+}

+  
and the FSM proves the absence, rather than relying on it

+  
fn p2_cannot_un_start() {
+    let w = Iwdg { phase: Running, .. };
+    if let Ok(n) = refresh(w) { assert_eq!(n.phase, Running); }
+    assert!(unlock(w).is_err());        // no escape from Running
+}

+  
The contract itself cannot express the one transition the
+  proof forbids. That is the argument for putting the seam in a type
+  system rather than in a comment.

 

 
 

@@ -103,19 +180,6 @@ ratio_x1000        1839   (mismatch=0)

   un-start. That stays a source-level proof.

 
 
-

-  
Act II · the car

-  
The tires are smaller than you would guess

-  

-    
seamA whole STM32 USART driver, dissolved326 B flash · 0 SRAM

-    
seamIts entire trusted surface3 relocations

-    
seamDMA modelled as an ownership round-trip218 B · 6 Kani proofs

-  

-  
The three relocations are mmio_read32, mmio_write32,
-  irq_poll. Everything above them — the protocol, the state machine,
-  the error handling — is wasm that got lowered.

-

-
 

   
Act III · the tires

   
Same bytes. Three different answerers.

@@ -142,6 +206,28 @@ ratio_x1000        1839   (mismatch=0)
per target.

+
+

Act III · the tires

+

The whole of a tire

+

web/shim-mmio.js — what a browser tab supplies

+ 
const REGS = new Uint32Array(64);
+const TIM2_CNT = 0x40000024;   // the one clock register the OS reads
+export function read32(addr) {
+  const a = addr >>> 0;
+  return a === TIM2_CNT ? clock : REGS[(a >>> 2) & 63];
+}
+

on silicon — same import, answered by the bus

+ 
#[no_mangle] extern "C" fn read32(addr: u32) -> u32 {
+    unsafe { core::ptr::read_volatile(addr as *const u32) }
+}
+

Nothing else about the component changes. That substitution + is the entire thesis — and it is small enough to read on one slide.

+
+
seamA whole STM32 USART driver, dissolved — trusted surface: read32, write32, irq_poll326 B · 0 SRAM · 3 relocs
+
seamDMA, modelled as an ownership round-trip218 B · 6 Kani proofs
+
+
+

Act IV · the factory

The pipeline is qualified once; every product @@ -218,6 +304,20 @@ ratio_x1000 1839 (mismatch=0) a verified compiler makes: don't trust the tool, check its output.

+
+

Act IV · the factory

+

Exactly how far this goes — and no further

+
+
shippingTheorem proving · SMT contracts · bounded model checking · translation validation 
+
partialRefinement to Lean · mutation testing · abstract interpretation 
+
not yetAn authority audit. We have not been audited. 
+
+

Bounded model checking is bounded. Proofs run on a verification schedule, + not on every commit. Our own docs say it out loud: closer to "well-specified + and comprehensively tested with local formal verification" than + "continuously formally verified."

+
+

Act IV · the factory

Every one of these gates was green for the wrong reason

@@ -246,19 +346,6 @@ timer 204 → 828 B wdg 638 → 1718 B number, and it is filed upstream rather than absorbed quietly.

-
-

Act V · what is missing

-

Where the verification story actually stands

-
-
shippingTheorem proving · SMT contracts · bounded model checking · translation validation 
-
partialRefinement to Lean · mutation testing · abstract interpretation 
-
not yetAn authority audit. We have not been audited. 
-
-

Proofs run on a verification schedule, not on every commit. Our own docs say - this out loud: closer to "well-specified and comprehensively tested with - local formal verification" than "continuously formally verified."

-
-

Act V · what is missing

Two things building this talk taught us

diff --git a/sass/_talk.scss b/sass/_talk.scss index 71d3616..c0599fe 100644 --- a/sass/_talk.scss +++ b/sass/_talk.scss @@ -211,41 +211,58 @@ color: $text; } -// ─── Stage chain (the pipeline, as a row of stages) ─────────────────── +// ─── 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. -.chain { - display: flex; - flex-wrap: wrap; - align-items: stretch; - gap: .5rem; +.flow { + display: grid; + gap: .4rem; width: 100%; } -.chain__stage { - flex: 1 1 8rem; - min-width: 7rem; +.flow__row { + display: grid; + grid-template-columns: minmax(6rem, auto) 1fr auto 1fr; + align-items: center; + gap: .5rem .9rem; + padding: .5rem .8rem; background: $surface; border: 1px solid $border-subtle; - border-radius: 10px; - padding: .75rem .85rem; - display: flex; - flex-direction: column; - gap: .3rem; + border-radius: 8px; } -.chain__name { +.flow__stage { font-family: $font-mono; - font-size: clamp(.85rem, 1.9vmin, 1.15rem); + font-size: clamp(.75rem, 1.6vmin, 1rem); font-weight: 600; color: $accent; } -.chain__what { - font-size: clamp(.7rem, 1.45vmin, .92rem); - color: $text-dim; +.flow__in, +.flow__out { + font-family: $font-mono; + font-size: clamp(.66rem, 1.42vmin, .9rem); 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(.8rem, 1.6vmin, 1rem); +} + +// 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); } +} + // ─── Two-column split ───────────────────────────────────────────────── .split { @@ -363,34 +380,52 @@ 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: .55; + opacity: .6; aspect-ratio: 16 / 10; - padding: .8rem; + justify-content: flex-start; + padding: .7rem .8rem; border: 1px solid $border-subtle; border-radius: 8px; background: $bg-subtle; cursor: pointer; overflow: hidden; - gap: .35rem; + gap: .3rem; transition: opacity .15s ease, border-color .15s ease; &.is-current { opacity: 1; border-color: $accent; } - &:hover { opacity: .9; } - - // Shrink everything so a whole slide fits the thumbnail. - h1 { font-size: 1.05rem; } - h2 { font-size: .88rem; } - p, li { font-size: .62rem; max-width: none; } - .slide__quote { font-size: .8rem; padding-left: .5rem; max-width: none; } - .slide__lead { font-size: .68rem !important; } - .evidence { font-size: .5rem; padding: .35rem .45rem; } - .ledger__row { padding: .2rem .35rem; font-size: .55rem; gap: .35rem; } - .chain__stage { padding: .3rem .35rem; } - .chain__name { font-size: .6rem; } - .chain__what { font-size: .48rem; } + &: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; } } } From cba69de7f02755c3494d2700caca5695f98ae2c6 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Tue, 4 Aug 2026 21:22:51 +0200 Subject: [PATCH 03/56] =?UTF-8?q?talk:=20fix=20the=20type=20scale=20?= =?UTF-8?q?=E2=80=94=20it=20was=20sized=20like=20a=20web=20page,=20not=20a?= =?UTF-8?q?=20slide?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Measured rather than eyeballed. At iPad landscape (1180x820) the deck was rendering body text at 16.8px and CODE BLOCKS AT 11.6px. That is document sizing on a slide, and unreadable over a shared screen — which for a remote talk gets downscaled again on the way to the audience. The cause was mine: every clamp()'s MAXIMUM was set at web-body values (1.4rem body, .95rem code), so the text could never grow past ~22px/~15px no matter how large the display. Raised all fourteen steps of the scale. before -> after, at 1180x820 h1 46 -> 52 lead 20 -> 29 body 17 -> 25 ledger 14 -> 18 code 12 -> 18 flow 12 -> 16 Also fixes a specificity bug the measurement exposed: `.slide p` (0,2,0) beat `.slide__act` and `.slide__cite` (0,1,0), so the act eyebrow and every citation line had been rendering at FULL BODY SIZE from the first commit — 25px where they should be 15. That is most of why the slides read as cluttered. Qualified all three as `.slide p.`. Bigger type means less fits, and that was paid in words rather than by shrinking back: trimmed the prior-art rows, compressed the three-dies logs to two lines per die, moved the DMA figure off the tire slide, and folded a duplicated caption into the honesty note. Verified at 1180x820: 0 slides overflow, 0 code blocks scroll sideways, 0 overview thumbnails spill. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo --- content/talks/wasm-research-day-2026.md | 43 ++++++++++++------------- sass/_talk.scss | 36 +++++++++++++-------- 2 files changed, 42 insertions(+), 37 deletions(-) diff --git a/content/talks/wasm-research-day-2026.md b/content/talks/wasm-research-day-2026.md index 6400a62..96a1426 100644 --- a/content/talks/wasm-research-day-2026.md +++ b/content/talks/wasm-research-day-2026.md @@ -21,14 +21,13 @@ slot = "25 + 5, remote"

Act I · the inversion

What this room has already established

-
2022Fixpoint: Computation-Centric Networking — wasm lowered ahead of time to native, invoked without an engineserver, x86-64
-
2023Bringing orchestration to the edge with the WebAssembly Component Model — pluggable HALs via the Component Modelpreliminary
-
2025WASI performance on IoT and embedded — the overhead of a runtime on a constrained deviceruntime present
-
todayWasmBounds — eliminating bounds checks by abstract interpretationtwo hours ago
+
2022Fixpoint — wasm lowered ahead of time, invoked with no engineserver, x86-64
+
2023Orchestration at the edge — pluggable HALs via the Component Modelpreliminary
+
2025WASI performance on IoT and embedded — a runtime's overhead on a small deviceruntime present
+
todayWasmBounds — eliding bounds checks by abstract interpretationtwo hours ago
-

Each of these is one ingredient. This talk is what happens - when you need all four at once — on a chip where the runtime the third - one measures does not fit at all.

+

Each is one ingredient. This talk needs all four at + once — on a chip where the runtime the third one measures does not fit.

@@ -50,6 +49,8 @@ slot = "25 + 5, remote"

The OS and everything above it is the car. The handful of native functions that actually touch the hardware are the tires. For new terrain — another chip, another board — you change the tires, not the car.

+

Declaring the bias: I work in automotive, so to me + everything is a car. The substrate is not — which is the next slide.

@@ -161,23 +162,20 @@ synth compile --target cortex-m3 \

Act II · the car

Three dies, one session

-

captured 2026-08-04, all three probes attached at once

Cortex-M4 · NUCLEO-G474RE
-gust-wdg-silicon OK: IWDG watchdog reset CONFIRMED on real STM32G474
-silicon (RCC_CSR=0x34000000, IWDGRSTF=1)
- 
Cortex-M3 · STM32F100 VLDISCOVERY — the same .o, a second die
-gust-wdg-silicon OK: IWDG watchdog reset CONFIRMED on real STM32F100
-silicon (RCC_CSR=0x34000000, IWDGRSTF=1)
+IWDG reset CONFIRMED on real STM32G474 +RCC_CSR 0x14000000 → 0x34000000 IWDGRSTF=1 + 
Cortex-M3 · STM32F100 — the same .o, a second die
+IWDG reset CONFIRMED on real STM32F100
+RCC_CSR 0x14000000 → 0x34000000   IWDGRSTF=1
RISC-V · ESP32-C3 rev v0.4
-correctness: IDENTICAL ok over [0,2047]
-gust_mix_native     271 milliticks/call
-gust_mix_dissolved  499 milliticks/call
-ratio_x1000        1839   (mismatch=0)
+native 271 dissolved 499 milliticks/call ratio 1.839× +correctness IDENTICAL over [0,2047] mismatch=0
-

The 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 stays a source-level proof.

+

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.

@@ -221,10 +219,9 @@ export function read32(addr) { unsafe { core::ptr::read_volatile(addr as *const u32) } }

Nothing else about the component changes. That substitution - is the entire thesis — and it is small enough to read on one slide.

+ is the entire thesis.

-
seamA whole STM32 USART driver, dissolved — trusted surface: read32, write32, irq_poll326 B · 0 SRAM · 3 relocs
-
seamDMA, modelled as an ownership round-trip218 B · 6 Kani proofs
+
seamA whole STM32 USART driver, dissolved326 B · 0 SRAM · 3 relocs
diff --git a/sass/_talk.scss b/sass/_talk.scss index c0599fe..4e55e28 100644 --- a/sass/_talk.scss +++ b/sass/_talk.scss @@ -69,7 +69,7 @@ // Sized in vmin so a slide reads the same projected, shared, or in a tab. .slide h1 { - font-size: clamp(2.2rem, 5.6vmin, 4rem); + font-size: clamp(2.5rem, 6.4vmin, 4.8rem); line-height: 1.1; font-weight: 700; letter-spacing: -0.02em; @@ -78,7 +78,7 @@ } .slide h2 { - font-size: clamp(1.6rem, 3.9vmin, 2.6rem); + font-size: clamp(1.85rem, 4.5vmin, 3.2rem); line-height: 1.15; font-weight: 600; letter-spacing: -0.015em; @@ -88,7 +88,7 @@ .slide p, .slide li { - font-size: clamp(1rem, 2.05vmin, 1.4rem); + font-size: clamp(1.2rem, 3vmin, 2.1rem); line-height: 1.55; max-width: 46ch; margin: 0; @@ -98,9 +98,10 @@ // 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(.7rem, 1.35vmin, .88rem); + font-size: clamp(.85rem, 1.8vmin, 1.15rem); letter-spacing: .14em; text-transform: uppercase; color: $text-faint; @@ -108,14 +109,14 @@ } .slide__lead { - font-size: clamp(1.15rem, 2.5vmin, 1.65rem) !important; + font-size: clamp(1.4rem, 3.5vmin, 2.5rem) !important; color: $text-dim; max-width: 40ch; } // A pull-quote slide: the project's own words, attributed. .slide__quote { - font-size: clamp(1.5rem, 3.6vmin, 2.5rem); + font-size: clamp(1.8rem, 4.3vmin, 3.1rem); line-height: 1.3; font-weight: 500; max-width: 26ch; @@ -124,9 +125,10 @@ padding-left: 1.2rem; } +.slide p.slide__cite, .slide__cite { font-family: $font-mono; - font-size: clamp(.72rem, 1.5vmin, .95rem); + font-size: clamp(.9rem, 1.95vmin, 1.25rem); color: $text-faint; } @@ -136,7 +138,7 @@ .evidence { font-family: $font-mono; - font-size: clamp(.62rem, 1.42vmin, .95rem); + font-size: clamp(.95rem, 2.25vmin, 1.5rem); line-height: 1.5; background: $bg-subtle; border: 1px solid $border-subtle; @@ -158,9 +160,10 @@ width: 100%; } +.slide p.evidence__label, .evidence__label { font-family: $font-mono; - font-size: clamp(.66rem, 1.32vmin, .84rem); + font-size: clamp(.8rem, 1.7vmin, 1.05rem); letter-spacing: .06em; text-transform: uppercase; color: $text-faint; @@ -193,7 +196,7 @@ background: $surface; border: 1px solid $border-subtle; border-radius: 8px; - font-size: clamp(.8rem, 1.75vmin, 1.05rem); + font-size: clamp(.98rem, 2.25vmin, 1.45rem); } .ledger__tag { @@ -234,7 +237,7 @@ .flow__stage { font-family: $font-mono; - font-size: clamp(.75rem, 1.6vmin, 1rem); + font-size: clamp(1rem, 2.2vmin, 1.4rem); font-weight: 600; color: $accent; } @@ -242,7 +245,7 @@ .flow__in, .flow__out { font-family: $font-mono; - font-size: clamp(.66rem, 1.42vmin, .9rem); + font-size: clamp(.88rem, 2vmin, 1.25rem); line-height: 1.35; } @@ -252,7 +255,7 @@ .flow__arrow { font-family: $font-mono; color: $text-faint; - font-size: clamp(.8rem, 1.6vmin, 1rem); + font-size: clamp(1rem, 2.1vmin, 1.3rem); } // Stack the row on a narrow screen rather than crushing four columns. @@ -263,6 +266,11 @@ .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(.85rem, 1.95vmin, 1.25rem); padding: .7rem .85rem; } + // ─── Two-column split ───────────────────────────────────────────────── .split { @@ -274,7 +282,7 @@ .split__col h3 { font-family: $font-mono; - font-size: clamp(.72rem, 1.45vmin, .9rem); + font-size: clamp(.88rem, 1.85vmin, 1.15rem); letter-spacing: .1em; text-transform: uppercase; color: $text-faint; From 4697d0f5bc0bd5e4bcd7062950ab004b8670ef98 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Tue, 4 Aug 2026 21:32:46 +0200 Subject: [PATCH 04/56] talk: presentation-sized type, and slide 5 runs the real dissolve MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit TYPE. Measured again after the first pass was still too small. Body text on a slide should be ~4% of slide height; mine was 3%. Raised sixteen steps of the scale — at 1180x820 body 25 -> 34px, code 18 -> 26px, h1 52 -> 69px — and paid for it in words rather than by shrinking back: trimmed prose on ten slides, cut the six-faces paragraphs to phrases, compressed the three-dies logs to two lines per die, dropped a redundant closing line on the gates slide. RECORDING. Slide 5 now has a "run it" button that replays a real asciinema capture of the dissolve: wasm-tools shows the component's WIT, loom optimizes, synth lowers to a Cortex-M3 object, then nm and size answer the slide's claim with `U read32 / U write32` and `text 1726 data 0 bss 0`. Recorded by actually running it — the wdg-thin driver had to be rebuilt first because the checked-in target/ wasm was a stale pre-componentization build importing env::mmio_read32. Written as a ~90-line player rather than pulling in a library: the capture contains only SGR colour escapes and newlines (verified — no cursor motion), so append-only rendering is faithful, not an approximation. Text stays selectable and crisp at any projection size, the file is 1.7 KB, casts are fetched once at load so clicking mid-talk never touches the network, and a missing file disables the button instead of breaking the slide. Two bugs fixed on the way: - the terminal 
 had min-height:0 inside a flex column, so siblings
  squashed it to a few pixels — you saw the first commands and nothing else.
  It now claims its space, and "run it" hides the flow diagram so the
  recording gets the whole slide. It auto-scrolls, ending on the payoff.
- `.slide p` (0,2,0) beat `.slide__act` and `.slide__cite` (0,1,0), so the act
  eyebrow and every citation had rendered at full body size since the first
  commit. Qualified as `.slide p.`.

Playback stops and resets when you leave the slide, so it never runs unseen.

Co-Authored-By: Claude Opus 5 
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
---
 content/talks/wasm-research-day-2026.md | 138 ++++++++++++------------
 sass/_talk.scss                         |  97 ++++++++++++++---
 static/casts/dissolve.cast              |  21 ++++
 templates/talk.html                     | 125 +++++++++++++++++++++
 4 files changed, 294 insertions(+), 87 deletions(-)
 create mode 100644 static/casts/dissolve.cast

diff --git a/content/talks/wasm-research-day-2026.md b/content/talks/wasm-research-day-2026.md
index 96a1426..2e3a979 100644
--- a/content/talks/wasm-research-day-2026.md
+++ b/content/talks/wasm-research-day-2026.md
@@ -21,13 +21,13 @@ slot = "25 + 5, remote"
   
Act I · the inversion

   
What this room has already established

   

-    
2022Fixpoint — wasm lowered ahead of time, invoked with no engineserver, x86-64

-    
2023Orchestration at the edge — pluggable HALs via the Component Modelpreliminary

-    
2025WASI performance on IoT and embedded — a runtime's overhead on a small deviceruntime present

-    
todayWasmBounds — eliding bounds checks by abstract interpretationtwo hours ago

+    
2022lowered ahead of time, no enginex86-64

+    
2023pluggable HALs via the Component Modelpreliminary

+    
2025a runtime's overhead on a small deviceruntime present

+    
todayeliding bounds checks, soundlytwo hours ago

   

-  
Each is one ingredient. This talk needs all four at
-  once — on a chip where the runtime the third one measures does not fit.

+  
Four ingredients. This talk needs all four at once —
+  where the runtime does not fit.
@@ -36,21 +36,17 @@ slot = "25 + 5, remote"

the usual arrangement

-

The OS is written for the chip. The application is written against the OS - and hoped to be portable. Every new board re-opens the OS.

+

OS written for the chip. Application hoped to be portable. + Every new board re-opens the OS.

what we are trying

-

The OS itself is WebAssembly components. The Component Model is the - integration step — between OS components, between the OS and its drivers, - and between the OS and the tenants above it.

+

The OS is components. The Component Model is the integration + step — OS to OS, OS to drivers, OS to tenants.

-

The OS and everything above it is the car. The handful of native functions - that actually touch the hardware are the tires. For new terrain — another chip, - another board — you change the tires, not the car.

-

Declaring the bias: I work in automotive, so to me - everything is a car. The substrate is not — which is the next slide.

+

The bias, declared: I work in automotive, so to me + everything is a car.

@@ -104,11 +100,15 @@ spi · timer · uart · dma
ld - .o + 3 native functions + .o + the native functions → firmware
no engine, no interpreter, no JIT
+
+ + 

+  

 

 
 

@@ -118,20 +118,21 @@ spi · timer · uart · dma
     

       
wit/gust-hal.wit

       
interface mmio {
-    read32:  func(addr: u32) -> u32;
-    write32: func(addr: u32, val: u32);
-    read8:   func(addr: u32) -> u8;
-    write8:  func(addr: u32, val: u8);
+  read32:  func(addr: u32) -> u32;
+  write32: func(addr: u32, val: u32);
+  read8 / write8 likewise
 }
-world wdg-driver { import mmio; export wdg; }

+world wdg-driver {
+  import mmio; export wdg;
+}
     

     

       
and the composition

-      
wac compose fused-gustos.wac -o fused.wasm
+      
wac compose fused-gustos.wac
 meld fuse --memory shared
 loom optimize --passes inline
 synth compile --target cortex-m3 \
-      --all-exports --relocatable

+  --all-exports --relocatable

     

   
   
A driver's capability is checked against a typed contract at composition
@@ -145,8 +146,9 @@ synth compile --target cortex-m3 \
   
A watchdog you can accidentally switch off is worthless. So the interface
   offers no way to switch it off:

   
interface wdg {
-    unlock · configure · lock · start · refresh · is-running
-    — there is no stop, and no disable
+  unlock · configure · lock
+  start · refresh · is-running
+  — no stop. no disable.
 }

   
and the FSM proves the absence, rather than relying on it

   
fn p2_cannot_un_start() {
@@ -164,11 +166,9 @@ synth compile --target cortex-m3 \
   
Three dies, one session

   

     
Cortex-M4 · NUCLEO-G474RE
-IWDG reset CONFIRMED on real STM32G474
-RCC_CSR 0x14000000 → 0x34000000   IWDGRSTF=1

-    
Cortex-M3 · STM32F100 — the same .o, a second die
-IWDG reset CONFIRMED on real STM32F100
-RCC_CSR 0x14000000 → 0x34000000   IWDGRSTF=1

+IWDG reset CONFIRMED   IWDGRSTF=1

+    
Cortex-M3 · STM32F100 — the same .o
+IWDG reset CONFIRMED   IWDGRSTF=1

     
RISC-V · ESP32-C3 rev v0.4
 native 271   dissolved 499 milliticks/call   ratio 1.839×
 correctness IDENTICAL over [0,2047]   mismatch=0

@@ -218,8 +218,7 @@ export function read32(addr) {
   
#[no_mangle] extern "C" fn read32(addr: u32) -> u32 {
     unsafe { core::ptr::read_volatile(addr as *const u32) }
 }

-  
Nothing else about the component changes. That substitution
-  is the entire thesis.

+  
That substitution is the entire thesis.

   

     
seamA whole STM32 USART driver, dissolved326 B · 0 SRAM · 3 relocs

   

@@ -239,22 +238,22 @@ export function read32(addr) {
   
Six faces, not four tools

   

     

-      
architect
spar — AADL / SysML. The WIT is generated from the model, not hand-written.

+      
architect
spar — the WIT is generated from the model

     

     

-      
build
meld fuse · loom optimize · synth lower · sigil attesting across all of it.

+      
build
meld · loom · synth, with sigil attesting across all of it

     

     

-      
verify
witness MC/DC on the shipped wasm · scry abstract interpretation · Verus, Rocq, Lean, Kani as build rules.

+      
verify
witness MC/DC on the shipped wasm · Verus, Rocq, Lean, Kani

     

     

-      
trace
rivet — typed requirements, decisions and tests. Broken links fail the build.

+      
trace
rivet — typed artifacts; broken links fail the build

     

     

-      
run
kiln runtime · gale verified kernel primitives · the applications above them.

+      
run
kiln · gale verified primitives

     

     

-      
agent
The loop that files findings between repos — and the governance that keeps 30+ repos to the same rules.

+      
agent
the loop that files findings between repos

     

   

 

@@ -277,41 +276,38 @@ export function read32(addr) {
   
Act IV · the factory

   
Faster because it is proven

   

-    
baselinenative LLVM, full clamp0.50 cyc/call · 1.00×

-    
todaydissolved, as shipped0.83 cyc/call · 1.65×

-    
measured floorclamp elided because a proof allows it0.23 cyc/call · 0.45×

+    
native LLVMfull clamp0.50 cyc · 1.00×

+    
dissolvedas shipped today0.83 cyc · 1.65×

+    
proof-carryingclamp elided because a proof allows it0.23 cyc · 0.45×

   

-  
Not a model — a measured floor, soundness-gated. The elision is only legal
-  because something upstream proved the bound. A compiler with no
-  verifier in its pipeline structurally cannot reach it.

+  
Legal only because something upstream proved the bound.
+  A compiler with no verifier cannot reach it.

 
 
 

   
Act IV · the factory

   
Qualify the checker, not the prover

-  
Certification asks: why do you believe the solver? "Qualify Z3" is not a
+  
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,
-  dependency-free checker is trusted — and that checker's soundness is
-  machine-checked in Lean 4, with no sorry anywhere in its kernel.

+  
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

   

-  
This turns unchecked-solver evidence into the argument
-  a verified compiler makes: don't trust the tool, check its output.

+  
Don't trust the tool — check its output.

 

 
 

   
Act IV · the factory

   
Exactly how far this goes — and no further

   

-    
shippingTheorem proving · SMT contracts · bounded model checking · translation validation 

-    
partialRefinement to Lean · mutation testing · abstract interpretation 

+    
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. Proofs run on a verification schedule,
-  not on every commit. Our own docs say it out loud: closer to "well-specified
-  and comprehensively tested with local formal verification" than
+  
Bounded model checking is bounded. Proofs run on a schedule, not every
+  commit. Our own docs say "comprehensively tested", not
   "continuously formally verified."

 

 
@@ -319,25 +315,25 @@ export function read32(addr) {
   
Act IV · the factory

   
Every one of these gates was green for the wrong reason

   

-    
scrya proof that never ran — the theorem was false when it did 

-    
synthtwo validators, same direction, same blind spot 

-    
looma gate with passing tests and zero callers 

-    
meldverified by a test on a path the shipped code didn't take 

-    
galea count over modules that cannot see instances 

+    
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 

   

   
The failure produced the same observable as
   success.

-  
The remedy is not more gates. It is that every check must be able to go red
-  for a reason you can state in advance.

+  
The remedy is not more gates — every check must be able
+  to go red for a reason you can state in advance.

 
 
 

   
Act V · what is missing

   
What componentizing actually costs

   
driver object .text, core module → component

-  
gpio    502 → 1196 B      spi    454 → 1244 B
-timer   204 →  828 B      wdg    638 → 1718 B
-.data / .bss, every one of them       0 → 0

+  
gpio   502 → 1196 B     spi  454 → 1244 B
+timer  204 →  828 B     wdg  638 → 1718 B
+.data / .bss, all of them   0 → 0

   
Roughly +700 B fixed per driver for canonical-ABI glue
   — a constant, not a proportion. On a chip with 8 KB of SRAM that is a real
   number, and it is filed upstream rather than absorbed quietly.

@@ -349,15 +345,13 @@ timer   204 →  828 B      wdg    638 → 1718 B
   

     

       
the runner broke on success

-      
Plugging in the third board made the first one unreachable — two probes,
-      an interactive prompt, and a harness with no terminal. The all-three-at-once
-      case was exactly the case nothing had run.

+      
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

-      
The RISC-V figure is recorded with a byte-reproducible command. The wasm
-      input to that command is not in the repository — it lived in a scratch
-      directory that no longer exists.

+      
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
diff --git a/sass/_talk.scss b/sass/_talk.scss
index 4e55e28..9030768 100644
--- a/sass/_talk.scss
+++ b/sass/_talk.scss
@@ -69,7 +69,7 @@
 // Sized in vmin so a slide reads the same projected, shared, or in a tab.
 
 .slide h1 {
-  font-size: clamp(2.5rem, 6.4vmin, 4.8rem);
+  font-size: clamp(2.8rem, 8.4vmin, 6rem);
   line-height: 1.1;
   font-weight: 700;
   letter-spacing: -0.02em;
@@ -78,7 +78,7 @@
 }
 
 .slide h2 {
-  font-size: clamp(1.85rem, 4.5vmin, 3.2rem);
+  font-size: clamp(2.1rem, 6vmin, 4.2rem);
   line-height: 1.15;
   font-weight: 600;
   letter-spacing: -0.015em;
@@ -88,7 +88,7 @@
 
 .slide p,
 .slide li {
-  font-size: clamp(1.2rem, 3vmin, 2.1rem);
+  font-size: clamp(1.45rem, 4.2vmin, 2.9rem);
   line-height: 1.55;
   max-width: 46ch;
   margin: 0;
@@ -101,7 +101,7 @@
 .slide p.slide__act,
 .slide__act {
   font-family: $font-mono;
-  font-size: clamp(.85rem, 1.8vmin, 1.15rem);
+  font-size: clamp(1rem, 2.3vmin, 1.5rem);
   letter-spacing: .14em;
   text-transform: uppercase;
   color: $text-faint;
@@ -109,14 +109,14 @@
 }
 
 .slide__lead {
-  font-size: clamp(1.4rem, 3.5vmin, 2.5rem) !important;
+  font-size: clamp(1.7rem, 5vmin, 3.4rem) !important;
   color: $text-dim;
   max-width: 40ch;
 }
 
 // A pull-quote slide: the project's own words, attributed.
 .slide__quote {
-  font-size: clamp(1.8rem, 4.3vmin, 3.1rem);
+  font-size: clamp(2.1rem, 5.6vmin, 4rem);
   line-height: 1.3;
   font-weight: 500;
   max-width: 26ch;
@@ -128,7 +128,7 @@
 .slide p.slide__cite,
 .slide__cite {
   font-family: $font-mono;
-  font-size: clamp(.9rem, 1.95vmin, 1.25rem);
+  font-size: clamp(1.05rem, 2.5vmin, 1.6rem);
   color: $text-faint;
 }
 
@@ -138,7 +138,7 @@
 
 .evidence {
   font-family: $font-mono;
-  font-size: clamp(.95rem, 2.25vmin, 1.5rem);
+  font-size: clamp(1.15rem, 3.2vmin, 2rem);
   line-height: 1.5;
   background: $bg-subtle;
   border: 1px solid $border-subtle;
@@ -163,7 +163,7 @@
 .slide p.evidence__label,
 .evidence__label {
   font-family: $font-mono;
-  font-size: clamp(.8rem, 1.7vmin, 1.05rem);
+  font-size: clamp(.95rem, 2.2vmin, 1.4rem);
   letter-spacing: .06em;
   text-transform: uppercase;
   color: $text-faint;
@@ -176,6 +176,73 @@
 .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, 1.85vmin, 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, 2.9vmin, 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.
@@ -196,7 +263,7 @@
   background: $surface;
   border: 1px solid $border-subtle;
   border-radius: 8px;
-  font-size: clamp(.98rem, 2.25vmin, 1.45rem);
+  font-size: clamp(1.15rem, 3vmin, 1.9rem);
 }
 
 .ledger__tag {
@@ -237,7 +304,7 @@
 
 .flow__stage {
   font-family: $font-mono;
-  font-size: clamp(1rem, 2.2vmin, 1.4rem);
+  font-size: clamp(1.2rem, 3vmin, 1.9rem);
   font-weight: 600;
   color: $accent;
 }
@@ -245,7 +312,7 @@
 .flow__in,
 .flow__out {
   font-family: $font-mono;
-  font-size: clamp(.88rem, 2vmin, 1.25rem);
+  font-size: clamp(1.05rem, 2.7vmin, 1.7rem);
   line-height: 1.35;
 }
 
@@ -255,7 +322,7 @@
 .flow__arrow {
   font-family: $font-mono;
   color: $text-faint;
-  font-size: clamp(1rem, 2.1vmin, 1.3rem);
+  font-size: clamp(1.2rem, 2.9vmin, 1.8rem);
 }
 
 // Stack the row on a narrow screen rather than crushing four columns.
@@ -269,7 +336,7 @@
 // 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(.85rem, 1.95vmin, 1.25rem); padding: .7rem .85rem; }
+.split .evidence { font-size: clamp(1rem, 2.7vmin, 1.7rem); padding: .7rem .85rem; }
 
 // ─── Two-column split ─────────────────────────────────────────────────
 
@@ -282,7 +349,7 @@
 
 .split__col h3 {
   font-family: $font-mono;
-  font-size: clamp(.88rem, 1.85vmin, 1.15rem);
+  font-size: clamp(1rem, 2.4vmin, 1.5rem);
   letter-spacing: .1em;
   text-transform: uppercase;
   color: $text-faint;
diff --git a/static/casts/dissolve.cast b/static/casts/dissolve.cast
new file mode 100644
index 0000000..5ca299d
--- /dev/null
+++ b/static/casts/dissolve.cast
@@ -0,0 +1,21 @@
+{"version":3,"term":{"cols":80,"rows":24},"timestamp":1785871650,"command":"bash demo.sh","env":{"SHELL":"/bin/zsh"}}
+[0.005, "o", "\u001b[38;5;245m# a watchdog driver, written as a wasm component\u001b[0m\r\n\r\n"]
+[0.912, "o", "\u001b[38;5;68m$\u001b[0m wasm-tools component wit wdg.component.wasm | head -6\r\n"]
+[0.568, "o", "package root:component;\r\n\r\nworld root {\r\n  import gust:hal/mmio@0.1.0;\r\n\r\n  export gust:hal/wdg@0.1.0;\r\n"]
+[0.000, "o", "\r\n"]
+[0.714, "o", "\u001b[38;5;245m# optimize it, then lower it to a Cortex-M3 object\u001b[0m\r\n\r\n"]
+[0.911, "o", "\u001b[38;5;68m$\u001b[0m loom optimize --passes inline core.wasm -o opt.wasm | tail -1\r\n"]
+[0.639, "o", "✅ Optimization complete!\r\n"]
+[0.000, "o", "\r\n"]
+[0.713, "o", "\u001b[38;5;68m$\u001b[0m synth compile opt.wasm --target cortex-m3 --all-exports --relocatable -o wdg.o\r\n"]
+[0.546, "o", "wrote wdg.o\r\n\r\n"]
+[0.714, "o", "\u001b[38;5;245m# what does that object still need from the outside world?\u001b[0m\r\n\r\n"]
+[0.915, "o", "\u001b[38;5;68m$\u001b[0m arm-zephyr-eabi-nm -u wdg.o\r\n"]
+[0.539, "o", "         U read32\r\n         U write32\r\n"]
+[0.001, "o", "\r\n"]
+[0.714, "o", "\u001b[38;5;245m# and what does it cost?\u001b[0m\r\n\r\n"]
+[0.916, "o", "\u001b[38;5;68m$\u001b[0m arm-zephyr-eabi-size wdg.o\r\n"]
+[0.534, "o", "   text\t   data\t    bss\t    dec\t    hex\tfilename\r\n   1726\t      0\t      0\t   1726\t    6be\twdg.o\r\n"]
+[0.001, "o", "\r\n"]
+[0.714, "o", "\u001b[38;5;114m# two symbols. zero SRAM. no engine.\u001b[0m\r\n"]
+[2.516, "x", "0"]
diff --git a/templates/talk.html b/templates/talk.html
index 5834ae5..44ac867 100644
--- a/templates/talk.html
+++ b/templates/talk.html
@@ -46,7 +46,11 @@
 
   var i = 0;
 
+  var shown = -1;
   function render() {
+    // Tell the slide we are leaving, so anything playing on it can stop.
+    if (shown !== -1 && shown !== i) slides[shown].dispatchEvent(new CustomEvent('deck:leave'));
+    shown = i;
     slides.forEach(function (s, n) { s.classList.toggle('is-current', n === i); });
     counter.textContent = (i + 1) + ' / ' + slides.length;
     bar.style.width = ((i + 1) / slides.length * 100) + '%';
@@ -137,6 +141,127 @@
     document.getElementById('hint').innerHTML = 'swipe to move';
   }
 
+  // ── Terminal recordings ─────────────────────────────────────────────
+  // A real asciinema capture, replayed inline. Not a GIF: the text stays
+  // selectable and crisp at any projection size, and the file is ~2 KB.
+  // Casts are fetched once at load and held in memory, so clicking play
+  // mid-talk never depends on the network.
+
+  // xterm-256 -> css colour, enough for SGR 38;5;N and the reset.
+  function xterm(n) {
+    if (n < 16) {
+      var base = ['#000','#a00','#0a0','#a50','#00a','#a0a','#0aa','#aaa',
+                  '#555','#f55','#5f5','#ff5','#55f','#f5f','#5ff','#fff'];
+      return base[n];
+    }
+    if (n < 232) {
+      var i = n - 16, s = [0,95,135,175,215,255];
+      return 'rgb(' + s[Math.floor(i/36)] + ',' + s[Math.floor(i/6)%6] + ',' + s[i%6] + ')';
+    }
+    return 'rgb(' + (8 + (n-232)*10) + ',' + (8 + (n-232)*10) + ',' + (8 + (n-232)*10) + ')';
+  }
+
+  function esc(s) {
+    return s.replace(/&/g,'&').replace(//g,'>');
+  }
+
+  // The recording contains only SGR colour escapes and newlines — verified,
+  // no cursor movement — so append-only rendering is faithful, not an
+  // approximation.
+  function ansi(text) {
+    var out = '', open = false;
+    var re = /\x1b\[([0-9;]*)m/g, last = 0, m;
+    while ((m = re.exec(text)) !== null) {
+      out += esc(text.slice(last, m.index));
+      last = re.lastIndex;
+      var p = m[1];
+      if (p === '' || p === '0') { if (open) { out += ''; open = false; } }
+      else {
+        var c = /^38;5;(\d+)$/.exec(p);
+        if (c) { if (open) out += ''; out += ''; open = true; }
+      }
+    }
+    out += esc(text.slice(last));
+    if (open) out += '';
+    return out;
+  }
+
+  function parseCast(txt) {
+    var lines = txt.split('\n').filter(function (l) { return l.trim(); });
+    if (!lines.length) return [];
+    var ver = 2;
+    try { ver = JSON.parse(lines[0]).version || 2; } catch (e) {}
+    var evs = [], t = 0;
+    for (var i = 1; i < lines.length; i++) {
+      var e;
+      try { e = JSON.parse(lines[i]); } catch (err) { continue; }
+      if (e[1] !== 'o') continue;
+      // v3 intervals are relative to the previous event; v2 are absolute.
+      t = (ver >= 3) ? t + e[0] : e[0];
+      evs.push([t, e[2]]);
+    }
+    return evs;
+  }
+
+  document.querySelectorAll('.cast').forEach(function (box) {
+    var screen = box.querySelector('.cast__screen');
+    var btn    = box.querySelector('.cast__play');
+    var evs = null, timers = [], playing = false;
+
+    fetch(box.dataset.cast)
+      .then(function (r) { return r.ok ? r.text() : Promise.reject(r.status); })
+      .then(function (t) { evs = parseCast(t); })
+      .catch(function () {
+        btn.textContent = 'recording unavailable';
+        btn.disabled = true;
+      });
+
+    function stop() { timers.forEach(clearTimeout); timers = []; playing = false; }
+
+    function paint(upto) {
+      var s = '';
+      for (var i = 0; i < evs.length && evs[i][0] <= upto; i++) s += evs[i][1];
+      screen.innerHTML = ansi(s.replace(/\r\n/g, '\n'));
+      screen.scrollTop = screen.scrollHeight;
+    }
+
+    btn.addEventListener('click', function () {
+      if (!evs) return;
+      if (playing) {                       // a second press skips to the end
+        stop();
+        paint(Infinity);
+        btn.textContent = 'replay';
+        return;
+      }
+      stop();
+      box.classList.add('is-open');
+      box.closest('.slide').classList.add('cast-open');
+      screen.innerHTML = '';
+      playing = true;
+      btn.textContent = 'skip';
+      var acc = '';
+      evs.forEach(function (ev) {
+        timers.push(setTimeout(function () {
+          acc += ev[1];
+          screen.innerHTML = ansi(acc.replace(/\r\n/g, '\n'));
+          screen.scrollTop = screen.scrollHeight;
+        }, ev[0] * 1000));
+      });
+      timers.push(setTimeout(function () {
+        playing = false; btn.textContent = 'replay';
+      }, (evs[evs.length - 1][0] + 0.2) * 1000));
+    });
+
+    // Leaving the slide stops playback so it never runs on unseen slides.
+    box.closest('.slide').addEventListener('deck:leave', function () {
+      stop();
+      box.classList.remove('is-open');
+      box.closest('.slide').classList.remove('cast-open');
+      btn.textContent = 'run it';
+      screen.innerHTML = '';
+    });
+  });
+
   var start = parseInt((location.hash || '').slice(1), 10);
   go(isNaN(start) ? 0 : start - 1);
 }());

From fc850a57cfb72d73977d0a1a48e93ccdcab690c2 Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier 
Date: Tue, 4 Aug 2026 21:37:01 +0200
Subject: [PATCH 05/56] =?UTF-8?q?talk:=20slide=205=20shows=20the=20whole?=
 =?UTF-8?q?=20chain=20=E2=80=94=20wac=20and=20meld=20included=20=E2=80=94?=
 =?UTF-8?q?=20on=20the=20OS=20itself?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The recording covered only loom -> synth, so it silently skipped the first two
rows of the very slide it sits on. Re-recorded against the real 5-provider
composition, and against the OS rather than a single driver:

  wac compose      5 components  -> 1 component, 20741 B
                                    exports 5 gust:os, imports mmio + taskdisp
  meld fuse        11 memories   -> 1 core module, 9874 B (-52.4%)
  loom optimize
  synth compile                  -> gustos.o
  nm -u                          -> poll-task, read32, write32
  size                           -> text 4812  data 0  bss 0

The whole gust OS as one relocatable object with a three-symbol trusted
surface and zero SRAM. That is a better demonstration than a driver was.

Flow rows re-stated from those measurements rather than from memory: the
slide had claimed "5 linear memories -> one shared memory" where meld
actually reports 11 -> 1 core module at 52% smaller, and the "3 native
functions" claim is now the measured undefined-symbol count, not an estimate.

Co-Authored-By: Claude Opus 5 
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
---
 content/talks/wasm-research-day-2026.md | 10 +++---
 static/casts/dissolve.cast              | 41 ++++++++++++++-----------
 2 files changed, 28 insertions(+), 23 deletions(-)

diff --git a/content/talks/wasm-research-day-2026.md b/content/talks/wasm-research-day-2026.md
index 2e3a979..596b031 100644
--- a/content/talks/wasm-research-day-2026.md
+++ b/content/talks/wasm-research-day-2026.md
@@ -78,13 +78,13 @@ spi · timer · uart · dma

       wac compose
       5 components
       →
-      1 component
exports gust:os · imports gust:hal
+      1 component · 20 741 B
exports 5 gust:os · imports mmio + taskdisp
     
     

       meld fuse
-      1 component
5 linear memories
+      1 component
11 linear memories
       →
-      1 core module
one shared memory
+      1 core module · 9 874 B
shared memory — 52% smaller
     

     

       loom optimize
@@ -96,11 +96,11 @@ spi · timer · uart · dma
       synth compile
       module + facts
       →
-      one relocatable .o + certificates
+      gustos.o · 4 812 B text · 0 SRAM
     

     

       ld
-      .o + the native functions
+      .o + 3 native functions
       →
       firmware
no engine, no interpreter, no JIT
     

diff --git a/static/casts/dissolve.cast b/static/casts/dissolve.cast
index 5ca299d..990ef93 100644
--- a/static/casts/dissolve.cast
+++ b/static/casts/dissolve.cast
@@ -1,21 +1,26 @@
-{"version":3,"term":{"cols":80,"rows":24},"timestamp":1785871650,"command":"bash demo.sh","env":{"SHELL":"/bin/zsh"}}
-[0.005, "o", "\u001b[38;5;245m# a watchdog driver, written as a wasm component\u001b[0m\r\n\r\n"]
-[0.912, "o", "\u001b[38;5;68m$\u001b[0m wasm-tools component wit wdg.component.wasm | head -6\r\n"]
-[0.568, "o", "package root:component;\r\n\r\nworld root {\r\n  import gust:hal/mmio@0.1.0;\r\n\r\n  export gust:hal/wdg@0.1.0;\r\n"]
-[0.000, "o", "\r\n"]
-[0.714, "o", "\u001b[38;5;245m# optimize it, then lower it to a Cortex-M3 object\u001b[0m\r\n\r\n"]
-[0.911, "o", "\u001b[38;5;68m$\u001b[0m loom optimize --passes inline core.wasm -o opt.wasm | tail -1\r\n"]
-[0.639, "o", "✅ Optimization complete!\r\n"]
-[0.000, "o", "\r\n"]
-[0.713, "o", "\u001b[38;5;68m$\u001b[0m synth compile opt.wasm --target cortex-m3 --all-exports --relocatable -o wdg.o\r\n"]
-[0.546, "o", "wrote wdg.o\r\n\r\n"]
-[0.714, "o", "\u001b[38;5;245m# what does that object still need from the outside world?\u001b[0m\r\n\r\n"]
-[0.915, "o", "\u001b[38;5;68m$\u001b[0m arm-zephyr-eabi-nm -u wdg.o\r\n"]
-[0.539, "o", "         U read32\r\n         U write32\r\n"]
+{"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.714, "o", "\u001b[38;5;245m# and what does it cost?\u001b[0m\r\n\r\n"]
-[0.916, "o", "\u001b[38;5;68m$\u001b[0m arm-zephyr-eabi-size wdg.o\r\n"]
-[0.534, "o", "   text\t   data\t    bss\t    dec\t    hex\tfilename\r\n   1726\t      0\t      0\t   1726\t    6be\twdg.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.714, "o", "\u001b[38;5;114m# two symbols. zero SRAM. no engine.\u001b[0m\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"]

From ffabdb74381dee7a4444658a1bfbf1f357fa1a49 Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier 
Date: Tue, 4 Aug 2026 21:40:09 +0200
Subject: [PATCH 06/56] talk: the cost slide now carries the measured response,
 not just the cost
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The componentization slide named a +700-1100 B canonical-ABI overhead and left
it there. It now also shows what we did about it: our wit-bindgen fork's
cabi-realloc-extern backs cabi_realloc with a bounded arena that traps instead
of growing, worth -318 B (-18%) on wdg-thin, 29% of that driver's overhead.

Measured today with the version bump controlled for — the fork is at 0.58, and
a naive comparison against the shipped 0.52 would have mis-credited the feature.
The slide says the drivers do not use it yet, because they do not.

Turns a slide that admitted a cost into one that shows the loop closing:
name the cost, patch the tool, measure the result, state what is still undone.

Co-Authored-By: Claude Opus 5 
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
---
 content/talks/wasm-research-day-2026.md | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/content/talks/wasm-research-day-2026.md b/content/talks/wasm-research-day-2026.md
index 596b031..2c921c2 100644
--- a/content/talks/wasm-research-day-2026.md
+++ b/content/talks/wasm-research-day-2026.md
@@ -332,11 +332,15 @@ export function read32(addr) {
   
What componentizing actually costs

   
driver object .text, core module → component

   
gpio   502 → 1196 B     spi  454 → 1244 B
-timer  204 →  828 B     wdg  638 → 1718 B
+timer  204 →  828 B     wdg  638 → 1726 B
 .data / .bss, all of them   0 → 0

-  
Roughly +700 B fixed per driver for canonical-ABI glue
-  — a constant, not a proportion. On a chip with 8 KB of SRAM that is a real
-  number, and it is filed upstream rather than absorbed quietly.

+  
and the response, measured for this talk

+  
wdg, canonical glue on a growing allocator   1746 B
+     backed by a bounded arena instead        1428 B   −318

+  
So we patched the bindings generator rather than absorbing the cost:
+  cabi_realloc delegates to an embedder arena that traps instead of
+  growing. 29% of the overhead back — and the drivers do
+  not use it yet.

 

 
 


From 9bbc00bcc554410514d8454758471ef12e317282 Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier 
Date: Tue, 4 Aug 2026 22:06:41 +0200
Subject: [PATCH 07/56] talk: scale the type to slide HEIGHT, so no slide
 overruns at any aspect
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Scanned every slide for anything crossing its padding box, at five viewport
shapes. Two real edge overruns (trailing code comments, 35px and 101px) and,
more importantly, a whole class of failure the earlier per-slide trimming could
never have fixed.

The type was sized in vmin, which tracks min(width, height). On a 16:10 screen
that is the width, so body text landed at 2.9% of slide height; on a 4:3 screen
vmin IS the height and the same rule gave 4.2%. Slide fit is height-bound, so
the denser slides overflowed on 4:3 and 1920x1080 while passing on 1180x820 —
and hand-trimming for one shape re-broke another.

Each size is now capped against vh at ~0.79 of its vmin coefficient, pinning
every aspect to ~3.3% of slide height and letting vmin bind only in portrait,
where height is abundant. One lever (`--fs`) remains for a floor on very short
laptop screens. Long code lines wrap rather than scroll below 900px, so a
tablet held in portrait never hides the end of a line behind a swipe.

Measured after, zero overflowing slides and zero elements crossing an edge:

  1024x768   body 25px   3.3%      1180x820   body 27px   3.3%
  1366x1024  body 34px   3.3%      1920x1080  body 36px   3.3%
  820x1180   body 34px   2.9% (portrait — vmin binds, as intended)

Also dropped the closing line on the gates slide; the pull-quote already says it
and it was the one item still overrunning at every size.

Co-Authored-By: Claude Opus 5 
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
---
 content/talks/wasm-research-day-2026.md |  8 ++--
 sass/_talk.scss                         | 51 ++++++++++++++++---------
 2 files changed, 38 insertions(+), 21 deletions(-)

diff --git a/content/talks/wasm-research-day-2026.md b/content/talks/wasm-research-day-2026.md
index 2c921c2..b200dc8 100644
--- a/content/talks/wasm-research-day-2026.md
+++ b/content/talks/wasm-research-day-2026.md
@@ -154,7 +154,8 @@ synth compile --target cortex-m3 \
   
fn p2_cannot_un_start() {
     let w = Iwdg { phase: Running, .. };
     if let Ok(n) = refresh(w) { assert_eq!(n.phase, Running); }
-    assert!(unlock(w).is_err());        // no escape from Running
+    // no escape from Running:
+    assert!(unlock(w).is_err());
 }

   
The contract itself cannot express the one transition the
   proof forbids. That is the argument for putting the seam in a type
@@ -209,7 +210,8 @@ correctness IDENTICAL over [0,2047]   mismatch=The whole of a tire
   
web/shim-mmio.js — what a browser tab supplies

   
const REGS = new Uint32Array(64);
-const TIM2_CNT = 0x40000024;   // the one clock register the OS reads
+// 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];
@@ -323,8 +325,6 @@ export function read32(addr) {
   
   
The failure produced the same observable as
   success.

-  
The remedy is not more gates — every check must be able
-  to go red for a reason you can state in advance.

 

 
 

diff --git a/sass/_talk.scss b/sass/_talk.scss
index 9030768..3b51b1b 100644
--- a/sass/_talk.scss
+++ b/sass/_talk.scss
@@ -23,6 +23,11 @@
   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%;
@@ -69,7 +74,7 @@
 // Sized in vmin so a slide reads the same projected, shared, or in a tab.
 
 .slide h1 {
-  font-size: clamp(2.8rem, 8.4vmin, 6rem);
+  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;
@@ -78,7 +83,7 @@
 }
 
 .slide h2 {
-  font-size: clamp(2.1rem, 6vmin, 4.2rem);
+  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;
@@ -88,7 +93,7 @@
 
 .slide p,
 .slide li {
-  font-size: clamp(1.45rem, 4.2vmin, 2.9rem);
+  font-size: clamp(1.45rem, min(calc(4.2vmin * var(--fs)), calc(3.32vh * var(--fs))), 2.9rem);
   line-height: 1.55;
   max-width: 46ch;
   margin: 0;
@@ -101,7 +106,7 @@
 .slide p.slide__act,
 .slide__act {
   font-family: $font-mono;
-  font-size: clamp(1rem, 2.3vmin, 1.5rem);
+  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;
@@ -109,14 +114,14 @@
 }
 
 .slide__lead {
-  font-size: clamp(1.7rem, 5vmin, 3.4rem) !important;
+  font-size: clamp(1.7rem, min(calc(5.0vmin * var(--fs)), calc(3.95vh * var(--fs))), 3.4rem) !important;
   color: $text-dim;
   max-width: 40ch;
 }
 
 // A pull-quote slide: the project's own words, attributed.
 .slide__quote {
-  font-size: clamp(2.1rem, 5.6vmin, 4rem);
+  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;
@@ -128,7 +133,7 @@
 .slide p.slide__cite,
 .slide__cite {
   font-family: $font-mono;
-  font-size: clamp(1.05rem, 2.5vmin, 1.6rem);
+  font-size: clamp(1.05rem, min(calc(2.5vmin * var(--fs)), calc(1.98vh * var(--fs))), 1.6rem);
   color: $text-faint;
 }
 
@@ -138,7 +143,7 @@
 
 .evidence {
   font-family: $font-mono;
-  font-size: clamp(1.15rem, 3.2vmin, 2rem);
+  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;
@@ -163,7 +168,7 @@
 .slide p.evidence__label,
 .evidence__label {
   font-family: $font-mono;
-  font-size: clamp(.95rem, 2.2vmin, 1.4rem);
+  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;
@@ -192,7 +197,7 @@
 .cast__play {
   align-self: flex-start;
   font-family: $font-mono;
-  font-size: clamp(.85rem, 1.85vmin, 1.1rem);
+  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;
@@ -211,7 +216,7 @@
 
 .cast__screen {
   font-family: $font-mono;
-  font-size: clamp(1.05rem, 2.9vmin, 1.8rem);
+  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;
@@ -263,7 +268,7 @@
   background: $surface;
   border: 1px solid $border-subtle;
   border-radius: 8px;
-  font-size: clamp(1.15rem, 3vmin, 1.9rem);
+  font-size: clamp(1.15rem, min(calc(3.0vmin * var(--fs)), calc(2.37vh * var(--fs))), 1.9rem);
 }
 
 .ledger__tag {
@@ -304,7 +309,7 @@
 
 .flow__stage {
   font-family: $font-mono;
-  font-size: clamp(1.2rem, 3vmin, 1.9rem);
+  font-size: clamp(1.2rem, min(calc(3.0vmin * var(--fs)), calc(2.37vh * var(--fs))), 1.9rem);
   font-weight: 600;
   color: $accent;
 }
@@ -312,7 +317,7 @@
 .flow__in,
 .flow__out {
   font-family: $font-mono;
-  font-size: clamp(1.05rem, 2.7vmin, 1.7rem);
+  font-size: clamp(1.05rem, min(calc(2.7vmin * var(--fs)), calc(2.13vh * var(--fs))), 1.7rem);
   line-height: 1.35;
 }
 
@@ -322,7 +327,7 @@
 .flow__arrow {
   font-family: $font-mono;
   color: $text-faint;
-  font-size: clamp(1.2rem, 2.9vmin, 1.8rem);
+  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.
@@ -336,7 +341,7 @@
 // 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, 2.7vmin, 1.7rem); padding: .7rem .85rem; }
+.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 ─────────────────────────────────────────────────
 
@@ -349,7 +354,7 @@
 
 .split__col h3 {
   font-family: $font-mono;
-  font-size: clamp(1rem, 2.4vmin, 1.5rem);
+  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;
@@ -514,3 +519,15 @@
   .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; } }

From 98ba9b526f90fdda2420e8fec4dfc6353cbd31d6 Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier 
Date: Tue, 4 Aug 2026 22:11:50 +0200
Subject: [PATCH 08/56] =?UTF-8?q?talk:=20add=20synth's=20architecture=20?=
 =?UTF-8?q?=E2=80=94=20where=20the=20evidence=20enters=20the=20pipeline?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The factory act described the toolchain as six cube faces, which is an
abstraction. synth's own architecture overview is better: it shows WHERE
evidence enters, block by block, and it is the project's own diagram rather
than one invented for a slide.

Six stages — upstream/untrusted, front, middle, back, per-compilation, out —
with the evidence-producing and evidence-checking blocks tinted and the one
hazard block in amber: trap re-introduction, because hardware is more total
than Wasm. That amber block is the most honest thing in the deck's middle: a
diagram that is all reassurance is not a diagram anyone should believe.

It also closes a loop with the cost slide. The FRONT column carries `cabi
arena bind` — wit-bindgen's dangling realloc import resolved to a defined
function — which is exactly the mechanism measured at -318 B two slides later.

Fitting it took the diagram its own scale, since a diagram is read rather than
declaimed: six columns across 1180px put the block labels at 11px, so it flows
3-across into two rows and the labels land at 18px with 15px sub-labels. Diagram
slides also get a smaller heading and tighter stacking than prose slides.

Verified at 1180x820: 22 slides, none overflowing, nothing crossing an edge.

Co-Authored-By: Claude Opus 5 
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
---
 content/talks/wasm-research-day-2026.md | 48 ++++++++++++++++
 sass/_talk.scss                         | 75 +++++++++++++++++++++++++
 2 files changed, 123 insertions(+)

diff --git a/content/talks/wasm-research-day-2026.md b/content/talks/wasm-research-day-2026.md
index b200dc8..75cd45c 100644
--- a/content/talks/wasm-research-day-2026.md
+++ b/content/talks/wasm-research-day-2026.md
@@ -260,6 +260,54 @@ export function read32(addr) {
   
 

 
+

+  
Act IV · the factory

+  
Where the evidence enters

+  

+    

+      upstream · untrusted
+      
loomZ3 validator → wsc.facts

+      
scryintervals · stack-depth

+      
meldcomponent → core wasm

+    

+    

+      front
+      
Wasm decodercore + component

+      
wsc.facts ingestbad section ⇒ no facts, never error

+      
WIT / ABIlift · lower

+      
cabi arena binddangling realloc → defined fn

+    

+    

+      middle
+      
CFG + SSAliveness · reaching defs

+      
Verified selector DSL50 rules · 50 Rocq Qed

+      
Fact specializationper-site SMT + LRAT

+      
Register allocationBelady spill

+    

+    

+      back
+      
Thumb-2Cortex-M3/M4/M7

+      
A32 · A64Cortex-R5 · cortex-a53

+      
RV32IMACqemu · ESP32-C3

+      
Trap re-introductionhardware is more total

+    

+    

+      per compilation
+      
Translation validationQF_BV · pure Rust

+      
Trap-preservation VCdiv · OOB · trunc

+      
Static-data addressing VCbyte equality

+      
Allocation validatorswhole-function · CFG

+    

+    

+      out
+      
Freestanding ELFvectors · linker · MPU

+      
WCET sidecarsound per-function

+      
DWARFrelocatable

+    

+  

+  
Tinted = produces or checks evidence · amber = this translation's hazard

+

+
 

   
Act IV · the factory

   
No stage trusts the one above it

diff --git a/sass/_talk.scss b/sass/_talk.scss
index 3b51b1b..52a79f8 100644
--- a/sass/_talk.scss
+++ b/sass/_talk.scss
@@ -531,3 +531,78 @@
 // 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(.arch) {
+  gap: .55rem;
+  h2 { font-size: clamp(1.5rem, min(4vmin, 3.2vh), 2.5rem); }
+}

From e972fa1c06ff328589110c23491ed0b4f1e969e2 Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier 
Date: Tue, 4 Aug 2026 22:18:30 +0200
Subject: [PATCH 09/56] talk: all three architectures, readable top-to-bottom,
 one tab each
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Two problems with the first attempt, both real.

READING ORDER. The source diagrams are left-to-right stage columns. Six of them
on a slide put the block labels at 11px, and reflowing 3-across into two rows
destroyed the one thing a pipeline diagram has to convey — which way it goes.
Stages are now ROWS with the stage name in a left gutter: one unambiguous
top-to-bottom order, and every block gets real width. Block labels 19px,
sub-labels 16px (was 11/9).

ONLY SYNTH. The talk is about the whole factory, so the slide carried one
tool's internals. meld, loom and synth each publish an architecture in the same
visual language, so the slide now has a tab per tool and switches instantly —
all three stay in the DOM, nothing fetched.

What that buys is the alignment across them, which is worth more than any one
diagram. Each names one hazard, and they are the same mismatch from three
sides:

  meld   Validates != correct     tool lenient · engine strict · run exact
  loom   Total-operation model    the verifier does not see traps
  synth  Trap re-introduction     hardware is more total than Wasm

loom's note states it plainly: Wasm is partial, and everything on both sides of
it is total. A compiler must put traps back; an optimizer must stop taking them
away. Same mismatch, opposite directions, both silent-wrong.

Verified at 1180x820: all three tabs fit with zero overflow, and no other slide
in the deck overflows either.

Co-Authored-By: Claude Opus 5 
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
---
 content/talks/wasm-research-day-2026.md | 129 +++++++++++++++++-------
 sass/_talk.scss                         |  95 ++++++++++++++++-
 templates/talk.html                     |  18 ++++
 3 files changed, 200 insertions(+), 42 deletions(-)

diff --git a/content/talks/wasm-research-day-2026.md b/content/talks/wasm-research-day-2026.md
index 75cd45c..4caa7bb 100644
--- a/content/talks/wasm-research-day-2026.md
+++ b/content/talks/wasm-research-day-2026.md
@@ -263,49 +263,100 @@ export function read32(addr) {
 

   
Act IV · the factory

   
Where the evidence enters

-  

-    

-      upstream · untrusted
-      
loomZ3 validator → wsc.facts

-      
scryintervals · stack-depth

-      
meldcomponent → core wasm

-    

-    

-      front
-      
Wasm decodercore + component

-      
wsc.facts ingestbad section ⇒ no facts, never error

-      
WIT / ABIlift · lower

-      
cabi arena binddangling realloc → defined fn

-    

-    

-      middle
-      
CFG + SSAliveness · reaching defs

-      
Verified selector DSL50 rules · 50 Rocq Qed

-      
Fact specializationper-site SMT + LRAT

-      
Register allocationBelady spill

-    

-    

-      back
-      
Thumb-2Cortex-M3/M4/M7

-      
A32 · A64Cortex-R5 · cortex-a53

-      
RV32IMACqemu · ESP32-C3

-      
Trap re-introductionhardware is more total

+  

+    
+    
+    
+  

+  

+    

+      
parse

+        Component decodercore + CM, nested
+        Core-instance topologyshared memories · tables
+        Canonical optionsencoding · realloc
+      

+      
resolve

+        Import resolutionproved sound + complete
+        Topological ordercycle detection terminates
+        Adapter-site IDsites found at every crossing
+      

+      
merge

+        Index-space remapinjective · complete · 6 spaces
+        Layout disjointnesssequential, non-overlapping
+        Per-boundary seamsaddress · call-lowering · PIC
+      

+      
adapt

+        Fused trampolineslift/lower roundtrip
+        Transcode · copy · reallocUTF-8/16 · memory.copy
+        Validates ≠ correcttool lenient · engine strict · run exact
+      

+      
out

+        One core moduleno runtime linking, no host
+        DWARF + provenanceremapped · fusion attestation
+      

     

-    

-      per compilation
-      
Translation validationQF_BV · pure Rust

-      
Trap-preservation VCdiv · OOB · trunc

-      
Static-data addressing VCbyte equality

-      
Allocation validatorswhole-function · CFG

+    

+      
in

+        Core module / componentwasmparser · no execution
+        wsc.* namespace stripinput facts never re-emitted
+      

+      
ir

+        Instructions → ISLE termstyped term rewriting
+        E-graphequality saturation
+        Value-attached factskeyed by value, not index
+      

+      
passes

+        inline · const-foldalgebraic mid-end
+        dce · dead-storescode removal — the risky class
+        forward-carrier · SROAseam dissolution
+      

+      
per compilation

+        Translation validationvalue equivalence · QF_BV
+        Trap-equivalence gatecertificate re-checked
+        Total-operation modelthe verifier does not see traps
+      

+      
gate

+        Behavioral differentialexecuted vs baseline
+        Revert-on-doubtskip the function, keep the original
+      

+      
out

+        Optimized Wasmbyte-identical when nothing proven
+        wsc.factsvalue-range invariants, schema v1
+      

     

-    

-      out
-      
Freestanding ELFvectors · linker · MPU

-      
WCET sidecarsound per-function

-      
DWARFrelocatable

+    

+      
upstream

+        loomZ3 validator → wsc.facts
+        scryintervals · stack-depth
+        meldcomponent → core wasm
+      

+      
front

+        wsc.facts ingestbad section ⇒ no facts, never error
+        WIT / ABIlift · lower
+        cabi arena binddangling realloc → defined fn
+      

+      
middle

+        Verified selector DSL50 rules · 50 Rocq Qed
+        Fact specializationper-site SMT + LRAT
+        Register allocationBelady spill
+      

+      
back

+        Thumb-2 · A32 · A64 · RV32IMACM3/M4/M7 · R5 · a53 · ESP32-C3
+        Trap re-introductionhardware is more total than Wasm
+      

+      
per compilation

+        Translation validationQF_BV · pure Rust
+        Trap-preservation VCdiv · OOB · trunc
+        Allocation validatorswhole-function · CFG
+      

+      
out

+        Freestanding ELFvectors · linker · MPU
+        WCET sidecarsound per-function
+        DWARFrelocatable
+      

     

   

-  
Tinted = produces or checks evidence · amber = this translation's hazard

+  
Tinted = produces or checks evidence · amber = this stage's hazard

 

 
 

diff --git a/sass/_talk.scss b/sass/_talk.scss
index 52a79f8..885338a 100644
--- a/sass/_talk.scss
+++ b/sass/_talk.scss
@@ -95,7 +95,9 @@
 .slide li {
   font-size: clamp(1.45rem, min(calc(4.2vmin * var(--fs)), calc(3.32vh * var(--fs))), 2.9rem);
   line-height: 1.55;
-  max-width: 46ch;
+  // 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;
 }
 
@@ -116,7 +118,7 @@
 .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: 40ch;
+  max-width: min(100%, 44ch);
 }
 
 // A pull-quote slide: the project's own words, attributed.
@@ -132,6 +134,7 @@
 
 .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;
   font-size: clamp(1.05rem, min(calc(2.5vmin * var(--fs)), calc(1.98vh * var(--fs))), 1.6rem);
   color: $text-faint;
@@ -532,6 +535,92 @@
 // 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; }
+}
+
+.archset { display: grid; width: 100%; }
+.archr { grid-area: 1 / 1; display: none; flex-direction: column; gap: .3rem; }
+.archr.is-on { display: flex; }
+
+.archr__row {
+  display: grid;
+  grid-template-columns: 10ch 1fr;
+  gap: .6rem;
+  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; }
+
+.ab {
+  flex: 1 1 auto;
+  background: $surface;
+  border: 1px solid $border-subtle;
+  border-radius: 6px;
+  padding: .3rem .5rem;
+  font-size: clamp(.9rem, min(2.9vmin, 2.35vh), 1.4rem);
+  font-weight: 600;
+  line-height: 1.25;
+
+  small {
+    display: block;
+    font-family: $font-mono;
+    font-size: .84em;
+    font-weight: 400;
+    color: $text-dim;
+    margin-top: .05rem;
+  }
+
+  // Produces or checks evidence.
+  &.ev { border-color: rgba(34,211,238,.5); background: rgba(34,211,238,.08); color: $cyan; }
+  // The hazard class specific to this translation.
+  &.hz { border-color: rgba(251,191,36,.6); background: rgba(251,191,36,.09); 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;
@@ -602,7 +691,7 @@
 
 // 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(.arch) {
+.slide:has(.archset) {
   gap: .55rem;
   h2 { font-size: clamp(1.5rem, min(4vmin, 3.2vh), 2.5rem); }
 }
diff --git a/templates/talk.html b/templates/talk.html
index 44ac867..faf3043 100644
--- a/templates/talk.html
+++ b/templates/talk.html
@@ -262,6 +262,24 @@
     });
   });
 
+  // ── Architecture tabs ───────────────────────────────────────────────
+  // Three tools, one diagram slot. Only one is shown; the others stay in the
+  // DOM so switching is instant and works with no network.
+  document.querySelectorAll('.archtabs').forEach(function (tabs) {
+    var slide = tabs.closest('.slide');
+    tabs.addEventListener('click', function (e) {
+      var btn = e.target.closest('.archtab');
+      if (!btn) return;
+      var want = btn.dataset.arch;
+      tabs.querySelectorAll('.archtab').forEach(function (b) {
+        b.classList.toggle('is-on', b === btn);
+      });
+      slide.querySelectorAll('.archr').forEach(function (d) {
+        d.classList.toggle('is-on', d.dataset.arch === want);
+      });
+    });
+  });
+
   var start = parseInt((location.hash || '').slice(1), 10);
   go(isNaN(start) ? 0 : start - 1);
 }());

From 48aa0a42c24270f2c8eac0bfb60be9753b819b27 Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier 
Date: Tue, 4 Aug 2026 22:23:44 +0200
Subject: [PATCH 10/56] talk: show the wsc.facts bytes, and explain what
 "faster" actually means
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

SLIDE 14 asserted a fact channel without ever showing one. It now carries a real
wsc.facts payload, computed from loom's own emitter (loom-core/src/lib.rs
build_wsc_facts_payload) rather than invented — schema v1, one value-range fact,
LEB128, nine bytes total:

  01  schema v1 · 01 one fact · 01 kind=value-range
  03  func_index · 07 value_id · 03 00 ff 0f  body: 0 <= v <= 2047

Nine bytes is the point: the whole proof-carrying channel is smaller than the
sentence describing it. The value_id annotation carries the design argument —
keyed to a VALUE, because an optimizer renumbers everything, and a fact keyed to
a position is still true of something while being asserted about something else.
Added loom's own honest scope: emitter and wire format are done and byte-verified
against the consumer, but the source that would populate it at volume is not
wired, so 232->104 is what the channel does when it carries a fact, not evidence
that we produce many.

SLIDE 15 gave three numbers and no mechanism — and mixed ratio directions, so
1.65x read as an improvement when it is a regression. It now shows the actual
function:

  gust_mix(ch) = clamp(1500 + (ch - 1024), 1000, 2000)

LLVM must emit the clamp because it cannot know ch. The OS primitives above
carry a proven bound, ch in [524,1524], so ch+476 is provably inside [1000,2000],
both clamp branches are dead, and the function collapses to `add r0,#476; bx lr`.
Ratios are now stated in words — 1.4x SLOWER today, 2.2x FASTER with the proof —
against a stated unit, so the direction cannot be misread.

That is the whole thesis in one function: not out-optimizing LLVM, but optimizing
with information LLVM structurally never had.

Co-Authored-By: Claude Opus 5 
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
---
 content/talks/wasm-research-day-2026.md | 42 ++++++++++++++++++-------
 1 file changed, 30 insertions(+), 12 deletions(-)

diff --git a/content/talks/wasm-research-day-2026.md b/content/talks/wasm-research-day-2026.md
index 4caa7bb..c865349 100644
--- a/content/talks/wasm-research-day-2026.md
+++ b/content/talks/wasm-research-day-2026.md
@@ -362,27 +362,45 @@ export function read32(addr) {
 

   
Act IV · the factory

   
No stage trusts the one above it

-  
When loom proves a value range, it does not just use it and
-  discard it. It writes it into a custom section — wsc.facts — keyed
-  to values, not positions, so renumbering cannot silently re-point a fact.

-  
synth never re-derives that fact and never takes it on faith. It
-  proves its own specialization correct given the fact, per site, and
-  emits a certificate.

+  
When loom proves a value range it does not discard it. It writes
+  it into a custom section — 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)

+  
Keyed to values because an optimizer renumbers everything. Key a fact
+  to an instruction index and the next pass deletes three above it — the fact
+  is still true of something, and now asserted about something else. A fact whose
+  value did not survive is dropped, never re-pointed.

   

-    
measuredA bounds-guard sequence, with the fact forwarded232 → 104 B

+    
measureda bounds-guard sequence, with the fact forwarded232 → 104 B

   

+  
Honest scope: the emitter, schema and wire format are done
+  and byte-verified against the consumer. The source that would populate
+  this at volume is not wired — 232→104 is what the channel does when it
+  carries a fact, not evidence that we produce many yet.

 

 
 

   
Act IV · the factory

   
Faster because it is proven

+  
gust_mix(ch) = clamp(1500 + (ch - 1024), 1000, 2000)

+  
LLVM must emit the clamp: it cannot know what ch is. But 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:

+  
add r0, #476
+bx  lr          — the whole function

   

-    
native LLVMfull clamp0.50 cyc · 1.00×

-    
dissolvedas shipped today0.83 cyc · 1.65×

-    
proof-carryingclamp elided because a proof allows it0.23 cyc · 0.45×

+    
native LLVMfull clamp — what LLVM ships0.50 ticks/call

+    
dissolved todayclamp still emitted0.70 — 1.4× slower

+    
with the proofclamp elided, correct only under the bound0.23 — 2.2× faster

   

-  
Legal only because something upstream proved the bound.
-  A compiler with no verifier cannot reach it.

+  
Soundness-gated: the bench asserts the elided form equals
+  the native one across the proven range. LLVM never had the bound.

 

 
 


From 5d5bdc6ebd0fa045103411bf414c2a1d44abc084 Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier 
Date: Tue, 4 Aug 2026 22:28:56 +0200
Subject: [PATCH 11/56] talk: split the dense slides, and stop hiding the
 controls
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

CONTROLS — my bug, and a bad one for a presenter. The nav was dimmed to .35
opacity under `@media (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 faded to near-invisible with no hover
available to bring them back. They are now always visible (.8, full on
hover/focus). A presenter always needs the controls; a little visual noise is
the correct trade.

SPLIT — 22 -> 29 slides. Six slides were carrying two ideas each:

  the pipeline flow          | running it
  the wdg contract           | the proof that the transition is impossible
  the wsc.facts bytes        | why a value and not a position | what it is worth
  the clamp-elision example  | the measured numbers
  the componentization cost  | the patch that recovers 29% of it
  the browser shim           | the silicon side

Each half now gets a slide. Measured after: average fill 62% of available
height (was crowding 100% on the worst), nothing overflows, densest slide 82%.

29 slides against a 25-minute slot is ~52s each, which suits slides that carry
one idea rather than three.

Co-Authored-By: Claude Opus 5 
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
---
 content/talks/wasm-research-day-2026.md | 80 ++++++++++++++++++-------
 sass/_talk.scss                         | 15 ++---
 2 files changed, 67 insertions(+), 28 deletions(-)

diff --git a/content/talks/wasm-research-day-2026.md b/content/talks/wasm-research-day-2026.md
index c865349..a44799e 100644
--- a/content/talks/wasm-research-day-2026.md
+++ b/content/talks/wasm-research-day-2026.md
@@ -105,6 +105,11 @@ spi · timer · uart · dma

       firmware
no engine, no interpreter, no JIT
     
   
+

+
+

+  
Act II · the car

+  
The same chain, actually run

   

     
     

@@ -150,16 +155,20 @@ synth compile --target cortex-m3 \
   start · refresh · is-running
   — no stop. no disable.
 }
-  
and the FSM proves the absence, rather than relying on it

+

+
+

+  
Act II · the car

+  
… and the FSM proves the absence

   
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 itself cannot express the one transition the
-  proof forbids. That is the argument for putting the seam in a type
-  system rather than in a comment.

+  
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.

 

 
 

@@ -216,13 +225,19 @@ export function read32(addr) {
   const a = addr >>> 0;
   return a === TIM2_CNT ? clock : REGS[(a >>> 2) & 63];
 }
-  
on silicon — same import, answered by the bus

+

+
+

+  
Act III · the tires

+  
… and on silicon

+  
same import, answered by the bus

   
#[no_mangle] extern "C" fn read32(addr: u32) -> u32 {
     unsafe { core::ptr::read_volatile(addr as *const u32) }
 }

-  
That substitution is the entire thesis.

+  
Nothing else about the component changes.
+  That substitution is the entire thesis.

   

-    
seamA whole STM32 USART driver, dissolved326 B · 0 SRAM · 3 relocs

+    
seama whole STM32 USART driver, dissolved326 B · 0 SRAM · 3 relocs

   

 

 
@@ -371,17 +386,31 @@ export function read32(addr) {
   03            func_index  3
   07            value_id    7  ← a VALUE, not a position
   03 00 ff 0f   body: 0 ≤ v ≤ 2047   (sleb128)
-  
Keyed to values because an optimizer renumbers everything. Key a fact
-  to an instruction index and the next pass deletes three above it — the fact
-  is still true of something, and now asserted about something else. A fact whose
-  value did not survive is dropped, never re-pointed.

+

+
+

+  
Act IV · the factory

+  
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 factory

+  
What the channel is worth

   

     
measureda bounds-guard sequence, with the fact forwarded232 → 104 B

   

-  
Honest scope: the emitter, schema and wire format are done
-  and byte-verified against the consumer. The source that would populate
-  this at volume is not wired — 232→104 is what the channel does when it
-  carries a fact, not evidence that we produce many yet.

+  
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.

 

 
 

@@ -394,10 +423,15 @@ export function read32(addr) {
   both clamp branches are dead code:

   
add r0, #476
 bx  lr          — the whole function

+

+
+

+  
Act IV · the factory

+  
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 elided, correct only under the bound0.23 — 2.2× faster

+    
with the proofclamp elided0.23 — 2.2× faster

   

   
Soundness-gated: the bench asserts the elided form equals
   the native one across the proven range. LLVM never had the bound.

@@ -451,13 +485,17 @@ bx  lr          — the whole function
   
gpio   502 → 1196 B     spi  454 → 1244 B
 timer  204 →  828 B     wdg  638 → 1726 B
 .data / .bss, all of them   0 → 0

-  
and the response, measured for this talk

+

+
+

+  
Act V · what is missing

+  
So we patched the generator

+  
measured for this talk

   
wdg, canonical glue on a growing allocator   1746 B
      backed by a bounded arena instead        1428 B   −318

-  
So we patched the bindings generator rather than absorbing the cost:
-  cabi_realloc delegates to an embedder arena that traps instead of
-  growing. 29% of the overhead back — and the drivers do
-  not use it yet.

+  
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.

 

 
 

diff --git a/sass/_talk.scss b/sass/_talk.scss
index 885338a..2cfc96c 100644
--- a/sass/_talk.scss
+++ b/sass/_talk.scss
@@ -441,13 +441,14 @@
   .deck__btn { transition: none; }
 }
 
-// On a pointer device the deck is driven from the keyboard; keep the buttons
-// available but quiet until approached.
-@media (hover: hover) {
-  .deck__nav { opacity: .35; transition: opacity .2s ease; }
-  .deck:hover .deck__nav,
-  .deck__nav:focus-within { opacity: 1; }
-}
+// 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) ───────────────────────────────────────────────
 

From 4e9c38684fcced6ce65c1f677c70834402a8e516 Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier 
Date: Tue, 4 Aug 2026 22:41:31 +0200
Subject: [PATCH 12/56] =?UTF-8?q?talk:=20the=20fonts=20were=20never=20load?=
 =?UTF-8?q?ing=20=E2=80=94=20and=20a=20single-file=20export=20that=20needs?=
 =?UTF-8?q?=20no=20server?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

FONT BUG, and very likely the "works in Safari, not Edge" report. `_fonts.scss`
self-hosts the Atkinson faces, but it was never imported into main.scss — zero
@font-face rules in the compiled CSS. The site got away with it because
base.html also links Google Fonts; the deck template does not, so it silently
fell back to system fonts: SF Pro on Safari/macOS, Segoe UI on Edge/Windows.
Same HTML, different metrics, different look. Importing it gives 18 @font-face
rules and the deck now actually renders in the face it was designed for — the
same one on every browser.

It also closes the privacy regression `_fonts.scss` exists to prevent: the file
says in its own comment that self-hosting eliminates the Google Fonts auto-load
that transmits visitor IPs, and that elimination had never taken effect.

SINGLE-FILE EXPORT (tools/bundle-talk.py). A presentation should not depend on
a working local server, on the browser not upgrading a plain-HTTP LAN address to
HTTPS, or on anything between the laptop and the screen. The bundler inlines the
stylesheet, all 18 fonts as data URIs, and the terminal recording, producing one
632 KB HTML file with ZERO external or absolute references that opens from disk,
offline, in any browser. The player prefers an inlined recording over a fetch,
which fetch() would refuse on file:// anyway.

DRONE SLIDE. Pays off the forward reference on the bias slide. A drone is a car
with four rotors instead of four tires: the flight stack and the building
supervision system are built from the same ten no_std stream-transformer crates,
the same WIT packages, the same component rules, the same traceability gate. And
stated at the same resolution as the claim — neither has flown, neither has
shipped to a home, and the flight dossier says so itself: "no claim of flight is
made anywhere." Aim, not result.

30 slides, none overflowing.

Co-Authored-By: Claude Opus 5 
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
---
 .gitignore                              |  4 +++
 content/talks/wasm-research-day-2026.md | 19 +++++++++-
 sass/main.scss                          |  1 +
 templates/talk.html                     | 21 +++++++----
 tools/bundle-talk.py                    | 46 +++++++++++++++++++++++++
 5 files changed, 83 insertions(+), 8 deletions(-)
 create mode 100644 tools/bundle-talk.py

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/talks/wasm-research-day-2026.md b/content/talks/wasm-research-day-2026.md
index a44799e..b420520 100644
--- a/content/talks/wasm-research-day-2026.md
+++ b/content/talks/wasm-research-day-2026.md
@@ -46,7 +46,24 @@ slot = "25 + 5, remote"
     
   
   
The bias, declared: I work in automotive, so to me
-  everything is a car.

+  everything is a car. The substrate is not — next slide.

+

+
+

+  
Act I · the inversion

+  
A drone is a car with four rotors

+  
Same substrate, a different vehicle. The flight stack and a building-supervision
+  system are built from the same no_std stream-transformer
+  crates, the same WIT interface packages, the same component rules, the same
+  traceability gate.

+  

+    
flightcFS-derived stream components, SITL + emulation10 shared crates

+    
buildingsensor streams, monitors, alertingsame crates

+  

+  
Stated at the same resolution as the claim: neither
+  has flown, and neither has shipped to a home. The flight dossier says so in
+  its own words — "no claim of flight is made anywhere." This is the
+  outlook the substrate is aimed at, not a result.

 

 
 

diff --git a/sass/main.scss b/sass/main.scss
index b7a9f40..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";
diff --git a/templates/talk.html b/templates/talk.html
index faf3043..3bc79fd 100644
--- a/templates/talk.html
+++ b/templates/talk.html
@@ -208,13 +208,20 @@
     var btn    = box.querySelector('.cast__play');
     var evs = null, timers = [], playing = false;
 
-    fetch(box.dataset.cast)
-      .then(function (r) { return r.ok ? r.text() : Promise.reject(r.status); })
-      .then(function (t) { evs = parseCast(t); })
-      .catch(function () {
-        btn.textContent = 'recording unavailable';
-        btn.disabled = true;
-      });
+    // A single-file export inlines the recordings on window.__CASTS, so the
+    // deck works from file:// with no server and no network at all — where a
+    // fetch would be blocked by CORS.
+    if (window.__CASTS && window.__CASTS[box.dataset.cast]) {
+      evs = parseCast(window.__CASTS[box.dataset.cast]);
+    } else {
+      fetch(box.dataset.cast)
+        .then(function (r) { return r.ok ? r.text() : Promise.reject(r.status); })
+        .then(function (t) { evs = parseCast(t); })
+        .catch(function () {
+          btn.textContent = 'recording unavailable';
+          btn.disabled = true;
+        });
+    }
 
     function stop() { timers.forEach(clearTimeout); timers = []; playing = false; }
 
diff --git a/tools/bundle-talk.py b/tools/bundle-talk.py
new file mode 100644
index 0000000..e8f1a7b
--- /dev/null
+++ b/tools/bundle-talk.py
@@ -0,0 +1,46 @@
+#!/usr/bin/env python3
+"""Bundle a rendered talk into ONE self-contained HTML file.
+
+A served deck depends on a working local server, on the browser not upgrading a
+plain-HTTP LAN address to HTTPS, and on nothing between the laptop and the
+screen. A presentation should not depend on any of that. This inlines the
+stylesheet, the fonts and the terminal recordings so the result opens from disk,
+offline, in any browser.
+
+    python3 tools/bundle-talk.py talks/wasm-research-day-2026
+"""
+import base64, pathlib, re, sys
+
+root = pathlib.Path(__file__).resolve().parent.parent
+slug = sys.argv[1] if len(sys.argv) > 1 else "talks/wasm-research-day-2026"
+html = (root / "public" / slug / "index.html").read_text()
+css  = (root / "public" / "main.css").read_text()
+
+# Fonts -> data URIs, so there is nothing left to fetch.
+def embed_font(m):
+    name = m.group(1)
+    f = root / "public" / "fonts" / name
+    if not f.exists():
+        return m.group(0)
+    b64 = base64.b64encode(f.read_bytes()).decode()
+    return f'url(data:font/woff2;base64,{b64}) format("woff2")'
+css, n_fonts = re.subn(r"""url\(/fonts/([^)]+\.woff2)\)\s*format\((?:'|")woff2(?:'|")\)""", embed_font, css)
+
+# Recordings -> a JS object, because fetch() is blocked on file://
+casts = {}
+for m in re.finditer(r'data-cast=([^\s">]+)', html):
+    ref = m.group(1)
+    f = root / "public" / ref.lstrip("/")
+    if f.exists():
+        casts[ref] = f.read_text()
+cast_js = "window.__CASTS = {" + ",".join(
+    "%s:%s" % (repr(k), repr(v)) for k, v in casts.items()) + "};"
+
+html = re.sub(r']*main\.css[^>]*>', "", html, count=1)
+html = re.sub(r']*rel=icon[^>]*>', "", html, count=1)
+html = html.replace("