Skip to content

test(config,mgmt,k8s-intf): generate valid configurations and property-test the validator - #1737

Draft
daniel-noland wants to merge 20 commits into
pr/daniel-noland/fuzz-flow-entryfrom
pr/daniel-noland/fuzz-config-generators
Draft

test(config,mgmt,k8s-intf): generate valid configurations and property-test the validator#1737
daniel-noland wants to merge 20 commits into
pr/daniel-noland/fuzz-flow-entryfrom
pr/daniel-noland/fuzz-config-generators

Conversation

@daniel-noland

Copy link
Copy Markdown
Collaborator

Last of five, stacked on #1736. Twenty commits spanning config, k8s-intf and
mgmt.

These three cannot be split by package — most commits touch two or three of them,
so any split leaves broken intermediate states. They are one body of work:
generating configurations that are valid by construction rather than
generated and filtered, then property-testing the validator and the dataplane
tables a validated configuration implies.

The generators build configurations from an algebra of valid operations, which is
what makes them useful: a TypeGenerator over the config types produces
syntactically valid, semantically impossible configurations that the validator
refuses, so a coverage-guided fuzzer spends its budget on rejection paths. See
development/code/config-algebra-testing.md for the reasoning.

Three fixes, each found by the properties:

  • Refuse a port-forwarding expose the dataplane cannot build, so the
    validator stops blessing configurations that fail at enactment. This is the
    constraint the whole campaign is aimed at — everything the validator accepts
    has to be enactable, because there is no channel back to the operator.
  • Give every vpc its own slots, and assert the control validates.
  • Put the generated gateway in its own gateway groups.

Plus a typed error for port-forwarding mismatches instead of a string.

Two notes for review:

  • The three feat(config): Generate … exposes commits also touched nat/. The
    nat half is superseded — main has since gained reserved.rs and the
    static-claims rework, so ReserveSets moved out of setup.rs and a test
    module targeting the old shape was dropped. One nat change was kept:
    overlay_offering moves out of nat/src/portfw/portfwtable/setup.rs into the
    config generator module, which is that commit's intent rather than collateral.
  • The final commit follows genid out of MasqueradeConfig::new into
    update_nat_allocator, where main moved it. Three commits introduced the
    affected call sites, so it is one commit rather than three amendments — which
    means those three, and the five between them, cannot compile dataplane-mgmt's
    tests on their own. --autosquash fixes that if bisectable history inside the
    branch is worth more than the smaller diff.

Verified locally rather than in CI, given the outage: config + mgmt +
k8s-intf 209/209, fmt --check and clippy -D warnings clean.

With this merged, pr/daniel-noland/icmp-flow-lock can be retired — everything
on it is either here, already landed in reworked form, or deliberately dropped.

🤖 Generated with Claude Code

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

coderabbitai Bot commented Aug 17, 2026

Copy link
Copy Markdown

Important

Review skipped

Draft detected.

Please check the settings in the CodeRabbit UI or the .coderabbit.yaml file in this repository. To trigger a single review, invoke the @coderabbitai review command.

⚙️ Run configuration

Configuration used: Organization UI

Review profile: CHILL

Plan: Pro

Run ID: 374f7e3c-c05b-49a7-ab3c-101add1323cd

You can disable this status message by setting the reviews.review_status to false in the CodeRabbit configuration file.

Use the checkbox below for a quick retry:

  • 🔍 Trigger review

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

@daniel-noland
daniel-noland force-pushed the pr/daniel-noland/fuzz-config-generators branch from 81dcce4 to 4a845a9 Compare August 18, 2026 03:07
@daniel-noland
daniel-noland force-pushed the pr/daniel-noland/fuzz-config-generators branch from 4a845a9 to 3ff0a99 Compare August 18, 2026 20:23
@daniel-noland
daniel-noland force-pushed the pr/daniel-noland/fuzz-config-generators branch from 3ff0a99 to c9c3d7c Compare August 18, 2026 20:31
@daniel-noland
daniel-noland force-pushed the pr/daniel-noland/fuzz-config-generators branch from c9c3d7c to cde279e Compare August 18, 2026 20:38
@daniel-noland
daniel-noland force-pushed the pr/daniel-noland/fuzz-config-generators branch from cde279e to 9b658dc Compare August 18, 2026 23:17
daniel-noland and others added 16 commits August 19, 2026 00:33
The configuration types had no generators, so every test of the path
from a configuration to a NAT table was driven by a handful of
hand-written overlays. That is the largest untested surface in the NAT
crate: the code that turns exposes into static, masquerade and
port-forwarding tables is reached only by the shapes somebody thought to
write down.

This is the first generator, for the port-forwarding flavour, chosen
because it has the tightest validity rules and the smallest surface
downstream. `config` grows an optional bolero dependency and a feature
to go with it, following what `net` and `lpm` already do.

Valid by construction rather than generate-and-reject. A rejected
configuration still counts as a run, so a generator that produces them
quietly buys less coverage than its iteration count suggests -- hence
one prefix per side of one family, drawn from blocks that are not
special-use, with a bounded port range on each side and matching totals.
Two tests in `config` hold it to that, and they are how the overflow in
its own port arithmetic was found: `start + count - 1` adds before it
subtracts, and the sum reaches 65536 at the top of the range.

The generator is deliberately narrower than the legal space. Validation
checks that the two sides have equal size, where size counts addresses
times ports, so sides with different prefix lengths and compensating
port counts satisfy it -- while `PortFwEntry` checks prefix length and
port count separately and rejects them. Generating that case would find
the disagreement rather than test anything past it, so it is left out
and written down, in the generator's own documentation and in the notes.

The property in `nat` is that an expose becomes the rules it describes,
and mostly that the two sides do not get crossed: `as_range` is what
traffic arrives on, `ips` is where it goes, and a rule holding them the
other way round forwards to the wrong place while passing every check
the rule itself makes. Swapping them in `expose_to_portfw_rule` fails it
on the first case.

It also found a constraint that was not obvious from reading: both
manifests of a peering must be of one IP version, so a fixed IPv4 remote
side cannot stand opposite a generated IPv6 expose.

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

Second generator, and the scaffolding both of them now sit on.

