Skip to content

plans/self-applying-lenses: complete the Retrofit-path stub with the full lens audit - #5596

Merged
briansrls merged 6 commits into
mainfrom
session/deep-raven-726
Jun 23, 2026
Merged

briansrls merged 6 commits into
mainfrom
session/deep-raven-726

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Jun 23, 2026

Copy link
Copy Markdown
Contributor

Completes the stub "Retrofit path (fix all current lenses)" section of docs/plans/self-applying-lenses.md (previously 6 lines) with the full audit assigned by the lens-family retrofit/cleanup work item.

What this is

A survey of every src/v2/lens/*.dag (39 top-level modules) classifying each for the produce-and-apply upgrade, into four buckets keyed on how the corrected Node is obtained:

  • A — redundancy / anti-unification → registry ROW of v2.lens.intent_linearity (one engine, N rows). The producer is the anti-unify generalization. Members: simulated_relationship (row 1, landed), structural_similarity, identical_variant_payload, table_decision_tree, cost's RunTime-axis catalog; plus fact_cardinality / languages_consumer_census / the extdeps_shape_transport_policy fusion-fork tell as consolidation ratchets (canonical form is picked, not computed).
  • B — decidable non-redundancy wall, fix = single mechanical deletion: unused_parameters (the lone clean instance; flag-gated, proposal-only — delete-vs-repair judgment + call-site cascade).
  • C — detect-only residue: C1 RatchetForever (undecidable by Rice / domain knowledge — complexity, synthesis, unit_modeling, idempotency, ownership); C2 decidable walls whose §5 end-state is construction (make it unwritable), not a patch lens (effect, layering_imports, resolved_imports, visibility, coverage, mock_totality, leaf_model_verification, …).
  • D — not a detector: the apply/write API (application/application_serializer), the registry engine itself (intent_linearity/registry), affected_set/edit_locus/testgen/subsumption, and the *_test.dag / producer fixtures.

Load-bearing finding

Produce-and-apply has real leverage almost only on bucket A — the one family where the same read that measures the redundancy computes the fix. For non-A walls the fix is chosen, researched, or (per §5 construction-first) should be dissolved at the substrate; upgrading them to a produce-and-apply lens would cement a validator where a wall was the right end-state. So the high-value retrofit is realizing the A rows over the shared anti-unify kernel, not N bespoke appliers.

Scope

Documentation only — no code, no deletes. The A-row realizations and C2 constructions are each separately gated (§6). Verified against the live tree (construction_justification classes, scaffold/Unrealized verdicts, and the pivotal A/B modules read directly).

🤖 Generated with Claude Code

…e full lens audit

Survey of every src/v2/lens/*.dag (39 modules) for the produce-and-apply
upgrade, classified into four buckets by how the corrected Node is obtained:

  A — redundancy/anti-unification -> fold into the v2.lens.intent_linearity
      registry as a ROW (simulated_relationship row 1 landed; structural_similarity,
      identical_variant_payload, table_decision_tree, cost's RunTime catalog;
      fact_cardinality / languages_consumer_census / extdeps fusion-fork as
      consolidation ratchets)
  B — decidable non-redundancy wall whose fix is a single mechanical deletion
      (unused_parameters; flag-gated, proposal-only)
  C — detect-only residue: C1 RatchetForever (undecidable by Rice / domain
      knowledge) + C2 decidable walls whose end-state is §5 construction, not a
      patch lens
  D — not a detector (the apply/write API, registry, affected_set engine,
      testgen, harness/fixtures)

Load-bearing finding: produce-and-apply has real leverage almost only on bucket
A, where the anti-unify read that measures the redundancy also computes the fix.
Non-A walls stay detect-only until their dissolve_on construction lands;
upgrading them would cement a validator where a wall was the right end-state.

No code/deletes executed — the classification is the deliverable.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review June 23, 2026 01:43
…r intent-linearity duality

Reconciles the audit's C2 placement of fact_density with the Consolidation-map
fork-check (#5591), which names it the other half of intent-linearity. Both are
right at different layers: the over/under duality (redundant spec vs hollow
carrier; description==information two-sided) is CONCEPTUAL, but the mechanism
diverges — the over-side minimal form is computed by anti-unify (a registry
row), the under-side fix needs domain knowledge (ground 4926 into contact_count)
so it is construction-residue, not an auto-apply row. Same concept, divergent
mechanism; that kills the apparent contradiction once both land in the file.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Jun 23, 2026

Copy link
Copy Markdown
Contributor Author

Handing off the one delta from the duplicate audit (#5598, which I'm closing as superseded by this PR). Your A-row table is more complete than mine on coverage (you fold fact_cardinality / extdeps_shape_transport_policy into the redundancy family; I'd parked those in C). The only thing mine carried that yours doesn't is two per-row tags the plan's own refinements make load-bearing — graft if you agree:

  • scheme (refinement 3, §S3 taxonomy): the term-layer rows are distinct schemes — simulated_relationship = foldl, cost's catalog = cost-recurrence reduce (SumCost/ProductCost), table_decision_tree = table-lookup (you already flag "not a fold"). This tag is what tells the apply-half which minimal form to emit (a fold vs a TotalMap dispatch vs a scan) — without it the producer can't pick. The type/variant/data-decl rows (structural_similarity/identical_variant_payload/languages_consumer_census) aren't fold-schemes — their "scheme" is the binder you already name (type parameter / merged arm / parameterized row).
  • §1-axis (the "honest disanalogy" section: "a row must tag which one it improves"): all your A-rows are change-time except cost = run-time (and idempotency, if you add it, is run-time algebraic op∘op→op). The axes genuinely diverge (an 8-byte unroll is change-time-redundant but O(1)-runtime), so the tag isn't decoration — it's how a row declares which §1 cost it displaces.

Suggest one extra column scheme · §1-axis on the A-table. That's the whole delta; no other graft needed.

— sent from sunny-crab-640

gunbai-bot Bot pushed a commit that referenced this pull request Jun 23, 2026
The doc-reachability floor fix (linking the orphaned intent-linearity design
draft) requires editing the generated-artifact authority dsl/gunbc/roadmap_authority.dag
+ regen, which collides with #5596 and is owned by witty-crane-380 (the orphan
came in with #5584). Handing the queue-wide unblock to a standalone PR; #5600
stays the pure complexity RunTime-axis feature and rebases once main is green.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
@briansrls
briansrls merged commit 7ed1505 into main Jun 23, 2026
2 checks passed
@briansrls
briansrls deleted the session/deep-raven-726 branch June 23, 2026 05:37
briansrls added a commit that referenced this pull request Jun 23, 2026
…ows (one engine, N rows, two axes). cost.dag computes runtime cost as a fold_node over the AST (SumCost for a sequence, ProductCost for a nested loop -> AsymptoticClass). Formalize its DECIDABLE rewrite catalog -- the §5 'O(n^2)->O (#5600)

* WIP: Bring complexity into the intent_linearity registry as RunTime-axis rows

* WIP: Bring complexity into the intent_linearity registry as RunTime-axis rows

* WIP: Bring complexity into the intent_linearity registry as RunTime-axis rows

* Drop ROADMAP doc-link from #5600 — unblock fix moves to a standalone PR

The doc-reachability floor fix (linking the orphaned intent-linearity design
draft) requires editing the generated-artifact authority dsl/gunbc/roadmap_authority.dag
+ regen, which collides with #5596 and is owned by witty-crane-380 (the orphan
came in with #5584). Handing the queue-wide unblock to a standalone PR; #5600
stays the pure complexity RunTime-axis feature and rebases once main is green.

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

* complexity_rewrite: match rewrite preconditions on asymptotic class, not a hand-rolled SymbolicCost wildcard

Replaces cost_is_nested_product (a nested match over the closed SymbolicCost
coproduct with _ => false arms -- non-fold residue per #5566) with class-equality
against cost.dag's exhaustive asymptotic_class_of_cost. The module now carries zero
wildcard-over-coproduct matches (single authority, total), and minimized_class
inherently checks the realized class equals the rewrite's before-class -- addressing
both non-blocking reviewer notes on the earlier APPROVE. Semantics unchanged: an
O(n^2) cost (ClassPolynomial degree 2) is rewritable to ClassLinear; linear / sum
costs are not.

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

* catalog_sound_test: drop the removed 'applies' field from bogus rewrite controls

Follow-on to the class-based refactor: ComplexityRewrite no longer carries an
'applies' fn field, so the identity/widening RED-control constructors must not set it.

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

* intent_linearity: RunTime axis is a candidate detector, not the redundancy wall (§5 fail-closed)

Addresses the REQUEST_CHANGES finding: wiring the RunTime row into chain_is_redundant
made the wall flag a genuine all-pairs O(n^2) loop as 'redundant intent' -- a §5
fail-OPEN (a false positive on the wall) since the row's sufficiency is ungrounded.

Fix: the two axes now compose differently. chain_is_redundant folds ONLY the ChangeTime
rows (anti-unification proves redundancy -> sound wall, no false positive), so
level_is_linear / body_is_linear never call a genuine program redundant. The RunTime axis
is read via a new chain_has_runtime_rewrite_candidate -- honestly a CANDIDATE (O(n^2) is the
decidable necessary condition; sufficiency waits on the independence carrier), so it does
not feed the wall. Both rows stay in linearity_registry() (one engine, N rows, two axes);
cost_axis_equal partitions them by axis with an exhaustive match (no wildcard residue).

Witnesses: nested_loop_not_changetime_redundant (the wall does NOT flag a genuine nested
loop) + nested_loop_is_runtime_candidate (the RunTime axis still fires) green by execution.

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

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant