test: Drive static NAT, masquerade and ACL with configuration-relative packets by daniel-noland · Pull Request #1738 · githedgehog/dataplane

daniel-noland · 2026-08-17T22:49:45Z

Stacked on #1737. Base: pr/daniel-noland/fuzz-config-generators — review the Commits tab or compare against the base, since Files Changed will show everything below it until the parents merge.

The fuzzing so far has been small, focused and intrusive: reach into a structure, exercise it directly, assert something about that structure. This is the other kind — configure a network function, put generated packets through it, and assert properties that would hold of any NAT or any ACL rather than of this one.

Three network functions, in increasing order of difficulty: static NAT (a pure function of its configuration), masquerade (stateful), and ACL (where a strong oracle already existed but stopped short of the packet).

Packets have to be drawn relative to the configuration

Packet has a TypeGenerator, and pointing it at a generated NAT configuration is useless: every packet misses every table, the fuzzer explores the miss path, and the run is vacuous while looking enormous.

This is the same failure the design note rejects for configuration values, one level down, so it takes the same answer. The configuration is a parameter to resolution, not a predicate to filter against. A ProbeSpec is drawn with no reference to any configuration — it is a handful of indices — and resolve interprets it against the built Fabric. Resolution is total, so no draw is discarded and no rejection loop skews the distribution.

The arrival state is the stage's precondition — and it is not always one stamp

Each stage assumes its predecessors annotated the packet, and nothing in the type system says so. Arrival writes that down once per stage, which is what the design note asks for when it puts contracts on network functions rather than on the pipeline.

Masquerade sharpened the point. FlowLookup attaches a flow entry only to a packet whose dst_vpcd is absent; the flow filter that sets dst_vpcd runs after it; Masquerade then requires it to be present. So the annotation has to arrive between two stages. The first version of the harness stamped everything up front, the way the static NAT one does — nothing crashed, but no packet was ever given flow state, every packet took the allocation path, and flows appeared to be re-allocated on every packet. Two properties failed and were right to: the harness was describing a pipeline that does not exist.

Seventeen properties, none with an oracle

Nothing here predicts what an address translates to. Each property is a metamorphic relation or an invariant, so nothing is a second copy of RangeBuilder or of the allocator.

Static NAT (11 — one suite for address-only exposes, one for the port-range path): round trip, injectivity, frame, permission, attribution, marking.

Masquerade (6): reversibility, stability (a flow keeps its first translation), exclusivity, containment (the translation lands inside a declared range), permission, attribution.

ACL (4): the stage's verdict is the configuration's verdict, the five-tuple survives the round trip through a packet, a packet with no discriminants is refused, underlay traffic is left alone.

The three stages fail differently, and the properties say so. Static NAT's round trip crosses two independently built tables. Masquerade's crosses no table at all — the reverse translation exists only because the forward packet recorded it, so it is a claim about state. ACL's has a real oracle already and the new claim is about the packet path in front of it.

Everything is break tested

A property that cannot fail is not evidence.

break	fires
static NAT mapping shifted by one	round trip
every address mapped to its range start	round trip, injectivity
`set_checksum_refresh` dropped	marking
`src_natted` mark dropped	marking
silent pass on a missing source vni	attribution
static NAT permission gates ignored	permission
a port rewritten the mapping never named	frame
`PortAddrTranslationValue::get_entry` broken	only the two port properties
`AddrTranslationValue::get_entry` broken	only the four address properties
masquerade flow hot path disabled	stability, reversibility
`requires_masquerade` ignored	masquerade permission
allocation reported outside the declared range	containment, exclusivity
allocation failure passed silently	masquerade attribution
ACL `done(AclDropped)` dropped	stage verdict
ACL source address misread	stage verdict, summary round trip
ACL `is_overlay` gate removed	underlay gate

Two of those are worth reading twice.

The two static NAT suites are mutually exclusive. Breaking the PAT path fails only the port properties; breaking the address path fails only the address properties. That is the evidence the extra suite reaches code the first does not, rather than re-running the same paths under new names.

The ACL re-point closes a measurable gap. Misread one field — take the source address from where the destination lives — and all five pre-existing fuzz:: properties pass, because they never build the packet that is misread. Both new properties fail. That is the whole argument for the change, demonstrated rather than asserted.

Generator gaps found along the way

