Reduce the micro-VM module to the grant authorization rule FCI-2 owns

dag/gunbc/product/fabric/grant_issue.dag

@@ -20,7 +20,7 @@ import product.fabric.supply {
 import product.fabric.work { Work }
 import product.fabric.budget {
   MoneyAccount, MoneyReservationRequest, MoneyRefusal,
-  AccountAdvanced, MoneyRefused, reserve_money,
+  AccountAdvanced, MoneyRefused, reserve_money, fence_admits,
 }
 import extdeps.accounting.encumbrance {
   EncumbranceLedger, EncumbranceRefusal,
@@ -436,3 +436,76 @@ fn issue_grant<P, Q, S>(
     }
   }
 }
+
+// DECLARED FRONTIER (DESIGN 3c). grant_authorizes_reservation has NO production consumer in this
+// change: its only caller is test.claim.fabric_grant_authorization_witness, which exercises it
+// rather than asserting it exists. NAMED CONSUMER: the FCI-3 executor, whose exit predicate in
+// gunbc.fabric_ci_program is that a persistent executor re-reads the committed Grant before
+// starting and that an absent, corrupt or expired Grant yields zero target processes -- this rule
+// is the agreement half of that re-read. TRIGGER, stated because a frontier without one is a
+// dangling declaration: the rule stays uncalled until FCI-3 lands an executor that re-reads a
+// committed grant. It is homed here, beside issue_grant, so that consumer imports one fabric
+// module rather than reaching into a runner-layer module for fabric vocabulary.
+
+// THE AGREEMENT COUNTERPART OF issue_grant, HOMED BESIDE THE ISSUER RATHER THAN AT A CONSUMER.
+// A grant that fences money proves the money; it proves nothing about WHICH execution was
+// authorized. Presented against another cell's reservation it would pass whenever the supplied
+// account fenced -- and that is worse than no grant, because the grant's presence reads as
+// authorization while authorizing nothing about the subject. The grant carries work, demand and
+// offer, and a reserved cell carries its own, so the join is available and is made here.
+
+// THE MONEY GENERATION IS PRESENTED, NOT READ OFF THE GRANT, BECAUSE THE GRANT DOES NOT CARRY IT.
+// ExecutionGrant.money_reservation is a bare ReservationRef; the counter the account holds for that
+// reference was recorded from the MONEY request (product.fabric.budget reserve_money writes
+// `generation: request.generation`), while grant_lease_generation answers the RESOURCE lease's
+// counter. Those are two independently advancing counters, and an earlier revision of this rule
+// fenced the money reservation with the lease generation -- so a grant authorized whenever the two
+// happened to coincide, and a legitimate grant whose counters had diverged was refused with a cause
+// naming the wrong fact. product.fabric.execution already records that class one authority over:
+// comparing generations alone was a real fencing hole, and it made prose describe a wall the code
+// did not build. Presenting it keeps the join between two independently authored facts -- what the
+// issuer requested against what the account recorded -- rather than between one fact and itself.
+
+// IT TAKES THE COORDINATES RATHER THAN A SNAPSHOT, AND THAT IS WHAT MAKES ITS RED AUTHORABLE.
+// RequiredBuildCellSnapshot is sole_constructor, so no witness outside its module can build a
+// DISAGREEING one; a rule reading the snapshot directly would have an unauthorable RED and be a
+// DESIGN 4b decoration -- permanently green and cited as coverage. FabricIdentity is an ordinary
+// record, so over coordinates the disagreement is writable, and four claims write it.
+
+// WHAT THIS DOES NOT ESTABLISH, stated because the name would otherwise read as more than it is:
+// ExecutionGrant is an ordinary constructible record, so a caller can author one. This proves
+// AGREEMENT between a presented grant and a presented reservation, not that fabric issuance
+// durably committed either. The unforgeable form re-reads the committed grant from durable storage
+// after the submitter terminates -- FCI-3's own exit predicate, and not something a pure rule can
+// assert about itself.
+type GrantAuthorization
+  = GrantAuthorizes
+  | GrantFenceRefused
+  | GrantAuthorizesDifferentWork
+  | GrantAnswersDifferentDemand
+  | GrantIssuedAgainstDifferentOffer
+
+fn grant_authorizes_reservation(
+  grant: ExecutionGrant<NonEmptyStr>,
+  account: MoneyAccount,
+  money_generation: Int,
+  work: FabricIdentity<NonEmptyStr, WorkKey>,
+  demand: FabricIdentity<NonEmptyStr, DemandKey>,
+  offer: FabricIdentity<NonEmptyStr, OfferKey>,
+) -> GrantAuthorization {
+  if !fence_admits(
+    a: account,
+    reference: grant.money_reservation,
+    presented: money_generation,
+  ) {
+    GrantFenceRefused
+  } else if !fabric_identity_eq(left: grant.context.work, right: work) {
+    GrantAuthorizesDifferentWork
+  } else if !fabric_identity_eq(left: grant.context.demand, right: demand) {
+    GrantAnswersDifferentDemand
+  } else if !fabric_identity_eq(left: grant.object.offer, right: offer) {
+    GrantIssuedAgainstDifferentOffer
+  } else {
+    GrantAuthorizes
+  }
+}

dag/gunbc/recurring_failure_mode/production_actuation_unmodeled_beside_a_modeled_probe.dag

@@ -0,0 +1,30 @@
+module gunbc.recurring_failure_mode.production_actuation_unmodeled_beside_a_modeled_probe
+
+import std.types { NonEmptyStr }
+import gunbc.recurring_failure_mode { RecurringFailureMode }
+
+data production_actuation_unmodeled_beside_a_modeled_probe: RecurringFailureMode = RecurringFailureMode {
+  identity: "production_actuation_unmodeled_beside_a_modeled_probe" as NonEmptyStr,
+
+  receipts: [
+    "**PRODUCTION ACTUATION UNMODELED BESIDE A MODELED PROBE** (INVALID STATE: one effect -- what CAUSES a thing to happen -- has two homes. The install path and a probe of the effect are modeled as ArgvCommand and executed through the modeled transport, so the corpus reads as owning the effect; the path PRODUCTION actually takes is hand-authored outside .dag, and .dag carries RECEIPTS of it after the fact. Both homes are honest on their own. Together they answer one question twice, and the modeled half is the one a reader finds first. ",
+
+    "HARM, AND IT IS THE READING KIND RATHER THAN A RUNTIME ONE. A reviewer asking 'is this effect modeled' greps, finds modeled argv and a witness asserting its flags, and concludes yes. The production path is not covered by that witness and cannot be, because the witness ranges over the probe's construction. So every guarantee argued from the modeled half is argued about a route production does not take, and the gap is invisible precisely where the corpus looks strongest. It also compounds: each new model authored against the unconsumed home adds mass to the wrong side, and each receipt authored against the live one adds prose where a fold should be. ",
+
+    "SPECIMEN WITH A RECEIPT, gunbc micro-VM runners, 2026-09-08. Mt. Collins runs real GitHub Actions jobs in a per-job micro-VM (#10733, run 34108061111, runner-canary-8). What is modeled: runner_microvm_host_ready firecracker_fetch_commands and firecracker_install_commands, as ArgvCommand lists run through run_shell_commands with LocalExec -- so INSTALL is modeled; and runner_microvm_boot_probe_witness_test, which asserts --no-api and --config-file on a modeled launch argv -- so a boot PROBE launch is modeled. What is NOT modeled is the launch real jobs take: runner_bound_attempt_receipt execution_chain is a List<NonEmptyStr> of prose describing the jailer exec, and the actuation itself is host tooling outside the substrate. ",
+
+    "THE PRECISION MATTERS AND THE FIRST STATEMENT OF THIS FINDING FAILED IT. The finding was first reported as 'no argv_command starting firecracker anywhere', which is false and a reviewer would have found the two exceptions immediately, discrediting a real defect. The defensible form names the three states separately: install modeled, probe modeled, production actuation not. A finding that overstates its scope is refuted by its own counterexample and the underlying gap survives unaddressed. ",
+
+    "DISTINGUISHING FACTS, because three neighbours are close. It is not `unmodeled realization` alone -- raw shell implementing semantics expressible in .dag -- since here a modeled expression EXISTS and production simply does not route through it; the defect is the fork, not the absence. It is not `parallel_representation_debt` in the ordinary sense of two data shapes for one value, because these two homes differ in KIND: one is a fold that could execute, the other is prose recording that something executed. And it is not the receipt pattern being wrong -- observing a live effect is correct and necessary; what makes this a class is a modeled route sitting BESIDE the observed one while nothing joins them. ",
+
+    "RECOGNITION RULE, checkable before the model is authored: for an effect the corpus models, ask which route PRODUCTION takes and name it. If the answer is 'a different one', the model is not coverage of that effect no matter how thorough its witness -- and adding to the model widens the fork. The tell in a diff is a new modeled effect path landing with zero importers while a receipt module for the same effect already carries prose rows. ",
+
+    "RUNG FOUND AT: 1 (mitigatable) -- the fork is visible to a reader who asks the recognition question, and nothing structural prevents authoring the second home. CEILING: 3 (structurally guaranteed), because the property is decidable from the module graph: whether an effect declared in .dag has a production consumer at execution is exactly the reachability question the impact-query lens already answers over the Node tree. It is not 4, because the hand-authored route lives outside the substrate and its absence cannot be made unrepresentable by any construction inside it. ",
+
+    "COROLLARY ON DETECTING THE FORK'S NEAREST COUSIN, AN APPEND-ONLY CARRIER SILENTLY LOSING ROWS. For any append-only carrier that is still a LIST -- a roster, an admit_callers list -- THE MERGE CHECK IS A COUNT COMPARISON AGAINST THE BASE, NOT A READ OF THE DIFF. A branch that re-applies its own rows onto a moved base renders as REORDERING, which is exactly what a reviewer expects a rebased roster to look like, so a row another lane appended after the branch point disappears with no visual signal. The count raises the alarm and the identity join says which row; neither alone is sufficient, and the diff is blind to both. SURVIVING SPECIMEN: `extdeps.exec.command` `command.dag` at 67 rows on main against 68 on a branch that had added two -- `admit_callers` is still that list. SUPERSEDED FOR ONE CARRIER ONLY: the failure-mode roster at 163 against 173. gunbc#10822 (aac9545a53) deleted the hand-appended `gunbc.recurring_failure_mode.roster` list; membership is now the row DIRECTORY, and there is no list to count. Refreshing that citation as if the roster were still countable would be `a_live_authority_name_carries_a_superseded_claim`. Do not invent a replacement count for the dissolved roster; directory membership is a different subject. ",
+
+    "NEXT-RUNG TRIGGER, named as the capability rather than an artifact: A JOIN THAT, FOR EACH DECLARED EFFECT PATH, ANSWERS WHETHER A PRODUCTION CONSUMER REACHES IT AT EXECUTION, and refuses a modeled effect that has none while a receipt module for the same subject exists. It must be SUFFICIENT FOR the general case -- any effect, not a per-module allowlist -- and a census that merely counts unconsumed modules CONTRIBUTES to it without retiring it, because the load-bearing half is the join to the receipt subject, not the count.",
+  ],
+
+  evidence: [],
+}