Partial

RFC 2516 - A Method for Transmitting PPP Over Ethernet (PPPoE)

Every requirement this repository extracted from RFC 2516, the tests bound to it, and what a reader has verified about them. This summary is enrolled and gated by ./le rfc check.

Overview

Positive

what Ze has

Tested both ways70.3%26 of 37 gated MUSTs

a positive test proves Ze does what the requirement demands and a negative one proves it refuses what the requirement forbids

One polarity plus reason16.2%6 of 37 gated MUSTs

the requirement admits no counter-case, so one polarity plus a recorded reason is the whole proof available for it

One polarity, unexcused0.0%0 of 37 gated MUSTs

one direction is tested, the other is neither tested nor excused, and nothing states which

Partial proof; remaining gap0.0%0 of 37 gated MUSTs

scoped tests exist; the remaining obligation is unmet or unproven, with zero whole-requirement credit

Proven by a recorded break86.9%73 of 84 tagged units

a red was observed once under a recorded procedure, and the unit, the claim and the producer it rested on still hash to what was recorded. The break is not re-run. A test pair is not a proof until one has been observed

Neutral

measures that are neither good news nor bad

Gated MUSTs37of 40 this summary declares

MUST-level requirements the gate HOLDS. A population, not a result: the shares beside it are what says how Ze stands

Out of scope0of 37 gated MUSTs

an obligation that does not bind Ze. A {not-applicable} annotation says it never bound; a {feature-declined} annotation says its condition is an optional feature Ze does not offer, and quotes the RFC sentence that makes it optional. Scope, not coverage: it stays in the denominator every share on this page is taken over

Not applicable0.0%0 of 37 gated MUSTs

a {not-applicable} annotation says the obligation does not bind Ze, so no test is owed for it. It stays in the denominator every share here is taken over

Met below Ze2.7%1 of 37 gated MUSTs

a {lower-layer} annotation says a layer under Ze performs the behavior, on state Ze installs into that layer, and names the producer that installs it. The obligation binds Ze and is met; Ze proves none of it, because its own boundary carries no value the behavior reads

Optional feature declined0.0%0 of 37 gated MUSTs

a {feature-declined} annotation says the obligation is conditional on a feature the RFC makes optional and Ze does not offer, and it quotes the sentence that makes it optional. The condition is false, so nothing is owed and nothing is missing. It stays in the denominator every share here is taken over

Negative

what Ze owes

No test at all10.8%4 of 37 gated MUSTs

no test carries the requirement id, whether or not a gap states why

The 8 shares marked as a part above are the whole of the 37 gated MUSTs: they add to 100%. Proven by a recorded break is a share of TAGGED UNITS, a different population, so it is not one of them.

How to read the colors

A color names what the measure MEANS, not how well Ze scores on it. Green is a good outcome at any value, red is a bad one, and neither a population nor a scope count is an outcome, so both take no color. The number under the label is what says how far Ze has got.

Card	Tone here	Why that color
Gated MUSTs	neutral	no color: a population is a scale, and a larger one is neither good news nor bad. It is the accounting total
Out of scope	neutral	no color: an obligation that never bound Ze is neither an achievement nor a failure, and counting it either way would be a claim
Tested both ways	ok	green at every value: a test pair is the outcome this gate exists to produce, and the share under the label is what says how far Ze has got
One polarity plus reason	ok	green at every value: where no counter-case exists, one polarity IS the complete answer, and a recorded reason is what the gate demands beside it
One polarity, unexcused	ok	green at zero, RED above it: half a proof with no reason for the other half
Partial proof; remaining gap	ok	green at zero, RED above it: a tested clause cannot prove the whole requirement
No test at all	bad	green at zero, RED above it: a binding obligation nothing exercises is a claim with nothing behind it, whether or not a reason is stated
Not applicable	neutral	no color: an obligation that never bound Ze is neither an achievement nor a failure, and counting it either way would be a claim
Met below Ze	neutral	no color: an obligation met below Ze is neither a test Ze wrote nor work Ze owes, and the two green shares above are what says how much Ze proves itself
Optional feature declined	neutral	no color: an obligation whose condition Ze never meets is neither an achievement nor a failure. The absent FEATURE is disclosed on the RFC's own status row, as an implementation gap a later scope decision can revisit
Proven by a recorded break	ok	green at every value: an observed break is the outcome the discrimination gate exists to produce. The denominator is TAGGED UNITS, not obligations, so this share is not one of the parts above
Audit verdicts	warn	RED on the first weak, wrong or unimplemented verdict, amber while a verdict is no longer current or a gated MUST is unjudged, green when every one is judged sound and current

At a glance

Field	Value
Public status	Partial
Enrolment	Enrolled
Requirements	40
Gated MUST-level	37
Not applicable, so out of scope	0
Declared gaps	4
Declared gaps a test demonstrates	0
Gated with no test	0
Nightly-only evidence	0
Test tags	84
Tagged units	84
Recorded audit verdicts	31
Discrimination records	73
Summary	`rfc/short/rfc2516.md`
Requirement shard	`rfc/requirements/rfc2516.md`
RFC text	`rfc/full/rfc2516.txt`

Enrolment

Enrolled: PPPoE access-concentrator and client roles: discovery framing and tags, session identity, kernel transport setup, PADT lifetime, and transport-specific LCP negotiation. Requirement bindings come from the tagged tests; the checklist records remaining kernel-path evidence and conditional feature decisions.

What the public ledger says

Status: Partial

What the ledger says is covered

Access concentrator (PADI/PADO/PADR/PADS/PADT discovery, AC-Cookie, session tables, AF_PPPOX kernel sessions) and PPPoE client/Host dialer share PPP codecs and option validation. The AC uses the PPP driver
the client runs its own negotiation loop. Requirement bindings are derived from the tagged tests. The PADT lifetime and prohibited-option regressions pass and carry discrimination records in rfc/discrimination/rfc2516.json (2026-10-09).

What the ledger says remains

Four MUST rows carry {gap}. BuildPADI limits the PPPoE header and payload to 1484 octets, excluding the Ethernet header; the returned frame can reach 1498 octets and an oversized request returns nil. Tests exercise that boundary and the 16-octet relay-tag reservation. The Linux pppoe module writes session CODE 0x00. Both roles now stop PPP transport on PADT and reject ACCM, ACFC and FCS Alternatives (type 9); their regressions carry discrimination records. PFC is NOT RECOMMENDED rather than prohibited by Section 7. Remaining annotations below cover kernel resource-allocation evidence and the conditional relay-agent and Generic-Error features proposed in existing specs. Error tags currently carry no data. The session table reserves SESSION_ID 0xffff, and PADO/PADS emit Service-Name even when its value is empty. Receive-side tolerance of absent or repeated Service-Name is documented in docs/architecture/l2tp/bng-5-pppoe.md; Sections 5.1 and 5.3 bind the sender. No optional-feature decision is implied by the backlog specs.

Coverage

Bucket	Count	What it counts
Positive and negative tests	26	one part of the gated population
Annotated (including scoped evidence)	11	one part of the gated population
One polarity only	0	one part of the gated population
No test and no annotation	0	one part of the gated population
Partial proof; remaining gap (subset of annotated; zero whole-requirement credit)	0	an overlay: each of these is also counted by the part it falls in
Evidence that runs nightly only	0	an overlay: each of these is also counted by the part it falls in
Derived from other rows	0	outside the gated population: each asserts nothing and derives its state from the rows it names, which the parts above already count
Gated MUST-level requirements	37	every gated MUST falls in exactly one bucket above

Positive and negative tests (26): RFC2516-x-1, RFC2516-x-2, RFC2516-x-4, RFC2516-5.2-1, RFC2516-5.3-1, RFC2516-x-5, RFC2516-5.2-2, RFC2516-5.2-4, RFC2516-5.4-1, RFC2516-5.4-2, RFC2516-x-6, RFC2516-x-7, RFC2516-x-9, RFC2516-7-1, RFC2516-4-1, RFC2516-5.1-4, RFC2516-5.1-5, RFC2516-5.2-6, RFC2516-5.3-5, RFC2516-5.4-3, RFC2516-5.5-3, RFC2516-5.5-4, RFC2516-7-2, RFC2516-7-3, RFC2516-7-4, RFC2516-x-10

Annotated (including scoped evidence) (11): RFC2516-5.1-1, RFC2516-5.1-2, RFC2516-5.3-2, RFC2516-x-8, RFC2516-3-1, RFC2516-6-1, RFC2516-x-11, RFC2516-x-12, RFC2516-x-13, RFC2516-x-14, RFC2516-x-15

Requirements

Requirement	Level	Section	Tests
`RFC2516-x-1`	The VER field is four bits and MUST be set to 0x1 for this version of the PPPoE specification. (§4)
	MUST	4	positive`unit/verifyTestBuildFrameVerType` negative`unit/verifyTestParseBadVersion`
`RFC2516-x-2`	The TYPE field is four bits and MUST be set to 0x1 for this version of the PPPoE specification. (§4)
	MUST	4	positive`unit/verifyTestBuildFrameVerType` negative`unit/verifyTestParseBadType`
`RFC2516-x-4`	This TAG indicates that there are no further TAGs in the list. The TAG_LENGTH of this TAG MUST always be zero. (Appendix A, §11)
	MUST	11	positive`unit/verifyTestParseEndOfListTag` positive`unit/verifyTestRFC2516NoSentFrameCarriesEndOfList` negative`unit/verifyTestRFC2516NoSentFrameCarriesEndOfList`
`RFC2516-5.2-1`	If the Access Concentrator receives this TAG, it MUST include the TAG unmodified in the associated PADO or PADS response. (Appendix A, §11)
	MUST	11	positive`unit/verifyTestBuildPADO` positive`unit/verifyTestBuildPADS` positive`unit/verifyTestRFC2516AdmittedPADSCarriesTheNewSessionsID` negative`unit/verifyTestBuildNoHostUniqEcho`
`RFC2516-5.3-1`	If a Host receives this TAG, it MUST return the TAG unmodified in the following PADR. (Appendix A, §11)
	MUST	11	positive`unit/verifyTestBuildPADREchoesTags` negative`unit/verifyTestBuildPADRNoOptionalTags`
`RFC2516-x-5`	If either the Host or Access Concentrator receives this TAG they MUST include it unmodified in any discovery packet they send as a response. (Appendix A, §11)
	MUST	11	positive`unit/verifyTestRFC2516RefusingPADSEchoesRelaySessionID` positive`unit/verifyTestRelaySessionIDEcho` negative`unit/verifyTestRFC2516RefusingPADSEchoesRelaySessionID` negative`unit/verifyTestRelaySessionIDNoEcho`
`RFC2516-5.1-1`	The PADI packet MUST contain exactly one TAG of TAG_TYPE Service- Name, indicating the service the Host is requesting, and any number of other TAG types. (§5.1)
	MUST	5.1	positive`unit/verifyTestBuildPADIDiscovery` negative`no test`no negative test {single-polarity}: emit-side count: BuildPADI always writes exactly one Service-Name tag (discovery.go:307). The AC does not enforce the count on receive (MatchServiceName tolerates zero or many, discovery.go:220): this is a deliberate choice, not an omission, per the owner decision of 2026-09-08 recorded in docs/architecture/l2tp/bng-5-pppoe.md ("Ze refuses a PADR with no Service-Name tag and serves a PADI with none"), because Section 5.1 binds the sending host and neither accel-ppp nor FreeBSD enforces this count on receipt either
`RFC2516-5.1-2`	The Host sends the PADI packet with the DESTINATION_ADDR set to the broadcast address. (§5.1)
	MUST	5.1	positive`unit/verifyTestBuildPADIDiscovery` negative`no test`no negative test {single-polarity}: emit-side: BuildPADI addresses the PADI to the Ethernet broadcast MAC (discovery.go:305); the receive-side non-broadcast-PADI discard is not enforced (handlePADI checks only SID, server.go:53)
`RFC2516-5.2-2`	The PADO packet MUST contain one AC-Name TAG containing the Access Concentrator's name, a Service-Name TAG identical to the one in the PADI, and any number of other Service-Name TAGs indicating other services that the Access Concentrator offers. (§5.2)
	MUST	5.2	positive`unit/verifyTestPADOAlwaysCarriesServiceName` positive`unit/verifyTestRFC2516PADOCarriesACNameAndServiceNames` negative`unit/verifyTestPADOAlwaysCarriesServiceName`
`RFC2516-5.2-4`	If the Access Concentrator can not serve the PADI it MUST NOT respond with a PADO. (§5.2)
	MUST NOT	5.2	positive`unit/verifyTestRFC2516UnservedServiceNameIsRefused` negative`unit/verifyTestRFC2516UnservedServiceNameIsRefused`
`RFC2516-5.3-2`	The PADR packet MUST contain exactly one TAG of TAG_TYPE Service- Name, indicating the service the Host is requesting, and any number of other TAG types. (§5.3)
	MUST	5.3	positive`unit/verifyTestBuildPADREchoesTags` negative`no test`no negative test {single-polarity}: emit-side count: BuildPADR writes exactly one Service-Name tag (discovery.go:322). The AC's requireServiceNameTag (server.go) now refuses a PADR carrying zero Service-Name tags on receipt, but that enforces PRESENCE, not COUNT: a PADR carrying two Service-Name tags is accepted, first-wins (TestDuplicateServiceNameTagTakesTheFirst), so there is still no receive-side enforcement of "exactly one, not more" to give a negative for this requirement
`RFC2516-5.4-1`	The PADS packet contains exactly one TAG of TAG_TYPE Service-Name, indicating the service under which Access Concentrator has accepted the PPPoE session, and any number of other TAG types. (§5.4)
	MUST	5.4	positive`unit/verifyTestBuildPADS` negative`unit/verifyTestPADSAlwaysCarriesServiceName`
