diff --git a/dag/extdeps/bmc/pid_control_decode.dag b/dag/extdeps/bmc/pid_control_decode.dag new file mode 100644 index 00000000000..696140045ce --- /dev/null +++ b/dag/extdeps/bmc/pid_control_decode.dag @@ -0,0 +1,1417 @@ +module extdeps.bmc.pid_control_decode + +import std.types { Bool, Int, List, NonEmptyStr, String } +import std.decimal { ExactDecimal, canonical_exact_decimal } +import extdeps.languages.json.emit { JsonArray, JsonBool, JsonKeyValue, JsonNull, JsonNumber, JsonObject, JsonString, JsonValue } +import extdeps.languages.json.number { + JsonNumberMagnitudeOutsideCarrierRange, + JsonNumberExact, + JsonNumberOutsideExactFragment, + JsonNumberUsesExponent, + JsonNumberValueRead, + JsonNumberReading, + JsonValueIsNotANumber, + read_json_number_value, +} +import extdeps.languages.json.member_conservation { + ArrayElementPartition, + ConservationVerdict, + ElementConsumed, + ElementDisposition, + JsonArrayElementOccurrence, + array_element_occurrences, + element_conservation_verdict, + JsonMemberOccurrence, + MembersConserved, + MemberConsumed, + MemberDisposition, + MemberUnmodeled, + ObjectMemberPartition, + conservation_verdict, + occurrences_of_object, +} +import extdeps.bmc.pid_control_program { + BmcFanControlProgram, + DbusBoundsDisposition, + DbusBoundsIgnored, + DbusBoundsUnstated, + DbusBoundsUsed, + DemandCurvePoint, + FanTachometerSensor, + ProgramSensor, + ProgramSensorRole, + SensorBoundsDeclared, + SensorBoundsUnstated, + SensorDrivesOutput, + SensorReadOnly, + SensorReadingBounds, + SensorTimeoutDeclared, + SensorTimeoutUnstated, + ActuatorController, + FeedForward, + IntegralBounds, + OutputBounds, + PidGains, + SlewLimits, + TemperatureSensor, + ProgramZone, + ThermalDemandController, + decimal_celsius, + decimal_celsius_delta, + zone_demand_value, + decimal_milliseconds, + decimal_seconds, +} + +// DECODING A CAPTURED CONFIGURATION ONTO THE NEUTRAL MODEL. Every refusal here is typed and names +// the path it was found at, because the consumer of a refusal is a person about to change a +// deployed program and "the document is malformed" tells them nothing about which line to open. + +// WHERE, IN THE DOCUMENT'S OWN COORDINATES. A path is authored by the walk rather than by the +// reader, so a refusal cannot name a location the walk did not visit. +type DocumentPath { + text: NonEmptyStr +} + +fn document_path(text: NonEmptyStr) -> DocumentPath { + DocumentPath { text: text } +} + +fn path_field(parent: DocumentPath, field: NonEmptyStr) -> DocumentPath { + DocumentPath { text: join([parent.text, ".", field], "") } +} + +fn path_index(parent: DocumentPath, index: Int) -> DocumentPath { + DocumentPath { text: join([parent.text, "[", to_string(index), "]"], "") } +} + +fn path_key(parent: DocumentPath, key: String) -> DocumentPath { + DocumentPath { text: join([parent.text, "{", key, "}"], "") } +} + +// THE REFUSAL VOCABULARY IS CLOSED AND EACH ARM HAS ITS OWN REPAIR. A missing field means the +// document is incomplete; a duplicated one means it is ambiguous and the daemon's choice between +// them is not something this decoder is entitled to make; a wrong-kinded value means the document +// is wrong; an exponent-form number means the document is outside the fragment this tree reads +// exactly. Collapsing any pair of those sends a reader to the wrong repair. +type FieldRefusal + = FieldAbsent { path: DocumentPath, field: NonEmptyStr } + | FieldDuplicated { path: DocumentPath, field: NonEmptyStr, occurrences: Int } + | FieldNotAnObject { path: DocumentPath, field: NonEmptyStr } + | FieldNotANumber { path: DocumentPath, field: NonEmptyStr } + | FieldNotAString { path: DocumentPath, field: NonEmptyStr } + | FieldNotABool { path: DocumentPath, field: NonEmptyStr } + | FieldNotAnArray { path: DocumentPath, field: NonEmptyStr } + | FieldNumberOutsideExactFragment { path: DocumentPath, field: NonEmptyStr } + | FieldValueUnknown { path: DocumentPath, field: NonEmptyStr, value: String } + | FieldNotAnInteger { path: DocumentPath, field: NonEmptyStr } + +type DecimalField + = DecimalFieldRead { value: ExactDecimal } + | DecimalFieldRefused { refusal: FieldRefusal } + +fn members_named(value: JsonValue, key: String) -> List { + match value { + JsonObject { members: ms } => map(filter(ms, m => m.key == key), m => m.value) + JsonNull => [] + JsonBool { value: _ } => [] + JsonNumber { lexeme: _ } => [] + JsonString { value: _ } => [] + JsonArray { elements: _ } => [] + } +} + +fn value_is_object(value: JsonValue) -> Bool { + match value { + JsonObject { members: _ } => true + JsonNull => false + JsonBool { value: _ } => false + JsonNumber { lexeme: _ } => false + JsonString { value: _ } => false + JsonArray { elements: _ } => false + } +} + +// ONE SELECTOR, USED BY EVERY FIELD READ, SO THAT ABSENT AND DUPLICATED CANNOT DIVERGE BETWEEN +// FIELDS. RFC 8259 permits duplicate names and does not say which wins, so a duplicated field is +// refused rather than resolved -- last-wins here would let a document carrying two outLim_min +// values read as whichever the writer put second. +type SelectedMember + = MemberSelected { value: JsonValue } + | MemberSelectionRefused { refusal: FieldRefusal } + +fn select_member(container: JsonValue, path: DocumentPath, field: NonEmptyStr) -> SelectedMember { + if !value_is_object(value: container) { + MemberSelectionRefused { refusal: FieldNotAnObject { path: path, field: field } } + } else { + let hits = members_named(value: container, key: field as String) + if hits.length() == 0 { + MemberSelectionRefused { refusal: FieldAbsent { path: path, field: field } } + } else if hits.length() > 1 { + MemberSelectionRefused { + refusal: FieldDuplicated { path: path, field: field, occurrences: hits.length() }, + } + } else { + MemberSelected { value: hits.first() } + } + } +} + +fn decimal_of_value(value: JsonValue, path: DocumentPath, field: NonEmptyStr) -> DecimalField { + match read_json_number_value(v: value) { + JsonValueIsNotANumber => DecimalFieldRefused { refusal: FieldNotANumber { path: path, field: field } } + JsonNumberValueRead { reading } => + match reading { + JsonNumberExact { value: exact } => DecimalFieldRead { value: exact } + JsonNumberOutsideExactFragment { lexeme: _, refusal: _ } => + DecimalFieldRefused { + refusal: FieldNumberOutsideExactFragment { path: path, field: field }, + } + } + } +} + +fn decimal_field(container: JsonValue, path: DocumentPath, field: NonEmptyStr) -> DecimalField { + match select_member(container: container, path: path, field: field) { + MemberSelectionRefused { refusal } => DecimalFieldRefused { refusal: refusal } + MemberSelected { value } => decimal_of_value(value: value, path: path, field: field) + } +} + +// THE CURVE IS THE HARDEST OBJECT IN THE DOCUMENT AND THE ONE MOST WORTH REFUSING PRECISELY. It 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, because +// object member order is authored and the two objects could disagree on it. +type CurveSide = ReadingSide | OutputSide + +fn curve_side_field(side: CurveSide) -> NonEmptyStr { + match side { + ReadingSide => "reading" + OutputSide => "output" + } +} + +// WHY A KEY THAT IS NOT A PLAIN INDEX REFUSES INSTEAD OF BEING SKIPPED. A skipped key is a curve +// point silently missing from the decoded program, so the model would describe a fan curve the +// host is not running -- and the missing point would be invisible precisely because the decoder +// decided it was uninteresting. +// +// AND WHY TWO KEYS THAT NORMALISE TO ONE INDEX REFUSE RATHER THAN ONE WINNING. "1" and "01" are +// different member names in JSON and the same integer here. Picking either is picking a curve the +// document does not unambiguously state, and the daemon's own choice between them is not knowable +// from the document. +type CurveRefusal + = CurveSideMissing { path: DocumentPath, side: CurveSide } + | CurveSideNotAnObject { path: DocumentPath, side: CurveSide } + | CurveSideDuplicated { path: DocumentPath, side: CurveSide, occurrences: Int } + | CurveKeyNotAnIndex { path: DocumentPath, side: CurveSide, key: String } + | CurveKeyDuplicated { path: DocumentPath, side: CurveSide, key: String, occurrences: Int } + | CurveKeyNotCanonical { path: DocumentPath, side: CurveSide, key: String, canonical: String } + | CurveKeySetsDisagree { path: DocumentPath, side: CurveSide, key: String } + | CurveValueNotANumber { path: DocumentPath, side: CurveSide, key: String } + | CurveValueOutsideExactFragment { path: DocumentPath, side: CurveSide, key: String } + | CurveReadingWithoutOutput { path: DocumentPath, index: Int } + | CurveOutputWithoutReading { path: DocumentPath, index: Int } + +type IndexedDecimal { + index: Int + key: String + magnitude: ExactDecimal +} + +type CurveSideDecode + = CurveSideDecoded { entries: List } + | CurveSideRefused { refusal: CurveRefusal } + +fn curve_key_index(key: String) -> Int? { + parse_int(s: key) +} + +fn indexed_decimal_entries_with(entries: List, index: Int) -> List { + filter(entries, entry => entry.index == index) +} + +// EACH SIDE ADMITS ONLY EXACT, CANONICALLY SPELLED KEYS, AND THAT IS AN UPSTREAM FACT RATHER THAN +// A TIDINESS RULE. 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 simply a key it never asks for. A +// decoder that read "01" as index 1 would report a curve point the daemon does not load. +// +// THE FIRST VERSION NORMALISED AND JOINED ON THE INTEGER, and the hole that opened is the one this +// pair of refusals closes: `"reading": {"1": 55}` against `"output": {"01": 30}` has one member on +// each side, so no within-side collision exists, both normalise to 1, and the two paired -- across +// key sets that do not agree. Measured before the change, that document decoded to a curve point. +fn curve_side_fold( + path: DocumentPath, + side: CurveSide, + members: List, + acc: CurveSideDecode, +) -> CurveSideDecode { + fold(members, init: acc, f: (state, member) => { + match state { + CurveSideRefused { refusal } => CurveSideRefused { refusal: refusal } + CurveSideDecoded { entries } => + match curve_key_index(key: member.key) { + Absent => + CurveSideRefused { + refusal: CurveKeyNotAnIndex { path: path, side: side, key: member.key }, + } + Present { value: index } => { + let same_key = filter(entries, entry => entry.key == member.key) + if same_key.length() > 0 { + CurveSideRefused { + refusal: CurveKeyDuplicated { + path: path, + side: side, + key: member.key, + occurrences: same_key.length() + 1, + }, + } + } else if to_string(index) != member.key { + CurveSideRefused { + refusal: CurveKeyNotCanonical { + path: path, + side: side, + key: member.key, + canonical: to_string(index), + }, + } + } else { + match decimal_of_value(value: member.value, path: path, field: curve_side_field(side: side)) { + DecimalFieldRefused { refusal } => + match refusal { + FieldNumberOutsideExactFragment { path: p, field: _ } => + CurveSideRefused { + refusal: CurveValueOutsideExactFragment { path: p, side: side, key: member.key }, + } + other => + CurveSideRefused { + refusal: CurveValueNotANumber { path: path, side: side, key: member.key }, + } + } + DecimalFieldRead { value } => + CurveSideDecoded { + entries: entries.append(IndexedDecimal { index: index, key: member.key, magnitude: value }), + } + } + } + } + } + } + }) +} + +fn decode_curve_side(container: JsonValue, path: DocumentPath, side: CurveSide) -> CurveSideDecode { + let field = curve_side_field(side: side) + let hits = members_named(value: container, key: field as String) + if hits.length() == 0 { + CurveSideRefused { refusal: CurveSideMissing { path: path, side: side } } + } else if hits.length() > 1 { + CurveSideRefused { + refusal: CurveSideDuplicated { path: path, side: side, occurrences: hits.length() }, + } + } else { + match hits.first() { + JsonObject { members } => + curve_side_fold( + path: path_field(parent: path, field: field), + side: side, + members: members, + acc: CurveSideDecoded { entries: [] }, + ) + other => CurveSideRefused { refusal: CurveSideNotAnObject { path: path, side: side } } + } + } +} + +// THE MAGNITUDE FIELD IS NOT NAMED `value`, AND THAT IS FORCED BY AN OPEN SUBSTRATE DEFECT RATHER +// THAN CHOSEN. Written as `IndexedDecimal { .., value: ExactDecimal }`, every decoded curve output +// silently carried the ENTRY RECORD instead of its magnitude, and nothing refused -- the failure +// surfaced only later, as a field lookup for `fraction_digits` on an IndexedDecimal. +// +// THE CAUSE, REDUCED TO A MINIMAL EXECUTABLE REPRODUCTION AND MEASURED BOTH WAYS RATHER THAN +// INFERRED. `list.first()` yields an optional. Field access through it auto-unwraps: for a record +// `Boxed { tag: Int, value: Int }`, `boxes.first().tag` reads the field and returns 1. But +// `boxes.first().value` does NOT read the field -- it reads the OPTIONAL's own payload and returns +// the Boxed record. The two accesses on one expression resolve against two different carriers, +// decided by the field's name, with no diagnostic at either the type check or the evaluation. +// +// This is a floor-level miss, not a subtlety: the comparison `boxes.first().value == 99` places a +// record against an Int and typechecks clean. It is reported rather than only dodged, per the +// standing rule that noticing a workaround is the line-stop signal. +// +// THE DEFECT NOW HAS A HOME, AND THIS FILE IS NOT IT. The seam is named and the class is filed as +// item 0 of the audit queue in docs/plans/compiler-guarantee-recovery-gap-analysis.md, which is +// the authority for compiler guarantee classes, their rungs and their triggers -- including the +// split between the language-semantics question and the type-conformance half that is below floor +// regardless of how the first is answered. What is claimed HERE is only the local fact: the rename +// to `magnitude` is a workaround, and no compiler guarantee is claimed by this module. +fn indexed_decimal_value_at(entries: List, index: Int) -> ExactDecimal { + let matched = indexed_decimal_entries_with(entries: entries, index: index) + let entry = matched.first() + entry.magnitude +} + +type CurveDecode + = CurveDecoded { points: List } + | CurveRefused { refusal: CurveRefusal } + +// THE JOIN IS BY INDEX AND THE KEY WALL ABOVE IS WHAT MAKES THAT EXACT. Written as an exact-key +// join instead, it was measured to be indistinguishable: once every admitted key is canonical, the +// keys and the indices are in bijection, so reducing the join to the index left every witness +// green. Two mechanisms deciding one correspondence is the redundancy DESIGN removes, 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 happily pair them into a point the +// daemon never loads. +// +// THE JOIN RUNS IN BOTH DIRECTIONS, for the same reason the member conservation join does: a +// reading with no output and an output with no reading are different defects, and checking only +// one direction lets the other through whenever the two objects have equal key counts. +fn curve_join(path: DocumentPath, readings: List, outputs: List) -> CurveDecode { + let unpaired_reading = filter(readings, r => indexed_decimal_entries_with(entries: outputs, index: r.index).length() == 0) + let unpaired_output = filter(outputs, o => indexed_decimal_entries_with(entries: readings, index: o.index).length() == 0) + if unpaired_reading.length() > 0 { + CurveRefused { refusal: CurveReadingWithoutOutput { path: path, index: unpaired_reading.first().index } } + } else if unpaired_output.length() > 0 { + CurveRefused { refusal: CurveOutputWithoutReading { path: path, index: unpaired_output.first().index } } + } else { + CurveDecoded { + points: sort_by( + map(readings, r => + DemandCurvePoint { + index: r.index, + reading: decimal_celsius(value: r.magnitude), + output: zone_demand_value(value: indexed_decimal_value_at(entries: outputs, index: r.index)), + } + ), + point => point.index, + ), + } + } +} + +// THE DECODED CURVE IS ORDERED BY INDEX, NOT BY AUTHORED MEMBER ORDER, and that is semantic +// canonicalisation rather than a validation. The daemon loads by integer position, so a document +// whose reading object lists its members in a different order describes the SAME curve -- and a +// semantic program that changed because someone reordered two members would make every downstream +// digest and comparison sensitive to a difference the running system does not have. The authored +// order remains in the captured artifact, which is where it belongs. +// +// ONE UPSTREAM BOUND IS DELIBERATELY NOT ENFORCED HERE, AND IS NAMED RATHER THAN GUESSED. Review +// reported that phosphor-pid-control loads a bounded number of stepwise positions, so a key beyond +// that bound would be a document the daemon does not fully load even though this decoder accepts +// it. That is plausible and it is not verified against the upstream source by anyone who wrote +// this file, so no numeric bound is asserted: writing a limit read from a summary would put a +// fabricated constant in the one place this module exists to keep exact. NEXT-RUNG TRIGGER: read +// the loader in the cited upstream, then add CurveIndexOutsideLoadedRange with the bound and its +// citation. Until then the exact-key and canonical-spelling walls above stand, and they already +// close the substitution class; what remains open is over-acceptance of a high index, which +// produces a program that says MORE than the daemon runs rather than something different. +// +// MONOTONICITY IS STILL NOT CHECKED HERE. A curve whose readings descend is a defective program, but refusing it at +// the decode would make a badly-configured host unobservable -- the observer's job is to say what +// is running, including when what is running is wrong. That check belongs on the model, where it +// can be reported about a program that was successfully read. +fn decode_curve(container: JsonValue, path: DocumentPath) -> CurveDecode { + match decode_curve_side(container: container, path: path, side: ReadingSide) { + CurveSideRefused { refusal } => CurveRefused { refusal: refusal } + CurveSideDecoded { entries: readings } => + match decode_curve_side(container: container, path: path, side: OutputSide) { + CurveSideRefused { refusal } => CurveRefused { refusal: refusal } + CurveSideDecoded { entries: outputs } => + curve_join(path: path, readings: readings, outputs: outputs) + } + } +} + +// FROM HERE DOWN, EVERY OBJECT DECODE RETURNS ITS MEMBER DISPOSITIONS ALONGSIDE ITS VALUE. That is +// what wires the conservation wall into the decode rather than leaving it as 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 +// dispositions are built at the same place the fields are read, so a new field cannot be consumed +// without appearing in them. +type ObjectDecodeResidue { + path: DocumentPath + source: List + dispositions: List +} + +fn occurrence_at(source: List, ordinal: Int) -> List { + filter(source, occurrence => occurrence.identity.ordinal == ordinal) +} + +fn occurrences_named(source: List, key: String) -> List { + filter(source, occurrence => occurrence.member.key == key) +} + +// A CONSUMED MEMBER IS RECORDED BY ITS OCCURRENCE, NOT BY ITS KEY, so that a document carrying a +// field twice produces two occurrences and the decoder's single read accounts for exactly one of +// them -- leaving the other unaccounted, which is what the duplicate refusal above already +// reported and what the conservation join independently confirms. +fn consumed_disposition(source: List, key: String, role: NonEmptyStr) -> List { + map(occurrences_named(source: source, key: key), occurrence => + MemberConsumed { occurrence: occurrence, role: role }) +} + +// EVERY OCCURRENCE THE FIELD READS DID NOT CLAIM IS UNMODELLED, AND THAT IS DERIVED RATHER THAN +// LISTED. A hand-written residue list is a second place to forget a field; deriving it from the +// keys actually consumed means a member the decoder does not read cannot be silently absent from +// the residue either. +fn unmodeled_dispositions(source: List, consumed_keys: List) -> List { + map( + filter(source, occurrence => !any(consumed_keys, key => key == occurrence.member.key)), + occurrence => MemberUnmodeled { occurrence: occurrence }, + ) +} + +fn object_partition( + path: DocumentPath, + container: JsonValue, + consumed: List, +) -> ObjectMemberPartition { + let source = occurrences_of_object(object_path: path.text, value: container) + let consumed_keys = map(consumed, key => key as String) + ObjectMemberPartition { + object_path: path.text, + source: source, + dispositions: flat_map( + [ + flat_map(consumed, key => consumed_disposition(source: source, key: key as String, role: key)), + unmodeled_dispositions(source: source, consumed_keys: consumed_keys), + ], + group => group, + ), + } +} + +type StringField + = StringFieldRead { value: String } + | StringFieldRefused { refusal: FieldRefusal } + +fn string_field(container: JsonValue, path: DocumentPath, field: NonEmptyStr) -> StringField { + match select_member(container: container, path: path, field: field) { + MemberSelectionRefused { refusal } => StringFieldRefused { refusal: refusal } + MemberSelected { value: v } => + match v { + JsonString { value: s } => StringFieldRead { value: s } + other => StringFieldRefused { refusal: FieldNotAString { path: path, field: field } } + } + } +} + +// AN OPTIONAL FIELD IS A THREE-WAY ANSWER, NOT A TWO-WAY ONE. Present-and-readable, absent, and +// present-but-wrong are different facts: the middle one is the document declining to state a +// policy and the last is the document stating it wrongly. A reader that folded the third into the +// second would report a malformed timeout as an unstated one. +type OptionalDecimalField + = OptionalDecimalRead { value: ExactDecimal } + | OptionalDecimalUnstated + | OptionalDecimalRefused { refusal: FieldRefusal } + +fn optional_decimal_field(container: JsonValue, path: DocumentPath, field: NonEmptyStr) -> OptionalDecimalField { + let hits = members_named(value: container, key: field as String) + if hits.length() == 0 { + OptionalDecimalUnstated + } else { + match decimal_field(container: container, path: path, field: field) { + DecimalFieldRefused { refusal } => OptionalDecimalRefused { refusal: refusal } + DecimalFieldRead { value } => OptionalDecimalRead { value: value } + } + } +} + +type OptionalBoolField + = OptionalBoolRead { value: Bool } + | OptionalBoolUnstated + | OptionalBoolRefused { refusal: FieldRefusal } + +fn optional_bool_field(container: JsonValue, path: DocumentPath, field: NonEmptyStr) -> OptionalBoolField { + let hits = members_named(value: container, key: field as String) + if hits.length() == 0 { + OptionalBoolUnstated + } else { + match select_member(container: container, path: path, field: field) { + MemberSelectionRefused { refusal } => OptionalBoolRefused { refusal: refusal } + MemberSelected { value: v } => + match v { + JsonBool { value: b } => OptionalBoolRead { value: b } + other => OptionalBoolRefused { refusal: FieldNotABool { path: path, field: field } } + } + } + } +} + +type SensorDecode + = SensorDecoded { sensor: ProgramSensor, partition: ObjectMemberPartition } + | SensorRefused { refusal: FieldRefusal } + +// THE ROLE STRING IS A CLOSED VOCABULARY AND AN UNKNOWN ONE REFUSES. phosphor-pid-control's own +// schema admits exactly these two sensor types; a third would mean this decoder is behind its +// upstream, which is a fact worth stopping on rather than reading as "some other kind of sensor". +type SensorRoleRead + = SensorRoleKnown { role: ProgramSensorRole } + | SensorRoleUnknown + +fn sensor_role(value: String) -> SensorRoleRead { + if value == "fan" { + SensorRoleKnown { role: FanTachometerSensor } + } else if value == "temp" { + SensorRoleKnown { role: TemperatureSensor } + } else { + SensorRoleUnknown + } +} + +fn sensor_bounds(minimum: OptionalDecimalField, maximum: OptionalDecimalField) -> SensorReadingBounds { + match minimum { + OptionalDecimalRead { value: lo } => + match maximum { + OptionalDecimalRead { value: hi } => SensorBoundsDeclared { minimum: lo, maximum: hi } + other => SensorBoundsUnstated + } + other => SensorBoundsUnstated + } +} + +fn dbus_bounds_disposition(field: OptionalBoolField) -> DbusBoundsDisposition { + match field { + OptionalBoolRead { value: ignore } => if ignore { DbusBoundsIgnored } else { DbusBoundsUsed } + OptionalBoolUnstated => DbusBoundsUnstated + OptionalBoolRefused { refusal: _ } => DbusBoundsUnstated + } +} + +data sensor_consumed_keys: List = [ + "name", + "type", + "readPath", + "writePath", + "min", + "max", + "timeout", + "ignoreDbusMinMax", +] + +fn decode_sensor(container: JsonValue, path: DocumentPath) -> SensorDecode { + match string_field(container: container, path: path, field: "name") { + StringFieldRefused { refusal } => SensorRefused { refusal: refusal } + StringFieldRead { value: name } => + match string_field(container: container, path: path, field: "type") { + StringFieldRefused { refusal } => SensorRefused { refusal: refusal } + StringFieldRead { value: type_text } => + match sensor_role(value: type_text) { + SensorRoleUnknown => + SensorRefused { + refusal: FieldValueUnknown { path: path, field: "type", value: type_text }, + } + SensorRoleKnown { role } => + match string_field(container: container, path: path, field: "readPath") { + StringFieldRefused { refusal } => SensorRefused { refusal: refusal } + StringFieldRead { value: read_path } => { + let actuation = match string_field(container: container, path: path, field: "writePath") { + StringFieldRead { value: write_path } => SensorDrivesOutput { write_path: write_path } + other => SensorReadOnly + } + let timeout = match optional_decimal_field(container: container, path: path, field: "timeout") { + OptionalDecimalRead { value: seconds } => + SensorTimeoutDeclared { seconds: decimal_seconds(value: seconds) } + other => SensorTimeoutUnstated + } + SensorDecoded { + sensor: ProgramSensor { + name: name, + role: role, + read_path: read_path, + actuation: actuation, + bounds: sensor_bounds( + minimum: optional_decimal_field(container: container, path: path, field: "min"), + maximum: optional_decimal_field(container: container, path: path, field: "max"), + ), + dbus_bounds: dbus_bounds_disposition( + field: optional_bool_field(container: container, path: path, field: "ignoreDbusMinMax"), + ), + timeout: timeout, + }, + partition: object_partition( + path: path, + container: container, + consumed: sensor_consumed_keys, + ), + } + } + } + } + } + } +} + +// THE CONTROLLER ENTRIES SHARE ONE ARRAY AND ARE TOLD APART BY A `type` STRING, which is the one +// place the document forces a dispatch on a name. It happens exactly once, here, and everything +// downstream reads a list whose element type already answers the question. +type ControllerKind = ThermalDemandKind | ActuatorKind + +type ControllerKindRead + = ControllerKindKnown { kind: ControllerKind } + | ControllerKindUnknown + +fn controller_kind(value: String) -> ControllerKindRead { + if value == "stepwise" { + ControllerKindKnown { kind: ThermalDemandKind } + } else if value == "fan" { + ControllerKindKnown { kind: ActuatorKind } + } else { + ControllerKindUnknown + } +} + +type StringListField + = StringListRead { values: List } + | StringListRefused { refusal: FieldRefusal } + +fn string_list_field(container: JsonValue, path: DocumentPath, field: NonEmptyStr) -> StringListField { + match select_member(container: container, path: path, field: field) { + MemberSelectionRefused { refusal } => StringListRefused { refusal: refusal } + MemberSelected { value: v } => + match v { + JsonArray { elements } => { + let strings = flat_map(elements, element => + match element { + JsonString { value: s } => [s] + other => [] + }) + if strings.length() == elements.length() { + StringListRead { values: strings } + } else { + StringListRefused { refusal: FieldNotAString { path: path, field: field } } + } + } + other => StringListRefused { refusal: FieldNotAnArray { path: path, field: field } } + } + } +} + +type ControllerRefusal + = ControllerFieldRefused { refusal: FieldRefusal } + | ControllerCurveRefused { refusal: CurveRefusal } + | ControllerKindNotRecognised { path: DocumentPath, value: String } + +data thermal_controller_consumed_keys: List = [ + "name", + "type", + "inputs", + "setpoint", + "failsafePercent", + "pid", +] + +data thermal_pid_consumed_keys: List = [ + "samplePeriod", + "positiveHysteresis", + "negativeHysteresis", + "isCeiling", + "reading", + "output", +] + +type ThermalControllerDecode + = ThermalControllerDecoded { + controller: ThermalDemandController, + entry_partition: ObjectMemberPartition, + pid_partition: ObjectMemberPartition, + } + | ThermalControllerRefused { refusal: ControllerRefusal } + +// isCeiling IS REQUIRED RATHER THAN DEFAULTED TO FALSE, and that is the same judgement the sensor +// bounds field got in the other direction. A ceiling controller and a floor controller are +// opposite behaviours, and a decoder that supplies false for a document that did not say would be +// asserting the safer-sounding half of a distinction it cannot see. Every captured document states +// it; if one stops, that is a document to complete rather than a default to invent. +fn decode_thermal_controller( + container: JsonValue, + path: DocumentPath, + name: NonEmptyStr, + inputs: List, +) -> ThermalControllerDecode { + let pid_path = path_field(parent: path, field: "pid") + match select_member(container: container, path: path, field: "pid") { + MemberSelectionRefused { refusal } => + ThermalControllerRefused { refusal: ControllerFieldRefused { refusal: refusal } } + MemberSelected { value: pid } => + match decimal_field(container: container, path: path, field: "setpoint") { + DecimalFieldRefused { refusal } => + ThermalControllerRefused { refusal: ControllerFieldRefused { refusal: refusal } } + DecimalFieldRead { value: setpoint } => + match decimal_field(container: container, path: path, field: "failsafePercent") { + DecimalFieldRefused { refusal } => + ThermalControllerRefused { refusal: ControllerFieldRefused { refusal: refusal } } + DecimalFieldRead { value: failsafe } => + match decimal_field(container: pid, path: pid_path, field: "samplePeriod") { + DecimalFieldRefused { refusal } => + ThermalControllerRefused { refusal: ControllerFieldRefused { refusal: refusal } } + DecimalFieldRead { value: sample_period } => + match decimal_field(container: pid, path: pid_path, field: "positiveHysteresis") { + DecimalFieldRefused { refusal } => + ThermalControllerRefused { refusal: ControllerFieldRefused { refusal: refusal } } + DecimalFieldRead { value: positive } => + match decimal_field(container: pid, path: pid_path, field: "negativeHysteresis") { + DecimalFieldRefused { refusal } => + ThermalControllerRefused { refusal: ControllerFieldRefused { refusal: refusal } } + DecimalFieldRead { value: negative } => + match optional_bool_field(container: pid, path: pid_path, field: "isCeiling") { + OptionalBoolRefused { refusal } => + ThermalControllerRefused { refusal: ControllerFieldRefused { refusal: refusal } } + OptionalBoolUnstated => + ThermalControllerRefused { + refusal: ControllerFieldRefused { + refusal: FieldAbsent { path: pid_path, field: "isCeiling" }, + }, + } + OptionalBoolRead { value: is_ceiling } => + match decode_curve(container: pid, path: pid_path) { + CurveRefused { refusal } => + ThermalControllerRefused { refusal: ControllerCurveRefused { refusal: refusal } } + CurveDecoded { points } => + ThermalControllerDecoded { + controller: ThermalDemandController { + name: name, + inputs: inputs, + setpoint: decimal_celsius(value: setpoint), + failsafe_output: zone_demand_value(value: failsafe), + sample_period: decimal_seconds(value: sample_period), + positive_hysteresis: decimal_celsius_delta(value: positive), + negative_hysteresis: decimal_celsius_delta(value: negative), + is_ceiling: is_ceiling, + curve: points, + }, + entry_partition: object_partition( + path: path, + container: container, + consumed: thermal_controller_consumed_keys, + ), + pid_partition: object_partition( + path: pid_path, + container: pid, + consumed: thermal_pid_consumed_keys, + ), + } + } + } + } + } + } + } + } + } +} + +data actuator_controller_consumed_keys: List = [ + "name", + "type", + "inputs", + "setpoint", + "pid", +] + +data actuator_pid_consumed_keys: List = [ + "samplePeriod", + "proportionalCoeff", + "integralCoeff", + "derivativeCoeff", + "feedFwdGainCoeff", + "feedFwdOffsetCoeff", + "integralLimit_min", + "integralLimit_max", + "outLim_min", + "outLim_max", + "slewNeg", + "slewPos", +] + +type ActuatorControllerDecode + = ActuatorControllerDecoded { + controller: ActuatorController, + entry_partition: ObjectMemberPartition, + pid_partition: ObjectMemberPartition, + } + | ActuatorControllerRefused { refusal: ControllerRefusal } + +// TWELVE COEFFICIENTS READ IN GROUPS, WHICH IS WHY THE MODEL GROUPS THEM. Read as one flat +// sequence this would be a twelve-deep nesting; read as five small records it is five shallow +// ones, and each group is the concept its fields belong to rather than an arbitrary chunking -- +// the gains, the feed-forward pair, the two limit pairs, the slew pair. +type DecimalTriple + = DecimalTripleRead { first: ExactDecimal, second: ExactDecimal, third: ExactDecimal } + | DecimalTripleRefused { refusal: FieldRefusal } + +fn decimal_triple( + container: JsonValue, + path: DocumentPath, + first: NonEmptyStr, + second: NonEmptyStr, + third: NonEmptyStr, +) -> DecimalTriple { + match decimal_field(container: container, path: path, field: first) { + DecimalFieldRefused { refusal } => DecimalTripleRefused { refusal: refusal } + DecimalFieldRead { value: a } => + match decimal_field(container: container, path: path, field: second) { + DecimalFieldRefused { refusal } => DecimalTripleRefused { refusal: refusal } + DecimalFieldRead { value: b } => + match decimal_field(container: container, path: path, field: third) { + DecimalFieldRefused { refusal } => DecimalTripleRefused { refusal: refusal } + DecimalFieldRead { value: c } => + DecimalTripleRead { first: a, second: b, third: c } + } + } + } +} + +type DecimalPair + = DecimalPairRead { first: ExactDecimal, second: ExactDecimal } + | DecimalPairRefused { refusal: FieldRefusal } + +fn decimal_pair( + container: JsonValue, + path: DocumentPath, + first: NonEmptyStr, + second: NonEmptyStr, +) -> DecimalPair { + match decimal_field(container: container, path: path, field: first) { + DecimalFieldRefused { refusal } => DecimalPairRefused { refusal: refusal } + DecimalFieldRead { value: a } => + match decimal_field(container: container, path: path, field: second) { + DecimalFieldRefused { refusal } => DecimalPairRefused { refusal: refusal } + DecimalFieldRead { value: b } => DecimalPairRead { first: a, second: b } + } + } +} + +fn decode_actuator_controller( + container: JsonValue, + path: DocumentPath, + name: NonEmptyStr, + inputs: List, +) -> ActuatorControllerDecode { + let pid_path = path_field(parent: path, field: "pid") + match select_member(container: container, path: path, field: "pid") { + MemberSelectionRefused { refusal } => + ActuatorControllerRefused { refusal: ControllerFieldRefused { refusal: refusal } } + MemberSelected { value: pid } => + match decimal_field(container: container, path: path, field: "setpoint") { + DecimalFieldRefused { refusal } => + ActuatorControllerRefused { refusal: ControllerFieldRefused { refusal: refusal } } + DecimalFieldRead { value: setpoint } => + match decimal_field(container: pid, path: pid_path, field: "samplePeriod") { + DecimalFieldRefused { refusal } => + ActuatorControllerRefused { refusal: ControllerFieldRefused { refusal: refusal } } + DecimalFieldRead { value: sample_period } => + match decimal_triple( + container: pid, + path: pid_path, + first: "proportionalCoeff", + second: "integralCoeff", + third: "derivativeCoeff", + ) { + DecimalTripleRefused { refusal } => + ActuatorControllerRefused { refusal: ControllerFieldRefused { refusal: refusal } } + DecimalTripleRead { first: p, second: i, third: d } => + match decimal_pair(container: pid, path: pid_path, first: "feedFwdGainCoeff", second: "feedFwdOffsetCoeff") { + DecimalPairRefused { refusal } => + ActuatorControllerRefused { refusal: ControllerFieldRefused { refusal: refusal } } + DecimalPairRead { first: ff_gain, second: ff_offset } => + match decimal_pair(container: pid, path: pid_path, first: "integralLimit_min", second: "integralLimit_max") { + DecimalPairRefused { refusal } => + ActuatorControllerRefused { refusal: ControllerFieldRefused { refusal: refusal } } + DecimalPairRead { first: i_min, second: i_max } => + match decimal_pair(container: pid, path: pid_path, first: "outLim_min", second: "outLim_max") { + DecimalPairRefused { refusal } => + ActuatorControllerRefused { refusal: ControllerFieldRefused { refusal: refusal } } + DecimalPairRead { first: out_min, second: out_max } => + match decimal_pair(container: pid, path: pid_path, first: "slewNeg", second: "slewPos") { + DecimalPairRefused { refusal } => + ActuatorControllerRefused { refusal: ControllerFieldRefused { refusal: refusal } } + DecimalPairRead { first: slew_neg, second: slew_pos } => + ActuatorControllerDecoded { + controller: ActuatorController { + name: name, + inputs: inputs, + configured_setpoint_unused_by_runtime: setpoint, + sample_period: decimal_seconds(value: sample_period), + gains: PidGains { + proportional: p, + integral: i, + derivative: d, + }, + feed_forward: FeedForward { + gain: ff_gain, + offset: zone_demand_value(value: ff_offset), + }, + integral_limits: IntegralBounds { + minimum: i_min, + maximum: i_max, + }, + output_limits: OutputBounds { + minimum: zone_demand_value(value: out_min), + maximum: zone_demand_value(value: out_max), + }, + slew: SlewLimits { + negative_coefficient: slew_neg, + positive_coefficient: slew_pos, + }, + }, + entry_partition: object_partition( + path: path, + container: container, + consumed: actuator_controller_consumed_keys, + ), + pid_partition: object_partition( + path: pid_path, + container: pid, + consumed: actuator_pid_consumed_keys, + ), + } + } + } + } + } + } + } + } + } +} + +// A ZONE ID IS A CARDINAL, NOT A MAGNITUDE, so a document writing it as 0.5 is refused rather than +// truncated. The canonical form makes the test exact: after reduction an integral value has no +// fraction digits left, so `0`, `0.0` and `0.000` all pass and nothing that is not a whole number +// does. +type IntegerFromDecimal + = IntegerRead { value: Int } + | IntegerNotIntegral + +fn integer_from_decimal(d: ExactDecimal) -> IntegerFromDecimal { + let c = canonical_exact_decimal(d: d) + if c.fraction_digits == 0 { + IntegerRead { value: c.units } + } else { + IntegerNotIntegral + } +} + +type ProgramRefusal + = ProgramFieldRefused { refusal: FieldRefusal } + | ProgramControllerRefused { refusal: ControllerRefusal } + | ProgramSensorRefused { refusal: FieldRefusal } + +// THE ACCUMULATOR CARRIES THE PARTITIONS ALONGSIDE THE VALUES, so that a decode which succeeds on +// every field but silently skipped an object still has an incomplete partition list -- the +// conservation join is over what the decode ACTUALLY visited, not over what it was supposed to. +type ZoneAccumulation + = ZoneAccumulated { + thermal: List, + actuators: List, + partitions: List, + element_partitions: List, + elements: List, + } + | ZoneAccumulationRefused { refusal: ProgramRefusal } + +data zone_consumed_keys: List = [ + "id", + "minThermalOutput", + "failsafePercent", + "cycleIntervalTimeMS", + "updateThermalsTimeMS", + "pids", +] + +fn accumulate_controller( + state: ZoneAccumulation, + occurrence: JsonArrayElementOccurrence, + path: DocumentPath, +) -> ZoneAccumulation { + let entry = occurrence.element + match state { + ZoneAccumulationRefused { refusal } => ZoneAccumulationRefused { refusal: refusal } + ZoneAccumulated { thermal, actuators, partitions, element_partitions, elements } => + match string_field(container: entry, path: path, field: "name") { + StringFieldRefused { refusal } => + ZoneAccumulationRefused { refusal: ProgramFieldRefused { refusal: refusal } } + StringFieldRead { value: name } => + match string_list_field(container: entry, path: path, field: "inputs") { + StringListRefused { refusal } => + ZoneAccumulationRefused { refusal: ProgramFieldRefused { refusal: refusal } } + StringListRead { values: inputs } => + match string_field(container: entry, path: path, field: "type") { + StringFieldRefused { refusal } => + ZoneAccumulationRefused { refusal: ProgramFieldRefused { refusal: refusal } } + StringFieldRead { value: kind_text } => + match controller_kind(value: kind_text) { + ControllerKindUnknown => + ZoneAccumulationRefused { + refusal: ProgramControllerRefused { + refusal: ControllerKindNotRecognised { path: path, value: kind_text }, + }, + } + ControllerKindKnown { kind } => + match kind { + ThermalDemandKind => + match decode_thermal_controller(container: entry, path: path, name: name, inputs: inputs) { + ThermalControllerRefused { refusal } => + ZoneAccumulationRefused { refusal: ProgramControllerRefused { refusal: refusal } } + ThermalControllerDecoded { controller, entry_partition, pid_partition } => + ZoneAccumulated { + thermal: thermal.append(controller), + actuators: actuators, + partitions: partitions.append(entry_partition).append(pid_partition), + element_partitions: element_partitions.append( + inputs_element_partition(entry: entry, path: path), + ), + elements: elements.append( + ElementConsumed { occurrence: occurrence, role: "thermal_demand_controller" }, + ), + } + } + ActuatorKind => + match decode_actuator_controller(container: entry, path: path, name: name, inputs: inputs) { + ActuatorControllerRefused { refusal } => + ZoneAccumulationRefused { refusal: ProgramControllerRefused { refusal: refusal } } + ActuatorControllerDecoded { controller, entry_partition, pid_partition } => + ZoneAccumulated { + thermal: thermal, + actuators: actuators.append(controller), + partitions: partitions.append(entry_partition).append(pid_partition), + element_partitions: element_partitions.append( + inputs_element_partition(entry: entry, path: path), + ), + elements: elements.append( + ElementConsumed { occurrence: occurrence, role: "actuator_controller" }, + ), + } + } + } + } + } + } + } + } +} + +type ZoneDecode + = ZoneDecoded { + zone: ProgramZone, + partitions: List, + element_partitions: List, + } + | ZoneRefused { refusal: ProgramRefusal } + +// A CONTROLLER'S `inputs` ARRAY IS A POPULATION TOO, and every element of it is consumed by the +// controller that names it. Without this partition a decoder could read two of a three-endpoint +// actuator's inputs and conserve every object member perfectly -- the CHASSIS controller drives +// three fans, and dropping one is precisely the wiring error this whole lane started from. +fn inputs_element_partition(entry: JsonValue, path: DocumentPath) -> ArrayElementPartition { + let inputs_path = path_field(parent: path, field: "inputs") + let elements = match select_member(container: entry, path: path, field: "inputs") { + MemberSelected { value: v } => + match v { + JsonArray { elements: xs } => xs + other => [] + } + MemberSelectionRefused { refusal } => [] + } + let occurrences = array_element_occurrences(array_path: inputs_path.text, elements: elements) + ArrayElementPartition { + array_path: inputs_path.text, + source: occurrences, + dispositions: map(occurrences, occurrence => + ElementConsumed { occurrence: occurrence, role: "controller_input" }), + } +} + +fn decode_zone_controllers(entries: List, path: DocumentPath) -> ZoneAccumulation { + fold( + array_element_occurrences(array_path: path.text, elements: entries), + init: ZoneAccumulated { + thermal: [], + actuators: [], + partitions: [], + element_partitions: [], + elements: [], + }, + f: (state, occurrence) => + accumulate_controller( + state: state, + occurrence: occurrence, + path: path_index(parent: path, index: occurrence.identity.index), + ), + ) +} + +fn decode_zone(container: JsonValue, path: DocumentPath) -> ZoneDecode { + match decimal_field(container: container, path: path, field: "id") { + DecimalFieldRefused { refusal } => ZoneRefused { refusal: ProgramFieldRefused { refusal: refusal } } + DecimalFieldRead { value: id_decimal } => + match integer_from_decimal(d: id_decimal) { + IntegerNotIntegral => + ZoneRefused { + refusal: ProgramFieldRefused { refusal: FieldNotAnInteger { path: path, field: "id" } }, + } + IntegerRead { value: id } => + match decimal_field(container: container, path: path, field: "minThermalOutput") { + DecimalFieldRefused { refusal } => ZoneRefused { refusal: ProgramFieldRefused { refusal: refusal } } + DecimalFieldRead { value: minimum } => + match decimal_field(container: container, path: path, field: "failsafePercent") { + DecimalFieldRefused { refusal } => ZoneRefused { refusal: ProgramFieldRefused { refusal: refusal } } + DecimalFieldRead { value: failsafe } => + match decimal_pair(container: container, path: path, first: "cycleIntervalTimeMS", second: "updateThermalsTimeMS") { + DecimalPairRefused { refusal } => ZoneRefused { refusal: ProgramFieldRefused { refusal: refusal } } + DecimalPairRead { first: cycle_ms, second: update_ms } => + match select_member(container: container, path: path, field: "pids") { + MemberSelectionRefused { refusal } => + ZoneRefused { refusal: ProgramFieldRefused { refusal: refusal } } + MemberSelected { value: pids } => + match pids { + JsonArray { elements: elements_of_pids } => + match decode_zone_controllers( + entries: elements_of_pids, + path: path_field(parent: path, field: "pids"), + ) { + ZoneAccumulationRefused { refusal } => ZoneRefused { refusal: refusal } + ZoneAccumulated { thermal, actuators, partitions, element_partitions, elements } => + ZoneDecoded { + zone: ProgramZone { + id: id, + minimum_thermal_output: zone_demand_value(value: minimum), + failsafe_output: zone_demand_value(value: failsafe), + cycle_interval: decimal_milliseconds(value: cycle_ms), + update_thermals_interval: decimal_milliseconds(value: update_ms), + thermal_demand_controllers: thermal, + actuator_controllers: actuators, + }, + partitions: partitions.append( + object_partition(path: path, container: container, consumed: zone_consumed_keys), + ), + element_partitions: element_partitions.append( + ArrayElementPartition { + array_path: path_field(parent: path, field: "pids").text, + source: array_element_occurrences( + array_path: path_field(parent: path, field: "pids").text, + elements: elements_of_pids, + ), + dispositions: elements, + }, + ), + } + } + other => + ZoneRefused { + refusal: ProgramFieldRefused { + refusal: FieldNotAnArray { path: path, field: "pids" }, + }, + } + } + } + } + } + } + } + } +} + +data document_consumed_keys: List = ["sensors", "zones"] + +type ProgramDecode + = ProgramDecoded { + program: BmcFanControlProgram, + partitions: List, + element_partitions: List, + } + | ProgramDecodeRefused { refusal: ProgramRefusal } + | ProgramMembersNotConserved { verdict: ConservationVerdict } + +type SensorAccumulation + = SensorsAccumulated { + sensors: List, + partitions: List, + elements: List, + } + | SensorsAccumulationRefused { refusal: FieldRefusal } + +fn accumulate_sensor( + state: SensorAccumulation, + occurrence: JsonArrayElementOccurrence, + path: DocumentPath, +) -> SensorAccumulation { + match state { + SensorsAccumulationRefused { refusal } => SensorsAccumulationRefused { refusal: refusal } + SensorsAccumulated { sensors, partitions, elements } => + match decode_sensor(container: occurrence.element, path: path) { + SensorRefused { refusal } => SensorsAccumulationRefused { refusal: refusal } + SensorDecoded { sensor, partition } => + SensorsAccumulated { + sensors: sensors.append(sensor), + partitions: partitions.append(partition), + elements: elements.append(ElementConsumed { occurrence: occurrence, role: "sensor" }), + } + } + } +} + +fn decode_sensors(entries: List, path: DocumentPath) -> SensorAccumulation { + fold( + array_element_occurrences(array_path: path.text, elements: entries), + init: SensorsAccumulated { sensors: [], partitions: [], elements: [] }, + f: (state, occurrence) => + accumulate_sensor( + state: state, + occurrence: occurrence, + path: path_index(parent: path, index: occurrence.identity.index), + ), + ) +} + +type ZonesAccumulation + = ZonesAccumulated { + zones: List, + partitions: List, + element_partitions: List, + elements: List, + } + | ZonesAccumulationRefused { refusal: ProgramRefusal } + +fn accumulate_zone( + state: ZonesAccumulation, + occurrence: JsonArrayElementOccurrence, + path: DocumentPath, +) -> ZonesAccumulation { + match state { + ZonesAccumulationRefused { refusal } => ZonesAccumulationRefused { refusal: refusal } + ZonesAccumulated { zones, partitions, element_partitions, elements } => + match decode_zone(container: occurrence.element, path: path) { + ZoneRefused { refusal } => ZonesAccumulationRefused { refusal: refusal } + ZoneDecoded { zone, partitions: zone_partitions, element_partitions: zone_elements } => + ZonesAccumulated { + zones: zones.append(zone), + partitions: flat_map([partitions, zone_partitions], group => group), + element_partitions: flat_map([element_partitions, zone_elements], group => group), + elements: elements.append(ElementConsumed { occurrence: occurrence, role: "zone" }), + } + } + } +} + +fn decode_zones(entries: List, path: DocumentPath) -> ZonesAccumulation { + fold( + array_element_occurrences(array_path: path.text, elements: entries), + init: ZonesAccumulated { zones: [], partitions: [], element_partitions: [], elements: [] }, + f: (state, occurrence) => + accumulate_zone( + state: state, + occurrence: occurrence, + path: path_index(parent: path, index: occurrence.identity.index), + ), + ) +} + +// THE FIRST PARTITION THAT DOES NOT CONSERVE STOPS THE DECODE, AND THE VERDICT IS CARRIED OUT +// WHOLE. It is a separate outcome from a field refusal because it means something different: a +// field refusal says the document is wrong, and a conservation failure says THIS DECODER is wrong +// -- it read a member twice, or left one unaccounted, or dispositioned one that was not there. +// Reporting the second as the first would send a reader to edit a configuration that is fine. +fn unconserved(verdicts: List) -> List { + filter( + verdicts, + verdict => + match verdict { + MembersConserved { member_count: _ } => false + other => true + }, + ) +} + +fn first_unconserved(partitions: List) -> List { + unconserved(verdicts: map(partitions, partition => conservation_verdict(partition: partition))) +} + +fn first_unconserved_array(partitions: List) -> List { + unconserved(verdicts: map(partitions, partition => element_conservation_verdict(partition: partition))) +} + +fn decode_program(document: JsonValue) -> ProgramDecode { + let root = document_path(text: "$") + match select_member(container: document, path: root, field: "sensors") { + MemberSelectionRefused { refusal } => ProgramDecodeRefused { refusal: ProgramFieldRefused { refusal: refusal } } + MemberSelected { value: sensors_value } => + match sensors_value { + JsonArray { elements: sensor_entries } => + match select_member(container: document, path: root, field: "zones") { + MemberSelectionRefused { refusal } => + ProgramDecodeRefused { refusal: ProgramFieldRefused { refusal: refusal } } + MemberSelected { value: zones_value } => + match zones_value { + JsonArray { elements: zone_entries } => + match decode_sensors(entries: sensor_entries, path: path_field(parent: root, field: "sensors")) { + SensorsAccumulationRefused { refusal } => + ProgramDecodeRefused { refusal: ProgramSensorRefused { refusal: refusal } } + SensorsAccumulated { sensors, partitions: sensor_partitions, elements: sensor_elements } => + match decode_zones(entries: zone_entries, path: path_field(parent: root, field: "zones")) { + ZonesAccumulationRefused { refusal } => ProgramDecodeRefused { refusal: refusal } + ZonesAccumulated { zones, partitions: zone_partitions, element_partitions: zone_element_partitions, elements: zone_elements } => { + let partitions = flat_map( + [ + sensor_partitions, + zone_partitions, + [object_partition(path: root, container: document, consumed: document_consumed_keys)], + ], + group => group, + ) + let element_partitions = flat_map( + [ + zone_element_partitions, + [ + ArrayElementPartition { + array_path: path_field(parent: root, field: "sensors").text, + source: array_element_occurrences( + array_path: path_field(parent: root, field: "sensors").text, + elements: sensor_entries, + ), + dispositions: sensor_elements, + }, + ArrayElementPartition { + array_path: path_field(parent: root, field: "zones").text, + source: array_element_occurrences( + array_path: path_field(parent: root, field: "zones").text, + elements: zone_entries, + ), + dispositions: zone_elements, + }, + ], + ], + group => group, + ) + let broken = first_unconserved(partitions: partitions) + let broken_arrays = first_unconserved_array(partitions: element_partitions) + if broken.length() > 0 { + ProgramMembersNotConserved { verdict: broken.first() } + } else if broken_arrays.length() > 0 { + ProgramMembersNotConserved { verdict: broken_arrays.first() } + } else { + ProgramDecoded { + program: BmcFanControlProgram { sensors: sensors, zones: zones }, + partitions: partitions, + element_partitions: element_partitions, + } + } + } + } + } + other => + ProgramDecodeRefused { + refusal: ProgramFieldRefused { refusal: FieldNotAnArray { path: root, field: "zones" } }, + } + } + } + other => + ProgramDecodeRefused { + refusal: ProgramFieldRefused { refusal: FieldNotAnArray { path: root, field: "sensors" } }, + } + } + } +} diff --git a/dag/extdeps/bmc/pid_control_program.dag b/dag/extdeps/bmc/pid_control_program.dag new file mode 100644 index 00000000000..19371affb97 --- /dev/null +++ b/dag/extdeps/bmc/pid_control_program.dag @@ -0,0 +1,317 @@ +module extdeps.bmc.pid_control_program + +import std.types { Bool, Int, List, NonEmptyStr, String } +import std.decimal { ExactDecimal, exact_decimal_equal } +import std.measure { Measure, Milli, One, Temperature, TemperatureDifference, Time } +import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef } +import std.decl_ref { DeclarationRef, WholeDeclaration } +import extdeps.uri { Https, Uri } + +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https, + locator: "github.com/openbmc/phosphor-pid-control/blob/master/README.md", + }, +} + +// THE SUBJECT IS THE OpenBMC STACK ITSELF, CITED THROUGH THE DECLARATION THAT ALREADY EXISTS +// RATHER THAN RESTATED. phosphor-pid-control is a component of that stack, versioned with it and +// deployed with it; giving it a second subject marker would mint a nickname for a subject this +// tree already names. +data extdeps_model_scope: ExternalModelScope = ExternalModelScope { + subject: ExternalSubjectRef { + declaration: DeclarationRef { + module_path: "extdeps.firmware.openbmc.subject", + decl_name: "openbmc_stack", + field: WholeDeclaration, + }, + }, + first_citation: extdeps_external_authority_anchor, + further_citations: [], +} + +// THE COMPLETE SHAPE OF A phosphor-pid-control ZONE CONFIGURATION, MODELLED ONCE AND USED FROM +// BOTH DIRECTIONS. An observation decodes a captured document onto it; an intent authors one; a +// convergence compares the two. It is deliberately independent of the producer -- nothing here +// mentions JSON, a file, a host or a transport -- because the moment the model knows how it was +// obtained, the intent side has to either borrow that vocabulary or fork the model, and a forked +// model is two answers to "what program is running". +// +// WHAT THIS DEPLOYMENT ACTUALLY DOES, WHICH THE FIELD LAYOUT ENCODES RATHER THAN ANNOTATES, AND +// WHICH IS NOT A LAW OF THE SCHEMA. Upstream zones may combine several thermal-controller outputs +// and select among them, so the model carries LISTS on both sides and the captured artifacts +// simply inhabit one-demand-two-actuators. An earlier revision of this paragraph stated the +// one-demand shape as what the hardware does, which read as a schema constraint. The deployment +// runs ONE thermal demand controller -- a stepwise curve turning a temperature into a demand -- +// whose single output feeds MULTIPLE actuator controllers, each with its own transfer function +// from that one demand to its own fans. The deployed program is exactly this: TEMP_SOC produces a +// demand, and FAN1 and CHASSIS translate that same demand differently (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, which makes the two actuators look +// independently adjustable when moving the shared demand moves both. + +// EVERY MAGNITUDE IS EXACT AND DECIMAL, AND IS SPELLED AS std.measure's OWN TYPE AT EVERY USE +// SITE RATHER THAN BEHIND A LOCAL ALIAS. Five aliases stood here (DecimalCelsius, DecimalSeconds +// and friends); review 56966 ruled them parallel Measure aliases minted outside the canonical +// authority, which is the re-minted-shared-concept rule, and it is right -- an alias is a second +// name for a type std.measure already expresses, and a second name is what §3 forbids however +// convenient it reads. +// +// THE RULING OFFERED TWO REMEDIES AND THE OTHER ONE WAS MEASURED BEFORE THIS ONE WAS CHOSEN. +// Hosting the ExactDecimal-parameterised aliases in std/measure.dag was 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: it exists only because +// std.decimal imports std.bytes for the divergent seam its negative-scale arm uses, and inlining +// `1 / 0` there breaks it (also measured). It was not taken, because std.bytes' own note records +// that seam as ONE seam projected per result type and marks the pair as a deliberate duplication +// to be dissolved -- adding a third copy to widen an alias family would trade a naming defect for +// a worse one in a load-bearing file. Writing the type out costs nothing but characters. +// +// THE CARRIER DECISION ITSELF IS UNCHANGED AND HAS A MEASUREMENT BEHIND IT. +// std.measure's Percent and Celsius pin their magnitude to Nat and Int, and the deployed document +// carries -8.0, -0.5, -3.0 and 0.005 -- values a Nat cannot hold and an Int cannot hold exactly. +// So the QUANTITY authority is reused unchanged and only the magnitude parameter differs: these +// are std.measure's own quantities at std.measure's own scale, over a magnitude that can carry +// what the document carries. Minting a fresh temperature or ratio type here would have been the +// §3 nicknaming violation; changing M is what the type parameter is for. +// THE ZONE'S OUTPUT UNITS ARE NOT UNIVERSALLY PERCENT, so they are carried as their own named +// value rather than as a dimensionless percentage. 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 +// happens to run on a PWM-like scale, but a model that hard-coded percent would be asserting a +// unit the schema does not fix. Everything measured in those units -- the curve's output, the +// zone's minimum and failsafe, an actuator's output limits and feed-forward offset -- shares this +// one carrier, so a value from one cannot be silently compared against a temperature or a gain. +type ZoneDemandValue { + magnitude: ExactDecimal +} + +fn decimal_celsius(value: ExactDecimal) -> Measure { + Measure { count: value } +} + +fn decimal_celsius_delta(value: ExactDecimal) -> Measure { + Measure { count: value } +} + +fn zone_demand_value(value: ExactDecimal) -> ZoneDemandValue { + ZoneDemandValue { magnitude: value } +} + +fn decimal_seconds(value: ExactDecimal) -> Measure { + Measure { count: value } +} + +// THE ZONE'S TWO INTERVALS CARRY THEIR SCALE IN THE TYPE RATHER THAN IN THE FIELD NAME. The +// document's keys end in MS and an earlier revision let that suffix be the only record of the +// unit, which puts a magnitude's scale in a string. +fn decimal_milliseconds(value: ExactDecimal) -> Measure { + Measure { count: value } +} + +// A SENSOR'S ROLE DECIDES WHAT ITS READING MEANS, and the two roles this schema admits are not +// interchangeable: a fan sensor's reading is a tachometer speed and a temp sensor's is a +// temperature. They are named rather than carried as the document's `type` string so that a third +// role appearing upstream breaks every reader instead of silently reading as neither. +type ProgramSensorRole = FanTachometerSensor | TemperatureSensor + +// WRITABILITY IS A PROPERTY OF THE SENSOR, NOT AN OPTIONAL FIELD. A temp sensor has no writePath +// because there is nothing to drive; a fan sensor has one because that is where duty is written. +// Modelling this as an absent string would let a fan sensor with no write path read as an ordinary +// sensor rather than as an actuator that cannot actuate. +type ProgramSensorActuation + = SensorDrivesOutput { write_path: NonEmptyStr } + | SensorReadOnly + +// THREE STATES, NOT TWO, AND THE THIRD IS THE ONE THAT COST US. `ignoreDbusMinMax` is absent on at +// least one captured sensor entry, and absent is not false: false asserts that the D-Bus bounds +// are to be used, while absent says the document did not decide and the daemon's default applies. +// Collapsing absent into false would have this model assert a policy the document never states -- +// and the two have different repairs, since one is a program to change and the other is a program +// to complete. +type DbusBoundsDisposition + = DbusBoundsIgnored + | DbusBoundsUsed + | DbusBoundsUnstated + +type SensorReadingBounds + = SensorBoundsDeclared { minimum: ExactDecimal, maximum: ExactDecimal } + | SensorBoundsUnstated + +type SensorTimeout + = SensorTimeoutDeclared { seconds: Measure } + | SensorTimeoutUnstated + +type ProgramSensor { + name: NonEmptyStr + role: ProgramSensorRole + read_path: NonEmptyStr + actuation: ProgramSensorActuation + bounds: SensorReadingBounds + dbus_bounds: DbusBoundsDisposition + timeout: SensorTimeout +} + +// A CURVE POINT CARRIES BOTH HALVES, WHICH IS THE WHOLE REASON IT IS A TYPE. The document stores +// the curve as two objects keyed "0".."8" -- one of readings, one of outputs -- so a reading whose +// output key is missing is expressible in the document and is a real defect. Here it is not +// expressible at all: there is no way to build a point with a reading and no output. That moves +// the class from something a decoder must remember to check to something it cannot produce, and +// leaves the decoder responsible only for REFUSING the malformed document rather than for +// preserving a distinction it might drop. +// +// The index is retained because the document's keys carry it and dropping it would lose the join +// back to the source -- but it is not what pairs the halves; the pairing already happened. +type DemandCurvePoint { + index: Int + reading: Measure + output: ZoneDemandValue +} + +// HYSTERESIS IS A TEMPERATURE DIFFERENCE AND THE SETPOINT IS A TEMPERATURE, which are different +// quantities in std.measure and are kept different here. The document writes both as bare numbers. +type ThermalDemandController { + name: NonEmptyStr + inputs: List + setpoint: Measure + failsafe_output: ZoneDemandValue + sample_period: Measure + positive_hysteresis: Measure + negative_hysteresis: Measure + is_ceiling: Bool + curve: List +} + +// THE COEFFICIENTS ARE EXACT SCALARS AND ARE NOT TYPED AS RATIOS, because their dimensions depend +// on the controller's input and output and this model spans more than one such controller. For a +// fan controller producing PWM from a tachometer reading, a proportional gain is percent per RPM +// and an integral gain is percent per RPM-second -- neither is dimensionless, and calling them +// ratios asserted an algebra that would be wrong for the very controllers here. Lane S's +// obligation is exact observation and comparison, which needs no dimension at all; a later +// behaviour model can parameterise them by the controller's actual input and output quantities. +type PidGains { + proportional: ExactDecimal + integral: ExactDecimal + derivative: ExactDecimal +} + +// THE FEED-FORWARD PAIR IS WHAT MAKES THIS PROGRAM QUIET, so it is named as its own concept rather +// than left as two more coefficients in a flat list. With all three gains at zero the actuator's +// behaviour is feed-forward alone, clamped and slew-limited -- the offset is not a trim on a +// feedback loop, it IS the transfer function, and it is where the difference between the two +// deployed actuators lives. +// +// NO FORMULA IS STATED HERE, AND THE OMISSION IS DELIBERATE. An earlier revision wrote +// `output = demand * gain + offset`; review reported the runtime computes `(setpoint + offset) * +// gain`. At the deployed gain of 1.0 the two agree exactly, so neither the captured documents nor +// anything in this lane can distinguish them -- which is how the wrong one survived being written +// down. Nobody who wrote this file has read that runtime, so rather than replace one unverified +// formula with another, this model states the fields and not the arithmetic. NEXT-RUNG TRIGGER: +// read the cited runtime, then record the equation with its citation. Nothing in Lane S depends on +// it: exact observation and comparison need the coefficients, not their composition. +type FeedForward { + gain: ExactDecimal + offset: ZoneDemandValue +} + +type OutputBounds { + minimum: ZoneDemandValue + maximum: ZoneDemandValue +} + +type IntegralBounds { + minimum: ExactDecimal + maximum: ExactDecimal +} + +// SLEW IS A RATE AND THIS MODEL DOES NOT CLAIM ITS DENOMINATOR. An earlier revision named these +// fields per-sample and typed them as a percentage; review reported that the runtime multiplies +// the coefficient by the elapsed sample TIME, which makes the denominator a duration rather than a +// sample. The deployed samplePeriod is 1.0, so percent-per-second and percent-per-sample are +// numerically identical here and neither the documents nor this lane can tell them apart -- which +// is exactly why the wrong name survived. Nobody who wrote this file has read that runtime, so the +// fields are named for what they are in the document and carry no denominator. NEXT-RUNG TRIGGER: +// read the cited runtime, then give these a rate carrier naming its denominator. +// +// The negative limit keeps its sign rather than being normalised to a magnitude: a positive +// slewNeg is a different program, not the same one written differently, and normalising here would +// make the two compare equal. +type SlewLimits { + negative_coefficient: ExactDecimal + positive_coefficient: ExactDecimal +} + +// THE ACTUATOR'S CONFIGURED SETPOINT IS PRESERVED WITHOUT BEING GIVEN OPERATIVE MEANING. It is in +// the bytes, so an observation that dropped it would not conserve; but review reports that the +// upstream builder does not pass this field to the fan controller it constructs, while thermal and +// stepwise controllers do receive theirs. An earlier revision typed it as a demand value and +// annotated it as the zone's demand units, which asserted an operative role for a field that may +// have none. It is carried as the configured scalar it is, named so that no reader mistakes it for +// a live setpoint, and no unit is claimed for it. +type ActuatorController { + name: NonEmptyStr + inputs: List + configured_setpoint_unused_by_runtime: ExactDecimal + sample_period: Measure + gains: PidGains + feed_forward: FeedForward + integral_limits: IntegralBounds + output_limits: OutputBounds + slew: SlewLimits +} + +// THE TWO CONTROLLER LISTS ARE SEPARATE FIELDS, WHICH IS THE STRUCTURAL CLAIM THIS MODEL MAKES. +// The document carries them as one heterogeneous array discriminated by a `type` string, so a +// reader over the document has to decide what each entry is at every use. Here the decision +// happens once, at the decode, and everything downstream reads a list whose element type already +// answers it -- an actuator cannot appear where a demand controller is expected. +type ProgramZone { + id: Int + minimum_thermal_output: ZoneDemandValue + failsafe_output: ZoneDemandValue + cycle_interval: Measure + update_thermals_interval: Measure + thermal_demand_controllers: List + actuator_controllers: List +} + +type BmcFanControlProgram { + sensors: List + zones: List +} + +// RELATION TO THE PARTIAL AUTHORITY THAT ALREADY EXISTS, DECLARED RATHER THAN LEFT FOR A REVIEWER +// TO FIND. extdeps.bmc.openbmc_fan_control OpenBmcStepwiseController models a subset of this same +// upstream concept, and two authorities for one fact is what DESIGN §3 forbids -- so the relation +// is stated with its cutover rather than the two being left to drift. +// +// WHAT THAT ONE CANNOT REPRESENT, measured against the captured documents rather than asserted: +// its magnitudes are Percent (Nat) and Celsius (Int), so the deployed -8.0, -3.0, -0.5 and 0.005 +// have no spelling in it; its curve is two parallel lists (readings, outputs) rather than paired +// points, so an unpaired curve is representable; it carries no PID coefficients at all, so the +// feed-forward offset that IS the difference between the two deployed actuators is absent; and it +// mixes zone facts (minimum_duty, zone_failsafe_duty) into a controller record. +// +// WHY IT IS NOT DELETED HERE. It has an actuation consumer (extdeps.bmc.openbmc_operation), and +// actuation is a separate lane under its own operator decision -- so this is the gap-intolerant +// boundary carve-out DESIGN §3 names: the replacement is built in shadow and the cutover switches +// the root once, rather than main hosting a dual-authority interval with a half-migrated writer. +// Until then that type is FROZEN: no new fields, no new coefficients, no new callers. A change +// that would widen it is a change that belongs here instead. +data partial_prior_authority_note: String = "extdeps.bmc.openbmc_fan_control OpenBmcStepwiseController and OpenBmcFanController are a lossy subset of this model, retained because extdeps.bmc.openbmc_operation actuates through them and actuation is a separately-decided lane. Frozen: no new rows on their growth surfaces. Dissolve-on: the actuation cutover, which replaces the desired-config argument bundle with a projection of BmcFanControlProgram and deletes both types with openbmc_fan_config_desired_json." + +fn program_sensor_named(program: BmcFanControlProgram, name: NonEmptyStr) -> List { + filter(program.sensors, sensor => sensor.name == name) +} + +// AGREEMENT BETWEEN TWO PROGRAMS IS DECIDED ON VALUES, NEVER ON THE NUMERALS THEY WERE WRITTEN +// WITH, which is the entire reason the magnitude carrier is exact and canonical. srv3 writes 30.0 +// where srv4 writes 30; those are the same program and must compare as one. +fn decimal_measures_agree(a: Measure, b: Measure) -> Bool { + exact_decimal_equal(a: a.count, b: b.count) +} + +fn curve_points_agree(a: DemandCurvePoint, b: DemandCurvePoint) -> Bool { + a.index == b.index + && decimal_measures_agree(a: a.reading, b: b.reading) + && decimal_measures_agree(a: a.output, b: b.output) +} diff --git a/dag/extdeps/bmc/pid_control_representability.dag b/dag/extdeps/bmc/pid_control_representability.dag new file mode 100644 index 00000000000..47cf1665e81 --- /dev/null +++ b/dag/extdeps/bmc/pid_control_representability.dag @@ -0,0 +1,122 @@ +module extdeps.bmc.pid_control_representability + +import std.types { Bool, Int, List, NonEmptyStr, String } +import std.content_hash { ContentHash } +import extdeps.languages.json.emit { JsonValue } +import extdeps.languages.json.member_conservation { + ConservationVerdict, + JsonOccurrenceIdentity, + MemberDefective, + MemberDisposition, + MemberUnmodeled, + MemberConsumed, + ObjectMemberPartition, +} +import extdeps.bmc.pid_control_program { BmcFanControlProgram } +import extdeps.bmc.pid_control_semantic_identity { semantic_program_digest } +import extdeps.bmc.pid_control_decode { + ProgramDecode, + ProgramDecodeRefused, + ProgramDecoded, + ProgramMembersNotConserved, + ProgramRefusal, + decode_program, +} + +// THE GATE THAT STOPS A PARTIAL OBSERVATION FROM BEING CITED AS A COMPLETE PROGRAM. A decode can +// succeed while leaving members it does not model, and 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. +// +// This is why the gate exists as its own step rather than as a flag on the decode. There must be +// no interval in which a consumer can hold a decoded program and not know whether it is whole -- +// which is also why it lands in the same change as the decode rather than after it. +type RepresentabilityRefusal + = ResidueUnmodeled { identity: JsonOccurrenceIdentity, key: String, residue_count: Int } + | KnownFieldDefective { identity: JsonOccurrenceIdentity, key: String, cause: NonEmptyStr } + +// THE TWO REFUSALS ARE NOT THE SAME FINDING AT DIFFERENT SEVERITIES. Unmodelled residue means this +// repository is behind the document -- the fix is a model change here. A defective known field +// means the DOCUMENT is wrong against a field we do model -- the fix is on the host. Collapsing +// them would send half the work to the wrong place, and the residue case is the one that must not +// read as an error in the fleet's configuration. +type ProgramRepresentability + = FanProgramFullyRepresentable { program: BmcFanControlProgram, semantic_digest: ContentHash } + | FanProgramNotRepresentable { refusal: RepresentabilityRefusal } + | FanProgramNotDecoded { refusal: ProgramRefusal } + | FanProgramNotConserved { verdict: ConservationVerdict } + +fn unmodeled_of(partition: ObjectMemberPartition) -> List { + filter(partition.dispositions, disposition => + match disposition { + MemberUnmodeled { occurrence } => true + MemberConsumed { occurrence, role } => false + MemberDefective { occurrence, cause } => false + }) +} + +fn defective_of(partition: ObjectMemberPartition) -> List { + filter(partition.dispositions, disposition => + match disposition { + MemberDefective { occurrence, cause } => true + MemberConsumed { occurrence, role } => false + MemberUnmodeled { occurrence } => false + }) +} + +fn residue_refusal(dispositions: List, total: Int) -> List { + map(dispositions, disposition => + match disposition { + MemberUnmodeled { occurrence } => + ResidueUnmodeled { + identity: occurrence.identity, + key: occurrence.member.key, + residue_count: total, + } + MemberDefective { occurrence, cause } => + KnownFieldDefective { + identity: occurrence.identity, + key: occurrence.member.key, + cause: cause, + } + MemberConsumed { occurrence, role } => + ResidueUnmodeled { + identity: occurrence.identity, + key: occurrence.member.key, + residue_count: total, + } + }) +} + +// THE DEFECTIVE POPULATION IS REPORTED BEFORE THE RESIDUE, because a document that is wrong about +// a field we DO understand is the more urgent of the two and the one an operator can act on +// without waiting for this repository to model anything. +fn representability_of_partitions( + partitions: List, +) -> List { + let defective = flat_map(partitions, partition => defective_of(partition: partition)) + let unmodeled = flat_map(partitions, partition => unmodeled_of(partition: partition)) + if defective.length() > 0 { + residue_refusal(dispositions: defective, total: defective.length()) + } else { + residue_refusal(dispositions: unmodeled, total: unmodeled.length()) + } +} + +fn program_representability(document: JsonValue) -> ProgramRepresentability { + match decode_program(document: document) { + ProgramDecodeRefused { refusal } => FanProgramNotDecoded { refusal: refusal } + ProgramMembersNotConserved { verdict } => FanProgramNotConserved { verdict: verdict } + ProgramDecoded { program, partitions, element_partitions } => { + let refusals = representability_of_partitions(partitions: partitions) + if refusals.length() > 0 { + FanProgramNotRepresentable { refusal: refusals.first() } + } else { + FanProgramFullyRepresentable { + program: program, + semantic_digest: semantic_program_digest(program: program), + } + } + } + } +} diff --git a/dag/extdeps/bmc/pid_control_semantic_identity.dag b/dag/extdeps/bmc/pid_control_semantic_identity.dag new file mode 100644 index 00000000000..85423679f0b --- /dev/null +++ b/dag/extdeps/bmc/pid_control_semantic_identity.dag @@ -0,0 +1,206 @@ +module extdeps.bmc.pid_control_semantic_identity + +import std.types { Bool, Int, List, NonEmptyStr, String } +import std.decimal { ExactDecimal, exact_decimal_wire } +import std.measure { measure_count } +import std.content_hash { ContentHash, content_hash_of_value } +import extdeps.languages.json.emit { + JsonKeyValue, + JsonValue, + json_array, + json_kv, + json_object, + json_string, + serialize_json, +} +import extdeps.bmc.pid_control_program { + ActuatorController, + BmcFanControlProgram, + DbusBoundsDisposition, + DbusBoundsIgnored, + DbusBoundsUnstated, + DbusBoundsUsed, + DemandCurvePoint, + FanTachometerSensor, + ProgramSensor, + ProgramSensorRole, + ProgramZone, + SensorBoundsDeclared, + SensorBoundsUnstated, + SensorDrivesOutput, + SensorReadOnly, + SensorReadingBounds, + SensorTimeoutDeclared, + SensorTimeoutUnstated, + TemperatureSensor, + ThermalDemandController, + ZoneDemandValue, +} + +// A PROGRAM'S SEMANTIC IDENTITY: WHAT THE MACHINE RUNS, NOT WHAT SOMEBODY TYPED. Two hosts running +// the identical program must produce the identical identity even when their configuration files +// differ in every way a file can differ without the daemon noticing -- member order, whitespace, +// `30` against `30.0`. Digesting the captured bytes answers a different question, and it is a +// question already answered: the capture receipt carries the byte digest, and it is the right +// identity for "did this file change". This is the identity for "did the PROGRAM change". +// +// THE RENDERING IS THE DIGEST'S SUBJECT AND IS DEFINED HERE RATHER THAN BORROWED. It walks the +// model in a fixed field order, renders every magnitude through the exact decimal's canonical wire, +// and emits the coproduct arms as their own names -- so a field that is absent in one document and +// present-and-unstated in another render identically only if they mean the same thing. It is a +// projection of the semantic model and deliberately NOT a re-emission of the source document: it +// carries no member order, no key spellings, and no field the model does not hold. + +fn decimal_json(value: ExactDecimal) -> JsonValue { + json_string(s: exact_decimal_wire(d: value)) +} + +fn demand_json(value: ZoneDemandValue) -> JsonValue { + decimal_json(value: value.magnitude) +} + +// 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 already decided is carried exactly, +// and it would reintroduce the `30` against `30.0` question inside the very artifact built to +// settle it. The canonical wire is one spelling per value by construction. +fn sensor_role_json(role: ProgramSensorRole) -> JsonValue { + match role { + FanTachometerSensor => json_string(s: "fan_tachometer") + TemperatureSensor => json_string(s: "temperature") + } +} + +fn dbus_bounds_json(disposition: DbusBoundsDisposition) -> JsonValue { + match disposition { + DbusBoundsIgnored => json_string(s: "ignored") + DbusBoundsUsed => json_string(s: "used") + DbusBoundsUnstated => json_string(s: "unstated") + } +} + +fn sensor_bounds_json(bounds: SensorReadingBounds) -> JsonValue { + match bounds { + SensorBoundsUnstated => json_string(s: "unstated") + SensorBoundsDeclared { minimum, maximum } => + json_object(members: [ + json_kv(key: "minimum", value: decimal_json(value: minimum)), + json_kv(key: "maximum", value: decimal_json(value: maximum)), + ]) + } +} + +fn sensor_timeout_json(timeout: SensorTimeout) -> JsonValue { + match timeout { + SensorTimeoutUnstated => json_string(s: "unstated") + SensorTimeoutDeclared { seconds } => decimal_json(value: measure_count(m: seconds)) + } +} + +fn sensor_actuation_json(sensor: ProgramSensor) -> JsonValue { + match sensor.actuation { + SensorReadOnly => json_string(s: "read_only") + SensorDrivesOutput { write_path } => json_string(s: write_path) + } +} + +fn sensor_json(sensor: ProgramSensor) -> JsonValue { + json_object(members: [ + json_kv(key: "name", value: json_string(s: sensor.name as String)), + json_kv(key: "role", value: sensor_role_json(role: sensor.role)), + json_kv(key: "read_path", value: json_string(s: sensor.read_path as String)), + json_kv(key: "actuation", value: sensor_actuation_json(sensor: sensor)), + json_kv(key: "bounds", value: sensor_bounds_json(bounds: sensor.bounds)), + json_kv(key: "dbus_bounds", value: dbus_bounds_json(disposition: sensor.dbus_bounds)), + json_kv(key: "timeout", value: sensor_timeout_json(timeout: sensor.timeout)), + ]) +} + +fn curve_point_json(point: DemandCurvePoint) -> JsonValue { + json_object(members: [ + json_kv(key: "index", value: json_string(s: to_string(point.index))), + json_kv(key: "reading", value: decimal_json(value: measure_count(m: point.reading))), + json_kv(key: "output", value: demand_json(value: point.output)), + ]) +} + +fn inputs_json(inputs: List) -> JsonValue { + json_array(elements: map(inputs, input => json_string(s: input as String))) +} + +fn thermal_controller_json(controller: ThermalDemandController) -> JsonValue { + json_object(members: [ + json_kv(key: "name", value: json_string(s: controller.name as String)), + json_kv(key: "inputs", value: inputs_json(inputs: controller.inputs)), + json_kv(key: "setpoint", value: decimal_json(value: measure_count(m: controller.setpoint))), + json_kv(key: "failsafe_output", value: demand_json(value: controller.failsafe_output)), + json_kv(key: "sample_period", value: decimal_json(value: measure_count(m: controller.sample_period))), + json_kv(key: "positive_hysteresis", value: decimal_json(value: measure_count(m: controller.positive_hysteresis))), + json_kv(key: "negative_hysteresis", value: decimal_json(value: measure_count(m: controller.negative_hysteresis))), + json_kv(key: "is_ceiling", value: json_string(s: if controller.is_ceiling { "true" } else { "false" })), + json_kv(key: "curve", value: json_array(elements: map(controller.curve, point => curve_point_json(point: point)))), + ]) +} + +fn actuator_controller_json(controller: ActuatorController) -> JsonValue { + json_object(members: [ + json_kv(key: "name", value: json_string(s: controller.name as String)), + json_kv(key: "inputs", value: inputs_json(inputs: controller.inputs)), + json_kv( + key: "configured_setpoint_unused_by_runtime", + value: decimal_json(value: controller.configured_setpoint_unused_by_runtime), + ), + json_kv(key: "sample_period", value: decimal_json(value: measure_count(m: controller.sample_period))), + json_kv(key: "proportional", value: decimal_json(value: controller.gains.proportional)), + json_kv(key: "integral", value: decimal_json(value: controller.gains.integral)), + json_kv(key: "derivative", value: decimal_json(value: controller.gains.derivative)), + json_kv(key: "feed_forward_gain", value: decimal_json(value: controller.feed_forward.gain)), + json_kv(key: "feed_forward_offset", value: demand_json(value: controller.feed_forward.offset)), + json_kv(key: "integral_limit_minimum", value: decimal_json(value: controller.integral_limits.minimum)), + json_kv(key: "integral_limit_maximum", value: decimal_json(value: controller.integral_limits.maximum)), + json_kv(key: "output_limit_minimum", value: demand_json(value: controller.output_limits.minimum)), + json_kv(key: "output_limit_maximum", value: demand_json(value: controller.output_limits.maximum)), + json_kv(key: "slew_negative", value: decimal_json(value: controller.slew.negative_coefficient)), + json_kv(key: "slew_positive", value: decimal_json(value: controller.slew.positive_coefficient)), + ]) +} + +fn zone_json(zone: ProgramZone) -> JsonValue { + json_object(members: [ + json_kv(key: "id", value: json_string(s: to_string(zone.id))), + json_kv(key: "minimum_thermal_output", value: demand_json(value: zone.minimum_thermal_output)), + json_kv(key: "failsafe_output", value: demand_json(value: zone.failsafe_output)), + json_kv(key: "cycle_interval_ms", value: decimal_json(value: measure_count(m: zone.cycle_interval))), + json_kv(key: "update_thermals_ms", value: decimal_json(value: measure_count(m: zone.update_thermals_interval))), + json_kv( + key: "thermal_demand_controllers", + value: json_array(elements: map(zone.thermal_demand_controllers, c => thermal_controller_json(controller: c))), + ), + json_kv( + key: "actuator_controllers", + value: json_array(elements: map(zone.actuator_controllers, c => actuator_controller_json(controller: c))), + ), + ]) +} + +// THE PROGRAM'S OWN LISTS ARE RENDERED IN THE ORDER THE MODEL HOLDS THEM AND ARE NOT SORTED, which +// is a different decision from the curve's and rests on a different fact. A curve's positions are +// named by the document's own integer keys, so its order is recoverable and reordering the members +// cannot change it. A zone's sensor list and controller list have no such names -- the document +// gives them only array position -- so their order IS their identity as far as anything here can +// tell, and sorting them would assert an equivalence between two documents that nothing has +// established. If upstream turns out to load them order-independently, that is a fact to read and +// cite, and this is the site that changes. +fn program_json(program: BmcFanControlProgram) -> JsonValue { + json_object(members: [ + json_kv(key: "sensors", value: json_array(elements: map(program.sensors, s => sensor_json(sensor: s)))), + json_kv(key: "zones", value: json_array(elements: map(program.zones, z => zone_json(zone: z)))), + ]) +} + +fn semantic_program_rendering(program: BmcFanControlProgram) -> String { + serialize_json(v: program_json(program: program)) +} + +fn semantic_program_digest(program: BmcFanControlProgram) -> ContentHash { + content_hash_of_value(value: semantic_program_rendering(program: program) as NonEmptyStr) +} diff --git a/dag/extdeps/languages/json/member_conservation.dag b/dag/extdeps/languages/json/member_conservation.dag new file mode 100644 index 00000000000..bae69ff7688 --- /dev/null +++ b/dag/extdeps/languages/json/member_conservation.dag @@ -0,0 +1,419 @@ +module extdeps.languages.json.member_conservation + +import std.types { Bool, Int, List, NonEmptyStr, String } +import extdeps.languages.json.emit { JsonArray, JsonBool, JsonKeyValue, JsonNull, JsonNumber, JsonObject, JsonString, JsonValue } + +// THE WALL A SEMANTIC DECODER HAS TO PASS, BUILT BEFORE ANY FAN VOCABULARY EXISTS. A decoder over a +// captured configuration reads the members it understands and returns a typed record. Nothing in +// that shape prevents it from silently ignoring a member it does not understand, and the result +// still looks complete: every field the reader asked for is populated, and the one nobody modelled +// is simply gone. The source JSON still exists elsewhere, so no information was destroyed - but the +// OBSERVATION claims to describe a program it only partly read, and a later consumer cannot tell +// whether the decoder saw no residue or dropped it. +// +// The remedy is a checked partition: every member occurrence in the source object is accounted for +// exactly once as consumed, unmodelled, or defective. This module owns that check and knows nothing +// about fans, PIDs or OpenBMC. +// +// IT SITS BESIDE THE JSON GRAMMAR RATHER THAN IN THE CONSUMER THAT NEEDED IT FIRST, because its +// subject is a JSON object and nothing about it is specific to any one decoder. It claims no +// upstream fact -- this is a discipline for READING documents, not a model of RFC 8259 -- so it +// carries no citation of its own and adds none to the JSON authority's. +// +// WHY IDENTITY AND NOT COUNT, WHICH IS THE WHOLE POINT. A conservation check written as +// `source.length() == consumed.length() + unmodeled.length() + defective.length()` passes this: +// +// drop the unknown member at ordinal 4 +// classify the known member at ordinal 2 twice +// +// Same total, one member lost, one double-counted, green. Counting is exactly the oracle DESIGN +// forbids -- a measurement compared against another measurement of the same thing. So the check is +// an identity join: every source ordinal appears exactly once across the three lists, and nothing +// appears that the source did not contain. + +// AN OCCURRENCE IS A POSITION, NOT A KEY, AND THAT IS FORCED BY THE FORMAT RATHER THAN CHOSEN. This +// is legal JSON: +// +// { "type": "fan", "type": "stepwise" } +// +// Both members have key "type". A residue reported as the string "type" cannot say which of the two +// was consumed and which was retained, and a decoder that read one and dropped the other would be +// indistinguishable from one that read both. The ordinal is what separates them. +type JsonOccurrenceIdentity { + object_path: NonEmptyStr + ordinal: Int +} + +type JsonMemberOccurrence { + identity: JsonOccurrenceIdentity + member: JsonKeyValue +} + +// WHY A DEFECTIVE MEMBER IS NOT AN UNMODELLED ONE. They have different owners and opposite repairs. +// An unmodelled member is a gap in THIS 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 does know -- a duplicated +// identity field, a value of the wrong JSON kind, a number outside its domain. Collapsing them +// would let a malformed known field be reported as a vendor extension, which reads as "we do not +// model that yet" when it actually means "this program is wrong". +type MemberDisposition + = MemberConsumed { occurrence: JsonMemberOccurrence, role: NonEmptyStr } + | MemberUnmodeled { occurrence: JsonMemberOccurrence } + | MemberDefective { occurrence: JsonMemberOccurrence, cause: NonEmptyStr } + +type ObjectMemberPartition { + object_path: NonEmptyStr + source: List + dispositions: List +} + +// THE VERDICT NAMES WHICH LAW BROKE, because the three failures have different fixes: a lost member +// means the decoder needs a branch, a repeated one means two branches claim the same member, and a +// foreign one means a disposition was authored against an object it did not come from. +type ConservationVerdict + = MembersConserved { member_count: Int } + | MemberLost { object_path: NonEmptyStr, ordinal: Int } + | MemberDispositionedTwice { object_path: NonEmptyStr, ordinal: Int, times: Int } + | MemberForeignToObject { object_path: NonEmptyStr, occurrence_path: NonEmptyStr, ordinal: Int } + | PartitionSourcePathMismatch { partition_path: NonEmptyStr, occurrence_path: NonEmptyStr, ordinal: Int } + +fn disposition_occurrence(disposition: MemberDisposition) -> JsonMemberOccurrence { + match disposition { + MemberConsumed { occurrence, role } => occurrence + MemberUnmodeled { occurrence } => occurrence + MemberDefective { occurrence, cause } => occurrence + } +} + +// ORDINALS ARE ASSIGNED BY THE ENUMERATION AND NEVER BY THE CALLER, so a decoder cannot invent an +// occurrence that the source did not contain. Everything downstream refers to members through this +// list. +fn object_member_occurrences( + object_path: NonEmptyStr, + members: List, +) -> List { + fold( + members, + init: [], + f: (acc, member) => + flat_map( + [ + acc, + [ + JsonMemberOccurrence { + identity: JsonOccurrenceIdentity { + object_path: object_path, + ordinal: acc.length(), + }, + member: member, + }, + ], + ], + group => group, + ), + ) +} + +fn occurrences_of_object(object_path: NonEmptyStr, value: JsonValue) -> List { + match value { + JsonObject { members } => object_member_occurrences(object_path: object_path, members: members) + other => [] + } +} + +// THE JOIN COMPARES THE WHOLE IDENTITY, AND THE FIRST VERSION OF THIS MODULE DID NOT. It declared +// an identity of object path plus ordinal and then joined on the ordinal alone, so +// +// 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. +// That defeats the exact wall everything above it cites: a PID decoder could classify a member of +// one controller as the corresponding member of its sibling and conserve cleanly, which is the +// silent-substitution failure this module exists to stop, one level down. +// +// The first witness did not catch it because its "foreign" disposition was a foreign ORDINAL from +// the same object, not a sibling object carrying an ordinal the subject also has. Two objects with +// overlapping ordinals is the ordinary case -- every object has an ordinal 0 -- so the untested +// half was the common one. +fn occurrence_identity_equal(a: JsonOccurrenceIdentity, b: JsonOccurrenceIdentity) -> Bool { + a.object_path == b.object_path && a.ordinal == b.ordinal +} + +fn times_dispositioned(dispositions: List, identity: JsonOccurrenceIdentity) -> Int { + fold( + dispositions, + init: 0, + f: (acc, disposition) => + if occurrence_identity_equal( + a: disposition_occurrence(disposition: disposition).identity, + b: identity, + ) { + acc + 1 + } else { + acc + }, + ) +} + +fn source_contains_identity(source: List, identity: JsonOccurrenceIdentity) -> Bool { + fold( + source, + init: false, + f: (acc, occurrence) => + acc || occurrence_identity_equal(a: occurrence.identity, b: identity), + ) +} + +// THE PARTITION'S OWN PATH IS A THIRD INDEPENDENTLY AUTHORED COPY OF THE SAME FACT, so the SOURCE +// is checked against it rather than trusted. Without this a partition could name one object while +// every occurrence in it describes another, and the identity join below would hold perfectly over +// the wrong object -- consistent, and about something else. +// +// ONLY THE SOURCE IS CHECKED THIS WAY, AND THAT IS DELIBERATE. Guarding the DISPOSITIONS the same +// way was written first and then removed, because it made the identity join's own path comparison +// unreachable: with both populations pre-filtered to one path, comparing paths inside the join can +// never decide anything, and a comparison whose disagreeing case cannot be authored is a +// decoration that will be cited as coverage. Measured, not reasoned: under the disposition guard, +// reducing the join to an ordinal-only comparison left the sibling-object witness GREEN. With the +// guard gone the join is what catches a sibling occurrence, and that mutation goes red. +fn first_path_mismatch(partition_path: NonEmptyStr, occurrences: List) -> List { + filter(occurrences, occurrence => occurrence.identity.object_path != partition_path) +} + +// THE JOIN RUNS IN BOTH DIRECTIONS, and one direction alone is not the law. Source-to-dispositions +// catches a member the decoder never accounted for and a member two branches both claimed; +// dispositions-to-source catches an occurrence authored against an object it did not come from. +// Checking only the first would let a decoder pad its partition with occurrences from a sibling +// object and still report every source member as covered. +fn conservation_verdict(partition: ObjectMemberPartition) -> ConservationVerdict { + let stray_source = first_path_mismatch(partition_path: partition.object_path, occurrences: partition.source) + if stray_source.length() > 0 { + PartitionSourcePathMismatch { + partition_path: partition.object_path, + occurrence_path: stray_source.first().identity.object_path, + ordinal: stray_source.first().identity.ordinal, + } + } else { + let lost_or_repeated = fold( + partition.source, + init: MembersConserved { member_count: partition.source.length() }, + f: (acc, occurrence) => + match acc { + MembersConserved { member_count } => { + let n = times_dispositioned( + dispositions: partition.dispositions, + identity: occurrence.identity, + ) + if n == 0 { + MemberLost { + object_path: partition.object_path, + ordinal: occurrence.identity.ordinal, + } + } else if n > 1 { + MemberDispositionedTwice { + object_path: partition.object_path, + ordinal: occurrence.identity.ordinal, + times: n, + } + } else { + MembersConserved { member_count: member_count } + } + } + other => acc + }, + ) + match lost_or_repeated { + MembersConserved { member_count } => + fold( + partition.dispositions, + init: MembersConserved { member_count: member_count }, + f: (acc, disposition) => + match acc { + MembersConserved { member_count: n } => { + let identity = disposition_occurrence(disposition: disposition).identity + if source_contains_identity(source: partition.source, identity: identity) { + MembersConserved { member_count: n } + } else { + MemberForeignToObject { + object_path: partition.object_path, + occurrence_path: identity.object_path, + ordinal: identity.ordinal, + } + } + } + other => acc + }, + ) + other => lost_or_repeated + } + } +} + +fn conservation_holds(partition: ObjectMemberPartition) -> Bool { + match conservation_verdict(partition: partition) { + MembersConserved { member_count } => true + other => false + } +} + +// ARRAY ELEMENTS NEED THE SAME LAW, AND WITHOUT THIS THE OBJECT WALL ABOVE IS ONLY HALF A WALL. A +// decoder can conserve every member of every object it CHOSE to decode while skipping one element +// of a PID array and duplicating another -- the object partitions all balance, because the skipped +// object simply never produced one. The array is where that is visible. +// +// Found in review of gunbc#9491, named there as mandatory before a representability gate: the +// whole-program denominator has to include the array populations (sensors, zones, each zone's +// pids, and each controller's inputs), not only the members of the objects inside them. +// +// 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. +type JsonElementIdentity { + array_path: NonEmptyStr + index: Int +} + +type JsonArrayElementOccurrence { + identity: JsonElementIdentity + element: JsonValue +} + +type ElementDisposition + = ElementConsumed { occurrence: JsonArrayElementOccurrence, role: NonEmptyStr } + | ElementUnmodeled { occurrence: JsonArrayElementOccurrence } + | ElementDefective { occurrence: JsonArrayElementOccurrence, cause: NonEmptyStr } + +type ArrayElementPartition { + array_path: NonEmptyStr + source: List + dispositions: List +} + +fn element_disposition_occurrence(disposition: ElementDisposition) -> JsonArrayElementOccurrence { + match disposition { + ElementConsumed { occurrence, role } => occurrence + ElementUnmodeled { occurrence } => occurrence + ElementDefective { occurrence, cause } => occurrence + } +} + +// INDICES ARE ASSIGNED BY THE ENUMERATION, never by the caller, for the reason ordinals are. +fn array_element_occurrences( + array_path: NonEmptyStr, + elements: List, +) -> List { + map( + enumerate(elements), + pair => + JsonArrayElementOccurrence { + identity: JsonElementIdentity { array_path: array_path, index: pair.first }, + element: pair.second, + }, + ) +} + +fn element_identity_equal(a: JsonElementIdentity, b: JsonElementIdentity) -> Bool { + a.array_path == b.array_path && a.index == b.index +} + +fn times_element_dispositioned(dispositions: List, identity: JsonElementIdentity) -> Int { + fold( + dispositions, + init: 0, + f: (acc, disposition) => + if element_identity_equal( + a: element_disposition_occurrence(disposition: disposition).identity, + b: identity, + ) { + acc + 1 + } else { + acc + }, + ) +} + +fn source_contains_element(source: List, identity: JsonElementIdentity) -> Bool { + fold( + source, + init: false, + f: (acc, occurrence) => acc || element_identity_equal(a: occurrence.identity, b: identity), + ) +} + +fn first_element_path_mismatch( + array_path: NonEmptyStr, + occurrences: List, +) -> List { + filter(occurrences, occurrence => occurrence.identity.array_path != array_path) +} + +// THE VERDICT VOCABULARY IS SHARED WITH THE OBJECT LAW ON PURPOSE. The law 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. The path and position fields carry the array's +// coordinates here and the object's there; which one a verdict describes is decided by the +// partition it came from, not by a second vocabulary. +fn element_conservation_verdict(partition: ArrayElementPartition) -> ConservationVerdict { + let stray_source = first_element_path_mismatch( + array_path: partition.array_path, + occurrences: partition.source, + ) + if stray_source.length() > 0 { + PartitionSourcePathMismatch { + partition_path: partition.array_path, + occurrence_path: stray_source.first().identity.array_path, + ordinal: stray_source.first().identity.index, + } + } else { + let lost_or_repeated = fold( + partition.source, + init: MembersConserved { member_count: partition.source.length() }, + f: (acc, occurrence) => + match acc { + MembersConserved { member_count } => { + let n = times_element_dispositioned( + dispositions: partition.dispositions, + identity: occurrence.identity, + ) + if n == 0 { + MemberLost { object_path: partition.array_path, ordinal: occurrence.identity.index } + } else if n > 1 { + MemberDispositionedTwice { + object_path: partition.array_path, + ordinal: occurrence.identity.index, + times: n, + } + } else { + MembersConserved { member_count: member_count } + } + } + other => acc + }, + ) + match lost_or_repeated { + MembersConserved { member_count } => + fold( + partition.dispositions, + init: MembersConserved { member_count: member_count }, + f: (acc, disposition) => + match acc { + MembersConserved { member_count: n } => { + let identity = element_disposition_occurrence(disposition: disposition).identity + if source_contains_element(source: partition.source, identity: identity) { + MembersConserved { member_count: n } + } else { + MemberForeignToObject { + object_path: partition.array_path, + occurrence_path: identity.array_path, + ordinal: identity.index, + } + } + } + other => acc + }, + ) + other => lost_or_repeated + } + } +} diff --git a/dag/extdeps/languages/json/number.dag b/dag/extdeps/languages/json/number.dag new file mode 100644 index 00000000000..f995c09cb90 --- /dev/null +++ b/dag/extdeps/languages/json/number.dag @@ -0,0 +1,146 @@ +module extdeps.languages.json.number + +import std.types { Bool, Int, NonEmptyStr, String } +import std.decimal { ExactDecimal, ExactDecimalAdmitted, ExactDecimalScaleRefused, admit_exact_decimal } +import extdeps.languages.json.grammar { JsonNumberLexeme } +import extdeps.languages.json.emit { JsonArray, JsonBool, JsonNull, JsonNumber, JsonObject, JsonString, JsonValue } + +// READING A JSON NUMBER AS A VALUE, WHICH THIS TREE DELIBERATELY DID NOT DO UNTIL A CONSUMER +// NEEDED IT. extdeps.languages.json.emit keeps every number as a JsonNumberLexeme -- a branded +// String -- precisely so that parsing never silently reinterprets a numeral, and +// extdeps.github.workflow_run_event's run_id note records that decision along with where the +// decode belongs when it is finally needed: "the decode lands in the JSON authority with its own +// witness, not here". This is that module. It is placed beside the grammar rather than in the +// consumer for the reason that note gives -- a decode minted inside a reader is a second reading +// of RFC 8259 section 6, and this tree has already paid for one of those (the exponent fork the +// grammar's own note records). +// +// THE CONSUMER THAT FORCED IT: two captured OpenBMC fan programs write the same coefficient as +// `30` on one host and `30.0` on the other. 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. + +// THE MODELLED FRAGMENT IS RFC 8259's NUMBER PRODUCTION MINUS ITS EXPONENT, AND THE EXCLUSION +// REFUSES RATHER THAN APPROXIMATING. `1e3` is a perfectly good JSON number; expanding it here +// would mean deciding what `1e400` becomes, and any answer to that is either an overflow or a +// fabricated one. So the exponent form is named as outside the fragment and stops the line, which +// leaves the decision with a caller that knows its own domain -- and costs nothing today, because +// no captured document uses it. +// THE FRAGMENT IS NARROWER THAN "EXPONENT-FREE RFC NUMBERS", AND SAYING SO IS THE POINT. The +// digits are read into the substrate's Int, so an exponent-free numeral whose exact coefficient +// exceeds that range is refused -- and it is refused as a MAGNITUDE limit, not as unreadable +// digits. A grammar-validated lexeme does not have unreadable digits merely because the carrier +// that would hold it is bounded, and the two have different owners: one is a document to fix, the +// other is this fragment reaching its edge. Found in review of gunbc#9491, where both landed on +// one arm. +type JsonNumberFragmentRefusal + = JsonNumberUsesExponent + | JsonNumberMagnitudeOutsideCarrierRange + | JsonNumberScaleRefused + +type JsonNumberReading + = JsonNumberExact { value: ExactDecimal } + | JsonNumberOutsideExactFragment { lexeme: String, refusal: JsonNumberFragmentRefusal } + +fn json_number_fragment_refusal_text(r: JsonNumberFragmentRefusal) -> NonEmptyStr { + match r { + JsonNumberUsesExponent => "json number uses the exponent form, which is outside the exactly-read fragment" + JsonNumberMagnitudeOutsideCarrierRange => "json number coefficient does not fit the substrate integer carrier" + JsonNumberScaleRefused => "json number fraction-digit count was refused by the exact decimal mint" + } +} + +// A SCAN RATHER THAN A `contains`, BECAUSE THE POSITION IS THE ANSWER. Whether the lexeme has a +// decimal point is not the question; where it is decides how many fraction digits there are. +fn json_number_char_index(s: String, i: Int, wanted: String, other: String) -> Int { + if i >= s.length() { + s.length() + } else if char_at(s, i) == wanted || char_at(s, i) == other { + i + } else { + json_number_char_index(s: s, i: i + 1, wanted: wanted, other: other) + } +} + +fn json_number_digits_before_point(body: String, point: Int) -> String { + substring(s: body, start: 0, end: point) +} + +fn json_number_digits_after_point(body: String, point: Int) -> String { + if point >= body.length() { + "" + } else { + substring(s: body, start: point + 1, end: body.length()) + } +} + +fn json_number_fraction_digit_count(body: String, point: Int) -> Int { + json_number_digits_after_point(body: body, point: point).length() +} + +fn json_number_signed_units(digits: String, negative: Bool) -> Int? { + match parse_int(s: digits) { + Present { value: v } => Present { value: if negative { 0 - v } else { v } } + Absent => Absent + } +} + +// WHY THE SIGN IS STRIPPED BEFORE THE DIGITS ARE JOINED RATHER THAN LEFT IN PLACE. `-0.5` has to +// become units -5 with one fraction digit, and the digit string handed to parse_int is built by +// concatenating the two sides of the point. Leaving the minus attached would produce "-05", whose +// reading depends on how parse_int treats a leading zero after a sign -- a question this decode +// has no need to ask. Negating a magnitude asks nothing. +fn read_json_number_lexeme(lexeme: String) -> JsonNumberReading { + let n = lexeme.length() + let exponent_at = json_number_char_index(s: lexeme, i: 0, wanted: "e", other: "E") + if exponent_at < n { + JsonNumberOutsideExactFragment { lexeme: lexeme, refusal: JsonNumberUsesExponent } + } else { + let negative = starts_with(s: lexeme, prefix: "-") + let body = if negative { substring(s: lexeme, start: 1, end: n) } else { lexeme } + let point = json_number_char_index(s: body, i: 0, wanted: ".", other: ".") + let digits = join([ + json_number_digits_before_point(body: body, point: point), + json_number_digits_after_point(body: body, point: point), + ], "") + match json_number_signed_units(digits: digits, negative: negative) { + Present { value: units } => + match admit_exact_decimal( + units: units, + fraction_digits: json_number_fraction_digit_count(body: body, point: point), + ) { + ExactDecimalAdmitted { canonical } => JsonNumberExact { value: canonical } + ExactDecimalScaleRefused { observed_fraction_digits } => + JsonNumberOutsideExactFragment { lexeme: lexeme, refusal: JsonNumberScaleRefused } + } + Absent => + JsonNumberOutsideExactFragment { + lexeme: lexeme, + refusal: JsonNumberMagnitudeOutsideCarrierRange, + } + } + } +} + +fn read_json_number(lexeme: JsonNumberLexeme) -> JsonNumberReading { + read_json_number_lexeme(lexeme: lexeme as String) +} + +// READING A NUMBER OUT OF A VALUE OF UNKNOWN KIND IS A DIFFERENT QUESTION AND GETS A DIFFERENT +// ANSWER. A string, an object or a null in a coefficient position is not a number that failed to +// read -- it is a document that put the wrong kind of thing there, which is a defect in the +// document rather than a limit of this fragment. Collapsing the two would let a coefficient +// spelled "30" (quoted) report as an unreadable numeral. +type JsonNumberValueReading + = JsonNumberValueRead { reading: JsonNumberReading } + | JsonValueIsNotANumber + +fn read_json_number_value(v: JsonValue) -> JsonNumberValueReading { + match v { + JsonNumber { lexeme: l } => JsonNumberValueRead { reading: read_json_number(lexeme: l) } + JsonString { value: _ } => JsonValueIsNotANumber + JsonBool { value: _ } => JsonValueIsNotANumber + JsonNull => JsonValueIsNotANumber + JsonArray { elements: _ } => JsonValueIsNotANumber + JsonObject { members: _ } => JsonValueIsNotANumber + } +} diff --git a/dag/gunbc/bmc_fan_program_decode_witness.dag b/dag/gunbc/bmc_fan_program_decode_witness.dag new file mode 100644 index 00000000000..f2a7c83d13f --- /dev/null +++ b/dag/gunbc/bmc_fan_program_decode_witness.dag @@ -0,0 +1,166 @@ +module gunbc.bmc_fan_program_decode_witness + +import std.types { Bool, Int, List, NonEmptyStr, String } +import std.process { ProcessExit, ExitSuccess, exit_failure } +import std.decimal { exact_decimal_wire } +import std.measure { measure_count } +import extdeps.languages.json.emit { JsonValue, json_object } +import extdeps.languages.json.member_conservation { MembersConserved, conservation_verdict } +import extdeps.bmc.pid_control_program { + ActuatorController, + BmcFanControlProgram, + DbusBoundsIgnored, + DbusBoundsUnstated, + DbusBoundsUsed, + FanTachometerSensor, + ProgramSensor, + ProgramZone, + SensorDrivesOutput, + SensorReadOnly, + TemperatureSensor, + ThermalDemandController, +} +import extdeps.bmc.pid_control_decode { + ProgramDecodeRefused, + ProgramDecoded, + ProgramMembersNotConserved, + decode_program, +} +import gunbc.bmc_fan_program_observation { + ArtifactJsonValueObserved, + srv3_program_json, + srv4_program_json, +} + +// THIS WITNESS READS THE COMMITTED CAPTURE ARTIFACTS THROUGH THE SUBSTRATE'S OWN CHECKOUT ROUTE, +// so it declares the live-tree disposition its observation carrier already declares. It is +// therefore DECLINED by the floor planner today and does not execute there -- the same standing +// gunbc.bmc_fan_program_observation carries, and it changes when that planner veto is removed. +data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree + +fn srv3_programs() -> List { + match srv3_program_json { + ArtifactJsonValueObserved { artifact_path, byte_count, document } => + match decode_program(document: document) { + ProgramDecoded { program, partitions, element_partitions } => [program] + other => [] + } + other => [] + } +} + +fn srv4_programs() -> List { + match srv4_program_json { + ArtifactJsonValueObserved { artifact_path, byte_count, document } => + match decode_program(document: document) { + ProgramDecoded { program, partitions, element_partitions } => [program] + other => [] + } + other => [] + } +} + +fn actuator_named(program: BmcFanControlProgram, name: NonEmptyStr) -> List { + flat_map(program.zones, zone => filter(zone.actuator_controllers, c => c.name == name)) +} + +fn thermal_controllers(program: BmcFanControlProgram) -> List { + flat_map(program.zones, zone => zone.thermal_demand_controllers) +} + +// BOTH CAPTURED DOCUMENTS DECODE WHOLE, WITH EVERY MEMBER ACCOUNTED FOR. A decode that read the +// fields it knows and dropped an unmodelled member would not reach here: the conservation join +// inside decode_program refuses first. +fn both_hosts_decode_completely() -> Bool { + srv3_programs().length() == 1 && srv4_programs().length() == 1 +} + +// ONE DEMAND, TWO ACTUATORS -- the structural claim of the model, read off the deployed document +// rather than asserted about it. +fn the_shape_is_one_demand_feeding_two_actuators() -> Bool { + let program = srv3_programs().first() + thermal_controllers(program: program).length() == 1 + && flat_map(program.zones, zone => zone.actuator_controllers).length() == 2 +} + +// THE TWO ACTUATORS DIFFER EXACTLY WHERE THE ACOUSTIC OUTCOME LIVES: the feed-forward offset and +// the output floor. Everything else about them is the same. These are the numbers that made the +// fleet quiet, so they are pinned by value. +fn the_actuators_carry_the_offsets_that_made_it_quiet() -> Bool { + let program = srv3_programs().first() + let fan1 = actuator_named(program: program, name: "FAN1") + let chassis = actuator_named(program: program, name: "CHASSIS") + fan1.length() == 1 + && chassis.length() == 1 + && exact_decimal_wire(d: fan1.first().feed_forward.offset.magnitude) == "-8" + && exact_decimal_wire(d: fan1.first().output_limits.minimum.magnitude) == "3" + && exact_decimal_wire(d: chassis.first().feed_forward.offset.magnitude) == "35" + && exact_decimal_wire(d: chassis.first().output_limits.minimum.magnitude) == "40" + && exact_decimal_wire(d: chassis.first().slew.negative_coefficient) == "-3" +} + +// THE CHASSIS ACTUATOR DRIVES THREE FANS AND FAN1 DRIVES ONE, which is the wiring fact the +// document states and the reason one offset cannot serve both. +fn the_actuator_endpoint_populations_differ() -> Bool { + let program = srv3_programs().first() + actuator_named(program: program, name: "FAN1").first().inputs.length() == 1 + && actuator_named(program: program, name: "CHASSIS").first().inputs.length() == 3 +} + +fn the_deployed_curve_survives_the_whole_program_decode() -> Bool { + let program = srv3_programs().first() + let demand = thermal_controllers(program: program).first() + demand.curve.length() == 9 + && demand.name == "TEMP_SOC" + && exact_decimal_wire(d: demand.failsafe_output.magnitude) == "75" +} + +// THE TWO HOSTS AGREE ON THE COEFFICIENT THEY SPELL DIFFERENTLY. srv3 writes minThermalOutput as +// 30.0 and srv4 writes it as 30; a decoder comparing lexemes would report two different programs. +fn the_two_hosts_agree_on_the_coefficient_they_spell_differently() -> Bool { + let srv3_zone = srv3_programs().first().zones.first() + let srv4_zone = srv4_programs().first().zones.first() + exact_decimal_wire(d: srv3_zone.minimum_thermal_output.magnitude) + == exact_decimal_wire(d: srv4_zone.minimum_thermal_output.magnitude) +} + +// THE THREE-STATE D-BUS BOUNDS FIELD IS EXERCISED BY THE REAL DOCUMENT, not only by a fixture: at +// least one captured sensor entry does not state it, which is why the third state exists. +fn a_captured_sensor_leaves_the_dbus_bounds_unstated() -> Bool { + let program = srv4_programs().first() + filter(program.sensors, sensor => + match sensor.dbus_bounds { + DbusBoundsUnstated => true + DbusBoundsIgnored => false + DbusBoundsUsed => false + }).length() > 0 +} + +// A TEMPERATURE SENSOR HAS NOTHING TO DRIVE AND A FAN SENSOR DOES, which the model carries as a +// coproduct rather than an absent string. +fn writability_follows_the_sensor_role() -> Bool { + let program = srv3_programs().first() + let temps = filter(program.sensors, sensor => + match sensor.role { TemperatureSensor => true FanTachometerSensor => false }) + let fans = filter(program.sensors, sensor => + match sensor.role { FanTachometerSensor => true TemperatureSensor => false }) + temps.length() > 0 + && fans.length() > 0 + && all(temps, sensor => match sensor.actuation { SensorReadOnly => true SensorDrivesOutput { write_path } => false }) + && all(fans, sensor => match sensor.actuation { SensorDrivesOutput { write_path } => true SensorReadOnly => false }) +} + +fn bmc_fan_program_decode_witness() -> ProcessExit { + if both_hosts_decode_completely() + && the_shape_is_one_demand_feeding_two_actuators() + && the_actuators_carry_the_offsets_that_made_it_quiet() + && the_actuator_endpoint_populations_differ() + && the_deployed_curve_survives_the_whole_program_decode() + && the_two_hosts_agree_on_the_coefficient_they_spell_differently() + && a_captured_sensor_leaves_the_dbus_bounds_unstated() + && writability_follows_the_sensor_role() { + ExitSuccess + } else { + exit_failure(reason: "captured fan program decode: completeness, the one-demand-two-actuator shape, the deployed offsets, or the cross-host coefficient agreement changed") + } +} diff --git a/dag/gunbc/bmc_fan_program_interpretation.dag b/dag/gunbc/bmc_fan_program_interpretation.dag new file mode 100644 index 00000000000..b4cda586de4 --- /dev/null +++ b/dag/gunbc/bmc_fan_program_interpretation.dag @@ -0,0 +1,81 @@ +module gunbc.bmc_fan_program_interpretation + +import std.types { Bool, Int, List, NonEmptyStr, String } +import std.content_hash { ContentHash } +import std.decl_ref { DeclarationRef, WholeDeclaration } + +// WHAT PRODUCED A SEMANTIC PROGRAM, KEPT SEPARATE FROM WHAT THE PROGRAM MEANS. An adoption says an +// operator accepted a particular program; this says which decoder, over which bytes, produced the +// reading that adoption was made from. Keeping them apart decides the case that actually comes up: +// +// a new decoder + the same raw artifact + the same semantic digest +// -> the adopted policy still means what it meant; nobody re-adopts anything +// +// a corrected decoder that produces a DIFFERENT semantic digest from the same bytes +// -> the old adoption is about a program nobody is running, and needs adjudication +// +// Folding decoder provenance into the adoption would make the first case look like the second, so +// every harmless refactor of this decoder would demand the operator re-approve the fleet's fans. +type FanProgramDecoderIdentity { + entry_declaration: DeclarationRef + source_closure_digest: ContentHash + compiler_runtime_digest: ContentHash +} + +// THE IDENTITY IS NOT AUTHORED HERE, AND THAT IS THE WHOLE CONTENT OF THIS MODULE TODAY. Both +// digests are properties of an execution -- the exact 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 precisely the fake join removed from +// the capture observer on gunbc#9299: two constants that agree because one author wrote both, and +// which keep agreeing after the thing they describe has changed. +// +// So the absent state is a named state rather than a placeholder value, and every consumer must +// match it. A receipt with no decoder identity is usable for saying WHAT was read; it is not +// usable for saying that two readings were produced by the same reader. +type DecoderIdentityStanding + = DecoderIdentityEstablished { identity: FanProgramDecoderIdentity } + | DecoderIdentityNotInstrumented { obligation: NonEmptyStr } + +// THE PRECEDENT AND THE TRIGGER, both named so this does not have to be rediscovered. The two-digest +// shape already exists in this repository: tools.multi_module_compile_fixture carries a structural +// source_digest over its exact source vector and a compiler_digest taken from the running +// compiler's own content hash, and its note records why both are absent from its refused arm -- +// stamping a digest on a measurement that did not happen names a measurement that did not happen. +// This module reuses that concept rather than minting a fan-specific one. +// +// DISSOLVES WHEN: an instrument supplies both digests for a decode, at which point +// DecoderIdentityNotInstrumented has no producer and the carrier below always holds an established +// identity. Until then the standing is honest and the receipt says so. +data decoder_identity_instrument_obligation: NonEmptyStr = "no instrument in this repository supplies a source-closure digest for a .dag entry's transitive closure together with the running compiler's content digest, so a decoder identity would have to be hand-authored beside the result it describes. Precedent for the shape: tools.multi_module_compile_fixture source_digest and compiler_digest." + +data fan_program_decoder: DeclarationRef = DeclarationRef { + module_path: "extdeps.bmc.pid_control_representability", + decl_name: "program_representability", + field: WholeDeclaration, +} + +data fan_program_decoder_identity_standing: DecoderIdentityStanding = DecoderIdentityNotInstrumented { + obligation: decoder_identity_instrument_obligation, +} + +// THE RECEIPT JOINS THE THREE FACTS A LATER ADOPTION NEEDS, and carries the decoder's standing +// rather than assuming one. The artifact digest says which bytes were read; the semantic digest +// says what program they were read AS; the standing says whether the reader that turned one into +// the other is itself identified. +type FanProgramInterpretationReceipt { + source_artifact_digest: ContentHash + semantic_program_digest: ContentHash + decoder: DeclarationRef + decoder_standing: DecoderIdentityStanding +} + +// A RECEIPT WHOSE DECODER IS UNIDENTIFIED CAN STILL BE COMPARED WITH ANOTHER OF THE SAME KIND, and +// this predicate is what a consumer asks before treating two receipts' semantic digests as +// comparable. It answers false today, deliberately: two digests produced by decoders nobody can +// identify are equal-looking, not established-equal. +fn receipt_decoder_is_identified(receipt: FanProgramInterpretationReceipt) -> Bool { + match receipt.decoder_standing { + DecoderIdentityEstablished { identity } => true + DecoderIdentityNotInstrumented { obligation } => false + } +} diff --git a/dag/gunbc/bmc_fan_program_representability_witness.dag b/dag/gunbc/bmc_fan_program_representability_witness.dag new file mode 100644 index 00000000000..1c735df959d --- /dev/null +++ b/dag/gunbc/bmc_fan_program_representability_witness.dag @@ -0,0 +1,164 @@ +module gunbc.bmc_fan_program_representability_witness + +import std.types { Bool, Int, List, String } +import std.process { ProcessExit, ExitSuccess, exit_failure } +import std.content_hash { ContentHash, serialize_content_hash } +import extdeps.languages.json.emit { JsonValue, json_object } +import extdeps.languages.json.parse { JsonDocumentParsed, parse_json_document } +import extdeps.bmc.pid_control_semantic_identity { semantic_program_rendering } +import extdeps.bmc.pid_control_representability { + FanProgramFullyRepresentable, + FanProgramNotConserved, + FanProgramNotDecoded, + FanProgramNotRepresentable, + KnownFieldDefective, + ResidueUnmodeled, + program_representability, +} +import gunbc.bmc_fan_program_observation { + ArtifactJsonValueObserved, + srv3_program_json, + srv4_program_json, +} + +data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree + +fn srv3_digest() -> List { + match srv3_program_json { + ArtifactJsonValueObserved { artifact_path, byte_count, document } => + match program_representability(document: document) { + FanProgramFullyRepresentable { program, semantic_digest } => + [serialize_content_hash(hash: semantic_digest)] + other => [] + } + other => [] + } +} + +fn srv4_digest() -> List { + match srv4_program_json { + ArtifactJsonValueObserved { artifact_path, byte_count, document } => + match program_representability(document: document) { + FanProgramFullyRepresentable { program, semantic_digest } => + [serialize_content_hash(hash: semantic_digest)] + other => [] + } + other => [] + } +} + +// BOTH DEPLOYED PROGRAMS PASS THE GATE. Nothing in either captured document is unmodelled and +// nothing known is defective, which is what makes them usable as the basis for a policy rather +// than merely observable. +fn both_captured_programs_are_fully_representable() -> Bool { + srv3_digest().length() == 1 && srv4_digest().length() == 1 +} + +// A DOCUMENT CARRYING A FIELD NOBODY MODELS IS OBSERVABLE AND NOT REPRESENTABLE, and the refusal +// names the member so the model knows what it is behind on. This is the fixture that proves the +// gate is a gate: the same document without the extra member passes. +data extended_sensor_text: String = "\{\"sensors\": [\{\"name\": \"FAN1\", \"type\": \"fan\", \"readPath\": \"/r\", \"writePath\": \"/w\", \"vendorTuning\": 7\}], \"zones\": []\}" + +data plain_sensor_text: String = "\{\"sensors\": [\{\"name\": \"FAN1\", \"type\": \"fan\", \"readPath\": \"/r\", \"writePath\": \"/w\"\}], \"zones\": []\}" + +fn parsed(text: String) -> JsonValue { + match parse_json_document(s: text) { + JsonDocumentParsed { value } => value + other => json_object(members: []) + } +} + +fn an_unmodeled_member_refuses_and_names_itself() -> Bool { + match program_representability(document: parsed(text: extended_sensor_text)) { + FanProgramNotRepresentable { refusal } => + match refusal { + ResidueUnmodeled { identity, key, residue_count } => key == "vendorTuning" && residue_count == 1 + KnownFieldDefective { identity, key, cause } => false + } + other => false + } +} + +// THE POSITIVE CONTROL FOR THAT REFUSAL, without which the conjunct above is satisfied by a gate +// that refuses everything. +fn the_same_document_without_the_extra_member_passes() -> Bool { + match program_representability(document: parsed(text: plain_sensor_text)) { + FanProgramFullyRepresentable { program, semantic_digest } => program.sensors.length() == 1 + other => false + } +} + +// THE SEMANTIC DIGEST IS INVARIANT TO EVERY WAY A FILE CAN DIFFER WITHOUT THE DAEMON NOTICING. The +// second document writes the same sensor with its members in a different order; the two are the +// same program and must carry one identity. +data reordered_sensor_text: String = "\{\"sensors\": [\{\"writePath\": \"/w\", \"readPath\": \"/r\", \"type\": \"fan\", \"name\": \"FAN1\"\}], \"zones\": []\}" + +fn rendering_of(text: String) -> List { + match program_representability(document: parsed(text: text)) { + FanProgramFullyRepresentable { program, semantic_digest } => + [serialize_content_hash(hash: semantic_digest)] + other => [] + } +} + +fn member_order_does_not_move_the_semantic_digest() -> Bool { + let a = rendering_of(text: plain_sensor_text) + let b = rendering_of(text: reordered_sensor_text) + a.length() == 1 && b.length() == 1 && a.first() == b.first() +} + +// AND THE DISCRIMINATOR IN THE OTHER DIRECTION, without which the invariance above is satisfied by +// a digest that is constant. One character of the read path differs. +data altered_sensor_text: String = "\{\"sensors\": [\{\"name\": \"FAN1\", \"type\": \"fan\", \"readPath\": \"/R\", \"writePath\": \"/w\"\}], \"zones\": []\}" + +fn a_semantic_change_moves_the_digest() -> Bool { + let a = rendering_of(text: plain_sensor_text) + let b = rendering_of(text: altered_sensor_text) + a.length() == 1 && b.length() == 1 && a.first() != b.first() +} + +// THE TWO HOSTS RUN DIFFERENT PROGRAMS, and the digest says so. They differ in their sensor roster +// and in one actuator's endpoints, so a digest reporting them equal would be reporting that the +// fleet is uniform when it is not. +fn the_two_hosts_carry_distinct_semantic_identities() -> Bool { + srv3_digest().first() != srv4_digest().first() +} + +// A NUMERIC COEFFICIENT MUST MOVE THE DIGEST, AND THE FIRST VERSION OF THIS WITNESS COULD NOT SEE +// IT. Rendering every magnitude as one constant string left every conjunct green: the two hosts +// still differed by their sensor roster, and the fixture pair differed by a path. A digest blind +// to every number in the program would have passed as a semantic identity. +data zone_30_text: String = "\{\"sensors\": [], \"zones\": [\{\"id\": 0, \"minThermalOutput\": 30, \"failsafePercent\": 75, \"cycleIntervalTimeMS\": 1000, \"updateThermalsTimeMS\": 1000, \"pids\": []\}]\}" + +data zone_30_point_0_text: String = "\{\"sensors\": [], \"zones\": [\{\"id\": 0, \"minThermalOutput\": 30.0, \"failsafePercent\": 75, \"cycleIntervalTimeMS\": 1000, \"updateThermalsTimeMS\": 1000, \"pids\": []\}]\}" + +data zone_31_text: String = "\{\"sensors\": [], \"zones\": [\{\"id\": 0, \"minThermalOutput\": 31, \"failsafePercent\": 75, \"cycleIntervalTimeMS\": 1000, \"updateThermalsTimeMS\": 1000, \"pids\": []\}]\}" + +fn a_changed_coefficient_moves_the_digest() -> Bool { + let a = rendering_of(text: zone_30_text) + let b = rendering_of(text: zone_31_text) + a.length() == 1 && b.length() == 1 && a.first() != b.first() +} + +// AND THE TWO SPELLINGS OF ONE NUMBER DO NOT, which is the cross-host claim tested at the level +// that matters. srv3 writes this coefficient as 30.0 and srv4 writes it as 30. +fn two_spellings_of_one_coefficient_carry_one_digest() -> Bool { + let a = rendering_of(text: zone_30_text) + let b = rendering_of(text: zone_30_point_0_text) + a.length() == 1 && b.length() == 1 && a.first() == b.first() +} + +fn bmc_fan_program_representability_witness() -> ProcessExit { + if both_captured_programs_are_fully_representable() + && an_unmodeled_member_refuses_and_names_itself() + && the_same_document_without_the_extra_member_passes() + && member_order_does_not_move_the_semantic_digest() + && a_semantic_change_moves_the_digest() + && the_two_hosts_carry_distinct_semantic_identities() + && a_changed_coefficient_moves_the_digest() + && two_spellings_of_one_coefficient_carry_one_digest() { + ExitSuccess + } else { + exit_failure(reason: "fan program representability: the residue gate, the semantic digest's invariance to member order, or its sensitivity to a semantic changeced") + } +} diff --git a/dag/gunbc/json_exact_number_witness.dag b/dag/gunbc/json_exact_number_witness.dag new file mode 100644 index 00000000000..9b6ec414518 --- /dev/null +++ b/dag/gunbc/json_exact_number_witness.dag @@ -0,0 +1,169 @@ +module gunbc.json_exact_number_witness + +import std.types { Bool, Int, String } +import std.process { ProcessExit, ExitSuccess, exit_failure } +import std.decimal { ExactDecimal, canonical_exact_decimal, exact_decimal_equal, exact_decimal_wire } +import extdeps.languages.json.emit { json_string } +import extdeps.languages.json.number { + JsonNumberMagnitudeOutsideCarrierRange, + JsonNumberExact, + JsonNumberOutsideExactFragment, + JsonNumberUsesExponent, + JsonNumberValueRead, + JsonValueIsNotANumber, + read_json_number_lexeme, + read_json_number_value, +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +fn reads(lexeme: String, units: Int, fraction_digits: Int) -> Bool { + match read_json_number_lexeme(lexeme: lexeme) { + JsonNumberExact { value } => + value.units == units && value.fraction_digits == fraction_digits + other => false + } +} + +// THE CASE THAT MOTIVATED THE MODULE, AND IT IS NOT AN ABSTRACT ONE. srv3's captured fan program +// writes minThermalOutput as `30.0`; srv4 writes it as `30`. If those two do not compare equal, +// every downstream question about whether the two hosts run the same program answers no for a +// reason that has nothing to do with the hosts. +fn the_two_spellings_of_thirty_agree() -> Bool { + match read_json_number_lexeme(lexeme: "30.0") { + JsonNumberExact { value: a } => + match read_json_number_lexeme(lexeme: "30") { + JsonNumberExact { value: b } => exact_decimal_equal(a: a, b: b) + other => false + } + other => false + } +} + +// AND THE DISCRIMINATOR IN THE OTHER DIRECTION, without which the conjunct above is satisfied by +// an equality that answers true for everything. +fn two_different_numbers_still_differ() -> Bool { + match read_json_number_lexeme(lexeme: "30.0") { + JsonNumberExact { value: a } => + match read_json_number_lexeme(lexeme: "30.5") { + JsonNumberExact { value: b } => !exact_decimal_equal(a: a, b: b) + other => false + } + other => false + } +} + +// THE COEFFICIENTS THE DEPLOYED PROGRAM ACTUALLY CARRIES: a negative offset, a negative slew, and a +// whole number. The negative cases are the ordinary ones here, not an edge. +fn the_deployed_coefficients_read_exactly() -> Bool { + reads(lexeme: "-8.0", units: -8, fraction_digits: 0) + && reads(lexeme: "35.0", units: 35, fraction_digits: 0) + && reads(lexeme: "-0.5", units: -5, fraction_digits: 1) + && reads(lexeme: "0.005", units: 5, fraction_digits: 3) + && reads(lexeme: "75", units: 75, fraction_digits: 0) +} + +// CANONICALISATION STRIPS THE FRACTION'S TRAILING ZEROS AND NOTHING ELSE. 300 must stay 300: the +// loop that removes a zero after the point would change the number if it ran past it. +fn canonicalisation_does_not_reach_the_whole_part() -> Bool { + let three_hundred = canonical_exact_decimal(d: ExactDecimal { units: 300, fraction_digits: 0 }) + three_hundred.units == 300 && three_hundred.fraction_digits == 0 +} + +// THE EXPONENT FORM REFUSES INSTEAD OF BEING APPROXIMATED, and the refusal names which limit was +// hit rather than reporting the lexeme as unreadable digits -- those have different owners. +fn the_exponent_form_refuses_by_name() -> Bool { + match read_json_number_lexeme(lexeme: "1e3") { + JsonNumberOutsideExactFragment { lexeme, refusal } => + lexeme == "1e3" && match refusal { + JsonNumberUsesExponent => true + other => false + } + other => false + } +} + +fn the_capital_exponent_refuses_too() -> Bool { + match read_json_number_lexeme(lexeme: "1E3") { + JsonNumberOutsideExactFragment { lexeme, refusal } => true + other => false + } +} + +// 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 would send the repair to the wrong place. +fn a_quoted_number_is_not_a_number() -> Bool { + match read_json_number_value(v: json_string(s: "30")) { + JsonValueIsNotANumber => true + other => false + } +} + +// THE PROJECTION BACK OUT RENDERS THE VALUE, NOT THE AUTHORED BYTES, and says so by example: +// `30.0` reads in and `30` renders out. +fn the_wire_renders_the_canonical_value() -> Bool { + match read_json_number_lexeme(lexeme: "30.0") { + JsonNumberExact { value } => exact_decimal_wire(d: value) == "30" + other => false + } +} + +fn the_negative_wire_carries_its_sign_outside_the_whole_part() -> Bool { + match read_json_number_lexeme(lexeme: "-0.5") { + JsonNumberExact { value } => exact_decimal_wire(d: value) == "-0.5" + other => false + } +} + +// EQUALITY CANONICALISES ITS OWN ARGUMENTS, WHICH THE READING PATH ALONE CANNOT DISCRIMINATE. +// read_json_number_lexeme returns a canonical value, so two numerals compared through it are +// already reduced before the comparison sees them -- deleting the reduction inside +// exact_decimal_equal leaves every conjunct above green. These two values are built by hand at the +// same number in two representations, which is the only way to reach that reduction. +fn equality_reduces_values_it_was_handed_unreduced() -> Bool { + exact_decimal_equal( + a: ExactDecimal { units: 300, fraction_digits: 1 }, + b: ExactDecimal { units: 30, fraction_digits: 0 }, + ) +} + +fn unreduced_equality_still_separates_different_numbers() -> Bool { + !exact_decimal_equal( + a: ExactDecimal { units: 305, fraction_digits: 1 }, + b: ExactDecimal { units: 30, fraction_digits: 0 }, + ) +} + +// AN EXPONENT-FREE NUMERAL TOO LARGE FOR THE CARRIER IS NAMED AS A MAGNITUDE LIMIT, NOT AS +// UNREADABLE DIGITS. The lexeme is perfectly well-formed JSON and its digits are perfectly +// readable; what it exceeds is this fragment's carrier, and the two facts have different owners. +fn an_oversized_coefficient_names_the_carrier_limit() -> Bool { + match read_json_number_lexeme(lexeme: "123456789012345678901234567890") { + JsonNumberOutsideExactFragment { lexeme, refusal } => + match refusal { + JsonNumberMagnitudeOutsideCarrierRange => true + other => false + } + other => false + } +} + +fn json_exact_number_witness() -> ProcessExit { + if the_two_spellings_of_thirty_agree() + && two_different_numbers_still_differ() + && the_deployed_coefficients_read_exactly() + && canonicalisation_does_not_reach_the_whole_part() + && the_exponent_form_refuses_by_name() + && the_capital_exponent_refuses_too() + && a_quoted_number_is_not_a_number() + && the_wire_renders_the_canonical_value() + && the_negative_wire_carries_its_sign_outside_the_whole_part() + && equality_reduces_values_it_was_handed_unreduced() + && unreduced_equality_still_separates_different_numbers() + && an_oversized_coefficient_names_the_carrier_limit() { + ExitSuccess + } else { + exit_failure(reason: "JSON exact number reading: canonical equality across spellings, the deployed coefficients, or the exponent refusal changed") + } +} diff --git a/dag/gunbc/json_member_conservation_witness.dag b/dag/gunbc/json_member_conservation_witness.dag new file mode 100644 index 00000000000..99abc7bd25a --- /dev/null +++ b/dag/gunbc/json_member_conservation_witness.dag @@ -0,0 +1,208 @@ +module gunbc.json_member_conservation_witness + +import std.types { Bool, Int, List, String } +import std.process { ProcessExit, ExitSuccess, exit_failure } +import extdeps.languages.json.emit { JsonKeyValue, JsonNumber, JsonString, JsonValue, json_object } +import extdeps.languages.json.parse { JsonDocumentParsed, parse_json_document } +import extdeps.languages.json.member_conservation { + ConservationVerdict, + JsonMemberOccurrence, + MemberConsumed, + MemberDefective, + MemberDispositionedTwice, + MemberForeignToObject, + PartitionSourcePathMismatch, + MemberLost, + MemberUnmodeled, + MembersConserved, + ObjectMemberPartition, + conservation_verdict, + occurrences_of_object, +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// A FAN PID ENTRY WITH A VENDOR EXTENSION THE DECODER DOES NOT MODEL, and a duplicated identity +// field. Both shapes occur in real OpenBMC configurations and both are legal JSON, which is why the +// partition has to carry them rather than the parser rejecting them. +data subject_text: String = "\{\"name\": \"CHASSIS\", \"type\": \"fan\", \"type\": \"stepwise\", \"vendorExtension\": 7\}" + +data subject: JsonValue = match parse_json_document(s: subject_text) { + JsonDocumentParsed { value } => value + other => json_object(members: []) +} + +data subject_occurrences: List = occurrences_of_object(object_path: "zones[0].pids[1]", value: subject) + +fn nth(occurrences: List, ordinal: Int) -> JsonMemberOccurrence { + filter(occurrences, occurrence => occurrence.identity.ordinal == ordinal).first() +} + +// FOUR MEMBERS, FOUR DISPOSITIONS: name consumed, both "type" occurrences carried separately -- one +// consumed and one defective, because a duplicated identity field is not a harmless unknown -- and +// the vendor extension retained as unmodelled. +data honest_partition: ObjectMemberPartition = ObjectMemberPartition { + object_path: "zones[0].pids[1]", + source: subject_occurrences, + dispositions: [ + MemberConsumed { occurrence: nth(occurrences: subject_occurrences, ordinal: 0), role: "controller_name" }, + MemberConsumed { occurrence: nth(occurrences: subject_occurrences, ordinal: 1), role: "controller_type" }, + MemberDefective { occurrence: nth(occurrences: subject_occurrences, ordinal: 2), cause: "identity field duplicated" }, + MemberUnmodeled { occurrence: nth(occurrences: subject_occurrences, ordinal: 3) }, + ], +} + +fn the_honest_partition_conserves() -> Bool { + match conservation_verdict(partition: honest_partition) { + MembersConserved { member_count } => member_count == 4 + other => false + } +} + +// THE SUBSTITUTION A COUNT-BASED CHECK PASSES, WHICH IS WHY THIS MODULE EXISTS. The unmodelled +// vendor extension at ordinal 3 is dropped, and the member at ordinal 1 is classified twice. Four +// dispositions for four source members -- every count agrees, one member is unaccounted for, and +// another is claimed by two branches at once. +data substituted_partition: ObjectMemberPartition = ObjectMemberPartition { + object_path: "zones[0].pids[1]", + source: subject_occurrences, + dispositions: [ + MemberConsumed { occurrence: nth(occurrences: subject_occurrences, ordinal: 0), role: "controller_name" }, + MemberConsumed { occurrence: nth(occurrences: subject_occurrences, ordinal: 1), role: "controller_type" }, + MemberConsumed { occurrence: nth(occurrences: subject_occurrences, ordinal: 1), role: "controller_type_again" }, + MemberDefective { occurrence: nth(occurrences: subject_occurrences, ordinal: 2), cause: "identity field duplicated" }, + ], +} + +fn the_substitution_is_caught_and_named() -> Bool { + let counts_agree = + substituted_partition.dispositions.length() == substituted_partition.source.length() + let caught = match conservation_verdict(partition: substituted_partition) { + MemberDispositionedTwice { object_path, ordinal, times } => ordinal == 1 && times == 2 + other => false + } + counts_agree && caught +} + +// A MEMBER NOBODY ACCOUNTED FOR. The vendor extension is simply absent from the partition, which is +// the ordinary silent-drop this wall exists to stop. +data lossy_partition: ObjectMemberPartition = ObjectMemberPartition { + object_path: "zones[0].pids[1]", + source: subject_occurrences, + dispositions: [ + MemberConsumed { occurrence: nth(occurrences: subject_occurrences, ordinal: 0), role: "controller_name" }, + MemberConsumed { occurrence: nth(occurrences: subject_occurrences, ordinal: 1), role: "controller_type" }, + MemberDefective { occurrence: nth(occurrences: subject_occurrences, ordinal: 2), cause: "identity field duplicated" }, + ], +} + +fn a_dropped_member_is_named() -> Bool { + match conservation_verdict(partition: lossy_partition) { + MemberLost { object_path, ordinal } => object_path == "zones[0].pids[1]" && ordinal == 3 + other => false + } +} + +// AN OCCURRENCE FROM A DIFFERENT OBJECT, which is how a partition could otherwise be padded to +// cover a source member it never read. +data foreign_partition: ObjectMemberPartition = ObjectMemberPartition { + object_path: "zones[0].pids[1]", + source: [nth(occurrences: subject_occurrences, ordinal: 0)], + dispositions: [ + MemberConsumed { occurrence: nth(occurrences: subject_occurrences, ordinal: 0), role: "controller_name" }, + MemberUnmodeled { occurrence: nth(occurrences: subject_occurrences, ordinal: 3) }, + ], +} + +fn a_foreign_occurrence_is_named() -> Bool { + match conservation_verdict(partition: foreign_partition) { + MemberForeignToObject { object_path, occurrence_path, ordinal } => ordinal == 3 + other => false + } +} + +// DUPLICATE KEYS SURVIVE ENUMERATION AS SEPARATE OCCURRENCES. If they collapsed, the partition +// would have three source members for a four-member object and the duplicated identity field would +// be invisible. +fn duplicate_keys_are_separate_occurrences() -> Bool { + subject_occurrences.length() == 4 + && nth(occurrences: subject_occurrences, ordinal: 1).member.key == "type" + && nth(occurrences: subject_occurrences, ordinal: 2).member.key == "type" +} + +// THE CASE THE FIRST VERSION OF THIS WITNESS MISSED, AND IT IS THE COMMON ONE. The foreign +// disposition above is a foreign ORDINAL from the same object; every real document instead has +// many SIBLING objects that each carry an ordinal 0, an ordinal 1, and so on. Joining on the +// ordinal alone accepts a member of one PID entry as the corresponding member of its sibling -- +// which is the silent substitution this module exists to stop, committed one level down inside the +// module that stops it. +data sibling_occurrences: List = occurrences_of_object(object_path: "zones[0].pids[2]", value: subject) + +fn sibling_nth(ordinal: Int) -> JsonMemberOccurrence { + filter(sibling_occurrences, occurrence => occurrence.identity.ordinal == ordinal).first() +} + +// THIS OBJECT'S OWN MEMBERS ARE ALL ACCOUNTED FOR EXACTLY ONCE, and one extra disposition names an +// occurrence of the SIBLING object at an ordinal this object also has. Under a full-identity join +// that extra is foreign and is named as such. Under an ordinal-only join it is indistinguishable +// from a second claim on this object's ordinal 1 -- so the ordinal-only reading reports the wrong +// defect about the wrong object, which is how a decoder's cross-object substitution would have +// been described. +data sibling_substituted_partition: ObjectMemberPartition = ObjectMemberPartition { + object_path: "zones[0].pids[1]", + source: subject_occurrences, + dispositions: [ + MemberConsumed { occurrence: nth(occurrences: subject_occurrences, ordinal: 0), role: "controller_name" }, + MemberConsumed { occurrence: nth(occurrences: subject_occurrences, ordinal: 1), role: "controller_type" }, + MemberDefective { occurrence: nth(occurrences: subject_occurrences, ordinal: 2), cause: "identity field duplicated" }, + MemberUnmodeled { occurrence: nth(occurrences: subject_occurrences, ordinal: 3) }, + MemberUnmodeled { occurrence: sibling_nth(ordinal: 1) }, + ], +} + +fn a_sibling_object_cannot_satisfy_this_objects_obligation() -> Bool { + let ordinals_all_present = + sibling_occurrences.length() == subject_occurrences.length() + let caught = match conservation_verdict(partition: sibling_substituted_partition) { + MemberForeignToObject { object_path, occurrence_path, ordinal } => + object_path == "zones[0].pids[1]" && occurrence_path == "zones[0].pids[2]" && ordinal == 1 + other => false + } + ordinals_all_present && caught +} + +// THE PARTITION'S OWN PATH IS CHECKED AGAINST ITS SOURCE TOO, because it is a third authored copy +// of the same fact: without this a partition can name one object while every occurrence in it +// describes another, and the identity join then holds perfectly -- about something else. +data mislabelled_partition: ObjectMemberPartition = ObjectMemberPartition { + object_path: "zones[0].pids[9]", + source: subject_occurrences, + dispositions: [ + MemberConsumed { occurrence: nth(occurrences: subject_occurrences, ordinal: 0), role: "controller_name" }, + MemberConsumed { occurrence: nth(occurrences: subject_occurrences, ordinal: 1), role: "controller_type" }, + MemberDefective { occurrence: nth(occurrences: subject_occurrences, ordinal: 2), cause: "identity field duplicated" }, + MemberUnmodeled { occurrence: nth(occurrences: subject_occurrences, ordinal: 3) }, + ], +} + +fn a_partition_labelled_for_another_object_is_named() -> Bool { + match conservation_verdict(partition: mislabelled_partition) { + PartitionSourcePathMismatch { partition_path, occurrence_path, ordinal } => + partition_path == "zones[0].pids[9]" && occurrence_path == "zones[0].pids[1]" + other => false + } +} + +fn json_member_conservation_witness() -> ProcessExit { + if the_honest_partition_conserves() + && the_substitution_is_caught_and_named() + && a_dropped_member_is_named() + && a_foreign_occurrence_is_named() + && duplicate_keys_are_separate_occurrences() + && a_sibling_object_cannot_satisfy_this_objects_obligation() + && a_partition_labelled_for_another_object_is_named() { + ExitSuccess + } else { + exit_failure(reason: "JSON member conservation: the identity join, the substitution catch, or duplicate-key occurrence separation changed") + } +} diff --git a/dag/gunbc/pid_control_curve_decode_witness.dag b/dag/gunbc/pid_control_curve_decode_witness.dag new file mode 100644 index 00000000000..3add4f46a5b --- /dev/null +++ b/dag/gunbc/pid_control_curve_decode_witness.dag @@ -0,0 +1,240 @@ +module gunbc.pid_control_curve_decode_witness + +import std.types { Bool, Int, List, String } +import std.process { ProcessExit, ExitSuccess, exit_failure } +import std.decimal { exact_decimal_wire } +import std.measure { measure_count } +import extdeps.languages.json.emit { JsonValue, json_object } +import extdeps.languages.json.parse { JsonDocumentParsed, parse_json_document } +import extdeps.bmc.pid_control_program { DemandCurvePoint } +import extdeps.bmc.pid_control_decode { + CurveDecoded, + CurveKeyDuplicated, + CurveKeyNotCanonical, + CurveKeyNotAnIndex, + CurveOutputWithoutReading, + CurveReadingWithoutOutput, + CurveRefused, + CurveSideMissing, + CurveValueNotANumber, + CurveValueOutsideExactFragment, + OutputSide, + ReadingSide, + decode_curve, + document_path, +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +fn parsed(text: String) -> JsonValue { + match parse_json_document(s: text) { + JsonDocumentParsed { value } => value + other => json_object(members: []) + } +} + +// THE CURVE THE FLEET IS ACTUALLY RUNNING, copied from the captured srv3 document. Nine points, +// authored in ascending order, temperatures against fan demand percentages. +data deployed_curve_text: String = "\{\"reading\": \{\"0\": 40, \"1\": 55, \"2\": 62, \"3\": 66, \"4\": 70, \"5\": 74, \"6\": 78, \"7\": 82, \"8\": 85\}, \"output\": \{\"0\": 22, \"1\": 30, \"2\": 38, \"3\": 44, \"4\": 52, \"5\": 62, \"6\": 75, \"7\": 88, \"8\": 100\}\}" + +fn decoded_points(text: String) -> List { + match decode_curve(container: parsed(text: text), path: document_path(text: "zones[0].pids[2].pid")) { + CurveDecoded { points } => points + other => [] + } +} + +fn point_at(points: List, index: Int) -> List { + filter(points, p => p.index == index) +} + +fn the_deployed_curve_decodes_paired() -> Bool { + let points = decoded_points(text: deployed_curve_text) + let third = point_at(points: points, index: 3) + points.length() == 9 + && third.length() == 1 + && exact_decimal_wire(d: measure_count(m: third.first().reading)) == "66" + && exact_decimal_wire(d: third.first().output.magnitude) == "44" +} + +// PAIRING IS BY KEY IDENTITY, NOT BY POSITION, and this is the discriminator that proves it: the +// output object is authored in a different member order from the reading object. Under positional +// pairing 66 would take 100 rather than 44, which is the difference between a quiet fan and a loud +// one at the same temperature. +data reordered_output_curve_text: String = "\{\"reading\": \{\"0\": 40, \"1\": 55, \"2\": 62, \"3\": 66\}, \"output\": \{\"3\": 44, \"2\": 38, \"1\": 30, \"0\": 22\}\}" + +fn pairing_survives_a_reordered_output_object() -> Bool { + let points = decoded_points(text: reordered_output_curve_text) + let third = point_at(points: points, index: 3) + let zeroth = point_at(points: points, index: 0) + points.length() == 4 + && third.length() == 1 + && exact_decimal_wire(d: third.first().output.magnitude) == "44" + && zeroth.length() == 1 + && exact_decimal_wire(d: zeroth.first().output.magnitude) == "22" +} + +// A NON-CANONICAL KEY IS NOT AN INDEX THE DAEMON ASKS FOR. phosphor-pid-control requests the exact +// key it computes from an integer position, so "01" is a key it never looks up; reading it as +// index 1 would report a curve point the running system does not load. +data noncanonical_curve_text: String = "\{\"reading\": \{\"0\": 40, \"01\": 62\}, \"output\": \{\"0\": 22, \"01\": 38\}\}" + +fn a_noncanonical_key_refuses_and_names_the_canonical_spelling() -> Bool { + match decode_curve(container: parsed(text: noncanonical_curve_text), path: document_path(text: "p")) { + CurveRefused { refusal } => + match refusal { + CurveKeyNotCanonical { path, side, key, canonical } => key == "01" && canonical == "1" + other => false + } + other => false + } +} + +// THE HOLE THE INTEGER-NORMALISING JOIN LEFT OPEN, AND THE REASON THIS DECODE WAS REWRITTEN. One +// member on each side, so no within-side duplicate exists; both normalise to 1; the two paired +// across key sets that do not agree. Measured before the change, this document decoded to a curve +// point. +data cross_side_normalisation_text: String = "\{\"reading\": \{\"1\": 55\}, \"output\": \{\"01\": 30\}\}" + +fn keys_that_only_agree_after_normalisation_do_not_pair() -> Bool { + match decode_curve(container: parsed(text: cross_side_normalisation_text), path: document_path(text: "p")) { + CurveRefused { refusal } => true + other => false + } +} + +// THE SAME POPULATION IN A DIFFERENT MEMBER ORDER IS THE SAME CURVE. The daemon loads by integer +// position, so a semantic program that changed because two members were reordered would be +// sensitive to a difference the running system does not have. +data reordered_reading_curve_text: String = "\{\"reading\": \{\"2\": 62, \"0\": 40, \"1\": 55\}, \"output\": \{\"0\": 22, \"1\": 30, \"2\": 38\}\}" + +fn member_order_does_not_change_the_semantic_curve() -> Bool { + let points = decoded_points(text: reordered_reading_curve_text) + points.length() == 3 + && points.first().index == 0 + && exact_decimal_wire(d: measure_count(m: points.first().reading)) == "40" + && exact_decimal_wire(d: measure_count(m: points.skip(n: 2).first().reading)) == "62" +} + +// 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. +data annotated_curve_text: String = "\{\"reading\": \{\"0\": 40, \"comment\": 55\}, \"output\": \{\"0\": 22, \"comment\": 30\}\}" + +fn a_non_index_key_refuses_by_name() -> Bool { + match decode_curve(container: parsed(text: annotated_curve_text), path: document_path(text: "p")) { + CurveRefused { refusal } => + match refusal { + CurveKeyNotAnIndex { path, side, key } => key == "comment" + other => false + } + other => false + } +} + +// THE JOIN RUNS IN BOTH DIRECTIONS, and these two fixtures are what separates a real join from a +// key-count comparison: each side has a key the other lacks, so the counts agree in the first +// fixture and the defect is real. +data reading_without_output_text: String = "\{\"reading\": \{\"0\": 40, \"1\": 55\}, \"output\": \{\"0\": 22, \"2\": 30\}\}" + +fn an_unpaired_reading_is_named_with_its_index() -> Bool { + let counts_agree = true + match decode_curve(container: parsed(text: reading_without_output_text), path: document_path(text: "p")) { + CurveRefused { refusal } => + match refusal { + CurveReadingWithoutOutput { path, index } => index == 1 + other => false + } + other => false + } +} + +data output_without_reading_text: String = "\{\"reading\": \{\"0\": 40\}, \"output\": \{\"0\": 22, \"7\": 30\}\}" + +fn an_unpaired_output_is_named_with_its_index() -> Bool { + match decode_curve(container: parsed(text: output_without_reading_text), path: document_path(text: "p")) { + CurveRefused { refusal } => + match refusal { + CurveOutputWithoutReading { path, index } => index == 7 + other => false + } + other => false + } +} + +data quoted_value_curve_text: String = "\{\"reading\": \{\"0\": \"40\"\}, \"output\": \{\"0\": 22\}\}" + +fn a_quoted_curve_value_refuses() -> Bool { + match decode_curve(container: parsed(text: quoted_value_curve_text), path: document_path(text: "p")) { + CurveRefused { refusal } => + match refusal { + CurveValueNotANumber { path, side, key } => key == "0" + other => false + } + other => false + } +} + +data exponent_value_curve_text: String = "\{\"reading\": \{\"0\": 4e1\}, \"output\": \{\"0\": 22\}\}" + +fn an_exponent_curve_value_refuses_as_outside_the_fragment() -> Bool { + match decode_curve(container: parsed(text: exponent_value_curve_text), path: document_path(text: "p")) { + CurveRefused { refusal } => + match refusal { + CurveValueOutsideExactFragment { path, side, key } => key == "0" + other => false + } + other => false + } +} + +data missing_output_side_text: String = "\{\"reading\": \{\"0\": 40\}\}" + +fn a_missing_side_refuses_and_names_which() -> Bool { + match decode_curve(container: parsed(text: missing_output_side_text), path: document_path(text: "p")) { + CurveRefused { refusal } => + match refusal { + CurveSideMissing { path, side } => + match side { + OutputSide => true + ReadingSide => false + } + other => false + } + other => false + } +} + +// RFC 8259 PERMITS A DUPLICATE MEMBER NAME AND DOES NOT SAY WHICH WINS, so a curve side carrying +// one is refused rather than resolved -- last-wins here would let a document carrying two values +// for one curve position read as whichever the writer put second. +data duplicate_key_curve_text: String = "\{\"reading\": \{\"0\": 40, \"0\": 62\}, \"output\": \{\"0\": 22\}\}" + +fn a_duplicated_exact_key_refuses() -> Bool { + match decode_curve(container: parsed(text: duplicate_key_curve_text), path: document_path(text: "p")) { + CurveRefused { refusal } => + match refusal { + CurveKeyDuplicated { path, side, key, occurrences } => key == "0" && occurrences == 2 + other => false + } + other => false + } +} + +fn pid_control_curve_decode_witness() -> ProcessExit { + if the_deployed_curve_decodes_paired() + && pairing_survives_a_reordered_output_object() + && a_noncanonical_key_refuses_and_names_the_canonical_spelling() + && keys_that_only_agree_after_normalisation_do_not_pair() + && member_order_does_not_change_the_semantic_curve() + && a_non_index_key_refuses_by_name() + && an_unpaired_reading_is_named_with_its_index() + && an_unpaired_output_is_named_with_its_index() + && a_quoted_curve_value_refuses() + && an_exponent_curve_value_refuses_as_outside_the_fragment() + && a_missing_side_refuses_and_names_which() + && a_duplicated_exact_key_refuses() { + ExitSuccess + } else { + exit_failure(reason: "phosphor-pid-control curve decode: key-identity pairing, the normalisation-collision refusal, or the two-directional join changed") + } +} diff --git a/dag/std/decimal.dag b/dag/std/decimal.dag index 928d11cba02..965dda62ffd 100644 --- a/dag/std/decimal.dag +++ b/dag/std/decimal.dag @@ -2,6 +2,7 @@ module std.decimal import std.types { String, Int, Bool } import std.render_repeat_string_bootstrap { repeat_string } +import std.bytes { pure_dag_seam_unreachable } data decimal_note: String = "Positional decimal notation for a FIXED-POINT magnitude: an integer paired with the power of ten it is scaled by. It exists because two unrelated boundaries needed the identical projection and neither is the right owner of it — WebAudio's gain and time arguments are decimal seconds and a linear amplitude in [0, 1], and CSS transform scale factors are decimal ratios. Each carried its magnitude integrally upstream (a fractional literal in a .dag row would be a second representation of the same number), so each needed to divide exactly once, at its own wire. Giving each boundary its own formatter would have put the same numeral logic in two places for no reason other than that the two consumers are far apart in the layer graph, which is the horizontal redundancy DESIGN section 2 names — the concept is one, so it is modeled once and both uses derive. @@ -40,3 +41,98 @@ fn fixed_point_wire(value: Int, decimals: Int) -> String { fn fixed_point_domain_ok(value: Int, decimals: Int) -> Bool { value >= 0 && decimals >= 0 } + +// A SIGNED EXACT DECIMAL, ADDED BECAUSE A CONSUMER NEEDED TO COMPARE TWO NUMERALS RATHER THAN +// RENDER ONE. Everything above this line projects an integer OUT to a wire. The reader that +// prompted this needs the other direction and a further step: two captured configuration documents +// write the same coefficient as `30` and as `30.0`, and a consumer asking whether the two programs +// agree must answer yes. Comparing lexemes answers no, so the lexeme is not the value. +// +// The carrier is `units / 10^fraction_digits`, which is exact for the whole of RFC 8259's +// number production minus its exponent form -- no rounding, no binary floating point, so a +// comparison is a comparison of the authored number and not of an approximation of it. A float +// carrier would have made `0.1` and its own nearest double indistinguishable, which is precisely +// the fabricated-plausible-output failure at the point where the question is whether two documents +// AGREE. +// +// SIGN IS ADMITTED HERE AND IS NOT ADMITTED ABOVE, which is a real difference and not an oversight +// in either place: fixed_point_wire's domain note records that a negative value would render its +// sign inside the whole part, and that stays true, so this type renders through its own projection +// that splits the sign off first. The deployed program this was built for carries `-8.0` and +// `-0.5`, so the negative case is the ordinary one, not an edge. +type ExactDecimal { + units: Int + fraction_digits: Int where range(min: 0) +} + +// WHAT THE REFINEMENT ABOVE ACTUALLY BUYS, STATED HONESTLY BECAUSE IT IS LESS THAN IT LOOKS. A +// literal `fraction_digits: -1` refuses at resolve; a COMPUTED negative reaches the field and is +// held. So this is mechanically preventable at authored sites and not structurally impossible, and +// every fn below that produces an ExactDecimal is responsible for its own non-negative argument. +// Next-rung trigger: feature:where-refinement-predicate-coproduct, the same one std.content_hash +// names for its non-literal digest positions. +data exact_decimal_refinement_rung_note: String = "ExactDecimal.fraction_digits carries where range(min: 0), which refuses an authored negative literal at resolve and does not refuse a computed one. Mechanically preventable, not structural; measured on the same partial-wall behaviour recorded for PositiveFanCount in gunbc.fleet_fan_wiring. Because the wall is partial, every producer routes through admit_exact_decimal below and the canonicaliser DIVERGES rather than reinterpreting a negative scale." + +// THE MINT, AND WHY THE CANONICALISER NO LONGER ABSORBS A NEGATIVE SCALE. The first version of +// this 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 is otherwise built to prevent, produced by the very function meant to +// make comparison exact. Found in review of gunbc#9491. +// +// So the domain is enforced where a value is BUILT rather than assumed where it is read. The +// canonicaliser's negative arm diverges through the std seam, which is the honest projection for +// a state the mint cannot produce: it does not return a plausible number, and it does not pretend +// the arm is unreachable by omitting it. +type ExactDecimalAdmission + = ExactDecimalAdmitted { canonical: ExactDecimal } + | ExactDecimalScaleRefused { observed_fraction_digits: Int } + +fn admit_exact_decimal(units: Int, fraction_digits: Int) -> ExactDecimalAdmission { + if fraction_digits < 0 { + ExactDecimalScaleRefused { observed_fraction_digits: fraction_digits } + } else { + ExactDecimalAdmitted { + canonical: canonical_exact_decimal(d: ExactDecimal { units: units, fraction_digits: fraction_digits }), + } + } +} + +// CANONICALISATION IS WHAT MAKES EQUALITY MEAN AGREEMENT. 30 and 30.0 are the same number written +// two ways, so they must reduce to one representation before any comparison or digest sees them. +// The reduction strips trailing zeros from the FRACTION only -- 300 with no fraction stays 300, +// because dropping a zero there would change the number rather than its spelling. +fn canonical_exact_decimal(d: ExactDecimal) -> ExactDecimal { + if d.fraction_digits < 0 { + ExactDecimal { units: pure_dag_seam_unreachable(), fraction_digits: 0 } + } else if d.fraction_digits == 0 { + ExactDecimal { units: d.units, fraction_digits: 0 } + } else if d.units - ((d.units / 10) * 10) == 0 { + canonical_exact_decimal(d: ExactDecimal { units: d.units / 10, fraction_digits: d.fraction_digits - 1 }) + } else { + d + } +} + +// ZERO IS THE ONE CASE THE TRAILING-ZERO RULE ABOVE DOES NOT FINISH ON ITS OWN, and it is worth +// its own arm rather than a comment: 0 with three fraction digits reduces by the loop to 0 with +// zero fraction digits, which is right -- but 0 units with 0 fraction digits and a units value of +// -0 are indistinguishable in Int, so no separate negative-zero case exists to reconcile. +fn exact_decimal_equal(a: ExactDecimal, b: ExactDecimal) -> Bool { + let ca = canonical_exact_decimal(d: a) + let cb = canonical_exact_decimal(d: b) + ca.units == cb.units && ca.fraction_digits == cb.fraction_digits +} + +// THE PROJECTION BACK TO A NUMERAL, WHICH IS NOT THE LEXEME IT WAS READ FROM AND DOES NOT CLAIM TO +// BE. It renders the canonical form, so `30.0` reads in and `30` renders out. That is a round-trip +// of the VALUE, never of the bytes; a consumer needing the authored bytes keeps the lexeme. +fn exact_decimal_wire(d: ExactDecimal) -> String { + let c = canonical_exact_decimal(d: d) + if c.units < 0 { + join(["-", fixed_point_wire(value: 0 - c.units, decimals: c.fraction_digits)], "") + } else { + fixed_point_wire(value: c.units, decimals: c.fraction_digits) + } +} diff --git a/docs/plans/compiler-guarantee-recovery-gap-analysis.md b/docs/plans/compiler-guarantee-recovery-gap-analysis.md index 43bb95ed911..3bfd680158d 100644 --- a/docs/plans/compiler-guarantee-recovery-gap-analysis.md +++ b/docs/plans/compiler-guarantee-recovery-gap-analysis.md @@ -1263,6 +1263,53 @@ enforces end to end. ## 11. Audit queue +0. **Optional payload member `value` shadows an unwrapped record field, and the resulting + record is then accepted in an `Int` context.** Filed 2026-08-27 from gunbc#9491, where it + silently made every decoded fan-curve output carry the entry record instead of its + magnitude. **The class is two questions and the eventual owner must not collapse them**, + because only the second is unambiguously a defect. + + **(1) Member-selection policy.** `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 field access through an optional auto-unwraps for every + spelling EXCEPT `value`, which selects the optional's own payload. Two accesses on one + expression resolve against two different carriers, decided by the field's name, with no + diagnostic. Whether that should select the payload, unwrap to the record's field, or refuse + as ambiguous is a language-semantics decision, not obviously a bug. + + **(2) Type conformance, and this half is below floor independently of (1).** Whichever + member selection is chosen, a record-valued expression must not be accepted where an `Int` + is required. It is: measured on a local record `Boxed { tag: Int, value: Int }`, the whole + of `boxes.first().value == 99` resolves clean, evaluates, and answers false — placing a + `Boxed` against an `Int`. That is DESIGN's own floor clause ("values inhabit declared + types") failing silently. + + MINIMAL REPRODUCTION, WITH ITS CONTROL, kept inline rather than as 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: + + ``` + type Boxed { tag: Int, value: Int } + data boxes: List = [Boxed { tag: 1, value: 99 }] + + boxes.first().tag -> 1 // control: auto-unwraps to the record's field + boxes.first().value -> Boxed // the payload, not the field; no diagnostic + boxes.first().value == 99 // resolves clean, evaluates false: record vs Int + ``` + + OWNER SEAM: `v1.compiler.infer_lookup` `field_summary_for_type` and `lookup_field_type_node` + for (1); the downstream expression-conformance path for (2). + CURRENT RUNG: **below floor**, on the measured source→interpretation path. Not a ladder + position — a silent wrong answer, which §4b places outside the ladder entirely. + WORKAROUND IN USE: avoid `value` as a record field name where the record is reached through + an optional. `extdeps.bmc.pid_control_decode` renames its field to `magnitude` on exactly + this ground and claims no compiler guarantee. + NEXT TRIGGER: the selection policy in (1) decided, and an executing compiler-floor witness + enrolled for (2) — which does not depend on (1) and can land first. + NOT ENROLLED as `floor_expected_red`: that roster's rows are executing failures somebody is + actively repairing, and this has no repair owner yet. Enrolling it would use the roster as + an ownerless defect backlog, which its own contract refuses. + 1. ~~Recover `docs/error-examples.md`~~ **DONE — see §8b**; ~~`correctness-dimensions`~~ **DONE — see §8c.** Still to pull: `what-falls-out`, `two-groundings`, `the-derived-homomorphism`.