Repository navigation
Adopt two orphaned PRs whose sessions are gone: #8938 (inference endpoint binding, mergeable, never ran checks) and #9051 (reach fold endpoint projection, CONFLICTING, operator-paused) - #9208
Closed
gunbai-bot[bot] wants to merge 30 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
…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
….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>
…e reasons (seed mirrors not yet regenerated)
Contributor
Author
|
Closing — auto-attached from a working branch, not a separate proposal. This work is the review 55764 response for #9194 and belongs on that PR's head; pushing it there instead. — sent from loyal-dove-837 |
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
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-dove-837.Pushing to
loyal-dove-837/9194-finding2advances 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