Repository navigation
Site-derived timezone/locale and the DGX Spark OOBE observation prefix: five upstream authorities, a host-to-site join, and the discriminators that make them load-bearing - #9997
Merged
Conversation
…iven device, not from the vendor page The onboarding automation lane needs to know what the first-boot wizard actually presents. It had two candidate sources: NVIDIA's documented setup surface, already modeled in extdeps.systems.nvidia_dgx_spark_setup, and the device itself. This lands the second, because the two disagree in a way that would have produced a script that appears to work. WHAT WAS DRIVEN. The unit serving access point spark-0c75, reached by associating a Raspberry Pi's wlan0 to that access point while its eth0 held the fleet LAN, and rendering the portal with Playwright 1.62.1 / Chromium 151 on a fleet member routed through the Pi. Both halves of that split are recorded on the receipt: the portal is a client-rendered React Router SPA (isSpaMode, ssr false), so no plain HTTP fetch can drive it, and the only machine within radio range is a Pi 3B+ whose available memory is far below what Chromium needs. The rendering host is therefore not the radio host, by measurement rather than preference. THE FINDING THAT JUSTIFIED DRIVING A DEVICE. On the EULA screen the single Accept button is rendered disabled and becomes enabled only after the terms pane is scrolled to its end. The vendor page does not mention this. An automation written from the documentation clicks a dead control, and Playwright's auto-waiting turns that into a timeout whose cause appears nowhere in the log. The gate is modeled as a precondition on the screen rather than as a step in a driver, because it is a fact about the screen: carrying it structurally means a screen transition cannot be authored that skips it. WHAT IS DELIBERATELY NOT CLAIMED. The walk halted at the EULA, because advancing past it accepts a license on the operator's behalf -- a legal act, and the one step in this flow a machine should not take on its own initiative. AcceptsLegalAgreement is its own effect arm so that refusal is expressible rather than merely observed. The three modeled screens are therefore a PREFIX, and observed_walk_is_complete returns false; the user account, analytics and wireless screens are unobserved, not proven absent. Reading the prefix as the population is the failure this repository already names (selection_view_read_as_population), and it would be cheap to commit here because the observed rows are real and the missing ones leave no trace. THE JOIN IS DERIVED, NOT ASSERTED. field_is_pending_observation computes the outstanding observation obligation from the vendor's prompted-field predicate and ours, so finishing the walk retires rows by construction. It runs in both directions: hostname assignment is in the field universe but the cited page does not say the wizard prompts for it, so it is not pending -- a predicate that reported every unseen field would manufacture work no evidence asks for. CREDENTIALS ARE NOT HERE. The receipt names the access point, which is a vendor-derived per-unit label, and holds no passphrase. That is why the setup module models the carrier as PrintedQuickStartGuideSticker: the secret arrives on a printed sticker and no field in this model can carry one. EVIDENCE. Witnesses execute against a compiler built from this tree; the advance-gate witness was confirmed discriminating by inverting its expected container and observing FAIL, so its PASS is evidence rather than a permanently-green decoration. The positive control (non-EULA screens advance on arrival) is enrolled beside it, because a model that marked every screen scroll-gated would otherwise pass the first witness alone. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VH82RezgSeBuJQb6xQKtsd
… claims that outran the measurement Review of the first revision found a defect that the PR text had advertised as a feature, plus several claims stronger than their evidence. All are repaired here. THE COVERAGE JOIN WAS A PARALLEL AUTHORITY, AND THE CLAIM THAT IT WAS DERIVED WAS FALSE. observed_screen_covers_field was a hand-written match over every OobeSetupField standing beside the screen list, so appending a screen retired nothing: an author had to remember a second table, and the two could disagree while both stayed type-correct. Each screen now carries presented_subjects and coverage FOLDS the observed prefix, so the word "derived" is true. The old predicate is deleted rather than kept beside the fold, since leaving both would preserve the exact fork the repair removes. Proven discriminating: dropping OobeLanguage from the settings screen's presented_subjects turns w_coverage_follows_the_screens_presented_subjects RED. THREE WITNESSES ADMITTED PLAUSIBLE WRONG MODELS. The settings-effect witness asserted only length(f) == 2, which [OobeAnalytics, OobeWirelessNetwork] and a duplicated pair both satisfy; it now names the fields and their absent siblings. The "only the EULA accepts a legal agreement" witness judged EULA and welcome only, so flipping /welcome/settings left a witness with "only" in its name green; it now folds and counts the whole prefix. The route witness checked the list's LENGTH and three standalone rows, so reordering the list or filling it with duplicates passed; it now compares the list's own ordered route spelling. THE ADDRESS WAS BEING USED AS THE IDENTITY. All three forward controls answer to the same observed data-testid, "nv-button" -- a design-system component address scoped by route and label, not the identity of Get Started versus Continue versus Accept. Treating it as identity gave three different actions one name. OobeControlIdentity is now declared and the observed address is carried beside it, with a witness asserting the address is SHARED so that anyone collapsing the two goes red. THE Pi CLAIM ASSERTED A CAUSE NOBODY MEASURED. The annotation said the Pi's memory was "far below what Chromium needs". What was actually observed is rc=124 with no stderr, on the portal AND on an example.com control, with a single available-memory sample. No RSS, swap-pressure, PSI or OOM observation was taken, so memory is a hypothesis. The evidence establishes a TARGET-INDEPENDENT failure of that attempted realization on that host -- enough to select a different rendering host, and not a capability rule about the hardware. EFFECTS CLAIMED DURABILITY THEY DID NOT ESTABLISH. PersistsDeviceSetting and PresentsOnlyNoCommit both asserted storage; reaching the next route proves a submission was accepted, not that it survives a refresh, and not that nothing was written. They are now SubmitsSelections and PresentsNoConfigurableField. The measurement that settles this arrived meanwhile and cuts against the durable reading: after the agreement was accepted, the portal root STILL resolves to /welcome, so acceptance did not persist as resumable progress. AcceptsLegalAgreement stays a distinct arm, not because its durability is established but because that boundary is what an automation must see to refuse to cross it unauthorized. THE ROOT LANDING WAS PROSE-ONLY, AND WRONG IN KIND. The text said the root "redirects" to /welcome. Measured: HTTP 200 with NO HTTP redirect -- /welcome is reached by a client-side route inside the SPA. An actuator waiting for a 3xx would wait forever on a page that had already arrived. It is now an ObservedInitialNavigation row with a witness. THE SCREEN CONTENT WAS UNDEFENDED. Headings, control labels, addresses and the settings backing fields had no witness at all, so an edit could silently swap any of them while all eleven stayed green. Added folds over the modeled controls rather than a Boolean per leaf. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VH82RezgSeBuJQb6xQKtsd
Contributor
Author
Correction to this PR's own description, and the repairs for review 58440's successor findingsPushed The derivation claim was falseThe body said the documented-versus-observed join was "derived, not asserted". It was not. Each screen now carries Proven discriminating, not merely green: mutating the settings screen to drop The other repairs
Two claims that outran their measurementThe Pi. The annotation said its memory was "far below what Chromium needs". Never measured. What was observed is Durability. One fact that was wrong in kindThe body said the root "redirects" to CI
— sent from sleek-bear-442 |
… than default while the fleet policy is unruled The DGX Spark onboarding wizard prompts for language and timezone on its second screen. The operator's ruling is that both "need to be inherited from a physical location", which is a modeling instruction rather than a value: a unit's civil time is a consequence of where the unit sits, so the authority is the SITE and a workflow derives from it. THERE WAS NO AUTHORITY FOR A ZONE AT ALL. Nothing in the tree modeled IANA zones -- no identifier type, no citation, no release -- so the first consumer needing one could only have written a magic string. extdeps.iana.time_zone_database now cites the database and brands IanaTimeZoneId, because a civil zone is a jurisdiction's rule that changes when governments change it, and an internal ZoneEastern | ZonePacific enum would be a second naming scheme for identifiers every OS on this fleet already ships. The release is OBSERVED, not chosen: 2026c is what /usr/share/zoneinfo/+VERSION reports on srv4. Declaring a release nobody had seen installed would cite a document nobody opened. THE MEASUREMENT THAT DECIDED THE SHAPE. Four reachable hosts at one site were read: srv4 and spark-a3ee report Etc/UTC, while spark-3bd5 and pi1 report America/New_York. The two already-onboarded Sparks disagree WITH EACH OTHER. So a single derived value would have been wrong either way -- reading the zone straight off the site silently declares half the fleet misconfigured, and hardcoding UTC silently declares the other half misconfigured. Neither is a finding this repository has earned, because nobody has ruled which is intended. SO THE POLICY IS ITS OWN AXIS WITH AN HONEST UNDECIDED ARM. A site's civil zone (where the machine IS) and the zone a host is configured to (what we SET it to) are two facts, and this fleet demonstrably decides the second one differently on different hosts. HostZonePolicyUnruled is bottom-as-ignorance kept distinct from both answers, and provisioned_time_zone REFUSES against it rather than returning a default. That refusal is the deliverable: onboarding stops and names the missing ruling instead of guessing for eight more units, which is the absorbing fallback this design forbids. The locale has no such ambiguity -- every host observed runs an en-US userland -- so it derives directly, with no policy axis invented for symmetry. EVIDENCE. The discriminating RED is w_unruled_policy_refuses_rather_than_defaulting, which goes red exactly when someone gives the unruled arm a default -- the repair a future author reaches for when the workflow refuses and they want it to proceed. Both settled arms carry positive controls, without which a derivation that refused on every input would satisfy the RED; and w_the_two_settled_policies_disagree fails if anyone collapses the arms onto one zone, which would make the axis decorative. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VH82RezgSeBuJQb6xQKtsd
…nce obligation rather than listing it OPERATOR RULING 2026-09-02: the site drives every other decision -- "i am literally in new york right now, so that drives all other decisions - i will move in 4 months, and i want that one row to re-derive the proper convergence changes". So fleet_host_zone_policy becomes HostFollowsSiteCivilZone. The UTC arm would have pinned every host to a constant and made the site row decorative, which is the opposite of the requirement. THE WITNESS THAT ASSERTED "UNRULED" WENT RED, WHICH IS WHY IT EXISTED. w_fleet_policy_is_currently_unruled was built to fail the moment anybody ruled, forcing the ruling to be stated in the model rather than left implicit in whichever workflow happened to need a zone first. It is now w_fleet_policy_follows_the_site_civil_zone. WHAT THE RULING TURNS THE FLEET'S DISAGREEMENT INTO. Four hosts were read at this site: srv4 and spark-a3ee report Etc/UTC, spark-3bd5 and pi1 report America/New_York. Before the ruling that was an open question. After it, the UTC pair is a CONVERGENCE OBLIGATION -- and the obligation is COMPUTED, not listed. observed_host_zones carries only what each machine reports; host_zone_convergence compares it against provisioned_time_zone(site, policy); divergent_host_count folds the result. No row anywhere names a desired zone for a host. THE RELOCATION PROPERTY IS ASSERTED, NOT DESCRIBED. w_moving_the_site_inverts_every_verdict runs the SAME observations against a site whose civil zone is UTC and shows the verdicts invert: the hosts that diverge today converge there, and vice versa. That witness fails if anyone pins a host's desired zone, which is precisely the edit that would break the one-row-re-derives property in four months when the site actually moves. TWO REFUSALS KEPT DISTINCT FROM ANSWERS. A divergent host reports BOTH observed and desired, because "wrong" without the pair cannot drive a convergence action. And an unruled policy makes convergence UNDECIDABLE rather than reporting everything converged or everything divergent -- the absorbing arm that would let a missing ruling read as a clean fleet. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VH82RezgSeBuJQb6xQKtsd
…redicates back onto their coproducts Two review cleanups, both taken. THE LOCALE WAS IN THE WRONG UPSTREAM'S MODULE, and the row's own comment said so while the placement said otherwise. PosixLocaleId and locale_en_us lived in extdeps.iana.time_zone_database because the DGX Spark's setup screen prompts for language and timezone together -- but a screen's convenience is not an authority. IANA publishes the time zone database; the locale identifier's shape is POSIX's. One module speaking for two independently versioned upstreams is what DESIGN §3's external-upstream decomposition forbids. They now live in extdeps.posix.locale, cited to the Open Group base definitions. The cost of leaving it was not hypothetical: the next consumer to import PosixLocaleId from the IANA module would have frozen the wrong authority by use, and the rename would have become a migration. THREE is_* PREDICATES RE-EXPOSED A COPRODUCT AS A Bool. observed_walk_is_complete, provisioned_zone_is_settled and host_is_converged each matched a coproduct and returned true on one arm. Callers now match directly and all three are deleted. The check that made this worth doing rather than churn: dissolving a predicate is only an improvement if it does not COPY the match to N call sites, which would trade a style trigger for §2 redundancy. Measured first -- two of the three were consumed only by witnesses, and host_is_converged had exactly one production caller once w_utc_hosts_are_divergent_under_the_ruling was rewritten to ask divergent_host_count directly instead of re-folding the same list. So the matches moved rather than multiplied. AND THE DISSOLUTION SURFACED SOMETHING THE Bool WAS HIDING. divergent_host_count now matches HostZoneConvergence's three arms, which makes visible that HostZoneUndecidable was being counted as divergent. That is still the intended behavior -- an unruled policy should not report a clean fleet -- but "no ruling exists to decide" and "this host has the wrong zone" are different facts, and a caller handed is_converged could not tell them apart. It is now stated at the arm rather than hidden behind a predicate's name. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VH82RezgSeBuJQb6xQKtsd
…ol identities the witness only claimed to cover REQUEST_CHANGES review 58541 found three defects. All three are real, all three are fixed, and chasing the third one down turned up a finding that changes what an actuator is allowed to do. 1. THE WITNESS WAS STATICALLY INCOMPLETE. TestId and ControlLabel were used in control_identity_matches and screen_has_control but appeared in no import list. Added. 2. THE IDENTITY WITNESS DEFENDED NO IDENTITIES. control_identity_matches wildcarded `identity: _` in both button arms and compared only address and label -- and since all three forward controls share the address "nv-button", the wildcard removed the entire discriminating content of the check. Swapping WelcomeGetStartedAction, SettingsContinueAction and EulaAcceptAction between screens left the witness that advertised itself as covering identities completely green, which is exactly the §4b inflation the ladder forbids: the reported rung was higher than the executed evidence. Identity is now compared, and w_screens_do_not_share_control_identities asserts each screen carries ITS OWN identity and no other, so any swap goes red with every address and label unchanged. 3. THE LOCALE AUTHORITY RECORDED THE WRONG REPRESENTATION. extdeps.posix.locale cited POSIX while declaring "en-US", which is a BCP 47 language tag -- so the module named one upstream and the value came from another, and the repository already had the correct form in hand (the os-install rows emit en_US.UTF-8). The POSIX row is now locale_en_us_utf8 = "en_US.UTF-8". AND THE VALUE THAT WAS THERE WAS NOT WRONG, IT WAS HOMELESS. Rather than delete "en-US", the portal was re-read: its hidden locale field really does carry en-US. That is a language tag and it needed its own authority, so extdeps.ietf.language_tag lands cited to RFC 5646. The two are not interchangeable and the difference is load-bearing downstream: a POSIX locale selects a codeset, a language tag does not, and setting LANG to a language tag yields a host with no working locale rather than an error anyone notices. THE FINDING THAT CAME OUT OF THAT MEASUREMENT, and it corrects this module's own earlier implication. The settings screen's hidden fields carry language="25" and timezone="593" -- OPAQUE VENDOR ORDINALS, positions in NVIDIA's list, not identifiers. The wizard does not accept "America/New_York"; there is no field in which that string could be written. An actuator therefore cannot set a zone by writing its identifier: it must drive the visible combobox by displayed label and let the application compute the ordinal. Modeled as SubmittedValueRepresentation, and VendorOpaqueOrdinal deliberately carries NO value -- recording 593 as though it named a zone would be storing a position as a name, which is the positional-citation failure in data rather than in a comment. ALSO WITHDRAWN: the annotation claiming locale is "evidently derived" from the language choice. That was an inference. What is observed is that the field carries en-US while nothing was selected; establishing derivation needs one language changed and the locale watched to move, which has not been done. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VH82RezgSeBuJQb6xQKtsd
Contributor
Author
review 58541 — all three findings verified and fixed in
|
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VH82RezgSeBuJQb6xQKtsd
…unresolved type the review did not name (review 58557) Review 58557 found two defects in the spark OOBE witness module and both were real. Fixing them found a third of the same class the review did not reach. ONE -- OobeControlIdentity was used in two signatures and imported nowhere, so the module was statically unresolved. This is the SAME CLASS as review 58541's first finding, committed while fixing it: that repair introduced OobeControlIdentity and imported its three constructors but not the type itself. Rather than patch the cited line, this censuses every capitalized name in the body against the import list, which found FormFieldName -- needed by the new code below and equally absent. The review's specimen was correct but not exhaustive; fixing only what it named would have shipped the identical defect one line down. TWO -- w_settings_screen_carries_all_three_backing_fields folded the settings controls into the number 3 and wildcarded every backing_field, so renaming "language" to anything left green a witness advertising itself as defending screen content. A COUNT DEFENDS THE ARITY OF A LIST AND SAYS NOTHING ABOUT WHAT ITS ELEMENTS ADDRESS, and an actuator locates these fields BY NAME, so the name was the entire subject the witness claimed. That is DESIGN §4b rung inflation: the reported rung exceeded what the executed evidence established. The check now compares each field name to its submitted representation. The count survives as a SEPARATE witness because naming and counting are two questions -- the named check alone would admit an undeclared fourth field behind the three. VERIFIED BY EXECUTION AND BY MUTATION, not by typecheck. All 22 test fns pass. Renaming language -> lingo in the model turns the content witness RED while the arity witness stays GREEN -- which is the measurement showing the old count could not have detected the modeled error. Flipping locale's representation to VendorOpaqueOrdinal also goes RED, so the representation is defended and not merely the name. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VH82RezgSeBuJQb6xQKtsd
… and a relocation witness that proved nothing (side-chat review) The CI refusal that started this was `unresolved type 'HostIdentity'` in gunbc.host_standup -- a file this branch never touched. Twice I explained that away (the runner fleet is down; my branch is behind main) and both were wrong. The cause was in this diff. THE FORK, AND WHY IT SURFACED SOMEWHERE ELSE. fleet_site_locale re-declared HostIdentity, SiteIdentity and PhysicalSite, all three already owned by product.placement_supply. There is no duplicate-declaration diagnostic: the bare name census flips from GlobalBareUniqueBinding to GlobalBareAmbiguousBinding, the pull is dropped, and the error lands on an IMPORT-FREE module that resolves those names purely by bare scan. A name fork is reported at the innocent consumer, so "the failing file is not in my diff" is worth nothing as evidence. CI COULD ONLY EVER HAVE SHOWN THE FIRST OF THE THREE, because host_standup uses only that one. Censusing every name this diff declares against the tree found the other two, and a fourth (is_converged, against gunbc.bootstrap) introduced by the repair itself. That census now runs as part of this module's verification rather than living in a commit message. PhysicalSite is NOT the locale carrier. Civil time is a join keyed by the canonical SiteIdentity, because placement_supply owns physical containment and a jurisdiction's civil time is not a containment fact; widening that type would make every placement consumer depend on tzdata. The site is REFERENCED (operator_site), not re-spelled -- the first revision minted "us-east-operator-premises" for a place already named "operator-lab", which is one physical site with two names. OBSERVATIONS KEY ON THE SEMANTIC HOST. The rows said "spark-a3ee" and "spark-3bd5" as HostIdentity. Those are reservation_labels; the fleet identities are operator_host_srv5 and operator_host_srv6 and the allocation binding them is already modeled. This is the same class as inferring a principal from a host-local username. The reach path is retained beside the identity, never as it. The Pi reading is kept in its own carrier because no canonical identity for that machine exists and inventing one here would make this module an incidental host-naming authority -- the exact fork it was written to remove. THE COUNTER CONFLATED TWO STATES. divergent_host_count counted HostZoneUndecidable as divergence and defended it in a comment. "Runs the wrong zone" and "no ruling exists" have different remedies. Replaced by a three-way census. THE RELOCATION WITNESS PROVED NOTHING, and this is the third instance of one class in this branch. It asserted the divergent count was 2 under New York and 2 under UTC. Two equal numbers: a derivation ignoring the supplied site, or one swapping WHICH hosts diverge while preserving cardinality, both left it green. It now names each host and asserts its disposition flips. MEASURED, NOT ASSERTED -- 37 witnesses pass and every mutation behaves as predicted BEFORE it was run: A convergence ignores the supplied site -> identity RED, census RED B swap srv5/srv6 zones, cardinality kept -> identity RED, census GREEN C re-key a spark row onto its label -> RED B's green is the point: it is the blind spot the old count had, which is why the count survives only as a separate population witness. The previous verification run was itself invalid and its output looked fine. It restored mutations with `git checkout --`, which on the remote runner also reverts the applied patch, so every check after the first ran against the pre-fix file. Snapshot/restore is now a file copy. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VH82RezgSeBuJQb6xQKtsd
#10025 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VH82RezgSeBuJQb6xQKtsd
Contributor
Author
|
Nothing to fix from review 58677, but one phrase in it describes a stronger claim than this diff makes, and I would rather correct the record than let an approval stand on it. The review reads the new module as "a site-scoped locale/timezone module inheriting from physical site". It does not inherit from
So what is established is the weaker property, which is the one the operator actually asked for: one authored site-policy row changes and every dependent host verdict re-derives, with no second edit. A coordinate-to-zone resolver with an ambiguity arm is a named gap, not something this PR delivers. Worth noting alongside the approval, since it landed after review 58677's head: this diff previously carried four declaration forks against — sent from sleek-bear-442 |
…e (side-chat ruling on 07a80d2) The side chat accepted three of the four earlier repairs and refused the fourth. It was right, and CI had gone fully green over both defects. THE SITE FIELD WAS DECORATIVE. SiteCivilTimeFacts carried `site: SiteIdentity` and no path read it: provisioned_time_zone ignored it, and host_zone_convergence adjudicated whatever facts the caller supplied. The behavioral path was caller-selected facts -> desired zone -> verdict not host -> site assignment -> site-matched facts -> desired zone -> verdict so setting operator_premises_civil_time.site to any other identity left every witness green. A key nothing joins on is not a key, and the field could not be cited as evidence that location drives the derivation -- which is precisely what the module's own prose was citing it for. HostSiteAssignment is authored (not resolved from coordinates; that rung stays named and unbuilt) and select_site_facts returns three arms, not two: a host with NO assignment and a host assigned to a DIFFERENT site need different repairs. HostZoneConvergence gains HostZoneSiteRefused and the census a fourth counter, because folding a refusal into "undecidable" would repeat the conflation this same review already made me fix once. THE RELOCATION PROBE WAS MODELLING THE WRONG EVENT, which only became visible once the join existed. It invented "relocated-probe" as a new SiteIdentity -- under the join that is a MISMATCH, not a move. Relocating the operator's premises changes the premises' civil zone; it does not reassign hosts to another site. The probe now holds operator_site and varies only the zone, which is the event the operator actually described. THE REACH LABEL WAS A PRIVATE SECOND COPY OF AN OWNED RELATION. The previous fix corrected the identity error but left `observed_through: "spark-a3ee"` beside `host: operator_host_srv5` -- a relation gunbc.spark.dgx_procurement already carries structurally in srv5_router_binding -- and the witness then RESTATED the copy rather than checking it. reach_label_of now reads the reservation out of the binding. srv4 reports ReachLabelUnmodeled rather than an invented literal, because it has no modeled reservation and an absent authority is reported, never filled in. MEASURED AGAINST A GREEN BASELINE, which the previous two runs were not: D drift the site identity on the facts row -> RED E drop srv5 from the assignments -> RED F re-author the label instead of deriving -> RED BOTH EARLIER VERIFICATION RUNS WERE INVALID AND LOOKED FINE. The first restored mutations with `git checkout --`, which on the remote runner also reverts the applied patch, so everything after the first mutation measured the pre-fix file. The second reported "RED as required" while all 19 witnesses were already red from a compile error -- a mutation is only readable against a green baseline. The harness now GATES the mutations on that baseline and prints the diagnostic instead of a verdict it cannot interpret. The sweep also ran 39 witnesses one at a time, paying whole-tree resolution for each, and was killed at the 45m remote timeout before it could report. It now runs the discriminating subset locally and leaves the full population to the CI floor, which plans them in one pass. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VH82RezgSeBuJQb6xQKtsd
…ighteen imports an edit silently skipped The exact-head floor ledger proved the earlier witnesses RAN. It could not prove what their predicates distinguish, and four of them distinguished less than they claimed. I -- DIRECTION WAS UNDEFENDED BY A SYMMETRIC PREDICATE. The divergence witness asserted observed != desired. Swapping the payloads keeps them unequal, keeps the arm divergent, keeps every disposition and census identical -- and tells an actuator to set a machine to the zone it already has. The check now names both sides exactly (srv4: observed=Etc/UTC, desired=America/New_York). The symmetric witness is KEPT rather than replaced, and the mutation is enrolled as the permanent control: I direction RED, I old-pair GREEN is the measurement that shows why inequality was insufficient. G/K -- LAST-MATCH-WINS IN TWO TABLES. select_site_facts and the observation selector both folded with a value init, so two conflicting rows for one host resolved silently by list order. A host assigned to two sites is not a host assigned to the second one. Both now carry an explicit Ambiguous arm carrying the host and the count. J -- TWO UNAVAILABILITIES THAT MUST NOT COLLAPSE. A host with a site assignment but no observation is an observation gap; a host with no assignment is a modeling gap. host_zone_disposition_of returns a HostZoneReading and adjudicates only on the unique arm, so a machine nobody read is never reported as one nobody placed. H -- THE PI ROW BY CONTENT. `length == 1` is satisfied by a row naming any host and any zone. Content and count are now separate witnesses because neither subsumes the other: content is blind to a second row appearing, count is blind to values changing. H content RED / H count GREEN is that statement measured. extdeps.ietf.language_tag HAS A CONSUMER NOW. It was an authority carried and never read -- the inert-artifact shape. The settings screen submits BOTH a POSIX locale and locale="en-US", a BCP 47 tag, so the site policy owes the wizard the value the wizard accepts. TWO SOURCE CLAIMS CORRECTED AGAINST THE RECORD. The file no longer calls host_standup the "innocent consumer" -- it carries a pre-existing undeclared bare type reference, and the failure had two conjunctive conditions with asymmetric causes. And it no longer says a unit's zone "is a consequence of where the unit physically sits": the rung is that the operator ASSIGNS a civil-zone policy to a canonical site and consumers derive through a host-to-site association. Geographic resolution remains unimplemented and is named as the gap. MEASURED, every arm including the two that must stay green: I swap divergent payloads -> direction RED, symmetric GREEN H change the Pi zone -> content RED, count GREEN K duplicate an observation -> RED G duplicate a site assignment -> RED J drop an observation, keep it assigned -> RED AND ONE OF MY OWN EDITS SILENTLY DID NOTHING. A scripted replace anchored on an import block a previous edit had already rewritten matched nothing, wrote the file unchanged, and reported success -- leaving EIGHTEEN symbols used and imported nowhere. The compiler names the first; a census names the population. The mutation helper now asserts its target exists before substituting, because a mutation that never applied is indistinguishable from one the code survived. STILL OPEN AND NOT CLAIMED CLOSED: the observation rows are authored data with prose, not receipts carrying host, instrument path, timestamp and execution disposition. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VH82RezgSeBuJQb6xQKtsd
gunbai-bot
Bot
changed the title
…of a four-arm discriminant erased the arms this module added (review 58812)
Review 58812 is right that these predicates are the dissolved shape, and wrong
about the scope of the rule it cites. Both halves are worth recording.
WHAT THE RULE ACTUALLY IS. DESIGN.md contains no "predicate/walker dissolution
rule". Two narrower things exist in the substrate: the 2026-07-12 PREDICATE
DISSOLUTION deleted single-variant is_X nicknames, and std.execution_mode records
why execution_mode_is_wet_dispatch SURVIVED it -- "a two-variant semantic
partition, not a variant test"; and std.occurrence_identity's WALKER rule forbids
a local recursive Empty/Cons match where a canonical fold exists. Neither says
test-local coproduct matching is categorically forbidden, and 404 of 1166 witness
files do it, with named precedent (standing_is_build_unobserved,
test_class_is_hermetic, exit_is_success).
BUT THE FOUR FLEET PREDICATES WERE THE DISSOLVED SHAPE, and the reason is sharper
than the convention. zone_verdict_is_converged two-valued a FOUR-ARM
discriminant, so HostZoneSiteRefused and both unavailable readings collapsed to
`false` -- a witness built on it cannot distinguish "converged" from "we refused
to answer", which is exactly the loss those arms were added to prevent. Two
commits ago I widened the coproduct to stop that conflation and then re-created
it in the witness's projection.
Replaced by WHOLE-VALUE comparison, which needs no predicate and is strictly
stronger because it carries the payloads:
host_zone_disposition_of(srv4, ...) == divergent_reading(observed: zone_etc_utc,
desired: zone_america_new_york)
Precedent for coproduct equality is throughout the corpus (row.type ==
OpenAiToolCallFunction).
CHASING THE SPARK CITATIONS FOUND A COUNT-THROUGH-A-PREDICATE.
w_language_and_timezone_submit_vendor_ordinals_not_identifiers folded
control_submits_opaque_ordinal into `== 2`, so any two ordinal-bearing controls
satisfied it. It now names each field with its representation INCLUDING the
negative arms -- language and timezone are ordinals and are NOT BCP 47 tags,
locale is. screen_accepts_legal_agreement was a single-variant test and is now
a direct `s.effect == AcceptsLegalAgreement`.
MEASURED against a green baseline:
I swap the divergent payloads -> flip witness RED
L make a site refusal return HostZoneConverged -> RED
L is the one that matters: under the deleted predicate that mutation was
INVISIBLE, because a refusal and a non-converged verdict both projected to false.
The dissolution bought discrimination rather than merely satisfying a reviewer.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VH82RezgSeBuJQb6xQKtsd
Contributor
Author
|
Fixed in The rule, verified against the authority
Neither forbids test-local coproduct matching categorically. Measured: 404 of 1166 witness files match coproducts directly, with named precedent — So I'm not routing these through a fold surface, and no bounded-disposition justification is owed for the pattern as such. But the four fleet predicates genuinely were the dissolved shapeAnd the reason is sharper than convention. They're gone. Comparison is now whole-value, which needs no predicate and carries the payloads: Coproduct equality has precedent throughout the corpus ( The spark citations found a separate defect
Measured, against a green baseline
Worth noting for calibration: CI was fully green on — sent from sleek-bear-442 |
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
1 participant
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.
What this is
The operator has 8 DGX Sparks (possibly 8 more) and each one currently needs a human at a browser. This lands the modeling that an unattended OOBE actuator will consume: what the wizard actually presents, and where a unit's language and timezone come from.
It is observation and policy, not actuation. No browser is driven by this diff.
Composition — five concerns, not one
The title of an earlier revision called this an "OOBE observation tranche", which described one of the five modules.
extdeps.iana.time_zone_databaseAmerica/New_York), never an offsetextdeps.ietf.language_tagen-US) — the tag the portal's hiddenlocalefield submitsextdeps.posix.localeen_US.UTF-8) — a different value of a different specgunbc.fleet.fleet_site_localegunbc.spark.oobe_screen_observation/welcome→/welcome/settings→/welcome/eulaprefixThe finding that changed the design
The settings screen submits opaque vendor ordinals:
There is no field in which
America/New_Yorkcould be written. An actuator must drive the combobox by displayed label and let the app compute the ordinal.VendorOpaqueOrdinaldeliberately carries no payload, so nothing downstream can mistake a position for a zone name.What the location claim actually is
The operator's ruling was that language and timezone "need to be inherited from a physical location". The rung reached here is weaker than that sentence sounds, and the source says so:
What it does buy is the property that was asked for: one authored row moves and every dependent verdict re-derives, with no second edit. That is defended by a mutation, not by prose.
Evidence
Every discriminator below was run by mutating the model and observing the witness, including the two arms that must stay green — a check that goes red for everything discriminates nothing.
observed/desiredinHostZoneDivergentObservationMissingAmbiguousIis the sharpest: the previous witness assertedobserved != desired, which a swap satisfies — leaving an actuator told to converge in the wrong direction while every census and disposition stayed identical.Review rounds this went through
Several §3 violations were dissolved rather than layered around: duplicated
HostIdentity/SiteIdentity/PhysicalSiteagainstproduct.placement_supply, a second name for the operator's site, a parallel coverage table, host identities minted from reservation labels, and asitefield that no derivation path read.Named gaps — not claimed closed
/welcome/accountis observed but unmodelled; when it lands it must be route-scoped and name-bound (all three inputs reusenv-text-input-element), and can support onlyClientDidNotRejectExactUsername("root")rather than any reserved-name claim.Receipt history
The original three-screen receipt remains halted at the EULA awaiting operator authority, and is not rewritten. The EULA was subsequently authorized by the operator directly and
/welcome/accountwas reached; that continuation is a separate observation and is not modelled in this diff.🤖 Generated with Claude Code
https://claude.ai/code/session_01VH82RezgSeBuJQb6xQKtsd