(scratch) test: track RFC 4787, and state its requirements as executable contracts - #1741
Draft
daniel-noland wants to merge 9 commits into
Draft
(scratch) test: track RFC 4787, and state its requirements as executable contracts#1741daniel-noland wants to merge 9 commits into
daniel-noland wants to merge 9 commits into
Conversation
|
Important Review skippedDraft detected. Please check the settings in the CodeRabbit UI or the ⚙️ Run configurationConfiguration used: Organization UI Review profile: CHILL Plan: Pro Run ID: You can disable this status message by setting the Use the checkbox below for a quick retry:
Comment |
❌ 2 Tests Failed:
View the top 2 failed test(s) by shortest run time
To view more test analytics, go to the Test Analytics Dashboard |
…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.
…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.
… 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.
…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.
… 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".
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>
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>
`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>
…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>
daniel-noland
force-pushed
the
pr/daniel-noland/spec-compliance
branch
from
August 20, 2026 02:32
cd0205c to
604bbfe
Compare
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