feat(gust): Kani-proven wrap-safe time-seam math (VER-OS-TIME-MATH-001, v0.5.1)

[avrabe]

What

v0.5.1 formal-hardening of the gust:os time capability, over the already-verified (test-level) VER-OS-SYSCALL-001. Extracts the deadline/elapsed arithmetic into a small Kani-proven verified core (drivers/os-time-math) that the time-provider binds to, instead of carrying the math inline.

Also fixes a latent correctness gap

The WIT documents time.elapsed as wrap-safe ("elapsed once now has passed it"), but the inline impl was now >= deadline — only correct in the non-wrapping window. The verified core uses the wrapping-difference half-range test (now.wrapping_sub(deadline) < 2^63) that is genuinely wrap-safe, and is a strict superset of >= in the practical non-wrapping regime (proven). At u64-µs the wrap is ~584,000 years out, so this is not a behavior change for real values — it just makes the impl match its documented contract, with a proof.

Kani (5/5, cargo kani)

• deadline_total_and_zero_is_now — deadline never panics/overflows; deadline(now,0)==now.
• fresh_deadline_not_elapsed — a just-set deadline is not elapsed for any real (0 < ticks < 2^63) delay.
• at_deadline_is_elapsed — elapsed(d,d) is true.
• advanced_to_deadline_is_elapsed — once now advances by the full delay, elapsed holds (wrap-safe across the domain).
• matches_plain_compare_without_wrap — agrees with >= whenever no wrap occurs.

Oracles

• cargo kani on os-time-math → 5/5 SUCCESSFUL.
• time-provider still builds for wasm32-unknown-unknown; the gale#214 provider drift gate stays green (8/8 crates).
• rivet validate → PASS (333 warnings, no new diagnostics); adds VER-OS-TIME-MATH-001 (verifies REQ-OS-SYSCALL-001).

Honest scope

Source-level proof over the pure math; the wasm→native dissolve of the provider remains differentially trusted, not proven equivalent (docs/safety/verification-honesty.md). This is additional evidence, not a claim that the whole seam is now formally verified end-to-end.

🤖 Generated with Claude Code

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!