Repository navigation
Conversation
gunbai-bot
Bot
changed the title
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>
Contributor
|
Review 51478 — both findings fixed in ff48fff. Finding 1 (blocking, unit modeling). You were right and the fix is a std addition rather than a local one. Ice40Package now carries body_width, body_height and contact_pitch as Micrometer, a new alias in std.measure directly beside Millimeter — same Length quantity, one finer decimal step. It needs to exist because a 0.5 mm pitch is not expressible in whole millimetres and Millimeter is Nat-backed; it is a scale argument on the axis that already exists, not a second length authority. contact_count stays Nat, which I believe is correct: it is a cardinality, not a length, and giving it a unit would be the mirror of the defect you found. Finding 2 (non-blocking, duplicated refusals). Confirmed by execution before fixing: assignment_refusals recomputed uniqueness inside the per-assignment walk, so two assignments on one pin filed two identical PinAssignedToSeveralSignals causes. Nothing was missed, but pin_refusal_set_count then measured how many rows touched a defect rather than how many defects there were, and that is a number a later consumer reads as a population. Collisions moved to their own scan reporting each at its first mention in source order. The two new witnesses count rather than name, because the existing tests named the cause and passed in both worlds. Both axes are asserted separately — a deduplication that ran only on pins would pass the doubled-pin test and still double-report a doubled signal. Twelve tests pass; the three touched modules compile with annotation noise only. |
…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>
Contributor
|
Thanks — took the non-blocking finding, and it turned out narrower than the review framed it, which is what made it worth fixing rather than inheriting. You read emit_pin_constraints_for dropping cs.rest as BoardEmission carrier debt shared with the SPICE and Verilog entries. R is a parameter, though, and SPICE and Verilog genuinely produce one cause each — their instantiation was right and the carrier was never the problem. The pin chain produces a SET, and I instantiated it at PinChainRefusal. So it is a wrong type argument, not a carrier limitation, and it fixes without touching BoardEmission at all. The consequence was worth closing: 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 — absent, with no way for the caller to learn it existed. Why nothing caught it: the admission arm already had a witness proving its causes cross intact, and the target arm had no mirror. It does now, planting exactly two defects and counting. Matching the arm passed before and after; the count is the part that moves. |
…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>
Contributor
|
Review 51488 — all three findings addressed, plus the CI red they sat next to. FUSED OBSERVATIONS: fixed, and it was worse than the review found. 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. A test then asserted the place-and-route observation contained the synthesis cell count AND the bitstream size — the fusion enshrined as the contract, which is why nothing caught it. 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. ORPHAN HELPER: wired rather than deleted, because it answers a question this PR depends on. The vendor-and-toolchain agreement compares 96 against 96, which 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. roster_pin_occurrences now backs a witness asserting every designator appears exactly once. WIKIPEDIA CITATION: agreed, and it is weak in the specific way that matters here — a legal name is the one fact a registrant states about itself under obligation, so a secondary source is a description of the authority rather than the authority. It now cites EDGAR submissions for CIK 0000855658, the same endpoint the SCM issuer rows already reach (LSCC, SIC 3674, Delaware). One note worth recording: EDGAR's own name field reads LATTICE SEMICONDUCTOR CORP, an index normalisation to upper case with a truncated suffix. 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. CI: the red was mine and unrelated to the review — adding Micrometer to std.measure made the generated std_measure.rs stale. Regenerated with regen_stage0 rather than hand-edited; the diff is the expected two lines. |
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>
Contributor
|
Review 51498 fixed, and the build red turned out to be a second single-authority violation that arrived by a different route. FORKED HELPER — correct, and worse than a near-duplicate: intent_declares was byte for byte the same fold over the same signals with the same equality as intent_declares_signal in digital_control, which admission and verilog_projection already consume. Deleted; the existing one is imported and called. Thirteen pin-chain witnesses pass. THE BUILD RED, since it is related. Micrometer landed on main while this branch was open, reached from a completely different direction: EIA-310's rack unit is 44.45 mm, so any quantity derived from a rack unit count is inexact at millimetre grain and exact at micrometre grain. Same carrier, same declaration, same Length axis — so the merge produced two pub type Micrometer in one generated module and the crate stopped compiling. Mine is deleted and main's kept. I folded my reason into the surviving comment rather than dropping it, because two unrelated subjects independently needing one decimal step finer is precisely what shows this is a scale argument on the Length axis rather than a rack-specific convenience — that is worth recording once, next to the declaration, instead of twice as two declarations. Package dimensions now use main's micrometer / micrometer_count constructor rather than a raw record literal. Regenerated per the generated-artifact gate's own instructions rather than by picking a side, and both passes were run: the first runs a binary that predates the change it emits and can self-verify at divergence 0 for the wrong reason. Second pass reports regen_divergence_count=0. |
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>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 13, 2026
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>
This was referenced Aug 13, 2026
Contributor
|
Consolidated into #8214 at the operator's request. These four were a linear stack and the tip branch already contained every commit from all of them, so nothing is lost by closing here — the same commits are in #8214, now based on main. Worth stating the cost plainly rather than letting it pass silently: this discards the approval tally these PRs accumulated. The combined diff is a different subject from any one slice and needs reviewing as one, so those approvals were not transferable in any case. Closing this one; review continues on #8214. |
briansrls
pushed a commit
that referenced
this pull request
Aug 13, 2026
…nd the attachment stack (#8214) * Slice 1: one signal, one pin, one chain — and a bitstream at the end of it * Ground the package dimensions in Measure; report a pin collision once 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> * Register what a coordinate frame's numbers mean 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> * Instantiate the pin-chain emission at its refusal SET, not its first 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> * Read a 2D extent in the frame's unit rather than asserting millimetres 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> * Split fused tool observations; reground the vendor on EDGAR; regen stage0 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> * Assert the extent count, not only that the wrong unit refuses 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> * Model the board as a shape, and check the two questions a layout must 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> * Declare the vendor module's model scope and enrol it as a carrier 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> * A package body is not a footprint — name it for what it is 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> * ALTRA-MOBO-0: six attachment layers, six authorities, one that must not 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> * Consume the Ampere authorities; select the 1P minimum; name real tool 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> * The frame owns the quantum: make the coordinate scalar unit-neutral 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> * Type the contact populations so unlike counts cannot compare The pin-population agreement I put forward as evidence was a coincidence wearing the shape of a join. It asserted bank_population_total == roster_pin_count: 92 general-purpose plus 4 configuration contacts against Project IceStorm's 96 placeable positions. Both sides really are 96 and the comparison really executed — which is what made it the dangerous kind of evidence, because nothing anywhere stated that those two totals count the same THINGS. Lattice's current product table describes the same device and package as 98 total I/O plus 2 dedicated I/O, which is 100 by a third inclusion rule, so at least one of the three counts something the others do not. A bare Int == Int cannot notice any of that. It is the cross-family comparison this repository already closed for content hashes, reappearing wherever two numbers happen to share a type. Populations are now kind-tagged, and comparison across kinds is PopulationsNotComparable rather than false — a false would claim the device disagrees with itself, when the truth is the question has no answer until someone states the projection. Different states, different remedies. The projection is now a DECLARED claim: IceStorm's placeable roster is asserted to comprise the vendor's general-purpose bank contacts plus the configuration contacts, with the reason given. That assertion can be wrong, and being wrong is the point — it is a statement about the world a later document can refute. The previous form asserted nothing and so could not be contradicted by anything. The unresolved 98-plus-2 count is carried as an open gap rather than omitted, together with the note that the 2017 family data sheet cited here is superseded by LP/HX v4.3. Leaving it out would let the 96-to-96 agreement read as though nothing else were known. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Decompose the population gap into typed rows Modeling-coherence violation: PopulationGap.unresolved was a bare primitive nicknaming a concept, and the check is right. That field held three separate facts in one sentence — a conflicting count, the authority stating it, and the fact that our own citation is superseded. A paragraph can be read by a human and by nothing else: no consumer can ask which population disagrees, or by how much, or whether the citation is current. The gap now speaks the same vocabulary as the agreement it qualifies. Reconciled and unreconciled are both List<ContactPopulation>, so 98 total I/O and 2 dedicated I/O are rows with kinds, counts and authorities rather than words inside a string. VendorTotalIo joins the kind coproduct because that is what the conflicting figure counts. Citation currency is its own coproduct rather than a remark: the cited DS1040 version 3.4 from October 2017 against the current version 4.3, so "our source is stale" is a value a consumer can test instead of a sentence someone has to read. The witness now asserts the gap is open, the citation is not current, and the unreconciled set contains a vendor-total row of 98 — three checkable facts where it previously grepped a substring out of prose. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * The NDA access route is an authority, not a sentence Review 51552, and the swap it found was real: the projection bound the actual access_route ExternalAuthority, discarded it, and put the subject label into the route field. A consumer asking WHERE to obtain the reference-board collateral received a description of WHAT it is. The fix is the carrier rather than the variable. NdaGated typed both fields NonEmptyStr, which is exactly why the swap typechecked — two strings side by side, nothing to distinguish a subject from a route. access_route is now ExternalAuthority, so putting a subject in it does not compile, and the same correction flows through NeedsCommercialAccess. The hard-coded holder is deleted rather than corrected. The upstream standing carries no holder field, so it was a fact invented at the projection, and the access authority already identifies who holds the collateral. The witness now checks both fields and checks the route AS an authority, which is what makes the swap unwritable rather than merely absent today. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * A run's inputs are a list, which is what the single artifact field could 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> * Make the power-good article an electrically coherent divider 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> * Re-home two orphan source annotations the widened compile scope exposed 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> * Refresh the iCE40 authority to the current revision, which closes the 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> * Model the iCE40 supply rails, whose table has three shapes a window cannot 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> * Check what the board supplies against what the device requires 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> * Delete SignedMillimeterComponent, the authority this PR's migration orphaned 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> * Model the configuration port, including a value the vendor withdrew 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> * Type the configuration timing quantities; the unit string was the same 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> * Enroll the two new iCE40 extdeps modules on the scope frontier 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 155204f22; 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> * Ground rail and mode equality structurally; the prose comparison recurred 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> * State what the distinctness witnesses cover, since it is less than it looks Self-census of the discriminants added in af26f0ad0. 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> * Close the 3D metric half of the frame migration; it was lying about units 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> * Guard cross3 too, and census the file rather than fix the named function 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> * Census the whole frame-migration surface, not one file at a time 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> * Migrate the last two consumers of the deleted accessor, found by census 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> * Derive the floating-terminal fixtures from the production nets instead 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> * Make the unused-bank vendor constraint refuse instead of being enrolled 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> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
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.
First PR of the PCB-MVP-0 stack. It selects a real programmable device and makes the pin chain — logical signal → Verilog port → constraint → package pin — a checked join rather than a string typed into several files. The chain ends in a bitstream, produced by executing the real toolchain on the model's own output.
The chain, executed
Both inputs came out of
gunbc run, not out of my editor. The pin constraints are byte-pinned in a witness.Device: ICE40HX1K-TQ144
Chosen against the brief's criteria and recorded as to why: non-BGA (144-pin TQFP, 20 × 20 mm, 0.5 mm pitch), public datasheet, and carried end to end by a fully open synthesis / place-and-route / bitstream chain. No NDA fact is required to design with it.
Two authorities, deliberately not fused
These are a specification and a reverse-engineering of it, so they get separate modules. Modelling one as the other is the same fusion the SPICE-medium/ngspice-runtime split already avoids.
The full pin assignment table is deliberately NOT transcribed. It is thirty-odd sheets of a copyrighted vendor document, and this repo is public; what the design actually needs for placement comes from IceStorm, which is licensed for it. The Altra module already records this distinction being got wrong once.
A cross-authority join falls out and is executed: Lattice's per-bank table gives 23 + 25 + 20 + 24 general-purpose plus 4 configuration pins; IceStorm's roster carries 96 designators. Two independently produced sources agreeing on a population — derived on both sides, so it cannot be kept true by editing one.
The copied string this makes impossible
The constraint's port name is read from the Verilog binding table, not authored here. There is no field in the new module that could disagree with the module declaration. The discriminating control respells one port and asserts the constraint file moves with it — if the two were independently authored, that test passes while the real design places a port the module never declares.
Seven refusals, each a defect that otherwise produces a working-looking artifact: a pin the package does not have, two signals on one pin, one signal on two pins (an ambiguity a fold would resolve by authoring order), a bound signal the article never declared, a signal with no target spelling, an unemittable constraint — and the one that needs the opposite walk, a declared signal with no pin at all, which no walk over assignments can see and which would otherwise leave the tool free to place a port wherever it liked. Four unassigned signals produce four causes, not one.
Stated bound, because it is invisible otherwise
The roster answers whether a package position is placeable. It does not say whether that position is one of the four configuration pins — per-pin function lives in the table I am not transcribing — so a binding onto a configuration pin would pass this check. The four pins in the production table were not read off a page: place-and-route was executed against them and accepted them, and that is the only evidence this repo currently has that they are ordinary I/O. Closing that gap needs per-pin function facts, not a stricter predicate over the facts already here.
Rung
Not in this PR
Board geometry, footprints, pads, routing, manufacturing artifacts. Those are the next PRs in the stack — this one stops at the device and the pin chain.