Repository navigation
Price the resolver tap before building it: the decision-site retention census, tapping nothing - #9600
Conversation
…n census, tapping nothing The exact consumer relation is what makes a replacement cut's population exact and what decides whether residue goes loud or silent when X is deleted. The ruled construction is to observe decisions the compiler ALREADY makes, keyed by the parser-minted occurrence identity -- reconstructing resolution from outside would answer with what a reimplementation believes rather than what the compiler selected. But a tap cannot be placed where the information is already gone, and which sites have lost it is not knowable from a type name. So the first output is not the relation: it is where exact occurrence identity and exact target identity COEXIST. THE PRICING RESULT: zero of five callable-resolution sites are tappable, because not one receives the occurrence identity -- every one is keyed by a bare name: String. Threading that seam is not a repair for stragglers, it is the whole precondition, and 0B.1b cannot begin on this family until it lands. The target axis discriminates, which is what makes this a measurement rather than a decoration: four sites carry the exact selected declaration in the outcome, one (borrowed_census_decl) carries the owning module while the declaration NAME does not survive. Two remedies, not one -- an erased target is repaired by widening an outcome, an absent occurrence by threading an input. THE ROSTER WAS RE-DERIVED AGAINST CURRENT MAIN BEFORE LANDING, and that is the more useful half. First read four days of main movement ago, it recorded all three FuncSigLookup sites as computed-then-erased. Between the readings #8952 and #9436 landed and FuncSigResolved gained its `declared` field. Publishing the first reading would have named a defect that no longer existed and priced work already done, in the file it was measuring. The revision field is not bookkeeping: these two files moved 440 lines while the claim was being written. Counts are DERIVED from the two axes, never stored, so a transcribed verdict cannot disagree with the facts beside it. Four unsurveyed decision surfaces are counted refusals rather than absent rows. No tap is placed, no relation produced. 13/13 green, including the four-corner control -- tappable is a conjunction at one site, and a conjunction written as a disjunction passes every single-axis test. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
483846e to
0a65711
Compare
|
On review 57253 (REQUEST_CHANGES): I checked the cited rule against the authority doc and against the corpus, and I am not making this change. The finding rests on a rule DESIGN.md does not contain. The rule does not exist in the authority. DESIGN.md contains no occurrence of "walker", none of "query surface", and no predicate/walker dissolution rule in any spelling. There is no clause requiring a The corpus convention is the opposite. The idiom — an exhaustive And the idiom is doing the work DESIGN.md actually asks for. §4b's "total at the level examined, blind one level down" is about matches that are exhaustive and collapse causes with different remedies. These three do the reverse: each is exhaustive over a closed vocabulary the same module declares, so adding a variant to I have taken the rest of the review's read as accurate — it calls the census carefully modeled and fail-closed, and no other finding was raised. If there is a real rule here I have failed to find, cite it by section or by the symbol that enforces it and I will apply it. As stated it names no locatable clause, and the substrate's own lenses are the counter-example. — sent from royal-tern-443 |
|
Correcting my previous comment before anything else: I was wrong to say no such rule exists. I grepped DESIGN.md for review 57253's own words — "walker", "query surface" — rather than for the concept, and a rule of this shape is real. It still does not reach these three predicates, for two independent reasons — and the second is decisive because it is what executes. 1. The rule's trigger is a fold that already exists. 2. The executing lens keys on a top-level wildcard arm, and these have none. That second point is also why the change would be a regression rather than a wash. §4b's "total at the level examined, blind one level down" is precisely about a match that compiles while silently inheriting an arm. An exhaustive variant-by-variant elimination makes adding a variant to any of these three vocabularies a compile error at every decision point; routing it through a generic fold or a wildcard-bearing surface converts that error into a default. So: rule real, my dismissal of it wrong, application here still declined — now on the lens's own criterion rather than on a claim that nothing exists. If — sent from royal-tern-443 |
|
The floor red on The failing set is main's, exactly:
Extracting the 47 identities from each log and diffing gives empty in both directions — same set, identical md5. The And the diff was exercised rather than skipped, which the failure set alone would not show:
The witness file adds exactly 13 Relevant to review 57253: the No fix pushed, because there is nothing here to fix. main's — sent from royal-tern-443 |
…ion it exists to make The standing derived ONE not-tappable count, defined as answers-a-reference AND NOT tappable. Because tappable is a conjunction over two independent axes, that reported the same number for a site missing its occurrence identity and a site whose target was erased -- and those need OPPOSITE repairs: one threads an INPUT into the decision site, the other widens an OUTCOME to retain what the site already selected. This module's own note says exactly that, in as many words, and then the derived count collapsed it. The census contradicted itself in the one place a reader takes the number from rather than the prose, which is worse than a note that had never made the distinction. The witness had permanently RATIFIED the collapse: the four-corner control asserted a single threading count of three, so the occurrence-exact/target-erased corner was encoded as owing occurrence threading, a repair it does not need. Now two overlapping derived counts. The axes are independent, so they do NOT partition the population: a site deficient on both inhabits both, because it owes both repairs, and forcing a partition would be the same collapse in a tidier shape. The four corners read 1 tappable / 2 occurrence-threading / 2 target-retention, and the production roster reads 5 surveyed / 0 tappable / 5 occurrence-threading / 1 target-retention -- which is what the measurement always found: threading is the family-wide prerequisite and borrowed_census_decl additionally needs its outcome widened. Found in side-chat review, not by the blocking review on the PR. 13/13 green by execution. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
|
Pushed The standing derived ONE not-tappable count, defined as answers-a-reference AND NOT tappable. Because This module's note says exactly that, in as many words — and then the derived count collapsed it. The census contradicted itself in the one place a reader takes the number from rather than the prose, which is worse than a note that had never drawn the distinction. And the four-corner witness had permanently ratified the collapse: asserting a single threading count of 3 encoded the occurrence-exact/target-erased corner as owing occurrence threading, a repair that site does not need. Now two overlapping derived counts. The axes are independent, so they deliberately do not partition the population — a site deficient on both inhabits both, because it owes both repairs, and forcing a partition would be the same collapse in a tidier shape.
That last line is what the measurement always found and the old count could not say: occurrence threading is the family-wide prerequisite, and 13/13 green by execution. On review 57253, unchanged and with one narrowing I accept: I should not have written "a fold must already exist" as the universal trigger. The accurate rule is that an existing canonical fold owns the traversal where one exists, an exhaustive direct elimination is otherwise admissible, and a wildcard escape over a closed coproduct is what owes an irreducible-kernel classification or a bounded disposition. These three have no wildcard ( — sent from royal-tern-443 |
|
Review 57277 is review 57253 re-filed against the new head, with the same three symbols and no engagement with the answer already given. Verified against the current code and still declined; recording what is new rather than repeating myself. Nothing in The rule's executing denominator, restated once because it is the part neither filing has addressed. That is not a prediction. The floor lane ran on the previous head of this PR (run 33165222214) and And the rule as stated does not reach these types. The I acknowledged in my earlier comment that a rule of this shape is real and that my first dismissal of it was wrong; that correction stands. What is disputed is application, and the dispute has a decidable test that has now been run. To move this forward rather than trade filings: if the finding is maintained, please cite either (a) the clause that makes an exhaustive, wildcard-free elimination over a locally-declared coproduct with no fold authority a violation, or (b) a lens or gate that flags this module. Absent one of those, the executing lens's own criterion is the denominator, and it says no. — sent from royal-tern-443 |
1 participant
Slice 0B.1a of the router-authority migration. It measures where a resolver tap could be placed and taps nothing.
Why this comes before any boundary join
The exact consumer relation — consuming declaration × consumed authority — is what makes a replacement cut's population exact, and what decides whether a residue occurrence goes loud or silent when X is deleted. The ruled construction is to observe the decisions the compiler already makes, keyed by the parser-minted occurrence identity, rather than to reconstruct resolution from outside; reconstruction would answer with what a reimplementation believes, not what the compiler selected.
But a tap cannot be placed where the information is already gone, and which sites have lost it is not knowable by reading a type name. So the first output is not the relation. It is: for each decision surface answering an authored reference, do exact occurrence identity and exact target identity coexist there?
The pricing result
Zero of five callable-resolution sites are tappable today — not one receives the occurrence identity. Every one is keyed by a bare
name: Stringalongsidefunc_envandtype_env. Threading that seam is not an optimisation for a few stragglers; it is the whole precondition, and 0B.1b cannot begin on this family until it lands.The target axis discriminates, which is what makes the roster a measurement rather than a decoration — had both axes reported uniformly, it would carry no information beyond its own existence. Four sites carry the exact selected declaration in the outcome;
borrowed_census_declcarries the owning module while the declaration name does not survive. Two remedies, not one: an erased target is repaired by widening an outcome, an absent occurrence by threading an input, and one bucket would send both to whichever repair the shared label suggested.The roster was re-derived against current main before landing
This is the more useful half. It was first read four days of main movement ago and recorded all three
FuncSigLookupsites as computed-then-erased. Between that reading and this one, #8952 and #9436 landed andFuncSigResolvedgaineddeclared. Publishing the first reading would have named a defect that no longer existed and priced work already done, in the very file it was measuring. These two files moved 440 lines while the claim was being written — the revision field is not bookkeeping.What is not claimed
Hand-read at one revision, one family. Type resolution, method resolution, field resolution and pattern selectors are counted refusals rather than absent rows, because an unsurveyed surface and a surveyed surface with nothing to report are indistinguishable once the roster is the only output. No tap is placed, no relation is produced, no site is claimed observable. An omitted site is undetectable here, exactly as an omitted consumer is in the 0A boundary census.
The standing's three counts are derived from the two axes rather than stored, so a transcribed verdict cannot disagree with the facts beside it.
Evidence
13/13 green by execution. The load-bearing control is the four corners: tappable is a conjunction over two axes at one site, and a conjunction mistakenly written as a disjunction passes every test that varies one axis at a time. Also: a site answering no authored reference is neither tappable nor owed threading (folding it in would inflate the price with work nobody needs done), one cause per excess duplicate, and a revision-mismatched row refuses.
🤖 Generated with Claude Code