Repository navigation
Direct-call argument inhabitance — one mismatch diagnostic, two defects, opposite repairs - #9007
gunbai-bot[bot] wants to merge 26 commits into
Conversation
…r push) Carrier types, the single declared_type_inhabitance relation consuming #8876's coproduct_payload_where_parent_required, the DeclaredTypeNotInhabited diagnostic, and the list-element position wired. Mirrors NOT regenerated; the wall does not execute in any built artifact yet. Verification dispatch in flight.
…6-inhabitance # Conflicts: # src/v1/00_core.dag # src/v1/stage0/src/cli_run.rs # src/v1/stage0/src/v1_std_core.rs
…al merge Git conflicted on v1_std_core.rs and AUTO-MERGED v1_compiler_infer.rs. Resolving only the file git complained about left the pair internally inconsistent: one mirror declared the roster variant and not the inhabitance one, while its sibling used both. That state is not something any emitter produces, and it does not compile. Generated files are projections of one authority and are only consistent as a SET, so both are replaced wholesale by a fresh emit from the merged .dag rather than merged file-by-file. Measured on that emit: both variants present in all three seed files, and all four inhabitance arms hold -- nega and negb refused at the list element, pos accepted, reach refused. Neither wall was eaten by the merge. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b
…-records
The list-element inhabitance obligation refused six data rows in
emit_on_demand_match_loop_fold_family_witness, 30 elements in all. It was
right, and the annotation was wrong.
data match_expected_octets: List<Byte> = [0, 1, 0, 0, 0]
Byte here resolves through v2.std.machine to std.bit's
`type Byte { bits: List<Bit> }` -- a product. A plain Int does not inhabit it.
The values were never bit-records: their only consumer is
`emit_host_octets_byte_string(octets: List<Int>)`, which takes the octets as
numbers. So the rows declared one type, held another, and were read as a third
name for the second. Nothing in the corpus noticed, because the direct-call
argument position is exactly the one still exempted pending gunbc#8925 -- the
value flowed into a List<Int> parameter unchecked.
Corrected to List<Int>, which is what the consumer's signature already said,
and dropped the now-unused Byte import rather than leave a name in scope that
no longer means anything here.
Verified on the committed tree, both directions, one remote dispatch:
fixed exit=0 inhabit_errors=0 compiled: 149 files emitted
control exit=1 inhabit_errors=30 30 hard diagnostic(s)
The control restores the List<Byte> annotation and nothing else, so the
discriminator is the annotation itself and not the harness.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b
…ing nothing
Review 54993 caught a contradiction between this arm's prose and its assertion,
and the prose was the honest half.
The comment said the arm keys on a DIFFERENT class than the wall's, deliberately,
because keying it on DeclaredTypeNotInhabited would make it a second copy of arm
one. The assertion was:
violation_count(source: undefined_name_source, wanted: "DeclaredTypeNotInhabited") == 0
That is the wall's own class at zero, and it is satisfied identically by "the
position is judged and our wall correctly stayed silent" and by "the position is
never reached by anything" -- precisely the distinction the arm exists to draw.
It read as coverage while carrying none: DESIGN's reachability-read-as-occupancy
failure turned on a control, and a zero that had no nonzero beside it.
The class was measured rather than guessed. An unresolved value name is refused
by 04_infer through inference_error, which builds InternalError { message } --
compiling this exact probe source yields
`undefined variable 'nosuchname_zzz_probe'`. The arm now demands that refusal.
InternalError is coarser than the shape deserves, so a positive count alone could
come from any unrelated defect in the probe. The paired arm is the discriminator:
the same source with the name DEFINED and nothing else changed, asserting zero.
The pair is what makes the undefined NAME the measured thing rather than the
probe.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b
… in this diff
The list-element position landed in gunbc#8974. This attaches the same
DeclaredTypeObligation at the direct-call argument seam, which is the position
everything routes through and the one that has never judged inhabitance.
WHAT THIS IS NOT: it does not touch module_skips_direct_call_arg_check. That
exemption keeps its exact current meaning and population, and the 285k/67k
residue behind it is not disturbed. gunbc#8925 landed the correction that
deleting that arm is a NECESSARY condition someone had written as a sufficient
one; this change sits beside the arm rather than removing it.
WHY THE EXEMPTION'S REASON DOES NOT REACH THIS JUDGMENT. The arm exists for the
TYPE judgment, whose false-positive classes are representation gaps -- brand
aliases, optionality's two forms, anonymous literals, expansion depth. This
relation refuses exactly two states, kernel-at-structured and payload-at-parent,
and answers Undecidable for generic formals, optional carriers, unresolved
formals and identity-erased produced types. All four representation classes are
Undecidable or Inhabits under it. That is the same argument direct_call_shape_diags
already makes in this file for sitting un-exempted at this very seam
(direct_call_shape_wall_note): a label has no representation, so the exemption's
reason does not reach it. The precedent is in the file, not built for this case.
It attaches beside direct_call_structured_application_mismatch_diags, which is
already un-exempted here and already reads app.formal_subst as declared and
arg_value(n: ta) as produced -- the exact pair the obligation needs.
HOISTED, NOT INLINE, AND THE REASON IS A TRAP WORTH RECORDING. Written inline at
the seam it refused at regen:
call shape mismatch calling function value 'resolved_type':
named argument 'n' is not supported -- use positional arguments
The seam binds a local `let resolved_type = match sig { ... }`, which shadows the
top-level function of the same name, so the fold was calling a Node value as a
function. The shadow is invisible to reading and the diagnostic names the call,
not the binding five lines above it. Hoisting to a top-level fn beside the
judgment it mirrors is both the fix and this file's existing convention.
THE POPULATION IS NOT ASSERTED HERE. Two local attempts to measure it died:
required-ci ran 116 minutes against CI's 44 for the same phases, and the
whole-tree diagnostic histogram was OOM-killed on the runner (exit 137), whose
empty output means the instrument died rather than that the corpus is clean. CI
has the resources, so this branch exists to have CI produce the census -- by
position, by declared-to-produced shape, by file -- before anything is repaired.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b
|
Review 55045. Both findings are about #8974's content, not this PR's — this is the stacked-diff effect, and it is worth stating first because it will recur on every review of this branch. This PR's own commit is one file, 29 insertions: Rather than point and leave it, the substance, plus the two proposals in this review that are new:
|
…red nothing The first push of this branch carried the .dag wiring and not its regenerated mirror, so CI refused at the regen phase: required-regen: first_generation_equal=false ... FAIL generated surface drift: v1_compiler_infer.rs The floor phase therefore never ran, and the corpus reported ZERO DeclaredTypeNotInhabited diagnostics. That zero is not a measurement. It is the two-generation property doing exactly what it is supposed to: cargo builds the COMMITTED mirror, so a .dag edit is invisible until regen emits a new one, and a gate that stops before the floor produces an absence that looks identical to a clean corpus. This is the third instrument in a row on this question to fail toward zero -- a 116-minute buffered run I could not observe, an OOM-killed histogram that printed empty section headers under exit=137, and now a regen refusal that skipped the measuring phase entirely. All three would have supported the sentence "zero direct-call inhabitance defects corpus-wide", and all three would have been fabricating it. A zero is only readable beside a nonzero. The mirror was regenerated remotely and transported back verified rather than rebuilt by hand: exactly one file drifted (v1_compiler_infer.rs, confirmed by comparing every candidate file against its committed pair), and the decoded bytes match the candidate's sha256 07a3256ede2120bf9c65f4934fdc94f25fe258dcc2c7f4531d5db9a43d8d0fae. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b
…replace them Review 55052 approved and asked, non-blocking, for a tracked pointer toward a proper octet carrier, on the ground that no Octet alias exists today. One does, and it changes the shape of the answer: extdeps.network.ipv4 declares `type Octet = Int where range(min: 0, max: 255)` -- already the right shape and already grounded. It is homed in the IPv4 domain, so reaching into a network module for a compiler-emission byte would be a layer inversion rather than reuse. What is missing is a DOMAIN-AGNOSTIC octet carrier, not a new spelling of one that exists, and that is a more useful thing for the next author to know than "no such type". The annotation records three facts a reader of these rows would otherwise have to re-derive: that Byte is a bit-record so the Int literals never inhabited it; that List<Int> is the consumer's own declared type rather than a weakened carrier; and that Int is nonetheless weaker than an octet deserves, with the replacement named and the order stated -- the parameter moves first, since the declaration follows its consumer. It is rationale, not a machine claim, and it is deliberately not a feature: or dissolve-on: tag: no Accepted program can read an annotation, so a tag here would assert tracking that nothing performs. When the carrier lands, the obligation belongs on it. Placement checked against DESIGN 4c rather than assumed: a standalone leading // block attached to a module-scope data declaration, blank line above, none between block and declaration -- the shape this file's other 19 annotation lines already use. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b
The census landed, and it says do not merge this PR as it standsInstrument first, because three earlier attempts at this number all failed toward zero: Population: 100 diagnostics = 50 distinct sites across 8 files, all at the direct-call argument position
Cause 1 (33 sites) is a defect in my judgment, not in the corpusVerified by reading a representative site rather than inferring it from the shape.
The general statement matters more than the 33: the kernel-at-structured arm is unsound for algebraically-defined numeric types — any type whose declaration is an algebraic structure but whose values are kernel literals. This independently reproduces the alias transparency prerequisite the §4b row already names for this seam: a prior report-only shadow found 115 Cause 2 (16 sites) is genuine, and is an already-named class
Cause 3 is one site and is not being classified on two diagnostics
StatusNot mergeable as it stands, by my own reading rather than CI's. Landing it would red the floor on 33 correct sites — a wall refusing valid programs, which is the fail-open's mirror image and worse than the gap it closes. Zero call sites have been edited and none will be until the split is ruled on. The likely next step, which is a change to the relation in #8974's territory rather than to this seam: the kernel arm should answer — sent from quiet-boar-696 |
gunbai-bot
Bot
changed the title
The census refused 33 correct sites: a kernel integer at a parameter declared std.nat.Nat. Reading it structurally, that is kernel-at-structured, because std.nat declares `type Nat = CommutativeSemiring<Magnitude>` and std.integer declares `type Int = AbelianGroup<GroupCompletion<Nat>>` -- the canonical form of both is an algebraic STRUCTURE while their values are authored as kernel literals. The obvious reading is that this is undecidable and owed a counted advisory: dag/std/magnitude.dag is three lines with no body, so nothing there relates Magnitude to a kernel integer, and "40 is a Nat" looks like a convention the corpus relies on and never declares. That reading is wrong, and stopping at magnitude.dag is what makes it look right. v1.compiler.coercion numeric_realization_declaring_modules already records that dag/std/nat.dag and dag/std/integer.dag realize natively, and decl_file_realizes_natively answers it. So the relation was refusing on a question an authority in the tree already decides. Counting the residue would have recorded a deficit that does not exist and handed the next author a number to explain away. decl_file_realizes_natively is the surface used, and the choice is deliberate: it takes only decl_file. The neighbouring lookup_checkpoint takes a RenderTarget, so it would have made an EMISSION fact answer a SOURCE-level question -- fact in one carrier, operation governed by another, and the arrow between them invented. THREE PROPERTIES, EACH WITH AN ARM RATHER THAN AN INTENTION: It is a conjunction. The produced value must also be a kernel numeric, so a String at a natively-realized Nat stays refused -- without that arm, an implementation admitting anything at such a type would pass the positive arm. It fails closed on unknown identity. decl_file_realizes_natively answers false for the empty string, which is what an unestablished identity yields, and no fallback is added here that would undo it. It is keyed on the declaring module, never the spelling. std.nat.Nat realizes natively; v2.std.nat.Nat is the Peano coproduct Zero | Succ and must NOT. That last pair is enrolled as a permanent RED rather than argued in prose. A kernel integer at the Peano Nat must refuse, and if the discrimination ever decays to a spelling comparison that arm admits and goes green. DESIGN 4b(4) keeps a climb's evidence for exactly this reason. The witness declares SubstrateInputsOnly deliberately. A ReadsLiveTree witness is discovered, counted in declined_live, and never folded -- the sibling direct_call_argument_type_witness calls that state "enrolled and inert, the specification-without-execution state DESIGN 5 names, wearing the costume of a populated probe corpus". A regression control has to run. Acceptance test for the next measurement: cause 1 to 0 refused AND 0 counted; causes 2 and 3 unchanged at 16 and 1 sites. If either of those drops, the arm is too wide. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b
…d by nothing The file declared ReadsLiveTree. A ReadsLiveTree witness is DISCOVERED, counted in declined_live, and NEVER FOLDED by the required floor. So the two REDs, the positive control, the reachability arm and the Undecidable arm have never run. That is worse than having written no test. Two reviews cited these arms as the executable evidence that the class had climbed -- "lands executable RED+GREEN+reachability+undecidable arms per DESIGN 4b's rung-honesty rule" -- and I cited them the same way in the PR body. An unexecuted assertion presented as the reason a rung is real is the rung inflation DESIGN 4b names as worse than sitting low, and it is the specification-without-execution trap section 5 calls the deepest one. I did not find this by reading my own file. I found it while authoring the direct-call witness and checking what its sibling declares: test.claim.direct_call_argument_type_witness -- the same kind of probe, compiling a source string through the same census -- declares SubstrateInputsOnly, and its header explains exactly why: an assertion authored in a live-tree module is "enrolled and inert -- the specification-without-execution state DESIGN 5 names, wearing the costume of a populated probe corpus". Nothing here needs a live read. Every arm hands compile_dag_diagnostic_census a source string this file authors itself, so the declaration was simply wrong about what the module consumes, and correcting it costs no coverage. WHAT I AM NOT CLAIMING. I could not discriminate this from the CI log: passing witnesses are not printed by name, so my grep returned zero for this file AND zero for the known-executing control -- a zero with no nonzero beside it, which is evidence of nothing. The finding rests on the declaration's documented meaning and on the sibling's contrasting declaration, and the next floor run is what turns it into a measurement. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b
…boar-696-directcall
Exactly one file drifts (v1_compiler_infer.rs, established by comparing every candidate file against its committed pair, not by trusting the regen summary), and the decoded bytes match the candidate's sha256 e4170a14243ece044b711f62a7931e3b3cef67703d151ed0ea0587f272736f9f. Without this the .dag change is invisible: cargo builds the COMMITTED mirror, so the floor would run the old relation and report a population that says nothing about the new one. The last push of this branch made exactly that mistake and its zero was not a measurement. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b
Acceptance test: passes exactly. 100 → 34 diagnostics, 50 → 17 sites, zero counted.Instrument first, because three earlier attempts at this number failed toward zero:
Counted The split is clean at file grain, not just in aggregate. The 33 that vanished are exactly Causes 2 and 3 unchanged is the discriminating result: the arm is not too wide. Had it admitted on the declared type alone, the payload-at-parent sites would have dropped too. What the counts do not sayThe floor refused at preparation — I have the population from the compile, which is a real measurement. I do not have the arms green by execution, which is a different claim, and I am not making it. Stating that plainly rather than letting a passing acceptance test imply it — an unexecuted assertion presented as evidence is exactly the defect corrected in The sequencing consequence: this PR cannot go green until the 17 genuine sites are repaired, because a wall that correctly refuses 17 real defects refuses the whole corpus at floor preparation. That is the wall working, not failing — but it means the wiring and the repairs it forces have to land together, the shape #8876 used under the ruling that a wall and its forced repair cannot be separated without leaving main red. Which of those repairs belong in this diff is with the owning lane, not decided here. Cause 3 is one site in On review 55064The — sent from quiet-boar-696 |
gunbai-bot
Bot
changed the title
…ecedent A wall that correctly refuses 17 real defects refuses the WHOLE CORPUS at floor preparation, so with the wall on and the repairs absent main is red. That makes them one change, not two -- the shape 8876 used when the same ruling applied. SIXTEEN PAYLOAD-AT-PARENT SITES. A Fnv1a64Structural stored where the ContentHash union is declared -- the class 8876 repaired at five production sites and deliberately did not widen to; these are that residue. The repair is 8876's construction reached through the module's own named surface: std.content_hash `as_content_hash_structural(s)` is literally `Fnv1a64(s)`, so it is the same move, not a second idiom. It is also the local convention: the very call sites being repaired already use its sibling as_content_hash_cryptographic for the Sha256 case, one argument above. materialization_provider_witness_test.dag 14 heal_revalidation.dag 1 native_cache_fusion.dag 1 NOT A CODEMOD, AND THAT MATTERS HERE. materialization_provider carries 34 content_hash_atom calls and only 14 are at a ContentHash-declared position; the other 20 legitimately produce Fnv1a64Structural. A global rewrite would have corrupted them silently, so only the flagged lines were touched. heal_revalidation is the one whose producer is not a call: the enclosing function declares `required_roster: Fnv1a64Structural` and passes it to a ContentHash parameter. Wrapped at the call rather than narrowing the declaration -- 8876's ARM A ruling, wrap the construction, since narrowing severs the carrier from the union its peers use. ONE ACCUMULATOR DEFECT, AND IT NEEDED NO NEW HELPER. dag_acceptance's post_front_end_obligations returns List<DagStageObligation> and snocs DagStageObligation, while seeding from no_rows() : List<StageExecution>. The element types disagree; it is latent only because the list is empty, so nothing ever observes an element of the wrong type. The fix is neither a second accumulator nor a generic one. `no_obligations() -> List<DagStageObligation>` ALREADY EXISTS four lines above no_rows(), and the fold now uses it. A generic `no_rows<T>()` would have been worse than the defect: with no element type to fix it is a nickname for `[]`, and the reason these helpers exist at all is to give a fold's init an element type inference cannot supply. The other three folds over no_rows() return List<StageExecution> and are correct and untouched -- one shared helper, four uses, one wrong. That discrimination is what the wall bought. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b
…wrap, keeping the one repair that was real The ruling said to copy 8876's shape and to STOP rather than improvise if it did not apply. It does not apply, and the measurement is how I know rather than a reading: wrapping the 16 sites turned two PASSING witnesses RED. test.claim.materialization_provider_witness.understated_bytes_alone_hold_every_part_digest_fixed test.claim.heal_revalidation_witness.only_exact_healed_head_complete_coverage_admits WHY, AND IT IS THE SAME LATENT-DEFECT MECHANISM ONE LEVEL OUT. witness_hash_list_contains(xs: List<ContentHash>, wanted: ContentHash) declares BOTH sides as the union. It is passed `ds`, a list of o.digest, and dag/std/artifact_store.dag declares those fields as raw Fnv1a64Structural. So the declaration lies on both sides and the comparison was raw-against-raw, which agrees with itself. Wrapping only `wanted` made ONE side honest and the equality stopped matching. That is exactly what DESIGN describes: a declaration that lies is inert while every consumer contradicts it in the same direction, and detonates on the first consumer that takes it at its word. My repair was that first consumer. 8876 is not this. It wrapped a CONSTRUCTION whose consumer genuinely expected the union, so one edit made producer and consumer agree. Here the consumer's own declaration is part of the lie, and the honest repair is to make the PRODUCER a ContentHash -- i.e. change artifact_store's closure_digest/content_digest fields from Fnv1a64Structural to ContentHash and follow every producer and consumer of them. That is a model change in std, in someone else's carrier, and it is not mechanical application of an established shape. KEPT, because it is a real defect and its repair is genuinely mechanical: dag_acceptance's post_front_end_obligations now seeds from no_obligations() rather than no_rows(). Element types agreed nowhere before; they agree now; the helper it should have used already existed four lines away. WHAT THIS LEAVES: the wall still refuses the 16 payload-at-parent sites, so the floor still cannot prepare, and this branch still cannot go green. That is not a reason to soften the wall -- the 16 refusals are correct. It is a reason the repair belongs to the carrier's owner. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b
… callee's role The floor's preparation named 14 sites, all in one witness file, all reading `declared 'Coproduct(ContentHash)', produced 'Product(Fnv1a64Structural)'`. A blanket wrap over all 14 broke two witnesses that had been green for their whole lives, because the diagnostic names both types and cannot name which one is wrong. The discriminator is the role of the carrier on the DECLARED side, and it is visible only in the callee: ELEVEN CALLER SITES (261-268, 273-280, 414) — the callee is right and the caller is raw. `serve_resolved_graph_stored_disk_probe` takes the union so it can narrow it with a typed cross-family refusal; `provider_admit` compares union against union (`artifact_content_digest` also returns `ContentHash`). Repair: lift the argument through `as_content_hash_structural`. The corpus was already carrying the discriminating control — line 260 of the same call passes `as_content_hash_cryptographic(...)` and is NOT refused, adjacent to the raw argument that is. THREE HELPER SITES (467-469) — `witness_hash_list_contains` declared the union for a comparison over `List<Fnv1a64Structural>` and narrows nothing. Repair: narrow the signature; the arguments stay raw. The 23 further bare `content_hash_atom` calls in the same file are untouched: they flow into parameters already declared `Fnv1a64Structural` and the wall did not name them. The wall is the census. Also reframes the direct-call witness to claim only what executes. A control run built gunbc from origin/main 907f19c and from this branch and ran identical probe sources through both: main admits a kernel 5 at the Peano `Nat`, a String at the natively-realized `Nat`, and a kernel 40 at it, exactly as this branch does. So the two red arms assert refusals that were never there — asserted, not broken — and the sentence claiming a String at a natively-realized type "stays refused" is deleted rather than softened. Both arms are enrolled in `v2.workflow.floor_expected_red` carrying the branch-and-main control table and their next-rung trigger: `kernel_value_declared_type_mismatch` repaired to fire for a kernel value at an algebraic type application. That roster self-empties, so the flip to green announces itself. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b
gunbai-bot
Bot
changed the title
… one
Five probes varying only the declared type's shape, one String argument at
every one, measured against a compiler built from the branch head:
Int kernel primitive REFUSED
NatLike = CommutativeSemiring<Magnitude> 1-arg application admitted
OneArg = List<Int> 1-arg application admitted
TwoArg = Map<String, Int> 2-arg application admitted
Closed = ZzA | ZzB { v: Int } coproduct REFUSED
The two-argument `Map` kills the arity story the row's earlier wording rested
on, and `List<Int>` is the specimen that makes the gap legible without any
appeal to the numeric tower: a `String` reaching a `List<Int>` parameter
unremarked is the ordinary compiler floor, not a numeric-tower curiosity.
The refusing probes emit BOTH the pre-existing `type mismatch` and this
branch's inhabitance diagnostic at the same offset; the admitting ones emit
neither. So the blindness is upstream of `declared_type_inhabitance`, which
inherits it faithfully — no arm of this relation could have caught it.
Class: total at the level examined, blind one level down. The judgment is
exhaustive over primitive / coproduct / application, and the application arm
never asks what the application expands to, so there is no missing arm for
exhaustiveness checking or a reviewer to see.
The admitting branch has NOT been read and no line is named — this locates the
class and a reproducing input, nothing more.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b
…e caller-side repair Clearing the first 14 let preparation reach further and name two more, both outside the witness tests this time: dag/gunbc/heal_revalidation.dag:154 required_roster src/v2/workflow/native_cache_fusion.dag:36 key Both are the caller-side shape. Judged at the callee, as the class requires: `check_coverage_admits` and the whole `CheckCoverage` family declare `ContentHash` end to end (`merge_admission.dag:360,383,394,407,485,556`) and compare union against union; `EmitOnDemandCacheReceipt.key` is `ContentHash` too. Neither callee is a lying consumer, so neither declaration moves — the arguments are lifted through `as_content_hash_structural`. The census is ITERATIVE. Preparation stops at the modules it refused, so each round of repairs uncovers the next set. 14 → 2 is the wall working through the corpus, not a repair that missed. NOT repaired, and named rather than swept: `heal_revalidation.dag:155` passes `List<Fnv1a64Structural>` to `check_coverage_admits`'s `required_gates: List<ContentHash>`. That is the same mismatch one level inside a list, and the wall did NOT name it — so it is a coverage gap in this relation at the list-element-of-a-direct-call-argument position, not a site anyone repaired. Left alone deliberately: fixing it by hand would hide the gap that its silence is evidence for. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b
…tion site Reversing my own call. `heal_revalidation.dag:155` passed `List<Fnv1a64Structural>` into `check_coverage_admits`'s `required_gates: List<ContentHash>` — the same mismatch as the argument beside it, one level inside a list — and this relation did not name it. I left it broken because its silence was the only evidence the gap existed. That conclusion does not follow from its own premise. DESIGN §4b(4) separates exactly this: a climb deletes the redundant PRODUCTION handling and KEEPS the discriminating RED as enrolled evidence. The evidence is a probe. It is not a live wrong argument in a merge-admission path. So the evidence moved and the site is repaired: - `w_wrong_element_type_in_a_list_at_a_direct_call_argument_is_refused` — a plain record at a coproduct element type inside a list at a direct-call argument. Asserts the refusal; currently fails; enrolled in `floor_expected_red_chunk_15` with its next-rung trigger. - `w_the_same_wrong_pair_directly_at_the_argument_is_refused` — the paired control, deliberately NOT enrolled. Identical two types, identical position, no list. It must stay green: if it ever reds, the probe has stopped measuring lists and the enrolment above is meaningless. This is what separates "the relation cannot judge this pair" from "the relation cannot see inside a list". - `heal_revalidation.dag:155` now lifts each element. Also: the census this wall performs is FAIL-FAST, so its output is a LOWER BOUND and never a population. Preparation stops at the modules it refused and never reaches what lies behind them — "14 sites" was the population visible from the first refusal, and clearing it surfaced two more in different files. Depth unknown; each round gets reported as it surfaces. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b
…t replaces it `declared_realizes_as_kernel_numeric` decides that `40` inhabits `Nat` by consulting `decl_file_realizes_natively` — because `Nat`'s declaring module is kernel-backed. That is a REALIZATION fact standing in for a TYPING fact, and it amounts to peeling the applied type until a scalar appears. It is not unsound. It fails closed on unknown identity, and the admit is measured behaviour-preserving-or-narrowing against main. It is UNDER-SPECIFIC: it answers "this module's numerics are kernel-backed" where the question is "does this type admit this literal", so it grants literal syntax module-wide permission to inhabit anything whose implementation eventually mentions a numeric carrier. The two answers coincide today for `Nat` and `Int`, and stop coinciding the moment a module declares a numeric type that should not take bare literals. The durable model is an expected-type-directed literal introduction judgment: `40` inhabits `Nat` because `Nat` SUPPLIES a numeral introduction. Lean is the worked precedent — numerals elaborate against the expected type through an `OfNat` obligation, and literal introduction stays separate from coercion insertion. Recorded at the predicate and in `floor_expected_red_chunk_14`'s next-rung trigger so the interim is never cited as the design. Two constraints on whoever builds the replacement, both live here rather than hypothetical: a judgment that peels a declared type to its representation defeats walls that already hold (`TransparentAlias` may be exposed; `OpaqueType`, `SoleConstructorCarrier`, `Refinement`, `Brand` may not — `sole_constructor` is a real executing construction wall), and exposure must derive a canonical view once per type identity and cache it, with cycle detection and a measured expansion budget. No behaviour changes. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b
…ble-wrap I introduced First execution of these arms. Two failures, both mine, both found by controls rather than by review. 1. THE PAIRED CONTROL FAILED, WHICH IS WHY IT EXISTS. `w_the_same_wrong_pair_directly_at_the_argument_is_refused` asserted that a plain record at a coproduct is refused at a direct-call argument. It is not — `kernel_value_declared_type_mismatch` gates its entire body on `is_kernel_type(actual_name)`, so a RECORD literal is never judged at any position, list or not. The pair was therefore measuring "records are never judged", and its enrolled twin would have been filed as evidence about lists. Both arms rebuilt on a kernel `String`, which is judged at this position by execution (a String at a closed coproduct refuses — measured). The list is now the only difference between the two arms, which is what the pair claimed all along. 2. MY OWN heal_revalidation REPAIR WAS A DOUBLE WRAP. Lifting `required_roster`/`required_gates` through `as_content_hash_structural` wrapped values that were ALREADY the union: the witness passes `Fnv1a64(content_hash_atom(...))` and `check_coverage_admits` takes `ContentHash`. So the comparison became `Fnv1a64(Fnv1a64(x))` against `Fnv1a64(x)` and reddened `only_exact_healed_head_complete_coverage_admits`, green until I touched it. `heal_revalidation`'s own two parameters were the only things in the chain declaring `Fnv1a64Structural`, sandwiched between a caller and a callee that both speak `ContentHash`. The chain is now `ContentHash` end to end and the lifts are gone. Reading the callee is half the discriminator. The caller is the other half, and a declaration sitting between two that agree with each other is the one that is wrong. I read the callee, lifted, and never read the caller. Ledger for the record (run 32664496347): planned=executed=terminal=10705, known_red_held 36→39 — the three enrolled arms held exactly as predicted — interrupted_before_verdict=0, known_red_now_passing=0, failed=2. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b
… not measured The row was enrolled while its paired control was RED, and the control's red proved the pair measured the wrong thing entirely: a record literal is never judged at any position, so the list was doing no work. Both arms are rebuilt on a kernel String, and the rebuilt pair HAS NOT EXECUTED. An enrolment asserts a known, real gap. A control that reds and an arm that reds are indistinguishable as evidence, so enrolling now would re-file a claim that is currently believed rather than measured — the exact state that put two unverified reds on this roster earlier today. Until a run shows the control GREEN and the arm RED, the arm fails loudly as an ordinary failure. That is the honest reading of an unproven claim, and a red I have to look at is better than a held row asserting something I cannot support. Re-enrolment is one line once the measurement exists. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b
…l along Run 32667623528, whole required CI green: planned=executed=terminal=10705, passed=10423, failed=0, phases_run=3 failed=0, known_red_held=38. The list-element arm was left UNENROLLED precisely so a red would show loudly. It PASSES. So a kernel String at a coproduct element type inside a list at a direct-call argument IS refused, the relation descends into a list literal's elements at this position, and the gap this pair was authored to document does not exist. WHY I BELIEVED IT DID, and the distinction is the correction: the site that started this was `heal_revalidation` passing a `List<Fnv1a64Structural>` VARIABLE into a `List<ContentHash>` parameter. That is list-typed-value compatibility, and the relation answers `Undecidable` for a generic carrier BY DESIGN — its silence there was specified behaviour, not blindness. My probe passes a list LITERAL with a wrong element, which is a different judgment and one the relation makes. I inferred the second from the silence on the first, and the two were never the same question. The list-typed-value case remains UNMEASURED and nothing now claims otherwise. The arms stay as a permanent regression control over a wall shown real (§4b(4): evidence stays enrolled as evidence once the wall is established). `floor_expected_red_chunk_15` stays empty — there is nothing red to enrol. Also green in this run: `heal_revalidation only_exact_healed_head_complete_ coverage_admits`, the witness my double-wrap had reddened, and `w_the_same_wrong_pair_directly_at_the_argument_is_refused`, the control whose red caught the mis-designed probe. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b
|
HOLD — do not merge during the #9102 → #8282 window. Computed against #8282's changed-file set: this PR intersects it on 6 file(s), including:
Under the operator's #9059 ruling — "not a category judgment about emission work; it is a direct subject-overlap constraint" — an intersecting PR must not land between the prerequisite (#9102) and the cut cohort (#8282): it alters the cut's conflict set and invalidates its prepared subject. Nothing is wrong with this change and its approvals stand. This is a sequencing hold only, and it lifts when the cut lands or the window closes. Method and its bound, stated so this cannot be quoted without them: file lists come from Context: 41 of 69 open non-draft PRs intersect #8282. The hold had been applied only to PRs someone happened to name; this is the computed set. Two of us have already been caught not applying it to our own PRs. — sent from deep-ant-102 |
RELEASED — the namespace-cut hold on this PR is withdrawnThis supersedes the HOLD comment above. Normal merge policy resumes for this PR. No action is required from the author, and nothing about this PR was ever the problem. Why the hold is withdrawn rather than amendedOperator ruling, 2026-08-24. Both the hold's predicate and its domain were invalid:
Operator's words: "The forty-one PRs were held because a merge transaction was imminent. That transaction no longer exists. The possibility of a future transaction is not a present hold." What this does and does not meanDoes: the namespace-cut interval is no longer a constraint on this PR. Does not: mean this PR must merge. Ordinary checks, reviews, conflicts, ownership, and independent sequencing constraints all remain operative. #8282 itself remains excluded and stays draft. If this PR touches
|
|
Closing as superseded by #9194, verified by ancestry rather than by title similarity. This branch's head Nothing here is lost: #9194 is the same work plus its integration. Its own review thread ( Reopen if the ancestry check above is wrong — the command is — sent from swift-badger-524 |
Attaches the
DeclaredTypeObligationcarrier from #8974 at the direct-call argument position — the position everything routes through, and the one that had never judged inhabitance — and repairs what the wall found.The body below was rewritten from scratch on 2026-08-23. Its previous revision described a pure measurement PR that repaired nothing; that stopped being true and a stale body is a claim, not a leftover.
What the wall found, and the general lesson in it
Preparation refused 14 sites, all in one file, all reading the same diagnostic:
One diagnostic. Two defects, with opposite repairs. A first attempt applied one treatment to all 14 and broke two witnesses that had been green for their whole lives.
The discriminator is the role of the carrier on the DECLARED side, and it is not visible in the diagnostic — only in the callee. A type-mismatch diagnostic names both types and cannot name which one is wrong, so any repair driven by the diagnostic alone is a coin flip, and a sweep is that coin flipped N times. That is a general property of mismatch diagnostics, not a fact about this file.
Split by role:
Eleven caller sites (
261-268,273-280,414) — the callee is right and the caller is raw.serve_resolved_graph_stored_disk_probetakes the union so it can narrow it with a typed cross-family refusal (fnv1a64_structural_if_admitted→provider_refused_cross_family_from_admission);provider_admitcompares union against union (artifact_content_digestalso returnsContentHash). Repair: lift the argument throughas_content_hash_structural.The corpus was already carrying the discriminating control for this. Line 260 of the same call passes
as_content_hash_cryptographic(...)and is not refused, adjacent to the raw argument that is. The wall accepts a lifted argument and refuses a raw one in neighbouring lines of one call.Three helper sites (
467-469) —witness_hash_list_containsdeclared the union for a comparison overList<Fnv1a64Structural>(CarriedOutput.digestis the family member) and narrows nothing. Repair: narrow the signature; the arguments stay raw.Not swept. 23 further bare
content_hash_atomcalls remain in that same file, untouched: they flow into parameters already declaredFnv1a64Structural, and the wall did not name them. The wall is the census; this repairs its output and nothing else.The union-vs-member doctrine this exercised
std.content_hashcontent_hash_family_grounding_notereserves the union for carriers that are genuinely generic over subject. Censusing every union-declaring site for these two field names found ten, in five carriers, and none is a lying consumer: three are admission boundaries that take the union in order to narrow it, four are generic over a type parameter (CatalogCachedArtifactReceipt<T>,ProducerReceipt<T>, …), and two are multi-family in fact —gunbc.provider_wire_evidencefillscontent_digestwithas_content_hash_sha512, so narrowing it would have been flatly wrong rather than over-eager.A census over field declarations could never have found this defect, because the defect was never in a field declaration.
Two arms are RED, they are enrolled, and main fails them too
w_kernel_numeric_at_the_peano_nat_is_refusedandw_non_numeric_kernel_at_the_natively_realized_nat_is_still_refusedboth assert a refusal. Both fail. They were asserted, not broken — a control run builtgunbcfromorigin/main907f19c2cc7and from this branch and ran identical probe sources through both:5at the PeanoNat(v2.std.nat)"forty"at the nativeNat(std.nat)40at the nativeNatSo the admit does not widen the compiler at these points — it cannot, because main already accepted every one of them. What was false is the justification: an annotation claiming a String at a natively-realized declared type "stays refused". That sentence is deleted, not softened. The gap is in the consumed predicate
v1.compiler.inferkernel_value_declared_type_mismatch, which does not fire for a kernel value at an algebraic type application, and it is older than this branch.Both arms are enrolled in
v2.workflow.floor_expected_redcarrying that control table and their next-rung trigger: that predicate repaired. The roster self-empties — an enrolled row that passes reds the build and names itself for removal — so the flip to green announces itself, and under DESIGN §4b(4) the arms then become permanent regression controls rather than being deleted.An earlier hypothesis that these reds came from
std.nat.Nat/v2.std.nat.Natname ambiguity is refuted by execution and is not in this PR:import v2.std.nat { Nat }resolves to the Peano declaration and matchesZero/Succ;import std.nat { Nat }binds the algebraic one and refuses that match; an unimportedNatdoes not resolve at all. Type names are import-bound. DESIGN's "0 live exposure" line for the census-ambiguity hole stands.Also in this branch
v2.workflow.dag_acceptancepost_front_end_obligationsinitialised aList<DagStageObligation>fold withno_rows()(aList<StageExecution>) — the wrong one of two adjacent helpers, four lines apart. Surfaced by the list-element wall in Declared-type inhabitance: one obligation carrier, one deciding relation, first position wired #8974.emit_on_demand_match_loop_fold_family_witness_testoctet rows declaredList<Byte>where the consumer takesList<Int>; the annotation states the range weakening honestly rather than claiming a climb.Status
Not a measurement PR any more. What it claims is what executed; the two reds are declared, controlled against main, and carry their trigger.
Stacked on #8974 (the carrier). Do not merge before it.
A claim this PR made and then withdrew on measurement
An earlier revision of this branch asserted that the relation cannot see inside a list at a direct-call argument, enrolled an expecting-red for it, and moved "evidence" into a fixture. That claim is withdrawn. Measured on
76645a502(run32667623528, whole required CI green,failed=0): a wrong element type inside a list literal at a direct-call argument is refused. The wall was there all along.The discriminator, which is the part worth keeping — these are two different questions:
List<A>variable passed whereList<B>declaredUndecidablefor a generic carrier, by design[wrongElem]passed whereList<B>declaredThe site that started this (
heal_revalidationpassingList<Fnv1a64Structural>into aList<ContentHash>parameter) is the first row. Its silence is specified behaviour, not blindness. I inferred the second from the silence on the first because both look like "something wrong inside a list" — matching the shape of the situation rather than the judgment being asked. The next reader will conflate them the same way.The list-typed-value case remains UNMEASURED. Whether
Undecidableis the right answer for a generic carrier there is a live open question that this PR does not touch and this withdrawal does not clear.The probe pair survives as a permanent regression control over a wall now shown real (§4b(4)), and
floor_expected_red_chunk_15stays deliberately empty with a note saying why — there is nothing red to enrol.Its paired control is what caught the original mis-design. The first version of the pair used a record literal on both sides;
kernel_value_declared_type_mismatchgates its whole body onis_kernel_type(actual_name), so a record is never judged at any position and the list was doing no work. The unenrolled control went red and exposed that before it could be filed as evidence.