Skip to content

NO-FALLBACK-0: a plan records completed decisions, and an ineligible candidate has no eligible cause - #9779

Merged
gunbai-bot[bot] merged 4 commits into
mainfrom
session/silent-crab-842-nofallback
Aug 31, 2026
Merged

gunbai-bot[bot] merged 4 commits into
mainfrom
session/silent-crab-842-nofallback

Conversation

@briansrls

@briansrls briansrls commented Aug 30, 2026 •

Copy link
Copy Markdown
Contributor

NO-FALLBACK-0 for boot artifact delivery. A delivery plan must name one transport and state, for every other candidate, why it is not one — never leave a second usable transport sitting in the plan for an executor to try when the first fails. Ordered fallback is the workflow this model exists to refuse.

What was wrong

Solving asks "is this candidate eligible"; a plan answers "this is the transport, and here is why every other candidate is not one". Those are different questions and they shared one type, so a plan could carry a second CandidateEligible verdict beside the selected one. An executor holding that plan reads it as the next thing to attempt.

What changed

Plan dispositions are their own vocabulary. BootDeliveryPlanCandidateDisposition = PlanCandidateSelected | PlanCandidateOutrankedBy { selected } | PlanCandidateIneligible { cause }. A candidate the policy outranked is recorded as outranked by the transport that was chosen, naming it, so the row states a completed decision rather than a standing offer. There is deliberately no arm meaning "eligible and not selected". BootDeliveryEligibilityProvenance.considered now carries these plan verdicts.

Ineligibility is a refusal-only coproduct. BootDeliveryCandidateIneligibility holds every named refusal cause and has no eligible inhabitant; BootDeliveryCandidateStanding = CandidateEligible | CandidateIneligible { cause }. The plan's ineligible arm carries the refusal-only type, so an ineligible candidate whose cause is that it was eligible — a contradictory row asserting a spare available transport inside a plan — has no constructor rather than merely no producer. This is construction where the previous cut left validation: the old type admitted the state and relied on the producer not to emit it.

Selection is named for what it is. first_eligible_boot_artifact_delivery became selected_boot_artifact_delivery; "first eligible" is the fallback vocabulary this change removes.

Evidence

  • The refusal-only wall is proven where its RED is authorable. The violation can no longer be written in the accepted corpus, so asking for the refusal inside the corpus would be a permanently-green decoration (DESIGN §4b). It is instead expressed as source handed to the compiler by a fixture in test.claim.machine_intake.no_fallback_plan_ineligibility_wall_test: the RED places CandidateEligible in the plan's ineligible arm and is refused with a blocking TypeMismatch; the positive control places a real ineligibility cause and still compiles, so a green RED cannot be attributed to a typo or a broken import. Both execute.
  • The existing boot delivery witnesses, including the two-eligible execution control and the contradictory-probe refusal, run against the migrated types.
  • 29 production and 24 witness construction sites migrated to the refusal-only cause.

Not claimed

This does not make every fallback-shaped state unwritable across the delivery model; it closes the plan-disposition class named above. The reviewing authority's remaining items for this PR are tracked in the machine-intake ruling thread.

THE HAZARD WAS NOT THE RANKING WALK, IT WAS WHAT THE PLAN CARRIED. Eligibility
is settled from evidence before any ranking happens, so walking the policy order
attempts nothing -- but the plan then carried the raw solving verdicts, and when
two transports were eligible it handed an executor a second CandidateEligible
row beside the selected one. That row IS the next thing to try, and an executor
holding it can turn a terminal refusal into an ordered search.

A plan now carries BootDeliveryPlanCandidateDisposition:

  PlanCandidateSelected
  PlanCandidateOutrankedBy { selected: BootDeliveryCandidate }
  PlanCandidateIneligible { standing: BootDeliveryCandidateStanding }

There is deliberately no arm meaning "eligible and not selected", so an
available alternative has NO REPRESENTATION in a plan -- construction, not a
check that could be satisfied by editing a declaration. A candidate the policy
outranked names the transport that beat it, so the row states a completed
decision rather than an offer. The raw standing survives on the refusal path,
where nothing was selected and the whole considered set is the evidence.

The candidate identity travels on BuiltBootArtifactDelivery, so a disposition is
decided by IDENTITY against the selection rather than by position in the
preference list, and first_eligible_boot_artifact_delivery is renamed
selected_boot_artifact_delivery: it ranks a set already decided, and the old
name described a search.

THE CREDENTIAL HALF. megarac_factory_login said the published password is "the
first credential to TRY", which is an ordered search with an implied next. There
is no next: a refusal is a terminal typed fact about the unit (rotated, or a
differently-shipped ODM build) carried by a workflow-layer intake receipt.
Guessing again is both the fallback this model refuses and how a fleet locks
itself out.

THE WITNESS IS THE TWO-ELIGIBLE CASE, which is the only shape that separates a
plan from a fallback list -- every other plan control asserts which transport was
selected, and a model that also ships a spare satisfies those identically. The
fixture's profile and live observation admit BOTH Redfish VirtualMedia and the
MegaRAC REST surface, so the policy has a real loser to record: exactly one
PlanCandidateSelected, it is Redfish, and at least one row is
PlanCandidateOutrankedBy naming Redfish. That last clause is what keeps the test
non-vacuous.

DISCRIMINATING, PROVEN BY MUTATION: with the outranked arm replaced so an
eligible unselected candidate stays selected-shaped, the witness returns false;
true with the repair. Corpus parse-clean at 4406 files; the boot-delivery
witnesses evaluate true.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019fKvi5dnJ8TcE514qbmWTk
@gunbai-bot gunbai-bot Bot changed the title INTAKE-N + BOOTDELIVERY-N NO-FALLBACK-0: a plan records completed decisions, and an ineligible candidate has no eligible cause Aug 31, 2026
Reviewing authority's hold on NO-FALLBACK-0. PlanCandidateIneligible carried
the whole BootDeliveryCandidateStanding, and that coproduct contains
CandidateEligible, so this was authorable:

    PlanCandidateIneligible { standing: CandidateEligible }

a candidate recorded as ineligible whose stated cause is that it was eligible
— a spare available transport sitting inside a plan, which is the exact state
NO-FALLBACK-0 exists to forbid. No producer emitted it, but the type admitted
it, so the guarantee rested on the producer's restraint. That is validation
standing where construction was available (DESIGN §5).

BootDeliveryCandidateIneligibility is now a refusal-only coproduct carrying
every named cause and no eligible inhabitant, and standing is the two-arm sum
CandidateEligible | CandidateIneligible { cause }. The plan's ineligible arm
carries the refusal-only type, so the contradictory row has no constructor
rather than merely no producer. 29 production and 24 witness construction and
pattern sites migrated to the nested cause.

THE WALL IS PROVEN WHERE ITS RED IS AUTHORABLE. The violation can no longer be
written in the accepted corpus, so a check for it inside the corpus would be
permanently green by construction — a decoration that would later be cited as
coverage (§4b). §4b names the boundary that decides this: a state
unrepresentable in the accepted corpus may still be representable as source
handed to the compiler by a fixture. no_fallback_plan_ineligibility_wall_test
does exactly that. The RED places CandidateEligible in the plan's ineligible
arm and is refused with a blocking TypeMismatch; the positive control places a
real ineligibility cause and still compiles, so a green RED cannot be
attributed to a typo or a broken import. Both execute.

The PR's placeholder title and auto-opened TODO body are replaced with the
actual NO-FALLBACK-0 summary and evidence.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019fKvi5dnJ8TcE514qbmWTk
@gunbai-bot
gunbai-bot Bot merged commit 1acdd1a into main Aug 31, 2026
5 checks passed
@gunbai-bot
gunbai-bot Bot deleted the session/silent-crab-842-nofallback branch August 31, 2026 17:30
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant