feat(proofs): Lean 4 proofs for latency monotonicity + ARINC 653 isolation

artifacts/requirements.yaml

@@ -2057,6 +2057,33 @@ artifacts:
     status: implemented
     tags: [mermaid, cli, v0100]
 
+  # ── Lean formal proofs — v0.10.0 ────────────────────────────────────────
+
+  - id: REQ-PROOF-LATENCY-001
+    type: requirement
+    title: Lean 4 proof of end-to-end flow latency monotonicity
+    description: >
+      System shall include a sorry-free Lean 4 proof that end-to-end flow
+      latency is monotone in per-component worst-case execution times: if
+      every component WCET in path c1 is pointwise ≤ the corresponding WCET
+      in path c2, then Latency s c1 ≤ Latency s c2 for any sampling delay s.
+      Proof lives in proofs/Proofs/Scheduling/Latency.lean and is exercised
+      by the `lake build` CI gate.
+    status: implemented
+    tags: [proof, latency, lean, v0100]
+
+  - id: REQ-PROOF-ARINC653-001
+    type: requirement
+    title: Lean 4 proof of ARINC 653 partition isolation
+    description: >
+      System shall include a sorry-free Lean 4 proof that, in a conformant
+      ARINC 653 Major Frame schedule, a thread whose static binding differs
+      from a window's owning partition cannot execute within that window.
+      Proof lives in proofs/Proofs/Scheduling/Arinc653Isolation.lean and is
+      exercised by the `lake build` CI gate.
+    status: implemented
+    tags: [proof, arinc653, lean, v0100]
+
   # ── CI / Verification gate ──────────────────────────────────────────────
 
   - id: REQ-VERIFY-GATE-001

artifacts/verification.yaml

@@ -2640,6 +2640,53 @@ artifacts:
 
   # ── Mermaid emission ────────────────────────────────────────────────────
 
+  # ── Lean formal proofs — v0.10.0 ────────────────────────────────────────
+
+  - id: TEST-PROOF-LATENCY
+    type: feature
+    title: Lean 4 latency monotonicity proof typechecks sorry-free
+    description: >
+      proofs/Proofs/Scheduling/Latency.lean defines Latency (sum of
+      per-component WCETs plus a constant sampling delay) and proves
+      latency_monotone: if every component WCET in c1 is pointwise ≤ the
+      corresponding WCET in c2, then Latency s c1 ≤ Latency s c2. Verified
+      by `lake build` under Lean 4 v4.29.0-rc6 + Mathlib with no sorry.
+      Gate runs a sorry-free smoke check; full `lake build` is exercised by
+      the dedicated "Lean proof typecheck (lake build)" CI workflow.
+    fields:
+      method: automated-test
+      steps:
+        - run: "test -f proofs/Proofs/Scheduling/Latency.lean"
+        - run: "! grep -E '^[[:space:]]*sorry[[:space:]]*(--.*)?$' proofs/Proofs/Scheduling/Latency.lean"
+    status: passing
+    tags: [proof, latency, lean, v0100]
+    links:
+      - type: satisfies
+        target: REQ-PROOF-LATENCY-001
+
+  - id: TEST-PROOF-ARINC653
+    type: feature
+    title: Lean 4 ARINC 653 partition isolation proof typechecks sorry-free
+    description: >
+      proofs/Proofs/Scheduling/Arinc653Isolation.lean defines
+      PartitionSchedule, ThreadBinding, and the scheduleConformant predicate,
+      then proves partition_isolation: in a conformant schedule, a thread
+      bound to a different partition than a window's owner cannot execute
+      within that window. Verified by `lake build` under Lean 4 v4.29.0-rc6
+      + Mathlib with no sorry.  Gate runs a sorry-free smoke check; full
+      `lake build` is exercised by the dedicated "Lean proof typecheck (lake
+      build)" CI workflow.
+    fields:
+      method: automated-test
+      steps:
+        - run: "test -f proofs/Proofs/Scheduling/Arinc653Isolation.lean"
+        - run: "! grep -E '^[[:space:]]*sorry[[:space:]]*(--.*)?$' proofs/Proofs/Scheduling/Arinc653Isolation.lean"
+    status: passing
+    tags: [proof, arinc653, lean, v0100]
+    links:
+      - type: satisfies
+        target: REQ-PROOF-ARINC653-001
+
   - id: TEST-MERMAID-FLOWCHART
     type: feature
     title: Flowchart emitter produces correct Mermaid markup

proofs/Proofs.lean

