Observe whether a runner host can measure a VMM's footprint, and model the probe

[gunbai-bot]

Split out of the micro-VM lifecycle branch, which was carrying three subjects under a title naming one. Under squash-merge that title becomes main's permanent commit subject, so the split is about what the history says as much as about review size.

What this is for

Micro-VM admission needs the VMM's own resident footprint. That quantity is not cited in extdeps.virtualization.firecracker — upstream documents a measured overhead for one configuration rather than a property of the realization, because it scales with guest size, device model and host page size. Inventing a number would be a fabricated plausible output, so it has to be measured, and measuring starts with whether a host carries an instrument that can.

What it does

• extdeps.tools.gnu_time — GNU time's max-RSS invocation, writing to a file rather than stderr, because Firecracker writes its own diagnostics there.
• extdeps.systemd.systemctl gains systemctl_version_command. MemoryPeak arrives in systemd v254, so whether a host can report a scope's peak is a fact about the systemd it runs. The version is read, not inferred from the distribution.
• runner_microvm_host_ready gains instrument standing without changing what makes a host ready — an unmeasurable host is still a runnable one.
• runner_microvm_footprint_probe samples across guest sizes, because one sample cannot separate the VMM's fixed overhead from the part that scales with the guest.

Two things the controls exist to catch

The completeness fold is count-guarded. A true-seeded fold over an empty list answers true about a population it never examined.

The sizes are converted, not widened. Storing a Mebibyte in a ByteSize field is accepted and does not convert — 4096 MiB becomes 4096 bytes, magnitude unchanged. The type system stops the read and permits the write. A span or ratio control cannot catch this, because a uniform unit error preserves every ratio, so one claim pins an absolute magnitude. That claim is what caught the bug.

Evidence

All 7 claims pass by execution on this branch (claim_batch --claim-run), and the entry compiles with 0 blocking errors. Not inherited from the branch this was split from — re-run here, because it is a different tree.

The extdeps rows are re-applied onto current main rather than copied from the source branch. Copying would have deleted the mosquitto_publish_command admit_callers row that landed on main after the branch point; a file diff reads that as reordering and only the row count shows it.

No wet receipt, and why that is not a reason to hold

Every claim here passes dry: the probe's construction, the completeness fold, the unit conversion. What is not here is a footprint measured on a real host running a real VMM — the number this model exists to obtain.

That receipt does not exist because srv2 access was reported granted and never landed; the host still refuses this session's key. So holding this branch for a wet receipt is waiting on a host nobody has, which converts an honest measurement model into an indefinite hold — and an indefinite hold justified by evidence that cannot be obtained is exactly the untracked stall §4b(2) forbids.

It lands on the claim it actually makes: this is the model and the instrument, not the measurement. The trigger that retires the gap is a wet footprint receipt from a host running the VMM under the probe — named as the capability, not as "srv2 access", because any host carrying the instrument discharges it.

Not in scope

The launch plan, the execution grant, and the JIT mint. This branch does not reference them.

🤖 Generated with Claude Code

https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN

[gunbai-bot]

All four findings confirmed and fixed. Review 62181.

1. Forked gnu_time_binary_path — confirmed

Two declarations of one literal, added in one diff: extdeps/tools/gnu_time.dag (NonEmptyStr) and runner_microvm_host_ready.dag:95 (String). The extdeps declaration exists because naming the binary by path is the fact worth owning, so re-minting it here contradicted the module I was landing beside it. The local one is deleted and the extdeps authority imported — and the review is right that the import was already available, since the same file imports systemctl_version_command from extdeps.

2. Hand-rolled KiB — confirmed

gnu_time_max_rss_unit_bytes: Int = 1024 was a second unit system beside std.measure, which already carries Kibibyte, kibibyte_to_byte_size and an IEC 80000-13 kibi_factor(). Now:

fn gnu_time_max_rss_bytes(kibibytes: Nat) -> ByteSize {
  kibibyte_to_byte_size(k: kibibyte(count: kibibytes))
}

The parameter is a Nat of kibibytes rather than a bare Int carrying an implicit unit, and the claim is renamed gnu_time_kibibytes_become_bytes — %M is KiB, and the old name said kilobytes. The review's framing is exactly right and worth restating: the module's comment was right about where the conversion belongs (the consumer knows what it measured) and wrong about how — owning the choice of unit is not owning the arithmetic.

The absolute-magnitude control still passes through the new path, which is the point of having had it.

3. Probe has no consumer — confirmed, declared as a §3c frontier

git grep confirms it: only its own witness, and gnu_time_max_rss_command has no call site outside the admit_callers roster row that permits it. Nothing runs a VMM under /usr/bin/time.

Rather than argue this in the PR body where no reader of the module will see it, the frontier is now declared in the module: named consumer is a wet footprint run, and the trigger is that run producing a receipt — deliberately not bound to a specific host, because waiting on one machine nobody has is the untracked stall §4b(2) forbids. It also records what separates it from dangling modeling: the sibling half, the instrument standing in runner_microvm_host_ready, does execute today and answers whether a host can measure at all.

4. Instrument roster forked into booleans — confirmed, and they had already drifted

This was the deepest one. Two independently editable enumerations of one set, and the review is right that they already disagreed: cgroup memory.peak had a boolean and no variant, and systemd was a raw String that the renderer re-interpreted by trimming for emptiness.

Repaired at the authority. FootprintInstrument is the single enumeration (now carrying CgroupMemoryPeak), and the standing is List<InstrumentStanding> keyed by it, so adding an instrument edits one place.

The systemd case also fixes a fail-open the boolean shape made unwritable-against. Observation is now three-valued:

type InstrumentObservation = InstrumentPresent | InstrumentAbsent | InstrumentUnreadable { cause: String }

"We could not read whether the host carries it" and "the host does not carry it" were rendering identically, and only one of those means the host cannot measure. In a receipt whose entire purpose is telling a human what can measure the reserve, collapsing them is the absorbing arm §5 names.

Evidence

All 7 footprint-probe claims pass by execution after the rework, including the absolute-magnitude control. Host-ready claims re-run against the new standing shape. Compile shows the 3 pre-existing dag/extdeps/gunbc/gunbc.dag shell-transport errors and nothing in these files.

One process note I owe this PR: this REQUEST_CHANGES stood on the current head for several hours while I reported the PR as ready to merge on CI and mergeStateStatus alone. I was checking the wrong two of the four gates.

— sent from nimble-swift-27

[gunbai-bot]

Both findings confirmed and fixed in a7e3368dcaa. Review 62352.

1. The systemd instrument asserted a capability from a non-empty line — confirmed, and it is the worst defect on this branch

The review is exactly right, including about the direction. I introduced the three-valued InstrumentObservation in the previous commit specifically so "we could not tell" would stop rendering as "absent" — and then reported SystemdMemoryPeak as InstrumentPresent for any non-empty version line. A host on v249, which cannot report MemoryPeak at all, rendered systemd-memory-peak=present on the receipt a human reads to decide what can measure the reserve.

That is a fabricated answer in the stronger direction, and the distinction matters: the absorbing arm loses information, this one asserts a capability the host does not have. §5's "no fabricated plausible output" is the right citation.

The v254 criterion was in this repo's own extdeps prose two files away, which is the general shape and why the fix is a model rather than a condition: a fact left in prose cannot be read, so nothing applies it.

extdeps.systemd.systemctl now carries systemd_memory_peak_minimum_version and a three-valued SystemdMemoryPeakSupport. The major version is parsed, not pattern-matched, so a line it cannot read answers Absent/SystemdVersionUnreadable rather than a fabricated number. The consumer maps below-threshold to InstrumentAbsent — a claim about the host — and unparseable to InstrumentUnreadable — a claim about our observation.

On the review's closing point that nothing goes red on this: that was the actual cause, not a side note. Four assertions now exercise it — v255 admits, v249 refuses carrying its version, empty is unreadable, and the 254/253 boundary is pinned, because an off-by-one there reports the exact version that gained MemoryPeak as unable to report it.

2. Re-minted cgroup path — confirmed

cgroup_v2_memory_peak_path now derives from cgroup_v2_mount_point and cgroup_memory_interface_file_name(MemoryPeak) via cgroup_v2_child_path, rather than re-coining /sys/fs/cgroup/memory.peak. Two authorities already owned both halves.

Evidence

5 claims pass by execution, including both new version-gate controls. Compile shows the 3 pre-existing dag/extdeps/gunbc/gunbc.dag shell-transport errors and nothing in these files.

— sent from nimble-swift-27