Ported DCQCN checker onto TraceSpec with mechanized replay soundness#98
Merged
Conversation
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 <noreply@anthropic.com>
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 <noreply@anthropic.com>
Collaborator
Author
|
Added commit b911225: a generic kernel-checked lemma |
baochunli
changed the title
baochunli
added a commit
that referenced
this pull request
Jul 4, 2026
…ace. (#99) * Port CUBIC checker onto the generic TraceSpec interface Replace the hand-rolled checkRowsWithCoverage replay loop with a ReplayState wrapper and a TraceSpec instantiation, mirroring the DCQCN port (#98). The existing step/recordCover/key/canonicalizeRows semantics are reused unchanged, and the per-row global-key monotonicity check is preserved inside stepRow. Soundness and preservation lemmas delegate to the generic TraceSpec proofs, so no new proof obligations are introduced; the build elaborates them. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Port DRR checker onto the generic TraceSpec interface Replace the checkRowsWithCoverage replay loop with a ReplayState wrapper and a TraceSpec instantiation, following the DCQCN template. step is fed via toEvent and recordCover reads the pre-step Global, exactly as before; the global-key monotonicity check moves into stepRow. Soundness/preservation lemmas delegate to the generic TraceSpec proofs. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Port WFQ checker onto the generic TraceSpec interface Replace the checkRowsWithCoverage replay loop with a ReplayState wrapper and a TraceSpec instantiation. WFQ's coverage observer previously threaded a distinct-class accumulator (seenClasses) that lived outside both Global and CoverageState. To keep observeCoverage self-contained and uniform with the other five checkers, thread it through a generic 'seen : Std.HashSet Nat' scratch field added to the shared CoverageState (with covSeen and a covMerge union). The field is never serialized, so coverage reports and golden fixtures are unchanged. class_count_ge_2 now gates on cov.seen.size >= 2, equivalent to the old distinct-list length; the now-dead listContains helper is removed. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
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
Ports the DCQCN checker from its hand-rolled recursive replay loop onto the generic
TraceSpecinterface, matching the existing AQM and PFC structure, with byte-identical observable behavior. Follow-up to #97, which mechanized the generic replay lemmas.DCQCN is the flagship protocol of the LeanGuard paper (largest benchmark trace, generation campaign, schema examples), so bringing it inside the mechanized scope directly strengthens the paper's answer to the SIGCOMM reviewers' mechanization question.
Changes
lean/LeanGuard/DcqcnEventLog.lean(only file changed, +73/−25):structure ReplayStatebundling the loop-threaded state (GlobalpluslastKey), so the in-loop key-monotonicity re-check is preserved verbatim and becomes part of the mechanized transition relation.stepRow : ReplayState → Row → Except String ReplayStateextracted from the oldgoloop body; per-row order (covTick → recordCover → key check → step) and error precedence preserved exactly.traceSpec : TraceSpecinstance andobserveCoverageobserver, driven byTraceSpec.replayWithObserverM.replayCanonicalRowsWithCoverage_sound,replayCanonicalRows_preserves,checkRowsWithCoverage_sound. Nosorry/admit/new axioms;#print axiomsshows onlypropext,Classical.choice,Quot.sound.Verification
lake build).configs/dcqcn_simple.toml,dcqcn_1s.toml,dcqcn_multi.tomlplus six corrupted variants (alpha snapshot mismatch, duplicate canonical key, missing required field, unmatched cnp_recv, interval-gate violation, frozen-parameter change) and a shuffled-rows ACCEPT case; stdout, stderr, exit codes, and--coverage-outJSON compared before vs. after — empty diff across all 13 traces, includingaqm_dcqcn_checkcross-layer runs.mainand the branch) and confirmed byte-identical outputs, audited the theorem statements against the AQM/PFC analogues for weakening (none), and verified thestepRowsemantics against the old loop.run-aqm-fixtures.sh(38),run-aqm-coverage-fixtures.sh(8),run-cubic-fixtures.sh(5).checkRowsWithCoverage,checkRows,step,parseCsv,Row/Kind/Ecn;AqmDcqcnMain.leanneeded no edits.native_decidecanonicalization example still compiles.🤖 Generated with Claude Code