Skip to content

feat(gust): gust:os timer-sleep — tickless component sleep over the verified executor (VER-OS-TIMER-001 verified) - #202

Merged
avrabe merged 12 commits into
mainfrom
spec/gust-timer-sleep
Jul 21, 2026
Merged

feat(gust): gust:os timer-sleep — tickless component sleep over the verified executor (VER-OS-TIMER-001 verified)#202
avrabe merged 12 commits into
mainfrom
spec/gust-timer-sleep

Conversation

@avrabe

@avrabe avrabe commented Jul 21, 2026

Copy link
Copy Markdown
Contributor

gust:os timer-sleep — tickless component sleep

Gives a dissolved component an efficient tickless sleep(interval) by surfacing the executor's already-verified per-task deadline[] + next_deadline() + expire() path (no-lost-wakeups + bounded-poll, proven). Closes the two gaps: no wake-registration (→ busy-poll) and raw ticks (→ no time unit). Built via brainstorm → spec → plan → subagent-driven execution (6 TDD tasks, each task-reviewed, whole-branch reviewed READY TO MERGE, 0 critical).

What lands

  • Verified core (src/executor.rs): set_deadline(h, d) + slept_status(h, now) — Verus 1162/0 (+2), Kani set_deadline_sets_only_h SUCCESSFUL, verus-strip 2/2. No existing lemma modified; no assume/admit/external_body. The proof{} re-derives inv() from the unchanged state/ready via the existing lemma_inv_ready_implies_pending.
  • WIT seam (gust-os.wit): time.resolution() (ticks/sec, mmio) + gust:os/timer { sleep(handle: u32, ticks: u32), slept(handle: u32) } (executor-backed). handle is the app's spawn.start handle — the cooperative batch-drain executor has no ambient "current task" (user decision).
  • Provider (benches/gust/drivers/timer-provider): dissolves to a 1783 B cortex-m3 object exporting both sleep+slept, undefined = read32 only (1-atom mmio TCB; executor fns inlined). ticks: u32 (v1 bound < 2^31) works around synth's ARM-backend loud-decline of a u64 param in a frame-backing fn — filed synth#837.
  • Demonstrator (gust_timer_probe.rs, qemu): drives the real executor — next_deadline() == the single armed deadline (tickless), expire(deadline-1) no premature wake (no spin), expire(deadline) readies + slept_status 0→1, non-vacuity (invalid→0xFFFF_FFFF, fresh→0). Green.
  • rivet: REQ+VER-OS-TIMER-001 → verified (rivet validate PASS), with honest v1 scope.

Honest scope (v1)

