Repository navigation
quest: plan proofs and nightly checks for moq-net - #8472
Conversation
Adds ten quests from a /quest-plan on what could be proved about moq-net: an inductive routing invariant, a Tamarin model of the route key proof, whole-session fuzzing, Kani codec proofs, a JS replay of the fuzz corpus, mutation testing, Miri seeds with ThreadSanitizer, and trace validation for the resume, reconnect, and subscribe models. Moves route trace validation to m1 and adds a Coverage-table symbol check to the nightly models quest. Co-Authored-By: Claude <noreply@anthropic.com>
|
Warning Review limit reachedYou've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. Next included review available in 16 minutes. View limit details
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. |
kixelated
left a comment
kixelated
left a comment
There was a problem hiding this comment.
Automated review by review (OpenAI)
Reviewed commit 6732990.
P2 — Correct the varint proof obligations before implementing the harnesses (quest/m4/codec-kani.md:20–24). The stated properties are false for the existing, intentionally supported wire formats: QUIC rejects values above 2^62 - 1, so not every u64 can round-trip through both codecs. Also, a valid non-minimal leading-ones encoding [0x80, 0x25] decodes to 37 but re-encodes as [0x25], which is not a prefix of its input (the existing leading_ones_spec_examples test explicitly covers this). These requirements would make a correct implementation fail the planned proof. Specify round-trip within each form's representable range, rejection without writes outside QUIC's range, and preservation of the decoded value after canonical re-encoding rather than byte-prefix equality.
Overall direction: the layered verification plan and explicit model bounds are sensible; fix the codec proof contract so the future check tests the intended protocol rather than rejecting legal encodings.
Verification limits: GitHub-only static review of all changed plans and targeted implementation checks, including the varint codec/tests and route-proof transcript. No builds, tests, Kani, Tamarin, or TLA+ tools run; this does not establish the proposed proofs.
![pullfrog[bot]](https://avatars.githubusercontent.com/in/1768019?s=60&v=4){kind=small}
There was a problem hiding this comment.
Important
The mutation-testing quest reintroduces work an m0 quest is deleting, without naming the existing weekly workflow, and the cut-gating route key quest sits in m1 where the tree says the cut waits on m2 alone. Both need a sentence of reconciliation before the tree reads consistently.
Reviewed changes
Reviewed the complete 15-file diff at 6732990 end to end and checked its load-bearing claims against the tree: the verify/ specs and rule names, route/proof.rs and js/net/src/lite/route_key.ts, the draft's Route Key Parameter section, the fuzz harness and fixtures, sh/rs/miri.sh, sh/rs/mutants.sh, .cargo/mutants.toml, the Nightly matrix, and every quest link.
- m1 proofs and checks —
route-inductive(Apalache inductive invariant for the route rules from any state),route-key-model(Tamarin proof of the Route Key Parameter, gating the cut), andsession-fuzz(whole-session fuzz on both protocols with a bystander broadcast as oracle). - Route trace validation promoted — moved from m4 to m1, with its decision log extended to hand its trace format to the other three models.
- m4 real-code checks —
codec-kani(varint and length proofs),fuzz-corpus-js(JS replays the Rust corpus),mutants, andmiri-seeds-tsan. - m4 trace validation —
resume,reconnect, andsubscribequests reusing route's recorder and TLC recipe. - Cut gate and drift —
lite07-finalizeadds the route key model toRequired;model-checks-nightlygains ajust checkfailure when a Coverage-table symbol disappears. - Indexes —
quest/m1/README.mdgains four entries;quest/m4/README.mddrops the route trace line and adds seven.
deepseek-v4.1-flash-1017 (free via Pullfrog for OSS) ｜ 𝕏
|
|
||
| cargo-mutants changes `rs/moq-net/src/route/` and | ||
| `rs/moq-net/src/model/resume.rs` one small edit at a time, and the tests fail | ||
| on every edit that changes behaviour. Nightly runs it and fails on any |
There was a problem hiding this comment.
quest/m0/ci/trim.md already plans to delete .github/workflows/mutants.yml — its one run failed all 24 shards creating target/mutants, and test/drill/sensitivity.sh already runs mutations nightly — while quest/m3/audit-ci.md records the opposite ("Keep"). This plan never names the existing weekly 24-shard workflow or the current .cargo/mutants.toml scope (which already contains model/resume.rs plus moq-auth, auth.rs, and expiry.rs), so it reads as new work and leaves the tree telling an implementer both to delete the job and to run it nightly.
Technical details
# Reconcile the mutation quest with the m0 workflow trim
## Affected sites
- `quest/m4/mutants.md:7` — "Nightly runs it and fails on any survivor"
- `quest/m4/mutants.md:18` — the same claim as a decision
- `quest/m4/mutants.md:28` — proposes a Nightly matrix with `--shard k/n`, which the weekly job already does
- `quest/m0/ci/trim.md:24` — "Delete `mutants.yml` … This PR deleted its quest"
- `quest/m3/audit-ci.md:215` — the CI audit row says Keep
- `.github/workflows/mutants.yml` — weekly on a 24-shard matrix, already fails on a survivor
- `.cargo/mutants.toml:examine_globs` — already scopes `rs/moq-net/src/model/resume.rs`, `rs/moq-auth/src/**`, `moq-net/src/auth.rs`, `moq-net/src/model/expiry.rs`
## Required outcome
- Say whether this replaces the weekly job (and that m0's deletion is reversed) or keeps it weekly and only widens the scope.
- Say whether the existing `moq-auth`, `auth.rs`, and `expiry.rs` scope stays in the config.
- If reviving the job, name the `target/mutants` creation failure as the first-run prerequisite rather than only "kill or exclude every survivor".| - ✅ Tamarin (rejected: no formal analysis; the proof is a hand-rolled | ||
| construction, the kind symbolic provers find reflection and relaying | ||
| attacks in). | ||
| - ✅ m1 and it gates the cut (rejected: ungated like the TLA+ models; m4). |
There was a problem hiding this comment.
quest/README.md says "The cut waits on m2 alone" and quest/m1/README.md says "The cut no longer waits on m1", yet this new m1 quest is listed in the cut's Required and says it "gates the cut". The only other m1 entry in that list (stream-credit/takeover) is held by an open claim, which is the tree's stated mechanism; this one has none. Either move it to m2 (its finding can change the frozen wire) or record the exception in m1's Plan.
Technical details
# A cut gate in m1 has no mechanism
## Affected sites
- `quest/m1/route-key-model.md:20` — "✅ m1 and it gates the cut"
- `quest/m2/lite07-finalize.md:137` — listed under the cut's `Required`
- `quest/README.md:16` and `:59` — "The cut waits on m2 alone"
- `quest/m1/README.md:15` — "The cut no longer waits on m1"
- `quest/m1/README.md:25` — the held-by-open-claims mechanism
- `quest/m2/README.md:30` — held claims are the stated exception
## Required outcome
- The tree no longer states both that the cut waits on m2 alone and that a fresh m1 quest gates it without a claim.| - Scope: both varint codecs in `rs/moq-net/src/coding/varint.rs` (every `u64` | ||
| encodes and decodes back to itself at the length the draft gives; every |
There was a problem hiding this comment.
The QUIC form caps at MAX_QUIC = 2^62 - 1, so "every u64 encodes and decodes back to itself" cannot be a proof obligation for that form, and a harness over kani::any::<u64>() would fail on values above the cap. State each form's admitted range and the round-trip property inside it, next to the existing "prefix of it" decoder property.
Technical details
# The varint proof obligation needs per-form ranges
## Affected sites
- `quest/m4/codec-kani.md:20` — "every `u64` encodes and decodes back to itself at the length the draft gives"
- `rs/moq-net/src/coding/varint.rs:18` — `MAX_QUIC = (1 << 62) - 1`
- `rs/moq-net/src/coding/varint.rs:234` — `decode_quic`, `encode_quic` returns `BoundsExceeded` above the cap
- `rs/moq-net/src/coding/varint.rs:26` — `Form::{Quic, LeadingOnes}`
## Required outcome
- The scope sentence names the admitted range per form (QUIC up to `2^62 - 1`, leading ones up to `u64::MAX`) and the round-trip property within each.
Problem
The maintainer asked what could be proved about moq-net, which tools would raise confidence in the protocol and its implementation, and how to keep such checks from rotting. They must fit Nightly. Loom was removed in moq-dev/moq#7474 because it never found a race and needed a shim around every primitive.
No tool proves 87k lines of async Rust. Today's checks are four TLA+ models bounded to small runs (moq-dev/moq#8447), codec-level fuzz targets, a narrow Miri run, and seeded sweeps. The gaps: nothing holds for unbounded runs, the hand-rolled route key proof has no analysis, no fuzz target drives a whole session, the Rust and JS codecs are compared only on a hand-written corpus, and only the route model has a planned mechanical tie to its code.
Approach
Goal confirmed with the maintainer: every layer of moq-net has a nightly check that either runs the real code or is mechanically tied to it, and the routing design is proved beyond bounded runs.
A check that runs the real code can fail but cannot rot; a model rots unless something mechanical ties it to the code. So the plan adds real-code checks, and ties every model to its code.
just checkfailure when a function a Coverage table names is renamed or deletedjs/netandmoq-netagree on every input the Rust fuzzers keeproute/andmodel/resume.rs, failing on any survivorFinalize moq-lite-07 now lists the route key model under Required.
Decisions
just check, ✅ trace validation for the other three models now. The last reverses "route only for now; judge the other models after" from earlier the same day.Chosen without asking, as recommendations in each Plan: no Bolero for Kani, mutant exclusions in
.cargo/mutants.tomlover#[mutants::skip], and separate quests over an epic, as the existing model quests are flat in m1.Impact
Public API: none. Wire: none. Quest files only.
Alternatives
Router(a model checker overSim): moq-dev/moq#8447 rejected it for trace validation, and this plan keeps that.Follow-ups
cargo miri testtoday. Recommend: plan it as an m5 quest waiting on rust-lang/miri.main. No new quest.Models
Size: M
Implementer: Claude Code, claude-fable-5-2, high effort
🤖 Generated with Claude Code
Review
Rewritten by
quest reviewafter each round.01a1c7e5-42d4-70b2-aa90-e0b987751646, round 1The change only adds and reorganizes quest plans, with no runtime changes or actionable defects, and is ready to land as planning documentation.(Written by Claude Fable 5 with high effort)