Masquerade's rules are looser than port forwarding's: several prefixes
per side, and their sizes need not agree, which is the point of it --
many private addresses behind few public ones. The one thing it forbids
is a port range on either side. Prefixes within a side are carved so as
not to overlap, since a manifest rejects overlapping ones, and the two
sides come from separate blocks.

overlay_offering moves into the generator module from the port-forwarding
test that first needed it. Every property downstream of a configuration
needs an overlay to put the expose in, and the two constraints it has to
satisfy are not obvious from reading: a manifest with no exposes is
rejected, so the remote side has to expose something, and a peering's two
manifests must agree on address family, so what it exposes has to follow
whichever family the generated expose came from. Better discovered once.

The property in nat is that masquerade only ever hands out an address the
expose named. That runs through most of the allocator -- the pool table
finding a pool for the private source, the public space being cut into
regions, the expose being given regions of its own -- and a mistake
anywhere along it shows up as an address from somewhere else. Building
the pools from `ips` instead of `as_range` fails it on the first case,
with the private address handed back as its own translation.

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

The last of the three NAT flavours, and the one the generator was worth
building for.

Static NAT's rule is that the two sides hold the same number of
addresses while being free to be cut up differently: a /26 on one side
can be answered by four /28s on the other. Working out the mapping
across boundaries that do not line up is the whole job of RangeBuilder,
the most intricate code in the NAT crate, and until now it was reached
by one bolero test over hand-built inputs and a handful of examples.

So the generator picks one total and splits it independently per side.
Two things had to be got right for that to mean anything:

Parts are laid out with a gap of their own size after each, not end to
end. Placed end to end they are aligned siblings, and validation
normalizes those back into a single prefix -- so the differing shapes
the generator had just worked out were collapsed away before anything
saw them. The generator's own test asserts the shapes do differ, which
is how that surfaced; without it the suite would have looked healthy
while only ever testing one prefix per side.

Sizes stay under 64 addresses so the property can enumerate rather than
sample.

The property is that the mapping is a bijection: every private address
lands somewhere public, no two land in the same place, and between them
they cover the public side exactly. Inverting the two arguments to
generate_nat_values fails it on the first case.

Port ranges are left out. Static NAT permits them and they take the
mapping down a second path -- PortAddrTranslationValue rather than
AddrTranslationValue -- which carries its own unfinished work, and wants
a generator written for it rather than this one stretched.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Validation compared the two sides of a port-forwarding expose by total
size, where a total is addresses times ports. That is the right check
for static NAT, whose whole job is mapping between differently shaped
sides -- but a port-forwarding rule maps one prefix onto another address
for address and one port range onto another positionally, so it can only
express matched lengths and matched port counts. A product is equally
satisfied by a /32 carrying 100 ports opposite a /30 carrying 25, and
that pairing validated.

PortFwEntry::is_valid refused it, so the configuration never took
effect. The trouble is where it refused it. Port forwarding is the last
of the NAT stages in apply_gw_config, and the sequence is a linear chain
with no staging, so by the time it fails the kernel interfaces, the flow
filter, the ACL tables, the static NAT tables and the masquerade
allocator have all been committed. The apply then returns an error and
rolls back, and the rollback restores the configuration -- but not the
masquerade flows that rebuilding the allocator has already judged
against the rejected config and torn down. Established connections
break for a configuration that was never applied, and the box takes two
disruptive transitions instead of none.

So the check moves to where rejecting is free. The two lengths and the
two port counts are compared directly, which is strictly stronger than
the product they replace: with one prefix on each side, equal lengths
and equal counts imply equal totals, while the converse is what let this
through. PortFwEntry keeps its own checks, which still guard callers
that build a rule without going through a configuration.