Single partition/executor (the provider's Tasks table is a separate instance from spawn-provider's — cross-provider compose is a follow-on); ticks: u32 / < 2^31 (synth#837 workaround); qemu logic demonstrator (not silicon); polled handle (no .await); Rocq track excludes this module (Verus+Kani). The demonstrator proves the mechanism at the executor level; full app→WIT→provider compose is a v1 follow-on.

Design intent

This is the concrete "async from kiln" on-ramp — the .await-on-a-timer future's deadline finally has a home in the verified executor.

🤖 Generated with Claude Code

avrabe and others added 12 commits July 21, 2026 21:15
@avrabe @claude
spec(gust): gust:os timer-sleep capability design (approved)
3f07e95 
Tickless component sleep over the verified executor. Split seam (time+=resolution
mmio, new timer interface executor-backed), handle-based sleep/slept mirroring
spawn, resolution() for units, set_deadline as the one new verified-core function
(surfaces the executor's existing per-task deadline[]). Reuses the proven
next_deadline/expire no-lost-wakeups path unchanged. v1: single-partition,
sleep<2^31 ticks, qemu demonstrator. rivet REQ/VER-OS-TIMER-001 lead.

User-approved design (2026-07-21).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
@avrabe @claude
plan(gust): gust:os timer-sleep implementation plan (6 TDD tasks)
27dc2ad 
rivet-lead → verified-core set_deadline+slept (Verus/Kani/strip) → WIT seam →
timer-provider dissolve → gust_timer_probe tickless demonstrator → close.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
@avrabe @claude
rivet(gust): REQ/VER-OS-TIMER-001 — tickless component sleep (proposed)
ae4d5da 
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
@avrabe @claude
feat(gust): executor set_deadline + slept_status — surface the tickle…
0c6ada0 
…ss deadline (REQ-OS-TIMER-001)

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
@avrabe @claude
wit(gust): time.resolution + gust:os/timer interface + worlds (REQ-OS…
f85374d 
…-TIMER-001)

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
@avrabe @claude
wit(gust): timer.sleep(handle,ticks) — app passes its spawn handle (u…
0c55ca8 
…ser decision)

The executor is a cooperative batch-drain with no ambient current task, so sleep
targets an explicit handle (the one the app holds from spawn.start) and sets its
deadline via the verified set_deadline. Resolves the T4 integration unknown.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
@avrabe
spec(gust): sync timer.sleep to sleep(handle,ticks) (user decision)
9deaa2a
@avrabe @claude
feat(gust): timer-provider — executor-backed gust:os/timer, dissolves…
446e4f2 
… clean

Backs gust:os/timer (world timer-provider) with the same verified executor
deadline table spawn-provider/exec-provider dissolve: sleep(handle, ticks)
rejects ticks >= 2^31 then calls Tasks::set_deadline(handle, now()+ticks);
slept(handle) delegates directly to Tasks::slept_status. now() reads the
same TIM2_CNT register as time-provider via gust:hal/mmio.

Crate builds and componentizes cleanly (wasm-tools component new/validate
pass); neither export crosses the taskdisp/poll_task seam (dead-code
eliminated, confirmed via wasm-tools print — sole import is
gust:hal/mmio.read32, same TCB class as sibling providers).

Dissolve is partial: slept compiles clean via synth 0.49.0 (346 B, sole
undefined symbol read32). sleep is skipped by synth's ARM backend — a
reproducible, version-independent limitation (also hits synth 0.45.1, with
or without --native-pointer-abi/--no-optimize/loom) lowering a u64 param
through a function that also makes a call. Documented in RESULTS.md with
full command output; the app-timer wac-plug compose was not attempted since
half the interface is absent from native code.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
@avrabe @claude
fix(gust): timer.sleep ticks u64->u32 — dissolves clean (both exports…
063eef7 
…, 1-atom TCB)

synth's ARM backend loud-declines a u64 param in a frame-backing fn that makes a
call; v1 bounds ticks < 2^31 which fits u32, so the seam takes u32 ticks (widened
to u64 internally for the deadline). synth 0.49.0 now compiles BOTH sleep+slept
(1783 B, undefined = read32 only, executor fns inlined). Provider dissolve complete.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
@avrabe @claude
feat(gust): gust_timer_probe — tickless sleep/expire/slept demonstrat…
f951bec 
…ed on qemu (VER-OS-TIMER-001)

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
@avrabe @claude
release(gust): VER-OS-TIMER-001 verified — tickless component sleep c…
1e63291 
…losed

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
@avrabe
docs(gust): tighten REQ-OS-TIMER-001 'end to end' → executor-mechanis…
9dc326c 
…m level (whole-branch review)

The probe drives the executor natively; full compose is a v1 follow-on (VER
scope already discloses this). Accuracy fix per the merge-gate review.
@codecov

codecov Bot commented Jul 21, 2026

Copy link
Copy Markdown

Codecov Report

❌ Patch coverage is 0% with 11 lines in your changes missing coverage. Please review.

Files with missing lines Patch % Lines
plain/src/executor.rs 0.00% 11 Missing ⚠️

📢 Thoughts on this report? Let us know!

@avrabe
avrabe merged commit d969cb1 into main Jul 21, 2026
78 of 79 checks passed
@avrabe
avrabe deleted the spec/gust-timer-sleep branch July 21, 2026 23:07
This was referenced Jul 23, 2026
Merged
Closed
avrabe added a commit that referenced this pull request Jul 23, 2026
@avrabe @claude
fix(gust): time-provider missing resolution() — restores gust:os sysc…
72c40fc 
…all seam (REQ-OS-SYSCALL-001) (#213)

PR #202 (gust:os timer-sleep) added `resolution: func() -> u64` to the
`time` interface in wit-os/gust-os.wit but never updated the `time-provider`
crate's `impl Guest for P`, so it silently broke `cargo build` for
time-provider (E0046, missing trait item) — and with it BOTH tl-node
(build-os-tl.sh) and ts-node (build-os-ts.sh), since both import `time`.
This regression shipped on main because gust_timer_probe (#202's own demo)
drives the executor natively and never exercises the time-provider dissolve
path, so nothing caught it.

Adds resolution() returning a documented placeholder tick rate (1 MHz) —
TIM2_CNT here is a raw mocked counter with no real PSC/ARR clock-tree config
crossing this seam, so there is no genuine Hz to report yet.

With the fix, re-verified end to end on the CURRENTLY INSTALLED toolchain
(synth 0.49.0, loom 1.2.0, meld 0.41.3 — all post meld#326/synth#757 fixes):
  - build-os-tl.sh: os-tl-cm3.o text=2206 data=52 bss=3096 (5354B/8192)
  - gust_os_tl_probe (qemu): "gust-os-tl-probe OK: log==\"gust:os up\\n\",
    run()=0xA" — buffer-carrying log.line crosses the fused-memory boundary
    UNCORRUPTED, exit 0.
  - build-os-ts.sh: os-ts-cm3.o text=1612 data=40 bss=2584 (4236B/8192)
  - gust_os_ts_probe (qemu): "gust-os-ts-probe OK: poll==1", exit 0.


Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo

Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
@avrabe avrabe mentioned this pull request Jul 23, 2026
Merged
avrabe added a commit that referenced this pull request Jul 23, 2026
@avrabe @claude
ci(gust): syscall-seam WIT↔impl drift gate — build providers for wasm…
45702e5 
…32 (gale#214) (#220)

Closes the process gap that let #202 ship green: it added time.resolution() to
the gust:os WIT without the time-provider Guest impl (E0046), silently breaking
the gust_os_tl/ts dissolve until #213 caught it by hand. No workflow built the
provider crates, so the compile error never fired in CI.

This gate builds every gust:os provider/app crate for wasm32 (the dissolve
target) — a WIT method that outruns its Guest impl now fails RED. Cargo-only;
the wit-bindgen-generated Guest trait makes the compile the oracle. Red-tested:
injecting a method into the time interface without the impl reproduces
E0046 'not all trait items implemented'; the gate on main is green (8/8 crates).

Co-authored-by: Claude Opus 4.8 <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