Repository navigation
The behavioral receipt reported DIVERGENT over a byte-identical file: measure instability instead of rendering it as a difference - #8743
Conversation
… measure instability instead of rendering it as a difference
`generate_receipt_driver` renders every derived call as `println!("... = {:?}", call)`, and a
mirror function returning `Rc<HashMap<..>>` renders in per-process randomized order. The seed and
candidate transcripts come from two separate driver processes, so a map-returning call is a coin
flip that the differential scores as a behavioural difference.
THE DISCRIMINATING OBSERVATION: on gunbc#8726's CI run, `required-regen` reported
`first_generation_equal=true` -- the emitted `std_algebra.rs` byte-identical to the committed
mirror -- and the receipt then installed that candidate over the mirror and reported DIVERGENT.
It compared a file against itself and could not answer EQUIVALENT. The printed `first_difference`
was `kernel_algebra_profile_value()` with the same seven entries in a different order.
MEASURED, not inferred: a one-line driver built against the committed `libv1_compiler.rlib`
printing that call through `{:?}`, run 20 times on an unchanged tree, produced 20 DISTINCT
transcripts. Two agreeing runs is the rare event, not the divergence.
This does not fail open. It fails WRONG, and nondeterministically -- the fabricated-difference
mirror of the fabricated-pass that `behavioral_differential`'s own dirty-tree refusal (review
54094) was hardened against.
WHY THE CHECK IS A SECOND RUN AND NOT A TYPE CHECK. The obvious fix is to refuse map-returning
functions at admission, at the function grain main moved to. It is the wrong instrument: order-
dependent rendering is a property of the value's TRANSITIVE shape, so a record CONTAINING a map
renders unstably while its own return type says `Record`, and `HashSet` has the property too. Any
check keying on the outermost constructor under-refuses BY CONSTRUCTION, and it under-refuses
silently -- the missed call lands in `Divergent`, indistinguishable from a real divergence. An
admission check also runs before anything has been rendered, so a proxy is all it could ever key on.
`run_receipt_driver` already builds the crate and compiles a driver binary. Running THAT SAME
BINARY a second time costs milliseconds -- no rebuild -- and two executions of one unchanged binary
that disagree PROVE the disagreeing call renders nondeterministically. The property itself, with
no type walk to keep in sync, catching `HashSet` and containing-record cases for free.
PLACEMENT: a verdict, not a `ReceiptExclusion`. The property is only knowable by RUNNING, and
selection happens before any run. That respects the boundary main's function-grain admission
draws rather than ignoring it.
WHAT LANDS
- `DriverTranscript { lines, unstable }`; `run_receipt_driver` runs the built binary twice.
- The differential unions BOTH sides' unstable sets (each side is its own binary, measured
independently) and compares only the lines proved stable.
- `Equivalent` carries `nondeterministic_calls` + the FUNCTION NAMES, because a green with an
excluded population is a different claim from a green over everything, and a name can be
acted on where a count cannot.
- `NondeterministicRendering` when every derived call is unstable: nothing was compared, so it
is neither equivalence nor divergence, and the fix lives in emission rather than in this gate
or in the diff under test.
- A counter printed EVERY run including zero, carrying its own FLOOR warning and its own
dissolution trigger.
THE COUNT IS A FLOOR AND THE LINE SAYS SO. Instability is proved by two runs disagreeing, so a
call whose randomized rendering happened to agree twice is not counted and is compared as if it
were deterministic. The warning is in the printed line rather than in a comment because the line
outlives the comment: someone will trend this number and read a small one as a nearly-closed
class. The residue SHRINKS with more executions, unlike a structural blind spot -- but one extra
run is what the evidence to date justifies, and speculatively adding more would be a threshold
nobody measured.
DISSOLUTION: the counter goes to zero when emission is deterministic (a `BTreeMap` container
template rather than `HashMap`), NOT when the probe gets better at spotting the residue. That
higher rung makes the nondeterminism unwritable rather than detected-and-excluded; this change is
the declared, counted, bounded reduction until then. Its blast radius --
`rust_container_templates` plus every `v1_rt` map signature -- is why it is not in this diff.
EVIDENCE BY EXECUTION
- `--behavioral-receipt-selftest` green: arm `preserving` EQUIVALENT over 12 derived calls,
arm `changing` DIVERGENT over 12 at the authored difference (`band_of(100i64) = High` vs
`Mid`). Both pre-existing controls still discriminate with the probe in place.
- The `preserving` arm is now ALSO a false-positive control: its fixture is deterministic, so
the probe must mark nothing unstable, and the arm fails loudly if it does. A probe that
marked everything would otherwise still print a green there while the gate had quietly
stopped comparing.
- Four unit tests over `DriverTranscript::of`, including one that PINS the residue: a
nondeterministic call that agreed twice is not caught. If someone makes the probe complete,
that test fails and forces the FLOOR wording to be revisited rather than left stale.
- MUTATION CONTROLS, both directions: flipping the length-difference branch to `false` reds
exactly `a_length_difference_marks_every_line`; flipping the line comparison from `a != b` to
`a == b` reds the other three. The tests are not vacuous.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…sage Review 54277's nit, and the way it was found matters more than the fix. The literal was authored with `\` line-continuations, which Rust strips along with the following indentation -- correct as written. `cargo fmt` then joined the continuation lines and kept the indentation as literal content, so the printed line carried two 25-space gaps. A regex over the source could not see it: the literal is one physical line with every continuation properly escaped, which is what I checked first and what came back clean. Compiling the exact literal and PRINTING it is what showed the gaps -- the same distinction this PR is about, that a rendering is a fact you measure rather than one you derive from the source. Swept the class rather than the site: every string literal in the file was checked for embedded space runs. One other hit, `FLOOR-COMPILE-CLEAN-OVER-BUDGET`, is pre-existing and not in this diff, so it is left alone. Selftest re-run after the change: arm preserving EQUIVALENT over 12 derived calls, arm changing DIVERGENT at the authored difference. Both arms still discriminate. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
End-to-end proof: the same tree, before and afterThis PR's own CI cannot produce this evidence. The receipt phase selects changed So I ran it against a tree that does change Before — ...over a After — same tree, patched gate: The arithmetic is exact: 31 previously-compared calls become 30 compared + 1 excluded. The single excluded call is The What this run also confirms is NOT fixedThat is a separate cause and this PR deliberately does not touch it. That artifact is generated by I nearly fixed it by excluding such authorities at selection, with the reason that byte coverage belongs to the generated-artifact drift gate. I checked, and that gate does not exist: — sent from snappy-ferret-99 |
The red on this PR is main's, and this run proves the fix works on CIRun
The single failure: That file is not in this diff. Main is red for it — Worth knowing before anyone attempts the obvious fix: — sent from snappy-ferret-99 |
…-merge was a hybrid The conflict was in a HAND-MAINTAINED bin/ file, so the mirror-hold rule does not apply. I first resolved the two conflict hunks mechanically, asserting that the HEAD side of each was empty (it was, in both). THAT STILL DID NOT COMPILE: the AUTO-MERGED region had pulled in main's call sites -- `admitted`, `AdmittedPlan<'_>` -- without their definitions, which live in a region my branch had diverged on. A hybrid whose halves are each authentic, produced this time by git's own clean merge rather than by a hand resolution. Root cause of the divergence: my branch was -362 lines against the merge base in this file, which an earlier integration must have produced by taking the branch side of an auto-merged region and reverting main's work. The namespace cut edits .dag only, so it has no reason to touch this file at all -- verified: ZERO lines in the branch's diff mention source-root, import, qualify or namespace. Resolution: take main's file whole. Verified by execution, not by inspection -- cargo check -p v1-compiler --bin claim_executor now passes, where the auto-merge failed with 3 errors.
The behavioral receipt reported DIVERGENT over a byte-identical file: measure instability instead of rendering it as a difference
generate_receipt_driverrenders every derived call asprintln!("... = {:?}", call), and amirror function returning
Rc<HashMap<..>>renders in per-process randomized order. The seed andcandidate transcripts come from two separate driver processes, so a map-returning call is a coin
flip that the differential scores as a behavioural difference.
THE DISCRIMINATING OBSERVATION: on gunbc#8726's CI run,
required-regenreportedfirst_generation_equal=true-- the emittedstd_algebra.rsbyte-identical to the committedmirror -- and the receipt then installed that candidate over the mirror and reported DIVERGENT.
It compared a file against itself and could not answer EQUIVALENT. The printed
first_differencewas
kernel_algebra_profile_value()with the same seven entries in a different order.MEASURED, not inferred: a one-line driver built against the committed
libv1_compiler.rlibprinting that call through
{:?}, run 20 times on an unchanged tree, produced 20 DISTINCTtranscripts. Two agreeing runs is the rare event, not the divergence.
This does not fail open. It fails WRONG, and nondeterministically -- the fabricated-difference
mirror of the fabricated-pass that
behavioral_differential's own dirty-tree refusal (review54094) was hardened against.
WHY THE CHECK IS A SECOND RUN AND NOT A TYPE CHECK. The obvious fix is to refuse map-returning
functions at admission, at the function grain main moved to. It is the wrong instrument: order-
dependent rendering is a property of the value's TRANSITIVE shape, so a record CONTAINING a map
renders unstably while its own return type says
Record, andHashSethas the property too. Anycheck keying on the outermost constructor under-refuses BY CONSTRUCTION, and it under-refuses
silently -- the missed call lands in
Divergent, indistinguishable from a real divergence. Anadmission check also runs before anything has been rendered, so a proxy is all it could ever key on.
run_receipt_driveralready builds the crate and compiles a driver binary. Running THAT SAMEBINARY a second time costs milliseconds -- no rebuild -- and two executions of one unchanged binary
that disagree PROVE the disagreeing call renders nondeterministically. The property itself, with
no type walk to keep in sync, catching
HashSetand containing-record cases for free.PLACEMENT: a verdict, not a
ReceiptExclusion. The property is only knowable by RUNNING, andselection happens before any run. That respects the boundary main's function-grain admission
draws rather than ignoring it.
WHAT LANDS
DriverTranscript { lines, unstable };run_receipt_driverruns the built binary twice.independently) and compares only the lines proved stable.
Equivalentcarriesnondeterministic_calls+ the FUNCTION NAMES, because a green with anexcluded population is a different claim from a green over everything, and a name can be
acted on where a count cannot.
NondeterministicRenderingwhen every derived call is unstable: nothing was compared, so itis neither equivalence nor divergence, and the fix lives in emission rather than in this gate
or in the diff under test.
dissolution trigger.
THE COUNT IS A FLOOR AND THE LINE SAYS SO. Instability is proved by two runs disagreeing, so a
call whose randomized rendering happened to agree twice is not counted and is compared as if it
were deterministic. The warning is in the printed line rather than in a comment because the line
outlives the comment: someone will trend this number and read a small one as a nearly-closed
class. The residue SHRINKS with more executions, unlike a structural blind spot -- but one extra
run is what the evidence to date justifies, and speculatively adding more would be a threshold
nobody measured.
DISSOLUTION: the counter goes to zero when emission is deterministic (a
BTreeMapcontainertemplate rather than
HashMap), NOT when the probe gets better at spotting the residue. Thathigher rung makes the nondeterminism unwritable rather than detected-and-excluded; this change is
the declared, counted, bounded reduction until then. Its blast radius --
rust_container_templatesplus everyv1_rtmap signature -- is why it is not in this diff.EVIDENCE BY EXECUTION
--behavioral-receipt-selftestgreen: armpreservingEQUIVALENT over 12 derived calls,arm
changingDIVERGENT over 12 at the authored difference (band_of(100i64) = HighvsMid). Both pre-existing controls still discriminate with the probe in place.preservingarm is now ALSO a false-positive control: its fixture is deterministic, sothe probe must mark nothing unstable, and the arm fails loudly if it does. A probe that
marked everything would otherwise still print a green there while the gate had quietly
stopped comparing.
DriverTranscript::of, including one that PINS the residue: anondeterministic call that agreed twice is not caught. If someone makes the probe complete,
that test fails and forces the FLOOR wording to be revisited rather than left stale.
falseredsexactly
a_length_difference_marks_every_line; flipping the line comparison froma != btoa == breds the other three. The tests are not vacuous.Co-Authored-By: Claude Opus 5 noreply@anthropic.com