Repository navigation
Reduce the micro-VM module to the grant authorization rule FCI-2 owns - #10674
Conversation
Four stages have to hold before a guest may start: the fabric cell must be owned, the VM config must resolve, the admission must pass, and the App credential must carry organization self-hosted-runners write. This composes them in that order and returns one typed plan. The order is load-bearing rather than stylistic. Every stage but the last is pure and free to refuse; a JIT mint is not, because it creates a runner identity at GitHub. A refusal after a mint leaves that identity registered against the organization for a VM that will never start, nothing on the host knows to delete it, and orphaned registrations are reconcilable only by name. So the mint runs last, and its authorized value is reachable only from inside LaunchAdmitted -- a caller cannot hold a mint authorization for a launch that was refused. Every admission arm is matched where the launch rules on it rather than through a helper over RunnerMicroVmAdmission. Such a helper needs an arm for the admitted case that cannot occur there, and the only thing to put in it is a fabricated refusal, in the one place nothing can observe it. plan_microvm_launch_of_binding carries the decisions and takes a binding a witness can build; plan_microvm_launch is the five-line projection over the sealed RequiredBuildCellSnapshot. Putting the ordering behind the seal would have made it unwitnessable, which is how the previous PR ended up with an annotation claiming coverage that did not exist. Refusal arms stay separate rather than collapsing into one cause string: the cell belongs to fabric_required_build_cell, the size to runner_slot_allocation, the topology to runner_unit, the credential to auth.github_credential, and collapsing them sends an operator to the wrong module. Credential fixtures are imported from test.claim.github_app_registry rather than rebuilt, so there is one answer to what an installation holds. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
… guest The launch plan read gunbc_runner_microvm_realization_reserve() inside the composition, which made the admitted arm unreachable from any caller. Production's reserve is ReserveUnmodeled -- deliberately, because no VMM resident footprint is a cited quantity in extdeps.virtualization.firecracker and inventing one would be a fabricated plausible output -- so every launch refuses at MemoryFitUnresolved and the mint stage below it was dead code no input could reach. The lane caught this: the positive control asserted LaunchAdmitted, a state no input can produce. That is the same decoration class this branch documented for members_owned, this time written into a test rather than a production path, and it would have shipped as coverage for an ordering nothing could exercise. The reserve is now a parameter. The fit judgment is decided by the caller that owns the quantity, the ordering below becomes reachable and therefore witnessable, and production keeps refusing at the entry point rather than by accident inside a composition. Adds the control that says what is true today: with production's own reserve, every launch refuses, so NO CI JOB RUNS IN A MICRO-VM until that quantity is cited or measured and declared. It goes red the day the reserve becomes declared, which is when the launch path becomes live and the claim has to be re-read. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
|
Back to draft, and not because of anything a review raised. The operator asked what consumes
So this is a plan for an action that is currently impossible: production refuses every launch on Worth recording that the defense I gave for Two approvals and four green checks are not evidence against this. They measured hygiene on a diff; none of them asked whether the thing should exist. The ordering error underneath: the first question for "run jobs in micro-VMs" was whether a VM can be admitted at all, which is a measurement on the host and cheap. Instead this modeled three layers above an admission that refuses unconditionally, and the refusal surfaced only when a test written here failed. Next is measuring the VMM resident footprint on srv2 so the reserve can be declared or rejected on evidence. This PR stays in draft until there is an actuator to consume it; if the measured shape says the composition should look different, this gets rewritten rather than defended. — sent from nimble-swift-27 |
The micro-VM path admits no guest because the realization reserve is ReserveUnmodeled: no VMM resident footprint is a cited quantity, and inventing one would be a fabricated plausible output. The quantity has to be OBSERVED on a host before it can be declared, so which instrument exists is a host readiness fact in the same way /dev/kvm is -- a host that boots a guest but cannot report what the VMM cost cannot retire the reserve. Reports GNU time, cgroup v2 memory.peak, and the systemd version line, in the receipt the existing microvm_host_converge mode already prints. No new module and no new workflow job: this had to have a consumer the moment it existed. The instruments are named rather than ranked and nothing here picks one. Each reports the same quantity exactly, and which is available is a property of the host's systemd and kernel, so selecting among them belongs with the measurement. The systemd version is read rather than inferred because MemoryPeak is version-gated at v254. Sampling /proc/<pid>/status VmHWM is deliberately not among them: it needs the process alive, so a guest that powers itself off can be missed, and a missed sample under-reports -- the wrong direction for a value that becomes a safety reserve. Readiness deliberately does not move with the instruments, with a control for it: wiring them into firecracker_host_ready would have taken every host not-ready the moment this field landed, to answer a measurement question. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
The fleet-converge dispatch died on srv2 with NoSuchFunction while the whole witnesses lane had reported RC=0 and FloorClean over the same tree. Two reasons stack and either alone is enough. runner_microvm_host_ready sits declined_outside_gate_closure, so no CI check compiles it. And claims evaluate only the functions they call, so the witnesses added beside this observer cover its pure functions while the func body is never evaluated -- wet bodies run only on a host. A green floor is not evidence that a wet function resolves. gunbc compile --entry DOES catch it, confirmed by running the red arm with the mutation verified applied first. So the gate existed and was not run; it is now run before any dispatch that executes a .dag entry on a host. Worth recording that this is the opposite blindness from the indented-annotation refusal earlier on this branch, where the lane's parse phase caught what compile --entry missed. Neither instrument dominates; a touched module needs both. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
The micro-VM path refuses every launch because the realization reserve is ReserveUnmodeled. This is the observation that could retire it, and it produces a RELATIONSHIP OVER SIZES rather than a constant, because the model's own reasoning is that the overhead is not constant. Sampling several sizes is not thoroughness, it is the whole experiment. Guest RAM is lazily faulted, so a page joins the VMM's resident set only when the guest touches it, and a guest that boots and powers off touches a small and roughly size-independent amount. One reading at one size therefore measures the workload, not the size. A peak that stays flat as declared size rises says the declared size is not committed; a peak that tracks it says it is. Those are different worlds for an admission rule and one sample cannot tell them apart. Stated in the module and not only here: this does NOT establish a worst case. That is what a guest costs when it USES its declared memory, which needs a guest workload that touches all of it. Reporting these numbers as if they bounded that case would be the fabricated plausible output the reserve refusal exists to prevent, arriving by way of a measurement instead of a guess. The instruments were chosen on evidence rather than assumption: the srv2 receipt reports gnu_time present, systemd 255 so MemoryPeak is available, and cgroup memory.peak absent. GNU time's %M is a kernel-maintained high-water mark, which is why it was preferred over sampling VmHWM -- sampling needs the process alive and under-reports a subject that exits on its own, the wrong direction for a reserve. The span check carries its own negative arm as a fixture rather than deferring to a mutation run: the collapses it exists to catch -- one size, two adjacent, three clustered -- are asserted to fail on every run. The third is the one reasoning alone would miss, since count >= 3 passes it and only the span requirement does not. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
The declared sample sizes were 512..4096 BYTES, not mebibytes. Assigning mebibyte(count: N) into a ByteSize field is accepted and does not convert -- the magnitude rides across unchanged -- and std.measure mebibyte_to_byte_size is the conversion that was available and unused. The type system stopped the READ and permitted the WRITE: mebibyte_count on a widened value is a hard error, so the obvious repair is to switch to byte_size_count, which compiles clean and relabels the same number as bytes. That repair is what I made earlier on this branch and reported as a units win. It was not one. WHY NOTHING ELSE CAUGHT IT, which is the part worth fixing rather than the typo. The span control asserts largest >= smallest * 4 over the same list. A uniform unit error preserves every ratio, so it passed identically on bytes and on mebibytes; only the absolute assertion in the render test went red, and that one covers the witness's own fixtures rather than the list production samples. So this also pins the production sizes in absolute bytes. The literals are the specification -- these are the sizes the probe declares it will sample -- so the control is a controlled fixture rather than a measurement copied out of the tree. General rule, recorded because it generalises past this file: when a suite tests a RELATIONSHIP -- ratio, ordering, spread, delta -- at least one control must pin an ABSOLUTE, or a scale error is invisible to the whole suite. Also enrolls the empty-receipt control permanently rather than as a one-off, per 4b(4): footprint_receipt_is_complete folds with init: true, so an empty outcome list is vacuously complete and only the count guard beside it refuses. That guard is load-bearing and had no control. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
The previous commit claimed to fix the unit bug and did not. It converted with a pattern requiring digits, so every literal call site was repaired while mebibyte(count: mib) in the sampled() helper -- an identifier, not a literal -- was silently skipped. That helper is exactly what the failing render claim drives, so the fix looked complete, compiled clean, and left the same claim red. A mechanical edit that matches most of its population and misses the rest is indistinguishable from a complete one at the diff, and the widening it failed to remove is legal, so nothing local objected. What found it was running the lane before pushing rather than reporting the fix from the edit. So the check is now over the POPULATION rather than the pattern: every mebibyte( in both files is wrapped in mebibyte_to_byte_size, verified by a grep whose expected output is empty, not by trusting the substitution's own reach. The absolute control added in the previous commit is what isolated this. It passed while the render claim failed, which said conversion works and the fault is in the render path -- without it the two hypotheses were indistinguishable. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
production_refuses_every_launch_while_the_vmm_reserve_is_unmodeled asserted that every launch refused at MemoryFitUnresolved, and it said in its own text that it would turn RED the day the reserve became declared -- at which point the launch path becomes live and the control has to be re-read rather than silently starting to pass a guest through. #10657 was that day. It set the allowance aside and made the reserve ReserveDeclared, so production now reaches an admitted guest and the assertion is false. The control was not broken; it fired. This is the re-reading it demanded. The red was only visible on the PR merge ref: my branch alone still has the unmodeled reserve, so both local instruments greened while CI -- which builds branch-merged-with-main -- refused. Running an instrument against a tree that lacks the change under test measures the wrong subject no matter how correct the instrument is, and a green from it looks exactly like a green from the right one. What replaces the row is the same question asked of the live path, in three parts. The admission control pins that the guest admitted is the DECLARED size rather than any default. The refusal control keeps that from being satisfied by a fit judgment that answers yes to everything: a reserve larger than the cell must admit no guest of any size. And the original discriminating RED stays enrolled with an explicitly unmodeled reserve -- 4b(4) keeps a class's red executing after its wall lands, and an unresolved fit is exactly what the launch path must never pass a guest through, whoever the caller is. The arithmetic is deliberately NOT re-derived in the witness. guest_memory_fits already carries the comparison, and recomputing it here would be a second representation of one constraint, satisfiable by editing the test while the production path still lied. Both new controls were verified by mutation rather than by reading: shrinking the oversized reserve and expecting a size production does not declare turn each of them red, while the untouched third stays green -- without that last one a run that failed everything would have looked like proof. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
…he fabric runner_microvm_launch_plan composed a launch straight from a cell binding and started a VMM. gunbc.fabric_ci_program FCI-3 owns that question -- what causes the target process -- and its exit predicate is that a persistent executor re-reads the committed Grant before starting, so an absent, corrupt or expired Grant yields ZERO target processes. FCI-1's non-goals name Work-process-start and ExecutionGrant explicitly; FCI-2's name process-start. The module therefore did FCI-3's job while skipping FCI-2, which is the second execution system ROADMAP forbids when it says the fabric is four consumers of one contract. That is also why nothing consumed the module. The correct consumer is the FCI-3 executor, and it could not consume a launch whose signature omitted the grant -- so writing any caller would have cemented the bypass rather than closing it. The grant is now a REQUIRED PARAMETER rather than something this module looks up. The absent case has no constructor, so it is unwritable rather than validated; the fence check against the issuing account covers corrupt and expired, because a grant whose lease generation no longer admits is a superseded authorization. Authorization is the first stage: nothing starts without it whatever the cell's state, and a control pins that ordering by presenting an unowned cell and requiring the grant refusal to still win. THE CONTROLS CAUGHT A BUG THAT PASSED THEM. issue_grant returns the account carrying the recorded lease, and the first version fenced against the PRE-issuance account -- so every launch refused, and both grant controls passed against a mechanism that was refusing everything. Only the seven positive claims failing revealed it. The grant and its committed account are now one IssuedAuthorization value, because splitting them is what made the error writable. Verified by mutation in PRODUCTION rather than in the test: neutering the fence check turns both grant controls red and leaves the other seven green. No claim asserts the absent-grant case, because its RED is unauthorable once the parameter is required -- that check would be a 4b decoration, permanently green and cited as coverage. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
The host-readiness observation and the footprint probe answer a different question than the launch plan does, and they stand alone: no reference to the launch plan, the execution grant or the mint. They are now PR #10806 off main. This branch keeps one subject -- what causes a micro-VM to start, and under whose authorization -- so its title is the one squash-merge writes into main's history. The extdeps rows move with the code that needs them: gnu_time_max_rss_command and systemctl_version_command are admitted for the probe, so they belong to the probe's branch and are reverted here rather than left admitting callers that no longer exist on this branch. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
|
Direction from Brian’s standing goal: the next success is a wet FCI-3 launch, followed immediately by one real One correction before proceeding: requiring an At head
That leaves a valid grant for A able to authorize a launch bound to snapshot B if the supplied account fences. It is the same admission/execution substitution class this lane has already been repairing. Also, Build this next: the smallest real FCI-3 executorThe executor—not a caller or workflow request—must:
A timer/path unit or narrowly scoped host service is sufficient for the first executor. Do not build a general scheduler. “Persistent” means the executor and committed grant survive the submitting process—not that this PR needs multi-host failover. Wet acceptance—do not substitute pure witnessesOn an isolated disposable grant/store subject on srv2:
The evidence must observe the actual GitHub request count/runner identity and actual systemd/VMM process population—not only #10806 is preflight, not the measurement result#10806’s host standing does useful instrument discovery and its new footprint module defines the sample/receipt vocabulary, but that module currently has no wet sampler or production receipt producer. Seven passing claims establish its pure model, not a VMM footprint. Add the minimum actuation route and run all declared sizes on srv2; return the complete receipt and run id. Use it to justify a canary-specific reserve, not a universal worst-case bound. Do this while building FCI-3 rather than serializing more groundwork behind its review. Continue directly to the user-visible milestoneAfter the wet FCI-3 positive path, do not stop for cache design, a replenishing pool, multi-host scheduling, or cutover. Route one explicitly selected existing A useful next update is therefore one of two things: the actual #10806 footprint receipt, or the exact first failing boundary while the persistent executor re-reads and launches from a committed grant. Another compile-only or pure-claim-only checkpoint is not progress toward this milestone. |
…rom authorization Requiring an ExecutionGrant parameter closed the absent-grant case and nothing else. The grant and the cell binding arrived as independent arguments and the only thing read off the grant was its money reservation, so a grant issued for execution A composed with the reserved cell for execution B was ADMITTED whenever the supplied account fenced A. That is worse than no grant: its presence reads as authorization while authorizing nothing about the subject. Found in review; the PR text claiming this bound the launch under the fabric contract overclaimed. MicroVmExecutionBinding is sole_constructor and reachable only through seal_execution_binding, which refuses unless Work, Demand and Offer all agree between the grant and the reservation. The mismatched pair now has no constructor rather than being caught by a check inside the planner. THE RULE IS FACTORED OUT OF THE SEAL SO ITS RED IS AUTHORABLE. RequiredBuildCellSnapshot is sole_constructor precisely so a caller cannot manufacture a reservation, which also means no witness outside its module can build a DISAGREEING one -- a control aimed at the seal could never construct the input it exists to catch, so it would be permanently green and cited as coverage. Exposing a snapshot builder for tests would punch the hole the seal exists to close, the tradeoff runner_microvm_attempt's own witness already records. So grant_authorizes_reservation takes the coordinates, where a disagreeing pair IS constructible, and the seal reads them off the snapshot and delegates to it. PLANNING NO LONGER PRETENDS TO BE AUTHORIZATION. plan_microvm_launch_of_binding takes no grant at all, because cell ownership, VM config, admission and the mint are not authorization questions and a signature that accepted a grant while ignoring its subject is what created the opening. Production reaches it only through the sealed value, so the gate cannot be routed around; witnesses drive each level where that level's red is writable. WHAT THIS STILL DOES NOT ESTABLISH, recorded because the type name would read as more. ExecutionGrant is an ordinary constructible record, so this proves AGREEMENT between a presented grant and a presented reservation, not that fabric issuance durably committed either. The unforgeable form is a persistent executor re-reading the committed grant from durable storage after the submitter terminates, which is FCI-3's own exit predicate and the next slice. Ten claims pass. The substitution control was verified by removing ONLY the Work join in production: it reds alone while the fence and positive controls stay green, so it is bound to this defect rather than to a rule that refuses broadly. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
The launch plan half is deleted. Not because it was unconsumed -- because it was REDUNDANT. runner_microvm_witness_test already carries a_reserve_larger_than_the_whole_envelope_admits_no_guest, the_production_reserve_is_the_declared_allowance, the_production_reserve_lets_the_declared_configuration_reach_admission_under_authored_topology, orphanable_unit_refuses_the_microvm_migration, shared_slot_directory_credential_is_refused and the whole guest-memory boundary family; cell ownership is in runner_microvm_attempt_witness_test and the credential join in the jit mint witness. Deleting the seven planning claims removes NO coverage. I re-derived them because this branch predated #10657 and I never read the neighbouring witness, which is the same root as a roster edit on this branch that would have dropped ten rows other lanes had landed. What survives is the part nothing else answers. Grant and cell binding arrived as independent arguments with only the money reservation read, so a grant issued for execution A authorized execution B whenever the account fenced A -- the grant's presence read as authorization while authorizing nothing about the subject. grant_authorizes_reservation now requires Work, Demand and Offer to agree, MicroVmExecutionBinding is sole_constructor so the mismatched pair has no constructor, and three controls carry it. The module is renamed for what it now contains. A module called launch_plan holding no launch plan is a name promising something it does not carry. ON THE SEAL, because the question was whether it is a 4b decoration. SoleConstructorViolation for cross-module construction is already proven by sole_constructor_violation_outside_module over a synthetic two-module pair, so the red IS authorable and the seal is not a decoration. A type-specific fixture would re-prove the general wall in a second home, which is the same redundancy this commit deletes. Stated honestly: that evidence runs under cargo test -p v1-compiler --lib, which no CI step executes -- the declared drop rust_unit_tests_off_the_merge_path -- so the wall is compile-enforced but the evidence one would cite for it is not on the merge path. This refusal and #10733's do not duplicate. jitconfig-bytes=0 is about CREDENTIAL MATERIAL; this is about AUTHORIZATION SUBJECT, and it orders strictly earlier because it refuses before any drive is built. They compose. Verified after the reduction rather than before: three claims pass, and removing ONLY the Work join in the renamed module reds the substitution control alone while the fence and positive controls stay green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
The near-misses this branch produced belong with the class they are nearest to: an append-only carrier losing a row renders as reordering, so the diff is blind and only the count against the base raises it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
REVIEW FINDING 1, CONFIRMED AND IT IS THIS PR'S OWN CLASS. Roster was 175 on main and 174 here: added production_actuation... and silently dropped decision_surface_truncation (#10712) and lookup_miss_read_as_positive_classification (#10727), both landed after the branch point and both with their module files still present. The triple-dot diff renders it as reorder-plus-two and shows nothing. Found by the count comparison the PR's own row prescribes, named by an identity join, and repaired by merging main so the roster is 176 with an empty join in both directions -- imports and list body checked separately, since either half can drop alone. REVIEW FINDING 2, CONFIRMED. The reduction left the launch graph's imports (32 lines -> 8 in the module, 37 -> 18 in the witness) and an annotation asserting mint-last/LaunchAdmitted ordering that no longer has a mint or a launch to range over -- a 4c annotation no Accepted program reads, so a false one never reds and it drifts to flatter the change. Annotation replaced with what the module now does, including why the ordering argument is NOT restated here. Orphan fixtures deleted (launch_org, launch_net, launch_binding, witness_reserve, both lifecycle intents, launch_test_slot); witness_reserve's own note was stale too, still saying production refuses every launch. Also declares the seal a 3c frontier rather than leaving it implicit: nothing consumes it, and no witness CAN -- its input is a sole_constructor snapshot -- so the trigger is named beside it, with the honest alternative stated. Three claims pass. Compile shows the 3 pre-existing extdeps/gunbc shell transport errors and nothing in these files. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
|
Both findings confirmed and fixed in 1. Silent roster drop — confirmed, and it is this PR's own classVerified by the count comparison rather than the diff, then named by an identity join:
Both landed after my branch point, both module files still present, and the triple-dot diff renders it as reorder-plus-two — exactly the blindness the row I am adding describes. The review is right that this PR filed the rule and then broke it. Repaired by merging The projection 2. Launch-plan residue — confirmed
One thing the review did not raise, found while fixing it
EvidenceThree claims pass by execution after the rework. Compile shows the 3 pre-existing — sent from nimble-swift-27 |
THE HOST/GUEST SLIP WAS THE SERIOUS ONE and the review is right that it would send a worker to the wrong cut root. Steps 3-9 run in the HOST image's early boot -- the banner is GUNBC-RUNNER-HOST, ~17s after the HOST kernel starts, and the guest does not exist yet because step 9 is what creates it. Two places said "guest image", including the sentence naming the load-bearing unknown. Corrected, with the earlier wrong wording called out in place so a reader who saw it knows it moved. CITATIONS: runner_microvm_execution_authorization, grant_authorizes_reservation, seal_execution_binding and the production_actuation... class resolve to NOTHING on this branch -- they are authored on #10674, which is open. Presenting them as corpus facts is the fabrication DESIGN section 5 forbids. Now marked PROPOSED at their use sites and in a standing note, which also records that none of this document's findings depend on #10674 landing: the census, the reading half and the axis dispositions come from probe captures, fleet-converge.yml and modules that do resolve on main. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
Ledger-Repair-Judged: docs/design-failure-modes.md Ledger-Rows-Repaired: docs/design-failure-modes.md production_actuation_unmodeled_beside_a_modeled_probe Ledger-Rows-Repaired: docs/design-failure-modes.md decision_surface_truncation Ledger-Repair-Judged: docs/design-rung-drops.md
Review 62349 is right and it is the sharpest catch on this branch. The rule has FOUR refusal arms -- fence, Work, Demand, Offer -- and the witness enrolled REDs for TWO. A rule that dropped the Demand and Offer checks entirely would have greened every claim in the file, so the join was reported at a rung its executed evidence does not establish. That is rung inflation in the module built to stop a substitution. Two controls added, same shape as the Work case. Arm-to-assertion count is now 4 and 4. MUTATION-PROVEN INDIVIDUALLY, because five passing claims do not establish discrimination -- a control that fails alongside others is not a discriminating RED: remove ONLY the Demand arm -> ONLY a_grant_for_another_demand reds remove ONLY the Offer arm -> ONLY a_grant_for_another_offer reds Both times the other four stay green. Also records in the witness WHY these REDs are authorable when the seal's is not, since the questions sound identical and get opposite answers: the seal's input is a sole_constructor snapshot, so a disagreeing one has no constructor a fixture can reach and a control there would be a 4b decoration; FabricIdentity is an ordinary record, so a disagreeing demand or offer is writable right here. The constructor decides it, not how important the check feels. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
|
Confirmed and fixed in The gap was real and it was rung inflationFour refusal arms — fence, Work, Demand, Offer — and two enrolled REDs. A rule that deleted the Demand and Offer joins would have greened every claim in the file, so the join was reported at a rung its executed evidence did not establish. That is §4b(1) rung inflation in the one module whose entire purpose is refusing a substitution, and the review is right that the join was only half-evidenced. Two controls added in the same shape as the Work case. Arm-to-assertion count is now 4 and 4 — one RED per refusal arm. Mutation-proven individually, because five passing claims do not establish discriminationA control that fails alongside others is not a discriminating RED. So each new arm was removed in isolation and the suite re-run:
Baseline: all five pass. The module was restored from git and re-verified (4 refusal arms, 3 identity joins) before committing, so no mutation leaked into the diff. One thing recorded in the witness rather than left hereThese two REDs are authorable while the seal's is not, and the questions sound identical — so the witness now carries the test that separates them. The seal's input is a The constructor decides it, not how important the check feels. I applied that test correctly in one direction on this module and missed it in the other, which is why it is now written down beside the controls rather than re-derived by the next reader. — sent from nimble-swift-27 |
Review 62356: the document landed with no doc-graph bind, and gunbc.doc_graph_roots is explicit that an unbound doc is an orphan, loudly -- hand-authored docs declare typed HandAuthoredDocBind rows and every one of the 158 existing binds states a retirement condition. Bound to the two carriers whose movement would make the document's framing wrong: FCI-3, whose exit predicate the receipted zero-byte-credential launch violates, and the host image store, whose resilient:false standing is what makes the unauthored actuation a single-copy risk rather than an untidy one. DELIBERATELY NOT BOUND TO THE FCI-2 MODULE OR THE FAILURE-MODE ROW, both authored on the unmerged #10674. A bind to a symbol that does not resolve is the citation defect this same document was already corrected for once -- my first draft of this row made exactly that mistake while its own prose claimed it had avoided it. Both cited symbols were verified to resolve on this branch. Count checked as a count, not a diff: 158 -> 159. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
…27-vm-lifecycle # Conflicts: # docs/design-failure-modes.md
Review 62362, both findings correct. THE SEAL IS DELETED, WHICH IS WHAT MY OWN ANNOTATION SAID TO DO. I had declared it a 3c frontier, but 3c admits one only with a NAMED LATER CHANGE, and mine was FCI-3 -- which the displacement analysis shows is blocked behind a prerequisite nobody has started. The review's phrasing is right: a gate id plus a missing plan and an unpriceable prerequisite is not a named later change. And the annotation cited docs/plans/microvm-launch-displacement-analysis.md, WHICH DOES NOT EXIST ON THIS BRANCH -- it is on the unmerged #10823. So the justification for keeping unconsumed code rested on an artifact that does not resolve, which is the citation defect this session has now made three times across unmerged branch boundaries. This also DISCHARGES rather than overrides the earlier ruling to keep the seal: that keep was conditional on a fixture being able to author the forbidden state and be refused. No witness can call it at all -- its input is a sole_constructor snapshot -- so the condition failed. Module is 79 lines: one rule, four refusal arms, five claims. All five still pass with the seal gone, which is the evidence that they were driving the RULE and never the seal. ROSTER WAS BEHIND MAIN AGAIN, 176 vs 177, missing guarded_filter_branch_dropped_by_emitter and match_variant_lookup_does_not_peel_type_alias. Merged: 178 imports and 178 list entries, empty join against main in both directions. Second time on this branch -- the ledger surface moves faster than an edit-review cycle, and only the count comparison catches it. The projection came back UU with NO conflict markers, the merge driver refusing as designed. That artifact is HealRegeneratesAfterProvisionalMerge, so the provisional state is staged for heal rather than hand-written. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
|
Both findings confirmed and fixed in 1. The seal is deleted — the review's argument is the one my own annotation made§3c admits a frontier only with a named later change, and mine was FCI-3, which #10823 shows is blocked behind a prerequisite nobody has started. The review's phrasing is exact: a gate id plus a missing plan and an unpriceable prerequisite is not a named later change. Worse, and this is the part I want on the record: the annotation cited This discharges rather than overrides the earlier ruling to keep the seal. That keep was explicitly conditional on a fixture being able to author the forbidden state and be refused. I later established no witness can call The module is now 79 lines: one rule, four refusal arms, five claims. All five still pass with the seal gone, which is the evidence that they were driving the rule and never the seal — a claim that had been leaning on the deleted code would have gone red here. 2. Roster behind
|
Ledger-Repair-Judged: docs/design-failure-modes.md Ledger-Rows-Repaired: docs/design-failure-modes.md guarded_filter_branch_dropped_by_emitter Ledger-Rows-Repaired: docs/design-failure-modes.md match_variant_lookup_does_not_peel_type_alias Ledger-Repair-Judged: docs/design-rung-drops.md
|
Repaired and measured — heal pushed The finding was correctRoster 178, projection 176, both restored identities missing from the index and the bodies. Confirmed exactly as reported before fixing anything. Repair, verified rather than assumed
Two of my first verification greps returned 381 — the whole file — because the extracted pattern was empty, and an empty pattern matches every line. A broken check reports total success, so I re-ran with literal substrings lifted from each module's receipts. Worth stating because it is the same shape as a control that cannot fail. The part of this that was mineI staged a projection I had personally measured as inconsistent (176 vs 178) and justified it as provisional because the artifact is I could not repair it locally, which is a real constraint rather than a preference: the heal job builds its own regenerator from the checkout, while my local binary (2026-09-05) fails on The authorization reduction the review found sound is unchanged: seal deleted, — sent from nimble-swift-27 |
…se annotation as false Review 62386, both findings correct. THE ANNOTATION WAS FALSE, NOT MERELY STALE. It said the rule was "factored out of the seal above it" and that "the seal delegates to it". The seal was deleted last commit, and bind_microvm_to_cell takes only a snapshot and never sees an ExecutionGrant -- so the sentence asserted a relationship between two declarations that does not exist in the corpus. Recorded as false rather than quietly removed: a 4c annotation is read by no Accepted program, so a false one never reds, and the next reader deserves to know the claim was wrong rather than find a tidy comment. THE FRONTIER WAS DECLARED FOR WHAT I DELETED AND NOT FOR WHAT I KEPT, which is the review's actual point and it is exact. 3c's two admissible states differ by whether the consumer and trigger are stated BESIDE the declaration; for grant_authorizes_reservation they were not, so the rule was dangling rather than declared. Now stated: named consumer is the FCI-3 executor whose exit predicate this rule is the agreement half of, trigger is that executor existing, and the route today is that nothing in the runner path calls it. STATED WITH ITS COST RATHER THAN AS A REASSURANCE: that trigger is not near, because the actuation FCI-3 must displace is authored in no repository. A reader weighing whether the module earned its place should have that beside what it does carry -- four typed refusal arms, each mutation-proven to red ALONE. Correctness established by execution; only production consumption deferred. AND A TENSION IN MY OWN REASONING, NAMED RATHER THAN LEFT FOR A REVIEWER: I deleted the seal partly on "the trigger is not near", and I now declare a frontier for the rule on that same trigger. 3c requires a trigger to be STATED, not to be near, so "not near" was over-applied there. The seal still went for the right reason -- no fixture could construct its sole_constructor input, so it had ZERO executed evidence. The seal failed consumption AND evidence; the rule fails only consumption. 5 claims pass. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
|
Both findings confirmed and fixed in 1. The rule had no declared frontier — the review's diagnosis is exact
The precise defect is the one the review names: the module header declared a frontier for what I deleted and said nothing about the rule it keeps. §3c's two admissible states differ by whether the consumer and trigger are stated beside the declaration, and for the rule they were not — so it was dangling rather than declared. Now stated: named consumer is the FCI-3 executor, whose exit predicate in It is stated with its cost rather than as a reassurance: that trigger is not near, because the actuation FCI-3 must displace is authored in no repository. A reader deciding whether this module earned its place should weigh that against what it carries — four typed refusal arms, each with a discriminating RED mutation-proven to red alone. Correctness is established by execution; only production consumption is deferred. 2. The annotation was false, not merely staleIt said the rule was "factored out of the seal above it" and that "the seal delegates to it". The seal was deleted in the previous commit, and Recorded as false rather than quietly removed. A §4c annotation is read by no A tension in my own reasoning, named rather than left to be foundI deleted the seal partly on the grounds that its FCI-3 trigger "is not near", and I am now declaring a frontier for the rule on that same trigger. §3c requires a trigger to be stated, not to be near, so "not near" was over-applied as if it were the test. The seal still went for the right reason, and it is a different one: no fixture could construct its Evidence5 claims pass by execution after the change. — sent from nimble-swift-27 |
…27-vm-lifecycle # Conflicts: # dag/gunbc/recurring_failure_mode/roster.dag # docs/design-failure-modes.md
…al variants
Review 62520 raised two findings and both were real.
The refusal type collapsed four named causes into AuthorizationDisagrees { cause: String }
while the annotation directly above it asserted "THE REFUSAL ARMS ARE NOT COLLAPSED INTO ONE
`cause` STRING". The four arms were four if-branches producing four prose strings. That is
DESIGN section 2's anemic String leaf, and because a section 4c annotation is read by no
Accepted program, the false claim could never red. The type is now a sum matching the sibling
ReceiptAdmission: GrantAuthorizes | GrantFenceRefused | GrantAuthorizesDifferentWork |
GrantAnswersDifferentDemand | GrantIssuedAgainstDifferentOffer. The five controls match a
named variant instead of string_contains, which strengthens them -- a refusal naming the
wrong authority could still contain the right words.
The home finding was also right, but its prescribed destination does not compile.
product.fabric.budget already imports product.fabric.execution, so homing a rule that needs
MoneyAccount and fence_admits into execution.dag creates an import cycle -- the one structural
law section 4 states. The rule is homed in product.fabric.grant_issue instead, which already
imports execution, budget, identity and work, and which issues the grant: the agreement join
is the direct counterpart of issue_grant, at FCI-2's grain. gunbc.runner_microvm_execution_authorization
is deleted and the witness moved beside the issuance fixture it already imported.
The section 3c frontier is re-declared at the new home: the rule still has no production
consumer, its named consumer is the FCI-3 executor, and the trigger is stated.
Executed evidence: five claims pass under claim_batch --claim-run against
dag/test/claim/fabric/fabric_grant_authorization_witness_test.dag.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
|
Both findings in review 62520 were real and both are fixed in The The five controls now match a named variant rather than The home — correct, but I homed it in I also re-declared the §3c frontier at the new home rather than losing it in the move: the rule still has no production consumer, its named consumer is the FCI-3 executor, and the trigger is stated beside it. Executed evidence, not a typecheck. All five claims pass under Still blocked, and not on a witness. The required run refuses at — sent from nimble-swift-27 |
* Measure what displacing the live micro-VM launch would cost Censuses the per-attempt path that starts a real Actions job on Mt. Collins against what .dag already owns, and finds the cut is one ordered driver over largely-existing facts -- but gap-intolerant, because the boundary is a host-side pre-boot lifecycle and the JIT credential is one-shot, so the two paths cannot be A/B'd. Builds nothing. It converts "should we build FCI-3" into a single measurement: can a modeled entry point run where the jailer exec does. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN * Answer the reading half, and give the six axes dispositions The reading half needed no host and it settles the open branch: the mechanism that displaced steps 1-2 runs LocalExec on a self-hosted runner, so it presupposes a runner, a checkout and a binary -- none of which exist at the jailer exec, because bringing a runner into being is what that boot is FOR. The dependency is circular. And the host boot script is not in this repository in any language. The six axes get dispositions rather than a verdict: two required (signature, expiry -- both whole-credential properties), four deferred behind one trigger, because none of the six is DEFINED anywhere here and the credential is an opaque blob a host cannot parse. So the cut is not a six-way credential-admission programme on today's reading. Also states the good news first: half the census is already displaced and the mechanism is proven wet. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN * Item 1 was a search, and the boot script is authored nowhere Mis-filed as needing host access. Org-wide code search, positive- controlled and with each private repo controlled separately, finds the banner and marker stream only in captures and artifacts -- ctrl is searchable and clean, gunbc-private is NOT searchable so it was cleared by reading its tree instead. Two things make this worse than "not in a repo". ctrl carries the sibling wrapper for the non-VM hosts, whose own header records that being host-only and uncommitted contributed to the 2026-05-29 GHA stall -- this org has already taken an outage from this exact class. And the carrier is one unreplicated ISO on srv1 (resilient: false), so the thing that starts every production micro-VM has no source to rebuild from. Consequence for the cut: there is no X to delete in source control, so the first move is recovering X's content, not building Y. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN * Fix the host/guest slip, and mark unmerged citations as proposed THE HOST/GUEST SLIP WAS THE SERIOUS ONE and the review is right that it would send a worker to the wrong cut root. Steps 3-9 run in the HOST image's early boot -- the banner is GUNBC-RUNNER-HOST, ~17s after the HOST kernel starts, and the guest does not exist yet because step 9 is what creates it. Two places said "guest image", including the sentence naming the load-bearing unknown. Corrected, with the earlier wrong wording called out in place so a reader who saw it knows it moved. CITATIONS: runner_microvm_execution_authorization, grant_authorizes_reservation, seal_execution_binding and the production_actuation... class resolve to NOTHING on this branch -- they are authored on #10674, which is open. Presenting them as corpus facts is the fabrication DESIGN section 5 forbids. Now marked PROPOSED at their use sites and in a standing note, which also records that none of this document's findings depend on #10674 landing: the census, the reading half and the axis dispositions come from probe captures, fleet-converge.yml and modules that do resolve on main. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN * chore: regenerate drifted generated artifacts (ci auto-heal) Ledger-Repair-Judged: docs/design-failure-modes.md Ledger-Rows-Repaired: docs/design-failure-modes.md decision_surface_truncation Ledger-Repair-Judged: docs/design-rung-drops.md * Name the search census's instrument instead of transcribing its counts Review 62347, and both findings are right. The whole "authored nowhere" conclusion rested on bare hit counts from an ad-hoc org-wide code search -- 11 hits, 914, 2, 0, 178 blobs -- with no producer named that re-derives any of them, while the rest of the document properly cites docs/probes captures. DESIGN section 6 is explicit: name the instrument, never transcribe its output, because a transcribed number is unreachable from the thing that owns it. Replaced with the four gh api search/code queries themselves, and the emphasis moved to where it belonged: the CONTROLS decide this result, not the counts. The positive control is what separates "the instrument works and found nothing" from "the corpus is empty"; the per-repo reachability control is what caught that gunbc-private returns ZERO FOR A UNIVERSAL WORD, so an org-wide sweep alone would have reported it clean while never having looked at it. AND THE SECOND FINDING IS THE WORSE ONE. The closing self-assessment claimed the document "transcribes no measurement" while the census did exactly that -- a false self-assessment is worse than the defect it covers, because the section then reads as already-checked. Corrected, and the correction says the earlier claim was false rather than quietly rewording it. Also stops restating the reap count in prose; runner_host_image_store's own first_reap row is the authority. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN * Bind the displacement analysis into the doc graph Review 62356: the document landed with no doc-graph bind, and gunbc.doc_graph_roots is explicit that an unbound doc is an orphan, loudly -- hand-authored docs declare typed HandAuthoredDocBind rows and every one of the 158 existing binds states a retirement condition. Bound to the two carriers whose movement would make the document's framing wrong: FCI-3, whose exit predicate the receipted zero-byte-credential launch violates, and the host image store, whose resilient:false standing is what makes the unauthored actuation a single-copy risk rather than an untidy one. DELIBERATELY NOT BOUND TO THE FCI-2 MODULE OR THE FAILURE-MODE ROW, both authored on the unmerged #10674. A bind to a symbol that does not resolve is the citation defect this same document was already corrected for once -- my first draft of this row made exactly that mistake while its own prose claimed it had avoided it. Both cited symbols were verified to resolve on this branch. Count checked as a count, not a diff: 158 -> 159. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN * Narrow an overstated claim: no Mt Collins runner serves production CI The document said the unauthored boot script starts "every production micro-VM on Mt. Collins", which reads as though the fleet's CI runs on that path. It does not. A runner_name census over the last completed runs returns srv1/srv2/srv3/srv4 only -- the bare-metal hosts running ctrl's jit-runner.sh -- and NO Mt Collins runner at all. Mt Collins has served micro-VM canary jobs and nothing more. The narrower claim is the load-bearing one and it is STRONGER: this script is the sole path any micro-VM migration must go through, so the risk is not that production runs on unversionable code today, but that the migration cannot proceed except through code nobody can rebuild. Corrected in place with the old wording quoted, rather than silently reworded -- a false premise in a document an escalation would cite is worse than a weak one, and a self-assessment that quietly improves itself is the defect review 62347 already caught here once. The census names its command rather than transcribing its counts, per the same section 6 correction, and states the control that makes the empty result meaningful: the query does not filter by host, so a Mt Collins runner would appear if one had served a job. 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> Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
…list #10822 deleted the hand-appended failure-mode roster: membership is the row DIRECTORY now, derived before compile. This row's corollary prescribed a count comparison against the base for append-only carriers and cited the roster at 163 against 173 as a live countable specimen. Half that citation is a superseded claim, and it had not landed yet -- so this corrects the row before it ever becomes an authority rather than editing a published one. I had declined this edit earlier on the grounds that the row was a live authority and that changing prose inside a PR waiting on an unrelated gate is how a superseded claim survives review. The reasoning was sound and its PREMISE WAS FALSE: the row is absent from origin/main and exists only on this branch. There is no landed authority to preserve. The corrected text is taken verbatim from #10853 (deep-crane-107, 9a2358a), which added the identical file and differed only in this one receipt string; that PR closes rather than landing a second copy for this one to later drop. The file is now byte-identical to its version, so one row has one authority. What the text now does: scopes the rule to append-only carriers that are STILL A LIST, keeps extdeps.exec.command admit_callers at 67-vs-68 as the surviving specimen, marks the roster SUPERSEDED FOR ONE CARRIER ONLY citing #10822, and keeps the closing instruction not to invent a replacement count for the dissolved carrier -- directory membership is a different subject. The correction is self-applying: refreshing that citation as though the roster were still countable would itself be a_live_authority_name_carries_a_superseded_claim. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
Review 62587 found two real defects and the second explains why the first survived. THE RULE JOINED TWO INDEPENDENTLY ADVANCING COUNTERS. fence_admits compares the generation the ACCOUNT holds for a reference, and product.fabric.budget reserve_money records that from the MONEY request (`generation: request.generation`). The rule presented grant_lease_generation, which answers the RESOURCE lease's counter. So a grant authorized whenever the two happened to coincide, and a legitimate grant whose counters had diverged was refused as GrantFenceRefused -- a cause naming the wrong fact. product.fabric.execution already records this class one authority over: comparing generations alone was a real fencing hole, and it made prose describe a wall the code did not build. This was that class re-introduced against a different generation authority. ExecutionGrant carries NO money generation -- money_reservation is a bare ReservationRef -- so there was no correct value to read off the grant. It is now a presented coordinate, which is what the rest of this rule already does and what makes its REDs authorable. The witness presents money_request.generation, what the ISSUER asked for, against what the account RECORDED: two independently authored facts. Reading it back off the account would compare a value to itself and green by construction, which is the 4b decoration this rule exists to avoid. THE POSITIVE CONTROL WAS GREEN BY FIXTURE COINCIDENCE. money_request.generation is 9 and fixture_lease.generation is 9, so the old control passed while proving only that two unrelated counters agreed. The fixtures are left at 9 and the discrimination is carried by a new claim that presents the RIGHT account against a WRONG generation -- the arm the coincidence was hiding, since the existing exhausted_account claim refuses because the account holds no lease for the reference AT ALL and would pass a rule that ignored the generation entirely. MUTATION-PROVEN, and the result is the review's finding as an executed measurement: with the defect restored, EXACTLY ONE claim fails -- a_grant_fenced_at_another_money_generation_authorizes_nothing -- while the other five pass, INCLUDING the old positive control. The pre-existing suite was structurally blind to this defect, which is how it survived. Reverted, all six pass. The now-unused grant_lease_generation import is dropped: leaving it would advertise a dependency the code no longer has. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
|
Both findings in review 62587 are real and both are fixed in The rule joined two independently advancing counters.
The positive control was green by fixture coincidence, as you said. Mutation-proven, and the result is your finding as an executed measurement. With the defect restored, exactly one claim fails: Five pass under the defect, including the old positive control. The pre-existing suite was structurally blind to this, which is how it survived review twice. Reverted, all six pass. I also dropped the now-unused One note on what this does not claim: the fence still establishes only that the account agrees with a presented money generation. It does not establish that fabric issuance durably committed the reservation, and the §3c frontier above the rule says so. Whether — sent from nimble-swift-27 |
Answers one question and stops there: does an execution grant authorize the reserved cell a micro-VM job would run in? The measurement work that was on this branch is now #10806, and the launch plan that was on it has been deleted rather than moved.
Why the launch plan is gone
The original module composed a launch straight from a cell binding and started a VMM.
gunbc.fabric_ci_programFCI-3 owns that question — what causes the target process — and its exit predicate is that a persistent executor re-reads the committed Grant before starting, so an absent, corrupt or expired Grant yields zero target processes.FCI-1's non-goals name
Work-process-startandExecutionGrantexplicitly; FCI-2's nameprocess-start. So the module was doing FCI-3's job while skipping FCI-2 — the second execution system ROADMAP forbids when it says the fabric is four consumers of one fabric, not four execution systems.That is also why nothing consumed it. The correct consumer is the FCI-3 executor, and it could not consume a launch whose signature omitted the grant. Any caller written would have cemented the bypass rather than closing it.
Requiring the grant as a parameter fixed the bypass but left the module still performing FCI-3's job with FCI-2's input bolted on. The honest reduction is to keep only the part that is FCI-2's: the authorization rule. Composition of the launch belongs to the executor, when that lane exists.
What survives, and why deleting the rest lost no coverage
grant_authorizes_reservationrefuses on four axes — the money fence, and Work / Demand / Offer agreement between the grant and the cell — andseal_execution_bindingpairs a grant with a binding through asole_constructortype, so an unauthorized binding has no constructor outside the module.The seven deleted planning claims were duplicates, which is why this is a §2 reduction rather than a §6 scope cut. Their subjects are already covered by execution elsewhere: the reserve and guest-memory boundary family and the orphanable-unit and shared-slot-credential refusals in
runner_microvm_witness_test, ownership inrunner_microvm_attempt_witness_test, and the credential in the JIT mint witness.Evidence
Three claims pass by execution:
a_grant_that_does_not_fence_authorizes_nothinga_grant_for_another_work_authorizes_nothing— the substitution seal: a grant issued for a different Work authorizes nothing herethe_issued_grant_authorizes_its_own_reservation— the positive controlVerified by mutation, re-derived against the reduced module rather than carried over from the pre-reduction run: removing only the Work join reds the substitution claim alone, while the fence check and the positive control stay green. The RED is discriminating, not a blanket failure.
The seal's forbidden state — constructing a
MicroVmExecutionBindingoutside the module — is already refused by execution under the existingsole_constructor_violation_outside_moduletest over a synthetic two-module pair, so a type-specific duplicate would be a second authority for one rule. One wrinkle, stated rather than left for a reader to find: compile-enforced on every build, but the evidence one would point at is off the merge path underrust_unit_tests_off_the_merge_path.No claim asserts the absent-grant case. Its RED is unauthorable once the grant is a required parameter, so that check would be a §4b decoration — permanently green and cited as coverage.
The finding this branch also files
A recurring failure mode row,
production_actuation_unmodeled_beside_a_modeled_probe: micro-VM install is modeled and a boot probe launch is modeled, but the launch real jobs take on Mt. Collins is host tooling outside the substrate with.dagcarrying prose receipts after the fact. Two homes for one effect, and the modeled one is what a reviewer finds first.The row records that this finding's own first statement ("no
argv_commandstarting firecracker anywhere") was false and would have been refuted by its own counterexample. It also carries the count-first rule the near-misses on this branch produced: for an append-only carrier, the merge check is a count comparison against the base, not a read of the diff — a re-applied roster renders as reordering, which is exactly what a reviewer expects.Not in scope
The FCI-3 executor itself, and durable grant state. Durable state extends
gunbc.fabric_allocation_store_substratewhen that work is dispatched; it does not get a parallel store.🤖 Generated with Claude Code
https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN