feat(proofs): reflection generator for scheduling_verified.rs (closes #321) - #336
Merged
Conversation
… reflect (#321) Milestone toward REQ-PROOF-SCHED-CODEGEN-001. The Expr→Rust reflector in Codegen.lean now reads the elaborated bodies of all five combinational recurrence defs and emits Rust matching the committed scheduling_verified.rs bodies exactly (verified locally via #eval, mathlib-free, <1s): interference -> ceil_div(r, period).saturating_mul(exec) rtaStep -> exec.saturating_add(total_interference(higher_priority, r)) interferenceJittered -> ceil_div(r.saturating_add(jitter), period).saturating_mul(exec) rtaStepJittered -> exec.saturating_add(jitter).saturating_add( total_interference_jittered(...)).saturating_add( total_isr_interference(...)) rtaStepJitteredBlocking -> rta_step_jittered(...).saturating_add(blocking) Handles the wrinkles: JitteredTask/JitteredHigherPriorityTask struct flattening to scalar params, the abstract isr:IsrOverhead function param (applied -> total_isr_interference fold call), and nested reflected-fn-calling-reflected-fn with argument flattening. Adds mathlib-free RTAJitteredCore.lean (extracted jittered/blocking defs). Not yet wired: whole-file emitter (main), byte-diff gate, RTAJittered/ ArincSupply dedup to import RTAJitteredCore, lakefile exe. WIP checkpoint. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…321) REQ-PROOF-SCHED-CODEGEN-001. `lake exe codegen` now GENERATES crates/spar-analysis/src/scheduling_verified.rs by REFLECTING the elaborated Lean `Expr` of the recurrence definitions (RTACore.lean + new mathlib-free RTAJitteredCore.lean) and lowering to Rust — the recurrence arithmetic is a function of the proven defs, not a hand-extraction. A byte-diff gate in proofs.yml fails on any drift. Honest reflected-vs-templated ledger: - REFLECTED from the Lean def bodies (drift-proof via the gate): interference, rta_step, interference_jittered, rta_step_jittered, rta_step_jittered_blocking — INCLUDING the jittered+blocking step spar actually runs (compute_response_time_jittered_blocking calls it), so the shipped analysis is generated, not manually extracted. - TEMPLATED trusted base (property-test-gated, named): ceil_div (leaf idiom a.div_ceil(b)); the summation folds (List.brecOn doesn't reflect cleanly — their bodies just loop the reflected interference*); the compute_response_time* fixed-point drivers + RtaResult (no executable Lean counterpart — the Lean side is iterN + convergence theorems; the driver is the Lean↔Rust boundary, justified by those theorems). Mechanism: exprToRust walks the Expr with a sound Nat→u64 lowering table (add/mul/sub → saturating_*), ceilDiv → ceil_div, struct flattening (Task/JitteredTask projections → scalar params via a defeq-keyed env), the abstract isr:IsrOverhead fvar (applied → total_isr_interference), and nested reflected-fn-calling-reflected-fn with arg flattening. Also: extracted mathlib-free RTAJitteredCore.lean and deduped the jittered defs out of RTAJittered.lean + ArincSupply.lean (import Core; theorems unchanged, proved over the same defs). Restored the codegen lakefile exe. Verification: lake exe codegen == committed (byte-identical); the gate is non-vacuous (a stray hand-edit turns it red); 15/15 scheduling_verified property tests; all 12 pub fns present. Full Lean re-verify + gate are CI-gated (proofs.yml). Closes #321. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
A clean-room review confirmed "closes #321" is defensible (decisive mutation test: change the Lean recurrence def → the emitted Rust changes; the jittered+blocking step spar runs is genuinely reflected). It flagged three honesty items, all fixed here: 1. RTACore.lean header still read "not yet generated / a future generator / #321 OPEN" — false on this branch (claim-drift in the closing commit). Now states it is GENERATED via reflection, #321 CLOSED. 2. Requirement ledger called the trusted-base gate "property tests" — they are example-based unit + differential-conformance tests (rta.rs's rta_conformance_systematic sweep), not proptest. Reworded accurately. 3. The templated jittered fold total_interference_jittered was only tested with 0/1-element HP lists (a dropped-tail bug would pass). Added jittered_fold_multi_element (2 HP tasks, sum=7) to the emitter's test template and regenerated — closes the gate hole. 16/16 tests now. Generator output remains byte-identical to the committed file (gate green); all 12 pub fns present. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Rivet verification gate✅ 20/20 passed
Filter: Failed artifacts(none) Updated automatically by |
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #321.
REQ-PROOF-SCHED-CODEGEN-001(verified). Builds on the v0.29.0 foundation (REQ-PROOF-SCHED-SPEC-SOURCE-001).lake exe codegennow GENERATEScrates/spar-analysis/src/scheduling_verified.rsby reflecting the elaborated LeanExprof the recurrence definitions (RTACore.lean+ new mathlib-freeRTAJitteredCore.lean) into Rust. A byte-diff gate inproofs.ymlfails on any drift. This retires #321's "manual extraction" line: the recurrence arithmetic is now a function of the proven defs, not a hand-transcription.Honest reflected-vs-templated ledger
REFLECTED from the Lean def bodies (drift-proof via the gate — change the Lean formula and the emitted Rust changes):
interference,rta_step,interference_jittered,rta_step_jittered,rta_step_jittered_blocking. This includes the jittered+blocking step spar actually runs (compute_response_time_jittered_blockingcalls it), so the shipped analysis is generated, not hand-extracted.TEMPLATED trusted base — named explicitly, gated by example/conformance tests (not reflection):
ceil_div(leaf idioma.div_ceil(b)); the summation folds (List.brecOndoesn't reflect cleanly — their bodies just loop the reflectedinterference*); thecompute_response_time*fixed-point drivers +RtaResult(no executable Lean counterpart — the Lean side isiterN+ convergence theorems; the driver is the Lean↔Rust boundary, theorem-justified).Mechanism
exprToRustwalks theExprwith a sound Nat→u64 lowering (add/mul/sub→saturating_*),ceilDiv → ceil_div, struct flattening (Task/JitteredTaskprojections → scalar params via a defeq-keyed env), the abstractisr : IsrOverheadfvar (applied →total_isr_interference), and nested reflected-fn-calling-reflected-fn with arg flattening.Verification
lake exe codegenoutput is byte-identical to the committed file; the gate is non-vacuous (a stray hand-edit turns it red — tested).scheduling_verifiedconformance tests (incl. a new multi-element jittered fold test); all 12pub fnpresent (regen-deletes-code guard).rtaStepin the Lean → emittedrta_stepgains.saturating_add(exec)); all 6 checks PASS; 3 flagged honesty items fixed in the last commit.RTAJitteredCoredefs) + the freshness gate are CI-gated (proofs.yml).🤖 Generated with Claude Code