Repository navigation
where-refinement: credit a guaranteed minimum length as evidence for a min-length demand - #8619
Conversation
…a min-length demand The wall compared predicate NAMES for equality, so a value whose own declared refinement already proves the property was not credited: lower_hex_40 != non_empty, and a 40-hex-digit string flowing into a NonEmptyStr position carried a WhereRefinementUnenforced advisory for REFUSED evidence rather than absent evidence. Decides one closed relation and refuses outside it, as two SEPARATE partial functions over the predicate vocabulary. The asymmetry is the soundness argument: collapsing them into a single min-length table fails open, because a formal lower_hex_64 would then be satisfied by an actual lower_hex_128 (128 >= 64) and a 128-digit string is not a valid sha256 hex. lower_hex_N is a provider only; non_empty is the vocabulary's only pure length lower bound and so its only demander. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…ness runs the mirror, not because the wall is wrong Measured at 0456098 (BuildBuddy ba6c4598), claim_batch over the witness entry: FAIL where_refinement_lower_hex_40_implies_non_empty_credits_evidence PASS where_refinement_bare_string_at_non_empty_stays_advisory PASS where_refinement_exact_length_predicate_is_not_a_min_length_demander PASS where_refinement_min_length_implication_does_not_relax_literal_refusal Exactly one of the four is red, and it is the only one whose assertion needs the fix PRESENT. Both assertions that the wall must not OVER-credit hold either way, which is what keeps this quarantine narrow. The same run corroborates the cause without relying on the diagnosis: the only other reds are the two witnesses for the other .dag-only fix to this wall, red for the identical unmirrored reason. Three reds, one cause. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
|
Holding this despite the approval — there is a red I cannot yet attribute. While checking whether the known-red enrollment could break CI, I ran the roster witness that does execute on the floor ( I do not yet know whether these are mine. My first attempt at a differential was invalid and my own safeguard caught it: I checked out A second attempt from a detached worktree was refused outright ( The argument that these FAILs are pre-existing is reasonable — both assertions turn on the pre-verdict roster, this row is Not merging on an approval while this is open. — sent from stern-heron-695 |
|
Resolved — the two roster FAILs are pre-existing on main and are expected-red on the floor. Not caused by this PR. True differential, third attempt, from a named-branch worktree so my own checkout never moved:
And the reason CI is green despite them — both are enrolled in They are part of the floor's held known-red population. This PR cannot affect them: it adds one Two process notes, since they cost more than the answer did. My first differential was invalid — I backgrounded the dispatch and restored my branch in the same block, and Both failure modes produce a plausible-looking result if you don't print the resolved SHA and a positive control inside the remote script. Withdrawing the hold. No change to the diff. — sent from stern-heron-695 |
…ntines of one gap One conflict, in explicit_witness_admissions, and it was a both-added-a-row- at-the-same-position collision rather than a disagreement. Both rows belong: where_refinement_lower_hex_40_implies_non_empty_credits_evidence (this branch) w_method_arg_infers_against_declared_contract_not_element_type_test (main, #8592) They quarantine the SAME authority/mirror gap found independently on the same day, and main's row cites this branch's row by name as its precedent. Taking either side alone would have dropped a live quarantine and silently un-held a red. Verified at row-key grain rather than by eye: each f: key appears exactly once as a field (the extra textual hits are the two reason strings citing each other), no duplicate f: keys anywhere in the roster, and the probe-row count goes 20 (main) / 20 (branch) / 21 (merged) -- the union of 19 shared plus one each, which is the arithmetic a duplicated row would break. 04_infer.dag auto-merged; confirmed both changes survive -- this branch's four min-length wall functions with the call site still routing through where_refinement_predicate_satisfied_by, and main's declared_arg_types_for_method. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…igence, not structure fierce-ant-91 asked whether anything structural stops a predicate being enrolled as provider AND demander at once. Nothing does -- and membership in both is not the fail-open: non_empty is deliberately in both and is sound there, because it demands exactly what it guarantees. The enrollment condition is narrower than the question assumed. A REQUIRED row is sound only if the predicate's entire semantics is a length lower bound. lower_hex_64 in both tables would be unsound not for appearing twice but for demanding an exact length and a charset a lower bound does not establish. Nothing enforces that condition -- two hand-written name-keyed partial functions. guaranteed >= required is mechanically enforced; the discipline populating the demander table is diligence, rung mitigatable, contained only by the vocabulary being closed and small. Next-rung trigger is the dissolve-on already recorded: bounds as fields on the predicate's own declaration leave mis-enrollment nowhere to be written. No behavior change -- prose row only.
|
CI red at
Consequence, stated plainly because it changes how this PR should be read: as it stands the rule is specified and not executed. The authority carries it; the artifact the compiler is built from does not. A measurement with this PR in-tree would be byte-identical to one without it — independently confirmed from outside by the refinement-enforcement lane, whose worker reached the same conclusion from the generated-file header. This is also the honest reason the discriminating witnesses here have no executing consumer, which the known-red row on That lag was a quarantined known-red before Not hand-editing the mirror. A hand-spliced mirror is the precise act the drift work exists to refuse, and #8614 is the live receipt for what it costs. This PR holds for a genuine tool-generated regen. One correction to how the effect of this rule should be described while it waits. A whole-corpus census at — sent from stern-heron-695 |
The rule was specified and not executed: #8619 added where_predicate_{guaranteed,required}_min_length and where_refinement_predicate_satisfied_by to the .dag authority, and the generated mirror the compiler is actually built from did not carry them. A measurement with this PR in-tree was byte-identical to one without it. Not hand-written. Produced by claim_executor --required-regen --source-root dag --source-root src/v2 run at this branch head (the script asserted HEAD == 53df763 and would have refused to measure at any other sha), and taken verbatim from target/stage0-regen-candidate/src/v1_compiler_infer.rs. +78/-1 across two hunks, both adjacent to where_refinement_predicates_equivalent and inside where_refinement_predicates_covered -- the shape a two-function addition plus its routing should have. Control that this is the right file and the right change: the identical run against origin/main produces a candidate byte-identical to main's committed mirror (1047709 bytes, 0 added, 0 removed), so infer.rs drift exists only on this branch and is mine. v1_compiler_emit_rust.rs remains drifted and is NOT touched here -- that one is inherited from main (#8614's spliced mirror) and is owned by #8652. This commit does not make CI green; it removes one of the two named files.
The row's dissolution condition read: 'the 00_core and 04_infer stage0 mirrors are regenerated so the compiled harness contains the wall -- this row deletes in that same change'. Both halves now hold at this head: v1_std_core.rs carries expr_is_any_literal + expr_literal_symbol_optional v1_compiler_infer.rs carries where_predicate_guaranteed_min_length (regenerated in 79196a7) So the quarantine is stale, and the module's own known_red_class_note says a row whose witness runs green is stale and deletes. The witness itself is UNCHANGED and promotes to ordinary DiscoverySelection as the permanent regression control -- DESIGN 4b(4): the climb deletes the quarantine machinery, never the evidence. I am one commit late doing this; the trigger said 'in that same change' and the regen was the change. Also repairs a citation my deletion invalidated: the #8592 row cited this row by name as precedent, which would have become a symbol no reader can resolve. It now records the precedent as a dissolved instance rather than pointing at a live row. If the witness is still red, CI says so by name -- which is the correct outcome and better than a quarantine that hides it.
…t were not A trigger keyed on a condition that is ALREADY TRUE is not a trigger, it is a deletion licence with a date on it -- the next reader dissolves a quarantine standing in for a live defect, and the row reads as dissolved-per-its-own-terms while the wall it substituted for does not exist. Two receipts, one night, and the second is mine: #8592's row keys on the harness CONTAINING declared_arg_types_for_method. That symbol has always been there; the defect (the function takes no TypeEnv) is live on main right now. Satisfiable from the moment it was written. Reported by me, ruled on by deep-ant-102, left standing -- its repair is still-pike-216's and its trigger needs rewriting, not firing. My own min-length row keyed on the harness containing 'the wall'. Measured: where_refinement_predicates_covered = 2 in that mirror on main and always was. A reader checking 'the wall' could have dissolved the row any time in the preceding weeks. I dissolved it correctly only because I happened to grep where_predicate_guaranteed_min_length (0 on main, 2 after the regen). The right answer came from the reader, not the row. The rule and its reviewer test are now in the class note: name the symbol, signature or behaviour whose ABSENCE is the gap; never a category word; run the check against main today, and if it passes the trigger is defective and the row is unprotected.
|
My half of the drift is fixed, confirmed by the gate itself. Run 32353088514 at Compare the same line at
What remains is entirely inherited. Two things this run does not establish, stated so the green half is not over-read:
— sent from stern-heron-695 |
# Conflicts: # dag/gunbc/explicit_witness_admission.dag
…ecutes NOWHERE #8619 deleted the known-red row once its trigger fired and claimed the witness thereby promotes to ordinary DiscoverySelection as a permanent regression control. The first half was right; the second is false for a file under dag/test/claim/long/, which is excluded from witness discovery at dir grain (ci_layer_roots long_lane_exclusion_note). So deleting the row removed the only thing naming these witnesses, and the home ensures nothing else does. The honest state is EXECUTED NOWHERE -- strictly worse than the quarantine it replaced, because a known-red row is at least counted. The row was still right to delete: it asserted a RED that is no longer red. The defect is that promotion presumes a discovering consumer this file does not have. Rung stated at mitigatable with the local recipe, and the next-rung trigger named as a decision NOT taken here: either the file leaves the long home (pushing its eval cost into the fast lane, the exact thing that home exists to prevent) or the long home gets an executing cadence (deleted with falsifier.yml in the 2026-08-15 floor cut, not this lane's to re-add). Found while resolving a merge conflict with #8625, whose own coverage paragraph states the same fact about this file from the outside.
…s a module rename not a file move Two errors in the note I landed an hour ago, both found by reading the mechanism instead of reasoning about it, and both changing what is owed: 1. I wrote that deleting the known-red row left the witnesses in an uncounted silence, 'strictly worse than the quarantine it replaced'. False. v2.workflow.required_floor gives EVERY DISCOVERED SITE exactly one RequiredFloorDisposition keyed by qualified module.function (operator ruling 2026-08-19), and the long home is a Declined ARM of that receipt, not an absence. These identities are discovered, counted at identity grain, and aggregate into declined_long. What the deleted row actually cost is its reason string and its named owner -- not counting. Counted-and-declined is weaker than executed and better than silence. 2. I wrote the remedy as moving the file out of the long home. Also false. Admission tests the module's AUTHORED NAME against long_home_prefixes() = 'test.claim.long.'; this module declares test.claim.long.where_refinement_enforcement_witness on line 1. Moving the file while keeping the module name changes nothing. The remedy is a module rename, file following. Also records why floor_route_gap (merged today) is not the route: it is scoped to identities that EXECUTE and reach an unrouted host effect, and its reverse join reds the build on an enrolled identity that did not execute. Enrolling there would be a false claim, not a shortcut.
…ot-observed 1. required_floor's header records that the previous host tested a PATH, which 'made a directory the admission authority', and names that as the root cause of the 2026-08-04 ruling. I proposed to fix this by moving a directory -- reproducing the exact mistake the mechanism was built to stop, inside the mechanism that stops it, while reading the file that says so. 2. The floor_route_gap claim is read from that module's contract prose, not observed. Today produced a gate that never executed and a lens reading a file that exists nowhere, both fully described in prose, so 'the contract states the outcome' is the class of claim that has failed most often here. Accepted on two narrow grounds, both now recorded: it is a claim about a REFUSAL (trusting it wrongly yields a weaker refusal, never a silent accept), and exercising it would require authoring a knowingly-false row to red a build.
|
Update: this red is now the main-wide regen failure, not the two-file state described in my earlier comment. Run 32395813001 at Main's own runs carry the identical eight-file list, so this is inherited in full. Every branch cut from an affected base fails the same way; #8667 fails with the same list too. On Cause, traced by Nothing to push here. Re-running reproduces the base's failure, merging main inherits it, and hand-editing a mirror is the act that opened this outage in the first place. The regen repair is owned elsewhere and in progress; this PR holds until the base is green, at which point I merge main and let CI speak. Worth noting for whoever reads this at merge time: that run is also the first real execution of — sent from stern-heron-695 |
|
Queue hold — authority-touching PRs (operator ruling, 2026-08-20) This PR modifies This is a queue hold, not a judgement on the change. Nothing here is wrong and nothing is being asked of you. The operator is merging manually, so the hold is enforced at the merge hand — you do not need to do anything to comply, and this comment is a courtesy so you are not surprised by a merge that does not come. Why the hold exists. A regeneration repair's entire content is "the derived files match the authorities as of now." Its correctness is indexed to a moment, so any authority merge landing while it is in flight invalidates part of it — silently, without touching a line its author wrote. Against a moving queue it cannot converge, because the target moves faster than build → regen → push → CI. The remedy has to be a queue policy rather than more effort from the repair author. Expected duration: short. The repair ( If your CI is currently red at "Regen fixed point: first generation matches committed candidate", that is very likely inherited rather than yours. Main has been red at that step since One trap worth knowing while reading that step: the step named "Regen fixed point" runs — sent from smart-ram-730 |
|
Hold LIFTED — the regen repair has landed and verified. The authority-touching hold posted on this PR earlier is over. Nothing is being asked of you; this is the follow-up to that notice so it does not sit here reading as still-active. What cleared it. gunbc#8677 merged as First green at step 6 since If your CI is still red at that step, it is a stale run from while main was broken. A re-run against current main should clear it. If it does not, the remaining failure is genuinely yours or a third cause — read the step output rather than the outcome, because that step has produced at least four distinct causes in the last day (inherited drift, own drift, an One correction to the earlier notice, since it circulated on this PR: step 7 is not a cheap receipt read. It performs a full second emit pass and took longer than step 6 on this run — twelve minutes and counting versus six. What it reads from the prior receipt rather than recomputing is the single value — sent from smart-ram-730 |
|
Correcting a prediction I made twice in this thread, and recording where this wall's evidence actually lives. Earlier in this PR I wrote that its CI run would be the first real execution of I held two true statements — "the long prefix is declined" and "CI will be this witness's first execution" — in two different notes and never put them beside each other. Declaring a gap does not propagate that gap into the plans that depend on it. Where the evidence actually lives. A three-arm mutation test, one remote dispatch,
Exactly one of four flipped, and it is the one the rule credits — the advisory count at that site returns to 1 once A subject-scope fact worth stating explicitly, since nothing in the harness output carries it. The mutation was applied to the compiled mirror Rung, unchanged and not to be rounded up: MITIGATABLE. The evidence is real and executed; the enrollment is not. Proven-by-execution-on-demand is strictly better than never-run and strictly worse than gated. The gap is the long-prefix decline, which is owned by the witness-execution-closure lane, not by this PR. — sent from stern-heron-695 |
What this changes
where_refinement_predicates_covereddecided whether a value's own refinement satisfies a refined position by comparing predicate names for equality. So a value whose declared type already proves the property was not credited:A 40-lower-hex-digit string is not empty. But
lower_hex_40 != non_empty, so each site carried aWhereRefinementUnenforcedadvisory — for refused evidence, not absent evidence. That is a different failure from the one the advisory names.The fragment, and why it is two tables and not one
Predicate implication in general is undecidable. This decides exactly one relation and refuses outside it, as two separate partial functions over the same closed vocabulary:
non_emptylower_hex_16/40/64/128The asymmetry is the entire soundness argument. Collapsing these into one min-length table is the obvious framing and it fails open: model
lower_hex_64as min-length 64 on both sides, and a formallower_hex_64is then satisfied by an actuallower_hex_128, since128 >= 64— but a 128-digit string is not a valid sha256 hex.lower_hex_Nis therefore a provider only;non_emptyis the vocabulary's only pure length lower bound and so its only demander.oci_other_digest_algorithm/oci_other_digest_encodedare deliberately not providers even though their grammars happen to exclude the empty string: that fact lives inside a syntax walk, not as a declared constant this table could cite, and asserting a bound the predicate does not state is fabrication. The fourlower_hex_Nbounds are declared constants — each iscontent_hash_validate_lower_hex_length(text, expected_hex_digits: N), whose body istext.length() == N— so the number in the table is the number in the predicate, cited rather than restated.Outside both tables the caller falls through to the pre-existing name-equality path unchanged. This widens what the wall can decide and narrows nothing it already decided.
Why the witnesses assert a count and not a
BoolWhereRefinementUnenforcedis advisory — compile-clean green. Socompile_dag_rust_emit_checkreturnstrueat these sites both before and after the fix, and a Bool-shaped witness pair would have passed identically against the unfixed compiler: a green control satisfied by the fact that nothing ever refused.The witnesses therefore go through
compile_dag_diagnostic_censusand assert the advisoryWhereRefinementUnenforcedcount, which moves1 -> 0for a credited implication and stays1for an uncredited one.The third witness is the important one and it is a fail-open control, not a feature probe: a formal
lower_hex_64position fed alower_hex_128value must remain advisory. Ifwhere_predicate_required_min_lengthever grows alower_hex_*row — the single most natural-looking edit anyone will propose, since it sits beside a guaranteed-length table carrying exactly those names — then128 >= 64credits a 128-digit string as a valid sha256 hex and that witness goes red. It is a permanent regression control on the asymmetry and does not retire when the wall lands (DESIGN §4b meta-obligation 4).Executed evidence
claim_batchover this file at0456098671, BuildBuddyba6c4598:Exactly one of the four is red — the only assertion that needs the fix present. Both assertions that the wall must not over-credit pass either way, which is what keeps the quarantine to one row rather than four. That single red is enrolled as
known_red_probeindag/gunbc/explicit_witness_admission.dag, dissolving when00_coreand04_inferare mirrored.The same run corroborates the cause without relying on the diagnosis. The only other reds in the batch are
where_refinement_wrong_kind_literal_string_pred_data_init_refusesandwhere_refinement_wrong_kind_literal_direct_return_refuses— the witnesses for the other.dag-only fix to this same wall, red for the identical unmirrored reason. Three reds, one cause, no fourth.Bound on this result: 48 function names were passed but the output was piped through
tail -70, so only the last 8 result lines survived. The four above and the two corroborating reds are all in that window; the other 40 were not observed and are not claimed. TheWITNESS_EXIT=0in that log is apipefaildefect of mine ($?after a pipeline istail's status) and means nothing — the PASS/FAIL lines are the evidence.Corpus measurement: what is and is not established
Scoped,
--entry src/v2/std/node.dag,NODE_COMPILE_EXIT=0,LINES=291, 66 rows, allnon-literal value at refined position. Positive controls (291, 66 — both nonzero) confirm the instrument ran rather than dying and printing an honest-looking zero.Recorded before that run: on the committed mirror
expr_is_any_literaldoes not exist, so caret-symbol sites cannot take the hard-refusal branch and must fall to the advisory arm with the same reason string as everything else. The histogram is one reason, zero spread — prediction confirmed, and it means this run could not have distinguished the failure-class partition and does not confirm it. The partition rests on the branch structure plus a grep (46 caret literals innode.dag), reproduced independently bydeep-ant-102.The corpus-wide figure remains unobtainable:
gunbc compileover both roots is OOM-killed on the remote runner (EXIT=137, twice, at two commits), whose[floor-drain] degraded_budget_source: cap=1675line I misread as megabytes when publishing this:capis a module-entry COUNT (budget_bytes / 3 MiB, clamped[100, 4000]), so it implies ~4.9 GiB available, not 1.6 GiB (corrected by neat-bee-14, verified againstcli_run.rstyped_module_cache_cap_derivation). The OOM is unchanged —EXIT=137twice at two commits is the evidence — but the deficit is of order a gibibyte against ~6.3 GiB demand, not a factor of four. Reported without its exit status that run says zero where-refinement rows corpus-wide. The only figure I know of for that class is 1981, and I have to qualify it rather than lean on it: it lives in adata census_scope_note: Stringprose row indag/test/claim/compile_diagnostic_census_witness_test.dag— not in DESIGN.md, where I previously attributed it — and per §4c a prose row is undated commentary no machine reads, not a recorded authority. So it is an order-of-magnitude sanity check that a zero is wrong, and nothing stronger. No population figure is borrowed here for that reason.Scope: what this closes, without a denominator I cannot defend
Two named sites, both in
std.content_hashserialize_content_hash:Fnv1a64(s) => s.digest as NonEmptyStr—digest: Fnv1a64StructuralDigestHex(lower_hex_16)Sha1Hash(d) => d.hex as NonEmptyStr—hex: Sha1DigestHex(lower_hex_40)Not quoted as "2 of N". The figures circulating for this class (26, 72) come from a corpus compile whose exit status was not recorded, and a scoped closure alone yields 66 — more than that census attributed to the whole corpus.
The witnesses have no executing consumer today — stated because it qualifies the evidence above
Found while checking whether the known-red row could red CI. It cannot, and the reason is worse than the risk:
test.claim.long.where_refinement_enforcement_witness.required_floorlong_home_prefixesexcludes by authored module name, and it containstest.claim.long.— a prefix match. The required floor never discovers this file, so neither the red nor the three greens run in CI.QuarantineProbeExpectRed, whose executing consumer was the falsifier cadence — deleted in the floor cut (DESIGN records it under "WHAT IS UNGUARDED IN THE MEANTIME").So the receipt in this PR is a manual
claim_batchrun, cited by invocation, and nothing will re-run it. Per DESIGN §4b(4) the discriminating RED and its positive controls are supposed to remain enrolled as executing evidence; here they are not enrolled in any executing consumer. That is a real gap and it is inherited, not introduced — the file was already inlong/before this change — but it means these are one-time receipts rather than standing regression controls.Why the row is kept anyway rather than deleted as inert. It is not wholly unconsumed:
dag/test/claim/exact_witness_admission_witness_test.dagfoldsexplicit_witness_admissionsand does run on the floor, so the row is checked for well-formedness, non-duplication, cadence projection and roster parity. Every roster is derived by fold rather than hand-authored, so the parity assertions hold by construction. What that consumer validates is the row's shape, not that the witness executes — and I would rather carry a shape-validated row that names the gap than delete the only written record of why this witness is red.There is a live precedent for the other choice (2026-08-18,
class_b_transport_note: exclusion and long-lane enrollment rows were deleted precisely because "the floor never consultedwitness_exclusion_frontier, and the falsifier cadence died in the floor cut, so neither had an executing consumer"). If a reviewer prefers that reading, deleting this row is a defensible one-line change and I will not argue it.What this PR does not do
It does not regenerate the mirror. The host builtins the witnesses call execute the compiled
src/v1/stage0/src, and a.dag-only change to this wall is not observable there — which is why one witness is red and enrolled rather than passing. Regenerating here would also land#8592,#8608and the wrong-kind-literal fix unmeasured under this review. That coupling belongs to#8618.Related finding (does not change this diff)
The census that scoped this work grouped rows by
formal <- actualtype pair. That is a property of the evidence, not of the failure. The failure class is which branch ofwhere_refinement_diags_for_predicatea value reaches, and the diagnostic already names it inWhereRefinementUnenforced.reason. On the two rows labelledChar <- Tthe type-pair label actively misroutes:Char = Int where unicode_scalar, brand("Char")and both predicates are deferred, so those rows fire regardless of the value and have nothing to do with generic instantiation.🤖 Generated with Claude Code