Skip to content

LensApplicationConfig carries only the parameter it represents - #9041

Merged
briansrls merged 3 commits into
mainfrom
session/witty-badger-734-lens-config-params
Aug 24, 2026
Merged

briansrls merged 3 commits into
mainfrom
session/witty-badger-734-lens-config-params

Conversation

@gunbai-bot

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

Copy link
Copy Markdown
Contributor

Reproducing the receipt below requires #9027. Clean main currently refuses to emit this entry outright: dag/test/manual/command_runner_local_argv_receipt_test.dag ends in a trailing unattached // block, which DESIGN §4c refuses, and an --entry compile is scoped in what it emits but whole-tree in what it parses (indexed 3851 modules … resolved 88 sources). #9027 fixes that file. The measurements here were taken on clean main with that one blocker lifted and nothing else changed.

Removes two type parameters from v2.lens.application LensApplicationConfig that are declared but reachable from no field, variant payload, or other representation-bearing position.

-type LensApplicationConfig<Output, Budget, Projected>
+type LensApplicationConfig<Budget>
   = LensIntrospect
   | LensEnforce { budget: Budget }

Budget is the only parameter the coproduct represents. The sole instantiation is in apply_advisory_lens, where all three arguments were already Report.

Why this is a defect rather than a style preference

The interpreter erases unused type parameters; Rust does not. The Rust emitter is faithful — it emits exactly what the declaration says — and rustc rejects the result, because an unused type parameter is an error and the serde derives cannot infer for parameters appearing in no field. So the declaration is well-formed on one realization path and ill-formed on another.

Corpus receipt

Measured with docs/probes/curated_cargo_probe_one.sh over entry src/v2/lens/affected_set.dag (emit → cssl_assemble → cargo build --release --lib), on clean main with a freshly built compiler.

Both arms differ by exactly the two lines under test, and each printed a positive control proving its edit applied before the measurement ran.

The prediction was registered before the run, including which row would survive: the E0308 at the budget() clone belongs to the established ABSENT_CLONE_BOUND mechanism and is unrelated to parameter arity.

control this PR
board primary sites 122 112
v2_lens_application.rs primary 11 1
E0392 board-wide 4 0
E0282 board-wide 9 3

Ten rows retired: E0392 ×4 (Output and Projected never used) and E0282 ×6 (the #[derive] line cannot infer for phantom parameters). The six E0282 removed board-wide are precisely the six that were in this file.

No row relocated. Thirteen error classes are identical across both arms:

E0308 43/43   E0004 19/19   E0560 9/9   E0277 6/6   E0614 5/5
E0609  5/5    E0599  5/5    E0369 4/4   E0310 4/4   E0425 3/3
E0061  3/3    E0631  2/2    uncoded 1/1

Rows were removed, not moved. The surviving E0308 is measured independence of the two mechanisms, not assumed independence.

Scope

Frozen to the one source decision. No other semantic change.

EnforceableLens and EnforcedApplication keep all three parameters and are deliberately untouched: both structurally represent the full trio (EnforceableLens via Lens<Output> and LensEnforcement<Output, Budget, Projected>; EnforcedApplication reaches all three through its enforceable_lens field). They are not instances of this class.

What this PR does not claim

It does not establish any general rule about undeclared unused generic parameters, and takes no credit toward the class repair. It is one bounded source repair with a complete corpus receipt.

Nor does it resolve how Rust should realize a parameter that is intentionally phantom. That is a separate target decision. Today the emitter already synthesizes PhantomData for unused parameters in struct and alias realization (struct_unused_param_names, alias_unused_param_names) while coproduct realization has no analogous carrier — which is why only the coproduct surfaced. Extending that existing policy to coproducts is the class repair and is compiler-side; this PR does not attempt it.

Prior art

Dead LensApplicationConfig structure was previously removed pending a real reading consumer, and the original surface was mechanically filled rather than explicitly phantom-designed — evidence that these parameters are residue rather than reserved for a planned variant.

Two of the three declared type parameters are reachable from no field,
variant payload, or other representation-bearing position. The interpreter
erases them; Rust does not, so the declaration is well-formed on one
realization path and ill-formed on the other.

Measured on clean main with the #9027 annotation blocker lifted and a
freshly built compiler: 122 -> 112 primary sites, E0392 4 -> 0 and
E0282 9 -> 3. No row relocated -- thirteen other error classes are
identical across both arms.

Frozen to the one source decision. EnforceableLens and EnforcedApplication
keep all three parameters and are untouched: both structurally represent
the full trio.

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

gunbai-bot Bot commented Aug 23, 2026

Copy link
Copy Markdown
Contributor Author

Verified the two structural claims independently of the receipt, and one of them is stronger than the body states.

Output and Projected are structurally absent — by reading the whole declaration, not by inference from the E0392s. The type has exactly two variants and one payload field between them:

type LensApplicationConfig<Output, Budget, Projected>
  = LensIntrospect
  | LensEnforce { budget: Budget }

LensIntrospect carries nothing; LensEnforce carries budget: Budget. There is no third position for either parameter to be reachable from. That is the StructurallyRepresented question answered from the declaration alone, which is what makes this decidable rather than a judgement about whether anything currently uses them.

The sibling is out of class by structure, and it is worth stating why the parallel does not hold. EnforcedApplication<Output, Budget, Projected> reaches all three: enforceable_lens: EnforceableLens<Output, Budget, Projected> carries Output and Projected through, and budget: Budget carries the third directly. So the three-parameter shape is not a module-wide convention being broken here — it is a shape the sibling genuinely needs and this type never did.

The blast radius is exactly one call site, corpus-wide, and I do not see that number in the body. grep -rn "LensApplicationConfig" --include=*.dag . returns two lines total: the declaration at :75 and a single use at :479, config: LensApplicationConfig<Report, Report, Report> — both in this file. So this is not a two-line diff whose consequences live elsewhere; the declaration and its only consumer are adjacent, and <Report, Report, Report> collapsing to <Report> is the whole downstream effect. Worth stating explicitly, because a reader seeing a generic-arity change on a shared type will reasonably assume it needs a corpus sweep to be safe. It does not, and that is checkable in one grep.

On the reachability-read-as-occupancy scruple, which the earlier discussion took seriously and correctly: it is discharged here by the module's own history rather than by occupancy. Dead LensApplicationConfig structure was previously removed pending a real reading consumer, and the original surface was mechanically filled rather than explicitly phantom-designed — so these are residue, not a placeholder for an unbuilt variant. The general form of that argument: an undeclared unused generic parameter is not a valid representation of future intent. Future intent has three honest spellings — add the parameter with the variant that uses it, declare it phantom now, or represent it in current structure — and inferring it from occupancy zero is not one of them.

Note the receipt cannot be reproduced on main as it stands today: clean main refuses this entry outright on the trailing-annotation break, so #9027 has to land first. Good that the body leads with that.

@gunbai-bot

gunbai-bot Bot commented Aug 23, 2026

Copy link
Copy Markdown
Contributor Author

The witnesses failure here is inherited from main, not caused by this PR, and I am deliberately not pushing a fix for it.

This PR's complete diff is one file, two lines (src/v2/lens/application.dag). It touches no ArgvCommand site and no file under dag/gunbc/.

The failure:

required-ci: FAILED PHASE floor refused: subject=50d7fc43c0d97730 modules_resolved=3847
dag/gunbc/runner_slot_provision.dag:240:28: error: field 'argv' not found in type 'ArgvCommand'
dag/gunbc/runner_slot_provision.dag:240:14: error: sole_constructor type 'ArgvCommand' cannot be constructed outside its defining module
dag/gunbc/runner_slot_provision.dag:240:14: error: missing required field 'program'
dag/gunbc/runner_slot_provision.dag:240:14: error: missing required field 'arguments'
required-ci: phases_run=3 failed=1

Main's own witnesses run at faf658346 — the exact commit this branch is cut from — fails byte-identically: same file, same line 240, same four errors, same phases_run=3 failed=1. Run 32646482842.

The cause is a partially-applied migration on main: extdeps.exec.command ArgvCommand is now sole_constructor { program, arguments } (the argv construction wall), while this one call site still constructs the old ArgvCommand { argv: ... } shape.

The fix is already in flight as #9031 ("Convert the one ArgvCommand site the seal missed, through a builder rather than by widening the seal"), which touches dag/gunbc/runner_slot_provision.dag among others and is OPEN/MERGEABLE.

Pushing a duplicate repair here would collide with #9031 on the same file, and would break this PR's freeze to a single source decision. This PR should go green once #9031 lands; it needs no change of its own.

Two other notes for whoever sequences the queue:

  • This PR's corpus receipt additionally depends on Main emission is refusing on a trailing annotation, and no required phase can see it #9027. Clean main refuses to emit the src/v2/lens/affected_set.dag entry outright, because dag/test/manual/command_runner_local_argv_receipt_test.dag ends in a trailing unattached // block that DESIGN §4c refuses, and an --entry compile is scoped in what it emits but whole-tree in what it parses (indexed 3851 modules … resolved 88 sources). The 122 → 112 measurement in the body was taken on clean main with that one blocker lifted and nothing else changed. That is stated in the first line of the PR body as well.
  • The two blockers are unrelated to each other and to this diff; this PR sits behind both without contributing to either.

— sent from witty-badger-734

gunbai-bot Bot pushed a commit that referenced this pull request Aug 24, 2026
…lared, not implied

Review 55260 is right that "proposes no repairs" was doing two jobs at once. Declining
to pre-decide a fix is a stance on repair design; §4b(2) separately forbids leaving a
discovered class with no stated trigger, and the document had conflated the two.

Each of the six now carries a disposition and a trigger. A is a repair in flight
(#9041) with the one question the counterfactual cannot answer named and handed to the
module's author. C is owned by the corpus-wide ABSENT_CLONE_BOUND population and gets
no second trigger here, because a second one would be a second authority for one class.
D's lane is #8952. B, E and F are declared UNOWNED -- 7 rows between them, no lane holds
them -- with the promote-to-measured counterfactual named for each. Declaring them
unowned is the disposition: it makes their absence countable, where inventing a lane row
would manufacture an owner that does not exist.

The trigger for a read mechanism is an executed counterfactual, which is a trigger and
not a repair -- the same order the two measured mechanisms here already went through.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@briansrls
briansrls merged commit 04e352a into main Aug 24, 2026
2 checks passed
@briansrls
briansrls deleted the session/witty-badger-734-lens-config-params branch August 24, 2026 01:32
briansrls pushed a commit that referenced this pull request Aug 24, 2026
… each with its evidence status (#9068)

* Five compiler-side mechanisms behind the affected-set emission board, each with its evidence status

Partitions the 24 rows landing in v2_lens_application.rs, std_change.rs and
v2_lens_affected_set.rs into six mechanisms with no residue; documents the five
compiler-side ones and names the sixth as already-owned so the arithmetic closes.
Two are measured by executed counterfactual, three are read from rustc text plus
.dag source, and that distinction is carried per-mechanism rather than flattened.

Proposes no repairs, deliberately.

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

* Pin the reproduction and script the blocker-lift; drop the positional citations

Review 55234, two findings, both real.

The recipe measured `$(git rev-parse HEAD)` while the board is pinned to faf6583,
and named the parse blocker without saying how to lift it — so run the documented
recipe at the documented tree and it refuses with EMIT_REFUSE and produces nothing.
It now checks out the pinned SHA, takes the one repaired file from #9027's merge
commit, and passes the pinned SHA to PROBE_EXPECT_BASE_SHA. It also states why the
resulting HEAD-vs-tree difference cannot be misread by the stale stamp of defect 2:
the lifted file is dag/ subject data, case 1 of this document's own discriminator.

Six positional `.dag:NN` citations sat beside symbols that already named the same
declaration; all are dropped, and the three rt_functions() call sites are named by
their enclosing symbols instead of by grep line prefixes. What remains is the
file:line:col inside verbatim rustc output against the generated mirror, which is
the no-symbol-exists case §3 leaves to a position — now said explicitly.

Also: the count above the defect list said two while listing three.

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

* Give every mechanism a disposition and a next trigger; unowned is declared, not implied

Review 55260 is right that "proposes no repairs" was doing two jobs at once. Declining
to pre-decide a fix is a stance on repair design; §4b(2) separately forbids leaving a
discovered class with no stated trigger, and the document had conflated the two.

Each of the six now carries a disposition and a trigger. A is a repair in flight
(#9041) with the one question the counterfactual cannot answer named and handed to the
module's author. C is owned by the corpus-wide ABSENT_CLONE_BOUND population and gets
no second trigger here, because a second one would be a second authority for one class.
D's lane is #8952. B, E and F are declared UNOWNED -- 7 rows between them, no lane holds
them -- with the promote-to-measured counterfactual named for each. Declaring them
unowned is the disposition: it makes their absence countable, where inventing a lane row
would manufacture an owner that does not exist.

The trigger for a read mechanism is an executed counterfactual, which is a trigger and
not a repair -- the same order the two measured mechanisms here already went through.

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

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Aug 24, 2026
…ry instrument (#9132)

* Bankrupt the measurement corpus: delete every transcription, keep every instrument

Operator ruling, 2026-08-24: less measuring, more fixing, and switch hard back
to qualitative analysis. Measurement documents go out of date fast and have to
be deleted and rewritten constantly, so the corpus is bankrupted rather than
maintained -- as the ~30k-line doc corpus was on 2026-06-16. History keeps it.

WHAT IS DELETED: 164 files, 44,736 lines under docs/probes/ -- every .md board,
every .tsv/.json/.txt/.log/.gz capture. WHAT SURVIVES: all 31 committed .sh/.py
instruments, untouched.

THE CUT IS ASYMMETRIC BY CONSTRUCTION: what is deleted is what cannot be
re-derived from the tree; what survives is what re-derives it.

WHY, with the receipt that priced it. The affected-set emission board's
mechanism A -- its only row carrying measured status with an executed
counterfactual -- was already fixed when the board merged:

  21:32:56  #9041 fixes it (LensApplicationConfig carries only the parameter
            it represents)
  21:33:04  #9068 merges the board documenting it as a live defect

Eight seconds. The board also named the wrong layer: it proposed an emitter
carrier migration, a coproduct analogue of struct_unused_param_names, where the
actual repair was +2/-2 in one .dag file dropping parameters that appear in no
payload -- a model fix, not an emitter fix. Mechanism B on the same board is
independently stale (smart-ram-730). Two of five wrong, on the newest board we
had, and a lane had already selected mechanism A as its next work on the
board's authority.

THE RULE, closing a question DESIGN explicitly left open: name the instrument,
never transcribe its output. This is §3's cite-the-symbol-not-the-position rule
extended from citations to measurements, for the same reason -- a transcribed
number is unreachable from the run that owns it, so it rots without anyone
touching either end.

WHY THE INSTRUMENTS SURVIVE, since one census argued otherwise. Enumerating
what they were load-bearing for found every apparent consumer to be a
data-colon-String prose note naming the filename, joined by witnesses asserting
that the note contains that filename -- nothing in the corpus executes any of
them, so those witnesses ratify that prose mentions a script: permanently
green, cited as coverage, §4b's decoration. That census reads as a mandate to
delete the instruments too, and it is wrong: it enumerated .dag consumers, and
the real consumers are lanes. While it was being taken, a peer re-ran
docs/probes/curated_cargo_probe_one.sh and re-derived the emission board's
headline from source. Deleting instruments would also refute this very rule --
naming an instrument that no longer exists is exactly the stale citation the
rule is derived from.

WHAT THIS DOES NOT CLAIM. The cut leaves a named residue it does not repair:
gitignore un-ignore rows for deleted paths, prose notes across ~20 modules
citing them, and the witnesses above, all still green over dead names. That
residue is the next cut, not a gap this one closes. DESIGN.md is NOT
regenerated here -- dag/gunbc/design_document.dag carries the authority edit and
the projection is blocked on the same generator deadlock as #9098, so the drift
gate will flag it. Declared, not hidden.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01DRMbwdtHZxTiMNZD5WLS3P

* Delete the instruments too: an ad-hoc script is unmodeled realization

Operator ruling, 2026-08-24: "we shouldn't have adhoc scripts in the repo -
those would need to be written in .dag if they were really needed."

This completes the cut. docs/probes/ is now gone whole -- 195 files, 50,601
lines across both commits -- and no .sh or .py survives anywhere in the
repository outside .githooks.

THE REASON IS §6, NOT SCOPE. A hand-authored shell or Python script implementing
semantics already expressible in .dag is unmodeled realization, one of §6's named
scaffold tells. If a measurement is worth re-deriving it is worth an entry point;
if it is not worth an entry point it is not an instrument, it is a one-off.

IT ALSO RESOLVES THE RULE RATHER THAN EXEMPTING IT. The previous commit kept the
instruments partly because "name the instrument, never transcribe its output" is
unsatisfiable if the instrument is deleted -- naming a file that no longer exists
is the stale citation the rule is derived from. Under this ruling the thing named
is a .dag entry point, so the rule has a live referent by construction and needs
no carve-out.

RULED AGAINST A LIVE OBJECTION, recorded because the objection was correct on its
own facts and still lost. A peer had re-run docs/probes/curated_cargo_probe_one.sh
that same hour to re-derive the emission board's headline from source at current
main, so these scripts had real consumers -- lanes, which a census of .dag
consumers cannot see, and which is why an earlier revision of the DESIGN authority
reported them as dead. The ruling does not deny that consumer. It denies that a
stray script is the right carrier for it.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01DRMbwdtHZxTiMNZD5WLS3P

* Declare the capability drop the bankruptcy makes, not only the artifacts it deletes

Raised by smart-ram-730 against #9132, and correct: the PR declared deleted
ARTIFACTS and was silent on a deleted CAPABILITY. Those are different facts and
§4b(3) obliges a cut to declare the second.

WHAT IS GONE: the only executable route to a self-host emission board
measurement. Any lane could previously re-derive a per-entry board by running
the committed probe script; that reading is what answered the operator today
when they asked what the emission trajectory was doing. No .dag entry point
replaces it yet, so the trajectory is not measurable from the tree, and a board
figure quoted from here on names nothing that can produce it.

RESTORATION TRIGGER: a .dag entry point that emits, assembles and compiles one
entry and returns the coded-diagnostic population, cited by name wherever a
board figure is quoted. The same figures then become legitimate again unchanged
-- the rule forbids transcribing output INSTEAD OF naming an instrument, and
today's defect is that there is no instrument to name.

WHY THE ROW IS THE ONLY MECHANISM. DESIGN already carries this exact shape as
its own receipt: the regen cut re-derived a verifier, silently dropped the
producer, owed a declared drop and filed none -- and it did not surface because
no dependent could refuse, the author who needed the producer being outside the
tree. Same here. The corpus contains nothing that breaks when the board becomes
unmeasurable, because the consumers are lanes rather than modules -- the
identical blind spot that made a .dag-consumer census report these instruments
as dead a few hours ago. Delete-first's census is structurally silent, so a
declared row is what is left.

Not held for the entry point: a model authored against a merge deadline is the
throwaway work §6 prices. The script survives in git history, so whoever models
it has the spec. smart-ram-730 takes the entry point as follow-up.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01DRMbwdtHZxTiMNZD5WLS3P

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 (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