Add Lean4 proof kernel, scheduling analysis, and conformance tests#38
Open
Add Lean4 proof kernel, scheduling analysis, and conformance tests#38
Conversation
17 tools catalogued with capabilities, differentiators, and adoption potential. Overview doc references artifacts via [[TOOL-*]] links. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
22 AADL tools now catalogued. Key additions: Sireum HAMR (only tool generating Rust from AADL), Sireum Awas (security flow analysis), EMFTA (open-source FTA), COMPASS (ESA formal verification suite), MASIW (AFDX network analysis). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Tool comparison revealed a blind spot: original STPA only covered "spar does X wrong" not "spar lacks critical X, creating false confidence." New findings: - H-7: Analysis scope creates false confidence (RM-only scheduling) - H-8: Missing standard safety outputs (FTA/FMEA from EMV2) - UCA-17..20: Misleading verdict, no margin, no FTA, no cross-check - LS-9..12: Concrete scenarios (blocking masks deadline miss, etc.) - CC-15..18: Algorithm assumption checks, margin reporting - STPA-REQ-024..031: 8 new safety requirements (all not-implemented) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Implement STPA-REQ-024 through STPA-REQ-026 and STPA-REQ-031: - Response Time Analysis (RTA) with fixed-point iteration for exact worst-case response times including higher-priority interference - EDF feasibility check (U ≤ 1.0 for implicit-deadline tasks) - Margin reporting with warnings at <5% and critical at <1% - Analysis limitation documentation info diagnostic Scheduling analysis now produces RMA utilization bound, RTA per-task response times, and EDF feasibility — matching capabilities of Cheddar/MAST for the common fixed-priority preemptive case. 15 tests (was 9): rta convergence/divergence, EDF feasibility, margin warnings, explicit deadlines, limitation docs. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Machine-checked proofs of the mathematical theorems underlying spar's scheduling analysis (RTA, EDF, RM bound): RTA.lean (fully proven, 0 sorry): - ceilDiv/interference/totalInterference monotonicity - rtaStep monotonicity and fixed-point iteration convergence - bounded_mono_nat_seq: pigeon-hole termination argument - rta_terminates: RTA either finds fixed point or exceeds deadline - iterN_le_fixed_point: iterate ≤ any fixed point (least FP) EDF.lean (1 sorry): - demand_le_interval: single-task demand ≤ interval when U≤1 - totalDemand_le_nL: total demand bound - demandBound_at_period: exact demand at period boundaries - edf_two_tasks_demand: sorry (needs rational arithmetic) RMBound.lean (1 sorry): - rmBound_one: RM bound for n=1 is exactly 1.0 - rm_single_task: U≤1 for C≤T - rmBound_ge_ln2: sorry (needs calculus) Uses Mathlib for push_neg, linarith, positivity, norm_num. Zero runtime cost — proofs are build-time only. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Codegen.lean generates verified Rust from proven Lean4 definitions. Nine conformance tests verify the actual scheduling.rs math matches the Lean-proven reference at every decomposition level (ceil_div, interference, total_interference, rta_step, full RTA iteration). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
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.
Summary
sorryin RTA.lean)lake exe codegen) generates verified Rust from proven definitionsLean proofs (12 theorems proven)
ceilDiv_mono,interference_mono,totalInterference_mono,rtaStep_monobounded_mono_nat_seq— core pigeon-hole termination argumentrta_terminates— bounded bydeadline + 1iterationsrta_finds_least_fixed_point— converged result is minimalTest plan
lake exe codegengenerates valid Rustlake build)🤖 Generated with Claude Code