From a5db8ae9b04fd0833a525b76fac24f3d0c0f215d Mon Sep 17 00:00:00 2001 From: Baochun Li Date: Fri, 3 Jul 2026 06:06:01 -0400 Subject: [PATCH 1/2] Port DCQCN checker onto the generic TraceSpec interface Replace the hand-rolled recursive replay loop in checkRowsWithCoverage with the mechanized TraceSpec instance used by the AQM and PFC checkers: - ReplayState bundles the per-endpoint source/sink maps and pending CNP map (Global) with the last canonical key, so the in-loop global key monotonicity re-check ("global key went backwards") is preserved verbatim inside the new stepRow transition function. - stepRow / traceSpec / observeCoverage / replayCanonicalRowsWithCoverage mirror the AqmEventLog structure; coverage recording moves into the replayWithObserverM observer, ticking and hitting the same coverpoints in the same order. - Instantiation theorems replayCanonicalRowsWithCoverage_sound, replayCanonicalRows_preserves, and checkRowsWithCoverage_sound are near-verbatim applications of the generic TraceSpec lemmas. Observable behavior is byte-identical: stdout, stderr, exit codes, and --coverage-out JSON match the previous binaries on three simulator- generated traces (dcqcn_simple, dcqcn_1s, dcqcn_multi), a shuffled-rows accept case, six corrupted REJECT variants, and the aqm_dcqcn_check cross-layer runs over the same traces. Co-Authored-By: Claude Fable 5 --- lean/LeanGuard/DcqcnEventLog.lean | 98 +++++++++++++++++++++++-------- 1 file changed, 73 insertions(+), 25 deletions(-) diff --git a/lean/LeanGuard/DcqcnEventLog.lean b/lean/LeanGuard/DcqcnEventLog.lean index 2976a86f..a76a98ff 100644 --- a/lean/LeanGuard/DcqcnEventLog.lean +++ b/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 From b9112259cb535a2772e5d1f674f4816190ebf0e3 Mon Sep 17 00:00:00 2001 From: Baochun Li Date: Fri, 3 Jul 2026 08:34:37 -0400 Subject: [PATCH 2/2] Prove coverage observation cannot change the replay verdict Add replayWithObserverM_agrees to the generic TraceSpec interface: for any spec, observer, initial state, rows, and coverage state, Except.mapError Prod.fst ((replayWithObserverM spec observe s rows cov).map Prod.fst) = replayM spec s rows i.e. instrumented replay and plain replay agree on the verdict, the final replay state, and the error message; the observer only threads the coverage component. This upgrades the one-directional replayWithObserverM_sound story to full verdict equivalence. Proof is by induction on rows; #print axioms reports [propext, Quot.sound]. Co-Authored-By: Claude Fable 5 --- lean/LeanGuard/Shared/TraceSpec.lean | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/lean/LeanGuard/Shared/TraceSpec.lean b/lean/LeanGuard/Shared/TraceSpec.lean index 3cc67c3a..4188822f 100644 --- a/lean/LeanGuard/Shared/TraceSpec.lean +++ b/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')