From d570507414429a3ace33a34186c58cce194f3999 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 11 Aug 2026 21:06:32 +0000 Subject: [PATCH 1/2] SPATIAL-2b: carried coordinate-frame identity and operational frame refusal #8091 claimed that a phantom frame parameter made cross-frame subtraction fail to typecheck, and called that the stronger of the two available options. Measured on the production compile-and-run path 2026-08-11, that program compiles clean and returns 9 -- a plausible number for a question with no answer, which is the fabricated output DESIGN 5 forbids. The cause is a v1 seed limitation, not a modelling slip: the argument-position judge compares nominal HEAD NAMES, and applied type arguments live in the type node's children where every name-level comparison discards them. Point3 matched Point3, so the frames were never compared. A separate compiler PR closes the call boundary; it cannot close the producer side, because return-position conformance declines to judge record types at all pending feature:conformance-produced-type-identity. So the carried identity is the authority and the honest claim is frame consistency BY CHECKED DERIVATION, not by construction: - std.coordinate_frame mints CoordinateFrameIdentity, declaration-owned and never derived from a name or from contents (the HostResourceIdentity precedent). Recorded as the third minted-occurrence carrier in the corpus, which is evidence the subject-parameterized extraction is due -- left as a trigger rather than built here. - Phantom is removed rather than demoted. Two authorities for one fact is the DESIGN 3 violation whichever is right, and the weaker one is the one the compiler cannot enforce end to end. - SpatialResult carries three arms: ready, arithmetic refusal, frame refusal. One coproduct rather than nested result types -- there is one question at the operation boundary and the causes are what differ. - The refusal names ROLES, not expected/observed: for a symmetric operation neither frame is normatively expected, so an operation identity and the required relation replace a report of argument order. - The frame check precedes the arithmetic everywhere, because operands in different frames pose no question to overflow. Green by execution, with discriminating controls: cross-frame subtraction, addition, subtraction, translation and transform application each refuse and name both frames; same-frame operations still answer (the positive sibling a refusal-only control cannot see); frame and overflow are asserted distinct in both directions; a transform's translation must be in its destination frame. The decisive one is the lying-producer control: a function handing back a room-frame value under a building-frame annotation cannot rewrite the carried frame, and the next operation refuses. Mutation-tested -- disabling a single frame guard reds the suite. Co-Authored-By: Claude Opus 5 (1M context) --- dag/std/affine_space.dag | 334 +++++++++++------ dag/std/coordinate_frame.dag | 68 ++++ dag/std/euclidean_geometry.dag | 88 +++-- dag/std/measure.dag | 4 +- dag/test/claim/affine_space_witness_test.dag | 362 ++++++++++++++----- 5 files changed, 622 insertions(+), 234 deletions(-) create mode 100644 dag/std/coordinate_frame.dag diff --git a/dag/std/affine_space.dag b/dag/std/affine_space.dag index 77dd7639d92..9dd9fb0a099 100644 --- a/dag/std/affine_space.dag +++ b/dag/std/affine_space.dag @@ -16,6 +16,7 @@ import std.measure { signed_millimeter_component, signed_millimeter_component_count, } +import std.coordinate_frame { CoordinateFrameIdentity, coordinate_frame_identity_eq } // SPATIAL-2: the affine layer. It exists because "can a measurement be negative" was the wrong // question. A length is never negative; a COORDINATE and a DISPLACEMENT are, and they are negative @@ -37,11 +38,19 @@ import std.measure { // are distinct types, an attempt to add two points does not typecheck. This mirrors the affine / // cardinal split product.placement_supply already draws between a rack POSITION and a rack HEIGHT. // -// FRAMES RIDE IN THE TYPE. Point3 carries its coordinate frame as a phantom parameter - the -// same shape std.measure already uses, where Measure holds only a count and carries its -// quantity and scale phantom. So subtracting a room-local point from a building-global point is -// not a refusal to be checked at runtime; it does not typecheck. That is the stronger of the two -// options, and it is available here rather than merely preferable. +// FRAMES ARE CARRIED BY THE VALUE, NOT BY THE TYPE - and the previous revision of this paragraph +// claimed the opposite, so the correction is recorded rather than quietly swapped. It read: a point +// carries its frame as a phantom parameter, so subtracting a room-local point from a building-global +// point "does not typecheck ... the stronger of the two options". Measured on the production +// compile-and-run path 2026-08-11: that program compiles clean and returns 9. The v1 seed's +// argument-position judge compares nominal head names and discards applied type arguments, so +// Point3 matched Point3 and the frames were never looked at. +// +// The seam is now `frame: CoordinateFrameIdentity` on every point and vector, and every operation +// below compares the identities its operands actually carry. std.coordinate_frame holds the full +// account, including why the compiler repair that landed with it closes the call boundary but not +// the producer side. The claim this layer supports is frame consistency BY CHECKED DERIVATION. +// It is NOT true that cross-frame programs are unwritable. // // FRAMES ARE RIGHT-HANDED ORTHOGONAL CARTESIAN, and that is a property of this slice rather than a // runtime choice. An earlier revision declared Handedness = RightHanded | LeftHanded on a @@ -52,75 +61,111 @@ import std.measure { // consumer needs one, and frame metadata - display identity, a human-facing origin description - // lands with the spatial-world carrier that actually registers frames. -type Vector3 { +type Vector3 { + frame: CoordinateFrameIdentity x: SignedMillimeterComponent y: SignedMillimeterComponent z: SignedMillimeterComponent } -type Point3 { +type Point3 { + frame: CoordinateFrameIdentity x: SignedMillimeterComponent y: SignedMillimeterComponent z: SignedMillimeterComponent } -type Vector2 { +type Vector2 { + frame: CoordinateFrameIdentity x: SignedMillimeterComponent y: SignedMillimeterComponent } -type Point2 { +type Point2 { + frame: CoordinateFrameIdentity x: SignedMillimeterComponent y: SignedMillimeterComponent } -fn vector3(x: Int, y: Int, z: Int) -> Vector3 { +fn vector3(frame: CoordinateFrameIdentity, x: Int, y: Int, z: Int) -> Vector3 { Vector3 { + frame: frame, x: signed_millimeter_component(count: x), y: signed_millimeter_component(count: y), z: signed_millimeter_component(count: z), } } -fn point3(x: Int, y: Int, z: Int) -> Point3 { +fn point3(frame: CoordinateFrameIdentity, x: Int, y: Int, z: Int) -> Point3 { Point3 { + frame: frame, x: signed_millimeter_component(count: x), y: signed_millimeter_component(count: y), z: signed_millimeter_component(count: z), } } -fn vector2(x: Int, y: Int) -> Vector2 { - Vector2 { x: signed_millimeter_component(count: x), y: signed_millimeter_component(count: y) } +fn vector2(frame: CoordinateFrameIdentity, x: Int, y: Int) -> Vector2 { + Vector2 { frame: frame, x: signed_millimeter_component(count: x), y: signed_millimeter_component(count: y) } } -fn point2(x: Int, y: Int) -> Point2 { - Point2 { x: signed_millimeter_component(count: x), y: signed_millimeter_component(count: y) } +fn point2(frame: CoordinateFrameIdentity, x: Int, y: Int) -> Point2 { + Point2 { frame: frame, x: signed_millimeter_component(count: x), y: signed_millimeter_component(count: y) } } -fn zero_vector3() -> Vector3 { - vector3(x: 0, y: 0, z: 0) +fn zero_vector3(frame: CoordinateFrameIdentity) -> Vector3 { + vector3(frame: frame, x: 0, y: 0, z: 0) } -// THE MATHEMATICS IS EXACT; THE FINITE MACHINE REALIZATION MAY REFUSE. Those are two statements and -// this slice used to make only the first. Translation of a point by a displacement is exact in -// integer millimetres - no approximation policy is needed to move a location - and the model's Int -// is unbounded. The realization's is not: every one of these operations runs on i64 in the seed and -// in emitted Rust, where a sum of two large coordinates has no representable result. Declaring the -// operation total while running it on a bounded carrier is the overclaim, not the arithmetic. +// THE MATHEMATICS IS EXACT; THE FINITE MACHINE REALIZATION MAY REFUSE, AND THE OPERANDS MAY NOT +// BELONG TOGETHER. Those are two independent ways one operation has no answer, and they are separate +// arms rather than one "failed" arm because the remedies differ absolutely: an overflow means the +// question was right and the carrier too small, a frame mismatch means the question was meaningless. +// Collapsing them would be the state-space conflation DESIGN 5 names. // -// So each operation answers SpatialArithmeticResult, and the refusal carries the exact -// IntegerOverflow cause std.checked_arithmetic produced: which operation, on which operands. A -// caller that cannot proceed knows precisely what could not be computed, and no caller receives a -// wrapped number described as a location. -type SpatialArithmeticResult - = SpatialArithmeticReady { value: T } +// ONE RESULT TYPE, NOT TWO NESTED ONES. An earlier sketch of this repair proposed a separate +// FrameRelationResult wrapping the arithmetic result. That forks the "this operation may have no +// answer" concept in two and forces every caller to unwrap twice for a question that is one +// question; the causes are what differ, and a coproduct is exactly the carrier for that (DESIGN 2). +// THE REFUSAL NAMES ROLES, NOT AN "EXPECTED" AND AN "OBSERVED". An earlier cut of this carrier had +// exactly those two fields, and they are misleading for a SYMMETRIC operation: in add_vector3(a, b) +// neither frame is normatively expected - the first operand merely happens to establish the result's +// frame, so calling it "expected" reports an artefact of argument order as though it were a +// requirement. The operation identity and the relation that was required make the refusal readable +// without knowing which operand the implementation looked at first. +type SpatialOperationIdentity + = OpTranslatePoint3 + | OpDisplacementBetween3 + | OpAddVector3 + | OpSubtractVector3 + | OpTranslatePoint2 + | OpDisplacementBetween2 + | OpAddVector2 + | OpDot3 + | OpCross3 + | OpApplyZQuarterTurnTransform3 + +type SpatialFrameRelation + = SameFrameOperandsRequired + | TransformSourceFrameRequired + | TransformTranslationInDestinationRequired + +type SpatialFrameRefusal { + operation: SpatialOperationIdentity + left_frame: CoordinateFrameIdentity + right_frame: CoordinateFrameIdentity + relation: SpatialFrameRelation +} + +type SpatialResult + = SpatialReady { value: T } | SpatialArithmeticRefused { cause: IntegerOverflow } + | SpatialFrameRefused { refusal: SpatialFrameRefusal } // FIRST CROSSING WINS, and every component is computed before the fold rather than after a partial // result exists. There is no arm here that produces a value from some components and a default for // the rest: a vector with one unrepresentable component is not a vector. -fn vector3_from_checked(x: CheckedInt, y: CheckedInt, z: CheckedInt) -> SpatialArithmeticResult> { +fn vector3_from_checked(frame: CoordinateFrameIdentity, x: CheckedInt, y: CheckedInt, z: CheckedInt) -> SpatialResult { match x { CheckedIntOverflow { cause: c } => SpatialArithmeticRefused { cause: c } CheckedIntReady { value: xv } => @@ -130,13 +175,13 @@ fn vector3_from_checked(x: CheckedInt, y: CheckedInt, z: CheckedInt) -> Spati match z { CheckedIntOverflow { cause: c } => SpatialArithmeticRefused { cause: c } CheckedIntReady { value: zv } => - SpatialArithmeticReady { value: vector3(x: xv, y: yv, z: zv) } + SpatialReady { value: vector3(frame: frame, x: xv, y: yv, z: zv) } } } } } -fn point3_from_checked(x: CheckedInt, y: CheckedInt, z: CheckedInt) -> SpatialArithmeticResult> { +fn point3_from_checked(frame: CoordinateFrameIdentity, x: CheckedInt, y: CheckedInt, z: CheckedInt) -> SpatialResult { match x { CheckedIntOverflow { cause: c } => SpatialArithmeticRefused { cause: c } CheckedIntReady { value: xv } => @@ -146,74 +191,107 @@ fn point3_from_checked(x: CheckedInt, y: CheckedInt, z: CheckedInt) -> Spatia match z { CheckedIntOverflow { cause: c } => SpatialArithmeticRefused { cause: c } CheckedIntReady { value: zv } => - SpatialArithmeticReady { value: point3(x: xv, y: yv, z: zv) } + SpatialReady { value: point3(frame: frame, x: xv, y: yv, z: zv) } } } } } -fn vector2_from_checked(x: CheckedInt, y: CheckedInt) -> SpatialArithmeticResult> { +fn vector2_from_checked(frame: CoordinateFrameIdentity, x: CheckedInt, y: CheckedInt) -> SpatialResult { match x { CheckedIntOverflow { cause: c } => SpatialArithmeticRefused { cause: c } CheckedIntReady { value: xv } => match y { CheckedIntOverflow { cause: c } => SpatialArithmeticRefused { cause: c } - CheckedIntReady { value: yv } => SpatialArithmeticReady { value: vector2(x: xv, y: yv) } + CheckedIntReady { value: yv } => SpatialReady { value: vector2(frame: frame, x: xv, y: yv) } } } } -fn point2_from_checked(x: CheckedInt, y: CheckedInt) -> SpatialArithmeticResult> { +fn point2_from_checked(frame: CoordinateFrameIdentity, x: CheckedInt, y: CheckedInt) -> SpatialResult { match x { CheckedIntOverflow { cause: c } => SpatialArithmeticRefused { cause: c } CheckedIntReady { value: xv } => match y { CheckedIntOverflow { cause: c } => SpatialArithmeticRefused { cause: c } - CheckedIntReady { value: yv } => SpatialArithmeticReady { value: point2(x: xv, y: yv) } + CheckedIntReady { value: yv } => SpatialReady { value: point2(frame: frame, x: xv, y: yv) } } } } -// Point + Vector -> Point. -fn translate_point3(point: Point3, by: Vector3) -> SpatialArithmeticResult> { - point3_from_checked( - x: checked_int_add(a: signed_millimeter_component_count(m: point.x), b: signed_millimeter_component_count(m: by.x)), - y: checked_int_add(a: signed_millimeter_component_count(m: point.y), b: signed_millimeter_component_count(m: by.y)), - z: checked_int_add(a: signed_millimeter_component_count(m: point.z), b: signed_millimeter_component_count(m: by.z)), - ) +// THE FRAME CHECK PRECEDES THE ARITHMETIC IN EVERY OPERATION BELOW, and the order is load-bearing +// rather than stylistic: if two operands are in different frames there is no question to overflow. +// Reporting an overflow for a meaningless subtraction would name the wrong cause, and reporting +// either one for both would be the conflation the result type exists to prevent. +// +// EXPECTED IS THE OPERAND THAT DEFINES THE RESULT'S FRAME - the point being translated, the origin +// of a displacement, the left operand of a composition, the transform's declared source. OBSERVED is +// the one that disagreed with it. A caller reading a refusal therefore learns which value was out of +// place, not merely that two frames differed. +fn translate_point3(point: Point3, by: Vector3) -> SpatialResult { + if !coordinate_frame_identity_eq(a: point.frame, b: by.frame) { + SpatialFrameRefused { refusal: SpatialFrameRefusal { operation: OpTranslatePoint3, left_frame: point.frame, right_frame: by.frame, relation: SameFrameOperandsRequired } } + } else { + point3_from_checked( + frame: point.frame, + x: checked_int_add(a: signed_millimeter_component_count(m: point.x), b: signed_millimeter_component_count(m: by.x)), + y: checked_int_add(a: signed_millimeter_component_count(m: point.y), b: signed_millimeter_component_count(m: by.y)), + z: checked_int_add(a: signed_millimeter_component_count(m: point.z), b: signed_millimeter_component_count(m: by.z)), + ) + } } // Point - Point -> Vector. The result is a displacement, not a location, and not a distance: it is // signed and directional. Its NORM is the nonnegative physical distance, and that lives in // std.euclidean_geometry because it is the operation that stops being exact. -fn displacement_between3(from: Point3, to: Point3) -> SpatialArithmeticResult> { - vector3_from_checked( - x: checked_int_subtract(a: signed_millimeter_component_count(m: to.x), b: signed_millimeter_component_count(m: from.x)), - y: checked_int_subtract(a: signed_millimeter_component_count(m: to.y), b: signed_millimeter_component_count(m: from.y)), - z: checked_int_subtract(a: signed_millimeter_component_count(m: to.z), b: signed_millimeter_component_count(m: from.z)), - ) +// +// THIS IS THE OPERATION THE MEASUREMENT CAUGHT. A RoomFrame origin and a BuildingFrame destination +// reached it and it answered 9. It now answers SpatialFrameRefused, and the witness that proves so +// is the regression control for the whole recut. +fn displacement_between3(from: Point3, to: Point3) -> SpatialResult { + if !coordinate_frame_identity_eq(a: from.frame, b: to.frame) { + SpatialFrameRefused { refusal: SpatialFrameRefusal { operation: OpDisplacementBetween3, left_frame: from.frame, right_frame: to.frame, relation: SameFrameOperandsRequired } } + } else { + vector3_from_checked( + frame: from.frame, + x: checked_int_subtract(a: signed_millimeter_component_count(m: to.x), b: signed_millimeter_component_count(m: from.x)), + y: checked_int_subtract(a: signed_millimeter_component_count(m: to.y), b: signed_millimeter_component_count(m: from.y)), + z: checked_int_subtract(a: signed_millimeter_component_count(m: to.z), b: signed_millimeter_component_count(m: from.z)), + ) + } } -fn add_vector3(a: Vector3, b: Vector3) -> SpatialArithmeticResult> { - vector3_from_checked( - x: checked_int_add(a: signed_millimeter_component_count(m: a.x), b: signed_millimeter_component_count(m: b.x)), - y: checked_int_add(a: signed_millimeter_component_count(m: a.y), b: signed_millimeter_component_count(m: b.y)), - z: checked_int_add(a: signed_millimeter_component_count(m: a.z), b: signed_millimeter_component_count(m: b.z)), - ) +fn add_vector3(a: Vector3, b: Vector3) -> SpatialResult { + if !coordinate_frame_identity_eq(a: a.frame, b: b.frame) { + SpatialFrameRefused { refusal: SpatialFrameRefusal { operation: OpAddVector3, left_frame: a.frame, right_frame: b.frame, relation: SameFrameOperandsRequired } } + } else { + vector3_from_checked( + frame: a.frame, + x: checked_int_add(a: signed_millimeter_component_count(m: a.x), b: signed_millimeter_component_count(m: b.x)), + y: checked_int_add(a: signed_millimeter_component_count(m: a.y), b: signed_millimeter_component_count(m: b.y)), + z: checked_int_add(a: signed_millimeter_component_count(m: a.z), b: signed_millimeter_component_count(m: b.z)), + ) + } } -fn subtract_vector3(a: Vector3, b: Vector3) -> SpatialArithmeticResult> { - vector3_from_checked( - x: checked_int_subtract(a: signed_millimeter_component_count(m: a.x), b: signed_millimeter_component_count(m: b.x)), - y: checked_int_subtract(a: signed_millimeter_component_count(m: a.y), b: signed_millimeter_component_count(m: b.y)), - z: checked_int_subtract(a: signed_millimeter_component_count(m: a.z), b: signed_millimeter_component_count(m: b.z)), - ) +fn subtract_vector3(a: Vector3, b: Vector3) -> SpatialResult { + if !coordinate_frame_identity_eq(a: a.frame, b: b.frame) { + SpatialFrameRefused { refusal: SpatialFrameRefusal { operation: OpSubtractVector3, left_frame: a.frame, right_frame: b.frame, relation: SameFrameOperandsRequired } } + } else { + vector3_from_checked( + frame: a.frame, + x: checked_int_subtract(a: signed_millimeter_component_count(m: a.x), b: signed_millimeter_component_count(m: b.x)), + y: checked_int_subtract(a: signed_millimeter_component_count(m: a.y), b: signed_millimeter_component_count(m: b.y)), + z: checked_int_subtract(a: signed_millimeter_component_count(m: a.z), b: signed_millimeter_component_count(m: b.z)), + ) + } } // Negation refuses at exactly one input per component - the minimum representable value, whose -// negation is the one integer two's complement omits. -fn negate_vector3(v: Vector3) -> SpatialArithmeticResult> { +// negation is the one integer two's complement omits. One operand, so no frame can disagree. +fn negate_vector3(v: Vector3) -> SpatialResult { vector3_from_checked( + frame: v.frame, x: checked_int_negate(a: signed_millimeter_component_count(m: v.x)), y: checked_int_negate(a: signed_millimeter_component_count(m: v.y)), z: checked_int_negate(a: signed_millimeter_component_count(m: v.z)), @@ -223,33 +301,49 @@ fn negate_vector3(v: Vector3) -> SpatialArithmeticResult> { // Scaling by an integer is exact. Scaling by a ratio is NOT offered: it would need a rounding // policy, and inventing one here would put approximation into the affine layer before the // numeric seam is decided. -fn scale_vector3(v: Vector3, factor: Int) -> SpatialArithmeticResult> { +fn scale_vector3(v: Vector3, factor: Int) -> SpatialResult { vector3_from_checked( + frame: v.frame, x: checked_int_multiply(a: signed_millimeter_component_count(m: v.x), b: factor), y: checked_int_multiply(a: signed_millimeter_component_count(m: v.y), b: factor), z: checked_int_multiply(a: signed_millimeter_component_count(m: v.z), b: factor), ) } -fn translate_point2(point: Point2, by: Vector2) -> SpatialArithmeticResult> { - point2_from_checked( - x: checked_int_add(a: signed_millimeter_component_count(m: point.x), b: signed_millimeter_component_count(m: by.x)), - y: checked_int_add(a: signed_millimeter_component_count(m: point.y), b: signed_millimeter_component_count(m: by.y)), - ) +fn translate_point2(point: Point2, by: Vector2) -> SpatialResult { + if !coordinate_frame_identity_eq(a: point.frame, b: by.frame) { + SpatialFrameRefused { refusal: SpatialFrameRefusal { operation: OpTranslatePoint2, left_frame: point.frame, right_frame: by.frame, relation: SameFrameOperandsRequired } } + } else { + point2_from_checked( + frame: point.frame, + x: checked_int_add(a: signed_millimeter_component_count(m: point.x), b: signed_millimeter_component_count(m: by.x)), + y: checked_int_add(a: signed_millimeter_component_count(m: point.y), b: signed_millimeter_component_count(m: by.y)), + ) + } } -fn displacement_between2(from: Point2, to: Point2) -> SpatialArithmeticResult> { - vector2_from_checked( - x: checked_int_subtract(a: signed_millimeter_component_count(m: to.x), b: signed_millimeter_component_count(m: from.x)), - y: checked_int_subtract(a: signed_millimeter_component_count(m: to.y), b: signed_millimeter_component_count(m: from.y)), - ) +fn displacement_between2(from: Point2, to: Point2) -> SpatialResult { + if !coordinate_frame_identity_eq(a: from.frame, b: to.frame) { + SpatialFrameRefused { refusal: SpatialFrameRefusal { operation: OpDisplacementBetween2, left_frame: from.frame, right_frame: to.frame, relation: SameFrameOperandsRequired } } + } else { + vector2_from_checked( + frame: from.frame, + x: checked_int_subtract(a: signed_millimeter_component_count(m: to.x), b: signed_millimeter_component_count(m: from.x)), + y: checked_int_subtract(a: signed_millimeter_component_count(m: to.y), b: signed_millimeter_component_count(m: from.y)), + ) + } } -fn add_vector2(a: Vector2, b: Vector2) -> SpatialArithmeticResult> { - vector2_from_checked( - x: checked_int_add(a: signed_millimeter_component_count(m: a.x), b: signed_millimeter_component_count(m: b.x)), - y: checked_int_add(a: signed_millimeter_component_count(m: a.y), b: signed_millimeter_component_count(m: b.y)), - ) +fn add_vector2(a: Vector2, b: Vector2) -> SpatialResult { + if !coordinate_frame_identity_eq(a: a.frame, b: b.frame) { + SpatialFrameRefused { refusal: SpatialFrameRefusal { operation: OpAddVector2, left_frame: a.frame, right_frame: b.frame, relation: SameFrameOperandsRequired } } + } else { + vector2_from_checked( + frame: a.frame, + x: checked_int_add(a: signed_millimeter_component_count(m: a.x), b: signed_millimeter_component_count(m: b.x)), + y: checked_int_add(a: signed_millimeter_component_count(m: a.y), b: signed_millimeter_component_count(m: b.y)), + ) + } } // QUARTER TURNS ONLY, and this is the numeric policy made structural rather than documented. @@ -264,28 +358,36 @@ type QuarterTurns | TwoQuarters | ThreeQuarters -// Rotation about +Z, right-handed: (x, y) -> (-y, x) per quarter turn. Z is unchanged. +// Rotation about +Z, right-handed: (x, y) -> (-y, x) per quarter turn. Z is unchanged. The rotated +// vector stays in the frame it started in - a rotation within a frame is not a change of frame. // // A PERMUTATION CAN STILL REFUSE. Rotation moves components between axes and negates some of them, // and the negation is where the bound bites: a component at the minimum representable value has no // negation, so the quarter turn of such a vector has no representable result. NoTurn is the one arm // that cannot refuse, because it negates nothing - and it is written through the same checked path // rather than short-circuited, so no arm produces a vector by a route the others do not take. -fn rotate_quarter_turns_about_z(v: Vector3, turns: QuarterTurns) -> SpatialArithmeticResult> { +fn rotate_quarter_turns_about_z(v: Vector3, turns: QuarterTurns) -> SpatialResult { let x = signed_millimeter_component_count(m: v.x) let y = signed_millimeter_component_count(m: v.y) let z = signed_millimeter_component_count(m: v.z) match turns { - NoTurn => vector3_from_checked(x: CheckedIntReady { value: x }, y: CheckedIntReady { value: y }, z: CheckedIntReady { value: z }) - OneQuarter => vector3_from_checked(x: checked_int_negate(a: y), y: CheckedIntReady { value: x }, z: CheckedIntReady { value: z }) - TwoQuarters => vector3_from_checked(x: checked_int_negate(a: x), y: checked_int_negate(a: y), z: CheckedIntReady { value: z }) - ThreeQuarters => vector3_from_checked(x: CheckedIntReady { value: y }, y: checked_int_negate(a: x), z: CheckedIntReady { value: z }) + NoTurn => vector3_from_checked(frame: v.frame, x: CheckedIntReady { value: x }, y: CheckedIntReady { value: y }, z: CheckedIntReady { value: z }) + OneQuarter => vector3_from_checked(frame: v.frame, x: checked_int_negate(a: y), y: CheckedIntReady { value: x }, z: CheckedIntReady { value: z }) + TwoQuarters => vector3_from_checked(frame: v.frame, x: checked_int_negate(a: x), y: checked_int_negate(a: y), z: CheckedIntReady { value: z }) + ThreeQuarters => vector3_from_checked(frame: v.frame, x: CheckedIntReady { value: y }, y: checked_int_negate(a: x), z: CheckedIntReady { value: z }) } } -// A frame-to-frame transform. Both frames are phantom parameters, so applying a RoomFrame point to -// a ZQuarterTurnTransform3 does not typecheck - the cross-frame error is -// unwritable rather than refused. +// A FRAME-TO-FRAME TRANSFORM, whose two frames are now DATA it carries rather than phantom +// parameters it advertised. The previous revision said applying a RoomFrame point to a +// ZQuarterTurnTransform3 "does not typecheck - the cross-frame error is +// unwritable rather than refused". Measured false with the rest of the phantom claim; the transform +// now declares its source and destination and apply checks both. +// +// THE TRANSLATION BELONGS TO THE DESTINATION FRAME. Rotation happens in the source frame and the +// translation is then applied in the target's coordinates, so a translation carrying any other +// frame is a construction error - checked at apply, because a record literal is reachable from +// anywhere and this carrier is not sealed. // // THE NAME STATES THE CAPABILITY. An earlier revision called this Transform3, which claims the // general affine transform, while the field was and is rotation about +Z only. The narrower name is @@ -293,30 +395,44 @@ fn rotate_quarter_turns_about_z(v: Vector3, turns: QuarterTurns) -> Spatia // quarter turn about +Z plus a 3D translation is exactly what planar room layout needs, and a later // physical consumer should derive the orientation operation it actually requires rather than // inherit a preselected rotation group. -type ZQuarterTurnTransform3 { +type ZQuarterTurnTransform3 { + from_frame: CoordinateFrameIdentity + to_frame: CoordinateFrameIdentity rotation_about_z: QuarterTurns - translation: Vector3 + translation: Vector3 } -// TWO STAGES, EITHER OF WHICH CAN REFUSE, and the first refusal is returned verbatim rather than +// THREE STAGES, ANY OF WHICH CAN REFUSE, and the first refusal is returned verbatim rather than // re-labelled: if the rotation could not be computed, the caller learns that a negation crossed the // bound, not that a translation did. -fn apply_z_quarter_turn_transform3( - transform: ZQuarterTurnTransform3, - point: Point3, -) -> SpatialArithmeticResult> { - let as_displacement = vector3( - x: signed_millimeter_component_count(m: point.x), - y: signed_millimeter_component_count(m: point.y), - z: signed_millimeter_component_count(m: point.z), - ) - match rotate_quarter_turns_about_z(v: as_displacement, turns: transform.rotation_about_z) { - SpatialArithmeticRefused { cause: c } => SpatialArithmeticRefused { cause: c } - SpatialArithmeticReady { value: rotated } => - point3_from_checked( - x: checked_int_add(a: signed_millimeter_component_count(m: rotated.x), b: signed_millimeter_component_count(m: transform.translation.x)), - y: checked_int_add(a: signed_millimeter_component_count(m: rotated.y), b: signed_millimeter_component_count(m: transform.translation.y)), - z: checked_int_add(a: signed_millimeter_component_count(m: rotated.z), b: signed_millimeter_component_count(m: transform.translation.z)), - ) +// +// The rotation runs on a displacement built in the SOURCE frame from the point's components, which +// is why that intermediate carries point.frame; the sum then lands in the destination frame. +fn apply_z_quarter_turn_transform3( + transform: ZQuarterTurnTransform3, + point: Point3, +) -> SpatialResult { + if !coordinate_frame_identity_eq(a: transform.from_frame, b: point.frame) { + SpatialFrameRefused { refusal: SpatialFrameRefusal { operation: OpApplyZQuarterTurnTransform3, left_frame: transform.from_frame, right_frame: point.frame, relation: TransformSourceFrameRequired } } + } else if !coordinate_frame_identity_eq(a: transform.to_frame, b: transform.translation.frame) { + SpatialFrameRefused { refusal: SpatialFrameRefusal { operation: OpApplyZQuarterTurnTransform3, left_frame: transform.to_frame, right_frame: transform.translation.frame, relation: TransformTranslationInDestinationRequired } } + } else { + let as_displacement = vector3( + frame: point.frame, + x: signed_millimeter_component_count(m: point.x), + y: signed_millimeter_component_count(m: point.y), + z: signed_millimeter_component_count(m: point.z), + ) + match rotate_quarter_turns_about_z(v: as_displacement, turns: transform.rotation_about_z) { + SpatialArithmeticRefused { cause: c } => SpatialArithmeticRefused { cause: c } + SpatialFrameRefused { refusal: fr } => SpatialFrameRefused { refusal: fr } + SpatialReady { value: rotated } => + point3_from_checked( + frame: transform.to_frame, + x: checked_int_add(a: signed_millimeter_component_count(m: rotated.x), b: signed_millimeter_component_count(m: transform.translation.x)), + y: checked_int_add(a: signed_millimeter_component_count(m: rotated.y), b: signed_millimeter_component_count(m: transform.translation.y)), + z: checked_int_add(a: signed_millimeter_component_count(m: rotated.z), b: signed_millimeter_component_count(m: transform.translation.z)), + ) + } } } diff --git a/dag/std/coordinate_frame.dag b/dag/std/coordinate_frame.dag new file mode 100644 index 00000000000..557edc7bdc8 --- /dev/null +++ b/dag/std/coordinate_frame.dag @@ -0,0 +1,68 @@ +module std.coordinate_frame + +import std.integer { Int } +import std.types { Bool } + +// A COORDINATE FRAME'S IDENTITY, CARRIED BY THE VALUES THAT LIVE IN IT. +// +// This module exists because of a measurement, and the measurement is the whole justification for +// its shape. SPATIAL-2 modelled the frame as a phantom type parameter - `Point3` - on the +// stated ground that a cross-frame subtraction "does not typecheck", which was called the stronger +// of the two available options. It was measured on the production compile-and-run path on +// 2026-08-11 and it is false: a `Point3` and a `Point3` flowed through +// `displacement_between3` and the program compiled clean and returned 9. Not a refusal, not a +// crash - a plausible number for a question that has no answer, which is precisely the fabricated +// output DESIGN 5 forbids. +// +// The cause is a v1 seed limitation, not a modelling slip. `v1.compiler.infer`'s argument-position +// judge compares nominal HEAD NAMES; applied type arguments live in the type node's children and +// every name-level comparison discards them. `Point3` equals `Point3`, so the frames were never +// compared. The repair to that judge (`applied_nominal_call_arg_mismatch`) lands alongside this +// module and does close the call-boundary case - but it CANNOT close the producer side, because +// return-position conformance is a separate relation that declines to judge record types at all, +// blocked on `feature:conformance-produced-type-identity`. So this stays writable regardless: +// +// fn falsely_reframe(p: Point3) -> Point3 { p } +// +// A consumer receiving that value sees only the declared type. It cannot reconstruct an identity the +// producer already erased. THEREFORE THE CARRIED IDENTITY IS THE AUTHORITY, and the honest claim is +// frame consistency BY CHECKED DERIVATION, not by construction. Every frame-sensitive operation +// compares the identities its operands actually carry and returns a typed mismatch refusal - which +// survives a lying return annotation, because the value still says where it came from. +// +// WHY NOT KEEP THE PHANTOM TOO. Two authorities for one fact is the DESIGN 3 violation whichever one +// is right, and the weaker of the two here is the one the compiler cannot enforce end-to-end. A +// phantom retained beside an authoritative carried identity invites exactly the reading that just +// cost a merged PR its central claim: that the type parameter is doing work. It is removed rather +// than demoted. Dissolve-on: when `feature:conformance-produced-type-identity` closes, a static +// frame projection can be reintroduced ABOVE this carrier and promoted to the construction rung, +// and the carried check remains as the serialization / external-input boundary where a static +// guarantee cannot reach anyway. +// +// IDENTITY IS MINTED AND DECLARATION-OWNED, never derived from a name, a path, or the contents of +// the frame. That follows the ruling already recorded for `gunbc.host_resource` +// `HostResourceIdentity`: a content-derived key makes two coincidentally-identical frames one frame, +// which is the heuristic DESIGN 4 rules unnecessary in a closed system. A frame's human-facing name +// is a display fact and belongs on whatever registers frames; it is deliberately absent here so it +// cannot be mistaken for the identity. +type CoordinateFrameIdentity { + occurrence: Int +} + +// THIRD INSTANCE OF ONE SHAPE, recorded rather than abstracted. `std.occurrence_identity` mints +// SOURCE-occurrence identities, `gunbc.host_resource` mints host-resource identities, and this mints +// coordinate-frame identities; all three are "a minted Int occurrence in a subject-specific space". +// The subject-parameterized carrier that would unify them is already a registered trigger on the +// fleet-reconcile lane, and it stays a trigger rather than being built here: sharing one Int space +// across subjects is what would let `coordinate_frame_identity_eq` answer true on a numeric +// coincidence with an unrelated subject, the cross-family comparison the ContentHash family +// grounding closed. What this row adds is evidence the extraction is due - three subjects, not two. +data coordinate_frame_identity_extraction_note: String = "std.coordinate_frame CoordinateFrameIdentity is the third minted-occurrence identity carrier in the corpus, after std.occurrence_identity (source occurrences) and gunbc.host_resource HostResourceIdentity (host resources). The subject-parameterized extraction is registered on the membership-diff reconcile spine lane as a trigger, not built here. Do not merge the Int spaces without the subject parameter: equality across two subjects sharing one space answers true on a numeric coincidence." + +fn coordinate_frame_identity(occurrence: Int) -> CoordinateFrameIdentity { + CoordinateFrameIdentity { occurrence: occurrence } +} + +fn coordinate_frame_identity_eq(a: CoordinateFrameIdentity, b: CoordinateFrameIdentity) -> Bool { + a.occurrence == b.occurrence +} diff --git a/dag/std/euclidean_geometry.dag b/dag/std/euclidean_geometry.dag index 8b5c6aa925a..570a8dbfef1 100644 --- a/dag/std/euclidean_geometry.dag +++ b/dag/std/euclidean_geometry.dag @@ -30,10 +30,15 @@ import std.affine_space { Vector3, Point3, displacement_between3, - SpatialArithmeticResult, - SpatialArithmeticReady, + SpatialResult, + SpatialReady, SpatialArithmeticRefused, + SpatialFrameRefused, + SpatialFrameRefusal, + SpatialOperationIdentity, OpDot3, OpCross3, + SpatialFrameRelation, SameFrameOperandsRequired, } +import std.coordinate_frame { CoordinateFrameIdentity, coordinate_frame_identity_eq } // SPATIAL-2, metric half. This is where integer millimetres stop being sufficient, so it is where // the numeric policy has to become structural. @@ -68,30 +73,38 @@ type ExactLength // is millimetre squared. Returning a bare Int erased that dimension at the first operation, and an // erased dimension is how a plausible-looking wrong quantity travels. Sign is retained because a // negative dot product means the displacements point away from each other. -fn dot3(a: Vector3, b: Vector3) -> SpatialArithmeticResult { +fn dot3(a: Vector3, b: Vector3) -> SpatialResult { + if !coordinate_frame_identity_eq(a: a.frame, b: b.frame) { + SpatialFrameRefused { refusal: SpatialFrameRefusal { operation: OpDot3, left_frame: a.frame, right_frame: b.frame, relation: SameFrameOperandsRequired } } + } else { let px = checked_int_multiply(a: signed_millimeter_component_count(m: a.x), b: signed_millimeter_component_count(m: b.x)) let py = checked_int_multiply(a: signed_millimeter_component_count(m: a.y), b: signed_millimeter_component_count(m: b.y)) let pz = checked_int_multiply(a: signed_millimeter_component_count(m: a.z), b: signed_millimeter_component_count(m: b.z)) match checked_add_results(a: checked_add_results(a: px, b: py), b: pz) { CheckedIntOverflow { cause: c } => SpatialArithmeticRefused { cause: c } CheckedIntReady { value: total } => - SpatialArithmeticReady { value: signed_square_millimeter(count: total) } + SpatialReady { value: signed_square_millimeter(count: total) } + } } } // An AREA vector, NOT a displacement vector. Its components are millimetre squared, and an earlier -// revision returned Vector3 - whose components are millimetre displacements - so the numbers +// revision returned Vector3 - whose components are millimetre displacements - so the numbers // were areas wearing a length type. That made translate_point3(point, by: cross3(a, b)) writable: // a cross-product area consumed as a physical translation. A separate carrier makes it unwritable // rather than merely wrong, and it is deliberately NOT an alias of Vector3: sharing three numeric // components is not sharing a dimension. -type AreaVector3 { +type AreaVector3 { + frame: CoordinateFrameIdentity x: SignedSquareMillimeter y: SignedSquareMillimeter z: SignedSquareMillimeter } -fn cross3(a: Vector3, b: Vector3) -> SpatialArithmeticResult> { +fn cross3(a: Vector3, b: Vector3) -> SpatialResult { + if !coordinate_frame_identity_eq(a: a.frame, b: b.frame) { + SpatialFrameRefused { refusal: SpatialFrameRefusal { operation: OpCross3, left_frame: a.frame, right_frame: b.frame, relation: SameFrameOperandsRequired } } + } else { let ax = signed_millimeter_component_count(m: a.x) let ay = signed_millimeter_component_count(m: a.y) let az = signed_millimeter_component_count(m: a.z) @@ -101,14 +114,15 @@ fn cross3(a: Vector3, b: Vector3) -> SpatialArithmeticResult(x: CheckedInt, y: CheckedInt, z: CheckedInt) -> SpatialArithmeticResult> { +fn area_vector3_from_checked(frame: CoordinateFrameIdentity, x: CheckedInt, y: CheckedInt, z: CheckedInt) -> SpatialResult { match x { CheckedIntOverflow { cause: c } => SpatialArithmeticRefused { cause: c } CheckedIntReady { value: xv } => @@ -118,7 +132,8 @@ fn area_vector3_from_checked(x: CheckedInt, y: CheckedInt, z: CheckedInt) -> match z { CheckedIntOverflow { cause: c } => SpatialArithmeticRefused { cause: c } CheckedIntReady { value: zv } => - SpatialArithmeticReady { value: AreaVector3 { + SpatialReady { value: AreaVector3 { + frame: frame, x: signed_square_millimeter(count: xv), y: signed_square_millimeter(count: yv), z: signed_square_millimeter(count: zv), @@ -137,7 +152,7 @@ fn area_vector3_from_checked(x: CheckedInt, y: CheckedInt, z: CheckedInt) -> // // Nonnegativity is still by construction - a sum of squares - which is why the crossing into the // Nat-backed area carrier is a magnitude read rather than a clamp. -fn norm_squared3(v: Vector3) -> SpatialArithmeticResult { +fn norm_squared3(v: Vector3) -> SpatialResult { let x = signed_millimeter_component_count(m: v.x) let y = signed_millimeter_component_count(m: v.y) let z = signed_millimeter_component_count(m: v.z) @@ -149,7 +164,7 @@ fn norm_squared3(v: Vector3) -> SpatialArithmeticResult CheckedIntReady { value: total } => match checked_int_magnitude(a: total) { CheckedNatOverflow { cause: c } => SpatialArithmeticRefused { cause: c } - CheckedNatReady { value: n } => SpatialArithmeticReady { value: square_millimeter(count: n) } + CheckedNatReady { value: n } => SpatialReady { value: square_millimeter(count: n) } } } } @@ -162,7 +177,7 @@ fn norm_squared3(v: Vector3) -> SpatialArithmeticResult // carries can itself cross the bound. The inner ExactLength is the kernel: even with unbounded // integers, a diagonal has no magnitude this axis kernel resolves. Collapsing them would tell a // caller holding a rational realization to go get a bigger integer, or the reverse. -fn norm3(v: Vector3) -> SpatialArithmeticResult { +fn norm3(v: Vector3) -> SpatialResult { let x = signed_millimeter_component_count(m: v.x) let y = signed_millimeter_component_count(m: v.y) let z = signed_millimeter_component_count(m: v.z) @@ -171,13 +186,14 @@ fn norm3(v: Vector3) -> SpatialArithmeticResult { match checked_int_magnitude(a: x + y + z) { CheckedNatOverflow { cause: c } => SpatialArithmeticRefused { cause: c } CheckedNatReady { value: n } => - SpatialArithmeticReady { value: LengthExact { value: millimeter(count: n) } } + SpatialReady { value: LengthExact { value: millimeter(count: n) } } } } else { match norm_squared3(v: v) { SpatialArithmeticRefused { cause: c } => SpatialArithmeticRefused { cause: c } - SpatialArithmeticReady { value: sq } => - SpatialArithmeticReady { value: LengthRootUnresolvedInExactKernel { + SpatialFrameRefused { refusal: fr } => SpatialFrameRefused { refusal: fr } + SpatialReady { value: sq } => + SpatialReady { value: LengthRootUnresolvedInExactKernel { squared: sq, reason: "this exact kernel resolves a magnitude only for an axis-aligned displacement; the root may itself be exact ((3,4,0) has magnitude 5, which an integer square root would find) or irrational ((1,1,0) has none), and this arm distinguishes neither", } } @@ -192,18 +208,20 @@ fn axis_count(value: Int) -> Nat { // Distance is the norm of the displacement, and inherits both partialities exactly. It is NOT a // separate approximation: one operation, asked of the vector between two points - and the point // subtraction is itself bounded, which is the third place this composite can refuse. -fn distance3(from: Point3, to: Point3) -> SpatialArithmeticResult { +fn distance3(from: Point3, to: Point3) -> SpatialResult { match displacement_between3(from: from, to: to) { SpatialArithmeticRefused { cause: c } => SpatialArithmeticRefused { cause: c } - SpatialArithmeticReady { value: d } => norm3(v: d) + SpatialFrameRefused { refusal: fr } => SpatialFrameRefused { refusal: fr } + SpatialReady { value: d } => norm3(v: d) } } // Squared distance takes no root, and is what a comparison should use. -fn distance_squared3(from: Point3, to: Point3) -> SpatialArithmeticResult { +fn distance_squared3(from: Point3, to: Point3) -> SpatialResult { match displacement_between3(from: from, to: to) { SpatialArithmeticRefused { cause: c } => SpatialArithmeticRefused { cause: c } - SpatialArithmeticReady { value: d } => norm_squared3(v: d) + SpatialFrameRefused { refusal: fr } => SpatialFrameRefused { refusal: fr } + SpatialReady { value: d } => norm_squared3(v: d) } } @@ -211,27 +229,29 @@ fn distance_squared3(from: Point3, to: Point3) -> SpatialArithmeticResu // nonnegative magnitudes. This is the operation most callers of "distance" actually want, and it // stays exact wherever both squared distances are representable - a comparison whose operands // cannot be computed has no answer, and returning false would be a verdict rather than a refusal. -fn closer_than3(a_from: Point3, a_to: Point3, b_from: Point3, b_to: Point3) -> SpatialArithmeticResult { +fn closer_than3(a_from: Point3, a_to: Point3, b_from: Point3, b_to: Point3) -> SpatialResult { match distance_squared3(from: a_from, to: a_to) { SpatialArithmeticRefused { cause: c } => SpatialArithmeticRefused { cause: c } - SpatialArithmeticReady { value: a2 } => + SpatialFrameRefused { refusal: fr } => SpatialFrameRefused { refusal: fr } + SpatialReady { value: a2 } => match distance_squared3(from: b_from, to: b_to) { SpatialArithmeticRefused { cause: c } => SpatialArithmeticRefused { cause: c } - SpatialArithmeticReady { value: b2 } => - SpatialArithmeticReady { + SpatialFrameRefused { refusal: fr } => SpatialFrameRefused { refusal: fr } + SpatialReady { value: b2 } => + SpatialReady { value: square_millimeter_count(m: a2) < square_millimeter_count(m: b2) } } } } -// A DIRECTION IS DIMENSIONLESS. An earlier revision returned Vector3 with components of -1, 0 +// A DIRECTION IS DIMENSIONLESS. An earlier revision returned Vector3 with components of -1, 0 // or 1 MILLIMETRES, which is not a direction at all - it is a one-millimetre displacement, and it // made translate_point3(point, by: normalized.direction) writable, moving the point by 1 mm. For // the exact integer-only slice the honest carrier is the axis enum: it names the six directions // integer arithmetic can represent exactly and carries no magnitude to be mistaken for one. A // general normalized direction needs division and arrives with the approximate realization. -type AxisDirection3 +type AxisDirection3 = PositiveX | NegativeX | PositiveY @@ -239,8 +259,8 @@ type AxisDirection3 | PositiveZ | NegativeZ -type Direction3Result - = DirectionExact { direction: AxisDirection3 } +type Direction3Result + = DirectionExact { frame: CoordinateFrameIdentity, direction: AxisDirection3 } | DirectionZeroVectorHasNone | DirectionUnresolvedInAxisKernel { squared_magnitude: SquareMillimeter @@ -262,16 +282,17 @@ type Direction3Result // axis_direction_of(1, 1, 0) answered PositiveX. Both are fabricated answers reachable by any // caller, safe today only because the single call site happened to be guarded. Inlined, the guard // is the enclosing branch and the case analysis cannot be reached without it. -fn normalize3(v: Vector3) -> SpatialArithmeticResult> { +fn normalize3(v: Vector3) -> SpatialResult { let x = signed_millimeter_component_count(m: v.x) let y = signed_millimeter_component_count(m: v.y) let z = signed_millimeter_component_count(m: v.z) let nonzero_axes = axis_count(value: x) + axis_count(value: y) + axis_count(value: z) if nonzero_axes == 0 { - SpatialArithmeticReady { value: DirectionZeroVectorHasNone } + SpatialReady { value: DirectionZeroVectorHasNone } } else { if nonzero_axes == 1 { - SpatialArithmeticReady { value: DirectionExact { + SpatialReady { value: DirectionExact { + frame: v.frame, direction: if x != 0 { if x < 0 { NegativeX } else { PositiveX } } else { @@ -285,8 +306,9 @@ fn normalize3(v: Vector3) -> SpatialArithmeticResult> } else { match norm_squared3(v: v) { SpatialArithmeticRefused { cause: c } => SpatialArithmeticRefused { cause: c } - SpatialArithmeticReady { value: sq } => - SpatialArithmeticReady { value: DirectionUnresolvedInAxisKernel { + SpatialFrameRefused { refusal: fr } => SpatialFrameRefused { refusal: fr } + SpatialReady { value: sq } => + SpatialReady { value: DirectionUnresolvedInAxisKernel { squared_magnitude: sq, reason: "this axis kernel resolves a unit direction only for an axis-aligned displacement; the direction may still be exactly representable ((3,4,0) is exactly (3/5,4/5,0)) and a richer realization - rational, algebraic, or error-bounded approximate - resolves it", } } diff --git a/dag/std/measure.dag b/dag/std/measure.dag index 3e0db4fccf2..93afd6b4a97 100644 --- a/dag/std/measure.dag +++ b/dag/std/measure.dag @@ -283,8 +283,8 @@ type Millimeter = Measure // spelled Measure. They were the SAME structural type, so the names implied a // distinction the typechecker did not carry - in work whose entire subject is that distinction. The // scalar really is one thing: a signed millimetre component. What separates a location from a -// displacement is the AGGREGATE that holds three of them and the operations over it - Point3 and -// Vector3 in std.affine_space, where Point + Point has no operation at all. Branding the +// displacement is the AGGREGATE that holds three of them and the operations over it - Point3 and +// Vector3 in std.affine_space, where Point + Point has no operation at all. Branding the // individual x, y and z would add conversion surface at every field access and buy no wall that the // outer types do not already carry. type SignedMillimeterComponent = Measure diff --git a/dag/test/claim/affine_space_witness_test.dag b/dag/test/claim/affine_space_witness_test.dag index 74378c626d9..c5c1e4b198a 100644 --- a/dag/test/claim/affine_space_witness_test.dag +++ b/dag/test/claim/affine_space_witness_test.dag @@ -19,8 +19,12 @@ import std.affine_space { negate_vector3, scale_vector3, rotate_quarter_turns_about_z, QuarterTurns, NoTurn, OneQuarter, TwoQuarters, ThreeQuarters, ZQuarterTurnTransform3, apply_z_quarter_turn_transform3, - SpatialArithmeticResult, SpatialArithmeticReady, SpatialArithmeticRefused, + SpatialResult, SpatialReady, SpatialArithmeticRefused, SpatialFrameRefused, + SpatialFrameRefusal, SpatialOperationIdentity, + SpatialFrameRelation, SameFrameOperandsRequired, + TransformSourceFrameRequired, TransformTranslationInDestinationRequired, } +import std.coordinate_frame { CoordinateFrameIdentity, coordinate_frame_identity, coordinate_frame_identity_eq } import std.euclidean_geometry { ExactLength, LengthExact, LengthRootUnresolvedInExactKernel, Direction3Result, DirectionExact, DirectionZeroVectorHasNone, DirectionUnresolvedInAxisKernel, @@ -29,24 +33,27 @@ import std.euclidean_geometry { dot3, cross3, norm_squared3, norm3, distance3, distance_squared3, closer_than3, normalize3, } -// Two distinct frames. They exist only as type-level tags: the room's origin is its southwest -// floor corner, the building's is elsewhere, and a coordinate means nothing without saying which. -type RoomFrame -type BuildingFrame +// TWO DISTINCT FRAMES, AS MINTED IDENTITIES THE VALUES CARRY. They were type-level tags, and the +// witness said the cross-frame error was unwritable; measured on the production compile-and-run +// path 2026-08-11, the cross-frame subtraction compiled clean and returned 9. std.coordinate_frame +// records the full account. The room's origin is its southwest floor corner, the building's is +// elsewhere, and a coordinate means nothing without saying which. +fn room() -> CoordinateFrameIdentity { coordinate_frame_identity(occurrence: 1) } +fn building() -> CoordinateFrameIdentity { coordinate_frame_identity(occurrence: 2) } -fn desk_a() -> Point3 { point3(x: 1200, y: 800, z: 0) } +fn desk_a() -> Point3 { point3(frame: room(), x: 1200, y: 800, z: 0) } // Nothing physically negative about this desk: it is 300 mm on the negative side of the chosen // x-origin. That is the whole point of the affine layer. -fn desk_b() -> Point3 { point3(x: 0 - 300, y: 2600, z: 0) } +fn desk_b() -> Point3 { point3(frame: room(), x: 0 - 300, y: 2600, z: 0) } -fn vector_equals(a: Vector3, b: Vector3) -> Bool { +fn vector_equals(a: Vector3, b: Vector3) -> Bool { signed_millimeter_component_count(m: a.x) == signed_millimeter_component_count(m: b.x) && signed_millimeter_component_count(m: a.y) == signed_millimeter_component_count(m: b.y) && signed_millimeter_component_count(m: a.z) == signed_millimeter_component_count(m: b.z) } -fn point_equals(a: Point3, b: Point3) -> Bool { +fn point_equals(a: Point3, b: Point3) -> Bool { signed_millimeter_component_count(m: a.x) == signed_millimeter_component_count(m: b.x) && signed_millimeter_component_count(m: a.y) == signed_millimeter_component_count(m: b.y) && signed_millimeter_component_count(m: a.z) == signed_millimeter_component_count(m: b.z) @@ -55,31 +62,35 @@ fn point_equals(a: Point3, b: Point3) -> Bool { // THE READY SIDE IS ASSERTED, NEVER ASSUMED. Every claim below that expects an ordinary // architectural value goes through one of these: a refusal makes the claim FALSE rather than being // silently skipped, so an implementation that started refusing everything could not read as green. -fn ready_vector_equals(r: SpatialArithmeticResult>, b: Vector3) -> Bool { +fn ready_vector_equals(r: SpatialResult, b: Vector3) -> Bool { match r { SpatialArithmeticRefused { cause: _ } => false - SpatialArithmeticReady { value: v } => vector_equals(a: v, b: b) + SpatialFrameRefused { refusal: _ } => false + SpatialReady { value: v } => vector_equals(a: v, b: b) } } -fn ready_point_equals(r: SpatialArithmeticResult>, b: Point3) -> Bool { +fn ready_point_equals(r: SpatialResult, b: Point3) -> Bool { match r { SpatialArithmeticRefused { cause: _ } => false - SpatialArithmeticReady { value: p } => point_equals(a: p, b: b) + SpatialFrameRefused { refusal: _ } => false + SpatialReady { value: p } => point_equals(a: p, b: b) } } -fn norm_squared_is(v: Vector3, expected: Nat) -> Bool { +fn norm_squared_is(v: Vector3, expected: Nat) -> Bool { match norm_squared3(v: v) { SpatialArithmeticRefused { cause: _ } => false - SpatialArithmeticReady { value: s } => square_millimeter_count(m: s) == expected + SpatialFrameRefused { refusal: _ } => false + SpatialReady { value: s } => square_millimeter_count(m: s) == expected } } -fn ready_bool_is(r: SpatialArithmeticResult, expected: Bool) -> Bool { +fn ready_bool_is(r: SpatialResult, expected: Bool) -> Bool { match r { SpatialArithmeticRefused { cause: _ } => false - SpatialArithmeticReady { value: b } => b == expected + SpatialFrameRefused { refusal: _ } => false + SpatialReady { value: b } => b == expected } } @@ -87,7 +98,7 @@ fn ready_bool_is(r: SpatialArithmeticResult, expected: Bool) -> Bool { fn witness_point_difference_is_signed_displacement() -> Bool { ready_vector_equals( r: displacement_between3(from: desk_a(), to: desk_b()), - b: vector3(x: 0 - 1500, y: 1800, z: 0), + b: vector3(frame: room(), x: 0 - 1500, y: 1800, z: 0), ) } @@ -95,27 +106,30 @@ fn witness_point_difference_is_signed_displacement() -> Bool { fn witness_translate_inverts_difference() -> Bool { match displacement_between3(from: desk_a(), to: desk_b()) { SpatialArithmeticRefused { cause: _ } => false - SpatialArithmeticReady { value: d } => + SpatialFrameRefused { refusal: _ } => false + SpatialReady { value: d } => ready_point_equals(r: translate_point3(point: desk_a(), by: d), b: desk_b()) } - && ready_point_equals(r: translate_point3(point: desk_a(), by: zero_vector3()), b: desk_a()) + && ready_point_equals(r: translate_point3(point: desk_a(), by: zero_vector3(frame: room())), b: desk_a()) } // Vector +/- Vector -> Vector, and negation is the additive inverse. fn witness_vectors_compose() -> Bool { - let u = vector3(x: 100, y: 0 - 50, z: 25) - let v = vector3(x: 0 - 30, y: 70, z: 0 - 5) + let u = vector3(frame: room(), x: 100, y: 0 - 50, z: 25) + let v = vector3(frame: room(), x: 0 - 30, y: 70, z: 0 - 5) match add_vector3(a: u, b: v) { SpatialArithmeticRefused { cause: _ } => false - SpatialArithmeticReady { value: sum } => + SpatialFrameRefused { refusal: _ } => false + SpatialReady { value: sum } => ready_vector_equals(r: subtract_vector3(a: sum, b: v), b: u) } && match negate_vector3(v: u) { SpatialArithmeticRefused { cause: _ } => false - SpatialArithmeticReady { value: nu } => - ready_vector_equals(r: add_vector3(a: u, b: nu), b: zero_vector3()) + SpatialFrameRefused { refusal: _ } => false + SpatialReady { value: nu } => + ready_vector_equals(r: add_vector3(a: u, b: nu), b: zero_vector3(frame: room())) } - && ready_vector_equals(r: scale_vector3(v: u, factor: 2), b: vector3(x: 200, y: 0 - 100, z: 50)) + && ready_vector_equals(r: scale_vector3(v: u, factor: 2), b: vector3(frame: room(), x: 200, y: 0 - 100, z: 50)) } // A quarter turn about +Z is exact: (x, y) -> (-y, x); four of them are the identity. @@ -125,14 +139,15 @@ fn witness_vectors_compose() -> Bool { // while the operation was a reflection. The defect was found by mutating the implementation and // watching this witness stay green; an asymmetric vector is what makes the sign observable. fn witness_quarter_turns_are_exact_and_close() -> Bool { - let v = vector3(x: 1000, y: 300, z: 7) - ready_vector_equals(r: rotate_quarter_turns_about_z(v: v, turns: OneQuarter), b: vector3(x: 0 - 300, y: 1000, z: 7)) - && ready_vector_equals(r: rotate_quarter_turns_about_z(v: v, turns: TwoQuarters), b: vector3(x: 0 - 1000, y: 0 - 300, z: 7)) - && ready_vector_equals(r: rotate_quarter_turns_about_z(v: v, turns: ThreeQuarters), b: vector3(x: 300, y: 0 - 1000, z: 7)) + let v = vector3(frame: room(), x: 1000, y: 300, z: 7) + ready_vector_equals(r: rotate_quarter_turns_about_z(v: v, turns: OneQuarter), b: vector3(frame: room(), x: 0 - 300, y: 1000, z: 7)) + && ready_vector_equals(r: rotate_quarter_turns_about_z(v: v, turns: TwoQuarters), b: vector3(frame: room(), x: 0 - 1000, y: 0 - 300, z: 7)) + && ready_vector_equals(r: rotate_quarter_turns_about_z(v: v, turns: ThreeQuarters), b: vector3(frame: room(), x: 300, y: 0 - 1000, z: 7)) && ready_vector_equals(r: rotate_quarter_turns_about_z(v: v, turns: NoTurn), b: v) && match rotate_quarter_turns_about_z(v: v, turns: TwoQuarters) { SpatialArithmeticRefused { cause: _ } => false - SpatialArithmeticReady { value: half } => + SpatialFrameRefused { refusal: _ } => false + SpatialReady { value: half } => ready_vector_equals(r: rotate_quarter_turns_about_z(v: half, turns: TwoQuarters), b: v) } } @@ -140,12 +155,13 @@ fn witness_quarter_turns_are_exact_and_close() -> Bool { // Squared magnitudes are exact wherever they are representable, including the diagonal case norm3 // must leave unresolved. fn witness_norm_squared_is_exact() -> Bool { - norm_squared_is(v: vector3(x: 3, y: 4, z: 0), expected: 25) - && norm_squared_is(v: vector3(x: 0 - 3, y: 0 - 4, z: 0), expected: 25) - && norm_squared_is(v: zero_vector3(), expected: 0) + norm_squared_is(v: vector3(frame: room(), x: 3, y: 4, z: 0), expected: 25) + && norm_squared_is(v: vector3(frame: room(), x: 0 - 3, y: 0 - 4, z: 0), expected: 25) + && norm_squared_is(v: zero_vector3(frame: room()), expected: 0) && match distance_squared3(from: desk_a(), to: desk_b()) { SpatialArithmeticRefused { cause: _ } => false - SpatialArithmeticReady { value: s } => + SpatialFrameRefused { refusal: _ } => false + SpatialReady { value: s } => square_millimeter_count(m: s) == (1500 * 1500) + (1800 * 1800) } } @@ -153,17 +169,19 @@ fn witness_norm_squared_is_exact() -> Bool { // THE NUMERIC POLICY, made executable. Axis-aligned magnitudes are exact; a diagonal is UNRESOLVED // and carries the exact squared magnitude so a richer kernel can finish. fn witness_norm_exact_on_axis_unresolved_on_diagonal() -> Bool { - match norm3(v: vector3(x: 0, y: 0 - 2500, z: 0)) { + match norm3(v: vector3(frame: room(), x: 0, y: 0 - 2500, z: 0)) { SpatialArithmeticRefused { cause: _ } => false - SpatialArithmeticReady { value: l } => + SpatialFrameRefused { refusal: _ } => false + SpatialReady { value: l } => match l { LengthExact { value: v } => millimeter_count(m: v) == 2500 LengthRootUnresolvedInExactKernel { squared: _, reason: _ } => false } } - && match norm3(v: vector3(x: 3, y: 4, z: 0)) { + && match norm3(v: vector3(frame: room(), x: 3, y: 4, z: 0)) { SpatialArithmeticRefused { cause: _ } => false - SpatialArithmeticReady { value: l } => + SpatialFrameRefused { refusal: _ } => false + SpatialReady { value: l } => match l { LengthExact { value: _ } => false LengthRootUnresolvedInExactKernel { squared: s, reason: _ } => @@ -172,7 +190,8 @@ fn witness_norm_exact_on_axis_unresolved_on_diagonal() -> Bool { } && match distance3(from: desk_a(), to: desk_b()) { SpatialArithmeticRefused { cause: _ } => false - SpatialArithmeticReady { value: l } => + SpatialFrameRefused { refusal: _ } => false + SpatialReady { value: l } => match l { LengthExact { value: _ } => false LengthRootUnresolvedInExactKernel { squared: s, reason: _ } => @@ -184,13 +203,13 @@ fn witness_norm_exact_on_axis_unresolved_on_diagonal() -> Bool { // Comparison needs no square root, and is exact where norm leaves the magnitude unresolved. fn witness_comparison_resolves_where_norm_does_not() -> Bool { ready_bool_is( - r: closer_than3(a_from: point3(x: 0, y: 0, z: 0), a_to: point3(x: 3, y: 4, z: 0), - b_from: point3(x: 0, y: 0, z: 0), b_to: point3(x: 30, y: 40, z: 0)), + r: closer_than3(a_from: point3(frame: room(), x: 0, y: 0, z: 0), a_to: point3(frame: room(), x: 3, y: 4, z: 0), + b_from: point3(frame: room(), x: 0, y: 0, z: 0), b_to: point3(frame: room(), x: 30, y: 40, z: 0)), expected: true, ) && ready_bool_is( - r: closer_than3(a_from: point3(x: 0, y: 0, z: 0), a_to: point3(x: 30, y: 40, z: 0), - b_from: point3(x: 0, y: 0, z: 0), b_to: point3(x: 3, y: 4, z: 0)), + r: closer_than3(a_from: point3(frame: room(), x: 0, y: 0, z: 0), a_to: point3(frame: room(), x: 30, y: 40, z: 0), + b_from: point3(frame: room(), x: 0, y: 0, z: 0), b_to: point3(frame: room(), x: 3, y: 4, z: 0)), expected: false, ) } @@ -198,27 +217,30 @@ fn witness_comparison_resolves_where_norm_does_not() -> Bool { // Zero has magnitude but no direction: a DIFFERENT arm from "this kernel did not resolve it", and // both are different again from "the machine could not compute it". fn witness_normalize_separates_no_direction_from_unresolved() -> Bool { - match normalize3(v: zero_vector3()) { + match normalize3(v: zero_vector3(frame: room())) { SpatialArithmeticRefused { cause: _ } => false - SpatialArithmeticReady { value: d } => + SpatialFrameRefused { refusal: _ } => false + SpatialReady { value: d } => match d { DirectionZeroVectorHasNone => true DirectionExact { direction: _ } => false DirectionUnresolvedInAxisKernel { squared_magnitude: _, reason: _ } => false } } - && match normalize3(v: vector3(x: 0, y: 0 - 900, z: 0)) { + && match normalize3(v: vector3(frame: room(), x: 0, y: 0 - 900, z: 0)) { SpatialArithmeticRefused { cause: _ } => false - SpatialArithmeticReady { value: d } => + SpatialFrameRefused { refusal: _ } => false + SpatialReady { value: d } => match d { DirectionExact { direction: a } => is_negative_y(d: a) DirectionZeroVectorHasNone => false DirectionUnresolvedInAxisKernel { squared_magnitude: _, reason: _ } => false } } - && match normalize3(v: vector3(x: 3, y: 4, z: 0)) { + && match normalize3(v: vector3(frame: room(), x: 3, y: 4, z: 0)) { SpatialArithmeticRefused { cause: _ } => false - SpatialArithmeticReady { value: d } => + SpatialFrameRefused { refusal: _ } => false + SpatialReady { value: d } => match d { DirectionUnresolvedInAxisKernel { squared_magnitude: s, reason: _ } => square_millimeter_count(m: s) == 25 @@ -233,34 +255,37 @@ fn witness_normalize_separates_no_direction_from_unresolved() -> Bool { // displacement - that is a type error, not a runtime refusal, which is why there is no claim here // asserting it: the code expressing it does not compile. fn witness_dot_and_cross_are_exact_and_dimensioned() -> Bool { - let u = vector3(x: 1000, y: 0, z: 0) - let v = vector3(x: 0, y: 1000, z: 0) + let u = vector3(frame: room(), x: 1000, y: 0, z: 0) + let v = vector3(frame: room(), x: 0, y: 1000, z: 0) dot_is(a: u, b: v, expected: 0) && dot_is(a: u, b: u, expected: 1000000) && match cross3(a: u, b: v) { SpatialArithmeticRefused { cause: _ } => false - SpatialArithmeticReady { value: c } => area_vector_equals(a: c, x: 0, y: 0, z: 1000000) + SpatialFrameRefused { refusal: _ } => false + SpatialReady { value: c } => area_vector_equals(a: c, x: 0, y: 0, z: 1000000) } && match negate_vector3(v: u) { SpatialArithmeticRefused { cause: _ } => false - SpatialArithmeticReady { value: nu } => dot_is(a: u, b: nu, expected: 0 - 1000000) + SpatialFrameRefused { refusal: _ } => false + SpatialReady { value: nu } => dot_is(a: u, b: nu, expected: 0 - 1000000) } } -fn dot_is(a: Vector3, b: Vector3, expected: Int) -> Bool { +fn dot_is(a: Vector3, b: Vector3, expected: Int) -> Bool { match dot3(a: a, b: b) { + SpatialFrameRefused { refusal: _ } => false SpatialArithmeticRefused { cause: _ } => false - SpatialArithmeticReady { value: d } => signed_square_millimeter_count(m: d) == expected + SpatialReady { value: d } => signed_square_millimeter_count(m: d) == expected } } -fn area_vector_equals(a: AreaVector3, x: Int, y: Int, z: Int) -> Bool { +fn area_vector_equals(a: AreaVector3, x: Int, y: Int, z: Int) -> Bool { signed_square_millimeter_count(m: a.x) == x && signed_square_millimeter_count(m: a.y) == y && signed_square_millimeter_count(m: a.z) == z } -fn is_negative_y(d: AxisDirection3) -> Bool { +fn is_negative_y(d: AxisDirection3) -> Bool { match d { NegativeY => true PositiveY => false @@ -271,23 +296,115 @@ fn is_negative_y(d: AxisDirection3) -> Bool { } } -// A transform carries a room point into the building frame. Its RESULT TYPE is Point3, -// so it cannot be fed back into a RoomFrame operation - the cross-frame error is unwritable rather -// than refused at runtime. -fn room_to_building() -> ZQuarterTurnTransform3 { - ZQuarterTurnTransform3 { rotation_about_z: OneQuarter, translation: vector3(x: 10000, y: 20000, z: 0) } +// A transform carries a room point into the building frame. It DECLARES both frames and apply +// checks them; the result carries the destination identity, so a building-frame point cannot be +// silently consumed by a room-frame operation - it is refused, not unwritable. +fn room_to_building() -> ZQuarterTurnTransform3 { + ZQuarterTurnTransform3 { + from_frame: room(), + to_frame: building(), + rotation_about_z: OneQuarter, + translation: vector3(frame: building(), x: 10000, y: 20000, z: 0), + } } fn witness_transform_crosses_frames_exactly() -> Bool { - match apply_z_quarter_turn_transform3(transform: room_to_building(), point: point3(x: 1000, y: 0, z: 500)) { + match apply_z_quarter_turn_transform3(transform: room_to_building(), point: point3(frame: room(), x: 1000, y: 0, z: 500)) { + SpatialFrameRefused { refusal: _ } => false SpatialArithmeticRefused { cause: _ } => false - SpatialArithmeticReady { value: moved } => + SpatialReady { value: moved } => signed_millimeter_component_count(m: moved.x) == 10000 && signed_millimeter_component_count(m: moved.y) == 21000 && signed_millimeter_component_count(m: moved.z) == 500 + && coordinate_frame_identity_eq(a: moved.frame, b: building()) + } +} + +// THE REGRESSION CONTROL FOR THE ENTIRE RECUT, and the one witness whose absence let a false claim +// merge. Each arm below is a program that SPATIAL-2 asserted could not be written and that was +// measured compiling clean and producing a plausible number. They must now refuse, and the refusal +// must name which frame was expected and which arrived - a bare "false" would be a verdict on a +// meaningless question rather than a refusal of it. +fn frame_refusal_is(r: SpatialResult, left: CoordinateFrameIdentity, right: CoordinateFrameIdentity) -> Bool { + match r { + SpatialReady { value: _ } => false + SpatialArithmeticRefused { cause: _ } => false + SpatialFrameRefused { refusal: fr } => + coordinate_frame_identity_eq(a: fr.left_frame, b: left) + && coordinate_frame_identity_eq(a: fr.right_frame, b: right) + && relation_is_same_frame(r: fr.relation) + } +} + +fn relation_is_same_frame(r: SpatialFrameRelation) -> Bool { + match r { + SameFrameOperandsRequired => true + TransformSourceFrameRequired => false + TransformTranslationInDestinationRequired => false + } +} + +fn relation_is_transform_source(r: SpatialFrameRelation) -> Bool { + match r { + SameFrameOperandsRequired => false + TransformSourceFrameRequired => true + TransformTranslationInDestinationRequired => false } } +fn witness_cross_frame_operations_refuse_and_name_both_frames() -> Bool { + let room_point = point3(frame: room(), x: 1, y: 2, z: 3) + let building_point = point3(frame: building(), x: 10, y: 20, z: 30) + let room_vector = vector3(frame: room(), x: 1, y: 1, z: 1) + let building_vector = vector3(frame: building(), x: 1, y: 1, z: 1) + frame_refusal_is(r: displacement_between3(from: room_point, to: building_point), left: room(), right: building()) + && frame_refusal_is(r: add_vector3(a: room_vector, b: building_vector), left: room(), right: building()) + && frame_refusal_is(r: subtract_vector3(a: room_vector, b: building_vector), left: room(), right: building()) + && match translate_point3(point: room_point, by: building_vector) { + SpatialFrameRefused { refusal: fr } => + coordinate_frame_identity_eq(a: fr.left_frame, b: room()) + && coordinate_frame_identity_eq(a: fr.right_frame, b: building()) + _ => false + } + && match apply_z_quarter_turn_transform3(transform: room_to_building(), point: building_point) { + SpatialFrameRefused { refusal: fr } => + coordinate_frame_identity_eq(a: fr.left_frame, b: room()) + && coordinate_frame_identity_eq(a: fr.right_frame, b: building()) + && relation_is_transform_source(r: fr.relation) + _ => false + } +} + +// THE POSITIVE SIBLING. Without it the witness above is satisfied by an operation that refuses +// everything, which is the failure mode a refusal-only control cannot see. +fn witness_same_frame_operations_still_answer() -> Bool { + let a = point3(frame: room(), x: 1, y: 2, z: 3) + let b = point3(frame: room(), x: 11, y: 22, z: 33) + match displacement_between3(from: a, to: b) { + SpatialFrameRefused { refusal: _ } => false + SpatialReady { value: d } => + signed_millimeter_component_count(m: d.x) == 10 + && signed_millimeter_component_count(m: d.y) == 20 + && signed_millimeter_component_count(m: d.z) == 30 + && coordinate_frame_identity_eq(a: d.frame, b: room()) + _ => false + } +} + +// A FRAME MISMATCH IS NOT AN OVERFLOW, asserted in both directions so the two causes cannot be +// collapsed into one "failed" arm later without this going red: operands that disagree on frame AND +// would also overflow report the frame, because there is no question to overflow. +fn witness_frame_and_overflow_are_distinct_causes() -> Bool { + let big_room = vector3(frame: room(), x: int_inclusive_max(), y: 0, z: 0) + let big_building = vector3(frame: building(), x: int_inclusive_max(), y: 0, z: 0) + let big_room_2 = vector3(frame: room(), x: int_inclusive_max(), y: 0, z: 0) + frame_refusal_is(r: add_vector3(a: big_room, b: big_building), left: room(), right: building()) + && match add_vector3(a: big_room, b: big_room_2) { + SpatialArithmeticRefused { cause: _ } => true + _ => false + } +} + // THE BOUND IS REAL AND EACH OPERATION CROSSES IT ITS OWN WAY. One enormous value proves one path; // these prove that add, subtract, negate, multiply, the squaring inside a squared norm, and the // two-stage transform each refuse where they individually must, and that the refusal names the @@ -295,10 +412,11 @@ fn witness_transform_crosses_frames_exactly() -> Bool { // // The identification matters more than the count: before this, every one of these produced a // wrapped i64 and the surrounding comment called the operation total and exact. -fn refusal_names(r: SpatialArithmeticResult>, op: IntegerArithmeticOperation) -> Bool { +fn refusal_names(r: SpatialResult, op: IntegerArithmeticOperation) -> Bool { match r { - SpatialArithmeticReady { value: _ } => false + SpatialReady { value: _ } => false SpatialArithmeticRefused { cause: c } => operation_equals(a: c.operation, b: op) + SpatialFrameRefused { refusal: _ } => false } } @@ -311,46 +429,51 @@ fn operation_equals(a: IntegerArithmeticOperation, b: IntegerArithmeticOperation } } -fn max_vector() -> Vector3 { - vector3(x: int_inclusive_max(), y: 0, z: 0) +fn max_vector() -> Vector3 { + vector3(frame: room(), x: int_inclusive_max(), y: 0, z: 0) } -fn min_vector() -> Vector3 { - vector3(x: int_inclusive_min(), y: 0, z: 0) +fn min_vector() -> Vector3 { + vector3(frame: room(), x: int_inclusive_min(), y: 0, z: 0) } fn witness_each_operation_refuses_at_its_own_bound() -> Bool { - refusal_names(r: add_vector3(a: max_vector(), b: vector3(x: 1, y: 0, z: 0)), op: IntegerAdd) - && refusal_names(r: subtract_vector3(a: min_vector(), b: vector3(x: 1, y: 0, z: 0)), op: IntegerSubtract) + refusal_names(r: add_vector3(a: max_vector(), b: vector3(frame: room(), x: 1, y: 0, z: 0)), op: IntegerAdd) + && refusal_names(r: subtract_vector3(a: min_vector(), b: vector3(frame: room(), x: 1, y: 0, z: 0)), op: IntegerSubtract) && refusal_names(r: negate_vector3(v: min_vector()), op: IntegerNegate) && refusal_names(r: scale_vector3(v: max_vector(), factor: 2), op: IntegerMultiply) && refusal_names(r: rotate_quarter_turns_about_z(v: min_vector(), turns: TwoQuarters), op: IntegerNegate) - && match displacement_between3(from: point3(x: int_inclusive_min(), y: 0, z: 0), to: point3(x: int_inclusive_max(), y: 0, z: 0)) { - SpatialArithmeticReady { value: _ } => false + && match displacement_between3(from: point3(frame: room(), x: int_inclusive_min(), y: 0, z: 0), to: point3(frame: room(), x: int_inclusive_max(), y: 0, z: 0)) { + SpatialReady { value: _ } => false SpatialArithmeticRefused { cause: c } => operation_equals(a: c.operation, b: IntegerSubtract) + SpatialFrameRefused { refusal: _ } => false } - && match norm_squared3(v: vector3(x: 4000000000, y: 0, z: 0)) { - SpatialArithmeticReady { value: _ } => false + && match norm_squared3(v: vector3(frame: room(), x: 4000000000, y: 0, z: 0)) { + SpatialReady { value: _ } => false SpatialArithmeticRefused { cause: c } => operation_equals(a: c.operation, b: IntegerMultiply) + SpatialFrameRefused { refusal: _ } => false } - && match dot3(a: vector3(x: 3000000000, y: 3000000000, z: 0), b: vector3(x: 3000000000, y: 3000000000, z: 0)) { - SpatialArithmeticReady { value: _ } => false + && match dot3(a: vector3(frame: room(), x: 3000000000, y: 3000000000, z: 0), b: vector3(frame: room(), x: 3000000000, y: 3000000000, z: 0)) { + SpatialReady { value: _ } => false SpatialArithmeticRefused { cause: c } => operation_equals(a: c.operation, b: IntegerAdd) + SpatialFrameRefused { refusal: _ } => false } && match apply_z_quarter_turn_transform3( - transform: ZQuarterTurnTransform3 { rotation_about_z: NoTurn, translation: vector3(x: 1, y: 0, z: 0) }, - point: point3(x: int_inclusive_max(), y: 0, z: 0), + transform: ZQuarterTurnTransform3 { from_frame: room(), to_frame: room(), rotation_about_z: NoTurn, translation: vector3(frame: room(), x: 1, y: 0, z: 0) }, + point: point3(frame: room(), x: int_inclusive_max(), y: 0, z: 0), ) { - SpatialArithmeticReady { value: _ } => false + SpatialReady { value: _ } => false SpatialArithmeticRefused { cause: c } => operation_equals(a: c.operation, b: IntegerAdd) + SpatialFrameRefused { refusal: _ } => false } } // THE OPERANDS TRAVEL WITH THE CAUSE. A refusal that named only the operation would tell a caller // that an addition failed somewhere in a three-component fold; this says which two numbers. fn witness_refusal_carries_its_operands() -> Bool { - match add_vector3(a: max_vector(), b: vector3(x: 1, y: 0, z: 0)) { - SpatialArithmeticReady { value: _ } => false + match add_vector3(a: max_vector(), b: vector3(frame: room(), x: 1, y: 0, z: 0)) { + SpatialReady { value: _ } => false + SpatialFrameRefused { refusal: _ } => false SpatialArithmeticRefused { cause: c } => match c.operands { UnaryOperand { value: _ } => false @@ -358,7 +481,8 @@ fn witness_refusal_carries_its_operands() -> Bool { } } && match negate_vector3(v: min_vector()) { - SpatialArithmeticReady { value: _ } => false + SpatialReady { value: _ } => false + SpatialFrameRefused { refusal: _ } => false SpatialArithmeticRefused { cause: c } => match c.operands { UnaryOperand { value: v } => v == int_inclusive_min() @@ -372,13 +496,66 @@ fn witness_refusal_carries_its_operands() -> Bool { // the maximum is reachable, and one past it is not. fn witness_bound_is_reached_not_merely_approached() -> Bool { ready_vector_equals( - r: add_vector3(a: vector3(x: int_inclusive_max() - 1, y: 0, z: 0), b: vector3(x: 1, y: 0, z: 0)), + r: add_vector3(a: vector3(frame: room(), x: int_inclusive_max() - 1, y: 0, z: 0), b: vector3(frame: room(), x: 1, y: 0, z: 0)), b: max_vector(), ) - && ready_vector_equals(r: negate_vector3(v: vector3(x: int_inclusive_max(), y: 0, z: 0)), - b: vector3(x: 0 - int_inclusive_max(), y: 0, z: 0)) - && ready_vector_equals(r: scale_vector3(v: vector3(x: int_inclusive_max() / 2, y: 0, z: 0), factor: 2), - b: vector3(x: (int_inclusive_max() / 2) * 2, y: 0, z: 0)) + && ready_vector_equals(r: negate_vector3(v: vector3(frame: room(), x: int_inclusive_max(), y: 0, z: 0)), + b: vector3(frame: room(), x: 0 - int_inclusive_max(), y: 0, z: 0)) + && ready_vector_equals(r: scale_vector3(v: vector3(frame: room(), x: int_inclusive_max() / 2, y: 0, z: 0), factor: 2), + b: vector3(frame: room(), x: (int_inclusive_max() / 2) * 2, y: 0, z: 0)) +} + +// THE LYING-PRODUCER CONTROL, and it is the reason the carried identity exists at all rather than +// being a nicety beside the static wall. Producer-side return conformance is open +// (feature:conformance-produced-type-identity), so a function may DECLARE a building-frame result +// while handing back a value minted in the room frame. Nothing at a call boundary can catch that: +// the consumer sees only the declared type, and the separate compiler repair judges ARGUMENTS. +// +// What this asserts is that the lie does not propagate. The value still carries room(), so the next +// frame-sensitive operation refuses and names both frames - the guarantee survives a false +// annotation precisely because it derives from the value rather than from what was written above it. +// If this ever passes by the value actually being in building(), the carried identity has stopped +// being the authority and the claim in std.coordinate_frame is false again. +fn falsely_reframed_point() -> Point3 { + point3(frame: room(), x: 5, y: 5, z: 5) +} + +fn witness_false_return_annotation_cannot_rewrite_carried_frame() -> Bool { + let claimed_building = falsely_reframed_point() + let genuine_building = point3(frame: building(), x: 0, y: 0, z: 0) + coordinate_frame_identity_eq(a: claimed_building.frame, b: room()) + && frame_refusal_is( + r: displacement_between3(from: genuine_building, to: claimed_building), + left: building(), + right: room()) +} + +// THE TRANSFORM'S SECOND FRAME OBLIGATION, distinct from the first and invisible to it. A transform +// whose translation is not expressed in its destination frame is a construction error the +// source-frame check cannot see, so it carries its own relation and its own control. +fn misframed_transform() -> ZQuarterTurnTransform3 { + ZQuarterTurnTransform3 { + from_frame: room(), + to_frame: building(), + rotation_about_z: NoTurn, + translation: vector3(frame: room(), x: 1, y: 1, z: 1), + } +} + +fn witness_transform_translation_must_be_in_destination_frame() -> Bool { + match apply_z_quarter_turn_transform3(transform: misframed_transform(), point: point3(frame: room(), x: 0, y: 0, z: 0)) { + SpatialFrameRefused { refusal: fr } => + coordinate_frame_identity_eq(a: fr.left_frame, b: building()) + && coordinate_frame_identity_eq(a: fr.right_frame, b: room()) + && match fr.relation { + TransformTranslationInDestinationRequired => true + SameFrameOperandsRequired => false + TransformSourceFrameRequired => false + } + SpatialFrameRefused { refusal: _ } => false + SpatialReady { value: _ } => false + SpatialArithmeticRefused { cause: _ } => false + } } test fn affine_space_witnesses() -> Bool { @@ -392,6 +569,11 @@ test fn affine_space_witnesses() -> Bool { && witness_normalize_separates_no_direction_from_unresolved() && witness_dot_and_cross_are_exact_and_dimensioned() && witness_transform_crosses_frames_exactly() + && witness_cross_frame_operations_refuse_and_name_both_frames() + && witness_same_frame_operations_still_answer() + && witness_frame_and_overflow_are_distinct_causes() + && witness_false_return_annotation_cannot_rewrite_carried_frame() + && witness_transform_translation_must_be_in_destination_frame() && witness_each_operation_refuses_at_its_own_bound() && witness_refusal_carries_its_operands() && witness_bound_is_reached_not_merely_approached() From 658e4aabdaf30eb44b7eec6d3e35504a4fa0ddad Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 11 Aug 2026 22:54:48 +0000 Subject: [PATCH 2/2] SPATIAL-3A: exact orthogonal geometry Everything here is closed under integer millimetre arithmetic -- no roots, no trigonometry, no rounding policy -- which is why the band sits before an approximate-numeric realization rather than after it. Rectilinear architectural geometry is exactly representable, so it is represented exactly, and the layer that needs a real number pays for it there. CARRIERS: Axis2/Axis3, AxisAlignedSegment2, AxisAlignedRectangle2, Plane3, AxisAlignedBox3, BoundingBox3, OrthogonalLoop2, AxisAlignedSurface3, OrthogonalPrism3, OrthogonalRotation3. THE WALLS ARE CONSTRUCTION, NOT VALIDATION. Every carrier is sole_constructor, so its record literal cannot be written and no cast reaches it from another module: the only route to a value is the mint beside it, and the mint refuses. A degenerate segment, an unclosed or self-intersecting loop, a zero-extent box and a cross-frame composition have no constructor outside this module rather than being checked by a caller who might not check. THE 24 ROTATIONS ARE 24 BY CONSTRUCTION. A rotation is fixed by the images of +X and +Y (six choices, then four perpendicular ones); +Z is DERIVED as their cross product, so orientation-preservation is not a determinant check that rejects reflections -- a reflection has no representation. Enumerating 24 variants would be a table to get wrong once and maintain forever, and storing three images concedes the reflected state is writable. TYPED REFUSALS, one per invalid state, because the remedies differ: coincident endpoints are an authoring slip, a diagonal is a limit of the exact kernel, a frame mismatch is a composition error. Extent refusals NAME THE AXIS that collapsed. TWO CARRIERS DELIBERATELY NOT MINTED, recorded rather than silently omitted: OrthogonalSegment2 and OrthogonalSurface3. In 2D an axis-aligned segment and an orthogonal segment denote the same set, as do an axis-aligned rectangle and an orthogonal surface in an axis-perpendicular plane; minting both spellings forks one concept across two authorities (DESIGN section 3). NO POLYGON BOOLEANS. Union, intersection and difference are absent, not stubbed and not approximated: rectilinear Booleans need a sweep with a canonical output ordering and a touching-edge degeneracy policy, and inventing that policy under the name `union` is how a plausible wrong region reaches a consumer. Green by execution, eight witnesses, every negative control with a positive sibling in the same witness -- a mint that refused everything would satisfy the refusal half of each pair, and that is exactly the gap that let SPATIAL-2 ship a wall which did not exist. Two controls earned their keep by failing first. The orientation control asserts a DERIVED z-image rather than that construction succeeded, and caught a sign inversion that made the identity rotation left-handed. The self-intersection control is a figure-eight whose eight edges are all axis-aligned, all adjacent pairs perpendicular, and no vertex repeated -- so nothing local to an edge distinguishes it, which is why the pairwise non-adjacent edge test exists rather than a repeated-vertex check standing in for it. Boundary convention, asserted rather than commented: touching faces are adjacent, not overlapping. Two rooms sharing a wall plane must not report as a collision. Co-Authored-By: Claude Opus 5 (1M context) --- dag/std/orthogonal_geometry.dag | 654 ++++++++++++++++++ .../orthogonal_geometry_witness_test.dag | 298 ++++++++ 2 files changed, 952 insertions(+) create mode 100644 dag/std/orthogonal_geometry.dag create mode 100644 dag/test/claim/orthogonal_geometry_witness_test.dag diff --git a/dag/std/orthogonal_geometry.dag b/dag/std/orthogonal_geometry.dag new file mode 100644 index 00000000000..e28dd0be70a --- /dev/null +++ b/dag/std/orthogonal_geometry.dag @@ -0,0 +1,654 @@ +module std.orthogonal_geometry + +import std.types { Bool, NonEmptyStr, List } +import std.integer { Int } +import std.nat { Nat } +import std.measure { Millimeter, millimeter, SignedMillimeterComponent, signed_millimeter_component, signed_millimeter_component_count } +import std.coordinate_frame { CoordinateFrameIdentity, coordinate_frame_identity_eq } +import std.affine_space { Point2, Point3, point2, point3 } +import std.euclidean_geometry { + AxisDirection3, PositiveX, NegativeX, PositiveY, NegativeY, PositiveZ, NegativeZ, +} + +// SPATIAL-3A: EXACT ORTHOGONAL GEOMETRY. Everything here is closed under integer millimetre +// arithmetic - no square roots, no trigonometry, no rounding policy - which is the whole reason the +// band exists at this point in the program rather than after an approximate-numeric realization. +// Rectilinear architectural geometry (rooms, walls, slabs, openings, racks) is expressible exactly, +// so it should be, and the layer that needs a real number should be the one that pays for it. +// +// WHAT THIS BAND DOES NOT CLAIM, stated first because the tempting overclaim is the one adjacent to +// it: there are NO general polygon Boolean operations here. Union, intersection and difference of +// arbitrary orthogonal loops are absent, not stubbed, not approximated. Rectilinear Booleans are +// exactly representable in principle, but they need a sweep with a canonical output ordering and a +// degeneracy policy for touching-but-not-overlapping edges, and inventing that policy underneath a +// name like `union` is how a plausible wrong region reaches a consumer. They arrive when a consumer +// needs them, with their own witnesses. +// +// THE WALLS ARE CONSTRUCTION, NOT VALIDATION. Every carrier below is `sole_constructor`, so its +// record literal cannot be written and no cast can reach it from any other module (DESIGN section +// 4b, rung four for these classes): the only route to a value is the mint beside it, and the mint +// refuses. A degenerate segment, a non-closed loop, a zero-extent box and a non-coplanar surface +// therefore have no constructor anywhere outside this module rather than being checked after the +// fact by a caller who might not check. +// +// FRAMES ARE CHECKED, NOT ASSUMED. Every mint taking more than one located value compares the +// carried CoordinateFrameIdentity of its inputs and refuses a mismatch. This is the same authority +// std.affine_space uses and for the same measured reason - see std.coordinate_frame for why the +// frame is carried data rather than a type parameter. + +// TWO CARRIERS DELIBERATELY NOT MINTED, recorded rather than silently omitted (DESIGN section 3 - +// the nicknaming rule). The band's sketch named both `AxisAlignedSegment2` and `OrthogonalSegment2`, +// and both `AxisAlignedSurface3` and `OrthogonalSurface3`. In two dimensions a segment whose +// endpoints differ on exactly one axis IS the orthogonal segment - the two names denote the same +// set, and minting both would be one concept with two authorities, which is the violation that gets +// consolidated later at cost. The same holds for a planar rectangle lying in an axis-perpendicular +// plane. If a consumer ever needs a segment that is perpendicular to a NEIGHBOUR without being +// parallel to a global axis - a rotated rectilinear loop - that is a genuinely different concept and +// earns its own carrier then, most likely as a loop plus an OrthogonalRotation3 rather than as a +// second segment type. +data orthogonal_segment_not_minted_note: String = "OrthogonalSegment2 and OrthogonalSurface3 are deliberately absent: in 2D an axis-aligned segment and an orthogonal segment denote the same set, as do an axis-aligned rectangle and an orthogonal surface in an axis-perpendicular plane. Minting both spellings would fork one concept across two authorities. A rotated rectilinear loop, if a consumer needs one, is an OrthogonalLoop2 plus an OrthogonalRotation3, not a second segment carrier." + +type Axis2 + = Axis2X + | Axis2Y + +type Axis3 + = Axis3X + | Axis3Y + | Axis3Z + +// TYPED REFUSALS, ONE PER INVALID STATE THIS MODULE CAN BE ASKED FOR. A single string reason would +// make every one of these the same fact to a consumer, and they have different remedies: a +// coincident pair of endpoints is an authoring slip, a frame mismatch is a composition error, and a +// self-intersecting loop is a geometry error. They are distinguished here so a caller can act. +type OrthogonalRefusal + = SegmentEndpointsCoincide + | SegmentNotAxisAligned + | ExtentNotPositive { axis: Axis3 } + | OrthogonalFrameMismatch { expected: CoordinateFrameIdentity, observed: CoordinateFrameIdentity } + | LoopTooFewVertices { supplied: Int } + | LoopNotClosed + | LoopEdgeNotAxisAligned + | LoopEdgesNotPerpendicular + | LoopSelfIntersects + | SurfaceNotInPlane { plane_axis: Axis3 } + | RotationAxesParallel + | BoundingBoxHasNoPoints + +type OrthogonalConstruction + = OrthogonalReady { value: T } + | OrthogonalRefused { cause: OrthogonalRefusal } + +fn axis3_index(a: Axis3) -> Int { + match a { + Axis3X => 0 + Axis3Y => 1 + Axis3Z => 2 + } +} + +fn axis3_eq(a: Axis3, b: Axis3) -> Bool { + axis3_index(a: a) == axis3_index(a: b) +} + +fn axis_direction_axis(d: AxisDirection3) -> Axis3 { + match d { + PositiveX => Axis3X + NegativeX => Axis3X + PositiveY => Axis3Y + NegativeY => Axis3Y + PositiveZ => Axis3Z + NegativeZ => Axis3Z + } +} + +fn axis_direction_is_negative(d: AxisDirection3) -> Bool { + match d { + PositiveX => false + NegativeX => true + PositiveY => false + NegativeY => true + PositiveZ => false + NegativeZ => true + } +} + +fn axis_direction_of(axis: Axis3, negative: Bool) -> AxisDirection3 { + match axis { + Axis3X => if negative { NegativeX } else { PositiveX } + Axis3Y => if negative { NegativeY } else { PositiveY } + Axis3Z => if negative { NegativeZ } else { PositiveZ } + } +} + +// THE 24 ORIENTATION-PRESERVING SIGNED AXIS PERMUTATIONS, AND THEY ARE 24 BY CONSTRUCTION RATHER +// THAN BY ENUMERATION OR BY A DETERMINANT CHECK. +// +// A rotation is fixed by where it sends +X and +Y: six choices for the image of X, and then four +// perpendicular choices for the image of Y, giving exactly 6 x 4 = 24. The image of Z is DERIVED as +// the cross product of the other two, which is what makes every reachable value orientation- +// preserving: a right-handed cross product cannot produce a reflection, so determinant -1 is not a +// state that gets checked and rejected - it has no representation. +// +// The two alternatives were both worse. Enumerating 24 named variants is a table to get wrong once +// and to maintain forever, and it makes composition a 24x24 case analysis. Storing three images and +// checking the determinant concedes that the reflected state is writable and then validates it away, +// which is the construction-over-validation inversion DESIGN section 5 names. +type OrthogonalRotation3 sole_constructor { + x_image: AxisDirection3 + y_image: AxisDirection3 +} + +// Cross product of two PERPENDICULAR signed unit axes. The caller establishes perpendicularity; this +// is total over that domain and its result for parallel inputs would be meaningless, which is +// exactly why the only mint that calls it refuses parallel axes first. +// SIGN COMPOSES AS A PRODUCT OF THREE SIGNS: the two operands' and the base orientation's, where +// the base is positive exactly when (a, b) is a cyclic pair - (X,Y), (Y,Z), (Z,X). Written as +// booleans, "the result is negative" is the XOR of the operand-sign disagreement with the +// anti-cyclic base, which reduces to equality with `cyclic`. An earlier revision wrote the exact +// negation of that and derived NegativeZ for the identity rotation X x Y; the orientation control +// caught it, which is the whole reason that control asserts a derived value rather than only that +// construction succeeded. +fn perpendicular_axis_cross(a: AxisDirection3, b: AxisDirection3) -> AxisDirection3 { + let ia = axis3_index(a: axis_direction_axis(d: a)) + let ib = axis3_index(a: axis_direction_axis(d: b)) + let third = 3 - ia - ib + let cyclic = ((ib - ia) + 3) % 3 == 1 + let operand_signs_disagree = axis_direction_is_negative(d: a) != axis_direction_is_negative(d: b) + let third_axis = if third == 0 { Axis3X } else { if third == 1 { Axis3Y } else { Axis3Z } } + axis_direction_of(axis: third_axis, negative: operand_signs_disagree == cyclic) +} + +fn orthogonal_rotation3(x_image: AxisDirection3, y_image: AxisDirection3) -> OrthogonalConstruction { + if axis3_eq(a: axis_direction_axis(d: x_image), b: axis_direction_axis(d: y_image)) { + OrthogonalRefused { cause: RotationAxesParallel } + } else { + OrthogonalReady { value: OrthogonalRotation3 { x_image: x_image, y_image: y_image } } + } +} + +fn rotation_x_image(r: OrthogonalRotation3) -> AxisDirection3 { r.x_image } + +fn rotation_y_image(r: OrthogonalRotation3) -> AxisDirection3 { r.y_image } + +// DERIVED, NEVER STORED. Storing z_image beside the other two would admit a record whose three +// images disagree - the reflection this construction exists to exclude - so it is computed on +// demand from the two that are stored (DESIGN section 2: one authority, no second representation). +fn rotation_z_image(r: OrthogonalRotation3) -> AxisDirection3 { + perpendicular_axis_cross(a: r.x_image, b: r.y_image) +} + +// A SEGMENT PARALLEL TO A COORDINATE AXIS. The axis is DERIVED from the endpoints rather than +// supplied beside them: a caller-supplied axis is a second representation of a fact the endpoints +// already determine, and the two can disagree. +// +// Both degenerate and diagonal inputs refuse, and they refuse DIFFERENTLY. Coincident endpoints are +// a segment with no direction - a point wearing a segment's type, whose direction and length every +// consumer would then have to special-case. A diagonal is a real segment this exact kernel cannot +// represent. Same rejection, different fact, so a caller can tell an authoring slip from a modelling +// limit. +type AxisAlignedSegment2 sole_constructor { + frame: CoordinateFrameIdentity + start: Point2 + end: Point2 + axis: Axis2 +} + +fn axis_aligned_segment2(start: Point2, end: Point2) -> OrthogonalConstruction { + if !coordinate_frame_identity_eq(a: start.frame, b: end.frame) { + OrthogonalRefused { cause: OrthogonalFrameMismatch { expected: start.frame, observed: end.frame } } + } else { + let dx = signed_millimeter_component_count(m: end.x) - signed_millimeter_component_count(m: start.x) + let dy = signed_millimeter_component_count(m: end.y) - signed_millimeter_component_count(m: start.y) + if (dx == 0 && dy == 0) { + OrthogonalRefused { cause: SegmentEndpointsCoincide } + } else if (dx != 0 && dy != 0) { + OrthogonalRefused { cause: SegmentNotAxisAligned } + } else { + OrthogonalReady { value: AxisAlignedSegment2 { + frame: start.frame, + start: start, + end: end, + axis: if dx != 0 { Axis2X } else { Axis2Y }, + } } + } + } +} + +fn segment2_start(s: AxisAlignedSegment2) -> Point2 { s.start } +fn segment2_end(s: AxisAlignedSegment2) -> Point2 { s.end } +fn segment2_axis(s: AxisAlignedSegment2) -> Axis2 { s.axis } +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 { + 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 }) +} + +// AN AXIS-ALIGNED RECTANGLE, held as its two extreme corners rather than as an origin plus a width +// and a height. The corner pair is what makes "positive extent on both axes" a single comparison the +// mint can perform, and it is also the form every consumer of a rectangle actually wants: a caller +// with an origin and a size can compute the far corner, while a caller with two corners handed an +// origin-plus-size carrier has to do signed arithmetic to recover what it already had. +// +// DEGENERATE IS REFUSED, not admitted as a thin rectangle. A rectangle with zero width is a segment +// and a rectangle with zero height is a segment; admitting either means every downstream area, +// containment and intersection operation carries a special case for a shape that is not a rectangle. +type AxisAlignedRectangle2 sole_constructor { + frame: CoordinateFrameIdentity + min: Point2 + max: Point2 +} + +fn axis_aligned_rectangle2(min: Point2, max: Point2) -> OrthogonalConstruction { + if !coordinate_frame_identity_eq(a: min.frame, b: max.frame) { + OrthogonalRefused { cause: OrthogonalFrameMismatch { expected: min.frame, observed: max.frame } } + } else if signed_millimeter_component_count(m: max.x) <= signed_millimeter_component_count(m: min.x) { + OrthogonalRefused { cause: ExtentNotPositive { axis: Axis3X } } + } else if signed_millimeter_component_count(m: max.y) <= signed_millimeter_component_count(m: min.y) { + OrthogonalRefused { cause: ExtentNotPositive { axis: Axis3Y } } + } else { + OrthogonalReady { value: AxisAlignedRectangle2 { frame: min.frame, min: min, max: max } } + } +} + +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_height(r: AxisAlignedRectangle2) -> Millimeter { + millimeter(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 +// it sits. This is the only plane family exactly representable here: a plane at any other +// orientation needs a normal whose components are not all zero-or-one, and normalising it needs a +// root. That restriction is the carrier's meaning rather than a limitation hidden inside it - a +// general plane is a different carrier, arriving with the approximate-numeric realization. +type Plane3 sole_constructor { + frame: CoordinateFrameIdentity + normal_axis: Axis3 + offset: SignedMillimeterComponent +} + +fn plane3(frame: CoordinateFrameIdentity, normal_axis: Axis3, offset: Int) -> Plane3 { + Plane3 { frame: frame, normal_axis: normal_axis, offset: signed_millimeter_component(count: offset) } +} + +fn plane3_frame(p: Plane3) -> CoordinateFrameIdentity { p.frame } +fn plane3_normal_axis(p: Plane3) -> Axis3 { p.normal_axis } +fn plane3_offset(p: Plane3) -> SignedMillimeterComponent { p.offset } + +fn point3_component_on_axis(p: Point3, axis: Axis3) -> Int { + match axis { + Axis3X => signed_millimeter_component_count(m: p.x) + Axis3Y => signed_millimeter_component_count(m: p.y) + Axis3Z => signed_millimeter_component_count(m: p.z) + } +} + +fn plane3_contains_point(plane: Plane3, p: Point3) -> Bool { + coordinate_frame_identity_eq(a: plane.frame, b: p.frame) + && point3_component_on_axis(p: p, axis: plane.normal_axis) == signed_millimeter_component_count(m: plane.offset) +} + +// AN AXIS-ALIGNED BOX, the 3D sibling of the rectangle and refused on the same grounds in three +// axes rather than two. The refusal NAMES WHICH AXIS collapsed, because "the box is degenerate" sends +// a caller to inspect three numbers when the mint already knows which one is wrong. +type AxisAlignedBox3 sole_constructor { + frame: CoordinateFrameIdentity + min: Point3 + max: Point3 +} + +fn axis_aligned_box3(min: Point3, max: Point3) -> OrthogonalConstruction { + if !coordinate_frame_identity_eq(a: min.frame, b: max.frame) { + OrthogonalRefused { cause: OrthogonalFrameMismatch { expected: min.frame, observed: max.frame } } + } else if signed_millimeter_component_count(m: max.x) <= signed_millimeter_component_count(m: min.x) { + OrthogonalRefused { cause: ExtentNotPositive { axis: Axis3X } } + } else if signed_millimeter_component_count(m: max.y) <= signed_millimeter_component_count(m: min.y) { + OrthogonalRefused { cause: ExtentNotPositive { axis: Axis3Y } } + } else if signed_millimeter_component_count(m: max.z) <= signed_millimeter_component_count(m: min.z) { + OrthogonalRefused { cause: ExtentNotPositive { axis: Axis3Z } } + } else { + OrthogonalReady { value: AxisAlignedBox3 { frame: min.frame, min: min, max: max } } + } +} + +fn box3_min(b: AxisAlignedBox3) -> Point3 { b.min } +fn box3_max(b: AxisAlignedBox3) -> Point3 { b.max } +fn box3_frame(b: AxisAlignedBox3) -> CoordinateFrameIdentity { b.frame } + +fn box3_contains_point(b: AxisAlignedBox3, p: Point3) -> Bool { + coordinate_frame_identity_eq(a: b.frame, b: p.frame) + && signed_millimeter_component_count(m: p.x) >= signed_millimeter_component_count(m: b.min.x) + && signed_millimeter_component_count(m: p.x) <= signed_millimeter_component_count(m: b.max.x) + && signed_millimeter_component_count(m: p.y) >= signed_millimeter_component_count(m: b.min.y) + && signed_millimeter_component_count(m: p.y) <= signed_millimeter_component_count(m: b.max.y) + && signed_millimeter_component_count(m: p.z) >= signed_millimeter_component_count(m: b.min.z) + && signed_millimeter_component_count(m: p.z) <= signed_millimeter_component_count(m: b.max.z) +} + +// TWO BOXES OVERLAP IFF THEY OVERLAP ON ALL THREE AXES, and touching faces do NOT overlap. That +// boundary convention is stated because it is a real choice with consequences: two rooms sharing a +// wall plane are adjacent, not intersecting, and a containment test that called them intersecting +// would report every neighbour as a collision. +fn box3_overlaps(a: AxisAlignedBox3, b: AxisAlignedBox3) -> OrthogonalConstruction { + if !coordinate_frame_identity_eq(a: a.frame, b: b.frame) { + OrthogonalRefused { cause: OrthogonalFrameMismatch { expected: a.frame, observed: b.frame } } + } else { + let overlaps_x = signed_millimeter_component_count(m: a.min.x) < signed_millimeter_component_count(m: b.max.x) + && signed_millimeter_component_count(m: b.min.x) < signed_millimeter_component_count(m: a.max.x) + let overlaps_y = signed_millimeter_component_count(m: a.min.y) < signed_millimeter_component_count(m: b.max.y) + && signed_millimeter_component_count(m: b.min.y) < signed_millimeter_component_count(m: a.max.y) + let overlaps_z = signed_millimeter_component_count(m: a.min.z) < signed_millimeter_component_count(m: b.max.z) + && signed_millimeter_component_count(m: b.min.z) < signed_millimeter_component_count(m: a.max.z) + OrthogonalReady { value: overlaps_x && overlaps_y && overlaps_z } + } +} + +// A BOUNDING BOX IS DERIVED, NEVER AUTHORED. It is the one construction here that cannot be wrong +// given a nonempty input, so it takes points rather than corners and computes the extremes. The +// empty list is the only refusal: the bounding box of nothing is not a degenerate box, it is a +// question with no answer, and returning a zero-extent box at the origin would be a fabricated one. +// +// It deliberately returns the CORNERS rather than an AxisAlignedBox3: a set of coplanar points has +// no positive extent on the axis they share, and that is not a defect in the input. A caller that +// needs a box passes the corners to axis_aligned_box3 and receives the degeneracy refusal with the +// axis named, which is strictly more information than this function collapsing the two cases. +type BoundingBox3 sole_constructor { + frame: CoordinateFrameIdentity + min: Point3 + max: Point3 +} + +fn min_int(a: Int, b: Int) -> Int { if a < b { a } else { b } } +fn max_int(a: Int, b: Int) -> Int { if a > b { a } else { b } } + +fn bounding_box3(points: List) -> OrthogonalConstruction { + match points |> first { + Absent => OrthogonalRefused { cause: BoundingBoxHasNoPoints } + Present { value: head } => + let frame_mismatch = fold(points, init: none, f: (acc, p) => + match acc { + Present { value: _ } => acc + Absent => if coordinate_frame_identity_eq(a: head.frame, b: p.frame) { none } else { Present { value: p.frame } } + }) + match frame_mismatch { + Present { value: other } => + OrthogonalRefused { cause: OrthogonalFrameMismatch { expected: head.frame, observed: other } } + Absent => + let lo_x = fold(points, init: signed_millimeter_component_count(m: head.x), f: (acc, p) => min_int(a: acc, b: signed_millimeter_component_count(m: p.x))) + let lo_y = fold(points, init: signed_millimeter_component_count(m: head.y), f: (acc, p) => min_int(a: acc, b: signed_millimeter_component_count(m: p.y))) + let lo_z = fold(points, init: signed_millimeter_component_count(m: head.z), f: (acc, p) => min_int(a: acc, b: signed_millimeter_component_count(m: p.z))) + let hi_x = fold(points, init: signed_millimeter_component_count(m: head.x), f: (acc, p) => max_int(a: acc, b: signed_millimeter_component_count(m: p.x))) + let hi_y = fold(points, init: signed_millimeter_component_count(m: head.y), f: (acc, p) => max_int(a: acc, b: signed_millimeter_component_count(m: p.y))) + let hi_z = fold(points, init: signed_millimeter_component_count(m: head.z), f: (acc, p) => max_int(a: acc, b: signed_millimeter_component_count(m: p.z))) + OrthogonalReady { value: BoundingBox3 { + frame: head.frame, + min: point3(frame: head.frame, x: lo_x, y: lo_y, z: lo_z), + max: point3(frame: head.frame, x: hi_x, y: hi_y, z: hi_z), + } } + } + } +} + +fn bounding_box3_min(b: BoundingBox3) -> Point3 { b.min } +fn bounding_box3_max(b: BoundingBox3) -> Point3 { b.max } + +// A CLOSED RECTILINEAR LOOP. The vertices are held in order and closure is IMPLICIT - the last +// vertex connects to the first - rather than being expressed by repeating the first vertex at the +// end. A repeated closing vertex is a second representation of a fact the carrier already +// guarantees, and it makes "is this loop closed" a runtime question about list contents instead of +// something true by construction. +// +// FOUR WALLS, and each refuses distinctly because each sends a caller somewhere different: +// - at least four vertices, since three axis-aligned edges cannot close +// - one frame across every vertex +// - every edge axis-aligned (consecutive vertices differ on exactly one axis) +// - consecutive edges perpendicular (the axis alternates, including across the closing edge) +// - no self-intersection +type OrthogonalLoop2 sole_constructor { + frame: CoordinateFrameIdentity + vertices: List +} + +fn point2_x(p: Point2) -> Int { signed_millimeter_component_count(m: p.x) } +fn point2_y(p: Point2) -> Int { signed_millimeter_component_count(m: p.y) } + +fn point2_same_position(a: Point2, b: Point2) -> Bool { + point2_x(p: a) == point2_x(p: b) && point2_y(p: a) == point2_y(p: b) +} + +fn loop_vertex_at(vs: List, i: Int) -> Point2? { + vs |> skip(i) |> first +} + +// Edge i runs from vertex i to vertex (i+1) mod n. Its axis is X when the y coordinates agree. +fn loop_edge_axis(a: Point2, b: Point2) -> Axis2? { + let dx = point2_x(p: b) - point2_x(p: a) + let dy = point2_y(p: b) - point2_y(p: a) + if dx != 0 && dy == 0 { + Present { value: Axis2X } + } else if dy != 0 && dx == 0 { + Present { value: Axis2Y } + } else { + none + } +} + +fn axis2_eq(a: Axis2, b: Axis2) -> Bool { + match a { + Axis2X => match b { Axis2X => true Axis2Y => false } + Axis2Y => match b { Axis2X => false Axis2Y => true } + } +} + +// TWO AXIS-ALIGNED SEGMENTS INTERSECT IFF THEY OVERLAP ON BOTH AXES, which is the whole reason this +// band restricts itself to axis-aligned geometry: the general segment-intersection predicate needs +// cross products and a degeneracy analysis, and this one is four integer comparisons. Endpoints +// count as intersection here (closed ranges) because two non-adjacent edges of a simple loop must +// not even touch. +fn ranges_overlap(a_lo: Int, a_hi: Int, b_lo: Int, b_hi: Int) -> Bool { + min_int(a: a_lo, b: a_hi) <= max_int(a: b_lo, b: b_hi) + && min_int(a: b_lo, b: b_hi) <= max_int(a: a_lo, b: a_hi) +} + +fn segments_touch(a1: Point2, a2: Point2, b1: Point2, b2: Point2) -> Bool { + ranges_overlap(a_lo: point2_x(p: a1), a_hi: point2_x(p: a2), b_lo: point2_x(p: b1), b_hi: point2_x(p: b2)) + && ranges_overlap(a_lo: point2_y(p: a1), a_hi: point2_y(p: a2), b_lo: point2_y(p: b1), b_hi: point2_y(p: b2)) +} + +// THE LOOP MINT. Each wall is checked in an order chosen so the refusal a caller receives is the +// most specific one true of their input: too few vertices before frames, frames before geometry, +// edge alignment before perpendicularity (a diagonal edge has no axis to be perpendicular about), +// and self-intersection last because it is the only check that is not local to one edge. +// AXIS QUERIES ARE COMPUTED PER EDGE FROM THE VERTICES rather than materialised as a +// List. The list form forced a nested optional at every read - the `first` of a list of +// optionals - and the seed resolves the inner pattern against Axis2 rather than against Optional, +// so the nesting was not merely awkward, it did not typecheck. One level of optional per lookup. +fn loop_edge_axis_at(vertices: List, i: Int, n: Int) -> Axis2? { + match loop_vertex_at(vs: vertices, i: i) { + Absent => none + Present { value: a } => + match loop_vertex_at(vs: vertices, i: (i + 1) % n) { + Absent => none + Present { value: b } => loop_edge_axis(a: a, b: b) + } + } +} + +fn edge_axis_is(vertices: List, i: Int, n: Int, wanted: Axis2) -> Bool { + match loop_edge_axis_at(vertices: vertices, i: i, n: n) { + Absent => false + Present { value: got } => axis2_eq(a: got, b: wanted) + } +} + +fn any_edge_unaligned(vertices: List, n: Int) -> Bool { + fold(vertices |> enumerate, init: false, f: (acc, pair) => + acc || loop_edge_axis_at(vertices: vertices, i: pair.first, n: n) == none) +} + +fn any_adjacent_edges_parallel(vertices: List, n: Int) -> Bool { + fold(vertices |> enumerate, init: false, f: (acc, pair) => + if acc { + true + } else { + match loop_edge_axis_at(vertices: vertices, i: pair.first, n: n) { + Absent => true + Present { value: this_axis } => + edge_axis_is(vertices: vertices, i: (pair.first + 1) % n, n: n, wanted: this_axis) + } + }) +} + +fn any_repeated_vertex(vertices: List) -> Bool { + fold(vertices |> enumerate, init: false, f: (acc, pair) => + if acc { + true + } else { + fold(vertices |> enumerate, init: false, f: (inner, other) => + inner || (other.first > pair.first && point2_same_position(a: pair.second, b: other.second))) + }) +} + +// NON-ADJACENT EDGES MUST NOT TOUCH. Adjacency is modular: edge i is adjacent to i-1 and i+1, and +// edge 0 is adjacent to edge n-1 across the implicit closure - which is exactly the pair a +// non-modular comparison forgets, admitting a loop whose closing edge lies along its first. +fn edges_are_adjacent(i: Int, j: Int, n: Int) -> Bool { + i == j || ((i + 1) % n) == j || ((j + 1) % n) == i +} + +fn any_nonadjacent_edges_touch(vertices: List, n: Int) -> Bool { + fold(vertices |> enumerate, init: false, f: (acc, a_pair) => + if acc { + true + } else { + fold(vertices |> enumerate, init: false, f: (inner, b_pair) => + if inner || edges_are_adjacent(i: a_pair.first, j: b_pair.first, n: n) || b_pair.first < a_pair.first { + inner + } else { + match loop_vertex_at(vs: vertices, i: (a_pair.first + 1) % n) { + Absent => inner + Present { value: a2 } => + match loop_vertex_at(vs: vertices, i: (b_pair.first + 1) % n) { + Absent => inner + Present { value: b2 } => + segments_touch(a1: a_pair.second, a2: a2, b1: b_pair.second, b2: b2) + } + } + }) + }) +} + +fn orthogonal_loop2(vertices: List) -> OrthogonalConstruction { + let n = vertices |> count + if n < 4 { + OrthogonalRefused { cause: LoopTooFewVertices { supplied: n } } + } else { + match vertices |> first { + Absent => OrthogonalRefused { cause: LoopTooFewVertices { supplied: n } } + Present { value: head } => + let frame_mismatch = fold(vertices, init: none, f: (acc, p) => + match acc { + Present { value: _ } => acc + Absent => if coordinate_frame_identity_eq(a: head.frame, b: p.frame) { none } else { Present { value: p.frame } } + }) + match frame_mismatch { + Present { value: other } => + OrthogonalRefused { cause: OrthogonalFrameMismatch { expected: head.frame, observed: other } } + Absent => + if any_edge_unaligned(vertices: vertices, n: n) { + OrthogonalRefused { cause: LoopEdgeNotAxisAligned } + } else if any_adjacent_edges_parallel(vertices: vertices, n: n) { + OrthogonalRefused { cause: LoopEdgesNotPerpendicular } + } else if any_repeated_vertex(vertices: vertices) { + OrthogonalRefused { cause: LoopSelfIntersects } + } else if any_nonadjacent_edges_touch(vertices: vertices, n: n) { + OrthogonalRefused { cause: LoopSelfIntersects } + } else { + OrthogonalReady { value: OrthogonalLoop2 { frame: head.frame, vertices: vertices } } + } + } + } + } +} + +fn loop2_vertices(l: OrthogonalLoop2) -> List { l.vertices } +fn loop2_frame(l: OrthogonalLoop2) -> CoordinateFrameIdentity { l.frame } + +// A RECTANGLE LYING IN AN AXIS-PERPENDICULAR PLANE. The plane fixes one coordinate and the +// rectangle supplies the other two, so the surface is a plane plus a 2D rectangle rather than four +// 3D corners: four corners admit a non-planar quadrilateral, and checking coplanarity afterwards +// concedes that the non-planar state is writable. Here it has no representation. +// +// The 2D rectangle's axes are the plane's two IN-PLANE axes, taken in ascending index order (a +// plane perpendicular to Y is spanned by X then Z). That ordering is a convention this carrier owns +// and states, so a consumer reading `min.x` knows which physical axis it is looking at. +type AxisAlignedSurface3 sole_constructor { + plane: Plane3 + extent: AxisAlignedRectangle2 +} + +fn axis_aligned_surface3(plane: Plane3, extent: AxisAlignedRectangle2) -> OrthogonalConstruction { + if !coordinate_frame_identity_eq(a: plane.frame, b: extent.frame) { + OrthogonalRefused { cause: OrthogonalFrameMismatch { expected: plane.frame, observed: extent.frame } } + } else { + OrthogonalReady { value: AxisAlignedSurface3 { plane: plane, extent: extent } } + } +} + +fn surface3_plane(s: AxisAlignedSurface3) -> Plane3 { s.plane } +fn surface3_extent(s: AxisAlignedSurface3) -> AxisAlignedRectangle2 { s.extent } +fn surface3_frame(s: AxisAlignedSurface3) -> CoordinateFrameIdentity { s.plane.frame } + +fn in_plane_axes(normal: Axis3) -> Axis3 { + match normal { + Axis3X => Axis3Y + Axis3Y => Axis3X + Axis3Z => Axis3X + } +} + +// A PRISM IS A RECTILINEAR FOOTPRINT EXTRUDED BETWEEN TWO PARALLEL PLANES, which is what a room, a +// slab and a wall all are. It is held as the loop plus the extrusion axis and two offsets rather +// than as a 3D solid, because that is the form the footprint was authored in and re-deriving it +// from a solid would need the face decomposition the band does not have. +// +// The extrusion refuses a non-positive height for the reason the box does: a prism of zero height +// is a surface, and admitting it makes every volume and containment operation carry a special case. +type OrthogonalPrism3 sole_constructor { + footprint: OrthogonalLoop2 + extrusion_axis: Axis3 + low: SignedMillimeterComponent + high: SignedMillimeterComponent +} + +fn orthogonal_prism3(footprint: OrthogonalLoop2, extrusion_axis: Axis3, low: Int, high: Int) -> OrthogonalConstruction { + if high <= low { + OrthogonalRefused { cause: ExtentNotPositive { axis: extrusion_axis } } + } else { + OrthogonalReady { value: OrthogonalPrism3 { + footprint: footprint, + extrusion_axis: extrusion_axis, + low: signed_millimeter_component(count: low), + high: signed_millimeter_component(count: high), + } } + } +} + +fn prism3_footprint(p: OrthogonalPrism3) -> OrthogonalLoop2 { p.footprint } +fn prism3_frame(p: OrthogonalPrism3) -> CoordinateFrameIdentity { p.footprint.frame } + +fn prism3_height(p: OrthogonalPrism3) -> Millimeter { + millimeter(count: signed_millimeter_component_count(m: p.high) - signed_millimeter_component_count(m: p.low)) +} diff --git a/dag/test/claim/orthogonal_geometry_witness_test.dag b/dag/test/claim/orthogonal_geometry_witness_test.dag new file mode 100644 index 00000000000..3b3a7aba148 --- /dev/null +++ b/dag/test/claim/orthogonal_geometry_witness_test.dag @@ -0,0 +1,298 @@ +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.affine_space { Point2, Point3, point2, point3 } +import std.euclidean_geometry { AxisDirection3, PositiveX, NegativeX, PositiveY, NegativeY, PositiveZ, NegativeZ } +import std.orthogonal_geometry { + Axis2, Axis2X, Axis2Y, + Axis3, Axis3X, Axis3Y, Axis3Z, + OrthogonalConstruction, OrthogonalReady, OrthogonalRefused, + OrthogonalRefusal, SegmentEndpointsCoincide, SegmentNotAxisAligned, ExtentNotPositive, + OrthogonalFrameMismatch, LoopTooFewVertices, LoopNotClosed, LoopEdgeNotAxisAligned, + LoopEdgesNotPerpendicular, LoopSelfIntersects, SurfaceNotInPlane, RotationAxesParallel, + BoundingBoxHasNoPoints, + OrthogonalRotation3, orthogonal_rotation3, rotation_x_image, rotation_y_image, rotation_z_image, + AxisAlignedSegment2, axis_aligned_segment2, segment2_axis, segment2_length, + AxisAlignedRectangle2, axis_aligned_rectangle2, rectangle2_width, rectangle2_height, + Plane3, plane3, plane3_contains_point, + AxisAlignedBox3, axis_aligned_box3, box3_contains_point, box3_overlaps, + BoundingBox3, bounding_box3, bounding_box3_min, bounding_box3_max, + OrthogonalLoop2, orthogonal_loop2, loop2_vertices, + AxisAlignedSurface3, axis_aligned_surface3, + OrthogonalPrism3, orthogonal_prism3, prism3_height, +} +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +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) } +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 +// everything would satisfy the refusal half of each pair, and that failure mode is invisible to a +// refusal-only control - the same gap that let SPATIAL-2 ship a wall which did not exist. +fn refusal_is_extent_not_positive(r: OrthogonalConstruction, axis: Axis3) -> Bool { + match r { + OrthogonalReady { value: _ } => false + OrthogonalRefused { cause: c } => + match c { + ExtentNotPositive { axis: a } => axis3_same(a: a, b: axis) + _ => false + } + } +} + +fn axis3_same(a: Axis3, b: Axis3) -> Bool { + match a { + Axis3X => match b { Axis3X => true Axis3Y => false Axis3Z => false } + Axis3Y => match b { Axis3X => false Axis3Y => true Axis3Z => false } + Axis3Z => match b { Axis3X => false Axis3Y => false Axis3Z => true } + } +} + +fn axis_direction_same(a: AxisDirection3, b: AxisDirection3) -> Bool { + match a { + PositiveX => match b { PositiveX => true _ => false } + NegativeX => match b { NegativeX => true _ => false } + PositiveY => match b { PositiveY => true _ => false } + NegativeY => match b { NegativeY => true _ => false } + PositiveZ => match b { PositiveZ => true _ => false } + NegativeZ => match b { NegativeZ => true _ => false } + } +} + +// A SEGMENT REFUSES DEGENERACY AND DIAGONALITY DIFFERENTLY, because one is an authoring slip and +// the other is a limit of the exact kernel. A single "bad segment" refusal would send both callers +// to the same wrong place. +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 + 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 + OrthogonalRefused { cause: _ } => false + } + let degenerate = match axis_aligned_segment2(start: p2(x: 7, y: 7), end: p2(x: 7, y: 7)) { + OrthogonalReady { value: _ } => false + OrthogonalRefused { cause: c } => match c { SegmentEndpointsCoincide => true _ => false } + } + let diagonal = match axis_aligned_segment2(start: p2(x: 0, y: 0), end: p2(x: 10, y: 10)) { + OrthogonalReady { value: _ } => false + OrthogonalRefused { cause: c } => match c { SegmentNotAxisAligned => true _ => false } + } + let cross_frame = match axis_aligned_segment2(start: p2(x: 0, y: 0), end: point2(frame: building(), x: 10, y: 0)) { + OrthogonalReady { value: _ } => false + OrthogonalRefused { cause: c } => + match c { + OrthogonalFrameMismatch { expected: e, observed: o } => + coordinate_frame_identity_eq(a: e, b: room()) && coordinate_frame_identity_eq(a: o, b: building()) + _ => false + } + } + axis_aligned && negative_direction_still_positive_length && degenerate && diagonal && cross_frame +} + +// THE REFUSAL NAMES WHICH AXIS COLLAPSED. "The box is degenerate" sends a caller to inspect three +// numbers the mint already narrowed to one. +test fn box_and_rectangle_walls_hold() -> Bool { + let good_box = match axis_aligned_box3(min: p3(x: 0, y: 0, z: 0), max: p3(x: 4000, y: 3000, z: 2400)) { + OrthogonalReady { value: b } => + box3_contains_point(b: b, p: p3(x: 100, y: 100, z: 100)) + && !box3_contains_point(b: b, p: p3(x: 100, y: 100, z: 9999)) + && !box3_contains_point(b: b, p: point3(frame: building(), x: 100, y: 100, z: 100)) + OrthogonalRefused { cause: _ } => false + } + let flat_x = refusal_is_extent_not_positive(r: axis_aligned_box3(min: p3(x: 0, y: 0, z: 0), max: p3(x: 0, y: 3000, z: 2400)), axis: Axis3X) + let flat_y = refusal_is_extent_not_positive(r: axis_aligned_box3(min: p3(x: 0, y: 0, z: 0), max: p3(x: 4000, y: 0, z: 2400)), axis: Axis3Y) + 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 + OrthogonalRefused { cause: _ } => false + } + let thin_rect = match axis_aligned_rectangle2(min: p2(x: 0, y: 0), max: p2(x: 1200, y: 0)) { + OrthogonalReady { value: _ } => false + OrthogonalRefused { cause: c } => match c { ExtentNotPositive { axis: a } => axis3_same(a: a, b: Axis3Y) _ => false } + } + good_box && flat_x && flat_y && flat_z && inverted && good_rect && thin_rect +} + +// TOUCHING IS NOT OVERLAPPING, and this is the control for that convention rather than a comment +// asserting it: two rooms sharing a wall plane are adjacent, and a containment test that called +// them intersecting would report every neighbour as a collision. +test fn box_overlap_treats_touching_faces_as_adjacent() -> Bool { + match axis_aligned_box3(min: p3(x: 0, y: 0, z: 0), max: p3(x: 1000, y: 1000, z: 1000)) { + OrthogonalRefused { cause: _ } => false + OrthogonalReady { value: a } => + match axis_aligned_box3(min: p3(x: 1000, y: 0, z: 0), max: p3(x: 2000, y: 1000, z: 1000)) { + OrthogonalRefused { cause: _ } => false + OrthogonalReady { value: touching } => + match axis_aligned_box3(min: p3(x: 999, y: 0, z: 0), max: p3(x: 2000, y: 1000, z: 1000)) { + OrthogonalRefused { cause: _ } => false + OrthogonalReady { value: overlapping } => + match box3_overlaps(a: a, b: touching) { + OrthogonalReady { value: t } => + match box3_overlaps(a: a, b: overlapping) { + OrthogonalReady { value: o } => !t && o + OrthogonalRefused { cause: _ } => false + } + OrthogonalRefused { cause: _ } => false + } + } + } + } +} + +// THE 24 ROTATIONS ARE 24 BY CONSTRUCTION. Z is derived by cross product, so a reflection has no +// representation - there is nothing to check and reject. What the controls prove is that the +// derivation is the right-handed one and that a parallel pair, the only unreachable-by-intent +// input, refuses. +test fn rotation_is_orientation_preserving_by_construction() -> Bool { + let identity_rotation = match orthogonal_rotation3(x_image: PositiveX, y_image: PositiveY) { + OrthogonalReady { value: r } => axis_direction_same(a: rotation_z_image(r: r), b: PositiveZ) + OrthogonalRefused { cause: _ } => false + } + let quarter_turn_about_z = match orthogonal_rotation3(x_image: PositiveY, y_image: NegativeX) { + OrthogonalReady { value: r } => axis_direction_same(a: rotation_z_image(r: r), b: PositiveZ) + OrthogonalRefused { cause: _ } => false + } + let quarter_turn_about_x = match orthogonal_rotation3(x_image: PositiveX, y_image: PositiveZ) { + OrthogonalReady { value: r } => axis_direction_same(a: rotation_z_image(r: r), b: NegativeY) + OrthogonalRefused { cause: _ } => false + } + let parallel_same = match orthogonal_rotation3(x_image: PositiveX, y_image: PositiveX) { + OrthogonalReady { value: _ } => false + OrthogonalRefused { cause: c } => match c { RotationAxesParallel => true _ => false } + } + let parallel_opposite = match orthogonal_rotation3(x_image: PositiveX, y_image: NegativeX) { + OrthogonalReady { value: _ } => false + OrthogonalRefused { cause: c } => match c { RotationAxesParallel => true _ => false } + } + identity_rotation && quarter_turn_about_z && quarter_turn_about_x && parallel_same && parallel_opposite +} + +// THE LOOP WALLS, each with its own refusal because each sends a caller somewhere different. The +// self-intersection pair is the one worth reading: both loops have four axis-aligned, alternating +// edges and no repeated vertex, so nothing local to an edge distinguishes them. +test fn loop_walls_hold() -> Bool { + let square = [p2(x: 0, y: 0), p2(x: 4000, y: 0), p2(x: 4000, y: 3000), p2(x: 0, y: 3000)] + let good = match orthogonal_loop2(vertices: square) { + OrthogonalReady { value: l } => (loop2_vertices(l: l) |> count) == 4 + OrthogonalRefused { cause: _ } => false + } + let l_shape = [ + p2(x: 0, y: 0), p2(x: 6000, y: 0), p2(x: 6000, y: 2000), + p2(x: 3000, y: 2000), p2(x: 3000, y: 4000), p2(x: 0, y: 4000) + ] + let good_l = match orthogonal_loop2(vertices: l_shape) { + OrthogonalReady { value: l } => (loop2_vertices(l: l) |> count) == 6 + OrthogonalRefused { cause: _ } => false + } + let too_few = match orthogonal_loop2(vertices: [p2(x: 0, y: 0), p2(x: 1, y: 0), p2(x: 1, y: 1)]) { + OrthogonalReady { value: _ } => false + OrthogonalRefused { cause: c } => match c { LoopTooFewVertices { supplied: n } => n == 3 _ => false } + } + let diagonal_edge = match orthogonal_loop2(vertices: [p2(x: 0, y: 0), p2(x: 4000, y: 100), p2(x: 4000, y: 3000), p2(x: 0, y: 3000)]) { + OrthogonalReady { value: _ } => false + OrthogonalRefused { cause: c } => match c { LoopEdgeNotAxisAligned => true _ => false } + } + let collinear_run = match orthogonal_loop2(vertices: [p2(x: 0, y: 0), p2(x: 2000, y: 0), p2(x: 4000, y: 0), p2(x: 4000, y: 3000), p2(x: 0, y: 3000)]) { + OrthogonalReady { value: _ } => false + OrthogonalRefused { cause: c } => match c { LoopEdgesNotPerpendicular => true _ => false } + } + let cross_frame = match orthogonal_loop2(vertices: [p2(x: 0, y: 0), point2(frame: building(), x: 4000, y: 0), p2(x: 4000, y: 3000), p2(x: 0, y: 3000)]) { + OrthogonalReady { value: _ } => false + OrthogonalRefused { cause: c } => match c { OrthogonalFrameMismatch { expected: _, observed: _ } => true _ => false } + } + good && good_l && too_few && diagonal_edge && collinear_run && cross_frame +} + +// A FIGURE-EIGHT. Eight vertices, every edge axis-aligned, every adjacent pair perpendicular, no +// vertex repeated - and two non-adjacent edges cross. Nothing except the pairwise edge test sees +// it, which is why that test exists rather than a repeated-vertex check standing in for it. +test fn self_intersecting_loop_refuses() -> Bool { + let figure_eight = [ + p2(x: 0, y: 0), p2(x: 2000, y: 0), p2(x: 2000, y: 2000), p2(x: 1000, y: 2000), + p2(x: 1000, y: 1000), p2(x: 3000, y: 1000), p2(x: 3000, y: 3000), p2(x: 0, y: 3000) + ] + match orthogonal_loop2(vertices: figure_eight) { + OrthogonalReady { value: _ } => false + OrthogonalRefused { cause: c } => match c { LoopSelfIntersects => true _ => false } + } +} + +// A BOUNDING BOX OF NOTHING IS NOT A DEGENERATE BOX AT THE ORIGIN. Returning one would be the +// fabricated plausible output DESIGN 5 forbids, so the empty list is the one refusal. +test fn bounding_box_is_derived_and_refuses_emptiness() -> Bool { + let derived = match bounding_box3(points: [p3(x: 10, y: 0 - 5, z: 3), p3(x: 0 - 2, y: 40, z: 3), p3(x: 7, y: 1, z: 99)]) { + OrthogonalRefused { cause: _ } => false + OrthogonalReady { value: b } => + signed_millimeter_component_count(m: bounding_box3_min(b: b).x) == 0 - 2 + && signed_millimeter_component_count(m: bounding_box3_min(b: b).y) == 0 - 5 + && signed_millimeter_component_count(m: bounding_box3_min(b: b).z) == 3 + && signed_millimeter_component_count(m: bounding_box3_max(b: b).x) == 10 + && signed_millimeter_component_count(m: bounding_box3_max(b: b).y) == 40 + && signed_millimeter_component_count(m: bounding_box3_max(b: b).z) == 99 + } + let coplanar_still_bounds = match bounding_box3(points: [p3(x: 0, y: 0, z: 5), p3(x: 10, y: 10, z: 5)]) { + OrthogonalRefused { cause: _ } => false + OrthogonalReady { value: b } => signed_millimeter_component_count(m: bounding_box3_max(b: b).z) == 5 + } + let empty = match bounding_box3(points: []) { + OrthogonalReady { value: _ } => false + OrthogonalRefused { cause: c } => match c { BoundingBoxHasNoPoints => true _ => false } + } + let cross_frame = match bounding_box3(points: [p3(x: 0, y: 0, z: 0), point3(frame: building(), x: 1, y: 1, z: 1)]) { + OrthogonalReady { value: _ } => false + OrthogonalRefused { cause: c } => match c { OrthogonalFrameMismatch { expected: _, observed: _ } => true _ => false } + } + derived && coplanar_still_bounds && empty && cross_frame +} + +test fn plane_surface_and_prism_hold() -> Bool { + let floor_plane = plane3(frame: room(), normal_axis: Axis3Z, offset: 0) + let on_plane = plane3_contains_point(plane: floor_plane, p: p3(x: 500, y: 500, z: 0)) + let off_plane = !plane3_contains_point(plane: floor_plane, p: p3(x: 500, y: 500, z: 1)) + let other_frame_not_on_plane = !plane3_contains_point(plane: floor_plane, p: point3(frame: building(), x: 500, y: 500, z: 0)) + let surface = match axis_aligned_rectangle2(min: p2(x: 0, y: 0), max: p2(x: 4000, y: 3000)) { + OrthogonalRefused { cause: _ } => false + OrthogonalReady { value: rect } => + match axis_aligned_surface3(plane: floor_plane, extent: rect) { + OrthogonalReady { value: _ } => true + OrthogonalRefused { cause: _ } => false + } + } + let surface_cross_frame = match axis_aligned_rectangle2(min: point2(frame: building(), x: 0, y: 0), max: point2(frame: building(), x: 10, y: 10)) { + OrthogonalRefused { cause: _ } => false + OrthogonalReady { value: rect } => + match axis_aligned_surface3(plane: floor_plane, extent: rect) { + OrthogonalReady { value: _ } => false + OrthogonalRefused { cause: c } => match c { OrthogonalFrameMismatch { expected: _, observed: _ } => true _ => false } + } + } + let prism = match orthogonal_loop2(vertices: [p2(x: 0, y: 0), p2(x: 4000, y: 0), p2(x: 4000, y: 3000), p2(x: 0, y: 3000)]) { + OrthogonalRefused { cause: _ } => false + OrthogonalReady { value: l } => + match orthogonal_prism3(footprint: l, extrusion_axis: Axis3Z, low: 0, high: 2400) { + OrthogonalReady { value: pr } => millimeter_count(m: prism3_height(p: pr)) == 2400 + OrthogonalRefused { cause: _ } => false + } + } + let flat_prism = match orthogonal_loop2(vertices: [p2(x: 0, y: 0), p2(x: 4000, y: 0), p2(x: 4000, y: 3000), p2(x: 0, y: 3000)]) { + OrthogonalRefused { cause: _ } => false + OrthogonalReady { value: l } => + match orthogonal_prism3(footprint: l, extrusion_axis: Axis3Z, low: 2400, high: 2400) { + OrthogonalReady { value: _ } => false + OrthogonalRefused { cause: c } => match c { ExtentNotPositive { axis: a } => axis3_same(a: a, b: Axis3Z) _ => false } + } + } + on_plane && off_plane && other_frame_not_on_plane && surface && surface_cross_frame && prism && flat_prism +}