Skip to content

Commit 6afa20a

Browse files
levylevy
committed
udp: level 2 pass of the standards test workflow against RFC 768
Level 2 reached: both mandatory features (delivery, header) have core checks that ran and passed, and the ledger's mechanism inventory shows where every mechanism of the three-page document went. Level 4 is recorded as not applicable: UDP has no timer and no control loop. Spec side (free of INET names): - standard/rfc768/: the cached text and an 8-entry catalog that exhausts the document except for two unit-test items - standard/rfc792/catalog.md: one entry added, RFC792-DU-3 port unreachable; the catalog now states that it serves several protocols - protocol/udp/: the standards family (RFC 9868 of October 2025 updates RFC 768 with options, level 5; RFC 1122 par. 4.1 is level 3), 4 features, 3 checks - protocol/ipv4/features.md: the coverage sentence now follows the per-area rule, since the shared catalog grew by an entry that is UDP's Tests, tests/protocol/udp/: 3 tests, 3 PASS; the IPv4 suite of the same tree stays at 8 PASS. No expected-result FAIL. Two observations could not run and are recorded as bounds, not forced: no application can send an empty datagram (the packet library refuses a zero-length chunk), and the program-interface half of the receive operation is not observable. Model side: results with the model analysis, the coverage ledger with the achieved level, the conformance matrix (4 confirmed), the category decisions. Findings recorded, not acted on: - Udp.ned says "the RFC" twice and never names it; Udp.cc quotes RFC 768 verbatim at the all-ones rule; the only dated citation is in a dead BSD header and dates RFC 768 to September 1981 (it is August 1980) - checksumMode defaults to "declared", a placeholder; the checksum test sets computed on one sender and disabled on the other - in computed mode the receiver verifies every checksum and accepts a zero over IPv4 as RFC 768 says; the drop signal for a closed port carries a packet stripped of its protocol tag The RFC 792 catalog stays one copy for every protocol that uses it. On the rebase onto master, which now carries the IPv4 level 3 pass, two shared documents were merged: the catalog gained the note that its closed-port entry is a host report whose strength RFC 1122 raises where that document is in scope, and the IPv4 feature map now counts the RFC 792 entries that belong to IPv4 apart from the one that belongs to UDP.
1 parent 7e8b081 commit 6afa20a

15 files changed

Lines changed: 1655 additions & 14 deletions

File tree

