Skip to content

close(v0.7.0): E1's V closes on a gated result, + the timer defect gets an artifact - #255

Merged
avrabe merged 2 commits into
mainfrom
close/e1-v-and-timer-defect
Aug 6, 2026
Merged

close(v0.7.0): E1's V closes on a gated result, + the timer defect gets an artifact#255
avrabe merged 2 commits into
mainfrom
close/e1-v-and-timer-defect

Conversation

@avrabe

@avrabe avrabe commented Aug 6, 2026

Copy link
Copy Markdown
Contributor

Two commits, reviewable separately.

1. REQ/VER-OS-COMPOSITE-EXEC-001verified

The evidence has been on main since #250. The V could not honestly close on it, because VER-OS-COMPOSITE-EXEC-001 requires:

run in CI on every change to any provider so the property cannot silently stop holding

…and nothing ran it. #254 wired it in. What closes here is a gate, not a run that happened once — which matters, because #254 also found that the previous "green" on this area came from a workflow whose path filter didn't cover the script it gates.

Recorded on the artifact: the handle crossing spawn → timer → exec, 21 passed / 0 FAILED, the joint 8-slot table exhaustion that distinguishes one table from two, and the negative control that must refute a two-scheduler composite.

Recorded because the checks pass anyway — the honest limits:

  • two stateless time-provider instances pass all 21 checks; both read the same register through the same host import, so they're indistinguishable at the seam. A second clock with a different source or offset is caught.
  • untouched: the dissolved path (REQ-OS-COMPOSITE-DISSOLVE-001), channel/io, 32-bit clock wraparound, multi-task interleaving, silicon.

2. FIND-OS-TIMER-SLEEP-CONTRACT-001 (new)

timer.sleep(8, 10)          -> 0   (id out of the 8-slot range)   spec: 0xFFFFFFFF
timer.sleep(0xDEADBEEF, 10) -> 0   (not a task id at all)         spec: 0xFFFFFFFF
timer.sleep(0, 10)          -> 0   (task already done)            spec: 0xFFFFFFFF

set_deadline correctly no-ops, so nothing is corrupted — the defect is the return value. The arm is silently lost and the caller believes a wake is scheduled that will never fire. On a failsafe path that's the difference between a missed deadline that is detected and one that isn't.

Reported-not-fixed in #250 (providers were out of scope), and until now it lived only in a PR body and a pinned count inside a CI step. A defect recorded nowhere is a defect nobody is tracking. The CI gate pins the count at 3 so a fourth fails the build — that bounds the blast radius, it doesn't fix these three.

Second commit: method: test is not an allowed value

Eight sw-verification artifacts carried a bare test, which warns and drops them out of any method-filtered query. All eight are script-driven executed tests, so automated-test is accurate rather than merely closest.

rivet validate: PASS, 341 → 333 warnings, invalid-method class now zero.

Oracle

rivet validate PASS throughout; the new finding adds no warnings.

Next

E2 — REQ-OS-COMPOSITE-DISSOLVE-001. It's the whole critical path for v0.7.0: T2 has no object to verify and T4 has nothing to bound until it lands, and T3 consumes T4.

avrabe and others added 2 commits August 6, 2026 06:32
…gets an artifact

REQ/VER-OS-COMPOSITE-EXEC-001 proposed -> verified.

The evidence existed on main since #250 but the V could not honestly close on it:
VER-OS-COMPOSITE-EXEC-001 requires "run in CI on every change to any provider so the
property cannot silently stop holding", and nothing ran it. #254 wired it in, so what
closes here is a gate, not a run that happened once.

Recorded on the verification artifact: the handle crossing spawn -> timer -> exec,
21 passed / 0 FAILED, the joint 8-slot table exhaustion that distinguishes one table
from two, and the negative control that must refute a two-scheduler composite.

Also recorded, because the checks pass anyway: two STATELESS time-provider instances
pass all 21 checks -- both read the same register through the same host import, so
they are indistinguishable at the seam. A second clock with a different source or
offset IS caught. And untouched: the dissolved path, channel/io, clock wraparound,
multi-task interleaving, silicon.

FIND-OS-TIMER-SLEEP-CONTRACT-001 (new): timer.sleep returns 0 (success) instead of
0xFFFFFFFF for an out-of-range id, a non-id, and an already-done task. set_deadline
correctly no-ops, so nothing is corrupted -- the defect is the RETURN VALUE. The arm
is silently lost and the caller believes a wake is scheduled that will never fire.
On a failsafe path that is the difference between a missed deadline that is detected
and one that is not.

It was reported-not-fixed in #250 (providers were out of scope there) and until now
lived only in a PR body and a pinned count in a CI step. A defect recorded nowhere is
a defect nobody is tracking. The CI gate pins the count at 3 so a fourth fails; that
bounds the blast radius, it does not fix these three.

rivet validate: PASS, 341 warnings before and after.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
…1 -> 333 warnings

The schema allows automated-test, manual-test, review, static-analysis,
formal-verification, simulation, inspection, walkthrough. Eight sw-verification
artifacts carried a bare 'test', which validates as a warning and silently drops them
out of any query that filters by method.

All eight are script-driven executed tests -- CI workflows or bench capture scripts --
so automated-test is the accurate value, not merely the closest one. VER-OS-WCET-EVT-001
and VER-OS-PARTITION-TENANT-001 run against silicon, but via scripts rather than a human
following steps, so they are automated-test too rather than manual-test.

Kept as its own commit: it is mechanical and touches seven artifacts this branch does
not otherwise change.