`RFC2516-5.4-2`	If the Access Concentrator does not like the Service-Name in the PADR, then it MUST reply with a PADS containing a TAG of TAG_TYPE Service-Name-Error (and any number of other TAG types). In this case the SESSION_ID MUST be set to 0x0000. (§5.4)
	MUST	5.4	positive`unit/verifyTestPADRWithoutServiceNameGetsServiceNameError` positive`unit/verifyTestRFC2516UnservedServiceNameIsRefused` negative`unit/verifyTestRFC2516AdmittedPADSCarriesTheNewSessionsID`
`RFC2516-x-6`	For Discovery packets, the value is either a unicast or broadcast address as defined in the Discovery section. For PPP session traffic, this field MUST contain the peer's unicast address as determined from the Discovery stage. (§4)
	MUST	4	positive`unit/verifyTestRFC2516AdmittedPADSCarriesTheNewSessionsID` negative`unit/verifyTestRFC2516SessionNeverBoundToANonUnicastPeer`
`RFC2516-x-7`	The SOURCE_ADDR field MUST contains the Ethernet MAC address of the source device. (§4)
	MUST	4	positive`unit/verifyTestParsePADI` positive`unit/verifyTestRFC2516BuildersWriteTheSendersMAC` negative`unit/verifyTestParseBroadcastSource` negative`unit/verifyTestParseMulticastSource`
`RFC2516-x-8`	If a discovery packet is received with a TAG of unknown TAG_TYPE, the TAG MUST be ignored unless otherwise specified in this document. (§5)
	MUST	5	positive`unit/verifyTestUnknownTagIgnored` negative`no test`no negative test {single-polarity}: tolerate requirement: parseTags stores unknown tag types generically and never errors on them (discovery.go:154); rejecting an unknown tag would itself violate the MUST NOT, so no negative exists
`RFC2516-x-9`	The Maximum-Receive-Unit (MRU) option MUST NOT be negotiated to a larger size than 1492. (§7)
	MUST NOT	7	positive`unit/verifyTestLCPConfigRequestMRU` positive`unit/verifyTestRFC2516AccessConcentratorNegotiatesMRUAtThePPPoECeiling` positive`unit/verifyTestRFC2516ClientNegotiatesMRUAtThePPPoECeiling` positive`unit/verifyTestRFC2516HostSessionMTUDefaultsToThePPPoECeiling` negative`unit/verifyTestRFC2516AccessConcentratorRefusesAnMRUAboveThePPPoECeiling` negative`unit/verifyTestRFC2516ClientRefusesAnMRUAboveThePPPoECeiling` negative`unit/verifyTestRFC2516HostRefusesASessionMTUAboveThePPPoECeiling`
`RFC2516-7-1`	The SESSION_ID MUST NOT change for that PPPoE session and MUST be the value assigned in the Discovery stage. (§6)
	MUST	6	positive`unit/verifyTestRFC2516AdmittedPADSCarriesTheNewSessionsID` negative`unit/verifyTestRFC2516PADRReplayKeepsTheSessionID`
`RFC2516-3-1`	Once a PPP session is established, both the Host and the Access Concentrator MUST allocate the resources for a PPP virtual interface (§3)
	MUST	3	positive`no test`no positive test negative`no test`no negative test {gap}: both roles allocate the interface (server.go::handlePADR, pppoeclient/dialer.go::Dial) but no tagged test observes the ppp unit, which only a QEMU run can; plan/pre-release/spec-pppoe-virtual-interface-proof.md
`RFC2516-4-1`	A value of 0xffff is reserved for future use and MUST NOT be used (§4)
	MUST NOT	4	positive`unit/verifyTestRFC2516AllocSIDReturnsUsableValue` negative`unit/verifyTestRFC2516SessionID0xffffIsNeverAllocated`
`RFC2516-5.1-4`	The CODE field is set to 0x09 and the SESSION_ID MUST be set to 0x0000. (§5.1)
	MUST	5.1	positive`unit/verifyTestRFC2516PADISessionIDIsZero` negative`unit/verifyTestRFC2516PADIWithNonZeroSessionIDIsDropped`
`RFC2516-5.1-5`	An entire PADI packet (including the PPPoE header) MUST NOT exceed 1484 octets so as to leave sufficient room for a relay agent to add a Relay-Session-Id TAG. (§5.1)
	MUST NOT	5.1	positive`unit/verifyTestPADINeverExceeds1484Octets` negative`unit/verifyTestPADINeverExceeds1484Octets`
`RFC2516-5.2-6`	The CODE field is set to 0x07 and the SESSION_ID MUST be set to 0x0000. (§5.2)
	MUST	5.2	positive`unit/verifyTestRFC2516PADOSessionIDIsZero` negative`unit/verifyTestRFC2516PADOWithNonZeroSessionIDIsNotAnOffer`
`RFC2516-5.3-5`	The CODE field is set to 0x19 and the SESSION_ID MUST be set to 0x0000. (§5.3)
	MUST	5.3	positive`unit/verifyTestRFC2516PADRSessionIDIsZero` negative`unit/verifyTestRFC2516PADRWithNonZeroSessionIDIsDropped`
`RFC2516-5.4-3`	The CODE field is set to 0x65 and the SESSION_ID MUST be set to the unique value generated for this PPPoE session. (§5.4)
	MUST	5.4	positive`unit/verifyTestRFC2516AdmittedPADSCarriesTheNewSessionsID` positive`unit/verifyTestRFC2516PADSCarriesTheSessionsID` negative`unit/verifyTestRFC2516PADSWithZeroSessionIDIsARefusal`
`RFC2516-5.5-3`	The DESTINATION_ADDR field is a unicast Ethernet address, the CODE field is set to 0xa7 and the SESSION_ID MUST be set to indicate which session is to be terminated. (§5.5)
	MUST	5.5	positive`unit/verifyTestBuildPADT` positive`unit/verifyTestRFC2516HostPADTNamesItsAccessConcentratorAndSession` positive`unit/verifyTestRFC2516SessionDownSendsPADTForThatSession` negative`unit/verifyTestRFC2516HostPADTNeverAddressesAGroupOrAForeignSession` negative`unit/verifyTestRFC2516UnknownSessionIDTerminatesNothing`
`RFC2516-5.5-4`	Even normal PPP termination packets MUST NOT be sent after sending or receiving a PADT (§5.5)
	MUST NOT	5.5	positive`unit/verifyTestRFC2516ACReceivedPADTClosesOnlyMatchingTransport` positive`unit/verifyTestRFC2516ACSentPADTClosesTransportBeforeSend` positive`unit/verifyTestRFC2516ClientPADTStopsOnlyMatchingSession` positive`unit/verifyTestRFC2516ClientSentPADTStopsPPPBeforeSend` negative`unit/verifyTestRFC2516ACReceivedPADTClosesOnlyMatchingTransport` negative`unit/verifyTestRFC2516ClientPADTStopsOnlyMatchingSession`
`RFC2516-6-1`	The PPPoE CODE MUST be set to 0x00. (§6)
	MUST	6	positive`no test`no positive test negative`no test`no negative test {lower-layer}: Linux pppoe (PX_PROTO_OE); internal/component/l2tp/pppoe/kernel_linux.go::pppoeCreate connects the AF_PPPOX socket to the session ID, the peer MAC and the device, and the module writes the CODE byte of every session frame itself, so no value Ze writes decides this field
