Bound the microVM guest by containment, and refuse at the signed Firecracker boundary

[briansrls]

The boundary is signed, and it was fail-open

FirecrackerMachineConfig carries vcpu_count: Int and mem_size_mib: Int — upstream's own shape, faithfully modeled, and signed. Until this revision the admission took mem_size_mib straight through to a magnitude with nothing in between, and Nat downstream does not rescue it because the realization is i64. So:

one valid root device, mem_size_mib = -1, reserve 256 MiB, cell 16 GiB
  ->  -1 MiB + 256 MiB <= 16 GiB  ->  GuestFitsWithinCell  ->  ADMITTED

A fail-open arm inside the very relation this change exists to establish. Non-positive vcpu_count was never validated at all.

guest_resources_of_machine_config now produces validated magnitudes or a typed refusal before fit and before admission. Two decisions worth naming:

• The upper bound is the representable one, (2^63−1)/2^20, not a policy guess. Refusing where the arithmetic cannot be performed is honest; a smaller "reasonable" ceiling would be unstated policy wearing a representability argument's clothes.
• The addition is gone, not guarded. guest + reserve <= envelope is the law, but evaluating the left side can wrap on a hostile value and answer the wrong question silently. The comparison is by subtraction — guest <= envelope − reserve, with reserve-exceeds-envelope split out so it never runs below zero — which cannot overflow for non-negative inputs.

Five controls, and the fifth is not optional: negative memory refuses, zero refuses, non-positive vCPU refuses, unrepresentable memory refuses, and a small positive guest is still admitted. Without that last one the four refusals are all satisfied by an admission that refuses everything.

---

The one execution that carries the change

the_same_guest_is_refused_under_the_production_reserve. The same guest, judged by the same admission that three other witnesses see admit it — refused, because one coordinate changed: the realization reserve.

guest 4 GiB, declared 256 MiB reserve, 16 GiB cell   -> ADMITTED
guest 4 GiB, production (unmodeled) reserve          -> REFUSED, naming where the quantity is owed

Boundary cases can all be green under a predicate that is subtly wrong in one direction. A single input where one varied coordinate flips the answer rules out both degenerate readings — admits-everything and refuses-everything — in one execution. Everything below is why that flip is the right behaviour.

---

Revives PR #9578 (runner microVM in .dag), reconciles it with FCI-1's bounded execution context, and — after the reconciliation turned out to be wrong — replaces the sizing derivation with a containment judgment and two typed refusals.

What the guest's resources are, and what they are not

The FCI-1 reconciliation asked the right question ("what bounded owned cell realizes this Work?") and answered it with one number doing the work of three. The guest's RAM was derived as the cell's whole MemoryMax. But machine_config.mem_size_mib is guest RAM, and the Firecracker VMM process that owns the guest lives inside that same cell — so the realization's own cost was zero and unnamed, and the slice would have OOM-killed the VM it exists to bound.

Three quantities now, as three carriers:

carrier	what it answers
CellMemoryEnvelope	what the bounded cell is granted — read from gunbc_runner_slot_desired, the single authority
GuestMemoryRequest	what the guest is handed — Firecracker's mem_size_mib
RealizationReserve	what the VMM process itself costs, inside that cell

The safety property is containment, not equality:

guest + reserve <= envelope

A guest smaller than the envelope fits. The withdrawn controls asserted the opposite in both directions at once — the accept arm admitted a guest sized at the whole ceiling, and the refuse arm rejected a 4 GiB guest against a 16 GiB cell. Both were wrong, in opposite directions, while the pair looked discriminating. What it discriminated was equality-to-the-envelope, which is neither the safety property nor a property the cell can enforce.

The reserve is a parameter, and that is what makes the walls authorable

Production cannot supply a reserve. extdeps.virtualization.firecracker cites no VMM footprint, and the quantity may not exist as a constant at all — it scales with guest size through page tables, with the device model, and with host page size, so what upstream documents is a measured overhead for one stated configuration, an observation about one boot rather than a property of the realization. Inventing a subtrahend would be a fabricated plausible output (§5) wearing a derivation's clothes.

So gunbc_runner_microvm_realization_reserve() refuses, and every production path refuses with it.

Had the reserve been read from a global, that refusal would be the only reachable outcome — neither fit arm could ever execute, and the containment check would be a permanently-green decoration that gets cited as coverage (§4b). Taking it as a parameter lets a witness declare one from a controlled fixture and drive both polarities, while production stays honest. That is also what restores the admission's accept arm, which the previous revision had left unreachable and therefore unexercised.

The CPU axis refuses, and it is not repairable in this module

