Mechanized LeanGuard replay lemmas.

lean/LeanGuard/AqmEventLog.lean

@@ -4,6 +4,7 @@ import LeanGuard.Shared.Check
 import LeanGuard.Shared.Csv
 import LeanGuard.Shared.Key
 import LeanGuard.Shared.Coverage
+import LeanGuard.Shared.TraceSpec
 import LeanGuard.Aqm.Semantics
 
 namespace LeanGuard.AqmEventLog
@@ -244,31 +245,66 @@ def recordCover (cov : CoverageState) (g : Global) (r : Row) : CoverageState :=
     | Strategy.red | Strategy.redEcn =>
         recordRedCover cov g e
 
-def checkRowsWithCoverage (rows : List Row) : CheckOutcome := do
-  let rowsSorted ←
-    match canonicalizeRows rows key (fun r => r.srcLine) with
-    | .ok rs => pure rs
-    | .error e => throw (e, {})
+def traceSpec : TraceSpec :=
+  { Row := Row
+    State := Global
+    init := {}
+    step := fun g r => step r.srcLine g (toEvent r) }
 
-  let rec go (g : Global) (prevKey : Option (Nat × Nat)) (rows : List Row)
-      (cov : CoverageState) : CheckOutcome := do
-    match rows with
-    | [] => pure cov
-    | r :: rs => do
-        let cov := covTick cov
-        let cov := recordCover cov g r
-        match prevKey with
-        | none => pure ()
-        | some pk =>
-            match require r.srcLine (keyLt pk (key r)) "global key went backwards" with
-            | .ok _ => pure ()
-            | .error e => throw (e, cov)
-        let g' ←
-          match step r.srcLine g (toEvent r) with
-          | .ok g' => pure g'
-          | .error e => throw (e, cov)
-        go g' (some (key r)) rs cov
-  go {} none rowsSorted {}
+def observeCoverage (cov : CoverageState) (g : Global) (r : Row) : CoverageState :=
+  recordCover (covTick cov) g r
+
+def replayCanonicalRowsWithCoverage (rows : List Row) (cov : CoverageState) :
+    Except (String × CoverageState) (Global × CoverageState) :=
+  TraceSpec.replayWithObserverM traceSpec observeCoverage traceSpec.init rows cov
+
+theorem replayCanonicalRowsWithCoverage_sound {rows : List Row} {cov : CoverageState}
+    {g : Global} {cov' : CoverageState} :
+    replayCanonicalRowsWithCoverage rows cov = .ok (g, cov') →
+      TraceSpec.Replay traceSpec traceSpec.init rows g := by
+  intro h
+  exact TraceSpec.replayWithObserverM_sound traceSpec observeCoverage h
+
+theorem replayCanonicalRows_preserves
+    {Inv : Global → Prop}
+    (hstep : ∀ {g r g'}, Inv g → traceSpec.step g r = .ok g' → Inv g')
+    {rows : List Row} {g : Global} :
+    TraceSpec.replayM traceSpec traceSpec.init rows = .ok g →
+      Inv traceSpec.init → Inv g := by
+  intro h hs
+  exact TraceSpec.replayM_preserves traceSpec hstep h hs
+
+def checkRowsWithCoverage (rows : List Row) : CheckOutcome :=
+  match canonicalizeRows rows key (fun r => r.srcLine) with
+  | .error e => .error (e, {})
+  | .ok rowsSorted =>
+      match replayCanonicalRowsWithCoverage rowsSorted {} with
+      | .error err => .error err
+      | .ok (_, cov) => .ok cov
+
+theorem checkRowsWithCoverage_sound {rows : List Row} {cov : CoverageState} :
+    checkRowsWithCoverage rows = .ok cov →
+      ∃ rowsSorted g,
+        canonicalizeRows rows key (fun r => r.srcLine) = .ok rowsSorted ∧
+        TraceSpec.Replay traceSpec traceSpec.init rowsSorted g := by
+  intro h
+  unfold checkRowsWithCoverage at h
+  cases hcanon : canonicalizeRows rows key (fun r => r.srcLine) with
+  | error e =>
+      simp [hcanon] at h
+  | ok rowsSorted =>
+      simp [hcanon] at h
+      cases hrun : replayCanonicalRowsWithCoverage rowsSorted {} with
+      | error err =>
+          simp [hrun] at h
+      | ok pair =>
+          rcases pair with ⟨g, cov'⟩
+          simp [hrun] at h
+          exact
+            ⟨ rowsSorted
+            , g
+            , by simp
+            , replayCanonicalRowsWithCoverage_sound hrun ⟩
 
 def checkRows (rows : List Row) : Except String Unit := do
   match checkRowsWithCoverage rows with

lean/LeanGuard/PfcEventLog.lean

@@ -4,6 +4,7 @@ import LeanGuard.Shared.Check
 import LeanGuard.Shared.Csv
 import LeanGuard.Shared.Key
 import LeanGuard.Shared.Coverage
+import LeanGuard.Shared.TraceSpec
 import LeanGuard.Pfc.Semantics
 
 namespace LeanGuard.PfcEventLog
@@ -156,31 +157,66 @@ def recordCover (cov : CoverageState) (g : Global) (r : Row) : CoverageState :=
     | Kind.pfcRecv => cov
   cov
 
-def checkRowsWithCoverage (rows : List Row) : CheckOutcome := do
-  let rowsSorted ←
-    match canonicalizeRows rows key (fun r => r.srcLine) with
-    | .ok rs => pure rs
-    | .error e => throw (e, {})
-
-  let rec go (g : Global) (prevKey : Option (Nat × Nat)) (rows : List Row)
-      (cov : CoverageState) : CheckOutcome := do
-    match rows with
-    | [] => pure cov
-    | r :: rs => do
-        let cov := covTick cov
-        let cov := recordCover cov g r
-        match prevKey with
-        | none => pure ()
-        | some pk =>
-            match require r.srcLine (keyLt pk (key r)) "global key went backwards" with
-            | .ok _ => pure ()
-            | .error e => throw (e, cov)
-        let g' ←
-          match step r.srcLine g (toEvent r) with
-          | .ok g' => pure g'
-          | .error e => throw (e, cov)
-        go g' (some (key r)) rs cov
-  go {} none rowsSorted {}
+def traceSpec : TraceSpec :=
+  { Row := Row
+    State := Global
+    init := {}
+    step := fun g r => step r.srcLine g (toEvent r) }
+
+def observeCoverage (cov : CoverageState) (g : Global) (r : Row) : CoverageState :=
+  recordCover (covTick cov) g r
+
+def replayCanonicalRowsWithCoverage (rows : List Row) (cov : CoverageState) :
+    Except (String × CoverageState) (Global × CoverageState) :=
+  TraceSpec.replayWithObserverM traceSpec observeCoverage traceSpec.init rows cov
+
+theorem replayCanonicalRowsWithCoverage_sound {rows : List Row} {cov : CoverageState}
+    {g : Global} {cov' : CoverageState} :
+    replayCanonicalRowsWithCoverage rows cov = .ok (g, cov') →
+      TraceSpec.Replay traceSpec traceSpec.init rows g := by
+  intro h
+  exact TraceSpec.replayWithObserverM_sound traceSpec observeCoverage h
+
+theorem replayCanonicalRows_preserves
+    {Inv : Global → Prop}
+    (hstep : ∀ {g r g'}, Inv g → traceSpec.step g r = .ok g' → Inv g')
+    {rows : List Row} {g : Global} :
+    TraceSpec.replayM traceSpec traceSpec.init rows = .ok g →
+      Inv traceSpec.init → Inv g := by
+  intro h hs
+  exact TraceSpec.replayM_preserves traceSpec hstep h hs
+
+def checkRowsWithCoverage (rows : List Row) : CheckOutcome :=
+  match canonicalizeRows rows key (fun r => r.srcLine) with
+  | .error e => .error (e, {})
+  | .ok rowsSorted =>
+      match replayCanonicalRowsWithCoverage rowsSorted {} with
+      | .error err => .error err
+      | .ok (_, cov) => .ok cov
+
+theorem checkRowsWithCoverage_sound {rows : List Row} {cov : CoverageState} :
+    checkRowsWithCoverage rows = .ok cov →
+      ∃ rowsSorted g,
+        canonicalizeRows rows key (fun r => r.srcLine) = .ok rowsSorted ∧
+        TraceSpec.Replay traceSpec traceSpec.init rowsSorted g := by
+  intro h
+  unfold checkRowsWithCoverage at h
+  cases hcanon : canonicalizeRows rows key (fun r => r.srcLine) with
+  | error e =>
+      simp [hcanon] at h
+  | ok rowsSorted =>
+      simp [hcanon] at h
+      cases hrun : replayCanonicalRowsWithCoverage rowsSorted {} with
+      | error err =>
+          simp [hrun] at h
+      | ok pair =>
+          rcases pair with ⟨g, cov'⟩
+          simp [hrun] at h
+          exact
+            ⟨ rowsSorted
+            , g
+            , by simp
+            , replayCanonicalRowsWithCoverage_sound hrun ⟩
 
 def checkRows (rows : List Row) : Except String Unit := do
   match checkRowsWithCoverage rows with

lean/LeanGuard/Shared/TraceSpec.lean

@@ -0,0 +1,134 @@
+import Std
+
+import LeanGuard.Shared.Coverage
+
+namespace LeanGuard.Shared
+
+universe u v
+
+/--
+Protocol-independent interface for replaying a canonicalized trace.
+
+The executable checker supplies a row type, replay state, initial state, and
+one partial transition function. Protocol modules instantiate this structure
+with their existing checker step functions.
+-/
+structure TraceSpec where
+  Row : Type u
+  State : Type v
+  init : State
+  step : State → Row → Except String State
+
+namespace TraceSpec
+
+variable (spec : TraceSpec)
+
+/-- Pure deterministic replay over an already-canonical row sequence. -/
+def replayM : spec.State → List spec.Row → Except String spec.State
+  | s, [] => .ok s
+  | s, r :: rs =>
+      match spec.step s r with
+      | .error e => .error e
+      | .ok s' => replayM s' rs
+
+/-- Declarative replay relation induced by the executable step function. -/
+inductive Replay : spec.State → List spec.Row → spec.State → Prop where
+  | nil {s} : Replay s [] s
+  | cons {s r s' rs s''} :
+      spec.step s r = .ok s' →
+      Replay s' rs s'' →
+      Replay s (r :: rs) s''
+
+/--
+Replay with a coverage observer. The observer is deliberately observational:
+it sees the pre-state and row, updates coverage, and cannot alter replay state
+or acceptance.
+-/
+def replayWithObserverM
+    (observe : CoverageState → spec.State → spec.Row → CoverageState) :
+    spec.State → List spec.Row → CoverageState →
+      Except (String × CoverageState) (spec.State × CoverageState)
+  | s, [], cov => .ok (s, cov)
+  | s, r :: rs, cov =>
+      let cov' := observe cov s r
+      match spec.step s r with
+      | .error e => .error (e, cov')
+      | .ok s' => replayWithObserverM observe s' rs cov'
+
+theorem replayM_sound {s : spec.State} {rows : List spec.Row} {s' : spec.State} :
+    replayM spec s rows = .ok s' → Replay spec s rows s' := by
+  induction rows generalizing s with
+  | nil =>
+      intro h
+      simp [replayM] at h
+      cases h
+      exact Replay.nil
+  | cons r rs ih =>
+      intro h
+      simp [replayM] at h
+      cases hstep : spec.step s r with
+      | error e =>
+          simp [hstep] at h
+      | ok s1 =>
+          simp [hstep] at h
+          exact Replay.cons hstep (ih h)
+
+theorem replayWithObserverM_sound
+    (observe : CoverageState → spec.State → spec.Row → CoverageState)
+    {s : spec.State} {rows : List spec.Row} {cov : CoverageState}
+    {s' : spec.State} {cov' : CoverageState} :
+    replayWithObserverM spec observe s rows cov = .ok (s', cov') →
+      Replay spec s rows s' := by
+  induction rows generalizing s cov with
+  | nil =>
+      intro h
+      simp [replayWithObserverM] at h
+      rcases h with ⟨hs, _⟩
+      cases hs
+      exact Replay.nil
+  | cons r rs ih =>
+      intro h
+      simp [replayWithObserverM] at h
+      cases hstep : spec.step s r with
+      | error e =>
+          simp [hstep] at h
+      | ok s1 =>
+          simp [hstep] at h
+          exact Replay.cons hstep (ih h)
+
+theorem Replay.preserves
+    {Inv : spec.State → Prop}
+    (hstep : ∀ {s r s'}, Inv s → spec.step s r = .ok s' → Inv s')
+    {s : spec.State} {rows : List spec.Row} {s' : spec.State} :
+    Replay spec s rows s' → Inv s → Inv s' := by
+  intro h
+  induction h with
+  | nil =>
+      intro hs
+      exact hs
+  | cons hrow htail ih =>
+      intro hs
+      exact ih (hstep hs hrow)
+
+theorem replayM_preserves
+    {Inv : spec.State → Prop}
+    (hstep : ∀ {s r s'}, Inv s → spec.step s r = .ok s' → Inv s')
+    {s : spec.State} {rows : List spec.Row} {s' : spec.State} :
+    replayM spec s rows = .ok s' → Inv s → Inv s' := by
+  intro h hs
+  exact Replay.preserves spec hstep (replayM_sound spec h) hs
+
+theorem replayWithObserverM_preserves
+    (observe : CoverageState → spec.State → spec.Row → CoverageState)
+    {Inv : spec.State → Prop}
+    (hstep : ∀ {s r s'}, Inv s → spec.step s r = .ok s' → Inv s')
+    {s : spec.State} {rows : List spec.Row} {cov : CoverageState}
+    {s' : spec.State} {cov' : CoverageState} :
+    replayWithObserverM spec observe s rows cov = .ok (s', cov') →
+      Inv s → Inv s' := by
+  intro h hs
+  exact Replay.preserves spec hstep (replayWithObserverM_sound spec observe h) hs
+
+end TraceSpec
+
+end LeanGuard.Shared