feat(proofs): Lean 4 proofs for latency monotonicity + ARINC 653 isolation#223
Open
avrabe wants to merge 4 commits into
Open
feat(proofs): Lean 4 proofs for latency monotonicity + ARINC 653 isolation#223avrabe wants to merge 4 commits into
avrabe wants to merge 4 commits into
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✅ 15/15 passed
Filter: Failed artifacts(none) Updated automatically by |
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