‎doc/project/evidence/model/udp/categories.md‎

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
# UDP checks — category decisions
2+
3+
> **Kind:** decision · **Status:** current · **Seal:** none · **Owns:** — · **Stands on:** [results.md](results.md), [test-anatomy.md](../../../design/test-anatomy.md)
4+
5+
Step 9 artifact of the standards test workflow. For each check, this document records the
6+
test category and the reason. The categories and what each one can establish are
7+
[test-anatomy.md](../../../design/test-anatomy.md#the-categories); the mapping from
8+
observation class to category is in the guide, step 9. The category was predicted at step 3
9+
from the observation class of each statement, and confirmed after the run recorded in
10+
[`results.md`](results.md).
11+
12+
## Decisions for the three checks
13+
14+
### Datagram delivery (RFC768-HDR-1, HDR-2, HDR-3, PROTO-1, UI-1) → protocol test
15+
16+
The ports, the length and the IP protocol number are wire fields; the handoff to the
17+
program is an end-to-end observation at the receiver. The size of each datagram is the
18+
scenario's way to tell the two programs apart, which is a scenario property and not a code
19+
property.
20+
21+
### Checksum presence and absence (RFC768-CKSUM-2, CKSUM-1) → protocol test, with a unit test beside it
22+
23+
Presence and absence of the checksum are wire values; the acceptance of both kinds is
24+
end-to-end. Whether the nonzero value is the right one — RFC768-CKSUM-1, the one's
25+
complement sum over the pseudo header — is an encoding statement, and a serializer unit test
26+
in `tests/unit` is its home. The protocol test does not check the arithmetic.
27+
28+
### Port unreachable (RFC792-DU-3, RFC768-HDR-2) → protocol test
29+
30+
The discard at the receiver is an internal event with a packet signal, the report is an
31+
ordinary packet on link 1, and the absence of a handoff is an end-to-end observation. The
32+
`may` strength of the report is a matter for the ledger and the matrix, not for the
33+
category.
34+
35+
## Category guidance for the open catalog entries
36+
37+
| Entry | Likely category | Reason |
38+
| --- | --- | --- |
39+
| RFC768-CKSUM-1 | unit test | the checksum arithmetic is a serializer concern |
40+
| RFC768-IP-1 | unit test | the pseudo header is where the module's view of the IP addresses becomes visible; a serializer test computes it |
41+
| RFC 1122 §4.1.3.4, discard on a wrong checksum | protocol test with interception | needs a corrupted datagram in flight; level 3, and a document outside the in-scope set |
42+
43+
UDP has no timer and no control loop, so no entry points at a statistical test.

‎doc/project/evidence/model/udp/conformance.md‎

Lines changed: 103 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,103 @@
1+
# UDP — model claims and conformance matrix
2+
3+
> **Kind:** report · **Status:** snapshot 2026-09-08 · **Seal:** none · **Owns:** — · **Stands on:** [features.md](../../protocol/udp/features.md), [coverage.md](coverage.md), [standards.md](../../protocol/udp/standards.md)
4+
5+
Step 8 artifact of the standards test workflow. The tests tell what the model does. This
6+
document adds what the model says it intends to do, and compares the two at the level of
7+
features, never at the level of a single test.
8+
9+
- Claim scan: 2026-09-08, source identical to `master`.
10+
- Support values: [`coverage.md`](coverage.md#feature-support), from the run of 2026-09-08.
11+
12+
This is the one document of the workflow whose first part reads the model documentation on
13+
purpose. The claims must not travel back into the catalogs, the feature map, or the check
14+
descriptions.
15+
16+
## Part 1 — what the model claims
17+
18+
### The claim of the active module
19+
20+
| Source | Verbatim text | Kind |
21+
| --- | --- | --- |
22+
| [Udp.ned:14](../../../../../src/inet/transportlayer/udp/Udp.ned#L14) | "UDP protocol implementation, for IPv4 (~Ipv4) and IPv6 (~Ipv6)." | protocol claim, no document |
23+
| [Udp.ned:45](../../../../../src/inet/transportlayer/udp/Udp.ned#L45) | "the outgoing packet will have the correctly computed checksum as defined by the RFC" | a reference to "the RFC", no number |
24+
| [Udp.ned:54](../../../../../src/inet/transportlayer/udp/Udp.ned#L54) | "a potentially incorrect checksum that is to be verified as defined by the RFC" | the same |
25+
26+
The module says "the RFC" twice and never says which. For UDP the reader can guess, and the
27+
guess is right; the document does not say so.
28+
29+
### Document references elsewhere in the UDP tree
30+
31+
| Source | Verbatim text | Kind |
32+
| --- | --- | --- |
33+
| [Udp.cc:872](../../../../../src/inet/transportlayer/udp/Udp.cc#L872) | "// Excerpt from RFC 768:" followed by the two sentences of `rfc768.txt:92-95`, quoted verbatim | the strongest reference in the tree: the source text itself, at the line that implements it |
34+
| [headers/udphdr.h:43](../../../../../src/inet/transportlayer/udp/headers/udphdr.h#L43) | "Per RFC 768, September, 1981." | a citation on a BSD-derived header that nothing in `src/` includes; the date is wrong, RFC 768 is dated 28 August 1980 |
35+
| [Udp.cc:88-95](../../../../../src/inet/transportlayer/udp/Udp.cc#L88-L95) | a `TODO` that paraphrases the IPv6 rule "the UDP checksum is not optional" | a rule stated without its document |
36+
37+
RFC 1122 and RFC 8085 appear nowhere under `src/inet/transportlayer/udp/`.
38+
39+
### How this pass reads the claim
40+
41+
As for IPv4: "UDP protocol implementation" is an implicit claim on the Internet Standard
42+
for UDP, RFC 768, which has never been obsoleted. The verbatim excerpt in the code makes
43+
the reading firmer than it was for IPv4 — the model demonstrably works from that text — but
44+
an excerpt on one rule is not a statement of scope. The matrix marks the claim `implicit`.
45+
46+
## Part 2 — conformance matrix
47+
48+
The verdict combines the claim on the governing source document, the support value of the
49+
ledger, and the level of the feature, by the table of step 8.
50+
51+
| Feature | Level | Claimed | Support | Verdict |
52+
| --- | --- | --- | --- | --- |
53+
| UDP-F-DELIVERY | mandatory | yes (implicit, RFC 768) | supported | **confirmed** |
54+
| UDP-F-HEADER | mandatory | yes (implicit, RFC 768) | supported | **confirmed** |
55+
| UDP-F-CHECKSUM | optional | yes (implicit, RFC 768; the modes are documented "as defined by the RFC") | supported | **confirmed** |
56+
| UDP-F-PORT-UNREACHABLE | optional | yes (implicit, RFC 792 through the ICMP module) | supported | **confirmed** |
57+
58+
Four features `confirmed`. No `defect`, no `partial`, no `unverified`, no `undocumented`,
59+
no `declined`.
60+
61+
## Findings
62+
63+
### 1. The model states no document, one edit away from doing so
64+
65+
`Udp.ned` says "the RFC" and `Udp.cc` quotes RFC 768 by name at the line that implements
66+
its all-ones rule. The number that the module documentation lacks is already in the code.
67+
The only place that cites the document with a date is a dead header, and the date there is
68+
wrong. The house style is one module away
69+
([Igmpv2.ned:25-26](../../../../../src/inet/networklayer/ipv4/Igmpv2.ned#L25-L26)). A
70+
documentation task for the model, not for the tests.
71+
72+
### 2. The checksum: real only on request, verified always when real
73+
74+
Two observations from the code, recorded in
75+
[`results.md`](results.md#model-observations-the-checks-did-not-claim):
76+
77+
- The default `checksumMode` is `"declared"`, a placeholder. The checksum check sets the
78+
computed mode on one sender and the disabled mode on the other; both behaviors of
79+
RFC 768 are then observable, and both pass.
80+
- In the computed mode the receiver verifies every nonzero checksum and discards on failure
81+
([Udp.cc:948-956](../../../../../src/inet/transportlayer/udp/Udp.cc#L948-L956)), and it
82+
accepts a zero over IPv4 as "no checksum"
83+
([Udp.cc:1012-1017](../../../../../src/inet/transportlayer/udp/Udp.cc#L1012-L1017)). That
84+
is RFC 768 honored exactly, and RFC 1122's discard rule already in place for level 3. The
85+
contrast with the IPv4 header checksum, which the model consults only when the header is
86+
already structurally wrong, is worth a look by whoever owns both.
87+
88+
### 3. Nothing is contradicted at level 2
89+
90+
Within four features and seven statements, on one topology, the model does what RFC 768
91+
describes. UDP is the first protocol in this tree to reach level 2 with every feature
92+
`supported` and no `partial`; it is also the smallest, and the two observations that could
93+
not run — the empty datagram and the program-interface half of the receive operation — are
94+
limits of the tooling, not of the model.
95+
96+
## What this document does not establish
97+
98+
- It says nothing about RFC 1122's requirements on a UDP host, which change the level of
99+
the checksum feature, nor about the options of RFC 9868.
100+
- It says nothing about IPv6, where the checksum rules differ and the model has code paths
101+
this pass did not exercise.
102+
- A `confirmed` verdict means the checks of the feature passed. It does not mean the
103+
feature is complete.

‎doc/project/evidence/model/udp/coverage.md‎

Lines changed: 99 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,99 @@
1+
# UDP — coverage ledger
2+
3+
> **Kind:** ledger · **Status:** current · **Seal:** none · **Owns:** — · **Stands on:** [rfc768/catalog.md](../../standard/rfc768/catalog.md), [rfc792/catalog.md](../../standard/rfc792/catalog.md), [features.md](../../protocol/udp/features.md), [results.md](results.md)
4+
5+
The single place that holds the changing state of the UDP workflow. Every other artifact
6+
of this protocol states what a standard says and never changes again unless the standard
7+
changes. This one changes on every pass.
8+
9+
**No step edits an artifact of an earlier step. Steps 5, 6 and 7 record their outcome here.**
10+
11+
State of the ledger: run of 2026-09-08, on top of the IPv4 branch, source identical to
12+
`master`.
13+
14+
## Statement coverage
15+
16+
`Status` is the state of the workflow, not of the standard: `selected` (a check targets it),
17+
`covered` (a selected check establishes it as a side effect), `candidate` (practical, not yet
18+
chosen), `later` (needs a toolset beyond the current level, or another test category).
19+
20+
| Catalog ID | Status | Check section | Test file | Verdict |
21+
| --- | --- | --- | --- | --- |
22+
| [RFC768-HDR-1](../../standard/rfc768/catalog.md#rfc768-hdr-1) | covered | [datagram-delivery](../../protocol/udp/checks.md#datagram-delivery) | Rfc768DatagramDelivery.test | PASS |
23+
| [RFC768-HDR-2](../../standard/rfc768/catalog.md#rfc768-hdr-2) | selected | [datagram-delivery](../../protocol/udp/checks.md#datagram-delivery), [port-unreachable](../../protocol/udp/checks.md#port-unreachable) | Rfc768DatagramDelivery.test, Rfc768PortUnreachable.test | PASS |
24+
| [RFC768-HDR-3](../../standard/rfc768/catalog.md#rfc768-hdr-3) | selected | [datagram-delivery](../../protocol/udp/checks.md#datagram-delivery) | Rfc768DatagramDelivery.test | PASS; the minimum of eight not observed, no sender can produce an empty datagram |
25+
| [RFC768-CKSUM-1](../../standard/rfc768/catalog.md#rfc768-cksum-1) | later (unit test) | — | — | — |
26+
| [RFC768-CKSUM-2](../../standard/rfc768/catalog.md#rfc768-cksum-2) | selected | [checksum-presence-and-absence](../../protocol/udp/checks.md#checksum-presence-and-absence) | Rfc768Checksum.test | PASS |
27+
| [RFC768-UI-1](../../standard/rfc768/catalog.md#rfc768-ui-1) | selected | [datagram-delivery](../../protocol/udp/checks.md#datagram-delivery) | Rfc768DatagramDelivery.test | PASS; the data half. The source port and address at the program interface are not observable, and confirmed on the wire |
28+
| [RFC768-IP-1](../../standard/rfc768/catalog.md#rfc768-ip-1) | later (unit test) | — | — | — |
29+
| [RFC768-PROTO-1](../../standard/rfc768/catalog.md#rfc768-proto-1) | selected | [datagram-delivery](../../protocol/udp/checks.md#datagram-delivery) | Rfc768DatagramDelivery.test | PASS |
30+
| [RFC792-DU-3](../../standard/rfc792/catalog.md#rfc792-du-3) | selected | [port-unreachable](../../protocol/udp/checks.md#port-unreachable) | Rfc768PortUnreachable.test | PASS |
31+
32+
9 entries: 7 reached a test and passed; 2 are unit-test material and wait for that suite.
33+
34+
## Feature support
35+
36+
The rule of step 7: `supported` when every core check ran and passed, `partial` when a core
37+
check passed and another core check failed as a model gap or did not run, `not supported`
38+
when every core check that ran failed as a model gap, `untested` when no core check ran.
39+
40+
| Feature | Core checks and their state | Support |
41+
| --- | --- | --- |
42+
| [UDP-F-DELIVERY](../../protocol/udp/features.md#udp-f-delivery) | RFC768-HDR-2, PROTO-1, UI-1 all PASS | **supported** |
43+
| [UDP-F-HEADER](../../protocol/udp/features.md#udp-f-header) | RFC768-HDR-3 PASS | **supported** |
44+
| [UDP-F-CHECKSUM](../../protocol/udp/features.md#udp-f-checksum) | RFC768-CKSUM-2 PASS | **supported** |
45+
| [UDP-F-PORT-UNREACHABLE](../../protocol/udp/features.md#udp-f-port-unreachable) | RFC792-DU-3 PASS | **supported** |
46+
47+
All four features supported. Three bounds on that word:
48+
49+
1. `UDP-F-HEADER` rests on datagrams of 100 and 200 octets; the minimum length of eight was
50+
not observed, because no sender in the model can produce an empty datagram. Whether the
51+
receiver accepts one is a level 3 question, for injection.
52+
2. `UDP-F-CHECKSUM` rests on presence and absence, which is all RFC 768 lets a wire check
53+
establish. That a nonzero value is the right one is RFC768-CKSUM-1, unit-test material;
54+
the test sets the computed mode, so the observed value is a real checksum, but the wire
55+
assertion alone would accept the model's declared placeholder.
56+
3. `UDP-F-DELIVERY` confirms the source port and address on the wire, not at the program
57+
interface.
58+
59+
## Achieved level
60+
61+
**Level 2 reached.** Target: level 2, from
62+
[`standards.md`](../../protocol/udp/standards.md#target-level).
63+
64+
**Hold** — every normal-path mandatory mechanism of RFC 768 appears as a feature. The
65+
document is three pages, and the inventory is short:
66+
67+
| RFC 768 mechanism | Where | Feature, or the reason it is not one |
68+
| --- | --- | --- |
69+
| source port, optional | Fields | UDP-F-HEADER (supporting), UDP-F-DELIVERY |
70+
| destination port selects the receiver | Fields | UDP-F-DELIVERY |
71+
| length, minimum eight | Fields | UDP-F-HEADER |
72+
| checksum over a pseudo header; zero means none | Fields | UDP-F-CHECKSUM, level `optional` |
73+
| the user interface: ports, receive with source, send | User Interface | UDP-F-DELIVERY |
74+
| addresses and protocol from the IP header | IP Interface | UDP-F-DELIVERY (supporting; unit test) |
75+
| protocol 17 | Protocol Number | UDP-F-DELIVERY |
76+
| port unreachable report | RFC 792 | UDP-F-PORT-UNREACHABLE, level `optional` |
77+
| options in the surplus area | RFC 9868 | level 5; not in the in-scope set |
78+
79+
**Run** — every mandatory feature has a core check that ran and has a verdict: 2 of 2, all
80+
core checks PASS.
81+
82+
| Level | State | Evidence |
83+
| --- | --- | --- |
84+
| 1, Survey | **reached** | The standards map pins the in-scope set; [`conformance.md`](conformance.md) maps the model claim onto it and names what the claim lacks. |
85+
| 2, Core | **reached** | The inventory above; 7 of 7 level-2 statements with a PASS. |
86+
| 3, Edge | not started | RFC 1122 §4.1 is not in the in-scope set; the discard of a wrong checksum and the 8-octet datagram need interception and injection. |
87+
| 4, Dynamics | **not applicable** | UDP defines no timer and no control loop. |
88+
| 5, Complete | not started | RFC 9868 options; the two unit-test entries. |
89+
90+
## Pass log
91+
92+
| Pass | Date | Level | Scope | Result |
93+
| --- | --- | --- | --- | --- |
94+
| 1 | 2026-09-08 | **2, reached** | RFC 768 in scope with RFC 792's port unreachable; 9 catalog entries (8 new, 1 added to the shared RFC 792 catalog); 4 features; 3 checks; 3 tests | 3 PASS; 4 features supported; two observations not runnable, recorded; see [`results.md`](results.md) and [`conformance.md`](conformance.md) |
95+
96+
## Out of scope
97+
98+
The catalog records what this pass left out: the checksum arithmetic and the IP interface
99+
rule, both unit-test material; the options of RFC 9868; the RFC 1122 host requirements.

0 commit comments

Comments
 (0)