test(net): property-test the headers view, matcher, and builder by daniel-noland · Pull Request #1734 · githedgehog/dataplane

daniel-noland · 2026-08-17T20:47:35Z

Second of five, stacked on #1733.

Property tests for net::headers — the HeadersView unsafe boundary, the
pattern matchers, the builder's Within::conform, and the embedded (ICMP-quoted)
header views. Coverage of the module went from roughly a third to the high
nineties; the lines still uncovered are the unreachable_unchecked arm of each
arity, which must stay uncovered because reaching one is the undefined behaviour
the whole HeadersView invariant exists to prevent.

The recurring finding, across five separate instances, was code that no
generator could reach rather than code that was wrong: embedded_ip was never
set by any generator, the absent-layer arm of every opt_* method was
unconstructible, no shape ever named Vxlan, the first-step-refusal branch was
unreachable at every arity, and conform was only reachable through a builder
no test used. In each case "we have tests for that" was false and the tests
looked fine.

Two things the tests pin rather than fix, both for the owner to decide:

when/inspect/otherwise on the embedded matchers read only the inner
accumulator, while done() requires both. A packet whose outer chain fails
but whose quoted packet matches runs inspect, skips otherwise, and then
returns None — 4,974 packets in 25,000. Documented behaviour, but
otherwise is the error hook and stays silent for a whole class of failure.
All twelve Within<Icmp4|Icmp6> for <subtype> conform bodies are dead.
Install runs afterwards from build_headers and overwrites whatever they
wrote, and nothing can be stacked on a subtype, so there is no arrangement in
which conform gets the last word.

The last commit is new, not extracted: the embedded vacuity guard only asserts
once a run is long enough for a miss to mean something, and its threshold was
set at the case count a default run managed when it was written. Coverage
instrumentation costs about a fifth of the throughput here — measured at 17 hits
in 20,206 cases against 21 in 25,857 — which left the threshold sitting a couple
of hundred cases below what CI actually draws, so a busier runner would drop
under it and the check would disappear silently. Lowered to ten thousand.

Worth recording since #1714 adds --cfg=instrumented for this purpose: these
properties are bound by the generator rather than by a counter loop, so unlike
the fib test that motivated the cfg, no iteration counts need cutting here.

Verified locally: dataplane-net 473/473, fmt --check and
clippy -D warnings clean.

🤖 Generated with Claude Code

coderabbitai · 2026-08-17T20:47:48Z

Important

Review skipped

Draft detected.

Please check the settings in the CodeRabbit UI or the .coderabbit.yaml file in this repository. To trigger a single review, invoke the @coderabbitai review command.

⚙️ Run configuration

Configuration used: Organization UI

Review profile: CHILL

Plan: Pro

Run ID: 35f71ac6-90aa-4697-a05b-bae5a8e7301c

You can disable this status message by setting the reviews.review_status to false in the CodeRabbit configuration file.

Use the checkbox below for a quick retry:

🔍 Trigger review

_{Comment @coderabbitai help to get the list of available commands.}

codecov · 2026-08-17T20:54:33Z

Codecov Report

❌ Patch coverage is 97.23270% with 22 lines in your changes missing coverage. Please review.
✅ All tests successful. No failed tests found.

Files with missing lines	Patch %	Lines
net/src/headers/embedded_view.rs	95.37%	5 Missing and 3 partials ⚠️
net/src/headers/view.rs	94.21%	4 Missing and 3 partials ⚠️
net/src/headers/within.rs	93.22%	3 Missing and 1 partial ⚠️
net/src/headers/mod.rs	98.78%	1 Missing and 1 partial ⚠️
net/src/headers/pat.rs	99.63%	0 Missing and 1 partial ⚠️

📢 Thoughts on this report? Let us know!

