Repository navigation
Fix latent red: fabric-membership claim follows srv1-13 (#12011) and srv2's refused width (#11762) - #12340
Merged
Conversation
…mber and srv2's refused width the_fabric_members_are_authored_identities_not_a_top_index_rule was false on main in two clauses (measured per clause: s3=2 s4=2 s1=1 s2=Unresolved): - srv1 `n == 0`: #12011 deliberately added srv1-13 (microVM shakedown slot, operator decision 2026-09-21) to fabric_execution_slot_identities and did not reach this file. The fold is right; the clause was stale. srv1-13 is now asserted as an authored identity like the others, and the count (1) follows from it. - srv2 `n == 0`: added by #11625, but since #11762 srv2's committed width is a typed refusal, so `derived_width_or_fail` is false by construction. Expecting 0 would be unknown-read-as-zero; the clause now asserts the count is UNRESOLVED. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Latent red on main (found by zesty-moth-868 on #12339):
the_fabric_members_are_authored_identities_not_a_top_index_ruleintest.claim.runner_slot_allocation_witnesswas false.Re-derivation (§6b). Measured per clause on main: srv3 fabric count = 2, srv4 = 2, srv1 = 1, srv2 = Unresolved. Two clauses were false, for two different reasons:
n == 0. microVM slot controller on srv1: the unit execs run_controller as MainPID, the 28 GiB shakedown slot, the reservation-authorized planner arm, the controller's release locus #12011 (0095b486bb) addedsrv1_microvm_shakedown_slot()(srv1-13) tofabric_execution_slot_identitieson purpose (operator decision 2026-09-21, documented at the roster). That change is justified. The witness was never reached, so its expectation went stale. The earliest unjustified link is this clause, not the fold. srv1-13 is now asserted as an authored identity (the law this claim guards), and the count of 1 follows from it.n == 0. Derive the runner memory envelope from the host, and give the fabric a second execution host #11625 (a6d1d2b194) wrote this clause, but Runner width is derived-or-unresolved-with-cause; unknown stops reading as zero #11762 had already made srv2's committed width a typed refusal (srv2_width_resolves_to_a_typed_refusal_naming_its_denominator). Soderived_width_or_failreturns false by construction, and the claim has been red since it landed. Expecting 0 there would be unknown read as zero (§5, the exact form Runner width is derived-or-unresolved-with-cause; unknown stops reading as zero #11762 removed). The clause now assertsresolution_is_unresolved.Receipts. I ran
gunbc run --source-root <probe> --source-root dag --source-root src/v2with a scratch ProcessExit wrapper that calls this claim together withthe_fabric_members_are_exactly_the_authored_identities. Result: main exit=1 (claim false), this head exit=0. The fold is unchanged.🤖 Generated with Claude Code