Expose Scheduling proofs (RTA/RMBound/EDF) as a reusable dependency for kiln-async's fuel-quantum scheduler

[avrabe]

Context

kiln's embedded async scheduler (kiln-async — no_std/no_alloc cooperative scheduler, REQ_ASYNC_SCHED / SM-ASYNC-001) plans to reuse spar's machine-checked scheduling theory for its bounded-latency / schedulability verification, rather than re-deriving it. The kiln design doc names this as headline reuse:

RTA iterN_le_fixed_point, RMBound, EDF → termination + WCRT + schedulability proofs

I surveyed proofs/Proofs/Scheduling/{RTA,RMBound,EDF}.lean and they are exactly what we need — fully proved (zero sorry/admit/axiom), parameterized over generic Nat cost units, so kiln-async's fuel quantum maps directly onto spar's exec unit. The directly-relevant results:

• bounded_mono_nat_seq (RTA.lean:123) + rta_terminates (RTA.lean:153) — fixed-point iteration terminates within deadline+1 steps.
• iterN_le_fixed_point (RTA.lean:174) — the converged value is the least fixed point (WCRT is not pessimistic).
• edf_two_tasks_demand (EDF.lean:88) — EDF feasibility from pairwise utilization; fully computational (no reals).
• rmBound_ge_ln2 (RMBound.lean:49) — Liu & Layland RM utilization bound.

This is forward-looking coordination, not a blocker: kiln-async is at Phase 1 (FIFO MVP, no deadline analysis yet). The reuse lands at kiln-async Phase 4 (fixed-priority + EDF modes) and Phase 5 (Lean+Aeneas refinement). Filing now so the dependency surface is shaped before we depend on it.

Asks (in priority order)

1. Make Proofs/Scheduling consumable as a stable dependency. Today it's the Proofs Lake library mixing all of spar's proofs. Could the scheduling theory be exposed as a stable, importable module boundary (a dedicated Lake package, and — since kiln's Lean toolchain integration runs through rules_lean — ideally a Bazel lean_library target) so kiln-async can depend on it without vendoring/copy-paste? A versioned/pinned boundary keeps a spar refactor from silently breaking kiln's proof gate.

2. A shared abstract task model (or a documented instantiation contract). RTA, EDF, and RMBound each define their own Task/TaskUtil struct. For a fuel-based consumer to instantiate cleanly we'd want either a single abstract task record the three modules share, or a short "how to instantiate with your own cost unit" note confirming the theorems are unit-agnostic (they appear to be — generic Nat). This is the difference between "import and instantiate" and "re-prove the glue."

3. Extend lake exe codegen to EDF/RM feasibility checks. Codegen.lean already extracts the proven RTA definitions to Rust (scheduling_verified.rs) — exactly the "verified code we can run/execute" path kiln-async wants. Could it be extended to also emit rm_schedulable (from RMBound) and edf_schedulable (from the demand-bound lemmas)? Then kiln-async's Phase-4 admission/feasibility test consumes spar-verified analysis instead of an unverified reimplementation.

What kiln owns (not asks of spar)

• The Rust→Lean refinement plumbing (Charon→Aeneas) is blocked in rules_lean (no charon_compile rule yet — kiln's risk R3); that's ours/rules_lean's, not spar's. Until it lands, kiln-async refines against your theorems via manual refinement statements, which is why a stable theorem API (ask Add semantic analysis layer, LSP server, WIT transform, and advanced analyses #1) matters now.

References

• kiln: docs/architecture/async-scheduler-plan.md (§6 verification plan, §9 reuse summary), REQ_ASYNC_SCHED, SM-ASYNC-001
• spar: proofs/Proofs/Scheduling/{RTA,RMBound,EDF}.lean, proofs/Codegen.lean

[avrabe]

Correction to the framing above (my "Charon not wired" claim was based on a stale local checkout):

Charon is wired in rules_lean — rules_lean#1 landed the hermetic charon_llbc rule + aeneas_translate on 2026-06-06, with an end-to-end tests/charon_llbc going real Rust → .llbc → Lean. So kiln-async's Rust→Lean refinement path is not blocked at the toolchain (kiln's risk R3 is closed).

That makes the asks here more actionable, not less: with the pipeline working, the gating factor for reuse is exactly ask #1 (a stable, importable Proofs/Scheduling boundary kiln-async can depend on) and ask #2 (the instantiation contract). We can refine kiln-async's Charon→Aeneas-translated Lean against your theorems as soon as they're consumable. Asks unchanged; priority on #1/#2 raised.

[avrabe]

Triaged into the rivet trace as REQ-PROOF-SCHED-002 (release v0.18.0), building on the already-shipped REQ-PROOF-SCHED-001.

Scope captured from the three asks here:

1. Expose Proofs/Scheduling as a stable importable boundary — a dedicated Lake package + a Bazel lean_library target (rules_lean) — so a spar refactor can't silently break kiln's proof gate.
2. Provide a shared abstract task model, or a documented "instantiate with your own cost unit" contract confirming the theorems are unit-agnostic (turning re-prove-the-glue into import-and-instantiate).
3. Extend lake exe codegen to emit rm_schedulable (RMBound) and edf_schedulable (EDF demand-bound) to Rust alongside the existing RTA extraction, so kiln-async's Phase-4 admission test runs spar-verified analysis.

Slotted at v0.18.0 to shape the surface before kiln-async depends on it (its Phase 4/5). This is the scheduling analog of the network-calculus substrate export in DEC-TSN-OSS-001 — concrete evidence for the cross-PulseEngine-substrate direction. Tracked in artifacts/requirements.yaml on the TSN-competitor roadmap (PR #274).