…cher `view.rs` was the most sensitive uncovered code in the tree, and its coverage number understated the risk. [`HeadersView`] buys zero-cost extraction with `unwrap_unchecked`: `Look::look` repeats the `ViewStep::step` chain that `sealed::Sealed::matches` already ran, and tells the compiler the `None` arms cannot happen. **Soundness rests entirely on those two chains agreeing** -- and the macro writes them out separately for every arity, eight-odd hand-written pairs, each threading the VLAN and extension cursors through by hand. That is the same shape as all six defects this campaign found in `routing`: an invariant enforced at a distance by a different function from the one relying on it. Only here a transposed cursor is not a wrong answer, it is undefined behaviour. `view.rs` sat at 42% line coverage. ## The generator was the reason, not missing tests `CommonHeaders` -- the sunny-day generator every packet test reaches for -- has six construction sites and **all six** set `vlan: ArrayVec::default()` and `net_ext: ArrayVec::default()`. It never produces a VLAN tag or an IPv6 extension header. Those are exactly the two things the view and matcher semantics are *about*: a tag the shape does not mention is a miss, extension headers are skipped silently until the shape enters the extension region and then `ExtGapCheck` turns strict. No existing generator could reach either. The tests were there; the inputs were not. Hence `ShapedHeaders`, which varies the structure: 0..=MAX_VLANS tags, and 0..=MAX_NET_EXTENSIONS extension headers of the variants that belong to the address family. Structural on purpose -- `step` walks in-memory layers with cursors, so whether `next_header` agrees with what follows it is a different property's business, and coupling the two would shrink the space this explores. Measured: **80% of generated packets carry a VLAN tag, 75% an extension header, and 20% match the shape under test.** Not vacuous. ## The oracle is the other implementation `Matcher` decides the same question safely and returns an `Option`, over the same `Within` graph and the same `ExtGapCheck`. Comparing the two is a differential test between implementations that both already exist, rather than against a third transcription of the rules. Layers are compared by **address**: two VLAN tags with equal contents pass an `assert_eq!` and are a bug if the two sides chose different ones. A shape starting at `Net` was tried and does not compile -- `Net` has no `Within<()>` -- so that half of the contract is enforced at compile time and needs no property. Left as a comment so the next person does not retry it. ## Verified, including what the verification cannot see The break test needed two attempts, which is the argument for always running it: making `matches` stricter in the **arity-1** arm changed nothing, because these shapes are arity 3 and 4. Patching the arity-3 arm fails in half a second with a shrunk packet. Both properties also run clean under miri, which is the only thing that can see the *unsound* direction -- a test that has already reached `unwrap_unchecked` on a `None` cannot report it. Recorded honestly at the property: bolero manages 5 cases a second under miri against ~35,000 native, and the miri recipe spawns its own `nix-shell` so the caller's `BOLERO_RANDOM_TEST_TIME_MS` never arrives, capping the run at 25 cases per property. A smoke test of the unsafe path, not a proof. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

The previous commit claimed the unsound direction of a `matches`/`look` divergence could only be seen under miri, on the reasoning that a test which has already reached `unwrap_unchecked` on a `None` is in no position to report it. That is wrong, and Daniel caught it. `unwrap_unchecked` bottoms out in `hint::unreachable_unchecked`, whose `assert_unsafe_precondition!` is gated on `ub_checks`, which follows `-Cdebug-assertions` -- and `profile.fuzz` sets that **on**. Measured rather than reasoned this time: unsafe precondition(s) violated: hint::unreachable_unchecked must never be reached thread caused non-unwinding panic. aborting. ... (signal: 6, SIGABRT: process abort signal) So `profile=fuzz` already detects it, and that is where most of the assurance comes from. Miri is still worth having for what `ub_checks` does not model -- aliasing and provenance across the `as_ref_unchecked` boundary -- but it is not the only thing standing between this and undefined behaviour. Both guards are now documented in the order they fire, each demonstrated by breaking the arity-3 arm deliberately: 1. **the differential, first.** The `Matcher` comparison runs *before* `look`, so a divergence in either direction fails with a shrunk counterexample instead of invoking undefined behaviour. Over-strict and accept-everything both fail here in under a second. 2. **the standard library's check, as a backstop**, for a divergence that slipped past guard 1 -- if `Matcher` carried the same bug. Verified by calling `look` on an over-permissive `matches` with the differential removed: `SIGABRT`, fuzz profile, no miri. Worth recording that guard 2 is a *non-unwinding* panic, so bolero cannot catch it and the process dies. Under libfuzzer that is the right outcome -- a saved `crash-*` artifact rather than a silent pass -- but it does mean the failure surfaces as an abort rather than a counterexample, which is why guard 1 running first is a design choice and not an accident. No behaviour change; comments only. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

