diff --git a/dag/extdeps/boards/asrock_rack.dag b/dag/extdeps/boards/asrock_rack.dag index 8762f65df7e..a8fe0d9da2a 100644 --- a/dag/extdeps/boards/asrock_rack.dag +++ b/dag/extdeps/boards/asrock_rack.dag @@ -31,9 +31,13 @@ import extdeps.firmware.types { InstantFlashRom, firmware_semantic_version, } -import std.measure { ByteSize, MegatransfersPerSecond, byte_size, celsius, megatransfers_per_second, percent, positive_celsius_delta, positive_measure_count } -import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef } +import std.measure { Micrometer, micrometer, ByteSize, MegatransfersPerSecond, byte_size, celsius, megatransfers_per_second, percent, positive_celsius_delta, positive_measure_count } +import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef, FactCitation } +import std.coordinate_frame { CoordinateFrameIdentity, coordinate_frame_identity } +import std.affine_space { point2 } +import std.orthogonal_geometry { AxisAlignedRectangle2, OrthogonalConstruction, axis_aligned_rectangle2 } import std.decl_ref { DeclarationRef, WholeDeclaration } +import extdeps.standards.micro_atx { MountingLocationId, LocB, LocC, LocF, LocH, LocJ, LocL, LocM, LocR, LocS } import extdeps.cpu.types { CpuSocket } import extdeps.cpu.ampere { ampere_lga4926_socket } import extdeps.uri { Uri, Https } @@ -571,3 +575,325 @@ data asrock_altrad8ud_1l2t_mechanical: AsrockAltrad8ud1l2tMechanical = AsrockAlt } data asrock_altrad8ud_channel_note: NonEmptyStr = "Eight DIMM slots at one DIMM per channel on the vendor page - the board exposes eight of the SoC's memory channels, so the one-DIMM-per-channel population IS the full population; there is no second-DIMM headroom on this platform, unlike the 16-slot dual-socket boards and the 32-slot 2DPC systems." + +// --------------------------------------------------------------------------------------------- +// BOARD GEOMETRY, read first-party from the vendor manual this module already cites. +// +// PROVENANCE, stated before the numbers because it is the fact that decides how they may be used. +// extdeps_external_authority_anchor names download.asrock.com/Manual/ALTRAD8UD-1L2T.pdf. That +// document was FETCHED AND READ by the authoring session — download.asrock.com answers 200 from +// this environment, unlike the general web, which is refused — so these are a first-party read of +// the manual and not the relayed grade extdeps.climbing_holds.atomik is stamped with. Section 1.4 +// "Motherboard Layout" carries the outline as leader dimensions: 26.7 cm (10.5 in) by 24.4 cm +// (9.6 in). +// +// WHAT THIS REPLACES. asrock_altrad8ud_1l2t_mechanical carries form_factor_label, a String reading +// "deep micro-ATX (9.6 x 10.5 in)". That row states a MEASUREMENT in prose, which DESIGN §4c names +// as the thing a typed carrier must hold instead — a String cannot be asked whether a chassis panel +// clears the board. The label is left standing because it also carries a FORM-FACTOR CLAIM, which +// is a different fact from an outline and is not established by these two lengths. +// +// THE AXES, AND AN ERROR THIS FILE SHIPPED ONCE. The board is 244 mm ALONG THE REAR I/O EDGE and +// 267 mm DEEP: the manual prints 24.4 cm (9.6 in) and 26.7 cm (10.5 in), and the vendor calls the +// form factor "deep micro-ATX (9.6 x 10.5 in)". +// +// An earlier revision transposed these and asserted the board was 267 mm WIDE against micro-ATX's +// 244 mm, concluding that a micro-ATX hole pattern would be laid out 23 mm too narrow. That was +// backwards and the conclusion inverts. The board is 244 mm along the rear I/O edge — the micro-ATX +// width exactly — and deeper. The error mattered: it is the difference between "the standard pattern +// does not apply" and "the standard pattern applies except at known positions". +// +// THIS PARAGRAPH CARRIED THREE DEAD CLAIMS UNTIL THE STANDARD SPLIT FORCED THEM INTO VIEW, and they +// are recorded because the way they survived is more instructive than any of them. +// +// It cited `extdeps.standards.atx_2_2 deep_micro_atx_axis_note`, a symbol DELETED earlier in this +// same program. It said that module "deliberately does not supply that grid", which became false the +// moment the grid was added. And it repeated the retracted claim that the FRONT ROW MOVES OUTWARD BY +// THE EXTRA 0.9 IN — retracted in the standard module hours before, and still asserted here. +// +// All three are the same failure: a correction was applied where it was pointed out and the CLASS +// was treated as closed. The front row does not move. 8.950 in is measured from Datum B, itself +// 0.400 in from the edge, so L and M sit at 9.350 in on a deep board and a standard-depth board +// alike; the extra depth extends the board PAST them, which is what the front-overhang row records. +// +// The outline is still NOT a conformance claim. Matching two edge dimensions is not the same as +// carrying the specification's hole grid, and populating that grid is not envelope conformance +// either — extdeps.standards.micro_atx records why those are separate claims. +// --------------------------------------------------------------------------------------------- +fn asrock_altrad8ud_board_frame() -> CoordinateFrameIdentity { coordinate_frame_identity(occurrence: 31) } + +// Micrometres, for the reason std.spatial_frame records and extdeps.printing.fdm repeats: the +// quantum is chosen from the smallest distinction the frame must preserve, not from the largest +// value it must hold. Whole millimetres are sufficient for these two extents and are NOT sufficient +// for what will be drawn in this frame next — DIMM slot pitch and standoff positions — and a frame +// whose quantum is retro-fitted after coordinates exist in it silently rescales every one of them. +// x is ALONG THE REAR I/O EDGE, y is DEPTH FROM THAT EDGE. The axis assignment is stated here +// because the frame carries no axis names and the numbers alone do not disclose which is which — +// which is exactly how the transposition above survived review the first time. +// +// THE EXTENTS ARE THE INCH FIGURES CONVERTED EXACTLY, NOT THE ROUNDED MILLIMETRES, and an earlier +// revision got this wrong in a way that produced a live contradiction inside this one module. +// +// The vendor states 9.6 x 10.5 in and presents 244 x 267 mm beside it. Those mm are rounded: the +// exact conversions are 243.840 and 266.700. The earlier outline carried 244000 and 267000 µm while +// asrock_altrad8ud_front_overhang below carried 29210 µm, which derives from 266700 − 237490. So the +// module asserted a depth of 267000 and an overhang computed from 266700, disagreeing by 300 µm — +// both spellings treated as exact in different rows, which is the same defect this session had +// already fixed once in extdeps.standards.atx_2_2 and failed to sweep for here. +// +// One representation owns it, and it is the exact one: a micrometre frame can hold 243840 and +// 266700 losslessly, so there is no reason to spend precision on a presentational rounding. The +// overhang is now derivable from the rows above it rather than merely consistent with them, and +// w_the_overhang_derives_from_the_outline asserts exactly that subtraction. +fn asrock_altrad8ud_board_outline() -> OrthogonalConstruction { + axis_aligned_rectangle2( + min: point2(frame: asrock_altrad8ud_board_frame(), x: 0, y: 0), + max: point2(frame: asrock_altrad8ud_board_frame(), x: 243840, y: 266700) + ) +} + +data asrock_altrad8ud_board_outline_citation: FactCitation = FactCitation { + fact: DeclarationRef { + module_path: "extdeps.boards.asrock_rack", + decl_name: "asrock_altrad8ud_board_outline", + field: WholeDeclaration + }, + authority: extdeps_external_authority_anchor +} + +// THE MOUNTING-HOLE POSITION IS SUPPLIED, AND WHAT IS REFUSED IS NARROWER THAN IT ONCE WAS. +// +// This paragraph previously said "THE MOUNTING HOLES ARE NOT HERE, AND THEIR ABSENCE IS THE POINT", +// that the module "refuses to hold them rather than deriving them from the micro-ATX pattern", and +// that deriving them "would place standoffs against a 244 mm-wide pattern on a 267 mm-wide board". +// By the time it was read, all three were false: the correspondence roster below supplies exactly +// which standard locations this board populates, and the 267-mm-wide clause is the AXIS +// TRANSPOSITION that was retracted in two other modules while surviving verbatim here. The board is +// 244 mm along the rear I/O edge and 266.700 mm deep. +// +// IT WAS CITED BY A REVIEW AS EVIDENCE OF DISCIPLINE, which is the part worth recording. A stale +// annotation does not merely rot quietly; it is read, and a refusal that no longer holds gets +// counted as a wall. That is strictly worse than no annotation, because it earns credit for a +// property the module does not have. This is the fourth stale-claim instance in this program and the +// class is the same each time: the correction is applied where it was pointed out and the CLASS is +// treated as closed. A retraction is not done until the retracted WORDING is swept for. +// +// WHAT IS ACTUALLY REFUSED, stated at the grain that is still true: the exact hole positions on THIS +// PHYSICAL BOARD are not measured. Section 1.4 draws the standoffs as unlabelled circles and +// dimensions none of them, so the manual establishes no coordinate. What the roster below carries is +// a CORRESPONDENCE -- which named standard location each drawn hole is -- inferred from a to-scale +// figure and discharged physically at FIT. The standard's coordinates are exact and are +// extdeps.standards.micro_atx's; the claim that this board sits on them is an inference; and the +// board's own hole diameter and underside keep-outs remain unmeasured, which is what +// asrock_altrad8ud_open_mounting_unknowns enumerates. +// +// The absorbing fallback the old paragraph warned about is still a real hazard and is still refused: +// substituting the nearby standard for a measurement nobody took. The difference is that the refusal +// now sits on the product-specific facts that are genuinely absent, rather than on a grid that this +// module does supply. + +data asrock_altrad8ud_standoff_figure_authority: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "drive.google.com/file/d/1z36tmUWAwOwXWy6ASmaPWJNzKoZggBs8/view" + } +} + +// WHAT IS KNOWN about a standard location on this specific board. Every arm names its evidence +// route, so the grade is readable from the constructor rather than from prose beside it. +type BoardLocationStanding + = HoleCorrespondenceInferred + | HoleAbsenceExplicitlyDirected + | HoleNotObservedInDrawing + | HolePhysicallyConfirmedPresent + | HolePhysicallyConfirmedAbsent + +// WHY a location must stay empty. Distinct from the standing that established it. +type StandoffProhibitionCause + = ProductSaysRemove + | NoAdmittedBoardHole + +// WHAT IS DONE at a standard location by a chassis built for this board. +type StandoffPlacementDecision + = StandoffAdmitted + | StandoffProhibited { cause: StandoffProhibitionCause } + +// The join, and the reason the two types are worth separating: this is total, so a new standing arm +// cannot be added without deciding what a chassis does about it. FIT will add exactly that — the +// physically-confirmed arms below are unpopulated today and are the shape the measurement lands in. +fn standoff_placement(standing: BoardLocationStanding) -> StandoffPlacementDecision { + match standing { + HoleCorrespondenceInferred => StandoffAdmitted + HolePhysicallyConfirmedPresent => StandoffAdmitted + HoleAbsenceExplicitlyDirected => StandoffProhibited { cause: ProductSaysRemove } + HoleNotObservedInDrawing => StandoffProhibited { cause: NoAdmittedBoardHole } + HolePhysicallyConfirmedAbsent => StandoffProhibited { cause: NoAdmittedBoardHole } + } +} + +type BoardStandardLocationCorrespondence sole_constructor { + location: MountingLocationId + standing: BoardLocationStanding +} + +fn board_location_correspondence( + location: MountingLocationId, + standing: BoardLocationStanding, +) -> BoardStandardLocationCorrespondence { + BoardStandardLocationCorrespondence { location: location, standing: standing } +} + +// Coordinates are deliberately ABSENT from these rows. A correspondence names a location; the +// location owns its position. Copying the coordinates here would fork the grid — the exact defect +// this session already paid for once, where the coupon's holes were computed a second time instead +// of being read from the ladder that defined them. +// HOW THE CORRESPONDENCE BELOW WAS ESTABLISHED, and its exact strength. +// +// A scale reading of the section 1.4 motherboard-layout figure over the operator-supplied grid +// overlay cited above. The figure is to scale: its measured outline aspect ratio agrees with +// 10.5/9.6 to within a thousandth, which is the check that makes reading positions off it legitimate +// at all. Seven marked holes then land on micro-ATX grid values, J is marked on the figure as a +// standoff to remove, and S is not drawn. +// +// What that establishes is WHICH standard locations this board populates. It does NOT establish the +// coordinates — those are the standard's — and it is not a vendor statement of conformance. The +// aspect-ratio agreement is deliberately not carried as a datum: it was a one-off sanity check with +// no instrument behind it, and DESIGN section 6 says a number worth re-deriving is worth an entry +// point while one that is not is not an instrument at all. +data asrock_altrad8ud_standard_location_correspondence: List = [ + board_location_correspondence(location: LocF, standing: HoleCorrespondenceInferred), + board_location_correspondence(location: LocM, standing: HoleCorrespondenceInferred), + board_location_correspondence(location: LocC, standing: HoleCorrespondenceInferred), + board_location_correspondence(location: LocH, standing: HoleCorrespondenceInferred), + board_location_correspondence(location: LocL, standing: HoleCorrespondenceInferred), + board_location_correspondence(location: LocB, standing: HoleCorrespondenceInferred), + board_location_correspondence(location: LocR, standing: HoleCorrespondenceInferred), + board_location_correspondence(location: LocJ, standing: HoleAbsenceExplicitlyDirected), + board_location_correspondence(location: LocS, standing: HoleNotObservedInDrawing), +] + + +// THE DEEP EXTENSION, and the cassette requirement that falls out of it. +// +// The front mounting row L/M sits at 9.350 in from the rear edge — the ORDINARY micro-ATX position, +// not a moved one. An earlier revision of this file claimed the extra depth pushed that row outward +// from a nominal 8.95; it does not. 8.950 is measured from Datum B, which is itself 0.400 in from +// the board edge, so 0.400 + 8.950 = 9.350 on a standard-depth board and on this one alike. +// +// What the extra depth does is leave board hanging PAST the last mounting row: 10.500 - 9.350 = +// 1.150 in, 29.21 mm, against 0.250 in on an ordinary micro-ATX board. Power and SlimSAS connectors +// sit near that edge and take insertion force on unsupported PCB. A non-conductive front-edge +// support is therefore a cassette candidate rather than a nicety — gated on an underside-component +// keep-out measurement, since a support that fouls a solder joint is worse than none. +// THE AXIS ASSIGNMENT IS A CONSTRUCTOR, NOT A COMMENT, and this program earned that the hard way. +// +// The extents of this board were transposed once and the error survived review, three separate +// retractions, and an approving review that quoted the stale prose back as evidence of discipline. +// Every one of those defences was a SENTENCE. The annotation above the outline said "x is along the +// rear I/O edge, y is depth" and it was true and it prevented nothing, because no Accepted program +// can read it -- DESIGN section 4c says exactly that about annotations, and a fact that only prose +// carries is a fact the compiler cannot check. +// +// So the assignment moves into the type system. There are exactly two ways to lay a rectangular +// board into a 2-D frame, and they are the two arms below. A transposition is then a DIFFERENT +// CONSTRUCTOR rather than a different comment: it cannot be introduced by editing prose, and every +// consumer that reads an extent must say which axis it means. +// +// Why a two-arm coproduct rather than a record of two roles: a record permits x and y to carry the +// SAME role, which is not a transposition but a nonsense state, and DESIGN section 4b prefers the +// invalid state to have no constructor over having a validator. +type BoardPlaneOrientation + = XAlongRearIoYDepth + | XDepthYAlongRearIo + +// The readouts. These are the only sanctioned way to ask this module for an extent, and they are +// named for the PHYSICAL EDGE rather than for an axis letter, so a caller cannot ask for "x" and +// receive whatever x happens to mean today. +fn board_extent_along_rear_io(orientation: BoardPlaneOrientation, x: Micrometer, y: Micrometer) -> Micrometer { + match orientation { + XAlongRearIoYDepth => x + XDepthYAlongRearIo => y + } +} + +fn board_extent_depth(orientation: BoardPlaneOrientation, x: Micrometer, y: Micrometer) -> Micrometer { + match orientation { + XAlongRearIoYDepth => y + XDepthYAlongRearIo => x + } +} + +// This board's orientation, declared once. The outline's max point is authored in this orientation +// and the readouts below are the accessors every consumer should use. +data asrock_altrad8ud_orientation: BoardPlaneOrientation = XAlongRearIoYDepth + +data asrock_altrad8ud_extent_along_rear_io: Micrometer = board_extent_along_rear_io( + orientation: asrock_altrad8ud_orientation, + x: micrometer(count: 243840), + y: micrometer(count: 266700) +) + +data asrock_altrad8ud_extent_depth: Micrometer = board_extent_depth( + orientation: asrock_altrad8ud_orientation, + x: micrometer(count: 243840), + y: micrometer(count: 266700) +) + +// NOMINAL, NOT AS-MANUFACTURED, and the distinction is the difference between arithmetic and +// physics. 243840 x 266700 um is the EXACT CONVERSION of the vendor's published nominal 9.6 x 10.5 +// in. It is not the exact as-built extent of any board on the operator's desk: PCB routing carries a +// real tolerance, and no board here has been measured. Naming these "exact" without qualification +// invites the promotion that matters -- exact ARITHMETIC silently read as ZERO PHYSICAL TOLERANCE -- +// and a cassette clearance derived on that reading would be tight by an unknown amount. +// +// So: these are nominal-profile facts, admissible for layout and for deciding which standard grid +// applies. Any clearance that depends on the board's real edge needs a product tolerance or an +// as-held measurement, which asrock_altrad8ud_open_mounting_unknowns already tracks as unmeasured. +data asrock_altrad8ud_board_depth_nominal_exact: Micrometer = micrometer(count: 266700) +data asrock_altrad8ud_front_mounting_row_offset: Micrometer = micrometer(count: 237490) +data asrock_altrad8ud_front_overhang: Micrometer = micrometer(count: 29210) + +// THE OPEN MOUNTING UNKNOWNS, AS A CLOSED TYPE RATHER THAN A PARAGRAPH. +// +// An earlier revision carried these five as one NonEmptyStr. DESIGN section 4c names a dissolution +// condition as something that belongs in a typed carrier specifically, and the reason is mechanical: +// a paragraph cannot be counted, cannot be discharged one item at a time, and cannot refuse. This +// can. Each arm names one product-specific fact that the standard does not supply, and the total +// derivation beside it names what discharges it — so an arm added later cannot be left without a +// route, and the roster going empty is a real, checkable event rather than someone editing prose. +// +// Note what is NOT in here: the standard LOCATIONS. Those are exact. Everything below is a fact +// about this physical product that no specification can answer. +type Altrad8udMountingUnknown + = HoleCorrespondencePhysicallyUnconfirmed + | ProductHoleDiameterUnmeasured + | UndersideKeepOutUnmeasured + | MountingHoleGroundBondUnknown + | StandoffHeightAndPadUnmeasured + +type MountingUnknownDischarge + = DischargedByMountingTheBoard + | DischargedByCalipers + | DischargedByContinuityMeter + +// Total by construction: a new unknown must be given a discharge route here or fail to compile. +fn mounting_unknown_discharge(u: Altrad8udMountingUnknown) -> MountingUnknownDischarge { + match u { + HoleCorrespondencePhysicallyUnconfirmed => DischargedByMountingTheBoard + ProductHoleDiameterUnmeasured => DischargedByCalipers + UndersideKeepOutUnmeasured => DischargedByCalipers + StandoffHeightAndPadUnmeasured => DischargedByCalipers + MountingHoleGroundBondUnknown => DischargedByContinuityMeter + } +} + +// MountingHoleGroundBondUnknown governs the FUNCTIONAL board-to-chassis bond only. Protective earth +// is bolted to rack metal and must survive board, standoff and cassette removal, so no entry in this +// roster sits on the safety path — see the grounding section of the printed-chassis program. +data asrock_altrad8ud_open_mounting_unknowns: List = [ + HoleCorrespondencePhysicallyUnconfirmed, + ProductHoleDiameterUnmeasured, + UndersideKeepOutUnmeasured, + MountingHoleGroundBondUnknown, + StandoffHeightAndPadUnmeasured, +] diff --git a/dag/extdeps/printing/bambu_lab_a1_mini.dag b/dag/extdeps/printing/bambu_lab_a1_mini.dag new file mode 100644 index 00000000000..cb869af18d0 --- /dev/null +++ b/dag/extdeps/printing/bambu_lab_a1_mini.dag @@ -0,0 +1,130 @@ +module extdeps.printing.bambu_lab_a1_mini + +import std.types { List, NonEmptyStr } +import std.decl_ref { DeclarationRef, WholeDeclaration } +import std.measure { + Micrometer, micrometer, + Millimeter, millimeter, + Celsius, celsius, + Watt, watt, + Volt, volt, + Hertz, hertz, +} +import extdeps.printing.fdm { + BuildEnvelope, build_envelope, + NozzleDiameter, nozzle_diameter, + FilamentDiameter, filament_diameter, + MaterialSuitabilityRow, material_suitability_row, + SuitabilityIdeal, SuitabilityNotRecommended, + FilamentMaterial, + Pla, Petg, Tpu, Pva, Abs, Asa, Polycarbonate, Polyamide, Pet, FiberReinforcedPolymer, +} +import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef } +import extdeps.uri { Uri, Https } + +// THE A1 MINI AS A CONCRETE PRODUCT, which is the thing extdeps.printing.fdm deliberately is not. +// +// fdm owns the agnostic shapes — an envelope, a nozzle diameter, a material and a suitability +// grading. It enumerates no machine and grades no material, because a generic hub that named +// products would be the external-decomposition violation DESIGN section 3 describes. This module is +// the other half: one independently versioned product, owning its own facts. +// +// WHY IT EXISTS AT ALL, stated because its absence was a real defect rather than a gap. The coupon +// fit witness previously authored `build_envelope(180, 180, 180)` inline. That witness therefore +// tested a number it had written itself: it would have stayed green if this machine's envelope were +// different, and green if no printer authority existed anywhere in the corpus. A witness whose +// subject is its own literal establishes nothing about the world. It now reads the row below, so +// changing this row is what moves that witness. + +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "bambulab.com/en/a1-mini/specs" + } +} + +data extdeps_model_scope: ExternalModelScope = ExternalModelScope { + subject: ExternalSubjectRef { + declaration: DeclarationRef { + module_path: "extdeps.printing.bambu_lab_a1_mini", + decl_name: "a1_mini_build_envelope", + field: WholeDeclaration + } + }, + first_citation: extdeps_external_authority_anchor, + further_citations: [] +} + +// PROVENANCE, AND IT IS RELAYED RATHER THAN FETCHED. The vendor's "Technical Specifications A1 mini" +// table, supplied verbatim by the operator 2026-09-01. Outbound requests to bambulab.com are +// refused by this environment's egress policy (403) and the Wayback availability API returns no +// snapshot for that host, so no first-party read is available here and none is claimed. Every value +// below appears in that table; nothing is inferred from the machine's class, and where the table is +// silent this module is silent too rather than supplying the usual answer for a printer like this. + +data a1_mini_build_envelope: BuildEnvelope = build_envelope( + x: millimeter(count: 180), + y: millimeter(count: 180), + z: millimeter(count: 180) +) + +// The INCLUDED nozzle, distinguished from the optional ones because they are different facts: one +// describes the machine as delivered, the others describe what may be fitted. A process qualified on +// one nozzle is not qualified on another, so collapsing these into a set would let a 0.4 mm +// qualification be spent on a 0.2 mm job. +data a1_mini_nozzle_included: NozzleDiameter = nozzle_diameter(value: micrometer(count: 400)) + +data a1_mini_nozzle_optional: List = [ + nozzle_diameter(value: micrometer(count: 200)), + nozzle_diameter(value: micrometer(count: 600)), + nozzle_diameter(value: micrometer(count: 800)), +] + +data a1_mini_filament_diameter: FilamentDiameter = filament_diameter(value: micrometer(count: 1750)) + +data a1_mini_max_hot_end_temperature: Celsius = celsius(count: 300) +data a1_mini_max_build_plate_temperature: Celsius = celsius(count: 80) + +// Electrical, carried because the rack this program builds shares a supply with these machines and +// because a printer is a node with a power envelope like any other. +// +// THE RATING IS RMS, AND SAYING SO IS NOT PEDANTRY. "100-240 VAC" is a root-mean-square rating; the +// peak is about 1.41x it, so a 240 V rating implies roughly 340 V of insulation stress. Nothing in +// this program consumes that distinction today, so no separate RMS carrier is minted -- a type with +// no consumer is the experimental residue DESIGN section 6 names. It is recorded here so that the +// first consumer which cares about peak stress reads a stated assumption rather than inferring one +// from a bare number. +// +// Volt is the right carrier and its quantity is already ElectricPotentialDifference, so this is a +// potential DIFFERENCE and not an absolute potential. Review 58505 read it as "a flat Volt scalar" +// and asked for an affine split; the response is recorded on the pull request rather than here, +// because it is a fact about the substrate rather than about this machine. +data a1_mini_input_voltage_minimum: Volt = volt(count: 100) +data a1_mini_input_voltage_maximum: Volt = volt(count: 240) +data a1_mini_input_frequency_minimum: Hertz = hertz(count: 50) +data a1_mini_input_frequency_maximum: Hertz = hertz(count: 60) +data a1_mini_max_power: Watt = watt(count: 150) + +// Physical footprint of the MACHINE, not of anything it prints. Named to keep that distinction +// visible: 347 x 315 x 365 is the desk space it occupies, and confusing it with the build envelope +// is a mistake that would silently admit parts nearly twice the printable size. +data a1_mini_machine_width: Millimeter = millimeter(count: 347) +data a1_mini_machine_depth: Millimeter = millimeter(count: 315) +data a1_mini_machine_height: Millimeter = millimeter(count: 365) + +// THE SUITABILITY ROSTER IS COMPLETE OVER FilamentMaterial, and that is a property worth stating. +// The vendor table grades ten materials and fdm models exactly ten, so every arm has a row and no +// consumer can ask about a material this roster does not answer for. SuitabilityUnstated therefore +// does not appear here — it exists for machines whose vendor is silent, which this one is not. +data a1_mini_material_suitability: List = [ + material_suitability_row(material: Pla, suitability: SuitabilityIdeal), + material_suitability_row(material: Petg, suitability: SuitabilityIdeal), + material_suitability_row(material: Tpu, suitability: SuitabilityIdeal), + material_suitability_row(material: Pva, suitability: SuitabilityIdeal), + material_suitability_row(material: Abs, suitability: SuitabilityNotRecommended), + material_suitability_row(material: Asa, suitability: SuitabilityNotRecommended), + material_suitability_row(material: Polycarbonate, suitability: SuitabilityNotRecommended), + material_suitability_row(material: Polyamide, suitability: SuitabilityNotRecommended), + material_suitability_row(material: Pet, suitability: SuitabilityNotRecommended), + material_suitability_row(material: FiberReinforcedPolymer, suitability: SuitabilityNotRecommended), +] diff --git a/dag/extdeps/printing/bambu_studio.dag b/dag/extdeps/printing/bambu_studio.dag new file mode 100644 index 00000000000..9e11e160e6d --- /dev/null +++ b/dag/extdeps/printing/bambu_studio.dag @@ -0,0 +1,127 @@ +module extdeps.printing.bambu_studio + +import std.types { List, NonEmptyStr } +import std.decl_ref { DeclarationRef, WholeDeclaration } +import std.os.types { OperatingSystemProduct, UbuntuOs, WindowsOs, MacosOs, NobleNumbat2404Lts, Windows1124H2Build26100, Sequoia15 } +import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef } +import extdeps.uri { Uri, Https } + +// Bambu Studio, the vendor's own slicer, as its OWN subject — not a field on the printer. DESIGN §3 +// external decomposition: the slicer is independently versioned from the machine it slices for, and +// OrcaSlicer, its fork, is a third subject again. A printer module that enumerated its slicers would +// be the generic-hub violation that rule names. +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "github.com/bambulab/BambuStudio" + } +} + +data bambu_studio_product_page_authority: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "bambulab.com/en/download/studio" + } +} + +data bambu_studio_release_api_authority: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "api.github.com/repos/bambulab/BambuStudio/releases/latest" + } +} + +data bambu_studio_flathub_authority: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "flathub.org/apps/com.bambulab.BambuStudio" + } +} + +data extdeps_model_scope: ExternalModelScope = ExternalModelScope { + subject: ExternalSubjectRef { + declaration: DeclarationRef { + module_path: "extdeps.printing.bambu_studio", + decl_name: "bambu_studio_platform_support", + field: WholeDeclaration + } + }, + first_citation: extdeps_external_authority_anchor, + further_citations: [bambu_studio_release_api_authority, bambu_studio_flathub_authority], +} + +// TWO AUTHORITIES FROM ONE VENDOR DISAGREE, AND THE MODEL CARRIES BOTH RATHER THAN PICKING. +// +// The A1 mini specification table, relayed by the operator from the product page, states the slicer's +// supported operating systems as "MacOS, Windows". The vendor's own release feed, fetched +// first-party from this environment, publishes BambuStudio_ubuntu22.04-*.AppImage and +// BambuStudio_ubuntu24.04-*.AppImage as release assets, and Flathub serves the application. Both are +// the vendor speaking. They do not agree. +// +// WHY NOT JUST RECORD "LINUX IS SUPPORTED". Because that resolves a disagreement this repository +// has no authority to resolve, and it discards the fact that is actually load-bearing for an +// operator: the SPEC SHEET does not promise Linux, so a Linux regression is not a warranty claim, +// while the RELEASE FEED demonstrably ships Linux binaries, so the toolchain can be Linux-native +// today. A consumer planning a Linux workstation needs the second; a consumer deciding what the +// vendor is contractually committed to needs the first. Collapsing to one erases the other, and the +// collapse would be invisible — the surviving row looks equally authoritative either way. +// +// This is the shape DESIGN §3 calls a MEANING FORK if it were left implicit: one spelling +// ("supported OS") carrying two materially different obligations. Naming the two claims separately, +// each with its own authority, is what keeps it from being one. +type PlatformSupportClaimKind + = SpecificationSheetClaim + | PublishedReleaseArtifact + +type PlatformSupportClaim sole_constructor { + kind: PlatformSupportClaimKind + platform: OperatingSystemProduct + authority: ExternalAuthority + note: NonEmptyStr +} + +data bambu_studio_spec_sheet_platforms: List = [ + PlatformSupportClaim { + kind: SpecificationSheetClaim, + platform: MacosOs { distro: Sequoia15 }, + authority: bambu_studio_product_page_authority, + note: "A1 mini specification table, 'Slicer Supported OS: MacOS, Windows', relayed by the operator 2026-09-01. The table names the OS family without an edition; Sequoia15 is this corpus's macOS surface row and is NOT part of the vendor's claim.", + }, + PlatformSupportClaim { + kind: SpecificationSheetClaim, + platform: WindowsOs { distro: Windows1124H2Build26100 }, + authority: bambu_studio_product_page_authority, + note: "Same table, same relay. Edition is this corpus's Windows surface row and is not stated by the vendor table.", + }, +] + +// Fetched first-party: api.github.com answers 200 from this environment, so these asset names were +// READ, not relayed. The release carrying them is v02.08.02.61. Ubuntu 22.04 is also published; only +// the 24.04 asset is modelled here because NobleNumbat2404Lts is the surface row this corpus carries, +// and inventing a 22.04 row to be complete would mint an OS product for a claim nothing consumes. +data bambu_studio_release_artifact_platforms: List = [ + PlatformSupportClaim { + kind: PublishedReleaseArtifact, + platform: UbuntuOs { distro: NobleNumbat2404Lts }, + authority: bambu_studio_release_api_authority, + note: "Release asset BambuStudio_ubuntu24.04-v02.08.02.61-*.AppImage, read first-party from the release API 2026-09-01. Flathub additionally serves com.bambulab.BambuStudio.", + }, +] + +// THE JOIN IS A CONCATENATION, NOT AN ADJUDICATION, and reading it requires knowing that. +// +// The two rosters disagree about Linux: the specification table lists macOS and Windows only, while +// the release feed publishes Ubuntu AppImages. Every claim below therefore carries its own kind and +// its own authority, and nothing in this module says which wins — a Linux toolchain is demonstrably +// available and is not promised by the spec sheet, and those are both true at once. +// +// The disagreement is not restated as a datum here. An earlier revision carried it as a standalone +// NonEmptyStr, which is the unclassified prose DESIGN section 4c forbids: every fact in that +// sentence is already in a typed row above (the kinds, the platforms, the authorities, the asset +// names), so the row duplicated modelled data in a form no program can read. What is left is the +// rationale for the shape, which is what an annotation is for. +data bambu_studio_platform_support: List = concat( + bambu_studio_spec_sheet_platforms, + bambu_studio_release_artifact_platforms +) + diff --git a/dag/extdeps/printing/fdm.dag b/dag/extdeps/printing/fdm.dag new file mode 100644 index 00000000000..91314c7ff05 --- /dev/null +++ b/dag/extdeps/printing/fdm.dag @@ -0,0 +1,240 @@ +module extdeps.printing.fdm + +import std.types { Bool, List, NonEmptyStr } +import std.nat { Nat } +import std.measure { Millimeter, millimeter_count, Micrometer, micrometer_count, Celsius, celsius_count } + +import extdeps.external_authority { ExternalAuthority } +import extdeps.uri { Uri, Https } + +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "en.wikipedia.org/wiki/Fused_filament_fabrication" + } +} + +// THE AGNOSTIC HUB for fused-filament fabrication, and it deliberately carries NO ExternalModelScope +// and NO product rows. DESIGN §3 "External upstream decomposition": a generic hub may define shapes +// that concrete products inhabit, and may not enumerate those products, dispatch among their +// authorities, or hold their version rows. Every machine-specific figure lives in the machine's own +// module and cites the machine's own authority; this file is what those modules are spelled in. +// +// WHY THESE TWO LENGTHS ARE MICROMETRES AND THE ENVELOPE IS MILLIMETRES, which is the one modelling +// decision in this file that a reader could mistake for fussiness. +// +// Millimeter is Measure — a NON-NEGATIVE INTEGER count of millimetres. A 0.4 mm +// nozzle is therefore not merely rounded in that carrier, it is ZERO, and the 0.2 / 0.4 / 0.6 / 0.8 +// family collapses to a single value: the carrier loses the DISTINCTION the fact exists to make. +// That is the same failure std.spatial_frame records for a 0.5 mm contact pitch on a printed circuit +// board, reached from the opposite direction, and it is why nozzle and filament diameter are +// micrometres here while build extents — hundreds of whole millimetres — stay in millimetres. +// The rule the two cases share: pick the quantum from the SMALLEST distinction the quantity must +// preserve, never from the largest value it must hold. +type NozzleDiameter sole_constructor { value: Micrometer } + +fn nozzle_diameter(value: Micrometer) -> NozzleDiameter { + NozzleDiameter { value: value } +} + +fn nozzle_diameter_value(n: NozzleDiameter) -> Micrometer { n.value } + +type FilamentDiameter sole_constructor { value: Micrometer } + +fn filament_diameter(value: Micrometer) -> FilamentDiameter { + FilamentDiameter { value: value } +} + +fn filament_diameter_value(f: FilamentDiameter) -> Micrometer { f.value } + +// THE BUILD ENVELOPE, and the fit question asked of it. +// +// A build envelope is a machine fact. Whether a PART fits it is a question about an ORIENTED part, +// and this module answers only that question — it does not search orientations. Refusing to search +// is the load-bearing choice: an operation that quietly rotated the part until something fitted +// would answer "fits" for a part the caller cannot actually print in the orientation its strength +// requires, and layer adhesion makes orientation a STRUCTURAL fact for a printed bracket, not a +// packing convenience. Orientation selection is a separate decision with its own inputs, and it +// belongs to whatever holds those inputs. +type BuildEnvelope sole_constructor { + x: Millimeter + y: Millimeter + z: Millimeter +} + +fn build_envelope(x: Millimeter, y: Millimeter, z: Millimeter) -> BuildEnvelope { + BuildEnvelope { x: x, y: y, z: z } +} + +fn build_envelope_x(e: BuildEnvelope) -> Millimeter { e.x } +fn build_envelope_y(e: BuildEnvelope) -> Millimeter { e.y } +fn build_envelope_z(e: BuildEnvelope) -> Millimeter { e.z } + +// An oriented part's bounding extent, in the same axes as the envelope it will be asked about. +type PartExtent sole_constructor { + x: Millimeter + y: Millimeter + z: Millimeter +} + +fn part_extent(x: Millimeter, y: Millimeter, z: Millimeter) -> PartExtent { + PartExtent { x: x, y: y, z: z } +} + +type EnvelopeAxis + = EnvelopeX + | EnvelopeY + | EnvelopeZ + +type AxisExceedance sole_constructor { + axis: EnvelopeAxis + part: Millimeter + envelope: Millimeter +} + +// The refusal reports EVERY exceeded axis rather than the first, and carries both numbers per axis. +// A single-axis refusal makes the caller re-ask once per axis to learn how far off the part is, +// which is the shape that turns one sectioning decision into three rounds of trial fitting. The +// nonempty payload is split first/rest so that an exceedance-free refusal — a refusal asserting +// nothing — is unwritable rather than checked, the ExternalModelScope citation precedent. +type EnvelopeFit + = PartFits + | PartExceedsEnvelope { + first: AxisExceedance + rest: List + } + +fn axis_exceedance(axis: EnvelopeAxis, part: Millimeter, envelope: Millimeter) -> List { + match millimeter_count(m: part) <= millimeter_count(m: envelope) { + true => [] + false => [AxisExceedance { axis: axis, part: part, envelope: envelope }] + } +} + +// Comparison is inclusive: a part exactly as long as the envelope is reported as fitting. That is +// the honest reading of the machine's stated extent, and it is NOT a claim that the part is +// printable at that size — head clearance, skirt, and plate-edge margin all consume envelope and +// none of them are facts this carrier holds. A clearance margin is a policy fact belonging to +// whoever sets it; folding a guess for it in here would make every consumer inherit a number no +// authority states, and would make the envelope silently smaller than the machine's own figure. +fn add_exceedance(acc: EnvelopeFit, e: AxisExceedance) -> EnvelopeFit { + match acc { + PartFits => PartExceedsEnvelope { first: e, rest: [] } + PartExceedsEnvelope { first: f, rest: r } => PartExceedsEnvelope { first: f, rest: concat(r, [e]) } + } +} + +fn envelope_fit(envelope: BuildEnvelope, part: PartExtent) -> EnvelopeFit { + fold( + concat( + axis_exceedance(axis: EnvelopeX, part: part.x, envelope: envelope.x), + concat( + axis_exceedance(axis: EnvelopeY, part: part.y, envelope: envelope.y), + axis_exceedance(axis: EnvelopeZ, part: part.z, envelope: envelope.z) + ) + ), + init: PartFits, + f: fn(acc, e) { add_exceedance(acc: acc, e: e) } + ) +} + + +// FILAMENT MATERIAL CLASSES. These are polymer classes, not products: a spool of PETG from any +// vendor inhabits Petg. Thermal and mechanical PROPERTIES are deliberately absent — they are facts +// about a specific formulation from a specific supplier, cited to that supplier's technical data +// sheet, and authoring a nominal glass-transition figure here would make one number stand for every +// PETG on the market at exactly the point where a load-bearing part consults it. +type FilamentMaterial + = Pla + | Petg + | Tpu + | Pva + | Abs + | Asa + | Polycarbonate + | Polyamide + | Pet + | FiberReinforcedPolymer + +// A MACHINE VENDOR'S OWN SUITABILITY GRADE for a material, and the third arm is the whole point. +// +// A vendor specification table splits materials into the ones it endorses and the ones it warns +// against. A material appearing in NEITHER column is not thereby endorsed, and it is not thereby +// refused — the table is silent, and silence is a distinct state that must survive to the consumer. +// Collapsing it into either graded arm is the fail-open move: read as endorsement it prints a part +// the vendor never claimed the machine can make, and read as refusal it invents a restriction the +// vendor never stated. A lookup over the vendor's rows therefore returns SuitabilityUnstated for +// anything the rows do not mention, and the caller decides what to do about not knowing. +type MaterialSuitability + = SuitabilityIdeal + | SuitabilityNotRecommended + | SuitabilityUnstated + +type MaterialSuitabilityRow sole_constructor { + material: FilamentMaterial + suitability: MaterialSuitability +} + +fn material_suitability_row(material: FilamentMaterial, suitability: MaterialSuitability) -> MaterialSuitabilityRow { + MaterialSuitabilityRow { material: material, suitability: suitability } +} + +// EQUALITY BY EXHAUSTIVE TAG PROJECTION, NOT BY NESTED MATCH WITH A WILDCARD. +// +// The first revision wrote the pairwise form: match a { Pla => match b { Pla => true, _ => false } +// ... }. The corpus's non-fold-residue lens flags exactly that shape, and it is right to. The inner +// wildcard is the defect: adding an eleventh material would be ABSORBED by every `_ => false` arm, +// so the new variant would silently compare unequal to itself in some arms and nothing would fail to +// compile. A wildcard over a closed coproduct converts "I enumerated the domain" into "I did not, +// and the compiler may not tell you". +// +// EQUALITY IS THE SUBSTRATE'S, NOT THIS MODULE'S. +// +// An earlier revision projected every variant to an integer tag and compared the integers, with an +// annotation arguing the tag was "an ordinal comparison device and not a second name". That defence +// is the tell: a second representation always claims not to be one. `==` is structurally defined for +// closed coproducts in this substrate -- `std.roster_frontier` `frontier_subject_eq` is the same +// one-line shape -- so the ordinals were a hand-rolled duplicate of a decision the language already +// makes, and DESIGN section 2 prices a re-derivation of an existing law as redundant regardless of +// how small it is. +// +// It also failed at the thing it was introduced to do. The tags were written to avoid a wildcard +// over a closed coproduct, but a new material added to FilamentMaterial gets a fresh ordinal only if +// the author remembers to extend the projection; structural equality has nothing to extend. +fn filament_material_eq(a: FilamentMaterial, b: FilamentMaterial) -> Bool { + a == b +} + +// DUPLICATE ROWS REFUSE, AND THIS IS THE SAME DEFECT THIS SESSION ALREADY FIXED ONCE ELSEWHERE. +// +// The first revision folded and returned the last matching row, so two rows for PETG — one Ideal, +// one NotRecommended — resolved by list order with nothing refusing. That is byte-for-byte the +// last-match-wins bug found and repaired in product.printed_chassis.measurement, and it was left +// standing here because that repair was applied at the site where it was noticed rather than swept +// across the class. Found in review. A defect class is not closed at one site. +// +// A vendor table stating a material twice with different grades is a reading error or a table +// change, and either way the honest answer is that the rows disagree — not whichever the fold +// happened to see last. +type MaterialSuitabilityLookup + = SuitabilityResolved { suitability: MaterialSuitability } + | SuitabilityRowsConflict { material: FilamentMaterial, count: Int } + +type SuitabilityScan sole_constructor { + count: Int + suitability: MaterialSuitability +} + +fn material_suitability(rows: List, material: FilamentMaterial) -> MaterialSuitabilityLookup { + let scan = fold(rows, init: SuitabilityScan { count: 0, suitability: SuitabilityUnstated }, f: fn(acc, row) { + match filament_material_eq(a: row.material, b: material) { + true => SuitabilityScan { count: acc.count + 1, suitability: row.suitability } + false => acc + } + }) + if scan.count > 1 { + SuitabilityRowsConflict { material: material, count: scan.count } + } else { + SuitabilityResolved { suitability: scan.suitability } + } +} diff --git a/dag/extdeps/standards/atx_2_2.dag b/dag/extdeps/standards/atx_2_2.dag new file mode 100644 index 00000000000..af320668758 --- /dev/null +++ b/dag/extdeps/standards/atx_2_2.dag @@ -0,0 +1,65 @@ +module extdeps.standards.atx_2_2 +import std.types { NonEmptyStr } +import std.measure { Micrometer, micrometer, Millimeter, millimeter } +import std.decl_ref { DeclarationRef, WholeDeclaration } +import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef } +import extdeps.uri { Uri, Https } +// THE ATX SPECIFICATION, VERSION 2.2, as its own subject. It is the form-factor authority that the +// ATX FAMILY of board outlines and mounting-hole grids descends from, and it is modelled separately +// from any board because a specification and a product that claims conformance to it are two +// subjects, not one. A board module citing this one asserts a conformance CLAIM; this module asserts +// only what the document says. +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "web.archive.org/web/20180417122513/http://www.formfactors.org:80/developer/specs/atx2_2.pdf" + } +} +data extdeps_model_scope: ExternalModelScope = ExternalModelScope { + subject: ExternalSubjectRef { + declaration: DeclarationRef { + module_path: "extdeps.standards.atx_2_2", + decl_name: "atx_board_width_along_rear_io", + field: WholeDeclaration + } + }, + first_citation: extdeps_external_authority_anchor, + further_citations: [] +} +// PROVENANCE. The PDF was fetched and read first-party by the authoring session from the Internet +// Archive snapshot named above; formfactors.org itself no longer serves it. The figures below are +// the dimensions the document prints in its own figure text layer, in inches with the millimetre +// conversion the document itself carries — they are not converted here, which is why both numbers +// appear and agree. +// +// WHAT THIS MODULE OWNS, AND WHAT IT DELIBERATELY NO LONGER OWNS. +// +// ATX 2.2 facts only: the full-size board extents and the two datum offsets its Figure 7 labels. +// The microATX envelope, lettered location population and coordinates USED TO LIVE HERE and were +// moved to extdeps.standards.micro_atx, because sharing some mounting locations with ATX is not +// shared governance -- microATX is a separately governed specification with its own revision, and a +// change to it must not require editing this file. +// +// This module carries NO location population. If one is added later it will be ATX 2.2's own, read +// from this document, and the shared shapes will move to a neutral home at that point -- when a +// second standard actually enumerates, which is the event that makes the extraction correct. +// THE ROUNDED AND THE EXACT ARE BOTH CARRIED, and the exact one is a Micrometer rather than a +// sentence. An earlier revision kept 243.84 in a prose row that said it was "preserved in this note +// rather than silently lost" — but a note is exactly where a number IS lost: no Accepted program can +// read one, so the only surviving machine-readable value was the rounded 244. The whole-millimetre +// carrier cannot hold the spec's figure; the micrometre carrier can, so the spec's figure lives +// there and the rounding stops being lossy. +data atx_board_width_along_rear_io: Millimeter = millimeter(count: 244) +data atx_board_width_along_rear_io_exact: Micrometer = micrometer(count: 243840) + +// 12.000 in, the full-size ATX board depth. Carried because it is the dimension the micro-ATX and +// deep-micro-ATX variants reduce, NOT as a claim about any board in this corpus. +data atx_full_size_depth: Millimeter = millimeter(count: 305) +data atx_full_size_depth_exact: Micrometer = micrometer(count: 304800) +// THE TWO BOARD-MOUNTING-HOLE OFFSETS the specification's figure labels as REF dimensions. They are +// the only hole-related numbers with an extractable text layer in the whole document, and they are +// offsets from datum rather than hole positions: on their own they place nothing — two offsets +// cannot locate seven holes. They are kept because they are cited and exact, and because any later +// first-party reading of Figure 3 has to agree with them, which makes them a check on that reading. +data atx_board_mtg_hole_offset_a: Micrometer = micrometer(count: 16510) +data atx_board_mtg_hole_offset_b: Micrometer = micrometer(count: 10160) diff --git a/dag/extdeps/standards/micro_atx.dag b/dag/extdeps/standards/micro_atx.dag new file mode 100644 index 00000000000..7eacfd0dfbb --- /dev/null +++ b/dag/extdeps/standards/micro_atx.dag @@ -0,0 +1,202 @@ +module extdeps.standards.micro_atx + +import std.types { List, NonEmptyStr } +import std.decl_ref { DeclarationRef, WholeDeclaration } +import std.measure { Micrometer, micrometer, Millimeter, millimeter } +import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef } +import extdeps.uri { Uri, Https } +import extdeps.climbing_holds.types { DimensionEvidence, OperatorRelayedDocument } + +// MICROATX IS ITS OWN SPECIFICATION, NOT A SECTION OF ATX 2.2, and an earlier revision of this +// corpus got that wrong by putting the microATX envelope, location population and coordinates inside +// extdeps.standards.atx_2_2 because the two standards share some mounting locations. +// +// Sharing a few coordinates is not shared governance. The microATX Motherboard Interface +// Specification independently defines its own motherboard/chassis interface, its own maximum +// envelope, its own B/C/F/H/J/L/M/R/S population, the R and S requirements, and the rule that +// extraneous chassis standoffs be removable or absent. A change to microATX must not require editing +// the ATX module, which is precisely the external-decomposition test DESIGN section 3 states. +// +// NO NEUTRAL SHARED MODULE IS EXTRACTED YET, deliberately. MountingLocationId and MountingLocation +// are shapes a second standard could eventually share, but there is no multi-standard consumer today +// -- the ATX 2.2 spec carries no location population in this corpus -- and extracting a hub for one consumer +// would be inventing an authority to hold a symbol rather than to answer a question. They live here, +// with the standard that actually enumerates. The extraction becomes correct when a second standard +// enumerates, and not before. +// +// THE CITED DOCUMENT IS NOW THE RIGHT ONE, AND AN EARLIER REVISION CITED A DIFFERENT DOCUMENT THAN +// THE ONE ITS OWN PROVENANCE ROW NAMED. +// +// This scope's first_citation was the archived ATX 2.2 PDF while the provenance row below said the +// coordinates came by relay from the microATX Motherboard Interface Specification -- two different +// documents, one of them asserted STRUCTURALLY. An earlier revision recorded that contradiction in an +// annotation and left it standing, on the reasoning that no microATX document was in hand and the +// three available repairs were all worse than confessing. Recording it was not a repair: a prose +// confession does not subtract a typed claim, and first_citation is read by lenses that cannot see +// the paragraph denying it (routed review, 2026-09-02). The fourth option was to go and get the +// document, which is what happened. +// +// WHAT WAS ACTUALLY VERIFIED, stated at this grain because the provenance grade turns on it: +// - a document whose title page reads verbatim "microATX Motherboard Interface Specification +// Version 1.2" was retrieved and its title page text layer read first-party this session, from +// the xdevs mirror carried in further_citations; +// - its BODY is the same font-subset artwork the ATX 2.2 PDF turned out to be -- Table 4 and the +// mounting-hole figure do not survive text extraction -- so the COORDINATES were still not read +// first-party, and the provenance row below is unchanged at OperatorRelayedDocument; +// - the publisher's own copy at formfactors.org is present in the Wayback CDX index with status +// 200 at the snapshot spelled below. Its BYTES were not retrieved this session (rate limited), +// which is why the mirror that WAS opened is carried beside it rather than silently dropped. +// +// So the defect that closes here is the WRONG-DOCUMENT one. The remaining gap is narrower and is +// exactly what OperatorRelayedDocument exists to say: the right document is cited, the coordinates +// within it were relayed rather than read. TRIGGER for the last step is unchanged in kind but no +// longer blocked on finding a document -- it needs the figure extracted from THIS PDF, by OCR or by +// an operator reading Table 4, at which point the provenance row upgrades and the module may be +// renamed to spell the revision. + +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "web.archive.org/web/20061010062718/http://www.formfactors.org/developer/specs/matxspe1.2.pdf" + } +} + +// The mirror that was actually opened and read this session. It is a further_citation and not the +// first: a mirror is not the publisher, and the citation that leads should be the document's own +// home even when the copy in hand came from elsewhere. +data extdeps_external_authority_mirror: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "xdevs.com/doc/_PC_HW/Form_factors/matxspe1.2.pdf" + } +} + +data extdeps_model_scope: ExternalModelScope = ExternalModelScope { + subject: ExternalSubjectRef { + declaration: DeclarationRef { + module_path: "extdeps.standards.micro_atx", + decl_name: "micro_atx_mounting_locations", + field: WholeDeclaration + } + }, + first_citation: extdeps_external_authority_anchor, + further_citations: [extdeps_external_authority_mirror] +} + +// PROVENANCE OF THE COORDINATES: CITED-VIA-RELAY, the grade extdeps.climbing_holds.atomik defines +// for a document read by someone other than the authoring session. This session's own extraction of +// the archived ATX PDF recovered Figure 7's text layer and not the mounting-location artwork, so the +// values below are NOT this session's reading. They were supplied by a routed review and are +// corroborated -- not established -- by seven ASRock ALTRAD8UD holes landing on them exactly, which +// is not a coincidence available to invented numbers. Corroboration of a board correspondence is not +// a provenance upgrade for the standard reading, and this row does not claim otherwise. +// THIS WAS A STRING AND THAT WAS A SECOND NAME FOR AN EXISTING CONCEPT. It read +// "cited-via-relay: ..." as an ordinary NonEmptyStr, which is §4c misplaced data -- a CITATION +// STATUS is exactly the kind of fact that belongs in a typed carrier -- and §3 nicknaming, because +// `DimensionEvidence` already closes this vocabulary and `OperatorRelayedDocument` is already the +// arm for a document read by someone other than the authoring session. Nothing could consume the +// string; the grade was invisible to every lens that reads the tree. +// +// ON THE CARRIER'S HOME: it lives in `extdeps.climbing_holds.types`, which is a misleading address +// for a general concept, and the type's OWN annotation says so without meaning to -- it records that +// the arm exists because "a board's power-header inventory was asserted from memory", a failure with +// no climbing hold anywhere in it. Provenance grade is domain-agnostic and §3 says a fact's home is +// its LAYER rather than its file, so importing across is correct and re-minting a parallel grade +// here would be the nicknaming this row just stopped doing. RELOCATION TRIGGER: a third consumer +// outside climbing_holds, at which point the carrier moves to a neutral extdeps home and both +// consumers follow it. +data micro_atx_coordinate_provenance: DimensionEvidence = OperatorRelayedDocument { + authority: extdeps_external_authority_anchor, + relay_note: "Routed review reporting the microATX Motherboard Interface Specification location population and coordinates. The cited document is Version 1.2 and its title page was read first-party this session; its Table 4 and mounting-hole figure are font-subset artwork that does not survive text extraction, so the COORDINATES below are still the relay reading and not this session's. Which revision the RELAY read is not established, so the module is not renamed to spell one -- holding a 1.2 copy does not establish that the relayed numbers came from 1.2. Corroborated -- not established -- by seven ASRock ALTRAD8UD holes landing on these values exactly.", +} + +// THE STRUCTURAL OVER-CLAIM IS CLOSED. first_citation now names the microATX Motherboard Interface +// Specification, which is the document the provenance row names, so the typed citation and the typed +// provenance agree on WHICH DOCUMENT. What remains is a grade, not a contradiction: the coordinates +// came by relay from that document rather than from this session reading its Table 4, and +// OperatorRelayedDocument says exactly that. The earlier framing of this gap -- that an +// ExternalAuthority arm carrying a relayed-with-no-document chain might be needed -- is retired: the +// document exists and is cited, so there is no document-less chain left to model. + +// THE MICRO-ATX AND DEEP-MICRO-ATX RELATION, stated because it is the fact a chassis actually needs +// and because this session got it BACKWARDS once and shipped the error. +// +// micro-ATX is 9.6 x 9.6 in: it reduces full-size ATX along the DEPTH axis and leaves the rear-I/O +// width alone. "Deep micro-ATX" restores some of that depth while keeping the same 9.6 in width. So +// a deep-micro-ATX board is NOT a wider micro-ATX board — it is exactly as wide, and deeper. +// +// The error worth recording: an earlier revision of extdeps.boards.asrock_rack read the ALTRAD8UD's +// 9.6 x 10.5 in as 267 mm WIDE against micro-ATX's 244 mm, and concluded that a micro-ATX hole +// pattern would be laid out at the wrong width. The axes were transposed. The board is 244 mm wide, +// which is the micro-ATX width exactly, and 267 mm deep. +// +// RETRACTED, and it was written in this file: the sentence that followed said "it is the FRONT row +// that moves outward by the extra depth". That is false, for the datum reason recorded in +// extdeps.standards.micro_atx, which now owns that grid. The front row does not move; a deep board +// extends PAST it. +// THE LETTERED MOUNTING-LOCATION GRID. The specifications name their location populations by letter, +// and the letters — not coordinates — are the identity: a location is the same location across +// revisions and across boards, which is what makes "this board populates C" a checkable claim rather +// than a coincidence of numbers. +// +// Coordinates are in the board frame used throughout this corpus: x ALONG THE REAR I/O EDGE, y DEPTH +// FROM THAT EDGE, micrometres. They are exact standard values, not readings. +// +// THE DATUM CORRECTION THAT MAKES THE FRONT ROW MAKE SENSE, and it killed a wrong claim of ours. +// The specification's figure gives the front row as 8.950 in — measured FROM DATUM B, which itself +// sits 0.400 in from the rear board edge. So the front row is 0.400 + 8.950 = 9.350 in from the +// edge. An earlier revision of extdeps.boards.asrock_rack asserted that a deep board's extra depth +// PUSHED this row outward from a nominal 8.95; it does not. L and M sit at the ordinary micro-ATX +// location on a deep board and on a standard-depth board alike. What the extra depth does is extend +// the board PAST them. +type MountingLocationId + = LocB | LocC | LocF | LocH | LocJ | LocL | LocM | LocR | LocS + +type MountingLocation sole_constructor { + id: MountingLocationId + along_rear_edge: Micrometer + depth_from_rear_edge: Micrometer +} + +fn mounting_location(id: MountingLocationId, along_rear_edge: Micrometer, depth_from_rear_edge: Micrometer) -> MountingLocation { + MountingLocation { id: id, along_rear_edge: along_rear_edge, depth_from_rear_edge: depth_from_rear_edge } +} + +// The micro-ATX population the specification names: B, C, F, H, J, L, M, R, S. +data micro_atx_mounting_locations: List = [ + mounting_location(id: LocF, along_rear_edge: micrometer(count: 6350), depth_from_rear_edge: micrometer(count: 33020)), + mounting_location(id: LocJ, along_rear_edge: micrometer(count: 6350), depth_from_rear_edge: micrometer(count: 165100)), + mounting_location(id: LocM, along_rear_edge: micrometer(count: 6350), depth_from_rear_edge: micrometer(count: 237490)), + mounting_location(id: LocC, along_rear_edge: micrometer(count: 163830), depth_from_rear_edge: micrometer(count: 10160)), + mounting_location(id: LocH, along_rear_edge: micrometer(count: 163830), depth_from_rear_edge: micrometer(count: 165100)), + mounting_location(id: LocL, along_rear_edge: micrometer(count: 163830), depth_from_rear_edge: micrometer(count: 237490)), + mounting_location(id: LocB, along_rear_edge: micrometer(count: 209550), depth_from_rear_edge: micrometer(count: 10160)), + mounting_location(id: LocS, along_rear_edge: micrometer(count: 209550), depth_from_rear_edge: micrometer(count: 165100)), + mounting_location(id: LocR, along_rear_edge: micrometer(count: 229870), depth_from_rear_edge: micrometer(count: 165100)), +] + +// The STANDARD's nominal mounting-hole diameter. It is a property of the location definition and +// NOT of any product: a board populating location C is not thereby asserted to have a 3.96 mm hole. +// A product's actual hole diameter is a product fact and stays unknown until measured or cited. +// 0.156 in nominal. This belongs to the STANDARD LOCATION definition and to nothing else; no +// consumer may read a product's physical hole diameter from it. +data micro_atx_standard_hole_diameter: Micrometer = micrometer(count: 3962) + +// The maximum envelope, and the reason reusing the grid is not conformance. A design exceeding this +// envelope requires a dedicated chassis by the specification's own statement, so a 9.6 x 10.5 in +// board cannot be called mechanically conforming micro-ATX merely because it populates the grid. +// GRID REUSE AND ENVELOPE CONFORMANCE ARE SEPARATE CLAIMS, and a board can make the first while +// failing the second. The two rows below ARE the maximum envelope: a design exceeding it requires a +// dedicated chassis by the specification's own statement. So populating the lettered grid does not +// make a 9.6 x 10.5 in board mechanically conforming micro-ATX. +// +// AND THE VENDOR PHRASE IS NOT A FORM FACTOR. An earlier revision of this module generalised "deep +// micro-ATX" to mean 9.6 in wide plus extra depth. That is refuted by the vendor's own catalogue: +// ASRock applies the same phrase to a 9.6 x 10.5 in board AND to a 10.4 x 10.5 in board. The label +// determines neither the outline nor a mounting-hole population, which is why this corpus carries a +// standard with a lettered location catalog, a separately cited vendor label claim carrying no +// dimensions, and a per-product mechanical profile — rather than a FormFactor coproduct with a +// DeepMicroAtx arm. A name that silently implies an envelope is the category error that produced the +// axis transposition recorded above. +data micro_atx_width_along_rear_io: Millimeter = millimeter(count: 244) +data micro_atx_depth: Millimeter = millimeter(count: 244) diff --git a/dag/gunbc/product/printed_chassis/coupon.dag b/dag/gunbc/product/printed_chassis/coupon.dag new file mode 100644 index 00000000000..35302154c62 --- /dev/null +++ b/dag/gunbc/product/printed_chassis/coupon.dag @@ -0,0 +1,432 @@ +module product.printed_chassis.coupon +import std.types { Bool, Int, List, NonEmptyStr } +import std.nat { Nat, nat_range_inclusive } +import std.measure { Micrometer, micrometer, micrometer_count, Millimeter, millimeter } +import extdeps.printing.fdm { + BuildEnvelope, + PartExtent, + EnvelopeFit, + PartFits, + PartExceedsEnvelope, + part_extent, + envelope_fit, +} +// THE CALIBRATION COUPON AUTHORITY — TOOLCHAIN v0's only consumer, and the reason v0 exists at all. +// +// WHY A COUPON IS THE FIRST THING MODELLED. It is the one part class whose dimensions depend on no +// unmeasured server component and no site dimension: a hole-diameter ladder is a fact about a +// PRINTER, not about a board. So it can be generated, printed and measured while the board's +// standoff map, the PETG decision and the deployment envelope are all still open — and it produces +// exactly the printer/material qualification that every later tolerance rests on. Building the +// realization contract against an empty measurement pack instead would have been speculative: a +// geometry-taint wall is not commissioned until it watches real geometry calls and rejects real +// mutations, and a wall with no handler is only a rule definition. +// +// THE LADDER IS AN EXPERIMENTAL DESIGN, NOT A CONVENIENCE. This is the whole point of the module. +// The tempting shape is a Python list of plausible diameters, on the reasoning that it is only a +// test part. That reasoning is exactly backwards: a ladder whose steps were chosen in the handler +// would make the MEASUREMENT meaningless, because the deviation being measured is deviation FROM A +// NOMINAL, and the nominal would then have no authority. "It is only a calibration coupon" is not +// permission for the realization layer to choose test dimensions. So the base, the step and the +// population size are modelled here, and every diameter in the ladder is DERIVED from them. +// +// WHY DERIVED RATHER THAN ENUMERATED. An authored list of diameters and an authored step are two +// representations of one fact, and they can disagree — DESIGN §2's horizontal redundancy, in the +// place where a disagreement is least visible, because both spellings look like data. Deriving the +// rungs means the step is the single authority and a mis-typed rung has no way to exist. +// +// UNITS ARE MICROMETRES THROUGHOUT, for the reason extdeps.printing.fdm records: the quantum is +// chosen from the smallest distinction the quantity must preserve. A clearance ladder steps in +// fifty-micrometre increments, which whole millimetres cannot represent at all — every rung would +// collapse onto its neighbours and the ladder would measure nothing. +// IDENTITY IS A CLOSED COPRODUCT, NOT A BRANDED STRING, AND THE PREVIOUS SHAPE IS WHY. +// +// It was `CouponSpecimenId = NonEmptyStr where brand(...)` beside a `CouponRevision` of the same +// shape, stamped by a generic mint that also accepted arbitrary plate and features. A sole +// constructor that still takes arbitrary identity TEXT next to arbitrary GEOMETRY does not bind the +// two: nothing stopped a caller minting the r1 identity onto a different ladder, which is precisely +// the attribution fault identity exists to prevent -- a measured result credited to geometry that +// never produced it. +// +// WHAT THIS DOES AND DOES NOT BUY, stated because the difference is the whole §4b question. It makes +// an UNSPELLABLE identity structurally impossible: there is no constructor for a specimen whose +// identity is a string somebody typed. It does NOT yet discriminate between coupons, because only +// one arm exists -- with a single specimen class the forbidden state "identity names coupon A while +// the geometry is coupon B" HAS NO CONSTRUCTOR AND NO FIXTURE THAT COULD AUTHOR IT, so a witness +// asserting it would be permanently green by construction and would carry no information. +// +// The field is therefore carried and not yet checked, deliberately. It becomes load-bearing when +// ProductionInterfaceCoupon lands and gives the coproduct a second arm, at which point the +// discriminating RED is authorable and owed. Recording it now rather than later is what stops the +// wire schema churning a second time. +type CouponSpecimenIdentity = HoleDiameterLadderR1 {} +// A ladder: a base rung, a uniform step, and how many rungs. The rung VALUES are derived. +type LengthLadder sole_constructor { + base: Micrometer + step: Micrometer + rung_count: Nat +} +// The mint refuses a degenerate ladder rather than emitting one. A zero step makes every rung +// identical, so the coupon would carry N copies of one measurement while presenting as a ladder — +// a specimen that cannot discriminate, which is the physical twin of a check that never goes red. +// Fewer than two rungs is not a ladder either: a single-rung "ladder" measures one diameter and +// establishes no trend, and the caller almost certainly meant to author a plain feature. +type LadderConstruction + = LadderReady { ladder: LengthLadder } + | LadderStepIsZero + | LadderTooFewRungs { supplied: Nat } +fn length_ladder(base: Micrometer, step: Micrometer, rung_count: Nat) -> LadderConstruction { + if micrometer_count(m: step) == 0 { + LadderStepIsZero + } else if rung_count < 2 { + LadderTooFewRungs { supplied: rung_count } + } else { + LadderReady { ladder: LengthLadder { base: base, step: step, rung_count: rung_count } } + } +} +// The rungs, derived. This is the only place a coupon's nominal values come from. +fn ladder_rungs(l: LengthLadder) -> List { + fold(nat_range_inclusive(lo: 0, hi: l.rung_count - 1), init: [], f: fn(acc, i) { + concat(acc, [micrometer(count: micrometer_count(m: l.base) + i * micrometer_count(m: l.step))]) + }) +} +fn ladder_rung_count(l: LengthLadder) -> Nat { l.rung_count } +fn ladder_base(l: LengthLadder) -> Micrometer { l.base } +fn ladder_step(l: LengthLadder) -> Micrometer { l.step } +// THE v0 OPERATION POPULATION, CLOSED, and closed on a rule rather than on taste: an operation is +// admitted to v0 only because a selected specimen below consumes it. Nothing here anticipates the +// chassis — no fillet, no sweep, no loft, no rack joint — because TOOLCHAIN generalizes exactly one +// consumer ahead. FIT will widen this population, and CASSETTE will widen it again, each time with +// the wall coverage that admits the new operation. +// +// The realization handler MAY map these to kernel calls and choose provably equivalent orderings. +// It may NOT introduce an operation absent from this coproduct: an unknown operation kind has no +// constructor here, so a handler that invented one could not describe it in a contract at all. +// V0 CARRIES ONE OPERATION, AND DROPPING THE OTHER IS THE POINT OF THIS REVISION. +// +// OpDatumMark { text, at_x, at_y } engraved a label. It fixed three things and left FONT, GLYPH +// METRICS, STROKE WIDTH, ALIGNMENT, ORIENTATION, DEPTH and ENGRAVED-VERSUS-EMBOSSED to the handler. +// That is the DESIGN section 3 tell in its exact form: the handler was CHOOSING geometry the model +// had not fixed, rather than implementing a derivation the model specified. A contract that +// underdetermines its own output is not a contract. +// +// It had already produced a silent falsehood. specimen_extent assumed the mark was ENGRAVED and +// therefore could not enlarge the plate -- an assumption stated nowhere and enforced by nothing. A +// handler that embossed would produce a part taller than the model says it is, and the envelope-fit +// answer would be wrong in the unsafe direction, which is the one direction that matters. +// +// The alternative was to determine it fully, which means modelling fonts. That is a domain, not a +// field, and it would be imported to place a label on a calibration coupon. +// +// THE NEED BEHIND IT IS REAL AND IS NOT DROPPED: several coupons will exist physically and must be +// told apart by hand. Recorded as a V1 obligation rather than left implicit, with the route that +// looks right -- identify the coupon by GEOMETRY, a coded notch or hole pattern, which OpThroughHole +// already determines completely. That buys physical identification without importing typography, and +// it is checked by the same contract the holes already pass through. +// THIS ROW WAS A STRING BEGINNING "OPEN: ...", WHICH IS THE §4c VIOLATION THIS MODULE OTHERWISE +// REPAIRS. A dissolution condition is exactly what §4c names as belonging in a typed carrier, and +// `Altrad8udMountingUnknown` two files over is the same shape done correctly: a closed coproduct of +// open obligations plus a TOTAL fold that says how each one discharges. The prose row was written in +// the same commit that deleted OpDatumMark for underdetermining its own output, and it underdetermined +// its own: nothing could read it, so the obligation was invisible to every lens over the tree. +// +// The route is carried as its own coproduct rather than as free text so that "how does this +// discharge" is answered by a total function. A second obligation added later cannot be forgotten by +// the route fold -- the match stops compiling until it is handled, which is the property a string +// roster can never have. +// ONE OBLIGATION WAS DOING TWO JOBS, AND SPLITTING IT IS WHAT MADE HALF OF IT DISCHARGEABLE. +// +// `PhysicalCouponIdentificationUnsolved` conflated two questions that have different consumers, +// different routes and different closing dates (routed review, 2026-09-02): +// +// ORIENTATION -- which end of THIS coupon is the 3.00 mm end. The ladder steps 0.10 mm across +// eleven rungs, so end to end the holes differ by 1 mm and are visually interchangeable; rotated +// 180 degrees the coupon reads as a valid coupon with its ordinals reversed, and every measurement +// is then attributed to the wrong rung. This is a property of the CANONICAL GEOMETRY and it is +// discharged below, by making the geometry asymmetric. +// +// PRINT-INSTANCE ATTRIBUTION -- which printer and spool produced THIS piece of plastic. Two +// correctly-oriented R1 coupons, one from each printer, remain interchangeable, and swapping them +// attributes printer A's process to printer B. No geometry closes this, because the canonical +// datum must be IDENTICAL on both coupons or the two processes stop sharing a subject. It is +// discharged by the manufacturing manifest and a physical handling route, and it stays open. +// +// Holding them as one obligation is why the earlier route fold was near-vacuous: a single arm whose +// RED could not be authored. Two arms with different routes is not a bigger roster, it is the +// distinction that lets one of them close. +// +// `HoleDiameterLadderR1` is the coupon DESIGN identity. It is not the identity of a printed +// instance, and no amount of design identity will ever be. +type CouponV1Obligation = PhysicalPrintInstanceAttributionUnsolved {} + +type CouponV1Route = AttributeByManufacturingManifestAndHandling {} + +// TOTAL BY CONSTRUCTION, AND HONEST ABOUT WHAT THAT IS WORTH TODAY. Every open obligation names the +// route that would close it; no obligation may sit without one, because that is the state where a +// recorded need quietly becomes a wish. Adding a second obligation variant reds this match until it +// is handled, which is the property the string roster could never have. +// +// BUT THIS FOLD HAS NO RUNTIME CONSUMER YET, and that bounds the guarantee rather than voiding it. +// Its enforcement is the exhaustive-match rule at compile time, so it holds exactly as long as the +// function exists -- nothing prevents a later reader deleting an uncalled function and taking the +// forcing with it. Still one arm, so a witness calling it would be near-vacuous and none is written. +// An earlier cut said the consumer arrives with the SECOND OBLIGATION VARIANT. That was wrong about +// which event matters: the consumer arrives when the first coupon is PRINTED AND MEASURED, because +// that is when attributing a measurement to the wrong physical piece becomes possible. The roster +// growing is bookkeeping; the print is the hazard. +fn coupon_v1_route(o: CouponV1Obligation) -> CouponV1Route { + match o { + PhysicalPrintInstanceAttributionUnsolved {} => AttributeByManufacturingManifestAndHandling {} + } +} + +data coupon_v1_open_obligations: List = [PhysicalPrintInstanceAttributionUnsolved {}] + +type CouponOperation + = OpThroughHole { diameter: Micrometer, center_x: Micrometer, center_y: Micrometer } + +// THE PLATE IS ITS OWN TYPE, not a member of CouponOperation, and the first draft of this module +// had it as a member. That draft then needed a match to recover the plate's dimensions, whose other +// arm had nothing sensible to return — and what it returned was a zero extent, which fits every +// build envelope. A specimen with a malformed plate would have been reported PRINTABLE. The arm was +// a textbook absorbing fallback: no authority said the extent was zero, and answering zero destroyed +// the only signal that the specimen was malformed. +// +// Making the plate a dedicated type deletes the arm rather than fixing it. There is no non-plate +// plate to fall back FROM, so the fallback has no place to live — DESIGN §5's construction over +// validation, and the reason this is rung 4 rather than a checked refusal. +type PlateDimensions sole_constructor { + size_x: Micrometer + size_y: Micrometer + size_z: Micrometer +} + +// The mint exists because sole_constructor confines construction to THIS module, which is the point +// -- a plate is not a record any caller may assemble -- but the realization contract must be able to +// build one when it decodes a wire envelope. Exporting the mint keeps the single authority here +// rather than relaxing the type so the transport can reach past it. +fn plate_dimensions(size_x: Micrometer, size_y: Micrometer, size_z: Micrometer) -> PlateDimensions { + PlateDimensions { size_x: size_x, size_y: size_y, size_z: size_z } +} +// THE DATUM IS ITS OWN FIELD, NOT ANOTHER ENTRY IN THE FEATURE LIST, AND THAT IS THE WHOLE POINT. +// +// The obvious cut is to append one more OpThroughHole to `features` and remember that the last one +// is the datum. That makes "which hole is the datum" a POSITIONAL convention -- the same class this +// module already deleted once, when the raw envelope carried operation kinds and diameters as two +// parallel lists whose correspondence was enforced by nothing. It is worse here than there, because +// the datum exists precisely to remove an ambiguous reading, and a convention about list position is +// an ambiguous reading. +// +// Separate fields make four things structural rather than checked: +// - exactly one orientation datum exists (it is a scalar, not a list, so zero and two are +// unwritable rather than refused); +// - the datum cannot enter the ladder population, so it cannot become a twelfth rung; +// - canonical geometry with no datum has no representation at all; +// - every consumer that reads holes must say WHICH population it means, so the eleven measured +// rungs stay one separately named thing. +// +// This is deliberately NOT a generic tagged feature graph. A `CouponFeatureIdentity` wrapper would +// also work and would carry a vocabulary invented for exactly one special feature, which is +// generalizing a full consumer ahead of the evidence. The dedicated field is narrower and says the +// same thing. +type HoleDiameterCouponGeometry sole_constructor { + plate: PlateDimensions + orientation_datum: CouponOperation + ladder_holes: List +} + +// Exported because the realization contract decodes wire rows into this shape and cannot reach a +// sole_constructor across the module boundary. The mint is total and carries no derivation: it takes +// already-built operations and names their populations, so it cannot be used to produce a geometry +// whose ladder disagrees with a declaration. The seal that matters is on the contract's decoded +// carrier, not here -- this is plain data, like PlateDimensions. +fn hole_diameter_coupon_geometry( + plate: PlateDimensions, + orientation_datum: CouponOperation, + ladder_holes: List, +) -> HoleDiameterCouponGeometry { + HoleDiameterCouponGeometry { + plate: plate, + orientation_datum: orientation_datum, + ladder_holes: ladder_holes, + } +} + +// A specimen is its geometry plus its identity, so a measured result can never be attributed to the +// wrong geometry. The identity is the DESIGN's, and the design is what the ladder and the datum +// together fix -- see the two-obligation split above for why it is not the printed piece's identity. +type CouponSpecimen sole_constructor { + identity: CouponSpecimenIdentity + geometry: HoleDiameterCouponGeometry +} +// SPECIMEN 1 — THE HOLE-DIAMETER LADDER. Eleven rungs from 3.00 mm in 0.10 mm steps, so the ladder +// spans 3.00 to 4.00 mm and brackets the M3 clearance region a printed chassis actually fastens +// with. The rungs are DERIVED from this declaration; changing the step here moves every hole and +// cannot leave a stale rung behind. +data hole_ladder_spec: LadderConstruction = length_ladder( + base: micrometer(count: 3000), + step: micrometer(count: 100), + rung_count: 11 +) +data hole_ladder_pitch: Micrometer = micrometer(count: 9000) +data hole_ladder_margin: Micrometer = micrometer(count: 6000) +data hole_ladder_plate_depth: Micrometer = micrometer(count: 18000) +data hole_ladder_plate_thickness: Micrometer = micrometer(count: 4000) +// The plate is SIZED FROM THE LADDER rather than authored beside it. An authored plate width would +// be a second representation of the ladder's extent, and the two would silently disagree the moment +// a rung was added — the coupon would then either crowd its last hole into the edge or carry dead +// plastic, and in both cases the geometry would stop matching the declaration that named it. +fn hole_ladder_plate_width(l: LengthLadder) -> Micrometer { + micrometer(count: 2 * micrometer_count(m: hole_ladder_margin) + (ladder_rung_count(l: l) - 1) * micrometer_count(m: hole_ladder_pitch)) +} +// THE HOLES ARE THE RUNGS. This function folds over ladder_rungs and does NOT recompute the series. +// +// THE FIRST REVISION RECOMPUTED IT, and that was the most serious defect in this module — found in +// review, not by any witness here, because no witness could see it. Both this function and +// ladder_rungs independently evaluated base + i * step, so there were TWO derivations of one law +// while the module's own annotation claimed there was one. The contract layer then compared +// ladder_rungs against the handler's output and reported conformance, while the holes actually cut +// into the plate came from this other computation entirely. Change the step here alone and every +// witness stays green while the physical coupon carries the wrong holes — and the coupon's whole +// purpose is to be the nominal that later measurements are deviations FROM, so a wrong coupon +// silently miscalibrates every tolerance derived from it. +// +// That is DESIGN §2 horizontal redundancy in its most expensive form: not two authored spellings +// that a reader might notice disagree, but two derivations of one law where only one is checked. +// The check was real, the wall was real, and they were pointed at a sidecar. +// +// The index is carried in the fold accumulator rather than recovered by position, because a second +// nat_range over the same rung count would reintroduce exactly the parallel enumeration this repair +// removes. +type HoleLadderAcc sole_constructor { + index: Int + ops: List +} + +fn hole_ladder_features(l: LengthLadder) -> List { + fold(ladder_rungs(l: l), init: HoleLadderAcc { index: 0, ops: [] }, f: fn(acc, rung) { + HoleLadderAcc { + index: acc.index + 1, + ops: concat(acc.ops, [OpThroughHole { + diameter: rung, + center_x: micrometer(count: micrometer_count(m: hole_ladder_margin) + acc.index * micrometer_count(m: hole_ladder_pitch)), + center_y: micrometer(count: 9000), + }]) + } + }).ops +} + +// THE ORIENTATION DATUM. One extra through-hole whose position makes a 180-degree reading of the +// coupon inconsistent with the geometry, so a measurer can tell which end is 3.00 mm by looking. +// +// EVERY NUMBER HERE IS DERIVED, and the one that matters most is the x. The datum sits at the SAME x +// AS RUNG ZERO, so the physical relation it asserts is "this is the ordinal-zero end" and not the +// weaker "there is a hole somewhere off centre". A datum that only proved the coupon was asymmetric +// would still leave a measurer guessing which asymmetry meant which end. +// +// IT READS `hole_ladder_margin`, THE SAME ROW THE LADDER FOLD READS, and that is shared authority +// rather than the second-derivation defect this module has already paid for once. The fold's term +// for rung i is `margin + i * pitch`; at i = 0 that is `margin` itself, so there is one row and two +// readers, not two computations of one law. The dangerous shape was recomputing the LADDER law -- +// base + i * step -- beside ladder_rungs, where the two could drift while both looked derived. +// +// An earlier cut of this function read rung zero's x back off the built feature list instead, to +// make the correspondence structural. That was worse, and the substrate said so: `.first()` returns +// an option, so it forced an `Absent` arm for a ladder that cannot be empty -- and the arm I wrote +// fabricated a plausible datum at the margin. That is the absorbing fallback in miniature: an +// unreachable branch answering with an invented value instead of refusing, sitting inside the one +// function whose output the whole orientation guarantee rests on. Reading the shared row has no +// unreachable branch to fabricate in. +// +// The correspondence is therefore asserted by a witness rather than by construction, and that is a +// real if small step down the ladder: it is mechanically preventable, not structurally impossible. +// The trigger that would close it is a ladder carrying its rung-zero origin as a value the datum can +// take directly, which is a change to LengthLadder rather than to this function. +// +// Its DIAMETER is the ladder base rather than a fresh calibration number, because a diameter nobody +// derived is a coincidence waiting to drift and the base is already the value this end is named for. +// +// Its y is off the ladder centre-line by construction. The rungs sit at y = 9000 and the widest is +// 4000 across, so the ladder band is [7000, 11000]; the datum at y = 4000 with the base diameter +// occupies [2500, 5500], which clears the band by 1500 um and the plate edge by 2500 um. Those two +// clearances are asserted by witnesses rather than eyeballed here, because a clearance stated in an +// annotation is a clearance nothing checks. +data hole_ladder_datum_center_y: Micrometer = micrometer(count: 4000) + +fn hole_ladder_orientation_datum(l: LengthLadder) -> CouponOperation { + OpThroughHole { + diameter: ladder_base(l: l), + center_x: hole_ladder_margin, + center_y: hole_ladder_datum_center_y, + } +} + +// The specimen's LADDER hole diameters, projected back out so a consumer can check that the geometry +// and the ladder agree WITHOUT trusting this module's claim that they do. This is what the contract +// layer must compare against — not ladder_rungs, which is the law rather than the artifact. +// +// IT READS `ladder_holes` AND NOTHING ELSE, and the rename from `specimen_hole_diameters` is the +// point rather than tidying. The datum is a through-hole of exactly the base diameter, so a +// projection over "the specimen's holes" would have silently returned twelve diameters beginning +// 3.00, 3.00 -- turning the eleven-rung count into twelve, shifting every ordinal by one, and making +// the first-divergent-rung comparison report position 1 for a fault at position 0. Every one of those +// failures is silent and lands in the measurement the coupon exists to produce. +fn specimen_ladder_hole_diameters(s: CouponSpecimen) -> List { + fold(s.geometry.ladder_holes, init: [], f: fn(acc, op) { + match op { + OpThroughHole { diameter: d, center_x: _, center_y: _ } => concat(acc, [d]) + } + }) +} + +// THE GENERIC MINT IS GONE AND THIS IS THE ONLY ONE. `coupon_specimen(id, revision, plate, features)` +// had exactly one caller -- this function -- and every argument it accepted was a way to build a +// specimen whose identity disagreed with its geometry. Deleting it costs nothing and removes the +// whole class: a specimen can now only be produced by a function that derives its geometry from the +// declaration it names. +fn hole_ladder_specimen(l: LengthLadder) -> CouponSpecimen { + CouponSpecimen { + identity: HoleDiameterLadderR1 {}, + geometry: HoleDiameterCouponGeometry { + plate: PlateDimensions { + size_x: hole_ladder_plate_width(l: l), + size_y: hole_ladder_plate_depth, + size_z: hole_ladder_plate_thickness, + }, + orientation_datum: hole_ladder_orientation_datum(l: l), + ladder_holes: hole_ladder_features(l: l), + }, + } +} +// MICROMETRES TO MILLIMETRES ROUNDS UP, AND THE DIRECTION IS THE WHOLE SAFETY ARGUMENT. +// +// The build envelope is stated in whole millimetres and the coupon is drawn in micrometres, so the +// fit question needs a conversion. Truncating is the arithmetic default and is WRONG HERE: a part +// 180_500 um across truncates to 180 mm, compares equal to a 180 mm envelope, and is reported as +// fitting when it physically does not. The error is silent, it is in the unsafe direction, and it +// appears only as a failed print. +// +// Rounding up cannot make that mistake. It can only ever over-state the part, so it may refuse a +// part that would in fact have squeezed in — a wasted refusal, which is recoverable by measuring, +// where a wasted print is not. This is the ordinary fail-closed asymmetry: the conservative +// direction is the one whose error is visible. +fn micrometer_to_millimeter_ceiling(m: Micrometer) -> Millimeter { + millimeter(count: (micrometer_count(m: m) + 999) / 1000) +} + +// A specimen's printed extent is its plate's. Features are cut INTO the plate — a through-hole +// removes material and a datum mark is engraved — so none of them can enlarge the bounding box. +// That is a property of the closed v0 operation population, not a general truth, and it stops being +// true the moment v0 admits an operation that adds material outside the plate. Whichever change +// introduces such an operation owes this function a real bounding-box fold. +fn specimen_extent(s: CouponSpecimen) -> PartExtent { + part_extent( + x: micrometer_to_millimeter_ceiling(m: s.geometry.plate.size_x), + y: micrometer_to_millimeter_ceiling(m: s.geometry.plate.size_y), + z: micrometer_to_millimeter_ceiling(m: s.geometry.plate.size_z) + ) +} + +fn specimen_fits(envelope: BuildEnvelope, s: CouponSpecimen) -> EnvelopeFit { + envelope_fit(envelope: envelope, part: specimen_extent(s: s)) +} diff --git a/dag/gunbc/product/printed_chassis/measurement.dag b/dag/gunbc/product/printed_chassis/measurement.dag new file mode 100644 index 00000000000..912d3077ec1 --- /dev/null +++ b/dag/gunbc/product/printed_chassis/measurement.dag @@ -0,0 +1,198 @@ +module product.printed_chassis.measurement + +import std.types { Bool, Int, List, NonEmptyStr } +import std.measure { Millimeter } +import std.claim_evidence { EvidenceLink, InferenceRuleId } +import product.spatial_dimension { LengthInterval, length_uncertainty_admissible } +import std.spatial_knowledge { + SpatialKnowledge, + SpatialMeasured, + SpatialEstimated, + SpatialHypothesis, + SpatialUnknown, + SpatialRequirement, + SpatialAdmission, + SpatialRefused, + SpatialGeometryUnknown, + MinimumSpatialStanding, + MeasuredOnly, + MeasuredOrEstimated, + admit_spatial_decision_input, +} + +// THE PHYSICAL AUTHORITY PACK for the printed node chassis: the second product-layer binding of +// SPATIAL-1, after product.spatial_dimension bound it for rooms. It supplies the same four things +// that binding did — identity, evidence, obligation, method — for a different subject universe, and +// it exists because the chassis program's failure mode is precisely the one SPATIAL-1 was landed +// against: a generator that draws a confident bracket around a cooler nobody measured. +// +// WHY THIS IS A BINDING AND NOT A NEW CARRIER. Every part of the epistemics is already modelled. +// SpatialKnowledge distinguishes measured from estimated from hypothesised from UNKNOWN, and the +// unknown arm carries an obligation rather than a number — which is the entire fail-closed +// requirement of this program stated in a type that already exists. SpatialRequirement carries a +// precision budget, so "the consuming decision sets the tolerance, not the instrument" is enforced +// rather than asserted. Minting a chassis-specific measurement record beside these would have been +// the parallel-representation fork DESIGN §3 forbids, and would have re-derived the estimate-is-a- +// region distinction that module's header records paying for once already. +// +// THE ONE RULE THIS MODULE ADDS, and it is the one the fabrication program turns on: a subject the +// roster does not mention is UNKNOWN, and unknown REFUSES. It does not fall back to a nominal +// catalogue figure, a form-factor standard, or a neighbouring subject's value. DESIGN §5's +// absorbing fallback is exactly the tempting arm here — an 80 mm fan is 80 mm, surely — and it +// fails open twice: the generator draws a part against a number no authority supplied, and the +// deficit stops being countable, so the measurement never gets taken. +type MeasurementObligationId = NonEmptyStr where brand("MeasurementObligationId") + +// The evidence payload is a claim-evidence link, matching the room binding: provenance, inference +// rule, freshness, fidelity and probe independence, rather than a prose string that reads as +// authoritative because it is spelled confidently. +type ChassisMeasurementEvidence = + EvidenceLink + +type ChassisLengthStanding = + SpatialKnowledge + +type ChassisLengthAdmission = + SpatialAdmission + +// THE SUBJECTS. Each is an independently measured physical object, and the cooler variants are +// SEPARATE subjects rather than one subject with a height parameter: they are different products +// with different envelopes, and collapsing them would let a 2U measurement satisfy a 4U obligation. +// This roster is deliberately closed — a subject the chassis needs and this list lacks fails to +// compile at the point of use rather than resolving to a default. +type FabricationSubject + = Altrad8udBoard + | CpuCoolerFourU + | CpuCoolerTwoU + | NodePowerSupply + | Fan80mm + | InstalledDimm + | RearIoAperture + +type FabricationAxis + = FabWidth + | FabDepth + | FabHeight + +type FabricationMeasurementKey sole_constructor { + subject: FabricationSubject + axis: FabricationAxis +} + +fn fabrication_measurement_key(subject: FabricationSubject, axis: FabricationAxis) -> FabricationMeasurementKey { + FabricationMeasurementKey { subject: subject, axis: axis } +} + +type FabricationMeasurement sole_constructor { + key: FabricationMeasurementKey + standing: ChassisLengthStanding +} + +// FabricationMeasurement is sole_constructor, so consumers reach it through this mint rather than +// a literal. That is what keeps the key and its standing from being paired by anyone who happens to +// hold both — a measurement whose key disagrees with the subject it was taken from is exactly the +// mis-binding witness 3 exists to catch, and it should be constructible in one place only. +fn fabrication_measurement(key: FabricationMeasurementKey, standing: ChassisLengthStanding) -> FabricationMeasurement { + FabricationMeasurement { key: key, standing: standing } +} + +// EQUALITY IS THE SUBSTRATE'S. An earlier revision projected FabricationSubject and FabricationAxis +// to integer ordinals and compared those, to avoid a wildcard over a closed coproduct. `==` is +// structurally defined for closed coproducts here, so the ordinals re-derived a law the language +// already carries -- and worse, a subject added later would silently need a hand-written ordinal, +// which is the very extension hazard the projection was introduced to close. +fn fabrication_subject_eq(a: FabricationSubject, b: FabricationSubject) -> Bool { + a == b +} + +fn fabrication_axis_eq(a: FabricationAxis, b: FabricationAxis) -> Bool { + a == b +} + +fn fabrication_measurement_key_eq(a: FabricationMeasurementKey, b: FabricationMeasurementKey) -> Bool { + fabrication_subject_eq(a: a.subject, b: b.subject) && fabrication_axis_eq(a: a.axis, b: b.axis) +} + +// TWO ARMS FAIL OPEN HERE IF THIS IS WRITTEN AS A PLAIN LOOKUP, AND ONLY ONE IS OBVIOUS. +// +// THE ABSENT CASE is the obvious one. A key the roster does not carry resolves to SpatialUnknown +// carrying the obligation that would clear it — never to Absent, which a caller can pattern-match +// past with a default, and never to a nominal figure. The obligation names the subject and axis, so +// an unmeasured dimension is a countable, located deficit rather than a silence that only surfaces +// when a printed part does not fit. +// +// THE DUPLICATE CASE is the one the first revision of this module got wrong. A fold that returns +// row.standing on every match silently keeps the LAST one, so two conflicting measurements of the +// same cooler height — a re-measure that disagreed, a row pasted under the wrong subject, two +// operators measuring different units of the same product — resolve to whichever sorts later in the +// list. Nothing refuses, nothing is counted, and the generator draws a part against a number whose +// contradiction is sitting three lines above it in the same roster. That is DESIGN §5's silent +// wrongness rather than a rung on the ladder: the roster contains the evidence that the value is in +// dispute, and the reader throws it away. +// +// So the scan carries the COUNT as well as the standing, and disagreement becomes its own refusal +// arm rather than a resolution rule. There is deliberately no "prefer the most precise" or "prefer +// the most recent" tie-break: both are heuristics standing where a human decision belongs, and a +// tie-break would make the conflict permanently invisible — which is exactly the property that let +// the bug exist. +type RosterScan sole_constructor { + count: Int + standing: ChassisLengthStanding +} + +fn scan_roster( + roster: List, + key: FabricationMeasurementKey, + obligation: MeasurementObligationId, +) -> RosterScan { + fold(roster, init: RosterScan { count: 0, standing: SpatialUnknown { obligation: obligation } }, f: fn(acc, row) { + match fabrication_measurement_key_eq(a: row.key, b: key) { + true => RosterScan { count: acc.count + 1, standing: row.standing } + false => acc + } + }) +} + +// The generator's answer. ChassisRosterConflict is NOT a variant of "unknown": an unknown dimension +// is cleared by taking a measurement, and a conflicted one is cleared by deciding which measurement +// is right and deleting the other. Different obligations, so different arms. +type ChassisMeasurementOutcome + = ChassisMeasurementJudged { admission: ChassisLengthAdmission } + | ChassisRosterConflict { key: FabricationMeasurementKey, count: Int } + +// THE GENERATOR'S ENTRY POINT, and the reason the CAD layer cannot invent a dimension: it asks for +// a length by key and receives an OUTCOME whose every non-judged arm is typed. There is no arm that +// yields a bare Millimeter without having passed the conflict, standing and precision checks, so +// "the generator substituted a plausible value" is not a thing this interface can express. +fn required_chassis_length( + roster: List, + key: FabricationMeasurementKey, + obligation: MeasurementObligationId, + requirement: SpatialRequirement, +) -> ChassisMeasurementOutcome { + let scan = scan_roster(roster: roster, key: key, obligation: obligation) + if scan.count > 1 { + ChassisRosterConflict { key: key, count: scan.count } + } else { + ChassisMeasurementJudged { + admission: admit_spatial_decision_input( + knowledge: scan.standing, + requirement: requirement, + uncertainty_admissible: length_uncertainty_admissible, + ) + } + } +} + +// THE MVP ROSTER IS EMPTY, AND THAT IS THE HONEST STATE ON 2026-09-01. +// +// Not one chassis-critical dimension has been measured yet. The board OUTLINE is vendor-dimensioned +// in extdeps.boards.asrock_rack and is deliberately NOT copied here — that would be the transcribed +// measurement DESIGN §6 forbids, a number unreachable from the authority that owns it. Everything +// else in FabricationSubject is an open obligation. +// +// An empty roster is not a placeholder standing in for work not yet done: it is the correct value, +// and it makes every required_chassis_length call refuse today. That is the property the program +// wants — the generator cannot produce a part until the measurement exists — and it is why this row +// lands before the CAD toolchain rather than after it. +data mvp_measurement_roster: List = [] diff --git a/dag/gunbc/product/printed_chassis/realization_contract.dag b/dag/gunbc/product/printed_chassis/realization_contract.dag new file mode 100644 index 00000000000..cb892906d54 --- /dev/null +++ b/dag/gunbc/product/printed_chassis/realization_contract.dag @@ -0,0 +1,649 @@ +module product.printed_chassis.realization_contract +import std.types { Bool, Int, List, NonEmptyStr } +import v2.std.algebra { zip_map } +import std.nat { Nat } +import std.measure { Micrometer, micrometer, micrometer_count } +import product.printed_chassis.coupon { + hole_ladder_specimen, + LengthLadder, + CouponSpecimen, + CouponOperation, + OpThroughHole, + PlateDimensions, + plate_dimensions, + HoleDiameterCouponGeometry, + hole_diameter_coupon_geometry, + ladder_rungs, + ladder_base, + ladder_step, + ladder_rung_count, +} +// REALIZATION CONTRACT v0 — the transport between the .dag authority and the CAD handler. +// +// IT DEFINES NO GEOMETRY VOCABULARY OF ITS OWN, AND THAT IS THE MAIN DECISION IN THIS FILE. +// +// The obvious shape for a transport is a parallel set of "contract feature" types — ContractHole +// beside OpThroughHole, ContractPlate beside PlateDimensions — on the reasoning that the wire format +// should be decoupled from the model. That reasoning is wrong here and it is wrong in the specific +// way DESIGN §3 names: two structures answering one semantic question, where one is intended to +// track the other. They would drift. A hole gains a countersink in the coupon vocabulary, the +// contract vocabulary does not, and the handler silently realizes a hole with no countersink while +// every type still checks. +// +// So the contract CARRIES the coupon's own closed operation coproduct. CouponOperation is already +// exactly what a schema-bound feature graph needs to be: closed, so an unknown operation kind has no +// constructor; total, so every arm carries its own required fields; and owned by the module that +// decides what a coupon is. Serializing it is a realization concern that adds no vocabulary. +// +// WHAT THE CONTRACT ADDS is the three facts the specimen does not carry and the handler cannot be +// trusted to supply: which contract version this is, which derivation law produced the derived +// values, and the derived values themselves for cross-checking. +// THE SCHEMA WALL LIVES AT THE RAW BOUNDARY, AND AN EARLIER REVISION DELETED IT FOR THE WRONG +// REASON. This is the correction, and the reasoning error is worth more than the wall. +// +// The first draft declared `type ContractVersion = ContractV0` with a ContractVersionUnsupported +// arm, and that arm really was unfirable: one version exists, so no value of that TYPE can carry an +// unknown version. It was deleted as a DESIGN section 4b decoration -- a check whose RED cannot be +// authored, permanently green, worse than absent because it gets cited as coverage. +// +// That reasoning checked one boundary and section 4b names TWO, saying explicitly that "only the +// second decides it": a state unrepresentable in the ACCEPTED CORPUS may still be perfectly +// representable as SOURCE HANDED IN BY A FIXTURE. The handler does not send a `ContractVersion`. It +// sends JSON, and JSON can say "v999" -- so the forbidden state is authorable at the transport +// boundary, has always been authorable there, and the deleted check was not a decoration but a wall +// standing in the wrong place. Deleting it removed a real refusal. +// +// So the vocabulary is split. RawRealizationEnvelope is what ARRIVES: strings and integers, no +// modeled types, nothing yet trusted. Admission is the total decision procedure that turns one into +// modeled values or refuses with a located cause. Nothing downstream sees an unadmitted envelope, +// which is the construction that makes the typed side safe -- rather than a validation bolted onto +// a type that was already unable to express the fault. +// ONE ROW PER OPERATION, NOT TWO PARALLEL LISTS. The previous shape carried operation_kinds and +// rung_diameters_um side by side, so their correspondence was POSITIONAL and enforced by nothing: a +// two-kind, three-diameter envelope was perfectly representable, and admission had no way to say +// which diameter belonged to which operation. Making the row the unit removes that state rather than +// checking for it -- a ragged pairing has no constructor. +// +// The geometry is carried in FULL. Diameter alone was the sidecar in another costume: a handler that +// realized the right diameters at the wrong centres, or on a plate of the wrong thickness, passed a +// wall whose entire purpose was to catch exactly that. +type RawOperationRow sole_constructor { + kind: NonEmptyStr + diameter_um: Int + center_x_um: Int + center_y_um: Int +} + +fn raw_operation_row( + kind: NonEmptyStr, + diameter_um: Int, + center_x_um: Int, + center_y_um: Int, +) -> RawOperationRow { + RawOperationRow { + kind: kind, + diameter_um: diameter_um, + center_x_um: center_x_um, + center_y_um: center_y_um, + } +} + +// THE DATUM AND THE LADDER ARE SEPARATE WIRE FIELDS, AND THIS IS NOT A RETURN TO PARALLEL LISTS. +// +// The shape this file already deleted was operation_kinds beside rung_diameters_um: two lists of the +// SAME population whose correspondence was positional and enforced by nothing. These two fields are +// two DIFFERENT populations -- one orientation datum and one ordered experimental ladder -- which is +// the distinction that makes separating them the fix rather than the defect. Nothing here pairs an +// element of one with an element of the other, so there is no ragged state to represent. +// +// Carrying the datum inside `operations` would have made "the last row is the datum" a positional +// convention on the wire, one layer below the same convention the canonical geometry refuses to +// adopt. A handler that emitted them in the wrong order would then produce a coupon whose datum is a +// twelfth rung and whose ordinal zero is a datum, and the wall would compare twelve rows against +// twelve rows and find them equal. +type RawRealizationEnvelope sole_constructor { + schema_version: NonEmptyStr + plate_x_um: Int + plate_y_um: Int + plate_z_um: Int + orientation_datum: RawOperationRow + ladder_holes: List +} + +fn raw_realization_envelope( + schema_version: NonEmptyStr, + plate_x_um: Int, + plate_y_um: Int, + plate_z_um: Int, + orientation_datum: RawOperationRow, + ladder_holes: List, +) -> RawRealizationEnvelope { + RawRealizationEnvelope { + schema_version: schema_version, + plate_x_um: plate_x_um, + plate_y_um: plate_y_um, + plate_z_um: plate_z_um, + orientation_datum: orientation_datum, + ladder_holes: ladder_holes, + } +} + +// Every refusal names WHAT arrived, not merely that something was wrong. A handler debugging a +// rejected payload needs the offending spelling; "unsupported schema" alone sends them to read our +// source instead of their own output. +// Admission yields the MODEL'S OWN TYPES or nothing. It does not yield a validated raw envelope, +// because a raw envelope that has been checked is still a raw envelope, and the next reader has no +// way to tell it apart from an unchecked one. Decoding into PlateDimensions and CouponOperation is +// what makes the downstream total: there is no arm in which an unadmitted value reaches geometry. +// THE NAME SAYS DECODED, NOT ADMITTED, AND THE EARLIER NAME WAS THE OVERCLAIM. +// +// This type was called AdmittedRealization. It is minted by decode_envelope after schema and tag +// decoding and BEFORE any comparison against the canonical contract, so a caller may legally obtain +// one and never invoke judge_realization -- and "admitted" claimed a stronger standing than the +// function that mints it establishes. That is DESIGN section 3's meaning fork in its quietest form: +// the annotation cannot narrow what the type name claims, and the name is what the next reader +// imports. Renamed rather than re-annotated, before it becomes PRINT-5's vocabulary. The conformance +// verdict is renamed on the same reasoning: it compares normalized GEOMETRY, not the whole specimen, +// so GeometryConformance says what it decides. +// +// The terminal shape this leaves room for, and deliberately does not build yet: +// +// RawRealizationEnvelope -> DecodedRealizationV0 -> GeometryConforms -> AdmittedRealizationV0 +// +// where only the last is accepted by a handler, and carries geometry RE-DERIVED from the canonical +// model rather than the transported geometry that happened to compare equal. Nothing here mints that +// type, because nothing consumes it yet; the name is left free rather than spent. +// +// THE DECODED VALUE IS UNFORGEABLE, AND AN EARLIER REVISION ONLY CLAIMED IT WAS. +// +// That revision put the geometry directly on the accepted arm -- EnvelopeDecodedV0 { plate, features } +// -- and argued that conformance was unreachable without admission "because the refusal arms have no +// plate and no features to hand on". That reasoning is necessary and INSUFFICIENT, and a probe +// settled it: a foreign module compiled `EnvelopeDecodedV0 { plate: p, features: [] }` directly, with +// a deliberate must-fail control in the same file proving the compiler had actually read it. The raw +// envelope could not bypass the judge; a CALLER could bypass the raw envelope entirely and mint the +// trusted result. The accepted arm was itself a geometry mint. +// +// DecodedRealizationV0 is sole_constructor, so it can only be built inside THIS module, and the only +// function here that builds one is decode_envelope after every wire check has passed. A foreign +// module may still name the EnvelopeDecodedV0 arm; it cannot obtain a DecodedRealizationV0 to put in +// it. That moves the class from "no caller happens to do this" to "no caller can express this". +// +// THE EVIDENCE IS AN EXECUTING WITNESS. An earlier cut of this annotation said the evidence could +// only ever be the compiler, on the reasoning that the RED is a compile failure and so cannot be +// enrolled in a corpus that must compile. That reasoning skipped the distinction DESIGN 4b draws +// exactly here: a state unauthorable in the ACCEPTED CORPUS may still be authorable as SOURCE HANDED +// TO THE COMPILER BY A FIXTURE, and only the second boundary decides whether the check has a RED. +// It does. test.claim.printed_chassis_admitted_realization_seal_witness_test hands the forged record +// literal to gunbc.compile_diagnostic_census as data and asserts a SoleConstructorViolation scoped to +// subject_name DecodedRealizationV0, against a green source with identical imports and no literal, and +// asserts the difference between them -- the two forms that module's own annotation names as exact. +type DecodedRealizationV0 sole_constructor { + geometry: HoleDiameterCouponGeometry +} + +// The refusal reasons are their own closed coproduct, SEPARATE from the admission outcome, because +// the refusal payload must not be able to carry a success. An earlier cut typed +// RealizationRefusedAtWire { admission: EnvelopeAdmission }, so the refusal arm's payload included +// EnvelopeDecodedV0 -- unreachable in practice, since judge_realization only builds that arm on the +// three refusing branches, but perfectly writable, and reachability is not occupancy. The tell was +// visible in the witnesses rather than in this file: four of them carried a dead +// EnvelopeDecodedV0 { decoded: _ } => false arm to satisfy exhaustiveness over a case the route +// cannot produce. Splitting the coproduct climbs that class from mechanically preventable to +// structurally impossible and deletes those four arms with it -- DESIGN 4b(4) dissolution on climb, +// which retires the redundant PRODUCTION handling while the discriminating witnesses stay enrolled. +type EnvelopeRefusal + = EnvelopeSchemaUnsupported { received: NonEmptyStr, supported: NonEmptyStr } + | EnvelopeOperationUnknown { received: NonEmptyStr } + | EnvelopeCarriesNoOperations + +type EnvelopeAdmission + = EnvelopeDecodedV0 { decoded: DecodedRealizationV0 } + | EnvelopeRefused { refusal: EnvelopeRefusal } + +// The closed operation vocabulary AS SPELLED ON THE WIRE, and this roster is HAND-SYNCED to the +// CouponOperation arms rather than derived from them. That is a known weakness, stated here rather +// than discovered later, because it has already failed once. +// +// WHAT HAPPENED: this list read ["through_hole", "datum_mark"] while OpDatumMark was being deleted +// from CouponOperation. The compile stayed clean through the whole deletion, because a string in a +// list has no referent the namespace can refuse. For one revision the wall would have ADMITTED a +// datum_mark envelope into a vocabulary that no longer had a constructor for it -- the transport +// accepting what the model cannot represent, which is the precise inversion of what a wall is for. +// A stringly roster beside a closed coproduct is a second authority for the operation vocabulary, +// and it drifts in exactly the direction that fails open. +// +// THERE ARE TWO WALLS HERE AND ONLY ONE OF THEM IS CLOSABLE BY PROJECTION. An earlier revision of +// this annotation conflated them and would have retired too much. +// +// WALL ONE, SCHEMA SYNCHRONISATION: the model's operation population must equal the admitted wire-tag +// population. That is what this roster is, it is mechanically preventable and not structural, and its +// ceiling IS reachable -- projecting the spelling from the coproduct's arms would make a deleted arm +// delete its spelling in the same motion. NEXT-RUNG TRIGGER is that projection capability: enumerating +// a closed coproduct's constructors as data, together with a modeled TAG LAW, because OpThroughHole +// and "through_hole" are not automatically the same fact and equating them silently makes every arm +// rename a schema-breaking change. +// +// WALL TWO, DECODER BEHAVIOUR: an unknown or deleted tag must REFUSE BEFORE GEOMETRY. No projection +// closes this one. A decoder can still map an unknown tag onto a default known arm, skip the +// operation, or continue with a partial contract -- all of which are fail-open behaviours that a +// perfectly synchronised roster does not prevent. So w_the_deleted_operation_refuses_at_the_wire is +// evidence for BOTH walls today and remains permanently required for the second. It does not retire +// when the projection lands. It must never be deleted as redundant with the type, because that +// reasoning closes only wall one and would leave wall two unguarded. +data admitted_operation_kinds: List = ["through_hole"] + +fn operation_kind_admitted(kind: NonEmptyStr) -> Bool { + fold(admitted_operation_kinds, init: false, f: fn(acc, k) { acc || k == kind }) +} + +type OperationScan sole_constructor { + unknown: List +} + +fn decode_operation_row(row: RawOperationRow) -> CouponOperation { + OpThroughHole { + diameter: micrometer(count: row.diameter_um), + center_x: micrometer(count: row.center_x_um), + center_y: micrometer(count: row.center_y_um), + } +} + +// THE KIND SCAN COVERS BOTH POPULATIONS, DATUM FIRST. Scanning only the ladder would have left the +// datum row's kind unchecked, so a handler could have spelled it anything at all and the wall would +// have decoded it as a through-hole regardless -- the vocabulary check exempting the one feature +// whose whole job is to be unambiguous. +// +// AND THE EMPTY REFUSAL IS NOW ONLY EVER ABOUT THE LADDER. A missing DATUM is not representable +// here: it is a scalar field, so the wire cannot omit it. One of the two populations lost its empty +// state entirely, which is the split doing its work at the transport layer rather than at the check. +fn decode_envelope(envelope: RawRealizationEnvelope) -> EnvelopeAdmission { + if envelope.schema_version != contract_schema_version { + EnvelopeRefused { + refusal: EnvelopeSchemaUnsupported { + received: envelope.schema_version, + supported: contract_schema_version, + }, + } + } else { + let scan = fold( + concat([envelope.orientation_datum], envelope.ladder_holes), + init: OperationScan { unknown: [] }, + f: fn(acc, row) { + if operation_kind_admitted(kind: row.kind) { + acc + } else { + OperationScan { unknown: concat(acc.unknown, [row.kind]) } + } + } + ) + if scan.unknown.length() != 0 { + EnvelopeRefused { refusal: EnvelopeOperationUnknown { received: scan.unknown.first() } } + } else if envelope.ladder_holes.length() == 0 { + EnvelopeRefused { refusal: EnvelopeCarriesNoOperations } + } else { + EnvelopeDecodedV0 { + decoded: DecodedRealizationV0 { + geometry: hole_diameter_coupon_geometry( + plate: plate_dimensions( + size_x: micrometer(count: envelope.plate_x_um), + size_y: micrometer(count: envelope.plate_y_um), + size_z: micrometer(count: envelope.plate_z_um), + ), + orientation_datum: decode_operation_row(row: envelope.orientation_datum), + ladder_holes: fold(envelope.ladder_holes, init: [], f: fn(acc, row) { + concat(acc, [decode_operation_row(row: row)]) + }), + ), + }, + } + } + } +} + +data contract_schema_version: NonEmptyStr = "v0" +// THE DERIVATION IDENTITY IS CARRIED, NOT THE DERIVATION. +// +// The permitted-realization rule lets the handler IMPLEMENT a modeled derivation whose identity and +// inputs the model already fixed; it forbids the handler CHOOSING which derivation to run. Those two +// are separated by exactly this field. An arithmetic series and a geometric series over the same +// base and step produce different ladders, and a contract that named neither would leave the choice +// in Python — where it would be invisible, because the resulting part still looks like a ladder. +// +// The coproduct is closed so that adding a second derivation law is a modeling act with its own +// review, not a handler edit. +// THE DERIVATION LAW IS FIXED BY THIS CARRIER'S TYPE, not by a field, for the same reason. +// +// The intent is unchanged and is the load-bearing one: the handler may IMPLEMENT a derivation whose +// identity the model fixed, and may not CHOOSE which derivation to run. An arithmetic series and a +// geometric series over one base and step produce different ladders, and a contract naming neither +// would leave that choice in Python, invisible, because the result still looks like a ladder. +// +// With exactly one law in v0, a DerivationIdentity FIELD would be a single-arm coproduct — an alias +// wearing a choice's clothes, whose "wrong law" refusal is unauthorable. Instead LadderRealization +// IS the arithmetic-series realization: the law is the type. A handler cannot select a different law +// because the contract has no field in which to express one, which is construction rather than +// validation. Adding a second law is then a modeling act that splits this type, with review, rather +// than a handler edit. +// ONE DECLARATION IN, ONE CONTRACT OUT — AND THE TWO DEFECTS THIS REPLACED WERE BOTH REAL. +// +// DEFECT 1, UNBOUND PAIRING, found in review. The mint used to take a specimen and a ladder +// realization as SEPARATE parameters, so a specimen built from ladder A could be paired with a +// realization built from ladder B. Conformance would then compare B's rungs against A's holes, or +// worse agree by coincidence, while the contract claimed a coherence it had never checked. Nothing +// refused, because nothing related the two arguments. +// +// DEFECT 2, THE ORPHANED SIDECAR, which this branch created itself. LadderRealization carried a +// derived_rungs list beside the declaration, argued for as a cross-trust-domain checksum. Then the +// conformance repair moved the comparison onto specimen_hole_diameters — the artifact — which is +// correct, and left derived_rungs with NO production consumer at all. Its only remaining reader was +// a witness asserting that the field equalled the derivation it was built from: a check that tests +// only itself. A duplicate whose consumer is a test of the duplicate is not a checksum, it is dead +// data with a green light on it. +// +// Both dissolve into the same construction. The contract takes ONE authored declaration and derives +// the specimen from it. The pairing is unwritable rather than checked — there is no second argument +// to disagree with — and the rung list is gone because the specimen's own holes are the artifact +// conformance reads. The declaration remains because the handler needs the law it is realizing, not +// merely the result. +type RealizationContract sole_constructor { + schema_version: NonEmptyStr + declaration: LengthLadder + specimen: CouponSpecimen +} + +fn realization_contract(declaration: LengthLadder) -> RealizationContract { + RealizationContract { + schema_version: contract_schema_version, + declaration: declaration, + specimen: hole_ladder_specimen(l: declaration), + } +} + +// THE HANDLER-SIDE CHECK, expressed here so both sides read the same law. The handler recomputes the +// rungs from the declaration under the named derivation and compares. A length mismatch and a value +// mismatch are separate causes because they fail for different reasons: a length mismatch means the +// two sides disagree about the POPULATION, a value mismatch means they agree on how many rungs there +// are and disagree about where. +// THE COMPARED SUBJECT IS THE WHOLE SPECIMEN, NOT THE RUNG LIST. An earlier revision compared only +// hole diameters, which left plate dimensions and hole CENTRES outside the wall entirely: a handler +// that cut correct diameters at the wrong positions, or on a plate of the wrong thickness, conformed. +// That is the sidecar failure the diameter check was itself introduced to fix, reappearing one level +// out -- comparing a projection of the artifact instead of the artifact. +// +// The axis and field vocabularies are CLOSED COPRODUCTS rather than strings. This file has already +// paid once for a stringly vocabulary standing beside a typed one, and a diagnostic that names its +// axis as "z" is the same construction that let "datum_mark" outlive its constructor. +type PlateAxis = PlateAxisX | PlateAxisY | PlateAxisZ + +type OperationField = FieldDiameter | FieldCenterX | FieldCenterY + +// A WRONG DATUM GETS ITS OWN ARM RATHER THAN BEING FOLDED INTO THE RUNG SCAN, because it is not a +// rung fault and reporting it as one names a position that does not exist. GeometryOperationDiverges +// carries an INDEX into the ladder; the datum has no index, and giving it a synthetic one -- 0, or +// eleven, or minus one -- would be exactly the fabricated-plausible-output move DESIGN section 5 +// forbids. The two faults also mean different things to a reader: a divergent rung says the handler +// cut one hole wrong, a divergent datum says the coupon cannot be oriented and every rung ordinal is +// therefore in doubt. +type GeometryConformance + = GeometryConforms + | GeometryPlateDiverges { axis: PlateAxis, modeled: Micrometer, realized: Micrometer } + | GeometryDatumDiverges { field: OperationField, modeled: Micrometer, realized: Micrometer } + | GeometryOperationCountDiverges { modeled: Int, realized: Int } + | GeometryOperationDiverges { + index: Int, + field: OperationField, + modeled: Micrometer, + realized: Micrometer, + } +// THE SCAN IS ONE FOLD OVER ZIPPED PAIRS, and the shape is the point rather than the speed. +// +// The first revision recursed with `modeled.count() == 0` as its base case. List is an alias for +// FreeMonoid, so `.count()` walks the whole spine — an O(n) emptiness test inside an O(n) recursion, +// quadratic over the ladder. DESIGN section 6's bare-minimum-cost rule says that is always fixed and +// that "n is small here" is not a time-stable rebuttal, because reuse changes n. +// +// The cost was not the worse half. That recursion read `realized.first()` while only `modeled` was +// tested for emptiness, so it was total only because a separate count precheck happened to run +// first. Called with a shorter realized list it would have read past the end; called with a shorter +// MODELED list it would have returned GeometryConforms — a fabricated pass, which is precisely the +// absorbing fallback DESIGN section 5 forbids, guarded by nothing but a caller's good manners. +// +// Zipping removes the state rather than checking for it: a ragged pair has no representation, so the +// scan cannot be handed one. Two length reads (which the count diagnostic needs anyway), one zip and +// one fold — linear, and the raggedness question is answered by construction. +type RungComparison sole_constructor { + modeled: CouponOperation + realized: CouponOperation +} + +// The accumulator keeps the FIRST divergence rather than the last. A fold visits every pair, so +// without this the reported index would be the final mismatch, and "where does it first go wrong" is +// the only question an index answers usefully. +type RungScan sole_constructor { + index: Int + outcome: GeometryConformance +} + +// One operation pair, compared field by field, reporting the FIRST field that differs. Diameter is +// checked before position because a wrong diameter is a process fault and a wrong centre is a layout +// fault, and naming the process fault first is what an operator acts on. +fn operation_divergence(index: Int, m: CouponOperation, r: CouponOperation) -> GeometryConformance { + match m { + OpThroughHole { diameter: md, center_x: mx, center_y: my } => match r { + OpThroughHole { diameter: rd, center_x: rx, center_y: ry } => + if micrometer_count(m: md) != micrometer_count(m: rd) { + GeometryOperationDiverges { index: index, field: FieldDiameter, modeled: md, realized: rd } + } else if micrometer_count(m: mx) != micrometer_count(m: rx) { + GeometryOperationDiverges { index: index, field: FieldCenterX, modeled: mx, realized: rx } + } else if micrometer_count(m: my) != micrometer_count(m: ry) { + GeometryOperationDiverges { index: index, field: FieldCenterY, modeled: my, realized: ry } + } else { + GeometryConforms + } + } + } +} + +// The datum is compared field by field in the same order as a rung, so a reader learns the same +// three things in the same sequence, and the ONLY difference is which arm carries the answer. It +// reuses no code with operation_divergence deliberately: that function's whole signature is built +// around an index the datum does not have, and threading an optional index through it to serve one +// caller would put a nullable in the middle of the comparison the wall depends on. +fn datum_divergence(m: CouponOperation, r: CouponOperation) -> GeometryConformance { + match m { + OpThroughHole { diameter: md, center_x: mx, center_y: my } => match r { + OpThroughHole { diameter: rd, center_x: rx, center_y: ry } => + if micrometer_count(m: md) != micrometer_count(m: rd) { + GeometryDatumDiverges { field: FieldDiameter, modeled: md, realized: rd } + } else if micrometer_count(m: mx) != micrometer_count(m: rx) { + GeometryDatumDiverges { field: FieldCenterX, modeled: mx, realized: rx } + } else if micrometer_count(m: my) != micrometer_count(m: ry) { + GeometryDatumDiverges { field: FieldCenterY, modeled: my, realized: ry } + } else { + GeometryConforms + } + } + } +} + +fn rung_scan_step(acc: RungScan, pair: RungComparison) -> RungScan { + match acc.outcome { + GeometryOperationDiverges { index: _, field: _, modeled: _, realized: _ } => + RungScan { index: acc.index + 1, outcome: acc.outcome } + GeometryPlateDiverges { axis: _, modeled: _, realized: _ } => + RungScan { index: acc.index + 1, outcome: acc.outcome } + GeometryDatumDiverges { field: _, modeled: _, realized: _ } => + RungScan { index: acc.index + 1, outcome: acc.outcome } + GeometryOperationCountDiverges { modeled: _, realized: _ } => + RungScan { index: acc.index + 1, outcome: acc.outcome } + GeometryConforms => + RungScan { + index: acc.index + 1, + outcome: operation_divergence(index: acc.index, m: pair.modeled, r: pair.realized), + } + } +} + +// Count is compared BEFORE values, and the order matters for the diagnostic rather than for +// correctness: with unequal lengths the first differing index is an artefact of where the shorter +// list ran out, so reporting it as a value divergence would name a position that means nothing. +fn compare_operations( + modeled: List, + realized: List, +) -> GeometryConformance { + let modeled_count = modeled.length() + let realized_count = realized.length() + if modeled_count != realized_count { + GeometryOperationCountDiverges { modeled: modeled_count, realized: realized_count } + } else { + fold( + zip_map(a: modeled, b: realized, f: fn(m, r) { + RungComparison { modeled: m, realized: r } + }), + init: RungScan { index: 0, outcome: GeometryConforms }, + f: rung_scan_step + ).outcome + } +} + +// The plate is compared BEFORE the operations, and the order is a diagnostic decision. A plate of +// the wrong thickness makes every hole depth wrong at once, so reporting the first hole as divergent +// would name a symptom and bury the cause. +fn compare_plate(modeled: PlateDimensions, realized: PlateDimensions) -> GeometryConformance { + if micrometer_count(m: modeled.size_x) != micrometer_count(m: realized.size_x) { + GeometryPlateDiverges { axis: PlateAxisX, modeled: modeled.size_x, realized: realized.size_x } + } else if micrometer_count(m: modeled.size_y) != micrometer_count(m: realized.size_y) { + GeometryPlateDiverges { axis: PlateAxisY, modeled: modeled.size_y, realized: realized.size_y } + } else if micrometer_count(m: modeled.size_z) != micrometer_count(m: realized.size_z) { + GeometryPlateDiverges { axis: PlateAxisZ, modeled: modeled.size_z, realized: realized.size_z } + } else { + GeometryConforms + } +} + +// THE BOUNDARY CHECK, AND IT READS THE SPECIMEN ITSELF -- twice corrected, in the same direction +// both times, which is why the direction is written down rather than the fix. +// +// The first revision compared contract.ladder.derived_rungs, the declaration's own sidecar. Review +// found that the specimen's holes were computed by a SECOND derivation, so the check could pass +// while the geometry handed to CadQuery carried different diameters: it compared the LAW instead of +// the ARTIFACT, and was structurally unable to see the fault it existed to catch. +// +// The second revision compared specimen_hole_diameters -- real diameters from the real operation +// graph, and still a PROJECTION of the artifact rather than the artifact. Plate dimensions and hole +// CENTRES sat outside the wall entirely, so a handler cutting correct diameters at wrong positions, +// or on a plate of the wrong thickness, conformed. The same fault one level out. +// +// It now compares plate on three axes, then operation count, then every operation field by field. +// The generalisation to write down is that a wall must compare the subject a consumer will actually +// receive, and every projection of that subject is a place the two can disagree while the check +// stays green. +// +// AND THIS IS WHOLE-GEOMETRY CONFORMANCE, NOT WHOLE-SPECIMEN CONFORMANCE. An earlier revision of +// this annotation said "the whole specimen", which is the same over-read one level up from the two +// it just corrected. What is compared is the normalized GEOMETRY PAYLOAD. What is NOT compared: +// +// specimen identity carried, single-armed, not compared +// revision not modeled as a compared subject at all +// feature identity POSITIONAL -- operation i is "the i-th rung" by list position, not by an +// identity the operation carries +// +// The distinction matters downstream rather than here: PRINT-5 will read a conforming verdict and +// must not take it as proof that identity and canonical ordering were adjudicated. A permutation is +// REFUSED (see w_an_unauthorised_operation_order_refuses) because position is compared -- which is +// not the same as features HAVING identities, and the difference reappears the moment two features +// share a geometry. +// THE ORDER IS PLATE, THEN DATUM, THEN THE LADDER, and each step is a diagnostic decision about +// which fault explains the others. A wrong plate makes every hole depth wrong at once. A wrong datum +// means the coupon cannot be oriented, so every rung ordinal below it is unreliable even where the +// geometry happens to match -- reporting rung 7 as divergent while the datum is wrong would name the +// symptom of an unreadable coupon. Only once plate and datum agree does a rung divergence mean what +// it says. +fn judge_realized_geometry( + contract: RealizationContract, + realized: HoleDiameterCouponGeometry, +) -> GeometryConformance { + let modeled = contract.specimen.geometry + let plate_outcome = compare_plate(modeled: modeled.plate, realized: realized.plate) + match plate_outcome { + GeometryConforms => { + let datum_outcome = datum_divergence( + m: modeled.orientation_datum, + r: realized.orientation_datum, + ) + match datum_outcome { + GeometryConforms => + compare_operations(modeled: modeled.ladder_holes, realized: realized.ladder_holes) + GeometryDatumDiverges { field: _, modeled: _, realized: _ } => datum_outcome + GeometryPlateDiverges { axis: _, modeled: _, realized: _ } => datum_outcome + GeometryOperationCountDiverges { modeled: _, realized: _ } => datum_outcome + GeometryOperationDiverges { index: _, field: _, modeled: _, realized: _ } => datum_outcome + } + } + GeometryDatumDiverges { field: _, modeled: _, realized: _ } => plate_outcome + GeometryPlateDiverges { axis: _, modeled: _, realized: _ } => plate_outcome + GeometryOperationCountDiverges { modeled: _, realized: _ } => plate_outcome + GeometryOperationDiverges { index: _, field: _, modeled: _, realized: _ } => plate_outcome + } +} + +// THE ONE ROUTE FROM WIRE TO VERDICT. A caller cannot reach conformance with an unadmitted envelope, +// because admission is what produces the modeled values conformance consumes -- the refusal arms have +// no plate and no features to hand on. That is the construction DESIGN section 5 asks for in place of +// a validation step a caller could forget to run. +type RealizationVerdict + = RealizationRefusedAtWire { refusal: EnvelopeRefusal } + | RealizationJudged { conformance: GeometryConformance } + +fn judge_realization( + contract: RealizationContract, + envelope: RawRealizationEnvelope, +) -> RealizationVerdict { + let admission = decode_envelope(envelope: envelope) + match admission { + EnvelopeDecodedV0 { decoded: a } => + RealizationJudged { + conformance: judge_realized_geometry(contract: contract, realized: a.geometry), + } + EnvelopeRefused { refusal: r } => RealizationRefusedAtWire { refusal: r } + } +} + +// THE ACTUATOR PAIRING IS UNBOUND, AND THAT IS AN OBLIGATION ON PRINT-5 RATHER THAN A DEFECT HERE. +// +// judge_realization returns a VERDICT and no geometry. So a handler that wants to cut something must +// obtain geometry from somewhere else -- today only decode_envelope -- and then associate that value +// with this verdict itself. That association is unbound: judge envelope A, retain the decoded +// geometry of envelope B, hand B to the handler under A's conforming verdict. Every honest caller +// passes the same envelope twice, and the invalid pairing stays writable regardless. It is the same +// class as the refusal payload that could carry a success, one level out: a state no route produces +// and nothing prevents (routed review, 2026-09-02). +// +// The close is a second sealed type returned FROM the judgment that established conformance, so +// there is no pair left to mis-associate -- and minted from the CONTRACT'S OWN canonical specimen +// rather than from the transported values that happened to compare equal, so what the handler cuts +// is the model's geometry and the wire is reduced to an assertion that was checked. The name +// AdmittedRealizationV0 is reserved for it above and deliberately unspent. +// +// WHY IT IS NOT BUILT IN THIS REVISION. Nothing actuates geometry yet: there is no handler, so the +// pairing has no site at which to go wrong, and the invariant "the decoded carrier never actuates" +// holds vacuously today. Minting a sealed carrier with zero consumers to hold a symbol is the +// speculative move DESIGN section 2 prices as redundant, and the same review that named this +// obligation also warned against establishing a public capability merely because the state +// conceptually exists. So the obligation is DECLARED rather than discharged, in a typed carrier +// rather than an annotation, because PRINT-5 must not be able to reach a handler without answering +// it -- and an annotation is a thing no Accepted program can read. +type RealizationV0Obligation = ActuatorGeometryPairingUnbound {} + +type RealizationV0Route = MintSealedGeometryFromCanonicalSpecimenAtJudgment {} + +// Total by construction: a second obligation reds this match until it is routed. The route is not a +// promise that the work is done, only that the open need names its close. +fn realization_v0_route(o: RealizationV0Obligation) -> RealizationV0Route { + match o { + ActuatorGeometryPairingUnbound {} => MintSealedGeometryFromCanonicalSpecimenAtJudgment {} + } +} + +data realization_v0_open_obligations: List = [ActuatorGeometryPairingUnbound {}] diff --git a/dag/test/claim/asrock_standoff_placement_witness_test.dag b/dag/test/claim/asrock_standoff_placement_witness_test.dag new file mode 100644 index 00000000000..d03747d11fb --- /dev/null +++ b/dag/test/claim/asrock_standoff_placement_witness_test.dag @@ -0,0 +1,202 @@ +module test.claim.asrock_standoff_placement_witness +import std.types { Bool, Int, List } +import extdeps.standards.micro_atx { MountingLocationId, LocJ, LocS, LocF, LocB } +import extdeps.boards.asrock_rack { + BoardLocationStanding, + HoleCorrespondenceInferred, HoleAbsenceExplicitlyDirected, HoleNotObservedInDrawing, + HolePhysicallyConfirmedPresent, HolePhysicallyConfirmedAbsent, + StandoffPlacementDecision, StandoffAdmitted, StandoffProhibited, + StandoffProhibitionCause, ProductSaysRemove, NoAdmittedBoardHole, + standoff_placement, + BoardStandardLocationCorrespondence, + asrock_altrad8ud_standard_location_correspondence, + Altrad8udMountingUnknown, + HoleCorrespondencePhysicallyUnconfirmed, ProductHoleDiameterUnmeasured, + UndersideKeepOutUnmeasured, MountingHoleGroundBondUnknown, StandoffHeightAndPadUnmeasured, + MountingUnknownDischarge, DischargedByMountingTheBoard, DischargedByCalipers, + DischargedByContinuityMeter, + mounting_unknown_discharge, + asrock_altrad8ud_open_mounting_unknowns, + asrock_altrad8ud_board_depth_nominal_exact, + asrock_altrad8ud_front_mounting_row_offset, + asrock_altrad8ud_front_overhang, + BoardPlaneOrientation, XAlongRearIoYDepth, XDepthYAlongRearIo, + board_extent_along_rear_io, board_extent_depth, + asrock_altrad8ud_orientation, + asrock_altrad8ud_extent_along_rear_io, + asrock_altrad8ud_extent_depth, +} +import std.measure { Micrometer, micrometer_count } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// WITNESS 1 — THE POSITIVE CONTROL. An inferred hole admits a standoff. Without this, every witness +// below is satisfied by a derivation that prohibits everything, which is the failure mode of a +// safety-shaped model: refusing universally looks conservative and is useless. +test fn w_an_inferred_hole_admits_a_standoff() -> Bool { + match standoff_placement(standing: HoleCorrespondenceInferred) { + StandoffAdmitted => true + StandoffProhibited { cause: _ } => false + } +} + +// WITNESS 2 — THE DISCRIMINATING RED, and the whole reason the standing type exists. J and S both +// end at "leave it empty", so a model that reports only the decision is green either way. This goes +// red the moment the two evidence routes are collapsed back into one constructor: it asserts that +// the same actuation arrives carrying DIFFERENT causes. +test fn w_j_and_s_are_both_prohibited_for_different_causes() -> Bool { + let j = standoff_placement(standing: HoleAbsenceExplicitlyDirected) + let s = standoff_placement(standing: HoleNotObservedInDrawing) + match j { + StandoffProhibited { cause: jc } => { + match s { + StandoffProhibited { cause: sc } => { + match jc { + ProductSaysRemove => { + match sc { + NoAdmittedBoardHole => true + ProductSaysRemove => false + } + } + NoAdmittedBoardHole => false + } + } + StandoffAdmitted => false + } + } + StandoffAdmitted => false + } +} + +// WITNESS 3 — A PHYSICAL CONFIRMATION AT FIT OVERTURNS THE WEAKER ROUTE WITHOUT SPECIAL-CASING. +// The unobserved-in-drawing claim about S is the one a real board can refute. This asserts the +// derivation already has somewhere for that measurement to land: confirming a hole admits a +// standoff by the same total function, no new branch, no edit to the J row. +test fn w_physical_confirmation_reaches_the_same_derivation() -> Bool { + let present = match standoff_placement(standing: HolePhysicallyConfirmedPresent) { + StandoffAdmitted => true + StandoffProhibited { cause: _ } => false + } + let absent = match standoff_placement(standing: HolePhysicallyConfirmedAbsent) { + StandoffAdmitted => false + StandoffProhibited { cause: c } => { + match c { + NoAdmittedBoardHole => true + ProductSaysRemove => false + } + } + } + present && absent +} + +// WITNESS 4 — THE ROSTER IS THE FULL MICRO-ATX POPULATION. Nine standard locations, every one +// decided. A chassis is built from the standard's grid, so a location this board simply forgot to +// mention is a location a chassis silently populates with a metal post. +test fn w_the_roster_decides_every_standard_location() -> Bool { + asrock_altrad8ud_standard_location_correspondence.length() == 9 +} + +// WITNESS 5 — EXACTLY TWO LOCATIONS ARE PROHIBITED, counted through the derivation rather than by +// reading the standings back. This is the count a chassis emitter consumes: seven posts, two voids. +test fn w_exactly_seven_of_nine_admit_a_post() -> Bool { + fold(asrock_altrad8ud_standard_location_correspondence, init: 0, f: fn(acc, row) { + match standoff_placement(standing: row.standing) { + StandoffAdmitted => acc + 1 + StandoffProhibited { cause: _ } => acc + } + }) == 7 +} + +// WITNESS 6 — THE OPEN UNKNOWNS ARE COUNTABLE, which is the whole reason they stopped being a +// paragraph. Five product-specific facts the standard cannot answer. This number is expected to go +// DOWN at FIT, and a change to it is a real event rather than someone rewording prose. +test fn w_five_mounting_unknowns_remain_open() -> Bool { + asrock_altrad8ud_open_mounting_unknowns.length() == 5 +} + +// WITNESS 7 — THE GROUND-BOND UNKNOWN NEEDS AN INSTRUMENT NOBODY ELSE NEEDS, and separating it is +// the point. Four of the five are answered by looking at or measuring the board; whether a mounting +// hole is bonded to board ground is answered only by a continuity meter. A derivation that routed +// everything to one instrument would let "I measured the board" discharge an electrical claim. +test fn w_the_bond_unknown_routes_to_its_own_instrument() -> Bool { + let bond = match mounting_unknown_discharge(u: MountingHoleGroundBondUnknown) { + DischargedByContinuityMeter => true + DischargedByCalipers => false + DischargedByMountingTheBoard => false + } + let fit = match mounting_unknown_discharge(u: HoleCorrespondencePhysicallyUnconfirmed) { + DischargedByMountingTheBoard => true + DischargedByCalipers => false + DischargedByContinuityMeter => false + } + let caliper = match mounting_unknown_discharge(u: ProductHoleDiameterUnmeasured) { + DischargedByCalipers => true + DischargedByMountingTheBoard => false + DischargedByContinuityMeter => false + } + bond && fit && caliper +} + +// WITNESS 8 — THE OVERHANG DERIVES, AND THIS IS THE RED FOR A PRECISION CONTRADICTION. +// +// The module previously carried a 267000 µm board depth beside a 29210 µm overhang computed from +// 266700 — the rounded millimetre spelling and the exact inch conversion both treated as exact, 300 +// µm apart, in one module. Nothing could see it, because no row subtracted one from the other. +// +// This does. It goes red if the depth is ever restated as the rounded 267000, if the front-row +// offset drifts, or if the overhang is hand-edited away from the difference. That is the whole point +// of asserting a DERIVATION rather than asserting the literal 29210: an equality against the +// constant would agree with itself no matter which of the two spellings the other rows adopted. +test fn w_the_overhang_derives_from_the_outline() -> Bool { + let depth = micrometer_count(m: asrock_altrad8ud_board_depth_nominal_exact) + let front_row = micrometer_count(m: asrock_altrad8ud_front_mounting_row_offset) + let overhang = micrometer_count(m: asrock_altrad8ud_front_overhang) + depth - front_row == overhang +} + +// WITNESS 9 — THE ROUNDED SPELLING IS NOT THE ONE THAT WOULD SATISFY IT. The positive control for +// witness 8: 267000 minus the same offset is 29510, not 29210, so the two spellings are genuinely +// discriminated rather than being within some tolerance that makes the check vacuous. +test fn w_the_rounded_depth_would_not_satisfy_the_derivation() -> Bool { + let front_row = micrometer_count(m: asrock_altrad8ud_front_mounting_row_offset) + let overhang = micrometer_count(m: asrock_altrad8ud_front_overhang) + 267000 - front_row != overhang +} + +// WITNESS 10 — THE AXIS SWAP MUTATION, and it is the only check in this program that could have +// caught the transposition that started all of this. +// +// Feeding the SAME two extents through the opposite orientation must exchange which physical edge +// each one answers for. If the readouts ignored the orientation — returning x for width and y for +// depth regardless — this goes red, and that failure mode is exactly what a prose annotation saying +// "x is along the rear I/O edge" left undetectable for as long as it stood. +test fn w_swapping_the_orientation_exchanges_the_physical_extents() -> Bool { + let a = micrometer_count(m: board_extent_along_rear_io( + orientation: XDepthYAlongRearIo, + x: micrometer(count: 243840), + y: micrometer(count: 266700) + )) + let d = micrometer_count(m: board_extent_depth( + orientation: XDepthYAlongRearIo, + x: micrometer(count: 243840), + y: micrometer(count: 266700) + )) + a == 266700 && d == 243840 +} + +// WITNESS 11 — AND THE DECLARED ORIENTATION IS THE ONE THE BOARD ACTUALLY USES. Witness 10 proves +// the readouts consume the orientation; this pins which orientation this board is authored in. The +// pair is what makes the model load-bearing: without this, a correct mechanism could still be +// declared backwards, which is the original defect wearing a type. +test fn w_the_board_reads_244_along_the_rear_io_edge_and_266_deep() -> Bool { + micrometer_count(m: asrock_altrad8ud_extent_along_rear_io) == 243840 + && micrometer_count(m: asrock_altrad8ud_extent_depth) == 266700 +} + +// WITNESS 12 — THE DEPTH READOUT AND THE OVERHANG DERIVATION AGREE. Two independent routes to this +// board's depth: the orientation-aware readout, and the row the overhang subtracts from. They must +// be the same number, or one of them is describing a different board. +test fn w_the_depth_readout_matches_the_overhang_derivation() -> Bool { + micrometer_count(m: asrock_altrad8ud_extent_depth) + == micrometer_count(m: asrock_altrad8ud_board_depth_nominal_exact) +} diff --git a/dag/test/claim/printed_chassis_admitted_realization_seal_witness_test.dag b/dag/test/claim/printed_chassis_admitted_realization_seal_witness_test.dag new file mode 100644 index 00000000000..9d42f3fc345 --- /dev/null +++ b/dag/test/claim/printed_chassis_admitted_realization_seal_witness_test.dag @@ -0,0 +1,69 @@ +module test.claim.printed_chassis_admitted_realization_seal_witness_test + +import gunbc.compile_diagnostic_census { + CompileDiagnosticCensus, + CompileDiagnosticCensusRow, + CensusObserved, + CensusNotRunnable, + census_blocking_rows, + census_rows_of_class, + census_total_count +} +import std.types { String, Bool, Int, List } +import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree } + +data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree + +// The seal on product.printed_chassis.realization_contract.DecodedRealizationV0 is what makes +// judge_realization the ONLY route from wire bytes to a judged realization: a foreign module that +// could write the record literal could hand a downstream consumer an admitted value that never +// passed decode. A probe run before the seal landed proved the arm WAS forgeable, and that probe +// measured nothing until a must-fail control distinguished "forgery permitted" from "the file was +// never compiled" -- so the evidence here is a DIFFERENTIAL between two sources that differ on one +// axis, plus a class-and-subject scoped count, which are the two exact forms +// gunbc.compile_diagnostic_census names. Asserting a total-count zero would be wrong: the imported +// closure carries its own diagnostics into both censuses, and it is precisely their cancellation +// under the differential that leaves the forged literal as the only difference. + +data forged_source: String = "module probe_chassis_forged_admitted\nimport product.printed_chassis.realization_contract { DecodedRealizationV0 }\nimport product.printed_chassis.coupon { PlateDimensions, plate_dimensions, CouponOperation }\nimport std.measure { micrometer }\nimport std.types { List }\nfn forged() -> DecodedRealizationV0 {\n DecodedRealizationV0 {\n plate: plate_dimensions(size_x: micrometer(count: 1), size_y: micrometer(count: 1), size_z: micrometer(count: 1)),\n features: [],\n }\n}\n" + +data lawful_source: String = "module probe_chassis_lawful_admitted\nimport product.printed_chassis.realization_contract { DecodedRealizationV0 }\nimport product.printed_chassis.coupon { PlateDimensions, plate_dimensions, CouponOperation }\nimport std.measure { micrometer }\nimport std.types { List }\nfn lawful(value: DecodedRealizationV0) -> DecodedRealizationV0 {\n value\n}\n" + +fn rows_of_subject(rows: List, wanted: String) -> List { + rows |> filter(r => r.subject_name == wanted) +} + +// -1 on the NotRunnable arm, so a harness that never ran can satisfy no witness below: every +// assertion here compares against a non-negative quantity. +fn seal_violation_count(source: String) -> Int { + match compile_dag_diagnostic_census(source) { + CensusObserved { rows: rows } => census_total_count( + rows: rows_of_subject( + rows: census_rows_of_class( + rows: census_blocking_rows(rows: rows), + wanted: "SoleConstructorViolation" + ), + wanted: "DecodedRealizationV0" + ) + ) + CensusNotRunnable { cause: _ } => 0 - 1 + } +} + +test fn w_foreign_record_literal_of_admitted_realization_refuses() -> Bool { + seal_violation_count(source: forged_source) >= 1 +} + +// The positive control. Same imports, same closure, no record literal: it proves the type is +// resolvable and legally nameable from a foreign module, so the red above is the literal being +// refused and not the import failing to resolve. +test fn w_lawful_foreign_use_of_admitted_realization_is_unsealed() -> Bool { + seal_violation_count(source: lawful_source) == 0 +} + +// The differential. Written as its own witness rather than left implicit in the pair, because the +// two counts above could both be satisfied by a census whose rows were dominated by the shared +// closure; the subtraction is what states that the forged literal is the whole difference. +test fn w_the_seal_is_the_only_difference_between_the_two_sources() -> Bool { + seal_violation_count(source: forged_source) - seal_violation_count(source: lawful_source) >= 1 +} diff --git a/dag/test/claim/printed_chassis_contract_witness_test.dag b/dag/test/claim/printed_chassis_contract_witness_test.dag new file mode 100644 index 00000000000..88fd056349e --- /dev/null +++ b/dag/test/claim/printed_chassis_contract_witness_test.dag @@ -0,0 +1,753 @@ +module test.claim.printed_chassis_contract_witness +import std.types { Bool, Int, List, NonEmptyStr } +import std.measure { Micrometer, micrometer, micrometer_count } +import product.printed_chassis.coupon { + LengthLadder, LadderConstruction, LadderReady, LadderStepIsZero, LadderTooFewRungs, + hole_ladder_spec, hole_ladder_specimen, ladder_rungs, ladder_base, specimen_ladder_hole_diameters, + CouponSpecimen, CouponOperation, OpThroughHole, PlateDimensions, + HoleDiameterCouponGeometry, hole_ladder_orientation_datum, hole_ladder_datum_center_y, +} +import product.printed_chassis.realization_contract { + RealizationContract, + realization_contract, + GeometryConformance, GeometryConforms, + GeometryPlateDiverges, GeometryDatumDiverges, + GeometryOperationCountDiverges, GeometryOperationDiverges, + PlateAxis, PlateAxisX, PlateAxisY, PlateAxisZ, + OperationField, FieldDiameter, FieldCenterX, FieldCenterY, + compare_operations, compare_plate, judge_realized_geometry, + RawRealizationEnvelope, raw_realization_envelope, + RawOperationRow, raw_operation_row, + EnvelopeSchemaUnsupported, EnvelopeOperationUnknown, EnvelopeCarriesNoOperations, + decode_envelope, contract_schema_version, + RealizationVerdict, RealizationRefusedAtWire, RealizationJudged, + judge_realization, +} +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// A FAITHFUL HANDLER IS SIMULATED BY PROJECTING THE CANONICAL SPECIMEN ONTO THE WIRE, and the +// weakness of that is stated rather than hidden: an envelope derived from the specimen agrees with +// the specimen by construction, so the positive control below proves the DECODE is lossless and +// nothing more. It is not evidence that the wall discriminates. +// +// The discrimination lives entirely in the MUTATION witnesses. Each perturbs exactly one field of an +// otherwise faithful envelope and requires the wall to name that field. A mutation is an independent +// oracle in a way an authored fixture is not, because it does not depend on the author having +// written the expected geometry correctly -- only on the wall noticing a difference the author made +// deliberately. +fn row_of(op: CouponOperation) -> RawOperationRow { + match op { + OpThroughHole { diameter: d, center_x: x, center_y: y } => + raw_operation_row( + kind: "through_hole", + diameter_um: micrometer_count(m: d), + center_x_um: micrometer_count(m: x), + center_y_um: micrometer_count(m: y), + ) + } +} + +fn rows_of(s: CouponSpecimen) -> List { + fold(s.geometry.ladder_holes, init: [], f: fn(acc, op) { concat(acc, [row_of(op: op)]) }) +} + +fn datum_row_of(s: CouponSpecimen) -> RawOperationRow { + row_of(op: s.geometry.orientation_datum) +} + +// EVERY MUTATION HELPER TAKES BOTH POPULATIONS, so a witness that means to perturb the datum cannot +// silently perturb the ladder and vice versa. An earlier shape here had one `operations` argument +// and the split would have let a datum witness pass rows into it by position. +fn envelope_from( + s: CouponSpecimen, + plate_z_um: Int, + datum: RawOperationRow, + ladder: List, +) -> RawRealizationEnvelope { + raw_realization_envelope( + schema_version: contract_schema_version, + plate_x_um: micrometer_count(m: s.geometry.plate.size_x), + plate_y_um: micrometer_count(m: s.geometry.plate.size_y), + plate_z_um: plate_z_um, + orientation_datum: datum, + ladder_holes: ladder, + ) +} + +fn envelope_of(s: CouponSpecimen) -> RawRealizationEnvelope { + envelope_from( + s: s, + plate_z_um: micrometer_count(m: s.geometry.plate.size_z), + datum: datum_row_of(s: s), + ladder: rows_of(s: s), + ) +} + +// The mutation helpers rebuild the envelope with ONE value replaced, so every witness below differs +// from the faithful envelope in exactly one place and the wall's answer names that place or fails. +fn envelope_with_plate_z(s: CouponSpecimen, z: Int) -> RawRealizationEnvelope { + envelope_from(s: s, plate_z_um: z, datum: datum_row_of(s: s), ladder: rows_of(s: s)) +} + +fn envelope_with_rows(s: CouponSpecimen, rows: List) -> RawRealizationEnvelope { + envelope_from( + s: s, + plate_z_um: micrometer_count(m: s.geometry.plate.size_z), + datum: datum_row_of(s: s), + ladder: rows, + ) +} + +fn envelope_with_datum(s: CouponSpecimen, datum: RawOperationRow) -> RawRealizationEnvelope { + envelope_from( + s: s, + plate_z_um: micrometer_count(m: s.geometry.plate.size_z), + datum: datum, + ladder: rows_of(s: s), + ) +} + +fn datum_moved_to(s: CouponSpecimen, x: Int, y: Int) -> RawOperationRow { + raw_operation_row( + kind: "through_hole", + diameter_um: datum_diameter_um(s: s), + center_x_um: x, + center_y_um: y, + ) +} + +fn datum_diameter_um(s: CouponSpecimen) -> Int { + match s.geometry.orientation_datum { + OpThroughHole { diameter: d, center_x: _, center_y: _ } => micrometer_count(m: d) + } +} + +fn datum_center_x_um(s: CouponSpecimen) -> Int { + match s.geometry.orientation_datum { + OpThroughHole { diameter: _, center_x: x, center_y: _ } => micrometer_count(m: x) + } +} + +// The far-end x is computed from the plate rather than read off the list, because `.last()` returns +// an option and the Absent arm would have to answer with something -- and there is no honest +// something. The ladder spans margin to plate_width - margin by construction, so the last rung's +// centre is the plate width less one margin. w_the_datum_is_at_rung_zero below is what keeps this +// from being a second unchecked derivation: it asserts the two ends against the built geometry. +fn last_rung_center_x_um(s: CouponSpecimen) -> Int { + micrometer_count(m: s.geometry.plate.size_x) - datum_center_x_um(s: s) +} + +fn bump_first_center_x(rows: List, delta: Int) -> List { + fold(rows, init: [], f: fn(acc, row) { + if acc.length() == 0 { + concat(acc, [raw_operation_row( + kind: row.kind, + diameter_um: row.diameter_um, + center_x_um: row.center_x_um + delta, + center_y_um: row.center_y_um, + )]) + } else { + concat(acc, [row]) + } + }) +} + +fn bump_first_diameter(rows: List, delta: Int) -> List { + fold(rows, init: [], f: fn(acc, row) { + if acc.length() == 0 { + concat(acc, [raw_operation_row( + kind: row.kind, + diameter_um: row.diameter_um + delta, + center_x_um: row.center_x_um, + center_y_um: row.center_y_um, + )]) + } else { + concat(acc, [row]) + } + }) +} + +// WITNESS 1 — THE DECODE IS LOSSLESS. A faithful envelope round-trips to a conforming verdict. This +// is the positive control: without it every refusal witness below is satisfied by a wall that +// refuses everything, which is the failure mode a negative-only suite cannot see. +test fn w_a_faithful_envelope_is_judged_conforming() -> Bool { + match hole_ladder_spec { + LadderReady { ladder: l } => { + let contract = realization_contract(declaration: l) + match judge_realization(contract: contract, envelope: envelope_of(s: contract.specimen)) { + RealizationJudged { conformance: c } => match c { + GeometryConforms => true + GeometryPlateDiverges { axis: _, modeled: _, realized: _ } => false + GeometryDatumDiverges { field: _, modeled: _, realized: _ } => false + GeometryOperationCountDiverges { modeled: _, realized: _ } => false + GeometryOperationDiverges { index: _, field: _, modeled: _, realized: _ } => false + } + RealizationRefusedAtWire { refusal: _ } => false + } + } + LadderStepIsZero => false + LadderTooFewRungs { supplied: _ } => false + } +} + +// WITNESS 2 — A WRONG PLATE THICKNESS IS CAUGHT, AND THIS FAULT WAS ADMITTED BEFORE THIS REVISION. +// +// The wall compared hole diameters only, so a handler that cut every hole correctly into a plate of +// the wrong thickness CONFORMED. For a hole-diameter coupon that is not cosmetic: plate thickness is +// the hole DEPTH, and hole depth is the aspect ratio the whole measurement is about. +test fn w_a_wrong_plate_thickness_is_caught_on_its_axis() -> Bool { + match hole_ladder_spec { + LadderReady { ladder: l } => { + let contract = realization_contract(declaration: l) + let bad = envelope_with_plate_z(s: contract.specimen, z: micrometer_count(m: contract.specimen.geometry.plate.size_z) + 500) + match judge_realization(contract: contract, envelope: bad) { + RealizationJudged { conformance: c } => match c { + GeometryPlateDiverges { axis: a, modeled: m, realized: r } => + match a { + PlateAxisZ => micrometer_count(m: r) - micrometer_count(m: m) == 500 + PlateAxisX => false + PlateAxisY => false + } + GeometryConforms => false + GeometryDatumDiverges { field: _, modeled: _, realized: _ } => false + GeometryOperationCountDiverges { modeled: _, realized: _ } => false + GeometryOperationDiverges { index: _, field: _, modeled: _, realized: _ } => false + } + RealizationRefusedAtWire { refusal: _ } => false + } + } + LadderStepIsZero => false + LadderTooFewRungs { supplied: _ } => false + } +} + +// WITNESS 3 — A HOLE AT THE WRONG POSITION IS CAUGHT, AND THIS FAULT WAS ALSO ADMITTED BEFORE. +// +// Correct diameters at wrong centres is the single most plausible handler bug -- an off-by-one in a +// pitch loop -- and it produced a conforming verdict under the diameter-only comparison. Overlapping +// or edge-breaking holes would have printed with the wall green. +test fn w_a_hole_at_the_wrong_position_is_caught_and_located() -> Bool { + match hole_ladder_spec { + LadderReady { ladder: l } => { + let contract = realization_contract(declaration: l) + let rows = bump_first_center_x(rows: rows_of(s: contract.specimen), delta: 250) + let bad = envelope_with_rows(s: contract.specimen, rows: rows) + match judge_realization(contract: contract, envelope: bad) { + RealizationJudged { conformance: c } => match c { + GeometryOperationDiverges { index: i, field: f, modeled: m, realized: r } => + match f { + FieldCenterX => i == 0 && micrometer_count(m: r) - micrometer_count(m: m) == 250 + FieldDiameter => false + FieldCenterY => false + } + GeometryConforms => false + GeometryPlateDiverges { axis: _, modeled: _, realized: _ } => false + GeometryDatumDiverges { field: _, modeled: _, realized: _ } => false + GeometryOperationCountDiverges { modeled: _, realized: _ } => false + } + RealizationRefusedAtWire { refusal: _ } => false + } + } + LadderStepIsZero => false + LadderTooFewRungs { supplied: _ } => false + } +} + +// WITNESS 4 — A WRONG DIAMETER IS STILL CAUGHT, AND IS REPORTED AS A DIAMETER RATHER THAN A +// POSITION. The field ordering is a diagnostic decision: diameter is a process fault and centre is a +// layout fault, and an operator acts on the first differently from the second. +test fn w_a_wrong_diameter_is_reported_as_a_diameter() -> Bool { + match hole_ladder_spec { + LadderReady { ladder: l } => { + let contract = realization_contract(declaration: l) + let rows = bump_first_diameter(rows: rows_of(s: contract.specimen), delta: 50) + let bad = envelope_with_rows(s: contract.specimen, rows: rows) + match judge_realization(contract: contract, envelope: bad) { + RealizationJudged { conformance: c } => match c { + GeometryOperationDiverges { index: i, field: f, modeled: m, realized: r } => + match f { + FieldDiameter => i == 0 && micrometer_count(m: r) - micrometer_count(m: m) == 50 + FieldCenterX => false + FieldCenterY => false + } + GeometryConforms => false + GeometryPlateDiverges { axis: _, modeled: _, realized: _ } => false + GeometryDatumDiverges { field: _, modeled: _, realized: _ } => false + GeometryOperationCountDiverges { modeled: _, realized: _ } => false + } + RealizationRefusedAtWire { refusal: _ } => false + } + } + LadderStepIsZero => false + LadderTooFewRungs { supplied: _ } => false + } +} + +// WITNESS 5 — A DROPPED OPERATION IS CAUGHT ON THE COUNT, and the refusal carries both populations. +// Realizing ten holes where the model declared eleven produces a coupon that measures perfectly well +// and calibrates against a ladder that never existed. +test fn w_a_dropped_operation_diverges_on_count() -> Bool { + match hole_ladder_spec { + LadderReady { ladder: l } => { + let contract = realization_contract(declaration: l) + let rows = rows_of(s: contract.specimen).skip(n: 1) + let bad = envelope_with_rows(s: contract.specimen, rows: rows) + match judge_realization(contract: contract, envelope: bad) { + RealizationJudged { conformance: c } => match c { + GeometryOperationCountDiverges { modeled: m, realized: r } => m == 11 && r == 10 + GeometryConforms => false + GeometryDatumDiverges { field: _, modeled: _, realized: _ } => false + GeometryPlateDiverges { axis: _, modeled: _, realized: _ } => false + GeometryOperationDiverges { index: _, field: _, modeled: _, realized: _ } => false + } + RealizationRefusedAtWire { refusal: _ } => false + } + } + LadderStepIsZero => false + LadderTooFewRungs { supplied: _ } => false + } +} + +// WITNESS 6 — THE PLATE IS JUDGED BEFORE THE OPERATIONS. A plate of the wrong thickness makes every +// hole depth wrong at once, so reporting the first hole as divergent would name a symptom and bury +// the cause. This witness perturbs BOTH and requires the plate answer. +test fn w_a_plate_fault_outranks_an_operation_fault() -> Bool { + match hole_ladder_spec { + LadderReady { ladder: l } => { + let contract = realization_contract(declaration: l) + let rows = bump_first_diameter(rows: rows_of(s: contract.specimen), delta: 50) + let bad = raw_realization_envelope( + schema_version: contract_schema_version, + plate_x_um: micrometer_count(m: contract.specimen.geometry.plate.size_x), + plate_y_um: micrometer_count(m: contract.specimen.geometry.plate.size_y), + plate_z_um: micrometer_count(m: contract.specimen.geometry.plate.size_z) + 500, + orientation_datum: datum_row_of(s: contract.specimen), + ladder_holes: rows, + ) + match judge_realization(contract: contract, envelope: bad) { + RealizationJudged { conformance: c } => match c { + GeometryPlateDiverges { axis: _, modeled: _, realized: _ } => true + GeometryConforms => false + GeometryDatumDiverges { field: _, modeled: _, realized: _ } => false + GeometryOperationCountDiverges { modeled: _, realized: _ } => false + GeometryOperationDiverges { index: _, field: _, modeled: _, realized: _ } => false + } + RealizationRefusedAtWire { refusal: _ } => false + } + } + LadderStepIsZero => false + LadderTooFewRungs { supplied: _ } => false + } +} + +// WITNESS 7 — AN UNSUPPORTED SCHEMA VERSION REFUSES AT THE WIRE AND NAMES BOTH SIDES. A handler +// debugging a rejected payload needs the offending spelling; "unsupported schema" alone sends them +// to read our source instead of their own output. +test fn w_an_unknown_schema_version_refuses_and_names_both() -> Bool { + match hole_ladder_spec { + LadderReady { ladder: l } => { + let contract = realization_contract(declaration: l) + let bad = raw_realization_envelope( + schema_version: "v999", + plate_x_um: 40000, + plate_y_um: 20000, + plate_z_um: 4000, + orientation_datum: raw_operation_row(kind: "through_hole", diameter_um: 3000, center_x_um: 6000, center_y_um: 4000), + ladder_holes: [raw_operation_row(kind: "through_hole", diameter_um: 3000, center_x_um: 5000, center_y_um: 10000)], + ) + match judge_realization(contract: contract, envelope: bad) { + RealizationRefusedAtWire { refusal: a } => + match a { + EnvelopeSchemaUnsupported { received: rv, supported: sv } => rv == "v999" && sv == contract_schema_version + EnvelopeOperationUnknown { received: _ } => false + EnvelopeCarriesNoOperations => false + } + RealizationJudged { conformance: _ } => false + } + } + LadderStepIsZero => false + LadderTooFewRungs { supplied: _ } => false + } +} + +// WITNESS 8 — AN UNKNOWN OPERATION KIND REFUSES AND NAMES IT. +test fn w_an_unknown_operation_kind_refuses_and_names_it() -> Bool { + match hole_ladder_spec { + LadderReady { ladder: l } => { + let contract = realization_contract(declaration: l) + let bad = raw_realization_envelope( + schema_version: contract_schema_version, + plate_x_um: 40000, + plate_y_um: 20000, + plate_z_um: 4000, + orientation_datum: raw_operation_row(kind: "through_hole", diameter_um: 3000, center_x_um: 6000, center_y_um: 4000), + ladder_holes: [raw_operation_row(kind: "chamfer", diameter_um: 3000, center_x_um: 5000, center_y_um: 10000)], + ) + match judge_realization(contract: contract, envelope: bad) { + RealizationRefusedAtWire { refusal: a } => + match a { + EnvelopeOperationUnknown { received: r } => r == "chamfer" + EnvelopeSchemaUnsupported { received: _, supported: _ } => false + EnvelopeCarriesNoOperations => false + } + RealizationJudged { conformance: _ } => false + } + } + LadderStepIsZero => false + LadderTooFewRungs { supplied: _ } => false + } +} + +// WITNESS 9 — AN EMPTY OPERATION LIST REFUSES. A coupon with no holes measures nothing, and an empty +// list is what a handler sends when its own derivation silently produced nothing -- the failure that +// looks most like success, because every comparison over an empty list agrees. +test fn w_an_envelope_carrying_no_operations_refuses() -> Bool { + match hole_ladder_spec { + LadderReady { ladder: l } => { + let contract = realization_contract(declaration: l) + let bad = raw_realization_envelope( + schema_version: contract_schema_version, + plate_x_um: 40000, + plate_y_um: 20000, + plate_z_um: 4000, + orientation_datum: raw_operation_row(kind: "through_hole", diameter_um: 3000, center_x_um: 6000, center_y_um: 4000), + ladder_holes: [], + ) + match judge_realization(contract: contract, envelope: bad) { + RealizationRefusedAtWire { refusal: a } => + match a { + EnvelopeCarriesNoOperations => true + EnvelopeSchemaUnsupported { received: _, supported: _ } => false + EnvelopeOperationUnknown { received: _ } => false + } + RealizationJudged { conformance: _ } => false + } + } + LadderStepIsZero => false + LadderTooFewRungs { supplied: _ } => false + } +} + +// WITNESS 10 — THE DELETED OPERATION REFUSES AT THE WIRE, AND THIS WITNESS WAS GREEN-AS-ADMITTED +// BEFORE THE CHANGE THAT ADDED IT. +// +// V0 deleted OpDatumMark from CouponOperation. The compile stayed clean through that deletion while +// admitted_operation_kinds still carried the string "datum_mark", because a string in a list has no +// referent the namespace can refuse -- so for one revision the transport would have ADMITTED an +// operation the model had no constructor for. This is the executed agreement between the wire +// spelling and the coproduct arms, and nothing in the type system provides it. It retires when the +// spelling is PROJECTED from the arms, and not before. +test fn w_the_deleted_operation_refuses_at_the_wire() -> Bool { + match hole_ladder_spec { + LadderReady { ladder: l } => { + let contract = realization_contract(declaration: l) + let bad = raw_realization_envelope( + schema_version: contract_schema_version, + plate_x_um: 40000, + plate_y_um: 20000, + plate_z_um: 4000, + orientation_datum: raw_operation_row(kind: "through_hole", diameter_um: 3000, center_x_um: 6000, center_y_um: 4000), + ladder_holes: [raw_operation_row(kind: "datum_mark", diameter_um: 0, center_x_um: 3000, center_y_um: 2000)], + ) + match judge_realization(contract: contract, envelope: bad) { + RealizationRefusedAtWire { refusal: a } => + match a { + EnvelopeOperationUnknown { received: r } => r == "datum_mark" + EnvelopeSchemaUnsupported { received: _, supported: _ } => false + EnvelopeCarriesNoOperations => false + } + RealizationJudged { conformance: _ } => false + } + } + LadderStepIsZero => false + LadderTooFewRungs { supplied: _ } => false + } +} + +// WITNESS 11 — THE SPECIMEN'S HOLES ARE THE LADDER RUNGS. The contract derives its own specimen from +// the declaration, so this is the check that the derivation the wall compares against is the same +// derivation the coupon authority publishes. +test fn w_the_specimens_actual_holes_are_the_ladder_rungs() -> Bool { + match hole_ladder_spec { + LadderReady { ladder: l } => { + let contract = realization_contract(declaration: l) + let holes = specimen_ladder_hole_diameters(s: contract.specimen) + let rungs = ladder_rungs(l: l) + holes.length() == rungs.length() && holes.length() == 11 + } + LadderStepIsZero => false + LadderTooFewRungs { supplied: _ } => false + } +} + +fn reversed_rows(rows: List) -> List { + fold(rows, init: [], f: fn(acc, row) { concat([row], acc) }) +} + +// WITNESS 12 — AN UNAUTHORISED OPERATION ORDER REFUSES, AND THE DIAGNOSTIC NAMES A FIELD RATHER THAN +// NAMING "ORDER". That is worth stating rather than leaving for a reader to discover. +// +// The ladder ascends, so reversing the operations puts the LARGEST diameter at index 0. The positional +// comparison therefore refuses immediately -- order is not a separate check and does not need to be, +// because comparing operation i against operation i already makes a permutation a divergence. The +// refusal reports FieldDiameter at index 0, which is TRUE and is the first place the artifact differs +// from the model; it simply is not the word "order". +// +// WHY NO SEPARATE ORDER CHECK IS OWED: one would be a second authority for a question the positional +// comparison already answers, and it could disagree with it. What IS owed is this witness, because +// without it the property is an inference from how zip_map happens to work rather than an executed +// fact -- and a reader could later "optimise" the comparison into a set or multiset comparison, which +// would still pass every other witness in this file while silently admitting every permutation. +test fn w_an_unauthorised_operation_order_refuses() -> Bool { + match hole_ladder_spec { + LadderReady { ladder: l } => { + let contract = realization_contract(declaration: l) + let rows = reversed_rows(rows: rows_of(s: contract.specimen)) + let bad = envelope_with_rows(s: contract.specimen, rows: rows) + match judge_realization(contract: contract, envelope: bad) { + RealizationJudged { conformance: c } => match c { + GeometryOperationDiverges { index: i, field: f, modeled: m, realized: r } => + match f { + FieldDiameter => i == 0 && micrometer_count(m: m) == 3000 && micrometer_count(m: r) == 4000 + FieldCenterX => false + FieldCenterY => false + } + GeometryConforms => false + GeometryPlateDiverges { axis: _, modeled: _, realized: _ } => false + GeometryDatumDiverges { field: _, modeled: _, realized: _ } => false + GeometryOperationCountDiverges { modeled: _, realized: _ } => false + } + RealizationRefusedAtWire { refusal: _ } => false + } + } + LadderStepIsZero => false + LadderTooFewRungs { supplied: _ } => false + } +} + + +// --------------------------------------------------------------------------- +// THE ORIENTATION DATUM. Four controls, and the reason there are four is that the datum's job is not +// "a hole exists somewhere off centre" -- it is that a 180-degree reading of the coupon is visibly +// inconsistent with the geometry. Each control breaks that property in a different way, and a datum +// implementation that satisfied only some of them would leave a real coupon ambiguous. +// --------------------------------------------------------------------------- + +// WITNESS 13 — THE CANONICAL COUPON'S DATUM IS ADMITTED. The positive control, and as weak as every +// positive control here: the envelope is projected from the specimen, so it agrees by construction. +// It earns its place by proving the datum survives the wire round trip at all -- without it, a datum +// the decoder silently dropped would make all three refusals below pass for the wrong reason. +test fn w_the_canonical_datum_conforms() -> Bool { + match hole_ladder_spec { + LadderReady { ladder: l } => { + let contract = realization_contract(declaration: l) + match judge_realization(contract: contract, envelope: envelope_of(s: contract.specimen)) { + RealizationJudged { conformance: c } => match c { + GeometryConforms => true + GeometryDatumDiverges { field: _, modeled: _, realized: _ } => false + GeometryPlateDiverges { axis: _, modeled: _, realized: _ } => false + GeometryOperationCountDiverges { modeled: _, realized: _ } => false + GeometryOperationDiverges { index: _, field: _, modeled: _, realized: _ } => false + } + RealizationRefusedAtWire { refusal: _ } => false + } + } + LadderStepIsZero => false + LadderTooFewRungs { supplied: _ } => false + } +} + +// WITNESS 14 — A DATUM AT THE OPPOSITE END REFUSES, WHICH IS THE 180-DEGREE READING ITSELF. This is +// the control the whole datum exists for: a handler that mirrored the coupon end to end would place +// the datum under the LAST rung instead of the first, and every measurement would then be attributed +// to the reversed ordinal. The refusal names FieldCenterX, and it must -- the diameter and the y are +// unchanged by a mirror, so x is the only field that can carry the fault. +test fn w_a_datum_at_the_far_end_is_refused_as_a_reversed_reading() -> Bool { + match hole_ladder_spec { + LadderReady { ladder: l } => { + let contract = realization_contract(declaration: l) + let s = contract.specimen + let mirrored = datum_moved_to( + s: s, + x: last_rung_center_x_um(s: s), + y: micrometer_count(m: hole_ladder_datum_center_y), + ) + match judge_realization(contract: contract, envelope: envelope_with_datum(s: s, datum: mirrored)) { + RealizationJudged { conformance: c } => match c { + GeometryDatumDiverges { field: f, modeled: m, realized: r } => + match f { + FieldCenterX => + micrometer_count(m: m) == datum_center_x_um(s: s) + && micrometer_count(m: r) == last_rung_center_x_um(s: s) + FieldDiameter => false + FieldCenterY => false + } + GeometryConforms => false + GeometryPlateDiverges { axis: _, modeled: _, realized: _ } => false + GeometryOperationCountDiverges { modeled: _, realized: _ } => false + GeometryOperationDiverges { index: _, field: _, modeled: _, realized: _ } => false + } + RealizationRefusedAtWire { refusal: _ } => false + } + } + LadderStepIsZero => false + LadderTooFewRungs { supplied: _ } => false + } +} + +// WITNESS 15 — A DATUM ON THE LADDER CENTRE-LINE REFUSES AS AMBIGUOUS. A datum at the correct x but +// at the rungs' own y is not an orientation mark at all: it sits in the ladder band, so by eye it +// reads as a twelfth hole in the row rather than as an asymmetry, and the coupon is once again +// symmetric to a measurer. The x is right, so this control passes only if the wall compares the y -- +// which is exactly the field an implementation that "put a hole near the 3 mm end" would get wrong. +test fn w_a_datum_on_the_ladder_centreline_is_refused_as_ambiguous() -> Bool { + match hole_ladder_spec { + LadderReady { ladder: l } => { + let contract = realization_contract(declaration: l) + let s = contract.specimen + let flat = datum_moved_to(s: s, x: datum_center_x_um(s: s), y: 9000) + match judge_realization(contract: contract, envelope: envelope_with_datum(s: s, datum: flat)) { + RealizationJudged { conformance: c } => match c { + GeometryDatumDiverges { field: f, modeled: m, realized: r } => + match f { + FieldCenterY => + micrometer_count(m: m) == micrometer_count(m: hole_ladder_datum_center_y) + && micrometer_count(m: r) == 9000 + FieldDiameter => false + FieldCenterX => false + } + GeometryConforms => false + GeometryPlateDiverges { axis: _, modeled: _, realized: _ } => false + GeometryOperationCountDiverges { modeled: _, realized: _ } => false + GeometryOperationDiverges { index: _, field: _, modeled: _, realized: _ } => false + } + RealizationRefusedAtWire { refusal: _ } => false + } + } + LadderStepIsZero => false + LadderTooFewRungs { supplied: _ } => false + } +} + +// WITNESS 16 — THE DATUM DOES NOT ENTER THE MEASUREMENT POPULATION. The datum is a through-hole of +// exactly the base diameter, so the single most likely implementation error is to let it into the +// ladder: the projection would then return twelve diameters beginning 3.00, 3.00, the eleven-rung +// count would read twelve, and every rung ordinal after the first would be off by one. None of that +// is visible to any other witness here, because a twelve-row envelope compared against a twelve-row +// specimen agrees perfectly. This is the check that the two populations stayed two. +test fn w_the_datum_stays_out_of_the_measured_ladder() -> Bool { + match hole_ladder_spec { + LadderReady { ladder: l } => { + let contract = realization_contract(declaration: l) + let s = contract.specimen + let diameters = specimen_ladder_hole_diameters(s: s) + let rungs = ladder_rungs(l: l) + diameters.length() == 11 + && diameters.length() == rungs.length() + && s.geometry.ladder_holes.length() == 11 + && datum_diameter_um(s: s) == micrometer_count(m: ladder_base(l: l)) + } + LadderStepIsZero => false + LadderTooFewRungs { supplied: _ } => false + } +} + +// WITNESS 17 — THE DATUM CLEARS BOTH THE LADDER AND THE PLATE EDGE. The clearances are stated in the +// coupon module's annotation, and an annotation is a thing no Accepted program can read -- so they +// are asserted here against the derived geometry rather than trusted. The widest rung is 4.00 mm at +// y = 9.00 mm, so the ladder band is [7000, 11000]; the datum must sit clear of it and clear of +// y = 0. A datum that overlapped either would print as a merged slot or break out of the edge, and +// in both cases the coupon is scrap rather than ambiguous. +test fn w_the_datum_clears_the_ladder_band_and_the_plate_edge() -> Bool { + match hole_ladder_spec { + LadderReady { ladder: l } => { + let s = hole_ladder_specimen(l: l) + let datum_top = micrometer_count(m: hole_ladder_datum_center_y) + datum_diameter_um(s: s) / 2 + let datum_bottom = micrometer_count(m: hole_ladder_datum_center_y) - datum_diameter_um(s: s) / 2 + datum_top < 7000 && datum_bottom > 0 + } + LadderStepIsZero => false + LadderTooFewRungs { supplied: _ } => false + } +} + + +// WITNESS 18 — THE DATUM IS AT RUNG ZERO'S X, AND THIS IS THE CHECK THE COUPON MODULE'S ANNOTATION +// PROMISES. The datum's centre_x reads `hole_ladder_margin`; rung zero's comes out of the ladder +// fold's `margin + i * pitch` at i = 0. One shared row, two readers -- and a shared row is only +// shared while both keep reading it, which is a property no type carries. If a later revision gives +// the ladder its own origin, or offsets the datum "slightly clear of the first hole", this goes red +// and the orientation guarantee stops silently meaning something weaker. +// +// It also pins the FAR end, because last_rung_center_x_um above computes that end from the plate +// width rather than reading the list, and an unchecked derivation used by a refusal control is +// exactly how a control comes to pass for the wrong reason. +test fn w_the_datum_is_at_rung_zero() -> Bool { + match hole_ladder_spec { + LadderReady { ladder: l } => { + let s = hole_ladder_specimen(l: l) + let rung_xs = fold(s.geometry.ladder_holes, init: [], f: fn(acc, op) { + match op { + OpThroughHole { diameter: _, center_x: x, center_y: _ } => + concat(acc, [micrometer_count(m: x)]) + } + }) + let first_x = fold(rung_xs, init: 0 - 1, f: fn(acc, x) { if acc == 0 - 1 { x } else { acc } }) + let far_x = fold(rung_xs, init: 0, f: fn(acc, x) { if x > acc { x } else { acc } }) + datum_center_x_um(s: s) == first_x + && last_rung_center_x_um(s: s) == far_x + && first_x != far_x + } + LadderStepIsZero => false + LadderTooFewRungs { supplied: _ } => false + } +} + + +// WITNESS 19 — A DATUM MIRRORED ACROSS THE CENTRE-LINE IS REFUSED, WHICH IS THE COUPON TURNED OVER. +// +// This is the gap the other two datum controls left, and it is the case a human actually creates: +// witness 14 catches the coupon rotated end for end, witness 15 catches a datum that never went off +// the centre-line at all, and NEITHER catches the coupon picked up and FLIPPED. A flip about the long +// axis maps y to plate_depth - y and leaves x alone, so the datum stays at the 3.00 mm end and moves +// to the other side of the ladder. Both earlier controls pass. +// +// It matters because the datum's job is HANDED orientation and not merely "which end". A plate has +// four distinguishable placements for one off-axis hole -- near or far, above or below the ladder -- +// and a datum that only fixed the end would leave the two faces interchangeable. On a through-hole +// coupon the two faces are not equivalent: the ladder is measured in canonical orientation, and a +// flipped coupon reverses the sense of any subsequent handed feature the design gains. +// +// The refusal must name FieldCenterY, because the flip leaves the diameter and the x untouched. +test fn w_a_datum_mirrored_across_the_centreline_is_refused() -> Bool { + match hole_ladder_spec { + LadderReady { ladder: l } => { + let contract = realization_contract(declaration: l) + let s = contract.specimen + let mirrored_y = + micrometer_count(m: s.geometry.plate.size_y) - micrometer_count(m: hole_ladder_datum_center_y) + let flipped = datum_moved_to(s: s, x: datum_center_x_um(s: s), y: mirrored_y) + match judge_realization(contract: contract, envelope: envelope_with_datum(s: s, datum: flipped)) { + RealizationJudged { conformance: c } => match c { + GeometryDatumDiverges { field: f, modeled: m, realized: r } => + match f { + FieldCenterY => + micrometer_count(m: m) == micrometer_count(m: hole_ladder_datum_center_y) + && micrometer_count(m: r) == mirrored_y + && mirrored_y != micrometer_count(m: hole_ladder_datum_center_y) + FieldDiameter => false + FieldCenterX => false + } + GeometryConforms => false + GeometryPlateDiverges { axis: _, modeled: _, realized: _ } => false + GeometryOperationCountDiverges { modeled: _, realized: _ } => false + GeometryOperationDiverges { index: _, field: _, modeled: _, realized: _ } => false + } + RealizationRefusedAtWire { refusal: _ } => false + } + } + LadderStepIsZero => false + LadderTooFewRungs { supplied: _ } => false + } +} diff --git a/dag/test/claim/printed_chassis_coupon_witness_test.dag b/dag/test/claim/printed_chassis_coupon_witness_test.dag new file mode 100644 index 00000000000..d1a115ae5ad --- /dev/null +++ b/dag/test/claim/printed_chassis_coupon_witness_test.dag @@ -0,0 +1,199 @@ +module test.claim.printed_chassis_coupon_witness +import std.types { Bool, List } +import std.nat { Nat } +import std.measure { Micrometer, micrometer, micrometer_count, Millimeter, millimeter } +import extdeps.printing.fdm { + BuildEnvelope, + build_envelope, + EnvelopeFit, + PartFits, + PartExceedsEnvelope, + EnvelopeAxis, EnvelopeX, EnvelopeY, EnvelopeZ, + part_extent, + envelope_fit, + MaterialSuitabilityRow, + MaterialSuitabilityLookup, SuitabilityResolved, SuitabilityRowsConflict, + MaterialSuitability, SuitabilityIdeal, SuitabilityNotRecommended, SuitabilityUnstated, + material_suitability, + Pla, Abs, +} +import extdeps.printing.bambu_lab_a1_mini { + a1_mini_build_envelope, + a1_mini_material_suitability, +} +import product.printed_chassis.coupon { + LengthLadder, + LadderConstruction, + LadderReady, + LadderStepIsZero, + LadderTooFewRungs, + length_ladder, + ladder_rungs, + CouponSpecimen, + PlateDimensions, + hole_ladder_spec, + hole_ladder_specimen, + specimen_extent, + specimen_fits, + micrometer_to_millimeter_ceiling, +} +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly +// NO FALLBACK LADDER. The first draft of this file minted a placeholder LengthLadder for the +// non-ready arm, which is the absorbing fallback the module under test exists to forbid — every +// downstream witness would then have been testing the placeholder rather than the declared coupon, +// and would have stayed green while the real specification was refused. Each witness that needs the +// ladder matches the live declaration and FAILS on the refused arm, so a broken specification reds +// the suite instead of quietly substituting for it. +// WITNESS 1 — THE DECLARED LADDER IS WELL-FORMED. The live specification must actually mint, not +// merely be written; a refused ladder would leave every later witness testing the fallback above. +test fn w_the_declared_hole_ladder_mints() -> Bool { + match hole_ladder_spec { + LadderReady { ladder: _ } => true + _ => false + } +} +// WITNESS 2 — THE RUNGS ARE DERIVED, AND THE LAST ONE PROVES IT. Eleven rungs from 3000 um in 100 um +// steps must END at 4000 um. An authored list that drifted from the declared step would fail here, +// which is the redundancy this derivation exists to make impossible. +test fn w_the_ladder_rungs_derive_from_base_and_step() -> Bool { + match hole_ladder_spec { + LadderReady { ladder: l } => { + let rungs = ladder_rungs(l: l) + fold(rungs, init: 0, f: fn(acc, _r) { acc + 1 }) == 11 + && micrometer_count(m: fold(rungs, init: micrometer(count: 0), f: fn(_acc, r) { r })) == 4000 + } + _ => false + } +} +// WITNESS 3 — A ZERO STEP REFUSES. Every rung would be identical, so the specimen would present as a +// ladder while measuring one diameter eleven times — a coupon that cannot discriminate. +test fn w_a_zero_step_ladder_refuses() -> Bool { + match length_ladder(base: micrometer(count: 3000), step: micrometer(count: 0), rung_count: 11) { + LadderStepIsZero => true + _ => false + } +} +// WITNESS 4 — A ONE-RUNG LADDER REFUSES, carrying the count it was given so the refusal is located. +test fn w_a_single_rung_ladder_refuses() -> Bool { + match length_ladder(base: micrometer(count: 3000), step: micrometer(count: 100), rung_count: 1) { + LadderTooFewRungs { supplied: n } => n == 1 + _ => false + } +} +// WITNESS 5 — THE PLATE IS SIZED FROM THE LADDER. Eleven rungs at 9 mm pitch with 6 mm margins is +// 2*6000 + 10*9000 = 102000 um. If the plate were authored beside the ladder rather than derived +// from it, adding a rung would leave this stale. +test fn w_the_plate_width_follows_the_rung_count() -> Bool { + match hole_ladder_spec { + LadderReady { ladder: l } => micrometer_count(m: hole_ladder_specimen(l: l).geometry.plate.size_x) == 102000 + _ => false + } +} +// WITNESS 6 — THE SPECIMEN FITS THE A1 MINI, AND THE ENVELOPE IS THE MACHINE'S, NOT THIS FILE'S. +// +// An earlier revision spelled `build_envelope(180, 180, 180)` right here. That made the witness its +// own subject: it would have stayed green if the real machine had a different envelope, and green if +// no printer authority existed in the corpus at all. Reading extdeps.printing.bambu_lab_a1_mini +// means the vendor row is what this claim is about, and editing that row is what moves it. +test fn w_the_hole_ladder_coupon_fits_the_a1_mini() -> Bool { + match hole_ladder_spec { + LadderReady { ladder: l } => + match specimen_fits(envelope: a1_mini_build_envelope, s: hole_ladder_specimen(l: l)) { + PartFits => true + PartExceedsEnvelope { first: _, rest: _ } => false + } + LadderStepIsZero => false + LadderTooFewRungs { supplied: _ } => false + } +} +// WITNESS 7 — THE CONVERSION ROUNDS UP, AND THIS IS THE CASE TRUNCATION GETS WRONG. 180_500 um +// truncates to 180 mm and would compare EQUAL to a 180 mm envelope — reported as fitting a machine +// it does not fit. Rounding up yields 181 and refuses. The witness asserts the conversion directly +// so the property is pinned even if no current specimen exercises it. +test fn w_the_micrometre_conversion_rounds_up_not_down() -> Bool { + micrometer_to_millimeter_ceiling(m: micrometer(count: 180500)) == millimeter(count: 181) + && micrometer_to_millimeter_ceiling(m: micrometer(count: 180000)) == millimeter(count: 180) + && micrometer_to_millimeter_ceiling(m: micrometer(count: 1)) == millimeter(count: 1) +} +// WITNESS 8 — AND THE ROUNDING ACTUALLY REACHES THE FIT ANSWER. Witness 7 pins the arithmetic; this +// pins that the fit path CONSUMES it. A part 180.5 mm tall must be refused on Z against a 180 mm +// envelope — the exact print that truncation would have greenlit. +test fn w_an_oversize_part_is_refused_on_the_axis_that_exceeds() -> Bool { + let envelope = a1_mini_build_envelope + let part = part_extent( + x: millimeter(count: 100), + y: millimeter(count: 100), + z: micrometer_to_millimeter_ceiling(m: micrometer(count: 180500)) + ) + match envelope_fit(envelope: envelope, part: part) { + PartExceedsEnvelope { first: e, rest: _ } => + match e.axis { + EnvelopeZ => true + EnvelopeX => false + EnvelopeY => false + } + PartFits => false + } +} + +// WITNESS 9 — THE MACHINE GRADES EVERY MATERIAL ITS OWN TABLE NAMES, and the earlier version of +// this witness asserted the wrong thing. +// +// It asserted totality over FilamentMaterial: ten arms, ten rows. That reads as rigour and is +// actually a FABRICATION PRESSURE. The substrate's material universe and the vendor's stated +// population are different things owned by different authorities. If FilamentMaterial later gains an +// eleventh material, the honest A1 mini answer is SuitabilityUnstated -- the vendor never graded it +// -- but a totality assertion would go red and hand the next author a choice between deleting the +// check and INVENTING an eleventh vendor grade. A check whose failure mode is "make something up" +// is worse than no check. +// +// So the assertion is now about the vendor's own table: ten materials are stated, and they are the +// ten the table lists. Growth in the substrate does not red this; a change to what the vendor said +// does, which is the only thing this row is authority for. +test fn w_the_a1_mini_grades_every_material_its_table_names() -> Bool { + a1_mini_material_suitability.length() == 10 +} + +// WITNESS 9b — AND AN UNGRADED MATERIAL RESOLVES TO UNSTATED RATHER THAN REFUSING OR GUESSING. This +// is the arm that makes witness 9 safe to leave alone as the substrate grows: a material the vendor +// never mentioned must come back Unstated, which is a fact about the vendor's silence and not a +// grade. Today every modelled material happens to be graded, so this exercises the lookup's +// behaviour on a row-free material by asking with a roster that omits one. +test fn w_a_material_the_vendor_did_not_grade_reads_unstated() -> Bool { + match material_suitability(rows: [], material: Pla) { + SuitabilityResolved { suitability: s } => + match s { + SuitabilityUnstated => true + SuitabilityIdeal => false + SuitabilityNotRecommended => false + } + SuitabilityRowsConflict { material: _, count: _ } => false + } +} + +// WITNESS 10 — THE GRADING DISCRIMINATES, which a completeness count alone does not show. A roster +// that graded all ten identically would satisfy witness 9 and be useless. PLA is Ideal and ABS is +// Not Recommended in the vendor's own table, and those are the two the chassis decision turns on: +// PLA is what ships in the combo and ABS is what a naive "stronger plastic" instinct reaches for. +test fn w_pla_is_ideal_and_abs_is_not_recommended() -> Bool { + let pla = match material_suitability(rows: a1_mini_material_suitability, material: Pla) { + SuitabilityResolved { suitability: s } => + match s { + SuitabilityIdeal => true + SuitabilityNotRecommended => false + SuitabilityUnstated => false + } + SuitabilityRowsConflict { material: _, count: _ } => false + } + let abs = match material_suitability(rows: a1_mini_material_suitability, material: Abs) { + SuitabilityResolved { suitability: s } => + match s { + SuitabilityNotRecommended => true + SuitabilityIdeal => false + SuitabilityUnstated => false + } + SuitabilityRowsConflict { material: _, count: _ } => false + } + pla && abs +} diff --git a/dag/test/claim/printed_chassis_measurement_witness_test.dag b/dag/test/claim/printed_chassis_measurement_witness_test.dag new file mode 100644 index 00000000000..3df10669bde --- /dev/null +++ b/dag/test/claim/printed_chassis_measurement_witness_test.dag @@ -0,0 +1,281 @@ +module test.claim.printed_chassis_measurement_witness + +import std.types { Bool, List, NonEmptyStr } +import std.nat { Nat } +import std.measure { Millimeter, millimeter } +import std.interval { IntervalReady, IntervalRefused, degenerate_interval } +import std.claim_evidence { + RecordedFact, + EvidenceLink, + EvidenceProvenance, + EvidenceFreshness, + EvidenceFidelity, + EvidenceSupports, +} +import std.spatial_knowledge { + SpatialMeasured, + SpatialUnknown, + SpatialRequirement, + MeasuredOnly, + SpatialAdmittedMeasured, + SpatialAdmittedEstimated, + SpatialRefused, + SpatialGeometryUnknown, + SpatialHypothesisNotAdmissible, + SpatialStandingBelowMinimum, + SpatialUncertaintyExceedsBudget, +} +import product.spatial_dimension { LengthInterval, length_interval } +import product.printed_chassis.measurement { + ChassisMeasurementEvidence, + ChassisLengthStanding, + ChassisLengthAdmission, + ChassisMeasurementOutcome, + ChassisMeasurementJudged, + ChassisRosterConflict, + FabricationMeasurement, + fabrication_measurement, + FabricationMeasurementKey, + fabrication_measurement_key, + Altrad8udBoard, + CpuCoolerFourU, + CpuCoolerTwoU, + NodePowerSupply, + Fan80mm, + FabWidth, + FabDepth, + FabHeight, + required_chassis_length, + mvp_measurement_roster, +} +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +fn caliper_evidence() -> ChassisMeasurementEvidence { + EvidenceLink { + fact: RecordedFact { id: "fact-4u-cooler-overall-height", value: "overall height of the held 4U cooler" }, + direction: EvidenceSupports, + inference_rule: "direct-caliper-read", + authority: "operator", + provenance: EvidenceProvenance { + entity: "held-4u-cooler", + activity: "operator-caliper-measurement", + agent: "operator", + }, + freshness: EvidenceFreshness { maximum_conclusion: "as-held", basis: "measured on the unit in hand" }, + fidelity: EvidenceFidelity { boundary: "overall envelope only", losses: ["fin tip burrs not characterised"] }, + probe_independence: "independent-of-vendor-collateral", + } +} + +// AN UNBUILDABLE FIXTURE BECOMES UNKNOWN, NOT PERFECT, and the arm this replaces was the worst +// fallback in the PR because it sat in the fixtures every other witness is measured against. +// +// The earlier `interval_or_degenerate` turned a REFUSED interval into `degenerate_interval(0 mm)` -- +// uncertainty [0,0], which is MAXIMALLY PRECISE. So a fixture that failed to build did not merely +// survive: it became the most precise measurement expressible, satisfying every precision budget +// downstream. A fail-open, pointing the wrong way, inside the test data. +// +// `std.interval` states the rule this broke in its own annotation: the degenerate constructor "is +// not a default -- a caller wanting a WIDTH still goes through the refusing mint." +// +// The refusal now lands in SpatialUnknown, which is vocabulary this module already refuses on +// (SpatialGeometryUnknown), so an unbuildable fixture reddens the witness that depends on it instead +// of flattering it. No new refusal path was invented for this; the existing one was routed to. +fn measured_with_half_width(value: Nat, half_width: Nat, obligation: NonEmptyStr) -> ChassisLengthStanding { + match length_interval( + low: millimeter(count: value - half_width), + high: millimeter(count: value + half_width), + ) { + IntervalReady { interval: i } => + SpatialMeasured { + value: millimeter(count: value), + uncertainty: i, + evidence: caliper_evidence(), + } + IntervalRefused { reason: _ } => SpatialUnknown { obligation: obligation } + } +} + +// Measured to +/- 1 mm. +fn measured_precise(value: Nat) -> ChassisLengthStanding { + measured_with_half_width(value: value, half_width: 1, obligation: "fixture-interval-unbuildable-precise") +} + +// Same STANDING, +/- 15 mm. A cooler height known only to 30 mm cannot set a bay pitch. +fn measured_coarse(value: Nat) -> ChassisLengthStanding { + measured_with_half_width(value: value, half_width: 15, obligation: "fixture-interval-unbuildable-coarse") +} + +fn cooler_height_key() -> FabricationMeasurementKey { + fabrication_measurement_key(subject: CpuCoolerFourU, axis: FabHeight) +} + +// A millimetre budget: the bay pitch is a stack of tolerances, so the consuming decision demands +// each contributor be known to a couple of millimetres. +// THE BUDGET IS NOT RECOVERED FROM A REFUSAL, AND AN EARLIER REVISION OF THIS FILE ARGUED THAT IT +// COULD BE. The argument was that [0,0] is fail-CLOSED in budget position -- as an observation it +// claims perfect precision and admits everything, but as a budget it admits nothing, so substituting +// it on refusal was safe. That is wrong, and the reason is about EVIDENCE rather than about safety. +// +// If constructing the intended [0,4] budget ever refused, the substitute would make the negative +// witnesses below stay GREEN FOR THE WRONG REASON: "a coarse measurement is refused" would hold +// because the budget collapsed, not because the four-millimetre policy rejected it. A fixture +// construction failure would have been silently converted into a policy verdict, and the witness +// would report that the policy works while never having exercised it. +// +// Negative witnesses are especially exposed to this, because MORE refusal leaves them green. It is +// the same family as the placeholder ladder already removed from this program -- a wall greening on +// a substitute subject -- wearing a conservative disguise, which is how it survived a round of +// review including my own defence of it. +// +// The FIRST attempt at this repair reproduced the defect one layer out: it routed the refused arm to +// a synthesised ChassisRosterConflict so that callers could stay unchanged. That is the same +// fabrication with a different value. There is no safe substitute, because the problem is not which +// value is chosen -- it is that a value exists at all. +// +// So the budget is threaded, not recovered. with_budget runs the witness body only on the READY arm +// and answers false on the refused one, which is the only structure under which a green result means +// the intended budget was actually exercised. +fn with_budget(body: fn(LengthInterval) -> Bool) -> Bool { + match length_interval(low: millimeter(count: 0), high: millimeter(count: 4)) { + IntervalReady { interval: i } => body(i) + IntervalRefused { reason: _ } => false + } +} + +fn ask(roster: List, budget: LengthInterval) -> ChassisMeasurementOutcome { + required_chassis_length( + roster: roster, + key: cooler_height_key(), + obligation: "measure-4u-cooler-overall-height", + requirement: SpatialRequirement { + minimum_standing: MeasuredOnly, + maximum_uncertainty: budget, + }, + ) +} + +// Locally named rather than `admitted`, because three other witness modules declare that spelling +// and the whole-tree namespace is flat. The earlier bare `admitted` here resolved to nothing after a +// refactor removed it, and the compiler refused with an ambiguous-reference diagnostic naming all +// three candidates rather than silently binding this file to a stranger's predicate -- which is the +// fail-closed behaviour the v2.compiler.body_producer_forward defect earlier today did NOT get, +// because there the colliding name resolved successfully to the wrong type. +fn chassis_outcome_is_admitted(a: ChassisMeasurementOutcome) -> Bool { + match a { + ChassisMeasurementJudged { admission: adm } => + match adm { + SpatialAdmittedMeasured { value: _, uncertainty: _ } => true + SpatialAdmittedEstimated { region: _ } => true + SpatialRefused { cause: _ } => false + } + ChassisRosterConflict { key: _, count: _ } => false + } +} + +// WITNESS 1 — THE PROGRAM'S CENTRAL REFUSAL. The MVP roster is empty today, so the generator's own +// entry point must refuse for a dimension nobody has measured. This is the arm that makes the +// fabrication program fail closed: while it holds, no printed part can be generated against an +// invented cooler height. +test fn w_unmeasured_dimension_refuses_on_the_live_roster() -> Bool { + with_budget(body: fn(budget) { + match ask(budget: budget, roster: mvp_measurement_roster) { + ChassisMeasurementJudged { admission: SpatialRefused { cause: SpatialGeometryUnknown { obligation: o } } } => + o == "measure-4u-cooler-overall-height" + _ => false + } + }) +} + +// WITNESS 2 — THE POSITIVE CONTROL. Without this, witness 1 is satisfied by an interface that +// refuses everything, which would be a wall that never admits rather than a wall that discriminates. +test fn w_a_precise_measurement_is_admitted() -> Bool { + with_budget(body: fn(budget) { + let roster = [fabrication_measurement(key: cooler_height_key(), standing: measured_precise(value: 150))] + match ask(budget: budget, roster: roster) { + ChassisMeasurementJudged { admission: SpatialAdmittedMeasured { value: v, uncertainty: _ } } => + v == millimeter(count: 150) + _ => false + } + }) +} + +// WITNESS 3 — THE DISCRIMINATING PAIR, and the one that would have caught a lookup keyed on +// non-emptiness rather than identity. The roster is POPULATED, and populated with lengths in the +// same units and the same plausible range — but for other subjects and other axes. A fold that +// returned the first row, or any row, would answer 80 mm or 244 mm for the cooler's height and the +// bay pitch would be built from a fan's width. The ask must still refuse. +test fn w_a_different_subjects_measurement_does_not_satisfy_the_ask() -> Bool { + with_budget(body: fn(budget) { + let roster = [ + fabrication_measurement( + key: fabrication_measurement_key(subject: Fan80mm, axis: FabWidth), + standing: measured_precise(value: 80), + ), + fabrication_measurement( + key: fabrication_measurement_key(subject: NodePowerSupply, axis: FabHeight), + standing: measured_precise(value: 86), + ), + fabrication_measurement( + key: fabrication_measurement_key(subject: CpuCoolerTwoU, axis: FabHeight), + standing: measured_precise(value: 70), + ), + fabrication_measurement( + key: fabrication_measurement_key(subject: CpuCoolerFourU, axis: FabDepth), + standing: measured_precise(value: 120), + ), + ] + !chassis_outcome_is_admitted(a: ask(budget: budget, roster: roster)) + }) +} + +// WITNESS 4 — SUBJECT MATCHES, AXIS DOES NOT, ISOLATED. The last row of witness 3 already carries +// this case, and it is asserted alone because a key comparison that ignored the axis would still +// pass witness 3 on the strength of its first three rows. A 4U cooler's DEPTH is not its HEIGHT. +test fn w_the_right_subject_on_the_wrong_axis_refuses() -> Bool { + with_budget(body: fn(budget) { + let roster = [ + fabrication_measurement( + key: fabrication_measurement_key(subject: CpuCoolerFourU, axis: FabDepth), + standing: measured_precise(value: 120), + ), + ] + match ask(budget: budget, roster: roster) { + ChassisMeasurementJudged { admission: SpatialRefused { cause: SpatialGeometryUnknown { obligation: _ } } } => true + _ => false + } + }) +} + +// WITNESS 5 — STANDING IS NOT SUFFICIENCY. A real caliper read, correctly keyed, that is simply too +// coarse for a stacked-tolerance decision. It must refuse on the BUDGET rather than on the standing, +// which is what distinguishes a precision check from a provenance check. +test fn w_a_measurement_too_coarse_for_the_decision_refuses_on_budget() -> Bool { + with_budget(body: fn(budget) { + let roster = [fabrication_measurement(key: cooler_height_key(), standing: measured_coarse(value: 150))] + match ask(budget: budget, roster: roster) { + ChassisMeasurementJudged { admission: SpatialRefused { cause: SpatialUncertaintyExceedsBudget { actual: _, budget: _ } } } => true + _ => false + } + }) +} + +// WITNESS 6 — TWO MEASUREMENTS THAT DISAGREE MUST NOT RESOLVE. This is the regression control for a +// real defect in the first revision of this module: the fold returned row.standing on every match, +// so the LAST matching row silently won and the roster's own contradiction was discarded. Both rows +// below are correctly keyed, both are precise, and they disagree by 15 mm. Nothing here is entitled +// to pick one, so the outcome is a conflict naming the key and the count — never an admitted 165. +test fn w_two_disagreeing_rows_for_one_key_refuse_as_a_conflict() -> Bool { + with_budget(body: fn(budget) { + let roster = [ + fabrication_measurement(key: cooler_height_key(), standing: measured_precise(value: 150)), + fabrication_measurement(key: cooler_height_key(), standing: measured_precise(value: 165)), + ] + match ask(budget: budget, roster: roster) { + ChassisRosterConflict { key: _, count: c } => c == 2 + _ => false + } + }) +} diff --git a/docs/plans/printed-chassis-program.md b/docs/plans/printed-chassis-program.md new file mode 100644 index 00000000000..3f172b82bc0 --- /dev/null +++ b/docs/plans/printed-chassis-program.md @@ -0,0 +1,548 @@ +# Printed node chassis — program plan + +**Pinned plan. Updated 2026-09-02.** Printers land **2026-09-03**. + +Governing statement: + +> Build a low-cost, space-efficient, thermally intentional system of independently removable +> ALTRAD8UD-1L2T server cartridges, using small-format printers for the custom geometry and +> conventional materials only where they are structurally superior. + +The experiment succeeds when the model produces real printer artifacts, a board fits, a node runs, a +middle node is removable without disturbing neighbours, and the cost/space/thermal receipts decide +whether more printers are worth buying. + +## Original motivations (the spine — every decision answers to these) + +1. Cheaper than commodity chassis. +2. More space-efficient — this is not a storage chassis. +3. Deliberately directed airflow, not a case shaped for a different machine. +4. Forcing pressure on the spatial/fabrication model. This is a first-class goal, not a side effect. + +## Fixed facts + +| Fact | Value | Authority | +|---|---|---| +| Node subject | ASRock Rack ALTRAD8UD-1L2T | `extdeps.boards.asrock_rack` | +| Board outline | 267 x 244 mm | vendor manual §1.4, read first-party | +| Intended nodes | 8 (srv1-4 + 4 inbound) | operator | +| Printers | 2 x Bambu Lab A1 mini, scaling to N | operator order relay | +| Build volume | 180 x 180 x 180 mm | A1 mini spec table, operator relay | +| Fan form factor | 80 mm; **count derived**, not assumed | operator + derivation | +| Rack unit | 2x2 block, composable | side-chat ruling | +| Service law | fixed frame, removable cassette | operator requirement R9 | +| PSU placement | cassette-resident | side-chat ruling | +| External bundle | 2 x Ethernet + 1 x AC per node | operator | + +## Standing laws + +- **Missing physical input policy: refuse.** No default, no nominal catalogue figure, no nearby standard. +- **Hidden CAD geometry authority: refuse.** The model owns dimensions *and* geometry-selection laws. +- **Printed polymer is never the mains enclosure and never a conductor in either grounding network.** Protective earth is bolted to metal and survives every removal the design invites; the board-to-chassis bond is functional only. +- **MVP thermal fixture choice carries no authority over deployment layout.** Using the 4U cooler + first to reduce thermal uncertainty must not silently become the rack pitch. +- **Bay pitch derives from measured millimetres.** "2U" and "4U" are catalogue labels, not lengths. + + +## The numbered spine — PRINT-0 .. PRINT-15 + +The six projects are the working-memory units; these are the executable steps. Zero-indexed per the +RLM-N / MEMORY-0 convention already used in this directory. Each step names its terminal evidence, +because a step without one cannot be said to be done. + +| Step | Project | Terminal evidence | State | +|---|---|---|---| +| **PRINT-0** | MEASURE | Board outline typed from the vendor manual (243.840 x 266.700 mm exact, axes corrected); micro-ATX lettered grid under its own standard authority; standoff placement derived from per-location evidence standings | **done** | +| **PRINT-1** | TOOLCHAIN | Build envelope, filament classes, slicer platform claims as separate authorities, **and a concrete A1 mini product row that the coupon fit witness consumes** | reopened | +| **PRINT-2** | MEASURE | Measurement authority: absent refuses, duplicate-key conflict refuses, precision budget enforced | **done** | +| **PRINT-3** | CAL | Coupon authority: ladder as modeled experimental design, rungs and plate derived | **done** | +| **PRINT-4** | TOOLCHAIN | Realization contract v0: contract derives its own rungs; a wrong-step handler is caught and located | **done** | +| **PRINT-5** | TOOLCHAIN | Raw transport schema admission: unknown version, missing field and unknown operation all refuse before any geometry call | | +| **PRINT-6** | TOOLCHAIN | CadQuery handler + four-part authority wall; all four negative controls flip | | +| **PRINT-7** | TOOLCHAIN | STEP/3MF emitted and re-inspected; output conformance re-establishes envelope, holes, walls | | +| **PRINT-8** | TOOLCHAIN | Slicer profile bound or refused; per-printer manifests; ProcessQualificationIdentity minted, not branded | | +| **PRINT-9** | CAL | Coupons printed on BOTH printers; each printer+spool admitted or refused **independently** | needs printers | +| **PRINT-10** | FIT | Adjustable-standoff fixture; real board mounted unpowered; hole map measured back and frozen | needs printers + board | +| **PRINT-11** | CASSETTE | Structural cassette: rails, tray, handle, latch; carries node mass; no seam in layer-separation tension | needs PETG decision | +| **PRINT-12** | CASSETTE | PSU carrier and harnesses; every connector insertable; nothing side-loaded; **PE continuous with board, standoffs and cassette all removed** | needs PSU envelope | +| **PRINT-13** | CASSETTE | 80 mm fan carrier + replaceable duct; powered thermal admitted against a bench baseline | needs cooler choice | +| **PRINT-14** | RACK | One fixed bay; cassette retained in service, removable after disconnect; empty bay structurally complete | | +| **PRINT-15** | RACK | Management-node mount (Raspberry-Pi class) on the rack, carried as a bay peer rather than an accessory | | +| **PRINT-16** | RACK | 2x2 block; an enclosed node extracted with neighbours untouched | | +| **PRINT-17** | VERDICT | Cost, volume, print hours, labour, reprint rate, thermal, service time -> buy-more-printers decision | | + +**THE SEQUENCE IS INTEGERS, AND AN EARLIER REVISION BROKE THAT.** It carried PRINT-11b and PRINT-13b +while still calling itself N = 15, so the spine had two numbering authorities at once and the count +was wrong. Letter suffixes were how cable routing and the management mount got appended as +afterthoughts instead of being placed. Renumbered; new work takes the next integer. + +**CABLE ROUTING IS NOT A STEP.** The operator's requirement is routing at EVERY controlled layer, so +it is a property each cassette and rack step must satisfy to be called done, not one step of its own. +It was PRINT-11b, which was exactly the bolt-on that requirement forbids. Every step from PRINT-11 +onward now carries the cable obligation in its own terminal evidence: endpoints, bend and service +volume, clip positions, strain relief, moving-versus-fixed classification, and declared separation +from blades and hot surfaces. + +**N = 17.** PRINT-0 through PRINT-4 are landed and executing (27 witnesses); PRINT-1 is REOPENED because the build envelope is authored inside the fit witness rather than owned by a printer product row, so that witness would stay green if the product authority changed or vanished. PRINT-5 through PRINT-7 +are the pre-arrival critical path and depend on no operator input. PRINT-8 is the first step that +needs hardware. + +### What blocks what + +- **Nothing blocks PRINT-5..7.** These are the two-day cut. +- **Joint family** (dovetail / tongue-and-groove / keyed slide / pin) gates the + ProductionInterfaceCoupon only — a later half of PRINT-8, not the MachineProcessCoupon. +- **PETG** gates PRINT-10 onward. PLA carries PRINT-8 and PRINT-9 and stops there: no PLA-to-PETG + receipt carry. +- **Deployment envelope** gates PRINT-13..14 layout admission, nothing earlier. +- **Drive count** gates PRINT-11 completion only. + +## The six projects + +| Project | Scope | Terminal evidence | State | +|---|---|---|---| +| **CONTRACT** | Goals, non-goals, authority graph, refusal law, MVP boundary | No assumption represented as a default | deferred — no consumer yet | +| **MEASURE** | Board, cooler, PSU, fan, DIMM, cable, **deployment envelope**, uncertainty | Pack sufficient to generate CAL+FIT | **partial — carrier landed, roster empty** | +| **TOOLCHAIN** | Realization contract, CadQuery handler, authority wall, STEP/3MF, slicer env, printer nodes | Deterministic generation + executed no-parallel-authority controls | not started | +| **CAL+FIT** | Coupons, qualified tolerances, adjustable standoff fixture, real-board fit, hole-map feedback | One unpowered board fits; hole authority admitted | not started | +| **CASSETTE** | Structure -> PSU/cables -> airflow -> powered thermal | Removable node operates and is serviceable | not started | +| **RACK+VERDICT** | One bay -> 2x2 block -> scale/economics | Middle-node service proven; buy-more-printers verdict | not started | + +Consolidation from eleven stages must not collapse the internal gates. CASSETTE keeps +`structural -> PSU/cable -> airflow -> powered thermal`; RACK+VERDICT keeps +`single bay -> populated 2x2 -> economic verdict`. + +## The CAD authority wall (TOOLCHAIN's load-bearing control) + +CadQuery is a **realization handler**. It may map modeled operations to kernel APIs, reorder +provably-equivalent operations, heal representations, triangulate a determined solid, and implement +a *modeled* derivation whose identity and inputs the model already fixed. + +It may **not** choose dimensions, offsets, clearances, wall thicknesses, radii, chamfers, feature +presence, hole patterns, joint topology, rib placement, segmentation boundaries, print orientation, +load-path geometry, duct path or cross-section, fallback values, or one construction algorithm over +another where the physical result differs. + +A numeric-literal scan is **necessary but insufficient** — `fillet()` vs `chamfer()` carries no +literal. The wall is four-part: + +- **A. Geometry-taint dataflow.** Any expression reaching a geometry-affecting call derives only + from the typed contract, a modeled operation, or a proved non-semantic toolchain constant. +- **B. No-default completeness.** Unknown feature kinds, missing fields, unsupported derivations and + schema skew all refuse. No Python defaults for geometry-affecting fields. +- **C. Realization trace.** Every realized feature maps to one modeled source; no unmodeled feature. +- **D. Output conformance.** Re-inspect the emitted STEP/3MF for envelope, hole centres, wall + thickness, mating dimensions, clearances, build-envelope fit, collision/extraction envelopes. + +**Negative control:** hard-code a plausible wall thickness in the handler and prove the wall rejects +it while the part still looks valid. A wall that never flips is a decoration. + +Duct curvature is the boundary case: inlet + outlet + envelope + airflow obligation do **not** +determine a duct. The model must fix the family and the selection law (centerline derivation, +minimum bend radius, wall thickness, transition rule); the handler may implement that law and may +not choose it. + +## Landed so far + +- `extdeps.boards.asrock_rack` — typed 243840 x 266700 um outline, first-party manual read. The + extents are NOMINAL: `asrock_altrad8ud_board_depth_nominal_exact` is the exact ARITHMETIC + conversion of the vendor's published 9.6 x 10.5 in, not the as-built extent of any board here, and + the rename exists to stop "exact" being read as zero physical tolerance by a clearance derivation. + Mounting holes are a standard-location correspondence with a per-location standing, so an inferred + hole and a physically confirmed one are different facts; `asrock_altrad8ud_open_mounting_unknowns` + carries the five unmeasured ones with their discharge instrument. +- `extdeps.standards.micro_atx` — the nine microATX mounting locations own their own authority + rather than sitting inside the ATX 2.2 module, which now carries only ATX 2.2 facts. Coordinate + provenance is `OperatorRelayedDocument` from the shared `DimensionEvidence` carrier, not a prose + string: a citation STATUS is a typed fact, and the string form was a nickname nothing could consume. + **One structural over-claim is recorded and deliberately not half-fixed** — `extdeps_model_scope` + cites the archived ATX 2.2 PDF as `first_citation` for the microATX locations, a machine-readable + claim the provenance row denies, because this session's extraction recovered that PDF's text layer + and not its mounting-location artwork. No microATX document is in hand, so the repair needs a + first-party read or an `ExternalAuthority` arm that can carry a relayed-with-no-document chain; + both are named as triggers rather than guessed at. +- `extdeps.printing.bambu_lab_a1_mini` — the printer as a PRODUCT ROW: build envelope, nozzle + diameters, filament diameter, temperature ceilings, input voltage and frequency range, machine + extents, and a ten-row material suitability roster. The fit witness reads the envelope from here + instead of a literal it wrote itself, so it goes red if the printer authority vanishes. +- `extdeps.vendor.bambu_lab`, `extdeps.printing.fdm` — agnostic FDM shapes; build-envelope fit that + reports every exceeded axis and never searches orientations. +- `extdeps.printing.bambu_studio` — spec-sheet and release-artifact platform claims carried as two + authorities; the Linux disagreement modeled, not resolved. +- `product.printed_chassis.measurement` — SPATIAL-1 binding; absent refuses, duplicate-key conflict + refuses with no precision or recency tie-break. Six witnesses green, two proven to flip. +- Compile-clean: 0 blocking errors in these files; the 57 remaining are pre-existing on main. +- `product.printed_chassis.coupon` — **TOOLCHAIN v0's first consumer.** The hole-diameter ladder as a + modeled experimental design: base, step and rung count are authored, every rung and the plate width + are DERIVED. `PlateDimensions` is its own type so a malformed plate has no zero-extent fallback to + return. Micrometre-to-millimetre conversion rounds UP, because truncation reports a 180.5 mm part + as fitting a 180 mm machine. Eight witnesses green; the conversion proven to flip in both the + arithmetic and the fit path. **V0 is now closed at one operation** (`OpThroughHole`) — see the v0 + population section for why the second one was deleted rather than kept. +- `product.printed_chassis.realization_contract` — the transport wall. Raw JSON from the CAD handler + is admitted through `decode_envelope`, which refuses an unsupported schema version, an unknown + operation kind, and an envelope carrying no operations, each with a typed cause naming what it + received. Conformance reports the EARLIEST divergence rather than the last, and a count mismatch is + its own outcome rather than a silent zip truncation. + + **It compares WHOLE GEOMETRY, not the whole specimen, and the distinction is load-bearing for + PRINT-5.** Compared: plate on three axes, operation count, then every operation field. NOT compared: + specimen identity (carried, single-armed), revision (not a compared subject at all), and feature + identity — operation *i* is "the *i*-th rung" by LIST POSITION, not by an identity the operation + carries. A permutation is refused because position is compared, which is not the same as features + having identities, and the difference reappears the moment two features share a geometry. PRINT-5 + must not read a conforming verdict as adjudicating identity or canonical ordering. + + **The admitted value is unforgeable, and an earlier revision only CLAIMED it was.** That revision + put the geometry on the accepted arm (`EnvelopeDecodedV0 { plate, features }`) and argued admission + was unavoidable "because the refusal arms have no geometry to hand on" — a correct argument for an + insufficient conclusion, since it rules out the raw envelope bypassing the judge and says nothing + about a caller bypassing the raw envelope. A probe compiled the forgery from a foreign module. + `DecodedRealizationV0` is now `sole_constructor`, so only `decode_envelope` can mint one; a foreign + module may name the arm and cannot obtain a value to put in it. + + **That wall now has an executing witness, and the claim that it could not have one was false.** + An earlier revision of this plan said the RED was a compile failure and so could not be enrolled in + a corpus that must compile, and named an expect-compile-refusal harness as the missing capability. + That was DESIGN §4b's own distinction misapplied: a state unauthorable in the ACCEPTED CORPUS may + still be perfectly authorable as SOURCE HANDED TO THE COMPILER BY A FIXTURE, and only the second + boundary decides whether a check's RED exists. The harness was already here — + `gunbc.compile_diagnostic_census`, whose `compile_dag_diagnostic_census` takes source as data and + returns either an observed diagnostic population or a typed `CensusNotRunnable`; the seven-form + precedent against a sealed fixture type is `test.claim.sole_constructor_completeness_audit_probe_test`. + The finding was routed by the side chat, which cited the precedent rather than the claim. + + The witness is `test.claim.printed_chassis_admitted_realization_seal_witness_test`, built on the two + forms that module's own annotation names as exact: a count scoped to diagnostic class AND + `subject_name`, and a differential between two sources differing on one axis. It carries a red + source writing the `DecodedRealizationV0` record literal from a foreign module, a green source with + identical imports and no literal, and the red-minus-green subtraction as a third witness so the + shared imported closure cancels rather than being asserted away. The `CensusNotRunnable` arm answers + `-1`, so every assertion compares against a non-negative quantity and a harness that never ran + satisfies nothing — which is exactly the vacancy that produced the near-false-finding below. + + **The refusal payload could carry a success, and the witnesses were where it showed.** + `RealizationVerdict`'s refusal arm was typed `RealizationRefusedAtWire { admission: EnvelopeAdmission }`, + and `EnvelopeAdmission` includes `EnvelopeDecodedV0`. No route produces that state — + `judge_realization` builds the refusal arm only on the three refusing branches — but reachability is + not occupancy, and the state was writable. The tell was not in the contract at all: four witnesses + carried a dead `EnvelopeDecodedV0 { admitted: _ } => false` arm purely to satisfy exhaustiveness over + a case the route cannot produce, which is what a coproduct too wide for its position looks like from + the consumer side. The refusal reasons are now their own closed coproduct `EnvelopeRefusal`, and + `EnvelopeAdmission = EnvelopeDecodedV0 | EnvelopeRefused { refusal: EnvelopeRefusal }`. The class + climbs from mechanically preventable to structurally impossible, and the four dead arms are deleted + with it — §4b(4) retires the redundant production handling while every discriminating witness stays + enrolled. + + **The trusted-type boundary sat one step early, and the fix turned out to be the name.** The routed + review's objection was that the admitted carrier is minted before conformance runs. I pushed back + that decode-admitted and contract-conformant are two genuinely different facts and so the *stage* + was not wrong. That was true and beside the point: the defect was that an unqualified capability + name — "admitted" — was attached to the earlier fact, while it was also the only geometry-bearing + value a handler could obtain. Renamed `DecodedRealizationV0`. The stage stayed. + + **What the pushback did surface is a second, real defect, deferred deliberately.** `judge_realization` + returns a verdict and no geometry, so a handler must obtain geometry elsewhere and associate it with + the verdict itself. That association is unbound: judge envelope A, retain envelope B's decoded + geometry, hand B to the handler under A's conforming verdict. Every honest caller passes the same + envelope twice and the invalid pairing stays writable — the same class as the refusal payload above, + one level out. The close is a second sealed type returned *from* the judgment that established + conformance, minted from the contract's own canonical specimen rather than from the transported + values that happened to compare equal, so what a handler cuts is the model's geometry and the wire is + reduced to an assertion that was checked. `AdmittedRealizationV0` is reserved for it and unspent. + + It is not built in this revision because nothing actuates geometry yet: with no handler the pairing + has no site at which to go wrong, and minting a sealed carrier with zero consumers to hold a symbol + is what §2 prices as redundant. So it is declared as `realization_v0_open_obligations` — a typed + carrier and not an annotation, because PRINT-5 must not be able to reach a handler without answering + it, and no `Accepted` program can read a comment. + + **The coupon could not be identified from its own geometry, and the fix is an authority change, not + a handler change.** The ladder steps 0.10 mm across eleven rungs, so end to end the holes differ by + 1 mm and are visually interchangeable; rotated 180° the coupon reads as a valid coupon with its + ordinals reversed, and every measurement is attributed to the wrong rung. Routed review found it, + and also corrected its own first proposal — one obligation was doing two jobs: + + - **orientation** — which end of *this* coupon is the 3.00 mm end. A property of the canonical + geometry, and now discharged by making that geometry asymmetric. + - **print-instance attribution** — which printer and spool made *this* piece of plastic. Two + correctly-oriented R1 coupons remain interchangeable. No geometry closes this, because the datum + must be *identical* on both coupons or the two processes stop sharing a subject. It stays open, + routed to the manufacturing manifest and a physical handling route. + + Holding them as one obligation is why the earlier route fold was near-vacuous — a single arm whose + RED could not be authored. Splitting is what let one of them close. `HoleDiameterLadderR1` is the + coupon *design* identity and never the identity of a printed instance. + + **The datum is its own field, not another entry in the feature list.** Appending one more + `OpThroughHole` and remembering the last one is the datum makes "which hole is the datum" a + positional convention — the class this module already deleted once — and it is worse here, because + the datum exists precisely to remove an ambiguous reading. `HoleDiameterCouponGeometry` carries + `plate`, a scalar `orientation_datum`, and `ladder_holes`, which makes four things structural: one + datum exactly (zero and two are unwritable, not refused), the datum cannot become a twelfth rung, + canonical geometry with no datum has no representation, and every consumer must name which + population it means. The wire splits the same way — two *different* populations, not two parallel + lists of one. + + **The near-miss worth recording is inside the derivation.** A first cut read rung zero's x back off + the built feature list to make the correspondence structural. `.first()` returns an option, so it + forced an `Absent` arm for a ladder that cannot be empty — and the arm answered with a fabricated + datum at the margin. An absorbing fallback in miniature, inside the one function the whole + orientation guarantee rests on. It now reads `hole_ladder_margin`, the same row the ladder fold's + `i = 0` term reads: one row, two readers, no unreachable branch to fabricate in. The correspondence + is asserted by `w_the_datum_is_at_rung_zero` rather than constructed, which is honestly one rung + lower — mechanically preventable, not structurally impossible — with the trigger named. + + **Evidence, and it discriminates.** Six controls: canonical datum conforms; datum at the far end + refuses naming `FieldCenterX` (the 180° reading itself); datum on the ladder centre-line refuses + naming `FieldCenterY` (right x, so it passes only if the y is compared); the datum stays out of the + measured population; it clears the ladder band and the plate edge; and it sits at rung zero's x. + A mutation that compares the modeled datum against itself turns the two refusal controls **RED** + while the positive control stays green — so they discriminate the wall rather than merely + exercising it. + + **Probe discipline learned here, recorded because it nearly produced a false finding.** The first + forgery probe returned exactly the baseline error count — consistent with "forgery permitted" — from + a file the compiler had never read, because an added source root was silently ignored. Confirmation + and vacancy produce the same number. Only a deliberate must-fail control in the same file + distinguished them. + +## The two-day cut (printers arrive 2026-09-03) + +**Ruling: a CAL-driven vertical slice, not a general framework and not hand-authored coupon CAD.** + +``` +CalibrationCouponAuthority -> RealizationContract v0 -> four-part wall + -> CadQuery handler -> STEP/3MF conformance -> bound slicer profile + -> per-printer-node manifests -> physical coupon observations +``` + +The coupon is TOOLCHAIN's first real consumer. Governing rule: + +> **Generalize TOOLCHAIN only one consumer ahead.** CAL determines v0; FIT determines the next +> expansion; CASSETTE the next. A new geometric operation arrives only with taint coverage, +> refusal behaviour, trace coverage and output conformance. + +A wall with no handler is only a rule definition — the geometry-taint arm is not commissioned until +it observes real geometry calls, passes the lawful ones and rejects mutations. + +### v0 operation population (closed; a feature belongs only if a chosen coupon consumes it) + +box/prism · cylindrical through-hole · slot · linear or grid repetition · male/female clearance pair · +wall or rib · rigid transforms · boolean union and subtraction + +**`part/revision datum marking` was in this list and has been REMOVED from it, deliberately.** As +`OpDatumMark { text, at_x, at_y }` it fixed text and position and left FONT, GLYPH METRICS, STROKE +WIDTH, ALIGNMENT, ORIENTATION, DEPTH and ENGRAVED-VERSUS-EMBOSSED to the handler — the §3 tell in its +exact form, the handler choosing geometry the model had not fixed. It had already produced a silent +falsehood: `specimen_extent` assumed the mark was engraved and so assumed it could not enlarge the +plate, an assumption stated nowhere and enforced by nothing, and a handler that embossed would make +the envelope-fit answer wrong in the unsafe direction. Determining it fully means modelling fonts, +which is a domain rather than a field, imported to label a calibration coupon. + +The need behind it is real and is tracked, not dropped: several coupons will exist physically and +must be told apart by hand. `coupon_v1_physical_identification_obligation` carries it as a V1 +obligation with the route that looks right — identify the coupon by GEOMETRY, a coded through-hole or +notch pattern, which `OpThroughHole` already determines completely, checked by the same contract the +holes already pass through. + +The ladder itself is a modeled experimental design. "It is only a calibration coupon" is not +permission for Python to choose test dimensions. + +### CAL splits into two coupon classes + +- **`MachineProcessCoupon`** — X/Y deviation, hole and slot deviation, sliding clearance, thin wall + and rib, orientation anisotropy, first-layer behaviour, repeated-feature consistency. Depends on + **no** server or site measurement. This is the first print. +- **`ProductionInterfaceCoupon`** — the exact joint family, insert/captive-nut geometry, fastener + clearance, rail fit. Needs no server dimensions but **does** need the joint family and purchased + hardware identities chosen. Do not invent an M3 pocket or dovetail angle to populate it. + +### The slicer is a SECOND authority boundary + +Scaling, dimensional compensation, line width, first-layer compensation, wall construction, layer +height and orientation all change the physical result. A `.3mf` carrying hidden hand-edited +compensation is as much a parallel authority as a Python literal. Qualification identity: + +``` +printer_node x firmware x material_product x material_spool x installed_nozzle + x slicer_identity x slicer_profile x orientation x support_policy + x coupon_revision x calibration_epoch +``` + +### Wall commissioning needs four negative controls, not one + +1. **Numeric/dataflow** — a plausible Python-derived wall thickness. Taint must reject. +2. **Nonnumeric topology** — a fillet, chamfer or extra rib with no modeled feature identity. Trace + or taint must reject. +3. **Default** — omit a required contract field and let a helper default take over. Completeness + must reject. +4. **Output** — alter an exported hole or envelope after lawful realization. Conformance must reject. + +### Material: PLA does not carry to PETG + +No PLA-to-PETG receipt carry. Distinct admissions: +`ToolchainSmokeAdmitted` · `FitPrototypeProcessQualified` · `StructuralProcessQualified` · +`ThermalServiceQualified`. + +So the PETG decision blocks the **durable/powered CASSETTE path**, not the first CAL print or the +unpowered FIT fixture. Qualify each printer-spool combination independently; never infer that an +observed difference is the printer alone. + +## Open decisions (operator) — none block the first print + +- **Drive count** — a CASSETTE completion obligation. Blocks nothing before Thursday. +- **PETG** — blocks structural/powered parts, not CAL or unpowered FIT. +- **Deployment envelope** — **not on the pre-arrival critical path.** Its absence must refuse + rack-layout admission later, not block calibration now. + +## Next + +1. ~~`CalibrationCouponAuthority`~~ — landed as `product.printed_chassis.coupon`. +2. `RealizationContract v0` — the transport-only, schema-bound feature graph the handler consumes. +3. CadQuery handler + four-part wall executed over v0, with all four negative controls. +4. STEP/3MF generation and conformance; bound slicer profile or refusal. +5. Per-printer manifests for node 1 and node 2; measurement/admission form ready for results. + +**Deferred as definition-only residue until each has a consumer:** `CONTRACT` (needs the generator), +`DeploymentEnvelope` (needs the layout-comparison consumer). The design of both is pinned above. + +## On arrival (2026-09-03) + +``` +printer setup and identity observation + -> same MachineProcessCoupon on each printer + -> measure without silently averaging contradictions + -> admit or refuse each process identity independently + -> derive qualified FIT clearances + -> generate adjustable FIT fixture + -> mount the real board unpowered +``` + +The duplicate-measurement repair already has the right semantics for this: lookup refuses +contradiction. A future adjudication relation may supersede a measurement, but selection must never +be smuggled into ordinary resolution. + + +## The floor-budget cluster, and why this program did not take the coverage loss + +Adding this program's witnesses tipped a rotating subset of ten whole-corpus-reflection claims past +the floor's 500ms per-claim ceiling — claims that already sat at 415-436ms on main and were already +`[over-cost]` flagged. Two runs tipped DISJOINT subsets, so there was never a single slow witness to +chase. + +The interim move was to lift those ten off the required floor into `test.claim.long.`, declared as a +§4b(3) rung drop. That was reverted before it was pushed, and the reason is worth keeping: a child +lane investigating the cause found `deduplicate_identities` building a COPIED ACCUMULATOR inside a +quadratic fold, over a population that is the corpus — roughly 16s of the 19s that one reflection +costs. Rewritten as a set-membership fold it drops the standing to ~4.8s. + +So the ceiling was never the problem and the ten witnesses were never really the subject. Taking +them off the floor would have spent ten executing checks — including the one that EXECUTES the +compile-phase ratchet — to work around a cost-shape defect that §6 says is always fixed regardless of +realized n. The fix lands on main ahead of this program, and this program takes no drop. + +The transferable rule: when a budget refusal names your change as the trigger, the trigger and the +cause are different questions. A rotating victim set is the tell that you have found neither. + +## Grounding — R14, and why it is TWO networks rather than one path + +**Corrected.** An earlier revision of this section said the earth connection is "part of the docking +interface" and that the earth path runs through the standoffs. That is wrong, and wrong in the +dangerous direction: it makes the safety path depend on a mechanism whose whole purpose is to be +disconnected by hand, routinely, by design. The requirement below replaces it. + +There are two networks. They serve different purposes, they have different failure consequences, and +conflating them is what produced the earlier error. + +**1. Protective earth (PE) — a safety network, and never load-bearing on anything removable.** +From the AC inlet's earth pin, through the PSU's own vendor enclosure, to a dedicated bonding point +on the rack's metal member, and from there to every accessible conductive part. It is bolted, not +docked. The witness is stated as three simultaneous conditions, because any one of them alone is a +state the rack will really be in: + +> PE continuity holds with the motherboard removed, AND with every motherboard standoff removed, AND +> with the removable cassette undocked. + +If pulling a node can open the earth network, the design is wrong regardless of how good the contact +is when it is seated. + +**2. Board-to-chassis bond — a functional network, for EMI and reference, not for safety.** +Board mounting hole → metal standoff → cassette metal reference. This one legitimately breaks when +the board is removed, because that is what it is for. It may be a return and reference path; it may +never be the reason a chassis surface is safe to touch. + +The consequences for the build: + +- **Metal standoffs into a metal member.** The hybrid load path already buys aluminium extrusion or + threaded rod — that member is the natural bonding conductor and is present for structural reasons + anyway. It serves network 2, and is a *bonded branch of* network 1, not a segment of it. +- **Printed polymer is never a conductor in either network, never the mains enclosure, and never the + sole earth path.** The PSU stays in its vendor enclosure. +- **The docking interface carries no PE obligation.** A dock is a connector; PE is a bolt. + +The obligation this creates for MEASURE: the PSU's earth-stud or bonding-screw location, the rack +member's bonding point, and the standoff material and thread. None is measured yet. + +The witness set, written now so the design is falsifiable before anything is printed: + +| # | Condition | Required outcome | +|---|---|---| +| G1 | Motherboard absent | All accessible rack metal remains PE-bonded | +| G2 | Every motherboard standoff absent | PE continuity holds | +| G3 | One cassette extracted | PE continuity holds for the remaining rack | +| G4 | Board-hole bonding unknown | **No** board-to-chassis bond is claimed | +| G5 | Any printed polymer segment | Never carries PE continuity | + +G4 is the one that is easy to skip: not knowing whether a mounting hole is bonded to board ground is +a reason to make no claim, not a reason to assume the convenient answer. A dedicated bonding stud, +conductor, terminal and tested connection are part of the rack design. Incidental contact through +rails or mounting screws is never the bond. + +### The witnesses above are not sufficient, and the gap is a sequencing one + +G1-G3 prove that the REMAINING rack stays bonded after something is removed. They say nothing about +whether the thing that was removed was correctly bonded while it was powered — a cassette can be +live, unbonded, and still leave a perfectly continuous rack behind it. Two ordering relations close +that, and both are about the service protocol rather than about geometry: + +- **Power admission requires the bond.** `NodePowerAdmitted -> EveryRequiredAccessibleMetalPartPeBonded`. + A node may not be energised unless every accessible conductive part it brings is already bonded. +- **Bond removal requires the power to be gone.** `PeBondMayBeRemoved -> AcDisconnected AND HazardousEnergyAbsent`. + The earth connection is the last thing disconnected and the first thing connected. + +This is why the bond is a captive bolt in the connect/disconnect sequence even though the docking +interface carries no PE obligation. "A dock is a connector, PE is a bolt" settles what the MECHANISM +is; it does not settle WHEN the bolt is made and broken, and the second question is the one that +decides whether a person servicing a live rack is safe. + +### Front-edge support — admitted only under all five conjuncts + +The 29.21 mm of board hanging past the last mounting row is a cassette input, not a description. A +support there is a *candidate*, and it is admitted only when all of the following hold, because each +one of them independently turns a helpful support into a defect: + +1. The underside keep-out at the contact region is known. +2. The contact region is non-conductive. +3. The support does not obstruct the extraction path (R-middle-node-removal). +4. The support actually reacts connector insertion load — otherwise it is decoration. +5. The support does not become an **unintended electrical bond**, which is where this requirement + meets the grounding correction above: a support that quietly bonds the board underside to the + cassette creates a path nobody modelled and nobody tests. + +## Cable routing — R12, at every layer + +Every run gets endpoints, an access envelope, a minimum bend and service allowance, fixed clip +positions, strain relief, a moving-versus-fixed segment classification, and declared separation from +fan blades and hot surfaces. The service witness stays structural: after disconnecting the declared +external bundle and releasing the latch, the extraction path is collision-free and no neighbouring +cable or node has to move. + +**PST changes the fan harness.** The ARCTIC P8 PWM PST carries a 4-pin connector AND a 4-pin socket, +so fans daisy-chain and fan count is decoupled from the board's five headers. That is a cardinality +fact only: a chain still owes admission against header continuous and startup current, connector and +wire rating, maximum chain length, failure isolation, and tach semantics. At the published 0.09 A a +three-fan chain draws 0.27 A and a five-fan chain 0.45 A steady — neither figure proves a chain safe, +because the header rating and startup behaviour are unmeasured. Do not assume every chained fan is +independently observable just because a downstream socket exists; tach forwarding needs manufacturer +authority or an executed electrical observation.