feat(gust): execute the composite — the claim holds, and the gate that checked it did not - #250
Merged
Conversation
…one clock observed, not asserted (REQ-OS-COMPOSITE-EXEC-001)
v0.6.0 shipped "exactly one scheduler and one clock" for the fused gust:os
component on STRUCTURAL evidence only: import routing across the unbundled core
modules (build-fused-gustos.sh gate 4) and executor-source ownership
(build-gustos-components.sh). Nobody had ever called it. This runs it.
gustos-hostrun instantiates fused-gustos.component.wasm on wasmtime 42.0.2,
supplying its two residual imports from the host — a fake gust:hal/mmio register
file (so every clock read is host-answered and observable) and gust:os/taskdisp
(so a task can actually be dispatched and complete).
Result: the claims HELD. 21/21 checks, notably
- spawn.start(0xA5) = 0; exec.state(0) = 1 (pending); timer.sleep(0,500) = 0 —
one handle accepted by all three interfaces;
- poll-round dispatched poll-task(0) — the id the trusted seam receives IS the
handle spawn minted, and the task's 1 -> 2 (done) transition is agreed by
exec.state, spawn.poll and timer.slept;
- spawn and exec exhaust ONE 8-slot table jointly (8 distinct handles across
both, then 0xFFFF_FFFF from either) — two private tables would allow 8 each;
- timer.sleep performs exactly ONE clock read, and the deadline it installs is
that read's answer + ticks (measured by sweeping the fake clock under the
pure timer.slept query: flips 0->1 at 4500 for a read served 4000, ticks 500)
— re-verified after jumping the register to 900000, where it flips at 901000.
A harness nobody has watched fail is not a gate, so the script also composes two
negative controls from the same unmodified providers. Control 1 binds timer to a
SECOND exec-provider instance: the harness refutes it (5 checks fail). That shape
is invisible to every existing gate — same world, same 5 unbundled core modules,
same import routing, gate 4 computes n_disp=n_spawn=n_timer=1 and ACCEPTS it; the
second task table is `(instantiate 0)` appearing twice, and a count over MODULES
cannot see a count over INSTANCES. Control 2 (a second time-provider instance) is
recorded as the known blind spot: the provider is stateless and both instances
read the same register through the same host import, so they are one clock source
reached twice and are indistinguishable at the seam.
Also observed, and NOT fixed here (timer-provider is out of scope for this
change): timer.sleep returns 0 (success) for an out-of-range handle (8,
0xDEADBEEF) and for a Done handle, where wit-os/gust-os.wit specifies
0xFFFF_FFFF. set_deadline correctly no-ops, so the arm is silently lost — the
caller is told a wake was armed that will never fire. Reported as a WIT
return-contract deviation in a separate bucket; it does not bear on the
one-scheduler/one-clock property.
Host-engine execution only. Nothing here is claimed about the dissolved/native
path — that is the second rung of REQ-OS-COMPOSITE-EXEC-001.
Co-Authored-By: Claude <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
…t checked it did not REQ-OS-COMPOSITE-EXEC-001. v0.6.0 shipped "one scheduler, one clock" as a STRUCTURAL claim, established by import routing and source ownership. The composite had never been run. It has now, on wasmtime, and the claim was NOT refuted: spawn.start(0xA5) = 0 (not the invalid sentinel) exec.state(0) = 1 (pending) (recognised) timer.sleep(0, 500) = 0 (success) (same handle accepted) poll-round(1500) dispatched poll-task[0] <- timer's arming woke SPAWN's task then all three agree the task is done 21/21 checks. Corroborated independently: spawn and exec exhaust ONE 8-slot table jointly (two private tables would allow 8 each). The more valuable finding is about our own gate. Composing the SAME exec-provider twice — once for spawn, once for timer — produces a composite with byte-identical WIT, the same five core modules, and the same import routing. Two private task tables behind one facade. Every check in build-fused-gustos.sh accepted it, including the "one scheduler" check added in v0.6.0 and verified by hand at the time. The reason is now obvious and was not before: a count over MODULES cannot see a count over INSTANCES. The split composite instantiates module 0 twice. The gate now asserts every core module is instantiated exactly once, and that check refutes the split composite while passing the real one. Also found, reported not fixed: timer.sleep returns 0 (success) for an out-of-range handle, a garbage handle, and a completed task, where gust-os.wit specifies 0xFFFFFFFF. Tasks::set_deadline correctly no-ops, so the arm is silently lost — the caller is told a wake was armed that will never fire. Providers were out of scope for this task. The one-clock check is honest about its limits: it catches a different source register, an extra read during arming, a deadline not derived from the served value, and a timer that ignores a register jump. It does NOT distinguish two stateless instances of the same time provider reading the same register — that composite passes, and is one clock SOURCE reached twice. Co-Authored-By: Claude <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! |
avrabe
added a commit
that referenced
this pull request
Aug 6, 2026
…ve seen it (#254) #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 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 6, 2026
…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>
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
1 participant
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.
REQ-OS-COMPOSITE-EXEC-001. v0.6.0 shipped "one scheduler, one clock" as a structural claim — import routing and source ownership. The composite had never been executed. It has now, on wasmtime.The claim was not refuted
21/21. Independently corroborated:
spawnandexecexhaust one 8-slot table jointly — two private tables would allow 8 each.The finding that matters more: our gate could not have caught the opposite
Composing the same
exec-providertwice — once forspawn, once fortimer— yields a composite with byte-identical WIT (same md5 over imports+exports), the same five core modules, and the same import routing. Two private task tables behind one facade.Every check in
build-fused-gustos.shaccepted it — including the "one scheduler" check added in v0.6.0, which I verified by hand at the time and reported as sound.The reason is obvious in hindsight: a count over modules cannot see a count over instances.
The gate now asserts every core module is instantiated exactly once. It refutes the split composite and passes the real one. The harness is also a live gate — run against the split composite it fails 5 checks (
3d,3e,4c,4d,4e), so it is not a test that can only pass.Secondary: a real WIT contract deviation, reported not fixed
Tasks::set_deadlinecorrectly no-ops, so the arm is silently lost — the caller is told a wake was armed that will never fire. Providers were out of scope here.What the one-clock check does and does not catch
Catches: a different source register or offset; an extra read during arming; a deadline not derived from the value actually served; a timer that ignores a register jump (verified by jumping the register to 900000 and showing the deadline tracks to 901000).
Does not catch: two stateless instances of the same time provider reading the same register. That composite passes all 21 checks — and honestly, it is one clock source reached twice.
Not exercised: the dissolved/native path,
channel/io, 32-bit clock wraparound, multi-task interleaving, silicon.🤖 Generated with Claude Code
https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo