Repository navigation
Mt. Jade first contact: the model, ahead of the run - #11758
Conversation
… discriminator Modeling for the read-only first-contact converge against Mt. Jade's factory static BMC (10.0.7.2/29, same L2 as srv1 - established by srv1 tcpdump RECEIVING the BMC's own ARP broadcasts, which do not cross L3). Not the run yet; this is the substrate it needs. extdeps.iproute2.ip_address - ShowDevice / AddSecondary / DeleteSecondary. Show exists so the caller can decide rather than adding blind: `ip addr add` is not idempotent and a second add exits nonzero, so without a read the only way to make the converge idempotent is to ignore an exit status, which is the fail-open section 5 refuses. The module says plainly that AddSecondary is a WRITE TO A PRODUCTION HOST. extdeps.iputils.arping - ProbeAddress, so reachability REFUSES rather than timing out. A curl connect timeout cannot separate "not on this segment" from "there but not serving"; an ARP reply proves the target is live at layer 2 AND, because ARP does not cross a router, that the segment is shared. The note is explicit that silence establishes none of wrong-interface, wrong-segment, powered-down or not-answering, so the caller carries a typed cause instead of widening. Both are new files under dag/extdeps and therefore CANNOT join the frozen legacy manifest - extdeps_scope_frontier refuses a manifest row naming a file added after its freeze sha. Each declares its own extdeps_model_scope and anchor and is added to scope_carrier_paths in this change. The neighbouring ss.dag declares neither and was not a template. extdeps.bmc.http gains GetManagers and GetManager, authenticated and carrying --fail-with-body. That flag direction is the opposite of ProbeServiceRoot's and the note says why: on the Manager resource a 401 or 404 is a FAILURE TO OBSERVE, not an observation. gunbc.machine_intake_bmc_firmware_family_discriminator is the only function that may construct FamilyObserved. It folds a TYPED ManagerIdentityObservation rather than sniffing a blob, so a wire-shape change breaks decoding instead of silently changing a family verdict. FamilyAmbiguous is its own arm: a Manager advertising both Oem keys is unresolvable and choosing one would select a rotation route against the wrong stack. Both Oem-key claims are TranscribedUncited with the read that would close them - they are how these stacks are known to present, not something I have cited. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…SG's DHCP claim The Mt. Jade GSG page 14 step 3 instructs the operator to cable the BMC management port to a switch that provides DHCP, and states no static default anywhere. This unit answered on a factory static before any lease existed. That divergence is the fact, so the standing is a COMPARISON of document expectation against observation rather than an observation filed under the document's expectation - recording the address as though it were the documented behaviour would erase the one thing the observation establishes. WHAT IT ESTABLISHES CONCRETELY: 'brand new' does not prove factory-default BMC NVRAM. The unit arrived sealed and its network configuration is not what the shipping document describes, so the safe reading is that this controller was configured before it reached us. The no-reset standing rests on this row rather than on a caution. The comparison is a coproduct, not a Bool, because a reader needs to know WHICH way the unit diverged and because an unobserved network is not agreement. Both divergence directions are modeled, so the fold is not a one-way assertion about this unit. Addresses and the MAC use the existing typed carriers (extdeps.network.ipv4 Ipv4Address/PrefixLength, extdeps.network.mac Eui48Address) rather than strings. srv1 takes 10.0.7.3, not the controller's configured gateway .1: a free host address in the same /29 reaches .2 on-link without impersonating the gateway. 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>
…reds Model-only, no hardware: every claim here runs against fixtures and production rows and none of them touches a BMC or a host. - the family discriminator in all four directions (OpenBMC key, AMI key, both, neither), so dropping either discriminator, collapsing the both-keys case into a family, or letting an unrecognised Manager answer anything but indeterminate each reddens one - only FamilyDiscriminated promotes to FamilyObserved; ambiguity and indeterminacy stay unobserved, because promoting either selects a rotation route against a stack nobody identified - host_was_left_as_found is true on exactly three dispositions and false on SegmentAddressReleaseRefused: the red is a fold that reports a failed "ip addr del" as clean while the address is still on a production interface - disposition_for_unplaced pairs already-present and refused acquisitions WITHOUT a delete, and returns Absent for a placed one so it cannot shortcut the release it owes - the lease deadline is three-valued across clock domains; the red is a comparison that calls an incomparable pair either live or expired - the observed static diverges from the GSG's DHCP expectation, and the same fold is exercised the other way (a document stating static, and an observed lease) so the claim is about the comparison rather than about this unit Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…n does not Operator wind-down: no hardware touches from this window, so the converge that consumes all of this is deliberately NOT in the change. Shipping an effectful entry point nobody is positioned to execute would be worse than shipping the model it needs. That makes every fold here dangling in the §3c sense, so they are a declared frontier with ONE shared consumer rather than eleven guesses. The trigger is a CAPABILITY and not an artifact: the converge existing is not enough, it must READ these on the path that actually probes the controller. A run that imports the discriminator and then decides a family some other way would satisfy an artifact-shaped trigger while the capability stayed dead - which is the §4b(3) defect this branch's parent PR had to repair on the transport-debt row. Each row says what does NOT satisfy it, and those clauses are the load-bearing half: citing the two Oem-key claims closes their read obligation but not their frontier row; a run that releases correctly without consulting host_was_left_as_found leaves a refused release out of the exit status; a run that spells either address as a literal re-forks the rows that exist to prevent exactly that. THE THREE EXTDEPS OPERATIONS ARE NOT ON THIS ROSTER and the module says so. Service operations are not data or fn declarations and the census that produced these rows reads those two forms, so their absence is a gap in the census rather than a claim that they are consumed. Stated in the module so a later reader does not take the roster's silence for coverage. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot
Bot
changed the title
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: 8df10980b4
ℹ️ 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".
| // must surface that as its worst outcome rather than returning findings as though the host were | ||
| // clean. | ||
| type SegmentAddressDisposition | ||
| = SegmentAddressReleased { lease: LeasedSegmentAddress, released_at: ObservationInstant } |
There was a problem hiding this comment.
When the future converge forgets to call DeleteSecondary, it can still construct SegmentAddressReleased from the lease and any instant; the new witness does exactly that without a deletion result, and host_was_left_as_found then reports true. Merely requiring a disposition therefore does not make release structural as claimed, so a missed cleanup path can return success while leaving the production interface changed; mint this arm only from a successful delete receipt rather than exposing an unrestricted record constructor.
Useful? React with 👍 / 👎.
| output { body: String from "stdout", success: Bool from "exit_success" } | ||
| readonly | ||
| transport shell { | ||
| argv: ["curl", "--fail-with-body", "-sS", "-k", "--netrc-file", "{netrc_file}", "https://{bmc_host}/redfish/v1/Managers"] |
There was a problem hiding this comment.
When a reachable BMC accepts a connection but stalls during TLS or the response, both new Manager requests can wait indefinitely because neither argv supplies a timeout; curl --help all describes --max-time as the “Maximum time allowed for transfer,” and the native shell transport waits with .output()? at src/v1/stage0/src/v1_compiler_emit_rust.rs:36480 rather than imposing its own deadline. In the declared converge this occurs after the secondary address is placed, so execution may never reach the release/disposition path; add bounded connect and total transfer times to both operations.
Useful? React with 👍 / 👎.
|
Review 69207 findings are correct and go on this draft's resumption plan (the lane closed under the operator's 2026-09-20 wind-down; the PR stays draft with its seven witnesses UNVERIFIED, so no change is pushed to a model nobody can execute in this window): (1) mtjade1_factory_network.dag mints the BMC address and the /29 prefix twice — derive mtjade1_bmc_address and the segment prefix from mtjade1_bmc_observed_network via an accessor so the frontier's probe target cannot drift from the observation; (2) srv1_segment_address_is_not_the_bmc is a negation of ipv4_address_eq wearing a name its signature does not carry — replace with a witness over srv1_factory_segment_address and mtjade1_bmc_address, decidable today. Both are step 0 of the PR body's steps 1-4 and are recorded in the roadmap wind-down record (#11867, item 6). — sent from eager-owl-205 |
…ares it (#11758 landed it from std.types under the fail-open floor) Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
1 participant
Modeling for a read-only first-contact converge against Mt. Jade unit 1's factory BMC. The run itself is deliberately not here — see What remains.
Why the model lands without the run
The unit's BMC answered on a factory static (
10.0.7.2/29, gw.1, MAC70:e2:84:95:33:6b) and srv1 shares its segment — established by a 90s tcpdump onenP3p3s0f1that received the BMC's own ARP broadcasts, which do not cross L3. An operator window was planned for a wet run; it closed. Landing the effectful entry point with nobody positioned to execute it would be worse than landing the model it consumes, so the converge is a declared frontier with a capability-shaped trigger.What's here
extdeps.iproute2.ip_addressShowDevice/AddSecondary/DeleteSecondary.Showexists so the converge decides rather than adding blind —ip addr addisn't idempotent, and the only other way to make it so is ignoring an exit status.extdeps.iputils.arpingProbeAddress, so reachability refuses instead of timing out. An ARP reply proves layer-2 liveness and shared segment; silence establishes none of wrong-interface / wrong-segment / powered-down / not-answering.extdeps.bmc.httpGetManagers+GetManager, authenticated, carrying--fail-with-body— the opposite direction fromProbeServiceRoot, because on the Manager resource a 401 is a failure to observe...._bmc_firmware_family_discriminatorFamilyObserved. Folds a typed observation, not a blob.FamilyAmbiguousis its own arm...._factory_segment_lease..._mtjade1_factory_networkFactoryBmcNetworkStanding— the observed static recorded against the GSG's DHCP claim.Both new extdeps files declare their own scope + anchor and join
scope_carrier_paths: a file added after the freeze sha cannot join the legacy manifest.Two things worth reviewing closely
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.The already-present case is why disposition is a coproduct. If the address is on the device when the run starts, the run did not place it and must not remove it. "We placed and removed it" and "it was already there and we left it alone" are different dispositions; neither is a failure.
SegmentAddressReleaseRefusedis the only arm where the host was not left as found.The GSG divergence
Page 14 step 3 instructs cabling the BMC port to a DHCP-serving switch and states no static default. This unit shipped on a static. The standing records that as a divergence rather than filing the address under the document's expectation — which is what makes "brand new does not prove factory-default BMC NVRAM" a fact rather than a caution, and is the reason the no-reset position holds.
What remains (not in this PR)
ManagerIdentityObservation(needs a JSON path).Rows 1–3 are the named consumer on
jade_first_contact_frontier_rows, with the trigger stated as a capability: the converge must read these on the path that probes the controller. A run that imports the discriminator and decides a family another way satisfies an artifact-shaped trigger while the capability stays dead.Evidence
Six witnesses, all pure folds, no hardware. Discriminator in all four directions; only
FamilyDiscriminatedpromotes toFamilyObserved;host_was_left_as_foundfalse on exactly one arm; unplaced acquisitions pair without a delete; the deadline is three-valued across clock domains; the static/DHCP comparison exercised both ways so the claim is about the fold rather than about this unit.🤖 Generated with Claude Code
The six model witnesses plus the frontier witness (7 total) have not been executed successfully. A remote
claim_batchrun over them returned 0 of 7 PASS. That is not seven failures: the run built the index, completeddeclarer-discovery(18 declarers), and then ended with no PASS lines, no FAIL lines and no diagnostics. The process died mid-run — the floor log showsdegraded_budget_source: declared-unverifiedand ~761MB RSS growth during index warm, so memory is the first thing to rule out, not a conclusion.So the claims in this PR are asserted by reading, not by execution. Given that reading is exactly what missed four resolution errors on this branch's parent PR (
all/anyimported fromstd.typeswhen they are builtins, a wrong field name on a coproduct arm, a non-exhaustive match), the prior on this file having at least one resolution defect is high. Treat every "the red is X" claim in the commits as a design intention that has not yet been demonstrated.First thing for whoever picks this up: re-run the witnesses and fix what falls out, before reviewing the modeling. Flipping to ready before that would spend review rounds on a file that may not resolve.
Assert the PASS count against the
test fncount —claim_batchexits 0 over an empty population, so the exit code establishes nothing.