rivet validate: PASS, 341 -> 333 warnings, invalid-method class now zero.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
@codecov

codecov Bot commented Aug 6, 2026

Copy link
Copy Markdown

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!

@avrabe
avrabe merged commit e6eb123 into main Aug 6, 2026
62 checks passed
@avrabe
avrabe deleted the close/e1-v-and-timer-defect branch August 6, 2026 05:35
avrabe added a commit that referenced this pull request Aug 6, 2026
… 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
avrabe added a commit that referenced this pull request Aug 7, 2026
* feat(gust): E2 — the whole OS dissolves, and the seam survives it

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

* ci(gust): gate E2 — run the dissolve on every change that could break 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

* ci(gust): the dissolve gate needs ubuntu-24.04 — loom's binary won't 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

---------

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
avrabe added a commit that referenced this pull request Aug 7, 2026
…already drifted (#258)

* feat(gust): E2 — the whole OS dissolves, and the seam survives it

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

* ci(gust): gate E2 — run the dissolve on every change that could break 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

* ci(gust): the dissolve gate needs ubuntu-24.04 — loom's binary won't 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

* fix(gust): one gust:hal, not two — delete the vendored copy that had already drifted

benches/gust/drivers/wit-os/deps/hal/gust-hal.wit was a hand-vendored copy of the
canonical wit/gust-hal.wit, and it had ALREADY drifted: 158 lines against 173. Missing
from the OS-side copy were `interface wdg` (all six functions) and `world wdg-driver`.

That is not an arbitrary interface to lose. wdg is the six-functions-no-stop contract
the driver model is argued from -- the absence of `stop` IS the cannot-un-start safety
property -- and half the repo could not see it.

It did not bite yet, and I checked rather than assumed: all seven SHARED interfaces
(mmio, irq, gpio, timer, spi, uart, dma) are byte-identical, and the only consumer of
wdg is wdg-thin, which builds against the canonical copy. So the drift was additive and
nothing shipped is wrong. The danger was the NEXT edit: change a shared interface and
drivers and providers get built against different definitions of the same seam --
exactly what composition is supposed to make impossible.

Fixed by removing the duplicate rather than policing it. The 8 crates that built against
wit-os now resolve both packages:

    world: "gust:os/time-provider@0.1.0",  path: ["../wit", "../wit-os"]

Two details, both forced by real errors rather than guessed:
  - canonical FIRST. wit-bindgen parses path entries in sequence, so ["../wit-os",
    "../wit"] fails: wit-os is read before gust:hal exists.
  - the world must be QUALIFIED. With a path list there is no single main package to
    infer from ("There are multiple main packages").

Verified: 8/8 crates build, and the dissolved composite is BYTE-IDENTICAL to before
this change -- 7473 B, text 4792 / data 0 / bss 0, undefined exactly {poll-task,
read32, write32}, negative control still refused. A WIT-resolution change that moved
the artifact would not have been plumbing.

wit-os/deps/sched/gust-sched.wit stays vendored, correctly: gust:sched has no canonical
copy elsewhere, so it is already single-source.

Durable half: wit/ is in the gustos-dissolve workflow's path filter, so an edit to the
canonical seam now re-runs the dissolve instead of drifting unnoticed.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo

* measure(T4): the whole OS bounds 1 function of 31 — and not for the reason we planned

E2 made T4 possible for the first time (no object existed to bound). Running
synth --emit-wcet over the dissolved composite gives the honest coverage number:

  BOUNDED   1 of 31   (gust:os/time#deadline, 36 cycles)
  DECLINED 30

  callee-unbounded 11   a cascade -- resolves when the leaves do
  unmodeled-op      9   "op not classified by the cycle model"   <- synth
  loop              8   backward branch, no proven trip count    <- scry
  call              2   direct call to an import                 <- BY DESIGN

The `call` pair is not a gap: gust:os/time#now and poll_task are exactly the two
functions that reach the SEAM -- now calls the imported read32, poll_task calls the
embedder's dispatch. An intra-procedural bound SHOULD stop at an import whose cost
belongs to the host. The seam showing up in the WCET data is a good sign it is real.

THE FINDING: docs/releases/v0.7.0-plan.md named ONE T4 blocker -- "scry loop-bound
inference ... the one thing standing between per-function bounds and a schedulability
argument". That is no longer accurate. unmodeled-op (9) is LARGER than loop (8), and
emit-wcet.sh's own header documents only reason=call and reason=loop -- this third
category is absent from the track's written model of itself. Closing loop-bound
inference alone takes coverage from 1/31 to at most 9/31, not to a schedulability
argument. Plan corrected rather than left to be discovered at the gate.

Real work is 17 leaves (9 unmodeled-op + 8 loop); the 11 cascades come free.

FRICTION TO ROUTE (synth): the unmodeled-op declines do not say WHICH op --
{"reason":"unmodeled-op","note":"op not classified by the cycle model"} and nothing
else. Not actionable without bisecting by hand. Requested: name the offending opcode
(and ideally its offset). Recorded here because GitHub is down; file when it is back.

NOT claimed: this is not a WCET for the OS, not a partition budget, and no hardware
was involved. Per the track's own rule DWT may only falsify a model, never size one.
1/31 is a baseline, not a regression -- T4 had never been run against the composite.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo

* docs: link the T4 unmodeled-op finding to synth#921

The measurement and the plan both recorded the friction and said it would be filed
when GitHub came back. It is filed: synth#921, a follow-up to the closed synth#778
that shipped --emit-wcet. Both now point at it, so the local record and the upstream
record agree rather than drifting.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo

---------

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant