(scratch) test: track RFC 4787, and state its requirements as executable contracts - #1741
Closed
daniel-noland wants to merge 37 commits into
Closed
(scratch) test: track RFC 4787, and state its requirements as executable contracts#1741daniel-noland wants to merge 37 commits into
daniel-noland wants to merge 37 commits into
Conversation
|
Important Draft PR not reviewedDraft PRs are not automatically reviewed by default.
To automatically review draft PRs, update your CodeRabbit configuration: reviews:
auto_review:
drafts: trueComment |
❌ 1 Tests Failed:
View the top 1 failed test(s) by shortest run time
To view more test analytics, go to the Test Analytics Dashboard |
daniel-noland
force-pushed
the
pr/daniel-noland/fuzz-nf-probes
branch
from
August 20, 2026 02:32
b9930af to
75db938
Compare
daniel-noland
force-pushed
the
pr/daniel-noland/spec-compliance
branch
from
August 20, 2026 02:32
cd0205c to
604bbfe
Compare
daniel-noland
force-pushed
the
pr/daniel-noland/spec-compliance
branch
from
August 23, 2026 19:27
976db44 to
d49c061
Compare
Anything with a timeout is untestable in a useful way if its deadline comes
from the wall clock: the test either sleeps for real -- seconds of CI time per
case, flaky under emulation -- or it does not test expiry at all. The flow
table's expiry, the masquerade and port-forwarding timeouts, the stats
delivery schedule and the FRR reconnect timers are all in that position.
tokio can already pause and advance time, and the dataplane already runs on
tokio. What stopped that from working was an asymmetry:
deadline = std::time::Instant::now() + timeout // does not move
sleep_until(tokio::time::Instant::from_std(deadline)) // does move
The two agree at the moment a test pauses the clock and diverge immediately
after, so a paused clock bought exactly **one** time step. Measured: a flow
opened after a single `advance` is born with a deadline already in the past
and is dead on arrival, which looks exactly like a masquerade bug and is not
one.
Three call sites define every flow lifetime, and pointing those three at
`tokio::time::Instant::now()` makes multi-epoch time control work today. It
also breaks confusingly later, the first time someone innocently writes
`Instant::now()` in a fourth place -- the symptom is a timeout test behaving
strangely under a paused clock, which is a long way from the cause.
So: one place the workspace reads the time, and a lint that refuses the
others. `.semgrep/rules/no-std-time-direct.yaml` is the same shape as
`no-std-sync-direct.yaml`, for the same reason -- clippy sees the facade's
re-exports by canonical path, so the rule catches the call sites.
`clock` follows `concurrency`: a cargo feature selects the backend, not a
`--cfg`. That is what `concurrency` actually does, and it matters here because
a `--cfg` cannot pull in an optional dependency -- tokio would become a hard
dependency of everything that reads a clock. With a feature, production `net`
has no tokio at all.
* `clock::now()` -- `std` in production, tokio's pausable clock under
`virtual`. Enabled in the dev-dependencies of every crate that reads a
clock, so a test build gets the routed clock across the whole graph rather
than in one crate.
* `clock::system_now()` -- wall clock, deliberately **not** routed. tokio
pauses its monotonic clock, not the system clock, and the values that use
it are timestamps reported outwards rather than deadlines anything waits
on. It lives in the facade so the lint has one chokepoint.
* `Duration` is exempt and the lint says so. A duration is a plain value with
no clock in it.
Production cost is zero, and checked rather than assumed. From tokio 1.53.1:
#[cfg(not(feature = "test-util"))]
mod variant {
pub(super) fn now() -> Instant { Instant::from_std(std::time::Instant::now()) }
}
`cargo tree -p dataplane -e features -i tokio | grep -c test-util` is 0: dev-
dependency features do not unify into the production binary.
47 `Instant::now()` and 3 `SystemTime::now()` sites across 22 files and 11
crates, all migrated. Whole workspace builds, 100 test binaries pass, clippy
clean at `-D warnings`.
The lint was break-tested both ways -- a planted `std::time::Instant::now()`
and a planted bare `Instant::now()` are both caught, and the tree is clean
with them removed.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
(cherry picked from commit 33eddb1)
The masquerade properties deliberately stayed inside one flow lifetime,
because until the workspace read its deadlines through `clock` there was no
way to write these. With the deadlines and the timers on the same clock,
expiry becomes an ordinary subject.
These cost nothing. A property covering a minute of flow lifetime runs in
0.00s of wall clock, where the real-time version would cost a minute per case
and be flaky under emulation.
## The three dispositions
The design note asks that every piece of live state a configuration change
could touch be classified, and expiry is the same question asked of time:
* **preserved** -- a flow inside its lifetime keeps behaving identically. Not
assumed: the cheap way to implement expiry is also the cheap way to drop
something whose deadline has not passed.
* **invalidated attributably** -- a flow past its lifetime stops translating
and is dropped. The failure ruled out is not the drop but the *pass*:
forwarding a packet still addressed to a public tuple is a leak, not a
timeout.
* **never resurrected** -- an expired flow does not come back, and a flow
created *after* the clock moved works. That one needs three epochs and was
unwritable before.
Plus `traffic_extends_a_flow_past_its_first_deadline`, which is the regression
test for the facade itself: `reset_expiry_unchecked` was one of the three sites
reading the wall clock while the timer consuming its answer read tokio's, so a
refresh under a paused clock wrote a deadline in the past and *shortened* the
flow's life.
## And it found something
`a_live_flows_tuple_is_reissued_after_its_original_deadline` is a
reproduction of an unfixed defect, `#[ignore]`d so the branch stays green.
Run it with `cargo test -p dataplane-nat -- --ignored reissued`.
A flow is opened and refreshed every second, so it is unambiguously alive --
its replies are delivered correctly throughout. Once `MASQUERADE_ONEWAY_TIMEOUT`
of virtual time has passed since it was opened, a newly opened flow is handed
the same public address and port, and the replies that were reaching the first
tenant start reaching the second.
The threshold is exactly the one-way timeout, by bisection:
| advance | flow alive | tuple reissued |
| --- | --- | --- |
| 4s | yes | no |
| 5s | yes | **yes** |
So the allocation is reclaimed on the deadline the flow was *created* with, and
the refreshes that keep the flow alive do not carry it. `MasqueradeState` holds
the `Allocation` in the forward entry only, which is consistent with the
forward entry being reclaimed while the reverse entry survives and keeps
translating -- but that is where an investigation should start, not what it has
concluded.
Production sets `randomize(true)`, and with randomization the same sequence
draws a different port, so the collision is unlikely rather than impossible --
a matter of load and range size rather than of correctness. What is wrong in
both modes is the underlying state: a flow that is still translating no longer
owns the tuple it is translating to. Two tenants sharing a public tuple is a
tenant isolation failure.
This is the class of defect a controllable clock exists to find. Reaching it on
the wall clock needs six seconds of real time per attempt and the right
allocation pattern; here it is deterministic and free.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
(cherry picked from commit 9136018)
The third and last NAT flavour, and the one where the campaign's only confirmed configuration bug lived. That was found by reading code and pinned at the configuration level; this covers the stage. ## The direction is the point Static NAT and masquerade translate a **source** on the way out. Port forwarding translates a **destination** on the way in, so every property reads the other half of the five-tuple and the failure modes differ in kind. A masquerade mistake leaks one tenant's traffic to another; a port-forwarding mistake delivers the outside world to an address inside a tenant that never published it. Six properties: reversibility (the reply must carry the tuple the client used, or the client drops it), containment, injectivity, permission, frame, and stability. Three more in `expiry`, on a paused clock: a published service keeps answering while time passes, a service re-established after its flow expires reaches the *same* backend -- the rule is configuration and does not expire with the flow -- and the mapping stays injective across an expiry. ## Two things break testing turned up **The probes were judging packets that never reached the code.** A rule is keyed by `(source vpc, protocol)`, and the probe drew its protocol independently of the rule it addressed. Roughly half of them therefore matched nothing, and `nothing_is_forwarded_that_was_not_published` -- whose subject is exactly the packets that should not match -- passed for the wrong reason. The protocol now comes from the rule. This is the same class of mistake as the arrival-state ordering in masquerade: a harness that looks like it is testing something and is not. **The port-range guard has three gates, not one.** A port past the published range is refused independently by `RangeSet::lookup`'s upper bound, by `PortRange::contains` via `indexof`, and by the size-matched arithmetic in `map_port_to`. Breaking any one, or any two, still refuses the packet; the property only fires with all three broken at once. That is defence in depth rather than redundancy, and it is why the property looked vacuous at first -- it is not, the code is simply hard to break there. | break | fires | | --- | --- | | address mapping collapsed onto one target | injectivity | | target shifted one past the declared prefix | containment | | `requires_port_forwarding` ignored | permission | | all three port-range gates opened together | permission | | flow fast path fails | stability, and the service-answers-over-time property | ## Also `PortForwardingExposes` gets the block-and-family treatment the other two flavours got, plus one constraint they do not have: a rule is keyed by protocol, so two exposes naming the same protocol produce two rules with the same key and the second silently replaces the first. One protocol per expose, assigned by position. The injectivity sweep is capped and strided at 256 pairs. Enumerating a rule that publishes 256 addresses over 1024 ports costs a quarter of a million packets, and that property was spending its entire budget on two configurations; it now reaches eleven. One observation, not fixed: a packet whose port is outside the published range is dropped with `DoneReason::InternalFailure`. Nothing is internally broken -- the operator did not publish that port. Attribution, not correctness. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com> (cherry picked from commit 1f7a52b)
`FlowInfo` is the state every stateful NAT flavour shares. Masquerade, port
forwarding and the flow table all keep a flow alive by refreshing this object,
and every timeout in the datapath is ultimately a comparison against its
`expires_at`. It had **no tests of its own**.
## An algebra, one level down
The network function harnesses build a configuration from an algebra of
operations and judge the result by relations. This is the same idea at unit
scale and much cheaper for it: `Op` is the vocabulary a flow supports --
refresh it two ways, move its status, invalidate it, let time pass -- and the
headline property asserts an invariant after *every prefix* of a drawn
sequence rather than after one fixed order.
That shape is what the subject needs. `reset_expiry` is gated on status,
`extend_expiry` on a different subset of it, and both on the clock; a test with
a fixed order would walk one path through that lattice and call it covered.
## The properties
* **expiry never moves backwards** -- the invariant the whole mechanism rests
on. A deadline that moves earlier is a flow that dies while in use: the
timer fires early, the entry is dropped, and the NAT state goes with it.
This is also the invariant that was quietly violated while deadlines came
from the wall clock and timers from tokio's -- the comparison inside
`reset_expiry_unchecked` was between values from two different timelines.
* **a refused refresh changes nothing** -- the frame condition, and load
bearing: every production call site discards the result with `let _ =`, so
a refusal that had already moved the deadline would be a silent write
behind an error return.
* **a refresh is permitted exactly when the status allows** -- stated as an
iff, because a gate that is too permissive is the defect and a one-way
check cannot see it.
* **invalidating is idempotent and cancels the timer** -- `invalidate` is
reached more than once for the same flow as a matter of course. A flow
marked cancelled whose token still sleeps is an entry that lingers to its
original deadline.
* **a related pair refers to its partner** -- `related_pair` builds two flows
that each hold a `Weak` to the other, through `Arc::new_uninit` and raw
pointer writes, because neither can exist before the other. Nothing
exercised that round trip: that each `Weak` upgrades, and to the *other*
flow rather than to itself.
* **a pair needs exactly one initiator**, and **every status survives its
byte** -- the latter matters because the status is read back through a
`TryFrom` that panics on an unrecognised value.
## Break tested
Five breaks, each firing exactly one property and leaving the other six green:
| break | fires |
| --- | --- |
| refresh may move the deadline backwards | expiry never moves backwards |
| a cancelled flow may be refreshed | permitted-exactly-when |
| invalidate leaves the timer sleeping | idempotent-and-cancels |
| each half of a pair refers to itself | related pair |
| `invalidate_pair` forgets the partner | related pair |
## Coverage
`net/src/flows/flow_info.rs` 73.63% -> **81.09%** lines, 70.00% -> **100.00%**
branches. Workspace 76.69 -> 76.92% lines, 68.35 -> 68.51% branches, which also
carries the port-forwarding chapter.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
(cherry picked from commit 1d89608)
A masqueraded connection is two flow entries, forward and reverse.
`refresh_masquerade_state` refreshed only the one a packet happened to hit; the
partner was refreshed exactly once, on the transition into `Established`.
So a connection whose traffic runs mostly one way lets the other half expire
while it is still in use -- and that is the common case rather than a corner. A
download is almost all reverse packets. So is a DNS response, or any session
that mostly receives.
## Why it is worse than a dropped connection
`MasqueradeState` carries the `Allocation` in the **forward** entry alone. The
forward half expiring therefore releases the address and port while the reverse
half goes on translating to them. The allocator hands that tuple to another
tenant, whose replies arrive at the first tenant's still-live reverse entry.
Two tenants sharing one public tuple is a tenant isolation failure, not a
routing one, and nothing on the packet path shows it: every reply to the first
tenant keeps being delivered correctly the whole time. Only a *new* flow taking
the tuple reveals it.
## The fix
Refresh the partner on every refresh rather than on one transition.
`reset_expiry_unchecked` refuses to move a deadline earlier, so extending the
partner can only lengthen its life. This is what conntrack has always done: a
packet in either direction is evidence the whole connection is alive.
## How it was found, and why not before
By the flow-expiry properties, on a paused clock. Reaching it on the wall clock
needs five seconds of real time per attempt plus the right allocation pattern --
and `randomize(true)` in production makes the reissue unlikely rather than
impossible, so it would surface in the field as a rare, unreproducible
cross-tenant delivery.
The reproduction landed in this branch as an `#[ignore]`d test. It is replaced
by two passing properties:
* `both_halves_of_a_pair_outlive_one_sided_traffic` -- the mechanism, asserted
on the live flow count, because the packet path cannot see it; and
* `a_live_flows_tuple_is_never_reissued` -- the outcome an operator would feel,
kept separate because it would also catch a different allocator bug that
released a tuple for some other reason.
Reverting this fix fails exactly those two and nothing else, out of 198 tests in
the crate.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
(cherry picked from commit 8955bc3)
Every rate the dataplane reports passes through this, and it had no tests.
`rate.rs` covers the Savitzky-Golay filter beside it well -- differentiating
generated polynomials against the analytic derivative, a real oracle honestly
come by -- but the exponentially weighted moving average had none, and it is the
piece that is a function of *time*.
## No runtime needed, and that is worth noticing
`update` takes the `Instant` as a parameter rather than reading a clock, so it
is already dependency-injected and a property can hand it any timeline. That is
the shape the rest of the workspace had to be converted to: a function given the
time it should use needs none of the machinery in `clock`.
## The properties
No oracle: recomputing `data * (1 - alpha) + last * alpha` in the test would be
a second copy of the thing under test. These are the properties an
exponentially weighted moving average has by construction.
* the first sample is the average, not something averaged against zero -- the
alternative reads low for seconds after a restart, which is exactly when
someone is looking;
* the average never leaves the range of the samples seen (convexity);
* a constant input stays constant, at every spacing -- a rate that drifts while
the counter advances steadily is the most misleading thing this code could
do, because it looks like real traffic;
* a step is approached monotonically and never overshot;
* **a longer gap weights the new sample strictly more**; and
* reading the average does not change it.
## The clock property had to be strict, and break testing is what showed it
The time-weighting property was first written with `<=`. Replacing the
time-weighted `alpha` with a constant -- an implementation that ignores elapsed
time altogether -- **passed**: both runs return the same number, and "not
further away" is true of equal values.
That is the whole point of the file, so `<=` was close to worthless. It is now
strict, with the inputs bounded so the difference is bigger than floating-point
noise: gaps of 1ms to 1s against a tau of 1s, at least 100ms between the two
gaps, and samples at least 1 apart. Past a few multiples of tau every gap
saturates to "the new sample entirely" and there is nothing left to order.
| break | fires |
| --- | --- |
| weights swapped | time weighting |
| weights no longer sum to one | convexity, constancy, monotone step, time weighting |
| elapsed time ignored (fixed alpha) | time weighting |
| the weighting inverted | time weighting |
| the first sample averaged against zero | first sample, convexity, constancy, monotone step |
One more thing the tolerance taught: convexity has to be checked relative to the
magnitude. A weighted mean of values near 44,000 lands an ulp or two outside the
bound, which is thousands of times `f64::EPSILON` and not a violation of
anything -- an absolute tolerance there tests floating point rather than
convexity.
`stats/src/rate.rs` 69.24% -> 72.96% lines, 54.35% -> 63.64% branches.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
(cherry picked from commit b4ec636)
`VpcStatsStore` is what the gateway reports about itself over gRPC: per-vpc and
per-vpc-pair packet and byte counters, the latest rates, and the names those
numbers are labelled with. It had **no tests at all** -- 0% coverage.
Statistics are an odd testing target because being wrong is not an outage,
which is exactly why they are worth pinning. A counter that silently wraps, a
rate attributed to the wrong pair, or a name that outlives the vpc it belonged
to all produce numbers an operator will act on with no way to tell they are
wrong.
## An operation algebra again
The store has a small vocabulary -- add counts, add drops, set rates, record
both at once, prune to a live set, snapshot -- and the properties are invariants
over drawn sequences rather than statements about any one order. Two are
relations between operations, needing no oracle at all:
* `record_pair` must equal `add_pair_counts` followed by `set_pair_rates`,
checked by driving two stores in parallel. A compound operation that drifts
from the parts it composes is how two call sites come to disagree about the
same numbers.
* the pair table and the per-vpc table must not disturb one another. They look
like they should be linked -- a per-vpc total ought to be the sum of its
pairs -- and they are not: each is maintained independently by the caller.
Writing that down is the point, because a reader who assumes the link exists
will under-report, and a change that introduced it would make every caller
that maintains both double count.
## Pruning is the sharp one
`prune_to_vpcs` keeps a pair only if its source **and** destination survive. A
slip to `||` keeps half-dead pairs that report traffic to a vpc which no longer
exists and which nothing will ever clean up, because the next prune has the same
defect. Both directions are asserted -- keeps exactly the live set, and removes
nothing that is alive -- since "exactly" is two claims and a one-sided test
would pass for a prune that deleted everything.
Names are pruned by the same rule for a different reason: a name outliving its
vpc gets attached to whichever discriminant is allocated next, so an operator
reads one tenant's traffic under another tenant's name.
## Break tested
| break | fires |
| --- | --- |
| prune keeps a pair if *either* end is alive | pruning keeps exactly |
| names are never pruned | pruning keeps exactly |
| counters wrap instead of saturating | saturation |
| `record_pair` forgets the rates | compound equals parts |
| pair counts leak into the per-vpc table | table independence |
Each fires exactly one property and leaves the other six green. Note that the
wrapping break is caught by the saturation property and *not* by monotonicity --
correctly, since reaching `u64::MAX` needs the boundary case that property
constructs deliberately rather than the drawn values monotonicity uses.
## Coverage
`stats/src/vpc_stats.rs` 0% -> **94.96%** lines, no branches -> **100%**.
One note for anyone writing async property tests here: build the runtime
*outside* `bolero::check!` and enter it per iteration. A bolero body is
synchronous, so blocking on a runtime from inside one is refused at run time.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
(cherry picked from commit 5dc4307)
When a batch of packets is counted, the interval it covers rarely lines up with
the reporting window it has to be attributed to. `TimeSlice::split_count`
decides how many belong to the window that is closing and how many carry over --
and it is the only arithmetic in the collector that can silently change what the
gateway reports. It was entirely uncovered, along with the `TimeSlice` impls
beneath it.
The invariant that matters is **conservation**: whatever the two intervals look
like, the halves must sum to exactly the count that went in. A split that loses
packets under-reports; one that duplicates them reports traffic that never
happened. Neither surfaces as an error anywhere -- the number is simply wrong, in
a shape indistinguishable from a real change in load.
## Two asymmetries, documented rather than asserted away
Three properties failed on first run, and all three were mine. Both causes are
real behaviours a reader would trip on:
**A zero-length sample goes wholly outside.** So the function is discontinuous
at zero: a one-nanosecond sample inside the window is wholly inside, while a
zero-length one at the same instant is wholly outside. That is the guard against
dividing by zero doing its job, but it means "growing the overlap never loses
inside share" is false across that step, and the monotonicity property has to
start from a non-empty sample.
**A sample entirely *before* the window is salvaged into it**, not discarded --
where a sample after it carries over. Not symmetry, and deliberate: the window a
late sample belongs to has already concluded and been reported, so the
alternative to folding it into the current one is losing the packets. It falls
out of the mirror in `split_count`, reads like a bug on the way past, and now has
a property saying it is not.
## A redundant branch, found by break testing
Weakening `next.start() >= self.end()` to `>` changed nothing, which looked like
a gap in the property written for exactly that boundary. It is not: deleting the
branch outright also changes nothing, and the whole `stats` suite passes without
it. `Instant::duration_since` saturates at zero, so the general arithmetic
computes `count * 0 / duration` and reaches the same answer.
It is a fast path rather than a semantic gate -- it would have been load bearing
when `duration_since` still panicked on a negative difference. Left in place and
noted where a reader will look, because what makes the boundary half-open is the
arithmetic, not that branch.
| break | fires |
| --- | --- |
| `outside` computed independently of `inside` | conservation, swap consistency |
| the overlap ratio inverted | monotonicity |
| the disjoint short-circuit weakened or deleted | nothing -- provably redundant |
`stats/src/dpstats.rs` 50.87% -> 56.50% lines, 56.25% -> 72.97% branches.
## Not tested, deliberately
`stats/src/{vpc,spec,register}.rs` stay at 0%. They build metric names and label
sets -- a variation on the standing "do not test printers" rule, where the test
would assert that a string is the string it was constructed from. Noting the
exemption is as much as is worth doing.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
(cherry picked from commit 87acbab)
`rio.rs` had the worst branch coverage in the workspace -- 28.95%, with 54
of 76 branches unreached -- and the part of it that matters most was
untested for a mundane reason: exercising the stale window costs sixty
seconds of wall clock per attempt.
## What the window is for
When FRR restarts, every route we hold becomes suspect. FRR will re-send
what it still believes; whatever it does not re-send was withdrawn while we
were not listening. `set_stale_timeout` opens a sixty-second window and
`check_stale_timeout` closes it, sweeping what did not come back. Get it
wrong in one direction and withdrawn routes persist; in the other, live
routes are blackholed for the length of the window.
On a paused clock the window costs nothing, so the boundary can be pinned
exactly rather than approached from a safe distance. This is the first
thing in `routing` to use the facade for what it was built for.
## Properties
* `arming_the_stale_timeout_sweeps_nothing` -- the sweep happens on
expiry, not on arm.
* `the_stale_timeout_survives_its_own_deadline` -- `check_stale_timeout`
asks `deadline < now`, so landing exactly on the deadline leaves the
window open for one more poll. Only a driven clock can put a caller on
that instant at all; on the wall clock the case is unreachable.
* `the_stale_timeout_fires_once_and_then_disarms` -- `take_if` consumes
the deadline. A plain comparison would re-sweep on every later poll,
which is harmless for routes that are already gone but would keep
re-deleting vrfs the control plane had since re-created.
* `an_unarmed_stale_timeout_never_fires`.
* `a_deleted_vrf_outlives_the_window_and_no_longer` -- the same boundary
seen from the vrf table rather than from the deadline.
* `an_frr_restart_opens_the_stale_window` -- and sweeps vrfs that were
mid-deletion immediately, because nobody is going to finish deleting
them now.
* `a_refresh_with_no_peer_to_ask_is_not_marked_done` -- `NeedRefresh`
means *we* restarted and must ask FRR to re-send. With no peer address
there is nobody to ask, so the status deliberately stays outstanding.
Transitioning to `Connected` here would silently accept a database that
was never refilled.
* `the_settled_cpi_states_do_nothing` -- `cpi_status_check` runs on every
pass of the IO loop, so the states it ignores must be free of side
effects, or the loop would re-arm the window continuously and never
sweep.
## Break testing
Each break fires exactly the properties it should and nothing else:
* `<` to `<=` in the deadline test: the boundary property and the vrf
one.
* `take_if` to a non-consuming `is_some_and`: the fires-once property.
* dropping `set_stale_timeout()` from the restart arm: the restart
property.
* hoisting the `Connected` transition out of the `if let Some(peer)`:
the no-peer property.
* `remove_deleting_vrfs` to `remove_deleted_vrfs` on restart: the restart
property, on the vrf assertion rather than the timeout one.
## Coverage, honestly
Branch coverage moves 28.95% to 32.89%: 3 of the 54 missed branches. Line
coverage reads 66.25% to 82.38%, but that number is inflated -- the tests
live in the same file and count as covered lines. Measured against the
production half alone the gain is 29 lines, and uncovered functions drop
from 9 to 5.
What remains is the IO loop and the socket paths under it --
`cli_sock_restore`, `cli_wake_on_writeable`, `reregister` -- which need a
live peer on the other end of a unix socket rather than a clock. That is a
harness, not a property, and it is the obvious next step here.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
(cherry picked from commit 3f025a5)
The IO loop was reachable only by starting it and sleeping, so `rio.rs` had
the worst branch coverage in the workspace and `cpi.rs` was barely better.
Neither needed a production change to fix: the CPI and CLI sockets are
ordinary unix datagram sockets, and a test can simply be the peer on the
other end.
## What the tests are
`CpiPeer` binds the far end of the CPI socket and speaks dplane-rpc at the
loop exactly as FRR's plugin does. `RunningRio` starts the real loop and
stops it on drop. Nothing is stubbed, so readiness, the read, the decode,
the dispatch and the addressed reply are all under test rather than around
it -- a reply only arrives if the loop sent it back to the address the
datagram came from.
* `the_cpi_is_not_attended_until_it_is_unlocked`
* `a_connect_over_the_cpi_socket_is_answered`
* `a_request_before_any_connect_is_ignored`
* `without_a_config_additions_are_refused_and_deletions_are_not`
* `a_malformed_datagram_draws_a_notification_and_does_not_wedge_the_loop`
* `the_cli_survives_having_its_socket_path_removed`
## What driving it taught us
Every CPI test timed out on the first run. The cause is deliberate and was
not obvious: `CPSOCK` is registered `Interest::PRIORITY`, which mio maps to
`EPOLLPRI` alone. A unix datagram socket never carries out-of-band data, so
no readable event is ever raised and the loop is deaf to the CPI by
construction -- not by a flag somewhere in the dispatch. `RouterCtlMsg::
Unlock` reregisters it `READABLE | WRITABLE`. That is
`85515956a feat(routing): do not attend cpi until configured`, and it now
has a test, because registering the socket `READABLE` "to fix a bug" would
silently undo the feature and every other assertion here would still pass.
Deafness turns out to defer rather than drop: a datagram sent while the CPI
is unattended sits in the socket's receive queue and is served on unlock.
So unlocking replays whatever arrived while we were not listening, bounded
by `SO_RCVBUF` rather than by anything this code decides. The `last_pid`
guard in `handle_request` is what keeps that safe. The property asserts the
replay explicitly.
## Break testing, including one break that did not fire
* registering `CPSOCK` readable from the start: the deafness property.
* dropping the no-prior-connect guard: the connect-guard property.
* refusing deletions without a config: four properties.
* swallowing the reply on a decode failure: the notification property.
* watching for `MODIFY` instead of `DELETE | MOVED_FROM`: the cli property.
* rebinding the cli socket without re-registering it with the poller: the
cli property -- but only after it was rewritten.
That last one is the useful failure. The cli property first asserted that
the socket *path* reappeared, which a rebind-without-register satisfies
perfectly while answering nobody. It now asserts that a new client is
served, which is the behaviour an operator would notice. Same class of
mistake as the EWMA inequality earlier on this branch: the property was
weaker than it read.
Noted and left alone: dropping the `deregister` of the old fd in
`cli_sock_restore` fires nothing, because closing the fd removes it from
the epoll set anyway. Defensive rather than load-bearing.
## Coverage
router/rio.rs lines 82.38% -> 90.61% branches 32.89% -> 55.21%
router/cpi.rs lines 58.11% -> 81.79% branches 39.39% -> 74.24%
`cpi.rs` is the larger prize and it came for free: 130 lines and 23
branches, purely from driving the real socket rather than the functions
behind it. Against this morning's baseline `rio.rs` branch coverage is
28.95% -> 55.21%.
What remains uncovered is the frrmi connect and disconnect paths, which
need a live frr-agent on the other end, `cli_wake_on_writeable`, which
needs a response large enough to block, and the error-path closures.
## Fixture
`SockDir` gives each test its own directory and removes it on drop. The
paths must be unique under two execution models -- `cargo test` runs every
test in one process on many threads, `nextest` gives each its own process
-- so a process-global counter covers the first and the pid covers the
second, with no coordination between tests either way.
`test_rio_ctl` is moved onto the same fixture. It bound the fixed
`/tmp/hh_dataplane.sock`, which is the path a *running* dataplane uses, and
`open_unix_sock` unlinks before it binds; under nextest, which runs test
binaries concurrently, it could pull the socket out from under a real
dataplane or another copy of itself.
The CPI socket could have avoided the filesystem entirely -- Linux abstract
sockets have no directory entry and vanish when closed -- but the CLI socket
cannot: `setup_clipath_watcher` watches the parent directory precisely
because unlinking the path leaves the inode alive while the socket is open,
so no `DELETE_SELF` is ever emitted. An abstract name has no parent and
`Rio::new` would refuse it. Half a fixture's worth of cleanup is not worth a
new production affordance on a component we intend to remove.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
(cherry picked from commit cae4a14)
The frrmi's wire format is already covered in `frr::frrmi` against a
`UnixStream::pair()`. What was not covered is the loop's lifecycle around
it: connect, disconnect, restart. Those were three of the five functions
`rio.rs` never entered.
## This is not a fake FRR
The frrmi does not talk to FRR. It talks to `frr-agent`, a Hedgehog
component that sits beside FRR and applies configuration to it, over a
Hedgehog wire format. `FakeAgent` is a `UnixListener` at the frrmi path
impersonating our own agent and nothing else -- no FRR, no bgpd, no zebra,
nothing GPL, and nothing that needs a container to run. Running a real FRR
stack to close a unit-test gap remains off the table; that is what the vlab
jobs are for.
frrmi is `SOCK_STREAM`, so an accepted connection has an implicit peer and
none of the addressing trouble that ruled out `socketpair` for the CPI
applies.
## Properties
* `the_loop_connects_to_the_agent_whenever_it_appears` -- rio starts with
nothing listening, so its first connect fails. That is the normal case
rather than an edge one: the dataplane and the FRR container come up in
whatever order they come up in, and a loop that gave up after one
refusal would need a restart to recover.
* `the_loop_reconnects_when_the_agent_goes_away` -- `frr-agent` restarts
whenever FRR does, which is the moment the dataplane most needs to push
configuration back. A loop that held the dead socket would go on
believing it had a link and quietly stop applying anything.
* `nonsense_from_the_agent_restarts_the_link` -- the first four octets are
an announced length, so a burst of `0xff` announces an absurd message.
`frr::frrmi` refuses it; this asserts what the loop does with the
refusal. The connection is deliberately held open, so the restart can
only have come from the refusal and not from an end-of-file.
## Break testing, and one break that did not fire
Commenting out the per-pass `frrmi_connect()` fails all three. Turning the
`Err(e) => frrmi_restart()` arm into a bare log fails two.
Removing the `frrmi_connect()` from inside `frrmi_restart` fails nothing.
The loop attempts a connect at the top of every pass regardless, so that
call only saves the one iteration between the failure and the next pass --
latency, not correctness. Distinguishing it would need an assertion on how
*fast* the reconnect happens, and an absolute timing bound measures how busy
the machine is rather than what the code does; that is the same mistake the
vacuity floors made earlier on this branch. Recorded here instead.
## Coverage
router/rio.rs lines 90.61% -> 92.62% branches 55.21% -> 56.12%
frr/frrmi.rs lines 76.88% -> 81.18% branches 52.94% -> 56.86%
Uncovered functions in `rio.rs` drop from 5 to 3. The missed *branch* count
in `rio.rs` is 43 either way -- the percentage moves only because the test
code adds branches of its own -- so the honest gain here is in `frrmi.rs`,
which loses 16 lines and 2 branches, and in the three functions that now run
at all.
What is left in `rio.rs` is `cli_wake_on_writeable`, which needs a response
big enough to fill the socket buffer, `reregister`'s error closure, and
`new`'s.
## Still owed: the ValidatedGwConfig harness
Everything here and in the previous commit deliberately avoids needing a
configuration, because `RouterCtlMsg::Config` wants a `ValidatedGwConfig`
and building one in a test is a substantial piece of work in its own right.
That is a real gap rather than a stylistic choice. Without it the tests
cannot reach the paths that matter most: a route actually installed into a
fib, `reapply_frr_config` after an FRR restart, the config round trip
through frrmi and out to `ShowFrrmiLastConfig`. It wants doing, and it is
large enough that it should be its own chapter rather than an afterthought
appended to this one.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
(cherry picked from commit dd53180)
It is the last uncovered function in `rio.rs` and it is not reachable yet.
The next person to look at the coverage report deserves to know that before
spending an afternoon on it, so the finding goes next to the tests rather
than into a review comment.
`cli_wake_on_writeable` runs only when a response cannot be sent in one go:
the send fails with `WouldBlock`, the remaining chunks are cached, and the
socket is re-armed for writability so the cache drains when the client
catches up. Reaching it needs a response larger than the client's receive
queue.
Both halves of that were measured rather than guessed:
* The queue floor is the kernel's `SOCK_MIN_RCVBUF`. Asking for 1024 gets
2304. The chunk size is 2048.
* With no configuration applied, the largest response the dataplane can
produce is `ShowTracingTargets` at 1694 octets. Every route, vrf, fib,
adjacency and nat listing is a header over an empty table -- 20 to 454
octets each. `Help` is not even implemented on this path.
One chunk, comfortably inside one queue, with no way to close the gap.
Filling the queue with many small answers instead does not work: a client
blocked in a read consumes each answer as fast as the loop produces it, so
the depth stays at one. I wrote that test first, and it passed while
`cli_wake_on_writeable` executed zero times -- deleting the re-arm entirely
did not fail it. Making it fill would take a sleep between asking and
reading, which buys reachability with a timing assumption, and a sleep that
is too short fails by making the test vacuous rather than by failing. That
is the same trade rejected for the frrmi reconnect latency in the previous
commit.
So this is a second, concrete claim on the `ValidatedGwConfig` harness: with
a real configuration the route and fib listings are large enough that the
question answers itself, and no timing assumption is needed at all.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
(cherry picked from commit 0a8c199)
`RouterCtlMsg::Configure` carries a `RouterConfig`, not a
`ValidatedGwConfig`, and a `RouterConfig` is three lines: a non-zero genid
and one vrf. `validate` objects only to duplicate vnis and to a vtep that is
not set up, and `handle_configure` calls `db.set_config`, so `have_config`
becomes true and the CPI starts accepting additions.
That was the whole blocker. The previous two commits deliberately routed
around it, which biased everything written so far toward guards and
refusals -- `Add` was only ever reachable as an `Ignored`.
## Routes
* `a_route_the_control_plane_announces_reaches_the_fib` -- the point of the
CPI: a datagram on a socket becomes a forwarding entry. Decode,
dispatch, rib insertion, reconciliation and the left-right publish are
all in the path of one assertion.
* `a_route_the_control_plane_withdraws_leaves_the_fib` -- a withdrawal that
did not take forwards at a next hop the control plane has stopped
believing in, which no reconvergence elsewhere can clear.
* `announcing_a_prefix_twice_leaves_one_route` -- FRR re-sends its whole
table after a restart, so every prefix arrives again for one already
held. A fib that grew on each pass would double every time FRR bounced.
The first two fail when `route.add` or `route.del` is stubbed out. The third
is a structural guard rather than a behavioural one: routes are held in a
prefix-keyed trie, so duplication is not representable and no break is
available for it. It is worth keeping against a change to a multimap for
ECMP.
`fib_v4` filters `0.0.0.0/0`, which a fresh vrf carries so that traffic with
nowhere to go is dropped rather than leaked. Counting it made every
assertion off by one and would have hidden a withdrawal that removed the
wrong route -- that is how the first run failed.
## The FRR configuration round trip
`a_configuration_reaches_the_agent_and_its_answer_comes_back` drives the
other half of the dataplane's job: hand FRR the configuration it should be
routing under, and remember which generation was applied. `FakeAgent` now
reads the `|length|genid|body|` frame off the wire and answers in kind.
Fails if the config is never handed to the frrmi, and fails if the
acknowledgement is never recorded -- which matters because
`reapply_frr_config` consults exactly that after a restart.
## Reassembly, and why cli_wake_on_writeable still is not covered
`a_large_answer_arrives_whole` announces 8192 routes and reads back an
850KiB fib listing across some four hundred chunks. It fails if the "more"
octet is computed from the wrong end of the loop.
It does not reach `cli_wake_on_writeable`, and the reason recorded in
`ac7ce3f93` was wrong. A configuration was necessary but nowhere near
sufficient: 850KiB to a client that is provably not reading -- held off by a
causal barrier on the CPI socket rather than a sleep -- still never blocks
the send.
What bounds it is the *sender's* buffer. `open_cli_sock` sets the loop's
`SndBuf` to `CLI_RX_BUFF_SIZE`, 2048 * 8192, or 16MiB, and on a unix
datagram socket that is what limits outstanding unread traffic. `RcvBuf` on
the client does not help: pinned to the kernel floor of 2304 it still
accepts about 100KiB, because that ceiling is the sender's too. Reaching the
cache path needs roughly 16MiB of unread answer, on the order of 150,000
routes.
That is not a proportionate test for one function, so it stays uncovered
deliberately, with the measurements recorded next to it.
## Coverage
router/cpi.rs lines 81.79% -> 82.70% branches 74.24% -> 78.79%
router/rio.rs lines 92.62% -> 92.55% branches 56.12% -> 55.26%
The `rio.rs` percentages drift down because the new tests add branches of
their own; the missed count is what moved, and it did not -- the gain here
is in `cpi.rs`, which loses 5 lines and 3 branches, and in reaching the
route path at all. `rio.rs` branch coverage over the day is 28.95% -> 55.26%.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
(cherry picked from commit fa7b8b9)
A first run of cargo-mutants over `net/src/flows/flow_info.rs` -- a file
covered by seven properties and one I would have called done -- caught 13
mutants and missed 28. Nine of the survivors were noise; nineteen were real.
## The one that made the case
if new < current {
return Err(FlowInfoError::TimeoutUnchanged);
}
`<` to `==` was caught. `<` to `>` was caught. `<` to `<=` survived.
That is the same boundary class hand-broken in `rio.rs` earlier today, where
it *was* caught, because there I suspected it and wrote the property.
Suspicion is not uniform, which is the whole argument for the tool: it
breaks what I would not have thought to break.
Nor is it academic. `reset_expiry_unchecked` is what the masquerade expiry
path calls on both halves of a flow pair -- the defect this branch already
fixed once.
## The properties
* `the_unchecked_refreshes_move_the_deadline_exactly` -- the checked
wrappers were covered by whether they *refuse*; nothing said what the
unchecked ones *do* when they accept. Extension adds exactly its
duration; reset lands exactly on `now + duration`; and resetting to the
deadline already held is accepted rather than refused, which is the only
place `<` and `<=` differ. Reachable only on a driven clock: on a wall
clock two instants are never exactly equal.
* `a_flow_is_active_exactly_when_its_status_says_so` -- `is_active` is what
the datapath asks before using a flow. All three of its mutants survived
before this.
* `a_flow_built_with_a_status_has_it` -- `new_with_status` ignoring its
argument would make every test that seeds a non-default state pass for
the wrong reason.
* `a_genid_is_remembered_and_reaches_the_partner` -- halves that disagree
about their generation get swept apart, one retired and the other left
translating to an allocation nobody owns.
* `each_flag_predicate_answers_for_its_own_bit` -- a predicate answering
for the wrong bit translates the wrong end of the flow.
* `the_destination_vpc_is_remembered` -- a reader that always said `None`
is indistinguishable, from the packet path, from a flow that has not been
through the lookup stage.
## Result
before 13 caught, 28 missed, 16 unviable
after 32 caught, 0 missed, 15 unviable
No timeouts in either run.
## .cargo/mutants.toml
Two exclusion categories, both in config rather than as `#[mutants::skip]`
attributes, so production crates take no dependency on the tool:
* Printers, per the standing "don't test printers" rule. A mutated `fmt`
that nothing notices is the rule working, not a gap.
* `contract::` modules. The workspace convention puts bolero generators
next to the type they generate, so cargo-mutants finds them and mutates
the harness at itself; a generator drawing a different distribution is
not a defect in the code under test.
Plus `sysfs/**`, whose write path needs root and a real sysfs.
Nothing in CI depends on this. It is run by hand over a crate or a diff, and
the product is the survivor list rather than the score.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
(cherry picked from commit 81baac0)
`cargo-mutants` over `nat/src/masquerade/` left 52 survivors, and 23 of them
were in one file: very nearly every match guard in `next_flow_status_tcp`,
plus the DNS arm of the UDP patch and the single ICMP transition.
There were already four TCP tests -- `test_masquerade_tcp_establish`,
`_reset`, and both close directions -- and they are not weak: each caught
thirty-odd mutants elsewhere in the module. But they walk a sequence and
check where it ends up, so they never discriminate *which* guard fired.
Replacing a guard with `true`, or `&&` with `||`, left all four passing.
## What the machine is for
Nothing forwards differently because of the status. The flow's *lifetime*
follows from it, and a public address and port are held for as long as the
flow lives. A machine that never reaches `Closed` conserves nothing; one
that reaches it early releases a tuple that can be handed to another tenant
while the connection is still running -- which is the failure this branch
already fixed once, approached from the other end.
## Exhaustive, not sampled
The whole TCP input space is 2 actions * 10 statuses * 16 flag combinations
= 320 cases. Sampling that would be perverse when enumerating it makes the
coverage argument disappear.
## A table, and why that is allowed here
Elsewhere on this branch the properties deliberately avoid restating the
implementation, because an oracle that mirrors the code mirrors its bugs.
That objection has teeth when the oracle would grow into a second dataplane.
Here the oracle is the TCP close sequence, which is older than this codebase
and will outlive it, so writing it down is specification rather than
duplication -- and where the two disagree, the table is what should be
argued about.
It is derived from what the flags mean, not from what the code does. It
agreed with the implementation on all 320 cases, so no defect fell out; what
fell out is that the machine now has a written specification.
Two properties are stated separately from the table because they should be
readable without checking it row by row: a segment carrying none of the four
flags moves nothing, and `Reset` absorbs.
Beyond TCP: a UDP reply from port 53, 853 or 8853 closes the flow at once
(one lookup, one reply, and the tuple is released rather than held for the
ordinary UDP lifetime -- on a busy gateway that is most of the port space),
and an ICMP reply moves a one-way flow to two-way and nothing else moves at
all.
## Result
protocol.rs before 23 missed, 21 caught, 7 unviable
after 0 missed, 45 caught, 6 unviable
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
(cherry picked from commit 6d06966)
…is not
We have run cargo-mutants over three targets and closed two of them. The
measurements, the exclusions, and the shape the weekly report should take
are worth writing down before they are forgotten, because rediscovering
them costs about a day.
The note argues one thing above all: this is a report, not a gate. Mutation
testing usually collapses under its maintenance cost, and nearly all of that
cost comes from being able to block a merge -- once it can, every equivalent
mutant must be triaged and annotated forever. As a report, unkillable
mutants cost nothing, which is what makes it affordable at all.
The proposed release gate is therefore that every mutant is **classified**,
not killed: accepted, aspirational, or gap. Sorting them into three buckets
is most of the value, and it turns an intimidating number into a short list
plus an explicit decision.
Also recorded, because each cost real time to learn:
* the config must be `.cargo/mutants.toml`; a `mutants.toml` at the root
is silently ignored;
* caught mutants are not printed, only `MISSED` -- read a catch rate off
the console and the answer is wrong by roughly the catch rate;
* a red baseline voids the entire run and looks identical to a bad result
in the summary line, so a scheduled job must report it distinctly;
* our vacuity guards can in principle inflate the score by catching
mutants that made a property unreachable rather than wrong. Measured on
`nat/src/masquerade/`: eighteen tripped a guard, zero were caught only
that way. The hazard is real but narrow -- it matters where a guarded
property is the sole coverage of a path.
The report generator itself is not written. This is the design for it.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
(cherry picked from commit 3dc6897)
`check_full_payload` decides whether an ICMP error carries the whole of the
packet that provoked it. Its two length checks were expressed in bits where
the values are octets, and between them they enforced neither of the two
requirements RFC 4884 actually states.
## What the RFC says
RFC 4884 section 3 has two separate requirements:
* the "original datagram" field MUST contain at least 128 octets;
* it MUST be zero padded to the nearest 32-bit boundary (ICMPv4) or
64-bit boundary (ICMPv6).
## What the code did
if icmp_length > buf.len() || !icmp_length.is_multiple_of(32) { ... }
if padding_length < 32 && ...
`icmp_length` is `length_attribute * 4` for ICMPv4 and `* 8` for ICMPv6,
because the attribute counts 32- and 64-bit words. So it is a multiple of 4
(or 8) octets by construction, and a correct alignment check cannot fail.
`is_multiple_of(32)` instead demanded a multiple of 32 *octets* -- requiring
the length attribute itself to be divisible by 8, which nothing asks for.
Seven of every eight lengths a conforming sender can express were refused:
field 120 octets (30 words) -> refused
field 124 octets (31 words) -> refused
field 128 octets (32 words) -> accepted
field 132 octets (33 words) -> refused
Meanwhile the 128-octet minimum was not checked at all, so a 32-octet field
was accepted. The check that existed rejected valid messages and admitted
invalid ones.
`padding_length < 32` was wrong in the same way and in the other direction:
when the original datagram is shorter than 128 octets the sender pads it up
to 128, so legitimate padding is routinely more than 31 octets.
## The fix
Check what the RFC requires: at least 128 octets, no more than the buffer
holds, and the region past the original datagram is all zeroes. Drop the
alignment test, which is vacuous, and the padding bound, which was invented.
Each surviving check now carries the sentence it implements, in the citation
format duvet reads, so the next reader can check the code against the
specification without leaving the file.
## Severity
Low today and latent. `is_full_payload()` and `payload_length()` have no
callers anywhere in the workspace -- the flag is computed and never read --
so nothing forwards differently. It would have failed quietly, by declining
to treat valid ICMP errors as complete, whenever the feature was switched on.
## How it was found, and the part worth remembering
`cargo-mutants` left 22 comparison mutants alive in this file, which is what
sent me looking. But mutation testing did not find *this*; it found that
nobody was looking. The bug is a deviation from a specification, and no
amount of "the tests notice when I change this line" can see that.
Worse, the existing test actively concealed it. It padded a 120-octet
packet to 128 with the comment "we need to pad on a 32-bit word boundary" --
and 120 is already on a 32-bit boundary. The padding was there to satisfy
the code, and the comment rationalised it. Had I closed those 22 mutants
with a property asserting the behaviour I found, the deviation would have
become load-bearing, defended by a test, and cited by the next reader as
deliberate.
That is the failure mode: chasing survivors can entrench a defect as easily
as expose one, and only the specification can tell the difference. The
comment on the old test is corrected here for the same reason.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
(cherry picked from commit 8083be5)
`duvet report` matches citations in the source against the requirements it
extracts from a specification, so a requirement with nothing implementing
it, or an implementation with nothing testing it, becomes visible. RFC 4884
is the first specification tracked because the code already cites it: the
"original datagram" length checks contradicted it, and the citations added
with that fix are the ones this now reads.
## Everything but the reports is committed, on purpose
`duvet init` generates a `.gitignore` containing only `reports/`, and that
turns out to be load-bearing rather than a style choice. Measured under
`unshare -rn`:
* with `.duvet/specifications/` present, `duvet report` runs offline;
* with it removed, it fails with "Network is unreachable".
There is no cache anywhere else -- nothing in `~/.cache`. So vendoring the
specification text is what makes the report runnable in a build sandbox at
all, rather than a nicety. RFC 4884 costs 42KiB.
It also means an errata, a reformat, or a fetch that quietly returns
something different arrives as a reviewable diff in a pull request rather
than as a change in results nobody can account for. Refreshing a
specification becomes a deliberate commit.
## What the first run says
TEXT[!MUST,implementation,test]: ..."original datagram" field MUST contain at least 128 octets.
TEXT[!MUST,implementation,test]: ...MUST be zero padded to the nearest 32-bit boundary. [v4]
TEXT[!MUST,implementation]: ...MUST be zero padded to the nearest 64-bit boundary. [v6]
The ICMPv6 requirement is implemented and cited but has no test: the three
tests added with the fix are all ICMPv4. Found on the first run, which is
the point.
## Two adjustments
The generated `[[source]]` pattern is `src/**/*.rs`, which matches nothing
in a workspace; it is `*/src/**/*.rs` here.
`routing/src/cli/display.rs` had thirteen banner comments of the form
`//======== Fib ========//`. `//=` is duvet's citation marker, so each was
read as a malformed citation -- 24 errors before the report could run. The
banners now start `// =`. The collision is worth knowing about before
writing new ones.
## The snapshot
`.duvet/snapshot.txt` is line-oriented and diffs cleanly, and its unit is a
sentence somebody else wrote. Unlike a mutant's `file:line:col`, that key
does not move when a function is reformatted -- which is what makes it
usable as a gate where the mutation report is only usable as a report.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
(cherry picked from commit 34e13e0)
…m it
RFC 5382 states ten numbered requirements for how a NAT must treat TCP. It
constrains values this codebase already has and chose without reference to
it. Four are now cited; the other six are visible in the report as
uncovered, which is the point of tracking it.
## Conformant, with a test
* REQ-7, no port overloading. The allocator's bitmaps enforce it and the
exclusivity property in `masquerade::fuzz` asserts it -- "two live flows
never share a translation" was written before anyone read RFC 5382, and
turns out to be exactly REQ-7.
* REQ-10, an ICMP message must not terminate the mapping. Held by
construction: no arm of `next_flow_status_icmp` yields `Closed` or
`Reset`. The test that says so was written yesterday for other reasons.
Both are cited rather than changed. The value is that they are now *claims*
somebody can check, instead of accidents.
## Marked todo, because they are decisions rather than defects
* REQ-5, idle timeouts. "Established connection idle-timeout" MUST NOT be
under 2 hours 4 minutes; "transitory" MUST NOT be under 4 minutes. Ours
are 5, 3 and 2 seconds for the transitory states, and the established
timeout is `idle_timeout` from the masquerade config, which has no
default, no bound and no validation.
The short values look deliberate -- `protocol.rs` says the statuses
exist "to know how much to extend the lifetime of flows for port
conservation", and a gateway holding a public port for two hours per
idle connection conserves nothing. But whether we are willing to state
that as a deviation from a BCP is a product decision.
* REQ-1, endpoint-independent mapping. Not held as stated: the allocation
depends on `dst_vpcd`, so one internal endpoint reaching two destination
VPCs can be given two public tuples. RFC 5382 assumes a NAT facing a
single external realm; here destination VPCs are distinct address spaces
behind distinct peerings, and sharing a pool across them would be the
surprising choice.
So this is probably an exception rather than a defect -- and "probably"
is why it is `todo`. Answering it is cheap now; discovering it mattered
after a peer-to-peer application fails is not.
`todo` rather than `exception` in both cases deliberately. duvet has both,
and an exception asserts a decision was taken. Neither of these was.
Converting them needs a rationale somebody is willing to sign, and the
report is where that queue lives.
## What was checked and found fine
REQ-2 requires handling the TCP simultaneous-open. Traced through the state
machine: the flow sits in `OneWay` while the two SYNs cross, then the peer's
SYN-ACK moves it to `TwoWay` and the ACK to `Established`. It works. Not
cited, because sitting in `OneWay` for two extra round trips interacts with
the REQ-5 timeouts above, and citing it as conformant would overstate what
was verified.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
(cherry picked from commit 46b4c32)
…ill open Two specifications are tracked and the tool has already paid for itself, but nothing recorded where the method stops working. That boundary is not obvious and is expensive to rediscover, so this writes it down before more specifications are added. The audit behind it ran duvet's extractor over the entire RFC series, 9,827 documents in 23 seconds, twice: - It is deterministic. Two sweeps produced 68,257 emitted files that are byte-identical, and single-threaded output matches parallel, so snapshot regression gating is sound. - 35 documents fail loudly, all invalid UTF-8, nearly all pre-1990. - It is blind to lowercase normative language. RFC 8200 and RFC 3022 contain zero RFC 2119 keywords and never cite RFC 2119, so the two specifications closest to what this dataplane is cannot be tracked directly. This is the real boundary of the method. - Composite BCP files silently lose most of their content. BCP 127 is RFC 4787 + 6888 + 7857 concatenated; duvet keys requirements by section anchor, every member has its own section 5, and the last one wins. 42 requirements extracted where the three members separately yield 129, with no warning and exit code 0. RFC 4787 loses section 5, NAT Session Refresh, which is where the UDP timeout requirements live. The note also records the intended route around the lowercase problem -- duvet accepts a Markdown specification, so the obligations can be restated in RFC 2119 form in-repo -- together with the hazard that goes with it. That is the one place the method can certify itself: once we author the specification we control both sides of the match, and the cheapest thing to write is the requirement the code already satisfies. It is the entrenchment failure mutation testing has, moved up a level and much harder to see, so the rules for synthesis are written down next to the mechanism. The open-questions list is deliberately a list rather than a plan, and is expected to grow. It is in the repository so that it grows in one place. Also corrects the RFC 5382 requirement count in .duvet/config.toml. It states ten numbered requirements, REQ-1 through REQ-10; 22 is RFC 5508's clause count. (cherry picked from commit bec3879)
…m it A trial run, chosen to answer two questions: whether a second specification is cheaper than the first, and where the procedure hurts. RFC 4787 is the UDP counterpart of RFC 5382, so it lands on code that already carries citations. Answer to the first question: much cheaper, because the specifications overlap. Four of the nine requirements cited here are restatements of RFC 5382 clauses already cited on the same lines -- REQ-1 is RFC 5382 REQ-1 without the "for TCP" qualifier, REQ-3 is REQ-7, REQ-12 is REQ-10. Those took minutes and mostly consist of noting that one decision settles two citations. Answer to the second: the requirements that do not overlap are where the findings are. REQ-5, the UDP mapping timer, is a materially worse deviation than its TCP sibling and the reason is structural. RFC 5382 distinguishes "established" from "transitory" connections, which is what makes our five- and three-second constants arguable -- they govern states where a connection is opening or closing. RFC 4787 draws no such distinction. A UDP mapping is a UDP mapping and the timer is "the time a mapping will stay active without packets traversing the NAT", against a floor of two minutes. Traced through `next_flow_status_udp`, a plain request/response exchange creates the flow at `OneWay` (five seconds), the reply moves it to `TwoWay` (three), and only a second outbound packet reaches `Established` and the two-minute `idle_timeout`. One round trip and a four-second pause loses the mapping. That is short of the floor by a factor of forty, for all UDP that is not a resolver exchange, and REQ-5a does not cover it: that exemption is for timers specific to one IANA-registered application on one well-known port, not a blanket rule. The resolver fast-close in protocol.rs turns out to be exactly what REQ-5a describes, and is cited as such -- with the caveat that 8853 sits above 1023, so the exemption reaches 53 and 853 but not it. REQ-14 is cited onto an existing bare `TODO: Check whether the packet is fragmented`. The TODO was already right; it now says which BCP it is a TODO about, and records that REQ-14a wants out-of-order fragment handling that cannot become a denial of service vector. REQ-9, hairpinning, is a MUST with no implementation anywhere -- "hairpin" does not appear in the workspace. There is a real argument that it does not apply under masquerade, where a public tuple exists only for the lifetime of an outbound flow and is not something a peer can learn and dial. The argument is recorded next to the citation and the citation is still `todo`, because nobody who owns that decision has made it. REQ-3a is the first `exception` in the tree, and is what an exception is for: `setup.rs` excludes well-known ports for TCP and UDP alike, so a host sourcing from a port below 1024 is always translated above it and the requirement can never be met. That was decided -- the range is named, a flag carries it, tests hold it -- so it is recorded as a decision rather than as an omission. Also corrects a claim in the RFC 5382 REQ-5 note: the masquerade `idle_timeout` does have a default, `DEFAULT_MASQUERADE_IDLE_TIMEOUT`, of two minutes. It has no lower bound and no validation, which is the part that stands. Cited as the individual RFC. BCP 127 concatenates RFC 4787, 6888 and 7857, whose section numbers collide, and duvet silently keeps only the last. (cherry picked from commit 1994193)
… and measure it The overarching goal is properties at the abstraction an RFC is written at: configure the NF, feed it generated packets, assert something implementation independent. RFC 4787 REQ-1 is a good test of whether that lines up, because it is a statement about the NF that no unit can make. It does line up, and the property immediately refuted a comment written two commits ago. That comment said the mapping was endpoint-dependent only across destination VPCs, and reasoned from `allocate_v4`'s signature, which takes no destination address and no destination port. That looked like grounds to call the deviation architectural and probably defensible. `an_internal_endpoint_keeps_one_public_address` holds the internal endpoint fixed and moves the destination. Written first as the full REQ-1 claim, it failed on the first input drawn: 10.0.0.0:1 gets public port 1024 talking to 3.3.3.1:1 and 1025 talking to 3.3.3.1:2. Same destination address, same VPC, only the destination *port* changed. That is "Address and Port-Dependent Mapping" in RFC 4787 section 4.1 -- the most restrictive of the three classes and the one REQ-1 forbids. The cost is UNSAF traversal, which is the entire justification the RFC gives for the requirement. The dependence was never in the allocator's arguments. It is in being called again for each new flow, which is invisible at the allocator and visible at the stage. That is the argument for this level of testing in one sentence. What the committed property asserts is the half that holds. The public *address* is stable across destinations even when the port is not, which is REQ-2, "IP address pooling behavior of Paired". So the same two lines in `Pool::allocate` satisfy REQ-2 and miss REQ-1, and they are now cited as both -- the partial conformance case in its clearest available form. Verified against a break: swapping `reuse_allocated_ip` and `allocate_from_new_ip` so a fresh address is drawn per flow moves the public address from 172.16.0.0 to 172.16.0.1 and the property fails. 20/20 configurations built, 160 flows reached the assertion. REQ-1 stays `todo` rather than becoming an `exception`. An exception asserts somebody weighed the requirement and accepted the cost; that has not happened, and now that the cost is stated precisely it is worth asking for. Also carries the first use of `reason=` on a citation, which duvet permits on exception, implication, implementation and test but not on todo, and which must fit on one line -- a bare continuation is parsed as a second source. (cherry picked from commit 794605d)
…it is not held REQ-6 is a MUST: an outbound packet must keep a mapping alive. The module already had `traffic_extends_a_flow_past_its_first_deadline`, which refreshes with replies -- that is *inbound* refresh, REQ-6a, and only a MAY. The permitted behaviour was covered and the required one was not. Writing the missing test turned up a defect. Measured on a paused clock, control against treatment, with a five-second `OneWay` lifetime. Silent for eight seconds: the reply to the mapping is dropped, as expected. An outbound packet at four seconds, then the same probe at eight seconds: also dropped. The packet changed nothing. `refresh_masquerade_state` is where it comes from. Its `OneWay` arm yields `None` for the extension, so no outbound packet ever moves the deadline of a flow that has not yet had a reply. The comment there reasons about the reverse direction and treats `OneWay` as a corner case, which is what makes returning `None` look harmless. It is not a corner: it is the steady state of every outbound-only flow. Syslog, netflow, telemetry, a resolver query nobody answers -- each has its mapping torn down five seconds after its first packet however much it sends, and rebuilt on the next one. Once a reply arrives the flow reaches `Established` and outbound refresh does work, so REQ-6 is met for connections and missed for one-way traffic. That half is now asserted: three outbound packets a hundred seconds apart against a hundred-and-twenty second idle timeout, five minutes with nothing arriving from outside. Two details make the assertion mean what it says. The step is near the timeout, because a step comfortably inside the lifetime the previous packet already bought would pass with refresh deleted. And the probe comes after a delay longer than a `OneWay` lifetime, so a mapping that had been silently torn down and rebuilt by the last outbound packet is already dead when it is checked -- reissuing the identical tuple cannot fake a pass. Verified by breaking the `Established` arm to `None`, which fails the test on exactly that assertion. The `OneWay` gap is recorded as `todo` rather than `exception`, and deliberately not written as a test. A test pinning the current behaviour would make the deviation permanent, which is the entrenchment failure this whole exercise exists to avoid. (cherry picked from commit 8a262fa)
… determinism A deliberate move to a different species of requirement, to find where the method strains. Everything cited so far has been first order and unconditional -- do this, never do that, not less than this many seconds. RFC 4787 has two that are neither. REQ-11 is second order. It is not a requirement about a packet; it requires that the answers to the *other* requirements stay the same "at any point in time, or under any particular conditions". Citing it correctly needs two readings settled first. "Behavior" means the class from section 4, not the values -- section 4.2.1 explicitly permits random port assignment, so the allocator shuffling port blocks is not a violation, and a naive citation would have called it one. And the conflict the RFC is aimed at, in section 8, is port preservation with a fallback path, which does not exist here because nothing ever tries to preserve a source port. That leaves address pooling as the thing that could still change under pressure, and it does not. 254 hosts, 256 flows each, 65,024 flows against a public /24: the pool spills to a second public address and no internal host is ever given more than one. Pairing before the spill is pairing after it. Two structural facts fell out of measuring it. A single internal host can never break pairing, because its own source port space is exactly the size of one public address's port space -- 64,512 flows from one host stayed on one address with nothing denied. So the transition only exists under contention between hosts, which is why the probe needs 254 of them. It costs fourteen seconds against a suite that runs in four, so it is `#[ignore]`d as a characterization probe, following the precedent in acl/src/dpdk/dyn_table.rs. REQ-8 is conditional, and is the one that actually gives the method trouble. It does not state a behaviour; it states two and picks between them on a priority nobody has written down -- Endpoint-Independent Filtering "if application transparency is most important", Address-Dependent Filtering "if a more stringent filtering behavior is most important". Three probes against one flow classify what we do exactly: same address and port delivered, same address different port dropped, different address dropped. That is Address and Port-Dependent Filtering, the most restrictive of section 5's three classes, and it satisfies neither branch of REQ-8 -- we are stricter than the stringent option, which would let the second probe through. Stricter than a SHOULD asks is still a departure from it. Recorded as `todo` rather than `exception` because this reads as a consequence of keying the flow table on the whole five-tuple rather than a filtering policy anyone chose; what is missing is a recorded priority, not code. The filtering test is committed unignored regardless of how REQ-8 is resolved. An unsolicited packet reaching a tenant because it guessed a live public tuple is a security failure, and the second and third probes are what rule it out. It carries its own positive control: the first probe is delivered through the same path the other two are dropped by, so it cannot pass vacuously. Also confirms a FIXME in apalloc/setup.rs is unreachable rather than latent. It warns that a public range restricted to a port range is not modelled by the pools, which reads as a silent misconfiguration; in fact validation refuses such a config outright with "Port ranges are not supported with masquerade". (cherry picked from commit 7e5aa33)
The errata question was open with one concrete item attached to it: RFC 4884 has errata, and MIN_ORIGINAL_DATAGRAM_OCTETS was chosen without reading them. It resolves to nothing. EID 3 corrects Section 7's description of the Extension Header checksum, carries no RFC 2119 keyword, and so was never extracted as a requirement; our citations are all in Section 3 and Section 5, on the length attribute. RFC 4787, 5382, 5508, 6888 and 7857 have no errata of any status, so the 221 untracked requirements are erratum-free. Two traps in the corpus are worth more than the answer. RFCs_for_errata.txt misses ten RFCs that do have verified errata, including RFC 1191 -- every one verified after the index was generated, so the index is stale forward and the rendering is authoritative. And 524 of the 1,750 renderings carry an erratum as an endnote with nothing spliced into the body, because its original text is not a locatable quote, so diffing a rendering against the base text under-reports. RFC 2663 EID 400 turns out to matter without being a defect. Corrected, it warns that a NAT cannot assume a FIN or RST is the last packet -- which is what masquerade assumes when it invalidates the pair on Reset or Closed. RFC 5382 leaves that behavior unspecified and names the throughput argument for taking it, so this is a decision rather than an oversight, and now a recorded one. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> (cherry picked from commit 73a199e)
A duvet citation records that somebody read a requirement. It cannot record that the code still does what the sentence says, and it cannot record that the test cited `type=test` checks the same thing as the code cited `type=implementation`. Those are two independent readings of one sentence, and a refactor can separate them without either comment changing. `contract::rfc4787::Req12` is the predicate written once. The implementation calls it from a `debug_assert!`; the exhaustive state machine test calls it directly. Injecting a mutant that sends an established flow to `Closed` on an ICMP packet now panics at the implementation site with the two states named, rather than at whichever assertion happened to notice. This closes a live gap rather than only demonstrating the pattern. RFC 4787 REQ-12 and RFC 5382 REQ-10 are the same sentence, kept by the same function and proved by the same test, but only RFC 5382 carried a `type=test` citation, so REQ-12 stood at `[!MUST,implementation]` -- implemented, untested -- while the test that establishes it sat six lines away. Manual bookkeeping across two specifications is exactly what a shared predicate removes. Only local predicates belong in `contract`. REQ-1 relates two mappings made at different times, REQ-6 relates a packet to a timer, REQ-11 is a statement about the answers to the other requirements; none is decidable at a point and all stay in `fuzz`. Where a requirement can be encoded more strongly it should be, per development/code/avoid-global-reasoning.md, and then it does not belong here at all. An `rfc5382::Req10` alias was written and deleted. Nothing called it, the compiler said so, and an uncalled contract is the decoration this replaces. The snapshot in .duvet/ is not regenerated here: duvet is not on PATH outside the dev shell, and hand-editing the regression gate would defeat it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> (cherry picked from commit d1a850c)
`Requirement` replaces the inherent `check` method, so the convention cannot be got wrong by the next contract: a trait has one shape, an inherent method has as many as there are authors. `Violation` and its two `&'static str` fields are gone, replaced by a `thiserror` type per requirement carrying the values that broke it -- development/code/error-handling.md calls string errors "actively hostile", and nothing forced one here, since `before` and `after` were already in hand. The part worth having is `SPEC` and `ID` being `const`. duvet emits one TOML per specification section under `.duvet/requirements/`, so the tree already holds a machine-readable copy of every requirement tracked, and a `const` assertion over `include_str!` checks that the section a contract names really states the requirement it claims. Changing `REQ-12` to `REQ-42` now fails the build with E0080 rather than passing review. Dropping RFC 4787 from .duvet/config.toml would fail it too, and because `include_str!` is recorded in rustc's dependency information, re-extracting a specification rebuilds the check instead of leaving it stale. This is what the citation axis could not do on its own. duvet verifies that a quoted sentence matches the specification; it cannot verify that the code naming that sentence still exists, and nothing verified the reverse direction at all. `unreachable!` rather than `panic!` at the call site, per development/code/error-handling.md: reaching it is programmer error. It is guarded on `cfg!(debug_assertions)` first so the check does not run in release, and it names the specification URL, the requirement id and both states, so a failure is readable without opening the file. The trait method cannot be `const fn` on stable, which settles where the build-time tier lives: constraints over `const`s -- RFC 4787 REQ-5 bounds timers that are `const`s -- stay plain `const` assertions and are deliberately not `Requirement`s. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> (cherry picked from commit 86cd54b)
…not three Both clauses are uncited and unheld, and the reason is structural rather than a missing branch: there is no MTU anywhere on this datapath. net::interface::Mtu appears in ten files, all of them control plane -- config, the FRR renderer and interface-manager, which push it to the kernel over netlink. It reaches neither dataplane, pipeline nor nat. Cited at vxlan_encap because that is the one place the dataplane makes a packet larger, which is the condition RFC 4787 section 10 governs. Its only failure modes on size are mbuf headroom and the 2^16 ceiling of the IP length field, and neither is a link MTU. The finding worth taking to the team is the scope. This stage originates no ICMP error at all: TTL expiry drops on DoneReason::HopLimitExceeded where RFC 1812 asks a router for ICMP Time Exceeded, and nat::icmp_handler only translates errors that arrive. REQ-13, REQ-13a and the TTL case are one question -- does this gateway originate ICMP errors? -- whose answer needs an egress MTU first. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> (cherry picked from commit 017b881)
…t stale Nothing regenerated it, so the regression gate had drifted two commits after being introduced. `just duvet-check` now catches this. (cherry picked from commit 02860ac)
…ons apply The RFC enumeration answers the first open question and changes the plan for extending past NAT: the largest specification surface in the tree, RFC 8200 in `net`, is the one duvet cannot parse at all. (cherry picked from commit c1bb982)
Measured, because the worry that this method penalises delegation, generics and macros is reasonable and was half-right. Macros are the real blind spot: cargo-mutants emits nothing for macro-generated code, so a normative comparison written inside a macro body cannot be checked. Generics and trait defaults cost nothing. The REQ-3 citation was diagnosed here earlier as a delegation problem; the wrong region and the unviable mutants turn out to have separate causes. (cherry picked from commit 6236cb2)
The citation claimed more than the test checked, twice over. Refusing 124 does not state "at least 128" -- a check written `<=` refuses a conforming 128-octet field and passes that test -- and the minimum is implemented once per address family, so the ICMPv6 copy had no test at all. Found by `just spec-interlock`, which flips this requirement from decorative to held: 4 surviving mutants to 6 caught. (cherry picked from commit 187a8d5)
REQ-3 and REQ-7 sat on `allocate_v4`, which forwards to `allocate_from_tables` and decides nothing. Every mutant of it was unviable, so the interlock could not check the citation at all -- and a citation that nothing can break is not a claim. Moving it to the bitmap makes the claim checkable, and it immediately fails: of fourteen mutants the cited property catches four. The seven in the second-half path are unreached because no test exhausts 128 ports from one block, and one of those -- `|=` to `&=` -- is port overloading itself. The remaining three divert allocation to the second half but still yield unique ports, so they do not bear on this requirement. Recorded as a decorative citation rather than fixed here: closing it needs the property to drive a half-block dry, which is a change to what the generator produces, not to what it asserts. (cherry picked from commit 24b5b77)
One requirement, two tests, because they reach different code. The stage property states port overloading where it is observable -- two flows, one reply path -- but it draws a handful of ports, so it never fills a 256-port block and never enters the second half of the bitmap. Walking a region dry does. Nine of the ten mutants the interlock reported now die, including the one that replaced the bit marking a port used. The test is unchanged: it already asserted this. Only the citation was incomplete, which is a failure mode duvet cannot see -- a requirement can be fully tested and still name the wrong test. (cherry picked from commit ad57787)
lie The interlock is no longer one check but an ordered three: coverage, then mutation, then a person. The order is the point -- coverage can fail a citation outright without building a mutant, which is what makes the expensive tier affordable. What the RFC 4787 REQ-3 case taught is worth more than the finding. A citation can sit on the wrong code, and it can sit on the right code while naming the wrong test -- the requirement was already fully tested by a test nobody had cited. duvet cannot see either, and only `no-mutants` catches the first, which is why it is not a pass. (cherry picked from commit 4332534)
A comment saying where a citation used to sit, or which tool moved it, is only legible to somebody who was there. What constrains the code is why the citation belongs where it is. (cherry picked from commit bcbab7a)
`clippy --all-targets` fails on this branch without it, which makes it useless as a gate for everything else. Unrelated to the surrounding work. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> (cherry picked from commit 1a797a6)
daniel-noland
force-pushed
the
pr/daniel-noland/fuzz-nf-probes
branch
from
August 26, 2026 02:55
75db938 to
1017959
Compare
daniel-noland
force-pushed
the
pr/daniel-noland/spec-compliance
branch
from
August 26, 2026 02:55
d49c061 to
762b44a
Compare
Collaborator
Author
|
Recreated with a corrected base after the stack was reordered into chapters. GitHub will not re-base a PR that is part of a stack, and these were never out of draft. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Scratch PR. Parking the specification-compliance line of work so it is pushed and reviewable;
not proposed for merge in this shape. Stacked on #1738.
What is here
Nine commits, continuing the duvet work already in the stack (RFC 4884 and RFC 5382 landed earlier).
Tracking RFC 4787 — the UDP counterpart of RFC 5382, 14 numbered requirements landing on the
same masquerade code that already carries RFC 5382 citations. Cited as the individual RFC, never as
BCP 127: that composite concatenates RFC 4787, RFC 6888 and RFC 7857, whose section numbers collide,
and duvet silently keeps only the last — 42 requirements where the three separately yield 129.
Findings recorded, not fixed. REQ-1 (mapping is address-and-port-dependent), REQ-8 (filtering is
stricter than either branch the RFC offers) and REQ-9 (no hairpinning) are one decision, not three:
this gateway is deliberately not UNSAF-traversal-friendly, or it is not deliberate and is a much
larger piece of work. REQ-13 is the same shape — this dataplane originates no ICMP error at all, and
has no MTU anywhere on the datapath to originate one from. All
todorather thanexception,because nobody has ruled.
Executable contracts.
nat/src/masquerade/contract.rsstates RFC 4787 REQ-12 as aRequirementthe implementation calls from a debug-only assertion and the test citedtype=testcalls directly, so the two citations are provably about the same predicate.
SPECandIDareconstand checked against duvet's extracted requirements at compile time: a citation naming arequirement its specification does not state now fails the build with
E0080.Errata. The corpus's
inline-errata/was audited. RFC 4787, 5382, 5508, 6888 and 7857 have noerrata of any status; RFC 4884 has one, and it does not touch us.
Open, and deliberately not done here
.duvet/snapshot is not regenerated — duvet is not on PATH outside the dev shell, andhand-editing the regression gate would defeat it. RFC 4787 REQ-12 should move to
[!MUST,implementation,test]on the nextduvet report.just duvetrecipe yet.development/code/spec-compliance.mdcarries a live open-questions list, expected to grow.time, only
.duvet/which is committed.Checks
cargo test -p dataplane-nat210 pass, 1 ignored. clippy and fmt clean ondataplane-natanddataplane.🤖 Generated with Claude Code