design: L1.13 follow-up — §10 dependency-model entry for v4.lens.match_arm_skeleton by briansrls · Pull Request #3466 · gunb-ai/gunbc

briansrls · 2026-05-21T01:30:00Z

What this PR proposes

Follow-up to PR #3455 (L1.13 Skeleton-collapse lens, merged at 601c90d60). Post-merge inline BLOCKING review surfaced that L1.13 introduces skeleton extraction as a required derived fact but §10's dependency model wasn't updated with the producer/consumer stage — leaving facts-flow-forward (INVARIANTS P2) unresolved.

This PR adds:

§10.1 row — "Match-arm RHS skeleton + histogram" as a shared index, produced by v4.lens.match_arm_skeleton (new derived stage), consumed by L1.13.
§10.2 fourth derived-stage entry — v4.lens.match_arm_skeleton with consumes / produces declaration, reusable-by note (L1.13 + future L1.13.b + future match-as-typed-table lens), and algorithm sketch matching L1.13's classifier (α-rename + matched-arm constructor substitution + histogram + distribution-shape classification).
Heading update — "Three small derived stages" → "Four" to reflect the addition.

The new entry mirrors the existing pattern (match_arm_shape / closed_vocab_scan / concept_home): a small deterministic fold producing a typed shared index that multiple lenses can consume. No framework change; lens framework dependency model stays unified per §10's "no parallel infrastructure" discipline.

Verification

§10 section structure intact:

## 10. Dependency model — lenses are pipeline stages
### 10.1 Shared indices come from existing pipeline stages   (now 9 rows including match-arm skeleton)
### 10.2 Four small derived stages cover what the pipeline doesn't already expose  (was Three)
### 10.3 A lens is a stage with declared dependencies
### 10.4 Parallelism falls out of the dependency graph
### 10.5 What this gives you

L1.13 entry on main (line 1087 in docs/design-dissolution-lens.md) references v4.lens.match_arm_skeleton via the §10.2 entry; the post-merge gap was that §10 itself didn't have the corresponding entry. Now both points reconcile.

Test plan

Documentation only; no test commands. Verification:

grep -n '^### 10\.' docs/design-dissolution-lens.md shows 10.1 → 10.5 in order
grep -n 'match_arm_skeleton' docs/design-dissolution-lens.md returns the §10.1 row + the §10.2 derived-stage entry (multiple occurrences expected)
Section heading "Four small derived stages" (was "Three")

— sent from sunny-wolf-435

Co-Authored-By: Claude Opus 4.7 (1M context) noreply@anthropic.com

…match_arm_skeleton derived stage Follow-up to PR #3455 (L1.13 merged). Addresses post-merge BLOCKING inline review: L1.13 introduces skeleton extraction as a required derived fact but §10's dependency model wasn't updated with the producer/consumer stage — leaving facts-flow-forward (INVARIANTS P2) unresolved. Added: - §10.1 row: "Match-arm RHS skeleton + histogram" produced by new v4.lens.match_arm_skeleton derived stage, consumed by L1.13 - §10.2 fourth derived-stage entry: v4.lens.match_arm_skeleton with consumes/produces declaration, reusable-by note (L1.13, future L1.13.b, future match-as-typed-table lens), and algorithm sketch - Updated heading from "Three small derived stages" to "Four" Mirrors the existing pattern (match_arm_shape / closed_vocab_scan / concept_home) — small deterministic fold producing a typed shared index multiple lenses can consume. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…codex #2 + #3) Address two additional codex BLOCKING findings on PR #3455 (merged): #2 — Outlier auto-fix conflated skeleton-equality holes with executable replacement syntax. "Substitute constructor with _ wildcard" works for COMPARING arms but doesn't produce compilable code when the constructor appears in the RHS. Fix: split Outlier fix-confidence by RHS form: - (a) Constructor NOT in uniform RHS → Direct auto-apply (literal `_ => <uniform_RHS>`) - (b) Constructor IS in uniform RHS → Templated auto-apply (bind the matched value via `c => <RHS_with_c_substituted>`) Explicit note that the wildcard-substitution form is for arm comparison only, not executable code generation. #3 — F14 worked example wrapped the singleton group with `{ kind: ModeledKind }` despite the sub-coproduct having only one member. That's overhead, no discrimination work. Fix: singleton groups become fieldless top-level variants; only non-singleton groups carry `{ kind: <SubKind> }` wrappers. Updated F14 example accordingly; added general rule applicable to all MultiOutlier / Categorical dissolutions. #1 (§10 dependency-model entry) was addressed in commit 260685c earlier on this same branch. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

