Repository navigation
model QSFP cabling surprise - #10683
Merged
Merged
Conversation
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Sep 7, 2026
DESIGN §6: name the instrument. The fixture pair is gunbc compile on the two if_join_pool_binding entries; the remaining production specimen is the same binary on the #10683 tree with --source-dir dag/gunbc/roadmap. Co-authored-by: Cursor <cursoragent@cursor.com>
2 tasks
briansrls
pushed a commit
that referenced
this pull request
Sep 8, 2026
…spelled product (#10737) * A local coproduct arm must not re-bind when an unrelated pool type claims the same spelling. Record-literal widening asked the corpus-wide binder whether the arm name declared its own type; that question is now the declaring module's chain, and the if_join_pool_binding fixture finally has an executing consumer. Co-authored-by: Cursor <cursoragent@cursor.com> * State the fixture consumer as local-only diligence, not merge-path evidence. The row had named an executing consumer that rust_unit_tests_off_the_merge_path does not run; that was rung inflation. The hand-Rust test now carries the same deferral receipt. Co-authored-by: Cursor <cursoragent@cursor.com> * Record that the isolated product and unit-arm fixtures do not close the class. The production Observed/BeltObserve refusal remains under this repair; an isolated off-chain unit arm pulled in by a Dummy import compiles clean, so that analogue is not the remaining channel. Co-authored-by: Cursor <cursoragent@cursor.com> * Drop the cargo-test consumer so the four-file fixture has one executing route. The required floor witness in gunbc#10740 is what can go red on the merge path; a v1-compiler-tests module compiled by clippy and run by nobody was a second consumer of the same specimen. Co-authored-by: Cursor <cursoragent@cursor.com> * Regenerate docs/design-failure-modes.md from the edited failure-mode row. The projection still carried the old reproduce sentence after the authority changed; the generated-artifact actuator is what adjudicates that file. Co-authored-by: Cursor <cursoragent@cursor.com> * Record that an isolated unit-arm analogue is not the production Observed specimen. Same binary, opposite verdicts: the four-file product fixture is not a faithful stand-in for roadmap_belt_actuate, and the row must not read as unit-arm closed. Co-authored-by: Cursor <cursoragent@cursor.com> * Cite the reproduce commands instead of a transcribed error count. DESIGN §6: name the instrument. The fixture pair is gunbc compile on the two if_join_pool_binding entries; the remaining production specimen is the same binary on the #10683 tree with --source-dir dag/gunbc/roadmap. Co-authored-by: Cursor <cursoragent@cursor.com> * Enroll the inverted floor witness with the product-channel repair. Review 61772 required an executing merge-path consumer and noted that lookup_binding_by_name_local still walks ancestry. The local-type carve-out now reads TypeEnv.str_bindings only; the required-floor witness compiles the same four fixture files and expects both manifests clean. Co-authored-by: Cursor <cursoragent@cursor.com> * Install the emitted stage0 mirror for the str_bindings-only lookup. required-witnesses-build failed generated-artifact stage0-mirrors on v1_compiler_infer.rs: the hand-edited seed omitted the clone the emitter produces. Co-authored-by: Cursor <cursoragent@cursor.com> * Drop the conjunction witness that recompiled both fixture arms. the_verdict_does_not_flip_on_pool_membership_alone was the two neighbouring tests ANDed and paid two extra nested compiles on the required floor for no extra RED. Co-authored-by: Cursor <cursoragent@cursor.com> * Regenerate design-failure-modes.md from the merged ledger authorities. The merge left the projection at the merge-base, so four main-landed identities were missing from the file readers are pointed at. Co-authored-by: Cursor <cursoragent@cursor.com> * Repoint the fixture headers and keep imported products on-chain for widening. The four-file comments still described a refusal the enrolled witness no longer produces. Widening now treats ancestry (direct imports) as declaring the type, still excluding intern/global_bare, so an imported product is not widened to a pool coproduct arm of the same spelling. Co-authored-by: Cursor <cursoragent@cursor.com> * Regenerate design-failure-modes.md from the merged ledger authorities. Co-authored-by: Cursor <cursoragent@cursor.com> * Regenerate ledger projections from the merged authorities. Co-authored-by: Cursor <cursoragent@cursor.com> * Past-tense the failure-mode receipts that still described a red collided witness. The enrolled arms already expect both manifests clean; leaving the #10740 defect-pin in the present tense was a meaning fork of the same row. Co-authored-by: Cursor <cursoragent@cursor.com> * Name the on-chain binding walk once in infer_env. lookup_binding_on_chain is the declared-or-imported tier; record-literal widening and type_ref_measure_binding_authority consume it, and lookup_binding_by_name_local is that walk plus intern. Co-authored-by: Cursor <cursoragent@cursor.com> * Regenerate ledger projections from the merged authorities. 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>
… its cables imply The switch had a desired-state module and no convergence binding, so every declaration in it was unconsumed -- the state DESIGN section 3c calls red regardless of how well the model is shaped. gunbc.spark.fabric_switch_converge binds the switch as its own subject to the one gunbc.world_converge authority: four handler stages, a handler data row, and converge_fabric_switch / fabric_switch_convergence entry points. The cable plant stays a separate subject, so a repair to one can never green the other. Three things are deliberate: - observe refuses in order -- undecided intent, then unread lane, then no lanes. Each later question is meaningless without the earlier one, and reporting over the lanes that happened to answer would make an uncaptured switch indistinguishable from a correct one. - apply always refuses. There is no modelled transport to RouterOS, so returning a receipt would fabricate the one thing convergence exists to prove. The refusal carries the full divergence list so an operator gets the exact edit. - readings are LaneNeverRead for every lane, because no RouterOS capture exists. Section 3 puts that gap downstream as a refusal here, never as an Unobserved field in extdeps.mikrotik.crs812. Six witnesses, including the positive control that keeps the refusals informative, two separate discriminating inputs for the absorbing fallback (an unread lane, and a lane outside the intent), and one holding the fleet's real red state: the switch refuses because its cables do, carrying the cable refusal rather than restating it. Evidence is TYPECHECK ONLY: 0 blocking errors, rc=0, against a control arm on the same instrument that gave 1 blocking error, rc=1. The witnesses have never executed -- every floor run on this branch refuses at resolve on the orphan roadmap_belt_actuate:3532 defect, which is unrelated to this change and remains unowned. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AigrH3JpxgSJBmqHMBAr6W
1 of 3 tasks
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AigrH3JpxgSJBmqHMBAr6W
…ported rate as SymbolRate Both findings from review 62557, and both were real. nominal_rate_reported_mbps: Nat -> nominal_rate_reported: SymbolRate. The review called the _mbps suffix a second encoding of a scale std.measure already carries. Reading that module's own annotation makes it worse than a duplicate encoding: ethtool renders SFF-8636 byte 140 as "BR, nominal" in Mb/s, but the specification defines it in units of 100 MBd, and on a PAM4 lane baud and bits/s differ by the modulation factor. The suffix asserted the wrong QUANTITY, which is exactly the conflation SymbolRate was minted after being caught in review. The scale belongs to the Measure. crs812_desired_lane_speed returned a literal Lane100GCr2 while the module's own annotation said the speed is a FUNCTION of the plant's convergence and is never written down here. The annotation was true of the intent and false of the code, and a section 4c annotation can never be checked, so nothing would have caught the drift. It now reads required_mode off the converged subject and selects through crs812_lane_speed_for_link_mode, a new citation in the vendor module recording which IEEE clause each RouterOS wire value implements. That mapping is deliberately PARTIAL. 400G-baseCR8 has no LinkMode row, and minting one inside a vendor module to make a fold total would author an IEEE fact where it does not live. An unmapped mode refuses through a new SwitchCannotRunRequiredMode arm rather than falling back to a neighbouring speed -- the absorbing fallback would configure the switch to something nobody asked for and hide that the hardware cannot do the job. Three new witnesses make the derivation falsifiable: a literal agrees with exactly one of the three modes, so a constant returning here goes red on two. A fourth holds that an unrunnable mode has no wire value. The mapping first used Present/Absent in an if-chain and hit 'if branches resolve to incompatible types: Coproduct(Crs812LaneSpeed) vs Coproduct(Optional)' -- the same widening family as the open roadmap_belt_actuate specimen. Replaced with a named closed coproduct, which is better modelled here anyway and does not route through that path. Typecheck: 0 blocking errors across all three affected closures, on the instrument whose control arm returns 1 blocking error. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AigrH3JpxgSJBmqHMBAr6W
Contributor
|
Correction to one line in review 62571, against my own PR's favour. The review says of the refusal arms: "Each of those has a discriminating RED and a positive control in the two new witness files, so §4b(1)'s rung-honesty evidence is executed, not asserted." The first half is right and the second half is not. No witness in this PR has ever executed. Every floor run on this branch — 34225196473, 34252602724, and 34256600036 — refused at resolve on the orphan §4b(1) is explicit that the reported rung must equal the rung established by executed evidence, and that a type name or a plan establishes nothing. The witnesses are written and shaped to discriminate; whether they actually do is unproven until the floor runs them. Recording this so the approval is not later read as evidence they passed. Related and worth stating here because it touches the same PR: #10838 did not close that resolver specimen. Its floor went green on a tree that never contained the trigger, and main was already green, so that run could not discriminate — my error, and I reported it as a receipt before checking what it ranged over. The specimen still refuses on this branch, which carries both the fix and the trigger, and is re-filed as its own work item. — sent from fierce-deer-825 |
2 tasks
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AigrH3JpxgSJBmqHMBAr6W
Review 62666, and the finding is one this file argued against itself. The comment above `leg_standing` names a per-question `match ... -> Bool` as the non-fold residue DESIGN §6 rules out, and then two declarations later I wrote exactly that -- moved one layer out, over the classification instead of over the finding, which is where it stops looking like the thing being warned about. `plant_divergent_outcomes` and `plant_conditional_outcomes` now match `leg_standing` directly and emit the row or nothing, the same shape `plant_unread_endpoints` already uses below them. `filter` and the two Bool helpers are gone; nothing else consumed them. The concrete cost of the old shape: a new LegStanding arm had to be remembered at each predicate, and a predicate that forgot it would answer false rather than fail to compile. Selecting through the classification fold makes a new arm one decision that every selector re-makes at once. Typecheck: 0 blocking errors on both affected closures; the control arm returns 3 blocking errors, rc=1. Prior head 6778964 executed these witnesses on the required floor (changed_witnesses=14, changed_witness_blocking=0), so this is a shape change over an executed baseline rather than a first landing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AigrH3JpxgSJBmqHMBAr6W
…ntinel, not a measurement Review 62687, and it lands on me twice. SFF-8636 byte 140 holds FFh on these legs, the escape saying the real rate is in byte 222. `ethtool -m` printed "BR, nominal: 25500 Mb/s", and 25500 is exactly 255 x 100 -- the escape multiplied out and rendered as though it were a measurement. extdeps.transceiver.sff_8636 names that number, in those words, as "the fabrication this whole subject exists to catch". I had edited that module. The first error was keeping the number at all, as nominal_rate_reported_mbps. The second was the repair I made for review 62557: retyping it to SymbolRate to satisfy a unit-modeling finding moved a sentinel INTO the type minted to make this exact conflation unwritable, where the corpus counts are baud (peers carry symbol_rate(25781250000), and the decoder itself builds code * 100000000). Renaming it made it look grounded while making it worse. So the field is deleted, not retyped a second time. It carried no information the model does not already hold -- byte 140 being 255 -- and NominalRateEscaped already says exactly that, honestly and with nothing attached. The witness that asserted == 25500 is replaced by one asserting the opposite: the escape resolves to no measurement at all, and it goes red the moment anyone reconstitutes a rate from it. What actually grounds this number is unchanged and unowned: nobody has run `ethtool -m <dev> raw on` against these legs to read byte 222, and until someone does, an escaped rate is a declared gap rather than a figure. Typecheck: 0 blocking errors across all three affected closures; control arm returns 1 blocking error, rc=1. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AigrH3JpxgSJBmqHMBAr6W
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Sep 9, 2026
…nd retract the stale plant claim CONFLICT RESOLUTION. main deleted gunbc.world_converge at the root and replaced it with std.goal_assessment, carrying all three modules from #10683 across with it. The single conflict was one import block where this branch adds LegNeverRead (the six-unread-legs repair) while main renames converge_cable_plant to inspect_cable_plant and CablePlantConvergence to CablePlantInspection. Resolved to main's vocabulary PLUS this branch's addition -- neither side wholesale. The migration is an improvement on what it replaced, and worth naming: the actuation arms are Never in GoalInspection<...>, so "this subject cannot be actuated from here" is now STRUCTURAL rather than my always-refusing apply function. That is section 4b's climb from a runtime refusal to a state with no constructor, in a place I had left at the lower rung. REVIEW 62808. The block heading the plant still said "every leg was read to the same bytes, so the plant is the lane roster joined to the one coding observation" -- the exact claim the previous commit was written to retract, sitting five lines above the retraction. Two annotations, one file, materially different answers to the same question. It now says the plant joins the roster to what was READ of each, which is not the same for every lane, and that a lane enters as unread until someone dumps it. Section title follows main's vocabulary from convergence to inspection. This is the third stale-prose finding on this PR and the mechanism has been identical each time: I rewrite the block I am editing and do not re-read its neighbour. The declaration changes, nothing forces the adjacent comment to move with it, and section 4c guarantees no Accepted program will ever notice. NOT CHANGED, deliberately: fabric_cable_plant_convergence still says "convergence" while returning a CablePlantInspection. That is a nickname against the new authority, but main authored it in the migration, and renaming a migrated symbol is not conflict resolution. Worth a follow-up. Typecheck: 0 blocking errors across all five affected closures on the merged tree. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AigrH3JpxgSJBmqHMBAr6W
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.
Auto-opened by session-dashboard for session
fierce-deer-825.Pushing to
session/fierce-deer-825advances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan