C2 opens by finding that its own strongest word meant nothing
C2's objective is that every module says whether it is broken. Step 1 is to enumerate what exists, and the enumeration produced a defect before it produced a list.
The count
| report tags the kernel prints | 33 |
lines carrying MUSTBEZERO | 6 |
| of those, read by the boot gate | 5 |
MUSTBEZERO is the strongest claim this kernel makes about itself. The word
means the boot gate fails if the number is not zero — that is the whole contract,
and it is why a reader trusts the word instead of checking.
[GUI] MUSTBEZERO guard_broken= did not have it. Printed on every boot for the
whole of C0, read by nobody.
Who wrote it, and why that is the point
It was added during C0's GUI work, in the session that had just quoted CLAUDE.md's rule at it:
A line in the serial log is not a check. The ring-3 ABI self-test printed "abi: mmap/mprotect/munmap wrong" for an entire session while the boot gate stayed green.
Knowing the rule, having just written it down, and walking into it anyway is the argument for mechanising it. Judgement did not survive one session.
Why neither existing check-on-checks saw it
Two already watch the checks, and this fell exactly between them:
check-counters-produced.pyasks whether anything can move a reported counter.g_gui_guard_brokenhas a++, so it was satisfied. It exists becauseVIBEOS_BLK_TIMEOUTwas defined, printed, asserted and produced by no driver — the mirror image of this defect.check-assertions-covered.pymatches everyreason=the gate can emit against the sabotage cases.guard_brokennever appeared in areason=, because that is precisely what was missing, so there was nothing to match.
A counter that is produced and never asserted satisfies both. That is the third
axis, and check-mustbezero-asserted.py is it: every MUSTBEZERO <name>=
string literal under kernel/, against every such pattern the gate searches
for. It reported unread=1 on its first run against the real tree — not a
simulation, the state the repository was already in.
It cannot tell whether the gate, having matched a name, compares it to zero. That is one line below the regex and stays in review; the file says so rather than implying coverage.
What was fixed, and what was recorded instead of fixed
The gate asserts gui_guard_broken now, and both cases in gui-guard.txt have
been run. Writing one guard word of the back buffer as zero took the boot from
status=pass to reason=invariant_failed:gui_guard_broken=1 - red for the right
reason, and counting the one word that was broken rather than the whole buffer.
Deleting the assertion again, with the kernel still printing the line, takes
check-mustbezero-asserted.py red; that case did not need simulating, because
it was the state the repository was already in.
Recorded and not fixed: the report line is assembled from twelve separate
serial_puts calls with no serial_lock around them. By this project's own
rule that is twelve critical sections, not one line, and CLAUDE.md records what
it costs — a hex field cut off after its 0x, and two investigations into
crashes that were a marker cut in half. It has not misread yet because the
report runs late, when little else is printing. That is an accident of timing,
not a property; it is the same sentence already written here about a page cache
with one caller. Bracketing it is a change to the log path and belongs with the
rest of C2, not with an assertion fix.
What C2 still has to do
The 33 tags against 6 must-be-zero lines is the real gap, and step 2 is
unchanged: for each module with none, name the harm, add the counter, print it
on the module's tag, assert it, and demonstrate it can be non-zero before
concluding anything from a zero. check-subsystem.py gains the must-be-zero
property at the end of that, not before it — a check shipped red against thirty
modules is the state check-mm-layering.sh sat in for a phase.
Second finding, and this one had a comment vouching for it
hw_cache_audit compares every resident page-cache page against the bytes its
file actually holds, and reports cache_audit_checked / cache_audit_changed
on the [EXEC] line. It runs on every boot. On the boot this was found it
compared 1821 pages.
The boot gate did not read the result — and the comment above the function said:
"Reported as a count, and the boot gate asserts it is zero."
A guarantee documented in the source and provided by nobody is worse than an undocumented gap, because the sentence is what the next reader trusts instead of checking. That is a different defect from the GUI counter found an hour earlier: that one was silent, this one was vouched for.
Why the check added an hour earlier could not see it
check-mustbezero-asserted.py knows counters that carry the word MUSTBEZERO.
This one did not carry it. So the check written specifically for this shape,
against a tree that contained a second instance of the shape, reported ok.
That is worth stating plainly rather than filing as bad luck: the check
mechanises a word, not a property. A counter opts into the guarantee by
spelling it, and one that never spells it is exactly as unwatched as before. The
fix for this instance is to spell it — cache_audit_changed carries the word
now, so both the check and the gate hold it — but the general gap remains, and
naming it is more useful than pretending the check closed it.
Why the harm is the worst class this project has had
Once a read-only image page is mapped from the cache instead of copied, one frame is the text of every process running that program. A stray write reaches all of them, and surfaces as an unrelated program misbehaving far from whatever wrote. That is the family that took four attempts and produced three confident wrong answers.
The audit compares against the file, not a checksum taken at fill time — a checksum only proves the bytes have not changed since the kernel last looked.
What was asserted, and the second assertion that matters more
Two, not one:
cache_audit_changedmust be zero.cache_audit_checkedmust be non-zero.
The second is the one this project has been taught to add. An audit that
examined nothing reports changed=0, which is byte-for-byte the healthy answer;
VIBEOS_BLK_TIMEOUT was asserted for months in exactly that state. Both were
sabotaged and both went red on metal:
| case | result |
|---|---|
| force one entry to differ | reason=invariant_failed:exec_cache_page_changed=1, with a witness naming file, offset, phys, byte index and both values |
| make the audit return immediately | reason=invariant_failed:exec_cache_audit_checked_nothing |
remove the MUSTBEZERO word | check stays green at counters=6, gate goes red with exec_cache_audit_missing |
The third is the interesting one. The check does not fail when a counter leaves
its view — it just stops counting it. The gate is what covers that here, and
that asymmetry is recorded in exec-cache-audit.txt rather than smoothed over.
And a note on writing this file
The case file was first written with ran: yes on all four cases before any
of them had been run. They were then run, and two of the four descriptions
turned out to be wrong: case 3 does not fail the way it was written, and case 4
proves something narrower than claimed. Both are corrected in place. The
sequence is the one this project keeps insisting on and it keeps being
necessary: write the sabotage first, run it, then write the sentence it
justifies.
Step 2 begins: the keyboard, and a counter that cannot report its own worst case
The sweep before this one is worth recording because it came out negative.
254 name=0x fields are printed under kernel/; 100 of them are not read by
the gate. That looks like a hundred defects and is not. Most are witness
fields - rax, pml4, fault_addr, freed_by, oor_lba - which exist to say
what when a count says how often, and asserting them is meaningless. Several
others carry comments stating deliberately that they are not must-be-zero:
rmap_untracked (a frame outside its region is legitimately unmapped),
rmap_audit_torn (a fact about concurrency, not a defect).
Building a check on that list would have repeated the mistake the lock property made an hour earlier, at three times the scale. A check whose first run reports a hundred things is reporting its own design.
One idea from that sweep died on inspection, which is the better outcome than
dying after being committed. The gate detects a TLB shootdown timeout by
matching a log string, not the counter, and log_dropped is printed and
unread — so "a dropped log line can hide a real timeout" looked like a strong
finding. It is false: hw_log_emit writes straight to the serial port and the
portable ring is a separate copy, so a drop there hides nothing from the gate.
And a ring that overwrites when full is behaving correctly, so asserting
log_dropped == 0 would have been wrong twice over.
The keyboard, which had no counter of any kind
Two bare returns dropped keystrokes: the IRQ path when the ring is full, and
vibeos_x86_64_keyboard_inject when the boot self-test's script does not fit.
They are different harms and are counted differently.
kbd_dropped — reported, not must-be-zero. A full ring under a fast typist
is how a ring behaves. It is printed because nobody types on a CI boot, so a
non-zero value there means something is injecting into the console.
kbd_inject_truncated — must-be-zero, and the reason is already in the
source. The comment above KBD_RING records this happening: the ring was 512,
the self-test script outgrew it, and the symptom was the last command silently
never running, which looked like the shell hanging rather than like input being
dropped. The ring was enlarged. Nothing was added that would say so next time.
A truncated injection means the self-test checks a prefix of what it meant to check and passes — the seventh instance of this project's "right about the outcome, wrong about the mechanism", arriving through the one path where the input is the test fixture.
And the honest limit, which is the part worth keeping
The plan says: demonstrate the counter can be non-zero before concluding anything from a zero. Two demonstrations were run and they establish different things.
Forcing the accessor to return a non-zero value took the boot to
reason=invariant_failed:kbd_inject_truncated=3, with the value 3 carried
intact through accessor, report line, regex, assertion and reason. That proves
the plumbing.
Shrinking the ring to 4 — the real harm at full strength — did not produce
a non-zero counter. The boot failed earlier with reason=missing:CLI_READY, and
none of the late report lines printed at all. With no input the machine never
reaches the point where it reports.
So: this counter is printed by a path that a working console is a precondition for. That bounds what it can catch, precisely:
- a partial truncation, where enough script survives to reach the report — the case that once looked like a hanging shell, and the case the counter exists for — is caught.
- a total loss of input is caught by
CLI_READYinstead, loudly. - the gap between them is untested, because the script length and ring size are both fixed and every ring small enough to truncate is small enough to break the boot first.
That last line is recorded as untested rather than counted as covered. It is the same distinction the AHCI cases already carry between "no case exists" and "the case exists and this environment cannot tell".
The keyboard counters made the plan's headline metric worse, and the check said so
check-blast-radius.py, written the same day, went red on the keyboard commit.
input device: 2 -> 4. Giving the keyboard its first must-be-zero counter
cost two files that have nothing to do with keyboards: an accessor declared in
arch_x86_64.h, and a print in kmain.c. Total across six points: 21 -> 23.
That is a structural regression caused by an observability change, caught within hours by a check written to measure exactly that, in the one direction nobody would have looked — the change made things better by C2's measure and worse by C1's.
The finding underneath it
This is not a keyboard problem, and it does not go away by being careful.
Observability itself has a blast radius here, and it is 2 per module.
There is no seam a module registers its statistics into. Every counter C2 adds — and there are roughly thirty modules left — pays the same two files, so C2 as planned would raise the total by about sixty and hand C6 a worse tree than it found.
The number is raised to 4 with that argument recorded in the check, which is what the plan asks for: a radius going up needs an argument, not an edit. A stats registration seam takes this row back to 2 and takes the next thirty counters with it, and that now has a measured justification rather than being a matter of taste.
And a defect in all four checks of this family
The failure arrived as VERDICT=RED with no reason beside it: the
blast-radius= line was missing from the summary entirely.
check.sh reads each check with | tail -1, and all four of these checks
printed their advice line after the verdict. So on failure the summary got
the advice and the verdict vanished — the line that matters printed and not
read, for the fourth time today, this time in the tooling built to stop that.
check-chokepoints.py had the same order from the day it was written and had
never shown it, because it has never gone red inside check.sh. Fixed in all
four: advice first, verdict last, and confirmed by breaking a baseline and
watching tail -1 produce subsystem=FAIL.