briansrls

Review metadata

Provider / model: codex / unknown
Commit: 934de7eb · Trigger: schedule
Thinking: 217s wall

BLOCKING (2)

Root Cause

docs/design-dissolution-lens.md v4.lens.match_arm_skeleton is modeled as a classifier summary instead of a carried structural index → make SkeletonReport carry arm ids/normalized RHS per skeleton group plus the RHS-constructor-occurrence fact consumed by the Diff emitter.
docs/design-dissolution-lens.md §10.1/§10.2 adds a producer without wiring the consumer edge → add v4.lens.match_arm_skeleton to the relevant dissolution/L1.13 lens consumes: list or split L1.13 into its own explicitly-consuming stage.

⚠️ The dependency-model addition needs the carried facts and consumer edge made explicit before it is a faithful L1.13 plan.

briansrls · 2026-05-21T02:13:01Z

+
+module v4.lens.match_arm_skeleton
+consumes: v4.compiler.02_parse, v4.compiler.03_resolve
+produces: Map<MatchExprId, SkeletonReport>  // {arm_count, distinct_skeletons, histogram, classifier_shape}


BLOCKING: SkeletonReport is specified as only counts/histogram/classifier, but L1.13 auto-fix needs per-arm skeleton groups and constructor-hole presence to avoid recomputing the stage, violating Facts Flow Forward / P2 single authority.

briansrls · 2026-05-21T02:13:01Z

 produces: Map<FnId, File>               // each fn's primary-concept home file
 // reusable by: L1.8
+
+module v4.lens.match_arm_skeleton


BLOCKING: The new v4.lens.match_arm_skeleton stage is introduced for L1.13, but the downstream v4.lens.dissolution consumes: declaration is not updated to consume it, leaving the one-pipeline dependency model incomplete under THESIS dependency modeling and INVARIANTS P2.

…nstructor-hole presence (briansrls BLOCKING #3466) Findings (Facts Flow Forward / P2 single authority): - SkeletonReport carried only summary counts/histogram/classifier_shape, but the L1.13 auto-fix mechanism (Outlier (a)/(b) split → Direct vs Templated; MultiOutlier/Categorical → templated wrapping-variant names) needs: 1. Per-arm group membership (which arms collapsed to which skeleton-equivalence class) 2. Constructor-hole presence per skeleton (drives Outlier Direct-vs-Templated distinction) 3. Matched-constructor list per group (derives MultiOutlier/ Categorical default wrapping-variant names) Without these, the auto-fix has to re-walk arms = second authority computing the same normalization = P2 violation. Fix: - §10.1 row reworded to explicitly include the new fields. - §10.2 SkeletonReport schema expanded with SkeletonGroup record: { skeleton, arm_ids, constructor_hole_present, matched_constructors }. - Algorithm sketch updated to reflect group-level emission. - Added explicit 'Facts Flow Forward (Practice 3)' clause stating no consumer re-walks arms or re-derives skeleton equivalence. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

… consumes: list (briansrls BLOCKING #3466) Finding: §10.3's v4.lens.dissolution consumes-declaration listed the other §10.2 derived stages but omitted v4.lens.match_arm_skeleton — leaves the one-pipeline dependency graph incomplete and contradicts THESIS dependency-modeling + INVARIANTS P2 single-authority discipline. The dissolution stage IS the L1.13 consumer, so it must declare the edge so the compiler's existing stage-ordering can schedule match_arm_skeleton before dissolution (same machinery as 04_infer after 03_resolve). Fix: add v4.lens.match_arm_skeleton to the consumes list. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

briansrls · 2026-05-21T02:14:54Z

Both findings addressed by commits landed after this review's HEAD (`934de7eb`)

Finding 1 — SkeletonReport modeled as classifier summary instead of carried structural index → addressed in commit 0de6a56cc (docs/design-dissolution-lens.md §10.1 + §10.2):

SkeletonReport now carries groups: [SkeletonGroup] where each SkeletonGroup records:

skeleton: RhsSkeleton — the normalized RHS expression tree
arm_ids: [MatchArmId] — arms in this skeleton-equivalence class
constructor_hole_present: Bool — drives Outlier Direct-vs-Templated auto-apply
matched_constructors: [ConstructorId] — drives MultiOutlier/Categorical default wrapping-variant names

Added explicit Facts-Flow-Forward / P2 clause: no consumer re-walks arms or re-derives skeleton equivalence.

Finding 2 — consumer edge not wired → addressed in commit 16bd01e76 (docs/design-dissolution-lens.md §10.3):

v4.lens.match_arm_skeleton is now in v4.lens.dissolution's consumes: declaration alongside match_arm_shape, closed_vocab_scan, and concept_home, so the existing stage-ordering machinery schedules it correctly.

Same two findings were already raised by briansrls's inline reviews at lines 1623 and 1621 in this review cycle; this codex review wrap re-states them. Both fix commits landed on the same head-move.

— sent from sunny-wolf-435

…(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>

…nickname-detection gap (#3479) * 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> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…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 changed the title PM design: L1.13 follow-up — §10 dependency-model entry for v4.lens.match_arm_skeleton May 21, 2026

briansrls mentioned this pull request May 21, 2026

design: L1.13 skeleton-collapse lens (kills parametric-arm duplication; Practice 11's runtime-symptom catcher; 3 real-corpus findings cited) #3455

Merged

briansrls marked this pull request as ready for review May 21, 2026 01:30

briansrls and others added 2 commits May 21, 2026 01:32

WIP: PM

934de7e

briansrls commented May 21, 2026

View reviewed changes

briansrls and others added 2 commits May 21, 2026 02:14

briansrls merged commit 85ef82b into main May 21, 2026
7 checks passed

This was referenced May 21, 2026

PM #3469

Closed

design: L1.12.b — structural-similarity sub-signature closes L1.12's nickname-detection gap #3479

Merged

briansrls mentioned this pull request May 21, 2026

design: producer-shape factoring + six sub-signature lens bindings + §11 subsumption model (operator-direct emit_rust.dag analysis) #3489

Merged

5 tasks

Navigation Menu

Repository navigation

design: L1.13 follow-up — §10 dependency-model entry for v4.lens.match_arm_skeleton - #3466

design: L1.13 follow-up — §10 dependency-model entry for v4.lens.match_arm_skeleton#3466
briansrls merged 5 commits into
mainfrom
session/sunny-wolf-435-l1-skeleton-collapse-followup

briansrls commented May 21, 2026 •

edited

Loading

Uh oh!

briansrls left a comment

Uh oh!

briansrls May 21, 2026

Uh oh!

briansrls May 21, 2026

Uh oh!

briansrls commented May 21, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

briansrls commented May 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

What this PR proposes

Verification

Test plan

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

briansrls May 21, 2026

Choose a reason for hiding this comment

Uh oh!

briansrls May 21, 2026

Choose a reason for hiding this comment

Uh oh!

briansrls commented May 21, 2026

Both findings addressed by commits landed after this review's HEAD (934de7eb)

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

briansrls commented May 21, 2026 •

edited

Loading

Both findings addressed by commits landed after this review's HEAD (`934de7eb`)