Repository navigation
Runner micro-VM: a built image is not-pinnable, and the road to running jobs in the VM - #10628
Merged
Merged
Conversation
fleet-converge run 33996923229 built the guest image and its receipt printed guest-image=unpinned-first-contact sha256=8fcf... (author this as ArtifactDigestPinned with FirstObservedOnFetch provenance) beside the image THAT BUILD had just produced. Following that advice pins a digest which legitimately changes whenever the tree does, and would demand byte-reproducible mke2fs output to stay green -- the module forbids exactly that, three lines away, in the row declaring the artifact. One arm was answering two questions. ArtifactDigestUnpinned covered both "fetched, and a pin should be authored from this" (advice correct) and "built here, and no pin can ever be authored" (advice actively wrong). They are now distinct: ArtifactDigestNotPinnable on the integrity side, ArtifactBuildReceipt on the verdict side, rendering "build-receipt sha256=... (this build's output; not a pin, and not to be authored as one)". Because the coproduct is closed and elimination exhaustive, the new arm forced every consumer to answer for it rather than falling through a default. The control the_built_image_reports_a_receipt_and_never_advises_authoring_a_pin has an AUTHORABLE red: give runner_guest_built_image_artifact the Unpinned arm instead and it goes red on both halves, because that arm is the one carrying the pin advice. It asserts the arm AND that the rendered text never names ArtifactDigestPinned -- asserting only that the text differs would pass on any rewording. Worth recording how this survived: three reviews approved this module while the receipt was advising a reader to do what the module forbids. It took a real run's output to see it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
…y applied TWO THINGS THE OPERATOR'S QUESTION FOUND. 1. THE PRIVILEGED OPERATIONS WERE AUTHORIZED AND NEVER APPLIED. executor_privileged_operation_argv had NO production consumer -- only witness tests. runner_host_privileged_operations fed only the sudoers renderer, which grants PERMISSION to run each argv, and runner_microvm_host_ready explicitly disclaims the KVM grant as belonging to the sudoers roster. Granted by one module, disclaimed by another, executed by neither. The consequence was a hand step per host per operation: srv2's /dev/kvm is writable because an operator typed the modeled argv by hand, verbatim the line already rendered into provisioning/srv2/gunbc-ghrunner.sudoers. gunbc.executor_privileged_apply closes it, and executes THE SAME argv function the sudoers line is rendered from. A separate command builder would let a grant and its execution drift into two spellings of one operation -- the §3 fork the operation type exists to prevent -- so "what is permitted" and "what is executed" are one fact by construction. Elevation is sudo -n, not -E: -n REFUSES when a command is not covered by a NOPASSWD grant, where -E can prompt and would hang a converge on a password nobody will type. Apply stops at the first failure and has no tolerable-failure arm. 2. THE NETWORK SLICE MODELED THE PROCEDURE INSTEAD OF THE FACT. The first draft added five privileged operations and two binary grants (ip, nft) because that is how an operator creates a tap by hand. srv2 was then MEASURED running systemd-networkd enabled and active. A tap is a .netdev file, its address a .network file, the firewall /etc/nftables.conf -- all FILE INSTALLS, which this fleet already grants. The slice collapsed to two operations (InstallFile, SystemdReloadUnit) on binaries already in the roster: the authorization surface SHRANK rather than grew, and the tap became state that survives reboot rather than a command someone ran. The observe-then-act standing the first draft needed is DELETED rather than ported: it existed because `ip tuntap add` fails on an existing device, and no operation here has that shape. MEASURING THE HOST ALSO PREVENTED AN OUTAGE. srv2 runs an active dockerd beside table ip filter / ip nat / ip mangle. In nftables every table hooking a point runs and ANY drop wins, so `policy drop` on our forward chain -- the obvious spelling of "isolate the guests" -- would have dropped every packet dockerd forwards. Policy is accept with an explicit tap-to-tap drop, and a witness goes red if anyone flips it back. Isolation's FIRST wall is arithmetic anyway: a /30 per slot leaves a guest no route to another guest at all. Nine witnesses, each with an authorable red. The three newest cover what the rewrite left uncovered -- User= (without it every launch needs privilege), ConfigureWithoutCarrier (without it the host has no route to an unbooted guest, presenting as a guest bug), and distinct unit paths per slot (without which the second slot silently overwrites the first). systemctl reload earns its own row: it runs ExecReload and the process never dies, where restart would drop every link networkd manages including the host's own uplink -- indistinguishable, from here, from the host going away. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
…sses TWO REVIEW FORKS (review 61223), BOTH DISSOLVED BY DERIVATION. netmask "255.255.255.252" and prefix_length 30 were two spellings of one fact. Only one would move on a re-prefix: the host's .network file would carry the new CIDR while the guest's kernel ip= line kept the old mask, and the guest would boot with a subnet that disagrees with its own gateway. Nothing refuses that -- the guest simply cannot reach the host. The mask now derives from the prefix; the kernel's ip= takes a dotted quad rather than a prefix, so the conversion has to happen somewhere, and doing it from the single prefix row keeps it one fact. supernet "172.30.0.0/16" re-minted what octet1/octet2 already say, and the annotation directly above it DESCRIBED the derivation while the row spelled it out. That one is worse: moving octet2 relocates every slot's network while the NAT rule keeps matching the old /16, so guest traffic silently stops being masqueraded and every per-slot row still reads correctly. ONE VALUE CANNOT PROVE A DERIVATION. Asserting only /30 -> 255.255.255.252 passes for a function that ignores its argument and returns a constant -- which is exactly the row being replaced. The control asserts four prefixes (/30, /24, /16, /31); no constant satisfies all four. A second control pins the invariant the fork actually broke: the guest's dotted quad and the host's prefix must describe ONE subnet, since if they diverge both rows still read correctly alone. THE CI FAILURE WAS MINE AND MY GATE COULD NOT SEE IT. `slot_index: i as Nat` in two witness helpers COMPILED CLEAN in every targeted compile and then errored at claim execution -- "cannot cast Int to Nat" -- taking six witnesses red on the required floor at fa4f529. A bare literal already inhabits Nat, so the cast was never load-bearing; what it did was defer a type error past the only instrument that would not catch it. The root cause is not the cast. It is that this lane's gate all session was `gunbc compile`, which type-checks and never RUNS a claim, so every witness written here had its correctness attested by an instrument structurally incapable of failing on an execution error. claim_executor is now built locally. A local run of the witnesses lane was attempted and ABANDONED, not passed: it reached discovery-authority at 720s and began thrashing (majflt 49 -> 150783, stall_majflt_per_min 23983), matching the memory-pressure signature this repo carries a typed refusal for. That run establishes nothing in either direction. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
…o Int THE CI RED WAS `slot.slot_index as Int` -- CASTING A VALUE THAT IS ALREADY Int. My previous fix was wrong and I reported it as root-caused. CI's first message said "cannot cast Int to Nat", I found an `as Nat` in a witness helper, fixed that, and pushed without running the claims. The real error is "cannot cast Int to Int" in runner_microvm_network, four occurrences. The discriminating evidence I did not have: the five ATTEMPT witnesses passed while the eight NETWORK witnesses errored, and both files used the identical helper -- so the helper was never the cause. The root cause is not the cast. This lane's gate was `gunbc compile`, which type-checks and never RUNS a claim, so every witness written here was attested by an instrument structurally incapable of failing on an execution error. claim_executor is now built and run locally: planned=3533 executed=3533 claims_failed=0, 20 of this lane's witnesses passing. That is the evidence for this commit; compile-clean is not. REVIEW 61259, BOTH FINDINGS, FIXED BY CONSTRUCTION. nft_chain_wire hardcoded `type filter` for every chain, including the postrouting chain whose only rule is a masquerade. nftables permits NAT statements ONLY in a chain of type nat and rejects the WHOLE ruleset otherwise, so the generated file could not load on any host -- taking the tap-to-tap drop down with the NAT rule that was wrong. The chain type is now modeled and paired with its hook. The witnesses could not have caught this: they asserted the rendered TEXT contained the right words, and a ruleset nftables rejects contains them equally well. A string assertion over a config language cannot separate a valid ruleset from an invalid one. runner_microvm_attempt_dir joined an unrestricted NonEmptyStr under the attempt root, so "../shared" escaped it and "a/../b" aliased another attempt's storage -- the storage isolation this module's own header promises, defeatable through the identity it is keyed on. Every path derives from that value, so one traversing id moves the rootfs, JIT drive and config together and cleanup would prove the WRONG subtree empty. AttemptSegment is sole_constructor and REFUSES rather than sanitizes: a rewritten id would silently disagree with the id every receipt names. MicroVmAttempt is sealed too -- a record that merely HOLDS a validated segment can be assembled beside the validator by anyone holding one, so the seal would guarantee only that SOME segment was checked, not that THIS attempt's was. The pair is the unit that must be constructible in one place. The seal proved itself immediately: the test helper's fallback tried to build an AttemptSegment and was refused at compile. Tests now go through microvm_attempt, so they would break if the refusal were deleted rather than passing over a path production cannot reach. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Sep 7, 2026
… was itself a 3c dangling consumer I declined to guess why apply_executor_privileged_operations_wet has no callers, and said so rather than approximating. The answer is one commit and it is not "unfinished wiring" either. #10628 introduced gunbc.executor_privileged_apply WHOLE, expressly to close the authorized-but-never-applied gap. Its own account: executor_privileged_operation_argv had no production consumer, runner_host_privileged_operations fed only the sudoers renderer, and this module "closes it, and executes THE SAME argv function". Then it landed without the caller it was written for. That is DESIGN section 3c precisely, down to the tell that section lists in its own words -- consumption described in the PR body but absent from the diff. So the repair meant to end this class was itself an instance of a neighbouring one. The two readings are the same missing edge, but only the second explains itself: "one wiring remains" says how much code, while "a section 3c dangling consumer" says WHY it is missing and therefore why waiting will not produce it. A reader with only the first may assume someone is mid-way through the wiring. Verified rather than inherited: section 3c exists in the current DESIGN.md and its text names this tell -- my in-context copy predated the section, so citing it from memory would have been a positional guess at a document that had moved. "Executed by neither" stays unchanged, and it is still the sentence that keeps the rung honest. Compile on this base: 26 blocking errors, none in any file this touches; identical to the count before this edit. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01632CTZ8diiLNBQaXobNWKQ
briansrls
pushed a commit
that referenced
this pull request
Sep 7, 2026
…specimens of it (#10703) * File the class a hand-converged host capability belongs to, and both specimens of it A host holds a capability no modeled path put there, so every later green on that host is uninterpretable: a receipt naming it cannot distinguish the modeled path working from a hand-run answering. The harm is not the capability, which usually works. It is that the ambiguity is permanent and travels with every future citation of that host. THE STRUCTURAL CAUSE IS A CAPABILITY AUTHORIZED BY ONE MODULE, DISCLAIMED BY ANOTHER, AND EXECUTED BY NEITHER. runner_host_grants emits EnsureSupplementaryGroupMembership and runner_host_sudoers_content renders permission to run its argv; runner_microvm_host_ready explicitly disclaims applying it and names the result "a hole an operator falls into once per host, by hand". A modeled capability with no executor is a manual step, and the row granting it makes that manual step look converged -- DESIGN section 6's out-of-band actuation wearing convergence vocabulary. Two specimens, both real. srv2 KVM, 2026-09-05: an operator ran the authorized argv by hand, so srv2 has read kvm=writable ever since while every sibling reads present-not-writable. The annotation recording the earlier measurement went stale at that moment and COULD NOT GO RED, because DESIGN section 4c says no Accepted program reads an annotation. It was found only because someone asked whether the grant was converged. srv1 Firecracker, 2026-09-06, this row's occasion: I ran the modeled runner_microvm_host_converge_wet by hand on srv1, installing Firecracker v1.16.1-aarch64 into the executor-owned root -- 30 paths under ~/.local/share/gunbc-firecracker, the root directory itself created by that run, so nothing pre-existed. Digest-verified, idempotent, spending no host grant, and still wrong: srv1 is the canary of record and its capability would not have come from the path that owns it. DECLARING THE DEVIATION WAS CONSIDERED AND REJECTED AS THE WEAKER ARM. Declaring makes the ambiguity legible but leaves every later srv1 receipt carrying a provenance caveat forever; removing it makes the question stop existing. Convergence is only meaningful if it is the only way state arrives. The install was reverted the same day, the enumerated tree removed with nothing adjacent touched, and the honest post-revert state is that srv1 cannot run a guest -- which is what makes the convergence gap visible rather than papered over. The row states the repair in preference order: bake the capability into a host image so the question cannot be asked, or close it in fleet converge. Never an applier bolted beside the disclaiming module, and never the sudoers argv by hand, which is how the srv2 specimen was produced. Distinguishing facts against the neighbours it is easy to misfile as are carried in the row: execution_provenance_loss concerns an observation that may not have run, where here it runs and reports faithfully; head_landed_by_hand concerns an artifact landing uncertified, where this is durable host state with unrecorded origin. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01632CTZ8diiLNBQaXobNWKQ * Locate the class on the ladder, since a row that does not is the stall it describes Review found the filing carried invalid state, harm, distinguishing facts, cause, specimens and a ruling, but never named rung found at, ceiling with reason, or a next-rung trigger. DESIGN section 4b requires all three, and "REPAIR, IN PREFERENCE ORDER" is a product preference rather than a derived ceiling and a capability-shaped trigger. A class that is not located on the ladder never ranks for climbing, which is the untracked stall the same section forbids -- so the omission was the failure this row exists to file, committed in the filing itself. RUNG FOUND AT is BELOW THE FLOOR, which is not a rung: section 4b puts silent wrongness outside the ladder and forbids it outright. Nothing executed distinguishes a converged capability from a hand-placed one -- runner_microvm_host_ready observes WHETHER a host holds a capability and never WHAT PLACED IT, so both produce byte-identical standing. srv2 is the measured proof: writability persisted through every later standing read, the annotation recording the earlier measurement went stale and could not go red, and it surfaced only when a human asked. Provenance has no mechanism at all, not a weak one. CEILING is derived and DIFFERENT FOR TWO HOST SHAPES, because one number would be dishonest. A host whose runtime root is rebuilt from a repository-built image each boot reaches STRUCTURALLY IMPOSSIBLE -- no persistent root survives to hold a capability the image did not place, so the invalid state has no constructor. A mutable persistent host reaches MECHANICALLY PREVENTABLE and no higher, since an operator with sudo can always place state. Section 4b(1) makes a class's rung the minimum across in-scope paths, so while any mutable host is in the population the attainable ceiling is mechanically preventable. NEXT-RUNG TRIGGER names capabilities, at the grain of the loss. The loss is plural -- every host, every capability -- so a trigger naming one host or one grant would be satisfied while the class stayed dead. To mechanically preventable: a host-standing observation reporting, per capability, the identity of the converge run that placed it, such that an unattributable capability is a typed refusal rather than a ready standing. A receipt that merely RECORDS provenance without refusing does not reach it -- srv2 was already recorded in prose and still could not go red. To structurally impossible: a runtime root reconstructed from a repository-built image on every boot. Naming a specific host-image pull request would name an artifact; what discharges the row is the property that a rebooted host cannot carry unattributed capability, whichever change delivers it. docs/design-failure-modes.md regenerated from the authority. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01632CTZ8diiLNBQaXobNWKQ * chore: regenerate drifted generated artifacts (ci auto-heal) Ledger-Repair-Judged: docs/design-failure-modes.md Ledger-Rows-Repaired: docs/design-failure-modes.md capability_arrives_outside_the_converged_path Ledger-Repair-Judged: docs/design-rung-drops.md * Say that the applier is built and unreachable, since "missing" sends the next author to fork it Review 61842 verified independently that apply_executor_privileged_operations_wet still has no callers, which is what made me look at it. It exists. This row's first draft implied the executing half had to be written, and that reading is wrong in the expensive direction. gunbc.executor_privileged_apply is already correct where it matters: it elevates with sudo -n, so a command not covered by a NOPASSWD grant REFUSES instead of hanging on a prompt no automated converge will answer, and it renders its argv through the SAME executor_privileged_operation_argv the sudoers line is rendered from -- so what is permitted and what is executed are one fact by construction rather than by review. It has zero callers anywhere in the corpus, test modules included; the only other occurrence is a decl_ref citation. So DESIGN section 4b(2)'s three-way split lands on its strongest arm. Not "cannot climb further", not "can climb after one grounding", but CAN CLIMB NOW WITH THE MECHANISM ALREADY WRITTEN -- the remaining work is one wiring into the converge path. Recording this is load-bearing rather than tidy. The opposite reading sends the next author to build a second applier beside the first, which is precisely the argv fork that module's own annotation says it exists to prevent: a sudoers line authorizing something nobody runs, beside a command nobody authorized. "Executed by neither" stays accurate and is unchanged -- nothing calls it. What changes is the repair's size and shape. Compile on this merged base: 26 blocking errors, none in any file this touches; the count rose from 22 because main moved under the branch, not because of this edit. The projection is left to heal, per the merge driver's instruction. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01632CTZ8diiLNBQaXobNWKQ * Name why the applier has no caller: the repair that closed this class was itself a 3c dangling consumer I declined to guess why apply_executor_privileged_operations_wet has no callers, and said so rather than approximating. The answer is one commit and it is not "unfinished wiring" either. #10628 introduced gunbc.executor_privileged_apply WHOLE, expressly to close the authorized-but-never-applied gap. Its own account: executor_privileged_operation_argv had no production consumer, runner_host_privileged_operations fed only the sudoers renderer, and this module "closes it, and executes THE SAME argv function". Then it landed without the caller it was written for. That is DESIGN section 3c precisely, down to the tell that section lists in its own words -- consumption described in the PR body but absent from the diff. So the repair meant to end this class was itself an instance of a neighbouring one. The two readings are the same missing edge, but only the second explains itself: "one wiring remains" says how much code, while "a section 3c dangling consumer" says WHY it is missing and therefore why waiting will not produce it. A reader with only the first may assume someone is mid-way through the wiring. Verified rather than inherited: section 3c exists in the current DESIGN.md and its text names this tell -- my in-context copy predated the section, so citing it from memory would have been a positional guess at a document that had moved. "Executed by neither" stays unchanged, and it is still the sentence that keeps the rung honest. Compile on this base: 26 blocking errors, none in any file this touches; identical to the count before this edit. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01632CTZ8diiLNBQaXobNWKQ * chore: regenerate drifted generated artifacts (ci auto-heal) Ledger-Repair-Judged: docs/design-failure-modes.md Ledger-Rows-Repaired: docs/design-failure-modes.md capability_arrives_outside_the_converged_path Ledger-Repair-Judged: docs/design-rung-drops.md --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.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.
What landed before this
#10589 got a micro-VM booting in CI on srv2:
boot=printed-runner-version 2.336.0, the guest powering itself off, and no VMM surviving (run 33997260934, cleanup verified on the host). That is slice 1's acceptance criterion from the brief.What this PR carries
One defect found by reading that run's output rather than the diff. The guest image build printed, beside the image it had just produced:
Following that advice pins a digest that legitimately changes whenever the tree does, and demands byte-reproducible
mke2fsoutput to stay green — which the row declaring the artifact forbids three lines away.One arm was answering two questions.
ArtifactDigestUnpinnedcovered both fetched, author a pin from this (advice correct) and built here, no pin can ever exist (advice actively wrong). Now split:ArtifactDigestNotPinnableon the integrity sideArtifactBuildReceipton the verdict side, renderingbuild-receipt sha256=... (this build's output; not a pin, and not to be authored as one)The coproduct is closed, so the new arm forced every consumer to answer for it rather than defaulting.
The control has an authorable red
the_built_image_reports_a_receipt_and_never_advises_authoring_a_pingoes red on both halves ifrunner_guest_built_image_artifactis given theUnpinnedarm instead, because that arm carries the pin advice. It asserts the arm and that the rendered text never namesArtifactDigestPinned— asserting only that the text differs would pass on any rewording.Worth recording: three reviews approved this module while the receipt was advising a reader to do what the module forbids. Execution caught it; review did not.
What still blocks running jobs in the VM
The booted VM cannot run a job. Being explicit, because "it boots" reads as closer than it is:
GuestNetworkAbsent— no tap, no egress. It cannot reach GitHub.ExecStartprints the runner version and powers off.Remaining, in order: tap networking with host NAT and nftables refusing tap-to-tap; JIT minting (App installation token ->
generate-jitconfig-> read-only drive); a guest agent that mounts the drive and runs the listener ephemerally; then one realrequired-witnesses-buildjob with verified teardown.Two items needing a decision, both now on the critical path:
EnsureSupplementaryGroupMembershipis authorized but never applied.runner_host_privileged_operationsfeeds only the sudoers renderer; nothing executes the op./dev/kvmon srv2 is currently writable because it was done by hand. Networking adds several privileged ops per host, so without an applier the manual debt compounds per host per op.sccacheis an isolation holeSCCACHE_SERVER_UDS=/var/lib/ctrl/sccache-ci/server.sock— a Unix domain socket, nothing listening on TCP, and guests receive block drives only. There is no transport by which a guest can reach the host sccache daemon. Model the runner microVM in .dag: the prerequisite is a refusal, and it belongs to the topology rather than to virtualization #9578's observation was about a topology where the invoking process could reach the host daemon; carrying its conclusion across the VM boundary was unjustified, and I did that without checking whether it survived the change.The real consequence is cost, not isolation: a 10 GiB working cache and the
MAKEFLAGSjobserver FIFO are both filesystem objects and both unreachable, so a migrated job compiles cold and its parallelism no longer participates in host-side coordination. Coordination belongs to the cgroup envelope (Slice=, already part of the attempt binding), not to smuggling the FIFO into the VM.Anyone reading this PR as a handoff should NOT treat sccache as a blocker for the canary. Ship it cold, with the absence explicit rather than accidental, and measure.
🤖 Generated with Claude Code
https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN