spec by daniel-noland · Pull Request #1757 · githedgehog/dataplane

daniel-noland · 2026-08-26T02:59:37Z

No description provided.

coderabbitai · 2026-08-26T02:59:43Z

Important

Draft PR not reviewed

Draft PRs are not automatically reviewed by default.

Trigger a manual review

To automatically review draft PRs, update your CodeRabbit configuration:

reviews:
  auto_review:
    drafts: true

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

codecov · 2026-08-26T17:53:51Z

Codecov Report

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

Files with missing lines	Patch %	Lines
nat/src/masquerade/expiry.rs	75.20%	31 Missing ⚠️
nat/src/masquerade/fuzz.rs	72.34%	8 Missing and 5 partials ⚠️
net/src/headers/embedded.rs	94.50%	2 Missing and 3 partials ⚠️
nat/src/masquerade/apalloc/display.rs	78.57%	2 Missing and 1 partial ⚠️
nat/src/masquerade/protocol.rs	60.00%	1 Missing and 1 partial ⚠️
net/src/icmp4/mod.rs	85.71%	1 Missing and 1 partial ⚠️
net/src/icmp6/mod.rs	85.71%	1 Missing and 1 partial ⚠️
nat/src/portfw/portfwtable/objects.rs	96.77%	1 Missing ⚠️

📢 Thoughts on this report? Let us know!

`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 section 3 states: the "original datagram" field MUST contain at least 128 octets, and 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. So: check what the RFC requires -- at least 128 octets, no more than the buffer holds, and the region past the original datagram all zeroes. The alignment test goes, being vacuous, and the padding bound goes, being invented. Each surviving check 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 is 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. The part worth remembering is how it stayed hidden. `cargo-mutants` left 22 comparison mutants alive in this file, which is what prompted a closer look -- 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 this line changes" 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. Closing those 22 mutants with a property asserting the behaviour as found would have made the deviation load-bearing, defended by a test, and cited by the next reader as deliberate. 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. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

`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. 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. Two adjustments. The generated `[[source]]` pattern is `src/**/*.rs`, which matches nothing in a workspace; it is `*/src/**/*.rs` here. And `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. `.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. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…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`, and the test that says so was written 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 defaults to two minutes and has no lower bound and no validation, so a deployment can set it anywhere. 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. REQ-2, handling the TCP simultaneous-open, was traced through the state machine and works: 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`. 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. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…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. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…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. The first answer is 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. The second answer is that the requirements which 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. Cited as the individual RFC. BCP 127 concatenates RFC 4787, 6888 and 7857, whose section numbers collide, and duvet silently keeps only the last. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The 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 lines up, and it settles the question REQ-1 was left `todo` over. The open reading was that the mapping is endpoint-dependent only across destination VPCs, reasoning 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. 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. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

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. 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. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

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". Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

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 matters 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 behaviour unspecified and names the throughput argument for taking it, so this is a decision rather than an oversight, and now a recorded one. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

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. 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. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

`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. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…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. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…t stale Nothing regenerated it, so the regression gate had drifted two commits after being introduced. `just duvet-check` now catches this. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…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. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The rule is one sentence: cite the narrowest region whose mutation would violate the requirement. It is worth stating because the obvious alternative -- cite the function whose name matches the requirement -- is what produced the RFC 4787 REQ-3 result, and because there is a live worry that a citation model tied to source regions penalises delegation, generics and macros. Measured, it mostly does not. Generics and trait defaults cost nothing, and the RFC 4884 finding is what the alternative costs: the same check written twice, once per address family, with the v6 copy untested and uncaught. 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. The REQ-3 citation was diagnosed as a delegation problem, and that ran two separate causes together. Citing a thin forwarding function is a genuine error -- the requirement lives in what it forwards to. Its mutants being *unviable* is a different problem: cargo-mutants replaces a function body with a synthesised return value, so an elaborate return type defeats it whatever the abstraction. An unviable region is not evidence of over-abstraction; it is evidence that nothing there was checkable. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

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. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

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. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

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. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

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. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

duvet is deterministic and takes milliseconds, so it can gate where the interlock -- hours of mutation testing -- cannot. Both steps land in this chapter rather than with the recipes they call, because they need the specifications this one vendors: without `.duvet/` the gate refuses to run. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

`payload_length` indexes octet 5 (v4) or 4 (v6) of what it is given, which is where the length attribute sits in an ICMP error message. It was given `cursor.inner` -- the whole frame. `Reader::inner` is never advanced (`consume` only decrements `remaining`) and `Headers::parse` hands it the buffer at the Ethernet header, so the octet read is the last byte of the destination MAC. Every other argument at that call site slices to the unread part; this one did not. So `check_full_payload` has been deciding whether an embedded packet is whole against a MAC address, for exactly the types NAT has to translate -- `supports_extensions` is Destination Unreachable, Time Exceeded and (v4) Parameter Problem. The header is nameable only at the top of `parse_payload`: `Headers::parse` consumed it immediately before, so it is the `size()` octets ending where the unread buffer begins, and the embedded headers are consumed after. Hence taking the reading first. Nothing caught it because nothing exercises the call site. All seventeen uses of `is_full_payload` are in `embedded.rs`'s own tests and every one calls `check_full_payload` directly with a length of its own -- which is also why the RFC 4884 citations on that function pass. The read is bounds-checked rather than argued: a malformed packet must not panic the dataplane. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>

RFC 4884 section 3 lists two ICMPv6 messages that may carry an extension structure, not three: An ICMP Extension Structure MAY be appended to ICMPv6 Destination Unreachable, and Time Exceeded messages. The sentence is in .duvet/specifications/, vendored by this PR, and the code beside it said otherwise. ICMPv6 Parameter Problem uses bytes 4 through 7 for its 32-bit Pointer, so treating octet 4 as a length attribute read the top byte of that pointer and multiplied it by eight. The v4 list is right to include Parameter Problem -- section 4.3 gives it a one-octet pointer and a length attribute at octet 5. The two lists differing is what makes this easy to get wrong by symmetry, so the sentence that settles it is now quoted on the function, and duvet refused the first draft of that citation for naming the wrong section. Signed-off-by: Daniel Noland <daniel@githedgehog.com>

`NatPool::for_range` seeds the bitmap with every offset in the region, capped at `u32::MAX`. Any public range of /96 or shorter therefore saturates at 2^32 entries, and a v6 /64 -- the size an operator actually writes -- is exactly that. `ips_in_bitmap` walked those one bit at a time, doing a `BTreeMap` lookup per offset to turn it into an address and then coalescing the results back into ranges: four billion lookups to print, for a pool with nothing allocated, one line. `roaring`'s `Iter::next_range` yields a whole run per step, so the cost is one iteration per run and runs are bounded by what has been allocated. The lock mattered more than the minutes. `Display` held the pool's read guard for the entire print while `allocate_ip` and `deallocate_ip` want it for writing, so rendering a v6 pool stalled every new masqueraded flow in it. The guard now covers a snapshot -- the ranges, and an upgrade of each live address -- and formatting happens after it is released. That upgrade is still what makes releasing safe: `AllocatedIp::drop` takes the same lock for writing, and holding a strong reference means none of the addresses examined here can be the last. The hand-rolled coalescing goes with it, `unreachable!()` arm included. A run of offsets is a run of addresses only while the mapping is a single linear translation, which is all `for_range` builds; that is now asserted rather than assumed, because the type is shaped to hold more. The regression test uses a stopwatch for an oracle without asserting on one: before this, printing a /64 pool does not return, and a test that does not return is a failure the runner reports by itself. Signed-off-by: Daniel Noland <daniel@githedgehog.com>

`a_large_answer_arrives_whole` announced eight thousand routes before reaching its subject, and `announce_routes` is a send and a `recv` per route against `PATIENCE` as a per-`recv` socket timeout. On a loaded runner one of those reads missed its ten-second window and the test failed in `CpiPeer::recv`, having never exercised reassembly at all -- in `check/debug`, not only under coverage. Tuning the count against a measurement does not fix that: the next runner is slower or busier and the measurement is stale. Making the setup cheap enough that it is not the thing under time pressure does. 256 routes is fourteen chunks and thirty-two times less work, with the same assertions. Nothing is lost. The failures worth catching -- a reassembly that loses its place, a "more" flag set from the wrong end of the loop -- show in a handful of chunks, and the boundary that would be interesting, `cli_wake_on_writeable`, needs about a hundred and fifty thousand routes. Eight thousand did not come close either, which the doc comment already said. The bar is now stated in chunks rather than as `100 * 2048`, since chunks are what reassembly loops over. Signed-off-by: Daniel Noland <daniel@githedgehog.com>

`NatFlowStatus::OneWay` means two different things and got one rule. For UDP and ICMP it is the *steady* state of a flow that never gets a reply -- `next_flow_status_udp` leaves it only on an inbound packet -- so it is where syslog, netflow, telemetry and an unanswered resolver query live for their whole lives. Returning no extension tore such a flow down five seconds after its **first** packet however much it sent, and drew a fresh public port each time it was rebuilt. That is RFC 4787 REQ-6's outbound refresh behaviour being "False" in the one state where a UDP mapping actually lives, and the citation on that arm becomes an implementation rather than a todo. For TCP it is a half-open connection -- `next_flow_status_tcp` leaves it only on a SYN-ACK -- so an outbound packet is a retransmitted SYN. That is evidence nobody answered rather than evidence the connection exists, and refreshing on it would let a half-open connection hold a public tuple for as long as the sender retries. RFC 4787 is the UDP document and does not ask for it. The interval is unchanged at five seconds, and the REQ-5 deviation that makes it short against a two-minute floor stays a todo: the defect was measuring the leash from the first packet rather than the last, and lengthening it is a separate decision. The regression test needed two attempts, and the reason is in its doc comment: the allocator is deterministic under `set_randomize(false)`, so a flow that is torn down and rebuilt is handed the same tuple back and every outbound-side observable looks identical either way. What separates survival from rebuild is an inbound packet after a gap, past the deadline the first packet set and inside the one the last packet set. Signed-off-by: Daniel Noland <daniel@githedgehog.com>

…ured `check_full_payload` compares two lengths -- `full_packet_length`, derived from the embedded IP header, and the RFC 4884 length attribute -- and both are offsets from the *start* of the original datagram. The buffer and remaining count it was given began `consumed` octets later, after `cursor.consume` had moved past the embedded headers. So the padding check indexed `buf[full_packet_length..icmp_length]` past the end of the field and into whatever followed it, and the no-extension case compared a whole-datagram length against a headers-excluded remainder. `parse_with` on the line above was already being handed the right slice; it is now shared. Two commits have corrected arguments at this call site now -- the length attribute read from the Ethernet header, and this -- and neither was catchable by the tests that existed. All seventeen uses of `check_full_payload` call it directly with a buffer and lengths of their own, so what the caller passes was never exercised. `an_icmp_error_from_the_wire_reports_a_full_payload` starts from a frame instead, which is the only place either defect is visible; it fails on the previous window and would have failed on the previous length. Still latent either way: `is_full_payload` has no caller in the workspace. Signed-off-by: Daniel Noland <daniel@githedgehog.com>

`validate_ruleset` returned `Ok(())` unconditionally, so `update_table` was infallible. The rules are installed later, inside `Absorb::absorb_first`, which returns nothing -- so a rule `add_entry` refused was logged and dropped while the caller was told the update succeeded, and the table held fewer rules than the configuration asked for. `mgmt`'s "whatever the validator accepts, the dataplane can enact" property asserts on that `Result`. Its port-forwarding leg has never been able to fail. `PortFwTable::dry_run` answers the question the writer needs to ask, and answers it where `add_entry` lives. A scratch table is equivalent to the real update because `update` removes every entry the incoming ruleset does not contain before adding, so whatever survives is a subset and re-adding a subset takes the "identical except for the timers" path. What is left to catch is a ruleset that disagrees with itself. Running the property suite against the live check found nothing, which is the answer worth having: the validator was not letting overlapping rulesets through, and now that is asserted rather than assumed. Two tests, because one is not enough and the reason is the same one that let this sit: `a_self_overlapping_ruleset_is_refused_up_front` covers `dry_run` and passes whether or not anything calls it, so `a_ruleset_the_table_cannot_hold_is_refused` goes through `PortFwTableWriter::update_table` instead. Only the second fails when `validate_ruleset` is put back the way it was. The absorb path keeps its log line, now naming the rule and the error it was given -- it was binding the error and never printing it -- against the case where the two checks ever disagree. Signed-off-by: Daniel Noland <daniel@githedgehog.com>

Signed-off-by: Daniel Noland <daniel@githedgehog.com>

daniel-noland force-pushed the pr/daniel-noland/clock-facade branch from 1576fc2 to 6498991 Compare August 26, 2026 17:30

daniel-noland force-pushed the pr/daniel-noland/spec-compliance branch from 762b44a to 8e60371 Compare August 26, 2026 17:30

daniel-noland force-pushed the pr/daniel-noland/spec-compliance branch from 8e60371 to e7929b8 Compare August 26, 2026 19:36

daniel-noland force-pushed the pr/daniel-noland/clock-facade branch from 6498991 to bd73f69 Compare August 26, 2026 19:36

daniel-noland force-pushed the pr/daniel-noland/spec-compliance branch from e7929b8 to ff2d1fb Compare August 26, 2026 20:41

daniel-noland force-pushed the pr/daniel-noland/clock-facade branch from 9889d61 to 409177c Compare August 26, 2026 21:02

daniel-noland force-pushed the pr/daniel-noland/spec-compliance branch 3 times, most recently from c4f741f to f560007 Compare August 26, 2026 21:25

daniel-noland force-pushed the pr/daniel-noland/clock-facade branch from 1ecf256 to 6a77767 Compare August 27, 2026 01:29

daniel-noland force-pushed the pr/daniel-noland/spec-compliance branch from f560007 to fdcb5f6 Compare August 27, 2026 01:29

daniel-noland force-pushed the pr/daniel-noland/clock-facade branch from 6a77767 to 668c5fc Compare August 27, 2026 01:41

daniel-noland force-pushed the pr/daniel-noland/spec-compliance branch from fdcb5f6 to bfd0877 Compare August 27, 2026 01:41

daniel-noland force-pushed the pr/daniel-noland/clock-facade branch from 668c5fc to 99956bf Compare August 27, 2026 04:33

daniel-noland force-pushed the pr/daniel-noland/spec-compliance branch from bfd0877 to 2e7cfee Compare August 27, 2026 04:34

daniel-noland force-pushed the pr/daniel-noland/clock-facade branch from 99956bf to d28e0ca Compare August 27, 2026 05:10

daniel-noland force-pushed the pr/daniel-noland/spec-compliance branch from 2e7cfee to ba806ce Compare August 27, 2026 05:10

daniel-noland force-pushed the pr/daniel-noland/clock-facade branch from d28e0ca to d682c66 Compare August 27, 2026 17:59

daniel-noland force-pushed the pr/daniel-noland/spec-compliance branch from ba806ce to 4775b0c Compare August 27, 2026 17:59

daniel-noland force-pushed the pr/daniel-noland/clock-facade branch from d682c66 to 17c12ab Compare August 27, 2026 18:29

daniel-noland force-pushed the pr/daniel-noland/spec-compliance branch from 4775b0c to 21e468c Compare August 27, 2026 18:29

daniel-noland force-pushed the pr/daniel-noland/clock-facade branch from 17c12ab to c4ea0ec Compare August 27, 2026 19:33

daniel-noland force-pushed the pr/daniel-noland/spec-compliance branch from 21e468c to f54b960 Compare August 27, 2026 19:33

daniel-noland force-pushed the pr/daniel-noland/clock-facade branch from c4ea0ec to 1e2a913 Compare August 27, 2026 19:54

daniel-noland force-pushed the pr/daniel-noland/spec-compliance branch 2 times, most recently from f150885 to e406d24 Compare August 27, 2026 20:17

daniel-noland force-pushed the pr/daniel-noland/clock-facade branch from a3d48a8 to efb7d61 Compare August 27, 2026 21:28

daniel-noland force-pushed the pr/daniel-noland/spec-compliance branch from b9defbf to acacc4b Compare August 27, 2026 21:28

daniel-noland and others added 28 commits August 28, 2026 01:42

style(spec-compliance): Drop added commentary

43af0f0

Signed-off-by: Daniel Noland <daniel@githedgehog.com>

daniel-noland force-pushed the pr/daniel-noland/clock-facade branch from 78c5c02 to 313696e Compare August 28, 2026 07:43

daniel-noland force-pushed the pr/daniel-noland/spec-compliance branch from 68d5d8f to 43af0f0 Compare August 28, 2026 07:43

Navigation Menu

Uh oh!

spec - #1757

spec#1757
daniel-noland wants to merge 29 commits into
pr/daniel-noland/clock-facadefrom
pr/daniel-noland/spec-compliance

daniel-noland commented Aug 26, 2026 •

edited

Loading

Uh oh!

coderabbitai Bot commented Aug 26, 2026

Draft PR not reviewed

Uh oh!

codecov Bot commented Aug 26, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

daniel-noland commented Aug 26, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

coderabbitai Bot commented Aug 26, 2026

Draft PR not reviewed

Uh oh!

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

Uh oh!

Codecov Report

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

daniel-noland commented Aug 26, 2026 •

edited

Loading

codecov Bot commented Aug 26, 2026 •

edited

Loading