Repeating a single-expose generator to get several does not work, for two reasons that are both facts about what a manifest accepts and so belong in the generator: exposes laid out from the same bases overlap, and independent draws mix address families, which a peering refuses.

Measured on the static NAT properties:

	configurations that validated
repeating `StaticNatExpose`	33%
one block per expose	59%
one block and one shared family	100%

Two thirds of the budget was going into configurations that were thrown away — and worse than the waste, multi-expose configurations were nearly unreachable, so the case with more than one rule in a table was the one being skipped. MasqueradeExposes got the same treatment for the same reason. Both single-expose generators are unchanged, so existing callers in nat and mgmt are untouched.

Vacuity

Every property counts what it reached and asserts a floor, because the failure that matters is an assertion that stops running rather than one that is wrong. All seventeen build 100% of the configurations they draw. The ACL guard also counts denials, since a run that only ever saw permits would pass while the drop path — the only path where the stage does anything — went entirely unexercised.

Packet::enforce removes a dropped packet from the output iterator, so probes carry keep: without it a drop and a pass-through are the same event from outside, and attribution could not be stated at all.

The design note comes along

docs(testing): Record the config-algebra testing strategy was stranded on an abandoned branch and never reached this stack, and these commits cite it throughout, so it is carried here. A follow-up commit corrects its status line — the per-packet half of its decomposition now has three worked examples, while the operation algebra itself is still unbuilt and the enactment path refactor it implies is still deferred.

Verification

CI cannot be trusted during the outage, so this was verified locally: acl-filter 28, nat 186, config 183, mgmt 19, all passing, with cargo fmt --check and clippy -D warnings clean on every package touched. Worth re-running once GitHub recovers, since local runs do not exercise the phasing, the cross-qemu path, or miri.

Not in scope

Flow expiry. Every masquerade property completes inside one flow lifetime, so none depends on expiry either happening or not. Expiry needs the explicitly driven clock the design note asks for, not a wall clock a property happens to outrun.
ICMP and arbitrary next headers through the ACL stage. No builder produces a packet matching those summaries, so they stay with the summary-level properties. Same for the CrossVersion stray, which asks for a v4 source with a v6 destination.
Port forwarding, FIB, and the remaining stages.
The operation algebra itself — sequences, undo, commutation from read and write sets. Still a design note.

🤖 Generated with Claude Code

coderabbitai · 2026-08-17T22:49:56Z

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-17T22:56:00Z

Codecov Report

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

Files with missing lines	Patch %	Lines
nat/src/masquerade/fuzz.rs	88.70%	14 Missing and 13 partials ⚠️
nat/src/static_nat/fuzz.rs	90.98%	13 Missing and 10 partials ⚠️
config/src/external/overlay/vpcpeering.rs	93.54%	6 Missing ⚠️
nat/src/static_nat/probe.rs	98.14%	3 Missing and 1 partial ⚠️
acl-filter/src/nf_fuzz.rs	98.64%	1 Missing and 1 partial ⚠️
nat/src/masquerade/probe.rs	99.25%	0 Missing and 1 partial ⚠️

📢 Thoughts on this report? Let us know!

A design note for testing the config-driven dataplane, plus links to it from the code guidelines and the property-testing guide. Nothing in it is implemented. Its value is mostly in the approaches it rejects, because each of those looked obviously right at the start of a conversation and turned out to be a dead end for a reason worth keeping: * Generating configuration values directly. A `TypeGenerator` over the config types yields syntactically valid, semantically impossible configurations -- colliding VNIs, peerings between VPCs that do not exist -- so the validator refuses nearly all of them and a coverage-guided fuzzer spends its budget exploring rejection paths. Filtering does not help, because the generator would then have to encode the validator's rules, leaving two copies to keep in agreement. Build configurations from an algebra of valid operations instead, and preconditions become unrepresentable rather than checked. * A shadow model as the oracle. It grows into a second dataplane, drifts from the first, and has to be rewritten whenever the real one is refactored. Operations emit claims about observable behaviour instead. * Reimplementing rule selection, or discovering precedence by ablation. Both are unnecessary: `acl/src/reference/` already answers "which rule should have won, and which did it shadow" in one pass, and the vocabulary in `match-action` is general enough to serve every function that consults a table. That reference scales with the match vocabulary rather than with the feature set, which is what keeps it from rotting. * Following the algebraic notation toward rigour. There is no inverse for "transmit a session", and the nearest thing to one advances the clock until transients decay. Chasing that ends in rebuilding a temporal logic. We want to find defects, not prove their absence, so the notation is a naming scheme for test shapes and nothing more. * Putting the oracles at the boundary of the whole pipeline. An ACL that drops traffic before the router sees it hides the router completely, and the expectation becomes a cross-product over domains. Contracts belong to individual network functions; pipeline behaviour is their composition. The recurring theme is that an oracle derived from the same source as the implementation cannot see that source being wrong, and that the way out is always to find something genuinely independent -- a parser, a transport protocol, a second walk over the same data. Two constraints are recorded as requirements on work that has not started yet, because both are cheap to honour in advance and expensive to retrofit: the generation-propagation logic of the planned network-function DAG has to be a pure state machine over a small hashable state, and a match-action rule has to name its action completely enough to serve as the specification for it. The note is a record under revision rather than settled doctrine; its open questions are live, and several of them are questions about this repository that nobody has answered yet. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com> (cherry picked from commit 74d4304)