@@ -12,9 +12,13 @@
 --   3. EDF optimality for implicit-deadline systems (Dertouzos 1974)
 --   4. Jittered RTA convergence (Tindell & Clark 1994) — PR #147
 --   5. Network Calculus min-plus closed-forms (Le Boudec & Thiran 2001)
+--   6. Flow latency monotonicity in component WCETs (Feiertag et al. 2009)
+--   7. ARINC 653 partition isolation (ARINC 653P1-5 §3)
 
 import Proofs.Scheduling.RTA
 import Proofs.Scheduling.RMBound
 import Proofs.Scheduling.EDF
 import Proofs.Scheduling.RTAJittered
+import Proofs.Scheduling.Latency
+import Proofs.Scheduling.Arinc653Isolation
 import Proofs.Network.MinPlus

proofs/Proofs/Scheduling/Arinc653Isolation.lean

@@ -0,0 +1,164 @@
+/-
+  ARINC 653 Partition Isolation — Formal Proof
+
+  Reference: ARINC Specification 653P1-5 §3 (Partitioning),
+  SAE AS5506C §14.5 (AADL ARINC653 annex).
+
+  ARINC 653 requires that the operating system enforce strict temporal
+  and spatial isolation between partitions. In the temporal domain this
+  means: during a partition's allocated window in the Major Frame, only
+  threads bound to *that* partition may execute.
+
+  We model:
+    * `Partition`  — an opaque identifier for a partition.
+    * `Thread`     — an opaque identifier for a thread.
+    * `Window`     — a time slot in the Major Frame; carries the id of
+                     the partition that owns the window.
+    * `PartitionSchedule` — the ordered list of (partition, window) pairs
+                     that make up one Major Frame.
+    * `ThreadBinding` — a function mapping each thread to its partition.
+    * `Executes`   — an axiomatised predicate: `Executes t w` means
+                     thread `t` runs during window `w`.
+
+  The isolation property: a conforming ARINC 653 schedule guarantees
+  that if a window is allocated to partition P, then no thread whose
+  binding is different from P can execute in that window.
+
+  We prove this from a single conformance hypothesis:
+    `scheduleConformant s binding` — every window in `s` only allows
+    threads bound to `w.partition` to execute.
+
+  This justifies the `arinc653_partition_isolation` check in
+  `crates/spar-analysis/src/arinc653.rs`.
+-/
+import Mathlib.Tactic
+
+namespace Spar.Scheduling.Arinc653
+
+/-! ## Type definitions -/
+
+/-- An opaque partition identifier. -/
+structure Partition where
+  id : Nat
+  deriving DecidableEq, Repr
+
+/-- An opaque thread identifier. -/
+structure Thread where
+  id : Nat
+  deriving DecidableEq, Repr
+
+/-- A time window in the Major Frame, allocated to a specific partition. -/
+structure Window where
+  /-- The partition that owns this window. -/
+  partition : Partition
+  /-- Slot index within the Major Frame (0-based). -/
+  slot : Nat
+  deriving DecidableEq, Repr
+
+/-- A Major Frame: an ordered list of (partition, window) pairs.
+    The pairing is redundant (window already carries its partition) but
+    mirrors the AADL `ARINC653::Module_Schedule` property structure,
+    which pairs each window with a partition reference. -/
+abbrev PartitionSchedule := List (Partition × Window)
+
+/-- Maps each thread to the partition it is statically bound to.
+    Corresponds to the `ARINC653::Partition_Identifier` property on
+    a virtual processor / process component in the AADL model. -/
+abbrev ThreadBinding := Thread → Partition
+
+/-! ## Execution predicate -/
+
+-- `Executes t w` is an abstract proposition: thread `t` runs during
+-- window `w`. We do not model *how* the OS schedules within a window;
+-- we only care about *which* partition's window a thread uses.
+-- We introduce this as a section variable so callers supply a concrete
+-- model if needed; all proofs work purely from the conformance hypothesis.
+variable (Executes : Thread → Window → Prop)
+
+/-! ## Conformance hypothesis -/
+
+/-- A schedule is conformant with a thread binding if, for every window
+    present in the schedule, no thread bound to a *different* partition
+    executes in that window. This is the machine-checkable form of
+    ARINC 653 §3's "partitioning" requirement. -/
+def scheduleConformant
+    (s : PartitionSchedule)
+    (binding : ThreadBinding) : Prop :=
+  ∀ (t : Thread) (w : Window),
+    (∃ p, (p, w) ∈ s) →
+    Executes t w →
+    binding t = w.partition
+
+/-! ## Helper lemmas -/
+
+/-- If the schedule is conformant and thread `t` executes in window `w`,
+    then `t`'s binding equals `w.partition`. -/
+theorem binding_eq_of_executes
+    {s : PartitionSchedule}
+    {binding : ThreadBinding}
+    (hconf : scheduleConformant Executes s binding)
+    {t : Thread} {w : Window}
+    (hmem : ∃ p, (p, w) ∈ s)
+    (hexec : Executes t w) :
+    binding t = w.partition :=
+  hconf t w hmem hexec
+
+/-- Contrapositive: if `t`'s binding differs from `w.partition`, and `w`
+    appears in the schedule, then `t` cannot execute in `w`. -/
+theorem not_executes_of_binding_ne
+    {s : PartitionSchedule}
+    {binding : ThreadBinding}
+    (hconf : scheduleConformant Executes s binding)
+    {t : Thread} {w : Window}
+    (hmem : ∃ p, (p, w) ∈ s)
+    (hne : binding t ≠ w.partition) :
+    ¬ Executes t w := by
+  intro hexec
+  exact hne (binding_eq_of_executes Executes hconf hmem hexec)
+
+/-! ## Main theorem -/
+
+/-- **Theorem — ARINC 653 Partition Isolation.**
+
+    Within a Major Frame `s` that is conformant with binding `binding`,
+    a thread `t` whose binding differs from window `w`'s owning partition
+    cannot execute during `w`.
+
+    Formally:
+      `scheduleConformant s binding →`
+      `w ∈ s →`
+      `w.partition ≠ binding t →`
+      `¬ Executes t w`
+
+    where membership is via the second component of the schedule pairs
+    (i.e. `∃ p, (p, w) ∈ s`). -/
+theorem partition_isolation
+    {s : PartitionSchedule}
+    {binding : ThreadBinding}
+    (hconf : scheduleConformant Executes s binding)
+    {t : Thread} {w : Window}
+    (hmem : ∃ p, (p, w) ∈ s)
+    (hne : w.partition ≠ binding t) :
+    ¬ Executes t w :=
+  not_executes_of_binding_ne Executes hconf hmem (Ne.symm hne)
+
+/-- Corollary: threads in *different* partitions cannot share a window.
+    If thread `t1` executes in window `w` and `t2` is bound to a
+    different partition than `t1`, then `t2` does not execute in `w`. -/
+theorem cross_partition_exclusion
+    {s : PartitionSchedule}
+    {binding : ThreadBinding}
+    (hconf : scheduleConformant Executes s binding)
+    {t1 t2 : Thread} {w : Window}
+    (hmem : ∃ p, (p, w) ∈ s)
+    (hexec1 : Executes t1 w)
+    (hne : binding t1 ≠ binding t2) :
+    ¬ Executes t2 w := by
+  have hb1 : binding t1 = w.partition :=
+    binding_eq_of_executes Executes hconf hmem hexec1
+  -- binding t2 ≠ w.partition: if it were equal, binding t1 = binding t2 via hb1,
+  -- contradicting hne.
+  have hne2 : binding t2 ≠ w.partition := fun h => hne (hb1.trans h.symm)
+  exact not_executes_of_binding_ne Executes hconf hmem hne2
+
+end Spar.Scheduling.Arinc653

proofs/Proofs/Scheduling/Latency.lean

@@ -0,0 +1,126 @@
+/-
+  End-to-End Flow Latency — Monotonicity in Component Execution Times
+
+  Reference: AADL AS5506C §12 (end-to-end flows); Feiertag et al.,
+  "A Compositional Framework for End-to-End Path Delay Calculation of
+  Automotive Systems", WATERS 2009.
+
+  We model an end-to-end flow as a `List ExecTime`, where each element
+  is the worst-case execution time (WCET) of one component along the path.
+  The aggregate latency is the sum of WCETs plus a fixed sampling delay
+  (one major frame period, also expressed as a `Nat`).
+
+  The key property: if every per-component WCET is pointwise non-decreasing
+  (i.e. the system is under higher load), the end-to-end latency cannot
+  decrease. This justifies spar-analysis's latency analysis pass — it
+  is sound to replace each component's WCET with a conservative upper
+  bound without underestimating the flow latency.
+
+  This justifies `compute_flow_latency` in
+  `crates/spar-analysis/src/latency.rs`.
+-/
+import Mathlib.Tactic
+
+namespace Spar.Scheduling.Latency
+
+/-! ## Type aliases -/
+
+/-- A worst-case execution time (non-negative, in picoseconds). -/
+abbrev ExecTime := Nat
+
+/-- An end-to-end flow is a sequence of component WCETs. -/
+abbrev FlowPath := List ExecTime
+
+/-- Time values (non-negative, in picoseconds). -/
+abbrev Time := Nat
+
+/-! ## Latency model -/
+
+/-- `Latency sampling path` is the sum of WCETs along `path` plus a
+    constant `sampling` delay (one major frame / hyper-period).
+    `sampling` accounts for the worst-case sampling jitter introduced
+    when the first component reads from an upstream periodic source. -/
+def Latency (sampling : Time) (path : FlowPath) : Time :=
+  sampling + path.sum
+
+/-! ## Helper lemmas -/
+
+/-- The sum of a list is monotone in each element: if every element of
+    `c1` is ≤ the corresponding element of `c2` (pointwise), then
+    `c1.sum ≤ c2.sum`. -/
+theorem list_sum_le_of_pointwise {c1 c2 : FlowPath}
+    (h : List.Forall₂ (· ≤ ·) c1 c2) : c1.sum ≤ c2.sum := by
+  induction h with
+  | nil => simp
+  | cons hle _ ih =>
+    simp only [List.sum_cons]
+    exact Nat.add_le_add hle ih
+
+/-- Latency is monotone in the sampling delay: increasing the sampling
+    delay increases (or preserves) the total latency. -/
+theorem latency_mono_sampling {s1 s2 : Time} (path : FlowPath)
+    (h : s1 ≤ s2) : Latency s1 path ≤ Latency s2 path := by
+  unfold Latency
+  exact Nat.add_le_add_right h _
+
+/-- Latency is monotone in the path: if every component WCET in `c1` is
+    ≤ the corresponding WCET in `c2`, then `Latency s c1 ≤ Latency s c2`. -/
+theorem latency_mono_path (s : Time) {c1 c2 : FlowPath}
+    (h : List.Forall₂ (· ≤ ·) c1 c2) :
+    Latency s c1 ≤ Latency s c2 := by
+  unfold Latency
+  exact Nat.add_le_add_left (list_sum_le_of_pointwise h) _
+
+/-! ## Main theorem -/
+
+/-- **Theorem — Latency Monotonicity.**
+
+    If every component's WCET in path `c1` is pointwise ≤ the corresponding
+    WCET in path `c2`, then the end-to-end latency under `c1` is ≤ the
+    latency under `c2`, regardless of the sampling delay.
+
+    Formally: `∀ i, c1[i] ≤ c2[i]  →  Latency s c1 ≤ Latency s c2`.
+
+    `List.Forall₂ (· ≤ ·) c1 c2` is the standard Mathlib spelling of
+    "pointwise ≤ on lists of the same length". -/
+theorem latency_monotone (s : Time) (c1 c2 : FlowPath)
+    (h : List.Forall₂ (· ≤ ·) c1 c2) :
+    Latency s c1 ≤ Latency s c2 :=
+  latency_mono_path s h
+
+/-- Corollary: adding a component to a flow never decreases its latency
+    (single-step extension). -/
+theorem latency_cons_le (s : Time) (e : ExecTime) (path : FlowPath) :
+    Latency s path ≤ Latency s (e :: path) := by
+  unfold Latency
+  simp only [List.sum_cons]
+  exact Nat.add_le_add_left (Nat.le_add_left path.sum e) s
+
+/-- Helper: `List.set i e' l` preserves all elements except position `i`. -/
+theorem list_sum_set_le {path : FlowPath} {i : Nat} {e' : ExecTime}
+    (hi : i < path.length) (he : path[i]'hi ≤ e') :
+    path.sum ≤ (path.set i e').sum := by
+  induction path generalizing i with
+  | nil => exact absurd hi (by simp)
+  | cons x xs ih =>
+    cases i with
+    | zero =>
+      simp only [List.set, List.getElem_cons_zero] at he
+      simp only [List.set, List.sum_cons]
+      exact Nat.add_le_add_right he _
+    | succ i' =>
+      simp only [List.set, List.sum_cons] at *
+      have hi' : i' < xs.length := Nat.lt_of_succ_lt_succ hi
+      have he' : xs[i']'hi' ≤ e' := by simpa [List.getElem_cons_succ] using he
+      exact Nat.add_le_add_left (ih hi' he') _
+
+/-- Corollary: replacing one component's WCET with a larger value
+    yields a larger or equal latency. -/
+theorem latency_replace_le (s : Time) (path : FlowPath)
+    (i : Nat) (e' : ExecTime)
+    (hi : i < path.length) (he : path[i]'hi ≤ e') :
+    Latency s path ≤ Latency s (path.set i e') := by
+  unfold Latency
+  exact Nat.add_le_add_left (list_sum_set_le hi he) _
+
+end Spar.Scheduling.Latency