diff --git a/dag/product/compute_board/physical.dag b/dag/product/compute_board/physical.dag new file mode 100644 index 00000000000..64abf9fa41c --- /dev/null +++ b/dag/product/compute_board/physical.dag @@ -0,0 +1,252 @@ +module product.compute_board.physical + +import std.types { String, Bool, NonEmptyStr, List } +import std.integer { Int } +import std.nat { Nat } +import std.measure { Micrometer, Micro, micrometer, micrometer_count } +import std.coordinate_frame { CoordinateFrameIdentity, coordinate_frame_identity, coordinate_frame_identity_eq } +import std.affine_space { Point2, point2 } +import std.measure { signed_millimeter_component_count } +import std.spatial_frame { + FrameRegistered, + FrameRegistrationRefused, + SpatialFrameRegistry, + empty_frame_registry, + frame_length_scale, + register_frame, + registry_with, + scales_agree, +} +import std.orthogonal_geometry { + AxisAlignedRectangle2, + OrthogonalConstruction, + OrthogonalReady, + OrthogonalRefused, + axis_aligned_rectangle2, + rectangle2_contains_rectangle, + rectangle2_overlaps, +} +import extdeps.programmable_logic.ice40.subject { Ice40Package } + +data physical_note: String = "THE BOARD AS A BODY-LEVEL SHAPE, WHICH IS WHAT THE ARTICLE'S PHYSICAL STANDING WAS STANDING IN FOR. That standing admitted an outline as a NonEmptyStr — a shape no consumer can intersect, measure or test for containment, so nothing could ask the two questions a board layout actually has to answer: is every part on the board, and does any part's BODY sit on top of another. This module answers both from geometry, and answers NOTHING about pads: a package body envelope is not a land pattern, the TQ144's leads span 22 mm against a 20 mm body, and a body-only collision check therefore under-approximates real clearance. The admission arm is named BodyEnvelopesAdmitted so that under-approximation cannot be read as a clearance claim. It reuses std.orthogonal_geometry's rectangle rather than minting a board-local one, and it draws in a micrometre-registered frame, which is why the two slices before it had to land first: at millimetre grain a 0.5 mm package pitch is not expressible and two adjacent pins collapse onto one coordinate." + +// THIS IS A PACKAGE BODY ENVELOPE. IT IS NOT A FOOTPRINT, and an earlier revision of this module +// called it one — a category error worth recording rather than quietly renaming, because it was +// approved by review and would have become load-bearing the moment copper appeared. +// +// A PCB footprint is a LAND PATTERN: numbered pads with positions, shapes and sizes, a mapping +// from each package contact to exactly one pad, solder-mask and paste apertures, a pin-one +// orientation, and a courtyard. None of that is here. What is here is the outline of the plastic +// body, which answers exactly one question — does this part's body fit in this space — and cannot +// answer where anything solders. +// +// THE UNDER-APPROXIMATION IS THE DANGEROUS PART, so it is stated at the carrier rather than left +// to a reader: a TQ144's leads extend beyond its body. The body is 20 mm; the lead and land span +// is 22 mm. So two bodies that clear each other by a millimetre have already collided at their +// leads, and a collision check over bodies alone ADMITS boards that cannot be assembled. That is +// why the admission arm below is named for what it checked and not for a clearance it did not +// establish. +type PackageBodyEnvelope { + package_designator: NonEmptyStr + body_width: Micrometer + body_height: Micrometer +} + +fn body_envelope_of_ice40_package(p: Ice40Package) -> PackageBodyEnvelope { + PackageBodyEnvelope { + package_designator: p.designator, + body_width: p.body_width, + body_height: p.body_height, + } +} + +// The placement's origin is its MINIMUM corner, and the occupied extent is derived from the +// footprint rather than authored beside it — an authored extent is a second answer to how big the +// part is, and the one that disagrees with the package is the one nobody notices. +type ComponentPlacement { + identity: NonEmptyStr + body_envelope: PackageBodyEnvelope + origin: Point2 +} + +type BoardPhysicalArticle { + frame: CoordinateFrameIdentity + outline: AxisAlignedRectangle2 + placements: List +} + +type PhysicalRefusal + = BoardFrameUnregistered { frame: CoordinateFrameIdentity } + | BoardFrameIsNotSubMillimetre { frame: CoordinateFrameIdentity } + | PlacementFrameDiffersFromBoard { placement: NonEmptyStr } + | PlacementExtentNotPositive { placement: NonEmptyStr } + | PlacementNotWithinOutline { placement: NonEmptyStr } + | PlacementsOverlap { first: NonEmptyStr, second: NonEmptyStr } + | PlacementIdentityRepeated { placement: NonEmptyStr } + +type PhysicalRefusalSet { + first: PhysicalRefusal + rest: List +} + +// THE ARM IS NAMED FOR WHAT WAS CHECKED. Calling this PhysicallyAdmitted would claim a board is +// physically realizable when nothing here has looked at a pad, a clearance, a trace or a layer — +// the rung inflation DESIGN 4b names, and the more dangerous for being one word. +// +// What this establishes: every part's BODY is inside the outline, no two BODIES share interior +// area, identities are distinct, and the frame's quantum is fine enough to express the geometry. +// What it does not establish, each its own separate standing and none of them started: land +// pattern, courtyard clearance, mask and paste apertures, contact-to-pad mapping, routing, +// stackup, or a fabricator's design rules. +type PhysicalAdmission + = BodyEnvelopesAdmitted { article: BoardPhysicalArticle } + | PhysicallyRefused { causes: PhysicalRefusalSet } + +fn push_physical_refusal(acc: PhysicalRefusalSet?, r: PhysicalRefusal) -> PhysicalRefusalSet? { + match acc { + Absent => Present { value: PhysicalRefusalSet { first: r, rest: [] } } + Present { value: s } => Present { value: PhysicalRefusalSet { first: s.first, rest: concat(s.rest, [r]) } } + } +} + +fn physical_refusal_count(s: PhysicalRefusalSet) -> Nat { + 1 + fold(s.rest, init: 0, f: fn(acc, _r) { acc + 1 }) +} + +// The rectangle a placement occupies. It is a construction rather than a record because a footprint +// with a zero extent has no rectangle at all, and the geometry layer already refuses that — this +// module does not get to decide the degenerate case differently from every other consumer. +fn placement_extent(p: ComponentPlacement) -> OrthogonalConstruction { + axis_aligned_rectangle2( + min: p.origin, + max: point2( + frame: p.origin.frame, + x: signed_millimeter_component_count(m: p.origin.x) + micrometer_count(m: p.body_envelope.body_width), + y: signed_millimeter_component_count(m: p.origin.y) + micrometer_count(m: p.body_envelope.body_height) + ) + ) +} + +// SUB-MILLIMETRE IS A REQUIREMENT OF THE SUBJECT, not a preference. A board carrying a half- +// millimetre package pitch cannot be drawn in whole millimetres at all, so a millimetre-registered +// frame is refused rather than accepted and quietly rounded. This is the article's +// RequiresExactSubMillimeterCoordinateQuantum cause discharged by a check rather than by a claim. +fn frame_is_sub_millimetre(registry: SpatialFrameRegistry, frame: CoordinateFrameIdentity) -> Bool { + match frame_length_scale(r: registry, identity: frame) { + Absent => false + Present { value: s } => scales_agree(a: s, b: Micro) + } +} + +fn identity_occurrences(ps: List, id: NonEmptyStr) -> Nat { + fold(ps, init: 0, f: fn(acc, p) { if (p.identity as String) == (id as String) { acc + 1 } else { acc } }) +} + +fn seen_identity(seen: List, id: NonEmptyStr) -> Bool { + fold(seen, init: false, f: fn(acc, k) { acc || (k as String) == (id as String) }) +} + +type PlacementScan { + seen: List + causes: List +} + +// EVERY PLACEMENT IS CHECKED, AND A REPEATED IDENTITY IS REPORTED ONCE. Two placements sharing an +// identity is one defect at one identity, not one per row — the same reading the pin chain +// arrived at, and for the same reason: the cause count is a number a consumer reads as a +// population. +fn placement_refusals( + registry: SpatialFrameRegistry, + article: BoardPhysicalArticle +) -> List { + let scanned = fold(article.placements, init: PlacementScan { seen: [], causes: [] }, f: fn(acc, p) { + let repeated = if identity_occurrences(ps: article.placements, id: p.identity) > 1 && !seen_identity(seen: acc.seen, id: p.identity) { + [PlacementIdentityRepeated { placement: p.identity }] + } else { + [] + } + let same_frame = coordinate_frame_identity_eq(a: p.origin.frame, b: article.frame) + let frame_cause = if same_frame { [] } else { [PlacementFrameDiffersFromBoard { placement: p.identity }] } + let geometry_causes = if !same_frame { + [] + } else { + match placement_extent(p: p) { + OrthogonalRefused { cause: _ } => [PlacementExtentNotPositive { placement: p.identity }] + OrthogonalReady { value: rect } => + match rectangle2_contains_rectangle(outer: article.outline, inner: rect) { + OrthogonalRefused { cause: _ } => [PlacementNotWithinOutline { placement: p.identity }] + OrthogonalReady { value: inside } => + if inside { [] } else { [PlacementNotWithinOutline { placement: p.identity }] } + } + } + } + PlacementScan { + seen: concat(acc.seen, [p.identity]), + causes: concat(acc.causes, concat(repeated, concat(frame_cause, geometry_causes))), + } + }) + scanned.causes +} + +// A COLLISION IS A FACT ABOUT A PAIR, so each unordered pair is considered exactly once. The pair +// is selected BY POSITION, not by comparing identities, and that distinction is load-bearing: an +// earlier revision filtered with a.identity < b.identity, which silently skipped every pair whose +// two members share an identity — so two parts stacked at the same coordinates under one repeated +// identity were reported as a naming defect and never as the collision they also are. Ordering by +// a value that is not guaranteed distinct is accidental correctness; position always is. +type OverlapScan { + index: Nat + out: List +} + +fn overlap_refusals(article: BoardPhysicalArticle) -> List { + let outer = fold(article.placements, init: OverlapScan { index: 0, out: [] }, f: fn(acc, a) { + let inner = fold(article.placements, init: OverlapScan { index: 0, out: [] }, f: fn(bacc, b) { + let hits = if bacc.index > acc.index { + match placement_extent(p: a) { + OrthogonalRefused { cause: _ } => [] + OrthogonalReady { value: ra } => + match placement_extent(p: b) { + OrthogonalRefused { cause: _ } => [] + OrthogonalReady { value: rb } => + match rectangle2_overlaps(a: ra, b: rb) { + OrthogonalRefused { cause: _ } => [] + OrthogonalReady { value: hit } => + if hit { [PlacementsOverlap { first: a.identity, second: b.identity }] } else { [] } + } + } + } + } else { + [] + } + OverlapScan { index: bacc.index + 1, out: concat(bacc.out, hits) } + }) + OverlapScan { index: acc.index + 1, out: concat(acc.out, inner.out) } + }) + outer.out +} + +fn physical_causes(registry: SpatialFrameRegistry, article: BoardPhysicalArticle) -> List { + let frame_causes = match frame_length_scale(r: registry, identity: article.frame) { + Absent => [BoardFrameUnregistered { frame: article.frame }] + Present { value: _ } => + if frame_is_sub_millimetre(registry: registry, frame: article.frame) { + [] + } else { + [BoardFrameIsNotSubMillimetre { frame: article.frame }] + } + } + concat( + frame_causes, + concat(placement_refusals(registry: registry, article: article), overlap_refusals(article: article)) + ) +} + +fn admit_body_envelopes(registry: SpatialFrameRegistry, article: BoardPhysicalArticle) -> PhysicalAdmission { + match fold(physical_causes(registry: registry, article: article), init: none, f: fn(acc, c) { + push_physical_refusal(acc: acc, r: c) + }) { + Absent => BodyEnvelopesAdmitted { article: article } + Present { value: s } => PhysicallyRefused { causes: s } + } +} diff --git a/dag/std/orthogonal_geometry.dag b/dag/std/orthogonal_geometry.dag index bf03def0690..1a1898db202 100644 --- a/dag/std/orthogonal_geometry.dag +++ b/dag/std/orthogonal_geometry.dag @@ -222,6 +222,45 @@ fn axis_aligned_rectangle2(min: Point2, max: Point2) -> OrthogonalConstruction Bool { + coordinate_frame_identity_eq(a: r.frame, b: p.frame) + && signed_millimeter_component_count(m: p.x) >= signed_millimeter_component_count(m: r.min.x) + && signed_millimeter_component_count(m: p.x) <= signed_millimeter_component_count(m: r.max.x) + && signed_millimeter_component_count(m: p.y) >= signed_millimeter_component_count(m: r.min.y) + && signed_millimeter_component_count(m: p.y) <= signed_millimeter_component_count(m: r.max.y) +} + +fn rectangle2_contains_rectangle(outer: AxisAlignedRectangle2, inner: AxisAlignedRectangle2) -> OrthogonalConstruction { + if !coordinate_frame_identity_eq(a: outer.frame, b: inner.frame) { + OrthogonalRefused { cause: OrthogonalFrameMismatch { expected: outer.frame, observed: inner.frame } } + } else { + OrthogonalReady { + value: rectangle2_contains_point(r: outer, p: inner.min) && rectangle2_contains_point(r: outer, p: inner.max) + } + } +} + +fn rectangle2_overlaps(a: AxisAlignedRectangle2, b: AxisAlignedRectangle2) -> 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) + OrthogonalReady { value: overlaps_x && overlaps_y } + } +} + fn rectangle2_min(r: AxisAlignedRectangle2) -> Point2 { r.min } fn rectangle2_max(r: AxisAlignedRectangle2) -> Point2 { r.max } fn rectangle2_frame(r: AxisAlignedRectangle2) -> CoordinateFrameIdentity { r.frame } diff --git a/dag/test/claim/compute_board_physical_witness_test.dag b/dag/test/claim/compute_board_physical_witness_test.dag new file mode 100644 index 00000000000..8f5d6f659ce --- /dev/null +++ b/dag/test/claim/compute_board_physical_witness_test.dag @@ -0,0 +1,269 @@ +module test.claim.compute_board_physical_witness + +import std.types { Bool, String, Int, NonEmptyStr, List } +import std.measure { Micro, Milli, micrometer_count } +import std.coordinate_frame { CoordinateFrameIdentity, coordinate_frame_identity } +import std.affine_space { Point2, point2 } +import std.spatial_frame { + FrameRegistered, + FrameRegistrationRefused, + SpatialFrameRegistry, + empty_frame_registry, + register_frame, + registry_with, +} +import std.orthogonal_geometry { + AxisAlignedRectangle2, + OrthogonalReady, + OrthogonalRefused, + axis_aligned_rectangle2, +} +import product.compute_board.physical { + BoardFrameIsNotSubMillimetre, + BoardFrameUnregistered, + BoardPhysicalArticle, + PackageBodyEnvelope, + ComponentPlacement, + PhysicalRefusal, + BodyEnvelopesAdmitted, + PhysicallyRefused, + PlacementExtentNotPositive, + PlacementFrameDiffersFromBoard, + PlacementIdentityRepeated, + PlacementNotWithinOutline, + PlacementsOverlap, + admit_body_envelopes, + body_envelope_of_ice40_package, + physical_refusal_count, +} +import extdeps.programmable_logic.ice40.subject { ice40_tq144_package } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +fn board() -> CoordinateFrameIdentity { coordinate_frame_identity(occurrence: 11) } +fn other_frame() -> CoordinateFrameIdentity { coordinate_frame_identity(occurrence: 12) } +fn mm_frame() -> CoordinateFrameIdentity { coordinate_frame_identity(occurrence: 13) } + +fn registry_with_scales() -> SpatialFrameRegistry { + let r0 = empty_frame_registry() + let r1 = match register_frame(r: r0, identity: board(), length_scale: Micro) { + FrameRegistered { frame: f } => registry_with(r: r0, f: f) + FrameRegistrationRefused { cause: _ } => r0 + } + let r2 = match register_frame(r: r1, identity: other_frame(), length_scale: Micro) { + FrameRegistered { frame: f } => registry_with(r: r1, f: f) + FrameRegistrationRefused { cause: _ } => r1 + } + match register_frame(r: r2, identity: mm_frame(), length_scale: Milli) { + FrameRegistered { frame: f } => registry_with(r: r2, f: f) + FrameRegistrationRefused { cause: _ } => r2 + } +} + +fn bp(x: Int, y: Int) -> Point2 { point2(frame: board(), x: x, y: y) } + +// A 100 by 80 millimetre board, drawn in micrometres. The numbers are large precisely because the +// unit is fine, which is the point: this is the coordinate grain at which a 500 um pitch is a +// distance rather than a rounding error. +fn outline_in(frame: CoordinateFrameIdentity) -> AxisAlignedRectangle2? { + match axis_aligned_rectangle2( + min: point2(frame: frame, x: 0, y: 0), + max: point2(frame: frame, x: 100000, y: 80000) + ) { + OrthogonalReady { value: r } => Present { value: r } + OrthogonalRefused { cause: _ } => none + } +} + +// THE FOOTPRINT IS THE CITED PACKAGE'S, NOT A NUMBER RETYPED HERE. If the datasheet row moved, +// this placement would move with it. +fn tq144_body_envelope() -> PackageBodyEnvelope { + body_envelope_of_ice40_package(p: ice40_tq144_package) +} + +fn placement(id: NonEmptyStr, x: Int, y: Int) -> ComponentPlacement { + ComponentPlacement { identity: id, body_envelope: tq144_body_envelope(), origin: bp(x: x, y: y) } +} + +fn article_with(placements: List) -> BoardPhysicalArticle? { + match outline_in(frame: board()) { + Absent => none + Present { value: o } => + Present { value: BoardPhysicalArticle { frame: board(), outline: o, placements: placements } } + } +} + +fn admits(placements: List) -> Bool { + match article_with(placements: placements) { + Absent => false + Present { value: a } => + match admit_body_envelopes(registry: registry_with_scales(), article: a) { + BodyEnvelopesAdmitted { article: _ } => true + PhysicallyRefused { causes: _ } => false + } + } +} + +fn refusal_is(r: PhysicalRefusal, wanted: String) -> Bool { + match r { + BoardFrameUnregistered { frame: _ } => wanted == "BoardFrameUnregistered" + BoardFrameIsNotSubMillimetre { frame: _ } => wanted == "BoardFrameIsNotSubMillimetre" + PlacementFrameDiffersFromBoard { placement: _ } => wanted == "PlacementFrameDiffersFromBoard" + PlacementExtentNotPositive { placement: _ } => wanted == "PlacementExtentNotPositive" + PlacementNotWithinOutline { placement: _ } => wanted == "PlacementNotWithinOutline" + PlacementsOverlap { first: _, second: _ } => wanted == "PlacementsOverlap" + PlacementIdentityRepeated { placement: _ } => wanted == "PlacementIdentityRepeated" + } +} + +fn refuses_naming(placements: List, wanted: String) -> Bool { + match article_with(placements: placements) { + Absent => false + Present { value: a } => + match admit_body_envelopes(registry: registry_with_scales(), article: a) { + BodyEnvelopesAdmitted { article: _ } => false + PhysicallyRefused { causes: cs } => + fold(concat([cs.first], cs.rest), init: false, f: fn(acc, r) { acc || refusal_is(r: r, wanted: wanted) }) + } + } +} + +// THE POSITIVE CONTROL, and it comes first because every refusal below is satisfied by an +// admission that refuses everything. Two TQ144 parts, 20 mm square each, placed well apart on a +// 100 by 80 mm board: both inside, not touching, distinct identities. +test fn w_a_coherent_placement_is_admitted() -> Bool { + admits(placements: [ + placement(id: "u1", x: 5000, y: 5000), + placement(id: "u2", x: 50000, y: 5000), + ]) +} + +// A PART HANGING OFF THE EDGE. The origin is inside the outline, which is what makes this the +// interesting case: a check that tested only the origin would pass it, and the part would be +// half in air. The extent is what has to be contained. +test fn w_a_part_that_does_not_fit_inside_the_outline_refuses() -> Bool { + refuses_naming( + placements: [placement(id: "u1", x: 90000, y: 5000)], + wanted: "PlacementNotWithinOutline" + ) +} + +// TWO PARTS IN THE SAME PLACE. Twenty-millimetre bodies five millimetres apart share interior +// area, which is a collision no fabricator can build. +test fn w_two_parts_sharing_area_refuse() -> Bool { + refuses_naming( + placements: [ + placement(id: "u1", x: 5000, y: 5000), + placement(id: "u2", x: 10000, y: 5000), + ], + wanted: "PlacementsOverlap" + ) +} + +// TOUCHING IS NOT OVERLAPPING — a fact about the GEOMETRY, and an earlier revision of this test +// said it was a fact about BOARDS. Its comment read "two parts butted exactly edge to edge are a +// legal, dense layout", which is physically false for this very part: a TQ144's leads and lands +// span 22 mm against a 20 mm body, so two bodies touching have already collided at their leads. +// The assertion is kept because the boundary convention is real and worth pinning; the claim +// attached to it is deleted. What this admits is a body-envelope verdict, and the name of the arm +// it checks now says so. +test fn w_touching_bodies_do_not_register_as_overlapping() -> Bool { + admits(placements: [ + placement(id: "u1", x: 5000, y: 5000), + placement(id: "u2", x: 25000, y: 5000), + ]) +} + +test fn w_a_repeated_placement_identity_refuses() -> Bool { + refuses_naming( + placements: [ + placement(id: "u1", x: 5000, y: 5000), + placement(id: "u1", x: 50000, y: 5000), + ], + wanted: "PlacementIdentityRepeated" + ) +} + +// ONE COLLISION IS ONE CAUSE, and one repeated identity is one cause, not one per participating +// row. Counting is what makes that visible; naming the cause passes either way. +test fn w_one_defect_is_reported_once() -> Bool { + match article_with(placements: [ + placement(id: "u1", x: 5000, y: 5000), + placement(id: "u1", x: 5000, y: 5000), + ]) { + Absent => false + Present { value: a } => + match admit_body_envelopes(registry: registry_with_scales(), article: a) { + BodyEnvelopesAdmitted { article: _ } => false + // One repeated identity plus one overlap between the two coincident bodies: two distinct + // defects, each counted once, rather than four rows for two facts. + PhysicallyRefused { causes: cs } => physical_refusal_count(s: cs) == 2 + } + } +} + +test fn w_a_placement_in_another_frame_refuses() -> Bool { + refuses_naming( + placements: [ + ComponentPlacement { + identity: "u1", + body_envelope: tq144_body_envelope(), + origin: point2(frame: other_frame(), x: 5000, y: 5000), + }, + ], + wanted: "PlacementFrameDiffersFromBoard" + ) +} + +// THE SLICE'S OWN PRECONDITION, ASSERTED RATHER THAN ASSUMED. A board carrying a half-millimetre +// package pitch cannot be drawn in whole millimetres, so a millimetre-registered board frame is +// refused here instead of being accepted and silently rounded. This is the article's +// RequiresExactSubMillimeterCoordinateQuantum cause discharged by a check. +test fn w_a_millimetre_board_frame_refuses() -> Bool { + match outline_in(frame: mm_frame()) { + Absent => false + Present { value: o } => + match admit_body_envelopes( + registry: registry_with_scales(), + article: BoardPhysicalArticle { frame: mm_frame(), outline: o, placements: [] } + ) { + BodyEnvelopesAdmitted { article: _ } => false + PhysicallyRefused { causes: cs } => + fold(concat([cs.first], cs.rest), init: false, f: fn(acc, r) { + acc || refusal_is(r: r, wanted: "BoardFrameIsNotSubMillimetre") + }) + } + } +} + +// An unregistered frame has no unit at all, which is a different state from having the wrong one +// and has a different remedy: one is a board drawn at the wrong grain, the other is a board whose +// grain nobody declared. +test fn w_an_unregistered_board_frame_refuses_distinctly() -> Bool { + match outline_in(frame: board()) { + Absent => false + Present { value: o } => + match admit_body_envelopes( + registry: empty_frame_registry(), + article: BoardPhysicalArticle { frame: board(), outline: o, placements: [] } + ) { + BodyEnvelopesAdmitted { article: _ } => false + PhysicallyRefused { causes: cs } => + fold(concat([cs.first], cs.rest), init: false, f: fn(acc, r) { + acc || refusal_is(r: r, wanted: "BoardFrameUnregistered") + }) + } + } +} + +// THE ENVELOPE TRACKS THE CITED PACKAGE BODY, and the test is named for the body because that is +// all it establishes. It was previously called w_the_footprint_is_the_cited_package_body, which +// stated the category error as though it were the finding: a footprint is a land pattern, and a +// body is not one. TQ144 is a 20 mm body, which is 20000 um, and that is what the placement +// reserves — 2 mm short of the 22 mm its leads actually occupy. +test fn w_the_envelope_is_the_cited_package_body() -> Bool { + micrometer_count(m: tq144_body_envelope().body_width) == 20000 + && micrometer_count(m: tq144_body_envelope().body_height) == 20000 + && (tq144_body_envelope().package_designator as String) == "TQ144" +}