`StaticNatExpose` draws one expose, and one expose builds a table with one rule in it. A property about a *lookup* wants several, because one rule gives a longest-prefix match nothing to choose between. Repeating the single-expose generator does not work. Two independent draws are refused by a manifest almost every time, for two separate reasons: * **Overlap.** Every expose is laid out from the same two bases -- 10.0.0.0 for the private side and 172.16.0.0 for the public one -- so two of them cover the same addresses and validation refuses the pair. * **Address family.** A peering's manifests must agree on one family, so a v4 expose beside a v6 one is refused as well. Both belong in the generator rather than in each caller, since both are facts about what a manifest accepts. `StaticNatExposes` draws the family once and places each expose in a block of its own, `BLOCK_STRIDE` apart -- wider than the widest span one expose can occupy, so distinct blocks cannot collide whatever the draw. ## It was two thirds of the budget Measured on the static NAT network function properties that motivated this, which draw between one and three exposes: * repeating `StaticNatExpose`: 33% of configurations validated, * one block per expose: 59%, * one block and one family: 100%. So two thirds of the fuzzing budget was being spent building configurations that were thrown away, and -- worse than the waste -- multi-expose configurations were nearly unreachable. The interesting case was the one being skipped, which is the same generator gap this campaign has now found several times: code that is unreachable rather than wrong. `StaticNatExpose` is unchanged and still draws a single expose, so the existing callers in `nat` and `mgmt` are untouched. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com> (cherry picked from commit 7f98556)

The fuzzing so far has been small, focused and intrusive: it reaches into a structure, exercises it directly, and asserts something about that structure. This is the first of the other kind -- configure a network function, put generated packets through it, and assert properties that would hold of any static NAT rather than of this one. ## Packets have to be drawn relative to the configuration `Packet` has a `TypeGenerator`, and pointing it at a generated NAT configuration is useless: every packet misses every table, the fuzzer explores the miss path, and the run is vacuous while looking enormous. This is the same failure the design note rejects for configuration values, one level down, so it takes the same answer. The configuration is a **parameter to resolution**, not a predicate to filter against. A `ProbeSpec` is drawn with no reference to any configuration -- it is a handful of indices -- and `resolve` interprets it against the built `Fabric`. Resolution is total, so no draw is discarded and no rejection loop skews the distribution. `acl-filter`'s `ProbeSpec` resolves against a built overlay the same way; this generalises the shape to a stage that takes real packets. ## The arrival state is the stage's precondition `StaticNat` sits mid-pipeline and assumes its predecessors annotated the packet: two vpc discriminants, the overlay flag, and the flags saying which directions of translation are wanted. Nothing says so in the type system -- `process` passes silently over a packet that lacks them. `Arrival` writes that down once, which is what the design note asks for when it puts contracts on network functions rather than on the pipeline: the assumption travels with the stage. `masquerade`'s tests hand-roll the same thing as a mock stage, and that is the drift this avoids. ## What is actually new `setup::config_driven` already proves the *mapping* right by enumeration. Nothing there touches a packet, its metadata, or `StaticNat`. These cover the half where the decisions live, and none of them needs an oracle -- each is a metamorphic relation or an invariant, so nothing here is a second copy of `RangeBuilder`: * **round trip** -- a translated source comes back. The outbound packet is rewritten by the local vpc's table, built from the local side of the peering; the reply is rewritten by the peer's table, built from the remote side, by a different code path. Whatever the first did, the second must undo. This is the one property that ties the two halves together. * **injectivity** -- distinct sources stay distinct, through the stage rather than through the table. A collision is a tenant isolation defect. * **frame** -- translating the source touches nothing else. The generated exposes carry no port ranges, so a rewritten port would be a mapping reaching further than it was configured to. * **permission** -- nothing is translated that did not ask. Covers every reason: not requested, already done, annotations missing or naming something absent, source not exposed. * **attribution** -- a packet that cannot be looked up is dropped with a `DoneReason`, not passed silently. A silent pass forwards untranslated traffic under a configuration that never mentioned it. * **marking** -- a packet whose address changed carries `src_natted` and `checksum_refresh`. Without the second it goes out with a checksum for an address it no longer has, and is discarded by the receiver rather than by anything that could report it. ## Every one of them was verified by breaking the code A property that cannot fail is not evidence. Each break fired exactly the property it should and left the others green: | break | fires | | --- | --- | | mapping shifted by one | round trip | | every address mapped to its range start | round trip, injectivity | | `set_checksum_refresh` dropped | marking | | `src_natted` mark dropped | marking | | silent pass on a missing source vni | attribution | | both permission gates ignored | permission | | a port rewritten the mapping never named | frame | ## Vacuity Every property counts what it reached and asserts a floor, because the failure that matters is an assertion that stops running rather than one that is wrong. All six now build 100% of the configurations they draw, and reach between 2,100 and 21,700 probes per second-long run. `Packet::enforce` removes a dropped packet from the output, so probes carry `keep`: without it a drop and a pass-through are the same event from outside, and attribution could not be stated at all. ## Why the vacuity floor is a ratio Each property counts the draws that reached its assertion and fails the run if too few did. That floor is relative -- at least one reaching draw per two configurations built, plus a small absolute minimum -- rather than an absolute count, because an absolute count measures how fast the machine was rather than whether the property ran. A property that reaches a couple of thousand draws on its own reaches a few dozen under coverage instrumentation beside nine hundred other tests, and a floor tuned to the fast case then fails for a reason that has nothing to do with the code under test. Both counts scale with the iteration budget, so their ratio does not, and a property that has genuinely stopped reaching its assertion still collapses the ratio to zero -- which is the only thing the guard was ever for. This shape was arrived at the hard way: the first `just coverage` run over `nat`, `net`, `flow-entry`, `acl-filter`, `config` and `mgmt` failed on a count-based floor rather than on a defect. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com> (cherry picked from commit 7d670e3)

The note was written before any of it existed and said so. The per-packet half of its decomposition now has a worked example -- packets drawn relative to a generated configuration, put through a real network function, judged by metamorphic relations -- so the blanket claim is no longer true and would mislead the next reader into rebuilding it. The operation algebra itself is still unbuilt, and the enactment path refactor it implies is still deferred, so the status line says which half is which rather than simply flipping. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com> (cherry picked from commit aecbf11)

…sses Static NAT permits a port range on a prefix, and a prefix that carries one takes the mapping down a second path entirely: `NatTableValue::Pat` and `PortAddrTranslationValue` rather than `NatTableValue::Nat` and `AddrTranslationValue`. The expose generator produced no port ranges, so that path had no configuration-driven coverage at all. ## The rule makes it the harder path Validation asks that the two sides cover the same **total**, counting addresses times ports. So a `/32` carrying 64 ports is a legal answer to a `/30` carrying 16, and the mapping has to run across both dimensions at once. That asymmetry is the reason the path exists, so `StaticNatExposes::with_ports` draws it on purpose: one total per expose, divided into addresses and ports independently per side, with both port ranges starting at a drawn offset so a mapping that quietly assumes they begin at the same port fails here. Worth noting what is legal for static NAT and not for port forwarding, which requires the two prefix lengths and the two port counts to match individually. The two flavours do not share this rule and must not share a generator. ## What changed in the harness An address on its own is no longer a thing the configuration maps -- the address-and-port pair is. So `Endpoint` replaces the bare address, carrying the range its prefix declares, and a probe draws its port from that range rather than freely, or it would miss. Three consequences: * the reply in the round trip must be addressed to the **translated** port, since that is the port the peer was contacted from; * injectivity sweeps every pair rather than every address -- an address-only sweep checks a diagonal of the space and calls it injective; and * the frame differs between the paths. With no port range the transport ports are part of the frame and must survive untouched; with one they are part of what is being translated, and only the destination and protocol remain. One property per flavour rather than one over a mix, following the same reasoning as the NAT flavour properties in `mgmt`: a mixed property reaches each path eventually, one that asks for a path reaches it every time and says in its name which one failed. ## The two suites provably exercise different code Break `PortAddrTranslationValue::get_entry` and the two port properties fail while all four address properties pass. Break `AddrTranslationValue::get_entry` and exactly the reverse happens. That mutual isolation is the evidence that the extra properties are earning their place rather than re-running the same paths under new names. All eleven properties build 100% of the configurations they draw. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com> (cherry picked from commit d3ac668)

