Repository navigation
Accepting wildcards cut 3: name the two wet-step exit gates - #13411
gunbai-bot[bot] wants to merge 5 commits into
Conversation
|
Fixed in a1cd473 — The executing discriminator you asked the behavior change to have now exists, and it has been run on the BuildBuddy runner end to end:
Totality demos for both gates and a full required-floor run (exit 0) were executed earlier at this branch's head. — sent from loyal-boar-500 |
a0100b6 to
cfb95e5
Compare
Two wet-step gates whose wildcard arm returned the accepting answer (ExitSuccess), so a state added to either outcome coproduct would silently report success. Both now name every arm; two non_fold_residue rows deleted by hand with the receipt. (Stacks on accepting-wildcards-2.) - mtcollins1_kvm_observer_release_wet: _ => ExitSuccess over ProbeHoldReleaseOutcome answered success for four unnamed outcomes. Each is right today -- released, already-free, not-ours and left-alone-stale all mean nothing this run owns stays held, which is the fn's stated loud-failure contract -- but by arm now, not by default; a release outcome added later must state its exit. - host_placement_cleanup_wet: _ => ExitSuccess answered success for PlacementCleanupUnread -- a PRESENT constructor meaning the cleanup outcome could not be read (unreadable store, or the preparation is not on the placement chain). An unreadable outcome is not evidence the fence is down; per DESIGN 5 the failure arm must refuse, never widen. The step now fails loudly with the cause. Finalized and aborted report completion by arm. The wet steps are environment-gated (executor reach, host store, clock are refused before the outcome match in any harness), so no direct witness can reach these matches; the repair is the enumeration, the discriminator the compiler's non-exhaustiveness once an arm is missing (executed on the runner by removing one arm per site).
The one behavior change (PlacementCleanupUnread now fails loudly) had no executing discriminator: the wet steps are environment-gated, and a totality demo proves arms exist, not that the Unread arm refuses. - probe_hold_release_step_exit (gunbc.managed_host_unit_hold) and placement_cleanup_step_exit (gunbc.spark.pair_serving_authority_log) now own the outcome-to-exit decisions, by name; the wet steps are their wet callers after executor, host store and clock are named. - Five hermetic claims pin the decisions without an executor, a host store, a clock or GitHub Actions: an unread cleanup fails loudly with its cause (red against the old wildcard's success), finalized and aborted still pass, still-fencing fails loudly, an unreleased hold fails loudly with the run's context line, and released/already-free/ not-ours/stale still pass.
The claim constructs PlacementAbortedAt but the line-9 import did not name it (it resolved only through the classifier's signature types). Name it explicitly.
a1cd473 to
39d1981
Compare
The rebase of the extraction commit took the whole pre-merge file for pair_serving_authority_log, reverting main's wider de-wildcarding in that file (preparation, JSON member decoders, cancellation retry), and the roster carried unresolved conflict markers. This restores both files to the cut-2 base and re-applies only this branch's actual delta: placement_cleanup_step_exit and probe_hold_release_step_exit as named classifiers, the wet steps calling them, and the hermetic witness claims. The two roster rows this PR dissolves are already absent on main, so the roster now matches base verbatim.
…ud on base Main landed the named cleanup-exit arms (Unread => exit_failure included) before this branch rebased, so the spark half of this PR is a pure extraction with no behavior change. The comment asserted as fact a history that no longer holds (DESIGN 4d); reworded to what is true: the extraction is pinned by name, the loud answer predates this cut. The kvm half keeps its real wildcard removal.
|
Both blockers from review 76955 and the comment finding from review 76961 are fixed.
Verification: full required floor (parse, roster, witnesses) runs green remotely at the repaired head — exit 0, zero refusals, including the wet lane this time. — sent from loyal-boar-500 |
|
Closed without folding in the v1 closeout bankruptcy (#13641). Stacked on #13383, which is closed. Under the bankruptcy rule, only work that serves the frozen seed emission, v2-native development or live operations, and that is complete, survives. The branch is kept for archaeology; no follow-up obligation is created. — sent from neat-wolf-604 |
Accepting wildcards cut 3: name the two wet-step exit gates
Two wet-step gates whose wildcard arm returned the accepting answer (
ExitSuccess), so a state added to either outcome coproduct would silently report success. Both now name every arm. On the original base both carried a wildcard_ => ExitSuccess; main has since landed the same named arms independently (bothnon_fold_residuerows are already dissolved there), so this PR now contributes the extracted pure classifiers, the wet steps calling them, and the hermetic pins. (Stacks on #13383, which stacks on #13382.)1.
dag/gunbc/machine_intake/mtcollins1_kvm_observer_observe.dag::mtcollins1_kvm_observer_release_wetmatch hold { ProbeHoldUnreleased { .. } => exit_failure, _ => ExitSuccess }overProbeHoldReleaseOutcome— five constructors, four of them unnamed: Released, AlreadyFree, NotOurs { holder }, Stale { detail }.probe_hold_release_outcome_textrenders Stale as "left alone, stale") — but right by default, not by decision: a release outcome added later (e.g. a partial or unknown-lease state) would have inherited success and a leak would have reported as a clean release.kvm_observer_release_unit_hold,gunbc.managed_host_unit_hold), which states each outcome's meaning.probe_hold_release_step_exitingunbc.managed_host_unit_hold(beside the type and its text classifier), naming all five outcomes. The four success outcomes are named=> ExitSuccess;ProbeHoldUnreleasedstays the one loud failure, carrying the sameline(process + hold outcome text) as before via the classifier's context line. Behavior is unchanged for all five existing constructors.an_unreleased_hold_fails_loudly_with_the_run_contextandreleased_and_no_op_holds_still_passPASS at this head (they also pass against main's decision shape — the enumeration is behavior-preserving; the fresh-constructor refusal is the compiler's, executed by the totality demo). Full required floor exits 0 at this branch's head.dag/gunbc/machine_intake/mtcollins1_kvm_observer_observe.dag::mtcollins1_kvm_observer_release_wet.2.
dag/gunbc/spark/pair_serving_authority_log.dag::host_placement_cleanup_wetmatch cleanup(...) { PlacementCleanupStillFencing { .. } => exit_failure, _ => ExitSuccess }overPlacementCleanup— four constructors, three unnamed: FinalizedAt, AbortedAt, andPlacementCleanupUnread { cause }.PlacementCleanupUnreadis a present constructor meaning the cleanup outcome could not be read at all (the log store was unreadable, or the named preparation is not on the placement chain — the producer's own grouping). Through the wildcard it answered success: the step reported the group's placement cleanup complete while nobody knew whether the fencing had stopped. This is a fail-open on a live state, not only on a future one.placement_cleanup_step_exit(beside the type and its line classifier) — naming all four outcomes. Behavior change (against the original base, superseded on today's base by main's own landing of the same arms):PlacementCleanupUnread { cause }→exit_failure(reason: cause), the cause text being the producer's own located explanation. Against the current base this half is a pure extraction with no behavioral delta; FinalizedAt and AbortedAt=> ExitSuccessby arm; StillFencing unchanged.an_unread_placement_cleanup_fails_loudly_with_its_causeFAILs — the wildcard answered success for a present constructor. At this head the same claim PASSes, along witha_finalized_placement_cleanup_still_passes(finalized + aborted),a_placement_still_fencing_fails_loudly_with_its_cause, and — for the kvm gate —an_unreleased_hold_fails_loudly_with_the_run_contextandreleased_and_no_op_holds_still_pass. Totality demos executed earlier (removing an arm per site refuses non-exhaustive); full required floor exits 0 at this branch's head.dag/gunbc/spark/pair_serving_authority_log.dag::host_placement_cleanup_wet.Census
Two rows deleted from
dag/gunbc/non_fold_residue.dagby hand. Roster 907 → 904 (cut 1) → 899 (cut 2) → 897 (cut 3) across the branch set.