Skip to content

(04) spec - #1799

Draft
daniel-noland wants to merge 21 commits into
pr/daniel-noland/clock-facadefrom
pr/daniel-noland/spec-compliance
Draft

(04) spec#1799
daniel-noland wants to merge 21 commits into
pr/daniel-noland/clock-facadefrom
pr/daniel-noland/spec-compliance

Conversation

@daniel-noland

Copy link
Copy Markdown
Collaborator

No description provided.

@coderabbitai

coderabbitai Bot commented Sep 3, 2026

Copy link
Copy Markdown

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.

@daniel-noland
daniel-noland force-pushed the pr/daniel-noland/spec-compliance branch from 305015f to c862a15 Compare September 3, 2026 05:53
@daniel-noland
daniel-noland force-pushed the pr/daniel-noland/clock-facade branch 2 times, most recently from cd223db to 695d16e Compare September 3, 2026 05:59
@daniel-noland
daniel-noland force-pushed the pr/daniel-noland/spec-compliance branch from c862a15 to 082262c Compare September 3, 2026 05:59
@codecov

codecov Bot commented Sep 3, 2026

Copy link
Copy Markdown

@daniel-noland
daniel-noland force-pushed the pr/daniel-noland/clock-facade branch from 695d16e to e3b65c1 Compare September 3, 2026 06:22
@daniel-noland
daniel-noland force-pushed the pr/daniel-noland/spec-compliance branch 2 times, most recently from a7ced5c to b5ae651 Compare September 3, 2026 07:02

use tracing::{error, warn};

//================================= Common ==========================//

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Are these comments going away because the comment style conflicts with duvet syntax?

@daniel-noland
daniel-noland force-pushed the pr/daniel-noland/spec-compliance branch from b5ae651 to 5035d76 Compare September 3, 2026 20:06
@daniel-noland
daniel-noland force-pushed the pr/daniel-noland/clock-facade branch 2 times, most recently from 1887ca0 to f3b2a1c Compare September 3, 2026 20:32
@daniel-noland
daniel-noland force-pushed the pr/daniel-noland/spec-compliance branch 2 times, most recently from 228b5d5 to df2eaad Compare September 3, 2026 23:04
@daniel-noland
daniel-noland force-pushed the pr/daniel-noland/clock-facade branch from f3b2a1c to 1ad13aa Compare September 3, 2026 23:04
@daniel-noland
daniel-noland force-pushed the pr/daniel-noland/spec-compliance branch from df2eaad to c0074fe Compare September 6, 2026 04:39
@daniel-noland
daniel-noland force-pushed the pr/daniel-noland/clock-facade branch 2 times, most recently from 180c6e0 to f4731dc Compare September 6, 2026 06:15
@daniel-noland
daniel-noland force-pushed the pr/daniel-noland/spec-compliance branch 2 times, most recently from a9f77a5 to 65bb86f Compare September 6, 2026 18:30
@daniel-noland
daniel-noland force-pushed the pr/daniel-noland/clock-facade branch from f4731dc to 15fe5eb Compare September 6, 2026 18:30
@daniel-noland
daniel-noland force-pushed the pr/daniel-noland/spec-compliance branch from 65bb86f to b1c26f8 Compare September 6, 2026 19:05
@daniel-noland
daniel-noland force-pushed the pr/daniel-noland/clock-facade branch 2 times, most recently from 60d94b2 to aee8206 Compare September 6, 2026 19:31
@daniel-noland
daniel-noland force-pushed the pr/daniel-noland/spec-compliance branch 3 times, most recently from 1977982 to ab37ed4 Compare September 6, 2026 21:27
@daniel-noland
daniel-noland force-pushed the pr/daniel-noland/clock-facade branch from aee8206 to 7686872 Compare September 8, 2026 02:49
@daniel-noland
daniel-noland force-pushed the pr/daniel-noland/spec-compliance branch from ab37ed4 to 2607954 Compare September 8, 2026 02:49
@daniel-noland daniel-noland self-assigned this Sep 8, 2026
@daniel-noland
daniel-noland force-pushed the pr/daniel-noland/clock-facade branch from 7686872 to 34a0918 Compare September 8, 2026 06:58
@daniel-noland
daniel-noland force-pushed the pr/daniel-noland/spec-compliance branch from 2607954 to 17f6be7 Compare September 8, 2026 06:58
@daniel-noland
daniel-noland force-pushed the pr/daniel-noland/clock-facade branch from 34a0918 to a021558 Compare September 8, 2026 07:04
@daniel-noland
daniel-noland force-pushed the pr/daniel-noland/spec-compliance branch from 17f6be7 to 3fb4be4 Compare September 8, 2026 07:04
@daniel-noland
daniel-noland force-pushed the pr/daniel-noland/clock-facade branch from a021558 to 0417969 Compare September 9, 2026 00:12
daniel-noland and others added 21 commits September 8, 2026 23:16
`check_full_payload` treated octet lengths as bits. It rejected seven of
every eight valid aligned lengths while accepting original-datagram fields
shorter than RFC 4884's 128-octet minimum. Its padding limit was also not
required by the RFC.

Require the field to be at least 128 octets, fit within the buffer, and
contain only zero padding after the embedded datagram. Remove the incorrect
alignment and padding-size checks and cite each remaining requirement.

Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Source citations could disagree with RFC 4884 without exposing missing
implementations or tests. Duvet also cannot fetch specifications inside
the build sandbox.

Add RFC 4884 to the Duvet configuration, vendor its text, and commit the
compliance snapshot. Scan every workspace crate, and adjust routing banner
comments that Duvet misread as citations. The report now exposes the
untested ICMPv6 padding requirement without requiring network access.

Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Masquerade's TCP behavior had no recorded relationship to RFC 5382, leaving
conformance and deliberate product choices indistinguishable.

Track and vendor RFC 5382. Cite the existing no-port-overloading and
non-terminating ICMP behavior as implemented and tested. Record the short
idle timeouts and endpoint-dependent mapping as unresolved decisions
rather than accepted exceptions, so the compliance report keeps them
visible.

Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
UDP masquerade behavior had not been checked against RFC 4787, hiding
material gaps in mapping lifetime, filtering, fragmentation, and
hairpinning.

Track and vendor RFC 4787, reusing overlapping TCP citations where the
requirements agree. Record the short UDP mapping timeout, missing hairpin
and fragmentation behavior, and well-known-port policy in the compliance
snapshot. Keep undecided behavior as TODOs and the deliberate port policy
as an exception.

Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
RFC 4787 endpoint-independent mapping had no stage-level test. Changing
only the destination port produced a different public port, proving the
current mapping is address-and-port dependent and does not satisfy REQ-1.

Add a configuration-driven property for the part that does hold: one
internal endpoint keeps the same public address across destinations, as
required by paired address pooling in REQ-2. Leave REQ-1 visible as an
unresolved compliance gap.

Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Existing expiry coverage tested inbound refresh, which RFC 4787 permits,
but not the required outbound refresh. Generated evidence showed that an
unanswered one-way mapping expired from its first packet even while
outbound traffic continued.

Verify outbound refresh for established mappings and record the one-way
failure as a TODO rather than pinning nonconforming behavior. The test
advances close to each deadline so deleting refresh cannot pass
accidentally.

Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Masquerade's filtering and address-pooling behavior under load were not
classified against RFC 4787. That left security behavior and conditional
compliance requirements undocumented.

Probe replies from the original endpoint, a different port, and a
different address. The stage uses address-and-port-dependent filtering,
stricter than either REQ-8 option, so retain it as an unresolved decision.
Add a positive control and an ignored exhaustion probe showing paired
address pooling remains stable under contention.

Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Separate implementation and test citations can drift while both still
appear current. RFC 4787 REQ-12 and RFC 5382 REQ-10 already described the
same state transition but were checked independently.

Define one `Req12` predicate, call it from a debug assertion in the state
machine, and invoke it from the exhaustive protocol test. A violating
transition now fails at the implementation boundary with both states
identified.

Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Nothing tied a runtime contract's specification and requirement ID to the
vendored Duvet data. A renamed or removed requirement could leave the code
claiming a stale contract without failing the build.

Introduce a common `Requirement` trait with constant specification and ID
values, validate them against Duvet's extracted requirements at compile
time, and replace string violations with typed requirement errors.

Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The dataplane has no egress MTU and does not originate ICMP errors. It
therefore cannot satisfy RFC 4787 REQ-13 for oversized packets, its DF-bit
variant, or the related TTL-expiry behavior.

