config by daniel-noland · Pull Request #1763 · githedgehog/dataplane

daniel-noland · 2026-08-26T03:01:28Z

No description provided.

coderabbitai · 2026-08-26T03:01:55Z

Important

Draft PR not reviewed

Draft PRs are not automatically reviewed by default.

Trigger a manual review

To automatically review draft PRs, update your CodeRabbit configuration:

reviews:
  auto_review:
    drafts: true

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

codecov · 2026-08-26T03:25:23Z

❌ 1 Tests Failed:

Tests completed	Failed	Passed	Skipped
1748	1	1747	0

View the top 1 failed test(s) by shortest run time

dataplane::bin/dataplane::packet_processor::fuzz::acl::the_acl_verdict_follows_the_protocol_the_packet_carries

Stack Traces | 1.23s run time

thread 'packet_processor::fuzz::acl::the_acl_verdict_follows_the_protocol_the_packet_carries' (9749) panicked at ..../src/packet_processor/fuzz.rs:501:5:
no packet was ever denied. Check for a `__fuzz__` corpus beside this test before reading further: replaying one can spend the budget on inputs chosen for being unusual. Move it aside and re-run to tell that apart from a real gap.
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

To view more test analytics, go to the Test Analytics Dashboard
_{📋 Got 3 mins? Take this short survey to help us improve Test Analytics.}

A device with no `driver` symlink has no driver bound, which is ordinary whenever the module was not loaded or was already unbound -- not the error `driver()` reported and not a reason for `BindToVfioPci` to refuse. Both now proceed to the override-and-bind that was always the intent. Reached first under QEMU, whose e1000 NICs the guest kernel does not claim, but the case is not virtual: a bare-metal NIC whose module was never modprobed presents exactly the same way. `e1000`/`e1000e` join the driver enum, and dpdk-sys links the matching PMD, for the same reason. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

`Conversation` built its reply from the address the sender aimed at rather than the address the request arrived on. Correct for every peer this load had ever met: `can_receive_connection` is false for masquerade, so `outward` could only ever find a forwarded expose, where the two are the same address. They differ as soon as an expose both translates and accepts connections. The far side then holds the private address, and answering from the public one is a source that vpc may not use -- which the flow filter refuses, and which looks exactly like a lost reply. This also makes `judge_reply`'s existing claim mean something. It asserts the reply's source is the address the request was aimed at; until now the load supplied that value itself, so the assertion could not fail. It is now a statement about the pipeline's reverse translation. Read off the delivered packet rather than computed from the configuration, for the reason `static_nat::fuzz` gives: a test that predicted an address would be a second copy of `RangeBuilder`, and two copies disagree. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Masquerade combined with static NAT allocated a fresh public tuple for every packet of a burst: eight packets of one flow left under eight public tuples and put eight reverse entries in the table. The pipeline runs `static_nat` before `masquerade`, so by the time masquerade sees a packet its destination has already been rewritten and the key it carries is no longer the key `FlowLookup` used. `create_flow_pair` files the forward flow under the *initial* key for exactly that reason -- `FlowLookup` runs first and would otherwise never find the flow again -- while the intra-burst fallback in `get_masquerade_state` looked it up under the key the packet carries now. Equal whenever nothing translated the destination, which is why one lookup sufficed. The fallback is tried second rather than first so this only adds a lookup where the old code found nothing: a reply is keyed on `new_reverse_session`'s derivation of the current key and must keep matching first. The combination was unreachable from the two-vpc fixture, whose far side is always one plain prefix; `overlay_between` lets a test name both sides. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