…ke miri usable The read path was the easy half. `Look::look` and `sealed::Sealed::matches` at least walk the stack the same way -- both chain `ViewStep::step`. `look_mut` does not: it builds a `MatcherMut` from `pat_mut()` and chains `ViewStepMut::chain` over it, then calls `unreachable_unchecked` if that returns `None`. **So the invariant is established by one traversal and consumed by a different one.** Nothing makes `ViewStep::step` and `ViewStepMut::chain` agree except that they were written to. Where the read path risks a mis-threaded cursor between two copies of one walk, this risks two walks disagreeing outright. Worth saying what is *not* tested: `look_mut` against `MatcherMut`. `look_mut` **is** `MatcherMut` plus an `unreachable_unchecked`, so comparing them is the implementation against itself. The question worth asking is whether `matches` -- which licensed the unchecked call -- agrees with the walk that has to deliver on it, and that is checked without calling `look_mut` at all, so a divergence is a counterexample rather than undefined behaviour. `look_mut` hands back several `&mut` into one `Headers`, pre-split through `Fields`. If that split ever aliased, two references would point at the same layer -- and the `ub_checks` backstop cannot see it. It checks the `unreachable_unchecked` precondition and nothing about aliasing. Only miri sees that, and only with stacked borrows on. Two obstacles, both now fixed in `miri.just`: - **the budget.** The recipe launches its own `nix-shell`, which does not inherit the caller's environment, so `BOLERO_RANDOM_TEST_TIME_MS` never arrived and every property stopped at bolero's one-second default -- about 25 cases under miri. Enough to prove the harness runs and nothing else. - **`stacked_borrow_check` was unreachable.** `just` will not override a *module's* variables from the command line: `just miri stacked_borrow_check=... test` parses as a recipe name, and `--set` is refused as "not present in justfile". The knob existed and could only be changed by editing the file. Both now read `env()`, so `STACKED_BORROW_CHECK=enabled just miri test ...` works. Under miri bolero manages about five cases a second, and the cost is wall-clock. Raising the budget buys cases linearly on one core; sharding buys them across cores for free. The aliasing property -- the expensive one and the one that matters most -- is instantiated as sixteen shards, each seeded from the OS so they explore independent streams, and nextest runs them concurrently. Sixteen rather than sixty because miri's per-process memory footprint is large and the other properties want cores too. Result: **963 cases across 24 properties under miri with stacked borrows enabled, no undefined behaviour** -- against 25 per property with stacked borrows off before this. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

