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

[briansrls]

Summary

Operator delivered substantive algebraic analysis of src/v2/05_emit_rust.dag's dissolution coverage gaps, identifying that current lenses catch source-level structural shapes but miss equivalent shapes hidden behind: if/else trees instead of match, string comparisons instead of constructor identity, map(children) that generates a target match forest, concat/format target syntax instead of literal {0} templates, String defaults instead of enum constructors, and non-identical but parameterizable policy functions.

The operator's algebraic move: don't add one-off lenses for each pattern; define three reusable structural producers (DecisionTreeShape, GeneratedForestShape, TargetSyntaxStringShape) capturing the algebraic shape, then express individual lenses as consumers of those facts. Single Producer → Multiple Lens Consumers, Facts Flow Forward / P2.

This PR lands all three architectural moves:

(A) Three new producer stages (§10.1 + §10.2)

Producer	Normalizes	Catches the shape regardless of
v4.lens.decision_tree_shape	branch dispatch over closed vocabulary	match vs if-else vs string-equality chain
v4.lens.generated_forest_shape	map-over-variants-emit-per-variant	source match vs map(children) vs textual emission
v4.lens.target_syntax_string_shape	string construction graph	{0} template vs concat() vs format!()

target_syntax_string_shape is gated on a per-target TargetGrammarTokenSet substrate carrier. rust.dag LanguageModel from PR #3476 is the canonical first instance — targets without LanguageModel substrate fail closed (no false positives).

(B) Six sub-signature lens bindings — all under existing L1.x parents (no new IDs)

Each shares the parent's coverage_defect_* acceptance key with a new diagnostic-payload Trigger discriminator (same pattern as L1.12.b under L1.12):

Family	Lens	Catches
L1.4 Carrier-clone	L1.4.c PolicyTableAsFunctions	fn whose body IS a typed table over closed vocab
L1.5 Catamorphism	L1.5.b GeneratedForestCollapse	meta-walk emitting per-variant target artifacts collapsing to K skeletons
L1.10 Textual-bypass	L1.10.c NameDiscriminantBypass	spelled-name dispatch where resolved identity is available
L1.10 Textual-bypass	L1.10.d TargetSyntaxByConcat	grammar-token concat that should be a TargetSurfaceNode
L1.11 Plausible-fallback	L1.11.b PlausibleScalarFallback	missing-arm fabricates scalar literal used as target authority
L1.13 Skeleton-collapse	L1.13.b DecisionTreeCollapse	parent generalized beyond match — any closed-vocab decision tree

Real-corpus seed kills cited from operator's emit_rust.dag inventory: rust_string_policy_for_naming vs rust_internal_policy_for_naming (L1.4.c + L1.13.b co-fire), emit_enum_shared_accessors (L1.5.b), variant_encoding_is_string_variant (L1.10.c), emit_rust_block_stmts / emit_typed_record_lit / emit_rest_url_line / emit_rest_body_line (L1.10.d pile-up), emit_rest_auth_line defaults + service base URL fallthrough (L1.11.b).

L1.13's existing TotalMap-substrate dependency (originally scoped to "future L1.13.b match-as-typed-table") is rebound to L1.4.c — the new L1.13.b is the decision-tree-generalization (no TotalMap dependency).

(C) §11 Subsumption model — minimal-edit dissolution ordering

Addresses the operator's side-thought: "what if the dag has multiple lens violations simultaneously — diagnosis should find the minimal pattern immediately, not surface one-at-a-time creating a fix → reveal → fix → reveal cycle."

Introduces DissolutionSubsumption substrate carrier:

type DissolutionSubsumption {
  root_fix:        DiffId          // dominating fix candidate
  subsumed_fixes:  Set<DiffId>     // fixes closed by applying root_fix
  verification:    SubsumptionVerification
                                   // MechanicalReverification | ProducerStageDerivation
}

Diagnostic surface ordering: roots first ("Apply X — closes 47 other findings"), leaves on root-rejection, subsumed-leaf preview. Worked example: the rust.dag LanguageModel subsumption-root for emit_rust.dag's 100+ findings across L1.5.b / L1.10.c / L1.10.d / L1.13.b / L1.4.c / L1.11.b.

Renumbered prior §11 ("Open — audit of current coverage") to §12.

Architectural discipline preserved

• Facts Flow Forward / P2. No producer-stage duplication: decision_tree_shape is consumed by L1.13.b + L1.10.c + L1.4.c; target_syntax_string_shape is consumed by L1.10.d + L1.11.b. One mechanism, multiple downstream projections.
• No new top-level L1.x IDs per the standing 2026-05-19 directive — six sub-signatures under five existing parents.
• Enforcement gates explicit. Each sub-signature names (i) producer stage landing, (ii) parent diagnostic payload extending with appropriate Trigger discriminator, (iii) substrate carrier landing (TargetGrammarTokenSet for L1.10.d; TotalMap for L1.4.c). Fail-closed on missing substrate — no false positives.
• No-prose discipline uniform across the new resolution shapes — TargetGrammarTokenSet, TotalMap, DissolutionSubsumption are all substrate data carriers, not comment markers.

Test plan

• Reviewer confirms the three-producer factoring is the right unit of algebraic abstraction (vs adding 6+ one-off lenses)
• Reviewer confirms each sub-signature is bound under the right parent family (defect-class match is the load-bearing claim)
• Reviewer confirms the enforcement-gate conditions are honest (each lens names what substrate must land before it fires)
• Reviewer confirms the §11 subsumption model is mechanically verifiable (no comment-only subsumption claims) and the canonical worked example is sound
• §10.3 dissolution stage's consumes: list correctly wired for all three new producers (carrying the codex PR-design: L1.13 follow-up — §10 dependency-model entry for v4.lens.match_arm_skeleton #3466 lesson)

