(01) validator - #1796
Draft
daniel-noland wants to merge 41 commits into
Draft
Conversation
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 documentation. 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. One constraint that is 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. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.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. 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. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.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; 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. 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. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.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. `MismatchedPrefixLengths` and `MismatchedPortRangeSizes` each carry what did not line up, naming 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` cannot be reused for the length case, tempting as that is: it compares addresses times ports, and the pairing this rejects has that product equal on both sides, so it would print two numbers that are the same and ask the operator to reconcile them. One shape is therefore reported differently than before: a /24 opposite a /25 said `MismatchedPrefixSizes(256, 128)`, and now says that port forwarding requires prefixes of the same length. That error's own message is reworded while here, since it named neither what has to hold nor which side is which. 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 mid-sentence. Giving that type a `Display` is worth doing in lpm. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.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 where a configuration
which validates and cannot be built would live.
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.
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
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. The family is now
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.
The remaining failures share 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. The vacuity test asserts a twentieth for
now, and is written to be strengthened to require peerings once that lands.
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The third arrow of the configuration chain --
GatewayAgent (CRD) ─▶ ExternalConfig ─▶ validated ─▶ InternalConfig ─▶ FRR
-- had never been given a peering. The CRD generators produce exposes that
validation always refuses, so the half of the model where the exposes, the NAT
and the ACLs live 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 that a configuration which validates can be built and rendered. One
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. The port-forwarding
expose that validated and could not be built is precedent for the class. It holds here
across mixed NAT flavours; nothing found.
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. One of those matters 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.
The vni checks alone cannot see a build that skipped the overlay, the underlay
vrf, the underlay's bgp peers or the community table, so the property asserts
each of those directly rather than inferring them.
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The CRD generators produced peerings in quantity and none survived validation.
Three causes were fixed alongside the measurement that found it; this finds the
rest, and turns the entry point into something a property can aim with.
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. 94% of generated configurations now validate, carrying peerings,
against 17% carrying none.
`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, so the name asserted a property it did
not have. 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.
Three smaller things:
- `start + size - 1` overflowed `u16` for a port range ending at 65535, since it
groups as `(start + size) - 1`. 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.
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.
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.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.
The ACL is built from the manifests rather than beside them, and 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 worth its own paragraph. 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. Letting
the flow-is-not-allowed case fall through to omitting the field therefore asks
for flow by another name: naming `packet` explicitly took ACL yield from 24% of
validated configurations to 64%.
The vacuity test asserts that share rather than 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, which an `acls > 0` assertion cannot see.
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.
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.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 port-forwarding expose that validated and could not be built
actually fired. So the claim is the same one carried a step further: a configuration that
validates builds every table it implies.
That defect was found by reading the code. This is what would have found it, from
generated CRD input, at the point it fires 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.
One property per NAT flavour, using the generator knobs: 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. Each asserts its
own yield so it cannot quietly go vacuous.
Masquerade runs at about a thirtieth of the others' rate, because rebuilding the
allocator walks the address-port pools. Worth knowing before anyone wonders why
that one test is slow.
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.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
that **anything the validator accepts must be enactable**, and every check living
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.
Everything up to here 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. "Usually" rather than "always" because `DemandFlowScope`
has a legitimate exception -- asking for flow scope on a peering that *is*
stateful throughout is legal.
No gap found yet.
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.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 the property runs under libfuzzer:
just sanitize=NONE fuzz \
tests::mgmt::validator_completeness::whatever_the_validator_accepts_can_be_enacted \
1800s -p dataplane-mgmt -j 60 -E=-workers=60
Note the `-E`: `-j 60` alone gives 32 workers, because libFuzzer defaults
`-workers` to `ncores/2` and only `-jobs` follows `-j`.
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.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.
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.
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.
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…alidates
Two changes that belong together: the scope the slot scheme has to have, and
the assertion whose absence made that expensive to find.
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: it says a
rate and nothing about which configuration or which prefix.
Asserted instead -- an unmutated configuration must validate -- bolero shrinks the
failure, 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. If a thing must hold, assert it, and let the shrinker do the
reading.
The rule is not what a per-manifest scheme expresses. Keeping the exposes of a
*manifest* apart is not enough. `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. The control's rejection rate goes from
2.3% to none observed.
The rule now has a mutation of its own. `OverlapWithAnotherPeer` breaks it
deliberately, and about one in six of the cases it builds is 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.
It also exposes an edge of the enactability property. Delete the
`OverlappingPrefixes` check and "whatever validates, builds" still passes: two
routes to one destination build fine and the dataplane picks one. That rule is
about *ambiguity*, not *feasibility*, so this property structurally cannot police
it -- a gap in the property, not in 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.
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The near-miss property asks whether an accepted configuration can be *enacted*.
Its edge on `OverlappingPrefixes` shows 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.
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 of permutation as the oracle 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.
It does not catch run-time ambiguity. With the `OverlappingPrefixes` check gone,
so that two peers of one vpc may advertise the same destination, this property
stays silent -- and structurally must, because 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 is
silently picked at build time. The picking happens later, in the forwarding plane,
on a packet.
So the concern splits, and this 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.
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…breaks
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 is narrower than it looks like it needs to be. Route
destinations come from `VpcExpose::public_ips`, which is the **translation range**
for anything that translates, so excluding masquerade is not enough: a static-NAT
expose's `ips` are its private side and never become a route at all, which makes
the "overlap" no overlap and the mutation a liar. Exclusions are out for the same
reason -- `public_ips` subtracts the `not`s, which can carve away the very prefix
copied.
Worth noting the shape of that: an assertion about the validator finds a defect in
the *generator's model of the validator*. That is the differential working in the
direction one does not plan for.
The thirteen equalities between applied and refused were previously an observation
printed in a tally. They are now enforced per case, and shrinkable.
`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 are strictly stronger.
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… for
The table-level ambiguity check needs no new property. It needs a mutation that
reaches the case, and then the permutation property already has 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, and 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.
Copying the donor expose whole would not do. Two *identical* exposes overwrite the
table entry with an identical value, so there is nothing to pick between and no
ambiguity to detect; ambiguity needs one prefix with **two different**
translations. So the copy's translation range moves 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 would drop the mutation's reach
from one draw in ten to one in 250.
With `check_private_prefixes_dont_overlap` gone, both guards fire from opposite
directions. The near-miss property fails because the mutation certainly broke a
rule and the validator accepted it. The ambiguity property fails naming the two
meanings:
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.
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.
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.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 so far. 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, either of which validation refuses.
Standing on that ground for the first time turns up 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.
Every property that renders a configuration is pinned 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 it.
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.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. 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 replaces, which needed the expected number of table entries and so needed exactly the model that would make it unreliable. Two defects fall out of it directly -- the gateway-group hole and the IPv6 rendering behind it, both in the commit before this one -- and a third by hanging. `NatAllocator`'s `Display` 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. 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`. 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, and the note that a floor on vpcs and peerings would do better than the ceiling `sizes()` can express. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.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. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…dent Nothing in this module uses `IpVer::V6`, and left to themselves the two prefix lists failed differently and both badly. The advertise list is `IpVer::V4` over unfiltered prefixes, so a v6 prefix failed `is_version_compatible` and came back as `ConfigError::InternalFailure` -- the one rejection this crate's own mutation property asserts a configuration must never get, on the grounds that "this is our bug" is not something anyone can act on from the outside. The import list was `IpVer::V4` *and* filtered by `is_ipv4()`, so v6 prefixes were dropped in silence. That half is the worse one: the configuration applies, reports success, and carries no traffic. `build_internal_config` runs in `process_incoming_config` before `apply`, so this was already a clean rejection and nothing was committed when it fired -- contrary to what the comment on `chain_properties::ipv4_agents` says, which took the partial-apply argument from the port-forwarding case, where `apply_port_forwarding_config` really does run after the other stages. What changes here is what the operator is told, and that the silent half stops being silent. Here rather than in `VpcExpose::validate` because it is this module that is IPv4-only. NAT's static, masquerade and port-forwarding tables build and translate v6 today; refusing a v6 expose outright would take that away to guard a limitation it does not have. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>
…n skip `ipv4_agents` documents widening its family list as the way to find out whether IPv6 rendering has landed, on the grounds that `chain` treats a declared limitation as a skip. It was a skip in one of the module's two build sites; the other unwrapped, so following the documented procedure would have failed `every_vpc_gets_a_vrf_and_no_more` on a legal configuration, with a message blaming the builder. The guard in `VpcRoutingConfigIpv4` also ran after the field it protects had already been extended. Signed-off-by: Daniel Noland <daniel@githedgehog.com>
`SUBNET_SLOTS` reserves sixteen slots, one per vpc, and `expose_slot` saturates. A caller asking `SpecBuilder` for more vpcs or exposes than that gets colliding slots rather than a panic, which puts the generator back to producing the overlapping prefixes the whole scheme exists to prevent -- and the only symptom is that the properties downstream go quiet. The doc comment describing `apply`, and its `too_many_lines` allowance, were attached to `stateful_throughout`: doc comments are attributes, so both blocks and the attribute bound to the following item. Signed-off-by: Daniel Noland <daniel@githedgehog.com>
|
Important Draft PR not reviewedDraft PRs are not automatically reviewed by default.
To automatically review draft PRs, update your CodeRabbit configuration: reviews:
auto_review:
drafts: trueComment |
daniel-noland
added
clean-up
The text above this const was removed at some point and the bare `///` left behind. `clippy::empty_docs` is denied at the crate root, so the whole crate fails to lint, and with it the `check/debug` CI job for every pull request in this stack. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>
These three are `pub` and return `Result`, so `clippy::missing_errors_doc` demands an `# Errors` section. The crate lints clean without the `bolero` feature and fails with it, which is how this got past a default build: only nat and mgmt turn the feature on, and they do it from dev-dependencies. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>
daniel-noland
force-pushed
the
pr/daniel-noland/fuzz-config-generators
branch
from
September 3, 2026 05:59
ada351f to
17aec1a
Compare
Codecov Report❌ Patch coverage is 📢 Thoughts on this report? Let us know! |
…dress
`num_prefix_bits` is how many high-order bits it takes to keep `count`
addresses apart. It was computed as `u32::BITS - count.leading_zeros()`
for v4 and `u128::BITS - count.leading_zeros()` for v6, but `count` is a
`u16`, so its leading zeros never exceed 16 and the width of the address
leaked into the width of the counter.
The floor that produced was 17 for v4 and 113 for v6. A generated gateway
interface could never be a /24 or a /64, whatever the driver chose. Per
development/code/property-testing.md, a `TypeGenerator` should eventually
cover all legal values, and `LegalValue<GatewayAgentGatewayInterfaces>`
reaches these through `LegalValue<GatewayAgentSpec>`, so this was a hole
in a spanning generator rather than a deliberate narrowing.
Measured before and after, for one address and for ten:
v4 1 /17../32 -> /1../32
v4 10 /17../32 -> /5../32
v6 1 /113../128 -> /1../128
v6 10 /117../128 -> /5../128
The existing uniqueness and network/broadcast properties could not see
this, so the extracted `distinguishing_bits` gets a deterministic test
rather than a sampled one.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Four holes in what `LegalValue<GatewayAgentSpec>` could reach. Per
development/code/property-testing.md a `TypeGenerator` should eventually
cover all legal values, and this one is the root of the whole config
chain, so each hole capped every property built on top of it.
- `VpcGenerator` drew a `Vni` spanning the 24-bit space and the spec
generator then overwrote it with `vni_base + i`, `vni_base` drawn from
1..=1000. No configuration ever named a vni above 1004. Keep the draw
and settle collisions by walking forward, as the internal id already
did.
- `for i in 0..=num_groups` over a count drawn from 0..=6 made a gateway
with no groups unreachable. That off-by-one was load bearing:
`LegalValuePeeringsGenerator::new` refuses to build a peering with no
group to name, and the caller unwrapped it. Peerings are now skipped
when there are no groups instead.
- `GatewayAgentGroups` drew up to ten members and then pushed exactly
one, so no group ever had a second member and no member ever had a
rank above zero.
- Community values were `format!("65000:{}", 100 + i)`, fully determined,
so no configuration named any other community.
The last two are coupled. A member's rank is its position in its group and
`validate_gw_groups` refuses a rank with no community, so the largest group
sets the floor on the community count; drawing them independently produces
an illegal config, which the suite caught at once with "No BGP community
exists for rank 0". Uniqueness is likewise a legality constraint, not a
nicety: `add_member` refuses a repeated name or vtep address and
`PriorityCommunityTable::insert` refuses a repeated community.
Two health guards go red with this, both because they were calibrated
against the old distribution rather than because they found a defect:
ambiguity permutation moved 71 of 759, needs 10%
relevance 28 of 1221 reached the comparison, needs 2.5%
`relevance` is thin for a structural reason worth fixing separately: it can
only drop an expose from a manifest that has two, and at the default knobs
only about 39% of configurations carry a peering at all.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
`reorder_agent` collected the peering names, shuffled the bodies, and zipped them back together. Names come out of a `BTreeMap` sorted, so this handed each name a different peering's body. That is a different configuration rather than a reordering of this one, and `ambiguity` asserts the built artifacts are unchanged, so the property was only correct because a peering's name never reaches the artifacts. Any future use of the name would have turned it into a false failure with no obvious cause. A `BTreeMap` has no order to permute, so the fix is to drop that step. The lists inside a peering are what an ordering property has to be about, and those were already being reordered. `moved` is now reported by `reorder` itself rather than recovered by comparing two `Debug` renderings of the whole peering map. That is cheaper than the permutation it was measuring, and truer: a list of equal elements really was reordered even though the rendering does not change. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>
The health checks guard against a property going quietly vacuous, which is
worth having, but they were ratio assertions calibrated against one
generator's output distribution. Two consequences.
Under miri and under qemu a property gets a handful of cases rather than a
few thousand, so every one of these thresholds measures nothing there and
can only flake. They now sit behind an `ENOUGH_CASES` gate; below it the
counts still print, and coverage data is the thing to watch.
Natively they were tuned so finely that improving a generator broke them.
Measured on the current generators, with the new floors:
ambiguity reordered 9% floor was 10%, now 4%
relevance reached comparison 2.4% floor was 2.5%, now 1%
vacuity carry an acl 51% floor was 50%, now 25%
Loosening a guard is normally the wrong repair, so each floor now records
what was measured and why the rate is what it is, and the numbers stay on
stdout. The acl rate moved because a gateway with no groups is now a
reachable shape and carries no peering, hence no acl. `relevance` is low
for a structural reason: an expose can only be dropped from a manifest
holding two, and most configurations carry no peering at all. Raising that
honestly needs a generator biased to guarantee a peering.
Break-tested: with `reorder` stubbed to do nothing, ambiguity still fails
with "0 of 873 comparisons actually reordered anything".
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
The subnet references were chosen with `take(n)` over a list, which selects a prefix of it rather than a subset. An expose could never name the second subnet without also naming the first, so a gap in the references was unreachable and nothing downstream ever saw one. Drawing a bool per subnet spans all of them. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>
`external_offering` called the gateway "test-gw" while the only member of
the "default" group that `VpcPeering::with_default_group` names was
"gw-default". `build_routing_config` looks the gateway up in the peering's
group and skips the peer when it is not a member, so the entire per-peering
half of the FRR build never ran. No advertised networks, no prefix lists,
no route-map entries, and not one of the generated exposes reached any
routing code. Everything the property asserted came from the per-vpc and
underlay build instead, so a NAT expose's public prefixes could have been
missing from the rendered configuration and this test would still pass.
Verified by probe both ways: with a `panic!` at the top of
`build_routing_config_peer` the property was green before this change and
fails after it.
Reaching that code immediately surfaces the IPv6 limitation, since half the
generated exposes are IPv6 and the FRR configuration built from a peering
is IPv4-only. Rather than narrow the generator to hide it, the refusal is
now checked: only an IPv6 configuration may be refused as unsupported, the
count is printed and asserted non-zero, and the arm says what to do if the
limitation ever lifts. A validated IPv6 peering still fails at apply time
rather than at submit time, which is a real gap this does not close.
3304/5906 built, 1290 with several exposes, 1646 refused as ipv6
The gateway name is a const now, next to the group that has to contain it,
because the two silently agreeing is the whole defect.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Now that the property actually runs the per-peering build, it should say
something about the result. Everything it asserted came from the per-vpc
and underlay half, so deleting the body of `build_routing_config_peer`
left it green.
Read the prefixes back out of the validated configuration rather than the
offered exposes, since validation collapses and normalises them and it is
the collapsed form that gets rendered. Masquerade in particular offers
adjacent blocks that merge.
Break-tested with `return Ok(())` at the top of `build_routing_config_peer`,
the mutant that used to pass everything:
3.3.3.0/24 is advertised by a peering but never reaches the rendered config
The four `chain_properties` tests still survive that mutant. They reach the
peering build but assert nothing downstream of it, which is the same gap
one layer up and is left for a follow-up.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
…lently
Two things these four properties could not see.
They ran `build_routing_config_peer` and then asserted nothing that came
out of it, so replacing its body with `return Ok(())` left all four green.
`whatever_validates_builds_and_renders` now checks that every prefix a
peering advertises reaches the rendered configuration, which is the one
assertion here that depends on that half of the build having happened.
Only peerings this gateway handles count. A peering whose group the gateway
does not belong to, or whose rank has no community, is legitimately absent
from the output; demanding its prefixes would assert a bug into place. The
first draft got this wrong and failed on a peering the gateway was not a
member of, which is worth recording because it is the same membership rule
that made the sibling property in mgmt.rs vacuous.
Separately, `build_or_skip` folded `ConfigError::Unsupported` into a `None`
that every caller quietly returned on. That error has one producer,
`reject_ipv6`, and these properties generate IPv4 only, so the arm never
fired and nothing counted it. It was a silent skip waiting for the day the
generator learned IPv6, at which point a real "the validator accepted what
the builder refuses" defect would have become invisible. It now builds or
panics.
Break-tested with `return Ok(())` at the top of `build_routing_config_peer`:
10.0.19.128/25 is advertised by a peering this gateway handles but
never reaches the rendered config
1769 advertised prefixes are checked across roughly 2000 configurations per
run. The remaining three properties still survive that mutant by design:
they are about vrf creation, generator health and determinism.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
`every_vpc_gets_a_vrf_and_no_more` compared two sets of vnis. That leaves
almost everything about a vrf unchecked: two vrfs sharing a vni collapse
into one set element, so "and no more" was not tested either, and name,
description, vpc id and route table were never looked at.
Each vpc's vrf is now matched and checked. The route table gets the most
attention because it is the part with a rule behind it: a vrf's table is
the vpc's vni, so an operator can reach it by the number they already know,
except for the three vnis that collide with tables the kernel reserves,
which move above the vni space. The uniqueness that rule exists to protect
is asserted directly.
Break-tested by pointing every vrf at `1000 + vni`, a mutant that used to
pass this and every other test in the branch:
the vrf for vpc0 points at the wrong route table
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
The oracle read the first port of each range and counted the rules. Two mutants got through it, both of which silently drop traffic. Collapsing each rule to a single port, by building it from `(start, start)` instead of `(start, end)`, passed because nothing looked at the end of a range. An expose may forward up to a thousand ports. Installing TCP twice for an `any` expose passed because the count was right and nothing read `key.proto()`. That leaves UDP forwarding entirely uninstalled for every `any` expose. The downstream NF fuzz in the (02) PR does not cover the protocol either: its probe chooses transport with `proto != L4Protocol::Udp`, so an `any` expose is only ever probed over TCP. Worth fixing there too. The match over `L4Protocol` is left exhaustive rather than given a catch-all, so a new protocol variant is a compile error here instead of a panic during a fuzz run. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Two steps of `apply_gw_config` that no property here touched. Around half
of validated configurations carry an ACL, and mgmt depends on dpdk with the
comment that it is for tests that build the rte_acl-backed filter, but
nothing was building one: an ACL the validator accepts and rte_acl refuses
would have gone unnoticed.
Its own property rather than another line in the three enactment helpers,
because an rte_acl build is expensive and those properties are worth more
cases than they are worth ACL coverage. It reports what it covered:
1690/1690 validated and built their filters, 321 carrying an acl
Also converts `drive` from a function to a macro. `bolero::check!()`
registers a fuzz target named for the item enclosing it, so four tests
sharing one helper registered a single target under the helper's name that
no test could be selected by. This is the fix from the (12) PR hoisted to
where the defect was introduced.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Two places where one fact was written down more than once, and the
duplicates were not tied together by anything.
`Mutation` had a hand-written `all()` next to a hand-written `COUNT = 15`
next to the enum itself. `check_generator_health` sizes
`[AtomicUsize; COUNT]` and indexes it by position in `all()`, so a variant
added to the list but not the count indexed out of bounds during a fuzz
run, and a variant added to the enum but not the list was simply never
drawn. The second is the exact vacuity that health check exists to catch,
defeated one layer earlier. `strum::VariantArray` derives the list from the
enum and `COUNT` from the list. Adding a variant is now a build error in
`apply`, which is where it should be caught.
`Dropped::nat` carried `Option<&'static str>` holding "static",
"masquerade" or "port forwarding", and `relevance` matched those literals
with an `unreachable!("unknown nat mode")` arm.
development/code/error-handling.md calls arbitrary string values actively
hostile and matching on their contents extremely fragile, and this is why:
a typo in the producer or the consumer compiled cleanly and surfaced as an
`unreachable!` during a fuzz run. It is a `NatFlavour` now, and the match
is exhaustive.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
`generate_prefixes`, `generate_v4_prefixes`, `generate_v6_prefixes`, `UniqueV4CidrGenerator` and `UniqueV6CidrGenerator` have had no callers since the exposes were rewritten onto `blocks`. This branch's only edit to that half of the file, raising their mask floors, was therefore dead when it was written. Their two self-tests go with them, along with the `ITERATIONS` constant that existed only to keep them fast. `choose` was dead for the same reason, but it is the helper that the hand-rolled index-into-slice sites should be using, so it is kept, given the empty-slice guard the copies lacked, and adopted at the five sites where it is a drop-in. That leaves one place deciding how a choice is drawn, which matters if these ever move to a generator that shrinks better. The two remaining copies are not drop-ins: `reduce` and `spec` want the index so they can `swap_remove`, not the value. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>
A manifest may not mix IPv4 and IPv6 exposes; the validator refuses one
outright. Each contract generator drew its own family, so a caller building
several exposes for one manifest produced an illegal configuration most of
the time, and saw it as a validation failure rather than as a limitation of
the generators.
Measured on `peering_chain`, where the whole list lands in one manifest:
before 3304/5906 built (56%), 1290 with several exposes
after 3912/4471 built (87%), 2400 with several exposes
That also lifts the `built * 2 >= seen` guard off its floor, which it was
sitting six points above.
The three generators take a `Family` that defaults to `Either`, so a lone
expose still draws its own and every existing call site keeps its
behaviour. Diagnosed by printing the refusals rather than guessing: a first
attempt widened the fixture's remote manifest to offer both families, which
moved the rate not at all, because the problem was the local manifest.
Also documents the two places a reader would otherwise have to work out for
themselves: `IMPORT_VRFS` is compile-time false and flipping it turns a
silent IPv6 omission into a hard refusal, and the port-forwarding table
assertion cannot fire until the (04) PR gives `validate_ruleset` a body.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
The two checks that keep one vpc's subnets off another vpc's exposes were `debug_assert!` followed by saturating arithmetic, and `private_run`, which lays subnets into the same space, had no check at all. A release build is where a fuzzing engine runs, so it is exactly where the saturating fallback would hand two exposes the same slot without a word. The failure then looks like the validator wrongly refusing a configuration, which is a long way from the sizes the caller actually asked for. Unconditional now, and `unreachable!` rather than a silent clamp, per the programmer-error guidance in development/code/error-handling.md. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>
`pub mod bolero` is gated on `any(test, feature = "bolero")`, so the module compiles in an ordinary `cargo test` where the optional `strum` dependency is not linked, and the `VariantArray` derive did not resolve. It is a dev-dependency now, the same way `bolero`, `lpm` and `net` already are. Found only by linting the crate on its own: linting it alongside mgmt, whose dev-dependencies turn the feature on, unified the feature and hid it. Worth remembering when checking a crate that has a test-only module. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>
… serve `enact` is reached only when the drawn mutation found no target, because a mutation that did apply is required to have been refused. The mutation names in its panic messages therefore identify the draw rather than describe a mutated configuration, which reads as though mutated input is being enacted when it never is. No behaviour change. The enactment half runs on unmutated input by design, and the mutations earn their keep in the refusal half. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Signed-off-by: Daniel Noland <daniel@githedgehog.com>
daniel-noland
force-pushed
the
pr/daniel-noland/fuzz-config-generators
branch
from
September 3, 2026 06:22
17aec1a to
51c9c5f
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.