fix(flow-entry): add an insertion that will not displace a live flow by daniel-noland · Pull Request #1736 · githedgehog/dataplane

daniel-noland · 2026-08-17T20:48:10Z

Fourth of five, stacked on #1735. One commit.

Adds an insertion that will not displace a live flow, and the test for it.
Displacing a flow takes the other half of its pair with it; the two halves have
different keys, so nothing displaces the partner in its own right, and it is
left live mapping a translation whose allocation has returned to the pool.

Small, but it is the commit that most needed adapting to a main that has moved
on, and it is worth knowing how it failed. It cherry-picked with no conflict,
then failed to compile because FlowInfo::related_pair became fallible, then
compiled and failed with InvalidPair("One of the flows must be the initiator") — an invariant main gained after this was written, which the test
was violating by flagging neither half. The forward half is now marked
INITIATOR, matching the sibling test in concurrent_fuzz.rs.

Three distinct failure modes behind one clean cherry-pick. With CI unavailable
this only surfaced because everything was run locally, which is the argument for
not trusting a clean apply on any of these branches.

Verified locally: dataplane-flow-entry 14/14, fmt --check clean.

🤖 Generated with Claude Code

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

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: 08c2b485-2964-4ccc-8fa2-28c8e02074f6

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:56:20Z

Codecov Report

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

Files with missing lines	Patch %	Lines
flow-entry/src/flow_table/table.rs	95.53%	3 Missing and 2 partials ⚠️

📢 Thoughts on this report? Let us know!

Debug binaries retained the complete Rust toolchain through their standard-library source paths, adding roughly 2.4 GB to the closure. They also carried a sizable DWARF index that neither packaged debugger consumes. Point those paths at the much smaller rust-src component, omit unused prebuilt documentation, and remove .debug_names. Source browsing and symbols remain available while the resulting diagnostic images become practical to store and transfer. Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

A core collected from the lab is useful only with the exact unstripped binaries and sources that produced it. A general debugging toolbox cannot reconstruct that relationship after the release has moved on. Provide a purpose-built gdb image alongside each build and teach it Rust's standard-library types without retaining rustc. This keeps post-mortem debugging reproducible while avoiding unrelated live-debugging tools. Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

Post-mortem inspection and live debugging need different tools. The core viewer cannot offer an editor-driven session, while bugstalker understands Rust layouts and can expose the running dataplane through the Debug Adapter Protocol. Track bugstalker upstream for its current remote DAP support and package it separately with the matching binaries and sources. Keeping the image single-purpose avoids making every diagnostic artifact carry every debugger. Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

Some failures need a record of the dataplane's kernel interactions rather than an interactive debugger. A small, repeatable tracing environment is easier to deploy and feed into existing log analysis than a general-purpose toolbox. Package lurk around the matching release binaries and follow the worker threads where the dataplane does its work. Because syscall tracing needs no symbols, this image can stay much smaller than the debugger images. Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

The diagnostic images are useful only when they match the build being investigated, but building roughly 850 MB of extra images for every pull request would undermine the runner-load reduction this CI rework is meant to achieve. Build them automatically for pushes, the merge queue, and manual runs, with an explicit label available for debugging a pull request. Publish all three beside tagged releases so the matching tools remain available when a deployed build needs investigation. Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

All three images built green while two of them could not do what the README documented. Building proves an image links; it says nothing about whether its entrypoint runs. `smoke-container` runs each one the way the README tells a user to: - the tracer under a plain `docker run`, with no seccomp relaxation, and requires an `execve` in the trace. Its failure mode is the reason this exists: lurk emitted eight well-formed JSON lines recording its own child failing to start, then exited 0, which the `jq -R 'fromjson? // empty'` filter we document accepts without complaint. Both guards fire against the pre-fix image. - the core viewer through its own entrypoint rather than by invoking gdb directly, since the `--directory` and `source` flags that register the printers live in that entrypoint. Checks that the printer set is registered, not merely that gdb started. - the debugger only for coming up and listening. Driving a real DAP session from CI means carrying a protocol client in-tree, and the contract it would pin is exercised better by pointing an editor at the image. It also would not have caught the defect on that image, which was in the documentation rather than the runtime. The trace goes to a file rather than a shell variable: at a few megabytes it overruns the here-string limit, and every grep against it then fails with E2BIG, which reads exactly like a failed trace. Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

The published images debug what CI built. Debugging what you are building meant either rebuilding an image by hand or falling back to a system gdb, which is exactly the case where symbols do not line up. `just debug <tool> <target>` builds the image that carries the tool at the current profile, platform, instrumentation, and sanitizer, and runs the target inside it: - `lurk` traces syscalls and streams JSON until the program exits. - `gdb` runs gdbserver and waits, printing the `target remote` line. - `bugstalker` waits for a DAP client, printing the `program` and `args` for the launch request -- in remote-DAP mode it takes those from the client rather than from its own command line. `target` is either one of the binaries the images already carry, in which case nothing needs mounting, or a nextest filter. For a test the archive is built and unpacked, and that binary was built outside the image, so the store comes along read-only and it runs with its package directory as the working directory the way nextest runs it. Naming a target exactly is the tedious part -- test paths are long and nobody remembers them -- so leaving it out offers everything through skim, and a filter matching several offers those. Resolution stays unambiguous: exactly one match runs without asking, no match is an error, and several with no terminal to ask at is an error listing them rather than a guess. That last case is what keeps this safe to call from a script. `just debug-list` prints the same list without running anything, and `just inspect-core` opens a core file in a gdb built from the same settings. Randomization stays enabled under gdbserver. Docker's default seccomp answers personality(ADDR_NO_RANDOMIZE) with EPERM, and while gdbserver treats that as non-fatal -- unlike lurk, which is why lurk is patched -- it otherwise opens with a warning that reads like a real failure. Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

`Checksum::increment_update_checksum` works out the new checksum and hands it back. It does not store it, despite taking `&mut self`. `EmbeddedTransport::update_checksum` called it and dropped the answer on the floor, under a comment about ignoring errors on a truncated header -- but there is no error to ignore; the return value is the checksum. So no quoted transport header has ever had its checksum updated. NAT rewrites the ports of the packet quoted inside an ICMP error and calls this to keep the checksum in step, and the call has been doing nothing. The only correct uses of the trait method in the tree are in a test, which is presumably how the shape survived. Setting it can fail, on a header too truncated to hold a checksum -- but that is a header the caller could not have read a checksum out of either, and every caller reads one first. Hence discarding that error rather than the value, which is what the comment was reaching for. update_checksum_for_address is new, and folds a change of one of the quoted packet's addresses in. TCP, UDP and ICMPv6 are checksummed over a pseudo-header built from the source and destination addresses, so rewriting one leaves the quoted checksum describing an address that is no longer there. ICMPv4 has no pseudo-header and is left alone. Incremental for the same reason as the rest: a quote is usually truncated, so there is no payload to compute over from scratch. The tests build the one case where both routes are open -- a full header over a known payload -- and hold the fold against a computation from scratch, over two words for v4 and eight for v6. The checksum starts out correct on purpose: an RFC 1624 update is exact given a correct starting value and says nothing given a wrong one. Both fail against the discarded update; the ICMPv4 one passes either way, which is the point of it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

…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>

First property tests in this crate, which had none -- 59 tests over 15,311 lines, and bolero already a dev-dependency waiting to be used. Two targets, both on the path from the rib to the fib the forwarder reads. `FibEntry::squash` folds every egress instruction of an entry into one, keeping the first interface and the last address of the resolution chain. That asymmetry is load-bearing: rib2fib notes that without it the address of a recursive next-hop never reaches the fib and the egress stage resolves the packet's destination instead, which is right only for a directly connected host. Four properties -- the other instructions survive in order, at most one egress and it goes last, the merge follows first-interface / last-address / first-name, and squashing twice is squashing once. Values come from a small alphabet so that egress objects disagreeing about the same field is the common case; independently drawn ones would almost never collide. `Nhop::build_nhop_fibgroup` walks the resolver graph and emits one entry per root-to-leaf path, squashed and filtered by `FibEntry::is_valid`, with a drop injected if nothing survives. The oracle enumerates the paths from the edge list instead of walking the same recursion. Removing the unresolved-leaf filter fails it; removing the drop fallback fails it and the companion property that every entry a group offers is one the forwarder can execute. `resolves_with` gets its own property, that it answers reachability in the resolver graph, checked against a closure over the edge list. It is worth stating plainly because everything above depends on it: neither `build_nhop_fibgroup_rec` nor `resolves_with` itself has a base case for a cycle. Acyclicity is an inductive invariant maintained entirely by `lazy_resolve` refusing an edge whose target already reaches the source. The generator produces graphs in topological order for that reason -- a generated cycle would not find a bug, it would exhaust the stack. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

Four separate recursions walk the next-hop resolver graph, and not one of them had a base case for a cycle: - `Nhop::resolves_with` - `Nhop::build_nhop_fibgroup_rec` - `fmt_nhop_resolvers` and `fmt_nhop_rec`, behind `Display for Nhop` and `Display for NhopStore` - `Nhop::quick_resolve_rec` (tests only) Acyclicity was an inductive invariant maintained entirely by `lazy_resolve`, which consults `resolves_with` before wiring each edge and refuses one that would close a cycle. That guard is correct, but nothing in the types connects it to the four recursions that depend on it, and `add_resolver` applies no guard at all. Worse, the recursion protecting the others could not protect itself: `resolves_with` is the first thing a cycle would break. Each walk now carries the set of next-hops it has already visited and stops rather than going round again. A next-hop is identified by address rather than by key, because a next-hop may hold resolvers belonging to another store, where an equal key would name a different object -- a resolution loop is a loop in the object graph. `build_nhop_fibgroup_rec` contributes nothing from a looping path, so a next-hop with no other way out ends up with the drop entry that `build_nhop_fibgroup` already injects for an empty group. That is the right answer: a packet caught in a routing loop should be dropped rather than forwarded round it. Along the way this found a live bug in the display path. `fmt_nhop_resolvers` tracked depth in a `u8` and incremented it per level, so a cycle recursed until that counter overflowed -- a panic raised from inside a `Display` impl, reachable from the CLI and from the very warning the new fib-group guard logs about a resolution loop. The counter is now saturating as well as guarded, which also removes the overflow for a legitimately deep chain. The property tests added in 317cc5bbb generated graphs in topological order and said so in a comment, because a generated cycle would have found the stack rather than a bug. They now generate an arbitrary adjacency list, self-loops included, which is where the interesting inputs were all along. Five million cases pass. Each guard was confirmed load-bearing by removing it: without the `resolves_with` visited set or the `build_nhop_fibgroup_rec` path set, the covering property overflows the stack and aborts the test process; without the display guard, `test_display_of_a_resolution_loop_terminates` panics at the increment. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

Builds a generator for a populated `Fib` and four properties over it. The generator is the one a pipeline harness will want: it reaches a fib the way production does, by pushing a sequence of `FibChange`s through a `FibWriter`, rather than by reaching into the tries. Alongside it runs a model -- two `BTreeMap`s, which is the fib with its tries, its group store's reference counting and its `UnsafeCell` sharing all taken away. What the model has to get right is not the data structure but which changes the fib *refuses*, and that turns out to be the valuable part. Four separate decisions, in three files, none of them stated where the next one can see it: - `FibGroupStore::add_mod_group` refuses a group with no entries - `FibGroupStore::del` keeps a group any route still names, by refcount - `FibWriter::add_fibroute` refuses a route with no next-hop keys, and `FibRoute::from_nhopkeys` refuses one naming an unregistered group - `Fib::del_fibroute` resets a root route to drop instead of deleting it, and purges unreferenced groups afterwards Together those are what keep `Fib::lpm` from reaching its `unreachable!()` and `Fib::lpm_entry_prefix` from reaching its outright `panic!` -- both on the forwarding path, for every packet that arrives. So the second property says that in as many words: every route a lookup lands on has at least one entry to execute, and the index arithmetic that picks among them is total over the range it is given. The prefix pool is nested so a longest match has something to be longer than, and holds both roots so that deleting one is reachable. The next-hop key pool is deliberately small, because the behaviour worth exercising is the collisions: a route pinning a group against deletion, a registration mutating a group two routes share. Verified by breaking each of the four decisions in turn. Letting the store accept an empty group fails in one change -- registering an empty group over the drop key empties the route both roots point at. Making the default route deletable fails three of the four properties. Ignoring the refcount in `del`, and dropping the purge after a route deletion, each fail the model. Five hundred thousand cases pass. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

A fib is reachable from the `FibTable` by two keys: its own `FibKey::Id`, and optionally a `FibKey::Vni` aliasing the same entry. `FibTable::del_fib` removed only the key it was given, so dropping the alias was a matter of the caller passing the vni the fib happened to be registered under -- which `FibTableWriter::del_fib` duly took as an argument, and passed on. That works only as long as every caller's idea of the vni matches the table's. `VrfTable` does keep them in step: `set_vni` calls `unset_vni` first, so a fib is never aliased under two vnis at once, and `remove_vrf` passes `vrf.vni`. So this was latent rather than live. It is the same shape as the next-hop resolution loop, though: an invariant held by discipline at a distance, with nothing in the types holding it, and one careless caller away from a `FibKey::Vni` that reaches a fib whose writer has been destroyed. The table does not need to be told. Each `FibTableEntry` records the identity of the fib it points at, and an alias shares the entry, so `del_fib` can find its own aliases: self.entries.retain(|_, entry| entry.id != id); With that, the vni argument to `FibTableWriter::del_fib` carries no information the table lacks, so it is gone -- which is the point. Restoring the invariant while leaving the argument in place would have left the trap. Found by a model-based property over the table: every key it holds reaches a live fib, and reaches it under its own identity. The counterexample was two changes long -- add a fib with a vni, delete it without one -- and the property fails again if `del_fib` goes back to removing a single key. The second half of that property is worth stating separately, because nothing else checks it: the thread-local read-handle cache keys on the identity the table reports for a key rather than on the key asked for, so an alias reporting the wrong identity would have two threads caching handles to different fibs under one name. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

`VrfTable::remove_vrf` took any `VrfId` and removed it, the default vrf included. `get_default_vrf` and `get_default_vrf_mut` then reach their `unreachable!()` -- they treat the default vrf's existence as given, and it is given everywhere except here. `Vrf::set_status` already says the default vrf cannot be deleted, and enforces half of it: it refuses to move the default vrf out of `Active`, so `remove_deleted_vrfs` and `remove_deleting_vrfs` never pick it up. Both production callers of `remove_vrf` sit behind that same `can_be_deleted()` check, and `Cpi`'s delete branches on `DEFAULT_VRFID` before it gets there. So, as with the fib alias, this was latent rather than live -- an invariant held by discipline at three call sites, stated in a comment on a fourth function, and enforced nowhere a caller has to look. Found by a model-based property over the vrf table, on a one-change counterexample. That property is the wider point of this commit. The vrf table is where four key spaces have to agree -- `by_id`, `by_vni`, each `Vrf`'s own `vni` field, and the fib table's `FibKey::Id` and `FibKey::Vni` spaces -- and nothing holds them together but its methods doing the right number of things in the right order. The model is one map, from vrf id to the vni and status it carries, and all four views are checked against it and so against each other: - `by_id` holds what the model says, each vrf carrying what the model says - `by_vni` is exactly the inverse of the vnis the vrfs carry, with no stale entry left by a removal and none missing after a vni was set - the fib table holds a fib per vrf, aliased by vni where there is one, and every key reaches a live fib under the right identity - the default vrf is present and active - `check_vni`, the in-tree half of this oracle, agrees Verified by breaking five separate updates: dropping the `by_vni` removal from `unset_vni`, the fib aliasing from `set_vni`, the `unset_vni` call that makes `set_vni` release the vrf's previous vni, the `by_vni` removal from `remove_vrf`, and the new default-vrf guard. Each fails the property, at four different assertions. Two hundred thousand cases pass. `VrfStatus` gains a derived `Debug` so a mismatch names the status it found. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

`IoBuffer` exists to cope with partial reads and writes on a stream socket. On the read side it got the distinction wrong, and the result is a live bug. `Frrmi::recv` sizes the read buffer for the read it is *about to attempt*: readb.buffer.resize(readb.used + len, 0); so after that call `buffer.len()` is what we hoped to have and `used` is what we actually got. `msg_len`, `next_read_len` and `is_ready` all consulted `buffer.len()`. Three consequences, in ascending order of how much they cost: **A header and a body arriving in separate reads killed the connection.** Read the 16-octet header, ask for the body, get `WouldBlock`: `buffer.len()` is now 17 for a one-octet body, so on the next pass `next_read_len` computed `1 - (17 - 16) = 0`, decided the message was complete, and called `recv` for zero octets. `read` into an empty buffer returns `Ok(0)`, which this code reads as end-of-stream -- so the frrmi raised `FrrmiPeerLeft`, dropped the socket and restarted, on the ordinary case of a response that does not arrive in one piece. It then retried the config, so the symptom is a reconnect loop rather than a stall, which is presumably why it has gone unnoticed. **A half-arrived header read as a complete one.** With fewer than 16 octets received, `buffer[0..8]` is partly the zeros `resize` wrote, so the announced length came out too small -- zero, if the received prefix of the length field happened to be zero, which is every short read of a header whose body length is a multiple of 256. `next_read_len` then returned 0 and `deserialize` sliced `buffer[16..used]` with `used` below 16, which panics outright in the routing thread. **The announced length was unbounded.** It comes off the wire and `recv` resizes to it, so a confused or hostile frr-agent announcing `u64::MAX` made `readb.used + len` overflow -- and a merely large announcement would have been a request to allocate that many octets. So: the three read-side predicates now count `used`, `IoBuffer::len` says in a comment that it means something only on the write side, `is_ready` subtracts 16 from `used` instead of adding it to a peer-supplied length, and a message longer than `MAX_MSG_LEN` is refused with `DecodeFailure`. Responses from the agent are a status word or an error message, so 16 MiB is generous by orders of magnitude; the bound is there to cap the allocation, not to constrain the protocol. Found by a round-trip property whose oracle is the message itself: serialize it, deliver its octets in generated chunks, and require what comes back out to be what went in. The first counterexample was `chunks: [16]` -- the header in one write and the body in the next. A second property runs the chunking across several messages on one connection, so a write may straddle a message boundary or carry two at once. Each of the three fixes was confirmed load-bearing by reverting it: reading `msg_len` off `buffer.len()` fails with a subtract overflow, counting `next_read_len` off it reproduces the original `Peer left`, and removing the length bound fails the absurd-length test with an add overflow. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

A route with no next-hops used to be accepted by `Vrf::add_route_complete` and put in the route trie, while `FibWriter::add_fibroute` refused it -- it rejects an empty key list. The rib and the fib then disagreed about the forwarding table, and disagreed in the worst direction: a packet matching that prefix falls through to a shorter one in the fib and is forwarded somewhere else, rather than dropped. Resolving via a default is how a routing loop starts. `add_route_rpc` knew this. It ended with: // If no next-hop was received with the route (or we could not successfully // process any), install the route anyway with an action drop. This is // better than not installing the route as that could break consistency // (e.g. resolving via a default) and cause a loop. if nhops.is_empty() { nhops.push(RouteNhop::default()); } Correct, well reasoned, and in the wrong place: one layer up, in a different module from the function whose contract it was upholding. It is the only production path into `add_route_complete`, so this was latent -- the fourth time on this branch that an invariant turned out to be held by a caller rather than by the function that depends on it. So the substitution moves into `Vrf::nhops_or_drop`, used by both `add_route_complete` and `add_route`. `add_route_rpc` keeps its warnings, since only that layer can tell "the control plane sent no next-hops" from "none of the ones it sent could be processed", but it no longer has to remember to inject anything. Found by a model-based property over the vrf's route table. Two structures move together on every route change -- the tries, and the `NhopStore` the routes hold `Rc`s into -- and a third, the vrf's `Fib`, is written through on the same calls. The model is one map, prefix to (next-hop keys, stale), and everything is checked against it: - the tries hold exactly the model's prefixes, each route naming the model's next-hop keys in order, with the model's stale flag - the next-hop store holds exactly the keys the routes name. One too many is a leak that keeps a stale fib group alive; one too few and a route names something nothing will resolve - `lpm` resolves for every address and lands where the model says, which is what keeps `lpm_v4`/`lpm_v6` and `check_deletion` off their `unreachable!()`s - the fib describes the same prefixes as the vrf Verified by breaking four separate things: removing the new substitution, not deregistering a replaced route's next-hops, not reinstalling a deleted default route, and letting `set_stale` mark the preset drop routes. Each fails a different one of the four checks above. Two hundred thousand cases pass. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

`Vrf::check_deletion` sits entirely behind `status == VrfStatus::Deleting`, and the property added in e36afa56d only ever held an `Active` vrf -- so the whole body, both of its `unreachable!()`s included, never ran. A coverage pass turned that up in a file the same commit had just reported at 95%. The transition matters: it is what moves a vrf from `Deleting` to `Deleted` once the only routes left are the two preset drop ones, and so it is what decides whether `VrfTable::remove_deleting_vrfs` ever picks the vrf up. The generator now draws status moves, and the model tracks the status and performs the same transition on route deletion. That needed one more thing in the model: whether a route is still the *preset* drop route, which is not the same as naming the drop next-hop. A generated route for a root prefix with no next-hops names it too, but carries a real origin, distance and metric, so `Route::is_preset_drop_route` says no -- and that is the question `check_deletion` asks. The check now asserts on it directly, which also reaches the conjuncts of `is_preset_drop_route` that short-circuiting had hidden. Production coverage of `rib/vrf.rs` goes 89.8% -> 93.9% (production lines only; `#[cfg(test)]` spans excluded, since llvm-cov counts test code as covered and a third of this crate's instrumented lines now are test code). Verified by breaking `check_deletion` two ways: dropping its `Deleting` precondition, and requiring only one root to be a preset drop route. Both fail the property. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

`VrfTable::refresh_non_default_fibs` and `refresh_fibs_by_vni` hand the default vrf to every other vrf as its resolution vrf. That is how a next-hop in an overlay vrf reaches an interface the underlay knows about, and it was the one part of next-hop resolution nothing had exercised: those two functions, `set_stale`, `remove_stale_routes` and `values_mut_except_default` were all at zero coverage, and every generated next-hop graph so far had lived inside a single vrf. Three properties over a generated topology -- vrfs with and without vnis, directly connected routes in the default vrf, recursive routes in the others: - a refresh resolves every other vrf's next-hops through the default vrf. The interface has to come from the default vrf's route, and the address has to stay that of the next-hop being resolved -- unless the resolver has an address of its own, in which case that one wins. The oracle is a longest-prefix match over the generated route list, which asks no next-hop anything. - `refresh_fibs_by_vni` refreshes the vrfs whose vni is named and leaves the rest untouched, checked by changing the underlay between a full refresh and a selective one and comparing against a snapshot. - marking everything stale and sweeping leaves every vrf holding only its two preset drop routes, the default vrf included -- it is swept separately from the rest, since it is their resolution vrf. All three also assert the rib-to-fib contract over the whole table: every entry in every fib is one the forwarder can execute. `FibEntry::is_valid` is the written-down half of that and `rib2fib` filters on it, but the drop injected for an empty group bypasses the filter, and nothing had checked the table at once. Verified by breaking three things: resolving each vrf against itself rather than the default vrf, dropping the vni filter, and skipping the default vrf in the stale sweep. Each fails a different property. The address half of `EgressObject::merge`'s rule -- first interface, last address -- is now pinned end to end, in the situation `rib2fib` describes it for: a next-hop supplies the layer-2 target "unless a next-hop deeper in the resolution chain provides one of its own". That needed the generator to draw underlay next-hops both with and without an on-link address of their own; without that, inverting the rule changes nothing observable. The interface half is not observable this way, and cannot be: the next-hop being resolved has no interface -- that is why it is being resolved -- and one that has an interface is not resolved further, so a chain never holds two. "First non-none" and "last some" therefore agree on every chain `lazy_resolve` will build. It stays covered by `squash_properties` at the unit level, which is where the distinction is visible. Production coverage of `rib/vrftable.rs` goes 73.1% -> 87.0%, and `routing/src` as a whole 58.8% -> 60.1% (production lines only; `#[cfg(test)]` spans excluded). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

`RouteNhop::from_rpc_nhop` looked the interface name up from `ifindex` against the interface table and put it in the `NhopKey`. The interface table is populated out of band from the routes, so the same next-hop off the wire keyed one way before we learned about its interface and another way after -- two `Nhop`s, two fib groups, two resolutions, for one next-hop. The file already argues against exactly this, thirty lines above, about the other derived field it could have put in the key: // Note: dmac is not set in nhops, because it may not be known when the // next-hop is added and the encapsulation is part of the next-hop key // which should be immutable for keying purposes. `ifname` is that: derived from `ifindex`, not known when the next-hop arrives, and part of the key. It also distinguishes nothing -- `NhopKey` is documented as holding "the properties that make a shared next-hop unique", and a name derived from an index that is already in the key is not one of them. So the lookup is gone, and with it the interface table argument to `from_rpc_nhop` and `add_route_rpc`. That is the part worth having: the invariant is now carried by the signature rather than by a test, since the conversion has no interface table to depend on. `IfTableWriter::as_reader` goes too -- the CPI route path was its only caller, which is itself evidence the dependency was only ever for the name. The cost is that `ifname` is now never populated in production. It reaches only a per-packet `debug!` in the forwarder, which already prints the ifindex, so nothing observable is lost -- but the field, and `EgressObject`'s copy of it, are vestigial. Removing them properly means touching `NhopKey`, `EgressObject`, `EgressObject::merge` and its property; worth doing, but as its own change. Found while giving `router/rpc_adapt.rs` its first tests. It translates `IpRoute`s and next-hops arriving from FRR over the CPI into routing state -- external input, the only production path into `Vrf::add_route_complete`, and it was at zero coverage. Four properties, with the wire message as the oracle: - a next-hop is refused for exactly the four reasons it should be (interface index zero, a vni that is not one, a vxlan next-hop that does not say which vtep to send to, and a forwarding next-hop with neither interface nor address), and otherwise yields the key the message describes - a route is installed with the origin, distance, metric and surviving next-hops the message describes -- or a drop next-hop if none survived - a prefix that cannot be parsed installs nothing - deleting the route the message names removes it and leaves the next-hop store holding only what the root routes need Verified by breaking six things: accepting interface index zero, keeping the ifindex on a vxlan next-hop, accepting a vxlan next-hop with no vtep address, dropping the connected-host-becomes-local rule, accepting a forwarding next-hop with nowhere to send, and installing a route for an unparseable prefix. Each fails. `router/rpc_adapt.rs` goes 0% -> 88.7% production coverage, `rib/rib2fib.rs` 90.7% -> 96.9% (the rpc path reaches its local-route branch), and `routing/src` as a whole 60.1% -> 61.4%. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

`router/cpi.rs` was at 1.8%. It is the layer above `rpc_adapt`: it picks the vrf, decides what a lookup failure means, and chains an operation's effects through the rest of the database. Seven properties over a whole `RoutingDb`, with an underlay route, an interface table and one overlay vrf on a vni. The one worth having is the evpn data path, end to end. An overlay route resolves through the underlay whether or not a router mac is known, but the encapsulation cannot be completed without one -- so until the mac arrives the only safe entry is a drop, and `Rmac::add` refreshing the fibs on that vni is what turns it into an encapsulate-then-egress with the right vni, remote and dmac. Breaking `VxlanEncapsulation::resolve` so it succeeds without a mac shows what that guards: the fib would offer [Encap(Vxlan { vni: 3000, remote: 7.0.0.1, dmac: None }), Egress(...)] which is a vxlan packet with no destination mac, put on the wire. Alongside it, and for the same reason, every entry is checked to be executable *and* to carry any `Drop` first. Resolution does produce `[Drop, Egress]` -- for an encapsulation that could not be completed -- and that is only safe because `packet_exec_instructions` stops at the first instruction that finishes the packet. Nothing said so; now something does. The rest: - withdrawing a router mac leaves the route forwarding. `Rmac::del` marks the entry stale rather than removing it and `resolve` accepts a stale one, so traffic keeps flowing to a mac that may have moved rather than the vni blackholing while the control plane catches up. Deliberate, and undocumented outside a one-line comment. - a route for a vrf we do not have fails on add, and is forgiven on delete until a config has been applied. The asymmetry is deliberate: a delete for a vrf we never had is a route we do not have either, so failing it would leave frr retrying something already true. - deleting the last route of a vrf on its way out takes the vrf with it, which is where `Vrf::check_deletion` and `VrfTable::remove_vrf` meet. - an interface address is refused unless both its mask and its interface index are usable, and lands in the interface table when it is not. - `nonlocal_nhop` spots a route whose next-hops live in another vrf. Verified by breaking five things: vxlan resolution succeeding without a mac, an rmac not refreshing its vni's fibs, an unknown vrf never being forgiven on delete, a deletable vrf being left behind, and an interface address skipping its mask check. Each fails. Production coverage: `router/cpi.rs` 1.8% -> 29.5% (the rest is the mio event loop and the socket plumbing, which needs a different harness), `routingdb.rs` 57.9% -> 84.2%, `interfaces/iftable.rs` 64.7% -> 81.4%, `iftablerw.rs` 58.1% -> 71.0%, `rib/vrftable.rs` 87.0% -> 91.7%, `rpc_adapt.rs` 88.7% -> 94.3%, and `routing/src` as a whole 61.4% -> 64.4%. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

`bfd`, `ospf` and `renderer/mod.rs` were at zero coverage and `vrf` at 19.6%. Each renderer had a test that printed its output and asserted nothing, so the code ran and no claim was ever made about it. A renderer's failure mode is not a crash. It is a BFD session, an OSPF area or a vni that never gets configured because a line was not emitted, or that gets configured twice -- neither visible anywhere but in FRR's own state. A round-trip oracle would need an FRR parser and is not worth building. What is worth checking is weaker and catches both: **every value the config holds appears in the output, and no value it does not hold appears.** Eight properties. The one the others cannot replace is `everything_configured_reaches_the_output`: a sub-renderer that works perfectly is no use if the top level never calls it, and only a whole-`InternalConfig` property sees that. Deleting either `render_vrfs_ospf` or the BFD peers from `InternalConfig::render` fails it and nothing else. The rest pin the rules that are not simply "render what is set": - a BFD source address is emitted only for a *multihop* peer. A single-hop peer with a source silently loses it, which is deliberate -- FRR has nowhere to put it -- and was written down only as a parenthesis in a comment. - a BFD section is not emitted at all when there are no peers, so an empty list does not leave a bare `bfd` / `exit` pair in the config. - the default vrf renders *without* a `vrf <name>` / `exit-vrf` wrapper: its configuration belongs at the top level, and wrapping it would put the underlay's static routes and vni into a vrf FRR does not have. - the four OSPF network keywords, written out independently so a transposed pair is visible. - rendering is deterministic. This one is about `frr-reload.py`, which diffs the output against what FRR is running: a rendering that varied would look like a configuration change every pass and reload FRR for nothing. Verified by breaking seven things: rendering a BFD source without multihop, emitting the BFD section when empty, transposing two OSPF network keywords, dropping an OSPF instance's vrf, dropping the OSPF and the BFD calls from the top-level renderer, and wrapping the default vrf. Each fails. One thing learned about the config model on the way, and recorded where the harness works around it: `VrfConfigTable` is a multi-index map with a *unique* index over `name`, `tableid`, `vni` and `vpc_id`, and an `Option` field's `None` counts as a value -- so it can hold at most one vrf without a vni, and at most one without a vpc id. Production satisfies that (the default vrf has neither, every other vrf is a vpc vrf and has both), but the types take `Option` and say nothing, and `add_vrf_config` calls a collision "a bug". Production coverage: `frr/renderer/bfd.rs`, `ospf.rs` and `mod.rs` 0% -> 100%, `vrf.rs` 19.6% -> 97.8%, `prefixlist.rs` 84.4% -> 95.6%, and `routing/src` as a whole 64.4% -> 66.5%. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

The interface table is a map, but two things about it are not. An interface's **attachment** names a vrf, which lives in a different structure and can be removed underneath it. Nothing in the types ties the two together: `VrfTable::remove_vrf` calling `detach_interfaces_from_vrf` is the whole of it, so the property checks the invariant that rests on it -- no interface is left attached to a vrf that has gone -- rather than trusting the one call site. That is the fourth structure on this branch where a reference outlives its referent only because one function remembers to clean up; the difference here is that the one function does. And a **reconfiguration has to leave the runtime state alone**. `mod_interface` replaces the name, description, type, admin state and mtu, and must not touch the addresses, the vrf attachment or the operational state -- none of which comes from the configuration being replaced, all of which is learned out of band. The model tracks both halves separately so that a reconfiguration touching the wrong one shows up. One asymmetry worth recording rather than fixing: an interface address for an interface the table does not hold is dropped, and the caller is not told. The error is raised inside `absorb_first`, where the only thing to do with it is log it, so `IfAddress::add` reports success. That is the same out-of-band-population hazard as the next-hop key in fa5398d01, but the consequence is much smaller: `Interface::addresses` is read only by the CLI and by the interface renderer, not by anything in the forwarding path. Noted in the harness where the model mirrors it. Verified by breaking six things: removing a vrf without detaching its interfaces, a reconfiguration clearing the addresses, a reconfiguration dropping the attachment, detach-from-vrf detaching every interface rather than that vrf's, attaching to a vrf that does not exist, and accepting a duplicate interface. Each fails. Production coverage: `interfaces/iftable.rs` 81.4% -> 94.1%, `iftablerw.rs` 71.0% -> 91.1%, `interface.rs` 75.9% -> 84.3%, and `routing/src` as a whole 66.5% -> 67.3%. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

The adjacency table is a map and its contents are dull. What is not dull is the *publishing*. `add_adjacency`, `del_adjacency` and `clear` each take a `publish` flag, and `AtResolver::refresh_atable_from_proc` depends on it: every poll clears the whole table with `publish: false`, adds back every entry the kernel reported with `publish: false`, and publishes once at the end. So the property is not about the map, it is about what a reader may see: > a reader sees the table as of the last publish, and never an intermediate state If it could see an intermediate one, the egress stage would find an empty adjacency table on every ARP poll and have no destination mac for anything. Breaking `clear` so it publishes unconditionally shows exactly that: the counterexample is two changes long and the failure message is "the table emptied under a reader mid-refresh". The model therefore holds two states -- what the writer has appended, and what a reader is entitled to see -- and the generator carries the `publish` flag on every mutation. A second test spells the same claim out in the shape the resolver uses, since that is the sequence whose failure has the consequence. Also three tests for the one part of the resolver that does not need `/proc`: resolving the device name an ARP entry carries to an interface index. Every entry the kernel reports goes through it and an unresolvable one is dropped, so the distinction between "no such device" and "a device whose index we cannot represent" has to survive -- the first is `Ok(None)` and drops the entry quietly, the second is an error that says why. `InterfaceIndex` is non-zero and the kernel should never report zero, but the number comes from outside. Verified by breaking four things: `clear` publishing unconditionally, an adjacency keyed by address alone so two interfaces collide, `del_adjacency` losing its key, and an interface index of zero becoming a miss rather than an error. Each fails. `atable/atablerw.rs` 66.7% -> 80.0%; `adjacency.rs` and `resolver.rs` were already at 85.4% and 79.7% from the live test that reads `/proc`, and did not move -- the new tests make claims about lines that already ran. `routing/src` as a whole 67.3% -> 67.4%, which is the honest measure of how little coverage was left to win here. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

Two packets of one new flow can reach a NAT stage at the same time. Packets of a 5-tuple usually land on one core, but nothing guarantees that, and each packet builds a pair of its own before inserting it. With a plain insert, whoever gets there second displaces the other's forward flow -- and only that half. The two reverse keys carry the allocations that made them, no two allocations agree, so the reverses never collide and the loser's is never displaced along with its partner. It stays in the table, live, mapping a translation whose allocation goes back to the pool as soon as the displaced forward half is collected. Return traffic for that public pair, once it has been handed out again, is then translated for whoever held it before. Two changes, either of which leaves a hole on its own. insert_if_absent stands aside when a live flow already holds the key, and reports that flow so the caller can go on with it. Arbitrating on one key is enough, because racing packets of a single flow share their forward key by construction: only whoever wins it inserts a reverse. A flow that is present but no longer live is displaced as before, since it is a corpse its timer has not swept yet and standing aside for one would drop a packet that could have replaced it. Displacing a flow now also invalidates the other half of its pair, wherever it happens. The race is not the only way to reach the orphan: the flow timer expires the two halves separately, so an expired forward half could be replaced by an ordinary insert while its partner was still live. That path needs no concurrency at all. Three tests, each of which fails against the code without its guard: a live flow keeps its key, a dead one does not, and displacing a flow takes its partner with it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com> Rebased onto a `related_pair` that is fallible and requires exactly one half of the pair to carry `INITIATOR`; both are invariants main gained after this was written. The test now marks the forward half and unwraps, matching the sibling test in `concurrent_fuzz.rs`.

daniel-noland · 2026-08-26T02:55:57Z

Its single commit now opens #1737, for the same reason as #1733.

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(config,mgmt,k8s-intf): generate valid configurations and property-test the validator #1737

Closed

daniel-noland force-pushed the pr/daniel-noland/fuzz-routing branch from b8475d0 to 315de5e Compare August 18, 2026 03:07

daniel-noland force-pushed the pr/daniel-noland/fuzz-flow-entry branch from c806fa7 to 731db9d Compare August 18, 2026 03:07

daniel-noland force-pushed the pr/daniel-noland/fuzz-routing branch from 315de5e to cb8dc50 Compare August 18, 2026 20:23

daniel-noland force-pushed the pr/daniel-noland/fuzz-flow-entry branch from 731db9d to 420ecb8 Compare August 18, 2026 20:23

daniel-noland force-pushed the pr/daniel-noland/fuzz-routing branch from cb8dc50 to 7fcf146 Compare August 18, 2026 20:31

daniel-noland force-pushed the pr/daniel-noland/fuzz-flow-entry branch from 420ecb8 to dfdf917 Compare August 18, 2026 20:31

daniel-noland force-pushed the pr/daniel-noland/fuzz-routing branch from 7fcf146 to 31459fb Compare August 18, 2026 20:38

daniel-noland force-pushed the pr/daniel-noland/fuzz-flow-entry branch from dfdf917 to 0c36ba2 Compare August 18, 2026 20:38

daniel-noland force-pushed the pr/daniel-noland/fuzz-routing branch from 31459fb to 0c3510b Compare August 18, 2026 23:17

daniel-noland force-pushed the pr/daniel-noland/fuzz-flow-entry branch from 0c36ba2 to 5d59ca1 Compare August 18, 2026 23:17

daniel-noland force-pushed the pr/daniel-noland/fuzz-routing branch from 0c3510b to d63ff7a Compare August 19, 2026 06:33

daniel-noland force-pushed the pr/daniel-noland/fuzz-flow-entry branch from 5d59ca1 to 809fc6d Compare August 19, 2026 06:33

daniel-noland force-pushed the pr/daniel-noland/fuzz-routing branch from d63ff7a to 1ab2290 Compare August 20, 2026 01:58

daniel-noland force-pushed the pr/daniel-noland/fuzz-flow-entry branch from 809fc6d to 64548d4 Compare August 20, 2026 01:58

daniel-noland force-pushed the pr/daniel-noland/fuzz-routing branch from 1ab2290 to d436cc1 Compare August 20, 2026 02:32

daniel-noland force-pushed the pr/daniel-noland/fuzz-flow-entry branch from 64548d4 to 695842b Compare August 20, 2026 02:32

daniel-noland and others added 10 commits August 21, 2026 09:13

daniel-noland and others added 23 commits August 21, 2026 09:13

mvachhar force-pushed the pr/daniel-noland/fuzz-routing branch from d436cc1 to 9df9cbe Compare August 21, 2026 15:13

mvachhar force-pushed the pr/daniel-noland/fuzz-flow-entry branch from 695842b to de3a6b8 Compare August 21, 2026 15:13

daniel-noland force-pushed the pr/daniel-noland/fuzz-routing branch from 9df9cbe to 20dc819 Compare August 26, 2026 02:55

daniel-noland closed this Aug 26, 2026

Navigation Menu

Uh oh!

fix(flow-entry): add an insertion that will not displace a live flow - #1736

fix(flow-entry): add an insertion that will not displace a live flow#1736
daniel-noland wants to merge 33 commits into
pr/daniel-noland/fuzz-routingfrom
pr/daniel-noland/fuzz-flow-entry

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!

daniel-noland commented Aug 26, 2026

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!

daniel-noland commented Aug 26, 2026

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