…cle reaches `matches`, `look` and `look_mut` are generated separately for each arity by a macro, with the VLAN and extension cursors threaded through by hand every time. Testing two arities tested two of eight copies, which is why the last commit moved `view.rs` coverage by two points and no more. Both walks are now checked at arities one through seven, read and mutable, from one macro so a new arity costs one line. ## Seven, not eight, and the reason is the oracle `Matcher`'s vocabulary is `eth`, `vlan`, `net`, `transport`, `vxlan`, `embedded`. The last two cannot be reached in a builder chain: `Vxlan: Within<Udp>` and the embedded header sits under `Icmp4`/`Icmp6` -- both *concrete* layers -- and `Matcher` has no concrete-layer methods. No `.udp()`, no `.tcp()`. So its longest expressible chain is `Eth`, four VLAN tags (`MAX_VLANS`), `Net`, `Transport`. Two gaps follow, and both belong to the oracle rather than the code: - the **arity-8** arm is generated and stays unchecked, because nothing `Matcher` can say is eight elements long; - shapes entering the **IPv6 extension region** cannot be expressed at all, and that is the more interesting loss. `ExtGapCheck` is the subtlest part of the contract and the part the module documentation spends most of its words on, and it has no oracle. Closing it needs extension-header methods on `Matcher`, or a different oracle. Recorded at the call site so the next person does not have to rediscover why the list stops where it does. ## Every arity proves it is not vacuous A shape the generator never produces makes its property pass for the wrong reason, and the higher arities are exactly where that would happen quietly: arity 7 needs a packet carrying *exactly* four VLAN tags, since a tag the shape does not name is a miss. So each property reports its hit rate and fails if it never matched. Measured, and pleasingly uniform: arity 1 matches everything, and arities 2 through 7 each match about 20% -- which is `P(exactly N tags)` for a uniform 0..=4 draw. Every arity is exercised at roughly the same rate rather than the long shapes being starved. ## Verification 1,386 tests green. Under miri with stacked borrows enabled -- the configuration that can see an aliasing fault in the `Fields` split, which the `ub_checks` backstop cannot -- **4,560 cases across 31 properties, no undefined behaviour.** That is up from 963 before the arity work and from 25 per property before the miri budget was reachable at all. Coverage-guided runs on the two differentials, 60 workers: roughly 1.7 billion executions each, no crashes. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

…nsion region `embedded_view.rs` sat at 33.9% line coverage, and the reason was not that nobody had written tests for it. Its hand-written tests are careful and thorough. Every one of them builds its packet through `HeaderStack` or `header_chain`, which pin the shape at `(Eth, Ipv4, Icmp4)` outside and `(Ipv4, Tcp)` inside and offer no way to attach an extension header to either side. Six of the eight `as_embedded` arities and the whole embedded extension region were unreachable by construction. The generators were the binding constraint, again. All six construction sites of `CommonHeaders` set `embedded_ip: None`, so neither it nor `ShapedHeaders`, which builds on it, can produce an ICMP error carrying a quoted packet at all. `ShapedIcmpError` does: it varies the outer VLAN tags and extension headers so the outer arity spans the range of `as_embedded` impls, varies whether the quote is present, and varies the quoted packet's network layer, extensions and truncated transport. The quoted family usually follows the quoting family, because that is what a real ICMP error looks like, but not always -- a mismatch is where two independent structural walks are most likely to disagree. What the new differential properties compare is the pairing soundness rests on, which is not the obvious one. `as_embedded_mut` *decides* with `Sealed::matches`, walking `EmbeddedHeaders` through `EmbeddedStep`. `look_mut` then *delivers* through `EmbeddedMatcherMut`, a separate implementation with its own pre-split fields and its own gap check, and unwraps that chain with `unreachable_unchecked` on the strength of the first one's answer. If they disagree the result is undefined behaviour, not a wrong answer. Every arity of both is now checked against the `pat()` oracle, read path and mutable path. Two claims in `view.rs` were wrong and are corrected here. `Matcher` does have concrete-layer and extension-header methods -- `matcher_net!`, `matcher_ext!` and `matcher_transport!` give it `.ipv4()`, `.hop_by_hop()`, `.tcp()` and the rest -- so neither gap that comment recorded was real. The arity-8 arm is now checked, and so is the extension region, where `ExtGapCheck` switches from skipping extensions silently to requiring all of them consumed. That is the subtlest part of the contract and the part the module documentation spends most of its words on, and it had no oracle at all. Hit rates are measured and asserted rather than hoped for, which mattered twice. A shape naming three extensions in sequence matched 2 packets in 36,000 -- honest, and useless -- until `ext_run` learned to follow RFC 8200's recommended order a quarter of the time; it now matches about 200. And naming one extension inside a quoted packet compounds six conditions, including `P(no VLAN tags) = 1/5`, which put `(&Ipv6, &DestOpts, &TruncatedTcp)` at 6 hits in 23,910. `ShapedQuote` produces that shape every time and fuzzes the contents instead: 32,000 hits. The division is deliberate -- a property comparing hit against miss needs both, a property asking only which layer was selected gets nothing from a packet it skips. Verified by breaking the code three ways. An off-by-one on the embedded extension cursor fails exactly the four extension-region differentials, in one second, with a counterexample carrying exactly one extension -- the case where a stalled cursor makes the gap check see `len 1 != ec 0`. Dropping the shape check from arity 7's `as_embedded` fails exactly `read_outer_7`, in 87ms, while `mutable_outer_7` correctly stays green. Reading one extension slot too far fails the six `same_layers_ext_*` properties through the vacuity guard, which reports that the shape was never produced -- the same class of defect this campaign has now found five times. Coverage: `embedded_view.rs` 33.9% -> 86.0%, `pat.rs` 55.4% -> 63.2% without a test written for it, `view.rs` 50.1% -> 53.8%, `net/` 66.8% -> 69.8%. The 49 lines still uncovered are all unreachable: three `unreachable_unchecked` arms, which is the point of them, and 44 in the arity-1 and arity-2 `as_embedded` arms, which cannot be instantiated -- asking for either is a compile error, so they could be deleted. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