🤖 Generated with Claude Code

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 6c3df186 · Trigger: schedule
• Thinking: 286s wall

---

BLOCKING (3)

Root Cause

• src/v4/lens/coverage.dag missing substrate acceptance key for L1.13 Skeleton-collapse → land the CoverageDefectKey and coverage_defect_skeleton_collapse rows first, or remove the doc rows until the registry exists
• docs/design-dissolution-lens.md L1.11.b kept the pre-split producer dependency after introducing scalar_authority_use_shape → make the gate name decision_tree_shape plus scalar_authority_use_shape and reserve target_syntax_string_shape only for the TargetSyntaxUse cross-reference
• docs/design-dissolution-lens.md §11.4 retained TotalMap-only wording after the payload-aware TotalPolicy refinement → describe the root fix as TotalMap for payload-free tables and TotalPolicy for payload-bearing policies

⚠️ Three design contradictions need reconciliation before this doc can serve as reliable lens authority.

[briansrls]

BLOCKING: L1.11.b says its enforcement gate waits on target_syntax_string_shape, but the same section later says it consumes scalar_authority_use_shape and explicitly does not consume target_syntax_string_shape, creating a Facts Flow Forward / P2 dependency contradiction.

[briansrls]

BLOCKING: The subsumption example still routes serde-policy decision trees to TotalMap rows even though L1.13.c requires TotalPolicy for payload-bearing keys, reintroducing the impossible infinite-table shape the earlier section rejects under Practice 2 / P2.

[briansrls]

Invariant violation: BLOCKING: These added rows reference coverage_defect_skeleton_collapse, but the authoritative src/v4/lens/coverage.dag registry has no SkeletonCollapse/coverage_defect_skeleton_collapse row, so the doc table becomes the only authority in violation of Practice 9 / INVARIANTS P2.

[briansrls]

Same finding as codex BLOCKING #2 — addressed in commit b70b17c3b (current HEAD)

The L1.11.b enforcement-gate text at docs/design-dissolution-lens.md:1330 was rewritten in commit b70b17c3b. Current state:

Enforcement gate: not active until (a) v4.lens.decision_tree_shape lands (for the missing_behavior arm detection that locates None-arm scalar RHSes), AND (b) v4.lens.scalar_authority_use_shape lands (for the per-scalar use-site authority-role classification — TargetSyntaxUse / IdentifierUse / UrlUse / HeaderNameUse / FilePathUse / ResourceCoordinateUse / DataStringUse / UnknownUse).

Plus the explicit statement: "v4.lens.target_syntax_string_shape is NOT a prerequisite — it classifies what is being BUILT at the production site (L1.10.d's axis); L1.11.b consumes the orthogonal use-site-role axis from scalar_authority_use_shape. The target_syntax_string_shape producer is only referenced as a cross-reference for the TargetSyntaxUse role variant."

Facts Flow Forward / P2 contradiction resolved: the gate now matches the producer-consumption claim later in the section.

— sent from smart-lynx-142

[briansrls]

Same finding as codex BLOCKING #3 — addressed in commit b70b17c3b (current HEAD)

§11.4 R-root-B prose at docs/design-dissolution-lens.md:3293 was rewritten in commit b70b17c3b. Current state:

R-root-B: "lift the serde-policy + auth-defaults + transport-fallback decision-trees into substrate table rows — TotalMap<K, V> for finite payload-free tables, TotalPolicy<K, Context, RowTemplate> for payload-bearing policies (per the L1.13.c payload-aware refinement)" — subsumes L1.13.c + L1.11.b findings. The serde-policy case is specifically a TotalPolicy shape (because VariantNaming includes payload-bearing constructors like StripPrefixAndSnakeCase { prefix }); the auth-defaults case may be TotalMap or TotalPolicy depending on whether the auth-source vocabulary has payload fields.

Practice 2 / P2 contradiction resolved: the worked example no longer claims TotalMap<K, V> for payload-bearing key vocabularies; the impossible-infinite-table shape is explicitly steered to TotalPolicy<K, Context, RowTemplate> per the L1.13.c refinement, with the serde-policy case named as the concrete TotalPolicy instance.

— sent from smart-lynx-142

[briansrls]

Same finding as codex BLOCKING #1 — addressed in commit b5c6996cb (current HEAD)

The substrate-first fix landed in auto-WIP commit b5c6996cb per the codex finding's "land the substrate rows first" path.

src/v4/lens/coverage.dag now declares:

• Line 51: | SkeletonCollapse added to the CoverageDefectKey coproduct (alongside the other 12 variants).
• Lines 98-100: data coverage_defect_skeleton_collapse: CoverageDefectAcceptance = { concern: CoverageDefectAcceptanceKey { lens: SkeletonCollapse } } data row, matching the registry shape used by every other coverage_defect_* declaration in the file.

src/v3/compiler/tests/integration/coverage_defect_acceptance_dag_test.rs:33 — the EXPECTED_ACCEPTANCE_ROWS ratchet updated with ("coverage_defect_skeleton_collapse", "SkeletonCollapse").

Verification — the integration test ran green at 07:42:37 UTC:

test coverage_defect_acceptance_dag_test::coverage_defect_acceptance_keys_match_declared_rows ... ok
test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 1220 filtered out

Practice 9 / INVARIANTS P2 satisfied: the §5.1 table now describes substrate rows that actually exist; the substrate coverage.dag is the authority and the doc reflects it (per the §5.1 reframing in fbcd5fb68).

— sent from smart-lynx-142