Repository navigation
Model the runner microVM in .dag: the prerequisite is a refusal, and it belongs to the topology rather than to virtualization - #9578
Merged
Conversation
…he prerequisite that makes it sound A runner slot's Runner.Listener can be orphaned by a restart and then delete the LIVE incarnation's credentials out of the shared slot directory, killing whatever job is running at its next token refresh. Confirmed at pid grain twice. A microVM per registration has no shared slot directory and no surviving listener, so the defect has nowhere to live. MEASURED ON srv4, touching no CI configuration: Firecracker v1.16.1 aarch64 on Neoverse N1 (which upstream tests continuously), Ubuntu 24.04.4 guest, tap networking with host-to-guest 2/2 at 0.297ms, and actions-runner 2.337.0 registering FROM INSIDE THE VM 5.3 seconds after boot. JIT config is minted on the host from the org GitHub App -- the same path jit-runner.sh uses -- and handed to the guest on a second block device; a one-shot unit runs one job and powers off. NOT yet proven: a workflow job end-to-end, clean poweroff, and the floor's working set inside a VM. THE SHAPE IS ONE VM PER REGISTRATION, NOT PER JOB BODY, and the distinction is load-bearing rather than stylistic: ROOTLESS_DOCKER_CI_PLAN.md isolates the job body and leaves the runner on the host, so it could not have prevented either specimen -- the victim and the killer are both listeners living outside that body. That is a finding against a plan currently awaiting sign-off as a fix for something it does not fix. Adopting an orchestrator is rejected on section 6 grounds: it would replace jit-runner.sh, unit-per-slot and JIT registration, which gunbc.runner_unit already models. THE PREREQUISITE IS THE PART A READER SHOULD NOT SKIP. Under KillMode=process the unit's tracked child becomes the VMM, and an orphaned VMM keeps its guest alive with the same credentials in the same directory -- the identical failure with a heavier process holding it. gunbc.runner_unit already carries the deciding predicate and the measurement behind it (the listener is a GRANDCHILD of MainPID because run.sh does not exec). So this design DEPENDS ON #9401's ExitType=cgroup being deployed rather than substituting for it. Unsolved and named rather than discovered late: cache strategy (sccache over a host UDS and the shared jobserver both assume a shared host), per-VM memory sizing (the 15.0 GiB peak is ONE sample -- the distribution is required, and if the honest size does not fit the slot count that is the finding), the cell resource boundary relocating into the guest, and srv3 unmeasured. Scaffold: the reproduction record in section 9 is temporary by construction, with its dissolution obligation naming a .dag authority rendering it the way runner_unit_file already renders the unit. Landed under explicit operator direction, recorded because a dissolution condition never authorizes its own debt. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Sg8fwMAaPgbsNtns1gpVd9
gunbai-bot
Bot
changed the title
…it belongs to the topology rather than to virtualization
Replaces the markdown design note with the modeling it was describing. A doc
asserting that a microVM closes the credential-orphan class is a claim no
Accepted program can read; a refusal that fires on the fleet's own declared
lifecycle intent is one the substrate checks.
WHAT LANDS
extdeps/virtualization/firecracker.dag cites Firecracker as upstream -- release
v1.16.1/aarch64, /dev/kvm, and its own configuration vocabulary in its own field
names, not renamed.
gunbc/runner_microvm.dag binds it. It reuses product.fabric.isolation's existing
guarantee vocabulary rather than minting a second one -- that module deliberately
leaves the delivering mechanism unnamed as a realization handler, and this is
that handler. The VM configuration is DERIVED from the image, size and credential
transport rather than authored beside them, so the fields a caller could get
wrong independently are consequences instead.
THE CREDENTIAL CARRIER IS THE MEASURED DEFECT, SO IT IS REFUSED BY NAME
Five confirmed specimens on srv4 (slots 04, 08, 13, plus the earlier pair) share
one shape: an orphaned listener from a prior incarnation, logged by systemd as
"remains running after unit stopped", deletes .credentials from the slot
directory a LIVE job is using; the job dies ~45 minutes later at token refresh.
srv4-13 carried two orphan generations racing on one directory.
A per-VM read-only drive has no such sharing to express, so AttemptScopedSecrets
becomes a property of the carrier rather than a promise a handler makes.
JitConfigInSharedSlotDirectory is refused with its own typed cause.
THE TOPOLOGY IS A CARRIED FACT, AND THIS IS THE CORRECTION THAT MATTERS
An earlier revision refused every microVM under an orphanable lifecycle intent,
reasoning that a microVM relocates the orphan to the VMM rather than removing it.
That is sound for ONE topology and wrong for the other:
VmmIsMainProcess the unit execs the jailer, which execs Firecracker,
so the VMM IS MainPID. Killing it destroys the guest.
No kill mode can orphan anything. Guarantee not needed.
VmmUnderLifecycleController a controller stays MainPID to wait for the VMM and
perform teardown and readback. That puts the VMM back
under a parent -- the shape that orphans today.
Guarantee IS needed.
Collapsing these would have refused a correct design and called it safety. The
prerequisite therefore attaches to the topology, not to virtualization, and
gunbc.runner_unit's lifecycle_intent_cannot_orphan is consumed rather than
re-derived.
ONE CONCEPT, ONE VERSION ROW
RunnerGuestImage.runner is the cited ActionsRunnerRelease itself, not a version
string. The MVP image happened to bake 2.337.0 while extdeps.github.actions_runner
pins 2.336.0 with upstream digests -- a second authority for one fact, drifting
the moment either moved. There is now no field in which they can disagree.
EVIDENCE
Ten witnesses, green by execution. The discriminating REDs were established by
mutation, not asserted:
collapse the topology split -> direct_exec_vmm_is_admitted true -> FALSE
topology_is_what_decides true -> FALSE
orphanable_unit_refuses true -> true
bypass the orphan gate entirely -> orphanable_unit_refuses true -> FALSE
cgroup_teardown_admits true -> true
shared_slot_credential_refused true -> true
Each mutation reds exactly the witnesses that encode its claim and leaves the
others standing, so none of the three gates is a constant. Both source files were
restored and verified by sha256 after each run.
MVP PROVEN BY EXECUTION, on srv4: Firecracker v1.16.1, Ubuntu 24.04 guest, tap
networking, stock runner reaching "Listening for Jobs" at 5.3s from boot.
WHAT THIS DOES NOT CLAIM
The model is not the migration. Successor creation gated on sanitation readback,
per-incarnation derivation of tap/MAC/subnet/writable layer (the MVP used
singletons), guest-local jobserver, and sccache -- where a miss compiles as a
child of the sccache server, so a host server would execute the miss outside the
isolation boundary -- are all unmodeled here. No job has run end to end in a VM,
no clean poweroff observed, and the floor's working set in a guest is unmeasured.
Memory sizing is deliberately absent: one 15.0 GiB sample cannot support a cap.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Sg8fwMAaPgbsNtns1gpVd9
gunbai-bot
Bot
changed the title
…not bare Int Review finding (codex/gpt-5.6-sol, review 57217): RunnerMicroVmSize propagated Firecracker's raw `mem_size_mib: Int` inward. Accepted. A bare Int is a second representation of a magnitude std.measure already owns, and product/fabric/envelope.dag -- the module family this VM will eventually answer to -- already speaks HardwareThreadCount and the Memory measure family for exactly these two quantities. Two spellings of one magnitude is the §3 failure, and it is what lets a vcpu count be compared against a memory size with nothing refusing. The raw Int stays at the cited extdeps boundary, which is correct: extdeps models what the API actually accepts. Conversion happens once, at the point the config is rendered. MEBIBYTE RATHER THAN THE ByteSize THE REVIEW NAMED, deliberately. Firecracker's field is denominated in MiB, so `Measure<Memory, Mebi, Nat>` grounds it EXACTLY -- the same authority, one scale along the axis that authority exists to carry, with no inbound multiply to get wrong. Grounding in bytes would restate the unit rather than ground it. The review's principle is right; ByteSize is one scale of it and not the one that fits this field. All ten witnesses re-run green by execution after the change, including guest_image_runner_is_the_cited_fleet_release and both topology arms. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Sg8fwMAaPgbsNtns1gpVd9
Contributor
|
Both findings from review 57217 verified against the code and the authority doc. One accepted and fixed in Finding 1 — accepted, fixed
The finding is right and the reason is stronger than style: One deviation, stated rather than made quietly: I used All ten witnesses re-run green by execution after the change. Finding 2 — rejectedEvery authority this finding cites is absent from
And the pattern called merge-blocking is the corpus idiom: 353
There is a real adjacent rule in DESIGN, under recurring failure modes: "total at the level examined, blind one level down". It warns against a match that is exhaustive over the type it examines while collapsing distinct causes into one arm — the tell being "a If there is a specific DESIGN clause intended here under a different name, quote it and I will act on it. — sent from cool-seal-638 |
Contributor
CI: the two failing checks are not from this change (8th identical sample)Verified on this head ( The sorted failing-identity set hashes to This PR's witnesses are enrolled and passingStated with its derivation, because absence from the log is not evidence on its own — the floor enumerates only non-passing rows (94 here: 47 FAIL, 44 INTERRUPTED, 2 OVER-COST, 1 STALE-QUARANTINE). No passing identity is ever named, so a green witness is invisible by construction. The discovery line is what settles it:
That is consistent with the local evidence: all ten witnesses green by execution, and the discriminating REDs established by mutation — collapsing the topology split reds I am not pushing a fix for the 47. It is a main-wide regression under separate triage, and a fix attempted from this branch would be re-measuring a defect already attributed eight times over. — sent from cool-seal-638 |
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Sep 2, 2026
…olve the coproduct predicates review 57217 named #9578 landed the microVM model with three things still open. This closes them. THE VM SIZE IS THE CELL'S RESOURCE ENVELOPE, DERIVED. FCI-1 freezes `cell-resource-envelope` as an output identity, and this fleet already answers it once in gunbc.runner_slot_allocation gunbc_runner_slot_desired. runner_microvm authored a second one beside it -- 4 vCPU / 4 GiB against a cell declaring 6 cores / 16 GiB -- which is the section 3 failure, and not a harmless one: a guest sized under the cell's ceiling makes the same work die inside a slice that still had room, with the cgroup ledger showing the slice well under its limit while the job died. The size is now derived from that one authority, so there is no second row to drift. THE PREDICATES ARE DISSOLVED INTO THE DECIDING SITE, not rostered. Review 57217's live finding was two Bools classifying coproducts -- jit_transport_is_attempt_scoped over JitCredentialTransport and topology_requires_cgroup_reaching_teardown over VmmProcessTopology. gunbc.non_fold_residue rosters matches carrying a top-level WILDCARD arm; these are total, so the roster is not their form. commit_workflow's CheckRemoval selection is: match the coproduct where the consequence is decided, so a new variant fails to compile at the site that must rule on it. runner_microvm_admission is now that cascade. The two functions I would otherwise have added for the envelope comparison are absent for the same reason. An unresolved envelope and a disagreeing envelope are separate refusal arms. They have different owners and different remedies, and one Bool would have answered for both. std.measure gains mebibyte_scale_factor_bytes and mebibyte_to_byte_size, exact peers of the gibibyte and kibibyte conversions already there -- a fill along the scale axis, not a new concept. Both files move into the runner family directories, where every other runner_*.dag and runner_*_witness_test.dag already lives; they were the only two stragglers. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EN2pmV7GbBZYhCZWYqFbCc
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Sep 2, 2026
…s a ConstructionMechanism where a Disposition belongs main at 4605989 refuses the entire required floor on one line: dag/extdeps/virtualization/firecracker.dag:15:3: error: field 'reason' not found in type 'SingleAuthority' `SingleAuthority` is a variant of ConstructionMechanism, not of Disposition, and it carries no fields at all; the row wrote it as a record with a `reason`. std.disposition's reason-carrying Disposition variant is `Terminal`, which 64 modules already use, and this is the ONLY site in the corpus spelling a Disposition as `SingleAuthority { .. }` -- a census of one, landed by #9578. The blast radius is the point rather than a footnote: the floor is one prepared subject and one fold, so a single module that fails to compile refuses all 2170 resolved modules before any witness executes. That is why no witness identity appears in the failing run and why required_floor_disposition.tsv was never written -- the run did not reach the phase that produces it. It also means the ci_budget_tree question is not answered by this run in either direction: those witnesses did not execute. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EN2pmV7GbBZYhCZWYqFbCc
gunbai-bot Bot
added a commit
that referenced
this pull request
Sep 2, 2026
…s a ConstructionMechanism where a Disposition belongs (#10023) main at 4605989 refuses the entire required floor on one line: dag/extdeps/virtualization/firecracker.dag:15:3: error: field 'reason' not found in type 'SingleAuthority' `SingleAuthority` is a variant of ConstructionMechanism, not of Disposition, and it carries no fields at all; the row wrote it as a record with a `reason`. std.disposition's reason-carrying Disposition variant is `Terminal`, which 64 modules already use, and this is the ONLY site in the corpus spelling a Disposition as `SingleAuthority { .. }` -- a census of one, landed by #9578. The blast radius is the point rather than a footnote: the floor is one prepared subject and one fold, so a single module that fails to compile refuses all 2170 resolved modules before any witness executes. That is why no witness identity appears in the failing run and why required_floor_disposition.tsv was never written -- the run did not reach the phase that produces it. It also means the ci_budget_tree question is not answered by this run in either direction: those witnesses did not execute. Claude-Session: https://claude.ai/code/session_01EN2pmV7GbBZYhCZWYqFbCc Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com> Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Sep 3, 2026
…cracker boundary (#10021) * Reconcile runner_microvm with FCI-1's bounded cell envelope, and dissolve the coproduct predicates review 57217 named #9578 landed the microVM model with three things still open. This closes them. THE VM SIZE IS THE CELL'S RESOURCE ENVELOPE, DERIVED. FCI-1 freezes `cell-resource-envelope` as an output identity, and this fleet already answers it once in gunbc.runner_slot_allocation gunbc_runner_slot_desired. runner_microvm authored a second one beside it -- 4 vCPU / 4 GiB against a cell declaring 6 cores / 16 GiB -- which is the section 3 failure, and not a harmless one: a guest sized under the cell's ceiling makes the same work die inside a slice that still had room, with the cgroup ledger showing the slice well under its limit while the job died. The size is now derived from that one authority, so there is no second row to drift. THE PREDICATES ARE DISSOLVED INTO THE DECIDING SITE, not rostered. Review 57217's live finding was two Bools classifying coproducts -- jit_transport_is_attempt_scoped over JitCredentialTransport and topology_requires_cgroup_reaching_teardown over VmmProcessTopology. gunbc.non_fold_residue rosters matches carrying a top-level WILDCARD arm; these are total, so the roster is not their form. commit_workflow's CheckRemoval selection is: match the coproduct where the consequence is decided, so a new variant fails to compile at the site that must rule on it. runner_microvm_admission is now that cascade. The two functions I would otherwise have added for the envelope comparison are absent for the same reason. An unresolved envelope and a disagreeing envelope are separate refusal arms. They have different owners and different remedies, and one Bool would have answered for both. std.measure gains mebibyte_scale_factor_bytes and mebibyte_to_byte_size, exact peers of the gibibyte and kibibyte conversions already there -- a fill along the scale axis, not a new concept. Both files move into the runner family directories, where every other runner_*.dag and runner_*_witness_test.dag already lives; they were the only two stragglers. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EN2pmV7GbBZYhCZWYqFbCc * The witness fixture's unresolved arm recursed instead of refusing, and the coverage hole gets its second cited instance TWO CHANGES, ONE A REAL DEFECT CAUGHT BY REVIEW 58648. THE UNRESOLVED ARM WAS UNBOUNDED MUTUAL RECURSION. specimen_config's unresolved arm substituted two_root_config(), and two_root_config built three of its four fields FROM specimen_config(). No descent, in a file whose subject is fail-closed refusal, reachable exactly when the cell envelope stops resolving -- the one case the arm existed to handle. It was a fabricated fallback on its own terms as well. 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. That is the absorbing arm DESIGN 5 forbids, and this PR's own module changes split those exact two states into separate refusal arms while the fixture quietly re-merged them. specimen_config -> specimen_resolution, returning RunnerMicroVmConfigResolution with NO fallback arm. All nine witness call sites match it, so an unresolved envelope makes each witness false by its own arm. two_root_config is rebuilt from mvp_sized_config, a plain constructor, so it no longer reaches the specimen at all. THE UNOWNED-MIRROR COVERAGE HOLE GETS ITS SECOND CITED INSTANCE, as an annotation on the witness that already documents it rather than as a new artifact. cli_run.rs IS in HAND_MAINTAINED_STAGE0_FILES; v1_compiler_compiler_tests_rust.rs is NOT, so it is emitted rather than copied. One instance on a hand-authored file is a bookkeeping gap; an instance on a GENERATED mirror says the crate-partition authority does not cover files the regen itself produces. The two differ on exactly the axis that separates those readings, which is why the second is evidence rather than a duplicate. Observed 2026-09-02 when --regen-round-cost refused its partitioned rebuild naming that mirror. Not fixed here: stage0_crate_partition_generated.dag declares itself generated from v2.workflow.rust_crate_partition and not hand-editable. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EN2pmV7GbBZYhCZWYqFbCc * Regenerate std_measure.rs: the mirror of the two Mebi conversions this branch added required-witnesses-build refused this branch: required-ci: regen FAIL generated surface drift: std_measure.rs required-ci: FAILED PHASE regen (1 failure(s)) dag/std/measure.dag gained mebibyte_scale_factor_bytes and mebibyte_to_byte_size in this branch; src/v1/stage0/src/std_measure.rs is its mirror and was never regenerated, so the committed surface did not carry them. PRODUCED, NOT HAND-WRITTEN: installed from the --required-regen candidate tree, which was also the check that std_measure.rs is the ONLY drift (diff -rq against the candidate names that file and no other; the run's own line reads declared_divergent=1 [main.rs], the standing declared divergence, and generated-artifact rostered=35 adjudicated=35 matches=35 drifted=0). ONE ROUND, NOT TWO: std_measure.rs is compiled from source rather than emitted through a seed function, so there is no install-and-rebuild step between the authority edit and the mirror -- unlike the compiler_tests.rs chain, where the emitted text comes from the seed's own compiled-in producer. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EN2pmV7GbBZYhCZWYqFbCc * The guest was sized at the WHOLE cell ceiling, so the slice would OOM its own VM Deriving the guest's RAM from the cell envelope fixed the AUTHORITY question and left the ARITHMETIC one. `machine_config.mem_size_mib` is GUEST RAM, and the Firecracker VMM process that owns the guest lives inside the SAME cell. Setting guest RAM to the cell's entire MemoryMax leaves nothing for the VMM's own resident footprint, so the slice OOM-kills the VM it exists to bound. It is the same class as the authored 4 GiB this module used to carry, inverted. Undersized, work dies inside a guest whose slice had room. Sized at exactly the ceiling, the guest believes it has an envelope the cell cannot honour. The safety property is not that the guest EQUALS the envelope, it is that the guest PLUS its realization FITS INSIDE it, and equality is the specific wrong answer that most resembles the right one -- which is why it survived both authoring and review. The refusal reason one function away already said "one sized above it escapes the boundary the slice exists to hold": the prose and the construction were never checked against each other. So the memory axis REFUSES, naming the missing fact rather than a symptom: guest RAM is the cell envelope MINUS the Firecracker realization's own footprint, and no such quantity is cited in extdeps.virtualization.firecracker. Inventing one would be a fabricated plausible output wearing a derivation's clothes. THE vCPU AXIS IS UNAFFECTED, and the witnesses keep that visible. The core resolution is now a PARAMETER, because gunbc_runner_cores_per_slot is nullary and always resolves -- at the fleet call site no witness input can reach its unresolved arm, so the pair would have been unauthorable. The two arms reach DIFFERENT causes, which is what separates a refusal that reports which fact is missing from one that refuses uniformly. The whole-mebibyte check is DELETED rather than kept for safety: the quantity whose wholeness mattered was the GUEST size, which no longer resolves, and asking it of the envelope would test an operand the code no longer states to Firecracker -- a check whose red cannot be authored. COVERAGE LOSS, STATED AS A LOSS. The admission checks the envelope last, so RunnerMicroVmAdmitted is now unreachable and THE SUCCESS PATH HAS NO EXECUTED COVERAGE AT ALL. The four witnesses that asserted admission now assert they REACH the envelope-unresolved arm -- strictly stronger for the axis each actually tests, since it proves the topology, credential and malformed-VM gates all passed -- but nothing demonstrates that an admissible VM is admitted. Filed as gunbc.guarantee_rung_drop runner_microvm_guest_size_derivation_stall, whose trigger requires BOTH the grounding and the restoration of that witness, so the accept arm cannot go live having never run. Also corrects an annotation this branch was carrying: #10037 gave v1_compiler_compiler_tests_rust.rs an owner, so the second MirrorHasNoOwningPackage instance filed here is CLOSED, and the text no longer claims it is live beside a witness proving it is not. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EN2pmV7GbBZYhCZWYqFbCc * Widen the microVM sizing stall: the CPU axis is unfounded too, and the cell is not what enforces it The row as filed named only the missing Firecracker footprint. That is a subset of the real obstacle, and a trigger naming only it would be satisfied while the CPU axis stayed unfounded -- the exact shape of a trigger naming less than the capability it restores. gunbc.fabric.fabric_cell_effect fabric_cell_slice_desired_directives emits five directives, and its CPU one is CPUWeight: a RELATIVE share that guarantees no amount of anything under contention. 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. So one bounded execution context is realized twice and the two realizations enforce different axes; deriving a guest vCPU count from the cell equates it to a quantity the cell never enforces. The trigger now carries three conjoined clauses -- memory grounding, CPU entitlement or an honest rename of guest topology as a declared product decision, and restoration of the admissible-accept witness -- and states that the controls must return as FIT controls where a SMALLER guest PASSES, since containment and not equality is the safety property. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EN2pmV7GbBZYhCZWYqFbCc * Delete the vacuous microVM witness rather than repair it no_fleet_constructed_vm_is_admissible_while_the_footprint_is_unmodeled was GREEN BY VACANCY. Its unresolved arm returned true, so it returned true without ever reaching runner_microvm_admission -- the fleet constructor derives the size, so an unresolved sizing makes the config unresolved and the witness took that arm every time. It could not fail, and it cleared the floor and two approvals in that state while standing in the PR body as the replacement for five witnesses withdrawn for demonstrating a false claim. A witness whose refusal arm returns true is not a control; it is a restatement of the refusal. Deleted rather than repaired, and the asymmetry is what decides it: a MISSING witness costs nothing while it waits for the redesign, while a GREEN one that cannot fail is active misinformation for as long as it exists and gets cited as coverage. Repairing it would be work against a block being rewritten wholesale; deleting removes a false claim and forecloses nothing, since the redesign authors the honest form regardless -- assert that the resolution IS unresolved AND that its cause NAMES the missing footprint, which has an authorable red. The seven `MicroVmConfigUnresolved => false` witnesses are deliberately left red. Their subject is topology and credentials, so the redesign must judge them against a plain constructor rather than the fleet-constructed config that drags unresolved sizing into them. That is a design requirement carried forward, not a patch owed here. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EN2pmV7GbBZYhCZWYqFbCc * Re-attach the deleted-witness annotation to a declaration: it was stranded at EOF The deletion left its explanatory annotation as the LAST thing in the file, with no module item after it. DESIGN 4c admits only standalone LEADING `//` blocks attached to a module-scope declaration, so the parse phase refused with 17 copies of "source annotation names no subject: no module item follows it" and took the whole floor with it. The wall is right; deleting the last declaration in a file strands any annotation that followed it. The annotation now leads the surviving replacement pair, which is also where it belongs semantically: it explains what happened to the fifth member of that set. One over-correction reverted rather than kept. I also collapsed the blank lines between adjacent comment runs, assuming a run had to sit immediately against its declaration. It does not: 118 files in dag/ separate comment runs with a blank line and parse clean. Only the end-of-file case was ever the defect, so the fix is the relocation alone. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EN2pmV7GbBZYhCZWYqFbCc * Separate the three memory quantities and judge FIT, not equality THE DEFECT. One number answered three different questions. The withdrawn derivation set the guest's RAM to the cell's whole MemoryMax, so the realization reserve was zero and unnamed -- and the Firecracker VMM process lives inside that same cell, so the slice would have OOM-killed the VM it exists to bound. The withdrawn controls were wrong in BOTH directions while looking discriminating: 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, which fits. THE THREE QUANTITIES, now distinct: CellMemoryEnvelope (what the cell is granted), GuestMemoryRequest (what the guest is handed), RealizationReserve (what the VMM process itself costs, inside that cell). The property is containment -- guest + reserve <= envelope -- and a SMALLER guest passing is a requirement of the repair, asserted as such. THE RESERVE IS A PARAMETER, NOT A GLOBAL, and that is what makes the fit controls authorable. Production cannot supply one: no VMM footprint is cited in extdeps.virtualization.firecracker, and it is not a constant -- it scales with guest size, device model and host page size, so upstream documents a measured overhead for one configuration rather than a property of the realization. If the reserve were read from a global, that refusal would be the only reachable outcome and neither fit arm could ever execute -- a wall whose red cannot be authored. Passing it lets a witness declare one from a controlled fixture and drive both polarities while production stays honest. THAT ALSO RESTORES THE ACCEPT ARM. The previous revision left RunnerMicroVmAdmitted unreachable, so the admission's success path shipped unexercised. It executes again under a declared reserve, and the pair that matters most is the_same_guest_is_refused_under_the_production_reserve: the same guest, the same admission, only the reserve changed, and the answer flips. The admission is therefore neither admitting everything nor refusing everything. THE CPU AXIS STILL REFUSES AND IS NOT REPAIRABLE HERE. fabric_cell_effect emits CPUWeight -- a relative share guaranteeing no absolute amount -- while the fleet's absolute CPUQuota lands on the runner UNIT, a different systemd object. Either an absolute cell entitlement becomes real, which is a change to fabric_cell_effect, or guest topology is declared as its own product decision. The sizing names which axis is unavailable rather than refusing uniformly. An earlier comment claiming "the vCPU axis is not what is blocked" was FALSE and is corrected: a resolved core count is a fact about the host survey, not a cell entitlement. The stall row's third clause is DISCHARGED -- the accept arm executes -- and the row says explicitly that PRODUCTION reaching it is not discharged and not claimed. mebibyte_to_byte_size is now genuinely consumed, by the fit comparison; four reviews had credited it while it had no callers at all. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EN2pmV7GbBZYhCZWYqFbCc * Close the fail-open at the signed Firecracker boundary; re-census the stall population BLOCKER 3, AND IT IS THE SERIOUS ONE. FirecrackerMachineConfig carries vcpu_count and mem_size_mib as SIGNED Int -- upstream's shape, faithfully modeled. The admission took mem_size_mib straight through mebibyte -> mebibyte_to_byte_size -> GuestMemoryRequest with nothing between the signed external value and the magnitude, and `Nat` downstream does not rescue it because the realization is i64. So a config with mem_size_mib = -1 satisfied -1 MiB + 256 MiB <= 16 GiB, reached GuestFitsWithinCell, and was 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 turns the signed pair into validated magnitudes or a typed refusal BEFORE fit and before admission. 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, while a smaller "reasonable" ceiling would be unstated policy wearing a representability argument's clothes. The addition is GONE rather than guarded. `guest + reserve <= envelope` is the law, but evaluating the left side can exceed the representable range on a hostile value and wrap, answering the wrong question silently. The comparison is now by subtraction -- guest <= envelope - reserve, with reserve-exceeds-envelope split out so the subtraction never runs below zero -- which cannot overflow for any non-negative inputs. Five witnesses, and the fifth is not optional: negative memory refuses, zero memory refuses, non-positive vCPU refuses, unrepresentable memory refuses, AND a small positive guest is still ADMITTED. Without the last one the four refusals are satisfied by an admission that refuses everything. BLOCKER 2. admission_is_envelope_unresolved_refusal accepted RunnerMicroVmRefusedEnvelopeUnresolved { reason: _ } -- it established the disposition and DISCARDED the located cause, so it stayed green under a mutation where the producer names the missing reserve and the admission returns a bare "unresolved". A witness on the producer cannot close that: it establishes what the producer emits, not that this path preserves it. The recognizer now matches the reason and requires the Firecracker identity AT THE ADMISSION. BLOCKER 1. The bounded population named runner_microvm_sizing_of_cores, which the previous commit deleted, and gave the witness module an intermediate `.runner` segment it does not declare. A phantom member beside an omitted live one means the row never carried the population 4b requires, so it is RE-CENSUSED from the module's declarations rather than spot-repaired -- the property that failed is completeness, and two typo fixes would leave completeness unestablished. The membership rule is now written into the row so it is checkable: a symbol is a member when, in PRODUCTION, it cannot reach its intended answer. Also removes an annotation citing runner_microvm_mvp_size_is_not_the_cell_envelope as an executed statement. That declaration does not exist -- it went with the withdrawn equality design -- and an annotation asserting a machine fact no Accepted program can read is what 4c forbids. Removed rather than repointed, because the claim belonged to a design that no longer stands. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EN2pmV7GbBZYhCZWYqFbCc * Move the subtraction rationale to module-item grain, and control the split it depends on The floor refused #10021's parse phase at six consecutive lines: the annotation explaining why guest_memory_fits compares by subtraction was written INSIDE the function body, and DESIGN 4c admits only standalone leading blocks attached to module-scope declarations. The prose is unchanged in substance and now leads the declaration it explains, which is the nearest grain the substrate admits. It also gains the two things a reader needs in order not to undo the design: why the addition is absent (there is no overflow to handle because the operation that could overflow does not exist -- rung 4, not a checked-add guard at rung 1), and that the reserve-exceeds-envelope split is load-bearing for that claim rather than a redundant early-out. That split had no control, so it gets one: a_reserve_larger_than_the_whole_envelope_admits_no_guest declares a reserve larger than the envelope and asserts the refusal. Its RED is authorable -- delete the split and the subtraction runs below zero -- which is what makes it evidence rather than decoration. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EN2pmV7GbBZYhCZWYqFbCc --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Sep 5, 2026
…n failure TWO REVIEW FINDINGS, BOTH REAL, AND THE FIRST IS THE SAME BUG FOR THE THIRD TIME. ACTIVATION, AGAIN. The original defect was a regular file in multi-user.target. wants/, which systemd skips because it is not a symlink. The repair moved to a drop-in and named it `10-gunbc-runner-agent.service` -- which systemd skips because it does not end in `.conf`. Two mechanisms, one outcome: an activation file that is written, looks right, and is never read. The suffix is now a named row so the next reader sees why it exists. THE WITNESS ALREADY DEMANDED IT AND WAS NEVER RUN. the_agent_is_pulled_in_by_a_ drop_in_systemd_will_actually_read asserts `.conf` in the path. It went RED in CI at 103bc7b and said so plainly (adjudication BLOCKING phase=floor ... returned Bool(false)), before any reviewer looked. The defect survived because this lane reported "compile clean" as though that were the gate, and dispatched a host run against a head whose required floor was failing. A typecheck is not a consumer; DESIGN 5 names this exactly, and the machinery that would have caught it was working the whole time. THE CONSOLE WAS DISCARDED EXACTLY WHEN IT MATTERED. The probe routed the VMM through run_shell_command_capture, whose classifier returns ProcessRefused { exit_code, stderr } on a non-admitted exit and DROPS stdout -- and a Firecracker guest's serial console arrives on stdout. So a guest that panicked and was then killed by its deadline lost its panic message, and the receipt labelled the surviving stderr "the console": a fabricated label over missing evidence, which DESIGN 5 forbids by name. The repair is a second function rather than a widened type. run_shell_command_ observe returns the raw triple and lets the caller classify; capture is now implemented over it, so there is one place a process is run instead of two. "What did this print if it succeeded" and "what did this print, especially when it failed" are different questions, and only the second is this probe's. Every failing verdict arm now carries the console, and BootVmmFailed joined as its own arm rather than being folded into a refusal that hid the exit code. A THIRD FIX, WHERE THE TEST WAS WRONG AND THE CODE WAS RIGHT. the_config_ document_carries_upstreams_own_key_spelling asserted `"network-interfaces":[]`; the emitter writes `": "` with a space, so it failed while every key it exists to check was correct. It is narrowed to the key spellings, which are its subject. A witness that reds on formatting it does not own is a change detector wearing a check's clothes, and the emptiness it reached for is already covered structurally by the witness that COUNTS interfaces instead of matching bytes. Also: the note claiming #10525's install "had never run on any host" is corrected where it was written. The observation was firecracker=absent at the executor-owned path ON srv2; #9578 reports an MVP executed on srv4 at this same version, so a binary existed there outside the modeled path. One host's absence is not a fleet's history. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
briansrls
added a commit
that referenced
this pull request
Sep 5, 2026
* Model the runner guest image as a built artifact, and build it without root gunbc.runner_microvm says WHAT makes two guest images the same image. Nothing said how bytes answering to that identity come to exist, so no host could produce one. This is that procedure, and it consumes the identity rather than restating any field of it: the image path is derived from all four, so a runner bump cannot land on the path the previous release's image occupies. THE BUILD NEEDS NO PRIVILEGE, and that is a property of the mechanism rather than a permission we decided to do without. The conventional path -- loop device, mount, root copy, unmount -- is three privileged mechanisms, each of which would have to be granted in sudoers on every runner host. mke2fs -d populates the filesystem from a directory in userspace, so none of the three is reached and there is nothing to grant. What that costs is stated in the module rather than hidden: an unprivileged extraction cannot restore ownership, setuid bits or device nodes. All three look survivable in THIS guest -- init is uid 0 regardless, the runner and job run as root, and the kernel mounts devtmpfs over /dev -- and survivable is not proven. The boot is the measurement, it fails loudly if any of them mattered, and that failure is the evidence that would justify buying root rather than a reason to have bought it up front. THE BASE ARTIFACTS CARRY PROVENANCE, NOT A FABRICATED PIN. Upstream publishes its CI kernel and rootfs with no digests beside them. Measuring one is a receipt in THIS layer, never a row appended to extdeps.virtualization. firecracker -- an observed digest written there would look like something the vendor published. The vocabulary is gunbc.fleet_host_key_enrollment's, because it is the same problem over bytes instead of keys: a digest taken from the first fetch grounds every later fetch against the first one and nothing more. Only a CONTRADICTED pin refuses; first contact reports what arrived so a row can be authored from it, and an unreadable file is a third state rather than a lenient second. THE GUEST AGENT IS A UNIT FILE, NOT A SCRIPT. The poweroff is ExecStopPost= rather than a second ExecStart=, and the placement is the property: systemd runs it on both arms, so a guest whose job FAILED still stops existing. Appended to the main command it would run only on success, and the one VM that most needs to disappear -- the one that failed holding a credential -- is exactly the one that would stay up. StandardOutput=journal+console for a structural reason too: a guest that powers off takes its journal with it. The two fleet-converge modes are how a named host is reached at all. observe reports and builds nothing; converge builds. Fusing them would leave no way to ask a host what it holds without changing what it holds. Their step budget is its own constant at 30m rather than the shared aux 5m, which the Spark serving envelope one section up already explains: that value is multiplied by step count in the job backstop, so raising it inflates every unrelated step fleet-wide. It is stated as an envelope and not a measurement -- none of the three downloads has a modeled byte size and throughput to either origin has never been measured -- and carries its dissolve-on. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN * Boot the guest image: the sizing repair, and the measurement the rootless build owed Slice 1 modeled the image and could not boot it, for two independent reasons. FIRST, NOTHING COULD BE SIZED. gunbc_runner_microvm_vm_config returned MicroVmConfigUnresolved on every production path: the cell grants a RELATIVE CPU share and no absolute quantity, so no entitlement existed to derive a vCPU count from. The module named two honest repairs and this takes the second -- making an absolute cell entitlement real is a change to fabric_cell_effect, a fabric decision wearing a runner module's clothes. So the guest's topology is declared HERE as this fleet's own fact. The cell did not stop mattering; it stopped SIZING. guest_memory_fits still decides containment at admission. The cell BOUNDS the guest, it does not dimension it -- those were one function and they were two facts. THE DECLARATION WITHDRAWS ITSELF. The day the cell grants an absolute entitlement, the declared size is a stale answer to a question that has become derivable, and a stale answer that keeps returning successfully is what would stop anyone from noticing the repair is available. That arm refuses and names the repair, which is what keeps this from being the absorbing fallback DESIGN section 5 forbids: not a widened substitute for a computation that failed, but a product fact standing where no computation exists, retracting the moment one does. Both arms are driven; an implementation returning the declaration on both passes the control and reds on the discriminating test. runner_microvm_mvp_size is FOLDED IN rather than left beside it. It carried this exact configuration as "a RECORD OF ONE BOOT, not a sizing anyone may provision against", retained as the only configuration known to have started a VM. Once this fleet provisions at a declared size, the only defensible number to declare is the one that has booted -- two rows holding identical values is the nicknaming section 3 forbids. The number did not change; its STANDING did. SECOND, A GUEST WITHOUT A TAP WAS INEXPRESSIBLE. The builder required a device and a MAC, so a boot smoke could only be spelled by naming a device that does not exist -- Firecracker would refuse at device setup and the failure would read as an image defect. A guest that cannot reach the network is not a degraded runner, it CANNOT REGISTER, so RunnerMicroVmNetworking says which kind of VM it is instead of leaving an argument blank. THE PROBE IS THE PROOF OBLIGATION THE ROOTLESS BUILD OPENED. runner_guest_image builds without root and states that this restores no ownership, no setuid bits and no device nodes, argues all three survivable here, and says plainly that survivable is not proven. A guest that boots and prints its runner's version has shown the kernel found a root filesystem, init came up, systemd reached its target and the runner binary is executable -- the set an ownership or device-node loss would have broken. A guest that does not fails loudly on a captured console. IT IS A PROBE AND NOT A PROVISIONER. Admission still refuses every production configuration because the VMM's own reserve is uncited; this boots ONE VM outside any cell to observe whether the image works. Reading its success as permission to provision would be reading a smoke test as a capacity decision. It boots a COPY: a root drive is attached read-write, so booting the artifact would mutate the bytes whose digest the build receipt just recorded. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN * Repair guest agent activation, and put the VM's lifetime in the host's hands TWO DEFECTS, AND THE SECOND IS ONLY VISIBLE BECAUSE OF THE FIRST. ACTIVATION. The merged image "enabled" its guest agent by writing the unit's bytes a second time into multi-user.target.wants/ as an ordinary file, under an annotation asserting systemd resolves such an entry exactly as it would an enable symlink. THAT CLAIM IS FALSE. systemd's dependency loader (src/core/load-dropin.c, process_deps) skips every entry in a .wants/ or .requires/ directory that is not a symlink, logging "dependency dropin ... is not a symlink, ignoring". The agent was never pulled into the boot: the image would have reached multi-user with nothing running. HOW IT SHIPPED IS WORTH RECORDING, because the mechanism is general. The false claim lived in an ANNOTATION, which DESIGN 4c says no Accepted program can read, so nothing could go red on it. The witness that "covered" it asserted WantedBy=multi-user.target appeared in the unit TEXT -- true, and silent about whether the placement systemd actually reads was correct. A correct assertion over the wrong subject. Reviewers reproducing it also observed that BOTH systemd-analyze runs exit 0, so the exit status would not have caught it either; only the diagnostic text distinguishes them. THE REPAIR IS A DROP-IN, NOT A SYMLINK, and the choice is reasoned rather than convenient. A symlink is the closer analogue of systemctl enable and is a file KIND this build cannot create -- Filesystem.Write writes regular files -- so reaching for one means minting an `ln -s` builder and making the image depend on a second mechanism. systemd already documents a fragment that expresses the dependency and IS a regular file honestly used as one: <target>.d/*.conf carrying [Unit] Wants=, merged by the ordinary drop-in path, no symlink requirement. extdeps.systemd.unit_file already modeled SystemdDropIn; the first implementation invented a placement instead of using it. The unit keeps its [Install] section and that is not a second authority: the section says which target the agent BELONGS to, so systemctl enable inside a running guest still works, while the drop-in is what activates it in an image nobody enables. Both read runner_guest_agent_target, so they cannot disagree. TEARDOWN. The probe's claim that a VM "powers itself off" rested entirely on the agent's ExecStopPost=, which covers only the arm where the agent STARTED -- and the defect above is precisely an agent that never starts. A kernel panic before userspace, a hung init, or a guest that never reaches its target present the same ownership problem, and in all of them the VMM holds a guest indefinitely. So the deadline is now the HOST'S, imposed on the VMM process where no guest behaviour can extend it, and it escalates to KILL unconditionally: a bare timeout sends TERM and then waits, so a wedged VMM outlives the bound it was supposed to be under, and a deadline the subject may decline is the escape hatch DESIGN 5 refuses. A step timeout is not a substitute -- it kills the step and can leave the VMM it spawned running, which is the uncontrolled VM this must not create. Exit 124 is timeout's own answer that the bound FIRED, which is a different event from a VMM that ran and failed, so it is its own verdict rather than folded into the failure arm. Both defects now carry regression controls written against the mechanism rather than the text: one asserts the drop-in systemd will actually read, one reds if any placement ever returns to a regular file in a .wants/ directory, and one distinguishes a killed-by-deadline guest from a failed one. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN * Regenerate fleet-converge.yml for the microvm_boot_probe mode Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN * Fix the activation defect properly, and stop discarding the console on failure TWO REVIEW FINDINGS, BOTH REAL, AND THE FIRST IS THE SAME BUG FOR THE THIRD TIME. ACTIVATION, AGAIN. The original defect was a regular file in multi-user.target. wants/, which systemd skips because it is not a symlink. The repair moved to a drop-in and named it `10-gunbc-runner-agent.service` -- which systemd skips because it does not end in `.conf`. Two mechanisms, one outcome: an activation file that is written, looks right, and is never read. The suffix is now a named row so the next reader sees why it exists. THE WITNESS ALREADY DEMANDED IT AND WAS NEVER RUN. the_agent_is_pulled_in_by_a_ drop_in_systemd_will_actually_read asserts `.conf` in the path. It went RED in CI at 103bc7b and said so plainly (adjudication BLOCKING phase=floor ... returned Bool(false)), before any reviewer looked. The defect survived because this lane reported "compile clean" as though that were the gate, and dispatched a host run against a head whose required floor was failing. A typecheck is not a consumer; DESIGN 5 names this exactly, and the machinery that would have caught it was working the whole time. THE CONSOLE WAS DISCARDED EXACTLY WHEN IT MATTERED. The probe routed the VMM through run_shell_command_capture, whose classifier returns ProcessRefused { exit_code, stderr } on a non-admitted exit and DROPS stdout -- and a Firecracker guest's serial console arrives on stdout. So a guest that panicked and was then killed by its deadline lost its panic message, and the receipt labelled the surviving stderr "the console": a fabricated label over missing evidence, which DESIGN 5 forbids by name. The repair is a second function rather than a widened type. run_shell_command_ observe returns the raw triple and lets the caller classify; capture is now implemented over it, so there is one place a process is run instead of two. "What did this print if it succeeded" and "what did this print, especially when it failed" are different questions, and only the second is this probe's. Every failing verdict arm now carries the console, and BootVmmFailed joined as its own arm rather than being folded into a refusal that hid the exit code. A THIRD FIX, WHERE THE TEST WAS WRONG AND THE CODE WAS RIGHT. the_config_ document_carries_upstreams_own_key_spelling asserted `"network-interfaces":[]`; the emitter writes `": "` with a space, so it failed while every key it exists to check was correct. It is narrowed to the key spellings, which are its subject. A witness that reds on formatting it does not own is a change detector wearing a check's clothes, and the emptiness it reached for is already covered structurally by the witness that COUNTS interfaces instead of matching bytes. Also: the note claiming #10525's install "had never run on any host" is corrected where it was written. The observation was firecracker=absent at the executor-owned path ON srv2; #9578 reports an MVP executed on srv4 at this same version, so a binary existed there outside the modeled path. One host's absence is not a fleet's history. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN * Record that srv2's KVM writability is a shell session, not convergence The operator asked whether the /dev/kvm grant was modeled or done by hand. It is modeled -- EnsureSupplementaryGroupMembership renders an argv and a sudoers line committed for every host, and provisioning/srv2/gunbc-ghrunner.sudoers:84 is verbatim the command I typed. So the hand action did not fill a modeling gap; it executed a row the model already owns, out of band, and the annotation in runner_microvm_host_ready that recorded "executor NOT in kvm" was true when written and false an hour later because I changed the host. No Accepted program reads an annotation, so nothing could ever go red on the stale sentence. It was found only because the operator asked. The annotation now states the observation as dated and attributed, says plainly that srv2 reads kvm=writable while every other host does not, and names the gap that permitted the hand step: EnsureSupplementaryGroupMembership is AUTHORIZED and never APPLIED. runner_host_privileged_operations feeds only the sudoers renderer, and this reconciler explicitly disclaims the grant -- so the operation is granted by one module, disclaimed by another, and executed by neither. The refusal here stays correct; the missing applier is an ownership decision about host actuation, not this module's to take unilaterally. srv1/srv3/srv4 are deliberately left unconverged rather than hand-patched to match srv2. They will refuse at the boot probe with kvm=present-not-writable, which is the informative failure. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN * Drop the dead image parameter from the boot probe's config builder review 61096 (non-blocking) found runner_microvm_boot_probe_config taking an image: RunnerGuestImage it never references. Correct, and checking why it was dead was worth more than the fix: identity IS threaded, one step earlier, by runner_microvm_boot_probe_stage_commands, which copies runner_guest_image_path(root, image) onto the FIXED probe path the config then boots. The question that mattered was whether a failed copy could leave the probe booting a stale probe-rootfs.ext4 from an earlier image while the receipt named the new one -- a silent wrong answer that would be near-impossible to see after the fact. It cannot: staging is sequenced before the boot and any non-ExitSuccess refuses instead of booting whatever the previous run left behind. So the parameter is dropped rather than threaded; threading it would invent a use for a value the fixed probe path deliberately does not need. An annotation now states why the function takes no identity, so it is not re-added as an apparent improvement. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN * Rebuild the guest tree with rm -rf, which its annotation already claimed fleet-converge run 33993440148 on srv2 failed at rm -f .../tree/ubuntu-24.04-aarch64-runner-2.336.0 rm: cannot remove '...': Is a directory runner_guest_tree_commands staged the tree with rm_force_command -- `rm -f` -- on a DIRECTORY it rebuilds every run. It could only ever succeed on a host that had never built before, which srv2 was at run 33985760921 and will never be again. An idempotence defect invisible on exactly one run per host is the shape to expect from staging only ever exercised on fresh state, and the earlier SUCCESS was the misleading result, not this failure. The substrate was correct. rm_force_command's own row says in terms that it never recurses and REFUSES a directory precisely so a mistaken call cannot destroy a tree; it fail-closed as designed. Had it accepted -rf silently, the build would have passed and produced an image carrying an earlier release's files wherever the new one did not overwrite them. What was wrong was this caller, whose annotation asserted "The removal is `rm -rf`" while the code issued `rm -f` -- a §4c annotation claiming the exact property that was missing, which no Accepted program can contradict. That is the third falsified annotation in this lane, and the second found only by execution. No new vocabulary: coreutils_rm_force_recursive_flags already existed, so rm_recursive_force_command is built from it, enrolled in extdeps.exec.command's admit_callers (the seal refused the mint until it was, working as intended). While there, consolidated a §3 fork found in the same file -- rm_program and coreutils_rm_binary_name, both "rm" -- rather than adding a third spelling; rm_program had no callers outside the module. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN * Compare the built image against itself, not against the base rootfs's pin fleet-converge run 33995287883 on srv2: the rm -rf repair worked -- the tree rebuilt over the leftover directory and the drop-in landed at the repaired path (multi-user.target.d/10-gunbc-runner-agent.service.conf) -- and the build then failed with guest-image=CONTRADICTS-PIN expected=c61b6ff3... (the BASE ROOTFS's pin) observed=369bff28... (the built image) Both image_digest sites passed runner_guest_base_rootfs_artifact as the artifact whose pin to compare against, while observing the BUILT IMAGE's bytes. Those are different files by construction, so the comparison could only ever contradict. IT WAS DORMANT UNTIL AN UNRELATED ROW WAS FILLED IN. At run 33985760921 the rootfs was still Unpinned -- that run is what measured it -- so the mismatched comparison rendered as a REPORT and refused nothing. Committing the pin ARMED a check that had been wrong since it was written. That is the third defect in this lane whose common shape is a check that could not fail in the state it was written in: the .conf witness passed while the image was inert, rm -f worked on a host that had never built, and this reported instead of refusing while the rootfs had no pin. In each case some later, unrelated change armed it. The correct descriptor already existed but only INLINE at the render site, so "what artifact is this digest about" had two answers and the two verdict sites took the wrong one. It is now one row, runner_guest_built_image_artifact, used by all three. Its integrity is permanently Unpinned: a built image has no pin to verify against -- its digest is a receipt of the build that just ran -- and pinning it would demand byte-reproducible mke2fs output and red on every legitimate change to the tree. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Replaces the markdown design note this PR opened with — the operator asked for the modeling itself, not a document describing it. A doc asserting that a microVM closes the credential-orphan class is a claim no
Acceptedprogram can read; a refusal that fires on the fleet's own declared lifecycle intent is one the substrate checks.What lands
dag/extdeps/virtualization/firecracker.dag— cites Firecracker as upstream (v1.16.1/aarch64,/dev/kvm), keeping its configuration vocabulary in its own field names rather than renaming it.dag/gunbc/runner_microvm.dag— the binding. It reusesproduct.fabric.isolation's existing guarantee vocabulary rather than minting a second one; that module deliberately leaves the delivering mechanism unnamed as a realization handler, and this is that handler. The VM configuration is derived from the image, size and credential transport, so fields a caller could get wrong independently are consequences instead.The credential carrier is the measured defect, so it is refused by name
Five confirmed specimens on srv4 (slots 04, 08, 13, plus an earlier pair) share one shape: an orphaned listener from a prior incarnation — logged by systemd as
remains running after unit stopped— deletes.credentialsfrom the slot directory a live job is using; the job dies ~45 minutes later at token refresh. srv4-13 carried two orphan generations racing on one directory.A per-VM read-only drive has no such sharing to express, so
AttemptScopedSecretsbecomes a property of the carrier rather than a promise a handler makes.JitConfigInSharedSlotDirectoryis refused with its own typed cause.The topology is a carried fact — the correction that matters
An earlier revision of this module refused every microVM under an orphanable lifecycle intent, reasoning that a microVM relocates the orphan to the VMM rather than removing it. That is sound for one topology and wrong for the other:
VmmIsMainProcessVmmUnderLifecycleControllerCollapsing these would have refused a correct design and called it safety. The prerequisite attaches to the topology, not to virtualization, and
gunbc.runner_unit'slifecycle_intent_cannot_orphanis consumed rather than re-derived. Caught in review by the side-chat, not by me.One concept, one version row
RunnerGuestImage.runneris the citedActionsRunnerReleaseitself, not a version string. The MVP image baked 2.337.0 whileextdeps.github.actions_runnerpins 2.336.0 with upstream digests — a second authority for one fact, drifting the moment either moved. There is now no field in which they can disagree.Evidence
Ten witnesses green by execution. The discriminating REDs were established by mutation, not asserted:
direct_exec_vmm_is_admittedtrue→falsetopology_is_what_decidestrue→falseorphanable_unit_refusestrue→trueorphanable_unit_refusestrue→falsecgroup_teardown_admitstrue→trueshared_slot_credential_refusedtrue→trueEach mutation reds exactly the witnesses encoding its claim and leaves the others standing, so none of the three gates is a constant. Both source files were restored and verified by sha256 after each run.
MVP proven by execution on srv4: Firecracker v1.16.1, Ubuntu 24.04 guest, tap networking, stock runner reaching
Listening for Jobsat 5.3s from boot.What this does not claim
The model is not the migration. Unmodeled here: successor creation gated on sanitation readback (
Restart=alwayswould start the next VM merely because the VMM exited); per-incarnation derivation of tap/MAC/subnet/writable layer — the MVP used singletons, which is a valid single-VM proof and not a fleet topology; guest-local jobserver; and sccache, where a miss compiles as a child of the sccache server, so a host server reached from a guest would execute the miss outside the isolation boundary.No job has run end to end in a VM, no clean poweroff observed, and the floor's working set in a guest is unmeasured. Memory sizing is deliberately absent — one 15.0 GiB sample cannot support a cap.
CI
The 47 failing witnesses on this branch are not from this change. The sorted failing-identity set hashes to
1a3b72ff1e3f5332cdf1090e47dfdd8187f6ff80a870f4f48bb64e4c76964972, byte-identical across six independent samples — this PR, #9531, #9568, #9434, and main itself — and originates from #9106, which this branch's base inherits. Verified by merge-base ancestry, and no failing identity resolves to a file this PR touches.