From 1b5e5a615cfe264500c9b2325de677e55db83f78 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 13 Aug 2026 04:06:06 +0000 Subject: [PATCH 1/2] Read a 2D extent in the frame's unit rather than asserting millimetres MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The declared residue from the previous slice, narrowed to what it actually was. The geometry carriers are scale-agnostic — a rectangle holds signed components and never commits to what they measure — so the millimetre commitment lived entirely in the READERS, which were right only because every frame in the corpus happened to be a millimetre frame. segment2_length, rectangle2_width and rectangle2_height are now segment2_extent / rectangle2_width / rectangle2_height returning FrameExtent, read in the unit the shape's own frame was registered with. An unregistered frame refuses; it does not fall back to millimetres, which would answer a plausible number for a real question. The millimetre answer is still available and is now DERIVED through frame_length_as_millimeter, which refuses when the frame is not a millimetre frame instead of truncating into one. The old readers are deleted rather than kept beside the new ones: a reader that asserts a unit and a reader that derives it are two answers to one question, and the asserting one is the one that was wrong. Blast radius was one file. Only the geometry witness consumed these three, and its existing assertions pass unchanged once the two frames it draws in are registered as millimetre frames — which is the fact they always relied on and never stated. Two new tests are the ones that discriminate, since the migrated assertions pass in both worlds: the same rectangle carrier in a micrometre-registered board frame is a 20 mm package body that the old reader would have called 20000 millimetres, a twenty-metre chip; and an unregistered frame refuses to be measured at all. Residue, still declared: prism3_height and the SquareMillimeter / CubicMillimeter surface across orthogonal_topology continue to assert. The 2D surface is what a board footprint needs and is what moved here. Co-Authored-By: Claude Opus 5 (1M context) --- dag/std/orthogonal_geometry.dag | 31 ++++- dag/std/spatial_frame.dag | 21 ++++ .../orthogonal_geometry_witness_test.dag | 106 +++++++++++++++++- 3 files changed, 147 insertions(+), 11 deletions(-) diff --git a/dag/std/orthogonal_geometry.dag b/dag/std/orthogonal_geometry.dag index 8f2cc56b953..bf03def0690 100644 --- a/dag/std/orthogonal_geometry.dag +++ b/dag/std/orthogonal_geometry.dag @@ -6,6 +6,7 @@ import std.nat { Nat } import std.measure { Millimeter, millimeter, SignedMillimeterComponent, signed_millimeter_component, signed_millimeter_component_count } import std.checked_arithmetic { IntegerOverflow } import std.coordinate_frame { CoordinateFrameIdentity, coordinate_frame_identity_eq } +import std.spatial_frame { FrameExtent, SpatialFrameRegistry, extent_in_frame } import std.affine_space { Point2, Point3, point2, point3 } import std.euclidean_geometry { AxisDirection3, PositiveX, NegativeX, PositiveY, NegativeY, PositiveZ, NegativeZ, @@ -177,11 +178,21 @@ fn segment2_frame(s: AxisAlignedSegment2) -> CoordinateFrameIdentity { s.frame } // Length is exact and nonnegative: one coordinate difference, magnitude taken. No root is involved // precisely because the segment is axis-aligned, which is the property the carrier guarantees. -fn segment2_length(s: AxisAlignedSegment2) -> Millimeter { +// +// THE UNIT IS THE FRAME'S, NOT THIS FUNCTION'S. An earlier revision returned Millimeter, which was +// true only because every frame the layer had been asked to hold was a millimetre frame. It is the +// reader that committed, never the carrier: a segment holds signed components and does not know +// what they measure. Handed a board frame the old reader answered a whole-millimetre count of a +// micrometre extent — 0 for a 500 um pitch — so the shape did not lose accuracy, it lost the +// distinction between two adjacent pins. The extent is now read in the frame's registered unit and +// an unregistered frame refuses rather than defaulting. The millimetre answer is still available +// and is now DERIVED: frame_length_as_millimeter over this, which refuses when the frame is not a +// millimetre frame instead of truncating into one. +fn segment2_extent(registry: SpatialFrameRegistry, s: AxisAlignedSegment2) -> FrameExtent { let dx = signed_millimeter_component_count(m: s.end.x) - signed_millimeter_component_count(m: s.start.x) let dy = signed_millimeter_component_count(m: s.end.y) - signed_millimeter_component_count(m: s.start.y) let d = dx + dy - millimeter(count: if d < 0 { 0 - d } else { d }) + extent_in_frame(registry: registry, identity: s.frame, count: if d < 0 { 0 - d } else { d }) } // AN AXIS-ALIGNED RECTANGLE, held as its two extreme corners rather than as an origin plus a width @@ -215,12 +226,20 @@ fn rectangle2_min(r: AxisAlignedRectangle2) -> Point2 { r.min } fn rectangle2_max(r: AxisAlignedRectangle2) -> Point2 { r.max } fn rectangle2_frame(r: AxisAlignedRectangle2) -> CoordinateFrameIdentity { r.frame } -fn rectangle2_width(r: AxisAlignedRectangle2) -> Millimeter { - millimeter(count: signed_millimeter_component_count(m: r.max.x) - signed_millimeter_component_count(m: r.min.x)) +fn rectangle2_width(registry: SpatialFrameRegistry, r: AxisAlignedRectangle2) -> FrameExtent { + extent_in_frame( + registry: registry, + identity: r.frame, + count: signed_millimeter_component_count(m: r.max.x) - signed_millimeter_component_count(m: r.min.x) + ) } -fn rectangle2_height(r: AxisAlignedRectangle2) -> Millimeter { - millimeter(count: signed_millimeter_component_count(m: r.max.y) - signed_millimeter_component_count(m: r.min.y)) +fn rectangle2_height(registry: SpatialFrameRegistry, r: AxisAlignedRectangle2) -> FrameExtent { + extent_in_frame( + registry: registry, + identity: r.frame, + count: signed_millimeter_component_count(m: r.max.y) - signed_millimeter_component_count(m: r.min.y) + ) } // AN AXIS-PERPENDICULAR PLANE, named by the axis it is perpendicular TO and the coordinate at which diff --git a/dag/std/spatial_frame.dag b/dag/std/spatial_frame.dag index 5a754baab71..029e027e242 100644 --- a/dag/std/spatial_frame.dag +++ b/dag/std/spatial_frame.dag @@ -163,3 +163,24 @@ fn frame_length_as_micrometer(l: FrameLength) -> LengthProjection { LengthProjectionRefused { cause: LengthScaleMismatch { held: l.scale, requested: Micro } } } } + +// READING AN EXTENT OUT OF A SHAPE, IN THE UNIT THE SHAPE'S OWN FRAME WAS REGISTERED WITH. This +// is the join the geometry layer was missing. Its shape carriers are scale-AGNOSTIC — a rectangle +// holds signed components and never commits to what they measure — so the commitment lived +// entirely in the readers, which named millimetres and were right only because every frame in the +// corpus happened to be a millimetre frame. A board is the counterexample, and the repair is to +// derive the unit from the frame rather than to assert it. +// +// UNREGISTERED REFUSES, and it matters more here than at the lookup: a reader that fell back to +// millimetres would answer 20 for a package body that is 20000 micrometres across, which is a +// plausible number for a real question and would be believed. +type FrameExtent + = ExtentInFrame { length: FrameLength } + | ExtentFrameUnregistered { identity: CoordinateFrameIdentity } + +fn extent_in_frame(registry: SpatialFrameRegistry, identity: CoordinateFrameIdentity, count: Nat) -> FrameExtent { + match frame_length_scale(r: registry, identity: identity) { + Absent => ExtentFrameUnregistered { identity: identity } + Present { value: s } => ExtentInFrame { length: frame_length(scale: s, count: count) } + } +} diff --git a/dag/test/claim/orthogonal_geometry_witness_test.dag b/dag/test/claim/orthogonal_geometry_witness_test.dag index bcdbc85d2ca..387a86c0fc3 100644 --- a/dag/test/claim/orthogonal_geometry_witness_test.dag +++ b/dag/test/claim/orthogonal_geometry_witness_test.dag @@ -3,6 +3,22 @@ module test.claim.orthogonal_geometry_witness import std.types { Bool, Int, List } import std.measure { millimeter_count, signed_millimeter_component_count } import std.coordinate_frame { CoordinateFrameIdentity, coordinate_frame_identity, coordinate_frame_identity_eq } +import std.measure { Micro, Milli } +import std.nat { Nat } +import std.spatial_frame { + ExtentFrameUnregistered, + ExtentInFrame, + FrameExtent, + FrameRegistered, + FrameRegistrationRefused, + LengthProjected, + LengthProjectionRefused, + SpatialFrameRegistry, + empty_frame_registry, + frame_length_as_millimeter, + register_frame, + registry_with, +} import std.affine_space { Point2, Point3, point2, point3 } import std.euclidean_geometry { AxisDirection3, PositiveX, NegativeX, PositiveY, NegativeY, PositiveZ, NegativeZ, @@ -16,7 +32,7 @@ import std.orthogonal_geometry { LoopEdgesNotPerpendicular, LoopSelfIntersects, RotationAxesParallel, BoundingBoxHasNoPoints, OrthogonalRotation3, orthogonal_rotation3, rotation_x_image, rotation_y_image, rotation_z_image, - AxisAlignedSegment2, axis_aligned_segment2, segment2_axis, segment2_length, + AxisAlignedSegment2, axis_aligned_segment2, segment2_axis, segment2_extent, AxisAlignedRectangle2, axis_aligned_rectangle2, rectangle2_width, rectangle2_height, Plane3, plane3, plane3_contains_point, plane3_normal_axis, AxisAlignedBox3, axis_aligned_box3, box3_contains_point, box3_overlaps, @@ -33,6 +49,35 @@ fn room() -> CoordinateFrameIdentity { coordinate_frame_identity(occurrence: 1) fn building() -> CoordinateFrameIdentity { coordinate_frame_identity(occurrence: 2) } fn p2(x: Int, y: Int) -> Point2 { point2(frame: room(), x: x, y: y) } + +// Both frames these tests draw in are millimetre frames, which is exactly the fact the readers +// used to assume and now have to be told. Registering them is what keeps every length assertion +// below meaning what it always meant. +fn mm_registry() -> SpatialFrameRegistry { + let r0 = empty_frame_registry() + let r1 = match register_frame(r: r0, identity: room(), length_scale: Milli) { + FrameRegistered { frame: f } => registry_with(r: r0, f: f) + FrameRegistrationRefused { cause: _ } => r0 + } + match register_frame(r: r1, identity: building(), length_scale: Milli) { + FrameRegistered { frame: f } => registry_with(r: r1, f: f) + FrameRegistrationRefused { cause: _ } => r1 + } +} + +// An extent measures a stated number of millimetres. Every arm other than the one that projects +// answers false, so an unregistered frame or a non-millimetre frame fails the assertion rather +// than being quietly read as a count. +fn extent_is_mm(e: FrameExtent, want: Nat) -> Bool { + match e { + ExtentFrameUnregistered { identity: _ } => false + ExtentInFrame { length: l } => + match frame_length_as_millimeter(l: l) { + LengthProjectionRefused { cause: _ } => false + LengthProjected { value: v } => millimeter_count(m: v) == want + } + } +} fn p3(x: Int, y: Int, z: Int) -> Point3 { point3(frame: room(), x: x, y: y, z: z) } // EVERY NEGATIVE CONTROL BELOW HAS A POSITIVE SIBLING IN THE SAME WITNESS. A mint that refused @@ -75,11 +120,11 @@ test fn segment_walls_hold() -> Bool { let axis_aligned = match axis_aligned_segment2(start: p2(x: 0, y: 0), end: p2(x: 3000, y: 0)) { OrthogonalReady { value: s } => match segment2_axis(s: s) { Axis2X => true Axis2Y => false } - && millimeter_count(m: segment2_length(s: s)) == 3000 + && extent_is_mm(e: segment2_extent(registry: mm_registry(), s: s), want: 3000) OrthogonalRefused { cause: _ } => false } let negative_direction_still_positive_length = match axis_aligned_segment2(start: p2(x: 0, y: 500), end: p2(x: 0, y: 0 - 500)) { - OrthogonalReady { value: s } => millimeter_count(m: segment2_length(s: s)) == 1000 + OrthogonalReady { value: s } => extent_is_mm(e: segment2_extent(registry: mm_registry(), s: s), want: 1000) OrthogonalRefused { cause: _ } => false } let degenerate = match axis_aligned_segment2(start: p2(x: 7, y: 7), end: p2(x: 7, y: 7)) { @@ -117,7 +162,7 @@ test fn box_and_rectangle_walls_hold() -> Bool { let flat_z = refusal_is_extent_not_positive(r: axis_aligned_box3(min: p3(x: 0, y: 0, z: 0), max: p3(x: 4000, y: 3000, z: 0)), axis: Axis3Z) let inverted = refusal_is_extent_not_positive(r: axis_aligned_box3(min: p3(x: 0, y: 0, z: 0), max: p3(x: 0 - 10, y: 3000, z: 2400)), axis: Axis3X) let good_rect = match axis_aligned_rectangle2(min: p2(x: 0, y: 0), max: p2(x: 1200, y: 800)) { - OrthogonalReady { value: r } => millimeter_count(m: rectangle2_width(r: r)) == 1200 && millimeter_count(m: rectangle2_height(r: r)) == 800 + OrthogonalReady { value: r } => extent_is_mm(e: rectangle2_width(registry: mm_registry(), r: r), want: 1200) && extent_is_mm(e: rectangle2_height(registry: mm_registry(), r: r), want: 800) OrthogonalRefused { cause: _ } => false } let thin_rect = match axis_aligned_rectangle2(min: p2(x: 0, y: 0), max: p2(x: 1200, y: 0)) { @@ -271,7 +316,7 @@ test fn plane_surface_and_prism_hold() -> Bool { let surface = match axis_aligned_rectangle2(min: p2(x: 0, y: 0), max: p2(x: 4000, y: 3000)) { OrthogonalRefused { cause: _ } => false OrthogonalReady { value: rect } => - millimeter_count(m: rectangle2_width(r: surface3_extent(s: axis_aligned_surface3(offset: 0, extent: rect)))) == 4000 + extent_is_mm(e: rectangle2_width(registry: mm_registry(), r: surface3_extent(s: axis_aligned_surface3(offset: 0, extent: rect))), want: 4000) } let surface_plane_is_derived = match axis_aligned_rectangle2(min: point2(frame: building(), x: 0, y: 0), max: point2(frame: building(), x: 10, y: 10)) { OrthogonalRefused { cause: _ } => false @@ -299,3 +344,54 @@ test fn plane_surface_and_prism_hold() -> Bool { } on_plane && off_plane && other_frame_not_on_plane && surface && surface_plane_is_derived && prism && flat_prism } + +// THE CASE THE OLD READER ANSWERED WRONGLY, and the reason this reader takes a registry at all. +// The board frame is registered in micrometres. The SAME rectangle carrier, holding the same +// components, is a 20000 um package body — 20 mm — and the old reader would have called it 20000 +// millimetres, a twenty-metre chip. Nothing about the carrier changed; the reader stopped +// asserting a unit it was never told. +// +// Read as micrometres it answers. Read as millimetres it REFUSES rather than dividing, because +// this reader is not a converter: the caller asked what the shape measures, not for a change of +// unit, and a 500 um pitch has no whole-millimetre answer at all. +fn board() -> CoordinateFrameIdentity { coordinate_frame_identity(occurrence: 77) } + +fn micro_registry() -> SpatialFrameRegistry { + let r0 = empty_frame_registry() + match register_frame(r: r0, identity: board(), length_scale: Micro) { + FrameRegistered { frame: f } => registry_with(r: r0, f: f) + FrameRegistrationRefused { cause: _ } => r0 + } +} + +test fn a_reader_takes_the_unit_from_the_frame_not_from_itself() -> Bool { + match axis_aligned_rectangle2( + min: point2(frame: board(), x: 0, y: 0), + max: point2(frame: board(), x: 20000, y: 20000) + ) { + OrthogonalRefused { cause: _ } => false + OrthogonalReady { value: rect } => + match rectangle2_width(registry: micro_registry(), r: rect) { + ExtentFrameUnregistered { identity: _ } => false + ExtentInFrame { length: l } => + match frame_length_as_millimeter(l: l) { + LengthProjected { value: _ } => false + LengthProjectionRefused { cause: _ } => true + } + } + } +} + +// An unregistered frame has no unit, and a reader that fell back to millimetres would answer a +// plausible number for a real question. The registry above holds the board frame only. +test fn an_unregistered_frame_refuses_rather_than_measuring() -> Bool { + match axis_aligned_rectangle2(min: p2(x: 0, y: 0), max: p2(x: 1200, y: 800)) { + OrthogonalRefused { cause: _ } => false + OrthogonalReady { value: rect } => + match rectangle2_width(registry: micro_registry(), r: rect) { + ExtentInFrame { length: _ } => false + ExtentFrameUnregistered { identity: _ } => true + } + } +} + From 5902659f8df498fa7e8fb376a530fbb7d1e79e6f Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 13 Aug 2026 04:31:18 +0000 Subject: [PATCH 2/2] Assert the extent count, not only that the wrong unit refuses MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Review 51493, and the finding is correct by this file's own stated rule that every negative control has a positive sibling. The headline test for this slice asserted only that frame_length_as_millimeter refuses on a micrometre-registered board frame. Every wrong answer satisfies that: a reader returning 200 instead of 20000 would have passed, so the reader's actual deliverable — returning the extent in the frame's registered unit — was never witnessed. The refusal half was the easy half. The micrometre projection is now asserted first and by count, then the millimetre refusal. Verified by mutation rather than by reading: perturbing the expected 20000 to 200 turns the test red, and restoring it turns it green. Co-Authored-By: Claude Opus 5 (1M context) --- .../orthogonal_geometry_witness_test.dag | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/dag/test/claim/orthogonal_geometry_witness_test.dag b/dag/test/claim/orthogonal_geometry_witness_test.dag index 387a86c0fc3..f360dc62255 100644 --- a/dag/test/claim/orthogonal_geometry_witness_test.dag +++ b/dag/test/claim/orthogonal_geometry_witness_test.dag @@ -1,7 +1,7 @@ module test.claim.orthogonal_geometry_witness import std.types { Bool, Int, List } -import std.measure { millimeter_count, signed_millimeter_component_count } +import std.measure { millimeter_count, signed_millimeter_component_count, measure_count } import std.coordinate_frame { CoordinateFrameIdentity, coordinate_frame_identity, coordinate_frame_identity_eq } import std.measure { Micro, Milli } import std.nat { Nat } @@ -15,6 +15,7 @@ import std.spatial_frame { LengthProjectionRefused, SpatialFrameRegistry, empty_frame_registry, + frame_length_as_micrometer, frame_length_as_millimeter, register_frame, registry_with, @@ -374,9 +375,19 @@ test fn a_reader_takes_the_unit_from_the_frame_not_from_itself() -> Bool { match rectangle2_width(registry: micro_registry(), r: rect) { ExtentFrameUnregistered { identity: _ } => false ExtentInFrame { length: l } => - match frame_length_as_millimeter(l: l) { - LengthProjected { value: _ } => false - LengthProjectionRefused { cause: _ } => true + // BOTH HALVES, AND THE FIRST IS THE DELIVERABLE. An earlier revision of this test + // asserted only that the millimetre projection refuses, which every wrong answer also + // satisfies: a reader returning 200 instead of 20000 would have passed it, and the + // reader's actual job — returning the extent in the frame's registered unit — went + // unwitnessed. The count is asserted first, then the refusal. + match frame_length_as_micrometer(l: l) { + LengthProjectionRefused { cause: _ } => false + LengthProjected { value: um } => + measure_count(m: um) == 20000 + && match frame_length_as_millimeter(l: l) { + LengthProjected { value: _ } => false + LengthProjectionRefused { cause: _ } => true + } } } }