RFC 2328 - OSPF Version 2

Overview

Positive

what Ze has

Neutral

measures that are neither good news nor bad

Negative

what Ze owes

The 8 shares marked as a part above are the whole of the 52 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.

At a glance

Enrolment

Enrolled: OSPF Version 2

What the public ledger says

Status: Partial

Coverage

Positive and negative tests (50): RFC2328-A.3.1-1, RFC2328-A.3.1-2, RFC2328-12.1.7-1, RFC2328-13-1, RFC2328-13-2, RFC2328-13-3, RFC2328-13.1-1, RFC2328-13-4, RFC2328-13.3-1, RFC2328-13.3-2, RFC2328-14-1, RFC2328-14-2, RFC2328-13.5-1, RFC2328-13.4-1, RFC2328-16.1-1, RFC2328-16.4-1, RFC2328-16.2-1, RFC2328-16.2-2, RFC2328-D.2-1, RFC2328-D.3-1, RFC2328-D.3-2, RFC2328-A.3.3-1, RFC2328-10.1-1, RFC2328-10.2-1, RFC2328-C.3-1, RFC2328-3.6-1, RFC2328-4.4-1, RFC2328-4.4-2, RFC2328-4.4-3, RFC2328-8.2-1, RFC2328-8.2-2, RFC2328-8.2-3, RFC2328-9.1-1, RFC2328-9.5.1-1, RFC2328-10.5-1, RFC2328-10.6-1, RFC2328-12.1.6-1, RFC2328-12.2-1, RFC2328-12.4-1, RFC2328-12.4.1-1, RFC2328-12.4.3-1, RFC2328-13-5, RFC2328-13-6, RFC2328-13-7, RFC2328-13.3-3, RFC2328-15-2, RFC2328-16.1-3, RFC2328-A.1-1, RFC2328-A.1-2, RFC2328-A.4.4-1

Annotated (including scoped evidence) (2): RFC2328-D.4.3-1, RFC2328-8.1-1

Requirements

Gaps and untested MUSTs

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.

RFC2328-A.3.1-1

The version number field must specify protocol version 2. (§8.2)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: accepting or emitting a Version other than 2. Red: TestOSPFHeaderRejectsBadVersionAndLength fails unless DecodeHeader returns ErrBadVersion for Version 3. Other polarity: TestOSPFHeaderRoundTrip fails unless every packet type written by WriteTo decodes, which needs the emitted Version octet to equal 2. One clause, both polarities.

RFC2328-A.3.1-2

The standard IP checksum of the entire contents of the packet, starting with the OSPF packet header but excluding the 64-bit authentication field. (§A.3.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. c20 judge: independent arithmetic (test-side RFC 1071 fold) for both sides. TestRFC2328PacketChecksumCoversHeaderExcludesAuth: with a simple password the generated field equals the reference over header+body excluding Auth, differs from the whole-packet sum, is unchanged by another password and moves with the Router ID. TestRFC2328PacketChecksumWrongRangeRefused: VerifyPacketChecksum refuses an Auth-included and a body-excluded checksum, accepts the correct one. Revert records PacketChecksum (+), VerifyPacketChecksum (-).

RFC2328-12.1.7-1

This field is the checksum of the complete contents of the LSA, excepting the LS age field. The LS age field is excepted so that an LSA's age can be incremented without updating the checksum. The checksum used is the same that is used for ISO connectionless datagrams; it is commonly referred to as the Fletcher checksum. It is documented in Annex B of [Ref6]. The LSA header also contains the length of the LSA in bytes; subtracting the size of the LS age field (two bytes) yields the amount of data to checksum. The checksum is used to detect data corruption of an LSA. This corruption can occur while an LSA is being flooded, or while it is being held in a router's memory. The LS checksum field cannot take on the value of zero; the occurrence of such a value should be considered a checksum failure. In other words, calculation of the checksum is not optional. (§12.1.7)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: (a) checksum covering LS age: TestOSPFLSAChecksumExcludesAge fails when the LS age octets are mutated and the LSA stops verifying, and TestOSPFLSAChecksum checks independent Fletcher sums over lsa[2:length] (not VerifyLSAChecksum's shared code); (b) an unchecked covered region: mutating Options must fail VerifyLSAChecksum; (c) accepting LS Checksum 0: TestRFC2328ZeroLSChecksumRejected solves the Fletcher sums to zero with the field zero, so only the zero rule can reject, and fails if VerifyLSAChecksum accepts it. Positive: the encoded LSA verifies with a non-zero backfilled checksum. Every clause has its assertion. Re-judged 2026-09-27 after the RFC905-x-6 tags moved here (J102). TestOSPFLSAChecksumExcludesAge now also carries the negative tag for the covered-octet mutation, clause (b). TestFletcherRFC905Vectors and TestFletcherIgnoresLSAge (ospf/types) add positives: the first pins 0x15ff over the window from Options, and the second shows LS Age mutation leaves the checksum unchanged. The verdict is unchanged.

RFC2328-13-1

Validate the LSA's LS checksum. If the checksum turns out to be invalid, discard the LSA and get the next one from the Link State Update packet. (2) Examine the LSA's LS type. If the LS type is unknown, discard the LSA and get the next one from the Link State Update Packet. (§13)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged 2026-10-12 (independent auditor). SHIFTED by 6e063fb498 (tests: give ten assert-nothing tests a real assertion), whose hunks sit in untagged sibling tests and the import block. The tagged unit is byte-identical (gate-verified) and no helper it calls changed. Verdict stands. Both steps proven on the real wire path: TestRFC2328DiscardedLSAThenNextLSAProcessed encodes one LS Update (bad-checksum LSA, or LS type 6 with a valid Fletcher, then a good router-LSA) and dispatches it through the engine from an Exchange neighbor; the bad LSA is neither stored nor acknowledged and the next is installed and acknowledged. Red against the pre-fix producers (ReceiveUpdate returned on the first bad checksum; DecodeLSUpdate failed the whole packet on an unknown type). D-8 fix read at the producer: LSAIterator.Next advances at least 20 octets per pass and a truncated or short Length still ends the packet with an error (fuzzed 20 s each, iterator and DecodePacket); skipped LSAs count against # LSAs. The DecodeLSReq unit lost its 13-1 tag (LS Request decoder, D-15).

RFC2328-13-2

AS-external-LSAs are not flooded into/throughout stub areas (§13)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged 2026-10-12 (independent auditor). SHIFTED by 6e063fb498 (tests: give ten assert-nothing tests a real assertion), whose hunks sit in untagged sibling tests and the import block. The tagged unit is byte-identical (gate-verified) and no helper it calls changed. Verdict stands. c20 judge: both clauses on the real flood path. Into: TestRFC2328ASExternalNotFloodedIntoStubArea, four-area ABR, Type-5 received on eth0 and self-originated, reaches the normal-area control eth3 and never leaves the stub eth1 or NSSA eth2, no stub/NSSA retransmission entry (red with eligibleInterface reverted). Throughout: TestRFC2328ASExternalFromStubInterfaceGoesNowhere, Type-5 from the stub/NSSA neighbor not installed and flooded out no interface, eth1 back included (red with shouldDropByArea reverted). Old helper-only units kept as supplementary. Helper rename by sed re-read: lsaFloodedOn consistent, no leftover.

RFC2328-13-3

If the neighbor is in a lesser state than Exchange, the packet should be dropped without further processing. (§13)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Engine drop now exercised: LS Updates dispatched through eng.dispatch from an unknown neighbor, Init, and ExStart are not stored and draw no LS Ack or LS Update even after FlushDelayedAcks; the same packet after Exchange is installed and acknowledged. Disabling the AcceptsFlooding drop in handleLSUpdate turns all three negatives red. 2-Way (not reachable on point-to-point) stays on the neighbor-package AcceptsFlooding units, which gate the same call.

RFC2328-13.1-1

The LSA having the newer LS sequence number is more recent. See Section 12.1.6 for an explanation of the LS sequence number space. If both instances have the same LS sequence number, then: o If the two instances have different LS checksums, then the instance having the larger LS checksum (when considered as a 16-bit unsigned integer) is considered more recent. o Else, if only one of the instances has its LS age field set to MaxAge, the instance of age MaxAge is considered to be more recent. o Else, if the LS age fields of the two instances differ by more than MaxAgeDiff, the instance having the smaller (younger) LS age is considered to be more recent. (§13.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. c20 judge: order and signedness now discriminated. TestRFC2328FreshnessStepsAppliedInOrder pits an earlier step against a later one in both argument orders (sequence over checksum+MaxAge, unsigned 0x8001 over 0x7FFF against MaxAge, MaxAge over age, age > MaxAgeDiff, MaxSequenceNumber over InitialSequenceNumber signed); TestRFC2328LessRecentByEarlierStepRefused through ReceiveUpdate (past MinLSArrival) keeps the database copy against a lower sequence or smaller checksum at MaxAge. Matrix and Older-sequence units kept. Revert records both polarities on CompareHeaders; author overlays (order swaps, signed checksum, unsigned sequence) red.

RFC2328-13-4

If the database copy has LS age equal to MaxAge and LS sequence number equal to MaxSequenceNumber, simply discard the received LSA without acknowledging it. (§13)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: acknowledging, or sending the database copy back for, an LSA received while the database copy is MaxAge at MaxSequenceNumber. Red: TestOSPFMaxSeqMaxAgeSilentDiscard installs a MaxSequenceNumber copy aged to MaxAge, receives an older instance, flushes delayed acks, and fails on any send. Other polarity: TestRFC2328OlderInstanceGetsDatabaseCopyBack fails if an ordinary more-recent copy is not sent back to the sender (so a blanket silent discard goes red). One clause, both polarities.

RFC2328-13.3-1

LSAs flooded out an adjacency are placed on the adjacency's Link state retransmission list. In order to ensure that flooding is reliable, these LSAs are retransmitted until they are acknowledged. The length of time between retransmissions is a configurable per-interface value, RxmtInterval. (§13.6)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged 2026-10-12 (independent auditor). SHIFTED by 6e063fb498 (tests: give ten assert-nothing tests a real assertion), whose hunks sit in untagged sibling tests and the import block. The tagged unit is byte-identical (gate-verified) and no helper it calls changed. Verdict stands. Clauses: (a) flooded LSAs go on the adjacency's retransmission list: TestOSPFFloodOutOtherInterfaces + (eth1 Full neighbor queued; record on queueRetransmit observed red) and TestOSPFFloodQueuesExchangeAndLoadingNeighbors - (2-Way and the receiving neighbor never queued; record on isFloodEligibleNeighborState observed red). (b) retransmitted until acknowledged, every configurable per-interface RxmtInterval: TestRFC2328RetransmitEveryConfiguredRxmtInterval parses a real OSPFv2 config (eth1 retransmit-interval 3, eth2 11, eth0 default), takes RxmtInterval from engine.lsdbTopology, floods via ReceiveUpdate and ticks RetransmitTick each second 1..24: + eth1 at 3,6,9,12 and eth2 at 11,22 (repeated, per interface); - nothing on any other second, so a hard-coded 5 s or a single retransmission fails, and after eth1's ack at 12 no eth1 resend at 15..24 while unacknowledged eth2 still resends at 22. Exact per-second set compared, buffers isolated (one LSA, one neighbor per interface). TestOSPFRetransmitTimer keeps its earlier default-interval pin. Records on RetransmitTick observed red for both polarities.

RFC2328-13.3-2

The LSA's LS age must be incremented by InfTransDelay (which must be > 0) when it is copied into the outgoing Link State Update packet (until the LS age field reaches the maximum value of MaxAge). (§13.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Clauses: LS age incremented by InfTransDelay and capped at MaxAge: TestRFC2328FloodIncrementsAgeByInfTransDelay (unchanged; records on floodCopy). The '(which must be > 0)' clause: TestRFC2328TransmitDelayMustBePositive + an OSPFv2 interface with transmit-delay 1 accepted by validateConfig, - transmit-delay 0 refused with ErrTransmitDelayZero (the config.go validateConfigAF check that production reaches through register.go validateConfig); each case its own single-interface config, so the refusal is this rule's and no other. Records on validateConfigAF observed red for both polarities.

RFC2328-14-1

An LSA's LS age is never incremented past the value MaxAge. LSAs having age MaxAge are not used in the routing table calculation. (§14)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: (a) LS age incremented past MaxAge: TestLSAgeAddSaturates fails unless MaxAge-10 plus 20 equals MaxAge exactly, and TestOSPFLSDBAgeToPurge fails unless the aged LSA sits at MaxAge; (b) a MaxAge LSA used in the routing calculation: TestOSPFGraphSkipsMaxAge fails if BuildGraph makes a router vertex of a MaxAge router-LSA. The fixture is isolated: BuildGraph (graph.go) turns a decodable non-MaxAge router-LSA into a vertex with no other filter, so only the age check can exclude it. Positive: age advances and saturation leaves DoNotAge untouched.

RFC2328-14-2

A MaxAge LSA must be removed immediately from the router's link state database as soon as both a) it is no longer contained on any neighbor Link state retransmission lists and b) none of the router's neighbors are in states Exchange or Loading. (§14)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged 2026-10-12 (independent auditor). SHIFTED by 6e063fb498 (tests: give ten assert-nothing tests a real assertion), whose hunks sit in untagged sibling tests and the import block. The tagged unit is byte-identical (gate-verified) and no helper it calls changed. Verdict stands. Clause (b) now holds Exchange as well as Loading: a purged MaxAge LSA on no retransmission list is kept with the only neighbor in exchange or loading and removed at once in full or exstart; a Loading-only guard turns the exchange subtest red while the older Loading unit stays green. Clause (a) stays on the retransmission-list units. The units call deletePurgedIfAcked directly, the LSDB seam every trigger uses.

RFC2328-13.5-1

Each newly received LSA must be acknowledged. This is usually done by sending Link State Acknowledgment packets. However, acknowledgments can also be accomplished implicitly by sending Link State Update packets (see step 7a of Section 13). (§13.5)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged 2026-10-12 (independent auditor). SHIFTED by 6e063fb498 (tests: give ten assert-nothing tests a real assertion), whose hunks sit in untagged sibling tests and the import block. The tagged unit is byte-identical (gate-verified) and no helper it calls changed. Verdict stands. c20 judge: TestRFC2328NewerLSAAcknowledgedThroughReceiveUpdate reaches the ordinary newer-LSA ack through ReceiveUpdate, not hand-set flags: point-to-point, DROther and Backup (from the DR) each send an LS Ack carrying the header on eth0 after FlushDelayedAcks; the DR receiving from a DROther acks implicitly by flooding back out eth0. Negative TestOSPFDRRefloodsBackOutReceivingInterface (flooded back, implicit ack, no explicit ack, Table 19) now carries a judge-observed revert record on ackForReceive. Direct ack of unknown MaxAge held by TestOSPFUnknownMaxAgeNoCopyIsAckedAndDiscarded.

RFC2328-13.4-1

A self-originated LSA is detected when either 1) the LSA's Advertising Router is equal to the router's own Router ID or 2) the LSA is a network- LSA and its Link State ID is equal to one of the router's own IP interface addresses. (§13.4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Both detection rules through ReceiveUpdate: router-LSA adv = own Router ID, and network-LSAs from 9.9.9.9 whose LSID is either own interface address, are each installed at MaxAge with sequence+1 and flooded at MaxAge. Negatives: a network-LSA with a foreign LSID, another router's router-LSA, and an AS-external whose LSID equals an own address (rule 2 is network-LSA only) are installed as received and never flushed. Disabling rule 2, or dropping its type check, turns the matching subtests red.

RFC2328-16.1-1

Look up the vertex W's LSA (router-LSA or network-LSA) in Area A's link state database. If the LSA does not exist, or its LS age is equal to MaxAge, or it does not have a link back to vertex V, examine the next link in V's LSA. (§16.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. c20 judge: every skip clause and the continuation. TestRFC2328SPFExaminesNextLinkAfterSkip: root lists links to a missing router-LSA, a MaxAge router-LSA, a router with no link back, and a transit net with no network-LSA BEFORE 5.5.5.5, which is still reached at 10 with only 192.0.2.0/24 at 15 routed. TestRFC2328SPFSkipsMissingOrMaxAgeVertex isolates missing/MaxAge for router and network LSAs with a below-MaxAge control. Link-back clause by TestOSPFSPFShortestPath / TestOSPFTwoWayCheck. Revert records Compute (+), BuildGraph (-).

RFC2328-16.4-1

Intra-area and inter-area paths are always preferred over AS external paths. (b) Type 1 external paths are always preferred over type 2 external paths. When all paths are type 2 external paths, the paths with the smallest advertised type 2 metric are always preferred. (§16.4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. All four orderings asserted: intra over external (route_test), inter-area at 100 over E1 and E2 at 1 (selectBestRoutes, both input orders), E1 over E2 regardless of metric (external_test), and among E2 the smallest advertised metric (7 via an ASBR 50 away) over 9 via an ASBR 1 away through ComputeExternal. Ranking inter-area below externals, or letting distance decide E2, turns the new units red.

RFC2328-16.2-1

If the router is attached to multiple areas (i.e., it is an area border router), only backbone summary-LSAs are examined. (§16)

Audit verdict: enforced (the tests do what the requirement demands), fresh. c20 judge: the 'attached to multiple areas' condition now discriminated: TestRFC2328NonABRUsesItsAreaSummaries, a router in area 0.0.0.1 only installs 10.40.0.0/24 from that area's summary at 2 via 3.3.3.3 (red under a backbone-only-for-every-router producer). Negative TestOSPFABRBackboneOnlyAcceptance: the ABR ignores the cheaper area-1 summary, metric 30 via 2.2.2.2; judge-observed revert record on ComputeInterAreaWith.

RFC2328-16.2-2

If the cost specified by the LSA is LSInfinity, or if the LSA's LS age is equal to MaxAge, then examine the the next LSA. (2) If the LSA was originated by the calculating router itself, examine the next LSA. (§16.2)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Closes the earlier gap (advertised LSInfinity unfed). + TestRFC2328SummaryAdvertisingLSInfinitySkipped: summary cost 20 through an ABR 10 away installs one route; - the same summary with cost LSInfinity installs none. MaxAge and self-originated skips stay on rfc2328_test.go; composed-cost saturation on interarea_test. Records: + v4SummaryReader, - ComputeInterAreaWith, observed red. Note: the advertised-cost check (v4SummaryReader, interarea.go:189) is subsumed by the composed-cost check (ComputeInterAreaWith, interarea.go:153), because clampMetric saturates any sum with an LSInfinity term to LSInfinity; a mutant removing only :189 stays green, but no input then installs a route, so the behaviour the clause demands is enforced by the unit either way. The AS-external tags on external_test/rfc2328_test prove s16.4 neighbours and are supplementary.

RFC2328-D.2-1

The 64-bit authentication field in the OSPF packet header must be equal to the 64-bit password (i.e., authentication key) that has been configured for the interface. (§D.5.2)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: accepting a Simple-password packet whose 64-bit authentication field differs from the configured password. Red: TestRFC2328SimplePasswordMismatchDiscarded fails if a packet signed with 'badpass' is accepted, and fails unless the reason is exactly password-mismatch (isolated: the AuType matches). Other polarity: the same unit fails if the configured 'goodpass' is rejected. One clause, both polarities.

RFC2328-D.3-1

The message digest appended to the OSPF packet is not actually considered part of the OSPF protocol packet: the message digest is not included in the OSPF header's packet length, although it is included in the packet's IP header length field. (§D.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. c21 judge (independent). Clause 1 (digest not in Packet Length): TestOSPFAuthSignVerifyCrypto fails unless Packet Length stays plen and len(signed) == plen + digest. Clause 2 (digest in the IP length): new TestRFC2328DigestCountedInIPLengthNotPacketLength, both send paths (SendPacket, SendPacketRouted) with packet.Sign keyed MD5 as signer: the socket receives 44+16 octets, Packet Length still 44, trailer equals an independent D.4.3 MD5; a raw proto-89 socket (backend_linux Sendto, no IP_HDRINCL) builds the IP header around exactly that payload. Trim-after-signer overlay red on both subtests (author log, judge diffed the overlay); record on SendPacket observed red. engine.signPacket returns Sign output unchanged and its framing is pinned by the untagged TestEngineSignPacketCrypto Verify round-trip (Verify requires plen+L == len). Negative TestOSPFAuthCryptoRejectsExtraTrailerBytes refuses a wire whose trailer exceeds the digest framing, now with a Verify record observed red.

RFC2328-D.3-2

Whenever an OSPF packet is accepted as authentic, the cryptographic sequence number is set to the received packet's sequence number. (§D.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: an authentic packet's sequence number not becoming the stored value, and an AuType 2 sequence treated as anything but non-decreasing. Red: TestOSPFAuthReplay accepts 10 then 11, accepts a second 11 (D.4.3 discards only 'less than'), then rejects 10 with reason replay, which holds only if 11 (not 10) was stored; 5 is rejected. TestOSPFAuthReplayEqualSequenceByAuType asserts the AuType 2 equal-sequence acceptance on its own. TestNeighborDownResetsCryptoSeq adds the per-neighbor reset. RFC 7474's strictly-greater rule governs only its AuType 3 (replayedSequence).

RFC2328-D.4.3-1

The checksum field in the standard OSPF header is not calculated, but is instead set to 0. (§D.4.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Non-compliant behaviour: an AuType 2 packet whose standard-header Checksum is calculated rather than set to 0. TestOSPFPacketChecksumZeroForAuType2 encodes a cryptographic-auth Hello through WriteTo and fails ('AuType2 checksum = %#04x, want 0') on any non-zero field. Single-polarity positive per the row's marker: the rule is generate-side and there is no receive path to reject.

RFC2328-A.3.3-1

Interface MTU should be set to 0 in Database Description packets sent over virtual links. (§A.3.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: a DD sent over a virtual link carrying a non-zero Interface MTU. Red: TestRFC2328VirtualLinkDBDescCarriesZeroMTU fails on any sent DD with InterfaceMTU != 0 over the MTU-less virtual interface, and TestRFC2328VirtualInterfaceHasNoMTU fails unless the engine-created virtual interface reports MTU 0 (so the DD stamps 0). Other polarity: the same units fail unless a real interface's DD carries 1500 and the real interface reports a non-zero MTU, so a blanket zero goes red.

RFC2328-10.1-1

Only one Database Description Packet is allowed outstanding at any one time. (§10.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged c18. Forbidden: a second DD leaving the master while one is unacknowledged. Setup gives the master (10.0.0.3) a summary list longer than one DD, so a non-compliant master has a DD n+1 to send. Positive TestRFC2328MasterHoldsOneOutstandingDD: three RxmtInterval expiries each send exactly one packet, DD n unchanged (sameDD), exactly three DDs all seq n; the slave DD acking n releases exactly one DD n+1 with the remaining 3 headers. Negative TestRFC2328MasterSendsNoSecondDDWithoutAck: a repeat of the slave's previous DD -> duplicate-drop with nothing sent; a slave DD n+2 -> SeqNumberMismatch and an Init DD; no non-Init DD n+1 is ever sent. Records: + resendLastDDLocked, - handleExchangeDDLocked, observed red. Old nsm_test tags kept as supplementary; TestOSPFDuplicateDD (negative) proves the slave's 10.8 duplicate, a neighbour, and carries no weight here.

RFC2328-10.2-1

If an LSA cannot be found in the database, something has gone wrong with the Database Exchange process, and neighbor event BadLSReq should be generated. (§10.7)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: an LS Request for an LSA absent from the database not generating BadLSReq. Red: TestOSPFBadLSReqRestart fails on HandleLSReq != reasonBadLSReq, on state != exstart, and on the resent DD not being the initial I|M|MS DD. Other polarity: TestOSPFValidLSReqSendsLSUpdate and TestRFC2328KnownLSRequestDoesNotRestartExchange go red if a satisfiable request restarts the exchange (state change, exstart) or is not answered with one LS Update carrying that LSA. One clause, both polarities.

RFC2328-C.3-1

The interface output cost must always be greater than 0. (§C.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged 2026-09-29 (independent judge). Explicit cost 0 stays refused (TestInterfaceCostAndTransmitDelayBoundary). The unset-cost gap is closed: TestRFC2328DefaultedInterfaceCostIsPositive resolves interfaces from config text with no cost leaf and reads interfaceCost, the one producer every consumer uses (instance.go Router-LSA and routing-table cost, ldp_sync.go, te_originate.go): 1 Gbit/s under 100 Gbit/s -> 100, and the inputs that divide to 0 (100 Gbit/s under a 1 Mbit/s reference, unknown speed) -> 1. Records: revert on interfaceCost (positive) and on DefaultMetric (negative); a mutant dropping DefaultMetric's MetricMin clamp would be sharper.

RFC2328-3.6-1

One or more of the stub area's area border routers must advertise a default route into the stub area via summary-LSAs. (§3.6)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: an ABR attached to a stub area not advertising a default route into it via a summary-LSA. Red: TestRFC2328StubAreaGetsDefaultSummary fails unless the stub area holds a Type 3 summary with Link State ID 0.0.0.0, mask 0.0.0.0 and the configured cost 5. Other polarity: TestRFC2328NormalAreaGetsNoDefaultSummary fails if a normal area receives one, and still checks the ordinary summary is originated. One clause, both polarities.

RFC2328-4.4-1

Support for receiving and sending IP multicast datagrams, along with the appropriate lower-level protocol support, is required. (§4.4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged 2026-10-12 (independent auditor). SHIFTED by 6e063fb498 (tests: give ten assert-nothing tests a real assertion), whose hunks sit in untagged sibling tests and the import block. The tagged unit is byte-identical (gate-verified) and no helper it calls changed. Verdict stands. Independent judgment: RFC 2328 section 4.4 says, "Support for receiving and sending IP multicast datagrams, along with the appropriate lower-level protocol support, is required." The production raw protocol-89 backend now has proof on both sides: TestOSPFTransportVethMulticastRoundTrip reads IP_MULTICAST_IF == 192.0.2.1 and TTL 1, sends AllSPFRouters over a real veth into a peer namespace, and asserts receiving interface, source and exact payload. TestOSPFTransportAllDRoutersReceive first receives on that same link, leaves AllDRouters and requires subsequent delivery to be absent. The original duplicate-join/drop errno assertions prove actual socket membership installation/removal; the foreign-group refusal is supplementary OSPF API confinement, not a general IP multicast forwarding obligation. Inspected runInNS: caller pins its thread, namespace entry and deferred restoration each load the real netlink backend, LoadBackend closes the old counter socket and the replacement lazily opens in its lookup namespace; no fake resolver bypass. Inspected four native recorded producer-halt observations and fresh records. This proves Ze's configured socket/send/receive boundary, not Linux multicast forwarding (expressly not required by this section). No new judge test run.

RFC2328-4.4-2

The router's IP protocol support must include the ability to divide a single IP class A, B, or C network number into many subnets of various sizes. This is commonly called variable-length subnetting; see Section 3.5 for details. IP supernetting support The router's IP protocol support must include the ability to aggregate contiguous collections of IP class A, B, and C networks into larger quantities called supernets. (§4.4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: a classful routing table (mask derived from address class) that cannot carry variable-length subnets or supernets. Red: TestRFC2328ClasslessPrefixesReachIPRIB fails unless 192.0.0.0/16 (a supernet of class-C networks), 192.0.2.0/24 and 192.0.2.128/25 (a variable-length subnet) each reach the IP Loc-RIB with its own next hop. Other polarity: TestRFC2328ClasslessWithdrawalPreservesOverlaps fails if withdrawing the /24 removes the /16 or the /25. Both the VLSM and the supernet clause have a prefix that a classful table would lose.

RFC2328-4.4-3

Indications must be passed from these protocols to OSPF as the network interface goes up and down. (§4.4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. c21 judge (independent). New positive TestRFC2328LinkIndicationsReachTheOSPFEngine builds the engine over the real transport.New(fakeBackend): an up neighbor on p2p eth0, then Transport.HandleLinkDown puts the OSPF interface in Down and the neighbor in down, and HandleLinkUp brings a running eth0 back to Point-to-point. Judge diffed the overlay that drops only instance.go OnInterfaceDown registration: red "state point-to-point, want Down"; dropping both registrations reds at setup while the transport-level TestOSPFTransportPassesLinkIndicationsToOSPF stays green, which was the old gap. Record on onInterfaceDown observed red. Transport-level positive kept. Negative TestOSPFTransportPassesNoIndicationForNonOSPFInterface: a non-OSPF interface link-up/down passes no indication, recorded.

RFC2328-8.1-1

On these interfaces, the IP source should be set to any of the other IP addresses belonging to the router. For this reason, there must be at least one IP address assigned to the router. (§8.1)

Audit verdict: unimplemented (no code path enforces the requirement), fresh. Re-judged 2026-10-02 under OWNER RULING 8 (g) (the stamping agent authored neither test). Section 8.1: 'Interfaces to unnumbered point-to-point networks have no associated IP address. On these interfaces, the IP source should be set to any of the other IP addresses belonging to the router.' Ze does not implement unnumbered point-to-point interfaces: transport/backend_linux.go::interfaceIPv4 sources OSPF packets from the interface's own IPv4 address and refuses an interface without one, and no config or ifIndex LinkData exists for an unnumbered link, so no layer performs the sourcing rule. The row carries {gap} citing owner ruling 8 (g) and the rfc2328 Support remaining text discloses it. The two former tags (TestResolveOSPFInterfaceUsesIfaceResolverOSName +, TestOSPFRefusesInterfaceWithoutIPv4Source -) proved no clause of the quote and left the row under D-15 approvals citing owner ruling 8; the tests and their assertions stay as Ze's numbered-interface rule. Recording the gap authorizes no unnumbered implementation.

No test carries RFC2328-8.1-1, so no unit is bound to it.

RFC2328-8.2-1

In order for the packet to be accepted at the IP level, it must pass a number of tests, even before the packet is passed to OSPF for processing: o The IP checksum must be correct. o The packet's IP destination address must be the IP address of the receiving interface, or one of the IP multicast addresses AllSPFRouters or AllDRouters. o The IP protocol specified must be OSPF (89). (§8.2)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Each listed test has both polarities through deliverDatagram, the Linux receive path. IP checksum: the 'checksum' case fails if a datagram with a broken header checksum is delivered. Destination: accepted for the interface address, AllSPFRouters and AllDRouters (TestOSPFReceiveAcceptsValidIPv4Envelope fails if any is rejected or not delivered), 'destination' case fails if a foreign address is delivered. Protocol: 'protocol' case (17) fails if delivered, while the valid datagrams carry 89. Rejections also assert one drop recorded and nothing on recvCh.

RFC2328-8.2-2

The Area ID found in the OSPF header must be verified. If both of the following cases fail, the packet should be discarded. The Area ID specified in the header must either: (1) Match the Area ID of the receiving interface. In this case, the packet has been sent over a single hop. Therefore, the packet's IP source address is required to be on the same network as the receiving interface. This can be verified by comparing the packet's IP source address to the interface's IP address, after masking both addresses with the interface mask. This comparison should not be performed on point-to-point networks. On point-to-point networks, the interface addresses of each end of the link are assigned independently, if they are assigned at all. (2) Indicate the backbone. In this case, the packet has been sent over a virtual link. The receiving router must be an area border router, and the Router ID specified in the packet (the source router) must be the other end of a configured virtual link. The receiving interface must also attach to the virtual link's configured Transit area. (§8.2)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged 2026-09-30 (independent judge, c10/c11). Case (1) as the prior judgement: Area-ID clause TestOSPFReceiveAcceptsMatchingAreaID + / TestOSPFReceiveDropsMismatchedAreaID -; source clause under the interface mask TestOSPFReceiveDropsOffNetworkSourceOnBroadcast -, TestOSPFReceiveAcceptsOnNetworkSourceOnBroadcast +, point-to-point skip TestOSPFReceiveAcceptsOffNetworkSourceOnPointToPoint +. Case (2), the gap of the prior verdict, now proven through engine.acceptsArea on an ABR fixture (eth0 transit 0.0.0.1, eth1 backbone, eth2 0.0.0.2, VL to 10.0.0.2 resolved): TestRFC2328VirtualLinkAreaIDAccepted + (backbone header from the VL endpoint on the Transit-area interface accepted); TestRFC2328VirtualLinkAreaIDRefused - with one assertion per clause, each discriminated by a targeted overlay mutants (go test -overlay, tree untouched, scratch/ospf-judge-mut) of virtualLinkTargetLocked: dropping the backbone check -> red at the non-backbone 0.0.0.2 assertion; dropping the neighbor Router ID match -> red at the 9.9.9.9 assertion; dropping the Transit-area match -> red at the eth2 assertion. The recorded negative red is the panic stub; these mutants are the clause-level evidence. 'Receiving router must be an ABR' is structural: a configured virtual link attaches the router to the backbone, and no separate refusal path exists. Behaviour note (R42, documented in ospf-4-component-config.md): only the interface's first IPv4 address/prefix forms the OSPF interface, so a neighbour on a secondary subnet is dropped.

RFC2328-8.2-3

The AuType specified in the packet must match the AuType specified for the associated area. (§8.2)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged 2026-09-29 (independent judge). Isolation gap closed and a product defect fixed (D-8): TestRFC2328NullAuTypeIntoPasswordAreaDroppedForAuType asserts the single auth failure carries reason 'autype-mismatch', not a password failure; TestRFC2328PasswordAuTypeIntoNullAreaDropped sends a Hello signed AuType 1 into a Null-auth interface and asserts the drop and no neighbor (red before the fix: dropped 0). Producer checked: authStore.verify now refuses any non-Null AuType on an interface with no key chain, RFC 2328 s8.2 quoted above the check; revert records on verify. Positive TestOSPFReceiveAcceptsMatchingAuType unchanged.

RFC2328-9.1-1

The router must also originate a network-LSA for the network node. (§9.1, §12.4.2)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: the Designated Router for a network not originating its network-LSA. Red: TestRFC2328DROriginatesNetworkLSA fails unless OriginateFromTopology produces a network-LSA for eth1 (where 1.1.1.1 is DR) listing exactly [1.1.1.1 3.3.3.3]. Other polarity: TestRFC2328NonDROriginatesNoNetworkLSA fails if the Backup on eth0 originates one. One clause, both polarities.

RFC2328-9.5.1-1

If the router is eligible to become Designated Router, it must periodically send Hello Packets to all neighbors that are also eligible. In addition, if the router is itself the Designated Router or Backup Designated Router, it must also send periodic Hello Packets to all other neighbors. This means that any two eligible routers are always exchanging Hello Packets, which is necessary for the correct operation of the Designated Router election algorithm. To minimize the number of Hello Packets sent, the number of eligible routers on an NBMA network should be kept small. If the router is not eligible to become Designated Router, it must periodically send Hello Packets to both the Designated Router and the Backup Designated Router (if they exist). (§9.5.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. c20 judge: eligible router to every eligible neighbor (TestOSPFNBMAEligibleRouterHellosEveryEligibleNeighbor) and DROther skipping priority-0 neighbors (negative TestOSPFNBMAPeriodicHelloSkipsIneligibleNeighbor); DR and Backup sending to the priority-0 neighbor too (TestRFC2328NBMAHelloTargetsByRole dr/backup, red under an overlay gating priority-0 in every state). Ineligible-router clause: the subtest asserts a priority-0 DROther targets both DR and BDR; no producer branch reads the router's own priority (it sends to every eligible neighbor, a superset the sentence allows), so no targeted overlay exists; the assertion fails on any producer that drops DR or BDR from that router's targets, and the unit's revert record is observed red. Single positive for that clause is the sentence's own shape (no MUST NOT).

RFC2328-10.5-1

Next, the values of the Network Mask, HelloInterval, and RouterDeadInterval fields in the received Hello packet must be checked against the values configured for the receiving interface. Any mismatch causes processing to stop and the packet to be dropped. (§10.5)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: accepting a Hello whose Network Mask, HelloInterval or RouterDeadInterval differs from the receiving interface. Red: TestRFC2328HelloMismatchRejectedAndNoTwoWayUnlisted mutates each of the three fields separately and fails unless ReceiveHello returns that field's drop reason and no neighbor is created (processing stopped). Other polarity: TestRFC2328HelloMatchingParametersAndTwoWay fails if a matching Hello is refused. Every listed field has its own case.

RFC2328-10.6-1

In states Loading and Full the slave must resend its last Database Description packet in response to duplicate Database Description packets received from the master. For this reason the slave must wait RouterDeadInterval seconds before freeing the last Database Description packet. (§10.8)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged c18. Clauses: (1) in Loading and Full the slave resends its last DD for a duplicate of the master's DD, (2) it keeps that DD RouterDeadInterval before freeing. Positive TestRFC2328SlaveResendsLastDDInLoadingAndFull (Loading and Full subtests): a duplicate of the master's last DD at 0 s and at RouterDeadInterval-1 s (table clock, aligned with the exchange at Unix(1,0)) gets exactly one packet, the slave's last DD (sameDD), state unchanged. Negative TestRFC2328SlaveRepeatsOnlyForTheLastMasterDD: the master's earlier Init DD 99 or a new DD 101 in Loading/Full -> SeqNumberMismatch, ExStart, next DD Init, never the slave's last DD. Records: + resendLastDDLocked, - sameDD and handleExchangeDDLocked, observed red. Retention read at the producer: lastSentDD is assigned only in dd.go and reset only on exchange restart/teardown, never on a timer, so no early-free path exists; the -1 s probe catches a time check on the receive path, not a timer-driven free, which no code has.

RFC2328-12.1.6-1

When an attempt is made to increment the sequence number past the maximum value of N - 1 (0x7fffffff; also referred to as MaxSequenceNumber), the current instance of the LSA must first be flushed from the routing domain. This is done by prematurely aging the LSA (see Section 14.1) and reflooding it. As soon as this flood has been acknowledged by all adjacent neighbors, a new instance can be originated with sequence number of InitialSequenceNumber. (§12.1.6)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged c18. Clauses: (1) flush by premature aging AND reflooding, (2) wait for ALL adjacent neighbors' acks, (3) then originate at InitialSequenceNumber. Positive TestRFC2328SequenceWrapFloodsFlushThenRestarts: the flush is decoded from LS Updates at MaxAge + MaxSequenceNumber out of eth0 AND eth1; after 2.2.2.2 and 3.3.3.3 both ack it is deleted; next origination is InitialSequenceNumber age 0 flooded out of both. Negative TestRFC2328SequenceWrapWaitsForEveryNeighbor (subtest per neighbor): one ack alone leaves it in the database, the next origination is the MaxAge instance at MaxSequenceNumber, and no InitialSequenceNumber instance is flooded, so a restart after the first ack goes red. Records: nextOwnSequenceForce and deletePurgedIfAcked, both polarities, observed red. Old flooding_test tags kept.

RFC2328-12.2-1

An implementation of OSPF must be able to access individual pieces of an area database. This lookup function is based on an LSA's LS type, Link State ID and Advertising Router. (§12.2)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: a lookup that ignores any element of the (LS type, Link State ID, Advertising Router) triple. + TestRFC2328LookupTellsApartLSAsSharingTwoElements: three LSAs from 4.4.4.4 (Router 4.4.4.4; Summary 4.4.4.4 differing only in type; Summary 9.9.9.9 differing only in LSID) each found by its own triple with its own sequence. - TestRFC2328LookupMissesWhenOneElementDiffers: a triple differing in LS type alone, LSID alone, or Advertising Router alone finds nothing. Records on lsdb.go::Lookup observed red; TestRFC2328LookupByTriple/NeedsFullTriple unchanged.

RFC2328-12.4-1

If a router advertises a summary-LSA for a destination which then becomes unreachable, the router must then flush the LSA from the routing domain by setting its age to MaxAge and reflooding (see Section 14.1). (§12.4.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged c18. Forbidden: keeping a self-originated summary-LSA for a destination that became unreachable. TestRFC2328SummaryFlushedWhenDestinationUnreachable drives OriginateSummaries with a real lsdb.LSDB as sink: pass 1 with 2.2.2.2 in the backbone SPF Result originates the Type 3 for 10.20.0.0/24 into 0.0.0.1; pass 2 with 2.2.2.2 unreached sets it to MaxAge AND a decoded LS Update carries it at MaxAge out of eth1, while the reachable 10.10.0.0/24 summary stays below MaxAge. The step from unreachable destination to keep-set exit (collectSummaryNetworks) is now exercised. Negative TestRFC2328SummaryKeptWhileDestinationReachable: two reachable passes leave it below MaxAge with no MaxAge copy flooded. Records: FlushStaleSummaryLSAs both polarities, collectSummaryNetworks negative, observed red. Unreachability is a hand-built SPF Result, not a full SPF run. Old lsdb-seam tags kept.

RFC2328-12.4.1-1

All of the router's links to the area must be described in a single router-LSA. (§A.4.2)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: splitting the area's links over several router-LSAs, or omitting one. Red: TestRFC2328SingleRouterLSACarriesEveryLink fails unless exactly one router-LSA from 1.1.1.1 exists in the area and its body holds a transit link for each of the two interfaces. Other polarity: TestRFC2328RouterLSAExcludesOtherAreaLinks fails if an interface of area 0.0.0.1 is described in the backbone router-LSA, so 'links to the area' is bounded. One clause, both polarities.

RFC2328-12.4.3-1

The router must then originate summary-LSAs into the newly attached area for all pertinent intra-area and inter-area routes in the router's routing table. (§12.4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged 2026-10-02 (independent judge, ospf c27). Section 12.4 event (7): 'The router must then originate summary-LSAs into the newly attached area for all pertinent intra-area and inter-area routes in the router's routing table.' New spf/rfc2328_newly_attached_area_test.go: real LSDB as Source and SummarySink, NewComputer, root 1.1.1.1 p2p to ABR 2.2.2.2; Run with area 0.0.0.1 configured but no Router-LSA of 1.1.1.1 in it (asserted: area holds 0 LSAs), then the area-1 Router-LSA installed (attachment; production triggers SPF via triggerSPF on the LSDB change) and Run again. + TestRFC2328NewlyAttachedAreaGetsIntraAndInterAreaSummaries: Type 3 for backbone intra-area 10.10.0.0/24 metric 7 and inter-area 10.30.0.0/24 metric 30 in area 1. - TestRFC2328NewlyAttachedAreaGetsNoSummaryOfItsOwnRoutes ('pertinent', section 12.4.3): no Type 3 for area 1's own 10.20.0.0/24 into area 1 (present in the backbone, metric 3), no inter-area summary into the backbone. Judge replayed overlays on summaryDesiredForArea: inter-area loop off -> only + red; src==dst skip off -> only - red; inter-area into the backbone -> only - red. Revert records on summaryDesiredForArea observed. HEAD units (range condensation) keep their records.

RFC2328-13-5

Remove the current database copy from all neighbors' Link state retransmission lists. (§13)

Audit verdict: enforced (the tests do what the requirement demands), fresh. TestRFC2328ReplacedInstanceLeavesSenderRetransmitList queues the old instance for 3.3.3.3, then the newer instance arrives FROM 3.3.3.3 so no flood can overwrite that entry; after install the list is empty for the key and a retransmit tick sends nothing on eth1. A no-op removeFromAllRetransmit turns it red while the older positive stays green. Negative: a duplicate leaves other lists intact (unchanged).

RFC2328-13-6

If the contents are different, the following pieces of the routing table must be recalculated, depending on the new LSA's LS type field: Router-LSAs and network-LSAs The entire routing table must be recalculated, starting with the shortest path calculations for each area (not just the area whose link-state database has changed). (§13.2)

Audit verdict: enforced (the tests do what the requirement demands), fresh. c21 judge (independent). Positive TestRFC2328ChangedContentsRecalculateEveryArea drives the production wiring (newEngine -> initSPF: lsdb.SetOnChange -> Computer.TriggerArea -> Run), nothing triggers by hand: a changed router-LSA and a changed network-LSA installed in area 0.0.0.1 each withdraw the neighbor stub 203.0.113.64/26 and move BOTH areas last-run stamps past the settled baseline; not-advertised ranges keep the ABR summary origination from triggering the backbone, so only the 13.2 whole-table behaviour recalculates area 0 (isolated). Judge re-ran the dirty-only Computer.Run overlay: both subtests red "area 0.0.0.0 was not recalculated"; record on TriggerArea observed red. Run is monolithic (every configured area, then summary and external steps), so the entire table follows. TestSPFRecalculatesEveryAreaOnOneAreaChange stays as unit-level supplement. Negative TestSPFRecalculationBoundedToConfiguredAreas bounds the recalculation to configured areas; 13.2 offers no refusal path (unchanged contents is a permission, not an obligation), so the row is judged on its positive, the negative held as supplementary.

RFC2328-13-7

If there is already a database copy, and if the database copy was received via flooding and installed less than MinLSArrival seconds ago, discard the new LSA (without acknowledging it) and examine the next LSA (if any) listed in the Link State Update packet. (§13)

Audit verdict: enforced (the tests do what the requirement demands), fresh. c20 judge: discard without ack and keep the earlier copy proven by TestRFC2328MinLSArrivalDiscardsWithoutAck (negative) and the elapsed case by TestRFC2328MinLSArrivalElapsedAccepts; the 'examine the next LSA' clause now by TestRFC2328TooSoonDiscardThenNextLSAExamined: one LS Update [too-soon 4.4.4.4, new 5.5.5.5], 4.4.4.4 keeps its sequence and is not flooded, 5.5.5.5 installed, flooded and the ONLY header acknowledged. Author overlay (continue->return on the TooSoon branch) red on the new unit only; revert record on ReceiveUpdate.

RFC2328-13.3-3

On non-broadcast networks, separate Link State Update packets must be sent, as unicasts, to each adjacent neighbor (i.e., those in state Exchange or greater). (§13.3)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: on a non-broadcast network, flooding by multicast or omitting a unicast to an adjacent (Exchange or greater) neighbor. Red: TestRFC2328NBMAUnicastsToEachAdjacency fails unless exactly one LS Update goes to each of 10.0.0.2 (Full) and 10.0.0.3 (Exchange); TestRFC2328NBMANeverMulticastsNorReachesTwoWay fails on any send to AllSPFRouters or AllDRouters, or to the 2-Way neighbor 10.0.0.4. Both polarities over floodExcept, the flooding producer.

RFC2328-15-2

The cost of a virtual link is NOT configured. It is defined to be the cost of the intra-area path between the two defining area border routers. This cost appears in the virtual link's corresponding routing table entry. When the cost of a virtual link changes, a new router-LSA should be originated for the backbone area. (§15)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Re-judged 2026-09-30 (independent judge, c10/c11). Prior clauses unchanged: cost = intra-area path cost carried by the routing table entry (spf/TestRFC2328VirtualCostIsTransitPathCost), a cost change originates a new backbone router-LSA (TestRFC2328VirtualCostChangeOriginatesNewInstance, TestRFC2328VirtualCostChangeReoriginatesBackbone +, TestRFC2328VirtualUnusablePathWithdrawsBackboneLink -). The missing MUST clause 'The cost of a virtual link is NOT configured' now has negatives on both virtual-link lists through the operator path (config text -> config.ParseTreeWithYANG over ZeOSPFConfYANG -> ToPluginMap -> parseOSPFConfig): TestRFC2328VirtualLinkCostNotConfigurable (ospf areas area virtual-link) and TestRFC2328VirtualLinkCostNotConfigurableV3 (address-family ipv6, ospf-af-topology grouping), each accepting the link without cost (reaches cfg.VirtualLinks / cfg.V6.VirtualLinks) and refusing `cost 10` with an error naming cost. Their records are no-break declaration-only (the tool cannot mutate an embedded YANG file); the judge observed the red with an overlay mutants (go test -overlay, tree untouched, scratch/ospf-judge-mut) adding `leaf cost { type uint16; }` to both lists of ze-ospf-conf.yang: both units red at the refusal assertion.

RFC2328-16.1-3

Note that when there is a choice of vertices closest to the root, network vertices must be chosen before router vertices in order to necessarily find all equal-cost paths. (§16.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: choosing a router vertex before a network vertex at equal distance. Red: TestRFC2328EqualDistanceNetworkVertexFirst pushes two routers and one network at dist 10 and fails unless the first pop is the network vertex. Other polarity: TestRFC2328CloserRouterVertexBeforeFartherNetwork fails if the network-first preference overrides distance (router at 10 must pop before network at 11). Both over spfHeap, the SPF candidate list itself.

RFC2328-A.1-1

Packets sent to these multicast addresses should never be forwarded; they are meant to travel a single hop only. To ensure that these packets will not travel multiple hops, their IP TTL must be set to 1. (§A.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Forbidden: OSPF packets sent with a TTL other than 1. Red: TestOSPFSocketTTLIsOne first proves the kernel default is not 1, then fails unless IP_TTL and IP_MULTICAST_TTL both read back 1 after setMulticastOptions (which hard-codes 1, backend_linux.go:307-316). Other polarity: TestOSPFSocketTTLFailureIsAnError fails if a setsockopt failure is swallowed, so a socket cannot enter service with the default TTL.

RFC2328-A.1-2

Both the Designated Router and Backup Designated Router must be prepared to receive packets destined to this address. (§A.1)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Both halves now asserted. + TestOSPFElectedDRJoinsAllDRouters: priority 5 vs 2 -> StateDR and exactly one JoinAllDRouters(eth0), no leave; TestOSPFElectedBDRJoinsAllDRouters keeps the BDR join. - the same unit: priority dropped to 0, re-election -> DROther and LeaveAllDRouters(eth0); TestOSPFDROtherDoesNotJoinAllDRouters keeps the never-joined case. Records on iface.go::runElectionLocked observed red; author's overlay making membership BDR-only turned the DR positive red. Judge lint fix (unparam on the shared electWith helper): the unit's neighbour priority is 2, not 1; records re-recorded.

RFC2328-A.4.4-1

This field is not meaningful and must be zero for Type 4 summary-LSAs. (§A.4.4)

Audit verdict: enforced (the tests do what the requirement demands), fresh. Sentence (A.4.4): the Network Mask 'must be zero for Type 4 summary-LSAs'. (a) Non-compliant behaviour: originating a Type 4 summary-LSA with a non-zero Network Mask. (b) TestRFC2328Type4SummaryMaskIsZero originates a Type 4 through OriginateSummary (origination.go, the only Type 4 producer) with mask 255.255.255.0 and fails on body.NetworkMask != 0.0.0.0 after decoding the stored LSA, so a producer that copied the caller's mask goes red. Negative: TestRFC2328Type3SummaryKeepsMask proves the zeroing is confined to Type 4 (a Type 3 keeps 255.255.255.0), so a producer that zeroed every summary mask goes red there. One clause, both polarities.

Extraction sign-off

Sections

Excluded sentences

Superseded

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