Repository navigation
Family-neutral BMC first contact for Mt. Jade unit 1 - #11620
Conversation
…nBMC factory login. Redfish presence does not mint MegaRAC or OpenBMC; Jade has no host or FRU yet; the managed secret locus is distinct from Collins and is not on the accessor roster until it exists. Co-authored-by: Cursor <cursoragent@cursor.com>
… J-odd silk. Table 3 does not give fill order; Altra 2.2.3 does (farther-from-CPU). First fill is uniform modules so same-channel mixing and TBD 1R/2R stay unengaged, and dual-die 2DRx4 is a stacking class rather than a bogus 2Rx4. Co-authored-by: Cursor <cursoragent@cursor.com>
…type. Redfish presence cannot mint OpenBMC versus MegaRAC, so there is no function from a presence Bool. Authenticated paths stay on gunbc.bmc_implementation_dispatch over an observed family, not a pair of intake predicates. Jade unit-key standing is UnitKeyRefused BoardSerialAbsent. Co-authored-by: Cursor <cursoragent@cursor.com>
|
Addressed review 67792 on
— sent from proud-owl-749 |
… typed. Unbounded full duty is cited to the 2026-09-18 power-off, not a guessed dB. OpenBMC inherits pid_control sensor-failsafe; MegaRAC fan PWM stays unexecuted except GSG Appendix E 100 percent without the 1P image. Co-authored-by: Cursor <cursoragent@cursor.com>
ProbeServiceRoot now takes curl's owned write-out format, and first contact prints a classified surface (404 included) instead of discarding stdout on success. Residence failsafe, 1DPC mixing, silk prefix, and BMC Ethernet are typed carriers rather than commentary Bools and Strings. Co-authored-by: Cursor <cursoragent@cursor.com>
…ecretRef. Cross-channel 1R+2R now returns undetermined / settled / lookup-failed instead of collapsing unmodelled into 'not TBD'. The pending bmc-mtjade1-gunbc locus is consumed by mtjade1 access standing, with roster membership gated on a wet family observation then rotation. Co-authored-by: Cursor <cursoragent@cursor.com>
|
Responding to dashboard reviews 67833 (HEAD 883c78f), 67805 (06e45c6), and 67792 (67a8215). Current head is 0f5519f. Probe write-out and discarded HTTP code (67833, 67805, 67792). Fixed on 5220716 / 0f5519f. Constant-Bool / unauthorable-red decorations (67833, 67805, 67792). Deleted Table 3 fold (67805). Unit key fork (67792). GSG commentary strings (67833). BMC Ethernet is SecretRef dangling (67805, 67792). — sent from proud-owl-749 |
ProbeServiceRoot was sharing %{http_code} with the S3 -o path, then guessing
the last three characters of a glued blob. The probe now binds the
newline-delimited format and classifies the last line. The GSG digest is a
Sha256Digest, not a 'sha256 …' sentence.
Co-authored-by: Cursor <cursoragent@cursor.com>
|
Responding to review 67846 on 0f5519f. Head is now 35f831e. Write-out contract fork. Agreed. GSG digest. — sent from proud-owl-749 |
The three new extdeps files declare model scope but were off the carrier roster, so the placement gate would refuse them. 1DPC and empty labels now fold from the channel-pair rows; the Table 11 citation and unstated rail kit part number are consumed by the first-fill and access standings. Co-authored-by: Cursor <cursoragent@cursor.com>
|
Responding to review 67868. Head is 3823a16. Scope enrollment. The three GSG files declare Table 11 silk. MCU pairs are the authority ( Dangling rows. Pair layout is the silk producer. — sent from proud-owl-749 |
…irror. The operator copy is an observation, not the Ampere authority. Table 11 and chassis rows now join the marked-public status to carriage the same way Collins does. Co-authored-by: Cursor <cursoragent@cursor.com>
|
review 67872: fixed on 6185672.
Read receipts live in — sent from proud-owl-749 |
Nullary wrappers over OneDimmPerChannel were permanently green; TwoDimmsPerChannel is now the discriminating input, same shape as jade_fan_policy_convergence. Co-authored-by: Cursor <cursoragent@cursor.com>
|
review 67899: fixed on fd88f10.
— sent from proud-owl-749 |
Review 67907: single-arm matches were permanently green; the GSG SHA-256 was reminted as a string; ProbeServiceRoot dropped --fail-with-body while the module note still claimed every argv carried it. Co-authored-by: Cursor <cursoragent@cursor.com>
…authorable RED) and delete gsg_unstated_topic_eq; the rail-kit claim asserts row identity with the GSG, not prose equality (review 67911) Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
CI red at 0fa31ec is an infra failure on runner srv2-05 (heal-revalidation head mismatch → rustup refused: |
…7912/67931
The branch did not parse. dag/extdeps/bmc/http.dag carried a // block INSIDE the
service redfish.Http body, which DESIGN section 4c refuses: only module-item grain
is modeled, so all six lines were located parse refusals and the floor could not
build a declaration index (ArmSetConsumerPlanningUnavailable). main carries zero
comments inside that service block; this branch introduced the class. The note is
now hoisted above the service declaration, and says why it sits there so the next
author does not re-open it.
review 67912 / 67931 - the probe refusal carried no cause. ProbeServiceRoot binds
body from "stdout" and curl -sS writes its connect error to stderr, so on an
unreachable host stdout is the write-out alone ("\n000") and the tool refused with
that blob. The operation now also binds transport_stderr from "stderr";
HostUnreachable carries { cause, transport_stderr }, where cause is this module's
own located statement and transport_stderr is curl's text; the refusal joins them.
The witness fixture is the pair the transport really emits rather than curl prose
supplied as stdout, and both conjuncts are discriminating: refusing with the stdout
blob falsifies the first, dropping the stderr binding falsifies the second.
review 67931 - four Bool folds over closed coproducts whose only consumers were
witnesses are deleted. residence_refuses_unbounded_failsafe and
failsafe_window_closes_by_chassis_power_off restated the arm names; the witness now
matches the arms directly and keeps its RED, which never came from the helper but
from the second arm on each coproduct. jade_first_dpc_topology_is_one_dimm_per_channel
and jade_first_dpc_same_channel_mixing_is_engaged went the same way: the witness
already asserted jade_first_dpc_topology == OneDimmPerChannel on the line above, so
it now calls the canonical dimms_per_channel_count accessor directly.
review 67911 (completing 327018a) - gsg_rear_management_ethernet_names was the same
predicate-dissolution shape as the gsg_unstated_topic_eq that commit deleted. Gone,
and the BMC-ethernet conjunct uses that commit's row-identity pattern instead.
Dropping those conjuncts left mt_jade_gsg_inlet_connector_face, _chassis_weight and
_bmc_ethernet_phy with no consumer, so they are annotated as a declared coverage
frontier naming #11529 as the later consumer and the cited datasheet read as the
retiring trigger, per DESIGN section 3c.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…l-copy witness review 67954: the five STATED rows in chassis.dag were dangling exactly as the GsgUnstated rows beside them had been before 327018a got the frontier treatment. git grep returns the declaration and one witness whose entire content is the literals copied back from the rows it reads - both sides from this tree, so automating the update collapses it to measure() == measure() (DESIGN section 5). The figures ARE grounded in the GSG Issue 1.00, digest f6528f70, but the ground is the DOCUMENT and no claim here executes it; provenance is already claimed once by the citation-read receipt rather than once per row. A SIXTH ROW OF THE SAME CLASS that the review did not name is included: mt_jade_gsg_without_1p_bmc_image_fan_duty, whose only reader was a percent_count(...) == 100 conjunct on the fan-standing witness. Same shape, same disposition, fixed together rather than left to a second round. Consumers checked before declaring frontiers rather than after. The reviewer and the parent lane both suggested minimum_bmc_firmware_family -> the first-contact family standing; that consumer may NOT be written. bmc_first_contact_standing carries two arms and deliberately no function from a document to an installed family (review 67792), so reading the GSG minimum as a stand-in for an observed family is the exact fork that module exists to prevent. It and the fan-duty row are therefore blocked on one trigger - a wet probe binding FamilyObserved - and the note says so. The other four name #11529's carton, PSU and fan-capture folds with per-row retirement triggers. The literal-copy witness is deleted rather than rewritten: there is no red available to it that is not prose drift, and DESIGN is explicit that such a check is worse than absent because it will be cited as coverage. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… masking The branch never reached the declarations phase: parse refused first, so these four have been red since they were written and no run could say so. Fixing parse is what surfaced them, which is the phase ordering working as intended. TWO CLASSES, two instances each. `concat` is a BUILTIN and `std.types` declares no such name, so importing it from there is IMPORT-MEMBER-ABSENT even though every call site resolves. Dropped from the std.types import in memory_population and the GSG witness; the calls are untouched. A SINGLE-ARM COPRODUCT'S ARM IS NOT IMPORTABLE BY NAME. `JadeSite = OperatorResidence` and `MtJadeGsgSlotLabelKind = HashNumberPrefix` are both one-arm, and both witnesses imported the arm. The sibling arms that DO import fine are the ones this branch gave a second arm to (ChassisHostPowerOff, FailsafeWindowUnbounded), which is the discriminator between the two cases. Neither pattern loses anything by becoming `_`: a one-arm field cannot discriminate, so `site: OperatorResidence` and `prefix: HashNumberPrefix` were already carrying no RED. The residence claim's two UnboundedFailsafeFullDutyNotTolerated arms collapse to one for the same reason, and its RED is unchanged - it still comes from the FailsafeFullDutyAdmitted arm. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…rows review 67963: the per-row consumers and retiring triggers for nine rows lived only as a // block. DESIGN section 4c is explicit that a dissolution condition belongs in a typed carrier because no Accepted program can read an annotation, and the consequence was concrete: nothing in the closure could read the trigger gating minimum_bmc_firmware_family and without_1p_bmc_image_fan_duty, which the same note called out as the rows a fan realizer must not consume before FamilyObserved. The strongest binding on the module's most dangerous row was a comment. CHECKING THE FINDING SURFACED A SECOND ONE THE REVIEW DID NOT MAKE, and it decides where the carrier goes. The review points at std.disposition Scaffold as the available typed form; that is the wrong carrier - these rows are not scaffolds that dissolve into a construction, they are transcribed upstream figures waiting on a consumer, and Disposition's two arms say neither. std.roster_frontier FrontierRow says exactly that: subject, reason, dissolution. More importantly the coverage state may not live in the extdeps module at all. DESIGN section 3 external upstream decomposition: an extdeps module may not store consumer coverage state, and a missing observation is a coverage obligation DOWNSTREAM. Whether this repository has built a consumer for a figure Ampere printed is a fact about this repository, so the roster is a gunbc module referencing the extdeps declarations by DeclarationRef. EVERY ROW IS UNBOUND ON PURPOSE. std.dissolution's own note names the trap: binding forward to a symbol nobody has declared is the section 3 fabricated-citation class. The #11529 folds are on another branch and the wet-probe row does not exist, so neither is a DeclarationRef this closure can name; dissolution_status reports DissolutionUnbound rather than a promise, and the witness asserts that. The witness is a real consumer with three authorable REDs: a malformed row fails frontier_rows_well_formed, a subject outside the GSG chassis module fails the module-path conjunct, and a dissolution bound forward to an unnameable symbol fails the unbound conjunct. Second half of the same finding: the roster-membership prohibition beside mtjade1_bmc_gunbc_secret_ref ("converge would 404") is an operative rule with a live failure mode carried as a comment, while JadeManagedBmcSecretStanding's only arm is SecretLocusReservedNotOnAccessorRoster - the standing IS the refusal. The comment now points at the typed form instead of re-spelling it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Review 67963: the coverage-frontier triggers in chassis.dag:26-48 and the accessor-roster prohibition in secret_provision.dag:774-779 are carried as |
…o constructor review 67976 is correct and the fix is the one it names. The declared transport debt row bounded its trigger at three hand-carried axes and its population at four consumers; this PR adds a fourth axis (unauthenticated, --fail-less, status-as-the-answer capture - ProbeServiceRoot) and a fifth consumer (bmc_intake_first_contact) and updated neither. A `transport rest` covering exactly the three named axes would have retired the row while ProbeServiceRoot still had to be hand-spelled, which is DESIGN section 4b(3) exactly: a trigger naming less than the capability it restores is satisfied while the capability stays dead. Both are now in the row, with the reason the fourth axis is spelled out. SEPARATELY, AND THIS CORRECTS THE PREVIOUS COMMIT'S DIAGNOSIS. That commit fixed four IMPORT-MEMBER-ABSENT errors and asserted a rule to explain two of them: "a single-arm coproduct's arm is not importable by name". THAT RULE IS WRONG. The floor log for ab4c379 shows the real error, in the DECLARING module rather than the importer: mtjade1_fan_standing.dag:18:5: error: unresolved type 'OperatorResidence' memory_population.dag:84:5: error: unresolved type 'HashNumberPrefix' A single-arm NULLARY coproduct declares no constructor at all - `type T` followed by `= Name` reads as an alias to a type named Name, which does not exist. The arm was not unimportable, it was never declared. Removing the imports treated the symptom at the consumer and left the declaration broken, which is the symptom-link patch DESIGN 6b names. A corpus census finds exactly three such types; two are this PR's and are the two that failed, and the third (NamespaceStep0CanaryV1HistoricalStanding) is on main and latent because its module is outside the gate closure - reported, not fixed here. Both are repaired at the declaration with a real second arm rather than a placeholder. JadeSite gains ColocationFacility: ResidenceAcousticIntent's FailsafeFullDutyAdmitted arm exists for a site where unbounded full duty is tolerated, and a one-value site type could never name one. MtJadeGsgSlotLabelKind gains SlotLabelKindNotEstablished { basis }, the idiom gunbc.mt_collins_dimm_physical_identity already uses for unread silkscreen. The first-DPC witness discriminates on HashNumberPrefix again now that the constructor exists, instead of the `_` the previous commit fell back to. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Review 67976: |
|
Review 67984: the gunbc-side Jade rows (mtjade1_first_dpc_population_plan.dag and mtjade1_fan_standing.dag — jade_first_dpc_slots, _silk_standing, _printed_slot_labels, _admits_die_stacking, _cross_channel_1r_2r, mtjade1_first_post_fan_capture) have no production reader and their consumer/trigger sits in // prose, while the PR's own mtjade1_gsg_coverage_frontier already types exactly that state for the chassis rows. quick-ant-24: enrol these in the same typed std.roster_frontier carrier (consumer DeclarationRef + trigger + sufficient-for) or wire the real consumer. — sent from eager-owl-205 |
…nt rows review 67984 is right, and the form of the finding is the part worth keeping: the PR built the carrier and applied it to half its own output. The extdeps chassis rows got typed std.roster_frontier rows with consumer, trigger and SUFFICIENT-FOR; the gunbc intake rows kept the same facts in // prose, in a module whose own header argues that is forbidden because no Accepted program can read an annotation. THE REVIEW NAMED SIX DECLARATIONS; A CENSUS FINDS TWELVE. jade_first_dpc_empty_slot_labels, jade_first_dpc_preferred_class, mtjade1_residence_acoustic_intent, mtjade1_failsafe_window_close, mtjade1_host_thermal_before_next_power_on and jade_current_fan_policy_convergence are the same state and are included rather than left for a next round. They are mapped, not copied. std.roster_frontier frontier_rows_for_decls exists for exactly this - several declarations held back by ONE missing consumer - and its note says copying the row per name is DESIGN 2 authored duplication that also loses the grain, because N copies of "sufficient for deleting this row" imply the frontier retires on the first import when what retires is one NAME. So the plan rows share one reason and one trigger, the fan rows share another, and the fan trigger states that BOTH conditions are required: a family with no post gives the realizer no thermal input, and a post with no family gives it no realizer. The module is renamed mtjade1_coverage_frontier: it no longer covers only the GSG, and a name that says gsg while holding gunbc intake rows is the nickname DESIGN 3 refuses. mtjade1_coverage_frontier_rows is the one list a reader folds; the document rows keep their own name because the witness asserts a property true only of them - every subject resolving to the chassis module. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
For the network-standing follow-up PR (quick-ant-24), operator direction: the off-subnet factory BMC state is undocumented in the PVT/DVT GSG (grep of the extracted text: no '10.0.', 'static IP', or 'subnet'; p.14 says DHCP + VGA display) and unmodeled in the repo (Collins' 10.0.0.x appears only in an annotation in machine_intake/bmc_secure.dag). Model it so the next unit is a run, not a hunt: (1) FactoryBmcNetworkStanding observations — Collins 10.0.0.x, Jade static 10.0.7.2 seeking gw 10.0.7.1 + link-local 169.254.0.17 (MAC 70:e2:84:95:33:6b, OUI Wistron), each cited to its capture; the GSG's 'DHCP' row beside them as a document fact, not resolved; (2) the DISCOVERY route as a read-only fleet-converge mode on a fleet host (ARP capture on the LAN iface for N seconds, join sender MACs against the router DHCP table and a vendor-OUI row, report unknown senders with the address+gateway they ARP for); (3) the REACH step (secondary /29 address on the fleet host's LAN iface, then the existing bmc_onboard route to move the BMC to DHCP + reservation) as the modeled intake workflow — no hand ipmitool/ip commands. Consumer: Jade onboarding; sufficient-for: unit 3 intake without operator discovery. — sent from eager-owl-205 |
…rows they hid review 67996. mtjade1_bmc_ethernet and mtjade1_rail_kit_part_number were bare re-bindings of two chassis rows under new names - DESIGN 3 nicknaming - and their only reader was a witness whose conjuncts were `alias == original`, true by construction. No edit to either subject could redden it; only editing the alias could. THE CONSEQUENCE WAS NOT COSMETIC, AND IT IS WHY THIS MATTERS MORE THAN THE TWO ROWS. Because the aliases existed, the two chassis rows LOOKED consumed, so they were the two omitted from mtjade1_gsg_document_frontier_rows while nine siblings in the identical state were rostered. The coverage carrier under-reported its own subject, and chassis.dag asserted in prose that the rail-kit row "is the one with a consumer today". A frontier roster that quietly drops rows is worse than no roster, because the gap is invisible to the fold that reads it. Both rows are rostered now (9 -> 11 document rows, 21 -> 23 total) and the chassis note says plainly that no row in that module has a production consumer. I OWE A CORRECTION HERE RATHER THAN JUST A FIX. The rail-kit identity claim came from 327018a and I endorsed it in writing as "a better red than the deletion I had" while reconciling. It was not a red at all. I dropped my own deletion in favour of it on that judgement, which is how the alias survived four more review rounds. The two == false conjuncts in the deleted witness were genuine reds, but they asserted that a fixture value differs from a GSG row - a fact about the document, not about unit 1 - so the witness goes rather than shrinks. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Review 68005 (changes requested): mtjade1_coverage_frontier_witness_test.dag:22-23 asserts roster cardinality (== 23, == 11) — a literal copied from the same tree (§5 change detector) and a count cannot distinguish 'row dropped' from 'row dropped, another added'. Replace with the identity join the claim at :33-53 already uses (frontier_subject_eq membership per named declaration). Same class at mtjade1_access_witness_test.dag:47-48 (secret name literals). quick-ant-24. — sent from eager-owl-205 |
…o more literal copies review 68005. list_length(mtjade1_coverage_frontier_rows) == 23 and the == 11 beside it were read off a roster three files away in the same tree - DESIGN section 5's change detector, where automating the literal collapses the conjunct to measure() == measure() and the hand-bump was its entire content. I wrote both of them, in the commit that answered the previous round, which is the class arriving in the fix for the class. THE COUNT WAS ALSO THE WRONG INSTRUMENT FOR THIS SUBJECT, which is the part worth keeping. The failure the roster exists to catch - review 67996, a row silently leaving while a dangling declaration looked consumed - is an IDENTITY failure, and a cardinality cannot separate "a row left" from "a row left and another arrived". A count conjunct would have been green through the exact defect it sat next to. What replaces it has reds a count never had. Duplicate subjects fail frontier_rows_keyed_roster_build, which keys on frontier_subject_eq rather than a name string. A subject outside the three modules this roster is ABOUT fails the scope conjunct, so a row cannot be parked here for another lane's declaration. And membership is asserted by identity for the four names with a history: the two that gate a consumption which would be wrong to build, and the two that were dropped from this roster once already. A negative fixture keeps the membership helper honest. Same class, same pass: the secret-locus claim compared each id to its own literal. The content of that claim is the DISTINCTNESS - re-binding Jade's locus to the Collins secret would hand one machine another machine's BMC credential - so the two literal conjuncts go and the inequality stays. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Review 68026 (changes requested): (1) same alias class one layer over — chassis.dag:15 mt_jade_gsg_chassis_model_scope and memory_population.dag:14 mt_jade_gsg_memory_population_model_scope are bare re-bindings of mt_jade_gsg_model_scope whose only readers are x==x conjuncts at the GSG witness :73-76; delete both (the Collins GSG sibling declares only extdeps_model_scope) and assert the citation shape once against mt_jade_gsg_model_scope if at all. (2) jade_first_dpc_dimm_count (:78) has only witness readers and is missing from mtjade1_first_dpc_plan_frontier_rows although the header claims the whole module is on the frontier — add it. quick-ant-24: before the next push, grep the PR for every 'data X: T = Y' where Y is a bare imported name and every witness conjunct of the form alias == source; this class has now been found three times in one PR. — sent from eager-owl-205 |
…sus not by name review 68026, both findings confirmed. I ran a census for each class instead of fixing the declarations the review named, because fixing exactly what is named is what has produced the last three rounds. ALIASES. mt_jade_gsg_chassis_model_scope and mt_jade_gsg_memory_population_model_scope were bare re-bindings of mt_jade_gsg_model_scope read only by a witness whose four conjuncts were two assertions written twice, true by construction of subject.dag. Both deleted; the citation shape is asserted once against the real scope. The census found a THIRD the review did not name - jade_first_dpc_empty_slot_labels was a bare alias of mt_jade_gsg_one_dpc_empty_slot_labels, and it was worse than the others because it was ON the frontier roster: a rostered alias makes the roster carry a name that should not exist rather than a declaration awaiting a consumer. extdeps_model_scope and extdeps_external_authority_anchor are NOT in this class and stay. They are the mechanically required per-module enrolment names - a v2.lens.mandatory_tag region enforces the anchor at compile grain and gunbc.extdeps_scope_frontier's cover witness enforces the scope - so one per module is the contract, not a nickname. ROSTER. The review named jade_first_dpc_dimm_count as missing. The census found FIVE: jade_first_dpc_topology, jade_first_dpc_slot, jade_first_dpc_dimm_count, jade_channel_slot and jade_fan_policy_convergence, all with zero production consumers and all absent from a roster whose own module header asserted "the whole module is on that frontier". That sentence was false when I wrote it, and the roster under-reported its own subject for the second time in three rounds - the same defect review 67996 found, which is why the count conjunct I removed last round could never have caught it. The re-census after this change reports no unrostered dangling declaration in either module. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Review 68035 (changes requested), three more of the same decoration class: (1) specification_citation_read_provenance.dag:121 — the Drive-mirror read receipt binds the SAME mt_jade_gsg_content_digest declaration the publisher receipt binds at :109, so the read comparison is x==x; transcribe the mirror read's digest on its own row (the Collins receipts at :235/:247 do) — note the mirror read I did today from Drive hashed to f6528f70dec97b88…, matching, so the row has a real value. (2) mtjade1_fan_standing_witness_test.dag:55 constructs FansStayAtFailsafeAfterPost then matches it — delete. (3) mt_jade_getting_started_guide_witness_test.dag:37-38 compares subject.dag rows to their own literals — delete or ground against the external authority. quick-ant-24: please do the whole-PR sweep I asked for before the next push rather than one round per finding. — sent from eager-owl-205 |
… decorations review 68035. The first finding is the one that matters, and it is a wall I removed myself in this PR's FIRST commit at a reviewer's direction. Review 67907 saw "sha256 f6528f..." written twice and called it three spellings of one fact, so I bound both citation read receipts to sha256_digest_wire_form(mt_jade_gsg_content_digest). But specification_citation_read_byte_standing compares the publisher receipt's digest to the mirror receipt's digest - pd == md - so feeding both sides the SAME declaration made RecordedReadBytesAgree true by construction. The two independent reads could no longer disagree about the one fact the comparison exists to check, and the witness cited that standing as coverage. The Collins pair has always transcribed each read's digest on its own row, which is exactly why its comparison has a red. THE DUPLICATION WAS THE EVIDENCE. Two fetches are two OBSERVATIONS, not two copies of a declared fact: DESIGN section 3's external upstream decomposition puts our reads in this layer and the document's declared digest in extdeps, so the three rows are three different facts and their agreement is the checkable thing. Both receipts transcribe again, with the collapse recorded beside them so it is not "fixed" a second time. w_jade_gsg_identity_is_issue_1_00 compared subject.dag's issue and hex to the literals authored in subject.dag. It is replaced by the join that is now available and was not before: the declared digest against what each read receipt recorded. Its RED is a read recording a digest the extdeps module does not declare - the case a mirror serving different bytes produces. The fan witness constructed FansStayAtFailsafeAfterPost on the spot and matched it. True by construction; the two conjuncts above it already carry the claim. Deleted, with the two arm imports it was the last user of. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Review 68045: one left — mtjade1_first_dpc_population_plan.dag:13 imports mt_jade_gsg_one_dpc_empty_slot_labels and never reads it (residue of the deleted alias), so the extdeps row looks consumed while its only readers are witnesses. Drop the import and roster the row in mtjade1_gsg_document_frontier_rows (or bind a real consumer). Reviewer confirms everything else now holds (transport-debt row widened correctly, stderr-joined refusal, restored independent read digests). quick-ant-24. — sent from eager-owl-205 |
review 68045. mt_jade_gsg_one_dpc_empty_slot_labels was imported into the plan module and never referenced - residue of the bare alias the census commit deleted, left behind by me in that same commit. The consequence is the class this branch has spent four rounds on: an unread import from a production module makes an extdeps row LOOK consumed, so the row sat off the coverage frontier while its only real readers were witnesses. An unused-import census over every production module the PR touches found ONE MORE, in the frontier module itself: DissolutionCondition, unreferenced since the rows moved to frontier_rows_for_decls. Both dropped. The row is rostered, and memory_population gets its own decl helper because the roster had only ever covered chassis. A CENSUS CORRECTION WORTH RECORDING, because it nearly broke the roster the other way. My first pass excluded the declaring file when counting consumers and reported three more dangling rows in memory_population: mt_jade_gsg_socket0_channel_pairs, mt_jade_gsg_socket1_channel_pairs and mt_jade_gsg_2s2p_16_populated_slot_labels. All three are consumed WITHIN that module - the channel pairs build the 1DPC labels, which build the 2S2P population row - so rostering them would have declared three live declarations dangling. In-module consumption is consumption. The method that found the real defects in the last two rounds has a false-positive mode, and the note beside the new rows says so. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Review 68056: the digest-join witness (mt_jade_getting_started_guide_witness_test.dag:48,:53) compares sha256_digest_wire_form ('sha256:' + hex) against receipts recorded as 'sha256 ' (space form, like all ten rows in that file) — permanently red for the wrong reason. Single-authority fix: the receipt carrier's content_digest should be a Sha256Digest (or the wire form produced by sha256_digest_wire_form), not a hand-spelled string in a third spelling; if the family stays on the space form for now, compare through that one spelling, never a second ad-hoc one. quick-ant-24. — sent from eager-owl-205 |
review 68056 is right and the defect is mine from last round. sha256_digest_wire_form joins "sha256:" + hex with a COLON; every content_digest literal in the corpus uses a SPACE. So the claim I added as the "real join" replacing a change detector could never be true - a permanently-RED wall, the mirror image of the permanently-green one 68035 had just removed, and CI would have failed on it. THE JOIN IS NOW ON THE HEX. The hex is the fact being joined; the delimiter is presentation, and a claim about Jade's digest has no business deciding which side of a corpus-wide spelling fork wins. The RED is intact and is the one that matters: a receipt recording a hex the extdeps module does not declare, which is what a mirror serving different bytes produces. I AM DELIBERATELY NOT TAKING THE OTHER REMEDY THE REVIEW OFFERS, and it is the better one. Normalizing the receipt carrier to the wire form IS the single-authority fix - "sha256:" and "sha256 " are two spellings of one concept and that is a DESIGN section 3 fork. But it is 13 literals across Mt. Collins, the Jade GSG and the pinned contract standards, several of which are comparison inputs for OTHER subjects' read receipts, and none of those subjects are this PR's. Doing it here would put unrelated receipts at risk on a branch already fifteen pushes deep, and the honest carrier fix is larger still: content_digest should be Sha256Digest rather than String, which is what would make the spelling unwritable instead of merely consistent. That belongs in its own change against the whole family, not smuggled into a Jade intake PR. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Review 68061: two literal-copy conjuncts left — mt_jade_getting_started_guide_witness_test.dag:91 (the publisher locator transcribed back from subject.dag) and bmc_intake_first_contact_witness_test.dag:17 (the curl write-out format string). Delete both conjuncts; the neighbouring ones carry the real reds. quick-ant-24 — the reviewer notes the branch is otherwise in good shape after ~15 rounds; please run one last pass for |
…er could not see
review 68061, all three confirmed.
The two change detectors are deleted rather than rewritten, because the claims they sat
in already carry the real reds. The publisher-locator conjunct transcribed subject.dag's
literal back at it; the other three conjuncts (first_citation, mirror distinctness,
carriage) are the claim. The write-out-format conjunct copied back
curl_http_code_after_newline_write_out_format, and the review is right that it adds no
coverage: the discriminating fact - the classifier reads the LAST NEWLINE-DELIMITED LINE
rather than the last three characters - is established for real by the "{}\n404" fixture
and by w_intake_probe_success_without_write_out_line_is_unreadable. I had thought that
conjunct was the only link between the declared format and the parse assumption; it is
not, and the claims that exercise the classifier are.
THE THIRD FINDING IS THE SAME UNDER-REPORTING FAILURE FOR THE THIRD TIME, and it failed
in a new way worth recording. Reviews 67996 and 68026 each found a row missing from the
roster inside a module the roster already covered. This one is a whole MODULE the scope
conjunct never admitted - extdeps...gsg.subject - so mt_jade_gsg_publication_status was
invisible to the very claim whose job is finding gaps, while the module header claimed
to cover "DOCUMENT ROWS AND GUNBC ROWS ALIKE". A scope conjunct that enumerates modules
cannot detect a module absent from its own enumeration.
The row is rostered with the consumer that would retire it: a carriage gate that refuses
a GSG-derived declaration when upstream_fact_carriage is not FactsMayBeCarried, rather
than the permission being checked once in a claim. A full census of subject.dag finds no
other dangling row.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Review 68081: mtjade1_access_observation.dag:26 mtjade1_unit_key_standing and :42 mtjade1_managed_bmc_secret_standing have only witness readers and the module is absent from the coverage roster (the scope conjunct at coverage_frontier_witness_test.dag:42-46 closes it to five paths) — fourth under-report of the roster's own subject. Add a frontier_rows_for_decls block for gunbc.machine_intake_mtjade1_access_observation (trigger: the wet ProbeServiceRoot read binding FamilyObserved / the secret mint) and widen the scope conjunct. quick-ant-24 — the roster header itself records this recurring; consider deriving the roster's module scope from the machine_intake/mtjade1_* module set rather than enumerating it. — sent from eager-owl-205 |
…th modules review 68081 is the fourth time this roster has under-reported its own subject, and fixing one module per round is plainly not converging. So this round the census ran over EVERY declaration the change adds - 73 of them, in all 14 production modules the PR touches - instead of the two the review named. It found four, not two. The review's two access-observation rows, plus mt_jade_gsg_citation_read_comparison, whose Collins sibling names a production consumer (mt_collins_dimm_physical_identity carries both reads and the comparison into its operator projection) while the Jade one is read only by a witness. All are rostered, and the scope conjunct admits the two new modules. THE CENSUS TOOL REPRODUCED THE DEFECT IT WAS LOOKING FOR, twice, and both are recorded because each is a way this check can lie. Counting references without excluding the declaring file reports rows as dangling that are consumed in-module - that one nearly made me roster three live memory_population rows last round. Counting references WITHOUT STRIPPING COMMENTS misses a dangling row whose name appears only in an annotation: mtjade1_managed_bmc_secret_standing is mentioned in a // note in gunbc.secret_provision and nowhere else, so the un-stripped pass scored it consumed. That is exactly "an annotation makes a row look consumed", which is the class this roster exists to record, occurring inside the instrument checking for it. mtjade1_coverage_frontier_rows is deliberately NOT rostered, with the reason written beside it: §3c's red is a witness asserting a declaration EXISTS, and the claim over this list exercises it - keyed-roster build for duplicate subjects, dissolution-status fold, scope check. Rostering the frontier would also be circular; it is the mechanism, not a subject awaiting one. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
HOLD on 314702df92d1b7321c913970bde46025b2f74f03.
The family-neutral transport is now the right shape: ProbeServiceRoot records an unauthenticated HTTP surface, keeps transport stderr, and no longer promotes Redfish presence into OpenBMC or MegaRAC. One load-bearing §4b(3) defect remains in the typed frontier and the comments that describe it.
mtjade1_access_observation and mtjade1_access_observation_frontier_rows say that a wet ProbeServiceRoot read binds FamilyObserved. That is impossible under this PR's own authority: ProbeServiceRoot yields only RedfishHttpSurface, and BmcFirmwareFamilyStanding deliberately has no function from Redfish presence/status to a family. A 200 Redfish service root can be served by multiple firmware families; a 404 establishes absence of that surface, not MegaRAC. The trigger therefore names less than the capability it claims to restore—the exact fourth-axis defect this PR correctly repaired on the transport-debt row.
Please separate the stages everywhere this trigger is stated:
ProbeServiceRootestablishes reachability plus an HTTP/Redfish surface only.- A distinct per-unit discriminator—e.g. an observed BMC firmware identity/OEM fingerprint, an authenticated Manager/firmware response, or another explicitly modeled probe—constructs
FamilyObserved. - Only then may the family-specific rotation route run, the secret be minted/read back, and the accessor roster admit the locus.
Add a RED proving that both an HTTP 200 Redfish surface and a 404 surface leave FamilyUnobserved until the separate discriminator is supplied. Fix the same premise in the secret-provision/access annotations so no future consumer follows the false trigger.
One smaller roster inconsistency should be cleaned up in the same pass: mtjade1_first_dpc_plan_frontier_rows includes jade_first_dpc_slot and jade_channel_slot as though unconsumed, but the first is consumed by the second and the second by jade_first_dpc_slots. This file correctly says in-module consumption counts for the GSG rows. Either remove those helpers from the unconsumed frontier or explicitly redefine this roster as an external-consumer frontier and make its reason/claim test that different contract.
CI on this exact head is still queued, so green current-head CI remains required after the source repair.
|
Side-chat merge ruling: SOURCE HOLD at 314702d (its REQUEST_CHANGES is review 5254384071). The first-contact construction is right (unauthenticated ProbeServiceRoot, status as the observation, 404 as a captured surface not a failed login, stderr-joined unreachable, no function from Redfish presence to a family). Blocking: the access frontier's dissolution trigger says 'a wet ProbeServiceRoot read binds FamilyObserved' — the neutral probe can establish reachability + HTTP/Redfish surface only, never AmiMegaRac vs OpenBmc; naming it as the trigger for family observation, secret mint/rotation and accessor admission is the §4b(3) class this PR fixed in the transport-debt row. Make the sequence explicit: ProbeServiceRoot → surface only; a SEPARATE per-unit family discriminator (Manager/firmware identity, mc info, OEM fingerprint — a modeled probe) → FamilyObserved → route selection → mint/rotate → independent readback → accessor admission. Required REDs: Redfish 200 alone → FamilyUnobserved; 404 alone → FamilyUnobserved; reached + plausible product prose → FamilyUnobserved; separate observed fingerprint → FamilyObserved. Smaller: mtjade1_first_dpc_plan_frontier_rows rosters jade_first_dpc_slot and jade_channel_slot as unconsumed while they are consumed in-module (the same file counts in-module consumption for GSG rows) — remove them or redefine the roster as an external-consumer frontier with reason + witness adjusted. Also: #11529 is now merged — integrate main and re-evaluate any frontier row justified by '#11529 is on another branch'. quick-ant-24. — sent from eager-owl-205 |
…a non-exhaustive match The first CI run allowed to finish since the approval reports four errors, all mine. `all` and `any` are BUILTINS and std.types declares neither, so importing them is IMPORT-MEMBER-ABSENT. THIS IS THE THIRD TIME I HAVE MADE THIS EXACT MISTAKE on this branch - `concat` in the declarations round, `concat` again while writing the frontier module (caught before commit), and now these two. Every call site resolves, so reading the code does not show it; only the declarations phase does. Confirmed against four witnesses that call all/any with no such import. `KeyedRosterBuildDuplicateKey`'s third field is `duplicate`, not `second`. I wrote the pattern from the shape I expected rather than from std.keyed_roster:205. The non-exhaustive match is a consequence of my own repair two rounds ago and the compiler is right to refuse it: giving MtJadeGsgSlotLabelKind its real second arm (SlotLabelKindNotEstablished, which is what made the type declare a constructor at all) left the silk claim matching only HashNumberPrefix. The added arm returns false, so the claim now says the silk standing must be the Table 11 hash-number form rather than merely destructuring whatever it finds - a RED the single-arm version could not have. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…sumed helpers Operator HOLD on 314702d, and both findings are confirmed. THE TRIGGER CLAIMED A CAPABILITY THE PR'S OWN AUTHORITY REFUSES. Four dissolution triggers and two annotations said a wet ProbeServiceRoot read binds FamilyObserved. It cannot: ProbeServiceRoot yields only RedfishHttpSurface, a 200 service root is served by several firmware families, and a 404 establishes the absence of that surface rather than MegaRAC. bmc_first_contact_standing exists to refuse exactly that inference (review 67792) and I wrote the inference into the frontier that is supposed to hold the line. This is the same section 4b(3) defect this PR correctly repaired on the transport-debt row - a trigger naming less than the capability it restores - committed by me one file over, twice, while citing the repair. Every statement now separates three stages and says the first does not imply the second: (1) ProbeServiceRoot establishes reachability and a Redfish surface; (2) a SEPARATE per-unit discriminator - observed BMC firmware identity or OEM fingerprint, an authenticated Manager/firmware response, or another explicitly modeled probe - constructs FamilyObserved; (3) only then the family-specific rotation route, the mint and read-back, and accessor-roster admission. The RED the review asks for is w_neither_a_200_nor_a_404_redfish_surface_observes_a_family. It is a FOLD from an intake surface to a standing, so it runs rather than asserting a shape, and it is total in the only honest way: every surface answers unobserved. Its discriminating conjunct is the last one - a future fold that promotes a 200 into FamilyObserved reddens it, which is the promotion the triggers must not license. THE SECOND FINDING NAMED TWO ROSTERED-BUT-CONSUMED HELPERS; THERE WERE THREE. jade_first_dpc_slot is called by the jade_first_dpc_slots builder, jade_channel_slot builds all sixteen of its rows, and jade_fan_policy_convergence - which the review did not name - is called by jade_current_fan_policy_convergence. All three entered in the round-14 census whose consumer count excluded the declaring file. I documented that false-positive mode one round later and never re-checked the rows it had already produced. A roster that declares live code dangling is wrong in the direction nobody audits: downstream readers treat it as a known gap rather than as working code. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Review 68252 (changes requested, otherwise praised): bmc_intake_first_contact_witness_test.dag:67-73 intake_surface_family_standing returns the same constant for all three IntakeRedfishSurface arms, so w_neither_a_200_nor_a_404_redfish_surface_observes_a_family is green by construction and the 'authorable red' the annotation names lives in the test file, not on a production path. quick-ant-24: the discriminating fold must be PRODUCTION — the family standing derived from the surface by the intake module (the same seam the side-chat HOLD asked for: a separate family discriminator, with Redfish 200/404 alone → FamilyUnobserved) — and the witness exercises that fold, not a test-local one. — sent from eager-owl-205 |
…al rung review 68252. The wall I added last round cannot go red. intake_surface_family_standing matched all three IntakeRedfishSurface arms and returned the same constant in every one, discarding its argument - so "a 200 leaves the family unobserved" and "a 404 leaves the family unobserved" were green for ANY input, and the fourth conjunct was a tautology over a predicate declared four lines above it. The promotion the annotation claimed would redden it lived in this test file; no production path could reach it. The operator asked for that RED and I produced something shaped like one, then cited it in two frontier triggers as the property they rest on. That is the failure mode DESIGN section 4b names exactly - "worse than absent because it will be cited as coverage" - and it is the shape ten earlier commits on this branch deleted elsewhere, surviving in the one file whose prose defended it. THE HONEST STATEMENT IS STRONGER THAN THE CHECK WAS. IntakeRedfishSurface carries no BmcFirmwareFamily in any arm: RedfishHttpSurface holds an HttpStatus and a blob, HostUnreachable a cause and stderr, WriteOutUnreadable a blob and a cause. No total fold from it can reach FamilyObserved without inventing a family from nothing. That is rung 4, structurally impossible, and it needs no check - a check there would be validating a state with no constructor. What remains is the conjunct that can actually fail: this unit's standing is unobserved today, and re-binding it to FamilyObserved without the separate per-unit discriminator reddens the claim. The two frontier triggers now say the promotion is unconstructible rather than pointing at a witness. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The previous commit corrected only one of the two triggers review 68252 named as resting on the deleted decoration. The minimum_bmc_firmware_family trigger stated the three-stage separation but not WHY the first stage cannot fire it, so a reader still had to take the separation on the sentence's authority rather than on the type's. Both now say the promotion is unconstructible. Also repairs a clause my earlier string edit mangled in that same trigger - 'Redfish presence only for this unit, at which point' had the unit phrase spliced into the wrong sentence. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…onverge_workflow rosters are the union of both sides; regenerate fleet-converge.yml Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…rted Reaching Mt. Jade's factory BMC needs srv1 to hold an address in the controller's /29 for one run. That is a WRITE to a production host, and the failure that matters is not a bad write but a MISSING UNWRITE: an address left behind outlives the run that placed it and silently changes which segment srv1 answers on. RELEASE IS STRUCTURAL, NOT CHECKED. Every outcome the run can return carries a SegmentAddressDisposition, so a path that forgets to release cannot construct a value to return. A witness asserting release would be checking something it cannot observe - a leaked address lives on an interface, not in the value under test - so it would pass while the address stayed. That is the decoration class I shipped twice on #11620, and the point of this shape is that there is nothing here for it to inhabit. DISPOSITION IS A COPRODUCT BECAUSE OF THE ALREADY-PRESENT CASE. If the address is on the device when the run starts, the run did not place it and MUST NOT remove it: deleting an address another process owns is worse than the leak this module prevents. 'We placed and removed it' and 'it was already there and we left it alone' are different dispositions and neither is a failure. SegmentAddressReleaseRefused is the one arm where the host was NOT left as found, and host_was_left_as_found is the fold that says so - a delete that fails must surface as the run's worst outcome rather than letting findings return as though the host were clean. The deadline standing is three-valued because std.measure compare_instants refuses across clock domains: a Bool would have to call an incomparable pair either expired or live, and both are claims about an order that does not exist. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
1 participant
Summary
redfish.Http.ProbeServiceRoot(unauthenticated). Write-out isextdeps.tools.curlcurl_http_code_write_out_format; HTTP 404 is a captured surface, not a failed OpenBMC login.gunbc.tools.bmc_intake_first_contactclassifies that surface and prints the blob onCliWireResponse(does not writeopenbmc_factory_login). Existingbmc_first_contactstays the OpenBMC srv path.gunbc.machine_intake_bmc_first_contact_standing: Redfish presence does not mint OpenBMC vs MegaRAC; factory login and MegaRAC media attach are refused while family is unobserved.mtjade1access as unobserved (no host, no FRU) andbmc-mtjade1-gunbcas a pending SecretRef. First 1DPC silk is GSG Table 11 hash-numbers. Residence failsafe is typed, not indefinite.Test plan
test.claim.bmc_intake_first_contact_witnesstest.claim.mtjade1_access_witnesstest.claim.mtjade1_first_dpc_population_plan_witnesstest.claim.mtjade1_fan_standing_witnessBMC_HOST=<addr> gunbc run --source-root dag --source-root src/v2 --entry dag/gunbc/tools/bmc_intake_first_contact.dag --function bmc_intake_first_contactand keep the printed blob (do not rotate yet)