(11) config - #1763
Open
daniel-noland wants to merge 44 commits into
Open
(11) config#1763daniel-noland wants to merge 44 commits into
daniel-noland wants to merge 44 commits into
Conversation
|
Important Review skippedAuto reviews are disabled on base/target branches other than the default branch. Please check the settings in the CodeRabbit UI or the ⚙️ Run configurationConfiguration used: Organization UI Review profile: CHILL Plan: Essentials Run ID: You can disable this status message by setting the Use the checkbox below for a quick retry:
Comment |
Codecov Report❌ Patch coverage is 📢 Thoughts on this report? Let us know! |
daniel-noland
force-pushed
the
pr/daniel-noland/model-checking
branch
from
August 26, 2026 17:30
8e14aad to
68de4de
Compare
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/model-checking
branch
from
August 26, 2026 19:36
68de4de to
bcbd57a
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/model-checking
branch
2 times, most recently
from
August 26, 2026 21:02
8cd913c to
be74286
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/model-checking
branch
from
August 26, 2026 21:13
be74286 to
95dd658
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/model-checking
branch
2 times, most recently
from
August 27, 2026 01:29
6446c90 to
e58b3d3
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/model-checking
branch
from
August 27, 2026 01:41
e58b3d3 to
bc6dcbb
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/model-checking
branch
from
August 27, 2026 02:25
bc6dcbb to
829e3f8
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/model-checking
branch
from
August 27, 2026 04:38
829e3f8 to
40659a3
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/model-checking
branch
from
August 27, 2026 05:12
40659a3 to
3a81a5b
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/model-checking
branch
2 times, most recently
from
August 27, 2026 18:00
93cb81d to
7295f75
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/model-checking
branch
from
August 27, 2026 18:29
7295f75 to
bdaa96a
Compare
daniel-noland
force-pushed
the
pr/daniel-noland/config-algebra
branch
from
August 27, 2026 18:29
b4be140 to
64c7005
Compare
Comparing generated overlays with arbitrary real configurations would report zero reachability because the algebra derives addresses from its handles. Survey schema degrees of freedom instead, using exhaustive destructuring to catch new unclassified fields and counters for actual draws. Report results only after the full sample count; shorter emulated runs state their size and make no coverage claim. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: Codex <codex@openai.com>
Config-apply tests need a frame condition: traffic outside the changed operation's footprint must continue unaffected. Split a generated sequence at its last operation, derive untouched loads from its read/write footprint, and assert stable re-enactment after the initial race. Also propagate worker panics through barriers and advance genids so the harness cannot hang or manufacture stale-config behavior. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: Codex <codex@openai.com>
Fleet always told the NAT allocator it was on generation one and never published a generation to pipeline stages. That made flow revalidation unreachable and caused repeated enactments to model the wrong configuration lifecycle. Publish allocator and stage generations in management order, enact one component at a time, and separate worker tuples with disjoint port ranges. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: Codex <codex@openai.com>
unsafe-allow-abi-mismatch disabled rustc's protection against linking crates built with different sanitizer flags, although build-std already instruments the full sysroot consistently. A stale sysroot could therefore produce a green but meaningless fuzz run. Restore the compiler check, stamp each sysroot with its sanitizer, and make just fuzz reject disagreement. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: Codex <codex@openai.com>
A short burst ended before a full configuration apply reached the masquerade allocator because rebuilding rte_acl took about a millisecond. The instrument then measured timing rather than impact and made the full apply look far safer than the allocator step. Keep traffic running across the entire update window and include the router-configuration gap used by management. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: Codex <codex@openai.com>
The enactment instrument found an allocator swap assigning one public tuple to two live flows, allowing a reply to reach the wrong tenant conversation. The harness's deterministic allocation was a possible artifact. Exercise both deterministic and randomized allocators, priming the randomized case before the swap, and confirm the transient belongs to the dataplane update. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: Codex <codex@openai.com>
Some model-checked properties synchronized workers with std::sync::Barrier, making those ordering points invisible to Loom and Shuttle. Route modeled barriers and related primitives through the concurrency facade. Keep direct standard synchronization only for process-global registries and diagnostic instruments, where modeled primitives are invalid or would perturb the schedule, with explicit lint suppressions. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-authored-by: Codex <codex@openai.com>
main grew a `no_multipath` field on `VpcPeering`, and the census destructures the type exhaustively so that exactly this cannot pass unnoticed: the build failed with E0027 until someone classified the new degree of freedom. That is the census working, not a rebase casualty to paper over. It is `Fixed(false)`. Every `VpcPeering` constructor sets it false and no operation flips it; the only writer is the k8s converter, from `GatewayAgentPeerings::no_multi_path`. So no generated configuration disables multipath, and any property about stateless peering is currently unreachable from the algebra. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: Codex <codex@openai.com>
`LazyLock` and `AtomicU64` were imported at file scope but referenced only inside `concurrency::with_std!`; the `loom` and `shuttle` arms build their statics from `std::sync::atomic` directly. So the imports were dead in exactly the two builds the block exists to serve, and warned there. Verified: no unused-import warnings under `--features shuttle`. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: Codex <codex@openai.com>
The rationale for `OnceLock` over a `static` initializer stopped at "would fail to typecheck on those", followed by two empty doc lines -- losing the half that says what `OnceLock` does about it. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: Codex <codex@openai.com>
…therwise The sanitizer guard only ran when `DATAPLANE_SYSROOT` was set *and* its `.sanitize` stamp was readable. With no stamp there is nothing to compare, so the check simply did not run and a request for instrumentation quietly got a sysroot that may carry none -- the exact failure the guard exists to prevent. Refuse in that case, but only when a sanitizer was actually asked for: the default `sanitize` is the empty string and `NONE` is an explicit opt-out, and neither has anything to be wrong about. Verified all three paths: default does not refuse, `sanitize=address` without a stamp refuses, `sanitize=NONE` does not. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: Codex <codex@openai.com>
Bring the applicable concurrency and race changes from #1805 into #1762: the Shuttle-aware left-right fork and feature wiring, process-global bookkeeping, the flow-table count, generation staging, port-forwarded flow migration and arbitration, and masquerade reverse-tuple protection. Carry their regression tests and sanitizer coverage guards with them. Adapt the changes to the current harness and retain native test coverage. Keep six pipeline tests excluded under Shuttle because DashMap's native shard locks can block its scheduler. The pipeline smoke test reproduces the same futex wait and needs that exclusion on this version of the tree. Use the process-global ACL registry mutex with an explicit lint exception under the model backends. Later clock, profile-rename, and VM-specific changes remain in #1805. Validation: 27 workspace Shuttle tests; 354 ordinary tests across the affected dataplane, NAT, flow-entry, pipeline, and ACL-filter packages; Clippy on both backends with -D warnings; workspace all-targets Loom check; formatting; feature resolution; Nix sanitizer flag evaluation. Signed-off-by: Daniel Noland <daniel@githedgehog.com>
A missing driver symlink means a NIC is unbound, which is valid when its kernel module was never loaded or it was already detached. Treating that as an error made BindToVfioPci refuse the device before its override-and-bind path. Continue binding unclaimed NICs, recognize e1000 and e1000e, and link the matching DPDK PMD for QEMU and bare-metal hosts. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Conversation replied from the address a sender dialed instead of the address that arrived after NAT. Those differ when an expose both translates and accepts connections, making the far side send from an address it does not own and causing a misleading flow-filter drop. Build replies from the delivered packet so the existing oracle genuinely checks reverse translation. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Static NAT rewrites a destination before masquerade, so the packet's current key differs from the initial key where FlowLookup filed its forward flow. The intra-burst fallback searched only the rewritten key and allocated a new public tuple for every packet. Keep the current-key lookup first for replies, then retry the original key on a miss and cover the combined translation. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The operation algebra could not produce static NAT, leaving two schema degrees unreachable and making the config-apply StaticNat step store only empty tables. Add the missing expose flavour using the algebra's disjoint private and public address blocks, and update the completeness census. Mixed static NAT and masquerade configurations now reach their shared pipeline path. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Inbound loads used a peer's public translation range as the sender address and answered to the dialed address rather than the request's delivered source. Both values happened to agree before translated inbound exposes were generated; afterward the flow filter correctly rejected them as unowned. Separate dial destinations from peer source addresses and reply to the observed sender. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Port forwarding was the last missing translated expose flavour and the only source of generated port ranges, leaving several configuration fields untested. Add equal-width but distinct public and private ranges, forbid conflicting directional translations on the opposite side, and require evidence that inbound loads exercise the new flavour. Leave protocol and timeout variation to separate changes. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Every generated peering permitted all traffic, so pipeline properties never exercised a configuration intended to deny a packet. Add coarse ACL shapes whose verdicts remain predictable without copying the production evaluator. Update traffic derivation to omit denied loads and retain guards proving ACL decisions are actually reached. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The completeness survey stopped at whether a peering had an ACL, hiding fixed rule, pattern, and scope fields behind a single present value. Extend the census through the entire ACL schema. This reports eight pre-existing fixed degrees of freedom without claiming the algebra gained new reach. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Packet-level ACL rules never exercise reverse-flow permission, where the verdict depends on NAT state. Generate permit-by-flow peerings and verify their replies through AclFilter's reverse lookup. The first run exposes and pins a separate defect: port-forwarded flows retain generation one and lose permission after any configuration change. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
With at most one rule per direction, generated ACLs could not make precedence affect a verdict. Add two predictable overlapping rules that partition a peering around one masquerade expose; reversing them now breaks the denial property. Track the named expose position and assign traffic variation before filtering so independent derivations remain comparable. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Gateway-group names, ACL logging, and idle timeouts remained fixed solely because the algebra never selected them. Vary all three and update the census. Record the current limits: disjoint exposes do not exercise gateway grouping semantics, and generated timeouts outlast these properties, so the fields lower successfully without testing expiration. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Generated ACLs still left protocol, port, and destination matching fixed, so dropping a field or lowering it as a wildcard could pass. Add predictable narrow rules whose target prefixes appear in exactly one traffic role, avoiding a duplicate ACL evaluator. Include a protocol guard that must not fire so both omission and wildcarding become observable. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Every generated port-forwarding expose accepted any protocol, leaving its protocol key and collision behavior untested. Cycle protocols across expose slots so one manifest can contain several. Because derived traffic is UDP, exclude TCP-only exposes from offered loads and make Draft::carries account for both expose protocol and peering ACL. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Generated exposes had no exclusions, so matchers, LPM tables, and RangeBuilder saw only contiguous prefixes. Remove a middle slice rather than one half, forcing the effective set into two ranges. This change measures reach and shape only; traffic derivation still selects from the effective set and therefore does not yet test the excluded hole. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The algebra could not express default-route exposes. Default routes overlap every neighboring route, so their validity depends on more than the operation's own arguments. Restrict them to otherwise empty peerings and let Op::reads inspect the draft, keeping applicability local and restoring the independence property. Skip loads whose expose protocol cannot carry their traffic. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Existing exclusion coverage drew traffic only from the effective address set, so a matcher that ignored every exclusion still passed. Aim packets directly at excluded addresses and require them to be unreachable. Exempt a manifest with a default expose because its default route legitimately covers the hole, and mark the census row as behaviorally enforced. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…t names The `-except` denial inherited `src_any_ports`/`dst_any_ports` = `[1..65535]` from the `rule` closure and only narrowed `pattern.src`/`dst`. Those ranges mean "any address within the peering, restricted to these ports", and `AclRule::validate_patterns_coverage` materializes them back into `src`/`dst`, so the narrowing was undone: the rule denied *all TCP across the peering* rather than the one prefix it was built to except. `PermitExcept` carries empty vectors already, so only the protocol-narrowed guard was affected -- and it was invisible because every derived load is UDP, so no property ever sent traffic the broken denial could match. It also contradicted the `AclPattern.src`/`dst` rows in the completeness census, which record the exception as address-scoped. Clear the matching `*_any_ports` when narrowing, and assert it over generated configurations: a `-except` denial that names a prefix on a side must not also carry any-ports on that side. Break-tested by restoring the old two lines -- `every_sequence_builds_a_valid_configuration` fails with the prefix and the ranges that undo it. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.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
2 participants
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.
todo:
The last commit needs cleanup. And a few lines of comments need trimmed.
I will push trivial fixes once (08)-(10) land. Till then this is ready for review