Repository navigation
PCB substrate + ALTRA-MOBO-0: board-scale geometry, device binding, and the attachment stack - #8214
Merged
Merged
Conversation
Review 51478, both findings. The blocking one: Ice40Package carried body_width_um, body_height_um and contact_pitch_um as bare Nat with the unit in the field name. A unit written in a name is a unit no consumer can read — a micrometre and a millimetre become the same type and adding them typechecks. The three fields are now Micrometer, a new alias in std.measure sitting beside Millimeter as a scale argument on the same Length axis (a half-millimetre pitch is not expressible in whole millimetres, which is why the finer step is needed at all). contact_count stays Nat, correctly: it is a cardinality, not a length. The second: assignment_refusals tested pin and signal uniqueness inside the per-assignment walk, so two assignments sharing a pin each observed the collision and each filed an identical cause. Nothing was missed, but the cause count then measured how many rows touched a defect rather than how many defects existed, and pin_refusal_set_count is exactly the number a later consumer reads as a population. Collisions moved to their own scan that reports each at its first mention in source order. Two witnesses count rather than name — naming the cause passed either way. Both axes are asserted, because a deduplication that ran on one would still double-report on the other. Twelve tests pass. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
std.coordinate_frame mints a frame identity and deliberately carries nothing else, deferring a frame's other facts to "whatever registers frames". Nothing registered them. This is that registrar, and the first fact it carries is not a display fact: it is the frame's length unit, which every coordinate living in the frame silently depends on. The affine layer fixes its component to SignedMillimeterComponent, so every coordinate in the corpus means millimetres by convention. That was true of every subject the layer had been asked to hold — racks, chassis, rooms. A printed circuit board is the first one it is false for: a TQ144 package sits on a 0.5 mm contact pitch, so in whole millimetres two adjacent pins occupy the same coordinate. The geometry does not lose accuracy, it loses the distinction, and every later question about clearance is then asked of a shape that already collapsed. The scale is a value, not a type argument, and that is not a shortcut. It is the pattern std.coordinate_frame arrived at by measurement: the v1 seed's argument-position judge discards applied type arguments, which is how a Point3<RoomFrame> and a Point3<BuildingFrame> flowed through one subtraction and returned a plausible 9. A scale parameter would be erased by the same mechanism and would announce a wall that is not there. Dissolve-on is shared with that module's. Projection refuses rather than converts, in BOTH directions. 500 um asked for in whole millimetres rounds to 0 or 1 and both are wrong invisibly. 3 mm asked for in micrometres is exactly 3000 and loses nothing — refused anyway, because the moment it answers that one it is a unit converter, and a caller who wants one should say so somewhere that names the factor rather than receiving it as a side effect of asking what something measures. Both directions are pinned. An unregistered frame has no unit rather than a millimetre default; a non-decimal Scale member cannot register a frame at all; one identity cannot hold two units. Seven witnesses pass, including the positive control without which "it refuses" is satisfied by a projection that refuses everything. Declared scope: the existing Millimeter-typed surface across orthogonal_geometry and orthogonal_topology still assumes its frame is a millimetre frame. This makes the unit readable and stops silent truncation; it does not yet guard that surface. That is the next increment, named here rather than left to be rediscovered. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…cause Review 51481, the one non-blocking finding. The reviewer called it BoardEmission carrier debt shared with the SPICE and Verilog entries. It is narrower than that, and the narrower reading is the fix: R is a parameter, SPICE and Verilog genuinely produce one cause each, and the pin chain produces a set. Their instantiation was right; mine was wrong. The consequence was real. A board with a pin off the package AND a signal left unassigned crossed the host boundary carrying one cause — the second was not refused and not deferred, it was absent, and the caller had no way to learn it existed. The admission arm already had a witness proving its causes cross intact; the target arm did not, which is why nothing caught this. The new witness plants exactly two defects and counts. Matching the arm passed before and after; the count is what moves. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The declared residue from the previous slice, narrowed to what it actually was. The geometry carriers are scale-agnostic — a rectangle holds signed components and never commits to what they measure — so the millimetre commitment lived entirely in the READERS, which were right only because every frame in the corpus happened to be a millimetre frame. segment2_length, rectangle2_width and rectangle2_height are now segment2_extent / rectangle2_width / rectangle2_height returning FrameExtent, read in the unit the shape's own frame was registered with. An unregistered frame refuses; it does not fall back to millimetres, which would answer a plausible number for a real question. The millimetre answer is still available and is now DERIVED through frame_length_as_millimeter, which refuses when the frame is not a millimetre frame instead of truncating into one. The old readers are deleted rather than kept beside the new ones: a reader that asserts a unit and a reader that derives it are two answers to one question, and the asserting one is the one that was wrong. Blast radius was one file. Only the geometry witness consumed these three, and its existing assertions pass unchanged once the two frames it draws in are registered as millimetre frames — which is the fact they always relied on and never stated. Two new tests are the ones that discriminate, since the migrated assertions pass in both worlds: the same rectangle carrier in a micrometre-registered board frame is a 20 mm package body that the old reader would have called 20000 millimetres, a twenty-metre chip; and an unregistered frame refuses to be measured at all. Residue, still declared: prism3_height and the SquareMillimeter / CubicMillimeter surface across orthogonal_topology continue to assert. The 2D surface is what a board footprint needs and is what moved here. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…age0 Review 51488, all three findings, plus the regen the Micrometer addition owed. The fused observation was the one worth fixing on its merits. Both the yosys run and the nextpnr run carried one blob holding all three tools' output, so each receipt vouched for tools it did not run — and if either output later drifted, the other would go on quoting it. Worse, a test asserted the place-and-route observation contained the synthesis cell count AND the bitstream size, which enshrined the fusion as the contract. Each run now records what its own tool reported, icepack gets its own row rather than riding on place-and-route's, and the test asserts each observation contains its own tool's output and NOT its neighbour's. The orphan helper is wired rather than deleted. roster_pin_occurrences had no consumer, but it answers a question the PR actually depends on: the vendor-and-toolchain agreement compares 96 against 96, and that is evidence only if the roster's 96 are 96 DISTINCT positions. A duplicated designator would hold the count while the real population shrank, so the agreement would stay green against a roster that had quietly lost a pin. The vendor row cited Wikipedia for a legal name, which is the one fact a registrant states about itself under obligation — a secondary source is a description of the authority, not the authority. It now cites EDGAR submissions for CIK 0000855658, the same endpoint the SCM issuer rows already reach. EDGAR's own name field reads LATTICE SEMICONDUCTOR CORP, an index normalisation; legal_name keeps the cover-page spelling, because copying the normalised form would have made the citation look tighter while making the fact less accurate. Stage0 regen: adding Micrometer to std.measure made std_measure.rs stale, which is what reddened CI. Regenerated by the generator, two lines. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Review 51493, and the finding is correct by this file's own stated rule that every negative control has a positive sibling. The headline test for this slice asserted only that frame_length_as_millimeter refuses on a micrometre-registered board frame. Every wrong answer satisfies that: a reader returning 200 instead of 20000 would have passed, so the reader's actual deliverable — returning the extent in the frame's registered unit — was never witnessed. The refusal half was the easy half. The micrometre projection is now asserted first and by count, then the millimetre refusal. Verified by mutation rather than by reading: perturbing the expected 20000 to 200 turns the test red, and restoring it turns it green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Two independent single-authority violations, one from a race and one mine. MICROMETER LANDED ON MAIN WHILE THIS BRANCH WAS OPEN, reached from a different direction: EIA-310's rack unit is 44.45 mm, so anything derived from a rack unit count is inexact at millimetre grain. Same carrier, same declaration, same Length axis. Mine is deleted and main's kept — but its reason is folded into the surviving comment rather than discarded, because two unrelated subjects independently needing one step finer is what shows this is a scale argument on the Length axis and not a rack-specific convenience. Package dimensions now use main's micrometer / micrometer_count rather than a raw record literal. This is what reddened the build: two pub type Micrometer in one generated module. Regenerated per the gate's own instructions, both passes, because the first pass runs a binary predating the change it emits and can self-verify at divergence 0 for the wrong reason. Second pass: regen_divergence_count=0. Review 51498: intent_declares reimplemented intent_declares_signal from digital_control — the same fold over the same signals with the same equality, while admission and verilog_projection already consume the existing one. Byte for byte a second authority for one fact. Deleted; the existing helper is imported and called. Thirteen pin-chain witnesses pass. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… answer The article's physical standing admitted an outline as a NonEmptyStr — a shape no consumer can intersect, measure, or test for containment, so nothing could ask whether every part is on the board or whether any part sits on top of another. Both are now answered from geometry. It reuses std.orthogonal_geometry's rectangle rather than minting a board-local one, and 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. A millimetre-registered board frame is refused rather than rounded, and an unregistered one refuses distinctly — a board drawn at the wrong grain and a board whose grain nobody declared have different remedies. The 2D siblings of box3_contains_point and box3_overlaps land upstream in std.orthogonal_geometry on the same boundary convention: an edge point is contained, and two rectangles sharing only an edge are adjacent rather than overlapping. That convention is what makes a dense layout legal instead of reporting every neighbour as a collision. They are plane siblings rather than a second implementation — lifting a footprint into a degenerate box to reuse the 3D test would invent a Z extent no authority supplies and then compare on it. The footprint is DERIVED from the cited package rather than retyped beside it, so a datasheet correction moves the placement with it. ONE DEFECT FOUND BY ITS OWN WITNESS AND FIXED, worth recording because it was the interesting one. The pair walk deduplicated with a.identity < b.identity, which silently skipped every pair whose members share an identity — so two parts stacked at identical coordinates under one repeated identity were reported as a naming defect and never as the collision they also are. The counting test caught it by expecting two causes and receiving one. Pairs are now selected by position: ordering on a value that is not guaranteed distinct is accidental correctness, and position always is. Ten witnesses pass, positive control first. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The floor refused, precisely and correctly: dag/extdeps/vendor/lattice_semiconductor.dag was a new extdeps module enrolled in neither scope_carrier_paths nor the machinery exemption, and it declared an authority anchor without an extdeps_model_scope beside it. That is not paperwork. The scope row names WHICH declaration the cited authority is about, so a citation is a typed edge to a subject rather than a URL sitting near some rows — the floating-island shape this repository already refuses elsewhere. Without it, the EDGAR citation I added in the previous commit pointed at the module rather than at the vendor fact. I enrolled the ice40 and icestorm subject modules when they landed and missed the vendor module beside them, which is why the gate exists rather than the convention being trusted. The gate itself cannot run hermetically here — it reads the change's own diff and refuses to fabricate one — so this is verified by CI rather than locally, which is stated rather than implied. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Operator ruling, and the defect is mine. ComponentFootprint held only a designator, a body width and a body height. That is a package BODY ENVELOPE. A footprint is a land pattern: numbered pads with positions, shapes and sizes, a contact-to-pad map, mask and paste apertures, a pin-one orientation and a courtyard. None of that is here, and #8205 explicitly did not supply it. The witness locked the error in rather than catching it: it was called w_the_footprint_is_the_cited_package_body, which states the category error as though it were the finding. Worse, one control asserted something physically false. Its comment read "two parts butted exactly edge to edge are a legal, dense layout" — 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 geometric assertion is kept, because the touching-is-not-overlapping convention is real and worth pinning; the board-level claim attached to it is deleted. That under-approximation is the dangerous half and is now stated at the carrier: a body-only collision check ADMITS boards that cannot be assembled. So the success arm is renamed BodyEnvelopesAdmitted. PhysicallyAdmitted claimed a board is physically realizable when nothing here has looked at a pad, a clearance, a trace or a layer — rung inflation, and the more dangerous for being one word. RequiresPackageFootprintAuthority is NOT discharged. The PR body claimed it was; that claim was false and is withdrawn. Ten witnesses pass. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ot be derived The processor package, the socket, the socket's board termination, the motherboard land pattern that termination solders to, the loading mechanism and the mounting are six independently governed identities. One vendor publishes the package, another manufactures the socket, and the motherboard designer owns neither. THE ERROR THIS MAKES UNWRITABLE is deriving the board land pattern from the processor package's bottom-land geometry. Both are grids of 4926 lands at the same pitch, so they look like one fact, and the package drawing is sitting in a datasheet this repository already cites. They are different surfaces on opposite sides of the socket. A board built on the first is a board where nothing solders. The wall is the absence: no function here takes a package and returns board pads, so a caller wanting them must go to the socket vendor. The contact POPULATION is deliberately the only thing that crosses — however the socket terminates, a 4926-contact processor needs 4926 board-side terminations — so it is a join key while the geometry is not. THREE AUTHORITY CATEGORIES, NOT TWO, because the third keeps collapsing into the second. Unresolved means nobody has looked for the document; recording it as NDA-gated invents a blocker and stops anyone looking. This repository already made the reverse error, declaring the Altra pin map NDA-only by reasoning from the reference-board collateral and defending it with a passing witness, while it was public in the cited datasheet. Redistribution is a fourth thing and is not availability: a freely downloadable document with a proprietary footer makes copying its tables into a public repository a licensing question — about where bytes may live, not about what we may know. So the package is PublicButRedistributionUndecided, and no contact row is hand-copied here. Blockers are typed by WHO ACTS: find-the-document, redistribution decision, commercial access. Collapsing them would send all three to the same person and make the tractable ones look intractable. Seven witnesses pass, including the cross-foot at 4926 reached by two independent routes and the assertion that zero attachment layers are NDA-gated. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot
Bot
changed the title
gunbai-bot
Bot
changed the base branch from
session/pcb-mvp-0-physical
to
main
August 13, 2026 05:50
This was referenced Aug 13, 2026
… inputs Review 51521 (REQUEST_CHANGES), review 51520, and the next ALTRA-MOBO-0 increment. CONSUME, DO NOT RE-MINT. attachment_stack declared its own ExternalAuthority rows for the Ampere product brief and the Customer Connect page, both of which already exist in extdeps.cpu.ampere_altra_package — and it imported that module for socket facts while doing it. One of the two duplicates was never even referenced, so it forked a fact and bought nothing. The NDA reference-board standing was likewise re-authored as product-layer prose beside the extdeps standing that already owns it, names the four boards and cites the route; it is now PROJECTED from that standing into this module's vocabulary rather than restated. A second representation in a module whose whole subject is that six layers must not collapse into fewer is a poor advertisement for the argument. THE 1P MINIMUM, and it carries a real wall rather than a threshold. The datasheet admits 1, 2, 4, 6 or 8 active DDR4 channels and documents one- and two-channel operation as engineering debug and bring-up. So the channel count is selected against a declared INTENT: two channels is admitted for bring-up and refused for production, which a bare Int cannot express. A design that quietly picked two to save routing effort would be a debug fixture wearing a product's name. The admitted set is the vendor's enumeration, not a range — three and five are unsupported rather than slow, so a range check would admit them and a comment would have to explain why nobody may use them. Every bound is read from the cited package rows, so a correction there moves the admission. Selected: four channels, one DIMM each, four PCIe lanes broken out. THE DIGEST NAMED BYTES THE ROW DID NOT POINT AT. Both the place-and-route and bitstream runs carried the .pcf as their artifact, but nextpnr consumes the synthesized netlist under those constraints and icepack consumes nextpnr's .asc. So the recorded sha256 identified an artifact no reader could reach from the field beside it. Each downstream run now names the input its tool actually consumed and which tool produced it; neither intermediate is retained, and saying so is more honest than pointing at the wrong blob. Fourteen witnesses pass across the three areas. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Contributor
Author
|
Review 51521 fixed, and it was right on all three counts — the irony is not lost that a module whose entire subject is six authorities not collapsing into fewer had itself forked two of them. RE-MINTED ANCHORS: deleted. Both the product-brief and Customer Connect authorities already live in extdeps.cpu.ampere_altra_package, which this module was importing for socket facts while declaring its own copies. One of the two was never referenced at all, so it forked a fact and bought nothing. NDA STANDING: now PROJECTED from altra_reference_board_collateral_standing rather than re-authored. The extdeps module owns the fact, names the four reference boards and cites the access route; this module needed it in its own AuthorityStanding vocabulary, and a projection gives that without a second representation to drift. Also took the non-blocking finding from review 51520 on the simulation receipts, because it was more than prose. Both the place-and-route and bitstream runs carried the .pcf as their artifact, but nextpnr consumes the synthesized netlist under those constraints and icepack consumes nextpnr's .asc — so the recorded sha256 identified bytes no reader could reach from the field beside it. Each downstream run now names the input its tool actually consumed and which tool produced it. Neither intermediate is retained, and saying that plainly beats pointing at the wrong blob. NEW IN THIS PUSH — the ALTRA-MOBO-0 1P minimum design. The datasheet admits 1, 2, 4, 6 or 8 active DDR4 channels and documents one- and two-channel operation as engineering debug and bring-up, so the channel count is selected against a declared INTENT rather than chosen as a scalar: two channels is admitted for bring-up and refused for production. That pair of tests is the point — without the bring-up admission, the wall is satisfied by a rule that merely dislikes small numbers. The admitted set is the vendor's enumeration rather than a range, because three and five are unsupported rather than slow. Selected: four channels, one DIMM each, four PCIe lanes. Fourteen witnesses pass across the three areas. |
Operator P0, and one I had already been shown and declined. A reviewer raised this on the slice that introduced it and I deferred it as pre-existing debt not worth churning an approved PR for. It was not pre-existing: my own slice created the contradiction. Point and Vector fields carried SignedMillimeterComponent — Measure<Length, Milli, Int> — while std.spatial_frame let a frame declare that the same counts mean micrometres. One coordinate, two unit authorities: the type said Milli, the frame said Micro, and the readers extracted the integer and believed the frame. Numerically right, structurally lying — the worse of the two failure modes, because a reader who trusts the declaration is misled while one who trusts the frame has to know not to. SignedFrameComponent carries an Int and no unit. The authority is now one chain: frame identity, then coordinate quantum, then the interpretation of every component in that frame. 169 sites across nine modules; consumers in euclidean_geometry, orthogonal_geometry, orthogonal_topology and the board physical layer are migrated, and their existing witnesses pass unchanged, which is the point — the numbers never moved, only the claim about what they mean. SEPARATELY, review 51530, and it is a good catch. length_scale_is_decimal admitted any Scale whose exponent is Present, which includes Kibi, Mebi, Gibi and Tebi — so a frame could register a BINARY MEMORY PREFIX as its length unit. A kibimetre is not a unit. Worse, those four report 10, 20, 30 and 40, binary exponents sharing a field with decimal ones, so scales_agree would have compared across bases as if commensurate. The comment above that function claimed deriving from the fold was safer than a hand list because a list would rot. The fold was answering a different question. It is now an exhaustive match, which fails CLOSED as Scale grows: a new member does not inherit a verdict from a numeric property it happens to have, it fails to compile until someone decides whether it is a length step. Kilo is admitted beside Kibi's refusal, because a kilometre is a real length — which makes the new witness discriminating rather than a blanket refusal of everything large. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…uld not say Review 51561's second non-blocking note, taken because it is the same carrier shape as the last three findings and I had only half-fixed it. The previous round added RunInput beside the artifact field, so the row said two things: artifact still held the .pcf, and a separate value said the tool had really consumed something upstream. A reader looking at artifact was still misled; I had documented the defect rather than removed it. The single field was the cause. It forced every run to name ONE blob, so place-and-route — which consumes a synthesized netlist AND the pin constraints — had to pick, picked the .pcf, and the bitstream run copied it. With inputs as a list, nextpnr names both, and icepack names the .asc it actually read and carries no retained blob at all. Retained bytes and upstream-produced artifacts stay separate arms because only the first can be compared against what the product emits today. The witness now asserts nextpnr names an upstream input AND consumes the emitted constraints, and that icepack retains nothing — where before it checked two standalone values that sat beside the rows rather than in them. Thirteen receipt witnesses pass. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The conditioning network was not one. The resistor and the capacitor both had terminal 1 on pg_raw and terminal 2 on power_return, so they were parallel across the source: no conditioned node existed, nothing was low-passed, and the digital conditioned_good signal referenced a net that carried the raw rail. It solved in ngspice and reported an operating point, which is what let it pass as a circuit. It is now a 30k/10k divider with the filter capacitor on the divided node, executed in ngspice: pg_cond 3.000 V from pg_raw 12 V at 300 uA through the 40k series total. The digital signal reference now names pg_cond. Two witnesses were measuring nothing and are repaired rather than re-baselined. The operating-point discriminator asserted a current from the superseded single-resistor deck; it now asserts both the divider ratio and the series current, each verified by mutation to fail alone. The SPICE perturbation control named a component literal that the rebuild deleted, so every real component was unbound and the projection refused for a reason unrelated to the perturbation - it now derives the list from the article's own bindings with exactly one standing flipped, and returns to green only when that flip is present. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Neither file is this lane's, and neither was broken by this branch: both carry a trailing annotation block with no declaration after it, which DESIGN 4c refuses because an annotation attaches to a module-scope subject. They were latent because main never compiled them - this branch's std.orthogonal_geometry changes pull both into the compile-clean affected set, and the gate then refuses at the first orphan. rack_mount's block explains why the aperture height is NOT a room-fit relation, so it moves above rack_mounting_aperture_height, which is the declaration it is about. The witness test's block is a deletion note that names its own authority - gunbc.resolved_graph_cache_hand_rust_scaffold - so keeping a copy here is the second representation section 3 refuses; it is deleted rather than reattached to a surviving test it does not describe. Both files' witnesses still pass and the orphan count over the closure is zero. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… gap The repository cited iCE40 LP/HX Family Data Sheet DS1040 version 3.4, October 2017, and carried an unreconciled contradiction against it: a product table saying 98 total I/O and 2 dedicated where the data sheet said 96. Pulled and read FPGA-DS-02029-4.3, February 2025. The document number itself changed - the revision history records "Changed document number from DS1040 to FPGA-DS-02029" - so the stale citation resolved to a real document rather than failing, which is why nothing surfaced it. The current revision states both terms the old one lacked. Its Pin Information Summary gives Total General Purpose Single Ended I/O = 96 and Total Dedicated Inputs = 2 for this column, and 96 + 2 is the product table's 98 exactly. The third inclusion rule was never a contradiction; it was a sum across two rows nobody here had read. It reconciles through a declared projection rather than a restated sum, with a control proving the projection refuses a population it does not admit. The vendor's own per-class decomposition of every bonded contact is carried in full, under its own row names, and it does not cross-foot: the classes the table names sum to 143 against its own Total Count of Bonded Pins of 144. That replaces the old gap as the open item, recorded rather than adjusted, because raising a class invents a contact and lowering the total contradicts a package that physically has 144 leads. The VQ100 column is carried as the control - same rows, same method, cross-foots exactly at 100 - which is what makes the shortfall a property of the document instead of the reading. The differential inputs are excluded from the partition as a recount of contacts already in it, witnessed by the fact that including them overshoots the package. Also: 96 is now confirmed by three independent authorities rather than the two the earlier comment claimed, since the vendor states the total itself rather than leaving it to be added. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…annot hold Table 4.2 Recommended Operating Conditions of FPGA-DS-02029-4.3 is the electrical article's missing authority, and transcribing it as six min/max pairs would have fabricated three facts. VPP_2V5's window depends on the CONFIGURATION MODE: 1.71-3.46 V under slave SPI, 2.30-3.46 V under master SPI and NVCM configuration, and 2.30-3.00 V while NVCM is being programmed. So the mode-free question has no answer, and asking it returns nothing rather than the widest window - which would admit 1.71 V under master SPI, a level the document refuses. The witness asserts both directions on both boundaries, so a table collapsed to one window cannot pass it. VPP_FAST has no window at all. Its row reads N/A with the instruction to leave the pin unconnected, so a min/max record would force inventing two volts where the answer is "do not connect this". MustBeLeftUnconnected is its own arm and admits no voltage, including one comfortably legal on every other rail of this device. And three of the table notes are constraints BETWEEN rails - like-voltage supplies must be one supply, an unused bank's VCCIO goes to VCC, VPP_FAST is left floating - which no per-rail record can carry. They are their own kind, each asserted distinguishable. std.measure gains Millivolt for the same reason it has Micrometer, one axis over: the core window is 1.14-1.26 V, so at volt grain both bounds are 1 and the check stops discriminating entirely. The witness pins that it now discriminates in both directions. Regenerated stage0 and confirmed the fixed point by execution - the second pass ran a binary that contains the change and produced byte-identical output. Also from the review on this PR: contact-population kind equality was decided by round-tripping both kinds through their display strings, so a copy-edit to documentation silently redefined which populations may be compared. It is a structural discriminant now, with a witness asserting the tags are pairwise distinct across every kind - verified by mutation, since the residual risk moved from "a rename changes equality" to "two kinds share a tag", which is decidable by execution where the first was not. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The cited rail windows had no consumer. This is the check, and it is a refusal rather than a report: a rail outside its window is not a warning, it is a board that does not work. Three of the six refusals are not about a single number, which is why this is not a loop over min/max pairs. A rail can sit inside its own window and still be wrong. The bank envelope is 1.71-3.46 V, so a 1.8 V bank rail passes every rail check; a bank driving LVCMOS 3.3 from it is out of spec, because that standard needs 3.14-3.46 V. A board verified only against rails would ship with outputs that do not meet their levels, and the witness asserts that case refuses on the bank cause and NOT on the window cause. Two rails at one voltage on two nets satisfy every window and violate the vendor's like-supply constraint. That is why a rail carries a net identity and not only a voltage: with voltages alone the compliant and the non-compliant design are indistinguishable. The control asserts the same pair at DIFFERENT voltages on different nets is fine, so this is a statement about like voltages rather than a ban on separate nets. And a pin the vendor says to leave unconnected, wired to a perfectly reasonable rail, gets its own refusal instead of a range violation - there is no range, and reporting one sends someone looking for the right voltage when there is none. Omitting it is a declared decision, so an oversight and a choice stop being the same absence. The configuration mode reaches the board check rather than stopping at the authority: the same board is admitted under slave SPI and refused under master SPI, because that mode raises the VPP_2V5 minimum to 2.30 V. Causes accumulate; the count is asserted at three for a board with three independent defects. The positive control is the design this repository is building, and it is verified by mutation - splitting the shared 3.3 V net or dropping VPP_2V5 to 1.8 V each turn it red, so admission depends on the checks rather than passing because nothing fires. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…rphaned Review 51597 is right and the finding is against my own change. Moving std.affine_space to a unit-neutral SignedFrameComponent left the old millimetre-fixed carrier standing in std.measure with its constructors exported and its prose still describing it as the scalar behind Point3 and Vector3. Zero importers remained across dag/; the only Rust reference was the generated seed. That is a second signed-spatial authority sitting beside the frame-owned one - exactly the fork the migration existed to close, added by the commit that closed it. Deleted with its two constructors. The carrier's home is recorded rather than the space left blank, because the deletion is the argument: a coordinate's unit is a property of the FRAME it is expressed in, so a component type hard-coding millimetres asserts one frame's scale for every frame in the corpus, and a board on a half-millimetre pitch and a room in millimetres cannot share it. Nat-backed Millimeter is untouched and not widened - a wall of length -3 m must stay unwritable, and that is a magnitude rather than a component. Also corrected std.spatial_frame's rationale, which described the millimetre-fixed component in the present tense and so asserted a deleted state as current - the same staleness class, one file over. Regenerated stage0 and confirmed the fixed point by execution: rebuilt the binary from the regenerated source and re-ran, byte-identical. 38 witnesses green across the power, supply, physical and rack suites. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Tables 4.28 and 4.29 of FPGA-DS-02029-4.3 carry two facts that are not numbers, and both would have become numbers under a plain transcription. A timing row has a SCOPE. tCR_SCK is a slave-SPI row, so asking a master-SPI board about it is asking about a transaction that board never performs - different from the specification being unknown. The scope shrinks the set a consumer sees rather than sitting decoratively on the row: master SPI sees two rows, slave SPI sees all five, and the witness asserts the inequality so a scope checked by nothing would fail. And the high-frequency tCONFIG values were DELETED by a revision. The change history records removing them for every device, and the surviving note says high frequency is supported only on SPI Master. A withdrawn value is not an absent one: the remedy for absent is to go and read, and the remedy for withdrawn is that there is nothing to read - so reporting it as unknown would invite someone to recover the retired figure from an older revision, which is precisely the wrong move. It is its own arm, and the low and medium figures that survive are asserted beside it. A reading note that changed an answer: Table 4.29 has a condition column between Parameter and Min, so tCRESET_B's 200 ns sits in the MINIMUM column. Read one column left it would have been a typical, and a design built to a typical where a minimum is required meets the specification on average and violates it intermittently. The column is carried on every bound so a consumer wanting a guaranteed value can refuse a typical rather than silently accept it. This was checked against the table's cell alignment rather than inferred from the parameter's name. SPI_SS carries this revision's spelling; SPI_SS_B names a signal in a superseded document, the same staleness class as the retired document number. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…e fork Review 51598 caught the defect this PR spent its length enforcing against: the configuration timing carried value: Int beside unit: NonEmptyStr holding "ns", "us", "MHz" and "clock cycles". A unit written in a name is a unit no consumer can read, so a nanosecond and a megahertz were one type and comparing them typechecked - which is word for word what the sibling module in the same directory says about package dimensions. The excuse was that the rows genuinely differ in kind. Rows differing in kind is the definition of a coproduct, not a licence for a string, and every carrier it needs already existed in std.measure: Nanosecond, Microsecond, Hertz and Millisecond. Nothing new was minted. The clock-cycle row is deliberately NOT a Measure. Forty-nine cycles is a cardinality like the package contact count, and how long they take depends on a clock this table does not name - so a duration there would be an invented fact rather than a converted one. ConfigurationTimeTypical carried a bare Int milliseconds and is now Millisecond, same class, same fix. The new witness asserts each row lands on the arm its kind requires, so a bound that fell back to a permissive representation would red rather than being carried unread. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Review 51599's third finding is correct and merge-blocking: supply.dag and configuration.dag each declare extdeps_model_scope but neither joined scope_carrier_paths, so the per-PR placement gate would refuse them. Only subject.dag was enrolled when the directory was created. Both added. Censused every dag/extdeps file this PR touches against the frontier rather than fixing the two the review named - all five are enrolled now, which is the check the review's finding is an instance of. The review's other two findings were the flat-scalar timing units, already fixed in 155204f; that review ran against the preceding head. The current tree has no unit-bearing string and no unit-in-a-field-name on any of these rows. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…rred twice Review 51600 flags scope_admits comparing configuration modes through their display names. It is right, and a census over this lane found the same shape a second time in power_distribution's rail_is - so this is the third and fourth instance of one defect in this PR, after contact_population's kind equality earlier. The failure is always the same: equality decided by round-tripping both members through a name meant for humans, so editing documentation silently redefines the relation and two members can be fused by a copy-edit. Here it decides whether a board's rail matches a device requirement and whether a timing row is in scope for a configuration mode, which is not a place for a relation a proofreader can change. Both now read a structural discriminant with no other job - not displayed, not parsed, not ordered - behind an exhaustive match, so a new rail or mode cannot be added without receiving one. The residual risk moves from "a rename changes equality" to "two members share a tag", which is the better failure because a witness decides it by execution; verified by mutation, collapsing two mode tags reds both new controls. The census is the part worth keeping: grep for the shape across the lane rather than fixing the one occurrence the review named. It found the second. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… looks Self-census of the discriminants added in af26f0a. All three rosters are complete against their coproducts today, checked by counting variants against roster entries against tag arms - but that is a snapshot, and the asymmetry underneath it is structural. The tag match is exhaustive, so the compiler refuses a new member with no discriminant. The roster the witness walks is hand-maintained and enforced by nothing, so a seventh rail added without joining it would leave the witness walking six, passing, and saying nothing about the seventh. The guarantee is therefore "every member the roster names has a distinct tag", not "every member has one" - and the second is what a reader assumes unless it is written down. Recorded rather than papered over, because the available patch does not work: a contiguity check on the tag range fails to catch it, since an unlisted member takes the next tag and leaves the listed range intact. Closing it needs the language to enumerate a coproduct's members. The class is mechanically preventable for tag assignment and unguarded for roster membership, and the carriers now say so. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…nits Review 51606 is correct on both counts, and the first is the serious one. Making Vector3 components unit-neutral moved the quantum onto the frame, and std.orthogonal_geometry was migrated to read extents through the registry - but std.euclidean_geometry's metric operations were left asserting millimetres on their results while consuming counts whose meaning the frame now owns. On a micrometre-registered board frame, norm3 of a thousand-count axis vector returned millimeter(1000): arithmetic that is right, a label wrong by a factor of a thousand, and nothing in the result that looks suspicious. That travels further than an error. dot3, norm_squared3, norm3 and the three composites over them now take the registry and REFUSE a frame whose quantum they cannot label, through a new MillimetreFrameRequired relation. An unregistered frame refuses too - no declared quantum means no unit to check the label against, and assuming the default is the convention this layer exists to remove. Refusal rather than derivation, deliberately and not for expedience: the length half could derive through FrameExtent today, but the area half needs a frame-relative area carrier that nothing in the corpus consumes, and inventing a concept ahead of its consumer is the speculation DESIGN refuses. The derivation is named on the carrier as the next rung. The control is the wall: a micrometre frame refuses, the SAME vector in a millimetre frame answers 1000 mm, and an unregistered frame refuses - so the frame decides the outcome rather than the operation refusing everything. Verified by mutation. Second finding: spatial_frame_note still described the millimetre-fixed component in the present tense, one row below an inline comment that had it right. Corrected. That is the third stale-prose fix in this PR and they share a shape - prose describing a state the same commit deleted. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Review 51607 is right, and this is the third consecutive REQUEST_CHANGES on one migration - so this time I censused every function in the file that puts a millimetre label on a result instead of patching the one named. cross3 was the remaining hole, and it is worse than the scalar cases it was grouped with rather than equal to them: it labels THREE components in square millimetres, so an unguarded micrometre frame mislabels a whole vector at once and each component then travels independently. It now takes the registry and refuses through the same MillimetreFrameRequired relation, with the control asserting a micrometre frame refuses and the same operands in a millimetre frame answer 1000000 mm squared. Verified by mutation. The census leaves exactly one labeller without a guard, area_vector3_from_checked, and that is the correct scope rather than a miss: it has one caller, cross3, which checks the frame before reaching it, and no module imports it. That reasoning is now written where the next census will surface it, with the condition under which it stops holding - a second caller or leaving the module. The pattern across these three rounds is the finding: I migrated the callers I was looking at rather than the ones that exist. The census is cheap, it is what closed this, and it should have run when SignedFrameComponent became unit-neutral. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Review 51609 named prism3_height, and it was right - but the finding I take from three consecutive rounds of this is that fixing the named function is what kept producing another round. So this censused every function in the corpus that puts a millimetre-family label on a value derived from frame-owned counts. prism3_height was the last DIRECT one, and it now answers in the frame exactly as rectangle2_width and rectangle2_height do. But the census as first written missed three more, because they label transitively rather than calling the component reader themselves: loop2_area, space_floor_area and space_volume multiply frame counts and spell the product in square and cubic millimetres. On a micrometre frame that is wrong by a factor of a million. Those refuse rather than derive, through a new MillimetreFrameRequiredForMetric cause, for the reason euclidean_geometry refuses: there is no frame-relative area or volume carrier for them to answer in, and inventing one ahead of a consumer is speculation. The registry threads through space_height, space_volume, complex_total_volume and world_total_volume to the product layer. Also fixes the CI red at f62fc5f, which was mine and unrelated to the above: the corpus mandatory-tag wall requires every extdeps module to declare its own extdeps_external_authority_anchor, and the two new iCE40 modules imported the subject module's instead. Binding to a shared value was tried first and refused, which is a fact about the wall worth recording rather than working around silently: it projects the anchor's scheme out of the declaration's own Node tree, so an aliased anchor reads as absent and the module reads as uncited. The three modules therefore each carry the record, and the note says why a shared binding cannot discharge a structurally-read citation duty. Controls: a micrometre frame refuses on the area fold and the same space in a millimetre frame answers; an unregistered frame yields no extent at all. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Review 51623 is correct: space_height_millimetres answered millimeter(count: 0) when the extent could not be projected or the frame was unregistered, and space_volume multiplied an area by that zero - so a space whose height nobody could state reported a volume of nothing. That is the absorbing fallback in its most deniable form: a number, in the right unit, and the one value least likely to be questioned for an empty-looking result. The comment above it claimed the projection refused exactly, which is how it survived being written. Both arms are typed refusals now. THEN THE CONTROL I WROTE FOR IT PROVED NOTHING, and that is the more useful finding. It asserted the volume path refuses through the height projection; mutating BOTH height arms back to fabricating zero left it green. space_volume consults space_floor_area first, and that guard refuses on exactly the frames that would break the height projection, so control never reaches the arms the control claimed to exercise. The witness now states what it establishes - a volume over an unlabelable frame refuses - and the module records that the height arms are defensive for a future direct caller rather than executing checks. Re-verified by mutating the guard that does fire, which reds it. Merged main. Two conflicts in std.affine_space, both additive - main's projection vocabulary (OpProjectPoint3, ProjectionSourceFrameRequired) and this branch's metric vocabulary (OpNormSquared3, OpNorm3, MillimetreFrameRequired) - unioned. std_measure.rs is generated, so it was regenerated rather than hand-merged, rebuilt, and re-run to a byte-identical fixed point. Main's new std.planar_projection imported signed_millimeter_component_count, which this branch deletes, so the merge broke it: migrated to signed_frame_component_count. Its 15 witnesses pass. That is the cost of deleting a std carrier while a sibling lane adds a consumer for it, and it was invisible until the merge. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Review 51633 names product.spatial_edit and product.spatial_projection, both still importing and calling signed_millimeter_component_count from std.measure after this branch deleted it. Correct, and they would have failed whole-tree resolution. The reason they survived is worth stating: I migrated std.planar_projection one round ago because the merge broke a suite I happened to run, and I never censused the corpus for the deleted symbol. So the fix reached the consumer I tripped over rather than the consumers that exist - which is the third time in this PR that fixing the named thing produced another round. This time both censuses ran. A grep for the deleted symbol across dag/ and src/v2 found exactly these two modules and nothing else. A second census checked EVERY call site of EVERY signature this branch changed - dot3, cross3, norm_squared3, norm3, distance3, distance_squared3, closer_than3, normalize3, prism3_height, space_height, loop2_area, space_floor_area, space_volume, complex_total_volume, world_total_volume - for a missing registry argument. It found one real site, in spatial_edit's witness, plus one false positive inside a comment. Both censuses now read clean. Verified by compiling the spatial_edit closure rather than by running the suites that happened to be nearby: that is the check which would have caught all three rounds of this at once, and it is the one I should have run when the carrier was deleted. spatial_edit 9, spatial_projection 8, spatial_placement 13, planar 15. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
# Conflicts: # dag/product/rack_mount.dag # dag/std/affine_space.dag
…d of restating them The emission-entry witness hand-authored the board's net topology. The divider rebuild moved the name "pg_cond" from the COMPONENT population to the NET population, so the fixture went on naming something real while naming the wrong kind of thing: its nets referenced a component that does not exist, the article stopped being admitted, and w_a_target_that_cannot_render_reaches_the_target_arm and w_the_same_board_still_emits_for_a_target_that_can_render_it stopped measuring the target arm at all — they failed against the admission arm instead. That is the fixture measuring nothing, not the fixture disagreeing. Both fixtures now derive their nets from power_interlock_article.analog.nets and drop exactly one terminal, so a topology change flows through rather than silently stranding a copy. The simulation-receipt witness carried the identical copy and was still correct by luck; it is derived too, because the shape is the defect. Each file also gains w_the_floating_fixture_actually_floats_exactly_one_terminal, which executes the fixture's own premise. Mutation-verified: breaking the drop predicate fails the guard AND the target-arm test, while the Verilog test correctly stays green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ed and inert
review 51692 (cursor) found UnusedBankSupplyGoesToCore folded into power admission
with an arm returning [] unconditionally. It is enrolled beside two constraints that
do refuse, so power_causes read as three enforced vendor constraints where only two
could ever fire, and a board violating the unused-bank rule was ADMITTED. That is
rung inflation: enrollment presented as enforcement.
The root cause was in the model, not the check. BankAssignment carried a mandatory
standard, so an unused bank could not be expressed at all — no input could reach the
constraint, which is why the arm had nothing to do. Modeling it is therefore the fix
rather than deleting the fold entry: BankUse = BankDrivesStandard { standard } |
BankUnused, and bank_causes checks the window only where a standard exists.
The arm now folds the bank population and refuses an unused bank whose VCCIO does not
share the core rail's net, taking the core rail from the constraint ROW so the vendor
roster stays the authority. An unused bank whose core rail was never built refuses as
its own cause rather than leaning on the rail side, because a board may declare core
deliberately unconnected and silence that one — an unanswerable constraint must not
read as a satisfied one.
Three witnesses execute the arm in all three directions: tied-to-core admits, not-tied
refuses, missing-core-rail refuses. Mutation-verified — neutering either refusal path
reds its test while both positive controls stay green.
Censused the same shape across the board modules. Every other empty arm is honest and
falls into one of two kinds: covered elsewhere (PinLeftUnconnected on the rail path,
the refused-extent arms in physical.dag) or making no claim about the subject being
checked (chassis bonds against the analog intent, preconditions with no board signal).
Both now say so where it was least obvious.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 13, 2026
Merges main through 3c533ba rather than through its tip. #8228 landed at 9c5d007, so this drops the BL-0 files this branch was duplicating and reduces the diff to the BL-2 work alone. It deliberately stops one commit short. #8214 (9156b78) introduced in-body source annotations across 13 files, confirmed by compiling dag/std/affine_space.dag against the live tree, so merging main's tip today would import a known compile-clean red into a branch that is currently green — turning an unrelated lane's defect into this PR's failure. 3c533ba is the newest main commit whose tree carries neither the in-body nor the unattached annotation form. The remainder of main merges once that class is repaired.
This was referenced Aug 13, 2026
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 13, 2026
Move indented // comments in PCB substrate modules and witnesses to module-item grain so dag_compile_clean_gate_passes can green after merging #8214. Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls
pushed a commit
that referenced
this pull request
Aug 13, 2026
* Move the ice40 NVCM-rail annotation to module-item grain DESIGN 4c admits standalone leading // blocks attached to module-scope declarations; an annotation inside a declaration body refuses. #8214 landed one inside rail_requirement's match, and the compile-clean gate reds on it -- main and every PR built on it, since PR CI evaluates the merge ref. The prose is preserved rather than deleted: it explains why the NvcmProgrammingSupply arm answers none, which is a real modelling fact (absent means ask-with-a-mode, not unknown), so it moves above the declaration and names the arm it is about. The file already carries six annotations correctly at that grain. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Move all 87 body-grain source annotations to module-item grain DESIGN 4c admits standalone leading // blocks attached to module-scope declarations; an annotation inside a declaration body refuses, and the compile-clean gate reds the whole tree on it. Main is red, and so is every PR that merges with it -- PR CI evaluates the merge ref. The first revision of this PR moved ONE of them (ice40 supply). That was the first file the gate happened to name, not the population: the same run also reported 'truncated hard diagnostics at 20; 87 total'. A census over dag/ and src/v2/ finds exactly 87 across 12 files, all from the recent spatial/PCB lane, which matches the gate's own count. Every block moves above the declaration that contains it. Nothing is deleted: the diff is 87 insertions and 87 deletions, and each file's comment-line count is identical before and after -- the prose carries real modelling rationale (why an arm answers none, why an area vector is not a displacement vector, why a metric operation refuses an unlabelable frame) and deleting it to green a gate would trade the rationale for the check. Verified by execution rather than by parse alone: witnesses in the edited files still resolve and pass. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Fix hoist provenance for test fn, and consolidate two duplicated blocks review 51790, three findings, all real and all mine. PROVENANCE BUG, and it was in my script rather than a judgement call: the declaration regex matched fn|func|data|type|service at line start, so a block inside a 'test fn' body attached to the previous PLAIN fn instead of its own declaration. In compute_board_physical_witness_test that moved a note about counting two distinct defects onto refuses_naming, which does not count anything. The regex now recognises 'test fn' and every block re-hoisted from the pre-move state; the counting note now sits above w_one_defect_is_reported_once, merged with the block already there. DUPLICATED RATIONALE: in affine_space two hoisted blocks restated prose already present above the same declaration -- the OpProjectPoint3 nicknaming argument on SpatialOperationIdentity and the asymmetric-projection argument on SpatialFrameRelation. Stacking a second copy is the redundancy the migration was supposed to be neutral about, so the redundant copy is deleted and the fuller pre-existing block kept. This DOES delete 7 comment lines, unlike the previous commit which was a pure relocation -- the PR body is corrected rather than left claiming otherwise. Every other file's comment count is unchanged. A shingle scan over the five hoisted non-test modules found no further duplicate stacks. Re-verified by execution: w_one_defect_is_reported_once, w_a_repeated_placement_identity_refuses, affine_space_witnesses and w_metric_operations_refuse_a_frame_they_cannot_label all pass. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls
pushed a commit
that referenced
this pull request
Aug 13, 2026
… can complete The earlier merge deliberately stopped at 3c533ba, one commit short of #8214, because that commit put in-body source annotations across 13 files and merging main's tip would have imported a known compile-clean red. #8235 moved all 87 body-grain annotations to module-item grain and main now carries none, so the reason for stopping short is gone and this takes the remainder. Recorded because the earlier stop was itself declared: a branch that resumes a partial merge should say what condition cleared, not silently catch up.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Consolidates #8205, #8206, #8209 and #8212, which were a linear stack; this branch already contained all of them. Merged with main. Those four are closed in favour of this one.
The lane started as "put one admitted board article in front of a fab" and ended somewhere more useful: the board forced two substrate repairs, and an operator ruling then redirected the product from an RC fixture to the actual Altra motherboard. What survives is substrate plus a real device binding.
Device binding, proven by execution
Lattice iCE40 and Project IceStorm land as INDEPENDENT authorities — one is a vendor specification, the other a reverse-engineering of it, and fusing them would make a Chrome change require editing Safari's module. The pin chain reads its port spelling FROM the Verilog binding, so the constraint file and the module declaration cannot disagree. Seven refusal causes, each with a discriminating red.
The end of that chain is not a claim: model-generated Verilog and PCF through yosys, nextpnr-ice40 and icepack produce a 32,220-byte bitstream. Simulation says the logic behaves; this says it FITS a device.
The two-authority pin population agreement (Lattice's per-bank 23+25+20+24+4 against IceStorm's 96 designators) is DERIVED, not pinned — and a witness asserts the roster's 96 are 96 distinct designators, without which the agreement is arithmetic rather than evidence.
Board-scale geometry — the unplanned half
A TQ144 sits on 0.5 mm pitch, and the whole spatial stack was hardwired to whole millimetres. Two adjacent pins collapsed onto one coordinate: not lost accuracy, lost DISTINCTION.
std.coordinate_framedefers a frame's facts to "whatever registers frames"; nothing did.std.spatial_frameis that registrar, and the first fact it carries is the frame's length unit. The scale is a VALUE, not a type argument — that is not a shortcut but the patternstd.coordinate_framereached by measurement, since the seed's judge discards applied type arguments (which is how aPoint3<RoomFrame>minus aPoint3<BuildingFrame>compiled clean and returned 9).Projection REFUSES rather than converts, in both directions. 500 um asked for in millimetres rounds to 0 or 1, both wrong invisibly. 3 mm asked for in micrometres is exactly 3000 and loses nothing — refused anyway, and pinned by its own test, because the moment it answers the easy direction it is a unit converter and the caller received one as a side effect of asking what something measures.
The geometry carriers turned out to be scale-agnostic already; only the READERS committed to millimetres. So the guard was one file, not the wide migration expected. The asserting readers are deleted rather than kept beside the deriving ones.
Package-body placement, and what it is not
The article's physical standing held its outline as a
NonEmptyStr— a shape nothing can intersect or measure. It is now real geometry with containment and collision.It is NOT a footprint. A footprint is a land pattern: numbered pads, a contact-to-pad map, mask and paste apertures, pin-one, courtyard.
RequiresPackageFootprintAuthorityis RETAINED. The success arm isBodyEnvelopesAdmitted, notPhysicallyAdmitted— the latter claimed physical realizability when nothing had looked at a pad. And the under-approximation is stated at the carrier: a TQ144's leads span 22 mm against a 20 mm body, so a body-only collision check ADMITS boards that cannot be assembled.ALTRA-MOBO-0: the attachment stack
Six independently governed identities between die and board: processor package, socket, socket board termination, board land pattern, loading mechanism, mounting.
The error made unwritable is deriving the board land pattern from the processor package's bottom-land geometry. Both are 4926-land grids at the same pitch and the package drawing is in a datasheet already cited here — so the conflation is tempting rather than careless. They are opposite sides of the socket, and a board built on the first is a board where nothing solders. The wall is an ABSENCE: no function takes a package and returns board pads. Only the POPULATION crosses.
Authority standing is three categories plus one.
Unresolvedmeans nobody has looked yet — recording that as NDA-gated invents a wall and stops anyone looking, and this repository already made the reverse error, declaring the public Altra pin map NDA-only from reference-BOARD collateral and defending it with a passing witness.PublicButRedistributionUndecidedseparates where bytes may live from what we may know: no contact row is hand-copied into this public repo, while the schema and completeness machinery are built. Zero attachment layers are NDA-gated, asserted by count.Three defects caught by counting, not naming
Worth flagging as a pattern rather than three incidents. Each passed a test asserting WHICH refusal fired and failed one asserting HOW MANY:
emit_pin_constraints_forinstantiated at a single refusal instead of the refusal SET, so a board with two defects crossed the host boundary carrying one;a.identity < b.identity, silently skipping every pair sharing an identity — two parts stacked at identical coordinates were reported as a naming defect and never as the collision they also are.Two further defects arrived from outside the diff and were invisible from inside it:
Micrometerlanded on main independently (reached via EIA-310's 44.45 mm rack unit), and a helper I wrote already existed indigital_control.Witness inventory
Pin chain 13, physical 10, attachment stack 7, spatial frame 7, geometry 10 (2 new discriminating), emission entry 6 (1 new), simulation receipts 12. All green by execution.