[avrabe]

First step on T3 (REQ-OS-SCHED-001), and the first gale Lean to land now that #288 made the proofs actually CI-checked.

What spar left to us

spar#331 delivered ArincSupply.lean (0 sorry/admit/axiom), which proves the inner response-time analysis sound conditional on

SupplyGuarantee sbf Π Θ  :=  ∀ t, lsbf Π Θ t ≤ sbf t

and states plainly that spar does not prove it — it is the partition scheduler's obligation, i.e. gale's. This is the arithmetic core of that discharge:

theorem lsbf_le_full_frames (Pi Theta t) (hPi : 0 < Pi) (hU : 2*Theta ≤ Pi+1) :
    lsbf Pi Theta t ≤ (t / Pi) * Theta

Why this shape

gust's major frame is static and cyclic — MajorFrame::check proves the windows tile [0, frame_len) with no gap, no overlap, every budget > 0 — so over any Π consecutive ticks a partition receives exactly its useful budget, and ⌊t/Π⌋·Θ is a sound floor on supply over any interval regardless of where it starts. This lemma shows that floor already dominates lsbf, so the discharge needs no reasoning about start offsets at all.

The hypothesis does real work: 2Θ ≤ Π+1 forces the blackout 2(Π−Θ) to be at least Π−1, hence at least the largest possible partial frame t % Π.

The hypothesis is proven necessary, not assumed

A machine-checked counterexample ships with it:

example : ¬ (lsbf 5 4 4 ≤ (4 / 5) * 4) := by decide

At Π=5, Θ=4 (so 2Θ = 8 > Π+1 = 6, and Θ < Π so not the degenerate case) the blackout is 2 and lsbf 5 4 4 = 1 > 0. Above one-half utilisation the conclusion is genuinely false — that regime needs a different argument, and it is not an artefact of how this proof was written. Same discipline as the CI gate: a hypothesis that has never been shown to bite is worth as little as a gate that has never failed.

Θ is Θ_eff, never the raw budget

Recorded in the file because it is the way to get this wrong. Switcher::tick fires at t == offset + budget - 1, so each owned window loses its final tick to ctx-save/region-swap/ctx-resume. A partition owning k windows receives Θ_eff = Θ − k.

Instantiating with the raw budget is unsound — lsbf's leading rate Θ/Π against a real rate (Θ−k)/Π — and it passes short tests. Exhaustive simulation over all worst-case start offsets:

frame	Π	Θ	k	first violation, raw Θ	with Θ_eff
one window	100	40	1	t = 2 560	none ≤ 6 000
two windows	100	50	2	t = 1 926	none ≤ 6 000
three windows	100	70	3	t = 828	none ≤ 6 000

More windows fails sooner, so splitting a budget to reduce blackout — the natural design move — makes the wrong instantiation fail faster.

Not the whole obligation

Stated in the file rather than glossed. Still owed:

• the supply-counting lemma from frame_inv (⌊t/Π⌋·Θ_eff ≤ real supply);
• the > ½ utilisation regime, which the counterexample above shows needs different reasoning;
• a side condition Lean cannot discharge: Θ_eff = Θ − k assumes the three-atom switch sequence completes within one tick — a WCET obligation on trusted native code, outside both BIN-VERIFY and MC/DC. It must be carried as an explicit hypothesis, in the same shape spar chose for SupplyGuarantee.

Verified locally bazel test //proofs/lean:all → 8 of 8. Rebased onto the #288 fix, so the Lean Proofs job here will actually check it — this is the first gale proof to land as gated evidence rather than locally-green.

🤖 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!