…rs watch `pat.rs` had 296 unreached lines and 250 of them were one thing: every `opt_*` method on all four matchers, plus `when`, `inspect` and `otherwise` on each. The optional half of the pattern-matching API had never been run. That half is not a thin wrapper over the strict half. Three families live under one naming convention. `opt_eth` cannot miss. `opt_vlan` and the optional extension methods cannot miss either, but advance their cursor only when they matched, so they skip rather than refuse -- and an optional extension still moves `Pos` into the extension region, which makes a later, unrelated transport step strict. `opt_net`, the optional transports and `opt_vxlan` are three-way: present and right is a hit, absent is a hit carrying `None`, present and wrong is a miss. Conflating the middle case with either neighbour is the mistake the design invites. Nothing could draw the middle case. `CommonHeaders` sets every layer on every path, so `net` and `transport` are always `Some` in anything it or `ShapedHeaders` produces, and the absent-layer arm of every optional method was unreachable by construction. `ThinHeaders` truncates the stack by suffix, which is the only shape a real short packet takes. `ShapedIcmpError` gained the quote too short to hold a network header, which RFC 792's header-plus- eight-bytes makes an ordinary thing rather than an exotic one. One invariant covers all three families and every layer: weakening a requirement cannot turn a match into a miss. It is worth stating because `map` and `and_then` differ by exactly that, and it is the direction a mis-wiring inverts. The guard on it counts both outcomes -- the strict form must sometimes match, and the optional form must sometimes accept what the strict form refused. An implication passes for free when its antecedent never holds, and just as quietly when the two sides never differ, which is the more likely failure and would leave the optional method's whole reason for existing untested. The property found something. `EmbeddedMatcher` and `EmbeddedMatcherMut` carry two accumulators and `done()` requires both, but `when`, `inspect` and `otherwise` all read the inner one alone. A packet whose outer chain fails -- an unconsumed VLAN tag will do it -- but whose quoted packet matches will run `inspect`, skip `otherwise`, and then return `None`. It happens to 4,974 packets in 25,000, so it is the common case rather than a corner. The doc comments say "inner accumulator" and "inner match", so this is documented rather than broken, but `otherwise` is the error-handling hook and there is a class of failure it stays silent for. `the_embedded_combinators_track_the_ inner_match_only` pins the behaviour as it stands and will fail if it is ever changed, so that becomes a decision rather than a discovery. A second finding, this one about what cannot be written down. The enum-level vocabulary is complete on the outer matchers and mostly missing on the embedded ones: `EmbeddedMatcher` has `net` but not `opt_net`, `transport` or `opt_transport`; `EmbeddedMatcherMut` has `net` and `transport` but neither optional form. All five missing methods are hand-written rather than macro-generated, which is likely how they came to be missing, since every per-variant method is present. The consequence is that a shape naming `Net` or `EmbeddedTransport` inside a quoted packet cannot be expressed as a matcher chain at all -- which is also why `embedded_view`'s differential properties have no read-side oracle for the enum forms. The table is in the source next to the tests that would use them. Verified by breaking the code twice. Making an optional extension advance its cursor unconditionally fails exactly the gap-check property, and nothing else. Making `opt_eth` refuse an absent Ethernet header fails exactly `read_opt_eth`, through the both-outcomes guard, reporting that the optional form never accepted anything the strict form refused. Coverage: `pat.rs` 63.2% -> 98.8%, 296 uncovered lines down to 10. `net/` 69.8% -> 73.1%. Of the 10 left, three are defensive `unreachable!()` and the rest are gap-fail arms on the mutable optional paths. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

