Take the singleton directly, and join the prerequisite bounds oracle to its rows

[briansrls]

Summary

Two follow-ups from the srv3 BMC surface-derivation lane that did NOT land with
#8211. That PR squash-merged almost all of this branch; these two commits were
made after install-0 branched off, so they stayed behind. After merging main
this PR is exactly those two changes and nothing else.

1. extdeps/bmc/types.dag — take the singleton directly.
bmc_redfish_surface_for's count == 1 arm folded over the one-element list with
an init: SurfaceShapeUncatalogued { firmware } that the fold is guaranteed to
discard. Fabricating a value in order to throw it away obscures that the arm is
already known to have exactly one row; it now reads
SurfaceShapeKnown { shape: matches.first().shape }. The count == 1 guard is
what makes .first() total here.

2. firmware_prerequisite_evidence_witness_test.dag — join the bounds oracle.
The bounds assertions transcribed 2/7 and 3/22 as literals. Those numbers'
single authority is the gating_version on each observation row, so re-flashing
at a different version would move the rows and leave this witness green until
someone remembered to edit it — the exact failure the same PR removed from the
declared-minimum path (DESIGN §5 test-oracle rule; caught in review 51524). All
four sites now compare against the row via same_firmware_version.

Joining does not weaken discrimination, which is what makes it safe here: both
orderings carry a THIRD, lower refusal at 1.00.00, so a first-wins fold reports
that instead of the refused row's own 2.07.00 and still fails.

The note above the RED controls is also split, because an earlier revision
conflated the two halves: a control's falsifying input stays authored (a probe
chosen to contradict the catalog would be unauthorable if joined to it), while its
expected value is an oracle like any other and joins to the row supplying it.

Merge resolution

Main had moved 37+ commits ahead. Both conflicts were in the two files above and
ours is the superset in each — main's version of the witness is this file minus
the join work — so taking ours drops nothing main added. Merge commit, not a
rebase, per the session's merge policy.

Test plan

No tests changed beyond the witness itself; relying on CI, whose ci job carries
the compile-clean gate and the witness corpus. Corpus scan on the merged tree
before pushing: zero body-grain annotations, zero trailing blocks.

[gunbai-bot]

Took the receipt finding from review 51290 — specifically the one you flagged as clearest, since it had a live consequence rather than being only stylistic.

The BIOS-tar prerequisite declared BMC >= 3.22.00 as a literal, while the two executed pushes that established it lived only in an unstructured String. So the release row and its evidence could not be joined, and a declared minimum that the evidence contradicted would have read exactly like one it supported.

FirmwarePrerequisiteObservation now carries each executed push — board, subject, packaging, gating target and version, outcome, timestamp — with the vendor diagnostic held on the refusal arm. The two ALTRAD8UD rows are the discriminating pair: identical bytes refused at BMC 2.07.00, accepted at 3.22.00. prerequisite_evidence_verdict checks a declared minimum against them.

One deliberate choice worth naming: the positive arm is PrerequisiteConsistentUpperBound, not a bare "consistent". Two pushes bound a threshold, they don't locate it — 3.06.00 sits in the capability catalog and was never pushed, so the declared 3.22.00 may be stricter than the vendor actually requires. A plain consistency verdict would have quietly upgraded "we bracketed it" into "we measured it", which is the same stronger-than-evidence move the surface derivation in this PR exists to prevent.

Witnessed both directions: a minimum inflated above the accepting version is contradicted by the acceptance; a minimum relaxed to or below the refusing version is contradicted by the refusal (the direction that would admit an unappliable push); and an empty observation list yields Absent, never consistent.

The prose row is trimmed to what the carrier genuinely cannot hold — that the vendor page documents no such dependency, that the cause was legible only in the BMC journal because Redfish reported Exception with none, and why the prerequisite belongs to the packaging rather than the release.

Not taking the rest of the class in this PR. You're right that it's corpus-wide debt with established sibling precedent, and converting the remaining notes (..._surface_catalog_note, ..._firmware_release_note, memory_training_step_note, memory_part_selection_note, host_diagnostic_channel_incident_receipt) is its own lane — those are rationale rather than joinable facts, so the payoff is real but much smaller than this one, where a checkable relation was missing.

— sent from quiet-badger-563

[gunbai-bot]

review 51298 verified and fixed. SupervisorIntervalKnowledge carried seconds on bare Nat while std.measure Second is the authority used for the same concept elsewhere. Now interval: Second on both arms; the declared-vs-measured epistemic split is unchanged, only the carrier moves. Same class as the ByteSize and MoneyAmountMicro fixes earlier in this stack.

Three further findings came from a separate review pass, and one of them was a defect this PR introduced — worth stating plainly:

Historical observations must be immutable. Editing the single srv3 firmware row in place from 2.07.00 to 3.22.00 moved every receipt that referenced it, so srv3's July update-service snapshot began claiming it had been observed under firmware installed in August. That is the same temporal-authority defect this PR set out to fix, relocated one field sideways. The two observations are now separate immutable rows, srv3_bmc_firmware_observation is the current standing and advances by re-binding rather than mutation, and the update-service receipt binds the 2.07.00 row it was actually taken under. A 3.22.00 receipt lands as a new row when one is measured.

Inventory is not an image fact. chassis_sensor_collection_member_count sat inside the image-derived shape. Two hosts returning nine members establishes agreement at those observations; it does not make cardinality invariant under fan, FRU, or sensor-service changes — and this same session measured installed fan sets differing under identical firmware, which is the identical nearby-question mistake one axis over. The count is dropped rather than derived from something that doesn't decide it. Route and resource availability stay, since those are compiled into bmcweb.

Duplicate keys refuse. bmc_redfish_surface_for took the first match, so two rows for one version resolved by list position — a silent, order-dependent answer where the catalog actually contradicts itself. It now answers SurfaceShapeAmbiguous with the collision count, with a RED control that plants the duplicate.

Also retargeted this PR's base from main to session/quiet-badger-563 and gave it a real title — it was showing the whole 22-file parent change under a placeholder. It's 7 files now.

Not taking one further suggestion in this PR: keying the catalog by a full image identity (digest / build id) rather than semantic version. It's right that a version is not an image, but I have no measured digest or build identity for either OpenBMC build, so the carrier would be Absent at every site and would assert a precision I haven't got. Board scoping is the more useful half and is worth doing properly alongside it. Follow-up, not silently dropped.

— sent from quiet-badger-563

[gunbai-bot]

Both taken.

review 51304 — fabricated bounds. Marked non-blocking, but it's a §5 violation by this repo's own standard, so I've fixed it rather than deferred. prerequisite_evidence_verdict stored the declared minimum into whichever bound had no observation behind it, so a verdict backed only by an acceptance reported a highest_refusal that never happened — a fabricated plausible value in exactly the field a consumer reads to judge how well-bounded the threshold is. And you're right that it was order-dependent, and right about why my positive test passed: the list is authored refused-then-accepted, so the coincidence held.

Both bounds are now Optional and computed as a genuine max-refusal / min-acceptance across all observations. Max and min are associative and commutative, so the result cannot depend on authoring order by construction rather than by accumulator discipline. Absent means absent. Two controls close it: the reversed list must yield an equal verdict, and an acceptance-only history must report no refusal bound.

review 51307 — missing imports, verified and fixed. firmware_semantic_version was used with no extdeps.firmware.types import in the module at all, and asrock_altrad8ud_openbmc_3_22_00_capabilities was referenced while the asrock block imported only the 2.07.00 and 3.06.00 rows. Both were mine, introduced by scripted edits that added references without their imports — a good catch, since these fail at resolution rather than anywhere I'd been looking. I swept the other changed witnesses for the same class; they're clean.

Worth noting the two findings are related: the missing imports came from the same batch-editing habit that produced the earlier misplaced-import parse error in this stack. The lesson I'm taking is that scripted edits to import blocks need the symbol check run afterward, not assumed.

On the port-number note from review 51305 (asrock_altrad8ud_scp_console_tcp_port: Nat): agreed it's a bare scalar for a domain unit, and not fixing it here. There's no port carrier in the corpus, so this would mean minting one — legitimate std modeling, but it's a new authority rather than consuming an existing one, and doing it inside a fleet-incident PR is how single-consumer carriers get shaped by one call site. Worth doing on its own with more than one consumer in view.

— sent from quiet-badger-563

[gunbai-bot]

All four findings from review 51313 verified and fixed. Two distinct causes, both mine.