`RFC2516-7-2`	An implementation MUST NOT request any of the following options, and MUST reject a request for such an option: Field Check Sequence (FCS) Alternatives, Address-and-Control-Field-Compression (ACFC), Asynchronous-Control-Character-Map (ACCM) (§7)
	MUST NOT	7	positive`unit/verifyTestRFC2516ACRejectsForbiddenLCPOptions` positive`unit/verifyTestRFC2516ClientRejectsForbiddenLCPOptions` negative`unit/verifyTestRFC2516ACRejectsForbiddenLCPOptions` negative`unit/verifyTestRFC2516ClientRejectsForbiddenLCPOptions`
`RFC2516-7-3`	When LCP terminates, the Host and Access concentrator MUST stop using that PPPoE session. (§7)
	MUST	7	positive`unit/verifyTestRFC2516HostStopsUsingTheSessionWhenLCPTerminates` positive`unit/verifyTestRFC2516SessionDownSendsPADTForThatSession` negative`unit/verifyTestRFC2516HostKeepsTheSessionUntilLCPTerminates` negative`unit/verifyTestRFC2516UnknownSessionIDTerminatesNothing`
`RFC2516-7-4`	If the Host wishes to start another PPP session, it MUST return to the PPPoE Discovery stage. (§7)
	MUST	7	positive`unit/verifyTestRFC2516HostReturnsToDiscoveryForTheNextSession` negative`unit/verifyTestRFC2516HostReturnsToDiscoveryForTheNextSession`
`RFC2516-x-10`	All PADI packets MUST guarantee sufficient room for the addition of a Relay-Session-Id TAG with a TAG_VALUE length of 12 octets. (Appendix A, §11)
	MUST	11	positive`unit/verifyTestPADINeverExceeds1484Octets` negative`unit/verifyTestPADINeverExceeds1484Octets`
`RFC2516-x-11`	A Relay-Session-Id TAG MUST NOT be added if the discovery packet already contains one. (Appendix A, §11)
	MUST NOT	11	positive`no test`no positive test negative`no test`no negative test {gap}: Ze fills no PPPoE relay agent; plan/spec-pppoe-relay-agent.md
`RFC2516-x-12`	This TAG (typically with a zero-length data section) indicates that for one reason or another, the requested Service-Name request could not be honored. If there is data, and the first octet of the data is nonzero, then it MUST be a printable UTF-8 string which explains why the request was denied. (Appendix A, §11)
	MUST	11	positive`unit/verifyTestRFC2516ErrorTagsCarryNoData` negative`no test`no negative test {single-polarity}: discovery.go::BuildPADSError writes the tag with no data, so the conditional never binds and no violating input exists
`RFC2516-x-13`	It MAY be included in PADS packets. If there is data, and the first octet of the data is nonzero, then it MUST be a printable UTF-8 string which explains the nature of the error. (Appendix A, §11)
	MUST	11	positive`unit/verifyTestRFC2516ErrorTagsCarryNoData` negative`no test`no negative test {single-polarity}: discovery.go::BuildPADSError writes the tag with no data, so the conditional never binds and no violating input exists
`RFC2516-x-14`	It can be added to PADO, PADR or PADS packets when an unrecoverable error occurs and no other error TAG is appropriate. If there is data then it MUST be an UTF-8 string which explains the nature of the error. (Appendix A, §11)
	MUST	11	positive`no test`no positive test negative`no test`no negative test {gap}: Ze emits no Generic-Error TAG (discovery.go::BuildPADT, BuildPADSError); plan/spec-pppoe-generic-error-tag.md
`RFC2516-x-15`	If there is data then it MUST be an UTF-8 string which explains the nature of the error. This string MUST NOT be NULL terminated. (Appendix A, §11)
	MUST NOT	11	positive`no test`no positive test negative`no test`no negative test {gap}: Ze emits no Generic-Error TAG (discovery.go::BuildPADT, BuildPADSError); plan/spec-pppoe-generic-error-tag.md
`RFC2516-5.2-5`	The Access Concentrator MAY include this TAG in a PADO packet. (Appendix A, §11)
	MAY	11	positive`no test`no positive test negative`no test`no negative test
`RFC2516-5.1-3`	The Host MAY include a Host-Uniq TAG in a PADI or PADR. (Appendix A, §11)
	MAY	11	positive`no test`no positive test negative`no test`no negative test
`RFC2516-5.5-1`	This packet may be sent anytime after a session is established to indicate that a PPPoE session has been terminated. It may be sent by either the Host or the Access Concentrator. (§5.5)
	MAY	5.5	positive`no test`no positive test negative`no test`no negative test

Gaps and untested MUSTs

Requirement	State	Reason
`RFC2516-3-1` Once a PPP session is established, both the Host and the Access Concentrator MUST allocate the resources for a PPP virtual interface (§3)	{gap}, no test	both roles allocate the interface (server.go::handlePADR, pppoeclient/dialer.go::Dial) but no tagged test observes the ppp unit, which only a QEMU run can; plan/pre-release/spec-pppoe-virtual-interface-proof.md
`RFC2516-6-1` The PPPoE CODE MUST be set to 0x00. (§6)	no test	no test carries this requirement id; annotated {lower-layer}: Linux pppoe (PX_PROTO_OE); internal/component/l2tp/pppoe/kernel_linux.go::pppoeCreate connects the AF_PPPOX socket to the session ID, the peer MAC and the device, and the module writes the CODE byte of every session frame itself, so no value Ze writes decides this field
`RFC2516-x-11` A Relay-Session-Id TAG MUST NOT be added if the discovery packet already contains one. (Appendix A, §11)	{gap}, no test	Ze fills no PPPoE relay agent; plan/spec-pppoe-relay-agent.md
`RFC2516-x-14` It can be added to PADO, PADR or PADS packets when an unrecoverable error occurs and no other error TAG is appropriate. If there is data then it MUST be an UTF-8 string which explains the nature of the error. (Appendix A, §11)	{gap}, no test	Ze emits no Generic-Error TAG (discovery.go::BuildPADT, BuildPADSError); plan/spec-pppoe-generic-error-tag.md
`RFC2516-x-15` If there is data then it MUST be an UTF-8 string which explains the nature of the error. This string MUST NOT be NULL terminated. (Appendix A, §11)	{gap}, no test	Ze emits no Generic-Error TAG (discovery.go::BuildPADT, BuildPADSError); plan/spec-pppoe-generic-error-tag.md

Proof state

A tagged unit reads unproven where no discrimination record exists for it: nothing in this tree has been observed to break it, so the claim its tag makes is unproven.

`RFC2516-x-1`