`view.rs` sat at 53.8% with 224 production lines unreached, and almost all of them were `look` and `look_mut`: the bodies at arities five through eight had never executed, nor had `look_mut` at one and two. The properties compared `matches` against the matcher chain -- the decision -- and stopped there. The delivery half was checked at arities three and four only, in the split test, because comparing two tuples means destructuring them into a fixed number of bindings and that has to be written out per arity. `Addrs` removes that constraint. Reducing a tuple of references to an array of addresses is arity-generic at the call site even though the impls are not, so the delivery check now runs wherever the decision check does. Addresses rather than values, because two VLAN tags can hold equal bytes without being the same tag, and picking the wrong one out of four is exactly the cursor bug this is looking for: `matches`, `look` and `look_mut` are generated separately at each arity, threading `vc` and `ec` through by hand every time, so a shape naming four tags has four chances to be off by one and the decision check cannot see any of them. Breaking arity six's `look` to read one tag early fails `read_6` and nothing else -- not even `read_ext_v6_three`, the other arity-six shape, whose third layer is an extension header and reads the other cursor. Two more gaps, both of the kind that hides behind a passing suite: `Vxlan` had no `ViewStep` coverage at all, not because the generators could not draw a VXLAN packet -- `CommonHeaders` has been drawing them all along -- but because no shape ever named the layer. It is the one step that runs no gap check and the one layer outside the linear stack, so nothing about it follows from the other arities. Two chains now name it; making the step refuse fails exactly those four tests and nothing else. The branch where the *first* step refuses is generated once per arity and was unreachable at every one of them, since `CommonHeaders` sets `eth` on all six of its paths. `ThinHeaders` can drop it but truncates four packets in five, which would cost the deep shapes most of their hit rate; `SometimesHeadless` drops it one packet in eight, enough for the branch and cheap enough that arity seven still matches six thousand times in thirty-five. The shapes are now derived rather than written. A shape and the chain matching it are one statement said twice, and every instantiation said it twice by hand: `(&Eth, &Ipv6, &HopByHop, &Transport)` next to `.eth().ipv6().hop_by_hop() .transport()`. A pair that disagrees compiles and passes and silently tests something else. `layer_ty!` holds the correspondence once, `shape_of!` builds the tuple from the chain, and the instantiations shrank to the chain alone. That is as far as generating tests from the macro tables usefully goes here. Enumerating the `Within` graph gives 4,755 legal chains up to arity eight -- 2,614 at arity eight alone -- so one property per chain is not a suite anyone would run, and the exhaustive version would have to be a shallow sweep over a fixed corpus rather than a fuzz run. It would also be worth less than it looks: an oracle enumerated from the same table the implementation is generated from cannot notice a wrong table entry. What survives the objection is the differential, since `matches` and the matcher chain are independent implementations and the table only chooses which chains to test, not the verdict. Coverage: `view.rs` 53.8% -> 98.4%, 224 uncovered lines to eight. The eight are the `unreachable_unchecked` arm of each arity, which must stay uncovered -- reaching one is the undefined behaviour the whole `HeadersView` invariant exists to prevent. `net` overall 74.2% -> 76.8%. Also fixes two lints in the previous commit that only appear under `--features bolero,test_buffer,builder` rather than `--all-features`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

`within.rs` sat at 32.7%, and the shape of the gap was unusually clean: thirty-two of the thirty-three `conform` bodies that do any work had never run, and the one that had was `DestOpts` inside `HopByHop`. Every unreached one was an IPv6 extension header transition, plus `Vlan` inside `Vlan`. The cause is a seam rather than an oversight. `conform` runs only from `HeaderStack::stack`, and the builder has had `.hop_by_hop()`, `.dest_opts()`, `.routing()`, `.fragment()`, `.ipv4_auth()` and `.ipv6_auth()` all along -- no test ever called one. The generators reach the extension region constantly, but they assemble `Headers` field by field and never go near the builder, so they never conform anything. Two ways to build a packet, and the fuzzing all went down the one that skips this trait. Seventeen chains cover the thirty-two transitions between them. Three extension headers is the ceiling, `MAX_NET_EXTENSIONS`, so the deeper corners of the graph need several short chains rather than one long one. The oracle is deparse-then-parse. Reading back the field `conform` just wrote would check the implementation against itself; the parser decides what follows an IPv6 header by reading that same field, so a `conform` naming the wrong protocol produces bytes that parse as a different packet, or as no packet at all. Naming TCP where the fragment header goes fails exactly the two chains carrying `routing -> fragment`. Each layer's protocol field is scrambled to a fuzzed byte before the next layer is stacked, so `conform` always overwrites a wrong value instead of filling in a blank one. That turns out to be load-bearing rather than cautious, and `Ipv4` inside `Eth` is the proof: `Blank for Eth` already produces `EthType::IPV4`, so on a blank header the conform setting `EthType::IPV4` has nothing to do. Deleting its body passes all seventeen chains unscrambled and fails two of them scrambled. `Vlan` has the same blank and the same exposure. Coverage: `within.rs` 32.7% -> 88.9%. `net` overall 76.8% -> 79.9%. The nineteen lines left are the no-op bodies -- the enum-level impls, the `EmbeddedStart` impls, and everything `impl_truncated_within!` generates. Those are unreachable through the builder, and the compiler says so twice over: `stack::<Net>` fails on both `Net: Blank` and `Headers: Install<Net>`, either of which would be enough on its own. They exist to give the pattern matcher its `Within` edges, which need the trait but not the method. Documented rather than deleted; whether to keep nineteen uncallable bodies belongs to whoever owns the trait. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

The last of `net/headers`. `builder.rs` had two untouched regions, both the same shape as everything else this campaign has turned up: methods the builder has always offered that no test ever called. The twelve ICMP message subtypes are one. `.dest_unreachable()`, `.redirect()`, `.time_exceeded()`, `.param_problem()`, `.echo_request()`, `.echo_reply()` and their v6 twins were unused, and ten of the twelve `Blank` impls behind them had never been called. The two that had are why the shared macro bodies looked covered -- a `macro_rules!` line counts as run once any one of its expansions runs, so a table of twelve generated impls reports green when one of the twelve is exercised, and only the hand-written part of each shows the difference. Scrambling had to change for these. `conform` writes a message type here rather than a protocol number, and the first attempt scrambled it to `Unknown` with a fuzzed type byte -- which fails six chains for a reason that has nothing to do with `conform`: `Unknown { type_u8: 3 }` deparses to the bytes of a destination-unreachable message and parses back as one. The scramble now uses 253 and 200, reserved for experimentation, which belong to no variant and survive the round trip as themselves. The round trip alone cannot check these. The scrambled type is a well-formed ICMP message, so a packet that never got specialized still deparses and parses back perfectly. The subtype chains assert separately that the scramble did not survive the build. That check is what exposes the finding: all twelve `Within<Icmp4|Icmp6> for <subtype>` conform bodies are dead. Empty them and every test still passes. `Install` runs unconditionally from `build_headers`, after `conform`, and overwrites whatever `conform` wrote; nothing can be stacked on a subtype, so there is no arrangement in which `conform` gets the last word. The two are indistinguishable until the caller customizes the subtype, because until then both write the same value -- `a_customized_subtype_survives_the_build` is the one test that separates them, and it fails on `Install` and not on `conform`. Pinned, not acted on; emptying them is a call for whoever owns the builder. The other region is an ICMP error quoting an ICMP packet. `EmbeddedAssembler::icmp4` and `::icmp6` were the two inner-transport methods nothing called, and with them the arm of `fixup_embedded` that writes `NextHeader::ICMP` onto the quoted IP header. A ping drawing a destination-unreachable is the ordinary way to produce one. The protocol number is asserted directly rather than left to the shape match, which would pass without it; naming TCP there fails exactly the one test. Coverage: `builder.rs` 79.1% -> 97.7%, `within.rs` unchanged at 88.9%, `net` 79.9% -> 81.1%. Eight lines left in `builder.rs`: two defensive `unreachable!` arms, two absent- layer arms, `Blank for ()` which `stack` never instantiates, and `Default for HeaderStack`. A test written to touch the last of those would be a test that exists to move a number, which is the failure mode this campaign has been finding, not one to add. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