The second network function, and the first stateful one. Static NAT's answer for a packet is fixed by its tables; masquerade's is whatever the allocator handed out the first time it saw the flow, kept in the flow table and reused after. Every property here is really about that state being kept consistently, which is a different subject from anything the allocator's own tests can reach. ## A probe is a flow, not a packet The first packet of a flow allocates and writes a flow entry; the second finds that entry and reuses it. Different code, and the interesting properties relate the two. So `Probe::packet` hands back a fresh packet on every call rather than being consumed once, because sending the same flow twice is how the hot path is reached at all. ## The stage order is load-bearing, and getting it wrong made the harness lie `FlowLookup` attaches a flow entry only to a packet whose `dst_vpcd` is **absent**, and the flow filter that sets `dst_vpcd` runs *after* it. `Masquerade` then requires `dst_vpcd` to be present. So the annotation has to arrive between the two stages -- not before both, not after. The first version of this harness stamped both annotations up front, the way the static NAT one does. Nothing crashed. What happened instead is that no packet was ever given flow state, every packet took the allocation path, and a flow appeared to be re-allocated on each packet. Two properties failed and were right to: the harness was describing a pipeline that does not exist. That is the sharper form of the arrival-state point from the static NAT work. A network function's precondition is not always a stamp a test can apply in one go -- here part of it is supplied by a stage that must run *after* another stage that requires its absence, and no test that ignores the ordering describes the real thing. ## The three prerequisites, handled rather than assumed The design note lists what has to be true before a stateful stage can be compared at all: * **Seeded non-determinism** -- `set_randomize(false)`, or two fabrics built from one configuration disagree on every flow. * **Timers** -- rather than fake a clock, every property completes inside one flow lifetime, so none depends on expiry either happening or not. Expiry is a separate subject and wants the explicitly driven clock the note asks for, not a wall clock a property happens to outrun. * **Projections, not state** -- nothing here inspects the allocator or the flow table. Every assertion is over what came out of the pipeline. The properties also need a tokio runtime, since `FlowTable::insert` spawns a per-flow expiry timer. The existing tests get one from `#[tokio::test]`; a bolero body is synchronous, so it enters a runtime instead. ## The properties None predicts which address and port a flow will be given -- that is the allocator's business and predicting it would be a second copy of it. * **reversibility** -- the reply comes back to where the flow started. Unlike static NAT there is no second table built from the other side of the peering: the reverse translation exists only because the forward packet recorded it. A forward translation not faithfully recorded is a connection that never gets an answer. * **stability** -- a flow keeps the translation it was first given. A stage that re-allocated would produce a legal-looking packet every time, and the connection would break in a way no allocator-level test could see, because the two allocations are individually correct. * **exclusivity** -- two live flows never share a translation. Distinct source ports as well as addresses, since masquerade collapses many private addresses onto few public ones and the port is what keeps them apart after. * **containment** -- every translation lands inside a range the configuration named. The one property that consults the configuration, and legitimately: a membership test, not a prediction of which member. An address from outside the declared set is unroutable, so the flow is a blackhole that looks like success from inside the box. * **permission** and **attribution** -- as for static NAT. Permission matters more here, because a translation is not merely applied but *recorded*: a packet masqueraded without permission leaves an entry behind that keeps translating its successors. ## Break tested | break | fires | | --- | --- | | flow hot path disabled | stability, reversibility | | `requires_masquerade` ignored | permission | | allocation reported outside the declared range | containment, exclusivity | | allocation failure passed silently | attribution | Reversibility surviving the third of those is the correct answer rather than a gap: it asserts the reverse undoes the forward, which stays true when both use the same wrong address. ## Generator `MasqueradeExposes` gets the same treatment `StaticNatExposes` did, for the same two reasons -- `MasqueradeExpose` draws its base index freely, so two exposes collide whenever their index ranges intersect, and independent draws mix address families. One slot of four indices per expose, family drawn once. All six properties build 100% of the configurations they draw. The vacuity guard is a ratio rather than an absolute count, for the reason recorded with the static NAT properties: a count measures how fast the machine was, and fails under coverage instrumentation for reasons that have nothing to do with the code under test. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com> (cherry picked from commit 2491063)

