Price the OVMX-EXECUTIVE claim on which code a defect edits, not on what an assertion says (vms-ecf, vms-f26)

[baron-3dl]

Closes vms-ecf and vms-f26 — the last two open blockers on vms-b33's Phase 2 verdict.

Four rounds. Rounds 1–3 were each refused by an adversary. Round 4 is the first whose central claim the adversary could not break.

The problem

The userspace service register grants exactly one full exemption, OVMX-EXECUTIVE, and the price kept being purchasable:

round	what a full exemption cost	how
1	one comment line	check 4 was grep -qF "$pname" "$proof" — a comment satisfies it
2	one phrase appended to an assertion string	edit the text in the suite and the manifest together
3	one declaration flip	the service was already OVMX-PARTIAL, so both checks were pre-satisfied
4	two edits, disclosed and filed	vms-38c

Round 2's instrument is the one that mattered: if editing an assertion's words is how a service becomes covered, coverage is a naming convention and not a measurement — and that was the same instrument used to make sys$readef "pay".

What lands

The universe is derived from the build, not from source text. The gate compiles all 127 product .c files and reads exported sys$* symbols with nm — 88 services, 88 exported, 0 symbol-only. On main the symbol set and the source set are equal, so nothing was papered over; an asm-alias rename now goes red. No hand-maintained cardinal anywhere.

The price is derived from which code a proven-reddening defect actually edits, in four code-only hops: call graph → the VMS_IOCTL_* constant the kif wrapper references → the case arm in src/kernel/vms_module.c → the file defining that handler. No check reads a service name out of prose.

The answer path is split, and the halves do opposite things. The executive half pays. The userspace remainder — the translation unit defining the service — refutes: a defect that changes an observable public-API answer by mutating code in the calling process is evidence a remainder exists, which is the negation of "all of it is the executive's." Check 6 is a disqualifier, not a sixth thing to buy, and the printed remedy is OVMX-PARTIAL + OVMX-LOCAL — never deletion.

sys$readef was resolved without renaming. Round 2's three renamed assertion texts are reverted in lockstep; git diff origin/main -- tests/qemu/ is empty. It pays like the others: eflag-clref-noop → 24/4, red set equal to require_fail exactly, one red at test_syssvc_ef_mproc.c:221 asserting on sys$readef's own return and out-param, cross-process; eflag-waitfr-eintr-normal → 27/1, both reds in that same proof.

The disqualifier's first result: three services demoted

sys$enq / sys$enqw / sys$deq drop from OVMX-EXECUTIVE to OVMX-PARTIAL + OVMX-LOCAL, taking the EXECUTIVE count 10 → 7.

That is a measurement, not a regression, and it was settled by execution rather than argument. All three kstat-* defects hit one case arm in kstat_to_ss(). Compiling the product TU verbatim, pristine vs. all-three-injected: diff -rq over src/ shows one file differs, zero executive code, while the public status the caller receives changes 3594→2488, 8484→2488, 8508→2488. SS$_DEADLOCK becoming SS$_NOTQUEUED is a different answer, not a different spelling — a caller branching on it behaves differently.

No /dev/vms was needed to prove that, which is exactly the point being claimed. The underlying defect is now filed as vms-82a: the executive uses a private numbering (100/108/116) and never produces an ssdef.h value, so the VMS-visible status is manufactured in userspace. Note the lock manager is the precedent the whole executive ruling rests on — so the one facility cited as proof OVMX does this properly is the one still finishing its answer outside.

Disclosed residual — not claimed closed

Buying a claim still costs two edits, and the round says so in the gate's own text rather than measuring it away. Four successive price statements have each been broken by execution, so no number is carried — the comment explains why and names the residuals instead. Tracked as vms-38c, corrected twice: the cheap route is addition (sys$wflor — flip its PARTIAL+LOCAL block, add one ignored (void)sys$wflor(0u, 0u) to a proof), not deletion, so flooring the manifest against deletion would not close it. The weak hop is check 4, "the proof calls the service" — a call that asserts nothing satisfies it. Only per-assertion runtime attribution closes that, which is what vms-38c exists to do.

Adversarial verification

• No hop can be made to certify silently — indirect ioctl constant, in-file dispatch thunk, and function-pointer call each go red naming the service and printing executive answer path is: (empty).
• "A price that cannot be computed must refuse, not certify" is a control: an earlier draft assumed unknown -Wno-* flags are ignored, measured otherwise (gcc rejects one at cc1, all 127 files failed), and the gate refused rather than certifying on an empty symbol set.
• Reproduced from a clean archive: register rc=0 · 88 services / 68 USERSPACE / 13 PARTIAL / 7 EXECUTIVE · negctl 44/0 · coverage 26/26 · facility_defects.sh selftest rc=0 · kif census rc=0 · census negctl 23/0 · test_runtime_target.sh rc=0.
• src/ change is comment-only — cpp output byte-identical. tests/qemu/ byte-identical to origin/main, so no test_syssvc_* suite changed and the negative-control job's inputs are unchanged.

🤖 Generated with Claude Code

[baron-3dl]

Round 5 — adca060, the CI refusal

The Build & Test failure was this branch's own gate working correctly:

FAIL: BROKEN SYMBOL SCAN: 126 of 127 product source file(s) compiled.
  src/vmsssh/vmssshd.c:37:10: fatal error: libssh/libssh.h: No such file or directory
  ... so a service could hide behind a build error. Do NOT let a compile failure pass silently.

The build-derived universe is new on this branch, so the gate hard-fails wherever libssh-dev is absent — the GitHub Build & Test job, and the workshop dev host. Legal answer taken: make the condition unreachable. libssh-dev is added to the Build & Test job's apt list (the only job running ctest, hence entries 8 and 9). The refusal itself is untouched — no skip, no allowlist, no tolerated short count, no downgrade to a warning. The gate header now documents why its dependencies are the whole product's dependencies, next to the SYMSCAN_EXCLUDE_DIR mechanism, so the next reader meets the reason before the workaround.

Source scan: 127 of 127 (was 126). Universe still 88 = 88, 0 symbol-only.

Verified in a container mirroring the job: configure rc=0, build rc=0, ctest 53/53 passed, 0 failed; entry 8 Passed (6.86 s), entry 9 Passed (197.8 s). The same tree in the same image without libssh-dev reproduces the CI failure exactly — the fix is load-bearing, not cosmetic.

One correction worth recording: the orchestrator predicted this would take ctest from 39 to 41 entries. Measured, that is wrong on this tree — ctest -N reports 53 with libssh-dev and 53 without, identical. CMake skips src/vmsssh (the daemon registers no tests) and tests/vmsssh (term_mapping) has no libssh dependency and is configured either way (CMakeLists.txt:171). The wrong number had already been written into the ci.yml comment and was corrected there rather than shipped.

Gates on the merge result against main @ ce11330 (merges clean): register rc=0 — 7 EXECUTIVE all paid, 13 PARTIAL, 68 USERSPACE, 127 objects · register negctl 44/0 · coverage 26/26 · kif census rc=0 · census negctl 23/0 · test_runtime_target.sh rc=0 · facility_defects.sh selftest rc=0.