(11) config - #1763
Draft
daniel-noland wants to merge 16 commits into
Draft
Conversation
|
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 |
Codecov Report❌ Patch coverage is 📢 Thoughts on this report? Let us know! |
daniel-noland
force-pushed
the
pr/daniel-noland/config-algebra
branch
from
August 26, 2026 17:30
47b6176 to
9ef4a02
Compare
daniel-noland
force-pushed
the
pr/daniel-noland/config-algebra
branch
2 times, most recently
from
August 26, 2026 20:41
120d507 to
f65f958
Compare
daniel-noland
force-pushed
the
pr/daniel-noland/config-algebra
branch
2 times, most recently
from
August 26, 2026 21:13
25deec3 to
a75a2b7
Compare
daniel-noland
force-pushed
the
pr/daniel-noland/config-algebra
branch
from
August 26, 2026 21:25
a75a2b7 to
70fd2e6
Compare
daniel-noland
force-pushed
the
pr/daniel-noland/config-algebra
branch
from
August 27, 2026 01:29
70fd2e6 to
2c7edca
Compare
daniel-noland
force-pushed
the
pr/daniel-noland/config-algebra
branch
from
August 27, 2026 01:41
2c7edca to
806e9de
Compare
daniel-noland
force-pushed
the
pr/daniel-noland/config-algebra
branch
from
August 27, 2026 02:25
806e9de to
ee7a16a
Compare
daniel-noland
force-pushed
the
pr/daniel-noland/config-algebra
branch
from
August 27, 2026 04:38
ee7a16a to
bf31000
Compare
daniel-noland
force-pushed
the
pr/daniel-noland/config-algebra
branch
2 times, most recently
from
August 27, 2026 06:30
9049415 to
9e27aed
Compare
daniel-noland
force-pushed
the
pr/daniel-noland/config-algebra
branch
from
August 27, 2026 18:00
9e27aed to
b4be140
Compare
daniel-noland
force-pushed
the
pr/daniel-noland/config-algebra
branch
from
August 27, 2026 18:29
b4be140 to
64c7005
Compare
daniel-noland
force-pushed
the
pr/daniel-noland/config-algebra
branch
from
August 28, 2026 17:16
c50fd96 to
ccbfc9c
Compare
daniel-noland
force-pushed
the
pr/daniel-noland/config-algebra
branch
from
August 28, 2026 17:33
ccbfc9c to
33377c4
Compare
daniel-noland
force-pushed
the
pr/daniel-noland/config-algebra
branch
from
September 1, 2026 17:41
33377c4 to
27c49c1
Compare
daniel-noland
force-pushed
the
pr/daniel-noland/config-algebra
branch
from
September 3, 2026 00:21
27c49c1 to
20ff6f8
Compare
daniel-noland
force-pushed
the
pr/daniel-noland/config-algebra
branch
from
September 3, 2026 05:53
20ff6f8 to
a564e33
Compare
daniel-noland
force-pushed
the
pr/daniel-noland/config-algebra
branch
from
September 3, 2026 05:59
a564e33 to
444884b
Compare
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>
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.