…nction `acl-filter/src/fuzz.rs` has the strongest oracle in this codebase: it evaluates the validated configuration directly and compares that against the lowered tables, so a lowering mistake cannot hide behind the thing it produced. What it never touches is a packet. Every probe there is a `PacketSummary` handed straight to `lookup`. Two pieces of production code sit between a packet and that summary, and neither had any coverage from a generated configuration: * **`PacketSummary::try_from`**, which reads the five-tuple and both discriminants out of the headers; and * **`AclFilter::process_packet`**, which turns a verdict into a fate -- `DoneReason::AclDropped`, `invalidate_flows`, and the `is_overlay` gate deciding whether any of it happens. This re-points the existing generators rather than writing new ones. The `OverlaySpec` and `ProbeSpec` are unchanged; a probe now becomes a packet and the answer is read off the packet's fate. The oracle is the same `oracle_resolved_action`, asked the same question, so this is a differential test over the packet path rather than a second ACL. ## The gap was real, and the break test shows exactly how big Misread one field -- take the source address from where the destination lives: ```rust let src_ip = net.dst_addr(); let dst_ip = net.dst_addr(); ``` **All five pre-existing `fuzz::` properties pass.** They never build the packet that is misread, so there is nothing for them to see. Both new properties fail. That is the whole argument for this change, demonstrated rather than asserted. ## The properties * **stage verdict** -- a packet the configuration denies is dropped with `AclDropped`; one it allows survives untouched. This tests the extraction implicitly: a field read from the wrong place makes the stage judge a different tuple from the one the oracle judged, and they disagree wherever that field decides the answer. * **summary round trip** -- the five-tuple read back is the one the packet was built with. Direct rather than implicit, so it also catches the misread that happens to be harmless for the ruleset drawn. * **missing discriminant** -- a packet naming no destination vpc is refused as `Unroutable`. An ACL is indexed by the vpc pair, so such a packet cannot be judged at all, and letting it through applies no policy whatsoever. * **underlay gate** -- traffic that is not overlay traffic is left alone. No ACL in the configuration describes it. Break tested: dropping the `done(AclDropped)` fires the stage verdict; the misread above fires both it and the round trip; removing the `is_overlay` gate fires the underlay property. Each leaves the others green. ## Scope Only TCP and UDP become packets. A probe drawing ICMP or an arbitrary next header is counted and skipped rather than approximated, because a packet whose headers did not match the summary it came from would make every disagreement meaningless. The same goes for the generator's `CrossVersion` stray, which asks for a v4 source with a v6 destination -- there is no such packet, and that case stays with the summary-level properties where it belongs. The vacuity guard here counts denials as well as arrivals: a run that only ever saw permits would pass while the drop path -- the only path where the stage does anything -- went entirely unexercised. Around a quarter of probes are denied in practice. The vacuity guard is a ratio rather than an absolute count, for the reason recorded with the static NAT properties: a count measures how fast the machine was, and fails under coverage instrumentation for reasons that have nothing to do with the code under test. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com> (cherry picked from commit e73a570)

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

Recreated with a corrected base after the stack was reordered into chapters. GitHub will not re-base a PR that is part of a stack, and these were never out of draft.

daniel-noland added the dont-merge Do not merge this Pull Request label Aug 17, 2026

daniel-noland changed the title ~~test(nat): Drive static NAT with configuration-relative packets~~ test: Drive static NAT, masquerade and ACL with configuration-relative packets Aug 17, 2026

daniel-noland force-pushed the pr/daniel-noland/fuzz-config-generators branch from 81dcce4 to 4a845a9 Compare August 18, 2026 03:07

daniel-noland force-pushed the pr/daniel-noland/fuzz-nf-probes branch 3 times, most recently from ec5c23a to 35eb35f Compare August 18, 2026 19:41

