Repository navigation
ALTRA-MOBO-0 board population + ALTRA-WORLD-0 PcbWorld/SVG (#8253): named DDR channels, composed geometry, design identity - #8233
Conversation
…e cited and refused where it cannot Placing a component requires its body envelope, and a body envelope is a VENDOR fact. The part is whatever size the vendor made it, so a dimension chosen because it looks about right is the fabricated plausible output DESIGN section 5 forbids, in its most dangerous form: a layout built from invented numbers passes every geometric check, draws convincingly, and cannot be assembled. One asymmetry makes this increment possible before the mechanical sources are settled. The board's frame and outline are OURS — how big we make our own board is a design decision, not a claim about anyone's document — so they are authored. The envelopes are not ours, so they are cited or they are obligations. There is no third arm carrying a provisional number, and that absence is the construction: a placement cannot be built from a guess because a guess has no representation here. Established today: one envelope, the iCE40 TQ144 board-control CPLD, read from the package row this tree already cites rather than retyped. Outstanding: thirteen, each a typed, counted obligation carrying its own cause. The two gaps are deliberately not one gap. The Altra package's mechanical data IS published (datasheet section 3), but every page is footed Ampere Computing Proprietary, so transcribing it into a PUBLIC repository is a licensing question rather than an availability one -- RedistributionUnresolved, the same distinction attachment_stack already draws between Unresolved and NdaGated. The sockets, flash, clock, reset, power controllers and endpoints have no selected part, so there is no document to consult at all -- VendorSelectionNotMade. One is answered by a lawyer and the other by an engineer; collapsing them into a single absent sends both to whoever reads it first. Completeness is an identity join over roles derived from the design, not a count: eight channels demand eight memory slots without editing this module, and both directions are walked, since a missing role is an unbuilt board while an extra component is a part nobody justified. Role equality is structural and includes the channel. altra_reference_plan returns an OrthogonalConstruction. An earlier draft answered a refused outline with a degenerate one-micrometre rectangle to keep the return type simple, which is the absorbing fallback exactly: every component would then have been reported outside the outline and the real cause replaced by a dozen plausible ones. Ten witnesses, green by execution. Mutation-verified in two directions: neutering the envelope refusal reds the refusal and count claims, and dropping the channel from role equality reds the slot-distinctness claim and stops a spurious channel-7 slot from being reported as unjustified. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
review 51737 flagged role_channel's -1 sentinel for non-memory roles, with roles_equal then comparing tag string AND channel. It worked only because the tag gated the number, and it contradicted the module's own note warning against equality through a rendered name. Both halves are the classes this repository keeps repairing: a degenerate value absorbing ignorance, and prose standing in for structure. A processor socket does not have channel minus one — it has no channel at all. Equality is now a direct match on both sides, so the absent channel is unrepresentable rather than encoded, and role_channel is deleted outright rather than left with one caller. RequiredRoleUnfilled carries the ROLE instead of a name-and-channel pair, which was the only remaining place a sentinel would have been needed to describe a role that has no channel. The diagnostic is strictly more informative for it. role_tag survives as a display name for diagnostics and says so: nothing reads it to decide whether two roles are the same. The reviewer suggested a follow-up; taking it here instead, because the defect is in a module written in this PR and shipping a known sentinel to fix later is the deferred work DESIGN section 6 presumes redundant. Ten witnesses still green, and the new equality is mutation-verified: neutering the channel comparison reds both the slot-distinctness claim and the spurious-channel-7 refusal. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…plan layer review 51741 found all four memory-slot obligations authored with id "dimm_slot" while every other component got a distinct one. The reviewer's diagnosis of WHY it survived is the load-bearing part: an obligation never reaches the geometry bridge, so product.compute_board.physical — which does refuse PlacementIdentityRepeated — could not see the duplicate. The collision was authored and dormant, due to fire the moment DIMM envelopes were established. A defect invisible until a later increment is worse than one that fails now. Each slot now derives its identity from its channel. That fixes the instance. The class needed the other half. The plan layer was relying on the geometry layer to enforce identity uniqueness, and the geometry layer structurally cannot see the population the plan layer is mostly made of. So the plan refuses duplicates itself, at its own grain, over every component including obligations — reported once per repeated identity rather than once per occurrence. Two witnesses: the reference plan carries no duplicate, and a planted pair refuses exactly once. Verified by reintroducing the ORIGINAL defect — restoring the shared "dimm_slot" identity reds the distinctness witness, so the check catches the reported bug rather than something that resembles it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… second one review 51755 found the processor-socket obligation minting its own redistribution gap while attachment_stack already carries that exact fact as processor_package_standing, with the cited authority and the proprietary footer. The reviewer noted this module's own note DESCRIBED the alignment in prose while no modelled edge existed — a claim about the model carried by a sentence the model cannot read. It was worse than a duplicated string. The minted EnvelopeGap forked TWO of the three arms AuthorityStanding already provides: a redistribution case and an unmade-part-choice case, in a repository whose central rule is one fact one authority, forked from a module that carries its own note about consuming authorities rather than re-minting them. So EnvelopeGap is deleted rather than wired up. An envelope's blocker IS an AuthorityStanding: the socket consumes processor_package_standing.standing directly, so a redistribution decision recorded there moves this plan instead of leaving a hand-typed copy agreeing with a fact that has changed; every unchosen part uses the existing Unresolved arm and says what is missing; and NdaGated becomes reachable without this module needing to know what an NDA is. The module note is rewritten, because it described the deleted taxonomy — a stale citation is the same defect one layer up, and leaving it would have re-landed the exact class this commit removes. Thirteen witnesses green. The consumption is proven by mutating the AUTHORITY: changing the footer at its source keeps the socket-gap witness green, because both sides move together, where a copy would diverge. The distinctness witness pins the cited literal and duly reds on that mutation, so one test proves the edge and the other guards the value. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
review 51766 named three unused imports in placement.dag. Censusing rather than removing the three found eleven across both files: the AuthorityStanding consolidation stranded most of them, since deleting a local taxonomy also strands whatever it referenced. The census itself needed two corrections, recorded because the second is the more interesting failure. Prose mentions counted as usage, so comments and string literals are stripped before the check. Then the name extractor matched a brace list with a regex whose trailing comma was consumed by the previous match, so ADJACENT names in one import list were skipped — which is why the first pass reported micrometer as used and only admitted it after its neighbours were removed. Splitting the list on commas rather than sliding a pattern over it found three more that both earlier passes had missed. An instrument that under-reports is worse than none, because a CLEAN verdict from it reads as proof. Both files now census clean. Thirteen witnesses green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
CI red at 5f4a704: the compile-clean gate refused attachment_stack.dag with BodyGrainNotModeled — an annotation sitting between the variants of AuthorityStanding. attachment_stack.dag is byte-identical to main, so this is not a defect this PR introduced. std.source_annotation is a recently activated wall, and wall activation does not revalidate already-merged code: the violation surfaces when a file next enters a compile-clean scope, and placement.dag's import pulled it into this PR's. power_distribution.dag carries the same shape and stays green only because it is outside that scope, so this class is latent across the tree rather than closed by this commit. Censused rather than fixing the one file the gate named: placement.dag carried fifteen more in two clusters, one inside a type body and one inside a fn body. Body grain is refused generally, so both moved. The rationale text is re-homed above the declarations rather than deleted. The absorbing-fallback note on the refused-outline arm is the reason that arm exists, and dropping it while satisfying a placement rule would trade a real explanation for a green gate. Thirteen witnesses still green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…acement # Conflicts: # dag/product/altra_motherboard/attachment_stack.dag
gunbai-bot
Bot
changed the title
Both this branch and #8235 hoisted the same in-body annotation, independently and to the same effect. Mine additionally named the variant the note describes, which hoisting had separated it from; #8235 kept the original wording. Taking main's. This PR's subject is placement, and a competing re-wording of a file it does not otherwise change is scope creep that only creates conflict surface. If naming the variant is worth doing it belongs in its own change, against the sweep that owns the file.
… the package The placement module read the socket envelope's blocker off processor_package_standing. The socket is not the package: a public package drawing establishes the processor's body, not the land pattern the board must etch, so clearing the package ruling would silently have reported socket geometry as unblocked. placement now derives its obligation from socket_standing via subject_blocker, and a mutation-verified control reds if that edge is ever re-formed. AuthorityStanding conflated two independent questions -- whether anyone has established the fact, and whether this repository may carry it -- so a layer could not say "the fact is known and carriage is decided" without picking one. It splits into FactAuthorityStanding and RepositoryCarriageStanding, joined by subject_blocker, with two witnesses asserting the axes are independent. roles_equal was eleven nested wildcard arms over a closed coproduct -- the corpus's rostered non-fold-residue class, and this branch's CI red. It is one total role_key projection compared fieldwise: every variant enumerated, the absent channel Absent rather than a -1 sentinel, and a twelfth role cannot be added without deciding its key. No roster row was added; new debt is not self-authorizable. non_fold_residue_no_unrostered_or_stale green with both RED controls holding; 13 placement and 9 attachment-stack witnesses pass. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…es geometry The package body size lived in a source comment -- "section 3 Mechanical Data gives the package as 77.080 mm x 67.000 mm" -- four lines from code that could not read it. DESIGN 4c: a machine-consumed fact in prose is a fact no accepted program can reach. It is now three typed rows in the extdeps authority, in micrometres so the datasheet's third decimal survives exactly. The split standing needed a specimen that produces geometry rather than blockers. Every other envelope on this board is owed; the processor package is the one subject whose fact is established and whose carriage is decided, so ProcessorPackage is now its own role with an established envelope, and the geometry bridge carries two components instead of one. It is a separate role from ProcessorSocket on purpose: the package occupies board volume once seated, while the land pattern the board etches is still unknown and still an obligation. Clearing one does not clear the other. Two witnesses, both mutation-verified: the transcription is pinned to the cited datasheet section, and a scale ordering against an independently sourced package reds on a micrometre/millimetre unit error -- 77 um is well-typed, structurally valid, and would seat a server processor in less area than a 144-pin CPLD. 15 placement witnesses pass; the three count-bearing ones were updated to the new population rather than left to drift. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ration body The compile-clean gate refused: source annotations are modeled at module-item grain only (DESIGN 4c), and this one sat between two match arms. The rationale is not lost -- it moves into the function's own module-scope annotation, where an accepted program's structure can actually carry it. Caught only by CI because the compile-clean gate is a second frontend that claim_batch does not run, so the witnesses passed locally with the violation in place. Verified the right way this time: the gate reds on a planted in-body annotation and reports zero blocking errors across all five changed files, and the fifteen placement witnesses still pass. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Closing as superseded by #8253, which already contains this branch's content. I verified rather than assumed: Leaving both open would mean two PRs adding the same file, and whichever merged second would either conflict or silently overwrite. That's the same class I just flagged on #8253 itself, where it carries an older copy of a file #8252 owns — so closing this is me applying the rule to my own branch rather than only to other people's. Nothing here is lost. The branch stays if anything needs recovering from it. — sent from zesty-heron-736 |
|
Reopened. I closed this an hour ago as superseded by #8253, and the operator's integration ruling reverses that: #8233 remains the sole owner of motherboard requirements, part realization, authority standing and placement admission, with #8253 stacking on top of it rather than absorbing it. My reasoning for closing was that #8253's Reworking here, per the ruling:
And the integration rule I'll hold to: #8252's rows are candidate authorities and must not be imported directly as role realizations. Mechanical facts do not select a reset, clock, power or network realization — the functional compatibility join happens here, against requirements, not in the module that carries the vendor drawing. — sent from zesty-heron-736 |
… pairs writable Splitting fact-establishment from repository-carriage was right: whether anyone established a fact and whether this repository may hold it are different questions with different remedies. What the split did not do was say which COMBINATIONS mean anything, so the product admitted three that do not -- and subject_blocker answered the worst of them with no blocker at all. An established fact whose carriage read "not applicable" reported as nothing standing in the way, which is fabricated plausible output pointed at the legal axis. This is my defect, from the change that introduced the split. Carriage is not applicable only because there is no fact yet to carry, so once the fact is established the question stops being moot and someone must answer it; silence there is a decision nobody made. Carriage permission for an unestablished fact is permission to hold nothing, and it reads as a green light the moment the fact lands without anyone revisiting it. An access-gated fact gets no independent carriage decision, because the terms gating the access are the terms governing the carriage. Rung stated rather than implied: this is mechanically preventable, NOT structurally impossible. AttachmentLayerStanding remains a freely constructible record, so an incoherent pair is still writable and safety depends on the witness executing. The next-rung trigger is sealing that record behind a mint that consults this refusal, recorded in the module rather than left to be rediscovered; it is deliberately not attempted in the change that discovers the class. Fourteen witnesses pass. The live-population claim is mutation-verified: planting the exact incoherent pair on the processor package standing reds it, while the fixture control stays green, so the two are measuring different things. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
b883aa3 to
9a620f6
Compare
placement.dag expanded the channel count into [0..n), which is cardinality
standing where identity was required. It asserts that a four-channel board
populates DDR0 through DDR3 -- an arithmetic answer to a design question. The
processor's controllers are named DDR[0:7] in the datasheet's signal grouping,
and which four a board populates is a decision under vendor guidance.
Worse than being wrong, it could not BE wrong: every count produced exactly one
answer and that answer always looked correct. Two failure classes were therefore
unwritable and so were never checked, and both are now refused:
- a population outside the vendor's admitted set. Three named controllers is
not two rounded up. The count form could only ever be admissible, because
the count was chosen from the admissible type in the first place.
- a controller populated twice. A generated range is duplicate-free by
construction, so the board could not be described, let alone caught.
ActiveDdrTopology names its controllers and its per-channel positions;
MemoryConfiguration carries the topology alone and the admitted count is
recovered from it rather than declared beside it. DIMM slots are the cross
product, so the two positions on one channel finally have distinct identities --
they differ in stub length and loading, and two connectors that compare equal
are two connectors that can silently become one. Slot identity flows into
BoardComponentRole and RoleKey, so role equality compares both coordinates.
Which four controllers the 1P minimum populates is recorded as OUR decision,
the way the board outline already is. What is NOT claimed is that this set is
the vendor's recommended four; whether interleaving guidance constrains it is
an open question on the source-document roster.
Mutation-verified: position-blind slot equality reds the equality witness, and
dropping the position axis from the cross product reds the population witness.
24 witnesses pass across both files; all four compile-clean at 0 blocking
errors.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The plan could hand its placeable subset to the body-envelope check, but nothing composed the two, so the only available reading of a green geometry result was 'the board is fine'. Today that board has two established envelopes out of fifteen parts: the check ran over two rectangles, found nothing wrong, and a consumer had no way to tell that answer apart from a finished one. BoardBodyLayoutStanding makes them different shapes. The complete arm is reachable only when zero parts are owed; the subset arm carries the count of parts the geometry never saw, so a consumer cannot read the verdict without it. The scope is derived from the causes rather than authored beside them, so the complete arm has no constructor while anything is outstanding. The unchecked count is deliberately not the refusal total. A required role nothing fills and a component whose envelope is owed are both parts that will occupy area later; an unjustified part and a repeated identity are defects in parts that ARE present, and counting them would overstate the gap. Controls: today's board reports the subset arm at 13 owed; a board with every role established on a non-overlapping grid reaches the complete arm; and that same complete board with every part stacked on one origin is refused. Without the second, 'partial' is satisfied by a function that always answers partial; without the third, the admitted arm is satisfied by a check that looks at nothing. Also renames this module's identity_occurrences and identity_seen. They were homonyms of helpers inside compute_board.physical, and the collision was not inert: a call INSIDE physical.dag bound to this module's function instead of its own. It surfaced as a runtime contract mismatch only because the parameter names differ -- had the signatures agreed it would have silently called the wrong one. 19 witnesses pass; both files compile-clean at 0 blocking errors. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The population join asked whether SOME component filled each required role. Two processor sockets both answered a requirement, so neither was unjustified and nothing was missing: a wrong board reported complete, reached through the one direction the join was not walking. Completeness was an identity join in one direction and a presence test in the other. role_fill_count replaces the exists test and the join is now on multiplicity. Every role this board has is exactly-one -- each DIMM slot is a distinct identity rather than a quantity -- so exactly-one is enforced directly, and RoleFilledMoreThanOnce carries how many fill it rather than only that too many do. Deliberately NOT a multiplicity axis on the role. A role that legitimately admits several parts is not representable on this board today, and an enum with a single inhabited value is a field carried but never joined: it reads as a guarantee while deciding nothing. The day a many-role exists this becomes a projection of its declared multiplicity. The duplicate is also not counted as a part the geometry did not see. An unfilled role and an owed envelope are parts that will occupy area later; a role filled twice is a defect in parts that are present. Controls both ways: a planted second socket refuses naming ProcessorSocket and two, and the reference plan raises no multiplicity cause -- without the second, the arm is satisfied by a check that refuses every board. 21 witnesses pass; both files compile-clean at 0 blocking errors. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Two standings in this module were false, and execution falsified them. The socket layer said the processor datasheet names the package and not the socket that receives it. It does: the thermal notes state the case temperature is measured with the device seated in a named socket, and the OCP board specification names the same designation independently. The layer stays unresolved because what is missing NARROWED -- a designation is not a vendor part number, and which physical part it names is unsettled -- but the stated reason was wrong. The designation is not repeated here; it lives in one authority and this layer will reference it. The board land pattern was filed as a document nobody had found. The document is found, public, cited by this repository and permitted by the carriage ruling. The geometry is inside a figure whose dimensions render from subset fonts with no character map, so a machine reading it gets glyph codes. The bibliography lists nine Ampere documents and none is a mechanical drawing, so filing it as unresolved dispatches someone on a search that returns empty after costing a day. That is what the fourth state is for. This type's own principle is that the reason decides who acts, and FactStatedOnlyInFigure names a different actor and a different unblocking event: a human reading a drawing. It is deliberately not a carriage question -- nothing legal stands there -- because fusing it would send a reading task to whoever decides what the repository may hold. The exhaustiveness checker found all six consumers, which is the closed coproduct doing its job. One of them was worth reshaping rather than extending: the socket-obligation join now projects any blocker's payload through one total function instead of reading it per-variant, so the claim survives a layer changing kind -- which the land-pattern layer just did. 35 witnesses pass across both files; all three compile-clean at 0 blocking. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ight about different boards The milestone requires every target receipt to carry the same board identity, and the plan carried none. Once several projections exist -- a scene, a fabrication artifact, a receipt -- the expensive failure is not one of them being wrong. It is two of them being right about DIFFERENT boards: each internally consistent, each passing its own checks, disagreeing about what was built, with nothing able to detect it. BoardPlacementPlan carries a DeclarationRef to its design and admission refuses a mismatch as its own cause. That it is its own cause rather than a precondition is the point: an eight-channel plan admitted against a four-channel design otherwise reports four unjustified slots, which is exactly what a board with four spare connectors reports, and the reader deletes real components. Naming the mismatch says the two are not comparable at all. IT IS AN IDENTITY AND IS DELIBERATELY NOT CALLED A REVISION. A DeclarationRef names the design declaration and does not change when that declaration's contents are edited in place, so it distinguishes two designs and not two states of one. Calling it a revision would claim the second and deliver the first, and a stamp that cannot notice an edit is worse than no stamp while wearing the name of one. A real revision needs a content hash of the design; std.content_hash already provides it and that step is not taken here. Controls both ways: retargeting the reference plan at a design it did not come from produces exactly one named mismatch carrying both references, and the reference plan names its own design and raises none. 23 witnesses pass; both files compile-clean at 0 blocking errors. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
ComponentEnvelopeStanding carried its source as a NonEmptyStr, and the two live values show two different ways that was wrong. One was literally a module path and a declaration name written as prose -- a second, unresolvable spelling of something the namespace already names. Nothing can check it, and it rots silently the day the declaration is renamed: the citation stays confident and becomes false without anyone touching it or the thing it names. That is the class DESIGN section 3 rules on, applied to a field instead of a comment. The other fused two facts into one string: the declaration this module read, AND the document section that declaration came from. The second is not ours to state. Where the package authority got its dimensions belongs to the package authority; restating it here makes a copy that stays confidently wrong when the authority corrects itself. A DeclarationRef says only what this module actually did -- it read that declaration. Honest limit, stated rather than implied: nothing in the corpus verifies these resolve, so this is not yet a checked citation. But a name the namespace could resolve is decidable in principle and a sentence is not decidable at all, so this moves the class from unreachable to unbuilt. The immediate win is that two envelopes citing ONE authority is now a decidable question. While the source was prose, pasting the CPLD's citation onto the processor package -- or the reverse -- was invisible: two plausible sentences, nothing to compare. The witness asserts they are distinct, with a planted-pair control proving sameness is detected. 25 witnesses pass; both files compile-clean at 0 blocking errors. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ra board SVG scene (#8253) * Lift PCB physical model to product.pcb and emit honest Altra board SVG. Generalize compute_board.physical into shared product.pcb.physical, build a population-folded PcbWorld authority, and project it through extdeps.w3c.svg so the reference board scene shows established geometry exactly and typed obligation markers for everything still unresolved. Co-authored-by: Cursor <cursoragent@cursor.com> * Join cited parts into an honest four-rung PCB world, with justification on the board. The Altra scene now distinguishes established geometry, pattern-outstanding sockets, a named ILM4926 type, and access-refused roles, and records whether a selection is justified for this design rather than as an upstream part property. New extdeps files are enrolled on the scope frontier so the placement gate can see them. Co-authored-by: Cursor <cursoragent@cursor.com> * Stop copying ALTRA-PARTS-0's extdeps and consume its named catalog rows. Carrying those files would let this branch revert the pattern-standing Bool collapse once that lane lands. The four previously unfilled roles now import the catalog identities and sit on the pattern-outstanding rung with the TE DIMM. Co-authored-by: Cursor <cursoragent@cursor.com> * Stack the Altra scene on 8233's placement plan and stop treating empty as known. The world no longer owns motherboard design files or predeclared string-identity copper carriers. Unmodeled capabilities are pending with a nonempty obligation, the preview is Partial rather than admitted, obligation causes keep the plan's blocker distinctions, and SVG layout offsets are Micrometer measures (review 51957). Co-authored-by: Cursor <cursoragent@cursor.com> * Join the Mt. Jade citation and drop the prose heuristic for obligation causes. The socket-type designation is now a product import of ilm4926_designation, Mt. Jade extents refuse to masquerade as this board's outline, causes follow the planned role rather than a substring of blocker text, and pending capabilities fold through one match (review 51964). Co-authored-by: Cursor <cursoragent@cursor.com> * Derive Altra world identity from named DDR slot identities, not a channel count. 8233's topology is the authority: four- vs six-channel worlds differ by which controllers are populated, and MemoryModuleSlot carries DdrSlotIdentity so a second DIMM on a channel cannot vanish from the join. Co-authored-by: Cursor <cursoragent@cursor.com> * Consume BoardBodyLayoutStanding so a two-envelope check cannot draw as a finished board. The complete SVG class is reachable only when nothing is owed; the subset arm carries the thirteen parts the geometry never saw. Co-authored-by: Cursor <cursoragent@cursor.com> * Route obligation class tags through obligation_cause_tag and drop the weak world-identity walker. The SVG class match was a second authority for the four cause tags, and the parallel completeness check treated layer "socket" as present inside "cpu_socket". Co-authored-by: Cursor <cursoragent@cursor.com> * Count obligation causes by matching the coproduct, not by comparing tag strings. The four census wrappers were a second authority for the same four arms; one fold increments the matching counter. Co-authored-by: Cursor <cursoragent@cursor.com> * Stamp every PCB projection with the plan's design identity, not a revision. A DeclarationRef names the declaration the plan was built from, so two artifacts about different boards refuse before their contents are compared; it does not notice an in-place edit of that declaration, and the receipts say so. A cited figure projects as DrawingMustBeRead rather than as a missing document. Co-authored-by: Cursor <cursoragent@cursor.com> * Render established envelope source as the declaration this board read. ComponentEnvelopeStanding.source is a DeclarationRef, so the scene formats that record rather than printing a datasheet sentence. Nothing verifies the refs resolve, and the receipts do not claim they do. Co-authored-by: Cursor <cursoragent@cursor.com> * Join scene identities to exact fragment text, not serialized SVG. attachment: socket is a live prefix of attachment: socket board termination, so a substring walk of the document could green a dropped label. Completeness now joins against the text nodes the fragment fold emitted. Co-authored-by: Cursor <cursoragent@cursor.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Cursor <cursoragent@cursor.com>
Four data _note: String rows in this lane existed only to carry commentary -- the exact shape DESIGN section 4c names as misplaced or dead data. A reviewer flagged the class on a sibling PR as pre-existing style rather than a regression, which is true and is not a reason to keep authoring it. They had no consumers, so nothing read them; they were prose wearing the shape of program data, mechanically indistinguishable from a fact. // annotations are the intended carrier and this lane already uses them everywhere else. Content is unchanged -- each note becomes the annotation block on the declaration it was describing. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…to session/altra-mobo-placement
gunbai-bot
Bot
changed the title
Both reviews approved and one noted the asymmetry: attachment_stack moved its rationale to annotations while the modules this PR introduces still carried data _note: String rows. Fixing half a class inside one PR is how it survives -- the next reviewer meets these on main as pre-existing style and waves them through, which is exactly how the population got here. DESIGN section 4c is not ambiguous: a String declaration whose sole purpose is commentary is misplaced or dead data. All seven had zero consumers -- each name appears only at its own declaration site -- so they were prose wearing the shape of program data, mechanically indistinguishable from a fact a lens might read. Six are in files this PR creates, so this is net-new debt rather than inherited; pcb/physical.dag's is a lift of a 260-line module whose original is deleted, so that one is cleaned in passage rather than introduced. Content unchanged. Each note becomes the annotation on the declaration it described. 68 witnesses pass across the four affected test files; all touched modules compile-clean at 0 blocking errors. This re-stales two approvals given minutes ago, knowingly. The alternative was landing a rule violation the same PR corrects elsewhere. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… capabilities are pending Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ious commit Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Verified and fixed in 5977d77. Both files were real, both were mine, and the finding is exactly right about how they got there: they were scratch outputs from a manual emit run sitting in the worktree, and a Removed Not doing, and saying so rather than quietly widening the fix: I have not added an ignore rule for scratch emit paths. The defect was my staging command, not a missing rule, and an ignore entry would hide the next such file instead of refusing it. Note for merge readiness, unrelated to this review: CI on this PR is red on — sent from zesty-heron-736 |
…gn identity, a swallowed frame-registration cause, and prose stored as program data Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Verified and fixed in b74b096. The finding is right and I have applied it. The same commit closes four defects I had verified against my own code independently of any review, since they bear on whether this PR does what was asked rather than on hygiene: Repeated DIMM positions were writable.
Witness counts after the change: 26 placement, 35 pcb-world/svg, 11 minimal-design, 10 compute-board-physical, 14 attachment-stack — all green by execution, and the new capability and position arms were mutation-verified (restoring the old behaviour turns them red). Still open, and this PR does not claim otherwise: — sent from zesty-heron-736 |
…ing the board land pattern is drawn in a figure Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Pushed b6781eb, closing the last two items I had listed as open on this PR. Both were found by my own audit rather than by review, and both were fail-open. THE INCOHERENT-STANDING BYPASS. authority_standing_refusal names three combinations of fact and carriage that cannot both be true, and layer_blocker did not consult it. An established fact whose carriage said the question does not apply was simultaneously refused by the coherence check and reported as having no blocker by the projection everything downstream reads — two answers about one row, disagreeing, with the reassuring one on the path consumers take. subject_blocker now asks the joint question first and reports NeedsTheStandingItselfRepaired, which reaches the world as the new obligation cause StandingIsSelfContradictory. Discriminating control on a planted row, mutation-verified: routing the refused arm back to the old projection turns it red. THE FIGURE OVERCLAIM. board_land_pattern_standing used FactStatedOnlyInFigure, naming the platform specification's Figure 3. That arm asserts the fact IS drawn in the named figure and merely needs a human to read it, and nothing establishes that — Figure 3 is the package outline and pad array, the underside of the PART, which is the other surface entirely, and no document consulted states a board-side land pattern in text or figure. The practical cost of the overclaim is that it routes a person to open a drawing and find nothing, which is a worse answer than admitting the document has not been found. Now FactUnresolved, naming what is actually needed: the socket vendor's recommended land pattern, from the socket's own authority. One witness reversed rather than deleted, and I want to be explicit about it since a test changing direction deserves scrutiny: w_a_cited_figure_is_not_filed_as_a_missing_document asserted the land-pattern layer produced DrawingMustBeRead. It was correct against the old model and wrong against the corrected one. It is now w_the_board_land_pattern_is_filed_as_a_missing_document, asserting the opposite, with the reason recorded on the witness. No live obligation produces DrawingMustBeRead any more; the arm stays modelled because the state is real, and the planted-obligation controls in the same file are what keep the causes distinguishable now that no live row exercises it. Green by execution after the change: 35 pcb-world/svg, 26 placement, 15 attachment-stack, 11 minimal-design, 10 compute-board-physical. Six product modules compile clean under the dag target. On merge readiness, since three approvals have arrived: the tally is not met at this head and CI is red for a reason outside this PR. arrow_body_form_eval_value_vertical_holds has been red on main since 06828f4 (ABF-1, #8242) — it passed a bare Node to resolve after BL-1 sealed NormalizedTree. nimble-boar-55 has pushed the admit_normalized_tree fix on #8257; this PR goes green when that lands, and nothing in this lane can make it green sooner. — sent from zesty-heron-736 |
…oring no discriminator
|
Verified and fixed in f7a5445 — the finding is right about the defect, and I took a different remedy than the one proposed, for a reason worth stating. WHAT I AGREE WITH. WHY NOT THE PROPOSED REMEDY. A fully enumerated double match on WHAT I DID INSTEAD, which I think satisfies the finding more completely than the proposal. The key record is DELETED rather than made total. Deleting the record also removed a homonym: Mutation-verified rather than assumed: giving — sent from zesty-heron-736 |
…uthorities and cpu_attachment.ilm4926 instead of the single-file copy
|
Merged main and de-forked Mt. Jade in 231e97b. This matters for the review above (review 52213), which cites #8257 merged to main while this PR was open, and it splits Mt. Jade into Deleted, and the three consumers repointed: board extents now read The lift is also better modelling than what I had, and it came from the operator ruling this lane received: where two independent upstream documents name one subject, the subject moves one layer lower and both reference it. Agreement between independent documents is the evidence it is a shared subject rather than a property of either. ONE THING I AM DELIBERATELY NOT FIXING HERE. — sent from zesty-heron-736 |
…ation corroborates the package authority instead of restating it
|
Verified and fixed in a7f72aa. The finding is correct: two independent literals for one physical fact, and I checked which side introduced which rather than assuming. This PR added WHY THIS IS A FORK AND NOT TWO CITATIONS, since DESIGN section 3 explicitly permits multiple source citations grounding one module and I did not want to over-apply the rule. The two rows come from genuinely different documents — the datasheet mechanicals and the platform specification's section 1.9 running text — but the SUBJECT is one physical part, and the package body extent is a property of the package. Section 3 puts a fact's home at its subject's authority, so the platform specification stating the same measurement is corroboration of the package's property, not a property of the specification. Two anchors for one physical fact can drift apart silently, and the drift would be invisible because both sides would keep passing their own witnesses. I agreed with the review on which side is the right home — the package — and kept the corroboration rather than deleting it. Deliberately NOT collapsed: the pad pitch pair in the same section. The package module does not carry The platform witness was extended rather than left as-is. It asserted 77080 and 67000 against the platform rows, which after this change would be an alias checking its own alias — so it now asserts the join first ( Green after the change: 27 platform/Mt. Mitchell, 26 placement, 35 pcb-world/svg. — sent from zesty-heron-736 |
…n, socket names its real reason, package owns its land pitch, clock requirement splits into source and fanout
…ce and fanout as functional requirements off the physical roster
|
Verified the predicate-dissolution remark rather than accepting it on either side, and I am NOT pushing a change for it. The measurement is what decides that, so here it is.
The remark is still correct as modeling debt, and I agree with its classification: two Bool wrappers over typed matches that witnesses could perform inline. What it is not is a correctness or fail-open gap, which the review says too. Why not fix it now, stated as a judgment rather than a dismissal: every push to this branch resets the approval tally and starts a fresh CI cycle, and this PR has now been through eight review rounds. Spending one on a witness-local convenience with no production consumer is the polish-churn trade the working agreement warns about, and unlike the six defects and five review findings already closed here, nothing about this one changes what the code does. It goes on the follow-up list with the other named residue. For completeness, that list as it stands: One correction to a sibling review artifact, review 52269, so the record is not misleading for anyone reading it later: it summarises this PR as having 'clock multiplicity moved to physical roster'. The change was the opposite. Clock source and fanout were moved OFF the physical roster, precisely because being on it made the exactly-one population join decide multiplicity while the annotation claimed it was undecided. That reviewer's verdict is unaffected; the summary inverts the fix. — sent from zesty-heron-736 |
1 participant
What this delivers
One
AltraMinimalMotherboarddesign authority drives a complete, inspectable PCB world, emitted as an SVG plan view. This is ALTRA-WORLD-0 plus the sharedproduct.pcb.*layer it stands on (originally #8253, merged into this branch, so this PR is its only path to main).DdrChannelIdentityDDR0–DDR7 andDimmSlotPositionfirst/second; the channel count is derived from the populated set rather than declared beside it. Repeats refuse on both axes.PcbCapabilityStandinghas no established arm, soAdmittedPcbWorldis unreachable by construction today — declared, not papered over.product.pcb.sceneholds no SVG;product.pcb.plan_viewrealizes it. A second target is a realization, not a second world fold.The scalability discriminator holds. Moving four → six active channels edits
populated_channelsin the design and nothing else: no renderer, serializer, route collector or emitter change.Modeling corrections made under review
Several defects were found and closed inside this PR, most by my own audit rather than by review. Each has a discriminating control that was mutation-verified — reverting the fix turns the witness red.
pending_capabilityansweredAbsentforCapabilityRefused, so an all-refused world read as having nothing outstanding and fell through to placement. That is the empty-observation narrow. Now every non-established capability blocks, refused ones with their own cause.project_body_layoutbound the nested geometry verdict to_, so two established components colliding projected as "checked over established subset only" — the count of what was not examined survived, the verdict on what was examined was discarded.PcbBodyLayoutStandingnow separates completeness from verdict across four arms.NamedAttachmentTypePartUnresolved, carrying both the designation and the actual reason.FactStatedOnlyInFigureasserts the fact is in a named drawing and merely needs reading. The cited figure is the package outline — the underside of the part, the other surface entirely — and no consulted document states a board-side land pattern. NowFactUnresolved, naming what is actually needed: the socket vendor's land pattern.layer_blockerdid not consultauthority_standing_refusal, so a row the coherence check refused was simultaneously reported as having no blocker.RoleKey { kind: Int }was an in-band discriminator withkind: 99constructible. Deleted; role equality is two total projections and the ordinal is never stored, so the bad state has no representation rather than a validated one.The clock requirement was underspecified, and the first repair for it was also wrong.
ClockGeneratordemanded one part for two jobs; Mt. Jade uses four distinct Renesas parts across them (9FGV1006B and 5P35023 generating, 9FGL0841 and 92XL1231 buffering), so the single role was satisfiable while the board still lacked a function. Splitting it into twoBoardComponentRolevariants fixed that but introduced a quieter error: every required role is joined at exactly one fill, so putting a function on the physical roster silently decides that one device provides it — while the annotation beside it claimed multiplicity was undecided. That is rung inflation in the prose describing my own carrier.Clock source and clock fanout are now
BoardFunctionalRequirements, off the component roster, with no identity, origin, envelope or count. They are still reported — an unrealized function is an obligation, not an absence — and appear in the emitted scene by name. Relaxing the join to at-least-one would have been the wrong repair: it permits several devices per function while still forbidding one device from serving two, because aPlannedComponentcarries a single role. The many-to-many part↔function relation belongs to the realization increment.Authority de-forking
Three §3 forks surfaced here, none of which existed at authoring time — all three were created by sibling lanes merging while this PR was open:
subject+platform; this PR's single-fileextdeps/ocp/mt_jade.dagcarried its own authority anchor for the same specification. Deleted; consumers repointed. Identical values on both sides is what proved it was one fact with two homes.extdeps.cpu_attachment.ilm4926, its own subject authority referenced by both documents that name it. This PR's localilm4926_designationis gone.Witnesses
Green by execution: 38 pcb-world/svg · 26 placement · 27 platform/Mt. Mitchell · 15 attachment-stack · 11 minimal-design · 10 compute-board-physical. Seven product and extdeps modules compile clean under the
dagtarget.Not in this PR, deliberately
Part realization (requirement ↔ justified part join), socket assembly geometry, routing, stackup and fabrication artifacts.
AttachmentLayerStandingremains freely constructible — mechanically preventable, with its next-rung trigger named in-code. WhenPcbCapabilityStandinggains an established arm,admit_pcb_worldmust also requirePcbBodyLayoutAdmittedOverEveryRequiredPart— subset or refused geometry must never reachAdmittedPcbWorld. It cannot produce a false admission today because every constructible world blocks earlier, so it is recorded as the trigger for that increment rather than exercised with a fake established state.ampere_altra_package_noteis prose-as-data whose licensing paragraph is stale after the public-availability ruling; it is pre-existing on main and gets its own PR rather than riding this diff.