Ported DCQCN checker onto TraceSpec with mechanized replay soundness

lean/LeanGuard/DcqcnEventLog.lean

@@ -5,6 +5,7 @@ import LeanGuard.Shared.Csv
 import LeanGuard.Shared.Key
 import LeanGuard.Shared.Numeric
 import LeanGuard.Shared.Coverage
+import LeanGuard.Shared.TraceSpec
 import LeanGuard.Dcqcn.Semantics
 
 namespace LeanGuard.DcqcnEventLog
@@ -388,31 +389,78 @@ def step (lineNo : Nat) (g : Global) (r : Row) : Except String Global := do
 
       pure { g with src := g.src.insert r.endpointId srcSt' }
 
-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 r with
-          | .ok g' => pure g'
-          | .error e => throw (e, cov)
-        go g' (some (key r)) rs cov
-  go {} none rowsSorted {}
+structure ReplayState where
+  g : Global := {}
+  lastKey : Option (Nat × Nat) := none
+deriving Repr
+
+def stepRow (s : ReplayState) (r : Row) : Except String ReplayState := do
+  match s.lastKey with
+  | none => pure ()
+  | some pk => require r.srcLine (keyLt pk (key r)) "global key went backwards"
+  let g' ← step r.srcLine s.g r
+  pure { g := g', lastKey := some (key r) }
+
+def traceSpec : TraceSpec :=
+  { Row := Row
+    State := ReplayState
+    init := {}
+    step := stepRow }
+
+def observeCoverage (cov : CoverageState) (s : ReplayState) (r : Row) : CoverageState :=
+  recordCover (covTick cov) s.g r
+
+def replayCanonicalRowsWithCoverage (rows : List Row) (cov : CoverageState) :
+    Except (String × CoverageState) (ReplayState × CoverageState) :=
+  TraceSpec.replayWithObserverM traceSpec observeCoverage traceSpec.init rows cov
+
+theorem replayCanonicalRowsWithCoverage_sound {rows : List Row} {cov : CoverageState}
+    {s : ReplayState} {cov' : CoverageState} :
+    replayCanonicalRowsWithCoverage rows cov = .ok (s, cov') →
+      TraceSpec.Replay traceSpec traceSpec.init rows s := by
+  intro h
+  exact TraceSpec.replayWithObserverM_sound traceSpec observeCoverage h
+
+theorem replayCanonicalRows_preserves
+    {Inv : ReplayState → Prop}
+    (hstep : ∀ {s r s'}, Inv s → traceSpec.step s r = .ok s' → Inv s')
+    {rows : List Row} {s : ReplayState} :
+    TraceSpec.replayM traceSpec traceSpec.init rows = .ok s →
+      Inv traceSpec.init → Inv s := 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 s,
+        canonicalizeRows rows key (fun r => r.srcLine) = .ok rowsSorted ∧
+        TraceSpec.Replay traceSpec traceSpec.init rowsSorted s := 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 ⟨s, cov'⟩
+          simp [hrun] at h
+          exact
+            ⟨ rowsSorted
+            , s
+            , by simp
+            , replayCanonicalRowsWithCoverage_sound hrun ⟩
 
 def checkRows (rows : List Row) : Except String Unit := do
   match checkRowsWithCoverage rows with

lean/LeanGuard/Shared/TraceSpec.lean

@@ -96,6 +96,28 @@ theorem replayWithObserverM_sound
           simp [hstep] at h
           exact Replay.cons hstep (ih h)
 
+/--
+Coverage observation cannot change the verdict: instrumented replay agrees
+with plain replay on acceptance, the final replay state, and the error
+message — the observer only threads the coverage component.
+-/
+theorem replayWithObserverM_agrees
+    (observe : CoverageState → spec.State → spec.Row → CoverageState)
+    (s : spec.State) (rows : List spec.Row) (cov : CoverageState) :
+    Except.mapError Prod.fst
+        ((replayWithObserverM spec observe s rows cov).map Prod.fst) =
+      replayM spec s rows := by
+  induction rows generalizing s cov with
+  | nil =>
+      simp [replayWithObserverM, replayM, Except.map, Except.mapError]
+  | cons r rs ih =>
+      simp only [replayWithObserverM, replayM]
+      cases hstep : spec.step s r with
+      | error e =>
+          simp [Except.map, Except.mapError]
+      | ok s1 =>
+          exact ih s1 (observe cov s r)
+
 theorem Replay.preserves
     {Inv : spec.State → Prop}
     (hstep : ∀ {s r s'}, Inv s → spec.step s r = .ok s' → Inv s')