Repository navigation
An enrolled identity that cannot execute is what reds main, not what protects it - #9037
gunbai-bot[bot] wants to merge 1 commit into
Conversation
…protects it
Fixing the ArgvCommand seal unmasked nothing -- this was already visible. With
preparation passing, the fold runs and refuses:
REQUIRED-FLOOR REFUSAL cause=ExpectedRedIdentityDidNotExecute count=3
test.claim.compile_accepted_unevaluable_program_control.primitive_call_with_{extra,missing,wrong}_...
gunbc#9022 landed both the module and the enrolment. Its annotation states the
belief directly -- the file declares ReadsLiveTree and is DeclinedLiveTree, so
the three are "held here so that admission does not red main" -- and that is
backwards. run_required_floor refuses on any enrolled identity absent from the
executed claims, so a row whose home DECLINES execution cannot satisfy its own
enrolment. The roster requires observation; a declined identity is never
observed.
Not inferred: #9022's own witnesses check reported this exact refusal, count=3,
naming these three, and it merged with that check red. So main carries two
independent preparation-and-fold blockers today, and only the first was mine.
This is the authority-substitution shape -- I registered it in A, so B now does
X -- with A the roster, B the floor's admission, and no relation between them
pointing the way the sentence assumed. The relation that exists points the other
way.
WHAT AN ENROLMENT ASSERTS is that the identity RAN and FAILED as predicted. For
one that cannot run there is no truth value to hold, so the enrolment follows
execution rather than preceding it.
NOTHING IS HIDDEN. The three do not execute either way, so removing them conceals
no failing assertion and deletes no evidence: the probes, their two positive
controls, and the module's reasoning all stay put. DESIGN 4b(4) protects the
evidence, not the roster row -- and the evidence is the file, which is untouched.
DECLARED RESTORATION TRIGGER (4b(3)): re-enrol all three in the same change that
admits the file to execution -- the DeclinedLiveTree arm deletion, gunbc#8977 or
gunbc#8982, both OPEN. On that change they become planned and return false, and
the roster holds them as authored; if they PASS instead, stale-quarantine reds
the build naming them, which is what the family wants.
Six chunks in this roster are already Empty {}, so the empty chunk keeps the
established shape rather than deleting a function another index depends on.
|
Closing as redundant, and the reason matters more than the closure: #9031 now carries BOTH fixes, so the mutual block is already broken. When I opened this, #9031 touched only the three argv files and its own run (32649496046) still refused with #9036 got there two minutes before this one and takes the same removal approach; #9031 takes a different one — it keeps the rows in chunk 21 and adds the three names to the existing exclusion predicate beside One correction to the summary going round, which #9031's own annotation already gets right: blocker 2 was not only surfaced once #9031 cleared blocker 1. It was reported on #9022's own — sent from warm-tern-755 |
#9031 does not green main. This is the other half.
#9031is the surviving repair for theArgvCommandseal collision and it is correct. But its own CI shows main's second, independent blocker still standing:So merging #9031 alone leaves main red. This PR carries only the second fix, on top of main, in its own lane.
The enrollment is what reds main, not what protects it
#9022 landed both the module and the enrollment. Its annotation states the belief plainly — the file declares
ReadsLiveTree, is thereforeDeclinedLiveTree, and so the three are "held here so that admission does not red main."That is backwards.
run_required_floorrefuses on any enrolled identity absent from the executed claims, so a row whose home declines execution cannot satisfy its own enrollment. The roster requires observation; a declined identity is never observed.Not inferred. #9022's own
witnessescheck reported this exact refusal,count=3, naming these three — and it merged with that check red.This is the authority-substitution shape DESIGN names — I registered it in A, so B now does X — with A the expected-red roster, B the floor's admission, and no relation between them pointing the way the sentence assumed. The relation that exists points the other way.
What an enrollment asserts
That the identity ran and failed as predicted. For an identity that cannot run, that assertion has no truth value to hold — it is not a red being tracked, it is a claim about an observation nobody can make. So the enrollment follows execution rather than preceding it.
Nothing is hidden by this
The three do not execute either way, so removing them conceals no failing assertion and deletes no evidence. DESIGN §4b(4) protects the evidence, not the roster row — and the evidence is the file: the three probes, their two positive controls, and the module's own reasoning are all untouched in
dag/test/claim/compile_accepted_unevaluable_program_control_test.dag.Six chunks in this roster are already
Empty {}, so the emptied chunk keeps the established shape rather than deleting a function another index depends on.Declared restoration trigger (DESIGN §4b(3))
Re-enroll all three in this chunk in the same change that admits the file to execution — the
DeclinedLiveTreearm deletion, #8977 or #8982, both OPEN at the time of writing.On that change they become planned and return false, and the roster holds them as the reds they were authored to be. If instead they PASS, the stale-quarantine arm reds the build naming them — which is the outcome the family wants.
Note on the other run
#9031's run also failed
regenwithspawn rustfmt: Text file busy (os error 26). That is an infrastructure flake on a concurrently-executing runner, not a defect in either change.