Repository navigation
product_introduction census: an identity join over named Conjs, not a count (red since #12766) - #12932
Merged
Conversation
… count (red since #12766, bisected) The claim read conjs == 4 and went red at #12766, which made each named-fn parameter reference a path-keyed reference carrier: a Conj under <parameter-reference>, so x + y carries two more products. The census now names every Conj infer is asked to derive by its children (edge label and the last atom the child subtree carries) and requires exactly that named list, each derived (DESIGN 5: completeness is an identity join, not a count). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ts_holds leaves Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…-census # Conflicts: # dag/gunbc/rung_drop_amendment/v2_test_family_reds_measured_outside_the_gate.dag # docs/design-rung-drops.md
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
github-merge-queue
Bot
removed this pull request from the merge queue due to a conflict with the base branch
Oct 1, 2026
…-census # Conflicts: # dag/gunbc/rung_drop_amendment/v2_test_family_reds_measured_outside_the_gate.dag # docs/design-rung-drops.md
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… added #12923 (a binder's target is a binder node) put each parameter's type under a <binder-type> Conj, so the specimen carries two more products. The identity join named the change instead of absorbing it; both are named and required derived. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…-census # Conflicts: # dag/gunbc/rung_drop_amendment/v2_test_family_reds_measured_outside_the_gate.dag # docs/design-rung-drops.md
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Oct 2, 2026
…nfer's string-literal payload read and the product_introduction census edge name read Authored, with an explicit structural arm Co-Authored-By: Claude Opus 5.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
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.
v2.test.execution.infer_product_introduction.product_introduction_derives_fully_evidenced_products_holdswas a silent red on main, counted on #12860 under calm-hawk-793.Bisected (BuildBuddy, path-restricted to
src/v2/{compiler,std,extdeps}anddag/std, from 1375c80 to main): the first bad commit is d5dc100, #12766 ("named-fn parameter references as path-keyed references; infer grounds them through the index"). That change is deliberate. Each named-fn parameter reference became a path-keyed reference carrier, a Conj under<parameter-reference>, so the specimen bodyx + ynow carries two more products. Both derive.Not a literal bump (lane-manager direction; DESIGN §5: "completeness is an identity join, not a count"). The claim read
conjs == 4. It now names every Conj infer is asked to derive: it walksnode_inferred_subtree_nodes, the existing authority, so no second set of skip rules exists. Each Conj is named by its children, meaning each child edge's label plus the last atom that child's subtree carries, because a parameter reference's path ends at the parameter it names. The claim requires exactly this named list, in walk order, with each derived:A non-derived Conj appears as
!name, so it can't match. The single-Arrow assertion is unchanged.Executed green on BuildBuddy: this claim, plus
product_introduction_composed_evidence_carries_child_groundings_holds(control). The identity leaves the #12860 amendment, and the projection is regenerated.🤖 Generated with Claude Code