`Flavour` had two members, so no generated configuration could contain static nat at all. The completeness census recorded that as two of its thirteen unreachable degrees of freedom, and the enactment instrument's `StaticNat` row was a store of an empty table reporting that it disturbed nothing -- which is not evidence about a store that has never run. The address plan already gives every expose a disjoint private and public /24, which is what a one-to-one mapping needs and what `validate_expose_collisions` asks of the combination, so no new rule was required: every drawn sequence still builds a configuration the validator accepts. Last of the three because it is what found the other two. A configuration mixing masquerade with static nat takes a path neither takes alone, and the two commits below are the harness fault and the dataplane defect that were sitting on it. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Two more of the same mistake `Conversation` had, on the load that runs the other way. Both are a packet sent from an address whose vpc does not own it, which the flow filter refuses as a source -- correctly, and looking exactly like a lost packet. `inward` named the peer's *public* range, so the outside host opening a connection to a forwarded service sent from an address it would only ever have after translation. `peer_of` answers "what do I dial"; `peer_source_of` answers "what does the far side send from", and they are the same address only when nothing translates. The distinction is the one `peer_of`'s own note already describes for a reply. The service then answered to the address the outside host used rather than the one the request arrived from, so a request that was translated on the way in was answered somewhere it was never contacted from. Neither was reachable while every peer asked these questions had nothing to translate. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The last flavour the configuration model has and the vocabulary did not. It is also the only one that puts ports in a generated configuration at all, so `VpcExpose.ips.ports` and `VpcExposeNat.as_range.ports` come off the blind list with it: two more rows, not one, and the census now records 9 unreachable rather than 11. Unlike static nat this needed a rule. `VpcPeering::validate` refuses masquerade or port forwarding opposite either of themselves -- both decide which way a connection may be opened, and a peering naming both directions would not say which translation a packet is owed. The algebra had half of that as "masquerade on the other side"; `Flavour::is_directional` is the whole of it, in one sentence that can be compared with the validator's. The two port ranges are equal width because the sides of a translation are one flat list of (address, port) pairs: unequal widths would stop the mapping being offset-preserving in the address, which is what a derived load reads it as. They hold different numbers so that confusing the two fails. The protocol stays `Any`, and the idle timeout absent. Each is a separate degree of freedom, and closing them alongside the flavour would leave none of the three measured on its own. `assert_covered` on inbound loads because this is the first flavour that produces one from a generated configuration: without it the property stays green while carrying none of the traffic the new flavour implies. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

An ACL is the one configuration object whose whole job is to change a verdict, which is what every property built on the algebra asserts over -- so a vocabulary without one left those properties stating their claims only about configurations that could never be told to refuse. The two shapes are coarse on purpose. A rule set a property has to evaluate in order to know what should have happened is a second copy of a decision procedure, and `acl_filter`'s own generator is the rich one. Config and dataplane together because they have to be: a denying guard makes traffic the derivation must stop offering, and either half alone leaves the suite red. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The survey stopped at `VpcPeering.acl`, so an ACL's rules, patterns and scope were unmeasured -- and a row reading "spans absent, present" would have been read as a vocabulary of ACLs rather than of one rule shape. The count of fixed degrees of freedom goes from 8 to 16 without the algebra losing any reach: the eight are holes that were always there and had nowhere to be reported. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

… packet The one shape whose replies are not permitted by a rule of their own, which is what reaches `AclFilter`'s reverse lookup and `reverse_summary` -- the only place an ACL verdict depends on what NAT did. It found a defect on its first run. A port-forwarded flow is stamped with a generation when it opens and nothing ever moves it off one; the generation upgrade lives in masquerade's allocator writer. So the first configuration change after such a connection opens denies its next reply, wherever in the configuration that change was. Pinned by `acl::a_port_forwarded_flow_loses_its_acl_permission_on_any_configuration_change` and deliberately not fixed here: which flows an allocator writer is responsible for is not a decision to make as a side effect of a test finding it. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

… rest Rule precedence was the last thing about an ACL that no generated configuration could say anything about: with at most one rule per direction, no packet ever matched two, so first-match order decided nothing. The excepted expose is a masquerading one, and that is what keeps the effect predictable without evaluating the ACL: nothing is ever aimed at a masquerading expose, so its prefix appears in the implied traffic only as the source of its own requests. Swapping the two overlapping rules fails `a_configuration_carries_nothing_it_denies`. `Named` gains the expose's position because a peering's answer is no longer one answer. The vary counter moves ahead of the filter as a consequence, which is a fix in its own right: two derivations under different filters now agree about every expose they both keep, and the footprint property takes two. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…eout Three degrees of freedom that were fixed for no reason beyond nothing having asked for them. Two are honest but partial, and the census rows say which part. A gateway group constrains only overlapping exposes, and the address plan gives every expose a block of its own, so the field varies while the rule that gives it meaning stays out of reach. An idle timeout is set far longer than any property here runs: a configuration naming one lowers and carries its traffic, and nothing ages out. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Three more degrees of freedom, and one of them buys a kind of evidence nothing else here has: `Guard::PermitByProtocol` is checked by a rule that must *not* fire. Drop the protocol on the way into the table, or lower it as a wildcard, and both generated-traffic properties fail. The destination narrowing is the mirror of the source one. A masquerading expose is never aimed at, so its private prefix is the source of its own requests and of nothing else; a port-forwarding expose never reaches, so its public prefix is the destination of the traffic aimed at it and of nothing else. Either way the prefix appears in exactly one place, which is what lets a narrowed rule be predicted without evaluating the ACL. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Port forwarding is the only flavour whose constructor takes a protocol, so it is the only one that can vary here. Cycled by slot rather than drawn, so a manifest holding several forwarded exposes holds several protocols -- a forwarding rule is keyed by `(source vpc, protocol)`, and exposes that agree on it are the ones whose keys can collide. An expose narrowed to tcp carries none of the traffic a configuration implies, every load of which is udp, so `Draft::carries` now answers for the expose as well as for the peering's ACL. A caller asking whether a configuration carries something should not have to know there were two ways for it not to. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

