feat(gust): E2 — the whole OS dissolves, and the seam survives it - #257
Merged
Conversation
v0.6.0 shipped the composed OS as 20 741 bytes and said plainly that this was a WASM
figure implying nothing about code size, SRAM or cycles. build-fused-gustos.sh
carried the same caveat in its own header: "NOT done here: lowering the composite to
native". It is done here.
fused-gustos.component.wasm 20741 B (wasm component)
-> meld fuse --memory shared -> loom optimize --passes inline
-> synth compile --target cortex-m3 --all-exports --relocatable
text 4792 data 0 bss 0 0 B of the STM32F100RB's 8192 SRAM
31 functions, 25 import-call relocations, 3 external symbols
Pinned to synth 0.52.0 (#208) rather than PATH, so the figure is comparable to what
is already recorded rather than to whatever happens to be installed.
THE GATE, and its direction. Undefined symbols must be EXACTLY the declared seam:
undefined (3): poll-task read32 write32
taskdisp gust:hal/mmio
Two ways to fail, and the second is the one worth stating: MORE than that means the
OS depends on something we never declared; an EMPTY set means the seam was inlined
away. That yields a smaller object and reads like a win, but an OS whose hardware
seam has been swallowed is no longer swappable -- which is the whole thesis. Exit 2.
The negative control BITES, and runs every invocation: wasm-kernel/fused.wasm lowers
with zero undefined symbols -- exactly the seam-swallowed shape -- and the gate
refuses it. If that control ever passes, the script exits 4, because a gate that has
stopped discriminating reports a green that means nothing. gale#254 is why this is in
the script rather than in my head.
NOT claimed, stated in the measurement doc rather than left to be assumed:
- 20741 -> 4792 is NOT a ratio. A wasm component carrying component metadata and a
.text section measure different things; quoting it as compression is the exact
conflation loom-across-the-fuse.md already had to correct once.
- bss 0 is zero STATIC allocation in the object, not "the OS needs no RAM".
Stacks and any arena come from the embedder.
- relocatable object, not a linked image -- it still needs the TCB bridge.
- NOT executed. E1 ran the component on a host engine; nothing has run this
object. Renode is E3, silicon is E4, both v0.7.1.
REQ-OS-COMPOSITE-DISSOLVE-001 proposed -> implemented, deliberately NOT verified:
nothing in CI runs this yet, so the property can still silently stop holding. That is
what VER-OS-COMPOSITE-DISSOLVE-001 asks for and it is the next commit.
This unblocks the rest of v0.7.0: T2 had no object to verify, T4 had nothing to
bound, and T3 consumes T4.
rivet validate: PASS, 333 warnings, unchanged.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
… the seam The dissolve existed as a script anyone could forget to run. VER-OS-COMPOSITE-DISSOLVE-001 asks for more than that: the seam property must not be able to silently stop holding. Its own workflow rather than a step in gustos-publish.yml, because this needs the full dissolve toolchain -- meld + loom + synth -- which NO gale workflow has ever installed. Keeping them apart means the cheap structural gate still runs in seconds on provider edits while this heavier one fires only when something that can change the dissolve moves. Toolchain by pinned RELEASE BINARY with checksum verification, not `cargo install --git`: faster, and the checksum is a gate rather than a hope. meld 0.41.3 / loom 1.2.0 / synth 0.52.0 -- the exact three that produced measurements/composite-dissolved.md, since a dissolve measured with a different compiler is not comparable to the recorded figure. The path filter covers build-fused-gustos.sh and build-dissolve-gustos.sh, not just the providers. gale#254 was precisely a filter that did not cover the script it gated, and a 61/61 green that said nothing about the change. Object drift is a WARNING, not a failure: if a provider change moves the committed object that is a real finding to review, not something to absorb silently or to block on. Also documented the script's exit 4 in its header -- the negative control passing is a distinct outcome from the gate failing, and it was implemented but unlisted. VER-OS-COMPOSITE-DISSOLVE-001 stays `proposed` in this commit. The gate has not run yet; marking it verified before it has is the mistake #254/#255 exists to prevent. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
…load on 22.04 First CI run of the E2 gate failed, and not in the gate: loom: /lib/x86_64-linux-gnu/libc.so.6: version `GLIBC_2.38' not found (required by loom) loom: /lib/x86_64-linux-gnu/libstdc++.so.6: version `GLIBCXX_3.4.31' not found loom v1.2.0's published x86_64-unknown-linux-gnu binary requires GLIBC 2.38; ubuntu-22.04 ships 2.35. meld 0.41.3 loaded fine on the same runner, so this is loom's binary specifically, not the toolchain approach. ubuntu-24.04 ships GLIBC 2.39 and GCC 13 (GLIBCXX 3.4.32), satisfying both. Worth noting the 'Versions actually in use' step did exactly what it is for: the failure is one legible line before the gate runs, rather than a confusing error from inside the dissolve. Keeping it. Reporting upstream separately -- a release binary that will not load on a currently supported GitHub runner is a portability problem for every consumer, not just us. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
v0.6.0 shipped the composed OS as 20 741 bytes and said plainly that this was a wasm figure implying nothing about code size, SRAM or cycles.
build-fused-gustos.shcarried the same caveat in its own header — "NOT done here: lowering the composite to native." It is done here.The result
Pinned to synth 0.52.0 (#208) rather than PATH, so the figure is comparable to what is already recorded rather than to whatever happens to be installed.
The gate, and its direction
Two ways to fail, and the second is the one worth stating:
The negative control bites, on every run.
wasm-kernel/fused.wasmlowers with zero undefined symbols — exactly the seam-swallowed shape — and the gate refuses it. If that control ever passes, the script exits 4, because a gate that has stopped discriminating reports a green that means nothing. #254 is why this lives in the script rather than in my head.Not claimed
Stated in
measurements/composite-dissolved.mdrather than left to be assumed:.textsection measure different things. Quoting it as compression is the exact conflationloom-across-the-fuse.mdalready had to correct once in this repo.bss 0is zero static allocation in the object, not "the OS needs no RAM" — stacks and any arena come from the embedder.Status
REQ-OS-COMPOSITE-DISSOLVE-001→implemented, deliberately notverified: nothing in CI runs this yet, so the property can still silently stop holding. That is whatVER-OS-COMPOSITE-DISSOLVE-001asks for, and CI has an established pinned-toolchain pattern (release-wasm.yml) to copy — next commit.What it unblocks
E2 was the critical path for everything left in v0.7.0:
REQ-OS-OBJVERIFY-001(T2)REQ-OS-WCET-001(T4)REQ-OS-SCHED-001(T3)rivet validate: PASS, 333 warnings, unchanged.