Cite the requirement at VXLAN encapsulation, where packet size grows, and
record these clauses as one unresolved architectural gap: originating ICMP
errors requires an egress MTU first.

Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The committed Duvet snapshot was already stale after adding the REQ-12 and
REQ-13 citations, so the new regression gate failed. Regenerate the
snapshot from the current citations.

Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The RFC 4884 citation claimed a 128-octet minimum, but tests checked only
rejection at 124 octets for IPv4. An incorrect `<= 128` check still passed,
and the separate IPv6 implementation had no coverage.

Test both sides of the 128-octet boundary for ICMPv4 and ICMPv6. The
specification interlock now kills the surviving boundary mutations.

Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
RFC port-overloading citations sat on a forwarding wrapper whose mutations
were all unviable. The specification interlock could not break the claimed
behavior, making those citations decorative.

Move the citations to the allocation bitmap that enforces uniqueness.
Mutation testing now reveals the remaining second-half bitmap path that
the current property does not exhaust.

Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The stage-level no-port-overloading property draws too few ports to reach
the allocator's second bitmap half. Its citation alone left the actual
port-marking operation outside the specification interlock.

Cite the existing region-exhaustion test alongside the stage property.
The combined coverage now kills nine of the ten relevant allocator
mutations, including removal of the used-port mark.

Signed-off-by: Daniel Noland <daniel@githedgehog.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The committed compliance snapshot could drift without a required check,
while the mutation-based specification interlock is too slow for normal
CI.

Gate development CI on the deterministic Duvet snapshot and print its
summary tables in the job output.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
`payload_length` expects an ICMP header but received the full Ethernet
frame. Full-payload detection therefore read the last byte of the
destination MAC as the RFC 4884 length attribute for supported ICMP error
types.

Slice the parsed ICMP header before embedded-header consumption and read
the attribute with bounds checking so malformed packets cannot panic the
dataplane.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: Daniel Noland <daniel@githedgehog.com>
RFC 4884 permits extension structures on ICMPv6 Destination Unreachable
and Time Exceeded messages only. Treating Parameter Problem the same way
read the high byte of its 32-bit pointer as a length attribute.

Remove ICMPv6 Parameter Problem from extension-capable messages and cite
the address-family-specific requirement beside the classification.

Signed-off-by: Daniel Noland <daniel@githedgehog.com>
`a_large_answer_arrives_whole` announced 8,000 routes with a request and
reply per route. Loaded debug runners could time out during setup before
exercising response reassembly.

Reduce the fixture to 256 routes. The response still spans fourteen chunks
and covers reassembly and continuation flags with one thirty-second of the
setup work.

Signed-off-by: Daniel Noland <daniel@githedgehog.com>
One-way UDP and ICMP mappings expired five seconds after their first packet
even when outbound traffic continued. Rebuilding could reuse the same tuple
and hide the loss until a later inbound packet, violating RFC 4787 REQ-6.

Refresh one-way UDP and ICMP mappings from their latest outbound packet.
Keep TCP SYN retransmissions on the existing short lifetime, and leave the
separate RFC minimum-timeout decision unchanged.

Signed-off-by: Daniel Noland <daniel@githedgehog.com>
RFC 4884 lengths are offsets from the start of the quoted datagram, but
`check_full_payload` received a slice beginning after its embedded headers.
Padding checks could read into following data, and no-extension packets
compared incompatible lengths.

Pass the complete quoted-datagram slice used by embedded-header parsing and
add a frame-level test that exercises the production call site.

Signed-off-by: Daniel Noland <daniel@githedgehog.com>
`validate_ruleset` always succeeded. Conflicting rules were rejected only
during absorption, where they were logged and dropped while the writer
reported a successful update with an incomplete table.

Dry-run the complete incoming ruleset through the same insertion logic
before updating the live table. Test both direct dry-run rejection and the
writer path so validation cannot become disconnected from installation.

Signed-off-by: Daniel Noland <daniel@githedgehog.com>
@daniel-noland
daniel-noland force-pushed the pr/daniel-noland/spec-compliance branch from 3fb4be4 to 260d489 Compare September 9, 2026 05:16
@daniel-noland daniel-noland added the ci:+merge-ready Run all checks which will be run in the merge queue regardless of label status label Sep 9, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ci:+merge-ready Run all checks which will be run in the merge queue regardless of label status

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants