feature: the DD-025 evidence gale asked for — on shipped gale-nano 0.7.0 the CLOCK does not advance (AFD-047)

[avrabe]

The DD-025 evidence gale asked for

gale answered the periodicity question on gale#223, fixed world app-timer (it was missing spawn, so no valid handle was obtainable), shipped a worked example — and left one thing explicitly open: who drives the executor, inviting jess's integration to force the answer.

jess built that integration. The answer is sharper than the question.

5 of 6 hold, including the control

property
deadline(t0,1) != t0	PASS — the clock does real arithmetic on our argument
spawn.start(0)	PASS — returns a handle, not the INVALID sentinel
timer.sleep(h,1)	PASS — reports armed (0)
timer.slept(h)	PASS — defined state, not INVALID
sleep(INVALID,1) == INVALID	PASS — negative control
time::now() advances	FAIL — constant 36 across 1000 spins

And an armed wake never fires: 10,000 polls made, slept() = 0 (pending) throughout.

The negative control is what makes this reportable. sleep(INVALID) correctly returns the sentinel, so gale-nano is not a stub returning 0 for everything — the timer logic is real, the time source is absent. Without that control this would be worthless.

Two wrong explanations, tested and discarded before reporting

1. "jess's HAL stub freezes it." The stub returns a value derived from the address — constant per address — so an MMIO-backed counter couldn't tick. I built a ticking variant (app/gust-hal-tick). The clock is still frozen, so gale's now() does not read through gust:hal/mmio. Observation right, mechanism wrong.
2. "the executor just needs driving." I called exec.poll-round from the app — first with now(), then with a synthetic advancing clock, since poll-round takes time as an argument and that suggested the caller supplies it. The wake still never fired.

So an application cannot make its own wake fire on the shipped runtime by any means available to it in pure wasm. Something outside the component graph must supply time. The open DD-025 question isn't only who drives the executor — it's who supplies the clock.

Version caveat, and it's load-bearing

gale's fix (7f09ada) merged today and is not in v0.7.0 (released 08-26). This tests a pre-fix runtime. So this is a question to gale, not a defect report — filing against a version that predates the fix is exactly the meld#390 mistake, and I'm not repeating it.

Two self-inflicted vacuities caught in the probe itself

• The poll loop broke on both an INVALID handle and exhaustion, and both produced elapsed_at == 0 — conflating "polled 10,000 times, never fired" with "bailed at poll 0". It now reports polls-actually-made: 10,000, so this is exhaustion.
• A refactor dropped the semantics flags from the packed return, so the decoder read the poll count as the flags and printed a coincidental PASS on bit 4. Fields now occupy disjoint bit ranges. Overlapping fields is how a probe lies.

tools/timer-probe/run.sh decodes rather than asserts — the informative outcome is that five properties hold and one does not, and a pass/fail oracle would have said "fail" and taught nothing.

🤖 Generated with Claude Code

https://claude.ai/code/session_017EKh2onUHpWSUiAEqWxfy2