A middle slice rather than a half, because the point of an exclusion is that the effective set stops being one prefix: a matcher, an lpm table and `RangeBuilder` each have to handle two, and taking a half would leave one and prove nothing. Reached, not yet enforced. The derivation reads its addresses off the effective set, so nothing generated is aimed at an excluded address and a matcher ignoring exclusions would still carry every load. The census row says so. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The last expose flavour the configuration model has. Legal only on a peering whose two vpcs have no other, which is stronger than the model requires and is chosen so the algebra's preconditions stay local: a default route overlaps every other route its vpc sees, and overlapping routes must agree about their gateway group and must not both be default -- conditions on a neighbourhood, which a later `AddPeering` can change underneath a rule that held when it was drawn. `Op::reads` takes a draft now. Its note said the read sets happened to be determined by an operation's own arguments, that this was not a law, and that the argument should come back rather than an operation be contorted to fit; this is the flavour that made it not a law, and `independent_operations_commute` found it by reporting an `AddPeering` and a `SetFlavour` as independent when swapping them changed whether the peering could be made at all. The derivation now skips an expose narrowed to a protocol its traffic does not carry. Such an expose still *routes* its prefix and only declines to translate, so the traffic is delivered untranslated -- neither the delivery an inbound load checks for nor a refusal. Predicting a refusal is what the deny property caught. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Every other use of an exclusion here reaches only the shape of the prefix set it produces, because the derivation reads its addresses off the effective set and so never aims at a hole. A matcher that ignored exclusions passed all of it. The prediction has one exception, and it is not obvious: a manifest with a default expose advertises every destination, so an address it excludes is still reachable. The property skips those, and the census row now says the hole is under test rather than only its shape. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

daniel-noland force-pushed the pr/daniel-noland/model-checking branch from 8e14aad to 68de4de Compare August 26, 2026 17:30

daniel-noland force-pushed the pr/daniel-noland/config-algebra branch from 47b6176 to 9ef4a02 Compare August 26, 2026 17:30

daniel-noland force-pushed the pr/daniel-noland/model-checking branch from 68de4de to bcbd57a Compare August 26, 2026 19:36

daniel-noland force-pushed the pr/daniel-noland/config-algebra branch 2 times, most recently from 120d507 to f65f958 Compare August 26, 2026 20:41

daniel-noland force-pushed the pr/daniel-noland/model-checking branch 2 times, most recently from 8cd913c to be74286 Compare August 26, 2026 21:02

daniel-noland force-pushed the pr/daniel-noland/config-algebra branch 2 times, most recently from 25deec3 to a75a2b7 Compare August 26, 2026 21:13

daniel-noland force-pushed the pr/daniel-noland/model-checking branch from be74286 to 95dd658 Compare August 26, 2026 21:13

daniel-noland force-pushed the pr/daniel-noland/config-algebra branch from a75a2b7 to 70fd2e6 Compare August 26, 2026 21:25

daniel-noland force-pushed the pr/daniel-noland/model-checking branch 2 times, most recently from 6446c90 to e58b3d3 Compare August 27, 2026 01:29

daniel-noland force-pushed the pr/daniel-noland/config-algebra branch from 70fd2e6 to 2c7edca Compare August 27, 2026 01:29

daniel-noland force-pushed the pr/daniel-noland/model-checking branch from e58b3d3 to bc6dcbb Compare August 27, 2026 01:41

daniel-noland force-pushed the pr/daniel-noland/config-algebra branch from 2c7edca to 806e9de Compare August 27, 2026 01:41

