Repository navigation
Repair the two-homes corollary: the failure-mode roster is no longer a count - #10853
Closed
gunbai-bot[bot] wants to merge 1 commit into
Closed
gunbai-bot[bot] wants to merge 1 commit into
gunbai-bot[bot] wants to merge 1 commit into
Conversation
Co-authored-by: Cursor <cursoragent@cursor.com> #10822 dissolved the hand-appended roster the two-homes corollary still cited as 163-vs-173. The class and the command.dag specimen stand; inventing a replacement count for a directory would be a live name on a dead mechanism.
Contributor
Author
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Sep 8, 2026
…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
6 tasks
briansrls
added a commit
that referenced
this pull request
Sep 9, 2026
…#10674) * Compose the micro-VM launch plan, and mint the credential last 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 * temp: diagnostic arm probes for the launch fixture Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN * Take the VMM reserve as an input, and state that production admits no 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 * Observe whether a runner host can measure a VMM's footprint 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 * Import systemctl_version_command, which no local gate had checked 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 * Model the VMM footprint probe, sampled across guest sizes 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 * Convert mebibytes to bytes explicitly; pin the sizes in absolutes 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 * Convert the one mebibyte site a digits-only regex could not match 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 * Re-read the launch control now that the reserve is declared 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 * Require the execution grant, so the micro-VM is a realization under the 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 * Move the VMM footprint measurement to its own branch 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 * Join the grant to the reservation it authorizes, and split planning from 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 * Reduce to the authorization rule, and file what the two homes cost 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 * Record the count-first merge check on the two-homes row 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 * Restore two dark roster rows, and cut the launch-plan residue 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 * chore: regenerate drifted generated artifacts (ci auto-heal) 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 * Give the Demand and Offer joins their own discriminating REDs 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 * Delete the unconsumed seal, and restore two more dark roster rows 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 * chore: regenerate drifted generated artifacts (ci auto-heal) 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 * Declare the frontier for the rule this module keeps, and record a false 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 * Home the grant-authorization join beside the issuer, with typed refusal 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 * Scope the append-only-carrier corollary to carriers that are still a 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 * Fence the money reservation with the money generation, not the lease's 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 --------- Co-authored-by: Brian Searls <cutencool.work@gmail.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com> Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.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
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.
Summary
production_actuation_unmodeled_beside_a_modeled_probestill names the class: a modeled probe beside unmodeled production actuation, plus the corollary that an append-only list can drop a row on rebase with no visual signal.gunbc.recurring_failure_mode.roster(163 vs 173). Stop merging the failure-mode ledger on every append #10822 dissolved that list: membership is the row directory, and there is no list to count. Refreshing the name while leaving the count claim would bea_live_authority_name_carries_a_superseded_claim.extdeps.exec.commandadmit_callers/command.dag(67 vs 68) remains the live specimen. Count-vs-base stays the prescribed check for carriers that are still a list. No replacement count is invented for the dissolved roster.The row is not yet on
main(it lives on #10674). This PR files it with the citation already repaired so the prose edit is the subject, rather than a silent hunk on that other change.Test plan
namespace-wave-admissionadmits this addedRecurringFailureModerow (new row files currently refuse until that base-roster derivation lands).command.dagand still forbids inventing a roster count.Made with Cursor