This changes the error for one shape already rejected. A /24 opposite a
/25 reported MismatchedPrefixSizes(256, 128); it now reports that port
forwarding requires prefixes of the same length. The new message says
what to change, which the totals did not, and the existing test moves
with it.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Follow-up to refusing these at validation. The first cut reported both
new rejections as Forbidden(&'static str), which is the stringly-typed
option: it throws away the values that differ and leaves a caller with
nothing to match on but prose.

Two variants instead, each carrying what did not line up.
MismatchedPrefixLengths and MismatchedPortRangeSizes name the private
and the public side rather than taking two positional numbers of one
type, since which is which is the whole content of the error.

MismatchedPrefixSizes could not be reused for the length case, tempting
as that is. It compares addresses times ports, and the pairing this
rejects -- a /32 carrying 100 ports opposite a /30 carrying 25 -- has
that product equal on both sides. Reporting it as a size mismatch would
have printed two numbers that are the same and asked the operator to
reconcile them.

Its own message is reworded while here. It said "Mismatched prefixes
sizes for static NAT: {0:?} and {1:?}", which named neither what has to
hold nor which side is which. It now leads with what to change. The
numbers stay behind `Debug` because `PrefixWithPortsSize` is a 145-bit
bnum type with no `Display`, and Debug pads it into a run of digits that
reads as gibberish -- so they come last rather than in the middle of the
sentence. Giving that type a `Display` is worth doing in lpm.

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

A gateway configuration passes through four steps before the dataplane sees it:

    GatewayAgent (CRD) ─▶ ExternalConfig ─▶ validated ─▶ InternalConfig ─▶ FRR

The converters, the validator and the renderers are all reasonably covered. The
third arrow is not: `build_internal_config` was exercised by one hand-built
sample in `check_frr_config`, a test that renders the result and prints it. So
the step that turns a *validated* configuration into the one the dataplane
applies had never seen a generated input -- and that is the step where a
configuration that validates and cannot be built would live. There is precedent:
`fix(config): Refuse a port-forwarding expose the dataplane cannot build`.

It matters because `apply_gw_config` is a linear `?`-chain with no transaction.
By the time a late step fails, kernel interfaces, the flow filter, ACLs, static
NAT and the masquerade allocator have all been committed, and rolling the
configuration back does not restore the masquerade flows already torn down.

Three properties, on generated `LegalValue<GatewayAgent>`: whatever validates
builds and renders; the built configuration carries a vrf for exactly the vnis
the overlay's vpcs have; and the whole chain is deterministic, which matters
because `frr-reload.py` diffs the rendered text against what FRR is running.

## The measurement is the finding

Every property is of the form "if it validates, then ...", so a fourth test
measures how often that is, rather than assuming. About a sixth of generated
configurations validate, carrying three vpcs each -- and **none of them has a
peering**. Twenty-four thousand peerings generated per four thousand
configurations, and not one survived validation.

Peerings are where the exposes, the NAT and the ACLs live. So the whole of that
half of the model was being generated in quantity and discarded before anything
downstream could see it, while `k8s-intf`'s generators sat at 94% coverage and
every per-converter property passed -- because those test the converters, which
run before validation.

Three causes fixed here, all in the generators:

  - **peering pairs were drawn independently.** `spec.rs` drew up to sixteen
    peerings and `pick2` chose a fresh vpc pair for each with no memory, so a
    duplicated pair was near-certain and one duplicate fails the whole
    configuration. Pair selection moves to the caller, which draws distinct ones.
  - **each expose drew a mix of address families.** It split every count into a
    v4 part and a v6 part, and a `VpcExpose` must be single-family. Now the
    family is chosen once per expose, and named vpc subnets of the other family
    are left out too, since a named subnet contributes its own prefix.
  - **prefixes were drawn as short as `/0`.** A v4 `/0` covers loopback and a
    `/2` at 64 covers `127.0.0.0/8`, so a short prefix always overlaps a
    special-use range that an expose may not. Minimum masks are now `/8` and
    `/16`; longer prefixes can still land in a reserved range, they just are no
    longer guaranteed to.

Also `min` rather than `max` when choosing how many vpc subnets an expose names:
with `max` the count was always at least the number that exist and the loop
stopped when they ran out, so every expose named all of them and the count never
varied.

## What is still blocked, and why it is its own change

The remaining failures are all one root cause: the expose is built first and its
NAT mode chosen afterwards, so the shape and the mode do not agree. Static NAT
gets mismatched address-port counts, port forwarding gets the exclusion prefixes
it forbids, and masquerade gets an empty `as` list. Fixing it means choosing the
mode first and shaping the expose to fit -- which is what `config`'s own
`contract` module does for the same three modes.

That is the next change, and the vacuity test is written to be strengthened by
it: it currently asserts that a twentieth of configurations validate and should
come to require peerings.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
The third arrow of the configuration chain --

    GatewayAgent (CRD) ─▶ ExternalConfig ─▶ validated ─▶ InternalConfig ─▶ FRR

-- had never been given a peering. 9bdde96e9 drove the whole chain from a
generated CRD and measured the result: about a sixth of configurations validate,
and *none* of them has a peering, because the CRD generators produce exposes that
validation always refuses. Peerings are where the exposes, the NAT and the ACLs
live, so the half of the model that matters most reached the builder never.

Fixing the CRD generators is its own piece of work. This gets at the same
question from the other side and now rather than after it: `config`'s contract
generators already produce exposes that are valid *by construction* for each of
the three NAT flavours, so an overlay built around them and spliced into the
sample underlay reaches `build_internal_config` with a peering in it.

The claim is the one that matters: a configuration that validates can be built
and rendered. A configuration that validates and then fails to build is a
half-applied dataplane -- `apply_gw_config` is a linear `?`-chain with no
transaction, so by the time a late step fails the kernel interfaces, the flow
filter, the ACLs, static NAT and the masquerade allocator are all committed, and
rolling the configuration back does not restore the masquerade flows already torn
down. There is precedent for the class: 9b216f5bd, a port-forwarding expose that
validated and could not be built.

**No defect found.** 300,000 configurations, 220,935 of them built, 120,215
carrying more than one expose across mixed NAT flavours, and the arrow holds.
That is the structural-risk question answered for this slice, and answered "no".

Two supporting changes:

  - `contract::overlay_with` and `overlay_with_exposes` split out of
    `overlay_offering`, which validated the overlay and returned it validated. A
    caller assembling a whole `ExternalConfig` needs the unvalidated one, because
    validating the overlay alone skips every check that spans the underlay and
    the overlay together. The first of those turned out to matter immediately:
    `VpcPeering::with_default_group` names a gateway group `default`, and
    whole-config validation checks that a peering's group exists -- a check
    overlay-only validation cannot make, since the group table sits beside the
    overlay rather than in it. So an overlay from these generators is not
    embeddable in a whole configuration without adding that group.
  - the contract module was gated `any(test, feature = "bolero")` but only ever
    compiled under `test`: it used `Prefix: From<&str>`, which the feature alone
    does not provide. Now it builds either way, which is what lets `mgmt` depend
    on it.

Verified by breaking four things: not building the overlay, not adding the
underlay vrf, not configuring the underlay's bgp peers, and not carrying the
community table across. The first three each needed an assertion the property did
not originally have -- the vni checks alone missed all of them -- and the fourth
was added for the same reason. Each fails now.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
The CRD generators produced peerings in quantity and none of them ever survived
validation. 9bdde96e9 measured it -- twenty-four thousand peerings per four
thousand configurations, zero validated -- and fixed three causes. This finds
and fixes the rest, and turns the entry point into something a property can aim
with.

## Valid by construction, not generate-and-reject

The principle is already written down in this repo, in `config`'s own contract
module:

    Valid by construction rather than by generate-and-reject, so every case
    reaches the code under test.

The CRD expose generator did the opposite: it drew the prefixes first and chose a
NAT flavour afterwards. Since every flavour constrains the shape -- static NAT
needs both sides to cover the same number of address-port pairs, port forwarding
needs one prefix per side of equal length with matched port ranges and no
exclusions at all, masquerade needs a non-empty translation range -- essentially
nothing it produced could be accepted, and no amount of context passed down would
have helped. The order was wrong.

Four further causes, all cross-cutting rules that no per-expose generator can
satisfy:

  - **the two manifests of a peering must agree on address family.** Each drew
    its own.
  - **only one manifest of a peering may use a stateful flavour.** Masquerade
    opposite masquerade, masquerade opposite port forwarding, and port forwarding
    opposite port forwarding are all refused. Both sides drew freely. The peering
    generator now draws which side may be stateful and restricts the other to the
    stateless flavours.
  - **a peering names a gateway group, and validation checks it exists.** The name
    was `d.produce::<String>()`, so it never did. Groups are now generated before
    peerings, and a peering picks one of them.
  - **a vpc's subnets are subject to the same rules as an expose's prefixes,**
    because an expose can name a subnet and a named subnet contributes its prefix.
    They were drawn across the whole address space, so `127.0.0.0/8` and
    `224.0.0.0/4` subnets made every expose naming them invalid. They now come
    from the private block, carved consecutively so they are distinct and
    non-overlapping without a rejection loop.

Prefixes throughout now come from blocks this validator does not treat as
special-use -- `10.0.0.0/8` and `172.16.0.0/12` for v4, halves of `2001:db8::/32`
for v6 -- with the private and public sides in different blocks so an expose's two
sides can never be the same prefix. The same choice, for the same reason, as the
contract module.

Result: **94% of generated configurations now validate, carrying 50,440 peerings
per 40,000 configurations.** It was 17% and zero.

## A generator a property can aim with

`LegalValue<GatewayAgentSpec>` implements `TypeGenerator`, which per
`development/code/property-testing.md` must "**never** produce an illegal value".
It did so on more than four draws in five, and the `LegalValue` name asserted a
property it did not have.

So the real generator is now `GatewayAgents`, a `ValueGenerator` produced by
`GatewayAgentBuilder`, with knobs for the NAT flavours, the address families and
the sizes. `LegalValue`'s `TypeGenerator` impls delegate to the defaults, so every
existing user keeps working, and a property that wants to aim at one flavour or
one family can now say so.

The defaults are much smaller: four vpcs, three peerings, two exposes each, three
prefixes a side. It was sixteen of everything nested four deep, which made a
single case thousands of prefixes -- costly to run and unreadable when it failed.

## Along the way

  - `start + size - 1` overflowed `u16` for a port range ending at 65535, since it
    groups as `(start + size) - 1`. The same slip, in the same shape, as one fixed
    earlier in the expose port generator; debug-mode overflow checks caught it.
  - `test_vpc_conversion`'s oracle had to learn that the conversion collects into
    a set-like structure, so a prefix written twice in one expose comes out once.
    Its expectation was only ever right because the previous generators drew from
    a uniqueness-preserving generator and never produced a repeat.
  - the vacuity test in `processor::confbuild::internal` now **requires** peerings,
    which is what it was written to be strengthened into.

## What this answers

With peerings now reaching the builder from the CRD side, the three chain
properties cover what they were meant to: 40,000 configurations, 37,627 built and
rendered, and no defect. Together with eab78aa5c, which came at the same arrow
from the `ExternalConfig` side, **a configuration that validates builds and
renders** now has generated evidence behind it from both directions.

Residue, at about one in a thousand: two exposes in one peering drawing
overlapping prefixes from the same block. Avoiding it needs coordination across
exposes, and it is legitimate rejection rather than a defect.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
The peering generators carried `acl: None // FIXME: Add a proper implementation
when used`, so no ACL ever reached the converter, the validator or anything past
them. `config/src/converters/k8s/config/acl.rs` is the largest converter in the
crate at 800 lines, with ten hand-written tests and no generated input.

ACLs are now generated, valid by construction, and flow through the whole chain:
roughly 25,000 of them per 40,000 configurations, on about two thirds of the ones
that validate.

## The ACL is built from the manifests, not beside them

That is the shape of the thing. A rule's `match` is checked against what the two
sides of the peering actually expose -- the **source** prefixes have to intersect
the *from* side's native addresses, the **destination** prefixes the *to* side's
advertised ones -- and `scope: flow` is checked against how they translate. So the
generator reads those facts back off the manifests the peering generator has just
built (`SideFacts::of`) and names prefixes that are really there. Drawing them
freely would produce rules that match nothing, which is refused outright.

The rules satisfied by construction:

  - `from` and `to` name the peering's two vpcs, in either order, and sometimes
    only one of them -- the converter completes the other, and that completion is
    code worth running;
  - a named prefix comes from the corresponding side, and carries no ports of its
    own: coverage compares addresses *and* ports, so ports named against a prefix
    that already restricts them in the manifest would intersect nothing;
  - only TCP and UDP may carry ports at all, so any other protocol and
    any-protocol get none;
  - ports are only named on a side whose exposes do not restrict them, i.e. one
    with no port forwarding;
  - an ACL has at least one rule, since one with none says nothing its peering's
    default action does not;
  - `scope: flow` only where one side of the peering is stateful throughout.

## The scope default is not "unspecified"

Worth its own paragraph, because it cost the most to find. The CRD says a rule's
scope "can be either 'flow' (default if empty) or 'packet'" -- so **omitting the
field asks for flow**, and is refused in exactly the cases an explicit `flow`
would be.

The first version of this drew the scope three ways and let the
flow-is-not-allowed case fall through to omitting the field, which asked for flow
by another name: 908 rules in 6,000 configurations refused for a scope the
generator believed it had avoided. Naming `packet` explicitly took ACL yield from
24% of validated configurations to 64%.

The vacuity test now asserts that *share*, not merely that some ACL survives. An
ACL refused for `scope: flow` is refused for something other than what the rule
says, so a generator that gets it wrong still produces some valid ACLs -- just
far fewer. Reverting the scope fix passes an `acls > 0` assertion and fails this
one.

## Verified

40,000 configurations: 37,611 validate, carrying 72,026 vpcs, 49,646 peerings and
24,742 ACLs, and the three chain properties hold throughout -- so the arrow from
a validated configuration to the one the dataplane applies is now exercised with
ACLs in it, and no defect. Breaking the peering so it attaches no ACL, and
reverting the scope fix, each fail.

Residue, about one in six thousand: a rule whose destination prefix does not
intersect the *to* side's advertised set. The advertised set is read here as "the
translation range where the expose has one, the native prefix otherwise", which
is not quite what `all_public_ips` computes in every case.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
`build_internal_config` turns a validated configuration into the FRR half of it,
and the chain properties cover that. The other half is the dataplane's own
tables, built from the same validated configuration by

  - `build_nat_configuration` -- static NAT,
  - `MasqueradeConfig::new` and `update_nat_allocator` -- masquerade,
  - `build_port_forwarding_configuration` and `PortFwTableWriter::update_table`
    -- port forwarding.

All of them are fallible from a configuration that has already validated, and the
last is where the one confirmed bug of this class actually fired.

So the claim is the same one carried a step further: **a configuration that
validates builds every table it implies.** One property per NAT flavour, using the
generator knobs from a87926f9b -- a property over the default flavour mix reaches
each flavour eventually, one that asks for a flavour reaches it in every case and
says in its name which one failed.

## It reproduces the historical bug

This is the part worth having. `fix(config): Refuse a port-forwarding expose the
dataplane cannot build` (9b216f5bd) was found by reading the code. Reverting it,
and letting the generator draw the shape it refused -- a `/32` carrying N ports
opposite a `/30` carrying N/4, equal totals and unequal lengths -- makes this
property fail on the first case, with the message the dataplane itself produces:

    a validated PortForward configuration would not build port forwarding:
    Can't do port-forwarding between prefixes of distinct length

That is the bug, from generated CRD input, caught at the point it fired in
production: during apply, at the last of the NAT stages, after the kernel
interfaces, the flow filter, the ACLs, the static NAT tables and the masquerade
allocator have all been committed. The class is now guarded by machine rather
than by having noticed it.

## Yields

Per flavour, and each asserted so the property cannot quietly go vacuous:

  - static NAT: 99% of generated configurations validate and build
  - port forwarding: 88%, and 178,152 of 200,000 over a long run
  - no NAT: 82%
  - masquerade: 77%, at a much lower rate per second -- rebuilding the allocator
    walks the address-port pools, so a masquerade case costs about thirty times
    what the others do. Worth knowing before anyone wonders why that one test is
    slow.

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

The validator ships as a wasm module in a process of its own. Its entire surface
is

    ExternalConfig::try_from(&crd)?.validate()?

-- convert, then validate, and nothing else. If it blesses a configuration, that
process writes the configuration to Kubernetes. The dataplane runs the same two
steps later, but it has no way to tell anyone something is wrong: by then the
configuration is the desired state. There is no path back to the user.

So the requirement is not "the dataplane reports bad configurations well". It is
**anything the validator accepts must be enactable**, and every check that lives
only in a downstream builder is a hole in it. A validator that is too strict is a
nuisance -- the user sees an error and fixes their input. One that is too
permissive is unrecoverable.

A panic is the same failure wearing a different coat: in wasm it traps, so the
calling process gets a failure with no `ValidateError` in it, and the user gets
nothing to act on.

## The sister generator

Everything built up to now generates configurations that are legal *by
construction*, which exercises everything downstream of validation and nothing of
validation itself. This adds the other kind: a legal configuration with **one**
rule deliberately broken.

Near-miss rather than arbitrary, because a configuration wrong in one way is far
more likely to slip past than one wrong in twenty. Thirteen mutations, each
naming a rule the validator is supposed to enforce -- mismatched port-forwarding
prefixes, mismatched static-NAT sizes, an exclusion on a port-forwarding expose,
mixed address families, a reserved prefix, an empty private list, a dropped
translation range, both manifests stateful, a missing gateway group, a stranger in
a rule's `from`, flow scope without state, port zero -- and a control that changes
nothing.

## What it asserts

  - **whatever the validator accepts, the dataplane can enact**: the internal
    config builds and renders, and the static NAT tables, masquerade allocator and
    port-forwarding table all build and are accepted;
  - **it never panics**, since reaching the assertions at all means it returned;
  - **a rejection is never `InternalFailure`**, because "this is our bug" is not
    something a user can act on.

Plus enough bookkeeping that the generator cannot quietly stop working: every
mutation must be drawn, the control must rarely be refused (otherwise the mutated
cases are being refused for the wrong reasons), and a mutation that finds a target
must usually be refused.

## Result

150,000 near-miss configurations, **no gap found.** Five of the twelve mutations
are refused exactly as often as they find a target; four are refused more often
than that, the excess being the ~6% baseline rejection the control shows.

`DemandFlowScope` is refused 2,387 times of 3,287 applied, and the ~900 that got
through are legitimate: asking for flow scope on a peering that *is* stateful
throughout is legal. Worth noting because it is why the per-mutation assertion is
"usually refused" rather than "always".

Verified by removing the port-forwarding length check from the validator, which is
the shape of the one confirmed bug of this class. `MismatchPortForwardPrefixes`
then finds it immediately:

    validator accepted a config port forwarding rejects:
    Can't do port-forwarding between prefixes of distinct length

So the property does what it is for: it fails when the validator is permissive,
naming the mutation that got through and the builder that refused what it passed.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
The generator-health assertions -- every mutation was drawn, the control is
rarely refused, an applied mutation is usually refused -- are now
`#[cfg(not(fuzzing))]`.

They describe the *distribution* of the inputs, which is the random engine's
contract. A coverage-guided engine deliberately skews that distribution:
libfuzzer keeps a corpus and steers toward inputs that reach new code, so it will
happily spend a run replaying one mutation ten thousand times. That is the right
behaviour for finding a gap, and fatal to a check that every mutation gets drawn.

The property itself -- whatever the validator accepts, the dataplane can enact --
is what a fuzzer is here to break, and it runs under both engines. `cargo bolero`
sets `--cfg fuzzing` for every engine it drives, so that cfg is exactly the right
question to ask; registered in `[lints.rust]` following `id`'s precedent for
`cfg(kani)`.

With this, `just sanitize=NONE fuzz
tests::mgmt::validator_completeness::whatever_the_validator_accepts_can_be_enacted
1800s -p dataplane-mgmt -j 60 -E=-workers=60` runs the property under libfuzzer.
Thirty minutes of that is **13.6M executions** at 7,567/s aggregate, a corpus of
21,807 inputs, `cov: 10,197  ft: 39,687`, and **no counterexample** -- roughly 90x
the random run, coverage-guided, and it finds nothing.

Note the `-E`: `-j 60` alone gives 32 workers, because libFuzzer defaults
`-workers` to `ncores/2` and only `-jobs` follows `-j`.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
The near-miss property's control is an *unmutated* configuration: legal by
construction, and expected to validate. Under uniform random input it was refused
6% of the time. Replaying libfuzzer's corpus, **22.5%** -- and 89% of those
rejections were a single error, `VPC prefixes overlap`.

That gap between the two numbers is the whole point of running a coverage-guided
engine. A generator flaw that shows up in one random draw in a thousand looks like
noise. A fuzzer finds it, saves the input, and mutates around it, because "the
validator rejects this" is new code and new code is what it is hunting. **The
corpus is a map of the generator's blind spots**, and reading it off is cheaper
than reasoning about where the generator might be weak.

The flaw: every expose of a manifest drew its prefixes from one shared block, so
whether two of them overlapped was a matter of chance. `validate_expose_collisions`
refuses that for most pairs of NAT modes.

## Slots

Overlap is broken by *sharing an address range*, so the fix is to make sharing
impossible rather than unlikely. Each prefix is confined to a nested box, and two
prefixes in different boxes cannot overlap however long they are:

  * **block** -- private or public. Already there; keeps an expose's two sides
    from being the same prefix.
  * **slot** -- one per expose of a manifest.
  * **sub-slot** -- one per prefix of an expose's own list, since a private list
    may hold several and those have to be disjoint from each other too.

`MIN_V4_LEN` goes 16 -> 20 to make room: `172.16.0.0/12` holds 256 slots of /20,
which a `u8` index cannot exceed. v6 keeps /48, which leaves 32,768.

Two consequences fall out of the same rule. A vpc's subnets get a reserved region
at the bottom of each private block, because a *named* subnet contributes its
prefix just as surely as a written-out one does, so it must not land in a slot an
expose draws from -- and the subnets are dealt out round-robin, since a subnet
named by two exposes of one manifest is a prefix those two exposes share. And
`VpcGenerator` now draws the subnet count *before* the mask length: the other order
lets the region run short at that length, and `private_run` would wrap and hand
back the same prefix twice, which is two overlapping subnets.

## Result

Measured over 200,000 configurations on the random engine, the control's rejection
rate falls from **6% to 2.3%**.

The residual is not explained yet. It is still `VPC prefixes overlap`, but the
offending prefixes do not appear literally in the CRD -- a `/51` reported against a
`/91` that *is* in the input, where no `/51` is. So it comes from the converter's
own output: either the post-exclusion decomposition, since subtracting a `not`
from a prefix yields a fan of longer ones, or `collapse_prefixes`. Worth picking
up separately, because if the converter can manufacture an overlap the input did
not have, that is a question about the converter.

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

Two changes that belong together: the generator defect the last commit only
half-fixed, and the assertion whose absence made it expensive to find.

## The assertion first, because it is the lesson

The near-miss property *counted* rejections of its unmutated control and checked
the rate stayed under 25%. It sat at 6%, which reads as tolerable noise. It was
not noise, and a tally is a terrible instrument for finding out why: I read
three-hundred-line configuration dumps and did prefix arithmetic by hand, one
hypothesis at a time, and got nowhere.

Asserted instead -- an unmutated configuration must validate -- bolero shrinks the
failure. One run, and the counterexample is one expose:

    ips: [ cidr 10.1.0.0/20, not 10.1.0.0/21 ]

in two manifests, plus the error naming `10.1.8.0/21` twice. `10.1.0.0/20` minus
`10.1.0.0/21` *is* `10.1.8.0/21`, and it appeared twice because two peers of one
vpc both exposed it. The whole diagnosis, handed over, from a property that
already had the data.

Same lesson as earlier in this campaign, in a new costume: a count looks like
coverage but does no work. If a thing must hold, assert it, and let the shrinker
do the reading.

## The defect

The slot scheme kept the exposes of a *manifest* apart. That is not the rule.
`VpcRouteTable::build` is per vpc, over the exposes its **peers** advertise to it,
and `validate` refuses overlap among them -- because a vpc with one destination
and two places to send it is ambiguous. So prefixes must be disjoint **across
vpcs**, not merely within a manifest, and slot 0 belonged to every vpc at once.

The vpc becomes the outermost level of the scheme: `blocks::expose_slot(vpc,
slots_per_vpc, expose)`, and each vpc's subnets get a slot of their own rather
than sharing one region. `pairs()` and `generate_for` now deal in indices, since a
vpc's *position* is what decides its slots.

Measured on the random engine: the control's rejection rate goes **2.3% -> 0 in
400,000 configurations**, and the near-miss run shows `None  14,495 drawn  0
refused`. Ten minutes of libfuzzer on 60 workers -- ~7.8M executions, corpus
19,393 -- finds no counterexample.

## And the rule now has a mutation

`OverlapWithAnotherPeer` breaks it deliberately: 2,754 applied, 2,309 refused, the
rest legitimately legal because `can_overlap` permits masqueraded and default
routes to overlap within one gateway group. Worth having, because until now this
validator path was reached *only* by the generator's accident, and fixing the
accident would have left it untested.

**Its break test is green, and that is the finding.** Delete the
`OverlappingPrefixes` check and "whatever validates, builds" still passes: two
routes to one destination build fine and the dataplane picks one. The rule is
about *ambiguity*, not *feasibility*, so this property structurally cannot police
it -- a gap in the property, not the validator. Policing it needs a companion
property, "a mutation that breaks a rule must be refused", which needs each
mutation to say whether the case it built is certainly illegal. Recorded at both
sites.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
The near-miss property asks whether an accepted configuration can be *enacted*.
Its break test on `OverlappingPrefixes` came back green, which showed the goal has
a second half it cannot reach: whether an accepted configuration can be enacted
only **one way**.

The two failures are nothing alike from where the user stands. An unenactable
configuration fails to build and somebody gets an error. An ambiguous one builds
perfectly -- two readings, both valid outputs of the code as written -- and the
chain takes whichever its containers hand it first. There is no error to report,
so nothing reports it. Only traffic going somewhere nobody chose, found much
later.

## Permutation as the oracle

A CRD's `expose` list, and the `ips` and `as` lists inside it, are *sets*: their
order is not part of what the configuration means. Nor is which name a peering
carries, since peering names reach no artifact -- the names in the rendered config
come from vpcs. So reordering all of that must leave every artifact the dataplane
installs identical.

The virtue is that it restates no rule, so it can notice an ambiguity nobody
thought to forbid. An ACL's `rules` are deliberately left alone: those are ordered
by definition, first match wins, and permuting them would assert something false.

Driven by `MutatedAgents`, not by legal configurations alone, and that is the
point. The generator now keeps every vpc's prefixes disjoint, so it *cannot*
produce an overlapping-route ambiguity by itself; a permutation property fed only
clean input would pass without ever meeting the case it exists for -- it would be
measuring its own generator. Near-misses put the question where it belongs: when
the validator lets a rule slide, is the result still unambiguous?

Comparison is over sorted lines, because some of these tables are hash maps whose
iteration order is not part of the configuration's meaning. That costs nothing that
matters: the artifacts whose order *is* semantic carry their sequence numbers in
the text, so reordering them changes the lines themselves.

## What it catches, and what it does not

41,623 comparisons, 7,649 of them genuinely reordered, no failure.

**It does not catch run-time ambiguity, and the break test says so plainly.**
Delete the `OverlappingPrefixes` check, so two peers of one vpc may advertise the
same destination, and this property stays silent across 13,908 comparisons. The
reason is structural: an import prefix-list is rendered per peer, so both routes
are installed, in two lists, and the rendered configuration is the same whichever
order the peerings are walked. Nothing was silently picked at build time. The
picking happens later, in the forwarding plane, on a packet.

So the concern splits, and this commit covers one half:

  * **build-time** -- one artifact, two possible contents. Covered here.
  * **run-time** -- one artifact, two rules inside it matching one packet. Not
    covered by anything, and it is the half that misbehaves in production rather
    than in a build.

Recorded at the property, since the next person to read it should know its edge.
The second half needs a check over the installed tables, and it is worth knowing
before writing it that for a rule with no downstream consumer such a check is
necessarily a second statement of the requirement rather than an independent one.

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

The green break test on `OverlappingPrefixes` showed nothing guards the validator
against growing *more permissive* about a rule no downstream builder enforces.
"Whatever validates, builds" cannot: the whole point of that class of rule is that
the thing builds fine.

The guard is the obvious one, and what it needed was not a new property but a
stronger contract on the generator: **a mutation now reports `true` only when the
result is certainly illegal**, so the near-miss property can assert the validator
refuses whatever was touched.

## Certainty is the generator's job

Two mutations broke rules that have legitimate exceptions, so both now check the
exception does not apply before touching anything, rather than producing a case
whose legality is arguable:

  - `DemandFlowScope` skips peerings where a side is stateful throughout, since
    flow scope is legal there. Mirrors `Acl::validate_scope`, and the two being
    separate statements of one rule is the point.
  - `OverlapWithAnotherPeer` copies a prefix only between exposes that advertise
    their `ips` verbatim -- no translation, no exclusions, not a default.

That second condition was wrong on the first attempt, and the new assertion caught
it in five seconds with a shrunk counterexample. Route destinations come from
`VpcExpose::public_ips`, which is the **translation range** for anything that
translates. I had excluded masquerade and thought that enough; the shrinker
produced a static-NAT expose, whose `ips` are its private side and never become a
route at all. So the "overlap" was no overlap, the validator was right to accept
it, and the mutation was lying. Exclusions are out for the same reason:
`public_ips` subtracts the `not`s, which could carve away the very prefix copied.

Worth noting the shape of that: an assertion about the validator immediately found
a defect in the *generator's model of the validator*. That is the differential
test working in the direction one does not plan for.

## Result

Every mutation, over 120,000 configurations: **applied == refused, exactly.** The
control, 26,355 draws, never refused. Those thirteen equalities were previously
an observation printed in a tally; they are now enforced per case, and shrinkable.

Break test: delete the `OverlappingPrefixes` check and the property fails in six
seconds naming the mutation, where before it passed in silence.

`OverlapWithAnotherPeer` applies to about one draw in forty -- it needs two
peerings sharing a vpc and a plain expose on each side. Low, so the new
`applied > 0` health check needs a big sample, and the health checks are now tiered
by sample size: the default one-second run says what it was too small to check
rather than either failing spuriously or looking like it checked. The old ratio
assertions are gone, since the per-case assertions above are strictly stronger.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
daniel-noland and others added 4 commits August 19, 2026 00:33
… for

The table-level ambiguity check turned out not to need a new property. It needed a
mutation that reaches the case, and then the permutation property already had the
answer -- which is a better outcome than a bespoke overlap checker, because it
restates no rule and its failure names the two meanings outright.

## The two tables are not alike

Reading them side by side is the finding:

  - **Port forwarding** cannot be ambiguous. `RangeSet::insert_range` says "overlap
    is forbidden" and returns `Err`, so two rules overlapping within one prefix are
    refused at enact time; and across distinct prefixes `lookup_cumulative` is a
    longest-prefix match, which is a defined total order rather than a choice. Its
    own comment spells out the boundary: "If prefixes overlap and ports too, more
    than a match could happen. This function will provide only one match, for the
    longest prefix."
  - **Static NAT** can be. `NatRuleTable::insert` takes no `Result` and checks
    nothing, so a second entry for one prefix **silently replaces** the first.
    Nothing anywhere reports it.

So `DuplicateAStaticExpose`: two exposes of one manifest claiming a single private
prefix, which `validate_expose_collisions` refuses for every pair of NAT modes
except masquerade-with-port-forwarding.

## Getting the mutation right took two goes

The first version copied the donor expose whole. Two *identical* exposes overwrite
the table entry with an identical value, so there is nothing to pick between --
and the ambiguity property, run against a validator with the overlap check
removed, reported no difference across 43,269 comparisons. It was right not to.
Ambiguity needs one prefix with **two different** translations.

The fix is to move the copy's translation range to the prefix next door. A sibling
is the same length, so static NAT's equal-totals rule still holds and overlap
stays the only rule broken; it is disjoint from the donor's, so the public-prefix
rule holds too; and it sits inside the same parent, so it cannot stray into a
reserved range or another expose's slot. It also needs no agreement between the two
exposes' prefix lengths, which an intermediate version required and which made the
mutation apply to one draw in 250 rather than one in ten.

## Both guards fire, from opposite directions

With `check_private_prefixes_dont_overlap` deleted:

  - the near-miss property fails in **2 seconds** -- the mutation certainly broke a
    rule and the validator accepted it;
  - the ambiguity property fails in **46 seconds**, and says what the two meanings
    were:

        only before:  [10.1.0.0 .. 10.1.7.255] -> [172.16.8.0 .. 172.16.15.255]
        only after:   [10.1.0.0 .. 10.1.7.255] -> [172.16.0.0 .. 172.16.7.255]

One private range, two public ones, and which you get depends on nothing but the
order the configuration was written in. That is the failure this whole line of work
was aimed at, finally on the page.

The first guard is a restatement -- it holds because the generator knows the rule.
The second is not: permutation asked no rule's permission, and would have caught
this even if nobody had thought to forbid it.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
`build_routing_config_peer` builds **every** import prefix list, advertise prefix
list, route-map and VRF import -- the entire peering half of the routing
configuration. It runs only when the peering's gateway group lists *this* gateway,
by name:

    if let Some(rank) = grouptable.get_group_member_rank(peer.gwgroup(), gwname)

Group members were generated with `name: driver.produce::<String>()`, an arbitrary
string, while the gateway's name is `metadata.name` (`host-a...`). An arbitrary
string is never that. So the condition was false in essentially every
configuration ever generated, and **that subsystem has been dead in every property
run of this campaign.** It is why `internal.rs` sat at 42% region coverage with 366
missed lines.

The fix renames a group's single generated member to the gateway's own name, for a
drawn subset of groups so that the not-a-member case still occurs -- a peering
pointed at a group this gateway does not belong to is a real configuration, and the
one that legitimately renders nothing. Replacing rather than adding, because a
group generated here holds at most one member, so replacing cannot collide on a
name or an address and validation refuses both.

Coverage went from `cov: 10197` to `cov: 10586` under libfuzzer: about four hundred
edges of ground no test had ever stood on.

## What was standing on that ground

Two IPv6 defects, in different places, each of which had been hiding the other.
`internal.rs` never uses `IpVer::V6`:

  - **advertise**: the prefix list is `IpVer::V4` and its prefixes are
    **unfiltered**, so a v6 prefix reaches `PrefixList::add_entry` and returns
    `ConfigError::InternalFailure`. Reached when the gateway *is* in the peering's
    group.
  - **import**: the prefix list is `IpVer::V4` *and* filtered by `is_ipv4()`, so v6
    prefixes are dropped in silence. No error, and no route either.

They never appeared together because the first needs the gateway in the group and
the second is only visible when it is not.

`ConfigError::InternalFailure` is the variant that means "this is our bug". The
wasm validator does not build the internal config, so it blesses the configuration
and it is written to Kubernetes; the dataplane then cannot build it, and has
nowhere to report that. This is the failure the whole campaign exists to find.

## Pinned to IPv4, in as few places as possible

Every property that renders a configuration is restricted to IPv4 until that is
settled, each with the reason at the call site, and `chain_properties` through a
single `ipv4_agents()` so there is exactly one line to widen. Three of those are
**pre-existing** properties that this change turns red -- independent confirmation
from tests nobody wrote for this.

`.scratch/ipv6-peering-exec-summary.md` has the write-up.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
The third question to ask of a blessed configuration, after "can it be enacted"
and "does it have one meaning": **is the dataplane doing all of it?**

The failure this hunts is a builder that silently ignores part of its input -- a
shape it does not handle, a `continue` on a branch nobody expected to be
reachable. Nothing else here covers that class, and unlike the ambiguity work it
needs no mutation to reach: such a bug lives in the builder rather than behind a
validator rule, so it shows up on configurations that are entirely legal.

The oracle is removal. Take one expose out and something the dataplane installs
must change.

## Per artifact, not in aggregate

The artifacts are asked **one at a time**, and that is the whole design. Every
expose contributes prefixes to the FRR render whatever else it does, so a merged
comparison would report a difference even where a NAT builder had ignored the
expose completely -- exactly the case worth catching. What each artifact is
entitled to expect comes from the removed expose's own NAT mode, read straight off
the CRD: no model of `collapse_prefixes` or of the PAT splitting is needed, and
none is wanted, since a wrong model would make this property lie rather than fail.

That also retires the counting formulation this replaced. Counting needs the
expected number of table entries, which needs exactly the model that would make it
unreliable.

## It found two defects on its first run, and a third by hanging

  - the gateway-group hole and the IPv6 rendering defects behind it, both fixed and
    documented in the commit before this one;
  - and `NatAllocator`'s `Display`, which never returns on an IPv6 masquerade pool:
    `ips_in_bitmap` walks every set bit of the pool's bitmap, a few thousand
    iterations for a v4 `/20` and unbounded for a v6 pool. Measured, not surmised --
    over IPv4 it completes 380 times in a one-second run, worst case 6ms; over both
    families it does not complete once in 200 seconds. Not a deadlock: 61 crash
    artifacts, every one `slow-unit`, none a `timeout`, at 99.4% CPU. That is why
    this property and `ambiguity` are pinned to IPv4 as well.

It also answered the question it was built on. There is no legitimately no-op
expose by *shape*, but there is by **context**: an expose in a peering whose gateway
group excludes this gateway is not this gateway's to route, so nothing it contains
reaches any artifact. Correct behaviour, unpredictable from the expose alone, and
now exempted by `handled_here`. The property found it by failing.

Once those were in, it held: 9.8 hours under libfuzzer at 60 workers, 470,302 runs
from the five workers that reported, **no counterexample.**

About one case in fourteen reaches the comparison; the rest are configurations with
no manifest holding two exposes, overwhelmingly because they have no peerings at
all. Hence the loose bound in the health check, set from that measurement rather
than from hope, and the note that a floor on vpcs and peerings would do better than
the ceiling `sizes()` can express.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Main moved the generation id from `MasqueradeConfig::new` to
`update_nat_allocator`, which is the right home for it -- the config
describes what to masquerade, and the generation belongs to the act of
installing it. The three call sites these tests grew still passed it the
old way.

Mechanical, and it is the only adaptation the config-generator work
needed against a main that has moved four hundred commits since this was
written.

Kept as one commit rather than folded back into the three that
introduced the call sites. That leaves those three, and the five between
them, unable to compile `dataplane-mgmt`'s tests on their own. Squashing
it back is a `--autosquash` away if bisectable history inside the branch
is worth more than the smaller diff to review.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
@daniel-noland
daniel-noland force-pushed the pr/daniel-noland/fuzz-config-generators branch from 9b658dc to 3ce58bb Compare August 19, 2026 06:33
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

dont-merge Do not merge this Pull Request

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant