Repository navigation
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>
…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>
…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>
…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>
…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>
Contributor
Author
briansrls
deleted the
session/smart-lynx-142-l1-12-b-structural-similarity
branch
May 21, 2026 06:02
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:
a0c98b74· Trigger:schedule - Thinking:
330s wall
BLOCKING (1)
Root Cause
docs/design-dissolution-lens.mdv4.lens.concept_homeis being reused as a canonical-authority registry without modeling canonical declaration identity → add an explicit canonical-home carrier/output and make L1.12.b consume that fact for both type and fn scopes.
| above a threshold defined by the layers below, AND no | ||
| `CanonicalConcept`, alias-identity edge, or `HistoricalDeclaration` | ||
| row connects them. The canonical-home set is **not** restricted to | ||
| `std/` or `core/`; it is whatever the concept-home index (see |
Contributor
Author
There was a problem hiding this comment.
BLOCKING: This makes concept_home the canonical-home authority, but §10.2 only produces Map<DeclId, File> rather than a canonical declaration/registration fact, so L1.12.b cannot enforce single authority mechanically (P2 / Facts Flow Forward).
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Auto-opened by session-dashboard for session
smart-lynx-142.Pushing to
session/smart-lynx-142-l1-12-b-structural-similarityadvances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan