feat(proofs): Lean 4 proofs for latency monotonicity + ARINC 653 isolation#223
Merged
Conversation
…ation
Add two sorry-free Lean 4 proof files that close the formal verification
gap vs HAMR's Logika coverage on the same analyses:
- proofs/Proofs/Scheduling/Latency.lean: proves `latency_monotone` —
if every component WCET in path c1 is pointwise ≤ c2 (expressed as
`List.Forall₂ (· ≤ ·) c1 c2`), then `Latency s c1 ≤ Latency s c2`
for any sampling delay s. Includes helper lemmas for sum monotonicity
and single-element replacement, and two corollaries (cons-extension,
set-replacement).
- proofs/Proofs/Scheduling/Arinc653Isolation.lean: proves
`partition_isolation` — in a Major Frame schedule satisfying
`scheduleConformant`, a thread whose `ThreadBinding` differs from a
window's owning partition cannot execute within that window (ARINC
653P1-5 §3). Models execution as an abstract predicate to keep the
proof independent of scheduler internals.
Wire-up: both modules imported in proofs/Proofs.lean; no new Mathlib deps.
Artifacts: REQ-PROOF-LATENCY-001, REQ-PROOF-ARINC653-001,
TEST-PROOF-LATENCY, TEST-PROOF-ARINC653 added to artifacts/.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…oofs - latency_cons_le: replace omega with Nat.add_le_add_left/Nat.le_add_left (omega failed because List.sum is opaque to the omega tactic after simp) - list_sum_set_le succ case: extract hi'/he' explicitly instead of relying on simp-at-* + omega/simpa; avoids getElem proof-term unification issues - Arinc653Isolation: convert /-- ... -/ doc comment before `variable` to plain -- comments (Lean 4 does not permit doc strings on variable decls) Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
# Conflicts: # artifacts/requirements.yaml
…n lands on runners The new TEST-PROOF-LATENCY / TEST-PROOF-ARINC653 artifacts had `cd proofs && lake build` as their verification step. The rivet verification gate runs on `[self-hosted, linux, x64, rust-cpu]`, which has no Lean toolchain — `lake` isn't on PATH, so the gate failed. Smithy will install `elan` + Lean on the runners (parallel work). Until then, the gate runs a smoke check: file exists + sorry-free grep. The full `lake build` is still exercised by the dedicated `Lean proof typecheck (lake build)` CI workflow on every PR, so coverage is not lost. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Rivet verification gate✅ 16/16 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! |
# Conflicts: # artifacts/requirements.yaml
2 tasks
avrabe
added a commit
that referenced
this pull request
May 18, 2026
…runners have ELAN_HOME (#227) PR #223 landed a sorry-grep + file-exists workaround for TEST-PROOF-LATENCY and TEST-PROOF-ARINC653 because the smithy runners didn't have Lean on PATH for the rivet verification gate. Smithy's been since fixed (commit dfb0eed): `ELAN_HOME=/home/ralf/.elan` is now in every runner's env, ProtectHome=read-only protects ralf's shared elan state, and `lake --version` confirmed working on all 12 runners with Lean 4.29.0-rc6 + Lake 5.0.0-src. Reverts the workaround to the proper `cd proofs && lake build` step. The full Lean typecheck now runs inside the verification gate, not just as a sorry-free smoke. The dedicated "Lean proof typecheck (lake build)" CI workflow remains as defense-in-depth. Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
This was referenced May 18, 2026
avrabe
added a commit
that referenced
this pull request
May 20, 2026
v0.10.0 ships: **Mermaid emission (M1 + M2 + M3)** - spar-mermaid foundation crate with `emit_flowchart` (#220) - `spar emit --format mermaid` CLI subcommand (#222) - `emit_class_diagram` + `emit_requirement_diagram` + matching CLI flags `--format mermaid-class` / `mermaid-req` (#228) **Soundness deepening** - Lean 4 sorry-free proofs of end-to-end latency monotonicity and ARINC 653 partition isolation, alongside the pre-existing RTA / EDF / Network Calculus proofs (#223) - Kani BMC harnesses on generated-code AADL contract preservation (thread Period, port Direction, bus access right) — spar's Logika-equivalent strategy for verified codegen (#224) **Safety analysis** - EMV2 error-propagation traversal across the AADL connection graph (closes the #1 gap vs OSATE/HAMR in safety-case reviews) (#225) **Verification infrastructure** - Rivet-driven verification gate that executes every artifact's `fields.steps[].run` commands and posts a sticky PR comment with pass/fail counts and failed artifact IDs (#221) - Workflow tuning: gate timeout 30→60 min for future Mathlib-heavy workloads; TEST-PROOF-* stay on sorry-grep until lake cache lands (#227, #229, #230) **Chore** - Pruned stale dev artifacts (.playwright-mcp logs + dashboard-render PNGs) and tightened gitignore (#226) Bumps Cargo.toml + vscode-spar/package.json from 0.9.3 → 0.10.0. The release workflow's `check-versions` job enforces tag/Cargo/vsix agreement, so these must move together with the v0.10.0 tag push. Co-authored-by: Claude Opus 4.7 <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
Latency.lean— sorry-free proof that end-to-end flow latency is monotone in per-component WCETs (latency_monotone). Closes the formal verification gap that HAMR's Logika covers via symbolic execution on the same property but spar had no machine-checked proof for.Arinc653Isolation.lean— sorry-free proof of ARINC 653 temporal partition isolation (partition_isolation). Models execution as an abstract predicate parameterised over ascheduleConformantMajor Frame; proofs are independent of scheduler internals. Closes the gap vs Logika's ARINC 653 isolation checks.proofs/Proofs.lean; no new Mathlib dependencies added.REQ-PROOF-LATENCY-001,REQ-PROOF-ARINC653-001,TEST-PROOF-LATENCY,TEST-PROOF-ARINC653added toartifacts/.Gap closed vs HAMR/Logika
HAMR's Logika checks latency monotonicity and ARINC 653 isolation via symbolic execution on generated code — but those checks are tied to the HAMR code generator's output and do not produce transferable machine-checked proofs. This PR gives spar a standalone, Lean 4 / Mathlib-checked formal proof that the mathematical models behind the analyses are correct, independent of any code generator.
Test plan
lake build) — exercises both new modules as part ofProofs.lean; will fail if anysorryis present (post-build grep gate in.github/workflows/proofs.yml)sorryvia:cd proofs && grep -rn 'sorry' Proofs/Scheduling/Latency.lean Proofs/Scheduling/Arinc653Isolation.leanrivet validate— artifact IDs resolve cleanly (pre-existing line-1615 YAML parse error inverification.yamlis unrelated to this PR)🤖 Generated with Claude Code