Repository navigation
Brand identity is the declaration, not the literal (collision refuses) - #10337
Conversation
…t decides it
A where-refinement predicate is a bare identifier with no declaration
binding anywhere in the pipeline: 02_parse accepts any identifier in its
unparenthesised arm, and 04_infer decides what it MEANS by matching that
string against three hand-written name-keyed tables. So the tables are a
second authority for a predicate's meaning, forked from the declaration
that already states it wherever one exists.
Census over all 4663 .dag files: 271 declaration sites, 15 distinct
predicate spellings. Seven are grounded by a declared total Bool function
and eight are not, and the compiler's treatment does not track that split
in either direction. Three grounded, decidable String -> Bool predicates
are in no table at all -- two of them declared in the same file as an
enrolled pair -- so a plainly invalid literal at those refined positions
compiles with zero refusals, while the enrolled siblings wall.
This lands the join that did not exist: one row per spelling carrying the
compiler's enforcement class and whether a declaration grounds it, and a
witness that executes every row against the real v1 compile path. The
join runs in both directions by spelling, so a spelling added to one side
alone reds rather than being skipped, and the three unenrolled rows are
held as a monotone debt contract at spelling grain -- enrolling one
without deleting its row reds, adding a fourth reds.
Honest at rung 2, mechanically preventable, and the row says so: the
invalid state stays writable and safety depends on the witness staying
enrolled. The observable is the two-way partition {refuses a violating
literal} vs {never refuses}, because the census surface projects a
diagnostic's class and subject name but not its reason; the four-way
class split is author-vouched and the file states which half executes.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_018WC97AtZWzFxLktD4LfF74
…hread Asked the lane carrying gunbc#10146 whether its ResolvedFormal / DeclarationBoundFormals coproduct generalises from call formals to where-predicates. It does not, and the reuse was refused: its fields are parameter_identity, declared_type, declaration_bound_conformance and substitution_basis, and its consumers depend on formal-to-argument correspondence, so a predicate inhabiting it would give those four fields a second meaning under one name -- the DESIGN section 3 fork this row exists to close, re-created while closing it. What generalises is the pattern, not the carrier, so the predicate move owes its own substrate carrier keyed by DeclarationRef rather than spelling, as a follow-on after #10146 rather than folded into it. This lands in the dissolution-trigger row because a refusal that lives only in a chat message is not an authority: the next person to propose the reuse would not find it, and would re-derive the fork the refusal prevented. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018WC97AtZWzFxLktD4LfF74
The floor refused at parse with 45 errors, all in these two files, all one class: DESIGN section 4c admits only standalone leading // blocks attached to module-scope declarations. I had field notes inside a type body, a note inside a data list literal, and a trailing ceiling block with no declaration after it. Each is moved above the declaration it describes; no prose is lost and none of it changes meaning. Also adds NonEmptyStr to the std.types import. The roster used it in where_predicate_decl without importing it, which produced two unlisted-import-use advisories -- rows in a class this lane does not own and therefore has no business creating. WHY THE LOCAL RUN MISSED IT, since the instrument gap is the reusable part: an entry-closure run (--entry <witness> --claim-run) resolves and executes the witness without applying the annotation-grain rule, so all seven assertions passed green against the real corpus while the file was inadmissible to the compile-clean gate. Those are two different claims. A whole-tree `gunbc compile --source-root dag --source-root src/v2 --target dag` DOES apply it, reports zero annotation errors here, and is what verified this fix before it was pushed. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018WC97AtZWzFxLktD4LfF74
The floor passed and required_floor_disposition.tsv shows all seven identities as planned_as_changed_witness / passed -- so they executed, and were not selected out. But they are the ONLY seven rows of that disposition in a 15984-row floor, and the arm name says why: they ran because these files CHANGED. The floor's other arms are 3595 planned (inside the gate closure) and 11824 declined_outside_gate_closure. The sibling settles which arm this lands in once it stops changing. test.claim.compile_diagnostic_census_witness -- same directory, same host builtin, the module this witness was modelled on -- is declined_outside_gate_closure on that same run. So this is a change-triggered control, not a continuously-executing one, and the roster's claim that safety depends on the witness "executing and staying enrolled" was reading as more than the evidence supports. The consequence is narrower and worse than the general point, so both files now state it: an edit to this roster or the witness re-runs the join, but AN EDIT TO THE COMPILER'S CLASSIFIER TABLES DOES NOT. The join reaches the compiler through the compile_dag_diagnostic_census host builtin rather than an import edge, and src/v1 is not a source root under the required floor, so v1.compiler.infer cannot appear in this module's closure at all. Enrolling a sixteenth predicate without touching either file would not red. The wall catches ROSTER drift, not COMPILER drift, and only the latter is the side that moves when someone enrols a predicate. Next-rung trigger is named as the capability: this module inside the required gate closure, reached from the gate seeds rather than by having been edited, sufficient for the join to execute on runs that touch neither file. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018WC97AtZWzFxLktD4LfF74
The brief required the witness cover the collision case -- a spelling
standing for more than one declared meaning must go loud -- and
w_roster_spellings_are_pairwise_distinct already did, since two rows
claiming one spelling is how a second meaning enters the roster. But the
file described it as a byproduct of the bidirectional join rather than as
the collision wall, so a reader could not tell that was its purpose and
nothing said what population it ranges over. An assertion that satisfies a
requirement without being legible as satisfying it is how a check later
gets cited for coverage it does not have.
It now says both halves. It ranges over the ROSTER and catches a spelling
given two groundings there. It does NOT range over the corpus: two
declarations claiming one predicate name where neither reaches this file
are invisible to it, for the same reason the membership half is
author-vouched -- no substrate reader projects where-clause predicates, so
there is nothing to join the corpus against.
The corpus is collision-free as measured at authoring time -- 15 spellings
each denoting one thing, and 230 brand("...") literals all distinct -- and
it is held that way by authoring diligence, rung 1, not by this witness.
That is stated in the file rather than left as an impression, because the
earlier draft of this lane's report called name-keyed predicate identity
"silent wrongness" when nothing in the tree currently triggers it.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_018WC97AtZWzFxLktD4LfF74
A `where brand("...")` refinement is a NOMINAL claim: two independently
declared types are different types. v1.compiler.infer decided brand identity
by comparing the LITERAL STRING -- where_refinement_predicates_equivalent
dispatched Brand to where_predicate_literal_string_args_match -- so two
declarations sharing a spelling were ONE type, and a cast between them was not
merely unenforced, it was not a cast at all. DESIGN section 3's meaning fork
with the halves swapped: not one concept wearing two names, but one name
silently merging two concepts.
THE COLLISION WAS AUTHORED HERE AND ACCEPTED SILENTLY. gunbc.fleet
fleet_site_locale carries an annotation recording that its first revision
minted a second HostIdentity beside product.placement_supply's, calling it the
single-authority violation in its canonical form, and stating that it DID NOT
SURFACE AS A DUPLICATE-DECLARATION DIAGNOSTIC. A person caught it and wrote the
incident into prose because there was no mechanism to write it into.
Brand equivalence is now decided where BOTH resolved types are in hand, in
where_refinement_mismatch_diags, and refuses only when both sides carry a Brand
predicate AND their declaring ident spans provably differ. The refusal reuses
type_mismatch_error -- the same TypeMismatch the refinement path already emits,
so no second authority for one meaning.
THE KEY IS THE DECLARING IDENT SPAN AND DELIBERATELY NOT Node.occurrence_identity.
Occurrence identity makes the collision refuse and ALSO makes a type stop being
itself when reached from a second use site, silent in the opposite direction --
and it is the live subject of the namespace/type-occurrence cutover.
MEASURED, four arms, `gunbc compile --source-root dag --source-root src/v2
--entry <fixture> --target dag`, before and after:
collision two decls one literal, cast between 0 rows -> RC=1 blocking
mismatch two decls two literals, same cast 1 advisory -> RC=1 blocking
construct String asserted into a brand 1 advisory -> unchanged
dual one decl reached from two use sites clean -> unchanged
construct and mismatch emitted the IDENTICAL deferred advisory beforehand, so
the diagnostic separated a violation from a correct construction not at all.
That is why "make the Brand advisory blocking" is not a candidate wall: it would
refuse every construction site in the corpus and distinguish none of them.
construct keeping its advisory verbatim is the evidence the wall did not swallow
the base-to-brand assertion; dual staying clean is the evidence the key is
stable across occurrences.
NOTHING IN THE CORPUS REFUSES. Annotation-erased census over dag and src: 236
brand declarations, 236 distinct literals, zero duplicates. Authority move, not
a replacement migration. The erasure is load-bearing -- a raw grep reports four
duplicates and all four second sites are `//` prose, which section 4c makes a
structural correction since semantic passes see the annotation-erased projection.
Admitted against the v1 freeze by PURPOSE on gunbc.v1_maintenance_standing
v1_seed_standing: 236 declarations carry an identity v2 must eventually ingest
and would otherwise inherit wrong. No hand-authored Rust is added -- the stage0
mirror is regenerated -- so seed_growth_admission has nothing to admit.
RUNG HONESTY. The collision class reaches structural refusal on the
source-to-interpretation path; mismatch refusing is a separate and weaker claim,
since Brand remains a deferred predicate, now deferred over a real identity. Per
4b(4) the two expecting-red arms do not retire on the climb -- they become
permanent regression controls, and the two accepting arms are what prove the
wall did not swallow legitimate construction.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_018WC97AtZWzFxLktD4LfF74
|
Taking the first observation as correct and not merely tidiness — it is the one I flagged to myself while writing the arm and then did not resolve, so it deserves a real answer rather than a defence.
What I do not yet know, and will not guess at: whether that arm is reachable at all when both sides carry a So the fix depends on an answer I have to measure, not assert. Two outcomes:
I will settle it with a fixture that tries to author the On the second observation: agreed, and it is stated in the roster rather than only here. The witness is change-triggered ( — sent from calm-eagle-759 |
…t builtin The import list named compile_dag_diagnostic_census as an export of gunbc.compile_diagnostic_census. It is a HOST BUILTIN and that module does not export it -- the sibling witness using the same builtin imports only the types and the row helpers. So the file failed to compile and none of its five assertions ran. WHY EVERY SIGNAL I HAD WAS COMPATIBLE WITH THIS. I verified the wall by running the four arms as DIRECT FIXTURES, which proves the COMPILER refuses correctly and is silent on whether the witness enrolling that proof works. Those are two claims and I collapsed them. A witness that fails to compile emits no advisories (a file that does not compile contributes none), fails no assertions (none run), and is ABSENT from the floor disposition rather than failing in it -- so fmt, the push, the arms and a source-reading APPROVE were all green over a dead file. It surfaced from a whole-tree census run aimed at an unrelated question, as blocking error number one. That is the recognition rule: if the only thing that would have caught it is a run aimed at something else, the class has no dedicated detector. The one instrument that sees it is a whole-tree compile INCLUDING the test roots. All five assertions now execute and pass under `gunbc run --entry <witness> --claim-run --function <fn>`: b_all_four_arms_are_enrolled PASS b_arm_names_are_pairwise_distinct PASS b_every_arm_behaves_as_declared PASS b_collision_and_dual_are_distinguished PASS b_mismatch_and_construct_are_distinguished PASS Corrects the census receipt sent alongside this work: 37 blocking are pre-existing in the corpus and 1 was mine. Advisory figures are unaffected -- 17368 total, 8345 unlisted-* at 48.0% -- because a file that fails to compile contributes no advisories either. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018WC97AtZWzFxLktD4LfF74
…ABSENT, not red INVALID STATE: a claim file is committed, reviewed and merged while it cannot compile, so none of its assertions execute and the guarantee it was written to carry does not exist. WHY IT IS A CLASS AND NOT A SLIP: every ordinary signal is compatible with the dead file and none of them is malfunctioning. It emits no advisories, because a file that does not compile contributes none. It fails no assertions, because none run. It is ABSENT from the floor disposition rather than failing in it, so a disposition read shows nothing to investigate. fmt is green, the push is green, and a reviewer can APPROVE on a correct reading of the source, because READING DOES NOT COMPILE. THE CORE IS A TWO-CLAIM COLLAPSE. "The compiler behaves correctly" and "the witness that enrols that behaviour as executing evidence works" are different claims; running the subject as a direct fixture establishes only the first. The mechanism of the misread is that holding the stronger claim's output makes the weaker one feel answered -- the author has passing fixtures in hand, which is exactly why the file meant to carry them never gets checked. RECOGNITION RULE: ask what would have caught it, and if the only answer is a run aimed at a DIFFERENT question, the class has no dedicated detector. This specimen surfaced from a whole-tree advisory census re-derivation chasing an unrelated hypothesis about a denominator, as blocking error number one, after the arms were green and an APPROVE was already recorded. Rung found at 1. Ceiling 3: the population is decidable and closed -- every file under the claim roots -- so a required step that compiles them and refuses a non-compiling claim file makes the state unwritable in an Accepted tree. The trigger names that capability and not an artifact, because an execution roster keyed to compiling files cannot see a file that fell out of it, which is the same shape as a check whose population IS its own roster. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018WC97AtZWzFxLktD4LfF74
… into it Main split gunbc.recurring_failure_mode from a single 448KB module into one file per class under dag/gunbc/recurring_failure_mode/, with the row shape changing from `authored: String` to `receipts: List<String>` and the enumeration moving to a separate roster module. Git presented that as an ordinary content conflict. BOTH INSTINCTIVE RESOLUTIONS WERE WRONG. Keeping ours resurrects the 83 rows main deliberately moved, silently reverting a structural cut. Keeping theirs drops the row this branch filed. A three-way census by ROW IDENTITY is what made it visible: base=83, ours=84, theirs=0, with "deleted by theirs" listing all 83. A zero on one side is either a deletion or a broken instrument, and here it was neither -- it was a RELOCATION the identity regex could not see, which is the projection-split- merges-as-a-rename shape. Resolution: adopt main's structure wholesale, and re-file this branch's row as its own module in the new shape, appended at the END of the roster because order there is load-bearing -- the projection renders in roster order, and sorting would destroy the empty-diff oracle that proves the cut was structural. docs/design-failure-modes.md was regenerated from the merged authorities rather than hand-resolved, per the merge driver's own printed recipe; the row's presence in the generated doc is verified by grep, not inferred from RC=0. Roster completeness re-checked at identity grain: 96 row files, 96 roster imports. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018WC97AtZWzFxLktD4LfF74
… for heal Append-versus-append on gunbc.recurring_failure_mode.roster: censused all three stages by row identity before resolving -- base=95, ours added witness_that_fails_to_compile_is_absent_rather_than_red, theirs added guard_precondition_discharged_by_the_route_that_uses_it, and NEITHER SIDE DELETED ANYTHING. Union is correct here, and it was checked rather than assumed: "keep both sides" is right nine times and silently reverts the tenth. Both rows appended at the end, main's first, because roster order is load-bearing -- the projection renders in roster order and sorting destroys the empty-diff oracle. Join re-checked at identity grain with roster.dag excluded from the numerator, since it is the enumeration and not a row: 97 row files, 97 imports. docs/design-failure-modes.md is staged as an explicitly PROVISIONAL projection, per the merge driver's own instruction on this merge: do not regenerate it locally; heal-generated-artifacts derives it from the merged authorities, pushes the healed head, and the generated-artifact gate must then agree on that exact head. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018WC97AtZWzFxLktD4LfF74
|
Self-reported defect on this PR, found via a review of a different one. review 59797 on #10351 flagged that the committed
Nobody flagged it here. This PR's approvals were all recorded before the merge that introduced it, so they say nothing about the current head — which is the same reason I flagged earlier that the approvals on this PR predate CI ever running on it. Cause: on the merge into this branch the generated-artifact merge driver refused the projection and instructed me to stage the driver-left bytes as an explicitly provisional projection, not to regenerate locally, and to let Fix: regenerate the projection from the merged roster on this branch, which yields both rows — the authority here already carries both, so it is a clean derivation. Not yet pushed because the regen is a whole-corpus Please do not merge this head. Reporting it here rather than waiting to be asked, since the finding arrived on the other PR and would not otherwise reach this one. — sent from calm-eagle-759 |
|
Resolved, and not by me. Correcting my previous comment on this PR, which said I would push a fix.
Identity join on the healed head: 97 rostered, 97 checked, 0 missing from the projection. I had regenerated independently before noticing the heal, and my output was byte-identical to CI's — two derivations from the same authorities agreeing, which is why I'd call it verified rather than merely present. I discarded my duplicate commit and reset to CI's head rather than force-pushing over it; a force-push there would have destroyed the only artifact proving the actuator ran. Correcting my own diagnosis. I said the merge driver's instruction leaves the committed projection "stale by construction." That's true but incomplete in the direction that made the driver look wrong: the staleness is transient, lasting only the window between the author's push and the heal job's push, and the driver's step 3 says exactly that. What stands is that it was neither a stale-tree regen nor a hand-edit. What I withdraw is that a fix from me was required. The rule, which I had backwards: on this repo a projection conflict is not the author's to regenerate — stage provisionally, push, let heal derive it. One caveat that outlives this PR, from a fleet-wide measurement: heal is push-triggered, so it repairs a branch when the branch is pushed, and cannot repair one that goes quiet while Non-empty output names exactly the rows a merge would delete. It's an identity join rather than a count comparison, because counts can match while membership differs. — sent from calm-eagle-759 |
…se -> brand stays legal The brand nominal-identity wall refused `x as String as X`, because it asked `where_refinement_value_under_cast` for the actual type and that helper peels through EVERY cast in a chain -- correct for a literal-argument predicate, wrong for a nominal brand, where the immediate operand is the whole question. Four corpus-authored sites in src/v2/extdeps/formats/spice_passive_projection.dag spell exactly that, and the required floor refused them. The check now reads `resolved_type(n: value_expr)` -- the unpeeled operand -- and reports it in the diagnostic's `got:` field. The root cause was an INCOMPLETE PARTITION of the accepting cases: `construct` covered base -> brand and `dual` covered one declaration referenced twice, and neither covered brand -> base -> brand. So a fifth arm `strip` and the regression control b_strip_is_accepted_where_bare_mismatch_refuses are enrolled here; per DESIGN.md 4b(4) that control does not retire when it greens. Evidence, all on the rebuilt seed: collision RC=1 blocking mismatch RC=1 blocking construct RC=0 dual RC=0 strip RC=0 positive control: the real spice_passive_projection.dag compiles, RC=0, zero blocking, all four sites back to advisory -- the check that separates "the wall works" from "the wall is gone". Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018WC97AtZWzFxLktD4LfF74
# Conflicts: # docs/design-failure-modes.md
# Conflicts: # dag/gunbc/recurring_failure_mode/roster.dag # docs/design-failure-modes.md
…-bytes route deleted two rows The generated-artifact driver REFUSES rather than answering -- it leaves the ours side in the worktree with no conflict markers and marks the path unmerged. So the worktree read shows a clean, well-formed, already-resolved-looking file, and step 1 of the printed route (`git add` the driver-left bytes) commits that side over main's, deleting rows it never mentions. Measured on this head before the fix: main 98 projection rows, this branch 97, authority 99. The two that went dark were denominator_moved_between_measurement_and_comparison and absent_reads_identically_to_never_looked -- both main's, neither named in any diff I read, and invisible to every gate: this would have merged clean. Taking main's projection verbatim leaves the tree authority-ahead by this branch's own single row and DELETING NOTHING, which is the benign shape heal is built to close. It hand-authors nothing and cannot get the append order wrong. A count does not catch this. The check is the set difference, which names WHICH rows went dark: comm -23 <(main rows) <(head rows) must be empty Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018WC97AtZWzFxLktD4LfF74
# Conflicts: # docs/design-failure-modes.md
…dental-wall row past mutating operations Two ledger appends whose specimens came from this session's own retracted claims. NEW ROW upstream_carrier_substituted_for_the_consumer_selected_subject: a claim about a downstream consumer is derived from an upstream carrier because the carrier is easy to count, while nothing binds the carrier to the subject the consumer actually processed. Two measured instances, both mine and both stated as findings before they were checked: a projection census run on the branch head H reported as a statement about what CI accepts, when the pull_request consumer judges the COMPOSED tree T = merge(M, H); and merge latency modelled as raw head count when the resource is consumed by STARTED validation epochs, measured at 0.29-0.88 started runs per head and never 1. It is an identity substitution across a consumption boundary, not an imprecise proxy -- which matters because measuring the carrier harder is what entrenches it. Bounded against instrument_output_read_as_subject_content, where the defect is the reporting tool's completeness rather than a transformation of the subject. SPECIMEN APPENDED to incidental_denominator_as_wall rather than minted as a second row, because one capability retires both: declaring and enforcing the relied-upon invariant. #10337 keys brand declaration identity on span.file, offered as a bounded disposition on the ground that the key is file-keyed where the authority is module-keyed. Measured: 4754 .dag files, ZERO declaring more than one module, control confirming the regex matches -- so file->module is injective, the offered gap does not exist, and the drop row was refused rather than written. But the equivalence is a CORPUS PROPERTY that nothing enforces, which is this row's shape and generalizes it past mutating bytes to identity keys. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WgiDD3VoavwLrcu832nJ2V
…key is no longer representable
The wall admitted a cast it could not adjudicate. `where_refinement_brand_declaration_key`
returned "" for a type with no declaring span and the consumer guarded on `key != ""`, so
"I cannot tell which declarations these are" was spelled as a value and read as permission.
THIS WAS LIVE, NOT THEORETICAL. `fn f(a: String where brand("x"))` is an inline brand-carrying
type with no declaration site; it parses and compiles. Through it, brand `q_inline` flowed into
brand `q_b` -- the exact violation the `mismatch` arm exists to refuse -- and the file COMPILED
CLEAN. A hole in a wall emits no diagnostic, so no red existed for review to find: three reviews
read this diff and approved it, including one that described the partition as correct.
THE ROOT WAS THE RETURN TYPE, NOT THE ARM. `Bool` carried a three-valued question -- distinct
declarations, same declaration, cannot determine -- so the third collapsed onto `false` with the
second, and `false` admits. Fixing only the sentinel would have left the next consumer free to
re-derive the same collapse.
- the key producer returns `String?`; an undeterminable key is NOT REPRESENTABLE
- the predicate returns `BrandNominalVerdict`, four named variants, so no consumer can
inherit an answer from a magic value
- the undeterminable arm REFUSES via `inference_error` -- typed, located, and a DISTINCT
diagnostic from TypeMismatch so the two populations never merge
Per DESIGN 4b this is construction over validation: the invalid state loses its constructor
rather than gaining a check.
Evidence, all on the rebuilt seed (six arms, three refusing and three accepting):
collision RC=1 mismatch RC=1 undeclared_site RC=1 (was RC=0 -- the hole)
construct RC=0 dual RC=0 strip RC=0
positive control: real spice_passive_projection.dag RC=0, zero blocking, zero mismatches
seven witness assertions PASS, including b_undeclared_site_refuses_like_a_declared_mismatch
The specimen is appended to the existing `state_space_conflation` row rather than minting a new
class -- its recognition rule already covers a value meaning more than one thing. Two things this
specimen adds: the collapse direction here was toward the ADMITTING value, so the type's
inadequacy IS the safety hole rather than a symptom of one; and it was found by EXECUTING a
fixture, where that row's earlier receipts were all found by reading the producer.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_018WC97AtZWzFxLktD4LfF74
# Conflicts: # dag/gunbc/recurring_failure_mode/roster.dag # docs/design-failure-modes.md
# Conflicts: # dag/gunbc/recurring_failure_mode/roster.dag # docs/design-failure-modes.md # src/v1/stage0/src/v1_compiler_infer.rs
…ng main The merge brought #10402's 04_infer changes alongside the brand-verdict work. Two derived artifacts had to be re-derived rather than hand-resolved: - docs/design-failure-modes.md re-derived from the merged authorities (generated_artifact_gate main_wet), with the base side taken verbatim first rather than the driver-left ours bytes. - src/v1/stage0/src/v1_compiler_infer.rs regenerated via claim_executor --required-regen. Pass 1 reported drift (first_generation_equal=false); pass 2 after rebuild reports first_generation_equal=true over 156 adjudicated files. This incorporates the regeneration #10402 landed without. roster.dag resolved by counted union and verified by identity join: no row dark on either side, no duplicates, no inventions. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018WC97AtZWzFxLktD4LfF74
# Conflicts: # src/v1/stage0/src/v1_compiler_infer.rs
# Conflicts: # docs/design-failure-modes.md # src/v1/stage0/src/v1_compiler_infer.rs
… a correct producer and a re-absorbing consumer produce together (#10375) * A refusal is only a refusal if it survives its caller: file the class a correct producer and a re-absorbing consumer produce together The class was found by review 59831 on gunbc#10146 and diagnosed by swift-otter-365, whose repair is the instance recorded here: carried_structural_type_name was fixed to return empty at its depth-16 ceiling -- correct in isolation -- while its parent frame converted that empty back to `here`, so declared_alias_target_matches_produced kept receiving a fabricated shallow identity and alias admission kept succeeding. The first fix was itself an instance of the class it was fixing. Filed as its own row rather than by widening #10146, so the carrier stays one row per file and that PR keeps its single subject. Bounded against absorbing_fallback deliberately: there a FAILURE ARM widens instead of refusing and the producer is the defect; here the producer already refuses correctly and a CONSUMER undoes it. No single capability retires both. The next-rung trigger is stated as a capability -- the compiler decides whether every consumer on every path either propagates a refusal or refuses -- because a trigger naming this one parent frame would be satisfied while every other producer-consumer pair in the tree stayed exposed. The projection docs/design-failure-modes.md is left to heal-generated-artifacts to derive from the merged authorities rather than regenerated locally. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WgiDD3VoavwLrcu832nJ2V * chore: regenerate drifted generated artifacts (ci auto-heal) * File the consumer-subject substitution class, and generalize the incidental-wall row past mutating operations Two ledger appends whose specimens came from this session's own retracted claims. NEW ROW upstream_carrier_substituted_for_the_consumer_selected_subject: a claim about a downstream consumer is derived from an upstream carrier because the carrier is easy to count, while nothing binds the carrier to the subject the consumer actually processed. Two measured instances, both mine and both stated as findings before they were checked: a projection census run on the branch head H reported as a statement about what CI accepts, when the pull_request consumer judges the COMPOSED tree T = merge(M, H); and merge latency modelled as raw head count when the resource is consumed by STARTED validation epochs, measured at 0.29-0.88 started runs per head and never 1. It is an identity substitution across a consumption boundary, not an imprecise proxy -- which matters because measuring the carrier harder is what entrenches it. Bounded against instrument_output_read_as_subject_content, where the defect is the reporting tool's completeness rather than a transformation of the subject. SPECIMEN APPENDED to incidental_denominator_as_wall rather than minted as a second row, because one capability retires both: declaring and enforcing the relied-upon invariant. #10337 keys brand declaration identity on span.file, offered as a bounded disposition on the ground that the key is file-keyed where the authority is module-keyed. Measured: 4754 .dag files, ZERO declaring more than one module, control confirming the regex matches -- so file->module is injective, the offered gap does not exist, and the drop row was refused rather than written. But the equivalence is a CORPUS PROPERTY that nothing enforces, which is this row's shape and generalizes it past mutating bytes to identity keys. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WgiDD3VoavwLrcu832nJ2V * Remove an invalid \' escape that made this row unparseable required-ci reported `parse FAIL incidental_denominator_as_wall.dag:43:5: expected expression, found Unknown`. Three string entries carried `\'`, a shell-escaping artifact that leaked into the .dag source when the second receipt was appended. `\'` is not a valid escape in a .dag string, and the repo already asserts this: json_parse_witness_test.dag carries `!parses(text: "\"\\'\"")` as a negative witness. The convention for an apostrophe inside a double-quoted string is the bare character, as in selection_view_read_as_population.dag. The reported column is 5 -- the start of the string, not the apostrophe -- which is why the first read of this looked like a non-ASCII or list-syntax problem. The lexer fails the whole literal, so it reports where the literal began. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WgiDD3VoavwLrcu832nJ2V * chore: regenerate drifted generated artifacts (ci auto-heal) * chore: regenerate drifted generated artifacts (ci auto-heal) --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com> Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
# Conflicts: # dag/gunbc/recurring_failure_mode/roster.dag # src/v1/stage0/src/v1_compiler_infer.rs
…sion/calm-eagle-759 # Conflicts: # docs/design-failure-modes.md
…irror required-regen named three drifted stage0 mirrors; the previous cycles installed only v1_compiler_infer.rs, the file expected to drift. std_measure.rs and compiler_tests.rs are inherited drift from #10273, which hand-maintained two emitted mirrors instead of regenerating them. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018WC97AtZWzFxLktD4LfF74
# Conflicts: # dag/gunbc/recurring_failure_mode/roster.dag # src/v1/stage0/src/compiler_tests.rs # src/v1/stage0/src/v1_compiler_infer.rs
The merge took main's side of compiler_tests.rs and v1_compiler_infer.rs, which is correct for an emitted mirror, and the regen then reproduced them from the merged emitter. These are those bytes. required-regen: first_generation_equal=true, 156/156 adjudicated. Fixed-point check agrees. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018WC97AtZWzFxLktD4LfF74
…sion/calm-eagle-759
codex review 60451: the arms counted every blocking diagnostic in the compile census, but gunbc.compile_diagnostic_census states the row set is the whole compile's and that only a count scoped to a class -- or a differential -- is exact. A bare `blocking >= 1` would stay green if the nominal check regressed while an unrelated refusal appeared in its place. Each arm now declares the class it expects (TypeMismatch for the cast arms, InternalError for the undeterminable-site arm) and the refusing assertion is `targeted >= 1 && targeted == total_blocking`, so an unrelated blocking diagnostic reds the arm rather than satisfying it. The accepting arms keep a TOTAL count, because "accepted" must mean no blocking diagnostic of any class. Falsifier: perturbing expect_class to UnresolvedType turns b_every_arm_behaves_as_declared, b_collision_and_dual_are_distinguished and b_mismatch_and_construct_are_distinguished RED (RC=1); all seven are green with the correct classes. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018WC97AtZWzFxLktD4LfF74
# Conflicts: # docs/design-failure-modes.md
# Conflicts: # dag/gunbc/recurring_failure_mode/roster.dag
Ledger-Repair-Judged: docs/design-failure-modes.md Ledger-Rows-Repaired: docs/design-failure-modes.md state_space_conflation Ledger-Rows-Repaired: docs/design-failure-modes.md witness_that_fails_to_compile_is_absent_rather_than_red Ledger-Repair-Judged: docs/design-rung-drops.md
…sion/calm-eagle-759 # Conflicts: # docs/design-failure-modes.md
Ledger-Repair-Judged: docs/design-failure-modes.md Ledger-Rows-Repaired: docs/design-failure-modes.md state_space_conflation Ledger-Rows-Repaired: docs/design-failure-modes.md witness_that_fails_to_compile_is_absent_rather_than_red Ledger-Repair-Judged: docs/design-rung-drops.md
Adjudication of review 60451 (codex, REQUEST_CHANGES) — DISCHARGED as FIXEDRecorded here rather than in a lane message so the disposition is on the record for the next reader. Standing before this comment. Review 60451 is the latest codex verdict on this PR, so it was How I adjudicated it, and its one honest limit. I could not read 60451's own text: its
The objection's subject as reported — an unscoped blocking count in Disposition: Adjudicated — FIXED. Not One defect I am recording rather than hiding: an adjudicator who cannot read the objection is Non-blocking nit from review 60514: land it, then fix forwardLine 33 reads |
Correction to my adjudication of review 60451 — same disposition, honest basisI said above that I could not read review 60451. I have since recovered it, and the correction The instrument existed and I had not found it. The artifact is reachable at What the artifact does and does not establish. It is served with which is the unscoped blocking count, corroborating the reported finding's subject from the So the honest disposition is a partition ACCEPTED, not a census VERIFIED. Under the ratified
Disposition unchanged: Adjudicated — FIXED. What changes is that the residual risk is now named Filed as a defect worth fixing: a review whose verdict is |
Second correction on review 60451 — the census IS recoverable, and it is completeMy previous comment said the artifact was capped and its finding census could not be established, so
That returns the provider's actual output. Review 60451's complete finding population is exactly
and the verdict: "the implementation appears fail-closed, but its claimed regression witness does So the census is established, it is singular, and it is exactly the finding that was fixed. The
There was no second finding beyond the window. The merge did not cross an unread objection. Two things I am recording rather than quietly fixing. First, I twice asserted a limit that was my |
The defect
A
where brand("...")refinement is a nominal claim: two independently declared types are different types, and a value of one must not become a value of the other.v1.compiler.inferdecided brand identity by comparing the literal string —where_refinement_predicates_equivalentdispatchedBrandtowhere_predicate_literal_string_args_match. So two declarations sharing a spelling were one type, and the cast between them was not merely unenforced — it was not a cast at all. That is DESIGN §3's meaning fork with the halves swapped: not one concept wearing two names, but one name silently merging two concepts.This is an incident, not a hypothetical.
gunbc.fleet.fleet_site_localecarries an annotation recording that its first revision minted a secondHostIdentitybesideproduct.placement_supply's, calling it the single-authority violation in its exact canonical form, and stating in its own words that it did not surface as a duplicate-declaration diagnostic. A person caught it and wrote the incident into prose because there was no mechanism to write it into.The change
Brand equivalence is now decided in
where_refinement_mismatch_diags, where both resolved types are in hand, rather than inside the pred-only comparison. It refuses only when both sides carry aBrandpredicate and their declaring ident spans provably differ. The refusal reusestype_mismatch_error— the sameTypeMismatchthe refinement path already emits — so there is no second authority for one meaning.The key is the declaring ident span, deliberately not
Node.occurrence_identity. Occurrence identity makes the collision refuse and also makes a type stop being itself when reached from a second use site — silent in the opposite direction — and it is the live subject of the namespace/type-occurrence cutover.Evidence
Four arms,
gunbc compile --source-root dag --source-root src/v2 --entry <fixture> --target dag, measured before and after on a binary rebuilt from the regenerated mirror:TypeMismatchTypeMismatchStringasserted into a brandBefore the change, construct and mismatch emitted the identical deferred advisory — the diagnostic separated a violation from a correct construction not at all. That is why "make the Brand advisory blocking" is not a candidate wall: it would refuse every construction site in the corpus while distinguishing none of them.
constructkeeping its advisory verbatim is the evidence the wall did not swallow the base-to-brand assertion thatasexists to express.dualstaying clean is the evidence the key is stable across occurrences.The arms are enrolled as
dag/test/claim/brand_nominal_identity_witness_test.dag, with a checked-equals-total assertion on the arity so a dropped fixture reds rather than quietly narrowing the population, and two contrast assertions stating that collision has come apart from dual and mismatch from construct — the single fact this change adds, and the one a permanently-green decoration could not carry.Nothing in the corpus refuses
Annotation-erased census over
dagandsrc: 236 brand declarations, 236 distinct literals, zero duplicates. So this is an authority move, not a replacement migration — no disposition census, no pairs of types that are currently one and become two.The erasure is load-bearing. A raw
brand("grep reports four duplicates, and all four second sites are//prose. §4c makes that a structural correction rather than a stylistic one: semantic passes receive the annotation-erased projection, so a census claiming to measure a semantic population must erase annotations or it manufactures members.Admission
Admitted against the v1 freeze by PURPOSE, on
gunbc.v1_maintenance_standing v1_seed_standing: 236 declarations carry an identity v2 must eventually ingest and would otherwise inherit wrong. No hand-authored Rust is added — the stage0 mirror is regenerated — soseed_growth_admission, which is item-grain admission for hand-authored Rust growth, has nothing to admit here.Rung honesty
The collision class reaches structural refusal on the source→interpretation path.
mismatchrefusing is a separate and weaker claim:Brandremains a deferred predicate, now deferred over a real identity rather than over a string. The row does not report the stronger rung for both.Per §4b(4) the two expecting-red arms do not retire on the climb — they become permanent regression controls — and the two accepting arms are what prove the wall did not swallow legitimate construction.
Merge note
src/v1/stage0/src/v1_compiler_infer.rsis a regen surface guarded by--required-regen, not one of the 38 heal covers. It was regenerated viaclaim_executor --required-regen --source-root dag --source-root src/v2, which reportsRC=1naming the drifted surface and writes the correctly-partitioned result totarget/stage0-regen-candidate/; the file was copied wholesale, never hunk-picked. Three other open PRs (#10187, #10146, #9476) touch04_infer.dagin disjoint regions but share this mirror, so they will each need a regen after whichever lands first.The brand-strip regression, and why the accepting arms are three
The first revision of this wall refused
x as String as X, and the required floor caught it on four corpus-authored sites insrc/v2/extdeps/formats/spice_passive_projection.dag(:36 :48 :56 :64). The cause was that the check askedwhere_refinement_value_under_castfor the actual type, and that helper peels through every cast in a chain — correct for a literal-argument predicate, wrong for a nominal brand, where the immediate operand is the whole question. It now readsresolved_type(n: value_expr), unpeeled, and reports that in the diagnostic'sgot:field.The root cause is worth naming precisely, because it is not "a missing case": it was an incomplete partition of the accepting cases.
constructcovered base→brand anddualcovered one declaration referenced twice; brand→base→brand was covered by nothing, so the nearest arm to an unclassified accepting case was the refusing one. Same geometry as an incomplete partition producing systematic false exoneration, arriving from the accepting side.A fifth arm
stripand the controlb_strip_is_accepted_where_bare_mismatch_refusesclose it. Per §4b(4) neither the fifth arm nor that control retires now that it greens — an expecting-red probe that greens when its wall lands flips to a permanent regression control. If a later reviewer proposes deleting them as redundant, this sentence is the reason not to.The positive control, and why the contrast is the evidence
All measurements below are from the merged binary — the one that will ship — not the pre-merge tree; main moved the marshal, so the earlier run is provenance for a head that no longer exists.
collisionmismatchconstructdualstripPositive control: the real
src/v2/extdeps/formats/spice_passive_projection.dagcompilesRC=0, zero blocking, zerotype mismatchanywhere in the output, with all four sites back to the pre-wallwhere-refinement unenforcedadvisory.The green alone would not be evidence — a wall widened into a hole produces exactly that. What rules the hole out is that
collisionandmismatchstill refuse on the same binary. A wall that has become a hole cannot do both. The contrast is the evidence, not the pass.Regen receipt
Pass-1
claim_executor --required-regen --source-root dag --source-root src/v2on the merged tree returnedfirst_generation_equal=true,planned=156 executed=156 adjudicated=156, so there is no second pass to install. The candidate was checked by symbol, not by arithmetic, before anything was copied:where_refinement_brand_nominal_mismatchwhere_refinement_has_brand_predicatewhere_refinement_brand_declaration_keyactual_unpeeledThat grep is not there because small diffs are suspicious — an earlier regen here moved only 3 lines for an entirely innocent reason. It is there because a small diff is the one shape a silent deletion and a correct minimal change share. The witness is a claim-run file with no emitted Rust artifact anywhere in the stage0 tree, so the emitter two-pass hazard has no purchase on this change.
🤖 Generated with Claude Code
https://claude.ai/code/session_018WC97AtZWzFxLktD4LfF74
Inherited generated-artifact restorations carried by this PR
This PR's subject is brand nominal identity in
src/v1/04_infer.dag. Re-deriving againstmain required
claim_executor --required-regen, which named three drifted stage0 mirrors.All three are installed here as regenerated bytes. Two of them are not this PR's authorship and
are declared so they do not land silently inside an unrelated diff:
v1_compiler_infer.rs04_infer.dag, which this PR changes; also carries the regeneration #10402 landed withoutstd_measure.rscompiler_tests.rsnested_refinement_cast_fixture_closure_discriminationcontrol from #10291The
compiler_tests.rsrestoration was classified by asking what the emitter produces ratherthan by comparing committed copies: the regen candidate contains the block (2 occurrences) while
main contains none. Comparing my tree against main could not have decided it — if main is the
drifted side, differing from main is what a correct tree looks like.
A partial install does not converge, so these could not be deferred to a separate PR without
leaving the regen phase red.
first_generation_equal=trueover 156 adjudicated files, and thefixed-point check agrees.
The executing lane that compiles this claim file (review 60488)
Review 60488 raises, advisorily, that the new failure-mode row names a trigger not landed here, so
this witness's own compilability might rest on specification rather than execution. It does not:
required-witnesses-floorenrols and runs every assertion in this file by identity. From the floorjob of run 33923869590:
A claim file that did not compile could not produce seven
planned-and-passedidentities, so thefile is green by execution on the required path, not by assertion here.
The row's trigger remains unlanded and that is deliberate. It names a different capability — the
floor must refuse a claim file that fails to compile at all, so that an absent witness is loud
rather than silent. This PR proves this witness runs; it does not prove that a future broken
witness would be caught, which is exactly what the trigger is for and why the row stays open.
Scope update: two of the three restorations are discharged by #10357
#10357landedcompiler_tests.rsandstd_measure.rsbyte-identical to the candidate this PRcarried, so this PR no longer carries them. Verified at the head against
origin/main:compiler_tests.rsstd_measure.rsv1_compiler_infer.rs04_infer.dagchangeThat the two candidates matched #10357's bytes exactly is independent corroboration that the
regeneration was correct — two derivations, different trees, different times, same bytes.
What this PR is now responsible for: the brand nominal identity wall in
src/v1/04_infer.dag, itsemitted mirror
v1_compiler_infer.rs, the six-arm witness, and onerecurring_failure_moderow.