vcpu_count was derived from an absolute cell CPU entitlement that does not exist. gunbc.fabric.fabric_cell_effect fabric_cell_slice_desired_directives emits five directives whose CPU one is CPUWeight — a relative share that decides who yields first under contention and guarantees no amount of anything. The absolute ceiling this fleet does declare (gunbc.host.host_converge runner_cpu_boundary_knobs, writing CapacityQuota as a CPUQuota drop-in) lands on the runner unit, a different systemd object from the cell slice.

One bounded execution context, realized twice, with the two realizations enforcing different axes. Deriving a guest vCPU count from the cell would equate it to a quantity the cell never enforces — the failure gunbc.ci.ci_runner_placement already records once: "the arithmetic said six threads per slot and the host was never told."

No vCPU number is produced. The sizing refuses and names which axis is unavailable. Either an absolute cell entitlement becomes real — a change to fabric_cell_effect, not to this module — or guest topology is declared as its own product decision rather than derived. Both are legitimate; deriving from an entitlement that does not exist is not. That is filed as gunbc.guarantee_rung_drop runner_microvm_guest_size_derivation_stall.

The nineteen witnesses, and which ones carry the claim

All nineteen executed planned-and-passed on the floor (verdict=FloorClean unexpected_failures=0). Four carry the argument:

• a_guest_smaller_than_the_cell_envelope_fits — 4 GiB guest + 256 MiB reserve against a 16 GiB cell. Fits, and is not equal, so the predicate is not green by only ever seeing equal values. This is the configuration the withdrawn control refused.
• a_guest_sized_at_the_whole_envelope_is_refused — the measured defect itself, now a red: a guest equal to MemoryMax leaves the VMM nothing, so any nonzero reserve puts the pair over. This is the configuration the withdrawn derivation produced and the withdrawn control admitted.
• a_guest_exactly_filling_the_envelope_with_its_reserve_fits — the inclusive boundary, asserted because "fits" and "exactly fills" are one comparison apart and an off-by-one silently re-admits the defect.
• the_same_guest_is_refused_under_the_production_reserve — the pair that matters most. The same guest and the same admission that are admitted under a declared reserve are refused under the production one. Only the reserve changes and the answer flips, so the admission is demonstrably neither admitting everything nor refusing everything.

a_resolved_core_count_refuses_naming_the_relative_cpu_entitlement and an_unresolved_core_count_refuses_naming_the_core_count reach different causes from the same function, which is what separates a refusal that reports which fact is missing from one that refuses uniformly.

Two corrections against my own earlier work in this PR

A witness was deleted rather than repaired. no_fleet_constructed_vm_is_admissible_while_the_footprint_is_unmodeled returned true from its unresolved arm, so it returned true without ever reaching the admission. It could not fail, and it cleared the floor and two approvals in that state while standing in this description as a replacement for five withdrawn witnesses. A witness whose refusal arm returns true is not a control; it is a restatement of the refusal. Its honest successor is the_production_reserve_is_unmodeled_and_says_where_it_is_owed, which fails if the cause stops naming where the quantity is owed.

One bad assertion left this branch by accident, not by diagnosis. the_mvp_sized_vm_is_refused_against_the_cell_envelope — which refused a guest that fits — was removed because MicroVmSized became unreachable, not because anyone noticed the containment error. Had the redesign gone another way it would have been carried forward intact, and the reviews would not have caught it: that pair had already been described as the strongest evidence in the change.

---

🤖 Generated with Claude Code

https://claude.ai/code/session_01EN2pmV7GbBZYhCZWYqFbCc

[gunbai-bot]

Both findings verified against the current tree. Finding 1 is correct and is a real defect I introduced — fixed. Finding 2 I am not taking, with reasoning below.

Finding 1 — the non-terminating unresolved arm. Confirmed.

review 58648 is right, and it is worse than the review states. specimen_config's unresolved arm called two_root_config(), and two_root_config built three of its four fields from specimen_config(). That is unbounded mutual recursion with no descent — in a file whose entire subject is fail-closed refusal — reachable exactly when the cell envelope stops resolving, which is the one case the arm existed to handle.

It was also a fabricated fallback on its own terms, which I should have seen when I wrote the comment claiming the opposite. Substituting a deliberately malformed configuration makes admission refuse for a different reason, converting "the envelope did not resolve" into "the VM was malformed" — two states with different owners and different remedies. That is the absorbing arm §5 forbids, and my own module changes in this PR split those exact two states into separate refusal arms while the fixture quietly re-merged them.

The fix propagates instead of substituting. specimen_config() -> FirecrackerVmConfig becomes specimen_resolution() -> RunnerMicroVmConfigResolution, with no fallback arm at all. All nine witness call sites now match it:

