Repository navigation
mtcollins1 read-only SMpro pass: per-socket boot stage over IPMI Master Write-Read, as a bundle section - #12222
Conversation
…d_int_magnitude, not an evaluator-refused cast Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… SEL reads; Redfish from the service root; evaluator-refusal frontier - Delete .run_claims.sh (review 70575): committed scratch that rewrote the fix back to `n as Nat` and swallowed failures. Mutation evidence is in the PR body. - Claims renamed/extended: a_stat_size_crosses_to_its_byte_size (inhabitance of the stat route), a_negative_or_non_numeric_stat_size_is_no_size, a_post_boot_sel_timeout_is_a_typed_after_section_and_moves_no_verdict. - extdeps.bmc.ipmi SdrDumpAuthenticated + SelListAuthenticatedCached (ipmitool(1) -S, sdr dump); the attempt dumps the SDR once pre-boot, both SEL snapshots read through it, a failed dump is a typed SdrCacheUnread in the bundle. Allowance counts 3 ipmi reads; step timeout stays 52 min. - Redfish inventory requests only the DSP0266 service root /redfish/v1/ and follows its published Systems link; an unpublished link is BmcLinkUnpublished. - Declared frontier at mtcollins1_boot_conclude: an evaluator refusal is not a value, so the conclusion cannot catch it; the wall is executed crossings. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
# Conflicts: # dag/gunbc/machine_intake/mtcollins1_boot_diagnostic_bundle.dag
…ion/quick-hawk-854
…, two-socket reference comparison, IPMI per-socket sensor reads Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… committed capture whole The four whole-file reference claims each cost ~97k eval steps against the 72.3k new-witness budget. Per DESIGN §3 the reference's three regions are supplied as verbatim excerpts, and one claim keeps the real route (61k steps). The relevance pass tests kernel lines against "Error" first, and still tests every non-kernel line against all six markers. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…variant directly (review 70756) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
# Conflicts: # .github/workflows/fleet-converge.yml # dag/gunbc/machine_intake/mtcollins1_boot_diagnostic_bundle.dag
…cked_int_to_nat Both sides repaired the same Int->Nat crossing. main's #12166 made std.checked_arithmetic checked_int_to_nat the single authority, so this side's checked_int_magnitude arm is dropped in its favour; the annotation now names that authority. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… the BMC answered The aggregate considered only the two SEL snapshots and the two Redfish collections, so an attempt whose SDR dump and sensor read succeeded still rendered "every BMC read failed". Every read section now derives one channel standing (answered / failed with its cause / not attempted); the finding fires only when nothing answered and names the failed channels. Discriminating control: cache and sensors answer while SEL and Redfish fail -> not all-failed. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
# Conflicts: # dag/gunbc/machine_intake/mtcollins1_boot_diagnostic_bundle.dag
…er Write-Read, as a bundle section Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
briansrls
left a comment
There was a problem hiding this comment.
Exact-head verdict: REQUEST CHANGES at f088e73.
Two blocking findings:
-
The promised probe order is not present in the dependency graph. In
mtcollins1_smpro_socket, the B2, B1, B3 and B0 reads are four independent effectfullets and are only placed into[control, cur, lo, hi, stage]afterward. There is no edgecur -> lo -> hi -> stage. At the cross-socket boundary, socket 1 is selected fromsocket0.first(), so it is downstream of socket 0's control but not structurally downstream of socket 0's terminal B0 read. The seed's eager source-order evaluation happens to realize the advertised order today, but the repository already records that source position is not modeled sequencing (gunbc.recurring_failure_mode.readback_ordered_only_by_statement_position). This is especially material because B0-last is the conservative evidence-preservation condition. Chain every sent probe through the preceding probe's typed outcome/after:receipt (or an equivalent Bind/control edge), including socket-0 terminal probe -> socket-1 control. Add a route/control witness that goes red when one of those edges is removed; the current supplied-outcome fixtures and the ten-probe count do not discriminate execution order. -
SmproResponseMalformedis classified asBmcChannelNotAttempted.smpro_channelcalls the channel answered only forSmproWordRead/SmproControllerRefused, failed only when it findsSmproTransportFailed, and otherwise falls through to NotAttempted. A malformed result, however, carries a sent raw request and exit 0: the BMC answered unreadably. With every other channel timed out, the current aggregate can therefore mintevery BMC read failed and the BMC did not answerwhile the SMpro channel did answer. Map this arm to a truthful attempted standing—preferablyBmcChannelFailed { cause: BmcResponseMalformed { ... } }, preserving its raw timestamp/detail—and add the bundle control where all other channels definitively fail but SMpro returns malformed bytes; it must not say the BMC did not answer.
The upstream register names/framing, typed private-bus bet, known-answer control, raw-outcome retention, no-new-mode integration, and derived allowance otherwise look aligned. The floor check was still running when this review was filed; these blockers are independent of its result.
briansrls
left a comment
There was a problem hiding this comment.
SOURCE HOLD at exact head f088e731bd63d3d7f9dda5375bc194095658bb5f.
The acquisition route is otherwise well-shaped: it extends the existing boot bundle; the IPMI Master Write-Read framing and the pinned SMpro names/offsets match the cited upstream sources; the private-bus value is an explicit, control-tested bet; socket 0 gates socket 1; every sent probe retains its raw request/result; BOOTSTAGE is last; no register-data write is issued; a completion code counts as a BMC answer; and the maximum ten reads are reflected in the derived allowance.
Two source blockers remain.
1. CUR_BOOTSTAGE is read but dropped from the socket-stage judgment
The upstream driver keeps two distinct facts:
CUR_BOOTSTAGE(0xB2), whose low byte is the current stage;BOOTSTAGE(0xB0), whose high byte is the stage being reported and whose low byte is that stage's status.
They are deliberately not equivalent: when the reported BOOTSTAGE stage is behind CUR_BOOTSTAGE, the driver writes the B0 low byte to 1 so firmware will report the next stage. This pass does not perform that write, so B0 may remain behind B2 by design.
At this head, mtcollins1_smpro_socket_stage establishes a socket only through B0. A successful B2 read is discarded when B0 fails. When both succeed, mtcollins1_smpro_findings compares only bootstage.stage/status; the current field is ignored. Therefore two sockets with identical B0 reports but different B2 current stages produce no finding, even though that difference is the pass's central discriminator.
Required repair: model current-stage and reported-stage/status as independent standings. A successful B2 read must remain established if B0 is unreadable, and the findings must surface a difference in current stage while keeping B0's report/status separate. Add discriminating controls for:
- equal B0 reports with socket 0
CUR_BOOTSTAGE=OSand socket 1CUR_BOOTSTAGE=DDR training; - a successful B2 read beside an unreadable B0, which must retain the current stage and say only that the report/status is unavailable.
2. An exit-0 malformed response is incorrectly treated as NotAttempted
smpro_probe_outcome produces SmproResponseMalformed only on an exit-0 command whose stdout is not exactly the expected two-byte rendering. That establishes that the IPMI transaction answered, while refusing its payload interpretation.
But smpro_channel counts only SmproWordRead and SmproControllerRefused as answered. If all sent outcomes are SmproResponseMalformed, it finds no transport failure and returns BmcChannelNotAttempted. With the other channels failed, this can allow the bundle to say every BMC read failed—or even that the BMC did not answer—despite an exit-0 SMpro exchange.
Required repair: count SmproResponseMalformed as BmcChannelAnswered for the aggregate liveness question, while preserving the malformed per-probe standing. Add a bundle control in which SEL/SDR/Redfish fail and SMpro exits zero with malformed bytes; neither all-failed nor did-not-answer may render.
No additional objection remains to the transport encoding, source citations, raw preservation, control gating, register order/read-safety standing, NAK classification, bundle placement, or timeout derivation.
…TSTAGE and BOOTSTAGE independent (1) The reads are one fold over the ordered plan; each read is handed count(acc), so it cannot be issued before every earlier probe has an outcome, and the gates read the folded controls. The witness runs that fold with a supplied read and asserts sequences 0..9 and register order. (2) An exit-zero malformed SMpro response answers the aggregate liveness question; the probe keeps its MALFORMED standing in the dossier. (3) Each socket carries CUR_BOOTSTAGE (current) and BOOTSTAGE (reported stage/status) as independent Established|Unavailable readings; findings name sockets that differ on either. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
|
Addressed the side-chat hold (GitHub reviews 5303560749 and 5303584755) in cf664f1:
Local: smpro 21/21, bundle 60/60, boot_run 16/16. — sent from quick-hawk-854 |
briansrls
left a comment
There was a problem hiding this comment.
APPROVE-MERGE at exact head cf664f111f35df336aec3daac9708abb953de8ec.
Reviews 5303560749 and 5303584755 are discharged.
-
The production probe route is now one ordered fold over the exact plan. Each step consumes the accumulated outcomes, the real service call receives
count(acc)as its sequence, and the folded controls gate later probes. The modeled order is control -> B2 -> B1 -> B3 -> B0 on socket 0, followed by socket-1 control -> B2 -> B1 -> B3 -> B0. Controls execute the production fold with a supplied reader, pin sequences 0..9 and the exact register order, refuse a register placed ahead of its control, and show that a failed socket-0 control leaves the other nine probes not sent. -
An exit-zero
SmproResponseMalformednow establishesBmcChannelAnsweredfor the aggregate liveness question while remainingMALFORMEDin the raw dossier. The bundle control holds SEL/SDR/Redfish failed, supplies a malformed SMpro reply, and refuses bothevery BMC read failedanddid not answerwhile retaining the malformed line. -
CUR_BOOTSTAGEandBOOTSTAGEare independent Established|Unavailable readings. A successful B2 survives a failed B0, and findings compare both readings, so different current stages render even when the two reported B0 stage/status values agree.
All five exact-head checks are green. No condition remains unless the head moves.
briansrls
left a comment
There was a problem hiding this comment.
APPROVE-MERGE at exact head cf664f111f35df336aec3daac9708abb953de8ec.
Both prior holds are discharged:
-
The probe order is now a real dependency chain. One fold walks the exact socket/register plan; each step consumes the accumulated prior outcomes through both the gate decision and the
count(acc)sequence input. The declared demand semantics preserve a fold whose step reads its previous accumulator as a sequential chain, so the resulting route is control -> B2 -> B1 -> B3 -> B0 on socket 0, then socket-0 B0 -> socket-1 control -> B2 -> B1 -> B3 -> B0. The controls execute that production fold with a supplied read, pin 0..9, pin the register order, refuse a register ahead of its control, and establish socket-0 control gating. -
SmproResponseMalformednow counts asBmcChannelAnsweredfor aggregate liveness while retaining MALFORMED plus raw request/stdout/stderr in the dossier. The bundle control combines failed SEL/SDR/Redfish with an exit-zero one-byte SMpro response and refuses bothevery BMC read failedanddid not answer. -
CUR_BOOTSTAGEandBOOTSTAGEare independent standings. A successful B2 survives a failed B0; findings compare current stage as well as reported stage/status, so equal B0 values no longer conceal differing current stages.
The delta from held f088e731... is one additive repair commit over four files. All five exact-head checks pass, and GitHub reports CLEAN/mergeable. No condition remains unless the head moves.
Regenerate fleet-converge.yml and design-rung-drops.md from the merged authorities. The shakedown job from #12178 carries Job.environment (none), which this branch adds to extdeps.github.actions Job. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
The ask (eager-owl-205): a read-only SMpro observation pass that tells us which boot stage each socket reached. It uses IPMI Master Write-Read (netfn 0x06, cmd 0x52) on bus 2, socket 0 at 0x4F first as the transport control, then socket 1 at 0x4E. Every probe is kept as an immutable raw observation with a typed refusal, and the dossier is published even when every probe fails. The operator is leaving the hardware untouched until this localizes a stage. Per the parent's routing, this is a new section of the existing boot diagnostic bundle, not a new fleet-converge mode: it reuses the bundle's modeled credential path and adds no scaffold.
Upstream, cited under its real names (
extdeps.ampere.smpro_register)From Ampere's Linux drivers, pinned:
drivers/mfd/smpro-core.c@9816d859239,drivers/misc/smpro-misc.c@995832b2ceb, and the ABI filesysfs-bus-platform-devices-ampere-smpro:[reg, 0x02], then read 2 bytes. The bus isREGMAP_ENDIAN_BIG, so the first byte on the wire is the high byte.MANUFACTURER_ID_REG(0x02) must read 0xCD3A; the core driver refuses the device otherwise. That makes it a known-answer transport control.BOOTSTAGE(0xB0): the high byte is the stage (the ABI table: 03 DDR initialization, 04 DDR training, 08 UEFI, 09 OS, …) and the low byte the status (00 not started, 01 started, 02 completed, 03 failed).BOOTSTAGE_LOis 0xB1,CUR_BOOTSTAGE0xB2 (low byte is the current stage),BOOTSTAGE_HI0xB3. The brief's 0xB4 and 0xB5 don't exist upstream.BOOTSTAGE, the driver's effect is its write(bootstage & 0xff00) | 0x1; its read is a plainregmap_read. The row names the Ampere document section (BMC Interface Spec §5.11) that would confirm or correct this.extdeps.ampere.scp_diagnosticAmpereBootStage/AmpereBootStatus, whose arms match the ABI order. A code with no table row stays a number.The IPMI command (
extdeps.bmc.ipmi_master_write_readandextdeps.bmc.ipmiMasterWriteReadAuthenticated)rawoutput is decoded: hex bytes on stdout, orrsp=0xNNon stderr.readonly: it performs an I2C write of the register pointer, and whether that has an effect is the device's fact, stated in its register model.The pass (
gunbc.machine_intake_mtcollins1_smpro_observation)SmproNotSent, with the control's outcome as the reason. A failed socket-0 control means nothing is sent to socket 1.SmproWordRead,SmproControllerRefused(NAK and the other completion codes),SmproTransportFailed, orSmproResponseMalformed(never a zero word).failed, or when one socket's stage couldn't be established. When both reached the same stage without failure, the refusal line gains nothing.Bundle integration
== smpro boot stage (ipmi master write-read) ==and its findings.4 + mtcollins1_smpro_probe_count()= 14. The diagnostics allowance grows by 250 s, so the derivedmtcollins1_bootstep timeout goes 53 → 57 minutes. I applied that single generated value infleet-converge.ymlby hand; CI's drift gate checks it.Evidence (local claim_batch, per file)
cd 3aand refusing a byte-swapped3a cd, NAK vs. timeout vs. malformed, the stage/status split, an undefined code, findings when sockets differ and none when they agree, and the dossier when nothing was sent.Not executed against hardware. No SMpro exchange with this BMC is in the corpus yet; the first
mtcollins1_bootdispatch after merge produces it. The fixtures are ipmitool's documented renderings and are labelled as supplied. The OEM "Get SCP Register Value" stays out until Ampere's spec is in hand.🤖 Generated with Claude Code