(05) route - #1753
Conversation
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: Organization UI Review profile: CHILL Plan: Essentials Run ID: 📒 Files selected for processing (1)
💤 Files with no reviewable changes (1)
Included review availability: 3 reviews are currently available. Your included PR review attempts over the past 7 days set your current allowance at 5 reviews per hour. 📝 WalkthroughWalkthroughThe pull request adds a shared clock abstraction, RFC requirement tracking, configurable Bolero generators, NAT validation, ICMP parsing fixes, routing API updates, and broad property-based test coverage. ChangesDataplane validation and test infrastructure
🚥 Pre-merge checks | ✅ 2 | ❌ 3❌ Failed checks (1 warning, 2 inconclusive)
✅ Passed checks (2 passed)
Comment |
20dc819 to
c54556c
Compare
Codecov Report❌ Patch coverage is 📢 Thoughts on this report? Let us know! |
c54556c to
e4d6dfb
Compare
e4d6dfb to
ddd5684
Compare
ddd5684 to
597e7a7
Compare
597e7a7 to
7fba952
Compare
7fba952 to
a1ca24d
Compare
a1ca24d to
6a68c58
Compare
4275bcc to
364a49e
Compare
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>
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>
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>
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>
`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>
Use changelog to model check fib. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>
A fib may be indexed by both id and vni. Make sure to delete every entry referring to the target fib so no alias outlives its writer. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>
- base receive framing on used (rather than the resized) buffer length. - Wait for complete headers, - handle partial bodies, - reject announced bodies over 16 MiB, Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>
An empty-next-hop route in the rib was rejected by the fib. This allowed traffic to fall through to a less-specific route. We now substitute an explicit drop so every caller preserves consistency. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>
- generate VRF status transitions - distinguish preset root-drop routes from ordinary drop routes. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Interface names come from the kernel. Letting these names say in the key can give the same next-hop different keys. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>
1a4ecd7 to
3396846
Compare
No description provided.