The guard only asserts once a run is long enough for a miss to mean something, and the threshold was set at the twenty-five thousand cases a default one-second run managed when it was written. That leaves no room: coverage instrumentation costs about a fifth of the throughput here -- 17 hits in 20,206 cases against 21 in 25,857 without it -- so the threshold now sits a couple of hundred cases below what CI actually draws. A busier runner drops under it and the check disappears without saying so, which is the failure mode the guard exists to prevent. Ten thousand instead. The thinnest shape in this module draws about eight hits per ten thousand, so at that many draws a shape that really is reachable comes up empty about three times in ten thousand runs. The instrumentation cost is small because these properties are bound by the generator rather than by a counter loop, which is the opposite of the fib test that `--cfg=instrumented` was added for. No iteration counts need cutting here. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

daniel-noland added the dont-merge Do not merge this Pull Request label Aug 17, 2026

daniel-noland mentioned this pull request Aug 17, 2026

test(routing): property-test the rib, fib, and control plane #1735

Draft

daniel-noland force-pushed the pr/daniel-noland/fuzz-net-headers branch from 8f36183 to 61cd021 Compare August 18, 2026 03:07

daniel-noland force-pushed the pr/daniel-noland/fuzz-net-headers branch from 61cd021 to e2c650c Compare August 18, 2026 20:23

daniel-noland force-pushed the pr/daniel-noland/fuzz-net-headers branch from e2c650c to 90b4298 Compare August 18, 2026 20:31

daniel-noland force-pushed the pr/daniel-noland/fuzz-net-headers branch from 90b4298 to 3ea0473 Compare August 18, 2026 20:38

daniel-noland force-pushed the pr/daniel-noland/fuzz-net-headers branch from 3ea0473 to 7954def Compare August 18, 2026 23:17

daniel-noland and others added 10 commits August 19, 2026 00:33

daniel-noland force-pushed the pr/daniel-noland/fuzz-net-headers branch from 7954def to aaa46d5 Compare August 19, 2026 06:33

Navigation Menu

Uh oh!

test(net): property-test the headers view, matcher, and builder - #1734

test(net): property-test the headers view, matcher, and builder#1734
daniel-noland wants to merge 10 commits into
pr/daniel-noland/fuzz-net-checksumfrom
pr/daniel-noland/fuzz-net-headers

daniel-noland commented Aug 17, 2026

Uh oh!

coderabbitai Bot commented Aug 17, 2026 •

edited

Loading

Review skipped

Uh oh!

codecov Bot commented Aug 17, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

daniel-noland commented Aug 17, 2026

Uh oh!

coderabbitai Bot commented Aug 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Review skipped

Uh oh!

codecov Bot commented Aug 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

coderabbitai Bot commented Aug 17, 2026 •

edited

Loading

codecov Bot commented Aug 17, 2026 •

edited

Loading