The VER field is four bits and MUST be set to 0x1 for this version of the PPPoE specification. (§4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. TestBuildFrameVerType asserts BuildPADI writes VER=1; TestParseBadVersion shows a VER=2 frame is refused

Polarity	Test	Kind and tier	Proof state
negative	`TestParseBadVersion`	unit/verify	unproven
positive	`TestBuildFrameVerType`	unit/verify	unproven

`RFC2516-x-2`

The TYPE field is four bits and MUST be set to 0x1 for this version of the PPPoE specification. (§4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. TestBuildFrameVerType asserts BuildPADI writes TYPE=1; TestParseBadType shows a TYPE=2 frame is refused

Polarity	Test	Kind and tier	Proof state
negative	`TestParseBadType`	unit/verify	unproven
positive	`TestBuildFrameVerType`	unit/verify	unproven

`RFC2516-x-4`

This TAG indicates that there are no further TAGs in the list. The TAG_LENGTH of this TAG MUST always be zero. (Appendix A, §11)

Audit verdict: enforced (the tests do what the requirement demands), fresh. first sentence: TestParseEndOfListTag. TAG_LENGTH MUST: Ze builds no End-Of-List; TestRFC2516NoSentFrameCarriesEndOfList walks the raw TLVs of the PADO and PADS replies and shows a received End-Of-List of TAG_LENGTH 4 is never copied out. Not observed: BuildPADR and BuildPADSError, which copy tags by type the same way (AddTagCopy of FindTag) and so cannot carry one either. Stale single-polarity marker removed

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC2516NoSentFrameCarriesEndOfList`	unit/verify	revert, verified
positive	`TestRFC2516NoSentFrameCarriesEndOfList`	unit/verify	revert, verified
positive	`TestParseEndOfListTag`	unit/verify	revert, verified

`RFC2516-5.2-1`

If the Access Concentrator receives this TAG, it MUST include the TAG unmodified in the associated PADO or PADS response. (Appendix A, §11)

Audit verdict: enforced (the tests do what the requirement demands), fresh. PADO echo byte-compared by TestBuildPADO; PADS echo now byte-compared both in TestBuildPADS and through handlePADR for two hosts with distinct Host-Uniq values (TestRFC2516AdmittedPADSCarriesTheNewSessionsID); TestBuildNoHostUniqEcho proves no Host-Uniq is invented. Observed-red records on BuildPADS for both new/changed units

Polarity	Test	Kind and tier	Proof state
negative	`TestBuildNoHostUniqEcho`	unit/verify	revert, verified
positive	`TestRFC2516AdmittedPADSCarriesTheNewSessionsID`	unit/verify	revert, verified
positive	`TestBuildPADO`	unit/verify	revert, verified
positive	`TestBuildPADS`	unit/verify	revert, verified

`RFC2516-5.3-1`

If a Host receives this TAG, it MUST return the TAG unmodified in the following PADR. (Appendix A, §11)

Audit verdict: enforced (the tests do what the requirement demands), fresh. TestBuildPADREchoesTags compares the echoed AC-Cookie bytes; TestBuildPADRNoOptionalTags shows none is invented

Polarity	Test	Kind and tier	Proof state
negative	`TestBuildPADRNoOptionalTags`	unit/verify	unproven
positive	`TestBuildPADREchoesTags`	unit/verify	unproven

`RFC2516-x-5`

If either the Host or Access Concentrator receives this TAG they MUST include it unmodified in any discovery packet they send as a response. (Appendix A, §11)

Audit verdict: enforced (the tests do what the requirement demands), fresh. the refusing PADS (BuildPADSError via handlePADR) and the admitting PADS now echo the Relay-Session-Id byte-for-byte, and a refusing PADS for a PADR without one invents none; PADO, PADR and PADS builder echo and no-echo units unchanged. Records red on BuildPADSError

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC2516RefusingPADSEchoesRelaySessionID`	unit/verify	revert, verified
negative	`TestRelaySessionIDNoEcho`	unit/verify	revert, verified
positive	`TestRFC2516RefusingPADSEchoesRelaySessionID`	unit/verify	revert, verified
positive	`TestRelaySessionIDEcho`	unit/verify	revert, verified

`RFC2516-5.1-1`

The PADI packet MUST contain exactly one TAG of TAG_TYPE Service- Name, indicating the service the Host is requesting, and any number of other TAG types. (§5.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. single-polarity; TestBuildPADIDiscovery counts exactly one Service-Name tag

Polarity	Test	Kind and tier	Proof state
positive	`TestBuildPADIDiscovery`	unit/verify	unproven

`RFC2516-5.1-2`

The Host sends the PADI packet with the DESTINATION_ADDR set to the broadcast address. (§5.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. single-polarity; TestBuildPADIDiscovery asserts the PADI DstMAC is the broadcast address

Polarity	Test	Kind and tier	Proof state
positive	`TestBuildPADIDiscovery`	unit/verify	unproven

`RFC2516-5.2-2`

The PADO packet MUST contain one AC-Name TAG containing the Access Concentrator's name, a Service-Name TAG identical to the one in the PADI, and any number of other Service-Name TAGs indicating other services that the Access Concentrator offers. (§5.2)

Audit verdict: enforced (the tests do what the requirement demands), fresh. TestRFC2516PADOCarriesACNameAndServiceNames drives handlePADI and asserts exactly one AC-Name equal to the configured name, the first Service-Name identical to the PADI's, then the other offered name in order; TestPADOAlwaysCarriesServiceName pins the Service-Name list and the zero-length edge. Records observed red on BuildPADO

Polarity	Test	Kind and tier	Proof state
negative	`TestPADOAlwaysCarriesServiceName`	unit/verify	revert, verified
positive	`TestRFC2516PADOCarriesACNameAndServiceNames`	unit/verify	revert, verified
positive	`TestPADOAlwaysCarriesServiceName`	unit/verify	revert, verified

`RFC2516-5.2-4`

If the Access Concentrator can not serve the PADI it MUST NOT respond with a PADO. (§5.2)

Audit verdict: enforced (the tests do what the requirement demands), fresh. TestRFC2516UnservedServiceNameIsRefused drives handlePADI: a PADI naming an unserved Service-Name draws no frame, the same PADI naming a served one draws exactly one PADO, so the silence is specific to the unserved service. Both polarities recorded red on handlePADI

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC2516UnservedServiceNameIsRefused`	unit/verify	revert, verified
positive	`TestRFC2516UnservedServiceNameIsRefused`	unit/verify	revert, verified

`RFC2516-5.3-2`

The PADR packet MUST contain exactly one TAG of TAG_TYPE Service- Name, indicating the service the Host is requesting, and any number of other TAG types. (§5.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. single-polarity; TestBuildPADREchoesTags counts exactly one Service-Name tag

Polarity	Test	Kind and tier	Proof state
positive	`TestBuildPADREchoesTags`	unit/verify	unproven

`RFC2516-5.4-1`

The PADS packet contains exactly one TAG of TAG_TYPE Service-Name, indicating the service under which Access Concentrator has accepted the PPPoE session, and any number of other TAG types. (§5.4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. re-read after TestBuildPADS changed (only its Host-Uniq check was tightened to a byte compare): TestBuildPADS and TestPADSAlwaysCarriesServiceName both count exactly one Service-Name tag in the PADS, including for a PADR carrying none

Polarity	Test	Kind and tier	Proof state
negative	`TestPADSAlwaysCarriesServiceName`	unit/verify	revert, verified
positive	`TestBuildPADS`	unit/verify	unproven

`RFC2516-5.4-2`

If the Access Concentrator does not like the Service-Name in the PADR, then it MUST reply with a PADS containing a TAG of TAG_TYPE Service-Name-Error (and any number of other TAG types). In this case the SESSION_ID MUST be set to 0x0000. (§5.4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. positive: a PADR with a PRESENT unserved Service-Name through handlePADR draws one PADS with Service-Name-Error and SESSION_ID 0x0000, no session, no socket (TestRFC2516UnservedServiceNameIsRefused); the absent-tag branch stays covered by TestPADRWithoutServiceNameGetsServiceNameError. negative: a served name draws a non-zero SID and no Service-Name-Error. All three recorded red on handlePADR

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC2516AdmittedPADSCarriesTheNewSessionsID`	unit/verify	revert, verified
positive	`TestRFC2516UnservedServiceNameIsRefused`	unit/verify	revert, verified
positive	`TestPADRWithoutServiceNameGetsServiceNameError`	unit/verify	revert, verified

`RFC2516-x-6`

For Discovery packets, the value is either a unicast or broadcast address as defined in the Discovery section. For PPP session traffic, this field MUST contain the peer's unicast address as determined from the Discovery stage. (§4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. session-stage addressing is set by connecting the pppox socket: the positive asserts each admitted session's socket is bound to its PADR's unicast source MAC; the negative shows a broadcast- and a multicast-sourced PADR are refused by ParseDiscovery before HandleDiscovery and bind nothing, while a unicast source binds itself. The negative mirrors Subsystem.discoveryReader's parse-then-dispatch inline (read at subsystem.go, it matches), so a change to the reader itself would not turn it red. Records red on createTransport and ParseDiscovery

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC2516SessionNeverBoundToANonUnicastPeer`	unit/verify	revert, verified
positive	`TestRFC2516AdmittedPADSCarriesTheNewSessionsID`	unit/verify	revert, verified

`RFC2516-x-7`

The SOURCE_ADDR field MUST contains the Ethernet MAC address of the source device. (§4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. TestRFC2516BuildersWriteTheSendersMAC asserts PADI, PADR, PADO, PADS, the refusing PADS and PADT write the sender MAC they are given in SOURCE_ADDR; every production call site passes the device's own MAC (s.hwAddr in server.go, hwaddr/srcMAC in pppoeclient/dialer.go), read, not asserted. Receive side refuses broadcast and multicast sources. Record red on NewBuilder

Polarity	Test	Kind and tier	Proof state
negative	`TestParseBroadcastSource`	unit/verify	revert, verified
negative	`TestParseMulticastSource`	unit/verify	revert, verified
positive	`TestRFC2516BuildersWriteTheSendersMAC`	unit/verify	revert, verified
positive	`TestParsePADI`	unit/verify	revert, verified

`RFC2516-x-8`

If a discovery packet is received with a TAG of unknown TAG_TYPE, the TAG MUST be ignored unless otherwise specified in this document. (§5)

Audit verdict: enforced (the tests do what the requirement demands), fresh. single-polarity; TestUnknownTagIgnored parses a frame with an unknown tag without error and keeps known tags findable

Polarity	Test	Kind and tier	Proof state
positive	`TestUnknownTagIgnored`	unit/verify	unproven

`RFC2516-x-9`

The Maximum-Receive-Unit (MRU) option MUST NOT be negotiated to a larger size than 1492. (§7)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-30 (access cont 10, independent). Both halves proven. Host: pppoeSessionMTU (dialer.go, producer read) defaults 0 -> 1492, keeps 68..1492, refuses the rest; Dial calls it before ResolveInterface. + TestRFC2516HostSessionMTUDefaultsToThePPPoECeiling (0/1492/1480, and the default drives negotiateLCP to a Configure-Request MRU 1492); - TestRFC2516HostRefusesASessionMTUAboveThePPPoECeiling (1493/1500/9000 refused; Dial with MTU 1500 refused before discovery). This closes the gap the cont 8 verdict named. Host LCP pair (TestRFC2516ClientNegotiatesMRUAtThePPPoECeiling / ...RefusesAnMRUAboveThePPPoECeiling) and AC pair (TestRFC2516AccessConcentratorNegotiatesMRUAtThePPPoECeiling / ...RefusesAnMRUAboveThePPPoECeiling) unchanged. Every unit but the older TestLCPConfigRequestMRU carries an observed-red record.

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC2516AccessConcentratorRefusesAnMRUAboveThePPPoECeiling`	unit/verify	revert, verified
negative	`TestRFC2516HostRefusesASessionMTUAboveThePPPoECeiling`	unit/verify	revert, verified
negative	`TestRFC2516ClientRefusesAnMRUAboveThePPPoECeiling`	unit/verify	revert, verified
positive	`TestRFC2516AccessConcentratorNegotiatesMRUAtThePPPoECeiling`	unit/verify	revert, verified
positive	`TestRFC2516HostSessionMTUDefaultsToThePPPoECeiling`	unit/verify	revert, verified
positive	`TestRFC2516ClientNegotiatesMRUAtThePPPoECeiling`	unit/verify	revert, verified
positive	`TestLCPConfigRequestMRU`	unit/verify	revert, verified

`RFC2516-7-1`

The SESSION_ID MUST NOT change for that PPPoE session and MUST be the value assigned in the Discovery stage. (§6)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Ze's share of Section 6 is binding the session socket: TestRFC2516AdmittedPADSCarriesTheNewSessionsID asserts the socket is bound once to the SID the PADS assigned (createTransport seam, production path unchanged), and TestRFC2516PADRReplayKeepsTheSessionID shows a retransmitted PADR keeps the SID, binds no second socket, adds no session. The kernel pppox socket keeps the SID fixed after connect. The PADT-MAC unit no longer carries the tag. Records red on createTransport and matchLiveCookie

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC2516PADRReplayKeepsTheSessionID`	unit/verify	revert, verified
positive	`TestRFC2516AdmittedPADSCarriesTheNewSessionsID`	unit/verify	revert, verified

`RFC2516-3-1`

Once a PPP session is established, both the Host and the Access Concentrator MUST allocate the resources for a PPP virtual interface (§3)

Audit verdict: not audited: no reader has judged these tests

No test carries RFC2516-3-1, so no unit is bound to it.

`RFC2516-4-1`

A value of 0xffff is reserved for future use and MUST NOT be used (§4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. TestRFC2516SessionID0xffffIsNeverAllocated exhausts the table and shows 0xffff is never handed out, even after freeSID

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC2516SessionID0xffffIsNeverAllocated`	unit/verify	revert, verified
positive	`TestRFC2516AllocSIDReturnsUsableValue`	unit/verify	revert, verified

`RFC2516-5.1-4`

The CODE field is set to 0x09 and the SESSION_ID MUST be set to 0x0000. (§5.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. TestRFC2516PADISessionIDIsZero asserts CODE 0x09 and SESSION_ID 0; the negative shows handlePADI drops a non-zero SESSION_ID PADI

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC2516PADIWithNonZeroSessionIDIsDropped`	unit/verify	revert, verified
positive	`TestRFC2516PADISessionIDIsZero`	unit/verify	revert, verified

`RFC2516-5.1-5`

An entire PADI packet (including the PPPoE header) MUST NOT exceed 1484 octets so as to leave sufficient room for a relay agent to add a Relay-Session-Id TAG. (§5.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. TestPADINeverExceeds1484Octets accepts exactly 1484 octets and refuses 1485

Polarity	Test	Kind and tier	Proof state
negative	`TestPADINeverExceeds1484Octets`	unit/verify	revert, verified
positive	`TestPADINeverExceeds1484Octets`	unit/verify	revert, verified

`RFC2516-5.2-6`

The CODE field is set to 0x07 and the SESSION_ID MUST be set to 0x0000. (§5.2)

Audit verdict: enforced (the tests do what the requirement demands), fresh. TestRFC2516PADOSessionIDIsZero asserts CODE 0x07 and SESSION_ID 0; the client refuses a PADO with a non-zero SESSION_ID

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC2516PADOWithNonZeroSessionIDIsNotAnOffer`	unit/verify	revert, verified
positive	`TestRFC2516PADOSessionIDIsZero`	unit/verify	revert, verified

`RFC2516-5.3-5`

The CODE field is set to 0x19 and the SESSION_ID MUST be set to 0x0000. (§5.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. TestRFC2516PADRSessionIDIsZero asserts CODE 0x19 and SESSION_ID 0; handlePADR drops a non-zero SESSION_ID PADR

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC2516PADRWithNonZeroSessionIDIsDropped`	unit/verify	revert, verified
positive	`TestRFC2516PADRSessionIDIsZero`	unit/verify	revert, verified

`RFC2516-5.4-3`

The CODE field is set to 0x65 and the SESSION_ID MUST be set to the unique value generated for this PPPoE session. (§5.4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. the fresh-admission PADS is now observed: two hosts each get CODE 0x65, a non-zero SESSION_ID equal to the SID the table holds for that host, and the two SIDs differ (TestRFC2516AdmittedPADSCarriesTheNewSessionsID); the replay path stays covered; the client refuses a zero-SID PADS (pppoeclient negative). Records observed red on handlePADR and tryReadPADS

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC2516PADSWithZeroSessionIDIsARefusal`	unit/verify	revert, verified
positive	`TestRFC2516AdmittedPADSCarriesTheNewSessionsID`	unit/verify	revert, verified
positive	`TestRFC2516PADSCarriesTheSessionsID`	unit/verify	revert, verified

`RFC2516-5.5-3`

The DESTINATION_ADDR field is a unicast Ethernet address, the CODE field is set to 0xa7 and the SESSION_ID MUST be set to indicate which session is to be terminated. (§5.5)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-30 (cont 7 re-judge). AC half unchanged and enforced (TestBuildPADT, handleSessionDown sends the PADT for that SID, an unknown SID terminates nothing). Host half, the gap of the prior weak verdict, now proven on raw octets: TestRFC2516HostPADTNamesItsAccessConcentratorAndSession (PADO+PADS through tryReadPADO/tryReadPADS, then sendPADT: DESTINATION_ADDR = offering AC's MAC with the group bit clear, CODE 0xa7, SESSION_ID 0x2345 from the PADS), observed red under a revert of sendPADT; TestRFC2516HostPADTNeverAddressesAGroupOrAForeignSession (a PADO from broadcast or multicast source is never an offer, so no PADT can be addressed to a group; a PADS from another AC carrying 0x3456 is ignored and the PADT names 0x2345), observed red under a revert of tryReadPADS. Residual, named not disqualifying: the two-line acMAC copy from padoPkt.SrcMAC in Dial is mirrored in the test helper because Dial needs kernel PPPoE; Dial passes the same acMAC/sessID to sendPADT on every path (read at dialer.go).

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC2516UnknownSessionIDTerminatesNothing`	unit/verify	revert, verified
negative	`TestRFC2516HostPADTNeverAddressesAGroupOrAForeignSession`	unit/verify	revert, verified
positive	`TestBuildPADT`	unit/verify	revert, verified
positive	`TestRFC2516SessionDownSendsPADTForThatSession`	unit/verify	revert, verified
positive	`TestRFC2516HostPADTNamesItsAccessConcentratorAndSession`	unit/verify	revert, verified

`RFC2516-5.5-4`

Even normal PPP termination packets MUST NOT be sent after sending or receiving a PADT (§5.5)

Audit verdict: not audited: no reader has judged these tests

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC2516ACReceivedPADTClosesOnlyMatchingTransport`	unit/verify	revert, verified
negative	`TestRFC2516ClientPADTStopsOnlyMatchingSession`	unit/verify	revert, verified
positive	`TestRFC2516ACReceivedPADTClosesOnlyMatchingTransport`	unit/verify	revert, verified
positive	`TestRFC2516ACSentPADTClosesTransportBeforeSend`	unit/verify	revert, verified
positive	`TestRFC2516ClientPADTStopsOnlyMatchingSession`	unit/verify	revert, verified
positive	`TestRFC2516ClientSentPADTStopsPPPBeforeSend`	unit/verify	revert, verified

`RFC2516-6-1`

The PPPoE CODE MUST be set to 0x00. (§6)

Audit verdict: not audited: no reader has judged these tests

No test carries RFC2516-6-1, so no unit is bound to it.

`RFC2516-7-2`

An implementation MUST NOT request any of the following options, and MUST reject a request for such an option: Field Check Sequence (FCS) Alternatives, Address-and-Control-Field-Compression (ACFC), Asynchronous-Control-Character-Map (ACCM) (§7)

Audit verdict: enforced (the tests do what the requirement demands), fresh. TestRFC2516ACRejectsForbiddenLCPOptions and TestRFC2516ClientRejectsForbiddenLCPOptions assert Configure-Reject of ACCM, ACFC and FCS Alternatives verbatim, that neither role requests them, and Ack for MRU/PFC

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC2516ACRejectsForbiddenLCPOptions`	unit/verify	revert, verified
negative	`TestRFC2516ClientRejectsForbiddenLCPOptions`	unit/verify	revert, verified
positive	`TestRFC2516ACRejectsForbiddenLCPOptions`	unit/verify	revert, verified
positive	`TestRFC2516ClientRejectsForbiddenLCPOptions`	unit/verify	revert, verified

`RFC2516-7-3`

When LCP terminates, the Host and Access concentrator MUST stop using that PPPoE session. (§7)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Judge 2026-09-30 (cont 7 re-judge). AC half unchanged and enforced (handleSessionDown removes the session and sends its PADT; an unknown SID leaves it). Host half, the gap of the prior weak verdict: TestRFC2516HostStopsUsingTheSessionWhenLCPTerminates drives production superviseNetworkPhase (extracted from Dial's anonymous goroutine with no behaviour change: keepaliveLoop then link.Close, same order, same args) with an AC Terminate-Request: exactly one Terminate-Ack, channel closed once, Done published, link.Write refused, a later Echo-Reply not written (the fake channel accepts writes after Close, so only the session guard refuses). Observed red under a revert of superviseNetworkPhase. Negative TestRFC2516HostKeepsTheSessionUntilLCPTerminates: an Echo-Request and a stray Terminate-Ack leave Done open and the Host answering; only the following Terminate-Request ends it, so the stop is tied to LCP termination and not to any LCP frame. Observed red under a revert of keepaliveLoop.

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC2516UnknownSessionIDTerminatesNothing`	unit/verify	revert, verified
negative	`TestRFC2516HostKeepsTheSessionUntilLCPTerminates`	unit/verify	revert, verified
positive	`TestRFC2516SessionDownSendsPADTForThatSession`	unit/verify	revert, verified
positive	`TestRFC2516HostStopsUsingTheSessionWhenLCPTerminates`	unit/verify	revert, verified

`RFC2516-7-4`

If the Host wishes to start another PPP session, it MUST return to the PPPoE Discovery stage. (§7)

Audit verdict: enforced (the tests do what the requirement demands), fresh. TestRFC2516HostReturnsToDiscoveryForTheNextSession shows the client redials (Discovery) after Done with SESSION_ID 0 and the old session cleaned up

Polarity	Test	Kind and tier	Proof state
negative	`TestRFC2516HostReturnsToDiscoveryForTheNextSession`	unit/verify	revert, verified
positive	`TestRFC2516HostReturnsToDiscoveryForTheNextSession`	unit/verify	revert, verified

`RFC2516-x-10`

All PADI packets MUST guarantee sufficient room for the addition of a Relay-Session-Id TAG with a TAG_VALUE length of 12 octets. (Appendix A, §11)

Audit verdict: enforced (the tests do what the requirement demands), fresh. TestPADINeverExceeds1484Octets asserts exactly 16 octets are left at the largest PADI and that one octet more is refused

Polarity	Test	Kind and tier	Proof state
negative	`TestPADINeverExceeds1484Octets`	unit/verify	revert, verified
positive	`TestPADINeverExceeds1484Octets`	unit/verify	revert, verified

`RFC2516-x-11`

A Relay-Session-Id TAG MUST NOT be added if the discovery packet already contains one. (Appendix A, §11)

Audit verdict: not audited: no reader has judged these tests

No test carries RFC2516-x-11, so no unit is bound to it.

`RFC2516-x-12`

This TAG (typically with a zero-length data section) indicates that for one reason or another, the requested Service-Name request could not be honored. If there is data, and the first octet of the data is nonzero, then it MUST be a printable UTF-8 string which explains why the request was denied. (Appendix A, §11)

Audit verdict: enforced (the tests do what the requirement demands), fresh. single-polarity; TestRFC2516ErrorTagsCarryNoData drives handlePADR and asserts the Service-Name-Error TAG_LENGTH is 0

Polarity	Test	Kind and tier	Proof state
positive	`TestRFC2516ErrorTagsCarryNoData`	unit/verify	revert, verified

`RFC2516-x-13`

It MAY be included in PADS packets. If there is data, and the first octet of the data is nonzero, then it MUST be a printable UTF-8 string which explains the nature of the error. (Appendix A, §11)

Audit verdict: enforced (the tests do what the requirement demands), fresh. single-polarity; TestRFC2516ErrorTagsCarryNoData drives a resource refusal and asserts the AC-System-Error TAG_LENGTH is 0

Polarity	Test	Kind and tier	Proof state
positive	`TestRFC2516ErrorTagsCarryNoData`	unit/verify	revert, verified

`RFC2516-x-14`

It can be added to PADO, PADR or PADS packets when an unrecoverable error occurs and no other error TAG is appropriate. If there is data then it MUST be an UTF-8 string which explains the nature of the error. (Appendix A, §11)

Audit verdict: not audited: no reader has judged these tests

No test carries RFC2516-x-14, so no unit is bound to it.

`RFC2516-x-15`

If there is data then it MUST be an UTF-8 string which explains the nature of the error. This string MUST NOT be NULL terminated. (Appendix A, §11)

Audit verdict: not audited: no reader has judged these tests

No test carries RFC2516-x-15, so no unit is bound to it.

Extraction sign-off

Field	Value
Reviewer	claude
Signed off	2026-09-21
Register	rfc2119
Source	rfc/full/rfc2516.txt
Source fingerprint	260dccfe0a8a3e8c
Record	rfc/extraction/rfc2516.json
Mapped sentences	35
Declined as scope	3
Relocated to a spec, which Ze OWES	0
Unclassified	0

Sections

Section	Name	Sites	Disposition	Reason
`front`	not stated	0	walked	not stated
`1`	not stated	0	walked	not stated
`2`	not stated	1	walked	not stated
`3`	not stated	1	walked	not stated
`4`	not stated	5	walked	not stated
`5`	not stated	1	walked	not stated
`5.1`	not stated	3	walked	not stated
`5.2`	not stated	3	walked	not stated
`5.3`	not stated	2	walked	not stated
`5.4`	not stated	3	walked	not stated
`5.5`	not stated	2	walked	not stated
`6`	not stated	2	walked	not stated
`7`	not stated	5	walked	not stated
`8`	not stated	0	walked	not stated
`9`	not stated	0	walked	not stated
`10`	not stated	0	walked	not stated
`11`	not stated	10	walked	not stated

Excluded sentences

Site	Excluded kind	Reason	Quote
`2:1`	`not-a-requirement` never bound Ze the sentence states a fact or describes another document, and directs no implementation	The RFC 2119 conventions boilerplate of section 2. It tells the reader how to read the keywords and states no obligation of its own.	The keywords MUST, MUST NOT, REQUIRED, SHALL, SHALL NOT, SHOULD, SHOULD NOT, RECOMMENDED, MAY, and OPTIONAL, when they appear in this document, are to be interpreted as described in [2].
`5.4:3`	`duplicate-of` never bound Ze the same obligation is already captured under another requirement id	The second half of the Service-Name-Error reply rule the previous sentence states. RFC2516-5.4-2 already carries it: the Access Concentrator 'MUST reply with a PADS carrying a Service-Name-Error tag, and MUST set SESSION_ID to 0x0000 in that reply'.	In this case the SESSION_ID MUST be set to 0x0000.
`7:3`	`duplicate-of` never bound Ze the same obligation is already captured under another requirement id	The same 1492 ceiling the previous sentence sets on the MRU option, restated as the PPP MTU with its arithmetic: 1500 octets of Ethernet payload less the 6-octet PPPoE header and the 2-octet PPP Protocol ID.	Since Ethernet has a maximum payload size of 1500 octets, the PPPoE header is 6 octets and the PPP Protocol ID is 2 octets, the PPP MTU MUST NOT be greater than 1492.

Superseded

No document obsoletes RFC 2516, so its obligations are stated where they were written.