daniel-noland force-pushed the pr/daniel-noland/model-checking branch from bc6dcbb to 829e3f8 Compare August 27, 2026 02:25

daniel-noland force-pushed the pr/daniel-noland/config-algebra branch from 806e9de to ee7a16a Compare August 27, 2026 02:25

daniel-noland force-pushed the pr/daniel-noland/model-checking branch from 829e3f8 to 40659a3 Compare August 27, 2026 04:38

daniel-noland force-pushed the pr/daniel-noland/config-algebra branch from ee7a16a to bf31000 Compare August 27, 2026 04:38

daniel-noland force-pushed the pr/daniel-noland/model-checking branch from 40659a3 to 3a81a5b Compare August 27, 2026 05:12

daniel-noland force-pushed the pr/daniel-noland/config-algebra branch 2 times, most recently from 9049415 to 9e27aed Compare August 27, 2026 06:30

daniel-noland force-pushed the pr/daniel-noland/model-checking branch 2 times, most recently from 93cb81d to 7295f75 Compare August 27, 2026 18:00

daniel-noland force-pushed the pr/daniel-noland/config-algebra branch from 9e27aed to b4be140 Compare August 27, 2026 18:00

daniel-noland force-pushed the pr/daniel-noland/model-checking branch from 7295f75 to bdaa96a Compare August 27, 2026 18:29

daniel-noland force-pushed the pr/daniel-noland/config-algebra branch from b4be140 to 64c7005 Compare August 27, 2026 18:29

daniel-noland force-pushed the pr/daniel-noland/model-checking branch from 92a66e6 to 80f15e5 Compare August 28, 2026 05:47

daniel-noland force-pushed the pr/daniel-noland/config-algebra branch from 4969a2f to 26e6361 Compare August 28, 2026 05:47

daniel-noland force-pushed the pr/daniel-noland/model-checking branch from 80f15e5 to 08540d3 Compare August 28, 2026 06:14

daniel-noland force-pushed the pr/daniel-noland/config-algebra branch from 26e6361 to 3ee9131 Compare August 28, 2026 06:18

daniel-noland force-pushed the pr/daniel-noland/model-checking branch from 08540d3 to 0f92aff Compare August 28, 2026 06:40

daniel-noland force-pushed the pr/daniel-noland/config-algebra branch from 3ee9131 to fcd1d11 Compare August 28, 2026 06:40

daniel-noland force-pushed the pr/daniel-noland/model-checking branch from 0f92aff to f1b4016 Compare August 28, 2026 07:08

daniel-noland force-pushed the pr/daniel-noland/config-algebra branch from fcd1d11 to b26928b Compare August 28, 2026 07:08

daniel-noland force-pushed the pr/daniel-noland/model-checking branch from f1b4016 to 3d615e7 Compare August 28, 2026 07:31

daniel-noland force-pushed the pr/daniel-noland/config-algebra branch from b26928b to 84d66cc Compare August 28, 2026 07:31

daniel-noland and others added 16 commits August 28, 2026 01:42

daniel-noland force-pushed the pr/daniel-noland/model-checking branch from 3d615e7 to 42579bb Compare August 28, 2026 07:43

daniel-noland force-pushed the pr/daniel-noland/config-algebra branch from 84d66cc to a842024 Compare August 28, 2026 07:43

daniel-noland force-pushed the pr/daniel-noland/model-checking branch from 42579bb to 76341eb Compare August 28, 2026 09:14

daniel-noland force-pushed the pr/daniel-noland/config-algebra branch from a842024 to c50fd96 Compare August 28, 2026 09:14

Navigation Menu

Uh oh!

config - #1763

config#1763
daniel-noland wants to merge 16 commits into
pr/daniel-noland/model-checkingfrom
pr/daniel-noland/config-algebra

daniel-noland commented Aug 26, 2026 •

edited

Loading

Uh oh!

coderabbitai Bot commented Aug 26, 2026

Draft PR not reviewed

Uh oh!

codecov Bot commented Aug 26, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

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

Uh oh!

Uh oh!

coderabbitai Bot commented Aug 26, 2026

Draft PR not reviewed

Uh oh!

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

Uh oh!

❌ 1 Tests Failed:

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

daniel-noland commented Aug 26, 2026 •

edited

Loading

codecov Bot commented Aug 26, 2026 •

edited

Loading