daniel-noland force-pushed the pr/daniel-noland/fuzz-config-generators branch from 4a845a9 to 3ff0a99 Compare August 18, 2026 20:23

daniel-noland force-pushed the pr/daniel-noland/fuzz-nf-probes branch from 35eb35f to fb86e74 Compare August 18, 2026 20:23

daniel-noland force-pushed the pr/daniel-noland/fuzz-config-generators branch from 3ff0a99 to c9c3d7c Compare August 18, 2026 20:31

daniel-noland force-pushed the pr/daniel-noland/fuzz-nf-probes branch from fb86e74 to 348b360 Compare August 18, 2026 20:31

daniel-noland force-pushed the pr/daniel-noland/fuzz-config-generators branch from c9c3d7c to cde279e Compare August 18, 2026 20:38

daniel-noland force-pushed the pr/daniel-noland/fuzz-nf-probes branch from 348b360 to c592c41 Compare August 18, 2026 20:38

daniel-noland force-pushed the pr/daniel-noland/fuzz-config-generators branch from cde279e to 9b658dc Compare August 18, 2026 23:17

daniel-noland force-pushed the pr/daniel-noland/fuzz-nf-probes branch 2 times, most recently from 5fa5ecf to 6f240db Compare August 19, 2026 00:58

daniel-noland force-pushed the pr/daniel-noland/fuzz-config-generators branch from 9b658dc to 3ce58bb Compare August 19, 2026 06:33

daniel-noland force-pushed the pr/daniel-noland/fuzz-nf-probes branch from be68f0a to 5dc1767 Compare August 19, 2026 06:33

daniel-noland force-pushed the pr/daniel-noland/fuzz-config-generators branch from 3ce58bb to 74bce9a Compare August 20, 2026 01:58

daniel-noland force-pushed the pr/daniel-noland/fuzz-nf-probes branch from 5dc1767 to b9930af Compare August 20, 2026 01:58

daniel-noland mentioned this pull request Aug 20, 2026

(scratch) test: track RFC 4787, and state its requirements as executable contracts #1741

Closed

daniel-noland force-pushed the pr/daniel-noland/fuzz-config-generators branch from 74bce9a to ef991bd Compare August 20, 2026 02:32

daniel-noland force-pushed the pr/daniel-noland/fuzz-nf-probes branch from b9930af to 75db938 Compare August 20, 2026 02:32

mvachhar force-pushed the pr/daniel-noland/fuzz-config-generators branch from ef991bd to 1f73a35 Compare August 21, 2026 15:13

daniel-noland and others added 5 commits August 25, 2026 20:50

daniel-noland and others added 2 commits August 25, 2026 20:50

daniel-noland force-pushed the pr/daniel-noland/fuzz-config-generators branch from 1f73a35 to 641ac94 Compare August 26, 2026 02:55

daniel-noland force-pushed the pr/daniel-noland/fuzz-nf-probes branch from 75db938 to 1017959 Compare August 26, 2026 02:55

daniel-noland closed this Aug 26, 2026

Navigation Menu

Uh oh!

test: Drive static NAT, masquerade and ACL with configuration-relative packets - #1738

test: Drive static NAT, masquerade and ACL with configuration-relative packets#1738
daniel-noland wants to merge 7 commits into
pr/daniel-noland/fuzz-config-generatorsfrom
pr/daniel-noland/fuzz-nf-probes

daniel-noland commented Aug 17, 2026 •

edited

Loading

Uh oh!

coderabbitai Bot commented Aug 17, 2026 •

edited

Loading

Draft PR not reviewed

Uh oh!

codecov Bot commented Aug 17, 2026 •

edited

Loading

Uh oh!

daniel-noland commented Aug 26, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

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

Uh oh!

Packets have to be drawn relative to the configuration

The arrival state is the stage's precondition — and it is not always one stamp

Seventeen properties, none with an oracle

Everything is break tested

Generator gaps found along the way

Vacuity

The design note comes along

Verification

Not in scope

Uh oh!

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

Uh oh!

Draft PR not reviewed

Uh oh!

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

Uh oh!

Codecov Report

Uh oh!

daniel-noland commented Aug 26, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

daniel-noland commented Aug 17, 2026 •

edited

Loading

coderabbitai Bot commented Aug 17, 2026 •

edited

Loading

codecov Bot commented Aug 17, 2026 •

edited

Loading