(09) pipeline - #1761
Draft
daniel-noland wants to merge 29 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/pipeline-harness
branch
from
August 26, 2026 17:30
8cb37c3 to
8027a81
Compare
daniel-noland
force-pushed
the
pr/daniel-noland/pipeline-harness
branch
2 times, most recently
from
August 26, 2026 20:41
cf9c73e to
fdb5ee2
Compare
daniel-noland
force-pushed
the
pr/daniel-noland/pipeline-harness
branch
from
August 26, 2026 21:02
fdb5ee2 to
70987f0
Compare
daniel-noland
force-pushed
the
pr/daniel-noland/pipeline-harness
branch
2 times, most recently
from
August 26, 2026 21:25
033504b to
f2eee32
Compare
daniel-noland
force-pushed
the
pr/daniel-noland/pipeline-harness
branch
from
August 27, 2026 01:29
f2eee32 to
d1f4f0d
Compare
daniel-noland
force-pushed
the
pr/daniel-noland/pipeline-harness
branch
2 times, most recently
from
August 27, 2026 02:25
b712bef to
66a7cd4
Compare
daniel-noland
force-pushed
the
pr/daniel-noland/pipeline-harness
branch
from
August 27, 2026 04:37
66a7cd4 to
67eba5b
Compare
daniel-noland
force-pushed
the
pr/daniel-noland/pipeline-harness
branch
2 times, most recently
from
August 27, 2026 06:30
0294067 to
11b3757
Compare
daniel-noland
force-pushed
the
pr/daniel-noland/pipeline-harness
branch
from
August 27, 2026 18:00
11b3757 to
7346f90
Compare
daniel-noland
force-pushed
the
pr/daniel-noland/pipeline-harness
branch
from
August 27, 2026 18:29
7346f90 to
fac79e0
Compare
daniel-noland
force-pushed
the
pr/daniel-noland/pipeline-harness
branch
2 times, most recently
from
August 28, 2026 02:19
1f1d323 to
86c8dca
Compare
The harness could not say anything about ACL correctness: its overlays carried no rules, so no verdict depended on the protocol, and the extension-header fix was not held by anything here. The generator is deliberately not `acl_filter`'s. That one is rich because ordering and lookup are its to check, and it has an evaluator to predict them; reusing the evaluator here would put a second copy of the decision procedure in the oracle. What this needs instead is a configuration whose answer is knowable without evaluating it -- one rule, all of the peering's traffic in one direction, discriminating only on protocol -- so `peering_acl` goes in `config`'s `contract` module next to the type, where the expose generators already are. The packet's protocol is known because the test built it, rather than read back through the accessor the filter uses. That accessor is the one that was wrong, and an oracle that asked it the same question could not have seen it. The claims are one-way. Asserting that a denied packet is dropped *by the ACL* fails on a generated ICMP error, which `IcmpErrorHandler` refuses before the ACL is consulted -- so the property carries a counter requiring that some denial actually came from the ACL. Without it, a pipeline that dropped everything early would satisfy the deny direction with the ACL removed entirely. 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> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Unblocks the underlay half of the dataplane pipeline harness, which could already construct `Ingress`, `IpForwarder` and `Egress` -- the readers they take are public -- but had no way to populate what those readers read. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The VLAN refusal in `IpForwarder` had no test. It now has two, at deliberately different depths: removing the guard fails only the shallower one, because the filters refuse a tagged shape as well, and an end-to-end property alone would have reported a defence that was no longer there. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Three limits had to move together, and two of them fail silently. bolero's driver zero-fills past its limit rather than erroring, so a batched generator that outgrew 4096 went on reporting cases whose tails were runs of defaults; libfuzzer's `-len_control` then kept inputs at 8 bytes on a target too slow to earn any length growth, which made raising the other two inert. Measured on `routed::a_tagged_shape_never_reaches_the_wire`: 13722 edges and 18655 features in 120s before, 14467 and 24247 in 60s after. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Workers are independent processes and the EAL targets already tolerate them -- `dpdk::test_support` gives each process its own file prefix and keeps the heap in memory -- so the limit is memory, not correctness. Measured at 1.8 GB a worker on the pipeline targets, which is what half rather than all is sized against. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`just test` replays whatever sits in `__fuzz__`, sharing one budget with the random phase, so every campaign made the next test run likelier to fail a coverage guard that was working correctly: 25 packets reached the wire with no corpus, 0 to 3 with 146 entries. Crashes stay where they were -- that replay is worth having and stays small. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The reply-side decapsulation had no test: the overlay slice stamps both directions' arrival by hand, so nothing exercised a reply arriving as a real tunnelled frame under the peer's vni. Building it turned up why that mattered. `round_trip`'s packet helper left the hop count at `Ipv4::default()`'s zero, which the slice cannot notice for want of a forwarding stage; every packet it built died at the first decrement here. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Two discriminations rather than one, because a single one could not say which claim this makes. Dropping `FlowLookup`'s flow attach fails it; turning masquerade's randomised port selection back on does not, which is what establishes that the table is being consulted rather than an allocator happening to be deterministic. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Every pipeline property so far ran against one peering, where "did this go to the right vpc" has one answer and cannot be got wrong. The oracle deliberately does not consult the peering table -- that is the flow filter's own decision procedure, and a filter reading the wrong table would be agreed with rather than caught. Peer n exposes 10.<n+1>.0.0/16 instead, so the answer is read off an address the test chose. Three peers rather than two because with two, an off-by-one and a swap are the same observation. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Every property so far sent one packet at a time, which is not how the pipeline runs: `FlowFilter::process` collects its whole input so it can pool classifications into batched rte_acl calls, so a burst puts every packet through `FlowLookup` before any reaches the nat stages. The members of a burst are distinct flows by construction. Two packets of one flow in one burst behave differently from the same two sent singly, and that difference is a defect rather than a licence -- see the note on the property. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`FlowFilter` collects the whole rx burst before anything downstream of it runs, so every packet of a burst carries a flow stamp taken before any of them was masqueraded. Reading only the stamp meant sixteen UDP packets of one flow in one burst took sixteen ports out of the pool and reached the far side as sixteen sources, and a TCP SYN with its first data segment in one burst had the data dropped as "TCP without SYN". Found by the pipeline harness, by probing the case its burst property excludes. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The routed harness only ever configured masquerade, so port forwarding -- the one direction here that starts outside the fabric -- had no end-to-end property. The mapping is offset-preserving, so the expected internal tuple is arithmetic on offsets the test chose rather than a lookup in the table the stage reads. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
A stage that changes nothing and asserts something is still a stage, so each contract is checked on every packet of every routed property rather than needing one of its own. What it buys over asserting at the end is attribution: a violation names the boundary. `inspect` rather than `filter_map`, and no collect, so a checkpoint structurally cannot modify a packet, drop one, or move the burst barrier that `FlowFilter` establishes. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
At 999 stages this sat within a few bytes per frame of overflowing a thread stack, so any new field on `PacketMeta` -- a production one as much as a test-only one -- aborted it, in a crate whose author had no reason to be thinking about packet metadata. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`burst::a_burst_of_one_flow_allocates_once` drives the case deliberately; this notices it in whatever traffic any property happens to generate, and names the boundary when it does. Today only that property produces the traffic, so it adds attribution rather than reach -- what it buys is that a future property is checked without its author thinking about allocation. `TestMeta` exists for this and nothing else: masquerade rewrites the source, so a flow key read after the stage describes the translated packet, and correlating the two sides needs packet identity. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Phrased as "changed" rather than "in the pool" because masquerade does not always rewrite the source: on the return path it restores the destination and leaves a source belonging to the far side, which is in no pool of ours, so the other phrasing fails correct replies. Reading the ranges from the configuration is not the allocator written twice -- choosing which address and port is its job, and this asks only that the answer be in a set the configuration named. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Two things already lean on this. `bolero` diagnoses by shrinking and replaying, so a pipeline that answered differently the second time would shrink towards nothing and report a case that does not fail. And it is what makes recording every case unnecessary: a failure can be re-run with as much instrumentation as it takes. Verified across processes too, by digesting a fixed scenario: 3525008ad91c215a four times. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Inline generate-and-judge works while there is one conversation at a time; it cannot be interleaved, because the loop producing packets would also have to be in the middle of judging them. Proven against the most demanding existing property rather than a new easy one, so that the trait's shape is decided by what is already needed. Both of that property's break tests still fail it, now carrying the conversation's history rather than a line number. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…sfied The first property here about superposition rather than about a stage, and it asserts nothing new: each conversation knows what it sent, so the joint claim is that every one of them was satisfied. A poll draws from several loads rather than one, because the shape that matters is a reply for one conversation sharing a burst with another's request -- and the harness counts how often that actually happened, since a schedule that never mixed would pass while testing what we already had. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
A request/response load can never offer a scheduler more than one packet, so a run of them is a run of singleton bursts however generous the schedule. A blast is what makes `take` mean anything, and what puts several packets of one flow into a burst alongside somebody else's traffic. The interleaving guards now count what each burst actually carried rather than what its poll named, which is the difference between a coverage guard and one that cannot fail. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Hand-aimed addresses work while the fixture is fixed and stop the moment it is not: a generated configuration exposes prefixes nobody wrote down, and traffic aimed by hand would miss every one of them. The derivation reads what a configuration offers, not what the dataplane should do with it; each load still judges only its own traffic. Counting derived loads per flavour rather than in total, because skipping an entire expose kind is the likeliest way for this to be quietly wrong. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Implements the operation algebra for the overlay, which the design note recorded as still unbuilt. The per-kind draw counters are load-bearing rather than decoration: they caught two separate ways the vocabulary went dead while every property stayed green. Both are written down where the mistake was made. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Closes the loop the config algebra was built for: the configuration, the traffic it implies, and the order that traffic runs in are now one draw. Three harness assumptions that a written fixture had been holding up failed here, one of them at about a run in ten. Each is a case where the configuration already knew the answer and the derivation had hard-coded it; the general form is in development/code/property-testing.md. 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>
…unting it `Load::checked` is documented as something a run may legitimately lack: a configuration that does not carry a load's traffic is not a defect. This property is where that does not apply. `loads_for` derives its loads from the validated overlay and skips any expose it cannot build traffic for, so every load it hands back is traffic the configuration says it carries -- and the property is named for exactly that claim. Counting them and requiring only `checked > 0` globally meant a regression confined to one vpc, expose type or direction passed as long as any other load anywhere completed, while `ABANDONED` climbed where nobody was reading. Signed-off-by: Daniel Noland <daniel@githedgehog.com>
The guard asked whether some *drawn* frame had been delivered, which is a random variable twice over: the configuration is drawn and so is the frame. Under coverage instrumentation the budget buys a couple of cases, and CI failed with `delivered=0 tagged=4` -- a run in which nothing was wrong and no draw happened to be deliverable. Aiming a built frame at the generated configuration does not fix it, because whether that frame is carried still depends on the exposes that were drawn; the filter refuses it as `Filtered`. So the control is `inner()` against the fixed fixture, which this module already documents as the thing its negative tests are only as good as. Signed-off-by: Daniel Noland <daniel@githedgehog.com>
The `concurrency::sync` facade is what swaps in loom and shuttle equivalents under the model-checker features, and opengrep gates on it -- so these were failing `lint` outright. It is not only a lint here. `packet_processor::fuzz` holds properties that run under `concurrency::model_test`, and a `LazyLock` or an atomic the model checker cannot see is a scheduling point it will not explore. Signed-off-by: Daniel Noland <daniel@githedgehog.com>
daniel-noland
force-pushed
the
pr/daniel-noland/pipeline-harness
branch
from
September 3, 2026 07:02
49f683d to
a61bedd
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.