Repository navigation
Compiler floor — one declared-type inhabitance authority, two grammar positions wired, ten declared - #9194
Merged
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
…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 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
…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
… 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
briansrls
marked this pull request as ready for review
August 25, 2026 15:04
….probe_fx probes Two conflicts, both resolved from the merged .dag authority rather than from the conflict text. src/v2/test/claim/execution/emit_on_demand_match_loop_fold_family_witness_test.dag Both sides independently made the same List<Byte> -> List<Int> change on the six octet rows; only this branch added the annotation explaining why (std.bit's Byte is a bit-record, so an Int literal never inhabited it, and the consumer's signature already carried List<Int>). Kept the annotation -- it is a standalone leading block attached to a module-scope declaration, per DESIGN 4c. src/v1/stage0/src/v1_compiler_infer.rs Generated mirror; not hand-merged. The single conflict is the sorted `use self::` header, where each side contributed variants of types it declared. Resolved as the sorted union, and each of the four names verified to be declared exactly once in the MERGED src/v1/04_infer.dag -- so the header is derived from the merged source, not guessed from the diff. The mirror body auto-merged; --required-regen adjudicates whether it corresponds to the merged .dag, and that is CI's answer to give, not a local claim. src/v2/workflow/floor_expected_red.dag auto-merged, and the result was checked at identity grain rather than by line count, since taking one side of a roster whole deletes rows with no conflict marker to see: base 87 ids, main 25 (63 dissolved on main), branch 89 (2 added here), merged 27 = main's 25 + this branch's 2. Both new expected-red rows present; zero main-side rows lost. .probe_fx/ (10 files) deleted. They are investigation scratch with no executing consumer: the required floor's source roots are exactly `dag` and `src/v2`, so nothing under .probe_fx is discovered, planned, or run. The one apparent reference is not an edge -- dag/test/claim/import_shadowed_by_local_definition_witness_test.dag carries the probe source INLINE as a string literal, byte-identical to .probe_fx/ish/probe.dag, so the file was a second representation of data the witness already holds. A fixture directory is not a consumer, and a citation is not an edge. Every other deletion in this merge (177 paths) was verified to come from main's own history since the merge base; zero unexplained. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
added 2 commits
August 25, 2026 15:51
…e reasons (seed mirrors not yet regenerated)
gunbai-bot
Bot
changed the title
…or the new variant
Contributor
Author
|
Thanks — Finding 2 — real, and worse than stated. Fixed.Confirmed. This is the "total at the level examined, blind one level down" shape DESIGN names — the match was Repaired as a counted, non-blocking, per-reason residue, not a refusal: Why advisory and not blocking, since that is the part worth challenging: refusing here would Finding 1 — real, and it was BOTH a title problem and an undeclared gap. Both fixed.Confirmed by construction site, not by reading. Of the twelve members of I also checked whether the residual ten were declared anywhere as expected-red rows with triggers. Deliberately not enrolled as expected-red rows: an expected-red row asserts an observed red, Finding 3 — the receipt exists, and I can now show it by execution rather than cite it.The hand-Rust gate is already answered in-tree by Rather than rest on the note, I measured it. Deleting one of the two arms and compiling: with the unmutated control green at exit 0, same command and same base. Neither match carries a One thing found while verifying, reported rather than folded inBuilding this branch surfaced that — sent from loyal-dove-837 |
Contributor
Author
One classification stated in advance:
|
added 3 commits
August 25, 2026 18:35
Only conflict was src/v1/stage0/src/v1_compiler_infer.rs, a GENERATED mirror ('Generated by v1
compiler -- do not edit', source module v1.compiler.infer). Its source 04_infer.dag auto-merged
clean, so it is resolved by REGENERATION in the following commit rather than by hand-editing a
do-not-edit artifact. The ours side is staged here only as a build seed -- it carries the new
DeclaredTypeInhabitanceUndecided variant that the merged cli_run.rs arms reference, so the tree can
compile well enough to run the emitter that replaces it.
SEMANTIC CHECK, because a clean textual merge is exactly where two rules answering one question
hide. #9192 landed select_formal_for_call_argument as the single authority for which formal a call
argument binds to, and rewrote build_call_application_plan to route matched_arg through
call_argument_selects_formal_index. This branch's pre-merge copy still used the old name-match-with-
raw-source-index fallback -- the rule #9192 exists to remove, and the one that fabricates a refusal
on f(b: 2, 1). Verified main's version won the merge: the plan builder at the merged seam calls
call_argument_selects_formal_index, and this branch contributes no second copy of that rule. The one
remaining 'skip(pair.first)' fallback is inside borrowed_callable_call_type, a different seam, and
origin/main carries it identically -- it is not something this merge introduced.
…ix, the .rs did not The merge commit 4c9c55c resolved the generated-mirror conflict by taking one side whole. That is a SILENT deletion -- no conflict markers, clean tree, and the committed mirror became an OLDER COMPILER than the .dag it claims to mirror. Measured, with the control that makes it a result rather than a name-mangling artifact: fn .dag .rs(before) select_formal_for_call_argument 1 0 call_argument_formal_at_position 1 0 call_formal_claimed_by_a_label 1 0 declared_type_inhabitance 1 1 <- pre-existing, same grep, present in both declared_type_obligation_diags 1 1 <- same and `select_formal_for_call_argument` IS spelled that way in origin/main's mirror, so the grep works and the absence is real. #9192 landed to stop inference binding named arguments by POSITION -- refusing valid programs -- and this branch would have re-shipped the seed without that fix while the .dag said it had it. REGENERATED, NOT RE-RESOLVED AND NOT SPLICED. No hand edit to the .rs. The emitted file was taken from target/stage0-regen-candidate/src/ and installed whole. Receipts, from runs that did not share a candidate directory: round 1 (broken head): first_generation_equal=false FAIL generated surface drift: v1_compiler_infer.rs round 2 (installed): first_generation_equal=true planned=135 executed=135 declared_divergent=1 [main.rs] The fixed point is demonstrated at byte grain, not just by the flag: the installed file's sha256 210e64fb2ad08be2 was recorded BEFORE the confirming run, and that run re-emitted the identical hash. diff -rq over the candidate tree reports no other differing file. CI independently reached the same verdict on the broken head (run 32884947431), with a byte-identical message -- so the mirror-to-source comparison on a PR is intact and this red was the gate working, not a flake.
…rror Main tip 151e771. ONE conflicting path: the generated mirror src/v1/stage0/src/v1_compiler_infer.rs. src/v1/04_infer.dag (+104 from main) and cli_run.rs (-373 from main) both AUTO-MERGED, verified by a tree-wide grep for conflict markers returning only the mirror. THE MERGE DRIVER DID NOT FIRE, and that is the second time on this PR. It is enrolled by BASENAME while the population is defined by a HEADER, so it protects 2 of 136 stage0 mirrors and v1_compiler_infer.rs is outside it. On #9196 the same driver DID refuse a generated .yml and printed the regeneration recipe; here git left ordinary conflict markers and would have accepted a hand-resolution. REGENERATED, NOT HAND-RESOLVED -- and the binary vintage mattered, measurably: binary built from f57bc0e (pre-merge): drift = extdeps_uri.rs, v1_compiler_compile.rs, v1_compiler_infer.rs, v1_rt.rs (4) binary built from the MERGED tree: drift = v1_compiler_infer.rs (1) Same tree, two binaries. Three of the four were EMITTER VINTAGE, not tree drift: this diff touches inference and has nothing to do with extdeps_uri.rs or v1_rt.rs. Installing the first candidate would have written an old emitter's bytes over mirrors main had already advanced -- silently, and it would have read as a clean regen. A drift list wider than the change is a claim about the instrument. So the recipe's order is wrong when the binary predates the merge: REBUILD FIRST, then regenerate once. The binary was dated before use -- it now accepts --required-lane and routes phases by lane, which the pre-merge one rejected. RECEIPTS, from a rebuild off the installed seed: required-regen: first_generation_equal=true planned=135 executed=135 declared_divergent=1 [main.rs] installed sha256 12110f0a3dc440ef... recorded BEFORE the confirming run and re-emitted identically by the rebuilt binary; diff -rq shows no other file differing. v1_src_dag_parse: 3998 file(s) parse-clean. The three #9192 functions stay 1/1 dag-to-rs: select_formal_for_call_argument, call_argument_formal_at_position, call_formal_claimed_by_a_label.
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 29, 2026
…prepare or build over the live tree carry a live-corpus ignore reason and leave the required run, and the rot the first-ever `cargo test` exposed is repaired at its authorities, not hidden `cargo test -p v1-compiler --lib` had never run in CI. Its first run (33238828500) was cancelled by its own 60-minute timeout with 204 of 682 tests finished, because ~126 of the "unit" tests each build a fresh multi-entry index over `src/v2`+`dag` (4,260 modules; ~197 single-thread minutes on srv2 under nextest, 97 tests over 60 s, `self_compile_all_modules` alone 505 s), and the runner executes them serially. Those tests now carry `#[ignore = "live-corpus: ..."]` — the crate's existing `manual:` convention, one class, declared on the carrier — and the rung-drop row `required_gate_bankruptcy` names them by their instrument (`cargo test -p v1-compiler --lib -- --ignored --list`). The unit population runs in ~10 s after the compile (srv2: 537 passed / 136 ignored). Of the 44 failures the full run exposed, the 15 in the unit population are repaired where the fact lives: - REAL DEFECTS (two): `try_index_source_root_into_module_index` keyed files by their walked path, absolute since #9548 anchored the root, while the strict builder keys through `module_index_path_key` — the primary-precedence index disagreed with the strict one on every path; keyed through the same authority now. `try_build_module_index` carried `if root_idx > 0 { continue; }` before its collision refusal (from #7791), so a module declared in two roots shadowed silently in the builder named strict; the guard is gone and overlay callers have `build_module_index_primary_precedence`. - v1 TYPECHECK DEFECT: `declared_type_inhabitance` reads `params` as generic type parameters, which is exactly what a callable formal carries, so every higher-order call produced a counted advisory with a false reason (#9194); `direct_call_argument_inhabitance_diags` now excludes callable formals like its sibling `direct_call_arg_type_mismatch`. Mirror regenerated (two passes: the test blob lives inside the emitter). - STALE AUTHORITY ROWS after the #9637 reorg: 12 entry literals in `gunbc.ci_layer_roots` and 2 in `gunbc.offline_local_recipe` repointed; the two long-lane rows and one freeze row whose subjects 611fd02 and #9206 deleted are gone; the three freeze rows for relocated witnesses are DELETED rather than repointed, because the freeze gate defines relocation as growth and the roster may only shrink. `gunbc.non_fold_residue` receives the 22 sites it lacked and loses the 4 whose subjects moved or greened; its .dag twin therefore leaves floor_expected_red (it passes) and joins cost-debt chunk 12 (629 ms against the 500 ms ceiling, its whole cost the corpus scan it checks). - DELETED SUBJECTS: `cli_run::floor_witness_a_prove` (its runner, prove test and fixtures went with the FLOOR-Y cutover); the census pin tests and helpers for `docs/probes/census_extra_excludes.txt` (#9132 deleted every transcription). - EARLY ABORTS: three witness-admission tests and the roadmap jsonl-carrier test were "fast" only because they failed before their expensive step; with their inputs repaired they read the live tree for 2-4 minutes each and join the live-corpus class. - TEST ROT: the reorg rewrote a revision-addressed literal (`9ce6526c528:dag/gunbc/roadmap/...`) that must name the pre-reorg path; the method-existence witness anchored on a `Primitive()` row the frontier no longer holds. Not done here, receipts-lane rot for follow-ups: `test.claim.expectation_frontier_witness_test` names the deleted long-lane file; the affected-set kernel (`floor_diff_edits_from_diff_text`, `rerun_frontier_nodes_for_entry`, …) has no production consumer since FLOOR-Y and should go with its remaining fixture-dependent tests; the roadmap jsonl-carrier test takes 453 s and fails after its expensive step. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013G3t66QwKJFK5w8jXxMXP2
briansrls
added a commit
that referenced
this pull request
Aug 29, 2026
…e prepares the roster's closure, not the tree; rust unit tests in their own job; the un-required phases declared as a rung drop (#9663) * Unbreak main: drop the JsSite artifact rows whose authority #9641 deleted, and give the six witness-bin TypeEnv initializers the unit_variant_index #9656 added Two integration collisions between independently green PRs: - #9641 deleted dag/examples/js_site but gunbc.generated_artifact and gunbc.generated_artifact_emit still imported it, so the whole-tree strict resolve refused and every floor on main has been red since. - #9656 added TypeEnv.unit_variant_index; infer_semantics_witness.rs builds six TypeEnvs by hand and none carried it, so --bins failed. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013G3t66QwKJFK5w8jXxMXP2 * The lib's own unit tests build one more TypeEnv by hand; give it unit_variant_index too Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013G3t66QwKJFK5w8jXxMXP2 * Required CI is the compiler floor: a static gate roster, prepared as its own import closure, with the other four phases and the product witnesses moved off the merge path Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013G3t66QwKJFK5w8jXxMXP2 * Drop the six duplicate unit_variant_index initializers the merge with #9648 produced * Drop the six duplicate unit_variant_index initializers the merge with #9648 produced * Regenerate .gitattributes: the six js_site rows projected from the deleted artifact registry entries go with them * Regenerate the four projections of this change: witnesses.yml (probe and all-bins steps gone, rust-unit-tests job added), DESIGN.md and design-ledgers.md (the rung-drop row), .gitattributes (js_site rows gone) * Restore the lib-test TypeEnv initializer's unit_variant_index (lost when the merge took main's cli_run.rs wholesale) * The gate closure is the loader's both-closure (imports + reference edges to a fixpoint), not the import headers: stripped modules reach their providers by reference, and the header walk left 1,190 names unresolved * Shrink the namespace transition roster: the 314 std->extdeps consolidation rows landed with #9641 and now refuse every PR as stale * Build the entry index once for both gate closures (it is the expensive part: ~75-110s per build on the corpus) * Gate closure includes containment ancestors to a fixpoint: a module importing only a child of the declaring module still binds the parent's declarations * The floor's policy module is always a closure seed: its rosters are evaluated in a frame over the prepared subject * The reference-closure index is keyed by the prepared subject's digest, bounded to the two subjects a floor process prepares by design — the gate's policy-closure preparation and the gate closure are two subjects in one process, and a once-per-process index refused the second (ReferenceIndexSubjectChanged built_for_modules=47 observed_modules=1952, CI and srv2 at 066725c) The old check keyed on module COUNT: two subjects of equal size would have shared one index silently. The new one keys on `subject_digest`, so the index a scope consults was built from the graph that scope is over, by construction. The population is bounded by FLOOR_PREPARED_SUBJECTS_PER_PROCESS = 2 (policy closure, gate closure) — a third distinct subject still refuses with the same cause, because a subject per claim is the corpus walk per row the index exists to avoid. Evidence: srv2 rerun of `claim_executor --required-ci --required-lane witnesses` at this tree builds the 47-module policy index (subject=09966adcd218af0e) and proceeds into the 1,954-module gate preparation instead of refusing at claim scope. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013G3t66QwKJFK5w8jXxMXP2 * The floor's own runtime authorities are explicit closure seeds: the gate-bounded subject refused at output-policy install because resolve_channel_policy had only ever resolved by pool-membership coincidence — the flat bare-name channel found gunbc.output_policy because the whole corpus was loaded, not because the policy closure references it REQUIRED_FLOOR_RUNTIME_AUTHORITY_MODULES names every module the floor's Rust evaluates by name outside the gate roster: the policy module (its rosters), v2.workflow.floor_naming_hygiene (qualified evaluations), and gunbc.output_policy (bare, from install_output_policy_in). All three are seeds of the gate closure; a new by-name evaluation adds its module here or refuses at its own call site. Measured: the first gate-bounded run (srv2, at 2d5502a) got past both reference-closure indexes and refused with "no declaration named 'resolve_channel_policy' in this execution's loaded index". Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013G3t66QwKJFK5w8jXxMXP2 * A by-name evaluation of a module's declaration runs in THAT module's scope: the floor installed the output policy and the naming-hygiene predicates from the policy module's frame, which reached gunbc.output_policy only by the accident of the whole-tree reference closure — under the gate-bounded subject the module was loaded and the name still refused floor_authority_frame(prepared, module) builds a hermetic frame over one module's exact claim scope. install_output_policy_in now receives the frame over gunbc.output_policy; floor_barren_test_sidecars the one over v2.workflow.floor_naming_hygiene. The policy module's frame keeps only the policy module's own rosters. Measured (srv2, lanes 5 and 6): with gunbc.output_policy present in the 1,954-module subject — the seeds changed the seed count 906 -> 908 and the closure not at all — resolve_channel_policy still refused as "no declaration named ... in this execution's loaded index". The scope, not the subject, was the coincidence. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013G3t66QwKJFK5w8jXxMXP2 * The floor's rosters are joined only over identities inside the required gate — an enrolled identity whose module the gate never loads is withheld with the same accounting as cost-debt withholding, not refused as stale; and two modules that reached rust_target_model_staging by bare reference now import it, because the loader follows bare references only for import-free modules while the claim scope follows all of them Measured on the first gate-bounded fold (srv2 lane 7, CI at 006b0ef): ExpectedRedIdentityDidNotExecute count=39, every row in a module outside the gate roster; and v2.test.lens_vacuity.vacuity_test x5 ERROR no-such-function `rust_target_model_staging`, reproduced standalone with `gunbc run --entry src/v2/test/lens_vacuity/vacuity_test.dag`. The loader's both-closure (build_both_closure_edge_index) skips the bare scan for any source that declares import lines, so rung_3_4_common (one import) and leaf_model_verification's bare edge to v2.extdeps.languages.rust was never followed; under the whole-tree subject the flat channel found it anyway. The import is the form 10 of the 12 sibling callers already use; the loader/scope divergence is recorded in the PR. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013G3t66QwKJFK5w8jXxMXP2 * The gate closure follows bare cross-module references from EVERY module, with the loader's own scanner, to a joint fixpoint with containment ancestors — the loader's both-closure bare-scans only import-free sources, while the claim scope the fold builds over the subject follows bare references from all of them; and route-gap expectations located outside the gate are withheld like the roster rows they join Measured 2026-08-29 on srv2: with the gate subject, `gunbc run` of v2.test.lens_vacuity.vacuity_test refused no-such-function `rust_target_model_staging`, then `eval_context` after the first was imported — one absent module per run, because rung_3_4_common (one import line) and leaf_model_verification reach them by bare reference and build_both_closure_edge_index skips the bare scan for any source that declares an import. The fixpoint reuses bare_reference_pull_paths_for_source, so the relation is the loader's and not a second scanner; the count of modules pulled this way is printed on the gate-closure line. Lane 8 (srv2) then refused `floor_route_gap_expectations: located identity is absent from derived roster` for an identity whose module is outside the gate: the roster had its outside-gate rows withheld and the expectations had not. Both sides now withhold by the same predicate, counted. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013G3t66QwKJFK5w8jXxMXP2 * Cost-debt rows outside the required gate are withheld from the staleness join, route-gap expectations honour cost-debt withholding, and emit_on_demand_classical_not_native_one_build_holds moves to the cost-debt roster — it is budget-refused before it reaches the host effect its route-gap enrollment expects, on both hosts Measured on the first complete gate-bounded fold (srv2 lane 10 and CI at e8effe8, identical): verdict=FloorRefused with unexpected_failures=0 — no claim inside the gate fails — and two bookkeeping refusals: 122 STALE-COST-DEBT rows, every one in a module the gate never loads, and one STALE-ROUTE-GAP row whose claim ran past its CPU ceiling before reaching the effect. The first is the same out-of-scope population the expected-red and route-gap joins already withhold, now counted the same way. The second is a real cost debt (floor_cost_debt already records this claim at 502 -> 2374 ms), and cost debt wins over route-gap enrollment by the roster's own rule; the expectations decode now treats a cost-debt-withheld identity as dormant rather than absent. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013G3t66QwKJFK5w8jXxMXP2 * Two lens_module_gate_witness rows leave the expected-red roster: under the gate-bounded subject both PASS on CI and on srv2, and the floor refuses a passing enrollment as STALE-QUARANTINE Measured at 1f4bda9 (CI) and srv2 lane 12: verdict=FloorRefused with unexpected_failures=0 and exactly these two STALE-QUARANTINE rows on CI. Both are "live" claims whose question ranges over the loaded corpus; under the gate closure that corpus is 2,021 modules rather than 4,260, and the population they were red on is outside it. That is a narrowing of what the claim observes, stated here rather than hidden: the whole-corpus receipts run is where the wider question is asked again. srv2 additionally passes four emit_host_* rows that stay red on the required host; those stay enrolled — CI is the oracle for the required gate. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013G3t66QwKJFK5w8jXxMXP2 * Eleven claims interrupted before verdict on the gate-bounded subject join the cost-debt roster as proven chunk 12 — the same eleven on the GitHub runner and on srv2, run after run At 92cc92e the floor reports verdict=FloorRefused with unexpected_failures=0, no stale rows, no now-passing rows, and eleven INTERRUPTED-BEFORE-VERDICT identities (cost_coverage_witness x3, loaded_carrier_receipts x3, lens_closure_question_zero_holds_live, green_control_sanctioned_reader_body_not_flagged, same_grammar_parse_ingest_bridge_holds, kotlin_grammar_parse_accepted, nominal_distinct_control_compiles_ok). The set is identical at e8effe8 and 1f4bda9 on CI and in srv2 lane 12, so it is a property of the subject, not of host load: on the gate closure these claims first-touch artifacts the whole-tree fold had warmed before reaching them. Declared here as the roster's own containment for a cost the ceiling cannot hold; the exit is the warm, as the roster's header states. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013G3t66QwKJFK5w8jXxMXP2 * lens_module_gate_holds_live joins cost-debt chunk 12: it was interrupted at 1076ms the run after its sibling was withheld, because the 1.07s pool-root module_path_index fill is billed to whichever consumer runs first CI 0829ad8: verdict=FloorRefused, unexpected_failures=0, one INTERRUPTED-BEFORE-VERDICT row. The claim-cost receipt reads budget_interrupted 1076ms for it and `[floor-shared-fill] cache=module_path_index key=.../src/v2/lens fill_ms=1070 paid_by=...lens_module_gate_holds_live consumer_claims=1`; at 92cc92e the same fill was paid by lens_closure_question_zero_holds_live (consumer_claims=2) and this claim passed. The index is keyed on a pool root the decl_facts seam asks for at claim time, so preparation cannot warm it ahead; with both consumers withheld nothing pays it. The roster's own header names the warm as the exit. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013G3t66QwKJFK5w8jXxMXP2 * The pool-root module_path_index for src/v2/lens is warmed in preparation by evaluating the declared producer once in its own module's scope — the 1.07s fill was a positional bill that interrupted a different lens_module_gate_witness live claim in each of three consecutive runs — and the two fill-only rows leave cost-debt chunk 12 CI 92cc92e, 0829ad8, 154fb1f: each run's single INTERRUPTED-BEFORE-VERDICT row was the next `lens_module_gate_witness` live claim in evaluation order, at 1068–1252ms, with the claim-cost receipt and `[floor-shared-fill] cache=module_path_index key=.../src/v2/lens` naming that claim as the payer. The witness-roots warm cannot reach a per-pool-root key; this warm evaluates `v2.lens.registry.completeness.lens_registry_completeness_live_facts` in that module's frame, so the root comes from `lens_registry_completeness_pool_roots` and the key is the consumers' by construction. Adjudicated with the other preparation warms as `ModulePathIndexBuild/lens-pool-roots`; skipped (printed) when the subject does not carry the producer; a producer that fails to evaluate refuses. The two rows whose entire cost was this fill leave chunk 12, as the roster header says they must once the warm exists. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013G3t66QwKJFK5w8jXxMXP2 * lens_closure_question_zero_holds_live leaves the expected-red roster: with the src/v2/lens pool-root index warmed in preparation it passes, as its two siblings did once they stopped paying that fill srv2 lane 13 at 8ad4091: `[floor-shared-fill] cache=module_path_index key=.../src/v2/lens paid_by=<outside-fold> consumer_claims=3`, no lens claim interrupted, and STALE-QUARANTINE for this row — the same row that was red only while it paid the fill (CI 92cc92e). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013G3t66QwKJFK5w8jXxMXP2 * The four bootstrap_footprint_anchor claims join cost-debt chunk 12: 474–505ms CPU on three consecutive CI runs with no fill billed to them, so the 500ms ceiling decides them run by run CI f462bc9: planned=executed=2834, passed=2754, known_red_held=27, failed=0, no stale rows, interrupted_before_verdict=4 — these four, at 502–505ms. At 154fb1f the same four completed at 487–504ms and at 0829ad8 at 474–485ms; the run-to-run spread is the runner slot, not the claim. The gate did not change their cost — nothing in the shared-fill attribution names them — so the disposition is the roster's, not a ceiling change: withheld as declared debt until the host-load row lands. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013G3t66QwKJFK5w8jXxMXP2 * The rust-unit-tests job runs the unit population: the lib tests that prepare or build over the live tree carry a live-corpus ignore reason and leave the required run, and the rot the first-ever `cargo test` exposed is repaired at its authorities, not hidden `cargo test -p v1-compiler --lib` had never run in CI. Its first run (33238828500) was cancelled by its own 60-minute timeout with 204 of 682 tests finished, because ~126 of the "unit" tests each build a fresh multi-entry index over `src/v2`+`dag` (4,260 modules; ~197 single-thread minutes on srv2 under nextest, 97 tests over 60 s, `self_compile_all_modules` alone 505 s), and the runner executes them serially. Those tests now carry `#[ignore = "live-corpus: ..."]` — the crate's existing `manual:` convention, one class, declared on the carrier — and the rung-drop row `required_gate_bankruptcy` names them by their instrument (`cargo test -p v1-compiler --lib -- --ignored --list`). The unit population runs in ~10 s after the compile (srv2: 537 passed / 136 ignored). Of the 44 failures the full run exposed, the 15 in the unit population are repaired where the fact lives: - REAL DEFECTS (two): `try_index_source_root_into_module_index` keyed files by their walked path, absolute since #9548 anchored the root, while the strict builder keys through `module_index_path_key` — the primary-precedence index disagreed with the strict one on every path; keyed through the same authority now. `try_build_module_index` carried `if root_idx > 0 { continue; }` before its collision refusal (from #7791), so a module declared in two roots shadowed silently in the builder named strict; the guard is gone and overlay callers have `build_module_index_primary_precedence`. - v1 TYPECHECK DEFECT: `declared_type_inhabitance` reads `params` as generic type parameters, which is exactly what a callable formal carries, so every higher-order call produced a counted advisory with a false reason (#9194); `direct_call_argument_inhabitance_diags` now excludes callable formals like its sibling `direct_call_arg_type_mismatch`. Mirror regenerated (two passes: the test blob lives inside the emitter). - STALE AUTHORITY ROWS after the #9637 reorg: 12 entry literals in `gunbc.ci_layer_roots` and 2 in `gunbc.offline_local_recipe` repointed; the two long-lane rows and one freeze row whose subjects 611fd02 and #9206 deleted are gone; the three freeze rows for relocated witnesses are DELETED rather than repointed, because the freeze gate defines relocation as growth and the roster may only shrink. `gunbc.non_fold_residue` receives the 22 sites it lacked and loses the 4 whose subjects moved or greened; its .dag twin therefore leaves floor_expected_red (it passes) and joins cost-debt chunk 12 (629 ms against the 500 ms ceiling, its whole cost the corpus scan it checks). - DELETED SUBJECTS: `cli_run::floor_witness_a_prove` (its runner, prove test and fixtures went with the FLOOR-Y cutover); the census pin tests and helpers for `docs/probes/census_extra_excludes.txt` (#9132 deleted every transcription). - EARLY ABORTS: three witness-admission tests and the roadmap jsonl-carrier test were "fast" only because they failed before their expensive step; with their inputs repaired they read the live tree for 2-4 minutes each and join the live-corpus class. - TEST ROT: the reorg rewrote a revision-addressed literal (`9ce6526c528:dag/gunbc/roadmap/...`) that must name the pre-reorg path; the method-existence witness anchored on a `Primitive()` row the frontier no longer holds. Not done here, receipts-lane rot for follow-ups: `test.claim.expectation_frontier_witness_test` names the deleted long-lane file; the affected-set kernel (`floor_diff_edits_from_diff_text`, `rerun_frontier_nodes_for_entry`, …) has no production consumer since FLOOR-Y and should go with its remaining fixture-dependent tests; the roadmap jsonl-carrier test takes 453 s and fails after its expensive step. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013G3t66QwKJFK5w8jXxMXP2 * The host-tool probe root carries the process id: temp_dir() is the host's shared /tmp on a self-hosted runner, and a fixed directory name collided with one another runner slot's uid left behind — PermissionDenied on two tests that had never run in CI before Found by the first green-by-duration run of the unit population (dc3ca52: 533 passed, 2 failed, 9.59s). The same class as the shared-/tmp emit_on_demand collision on srv2: a test that writes a fixed path into a location the process does not own. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013G3t66QwKJFK5w8jXxMXP2 --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Auto-opened by session-dashboard for session
loyal-lynx-169.Pushing to
adopt/9007-directcalladvances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan
The wall found two live defects on its first outing
Not authored as part of the carrier — exposed by it, on the list-element seam, and both are the
same class: a
ContentHashfamily member standing where the union is declared, or thereverse. DESIGN §3's convergence thread is explicit that these are different types and that
conflating them re-opens the cross-family comparison that row exists to close.
gunbc.heal_revalidationclassify_heal_revalidation_admission/heal_revalidation_admitsrequired_roster: Fnv1a64Structural,required_gates: List<Fnv1a64Structural>ContentHash/List<ContentHash>v2.workflow.native_cache_fusionfusion_agreement_holds_forcontent_hash_atom(...)passed directly as aContentHashkeyas_content_hash_structuralThe second is the list-element position specifically:
content_hash_atomreturns the structuralfamily member, and the declared key is the union, so the coercion was never stated. Both compiled
before this PR and neither was reachable by any existing check.
This is the argument for the wall that no amount of internal-consistency review can supply: a check
whose first execution finds live defects in code nobody was suspicious of is demonstrating
discrimination rather than restating a type. Neither defect was found by reading — both surfaced as
refusals from the new obligation relation.
Observed in CI on this branch, and NOT from this change
Run
32884947431(against the superseded head, before the mirror regeneration) reported oneline unrelated to anything here, recorded so a reviewer does not attribute it to this PR:
It touches no file in this diff. It is worth someone's attention on its own terms rather than
mine: an enrollment asserts an expected verdict, and a claim that threw produced none — so the
row is currently documenting a red it never measured. Being routed for an owner separately.
That run's only failing phase was
regen, which is the mirror drift this branch now fixes(
phases_run=4 failed=1,FAILED PHASE regen).Note for whoever writes the squash message: the shipped repair count is 3, not 17
Branch history contains a commit titled "The 17 repairs the wall forces" (
d4b0e524065). It issuperseded by the very next commit,
3106d524450— "8876's repair shape does NOT apply tothese 16 sites — reverting the wrap, keeping the one repair that was real". The history is
self-consistent, but the retraction is easy to miss, and a review of this PR has already quoted the
17 as though it described the diff.
What actually ships, all caller-side:
dag/gunbc/heal_revalidation.dagFnv1a64Structural→ContentHashsrc/v2/workflow/native_cache_fusion.dagas_content_hash_structuralliftsrc/v2/workflow/dag_acceptance.dagno_rows()→no_obligations()floor_expected_red.dagis enrollment, not a repair. Squashing the branch flattens the retractioninto the same message as the claim, so stating the net here keeps a superseded count from being
read later as this change's receipt.
The generated-artifact merge driver did not fire here, twice
Recorded because a gap that keeps being paid silently never gets prioritised, and this PR paid it
twice on its own.
src/v1/stage0/src/v1_compiler_infer.rsis a generated mirror. On both merges into this branch gitleft ordinary conflict markers and would have happily accepted a hand-resolution — which is
exactly how this PR lost #9192's mirror content the first time round: clean tree, no markers, and a
committed seed that was an older compiler than the
.dagit claimed to mirror.The driver is working where it is enrolled. On #9196 the same mechanism refused a generated
.yml, left the path unmerged, and printed the regeneration recipe. The difference is enrolment,not behaviour: it is enrolled by BASENAME while the population it should cover is defined by a
HEADER, so it protects 2 of 136 stage0 mirrors and
v1_compiler_infer.rsfalls outside.Not fixed here — it is not this PR's subject, and enrolling 136 mirrors is its own change with its
own blast radius. Named so it is costed rather than rediscovered.
Binary vintage changed the drift list, and that is worth carrying
The regeneration was run twice, and the two runs disagree on the same tree:
f57bc0ec(pre-merge)extdeps_uri.rs,v1_compiler_compile.rs,v1_compiler_infer.rs,v1_rt.rs— 4v1_compiler_infer.rs— 1Three of the four were emitter vintage, not tree drift: this diff touches inference and has
nothing to do with
extdeps_uri.rsorv1_rt.rs. Installing the first candidate would have writtenan old emitter's bytes over mirrors main had already advanced — silently, and it would have read as
a successful regen.
A drift list wider than your change is a claim about your instrument. The driver recipe's order
("regenerate → install → rebuild → verify again") assumes a current binary; when the binary
predates the merge the correct order is rebuild first, then regenerate once. The binary was
dated before being trusted: it now accepts
--required-laneand routes phases by lane, which thepre-merge one rejected outright.
Receipts
Byte grain, not just the flag: installed
sha256 12110f0a3dc440ef…was recorded before theconfirming run and re-emitted identically by a binary rebuilt from the installed seed;
diff -rqover the candidate tree shows no other file differing. The three #9192 functions remain 1/1
dag-to-rs.