[avrabe]

gale#223 asked which interface drives a periodic control loop. I answered with the shape, and had to add "world app-timer is declared but has no implementation — you are on new ground". Writing it found the world was also wrong.

The world could not work as declared

before: world app-timer { import time; import timer; export run }

timer.sleep(handle, ticks) takes the handle the app holds from spawn.start — the WIT says so itself, in the app-ts note: "a handle it returns is the executor's own handle and means the same thing to timer.sleep".

With no spawn import, an app in this world cannot obtain a valid handle. The only path it can exercise is sleep's 0xFFFF_FFFF invalid-handle return. A tickless-one-shot-sleep slice that can only demonstrate the error path is not a slice.

after:  world app-timer { import time; import spawn; import timer; export run }

The example

app-timer/src/lib.rs — spawn.start → timer.sleep(h, 50) → poll timer.slept under a bounded budget. Component validates; imports exactly {time, spawn, timer}, exports run: func() -> u32.

It propagates 0xFFFF_FFFF unchanged rather than folding it into 0, so a caller can distinguish "not yet" from "never armed" — the same distinction #283 fixed in the provider, and it would be odd for the example to lose it.

What it deliberately does not do

It does not call exec.poll-round. Who drives the executor — timer ISR vs partition window — is the embedder's choice and gale has not settled it (#223 Q1). An app arms its wake and reports; the node decides when to poll. The header also carries the two measured caveats a real periodic budget needs:

• T4 static WCET bounds 3 of 31 functions today, so a 1 kHz budget from observation is an observation, not a bound;
• a partition owning k windows receives Θ − k, not Θ (proofs/lean/PartitionSupply.lean).

And the gate was not covering it

check-providers.sh had a hand-written CRATES list, so it cheerfully reported "all 8 provider/app crates … in sync" while never building app-timer. Same shape as the Lean gate's enumerated target list (#292).

Now discovered by glob over app-* / *-provider, with a FATAL if discovery finds nothing, and the legacy list deleted rather than left as a second source of truth.

before: all 8 crates       after: all 9 crates, app-timer included

🤖 Generated with Claude Code

https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!