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

Closed

daniel-noland wants to merge 65 commits into

pr/daniel-noland/fuzz-flow-entryfrom

pr/daniel-noland/fuzz-config-generators

Commits on Aug 26, 2026

build(nix): keep debug outputs lean

daniel-noland
and
claude
committed
a036a6f
feat(debug): add a version-matched core viewer

daniel-noland
and
claude
committed
b1ef45d
feat(debug): add a live DAP debugger

daniel-noland
and
claude
committed
74af5d2
feat(debug): add a syscall tracer image

daniel-noland
and
claude
committed
43ad401
ci: publish debug images on a deliberate cadence

daniel-noland
and
claude
committed
9b9b9bf
test(debug): exercise the debug images instead of only building them

daniel-noland
and
claude
committed
c666922
feat(debug): run a binary or a single test inside the debug images

daniel-noland
and
claude
committed
06c0cca
docs: Record what a commit message carries

daniel-noland
and
claude
committed
1f46121
build(just): Write an lcov report beside the html one

daniel-noland
and
claude
committed
d2e63fe
build(nix): Add cargo-expand, cargo-mutants and cargo-show-asm to the dev shell

daniel-noland
and
claude
committed
c99490e
feat(debug): Build gdb and perf to run where there is no nix store

daniel-noland
and
claude
committed
d1398e3
feat(debug): Dump a core from a running process without ending it

daniel-noland
and
claude
committed
9016291
build(nix): Add duvet to the dev toolchain

daniel-noland
and
claude
committed
3a27f88
build(nix): Add deno to the dev toolchain
daniel-noland
committed
90a2468
feat(spec): Cross-check a test citation against its implementation citation
daniel-noland
committed
1888d67
build(just): Recipe-ise duvet, cargo-mutants, and the interlock
daniel-noland
committed
fa4dca5
feat(spec): Let the interlock classify a mutant instead of only killing it
daniel-noland
committed
931636e
feat(spec): Say why a mutant survived, using coverage
daniel-noland
committed
8b75611
fix(spec): Accept the second-half boundary the block guard makes unreachable
daniel-noland
committed
0ea0d48
fix(net): Store the checksum an incremental update computes

daniel-noland
and
claude
committed
5be2ae5
test(net): Check the HeadersView unsafe boundary against the safe matcher

daniel-noland
and
claude
committed
88c3696
docs(net): Correct where the HeadersView soundness check actually fires

daniel-noland
and
claude
committed
6edcf93
test(net): Check the mutable half of the HeadersView boundary, and make miri usable

daniel-noland
and
claude
committed
83f48b5
test(net): Extend the HeadersView differential to every arity the oracle reaches

daniel-noland
and
claude
committed
1ef005f
test(net): Reach the quoted packet inside an ICMP error, and the extension region

daniel-noland
and
claude
committed
bcaf281
test(net): Cover the optional matchers, and find what their combinators watch

daniel-noland
and
claude
committed
1f0592e
test(net): Make the shape follow the chain, and reach every arity's look

daniel-noland
and
claude
committed
c7cde9b
test(net): Stack the extension headers the builder always could

daniel-noland
and
claude
committed
9833e03
test(net): Specialize the ICMP subtypes, and find that conform is dead

daniel-noland
and
claude
committed
214a62b
test(net): Keep the embedded vacuity guard armed under coverage

daniel-noland
and
claude
committed
f5188c3
test(routing): Property-test the rib-to-fib conversion

daniel-noland
and
claude
committed
d76f633
fix(routing): Survive a resolution loop in the next-hop walks

daniel-noland
and
claude
committed
651e14f
test(routing): Model-check a fib against its change log

daniel-noland
and
claude
committed
f73e5e2
fix(routing): Drop a fib's vni alias when the fib goes

daniel-noland
and
claude
committed
f5914fa
fix(routing): Refuse to remove the default vrf

daniel-noland
and
claude
committed
975ce59
fix(frrmi): Frame a message by what arrived, not by what was asked for

daniel-noland
and
claude
committed
55dae08
fix(routing): Install a route with no next-hops as a drop, in the rib

daniel-noland
and
claude
committed
5930a7a
test(routing): Cover the vrf deletion check

daniel-noland
and
claude
committed
cc439c9
test(routing): Property-test resolution across vrfs

daniel-noland
and
claude
committed
13d1391
fix(routing): Keep the interface name out of the next-hop key

daniel-noland
and
claude
committed
cb73a72
test(routing): Property-test the control-plane operations

daniel-noland
and
claude
committed
4a29b7c
test(routing): Property-test the FRR config renderers

daniel-noland
and
claude
committed
bde423f
test(routing): Model-check the interface table and its attachments

daniel-noland
and
claude
committed
e808861
test(routing): Property-test the adjacency table's publish discipline

daniel-noland
and
claude
committed
20dc819
fix(flow-entry): Add an insertion that will not displace a live flow
daniel-noland
committed
9c58af9
feat(config): Generate port-forwarding exposes for property tests

daniel-noland
and
claude
committed
bddea17
feat(config): Generate masquerade exposes, and share the overlay around them

daniel-noland
and
claude
committed
26e386f
feat(config): Generate static NAT exposes, and pin the mapping is a bijection

daniel-noland
and
claude
committed
2c5390f
fix(config): Refuse a port-forwarding expose the dataplane cannot build

daniel-noland
and
claude
committed
c37054f
refactor(config): Report a port-forwarding mismatch as a typed error

daniel-noland
and
claude
committed
fca2514
test(mgmt): Property-test the configuration chain, and unblock its generators

daniel-noland
and
claude
committed
4b30d51
test(mgmt): Drive the config builder with generated NAT peerings

daniel-noland
and
claude
committed
da7879d
test(k8s-intf): Generate configurations that are valid by construction

daniel-noland
and
claude
committed
a81bcb8
test(k8s-intf): Generate peering ACLs

daniel-noland
and
claude
committed
3fd3f38
test(mgmt): Build every dataplane table a validated config implies

daniel-noland
and
claude
committed
c0ca439
test(config): Hunt validator permissiveness with near-miss configurations

daniel-noland
and
claude
committed
d2aedf8
test(mgmt): Let a fuzzing engine drive the near-miss property

daniel-noland
and
claude
committed
8e511d9
test(k8s-intf): Draw prefixes from slots so exposes cannot overlap

daniel-noland
and
claude
committed
3fa5286
fix(k8s-intf): Give every vpc its own slots, and assert the control validates

daniel-noland
and
claude
committed
868052f
test(mgmt): Check that a validated configuration has only one meaning

daniel-noland
and
claude
committed
aebfa90
test(config): Assert the validator refuses what a mutation certainly breaks

daniel-noland
and
claude
committed
92ec8f2
test(nat): Catch a static NAT table that holds one of two rules asked for

daniel-noland
and
claude
committed
a6ae1c0
fix(k8s-intf): Put the generated gateway in its own gateway groups

daniel-noland
and
claude
committed
4a0d639
test(mgmt): Check that every expose leaves a trace

daniel-noland
and
claude
committed
5fa4347
test(mgmt): Follow the genid out of MasqueradeConfig

daniel-noland
and
claude
committed
641ac94