Repository navigation
design: L1.12.b — structural-similarity sub-signature closes L1.12's nickname-detection gap - #3479
Merged
briansrls merged 9 commits intoMay 21, 2026
Conversation
…nickname-detection decidability gap L1.12's decidability boundary explicitly names the gap: 'two homes use *different* lexical names AND no CanonicalConcept row registers them as the same concept — closing it requires either operator judgment or an extension primitive (e.g., a structural similarity fold).' Operator asked for that extension primitive (anti-nickname detector for unnecessarily-reinvented helpers/models). Adds L1.12.b sub-signature with Trigger C (structural similarity) covering two scopes: - Type-scope: variant-set + field-shape bijection against std/ carriers - Fn-scope: signature-shape bijection + body catamorphism-form classifier Three decidability layers, ordered by workhorse-first: - (C1) Signature-shape match — substrate-readable bijection on variant/parameter sets preserving type identity - (C2) Catamorphism-equivalence — Practice 10 homomorphism heuristic mechanized as one-arm-per-T-variant detection - (C3) Token-vocabulary overlap — triage-only, never fires alone (operator no-fourth-tier rule) Shares the 5-outcome resolution table with the parent L1.12 (alias / retirement / disambiguation / canonical-concept-no-resolution / silence-fails-closed). Verdict: hard error. Fix-confidence: templated auto-apply (alias-rewrite for C1, fold_T derivation for C2). Escape (clean 🟢) covers refinement-not-parallel, Practice-11-parameterized identical-body cases, and distinct domains via ConceptDisambiguation. Real-corpus kills cited: - count_named_bind quadruplet (identical across 3 test fixtures + 1 lens file) → C1 fires - RegisterStateSpace parallel to StateSpace in ptx.dag (refinement declared as parallel coproduct) → C1 fires - lookup_chain hand-rolled structural recursion over Scope vs fold_right (resolver) → C2 fires (Practice-10 un-derived catamorphism) §10 dependency model: - §10.1 row added for the new per-decl structural-shape index - §10.2 v4.lens.structural_similarity derived stage spec (produces Map<DeclId, StructuralShape> = TypeShape | FnShape with per-field semantics for downstream lens consumption — Facts Flow Forward / P2 single-authority) - §10.3 dissolution stage's consumes: list updated Binding rationale (vs new L-ID or Practice-instance): L1.12's own decidability text names the gap; the resolution table is the same; the lens-framework producer-stage shape requires lens-binding. Sub- signature is honest. Operator's no-new-IDs directive (2026-05-19) is preserved — no new top-level L1.x minted. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…observation) claude reviewed PR #3479 with a non-blocking exploratory observation: firing on the (r1_gates.template.dag → r1_gates.dag) pair would be a false positive, since r1_gates.dag is generated from the template via build.rs emit_r1_gates_fixture splicing the lens source into the source: field. Generated artifacts shouldn't independently trigger nickname findings against their templates — by construction. Fix: - Add 'Template → generated artifact' Escape rule (clean 🟢). The substrate carries the generation edge explicitly (template header + build.rs splice site, or a future GeneratedFrom registry row); reading that edge prevents the false positive. Same flow as outcome (1) alias-identity, scoped to mechanical generation. - Tighten the 'count_named_bind' corpus citation accordingly: named_function_count.dag (canonical) vs t_demo_fixtures.dag (hand-authored copy) is the actual (C1) fire; the template→ generated pair is cited to show the boundary works. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…prose-escape leak) codex REQUEST_CHANGES on PR #3479 raised two valid findings: [#1] Fn-scope (C1) widening to signature-only — false-positive prone. The trigger text said 'body structurally equivalent' but (C1) and the producer-stage FnShape only carried signature shape, widening the detector to 'same type signature' = nickname. Two unrelated fns with the same (T) -> U signature is the expected steady-state, not a nickname; firing on that is false-positive territory. Fix: - Trigger language tightened: fn-scope fires under EITHER (C1) [signature-shape match AND α-renamed body equality] OR (C2) catamorphism-equivalence. Signature-alone is explicitly NOT a fire. - (C1) rule updated: fn-pair matches iff signature-bijection AND body shape (α-renamed expression tree) are BOTH structurally identical. - Producer-stage FnShape extended to carry body_normalized: BodyShape — required for (C1) fn-scope; signature-only-match documented as deliberate non-fire. [#2] Template-generation Escape leaked prose authority. The Escape allowed 'template header marker + build.rs splice site' to satisfy resolution — but L1.12's parent explicitly rules out comment markers and prose-shaped resolution paths. That re-introduced a prose-shaped authority and conflicted with the no-prose discipline. Fix: - Escape rewritten to require ONLY a structural GeneratedFrom registry row in the substrate: data foo_generated_from: GeneratedFrom = { generated: ..., authority: ..., emitter: ... } - Explicit statement: header comments and build.rs files alone do NOT satisfy the escape; the GeneratedFrom row must land. - Worked example tightened: r1_gates pair fires L1.12.b TODAY (as it should — substrate has not taken a structural position); landing the GeneratedFrom row resolves it. Both fixes preserve the mechanically-decidable, structural-only contract the section is trying to strengthen. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
commented
May 21, 2026
briansrls
left a comment
briansrls
left a comment
Contributor
Author
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
40a82d01· Trigger:schedule - Thinking:
232s wall
BLOCKING (3)
Root Cause
docs/design-dissolution-lens.mdThe type matcher conflates exact isomorphism with refinement/subset similarity → split exact structural identity from refinement/subset matching and carry the relation needed for the refinement escape.docs/design-dissolution-lens.mdL1.12.b extends the escape vocabulary without extending the closed resolution outcomes → either map refinement/GeneratedFrom to existing outcomes explicitly or add them to the trigger, resolution table, and clearing receipt.docs/design-dissolution-lens.mdThe producer records only a classifier, not the fold algebra or arm mapping → carry aCatamorphismShape/algebra witness forward or remove the auto-fix promise.
| between their variant sets preserving field arity + field-type | ||
| coproduct identity (modulo coproduct-of-leaves identity per | ||
| Practice 11). For fn-scope: the parsed model carries the fn's | ||
| **signature shape** (input coproduct, output coproduct, |
Contributor
Author
There was a problem hiding this comment.
BLOCKING: C1 requires a bijection over the full variant sets, but the section's own RegisterStateSpace kill is a subset/refinement of StateSpace, so the lens will not fire on a named target case (INVARIANTS P1/P4).
| - `src/v3/lenses/named_function_count.dag:15` — canonical lens | ||
| (the program-text authority). | ||
| - `src/v3/compiler/tests/t_demo/t_demo_fixtures.dag:28` — | ||
| hand-authored test fixture: **fires on (C1)** as an |
Contributor
Author
There was a problem hiding this comment.
BLOCKING: The clearing receipt only accepts the parent L1.12 resolution shapes, while this section adds refinement and GeneratedFrom escapes, leaving no single authoritative resolution table (INVARIANTS P2 / Practice 5).
|
|
||
| module v4.lens.match_arm_skeleton | ||
| consumes: v4.compiler.02_parse, v4.compiler.03_resolve | ||
| produces: Map<MatchExprId, SkeletonReport> |
Contributor
Author
There was a problem hiding this comment.
BLOCKING: CatamorphismForm preserves only StructuralFoldOver(TypeId), but L1.12.b promises a C2 auto-fix using the extracted fold algebra, so a downstream-required fact is silently dropped (Practice 3 / INVARIANTS P2).
…ollision note + sweep prior WIP into clean commit) Three of the four cursor APPROVE_WITH_COMMENTS items got auto-snapshotted as a WIP commit (d47e523); this commit lands the fourth (the GeneratedFrom naming-collision note in the Template→generated Escape) and serves as the named clean commit for the cursor reconcile work. Findings addressed (cumulative summary across d47e523 + this commit): [main] RegisterStateSpace was claimed '(C1) fires' but (C1) requires full variant-set bijection — StateSpace has 8 variants, RegisterStateSpace has 6 with renamed constructors (subset+extension, not bijection). Demoted to honest known gap labeled '(C1') refinement- subset future sub-layer candidate'; auto-fix restricted to firing-today cases only. [exploratory 1] §10.2 'Four small derived stages' → 'Five' (count updated to include structural_similarity). [exploratory 2] GeneratedFrom carrier name collides semantically with DependencyKind::GeneratedFrom variant in src/v4/std/dependency.dag:25. Added implementation-time naming note in the Escape rule suggesting GeneratedArtifactBinding (or similar) at implementation time; design- doc uses short form for clarity. [exploratory 3] L1.12.b missing from §5.0/§5.1 lens tables. §5.0 row updated to L1.12 as lens family with L1.12.b sub-signature (mirroring L1.10's family entry). §5.1 row added sharing parent's coverage_defect_parallel_authority key — sub-signature contributes to the same key; no separate key minted (consistent with no-new-IDs). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Contributor
Author
Same finding as cursor's review — addressed in commits
|
…ive table (briansrls BLOCKING + P2/Practice 5) Finding (briansrls inline at :1237): clearing-receipt text said 'one of the parent's five resolution shapes' but the parent has 3 PASSING shapes (outcomes 1/2/3 — alias, retirement, disambiguation); outcomes (4) and (5) are FIRES, not resolutions. L1.12.b then added two more passing shapes (refinement edge, GeneratedFrom row) that lived scattered in the Escape list, with no single authoritative resolution table. Violates P2 / Practice 5 single-authority. Fix: - Clearing-receipt rewritten as a table enumerating all five passing resolution shapes: (R1) Alias-identity edge — parent (R2) HistoricalDeclaration retirement — parent (R3) ConceptDisambiguation row — parent (R4) Refinement edge — L1.12.b (R5) GeneratedArtifactBinding registry row — L1.12.b - Explicit note that parent outcomes (4)/(5) are FIRES not resolutions. - Explicit no-prose discipline applies uniformly across the table. - Deletion clarified as 'trigger absence' not a sixth shape. - Fix-confidence text references the (R1)/(R3)/(R4) shapes by ID, so the table is the single source of truth. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…(briansrls BLOCKING + Practice 3 / P2) Finding (briansrls inline at :1850): CatamorphismForm was specified as 'None | StructuralFoldOver(TypeId)' carrying only the TypeId, but L1.12.b's (C2) auto-fix promises 'the rewrite is the fold_T call with the algebra extracted from the original arms.' To do that, the auto-fix needs the EXTRACTED ALGEBRA (per-variant arm bodies). The producer-stage was silently dropping a downstream-required fact — same Facts Flow Forward violation pattern as the SkeletonReport finding on PR #3466. Fix: - CatamorphismForm::StructuralFoldOver extended to carry { type_id, algebra } where AlgebraShape = { per_variant: Map<VariantId, NormalizedArmBody>, recursive_positions: Set<VariantField> }. - Explicit note: algebra extraction is the SAME fold-walk that classifies the form — emitted in the same record, single pass. - Explicit Facts Flow Forward (Practice 3 / P2) statement: the (C2) auto-fix consumes the algebra directly; no consumer re-walks the fn body or re-extracts the algebra. Pattern reuse: same shape as PR #3466 SkeletonReport schema expansion — producer carries everything the auto-fix needs, no silent re-walks. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Contributor
Author
All three BLOCKINGs addressed by commits landed after this review's HEAD (
|
…ement + clarify r1_gates fires-until-R5 (cursor APPROVE_WITH_COMMENTS reconcile) cursor APPROVE_WITH_COMMENTS on PR #3479 raised one valid wording finding plus one exploratory ambiguity: [wording finding] Type-scope trigger bullet (:1109-1111) listed RegisterStateSpace/StateSpace as something L1.12.b catches ('refinements declared as parallel coproducts'), but (C1) requires a full variant-set bijection, and the Kills section explicitly demoted that pair to an honest known gap for future (C1'). Internal contradiction. Fix: - Type-scope trigger reworded: catches model nicknames 'where the variant sets are in full structural bijection' (positive scope statement matching (C1)). Refinement/subset cases explicitly marked NOT in scope, with pointer to the Kills section for the future (C1') refinement-subset sub-layer. - Example tightened from RegisterStateSpace (which is now the known-gap example) to a hypothetical 3-variant DominanceResult that genuinely fits the (C1) full-bijection criterion. [exploratory ambiguity] Kills called the r1_gates pair 'resolved by' the template escape, while the escape section said it 'fires until' the GeneratedArtifactBinding row lands. Same fact, two phrasings — implementation workers could read 'resolved by' as 'doesn't fire,' which contradicts the no-prose discipline. Fix: - r1_gates citation reworded: 'fires (C1) today AND will continue to fire until a (R5) GeneratedArtifactBinding registry row lands — (R5) IS the resolution path.' Removes the ambiguity between trigger-state and resolution-shape. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Operator delivered a thorough review on PR #3479 with 7 specific issues. All addressed in one cohesive tightening pass (hardening the spec, not reframing): [1] 'std/core carrier' conflicts with count_named_bind kill citing non-std canonical home (named_function_count.dag). Fix: Trigger language changed to 'registered canonical-home declaration'; std/ and core/ are defaults but the concept-home index defines what's canonical. Non-std canonical homes qualify. [2] Status needs explicit enforcement gate despite shared parent acceptance key. Without trigger-distinguishing payload, downstream consumers can't tell parent vs sub-signature findings under coverage_defect_parallel_authority. Fix: Status promoted to 'reserved-proposed' (parallel to L1.13) with three explicit gating conditions: (a) v4.lens.structural_similarity lands with the schema, (b) L1.12 diagnostic carries ParallelAuthorityTrigger discriminator, (c) R1-R5 carriers mechanically consumable. New ParallelAuthorityTrigger coproduct declared with three variants (LexicalNameCollision / CanonicalConceptCollision / StructuralSimilarity{layer}). [3] Type-scope (C1) breadth ergonomics needed explicit posture: hard-fire on common shape-equivalent domain sums until ConceptDisambiguation lands? Fix: Posture made explicit. Yes — common Result-like/Option-like/ status-enum/domain-sum shapes WILL fire L1.12.b until (R3) ConceptDisambiguation lands. Stated as 'the design's chosen posture' (ergonomic cost is intentional). [4] C2 'known fold_T' was naming-convention, not substrate fact. Fix: New FoldRegistryEntry carrier declared (carrier, fold, recursive_positions, algebra_carrier). C2 now requires both (i) CatamorphismForm resolves to StructuralFoldOver{T, algebra} AND (ii) a substrate FoldRegistryEntry row for T. Without the row, C2 does not fire — substrate authority required. [5] AlgebraShape needed more for C2 auto-fix (lookup_chain rewrite needs free params, fold order, accumulator, short-circuit). Fix: AlgebraShape extended with four new fields: - free_params: List<ParamSlot> (e.g., name in lookup_chain) - fold_order: FoldOrder (LeftFold | RightFold | UnorderedFold) - result_carrier: TypeId (the output type) - short_circuit: Optional<ShortCircuitCarrier> (None for total folds; Some(...) for early-return semantics like lookup_chain) Extracted in the same single fold-walk pass as the classifier. [6] GeneratedArtifactBinding should be the final name now, not 'implementation-time note.' Fix: All four references to 'GeneratedFrom' in the Escape rule + Kills citation + (R5) table renamed to 'GeneratedArtifactBinding'. Naming-note repurposed as the rationale (one paragraph at the declaration site) instead of a future-implementation flag. The example data row updated to r1_gates_generated_binding. [7] '5-outcome table' vs '5 passing resolution shapes' was overloaded vocabulary. Fix: Clearing-receipt prologue rewritten to separate the terms: - 'outcome' = parent L1.12 decision-table evaluations (5 cases, 3 passing + 2 firing — outcomes (4)/(5) are firing states) - 'resolution shape' = substrate carriers that clear a firing (5 shapes R1-R5, all passing) Vocabulary distinction explicitly flagged as load-bearing. Operator's stated merge posture: merge as design proposal after these fixes; tighten before enforcement. This commit completes the design-proposal tightening. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
4 tasks
briansrls
added a commit
that referenced
this pull request
May 21, 2026
…t-level type-only differences (sweep companion) (#3484) * design: L1.12.b — structural-similarity sub-signature closes L1.12's nickname-detection decidability gap L1.12's decidability boundary explicitly names the gap: 'two homes use *different* lexical names AND no CanonicalConcept row registers them as the same concept — closing it requires either operator judgment or an extension primitive (e.g., a structural similarity fold).' Operator asked for that extension primitive (anti-nickname detector for unnecessarily-reinvented helpers/models). Adds L1.12.b sub-signature with Trigger C (structural similarity) covering two scopes: - Type-scope: variant-set + field-shape bijection against std/ carriers - Fn-scope: signature-shape bijection + body catamorphism-form classifier Three decidability layers, ordered by workhorse-first: - (C1) Signature-shape match — substrate-readable bijection on variant/parameter sets preserving type identity - (C2) Catamorphism-equivalence — Practice 10 homomorphism heuristic mechanized as one-arm-per-T-variant detection - (C3) Token-vocabulary overlap — triage-only, never fires alone (operator no-fourth-tier rule) Shares the 5-outcome resolution table with the parent L1.12 (alias / retirement / disambiguation / canonical-concept-no-resolution / silence-fails-closed). Verdict: hard error. Fix-confidence: templated auto-apply (alias-rewrite for C1, fold_T derivation for C2). Escape (clean 🟢) covers refinement-not-parallel, Practice-11-parameterized identical-body cases, and distinct domains via ConceptDisambiguation. Real-corpus kills cited: - count_named_bind quadruplet (identical across 3 test fixtures + 1 lens file) → C1 fires - RegisterStateSpace parallel to StateSpace in ptx.dag (refinement declared as parallel coproduct) → C1 fires - lookup_chain hand-rolled structural recursion over Scope vs fold_right (resolver) → C2 fires (Practice-10 un-derived catamorphism) §10 dependency model: - §10.1 row added for the new per-decl structural-shape index - §10.2 v4.lens.structural_similarity derived stage spec (produces Map<DeclId, StructuralShape> = TypeShape | FnShape with per-field semantics for downstream lens consumption — Facts Flow Forward / P2 single-authority) - §10.3 dissolution stage's consumes: list updated Binding rationale (vs new L-ID or Practice-instance): L1.12's own decidability text names the gap; the resolution table is the same; the lens-framework producer-stage shape requires lens-binding. Sub- signature is honest. Operator's no-new-IDs directive (2026-05-19) is preserved — no new top-level L1.x minted. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: L1.12.b — add template→generated Escape rule (claude PR #3479 observation) claude reviewed PR #3479 with a non-blocking exploratory observation: firing on the (r1_gates.template.dag → r1_gates.dag) pair would be a false positive, since r1_gates.dag is generated from the template via build.rs emit_r1_gates_fixture splicing the lens source into the source: field. Generated artifacts shouldn't independently trigger nickname findings against their templates — by construction. Fix: - Add 'Template → generated artifact' Escape rule (clean 🟢). The substrate carries the generation edge explicitly (template header + build.rs splice site, or a future GeneratedFrom registry row); reading that edge prevents the false positive. Same flow as outcome (1) alias-identity, scoped to mechanical generation. - Tighten the 'count_named_bind' corpus citation accordingly: named_function_count.dag (canonical) vs t_demo_fixtures.dag (hand-authored copy) is the actual (C1) fire; the template→ generated pair is cited to show the boundary works. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: L1.12.b — fix codex BLOCKING #1+#2 (fn-scope (C1) widening + prose-escape leak) codex REQUEST_CHANGES on PR #3479 raised two valid findings: [#1] Fn-scope (C1) widening to signature-only — false-positive prone. The trigger text said 'body structurally equivalent' but (C1) and the producer-stage FnShape only carried signature shape, widening the detector to 'same type signature' = nickname. Two unrelated fns with the same (T) -> U signature is the expected steady-state, not a nickname; firing on that is false-positive territory. Fix: - Trigger language tightened: fn-scope fires under EITHER (C1) [signature-shape match AND α-renamed body equality] OR (C2) catamorphism-equivalence. Signature-alone is explicitly NOT a fire. - (C1) rule updated: fn-pair matches iff signature-bijection AND body shape (α-renamed expression tree) are BOTH structurally identical. - Producer-stage FnShape extended to carry body_normalized: BodyShape — required for (C1) fn-scope; signature-only-match documented as deliberate non-fire. [#2] Template-generation Escape leaked prose authority. The Escape allowed 'template header marker + build.rs splice site' to satisfy resolution — but L1.12's parent explicitly rules out comment markers and prose-shaped resolution paths. That re-introduced a prose-shaped authority and conflicted with the no-prose discipline. Fix: - Escape rewritten to require ONLY a structural GeneratedFrom registry row in the substrate: data foo_generated_from: GeneratedFrom = { generated: ..., authority: ..., emitter: ... } - Explicit statement: header comments and build.rs files alone do NOT satisfy the escape; the GeneratedFrom row must land. - Worked example tightened: r1_gates pair fires L1.12.b TODAY (as it should — substrate has not taken a structural position); landing the GeneratedFrom row resolves it. Both fixes preserve the mechanically-decidable, structural-only contract the section is trying to strengthen. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: PM * design: L1.12.b — finish cursor reconcile (add GeneratedFrom naming-collision note + sweep prior WIP into clean commit) Three of the four cursor APPROVE_WITH_COMMENTS items got auto-snapshotted as a WIP commit (d47e523); this commit lands the fourth (the GeneratedFrom naming-collision note in the Template→generated Escape) and serves as the named clean commit for the cursor reconcile work. Findings addressed (cumulative summary across d47e523 + this commit): [main] RegisterStateSpace was claimed '(C1) fires' but (C1) requires full variant-set bijection — StateSpace has 8 variants, RegisterStateSpace has 6 with renamed constructors (subset+extension, not bijection). Demoted to honest known gap labeled '(C1') refinement- subset future sub-layer candidate'; auto-fix restricted to firing-today cases only. [exploratory 1] §10.2 'Four small derived stages' → 'Five' (count updated to include structural_similarity). [exploratory 2] GeneratedFrom carrier name collides semantically with DependencyKind::GeneratedFrom variant in src/v4/std/dependency.dag:25. Added implementation-time naming note in the Escape rule suggesting GeneratedArtifactBinding (or similar) at implementation time; design- doc uses short form for clarity. [exploratory 3] L1.12.b missing from §5.0/§5.1 lens tables. §5.0 row updated to L1.12 as lens family with L1.12.b sub-signature (mirroring L1.10's family entry). §5.1 row added sharing parent's coverage_defect_parallel_authority key — sub-signature contributes to the same key; no separate key minted (consistent with no-new-IDs). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: L1.12.b — consolidate clearing-receipt into single authoritative table (briansrls BLOCKING + P2/Practice 5) Finding (briansrls inline at :1237): clearing-receipt text said 'one of the parent's five resolution shapes' but the parent has 3 PASSING shapes (outcomes 1/2/3 — alias, retirement, disambiguation); outcomes (4) and (5) are FIRES, not resolutions. L1.12.b then added two more passing shapes (refinement edge, GeneratedFrom row) that lived scattered in the Escape list, with no single authoritative resolution table. Violates P2 / Practice 5 single-authority. Fix: - Clearing-receipt rewritten as a table enumerating all five passing resolution shapes: (R1) Alias-identity edge — parent (R2) HistoricalDeclaration retirement — parent (R3) ConceptDisambiguation row — parent (R4) Refinement edge — L1.12.b (R5) GeneratedArtifactBinding registry row — L1.12.b - Explicit note that parent outcomes (4)/(5) are FIRES not resolutions. - Explicit no-prose discipline applies uniformly across the table. - Deletion clarified as 'trigger absence' not a sixth shape. - Fix-confidence text references the (R1)/(R3)/(R4) shapes by ID, so the table is the single source of truth. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: L1.12.b — extend CatamorphismForm to carry extracted algebra (briansrls BLOCKING + Practice 3 / P2) Finding (briansrls inline at :1850): CatamorphismForm was specified as 'None | StructuralFoldOver(TypeId)' carrying only the TypeId, but L1.12.b's (C2) auto-fix promises 'the rewrite is the fold_T call with the algebra extracted from the original arms.' To do that, the auto-fix needs the EXTRACTED ALGEBRA (per-variant arm bodies). The producer-stage was silently dropping a downstream-required fact — same Facts Flow Forward violation pattern as the SkeletonReport finding on PR #3466. Fix: - CatamorphismForm::StructuralFoldOver extended to carry { type_id, algebra } where AlgebraShape = { per_variant: Map<VariantId, NormalizedArmBody>, recursive_positions: Set<VariantField> }. - Explicit note: algebra extraction is the SAME fold-walk that classifies the form — emitted in the same record, single pass. - Explicit Facts Flow Forward (Practice 3 / P2) statement: the (C2) auto-fix consumes the algebra directly; no consumer re-walks the fn body or re-extracts the algebra. Pattern reuse: same shape as PR #3466 SkeletonReport schema expansion — producer carries everything the auto-fix needs, no silent re-walks. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: L1.12.b — align type-scope trigger with (C1) bijection requirement + clarify r1_gates fires-until-R5 (cursor APPROVE_WITH_COMMENTS reconcile) cursor APPROVE_WITH_COMMENTS on PR #3479 raised one valid wording finding plus one exploratory ambiguity: [wording finding] Type-scope trigger bullet (:1109-1111) listed RegisterStateSpace/StateSpace as something L1.12.b catches ('refinements declared as parallel coproducts'), but (C1) requires a full variant-set bijection, and the Kills section explicitly demoted that pair to an honest known gap for future (C1'). Internal contradiction. Fix: - Type-scope trigger reworded: catches model nicknames 'where the variant sets are in full structural bijection' (positive scope statement matching (C1)). Refinement/subset cases explicitly marked NOT in scope, with pointer to the Kills section for the future (C1') refinement-subset sub-layer. - Example tightened from RegisterStateSpace (which is now the known-gap example) to a hypothetical 3-variant DominanceResult that genuinely fits the (C1) full-bijection criterion. [exploratory ambiguity] Kills called the r1_gates pair 'resolved by' the template escape, while the escape section said it 'fires until' the GeneratedArtifactBinding row lands. Same fact, two phrasings — implementation workers could read 'resolved by' as 'doesn't fire,' which contradicts the no-prose discipline. Fix: - r1_gates citation reworded: 'fires (C1) today AND will continue to fire until a (R5) GeneratedArtifactBinding registry row lands — (R5) IS the resolution path.' Removes the ambiguity between trigger-state and resolution-shape. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: L1.12.b — operator review tightening pass (7 issues addressed) Operator delivered a thorough review on PR #3479 with 7 specific issues. All addressed in one cohesive tightening pass (hardening the spec, not reframing): [1] 'std/core carrier' conflicts with count_named_bind kill citing non-std canonical home (named_function_count.dag). Fix: Trigger language changed to 'registered canonical-home declaration'; std/ and core/ are defaults but the concept-home index defines what's canonical. Non-std canonical homes qualify. [2] Status needs explicit enforcement gate despite shared parent acceptance key. Without trigger-distinguishing payload, downstream consumers can't tell parent vs sub-signature findings under coverage_defect_parallel_authority. Fix: Status promoted to 'reserved-proposed' (parallel to L1.13) with three explicit gating conditions: (a) v4.lens.structural_similarity lands with the schema, (b) L1.12 diagnostic carries ParallelAuthorityTrigger discriminator, (c) R1-R5 carriers mechanically consumable. New ParallelAuthorityTrigger coproduct declared with three variants (LexicalNameCollision / CanonicalConceptCollision / StructuralSimilarity{layer}). [3] Type-scope (C1) breadth ergonomics needed explicit posture: hard-fire on common shape-equivalent domain sums until ConceptDisambiguation lands? Fix: Posture made explicit. Yes — common Result-like/Option-like/ status-enum/domain-sum shapes WILL fire L1.12.b until (R3) ConceptDisambiguation lands. Stated as 'the design's chosen posture' (ergonomic cost is intentional). [4] C2 'known fold_T' was naming-convention, not substrate fact. Fix: New FoldRegistryEntry carrier declared (carrier, fold, recursive_positions, algebra_carrier). C2 now requires both (i) CatamorphismForm resolves to StructuralFoldOver{T, algebra} AND (ii) a substrate FoldRegistryEntry row for T. Without the row, C2 does not fire — substrate authority required. [5] AlgebraShape needed more for C2 auto-fix (lookup_chain rewrite needs free params, fold order, accumulator, short-circuit). Fix: AlgebraShape extended with four new fields: - free_params: List<ParamSlot> (e.g., name in lookup_chain) - fold_order: FoldOrder (LeftFold | RightFold | UnorderedFold) - result_carrier: TypeId (the output type) - short_circuit: Optional<ShortCircuitCarrier> (None for total folds; Some(...) for early-return semantics like lookup_chain) Extracted in the same single fold-walk pass as the classifier. [6] GeneratedArtifactBinding should be the final name now, not 'implementation-time note.' Fix: All four references to 'GeneratedFrom' in the Escape rule + Kills citation + (R5) table renamed to 'GeneratedArtifactBinding'. Naming-note repurposed as the rationale (one paragraph at the declaration site) instead of a future-implementation flag. The example data row updated to r1_gates_generated_binding. [7] '5-outcome table' vs '5 passing resolution shapes' was overloaded vocabulary. Fix: Clearing-receipt prologue rewritten to separate the terms: - 'outcome' = parent L1.12 decision-table evaluations (5 cases, 3 passing + 2 firing — outcomes (4)/(5) are firing states) - 'resolution shape' = substrate carriers that clear a firing (5 shapes R1-R5, all passing) Vocabulary distinction explicitly flagged as load-bearing. Operator's stated merge posture: merge as design proposal after these fixes; tighten before enforcement. This commit completes the design-proposal tightening. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: L1.4.b Variant-parameter-clone — catches intra-carrier variant-level type-only differences (operator sweep ask) Operator surfaced Practice 11 at a finer grain than L1.4 / L1.12.b currently cover: variants WITHIN one coproduct whose structural shape is identical (modulo field-name nickname) but the field TYPE is the actual discriminator — that IS what parametric carriers exist for. Seed case: src/v4/std/diagnostic.dag's type Locus = Textual {...} | NodeLocus { node: Node } | PortLocus { port: Symbol } NodeLocus and PortLocus are both single-field anchored records differing only in field type (Node vs Symbol); the field names (node, port) are nicknames for the anchor type. Binding: L1.4.b sub-signature under Carrier-clone family. - Parent L1.4: whole coproduct clones a std/ carrier. - L1.4.b: variants within one coproduct clone each other modulo type substitution. Same defect class (carrier dissolution), different grain. Sub- signature shares parent's coverage_defect_carrier_clone acceptance key with a CarrierCloneTrigger discriminator on the diagnostic payload — same pattern as L1.12.b under L1.12. Status: reserved-proposed (parallel to L1.12.b / L1.13). Enforcement gate (3 conditions): - v4.lens.structural_similarity lands with per-variant field-shape facts (already specified for L1.12.b; same producer stage, shared substrate index — Facts Flow Forward / P2). - L1.4 diagnostic payload carries CarrierCloneTrigger discriminator. - Substrate has at least one Practice-11-parameterized dissolution shape landed (the Locus rework is the seed target). Decidability: substrate-readable; compares VariantShape records within each coproduct under field-name α-renaming. Same mechanical contract as L1.13 (skeleton extraction) at variant scope instead of match-arm scope. Auto-fix: two clean-shape candidate Diffs emitted, reviewer picks: - Pattern A (type-level parameterization): type T<A> = T { at: A } — eliminates variant axis entirely when callers can thread the type parameter. - Pattern B (parametric sub-carrier lift): type Anchored<T> { at: T }; type Locus = TextualLocus {...} | NodeAt(Anchored<Node>) | PortAt(Anchored<Symbol>) — keeps coproduct discriminator for asymmetric variants while parameterizing the shared shape. Escapes (clean 🟢): ConceptDisambiguation row (R3); carrier already parametric (no fire by construction); variant carries non-type-only auxiliary structure (genuine variant-axis information). Decidability boundary: catches intra-coproduct variants only. Cross-decl variant matches route to L1.4 parent or L1.12.b. Variants differing in arity/nesting don't fire (no bijection). §5.0 + §5.1 cross-refs added; producer stage reuses v4.lens.structural_similarity (no new derived stage needed — TypeShape.variant_set is the shared index). Parallel to this design draft: jolly-eagle-492's modeling lane runs the full sweep across src/v4/std/ + extdeps/ + compiler/ for variant-clone instances; Locus rework lands as the migration- target precedent. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
May 21, 2026
…xtend concept_home producer to type-scope (cursor APPROVE_WITH_COMMENTS reconcile) cursor APPROVE_WITH_COMMENTS on PR #3479 raised one valid non-blocking finding plus one exploratory: [main finding, non-blocking] When I propagated 'registered canonical- home' through the trigger + Kills in the operator-tightening pass, I missed the Fn-scope bullet (:1156-1163) and the (C2) text. Internal inconsistency — Trigger C says canonical-home (concept-home index); Fn-scope and (C2) said 'std/' fn / 'std/-registered' type. Worker following Fn-scope literally would miss the count_named_bind (C1) case against the non-std/ canonical home src/v3/lenses/named_function_count.dag. Fix: - Fn-scope bullet updated to say 'matches an existing registered canonical-home fn' with explicit pointer to count_named_bind as the precedent of a non-std/ canonical home. - (C2) text updated to require FoldRegistryEntry.carrier points at a 'registered canonical-home type' (same canonical-home discipline as type-scope and (C1) fn-scope; std/ default, non-std/ qualifies when the concept-home index says so). [exploratory] v4.lens.concept_home is defined as Map<FnId, File> only — type-scope canonical-home would need an extended index when non-std/ canonical types matter beyond the fn example. Type-scope (C1) was relying on a concept-home authority the producer stage didn't actually provide. Fix: - v4.lens.concept_home's produces signature broadened to Map<DeclId, File> where DeclId = FnId | TypeId. Same producer stage, broader output — no new derived stage; the type-scope canonical-home authority lives in the same record as fn-scope. Facts Flow Forward / P2 preserved (one producer, multiple consumers). - Explicit prose explaining why the broadening: L1.12.b's type-scope (C1) needs the same canonical-home resolution fn-scope (C1) does; one mechanism for both. - 'reusable by' updated to call out the dual consumer pattern (L1.8 fn-home class, L1.12.b fn + type canonical-home authority). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This was referenced May 21, 2026
Closed
briansrls
added a commit
that referenced
this pull request
May 21, 2026
…xtend concept_home producer to type-scope (cursor APPROVE_WITH_COMMENTS reconcile) (#3487) cursor APPROVE_WITH_COMMENTS on PR #3479 raised one valid non-blocking finding plus one exploratory: [main finding, non-blocking] When I propagated 'registered canonical- home' through the trigger + Kills in the operator-tightening pass, I missed the Fn-scope bullet (:1156-1163) and the (C2) text. Internal inconsistency — Trigger C says canonical-home (concept-home index); Fn-scope and (C2) said 'std/' fn / 'std/-registered' type. Worker following Fn-scope literally would miss the count_named_bind (C1) case against the non-std/ canonical home src/v3/lenses/named_function_count.dag. Fix: - Fn-scope bullet updated to say 'matches an existing registered canonical-home fn' with explicit pointer to count_named_bind as the precedent of a non-std/ canonical home. - (C2) text updated to require FoldRegistryEntry.carrier points at a 'registered canonical-home type' (same canonical-home discipline as type-scope and (C1) fn-scope; std/ default, non-std/ qualifies when the concept-home index says so). [exploratory] v4.lens.concept_home is defined as Map<FnId, File> only — type-scope canonical-home would need an extended index when non-std/ canonical types matter beyond the fn example. Type-scope (C1) was relying on a concept-home authority the producer stage didn't actually provide. Fix: - v4.lens.concept_home's produces signature broadened to Map<DeclId, File> where DeclId = FnId | TypeId. Same producer stage, broader output — no new derived stage; the type-scope canonical-home authority lives in the same record as fn-scope. Facts Flow Forward / P2 preserved (one producer, multiple consumers). - Explicit prose explaining why the broadening: L1.12.b's type-scope (C1) needs the same canonical-home resolution fn-scope (C1) does; one mechanism for both. - 'reusable by' updated to call out the dual consumer pattern (L1.8 fn-home class, L1.12.b fn + type canonical-home authority). Co-authored-by: Claude Opus 4.7 (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.
Summary
CanonicalConceptrow. L1.12's own boundary text names "an extension primitive (e.g., a structural similarity fold)" as what's missing — this PR adds that primitive as L1.12.b.Real-corpus kills cited (grep-verified before drafting)
count_named_bindquadruplet — identical body acrosssrc/v3/compiler/tests/fixtures/r1_gates.template.dag:139,r1_gates.dag:139,src/v3/compiler/tests/t_demo/t_demo_fixtures.dag:28,src/v3/lenses/named_function_count.dag:15. C1 fires; Practice-11-parameterized clean shape per the Escape rule.RegisterStateSpaceparallel toStateSpaceinsrc/v4/extdeps/languages/ptx.dag:34and:102. Variant bijection holds across the shared variants;ResParam{...}is the refinement extension. C1 fires; refinement-not-parallel clean shape.lookup_chain(resolver) vsfold_rightoverScopeinsrc/v4/compiler/03_resolve.dag:205. Hand-rolled one-arm-per-T-variant structural recursion. C2 fires (un-derived catamorphism, per Practice 10).§10 dependency-model entries (Facts Flow Forward / P2)
v4.lens.structural_similarityderived stage spec: producesMap<DeclId, StructuralShape>whereStructuralShape = TypeShape | FnShapecarrying everything (C1/C2/C3) needs without re-walking declarations.v4.lens.dissolution'sconsumes:list updated.Test plan
consumes:list)🤖 Generated with Claude Code