Repository navigation
BmcSecure gets a route table, and the MegaRAC arm refuses before any controller write - #10952
Merged
gunbai-bot[bot] merged 15 commits intoSep 11, 2026
Merged
Conversation
gunbai-bot
Bot
changed the title
briansrls
marked this pull request as ready for review
September 10, 2026 21:02
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: e135368f64
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| // filed as gunbc.recurring_failure_mode.ad_hoc_hardware_probe_produces_no_receipt. So the honest | ||
| // state is not "MegaRAC cannot rotate" -- it is "we have seen it answer and we cannot say how we | ||
| // asked". | ||
| fn rotation_route_for_family(family: BmcFirmwareFamily) -> BmcRotationRoute { |
There was a problem hiding this comment.
When a producer is added, this API permits it to pass any freely constructed BmcFirmwareFamily, including a product expectation or a family copied from another unit, even though the module's safety premise requires the family to come from the current unit's observation. The new witnesses likewise call it with bare OpenBmc/AmiMegaRac values, so they cannot detect this provenance loss. Accept the bound BmcAccessObservation (or its receipt/standing) and derive the family from its observed identity so an unobserved or mismatched endpoint cannot select a credential-write route.
Useful? React with 👍 / 👎.
…thing Two instances of one class, which is the filing threshold, and both are about the same controller. 2026-08-29: an operator run saw GET /redfish/v1 return 404 on a held Mt. Collins unit, the firmware self-report as 0.32, and the service roster. extdeps.ampere.mt_collins_product_brief.bmc records that the raw producer output was NOT PRESERVED, and therefore types the AMI MegaRAC identification as an EXPECTATION, forbidding any workflow from reading it as an observation or as authority. That module is the corroborating evidence that the corpus already knew and could not act: it names the receipt that would settle the question and no such receipt exists. 2026-09-06, found today: a rotation attempt answered "attempt to set previous password" against a policy-conforming secret -- a DECIDED semantic response proving the endpoint exists, parses the field, and applies a history policy. gunbc#10630 records the sentence and nothing else. A corpus-wide search returns no /api/ user or password request shape; the only rotation body committed anywhere is the Redfish PATCH in gunbc.tools.bmc_onboard, whose plans name srv3 and srv4, and which cannot be the call that answered because Redfish against a controller with no Redfish returns 404 rather than a password-policy error. The request is unrecoverable from the diff. THE DISTINGUISHING FACT IS NOT THAT SOMEBODY FORGOT TO WRITE IT DOWN. Preservation was never available to skip, because the probe's OUTPUT WAS NEVER A RECEIPT -- there is no carrier the run could have committed, so the only artifact that can survive is a recollection, which is precisely what the corpus refuses as authority. The defect is in the probe's shape, not in anyone's diligence, and no amount of note-taking discipline produces a citable observation from a run with no carrier. The harm compounds rather than repeats. The controller answered no ARP from its own /24 today, so neither specimen can be re-run until someone physically plugs the unit in; specimen two was undertaken WITHOUT the firmware fact specimen one would have supplied, spending a second irreproducible probe partly re-establishing the first; and a third lane was then briefed to model a rotation endpoint against an identification the corpus explicitly refuses to certify, which would have made two files of this repository contradict each other with the correct one losing. Ceiling is structurally guaranteed rather than impossible: a probe whose result is a typed observation by construction cannot produce an uncitable answer, but nothing stops a human opening a terminal beside the modeled path. The trigger is the identity-observation operation, and it carries one design constraint from the class itself -- the receipt must be shaped so EITHER answer lands cleanly, because a probe designed around the expected firmware is how the unpreserved run became de-facto authority in the first place. Membership is the directory; ensure_derived_recurring_failure_mode_roster derives the roster, so adding the file is the act. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CHmuTG7e714e4VEE5zAaju
…ce, not the probe As first written this row claimed specimen one's evidence was destroyed and every later lane must re-probe. That overstated it. The fact had already been recovered on 2026-09-05 by gunbc.machine_intake.mtcollins1_access_observation -- the very receipt the extdeps module specified -- with committed raw bytes, a digest I recomputed and verified, and five Redfish paths refused against a web root answering 200 as the discriminating control. THE HARM IS NOW KEYED ON THE PROBE RATHER THAN ON WHAT HAPPENED AFTERWARDS, and that is the sharper form. Whether the fact is recoverable is CONTINGENT: it needs the hardware to still exist, still be reachable, and someone willing to make the trip. A row keyed on 'the evidence was destroyed' keys on the consequence and would have MISSED specimen one entirely -- the instance where recovery happened. The class is the probe shape, and it fires in both: specimen one paid the cost and recovered, specimen two cannot pay it at all today because the request shape is nowhere and the controller answers no ARP. AND THE AMENDMENT IS RECORDED IN THE ROW RATHER THAN APPLIED QUIETLY, because how I got it wrong is the mechanism the row is about one level up. I read extdeps.ampere.mt_collins_product_brief.bmc -- which correctly declines to be the authority for an observation outside its layer, and whose sentence that no receipt is authored WAS TRUE WHEN WRITTEN -- as a census of the corpus. It was superseded eight days later by the receipt it named. A module declining authority for something outside its layer is not evidence about what the corpus holds. A failure-mode ledger whose own entries overstate their harm teaches the next reader to discount it, which is the one thing a ledger cannot afford. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CHmuTG7e714e4VEE5zAaju EOF
…controller write BmcSecure has been a declared Arrival phase with an adjudicator, a sole_constructor observation and a receipt shape, and NO PRODUCER -- gunbc.bmc.bmc_onboarding says so in its own annotation. This is the piece that decides whether a producer can run at all, and for the firmware the fleet actually holds the answer today is no. THE ROUTE IS KEYED ON AN OBSERVATION, NEVER AN EXPECTATION, and that distinction is the whole reason this lands the way it does. gunbc.machine_intake_mtcollins1_access_observation carries family AmiMegaRac with committed raw bytes and a digest I recomputed and verified, and it established Redfish absence against a DISCRIMINATING CONTROL: five Redfish paths refused over TLS while the same host answered 200 on its web root, separating "no Redfish service" from "host unreachable". extdeps.ampere.mt_collins_product_brief.bmc holds only an expectation and forbids its own promotion; nothing here reads it. WHY THE MEGARAC ARM IS UNAVAILABLE RATHER THAN IMPLEMENTED, and it is the module's own rule that decides it. extdeps.bmc.megarac admits an operation row only as EXECUTED -- its scope note says the REST rows are "the SP-X interface shape as executed on that build ... and carry that provenance explicitly" -- and all six rostered operations were run against the controller. No user-management operation has been executed, AMI publishes no SP-X reference to cite instead, and authoring the row anyway would put an unexecuted row beside six executed ones under a rule admitting only the executed. The honest state is not "MegaRAC cannot rotate": gunbc#10630 saw a REST path answer "attempt to set previous password", which is a DECIDED response proving an endpoint exists and parses the field. What is missing is the request that reached it, which was never committed -- filed as gunbc.recurring_failure_mode.ad_hoc_hardware_probe_produces_no_receipt. THE REFUSAL LANDS BEFORE A WRITE, WHICH IS WHY THE ROUTE PRECEDES THE ATTEMPT. An unavailable route yields AccountManagementUnavailable, which the existing adjudication turns into a typed located refusal whose owner is DERIVED -- so a MegaRAC unit fails its Arrival phase and is never certified secured, does not silently skip, and is not filed as a hardware defect against the seller's return clock. That matters more than usual here: the controller currently answers no ARP from its own /24, so a producer that assumed a transport would fail at the wire instead of at the model. FOUR WITNESSES, PAIRED SO NEITHER ARM CAN PASS ALONE. MegaRAC refuses and OpenBMC routes, over the same fold, because a witness that only asks the unavailable arm cannot distinguish a correct route table from one that refuses everything -- and refusing everything would fail the OpenBMC fleet too, invisibly. The application fold gets the same treatment: unavailable must yield AccountManagementUnavailable specifically (returning Absent there would let a caller proceed and adjudicate into "nobody tried" rather than "there is no way to try"), and available must yield Absent so an implementation that refused unconditionally cannot pass. Dispatch sits here rather than in either extdeps module because DESIGN §3 puts realization selection in realization: extdeps.bmc.redfish and extdeps.bmc.megarac each own their surface and neither learns the other exists. The frontier names the CAPABILITY -- an executed MegaRAC user-management request committing its shape and response -- and explicitly refuses satisfaction by authoring a row from documentation, from the srv3/srv4 Redfish shape, or from the uncommitted 10630 attempt. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CHmuTG7e714e4VEE5zAaju
…ation
dag/gunbc/machine_intake/bmc_rotation_route.dag:51:62: error: undefined variable 'account_id'
I wrote the Redfish account path into a contract note as
/redfish/v1/AccountService/Accounts/{account_id}, copying the spelling from extdeps.bmc.http where
it is CORRECT -- there it sits in a transport shell argv and the braces are exactly what binds the
input. In a prose string the same bytes are an interpolation of a variable that does not exist, so
the note reads as documentation and compiles as a reference.
The tell is worth keeping: a placeholder convention that is load-bearing in one position and inert
in another does not exist -- it is load-bearing in both, and the position decides whether that is
what you meant. Rephrased to name the account id in words.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01CHmuTG7e714e4VEE5zAaju
gunbai-bot
Bot
force-pushed
the
session/fierce-wren-75-bmc-identity-receipt
branch
from
September 10, 2026 21:17
e135368 to
db15293
Compare
Review 63236, and it is correct on both halves. TENSE. The block asserted "a unit whose firmware has no rotation transport FAILS ITS ARRIVAL PHASE and is never certified as secured". That describes the terminal architecture wearing the tense of the current one. BmcCredentialRotationObservation takes `rotation` as a SUPPLIED field, so no unit's arrival phase consults this table today, and bmc_secure says so itself: the effectful rotation actuator "does not exist yet". The executed evidence is this module's witness fold and nothing else, so citing it for a claim about arrival phases is DESIGN §4b(1) rung inflation. Re-tensed to describe the value the fold returns, with the original sentence quoted rather than deleted so the correction is legible. CONSUMPTION. §3c requires each added declaration to name its consumer and route, or be classified honestly. Today the only executing consumer of both folds is the witness. That is the admissible middle state -- a named consumer landing in a named later change -- but the module never declared it, and a consumption described in a PR body and absent from the diff is precisely §3c's red. Now declared as rotation_route_consumption_frontier with its own trigger. THE NEW ROW IS SEPARATE FROM megarac_rotation_route_frontier ON PURPOSE. That one dissolves the UNAVAILABLE ARM and is silent about whether any caller exists; citing it for consumption would be one dissolution condition doing two jobs. The new trigger names the capability -- the actuator DERIVING the rotation field by calling this fold -- and explicitly refuses to be satisfied by a typecheck, by the witness, or by a caller passing a route it built itself. NOT VERIFIED LOCALLY, AND SAYING SO RATHER THAN IMPLYING OTHERWISE: the session's gunbc binary is too old to parse the current corpus -- it dies on dag/extdeps/uri.dag:153 -- and the control confirms it, since unmodified main fails identically with the same binary. So the four witnesses are unrun here and CI is the only evidence for this commit. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UwLGmTkGxdNTHZo3qpZnAg
Contributor
Author
|
Both findings in review 63236 are correct and are fixed in 56a6f94, not argued with. The tense. The block asserted "a unit whose firmware has no rotation transport FAILS ITS ARRIVAL PHASE and is never certified as secured." That describes the terminal architecture in the tense of the current one. The consumption gap. Correct that One thing I could not do, stated rather than implied: I did not run the four witnesses locally. This session's Also on this head: the PR was re-cut from — sent from fierce-wren-75 |
Review 63250. Both findings correct; the first is fixed by MOVING rather than by
documenting the divergence, because DESIGN §3 prefers one authority over a
stated exception.
THE FORK. rotation_route_for_family was a FOURTH `match family { OpenBmc |
AmiMegaRac }`, and gunbc.bmc_implementation_dispatch is the home the corpus
already built for exactly that -- it carries the other three. My block comment
reasoned at length that a realization dispatch belongs peripheral to both extdeps
modules rather than inside either, which is correct §3 reasoning and the wrong
conclusion: the peripheral home EXISTED and the argument never mentioned it.
Under §3b that is "diverges with no reason", the only red, because a reader
cannot tell whether the split was deliberate.
AND IT WAS LOAD-BEARING, NOT COSMETIC. bmc_implementation_dispatch says of itself
that a third implementation "refuses to compile here and nowhere else; that is
the census". A fourth family match in another module falsified that sentence the
moment it landed, splitting the third-implementation census across two modules
with no cross-reference. gunbc#9678 already paid for this exact fork in the other
direction.
THE SPLIT IS NOW AT THE LAYER BOUNDARY. BmcRotationRoute and
rotation_route_for_family are keyed on BmcFirmwareFamily and cite only extdeps.bmc
facts, so they moved to the dispatch home, and megarac_rotation_route_frontier
moved with the arm it guards. rotation_application_for_route stayed: it maps a
route to a machine_intake CredentialRotationApplication, so hoisting it would make
the peripheral dispatch module import machine_intake and invert the layering it
exists to keep straight. The census sentence now records why the fourth fold is
there.
THE CITATION DEFECT. The §3c note named its consumer
test.claim.machine_intake.machine_intake_bmc_rotation_route_witness; the module is
test.claim.machine_intake_bmc_rotation_route_witness_test. It resolved to nothing
-- and it is the one sentence that makes the dangling declaration admissible, so a
§3c frontier citing a module that does not exist is worse than no note.
TWO MORE FOUND WHILE IN THERE, both mine, both the same class as the finding.
megarac_rotation_route_frontier still said the Arrival phase "stays unsatisfied
for every MegaRAC unit" -- the same present-tense §4b(1) inflation corrected one
commit ago, surviving in a second row. And the consumption note cited the other
frontier as "the frontier below", a positional citation this very move would have
silently invalidated: §3 names the symbol, not the position, for exactly this
reason.
Still not run locally -- the session binary cannot parse the current corpus and
the control confirms it fails identically on unmodified main. CI is the evidence.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UwLGmTkGxdNTHZo3qpZnAg
…eady models Review 63263, and it is right on both halves. THE LEAF. RotationRouteRedfishAccountService carried one path_note String spelling out the method, the path template, the JSON member, the operation name and the executing tool. Every one of those is already modeled: the argv is `operation SetAccountPassword` on the redfish.Http service, the action shape is the SetAccountPassword arm of RedfishSystemAction, and the provenance is the call site in gunbc.tools.bmc_onboard. A String leaf hiding named parts is anemic modeling (DESIGN section 2), and a symbol cited INSIDE a string literal is unreachable from the Node tree -- so unlike a DeclarationRef it is never harvested by the citation checker and can rot with neither end touched. The arm now carries transport_operation and action_shape as DeclarationRefs. IT WOULD NOT HAVE SURVIVED ITS OWN FRONTIER, which is what makes this more than tidying. rotation_route_consumption_frontier promises an actuator that DERIVES the rotation by calling this table. That actuator needs the operation, not a description of it, so the arm would have been rewritten rather than consumed -- section 6's reviewer test answered "no" on the one arm that is supposed to work. AND THE SECOND HALF WAS NOT FIXED BY THE FIRST. The finding was also that nothing READS the field. Swapping prose for references leaves it unconsumed, and a reference nothing reads is still dead data by section 4c's own test. So the witness now destructures the available arm and asserts the operation it names: a route table pointing at the wrong operation reds in the witness rather than being discovered later by the actuator. Still not run locally; the session binary cannot parse the current corpus and the control confirms it fails identically on unmodified main. CI is the evidence. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UwLGmTkGxdNTHZo3qpZnAg
Review 63271. Both findings are real. The first one's CONSEQUENCE is wrong in a
direction that makes it worse, and that is worth stating rather than quietly
taking the fix.
THE TYPE ERROR IS REAL. `data bmc_rotation_route_disposition: Disposition =
SingleAuthority` -- SingleAuthority is an arm of ConstructionMechanism, not of
Disposition, which has exactly Terminal and Scaffold. Every other `: Disposition
=` site in the corpus uses one of those two. Mine was wrong. It is now Terminal
with a stated reason.
BUT "THE MODULE THEREFORE DOES NOT COMPILE" IS FALSE, AND THAT IS THE MORE
SERIOUS READING. It compiles. Two independent pieces of evidence from this
session: a `gunbc run` against this closure RESOLVED it and failed only on a
wrong function name, and gunbc#10952 was green on all four required checks with
this row present. The cause is a rostered below-floor defect -- a wrong COPRODUCT
value is accepted into a declared field with no diagnostic, while the same check
fires for primitives and for unresolved names. So the ordinary compiler floor,
"values inhabit declared types", did not hold, and a plainly wrong row rode four
green checks. If the module had failed to compile I would have found this myself
an hour ago; it passed because the wall is off.
THE SECOND FINDING IS MINE TWICE OVER. The witness added one commit ago to read
the arm's payload asserted module_path and decl_name on both refs and never
touched `field` -- which is the only position the operation name lives in. A
table returning NamedField { field_name: "DeleteAccount" } would have GREENED
while the comment directly above it claimed a wrong operation would red. That is
a check whose subject is narrower than its stated claim: the same §4b(1)
inflation this PR has now corrected in three different rows, in three
consecutive reviews, each time in prose I wrote confidently. The witness now
reads the field through decl_field_name, so the assertion and the sentence
describe the same test.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UwLGmTkGxdNTHZo3qpZnAg
Contributor
Author
|
Both findings in review 63271 are real and are fixed in The type error is real. But "the module therefore does not compile" is false, and that is the more serious reading. It compiles. Two independent pieces of evidence:
The cause is a rostered below-floor defect: a wrong coproduct value is accepted into a declared field with no diagnostic, while the same check fires for primitives and for unresolved names. So the ordinary compiler floor — "values inhabit declared types" (DESIGN §4b) — did not hold here, and a plainly wrong row rode four green checks. Had the module actually failed to compile, I would have found this myself an hour ago. It passed because the wall is off, which is worth recording separately from this PR. The second finding is mine twice over. The witness I added one commit ago specifically to read the arm's payload asserted That is a check whose subject is narrower than its stated claim: the same §4b(1) inflation this PR has now corrected in three different rows across three consecutive reviews, each time in prose I wrote confidently. The witness now reads the field through Not claiming local verification: this session's Note on CI: this PR's red is currently inherited from main, not introduced. — sent from fierce-wren-75 |
…reen checks
Review 63271 found `Disposition = SingleAuthority` in this PR. DESIGN section 4b
requires a recurring_failure_mode row from whoever discovers a class, and this
one had none despite being measured in August.
THE CLASS IS SHARPER THAN "a wrong coproduct is accepted", and I read the
relation rather than inferring it from its name -- which is the mistake the
review itself made in the other direction. `kernel_value_declared_type_mismatch_bounded`
short-circuits at its second guard: `is_kernel_type(name: actual_name) == false`
returns FALSE, meaning NO MISMATCH, before any formal type is consulted. So the
wall decides on the KIND OF THE OFFENDING VALUE, not on inhabitance.
WHICH MEANS "one more declared-type position needs a member" IS THE WRONG SHAPE,
and that is the finding worth having. The kernel-inhabitance census enumerated
fourteen positions from the grammar and closed seven; that guard sits INSIDE the
relation those positions consult, so closing a position does nothing for a
non-kernel wrong value. The record-literal field seam was ALREADY closed for
kernels -- the witness cites KHold { subject: 5 } refusing there -- and still
admitted my row. The uncovered half is not a position, it is every position.
HARM, FROM THIS PR'S OWN SPECIMEN: the review concluded "the module therefore
does not compile, and with it the whole witness closure". Reasonable, and false.
The defect does not only admit a wrong value; it makes a reader who assumes the
floor holds derive a wrong consequence from a correct observation. Four green
checks said the row was fine, a reviewer said the module was absent, and neither
was true.
WHAT I DID NOT CLAIM: how many of the fourteen positions admit a non-kernel wrong
value. The guard's placement implies all of them; I measured two specimens and
did not census the rest. The row says so, and names that census as the honest
next measurement.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UwLGmTkGxdNTHZo3qpZnAg
…5-bmc-identity-receipt
…5-bmc-identity-receipt
Review 63497. The new failure-mode row ended every receipt "." with an `as NonEmptyStr` cast; the field is `receipts: List<String>` and `authored` folds them with `concat` and NO separator, whose own annotation says each receipt carries its own trailing space so the fold reproduces the string it replaced BYTE FOR BYTE. So this row rendered as "...not a rung on the ladder.READ FROM THE RELATION..." at all eight boundaries in the docs projection. THE TELL IS SHARPER THAN THE REVIEW PUT IT: both files are mine, written hours apart in the same PR. ad_hoc_hardware_probe_produces_no_receipt.dag ends its seven receipts `. ",` -- trailing space, no cast -- and I wrote it earlier the same evening. I did not copy the convention from the row I had just authored; I re-derived a shape from the `identity` field beside it, which IS NonEmptyStr, and carried that cast onto a String field. Nine receipts converted to the carrier's convention. The `identity` cast stays, because that field really is NonEmptyStr. VERIFIED BY RENDERING, not by reading: reconstructing the fold over the nine receipts now yields "ladder. READ FROM", "exit. WHY THIS", "position. MEASURED" and so on at all eight boundaries, with zero receipts lacking a trailing space. Before the fix every one of those was jammed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UwLGmTkGxdNTHZo3qpZnAg
Review 63521, and it is the third instance tonight of one move: taking a shape
from what is adjacent instead of reading the module that owns the thing.
THE RE-INVENTION. The witness hand-rolled decl_field_name, a fold over DeclField
returning a String, so it could compare the operation name. std.decl_ref already
owns decl_field_eq, and that module's annotation states the rule outright: a
module needing a DeclarationRef imports the constructor from the type's own
module and never re-mints it. DESIGN section 2 -- net concepts must not grow by
re-invention. Now decl_field_eq(a: op.field, b: NamedField { ... }).
THE FABRICATED ARM COMPOUNDED IT. decl_field_name's WholeDeclaration arm returned
"" -- a plausible value manufactured where the canonical surface refuses to
conflate the two shapes (section 5, no fabricated plausible output). It happened
to compare false and stay fail-closed, which was luck of the call site and not a
property of the helper. A second caller comparing against "" would have read a
WholeDeclaration ref as a match.
AND THE SAME NOTE COVERS THE CONSTRUCTION SIDE, so it is fixed in the same
motion: the dispatch module spelled DeclarationRef record literals inline rather
than calling the co-located decl_field_ref. Both refs now go through the
constructor. That is the same defect one layer down from the prose leaf this arm
already replaced two commits ago -- I removed a prose citation in favour of a
typed one, then built the typed one by hand.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UwLGmTkGxdNTHZo3qpZnAg
…5-bmc-identity-receipt
The §3c block opened "Today: nobody in production." That is a claim with no producer that can re-derive it and no consumer whose addition contradicts it, so it would have gone silently false the moment an actuator landed and nothing would have said so. The frontier beside it is not a revalidation dependency: it fires only if a human dissolving it remembers to re-tense the prose. THE REPLACEMENT WAS ALREADY IN THE NEXT SENTENCE. "The only executing consumer of rotation_application_for_route is test.claim.machine_intake_bmc_rotation_route_witness_test" carries the same content in the form that survives -- a named join is falsified MECHANICALLY when a caller appears, because its identity is reachable through the namespace tree. So the deleted sentence was not carrying anything the kept one lacks; it was carrying it in the shape that rots. THE RULE, STATED SO THE NEXT AUTHOR HAS IT: universal negatives are not intrinsically invalid -- structurally tracked, complete-population derived, and snapshot-bound claims are all sound. A LIVE open-world negative with no complete producer and no revalidation dependency is the refused shape. This is DESIGN §3's cite-the-symbol-not-the-position rule applied to a claim about a population, and §3c already asks for it: name the consumer and the route, never assert the absence of consumers. FOUND BY keen-dove-322 on gunbc#10972, which is held for the identical shape. Ruled by sunny-tern-813 as a §4c finding rather than style, on consistency: the tree should not carry two rulings for one class depending on whose reviewer noticed. The replacement paragraph quotes the deleted sentence as history, which is snapshot-bound and cannot rot. Touches no declaration. The five witness claims the required floor measured pass/observed are unchanged. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UwLGmTkGxdNTHZo3qpZnAg
gunbai-bot
Bot
deleted the
session/fierce-wren-75-bmc-identity-receipt
branch
September 11, 2026 10:42
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
BmcSecurehas been a declared Arrival phase with an adjudicator, asole_constructorobservation and a receipt shape, and no producer —gunbc.bmc.bmc_onboardingsays so in its own annotation. This is the piece that decides whether a producer can run at all, and for the firmware this fleet actually holds, the answer today is no.The route is keyed on an observation, never an expectation
gunbc.machine_intake_mtcollins1_access_observationcarries familyAmiMegaRacwith committed raw bytes and a digest I recomputed and verified (3227 bytes,3c358eb4…). It established Redfish absence against a discriminating control: five Redfish paths refused over TLS while the same host answered 200 on its web root — separating "no Redfish service" from "host unreachable", which a bare set of 404s cannot do.extdeps.ampere.mt_collins_product_brief.bmcholds only an expectation and forbids its own promotion. Nothing here reads it.Why the MegaRAC arm is unavailable rather than implemented
The module's own rule decides it.
extdeps.bmc.megaracadmits an operation row only as executed — its scope note says the REST rows are "the SP-X interface shape as executed on that build … and carry that provenance explicitly" — and all six rostered operations were run against the controller.No user-management operation has been executed. AMI publishes no SP-X reference to cite instead. Authoring the row anyway would put an unexecuted row beside six executed ones under a rule admitting only the executed — the module contradicting itself in its own file.
The honest state is not "MegaRAC cannot rotate": #10630 saw a REST path answer
attempt to set previous password, a decided response proving an endpoint exists and parses the field. What is missing is the request that reached it, which was never committed — filed asgunbc.recurring_failure_mode.ad_hoc_hardware_probe_produces_no_receipt.The refusal lands before a write
An unavailable route yields
AccountManagementUnavailable, which the existing adjudication turns into a typed, located refusal whose owner is derived rather than authored. So a MegaRAC unit fails its Arrival phase, is never certified secured, does not silently skip, and is not filed as a hardware defect against the seller's return clock —bmc_secure_refusal_ownerroutes an access state to a PartsHold, because a firmware we cannot yet drive is not a defect of the unit that was shipped.That ordering matters more than usual right now: the controller answers no ARP from its own /24, so a producer assuming a transport would fail at the wire rather than at the model.
Four witnesses, paired so neither arm passes alone
MegaRAC refuses and OpenBMC routes, over the same fold — a witness that only asks the unavailable arm cannot distinguish a correct route table from one that refuses everything, and refusing everything would fail the OpenBMC fleet too, invisibly. The application fold gets the same treatment: unavailable must yield
AccountManagementUnavailablespecifically (returningAbsentwould let a caller proceed and adjudicate into "nobody tried" rather than "there is no way to try"), and available must yieldAbsentso an implementation refusing unconditionally cannot pass.Placement
Dispatch sits in the workflow layer rather than in either extdeps module, per DESIGN §3: the dispatch that selects a realization is itself realization.
extdeps.bmc.redfishandextdeps.bmc.megaraceach own their surface and neither learns the other exists.The frontier names the capability — an executed MegaRAC user-management request committing its shape and response — and explicitly refuses satisfaction by authoring a row from documentation, from the srv3/srv4 Redfish shape, or from the uncommitted #10630 attempt.
Not claimed
No rotation is performed and none can be from here. This lands the route and the refusal; the producer that consumes it needs a live controller and an executed endpoint, neither of which exists today.
🤖 Generated with Claude Code
https://claude.ai/code/session_01CHmuTG7e714e4VEE5zAaju