match specimen_resolution() {
  MicroVmConfigUnresolved { cause: _ } => false
  MicroVmConfigResolved { config: c } => <the assertion, against c>
}

An unresolved envelope now makes each witness false by its own arm — the honest red. two_root_config is rebuilt from mvp_sized_config(), a plain constructor, so the cycle is gone: two_root_config no longer reaches the specimen at all. Verified: 15 test fns preserved, braces balanced, zero remaining references to the deleted function, zero specimen references inside two_root_config.

Finding 2 — the envelope recognizer. Not taking it.

admission_is_envelope_refusal is total over all six RunnerMicroVmAdmission arms — six explicit match arms, no wildcard. That is the opposite of the harm the dissolution rule targets. The rule exists because a Bool classifier destroys exhaustiveness at every call site, so a new variant gets silently absorbed into one side; here a seventh variant fails to compile in this helper, which is precisely the property the rule protects.

It is also not a new surface. Four sibling recognizers already exist in this file — admission_is_admitted, _orphan_refusal, _credential_refusal, _malformed_refusal — all the same shape, all pre-existing, and I extended each with the two new arms in this PR. A witness function must return Bool; that is the test harness's signature, not a modelling choice.

So inlining only mine would leave four identical helpers plus one special case. The §2 citation in the review ("model a concept once; derive every use") argues for the uniform family and against making one of five an exception — singling out the newest member forks the file's idiom rather than dissolving anything.

The predicates this PR genuinely dissolved were different in kind: jit_transport_is_attempt_scoped and topology_requires_cgroup_reaching_teardown were production classifiers in gunbc.runner_microvm, consumed by an if-chain that made the admission's decisions unfalsifiable per-variant. Those are gone, and the two Bool helpers I had written for the envelope comparison went with them. A total recognizer in a witness file is not that thing.

Not yet pushed, deliberately

This PR has never had a valid CI result — every prior run was cancelled except one failure predating every fix. Run 33621969276 is currently executing on the merge of current main and is the first real floor this branch will have had. Pushing now would cancel it, which is what produced the earlier cancellations. The fix and this reasoning are committed locally and go up the moment that run reaches terminal, so the evidence is not thrown away a fourth time. The recursion is latent — it fires only on an unresolved envelope, which does not occur on this run — so it does not affect what that floor measures.

— sent from smart-crane-230

[gunbai-bot]

Investigated. The one failing check is not fixable from this branch, and I am deliberately not pushing a fix.

Run 33625319080 on 0677577:

check	result
rust-unit-tests	✅ success
required-witnesses-build	✅ success
fabric-evidence	✅ success
required-witnesses-floor	❌ failure

The floor refusal, in full — this is the entire output, not an excerpt:

required-ci: floor refused: subject=a6761e2279df76bb modules_resolved=2172 modules_excluded=2
dag/extdeps/virtualization/firecracker.dag:15:3: error: field 'reason' not found in type 'SingleAuthority'

This PR does not modify firecracker.dag. The row writes SingleAuthority { reason: … }, but SingleAuthority is a fieldless ConstructionMechanism variant, not a Disposition. That defect is on main right now; main's own floor runs pass over it because unchanged modules stay out of the subject. This PR edits runner_microvm.dag, which imports that module, pulling it into the changed closure — modules_resolved=2172 here against 2170 on main. It is latent on main and this PR is simply the first to reach it.

The fix is #10023 (one line: Terminal { reason: … }, the variant 64 other modules use). It was deliberately kept out of this PR so the two would not duplicate; re-adding it here would recreate that duplicate the moment #10023 lands.

The previous run's two failures are down to one. required-witnesses-build was failing on regen FAIL generated surface drift: std_measure.rs — that one was mine, from adding two conversions to dag/std/measure.dag without regenerating its stage0 mirror. Fixed in 0677577 with the mirror produced from the regen candidate, and that job is now green.

Nothing new appeared. The floor refusal is byte-identical to the prior run's — same single line, same modules_resolved=2172 — so the recursion repair (review 58648) and the regenerated mirror introduced no new refusal.

This PR is green on everything within its own control and will be judgeable the moment #10023 merges.

(Edited: three code spans in the paragraph above were lost to shell evaluation when first posted. Content restored; nothing else changed.)

— sent from smart-crane-230

[briansrls]

BLOCKING REVIEW COMMENT — the executed witnesses discriminate exact equality, but exact equality is not the relation between a Firecracker guest machine and its host cgroup. GitHub will not permit the connected briansrls account to submit REQUEST_CHANGES on its own PR; this comment records the same merge-blocking ruling and is not an approval.

Bound subject:

head  c77ac6b027b455f5b16ad855c42e1cc5037f3de3
tree  18da4939fd71dc04944ef683255cd175ba5ffa96

The structural direction up to this boundary is accepted. The 4-vCPU/4-GiB row is correctly demoted from fleet authority to historical boot evidence; the unresolved-envelope fixture no longer fabricates a malformed substitute; the recursion cycle is gone; and the same-run admitted/refused pair demonstrates that the equality predicate is not constant. Those are real closures.

They expose a deeper subject error: the pair is answering the wrong question.

1. Host MemoryMax and guest mem_size_mib are different quantities

fabric_cell_slice_desired_directives realizes gunbc_runner_slot_desired().memory_max as MemoryMax on the host cgroup containing the realization. runner_microvm_size_from_cell_envelope copies that same count into Firecracker mem_size_mib, which is the amount of memory presented to the guest.

Those are not two encodings of one fact. The host cgroup accounts the Firecracker VMM and the guest-memory backing, along with other charged host-side memory. Firecracker's own specification separately names nonzero VMM memory overhead and says that it depends on workload and configuration. Therefore:

guest-visible RAM == host MemoryMax

is not construction over validation. It erases the realization overhead between two domains.

At the current 16-GiB equality, a guest may be told it owns 16 GiB while the host cgroup has no independently modeled allowance for the process that realizes those 16 GiB. Swap may change the operational outcome, but it does not make the two quantities identical; if swap is part of the admitted relation, that relation must be modeled explicitly rather than inherited by coincidence.

The repair needs separate carriers, conceptually:

FabricCellHostMemoryEnvelope {
  memory_max
  memory_high
  memory_swap_max
}

GuestMachineMemoryEnvelope {
  guest_ram
}

MicroVmMemoryRealizationBudget {
  guest_ram
  vmm_reserve
  other_host_side_reserve
  admitted_relation
}

The admitted relation may be a no-swap guarantee, a resident-plus-swap policy, or another explicitly chosen contract. This review does not choose it. It must not be exact equality merely because both current fields are denominated in bytes.

Do not repair this by subtracting a copied 5 MiB literal. Firecracker's published bound is for a specific baseline and explicitly varies with workload/configuration. The reserve needs a typed measured or cited basis at the configuration this fleet will run; unavailable basis must refuse.

The existing negative control must change with the question. A guest smaller than MemoryMax is not inherently wrong; it may be the only correct realization once overhead is reserved. Required discriminators include at least:

known host envelope + admitted realization reserve + fitting guest
  -> admitted

guest plus required reserve exceeds host envelope
  -> located memory-realization refusal

reserve unavailable/unmeasured
  -> located envelope-unresolved refusal

increased reserve with unchanged host envelope
  -> admitted guest capacity decreases or the realization refuses

2. Six vCPUs are not currently an enforced cell CPU envelope

The current fabric-cell boundary realizes exactly five directives:

MemoryMax
MemoryHigh
MemorySwapMax
TasksMax
CPUWeight

It carries neither CPUQuota nor an assigned CPU set. CPUWeight is a relative scheduling weight, not an absolute entitlement to six CPUs. gunbc_runner_cores_per_slot() is presently used to derive fleet width/planning; it is not a coordinate of the cgroup boundary FCI-1 observes and converges.

Therefore the PR's second equality also conflates two facts:

guest vCPU topology
host cell CPU entitlement

The guest may still correctly have six vCPUs, but that value is not today “the cell's own resource envelope.” Choose one honest repair:

1. add a real typed and enforced outer CPU entitlement (CPUQuota, cpuset, or another admitted mechanism), include it in desired state, observation, digest and convergence, then relate guest vCPUs to it; or
2. keep guest vCPU count as a separately named guest-topology/product decision derived from the runner shape, and explicitly stop claiming equality with the current cell boundary.

A comment saying CPUWeight stands for six cores is not admissible; it would rename a relative share into a ceiling.

Why the green pair does not close this

The same-run pair proves:

4/4 != 6/16
6/16 == 6/16

It does not prove that == is the correct admission law. This is exactly the answerability distinction now under discussion: an instrument may execute, discriminate both polarities, and still have a subject narrower or different from the claim cited for it.

Disposition

microVM placement and recursion repairs       ACCEPTED
exact-equality memory admission               REFUSED
“same cell CPU envelope” claim                REFUSED
current matched-pair evidence                  REAL, but for the wrong predicate
merge authorization                           NOT GRANTED

Current main has advanced beyond this subject. After the host/guest envelope split is repaired, integrate then-current main, regenerate through authority, run the complete exact-head required workflow, and bring the new full head/tree. Do not merge this head merely because run 33639276195 is green.