The compile break. Rewriting the evidence-bounds block for the previous review deleted prerequisite_observation_contradicts along with the accumulator it sat beside, while prerequisite_contradiction still called it. You're right that git grep finds only the call site — nothing defined it anywhere, so the module could not compile, and the contradiction arms (the ones that actually gate correctness) were unreachable. Restored with its own rationale: an acceptance strictly below the minimum falsifies it, a refusal at or above falsifies it the other way, and consistent is not supporting — the bounds report that separately.

The stale fixtures, and they were worse than stale. Three classification witnesses used srv3 as their drifted-host fixture. Advancing srv3's current standing to 3.22.00 didn't merely break them: once srv3 satisfies the pinned track-3 intent, Drifted/Apply becomes Converged/Noop, so those tests would have inverted what they claim to check rather than failing loudly. They now bind srv3_bmc_firmware_2_07_00_observation — the immutable historical row — which is what each test was always about: classification logic on a host behind its intent, not srv3's present state.

Your fourth finding resolves without a separate change once that's done. The update-service receipt is bound to the 2.07.00 observation, so the plan test now pairs one firmware identity with itself and the update-surface identity check no longer refuses. Worth noting that finding was only reachable because the earlier review made observations immutable — under the in-place edit, the receipt and the firmware row would have moved together and silently agreed while both described a state no measurement supported.

That's the immutable split paying for itself within one review cycle: the historical row existing is what let three tests keep their meaning instead of being rewritten around a moved fact.

— sent from quiet-badger-563

[cursor]

Bugbot is not enabled for your account, so this pull request was not reviewed.

Enable Bugbot in the Cursor dashboard to get automatic reviews on future PRs.

[gunbai-bot]

No findings in review 51324 — nothing to fix. But the dashboard readout says something the approval doesn't, and it should be visible before anyone merges this.

This PR currently gets no CI at all, and that's my doing. ci.yml triggers on pull_request: branches: [main]. I retargeted this PR's base from main to session/quiet-badger-563 earlier so the diff would show its own 7 files instead of re-presenting the parent's 22 — which was right for review, but it also took the PR out of CI's trigger scope. The dashboard reflects it exactly: checks: "none", and merge_criteria.ready: false on the checks requirement alone, with approvals at 2/2 and mergeable: MERGEABLE.

So the state here is 2 approvals and zero executed verification. That combination is worth naming rather than leaving to be inferred from a green-looking summary: no check is not a passed check. I'd rather flag it than have the approvals read as evidence the code runs.

The normal stacked flow resolves this without any action: when #8171 merges, GitHub retargets this PR to main, CI fires, and the checks requirement becomes real. Until then this should not merge — not because of a defect, but because nothing has executed it.

The alternative is retargeting back to main now to get CI, at the cost of the diff re-presenting all of #8171 again and the reviews above losing their scope. I'd rather keep the honest small diff and let the stack drain in order, but say the word if you want CI on it sooner and I'll retarget.

— sent from quiet-badger-563

[gunbai-bot]

The red here is not this PR. It is pre-existing main debt, and the fix is #8215.

dag_compile_clean_gate_passes reports 18 identical, unlocated diagnostics:

compile-clean: source annotation sits inside a declaration body. Only module-item grain is modeled; move it above the declaration it describes.

I first assumed my own new comment blocks were the cause and pushed a bisection commit stripping 93 of them. That hypothesis was wrong, and two independent measurements killed it:

• the arithmetic never closed — 14 blocks added, 18 reported
• srv3+4 upgrade check #8211, a different branch with an entirely different file set, produces the identical failure

Scanning the corpus at brace depth > 0 gives exactly 18 in-body comment blocks under dag/ on clean main — an exact match to the diagnostic count — plus 2 under src/v2/ that the --target dag gate does not reach. They come from #8045, #8073, #8122, #8147 and the current head. Main's own recent runs are cancelled or in-flight, so no green verdict ever observed it.

The bisection strip is now reverted — the prose it removed was never the cause and is restored in full. This branch stays red until #8215 merges; then I merge main in.

Separately worth recording: the diagnostic is typed but carries no file, line, or declaration name, even though AnnotationAttachmentRefusal carries origin: SourceSpan on every arm and BodyGrainNotModeled is constructed with it — the consumer discards the span it was handed. That §5 located-ness gap is what cost a full CI cycle and a bisection commit here. Filed in #8215's body, not repaired there, so that PR stays comment-only.

— sent from quiet-badger-563

[gunbai-bot]

Fixed in d3c3b2da1. review 51524 is correct and the finding was exact — this file already identity-joins the declared minimum and carries a comment explaining why tree-copied literals are forbidden, while two witnesses a few lines below still hard-coded 2/7 and 3/22.

Both now join through one same_firmware_version helper to asrock_altrad8ud_bios_310_push_refused_at_bmc_207.gating_version and asrock_altrad8ud_bios_310_push_accepted_at_bmc_322.gating_version.

Two things I did beyond the review:

The same defect sat in two witnesses it didn't name. a_minimum_above_the_accepting_version_is_contradicted and a_minimum_at_or_below_the_refusing_version_is_contradicted transcribed the same two versions as their expected values. Joining only the flagged sites would have left identical rot one screen down, so those are joined too.

That exposed a distinction the file had wrong in prose. A RED control has two halves under different rules: its falsifying input — the minimum deliberately set above or below the evidence — stays authored, because a probe joined to the catalog it contradicts would be unauthorable. Its expected value is an oracle like any other and joins. The old note claimed the RED controls "deliberately do NOT join" without that split, which is why the transcription there read as intentional rather than as the same defect. The note now states both halves.

Discrimination is unchanged, which is what makes this a join rather than a loosening: both orderings feeding bounds_are_the_executed_pair carry a third, lower synthetic refusal at 1.00.00, so a first-wins fold still reports 1.00.00 against the refused row's 2.07.00 and still fails. The order-independence claim doesn't weaken by sourcing its expected value from the row.

CI on this branch stays red on an unrelated pre-existing main issue — 18 body-grain source annotations, fixed in #8215 (details in the comment above).

[gunbai-bot]

Both of you flagged the count == 1 arm as awkward-but-functional, each on the premise that no head-of-list primitive was at hand (review 51522, review 51533). That premise turns out to be false — .first() is used widely in the corpus and returns the element directly (steps.first(), srv1_live_deploy_privileged_commands().first()).

Fixed in cc69a4ffb, and it's slightly more than the style nit you both scoped it as. The fold carried:

init: SurfaceShapeUncatalogued { firmware: firmware }

That is a fabricated plausible value which is never the correct answer in an arm already guarded by count == 1 — a well-formed derivation saying "this firmware is not in the catalog", sitting as the default of a branch reached only because it is in the catalog exactly once. Nothing can return it today, since the guard holds and the fold visits its one element. But it's the fail-open shape §5 names, and it stays harmless only as long as the guard above it does. Removing the fold removes the fabricated value with it.

Behavior is unchanged: for a one-element list the fold's f ran exactly once and returned SurfaceShapeKnown { shape: row.shape }, which is what the direct read produces.

— sent from quiet-badger-563

[gunbai-bot]

Investigated cc69a4f. There is nothing in this PR to fix — I'm not pushing a speculative change.

The only failing witness is dag_compile_clean_gate_passes, and I checked it isn't fallout from the .first() simplification: no other witness fails, and the diagnostics are the corpus-wide annotation debt described in my earlier comment — 18 body-grain plus 11 unattached.

I then attributed every refusing site against this PR's changed files. Zero overlap. The refusals are in:

• dag/product/compute_board/article.dag, ci_deploy_witness_test.dag, fleet_converge_cli_witness_test.dag, host_phase_status_witness_test.dag, posix_principal_allocation_witness_test.dag (body-grain)
• extdeps/{cloud/gcp/iam,git/inspect,git/publication_transport,sec/edgar_rest,tailscale/serve}.dag, resolved_graph_cache_hand_rust_witness_test.dag (unattached)

None of those are among the 18 files this PR changes.

The fix lives in #8215, which clears the body-grain class entirely and 2 of the unattached ones. Its remaining 5 are comments above service declarations — service never calls stamp_parsed_node, so it produces no occurrence index entry and can't be an annotation subject. That needs an operator decision (make service eligible in the v1 seed, vs. rule such annotations unsupported), which I've raised rather than improvised.

When #8215 lands I'll merge main into this branch and re-run. Content-wise this PR is done: 2/2 approvals, the REQUEST_CHANGES on the bounds oracle resolved, and the count == 1 fold nit fixed.

— sent from quiet-badger-563