Repository navigation
Lane S: read the deployed fan programs exactly, conserve every occurrence, and gate representability - #9491
Merged
Conversation
…n, not a count
Lane S, step one. A semantic decoder over a captured configuration reads the
members it understands and returns a typed record, and nothing in that shape
stops it silently ignoring a member it does not model. The result still looks
complete: every field the reader asked for is populated and the unmodelled one
is simply gone. The source JSON still exists, so no information was destroyed
-- but the OBSERVATION claims to describe a program it only partly read, and a
consumer cannot tell whether the decoder saw no residue or dropped it.
The remedy is a checked partition: every member occurrence is accounted for
exactly once as consumed, unmodelled, or defective. This module owns that and
knows nothing about fans, PIDs or OpenBMC.
WHY IDENTITY AND NOT COUNT, WHICH IS THE ENTIRE CONTENT. A conservation check
written as source.length() == consumed + unmodeled + defective passes this:
drop the unknown member at ordinal 3, classify the member at ordinal 1 twice.
Same total, one member lost, one double-counted, green. That is the oracle
DESIGN forbids -- a measurement compared against another measurement of the
same thing. The check is therefore an identity join in BOTH directions:
source-to-dispositions catches a lost or twice-claimed member, and
dispositions-to-source catches an occurrence authored against an object it did
not come from, which is how a partition could otherwise be padded to cover a
member it never read.
AN OCCURRENCE IS A POSITION, NOT A KEY, and the format forces it rather than
taste choosing it. { "type": "fan", "type": "stepwise" } is legal JSON. A
residue reported as the string "type" cannot say which occurrence was consumed
and which retained, so a decoder reading one and dropping the other would be
indistinguishable from one reading both. Ordinals are assigned by the
enumeration and never by the caller, so a decoder cannot invent an occurrence
the source did not contain.
DEFECTIVE IS NOT UNMODELLED, because the owners and repairs are opposite. An
unmodelled member is a gap in the DECODER -- the document is fine and the model
is behind it. A defective member is a gap in the DOCUMENT against a field the
decoder knows: a duplicated identity field, a wrong JSON kind, a number outside
its domain. Collapsing them lets a malformed known field be reported as a
vendor extension, which reads as "not modelled yet" when it means "this program
is wrong".
The witness subject carries both real shapes -- a vendor extension and a
duplicated identity field -- parsed from text rather than hand-built, so the
duplicate survives as two occurrences or the witness fails.
Discriminating reds, each restored: conservation reimplemented as count
equality (goes red against the substitution, which is the point); the reverse
join dropped; ordinals collapsed so duplicate keys share one identity.
gunbai-bot
Bot
changed the title
added 12 commits
August 27, 2026 18:15
…ts spell one coefficient two ways srv3's captured fan program writes minThermalOutput as `30.0` and srv4 writes it as `30`. Asking whether the two hosts run the same program is asking whether two numerals denote the same number, and no comparison of lexemes answers that. This tree deliberately had no JSON-number-to-value decode: emit keeps every number as a branded lexeme so that parsing never silently reinterprets a numeral. extdeps.github.workflow_run_event's run_id note records both that decision and where the decode belongs when a consumer finally needs it -- "the decode lands in the JSON authority with its own witness, not here". So it lands there, not in the fan reader, where it would have been a second reading of RFC 8259 section 6 beside the grammar's. The carrier is exact -- units over a power of ten, no binary floating point -- so a comparison is of the authored number rather than of an approximation of it. A float carrier would make 0.1 and its nearest double indistinguishable at exactly the point where the question is whether two documents agree. The exponent form is named as outside the fragment and refuses. Expanding it means deciding what 1e400 becomes, and every answer to that is an overflow or a fabrication. No captured document uses it, so the refusal costs nothing today and leaves the decision with a caller that knows its own domain. A number-shaped string is a defective document, not an unreadable number: a coefficient spelled "30" with quotes is the wrong kind of value in that position, and reporting it as a numeral this fragment cannot read sends the repair to the wrong owner. Five mutations, each red and restored: equality without canonicalisation; reduction running past the decimal point into the whole part; the sign left attached to the digit string; the exponent form truncated at its marker instead of refused; a quoted number read as a number. The first of those did not discriminate at first, and the witness records why rather than the fix being silent: the reading path canonicalises at construction, so two numerals compared through it are already reduced and deleting the reduction inside the equality left every conjunct green. Two hand-built values at one number in two representations are the only way to reach it.
…actuators, which is what the hardware does A zone runs ONE stepwise controller turning a temperature into a demand, and that single demand feeds SEVERAL actuator controllers, each with its own transfer function to its own fans. The deployed program is exactly that: TEMP_SOC produces a demand, FAN1 subtracts 8 and floors at 3, CHASSIS adds 35 and floors at 40. An earlier framing of this as "two curves" was wrong and would have modelled two demands where there is one -- making the two actuators look independently adjustable when moving the shared demand moves both. The model is independent of the producer: nothing in it mentions JSON, a file, a host or a transport. The moment the model knows how it was obtained, the intent side must either borrow that vocabulary or fork the model, and a forked model is two answers to "what program is running". Three things are unrepresentable rather than checked. A curve point carries both its reading and its output, so the document's two parallel keyed objects cannot produce a half-paired point here. The demand controllers and the actuators are separate fields rather than one array discriminated by a type string, so an actuator cannot appear where a demand controller is expected. And the two `setpoint` keys -- degrees for the thermal controller, demand units for the actuator -- are separated by their types, so a reader cannot mistake one for the other. ignoreDbusMinMax gets three states, not two. It is absent on a captured sensor entry, and absent is not false: false asserts the D-Bus bounds are to be used, absent says the document did not decide. They have different repairs -- one is a program to change, the other a program to complete. Magnitudes are exact decimal over std.measure's own quantities. Percent pins its magnitude to Nat and Celsius to Int, and the deployed document carries -8.0, -3.0, -0.5 and 0.005. Reusing the quantity authority and varying only the magnitude parameter is what that type parameter is for; minting a fresh temperature type here would have been the nicknaming violation. RELATION TO THE PARTIAL AUTHORITY THAT ALREADY EXISTED, declared rather than left for review to find. extdeps.bmc.openbmc_fan_control OpenBmcStepwiseController models a subset of the same concept: Nat and Int magnitudes that cannot spell the deployed coefficients, a curve as two parallel lists so an unpaired curve is representable, no PID coefficients at all so the feed-forward offset that IS the difference between the two deployed actuators is absent, and zone facts mixed into a controller record. It is not deleted here because it has an actuation consumer and actuation is a separately-decided lane -- the gap-intolerant boundary carve-out. Until that cutover it is frozen, with the dissolution named on the new model.
…an be ambiguous about it
The curve is stored as two objects, `reading` and `output`, each keyed by a decimal
index string, and the pairing between them is by key identity and nothing else.
Position would be wrong: object member order is authored, and the two objects can
disagree on it. The discriminating fixture authors the output object in reverse
member order -- under positional pairing 66 degrees would take 100 percent instead of
44, which is the difference between a quiet fan and a loud one at the same
temperature.
Four ambiguities refuse rather than resolve, each named with its own arm because each
has a different repair. Two keys that normalise to one index ("1" and "01") refuse
naming BOTH keys, because picking either is picking a curve the document does not
state and reporting only the second leaves a reader hunting for what it collided
with. A key that is not an index at all refuses rather than being skipped -- a skipped
key is a curve point silently missing from the decoded program, invisible precisely
because the decoder judged it uninteresting. A reading with no output and an output
with no reading are separate refusals, and the fixtures give each side a key the other
lacks so the key counts agree and only a real join catches it. A duplicated side, a
non-object side, a quoted value and an exponent-form value each refuse by name.
Monotonicity is NOT checked here and the module says why: a descending curve is a
defective program, but refusing it at the decode makes a badly-configured host
unobservable. The observer's job is to say what is running, including when what is
running is wrong.
Four mutations, each red and restored: positional pairing; the collision accepted with
first-key-wins; a non-index key skipped; the join run in one direction only.
A SUBSTRATE DEFECT WAS FOUND AND IS REPORTED RATHER THAN ONLY DODGED. A field named
`value` on a record read through `list.first()` does not resolve to that field: field
access through an optional auto-unwraps for every other name (`boxes.first().tag`
reads the field) but `.value` reads the OPTIONAL's payload and returns the record.
Both resolve on one expression, decided by the field's name, with no diagnostic --
and `boxes.first().value == 99` places a record against an Int and typechecks clean,
which is a floor-level miss. Here it made every decoded curve output silently carry
the entry record instead of its magnitude. The field is renamed to `magnitude`; that
rename is a workaround, is marked as one at the site, and carries the minimal
reproduction so the defect can be re-derived without this file.
…try with absent distinguished from false Every object decode from here returns its member dispositions alongside its value, which is what wires the conservation wall into the decode rather than leaving it a check somebody might run: a decoder that reads five of a sensor's six members produces five dispositions, the join against the source occurrences fails, and the program does not become representable. The residue is DERIVED from the keys actually consumed rather than listed by hand -- a hand-written residue list is a second place to forget a field. A consumed member is recorded by its occurrence, not its key, so a document carrying a field twice produces two occurrences and a single read accounts for exactly one of them. An optional field is a three-way answer: present-and-readable, absent, and present-but-wrong. The middle is the document declining to state a policy and the last is the document stating it wrongly, so a malformed timeout cannot report as an unstated one. That is what lets ignoreDbusMinMax carry its three states honestly. An unknown sensor type refuses rather than reading as some other kind of sensor: a third type means this decoder is behind its upstream, which is worth stopping on. The conservation module moved from gunbc to extdeps.languages.json.member_conservation. Its subject is a JSON object and nothing in it is specific to any decoder, so it belongs beside the grammar rather than in the consumer that needed it first. It claims no upstream fact -- it is a discipline for reading documents, not a model of RFC 8259 -- so it carries no citation.
…oined on the ordinal alone Found in review of #9491, and it defeated the exact wall the rest of this lane cites. source occurrence zones[0].pids[0] / ordinal 0 disposition occurrence zones[0].pids[1] / ordinal 0 were accepted as the same occurrence. The axis that distinguishes them was never consulted, so a PID decoder could classify a member of one controller as the corresponding member of its sibling and conserve cleanly -- the silent substitution this module exists to stop, committed one level down inside the module that stops it. The first witness did not catch it because its "foreign" disposition was a foreign ORDINAL from the same object. Every object has an ordinal 0 and an ordinal 1, so the untested half was the common case, not the exotic one. The join now compares the whole identity, and the partition's own object_path -- a third independently authored copy of the same fact -- is checked against its source population, because otherwise a partition can name one object while every occurrence in it describes another and the join holds perfectly about something else. ONLY THE SOURCE IS GUARDED THAT WAY, AND THE REASON IS A MEASUREMENT RATHER THAN A PREFERENCE. Guarding the dispositions the same way was written first and removed: with both populations pre-filtered to one path, the path comparison inside the join can never decide anything. Measured under that version, reducing the join to ordinal-only left the new sibling-object witness GREEN -- the guard had made the join's own path half unreachable, and an unreachable comparison is the decoration DESIGN calls worse than absent because it gets cited as coverage. With the disposition guard gone the join is what catches a sibling occurrence, and the ordinal-only mutation goes red. The sibling fixture accounts for every one of this object's members exactly once and adds one disposition naming the SIBLING's occurrence at an ordinal this object also has. Full identity calls that foreign and names both paths; ordinal-only cannot distinguish it from a second claim on this object's own member, so it reports the wrong defect about the wrong object -- which is exactly how a cross-object substitution would have been described. Two mutations, both red and restored: the ordinal-only join, and the partition's source path left unchecked.
… integer Found in review of #9491 and confirmed by execution before the change: this document decoded to a curve point. "reading": { "1": 55 } "output": { "01": 30 } One member on each side, so no within-side duplicate existed; both normalised to the integer 1; the two paired across key sets that do not agree. The previous refusal only caught a collision WITHIN one side, which is the rarer half. phosphor-pid-control asks each of these objects for the exact key it computes from an integer position. It does not normalise, so "01" is a key it never looks up, and a decoder reading it as index 1 reports a curve point the running system does not load. A non-canonical key is therefore refused with the canonical spelling named, and a duplicated exact key is refused rather than resolved -- RFC 8259 permits the duplicate and does not say which wins, so last-wins would let a document carrying two values for one curve position read as whichever the writer put second. THE JOIN STAYS ON THE INDEX AND THAT IS A MEASUREMENT, NOT AN OVERSIGHT. Rewritten as an exact-key join it was indistinguishable: once every admitted key is canonical the keys and indices are in bijection, so reducing the join to the index left every witness green. Two mechanisms deciding one correspondence is redundancy, and the canonical wall is the one that does work the other cannot -- it refuses "01" on BOTH sides, where the key sets agree and an exact-key join would pair them into a point the daemon never loads. The decoded points are now ordered by index rather than by authored member order. The daemon loads by integer position, so a document whose members were reordered describes the same curve, and a semantic program that changed on reordering would make every downstream digest sensitive to a difference the running system does not have. The authored order stays in the captured artifact, which is where it belongs. ONE UPSTREAM BOUND IS NAMED RATHER THAN GUESSED. Review reported that the loader takes a bounded number of stepwise positions, so a key past that bound is a document the daemon does not fully load. Nobody who wrote this file has read that loader, so no numeric bound is asserted -- a limit copied from a summary would put a fabricated constant in the one module that exists to stay exact. The trigger is recorded at the site. What stays open is over-acceptance of a high index, which says MORE than the daemon runs rather than something different; the substitution class is closed. Three mutations red and restored: the non-canonical key admitted; the points left unordered; and the join reduced to a constant. A fourth -- the join by normalised index -- stayed GREEN, which is what established the redundancy above rather than a gap.
…nt is not unreadable digits Two foundation corrections found in review of #9491. The canonicaliser opened `if fraction_digits <= 0` and returned the same units at scale zero, so a computed -4 was not merely representable -- it was silently reinterpreted as an integer, and both the equality and the wire consumed that reinterpretation. A negative scale means something: a value scaled up by ten to the four. Reading it as zero scale is the fabricated plausible output this file exists to prevent, produced by the function meant to make comparison exact. The domain is now enforced where a value is BUILT rather than assumed where it is read: admit_exact_decimal refuses a negative scale, every producer routes through it, and the canonicaliser's negative arm diverges through the std seam. That is the honest projection for a state the mint cannot produce -- it returns no plausible number, and it does not pretend the arm is unreachable by omitting it. Separately, the modeled fragment is narrower than 'exponent-free RFC numbers'. The digits are read into the substrate's Int, so an exponent-free numeral whose exact coefficient exceeds that range was reported as unreadable digits. A grammar-validated lexeme does not have unreadable digits merely because the carrier that would hold it is bounded; one is a document to fix and the other is this fragment reaching its edge. They are now separate refusals and the witness pins each by name.
Review of #9491 found several field semantics that claimed more than the schema fixes or than anyone here has read. Each is corrected by WEAKENING the assertion rather than by substituting the reviewer's alternative, because replacing one unverified claim with another is the same move in the other direction. The zone's output units are not universally percent. Upstream describes the zone's thermal output as commonly fan RPM and does not require the setpoint to be RPM either. This deployment's demand runs on a PWM-like scale, but a model hard-coding percent asserts a unit the schema does not fix. Everything in those units -- curve output, zone minimum and failsafe, actuator output limits and feed-forward offset -- now shares one named ZoneDemandValue, so a value from one cannot be silently compared against a temperature or a gain. P, I and D are not dimensionless ratios: their dimensions depend on the controller's input and output, and for a fan controller producing PWM from a tachometer a proportional gain is percent per RPM. Calling them ratios asserted an algebra that is wrong for the very controllers here. They are exact scalars; exact observation and comparison need no dimension, and a later behaviour model can parameterise them. The actuator's configured setpoint is preserved without operative meaning. It is in the bytes so dropping it would not conserve, but review reports the upstream builder does not pass it to the fan controller it constructs. It was typed as a demand value and annotated as the zone's demand units, which gave a live role to a field that may have none. Two claims are now ABSENT rather than corrected, and that is the honest state. The feed-forward annotation stated `output = demand * gain + offset`; review reports the runtime computes `(setpoint + offset) * gain`. At the deployed gain of 1.0 those agree exactly, so nothing in this lane can distinguish them -- which is how the wrong one survived being written down. Likewise slew was named per-sample and typed as a percentage; review reports the runtime multiplies by elapsed sample TIME, and the deployed samplePeriod of 1.0 makes the two numerically identical. Nobody who wrote this file has read that runtime, so the model now states the fields and not the arithmetic, with the next-rung trigger recorded at each site. Nothing in Lane S depends on either: exact observation needs the coefficients, not their composition. The zone's two intervals carry their scale in the type instead of in a field-name suffix, which had put a magnitude's scale in a string. And the one-demand-two-actuator shape is restated as this DEPLOYMENT's shape rather than the schema's law. Upstream zones may combine several thermal-controller outputs; the model always carried lists, but the annotation read as a constraint. A REGRESSION IN THE PRECEDING COMMIT IS ALSO FIXED HERE: renaming a JSON number refusal left a stale import in the decoder, and both decode witnesses went red. It was committed because only two of the four witnesses were run before committing. All four are run together now.
… wall Named in review of #9491 as mandatory before the representability gate, and the argument is decisive: a decoder can conserve every member of every object it CHOSE to decode while skipping one element of a PID array and duplicating another. All the object partitions balance, because the skipped object never produced one. The array is the only place that is visible. An element's identity is its position, exactly as a member's is, and for the same reason: two PID entries can be byte-identical and are still two entries. An unsupported entry must still produce exactly one disposition, which is what makes "source element count equals observation count" an identity result rather than a scalar comparison. The verdict vocabulary is shared with the object law on purpose. It is the same law -- every source position accounted for exactly once, nothing accounted for that the source did not contain, and the partition's own label agreeing with its population -- so a second verdict type would be two names for one set of outcomes. Four populations are now conserved across a whole program: the sensors array, the zones array, each zone's pids array, and each controller's inputs array. That last one is not filler: the CHASSIS controller drives three fans, and a decoder reading two of them would conserve every object member perfectly. Dropping a driven fan is precisely the wiring error this lane started from. Two mutations, red and restored: a sensor array element left undispositioned, and one controller input dropped from its partition.
…is not its bytes This closes lane S step 2, in the same change as the decode, because that is what the ruling required: there must be no interval in which a consumer can hold a decoded program and not know whether it is whole. A decode can succeed while leaving members it does not model. Such a program is a perfectly good OBSERVATION and an unusable basis for policy -- the residue is exactly the part nobody has decided about, so an intent derived from the represented part would silently drop it on the next write. The gate refuses while any residue remains. The two refusals are not one finding at two severities. Unmodelled residue means this repository is behind the document and the fix is a model change here; a defective known field means the document is wrong against a field we do model and the fix is on the host. Collapsing them sends half the work to the wrong place, and the residue case must not read as an error in the fleet's configuration. Defective is reported first, because an operator can act on it without waiting for anything here. THE SEMANTIC DIGEST ANSWERS "DID THE PROGRAM CHANGE", WHICH IS NOT "DID THE FILE CHANGE". The capture receipt already carries the byte digest and that is the right identity for the file. Two hosts running the identical program must carry one identity even when their files differ in every way a file can differ without the daemon noticing: member order, whitespace, `30` against `30.0`. The digest's subject is a rendering of the semantic model in a fixed field order, with every magnitude through the exact decimal's canonical wire and every coproduct arm as its own name -- so an absent field and a present-but-unstated one render alike only if they mean the same thing. Every magnitude renders as a string, which looks odd and is the point: a JSON number in the rendering would be a second numeral for a value this tree carries exactly, and would reintroduce the `30` against `30.0` question inside the artifact built to settle it. The program's sensor and controller lists are rendered in model order and NOT sorted, which is the opposite of the curve's treatment and rests on a different fact. A curve's positions are named by the document's own integer keys, so its order is recoverable. These lists have only array position, so their order is their identity as far as anything here can tell, and sorting would assert an equivalence nothing has established. If upstream loads them order-independently, that is a fact to read and cite, and the site that changes is named. Both captured programs pass the gate, and their digests differ -- the two hosts do not run the same program, and a digest reporting them equal would report a uniform fleet that does not exist. Three mutations red and restored: the residue gate disabled; the read path dropped from the rendering; every magnitude rendered as one constant. THE THIRD OF THOSE STAYED GREEN AT FIRST AND THE WITNESS RECORDS WHY. A digest blind to every number in the program passed every conjunct: the two hosts still differed by their sensor roster, and the fixture pair differed by a path. Two zone fixtures differing only in one coefficient, and a second pair spelling one coefficient two ways, are what reach it.
… and refuse to invent it
An adoption says an operator accepted a particular program. Decoder provenance says
which decoder, over which bytes, produced the reading that acceptance was made from.
Folding the second into the first decides one case wrongly:
a new decoder + the same artifact + the same semantic digest
-> the adopted policy still means what it meant; nobody re-adopts anything
a corrected decoder producing a DIFFERENT digest from the same bytes
-> the old adoption is about a program nobody runs, and needs adjudication
Folded together, every harmless refactor of this decoder would look like the second and
demand the operator re-approve the fleet's fans.
THE IDENTITY IS NOT AUTHORED, AND THAT IS THIS MODULE'S ENTIRE CONTENT TODAY. Both
digests are properties of an execution -- the transitive source closure that ran, and
the compiler binary that ran it -- so a hand-written pair would be two literals typed by
the same person who typed the decoder, joined by nothing. That is exactly the fake join
removed from the capture observer on #9299: two constants that agree because one author
wrote both, and that keep agreeing after the thing they describe has changed.
So the absent state is a named state that every consumer must match, not a placeholder
value. A receipt with no decoder identity is usable for saying WHAT was read and not for
saying that two readings came from the same reader --
receipt_decoder_is_identified answers false today, deliberately.
The two-digest shape already exists here: tools.multi_module_compile_fixture carries a
structural source_digest over its exact source vector and a compiler_digest from the
running compiler's own content hash, and its note records why both are absent from its
refused arm. This reuses that concept rather than minting a fan-specific one, and names
the instrument obligation that dissolves the absent state.
gunbai-bot
Bot
changed the title
…e local aliases
review 56966, and it is right: DecimalCelsius, DecimalCelsiusDelta, DecimalPercent,
DecimalSeconds and DecimalMilliseconds were parallel Measure aliases minted outside the
canonical authority. An alias is a second name for a type std.measure already
expresses, and a second name is what single-authority forbids however convenient it
reads. They are deleted; the types are written out where they are used.
THE RULING'S OTHER REMEDY WAS MEASURED BEFORE THIS ONE WAS CHOSEN. Hosting the
ExactDecimal-parameterised aliases in std/measure.dag is refused by execution:
circular dependency detected: std.bytes -> std.decimal -> std.integer -> std.measure
since std.integer already consumes std.measure. That cycle is closable, and the honest
statement is that I closed it in this session rather than that it is a law: it exists
only because std.decimal imports std.bytes for the divergent seam its negative-scale
arm uses, and inlining `1 / 0` in decimal breaks it -- also measured, the alias then
resolves in std.measure.
It was not taken. std.bytes' own note records that seam as ONE seam projected per
result type and marks the existing pair as a deliberate duplication awaiting a bottom
type; adding a third copy to widen an alias family trades a naming defect for a worse
one, in a load-bearing file, to save characters. Writing the type out costs nothing.
DecimalPercent went further and was deleted outright rather than expanded: it had no
remaining use once the zone's output units became their own named ZoneDemandValue, and
its constructor was dead too. A dead alias is the cheapest kind to remove.
All five witnesses green after the change.
Contributor
Author
|
Fixed in the head commit — the five aliases are gone. Verified first, and the finding holds. The first remedy you offered is not available, and I measured that rather than assuming it. Hosting the
One correction to that, because it would be misleading to leave it as an immovable law: the cycle exists only because of an edge I added in this same PR. I did not take it.
All five lane witnesses are green after the change. — sent from wise-eagle-112 |
…with its seam named The side-chat traced the defect to an exact owner and I verified it against the source: src/v1/04_lookup.dag `field_summary_for_type` opens `if field == "value" && normed_opt`, and `lookup_field_type_node` carries the same name-conditioned branch. So the behaviour is a decision written down, not an emergent one -- field access through an optional auto-unwraps for every spelling except `value`, which selects the payload. THE CLASS IS TWO QUESTIONS AND THE ROW KEEPS THEM APART, because only one is unambiguously a defect. Whether `.value` should select the payload, unwrap to the record's field, or refuse as ambiguous is a language-semantics decision. But whichever is chosen, a record-valued expression must not be accepted where an Int is required -- and `boxes.first().value == 99` resolves clean, evaluates, and answers false. That half is below floor independently, and it can be fixed first. It is filed as item 0 of the audit queue in the compiler-guarantee recovery gap analysis, which is DESIGN's named authority for compiler guarantee classes, rungs and triggers. The reproduction and its `.tag` control are inline there rather than in a separate artifact: docs/probes/ was bankrupted and deleted whole on 2026-08-24, and re-creating a probe directory would re-open the parallel measurement corpus that deletion closed. It is NOT enrolled as floor_expected_red. That roster's rows are executing failures somebody is actively repairing; this has no repair owner. Enrolling it would use the roster as an ownerless defect backlog, which its own contract refuses. The lane annotation now points at that row and keeps only the local fact -- the rename to `magnitude` is a workaround and this module claims no compiler guarantee. It is no longer the sole home of the reproduction.
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 28, 2026
gunbc.bmc_fan_alignment_standing held srv3 and srv4 at ObservedProgramNotRepresentableByIntent, whose payload named the exact gap: "the host runs two fan controller entries and BmcFanCurve models one". That gap is closed. extdeps.bmc.pid_control_program ProgramZone carries thermal_demand_controllers and actuator_controllers as separate lists, each ActuatorController with its own feed_forward, output_limits and slew -- one thermal demand feeding several actuators, which is the shape that was missing. ESTABLISHED TWO INDEPENDENT WAYS, not by reading the type. The representability gate passes on both captured hosts by execution (#9491); and the captures themselves carry exactly one `stepwise` TEMP_SOC controller driving two `fan` entries, FAN1 and CHASSIS. The captures are dated 2026-08-27, AFTER the 2026-08-26 hand reconfiguration, so they are the running programs rather than their predecessors -- checked, because representability proven against a superseded capture would have been a false claim with the same green. A FOURTH ARM RATHER THAN A RECLASSIFICATION INTO AN EXISTING ONE. IntentMatchesObservedProgram is false AND admits apply, so relabelling into it would hand the actuator permission to overwrite the quieter hand-split program with the old single-actuator curve -- the exact outcome this carrier exists to prevent, reached with no code change. ObservedProgramNotAdopted is false too; somebody looked. The true state is representable, read, and DIVERGENT from the intent, and its remedy is an operator adoption decision rather than a modelling task or a host visit, so it may not share a reason symbol with either. BmcFanProjectionApplyRefusalCause gains the matching cause for the same reason. Alignment flipped; actuation did not. Apply stays refused for every host. THE VACATED ARM KEEPS ITS EVIDENCE. srv3/srv4 left ObservedProgramNotRepresentableByIntent but the arm is still live and a future host may occupy it, so the witness now CONSTRUCTS that standing rather than borrowing it from the fleet roster, and srv3_srv4_expected_missing survives as that construction's payload instead of becoming dead data. Verified by execution: all twelve witness conjuncts pass; the discriminating RED holds -- marking srv3 IntentMatchesObservedProgram turns the witness red and restoring returns it green; five neighbouring fan witnesses green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This was referenced Aug 28, 2026
briansrls
pushed a commit
that referenced
this pull request
Aug 28, 2026
* srv3/srv4 are representable now: split alignment from adoption gunbc.bmc_fan_alignment_standing held srv3 and srv4 at ObservedProgramNotRepresentableByIntent, whose payload named the exact gap: "the host runs two fan controller entries and BmcFanCurve models one". That gap is closed. extdeps.bmc.pid_control_program ProgramZone carries thermal_demand_controllers and actuator_controllers as separate lists, each ActuatorController with its own feed_forward, output_limits and slew -- one thermal demand feeding several actuators, which is the shape that was missing. ESTABLISHED TWO INDEPENDENT WAYS, not by reading the type. The representability gate passes on both captured hosts by execution (#9491); and the captures themselves carry exactly one `stepwise` TEMP_SOC controller driving two `fan` entries, FAN1 and CHASSIS. The captures are dated 2026-08-27, AFTER the 2026-08-26 hand reconfiguration, so they are the running programs rather than their predecessors -- checked, because representability proven against a superseded capture would have been a false claim with the same green. A FOURTH ARM RATHER THAN A RECLASSIFICATION INTO AN EXISTING ONE. IntentMatchesObservedProgram is false AND admits apply, so relabelling into it would hand the actuator permission to overwrite the quieter hand-split program with the old single-actuator curve -- the exact outcome this carrier exists to prevent, reached with no code change. ObservedProgramNotAdopted is false too; somebody looked. The true state is representable, read, and DIVERGENT from the intent, and its remedy is an operator adoption decision rather than a modelling task or a host visit, so it may not share a reason symbol with either. BmcFanProjectionApplyRefusalCause gains the matching cause for the same reason. Alignment flipped; actuation did not. Apply stays refused for every host. THE VACATED ARM KEEPS ITS EVIDENCE. srv3/srv4 left ObservedProgramNotRepresentableByIntent but the arm is still live and a future host may occupy it, so the witness now CONSTRUCTS that standing rather than borrowing it from the fleet roster, and srv3_srv4_expected_missing survives as that construction's payload instead of becoming dead data. Verified by execution: all twelve witness conjuncts pass; the discriminating RED holds -- marking srv3 IntentMatchesObservedProgram turns the witness red and restoring returns it green; five neighbouring fan witnesses green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Rename a binding that conflated the two states this PR separates (review 57145) `srv4_maps_to_unrepresentable` held the representable-but-not-adopted verdict. Cosmetic anywhere else; here it undercuts the change's own thesis, since the whole point is that "no shape for it" and "shape exists, nobody adopted it" are different states with different remedies, and a reader trusting the binding name would take the conjunct as evidence for the arm it is not testing. Swept the file for the class rather than fixing the cited line alone: the other `unrepresentable` names are the constructed vacated-arm conjunct and its payload, where the word is correct and stays. Witness re-run green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * The fourth alignment state needs a refusal reason too (floor: non-exhaustive match) The split added BmcFanProjectionObservedProgramRepresentableNotAdopted to BmcFanProjectionApplyRefusalCause; bmc_converge's refusal-reason renderer still matched only the three it replaced. Total at the level examined, blind to the distinction this PR exists to draw. Caught by the required floor's strict preparation over the whole corpus, not by either entry compile or either review. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
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.
Lane S of three — the semantic lane. Steps 1 and 2 both land here, which is required rather than convenient.
The remaining fan-convergence work was adjudicated into three lanes with different operator authority:
Lane A is deliberately not bundled: srv3/srv4 already run the desired program, so a writer buys no thermal or acoustic benefit today. It buys repair of future drift and introduces the possibility of damaging cooling — a different risk class deserving its own decision.
Steps 1 and 2 are one PR because there must be no interval in which a consumer can hold a decoded program and not know whether it is whole.
What the fleet actually runs, and what the model says about it
One stepwise controller turns
TEMP_SOCinto a demand; that single demand feeds two actuator controllers with different transfer functions —FAN1subtracts 8 and floors at 3,CHASSISadds 35 and floors at 40. An earlier framing of this as "two curves" was wrong: it would model two demands where there is one, making the actuators look independently adjustable when moving the shared demand moves both.Three things are unrepresentable rather than checked: a curve point carries both halves, so the document's two parallel keyed objects cannot produce a half-paired point; demand controllers and actuators are separate fields, so an actuator cannot appear where a demand controller is expected; and the two
setpointkeys — degrees for one, demand units for the other — are separated by type.The conservation wall
A decoder reads the members it understands and returns a typed record. Nothing in that shape stops it silently ignoring a member it does not model, and the result still looks complete. The wall is a checked partition: every member occurrence accounted for exactly once.
Identity, not count.
source.length() == consumed + unmodeled + defectivepasses this: drop the unmodelled member at ordinal 3, classify the member at ordinal 1 twice. Same total, one member lost, one double-counted, green. The join therefore runs both directions and compares whole identities.An occurrence is a position, not a key —
{"type": "fan", "type": "stepwise"}is legal JSON, and a residue reported as"type"cannot say which occurrence was read.Defective is not unmodelled — opposite owners. Unmodelled means this repo is behind the document; defective means the document is wrong against a field we do model.
Arrays conserve too, and without that the object wall is half a wall: a decoder can conserve every member of every object it chose to decode while skipping one PID array element. Four populations are covered —
sensors,zones, each zone'spids, and each controller'sinputs. That last is not filler:CHASSISdrives three fans, and dropping one is the wiring error this whole lane started from.Exact numbers, in the JSON authority
srv3 writes
minThermalOutputas30.0; srv4 writes30. Asking whether the two hosts run the same program is asking whether two numerals denote the same number, and no comparison of lexemes answers that.This tree deliberately had no JSON-number-to-value decode.
extdeps.github.workflow_run_event's run_id note already ruled where one belongs when a consumer finally needed it — "the decode lands in the JSON authority with its own witness, not here" — so that is where it went, rather than becoming a second reading of RFC 8259 inside a fan reader.The carrier is exact (units over a power of ten). A float carrier would make
0.1and its nearest double indistinguishable at exactly the point where the question is whether two documents agree. Exponent form refuses rather than being expanded — deciding what1e400becomes has no non-fabricated answer.The curve
Pairing is by the key the daemon asks for. phosphor-pid-control requests the exact key it computes from an integer position; it does not normalise, so
"01"is a key it never looks up.Refusals: a non-canonical key (naming the canonical spelling), a duplicated exact key, a reading with no output and an output with no reading as separate arms, a duplicated or non-object side, a quoted value, an exponent value. Points are ordered by index, not authored member order — the daemon loads by position, so a program that changed on reordering would make every downstream digest sensitive to a difference the running system does not have.
Monotonicity is not checked: a descending curve is defective, but refusing it at the decode makes a badly-configured host unobservable. The observer's job is to say what is running, including when what is running is wrong.
Representability and semantic identity
The gate refuses while any residue remains, because residue is exactly the part nobody has decided about — an intent derived from the represented part would silently drop it on the next write.
The semantic digest answers did the program change, which is not did the file change; the capture receipt already carries the byte digest for the latter. Two hosts running one program must carry one identity even when their files differ in member order, whitespace, or
30vs30.0. Both captured programs pass the gate, and their digests differ — the two hosts do not run the same program.Decoder identity is modelled and not authored. Both digests are properties of an execution, so a hand-written pair would be two literals typed by the same person who typed the decoder, joined by nothing — the fake join removed on #9299. The absent state is a named state every consumer must match.
Discriminating evidence
Every wall has mutations that go red and are restored. Three of them are recorded because they stayed green and that is the more useful result:
Relation to the partial authority that already existed
extdeps.bmc.openbmc_fan_controlOpenBmcStepwiseControllermodels a subset of the same concept:Nat/Intmagnitudes that cannot spell the deployed-8.0,-3.0,-0.5; a curve as two parallel lists so an unpaired curve is representable; no PID coefficients at all, so the feed-forward offset that is the difference between the two deployed actuators is absent. It has an actuation consumer, and actuation is lane A, so this is the gap-intolerant-boundary carve-out: frozen, with the dissolution named on the new model. Lane A is a cutover, not a greenfield write.Two things this PR does not claim
A substrate defect is reported, not repaired. A field named
valueon a record read throughlist.first()does not resolve to that field: access through an optional auto-unwraps for every other name (boxes.first().tagreads the field) but.valuereads the optional's payload and returns the record — andboxes.first().value == 99places a record against anIntand typechecks clean. Here it made every decoded curve output silently carry the entry record instead of its magnitude. The field is renamed tomagnitude; that rename is a workaround, is marked as one, and carries the minimal reproduction. It needs an owner below this lane.Two upstream facts are named as open rather than asserted. Review reported the runtime computes
(setpoint + offset) * gainwhere an earlier annotation saiddemand * gain + offset, and that slew is per unit time rather than per sample. At the deployed gain of1.0and sample period of1.0both pairs are numerically identical, so nothing in this lane can distinguish them — which is how the wrong ones survived being written down. Nobody who wrote these files has read that runtime, so rather than replace one unverified claim with another, the model states the fields and not the arithmetic, with the trigger recorded at each site. The same applies to a bounded stepwise position count, which is why no numeric bound is enforced.CI
A floor failure attributable to
product.fabric.contentionis inherited main breakage, not evidence about this PR. #9397 renamedsupply'sgrant_duration_secondsand made it partial;contentionwas not migrated with it. #9488 is the focused repair. When it lands, main merges in and the lane controls rerun before CI is read.