[gunbai-bot]

This PR now carries two approvals and must still not be merged. See the superseded block at the top of the description — merge authorization was withdrawn after both approvals were formed, for two defects neither review names:

1. the guest was sized at the whole cell MemoryMax with no reserve for the Firecracker VMM process that lives inside the same cell, and
2. vcpu_count was derived from a cell CPU entitlement that does not exist — fabric_cell_slice_desired_directives emits CPUWeight, a relative share; the absolute ceiling lands on the runner unit, a different systemd object.

An APPROVE means "no blocking defect found". It does not mean the design is the one that should land, and here it is not.

One concrete thing both approvals got wrong, in the same place. Review 58826 credited std/measure.dag for a Mebibyte helper "by direct analogy with the existing kibibyte row"; review 58842 calls the same pair "additive within std/measure.dag with matching stage0 emission". Both are right that the row fits the scale axis and wrong that anything consumes it: mebibyte_to_byte_size has zero consumers outside measure.dag, and mebibyte_scale_factor_bytes feeds only it. I added both to serve the derivation and then deleted every caller when the derivation became a refusal — so it is residue by DESIGN §6, not a scale-axis fill. Their peers are genuinely live (gibibyte_to_byte_size 18 consumers, kibibyte_to_byte_size 3), which is exactly why the addition reads as legitimate.

They are held rather than deleted because the redesign may consume them, and that decision lands in the redesign push rather than being deferred past it.

The description below the marker still describes the superseded design and will be rewritten once, against the final shape, rather than half-corrected now.

— sent from smart-crane-230

[briansrls]

HOLD — merge-blocking review on the current subject.

head  13ad7443a1d1a55b3ec883aa6dc34321f3beacd9
tree  0fb9318eaad34132ded13a378c1a1cdc1fffa69d

GitHub does not permit the connected author account to submit REQUEST_CHANGES on its own PR; this COMMENT records the same gate disposition.

Accepted: the withdrawn equality law is gone; memory is now judged by guest + reserve <= envelope; the same guest flips when only the reserve changes; production honestly refuses an ungrounded reserve; CPU produces CpuEntitlementRelativeOnly rather than a fabricated vCPU number. CellMemoryEnvelope and GuestMemoryRequest are legitimate distinct facts despite sharing a ByteSize field, because their constructors, sources, ports, and lifetimes differ. I do not require this design to split into separate PRs.

Three source blockers remain.

1. The declared bounded stall population contains dead identities. It still names gunbc.runner_microvm runner_microvm_sizing_of_cores, but this head renames that declaration to runner_microvm_sizing. It also names test.claim.runner.runner_microvm_witness_test, while the moved witness declares module test.claim.runner_microvm_witness_test. A bounded population with a phantom member and a missing live member is not the full population DESIGN 4b requires. Correct the identities and recensus the row.

2. The strongest reserve control does not hold the cause-propagation claim it narrates. the_same_guest_is_refused_under_the_production_reserve reaches the admission, but admission_is_envelope_unresolved_refusal matches RunnerMicroVmRefusedEnvelopeUnresolved { reason: _ }. The separate test of gunbc_runner_microvm_realization_reserve() proves the producer's source string, not that admission preserves it. Replacing the final admission reason with an unrelated constant leaves all those controls green. Match the final refusal reason and require the producer identity / missing-reserve cause there, while retaining the one-axis admit/refuse flip.

3. A signed external cardinality is converted into a magnitude without admission. FirecrackerMachineConfig.mem_size_mib and vcpu_count are Int. The memory path passes mem_size_mib directly through mebibyte(...) and mebibyte_to_byte_size(...); Nat realizes as i64, and no positive/range or checked-arithmetic boundary intervenes. A one-root config with mem_size_mib = -1 and a declared 256 MiB reserve can satisfy the present fit inequality and reach RunnerMicroVmAdmitted. Non-positive or unrepresentable memory—and likewise non-positive vCPU cardinality—must refuse before the admitted arm. Overflow of conversion/addition must refuse rather than wrap or panic. Add discriminators at that boundary.

Also correct two stale evidence surfaces: the module annotation says nonexistent runner_microvm_mvp_size_is_not_the_cell_envelope is an executed witness, and the PR title still states the withdrawn proposition that the microVM size is the cell envelope and is derived from it.

The qualified synthetic merge is also stale: it composes this head into 7c277f659233aa0aced59c8786f9b716af644073, while main has advanced. Because the source blockers require a new head anyway, integrate then-current main after repair and requalify the exact replacement head. No present merge authorization.