Skip to content

fix(gust): the composite gate had a syntax error, and CI could not have seen it - #254

Merged
avrabe merged 1 commit into
mainfrom
fix/composite-gate-syntax-and-ci
Aug 6, 2026
Merged

fix(gust): the composite gate had a syntax error, and CI could not have seen it#254
avrabe merged 1 commit into
mainfrom
fix/composite-gate-syntax-and-ci

Conversation

@avrabe

@avrabe avrabe commented Aug 6, 2026

Copy link
Copy Markdown
Contributor

#250 found that a gate could not detect the thing it existed to guard. It shipped with the same defect one level up. Found by running the harness on main, not by reading it.

1. build-fused-gustos.sh does not parse on main

line 178: syntax error near unexpected token `&&'

The new instantiation-count block was inserted between a line-continuation \ and its && echo, orphaning the continuation. bash -n is clean on a9bbfbf~1, broken on a9bbfbf.

The script aborts at 178, so every check after it never ran — including the residual-import delivery invariant, which is the gate the v0.6.0 release notes tell people to verify with.

2. CI structurally could not have caught it

gustos-publish.yml's path filter lists build-gustos-components.sh but not build-fused-gustos.sh. None of the six files #250 touched matched the filter, so the workflow that runs the script never triggered. Its 61/61 green was real, and said nothing whatsoever about this change.

3. The harness swallowed the failure

build-fused-gustos.sh | tail -2 || exit 1 tests tail's status, not the script's. That is why a syntax error stayed quiet. Now checks PIPESTATUS[0].

Fixes

And the point: CI now executes the composite

VER-OS-COMPOSITE-EXEC-001 requires "run in CI on every change to any provider so the property cannot silently stop holding." Nothing ran it, so E1 was committed evidence, not a gate. This wires the harness and its negative controls in.

The harness exits 3, not 0 — claims held, but 3 WIT return-contract deviations (timer.sleep returns success for an out-of-range or already-done handle, so the arm is silently lost; reported-not-fixed in #250, providers were out of scope). A bare run: would have failed the step on a passing result. The gate accepts 3 only when the count is exactly 3, so a fourth deviation fails rather than hides.

Verified locally after the fix

bash -n                          16/16 scripts clean
E1                               21 passed, 0 FAILED — one-scheduler and one-clock HELD
negative control 1 (2 scheds)    16 passed, 5 FAILED, exit 1 — still a live gate
negative control 2 (2 clocks)    21 passed — the documented blind spot, recorded not gated

Follow-up, not in this PR

REQ/VER-OS-COMPOSITE-EXEC-001 stay proposed. Once this gate is green on main the V can close on gated evidence rather than committed evidence — and the timer.sleep deviation deserves its own artifact rather than a footnote in a verification note.

@avrabe @claude
fix(gust): the composite gate had a syntax error, and CI could not ha…
273c73f 
…ve seen it

#250's finding was that a gate could not detect the thing it existed to guard.
It shipped with the same defect one level up.

1. build-fused-gustos.sh does not parse. The new instantiation-count block was
   inserted BETWEEN a line-continuation backslash and its `&& echo`, orphaning the
   continuation:

       line 178: syntax error near unexpected token `&&'

   `bash -n` is clean on a9bbfbf~1 and broken on a9bbfbf. The script aborts at 178,
   so every check after it never ran -- including the residual-import delivery
   invariant, which is the gate the release notes tell people to trust.

2. CI structurally could not have caught it. gustos-publish.yml's path filter lists
   build-gustos-components.sh but not build-fused-gustos.sh. NONE of the six files
   #250 touched matched the filter, so the workflow that runs the script never
   triggered. Its 61/61 green was real and said nothing about this change.

3. run-gustos-hostrun.sh swallowed the failure. `build-fused-gustos.sh | tail -2 ||
   exit 1` tests tail's status, not the script's -- which is exactly why a syntax
   error stayed quiet. Now checks PIPESTATUS[0].

Fixes: reattach the continuation; extend the path filter to build-fused-gustos.sh,
run-gustos-hostrun.sh and gustos-hostrun/** (all six of #250's files now match); add
a `bash -n` gate over the 16 driver + silicon scripts, because this class is free to
catch; propagate the build failure.

And the one that was the point: CI now EXECUTES the composite. VER-OS-COMPOSITE-EXEC-001
requires "run in CI on every change to any provider so the property cannot silently
stop holding" -- until now nothing ran it, so E1 was committed evidence rather than a
gate. The step runs the harness and its negative controls.

The harness exits 3, not 0: claims held, 3 WIT return-contract deviations observed
(timer.sleep returns success for an out-of-range or already-done handle, so the arm is
silently lost -- reported not fixed in #250, providers were out of scope). A bare
`run:` would have failed the step on a passing result. The gate accepts 3 only when
the count is exactly 3, so a FOURTH deviation fails instead of hiding.

Verified locally after the fix:
  bash -n: 16/16 scripts clean
  E1: 21 passed, 0 FAILED -- one-scheduler and one-clock HELD under execution
  negative control 1 (two schedulers): 16 passed, 5 FAILED, exit 1 -- still a live gate
  negative control 2 (two stateless clocks): 21 passed -- the documented blind spot,
    recorded not gated

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 878a2ed into main Aug 6, 2026
63 checks passed
@avrabe
avrabe deleted the fix/composite-gate-syntax-and-ci branch August 6, 2026 04:23
@avrabe avrabe mentioned this pull request Aug 6, 2026
Merged
avrabe added a commit that referenced this pull request Aug 6, 2026
@avrabe @claude
close(v0.7.0): E1's V closes on a gated result, + the timer defect ge…
e6eb123 
…ts an artifact (#255)

* close(v0.7.0): E1's V closes on a GATED result, and the timer defect 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

* chore(rivet): method 'test' is not an allowed value — 8 artifacts, 341 -> 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

---------

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
@avrabe avrabe mentioned this pull request Aug 6, 2026
Merged
avrabe added a commit that referenced this pull request Aug 6, 2026
@avrabe @claude
ci(gust): gate E2 — run the dissolve on every change that could break…
d551d38 
… 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
@avrabe @claude
feat(gust): E2 — the whole OS dissolves, and the seam survives it (#257)
7609bba 
* 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
@avrabe @claude
fix(gust): one gust:hal, not two — delete the vendored copy that had …
8c05e55 
…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

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@avrabe