feat(analysis): ARINC-653 partition-supply-derived inner RTA (REQ-RTA-ARINC-SUPPLY-001)

[avrabe]

Closes #331. Requirement REQ-RTA-ARINC-SUPPLY-001 → REQ-RTA-001 / REQ-PROOF-SCHED-001 / REQ-PROOF-ARINC653-001.

Threads bound inside an ARINC-653 partition run against the partition supply, not wall-clock. This adds Arinc653SupplyRtaAnalysis (crates/spar-analysis/src/arinc_supply.rs) that turns a periodic resource Γ = (Π, Θ) into a per-inner-task worst-case response-time bound, reusing the Lean-verified jittered+blocking recurrence unchanged.

The two paths

• (b) Supply-derived jitter J_i = 2(Π−Θ) (worst-case contiguous blackout), emitted as the busy-window w-form R = 2(Π−Θ) + w, sound under w ≤ Θ. The single call compute_response_time_jittered_blocking(C, deadline=Θ, jitter=0, B, hp=[(T,C,2(Π−Θ))]) returns Converged(w) ⟺ w≤Θ / Diverged ⟺ w>Θ — the divergence bound is the side-condition test.
• (c) Cooperative blocking B_i = max_{lp} C_j^seg, derived run-to-completion (C_j^seg = C_j) with a Poll_Segment_Time override.
• (d) Demand-vs-supply fallback when w>Θ: lsbf_Γ(t)=⌊Θ(t−2(Π−Θ))/Π⌋, R = min{t : rbf(t) ≤ lsbf(t)} via a monotone fixed point (efficient on ps-scale t). Unschedulable / ill-formed / extra-jitter+fallback → hard Error, never a silently-wrong bound.

No double-analysis

Inner threads are discovered by VP-tree containment with no Actual_Processor_Binding, so the ordinary RtaAnalysis skips them (unbound) and this pass is their sole analyzer — no contradictory blackout-ignoring wall-clock number. Pinned by integration_no_double_analysis_from_rta.

Oracle

Golden (Γ = 1000µs/300µs, blackout 1400µs): τ1/τ2/τ3 → 1520/1570/1570 µs in the busy-window w-form (form pinned in the assertion per #331's form note). Four fixtures: jitter path; w>Θ fallback (2567µs); unschedulable hard Error; extra-jitter decline. Plus lsbf-conservatism regression (τ3 → 1967µs). AADL-level integration test builds the two-level model and asserts the emitted bounds + no-double-analysis. spar-analysis lib suite: 913/913. Workspace clippy -D warnings: clean.

Lean (proofs/Proofs/Scheduling/ArincSupply.lean, 0 sorry)

• PROVEN: constant blocking folds into the release jitter (rtaStepJitteredBlocking_fold), so monotonicity + least-fixed-point convergence transfer from RTAJittered.lean by the same bounded_mono_nat_seq argument; lsbf monotone; conditional fallback soundness (fallback_sound_of_supply_guarantee).
• ASSUMED (not spar's proof): the OS delivers supply ≥ lsbf_Γ(t) — carried as the SupplyGuarantee Lean hypothesis. gust owns this contract.

Local Lean toolchain unavailable in this environment; the proof is gated by the proofs.yml CI job (lake build). The proofs mirror the already-verified RTAJittered.lean structure and are 0-sorry by construction.

Honesty caveats (docs)

Sound-WCET inputs only (no measured high-water-marks; companion synth#778); an unqualified proof assistant carries no tool-qualification credit by itself.

Falsification

Reverting J_i = 2(Π−Θ) → 0 drops the golden to the wall-clock 120/170/170 µs (blackout ignored) — golden_jitter_path_* fail. Reverting the w>Θ dispatch makes fixture2 emit an unsound jitter number instead of the conservative 2567µs fallback.

🤖 Generated with Claude Code

[github-actions]

Rivet verification gate

✅ 20/20 passed

	count
Passed	20
Failed	0
Skipped (no steps)	0

Filter: (and (= type "feature") (or (has-tag "v093") (has-tag "v0100")))

Failed artifacts

(none)

_{Updated automatically by tools/post_verification_comment.py. Source of truth: artifacts/verification.yaml.}

[codecov]

Codecov Report

❌ Patch coverage is 88.26185% with 52 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/spar-analysis/src/arinc_supply.rs	88.40%	51 Missing ⚠️
crates/spar-analysis/src/lib.rs	50.00%	1 Missing ⚠️

📢 Thoughts on this report? Let us know!