Accepting wildcards refuse instead of widening: arrow-contract walls, neutral verdicts, and the wet-step exit gates (re-derives #13382, #13383, #13411)

dag/gunbc/fleet/fleet_revision_acceptance.dag

@@ -435,20 +435,27 @@ fn run_is_merge_group(run: WorkflowRun) -> Bool {
   run.event == github_event_name_merge_group
 }
 
+// A run carries a verdict when GitHub states a terminal outcome for it: Success, Failure,
+// TimedOut, ActionRequired and StartupFailure say what happened. Neutral, Cancelled and Skipped
+// report that no verdict was rendered -- the run did not judge the revision -- so they are not
+// verdicts, and an unconcluded floor refuses as RequiredCiMergeGroupRunUnconcluded. A run that
+// has not completed (Queued, InProgress, Waiting, Requested, Pending) has rendered nothing yet.
+// Every status and every conclusion is named so an addition to either cannot inherit
+// verdict-carrying without an arm.
 fn merge_group_run_carries_verdict(run: WorkflowRun) -> Bool {
   match run.status {
     Completed =>
       match run.conclusion {
         Present { value: c } =>
           match c {
-            Cancelled => false
-            Skipped => false
             Success => true
             Failure => true
-            Neutral => true
             TimedOut => true
             ActionRequired => true
             StartupFailure => true
+            Neutral => false
+            Cancelled => false
+            Skipped => false
           }
         none => false
       }

dag/gunbc/host/managed_host_unit_hold.dag

@@ -683,6 +683,21 @@ fn probe_hold_release_outcome_text(o: ProbeHoldReleaseOutcome) -> String {
   }
 }
 
+// THE HOLD EXIT IS DECIDED BY THE OUTCOME, BY NAME. The release step fails loudly only when
+// something this run owns stays held (Unreleased); released, already-free, not-ours and
+// left-alone-stale each report that nothing of ours is held -- by arm, not by wildcard, so a
+// release outcome added later must state its exit here instead of inheriting success. The caller
+// owns the failure's wording; this fn owns the decision.
+fn probe_hold_release_step_exit(o: ProbeHoldReleaseOutcome, context_line: String) -> ProcessExit {
+  match o {
+    ProbeHoldReleased => ExitSuccess
+    ProbeHoldAlreadyFree => ExitSuccess
+    ProbeHoldNotOurs { holder: _ } => ExitSuccess
+    ProbeHoldStale { detail: _ } => ExitSuccess
+    ProbeHoldUnreleased { cause: _ } => exit_failure(reason: context_line)
+  }
+}
+
 fn kvm_observer_release_unit_hold(host: HostIdentity, run_id: NonEmptyStr) -> ProbeHoldReleaseOutcome
   admit_callers: [
     decl_ref(module_path: "gunbc.machine_intake_megarac_kvm_observer_observe", decl_name: "megarac_kvm_observer_release"),

dag/gunbc/machine_intake/megarac_kvm_observer_observe.dag

@@ -12,8 +12,7 @@ import gunbc.owned_process { OwnedRelease, OwnedReleased, OwnedAlreadyGone, Owne
 import gunbc.megarac_managed_host { AdmittedMegaRacHost, admitted_megarac_host_identity }
 import gunbc.managed_host_unit_hold {
   UnitHeld, UnitHoldRefused, kvm_observer_acquire_unit_hold, unit_hold_release,
-  ProbeHoldReleased, ProbeHoldAlreadyFree, ProbeHoldNotOurs, ProbeHoldStale, ProbeHoldUnreleased,
-  kvm_observer_release_unit_hold, probe_hold_release_outcome_text,
+  kvm_observer_release_unit_hold, probe_hold_release_outcome_text, probe_hold_release_step_exit,
 }
 import gunbc.machine_intake_megarac_kvm_still {
   KvmObserverRecord, KvmObserverStart, KvmObserverStarted, KvmObserverNotStarted,
@@ -268,8 +267,5 @@ fn megarac_kvm_observer_release(host: HostIdentity, run_id: NonEmptyStr, paths:
   }
   let hold = kvm_observer_release_unit_hold(host: host, run_id: run_id)
   let line = join(["megarac kvm observer release: process ", owned_release_text(r: process), "; unit hold ", probe_hold_release_outcome_text(o: hold)], "")
-  match hold {
-    ProbeHoldUnreleased { cause: _ } => exit_failure(reason: line)
-    _ => ExitSuccess
-  }
+  probe_hold_release_step_exit(o: hold, context_line: line)
 }

dag/gunbc/non_fold_residue.dag

@@ -766,11 +766,8 @@ data non_fold_residue_frontier: List<FrontierRow> = [
   FrontierRow { subject: PathSubject { path: "src/v2/lens/text_string_importer_census.dag::position_is_structural" }, reason: nfr_reason_typed_census_ca5ed1724b, dissolution: nfr_dissolve_owning_fold },
   FrontierRow { subject: PathSubject { path: "src/v2/lens/text_string_importer_census.dag::position_is_unresolved" }, reason: nfr_reason_typed_census_ca5ed1724b, dissolution: nfr_dissolve_owning_fold },
   FrontierRow { subject: PathSubject { path: "src/v2/std/arrow_contract.dag::arrow_contract_atom_is_self_named" }, reason: nfr_reason_typed_census_ca5ed1724b, dissolution: nfr_dissolve_owning_fold },
-  FrontierRow { subject: PathSubject { path: "src/v2/std/arrow_contract.dag::arrow_effect_claims_edge_target_reads" }, reason: nfr_reason_typed_census_ca5ed1724b, dissolution: nfr_dissolve_owning_fold },
   FrontierRow { subject: PathSubject { path: "src/v2/std/arrow_contract.dag::arrow_effect_claims_target_conforms" }, reason: nfr_reason_typed_census_ca5ed1724b, dissolution: nfr_dissolve_owning_fold },
   FrontierRow { subject: PathSubject { path: "src/v2/std/arrow_contract.dag::arrow_execution_mode_claim_target_conforms" }, reason: nfr_reason_typed_census_ca5ed1724b, dissolution: nfr_dissolve_owning_fold },
-  FrontierRow { subject: PathSubject { path: "src/v2/std/arrow_contract.dag::arrow_execution_mode_edge_target_reads" }, reason: nfr_reason_typed_census_ca5ed1724b, dissolution: nfr_dissolve_owning_fold },
-  FrontierRow { subject: PathSubject { path: "src/v2/std/arrow_contract.dag::arrow_resource_requirements_edge_target_reads" }, reason: nfr_reason_typed_census_ca5ed1724b, dissolution: nfr_dissolve_owning_fold },
   FrontierRow { subject: PathSubject { path: "src/v2/std/compilers/target_model.dag::target_value_expr_record_construct_type_name_optional" }, reason: nfr_reason_typed_census_ca5ed1724b, dissolution: nfr_dissolve_owning_fold },
   FrontierRow { subject: PathSubject { path: "src/v2/std/compilers/target_model.dag::target_value_semantics_carrier_snoc" }, reason: nfr_reason_typed_census_ca5ed1724b, dissolution: nfr_dissolve_owning_fold },
   FrontierRow { subject: PathSubject { path: "src/v2/std/datetime.dag::calendar_date_admits" }, reason: nfr_reason_typed_census_ca5ed1724b, dissolution: nfr_dissolve_owning_fold },

dag/gunbc/runner/runner_throughput_qualification_route.dag

@@ -362,7 +362,9 @@ fn route_control_plane_write_count(route: List<QualificationStage>) -> Int {
   )
 }
 
-// EVERY BMC WRITE IS UNDER THE APPROVAL GATE, by declaration identity.
+// EVERY BMC WRITE IS UNDER THE APPROVAL GATE, by declaration identity. The arms are named, not
+// wildcarded: a stage effect added later must state here what the gate audit reads from it, or the
+// route stops compiling -- a fresh write-shaped effect may not inherit the audit's pass.
 fn route_bmc_writes_are_gated(route: List<QualificationStage>) -> Bool {
   route |> all(s =>
     match stage_effect(stage: s) {
@@ -414,6 +416,8 @@ fn route_deregisters_what_it_registered(route: List<QualificationStage>) -> Bool
     && (registered |> all(u => deregistered |> any(d => d == u)))
 }
 
+// Only a dispatch stage is asked to name the attempt; the other four stages say so by name, not
+// by wildcard, so a stage added later must state that here rather than inherit the vacuous pass.
 fn route_dispatch_selector_names_the_attempt(route: List<QualificationStage>, attempt: NonEmptyStr) -> Bool {
   route |> all(s =>
     match s {

dag/gunbc/spark/pair_serving_authority_log.dag

@@ -2097,6 +2097,19 @@ fn placement_cleanup_line(c: PlacementCleanup) -> String {
   }
 }
 
+// THE CLEANUP EXIT IS DECIDED BY THE OUTCOME, BY NAME. Finalized and aborted report completion;
+// still-fencing fails loudly; and an UNREADABLE outcome is not evidence that the fence is down, so
+// it fails loudly with its cause too -- a failure arm must refuse, never widen (DESIGN 5). A
+// cleanup state added later must state its exit here instead of inheriting success.
+fn placement_cleanup_step_exit(c: PlacementCleanup) -> ProcessExit {
+  match c {
+    PlacementFinalizedAt { preparation: _, id: _ } => ExitSuccess
+    PlacementAbortedAt { preparation: _, id: _ } => ExitSuccess
+    PlacementCleanupStillFencing { preparation: _, cause: why } => exit_failure(reason: why)
+    PlacementCleanupUnread { cause: unread } => exit_failure(reason: unread)
+  }
+}
+
 // THE OPERATOR'S ENTRIES, for a saga that died between its steps. The group is the preparation's
 // own, read from the record. Finalize when the authority event landed (the join finds it); abort
 // when it did not, under a typed disposition of the writer that claimed the append:
@@ -2124,6 +2137,8 @@ fn host_placement_abort_wet(preparation: String, reason: String, claimant: Strin
   }
 }
 
+// The outcome-to-exit decision is placement_cleanup_step_exit, by name; this step is its wet
+// caller, after the executor, the host store and the clock are identified.
 fn host_placement_cleanup_wet(preparation: String, cleanup: fn(FabricStorageBinding, NonEmptyStr, EpochSecs) -> PlacementCleanup) -> ProcessExit
 {
   match observe_executor_reach() {
@@ -2134,13 +2149,7 @@ fn host_placement_cleanup_wet(preparation: String, cleanup: fn(FabricStorageBind
         HostStoreResolved { store: store, executor: _ } =>
           match now_epoch_seconds() {
             Absent => exit_failure(reason: "the clock could not be read as epoch seconds")
-            Present { value: at } =>
-              match cleanup(store, executor as NonEmptyStr, at) {
-                PlacementCleanupStillFencing { preparation: _, cause: why } => exit_failure(reason: why)
-                PlacementFinalizedAt { preparation: _, id: _ } => ExitSuccess
-                PlacementAbortedAt { preparation: _, id: _ } => ExitSuccess
-                PlacementCleanupUnread { cause: why } => exit_failure(reason: why)
-              }
+            Present { value: at } => placement_cleanup_step_exit(c: cleanup(store, executor as NonEmptyStr, at))
           }
       }
   }

dag/test/claim/fleet/fleet_desired_merge_queue_admission_witness_test.dag

@@ -5,7 +5,7 @@ import std.contract_identity { ContractEpoch }
 import extdeps.git.object_store { GitObjectId, git_object_id_from_untagged_hex, git_object_id_eq }
 import extdeps.github.workflow_runs {
   WorkflowRun, WorkflowRunList, WorkflowRunStatus, WorkflowRunConclusion,
-  Completed, InProgress, Queued, Success, Failure, Cancelled, TimedOut,
+  Completed, InProgress, Queued, Success, Failure, Cancelled, Neutral, TimedOut,
 }
 import extdeps.github.push_event { PushRefUpdate, push_ref_update_from_event_json, PushRefUpdateObserved, PushRefUpdateMemberAbsent }
 import gunbc.generated_artifact { WitnessFloorYamlArtifact, artifact_path }
@@ -118,6 +118,26 @@ test fn a_cancelled_run_beside_a_success_admits() -> Bool {
   admits(push: main_push(after: sha_r), rs: runs(rs: [mg(id: 11, conclusion: Cancelled), mg(id: 12, conclusion: Success)]))
 }
 
+// NO VERDICT RENDERED IS NOT A FAILED VERDICT. A neutral conclusion reports that the workflow did
+// not apply to this revision; it carries no verdict, so a floor of only-neutral runs is
+// UNCONCLUDED -- not "the floor ran and did not succeed", which is a different refusal and a
+// different operator action. merge_group_run_carries_verdict names all eight conclusions so a
+// conclusion added later cannot inherit verdict-carrying without an arm.
+test fn a_floor_of_neutral_runs_refuses_as_unconcluded_not_not_success() -> Bool {
+  match ci_on_r(rs: runs(rs: [mg(id: 11, conclusion: Neutral)])) {
+    Present { value: RequiredCiRefused { cause: RequiredCiMergeGroupRunUnconcluded { revision: _, run_ids: ids } } } =>
+      ids == [11]
+    _ => false
+  }
+}
+
+// A neutral run beside a success neither contradicts it nor blocks the entry: not applicable is
+// not a competing verdict, and the refusal it caused before the classification named Neutral
+// as non-verdict read as two runs disagreeing about one revision.
+test fn a_neutral_run_beside_a_success_admits() -> Bool {
+  admits(push: main_push(after: sha_r), rs: runs(rs: [mg(id: 11, conclusion: Neutral), mg(id: 12, conclusion: Success)]))
+}
+
 // THE CONTRADICTION. Nothing picks one: the refusal carries both id sets so an operator reads both logs.
 test fn a_success_and_a_failure_on_one_revision_refuse_carrying_both_run_ids() -> Bool {
   match ci_on_r(rs: runs(rs: [mg(id: 11, conclusion: Success), mg(id: 12, conclusion: Failure)])) {

dag/test/claim/host/managed_host_unit_hold_witness_test.dag

@@ -20,7 +20,7 @@ import gunbc.managed_host_unit_hold {
   unit_hold_refusal, operator_maintenance_owner, boot_run_owner, host_reset_owner,
   ProbeHoldReleaseDecision, ProbeHoldReleaseAt, ProbeHoldFreeNoop, ProbeHoldForeignNoop, ProbeHoldUnobservable,
   ProbeHoldReleaseOutcome, ProbeHoldReleased, ProbeHoldAlreadyFree, ProbeHoldNotOurs, ProbeHoldStale, ProbeHoldUnreleased,
-  probe_hold_release_decision, probe_hold_release_refused, probe_hold_release_committed,
+  probe_hold_release_decision, probe_hold_release_refused, probe_hold_release_committed, probe_hold_release_step_exit,
   HolderLivenessRoute, HolderObserveProcess, HolderNotObservable, holder_liveness_route,
   UnitHoldSubjectAdmitted, UnitHoldNotRequired, admit_unit_hold_subject,
   UnitHoldHostAdmitted, UnitHoldHostNotManaged, UnitHoldHostNotRequired,
@@ -400,3 +400,22 @@ test fn a_probe_holder_is_observed_by_its_process_and_a_processless_one_is_not()
       _ => false
     })
 }
+
+// THE HOLD EXIT IS A HERMETIC DECISION: probe_hold_release_step_exit answers each release outcome
+// by name, so the wet step's verdict is pinned here without GitHub Actions, a journal or a store.
+// ONLY UNRELEASED IS LOUD -- released, already-free, not-ours and left-alone-stale each report
+// that nothing this run owns stays held -- and the failure carries the run's context line.
+test fn an_unreleased_hold_fails_loudly_with_the_run_context() -> Bool {
+  match probe_hold_release_step_exit(o: ProbeHoldUnreleased { cause: "the unit is still held" }, context_line: "megarac kvm observer release: unit hold NOT released: the unit is still held") {
+    ExitFailure { code: _, reason: r } => r == "megarac kvm observer release: unit hold NOT released: the unit is still held"
+    _ => false
+  }
+}
+
+// A REAL RELEASE STILL PASSES, by arm; so do already-free, not-ours and stale.
+test fn released_and_no_op_holds_still_pass() -> Bool {
+  probe_hold_release_step_exit(o: ProbeHoldReleased, context_line: "unused on success") == ExitSuccess
+    && probe_hold_release_step_exit(o: ProbeHoldAlreadyFree, context_line: "unused on success") == ExitSuccess
+    && probe_hold_release_step_exit(o: ProbeHoldNotOurs { holder: "another-run" }, context_line: "unused on success") == ExitSuccess
+    && probe_hold_release_step_exit(o: ProbeHoldStale { detail: "the slot moved to another generation" }, context_line: "unused on success") == ExitSuccess
+}

dag/test/claim/spark/pair_serving_authority_log_witness_test.dag

@@ -2,6 +2,7 @@ module test.claim.spark.pair_serving_authority_log_witness
 
 import std.logic { Bool }
 import std.types { String, NonEmptyStr, List }
+import std.process { ExitSuccess, ExitFailure }
 import std.optional { Present, Absent }
 import product.host_identity { HostIdentity }
 import gunbc.spark.fabric_switch_observed { fabric_group_hosts, FabricGroup, FabricGroupB, parse_fabric_group }
@@ -31,6 +32,7 @@ import gunbc.spark.pair_serving_authority_log {
   RecordedFabricGroup, RecordedLiveGroup, RecordedRetiredGroupA, parse_recorded_group, recorded_group_wire,
   RecordedAuthority, RecordedLiveAuthority, RecordedRetiredGroupAAuthority, Finalized,
   PlacementFold, PlacementFolded, PlacementFoldRefused, placement_fold, PlacementPreparationRecord, AppendClaimed, Prepared, Aborted, group_live_commitment, group_fenced_hosts, same_host_set,
+  placement_cleanup_step_exit, PlacementFinalizedAt, PlacementAbortedAt, PlacementCleanupStillFencing, PlacementCleanupUnread,
 }
 
 // THE CODEC AND THE FOLD, OVER SUPPLIED VALUES. Every arm of the authority round-trips through
@@ -903,3 +905,27 @@ test fn a_full_retired_group_a_saga_then_group_b_folds_through_the_real_codec()
     }
   }
 }
+
+// THE CLEANUP EXIT IS A HERMETIC DECISION: placement_cleanup_step_exit answers each cleanup state
+// by name, so the wet step's verdict is pinned here without an executor, a host store or a clock.
+// AN UNREADABLE OUTCOME IS NOT EVIDENCE THE FENCE IS DOWN: it fails loudly with its cause.
+test fn an_unread_placement_cleanup_fails_loudly_with_its_cause() -> Bool {
+  match placement_cleanup_step_exit(c: PlacementCleanupUnread { cause: "the log store could not be read" }) {
+    ExitFailure { code: _, reason: r } => r == "the log store could not be read"
+    _ => false
+  }
+}
+
+// A REAL COMPLETION STILL PASSES: finalized and aborted report completion, by arm.
+test fn a_finalized_placement_cleanup_still_passes() -> Bool {
+  placement_cleanup_step_exit(c: PlacementFinalizedAt { preparation: "authoritative-preparation" as EventId, id: "e-1" as EventId }) == ExitSuccess
+    && placement_cleanup_step_exit(c: PlacementAbortedAt { preparation: "authoritative-preparation" as EventId, id: "e-2" as EventId }) == ExitSuccess
+}
+
+// STILL FENCING FAILS LOUDLY WITH ITS CAUSE, by arm as before.
+test fn a_placement_still_fencing_fails_loudly_with_its_cause() -> Bool {
+  match placement_cleanup_step_exit(c: PlacementCleanupStillFencing { preparation: "authoritative-preparation" as EventId, cause: "the fence release has not committed" }) {
+    ExitFailure { code: _, reason: r } => r == "the fence release has not committed"
+    _ => false
+  }
+}

src/v2/std/arrow_contract.dag

@@ -8,6 +8,8 @@ import v2.std.node {
   Conj,
   Edge,
   Found,
+  Ambiguous,
+  Absent,
   Authored,
   ArrowEffectClaimsEdge,
   ArrowExecutionModeClaimEdge,
@@ -123,6 +125,13 @@ fn arrow_contract_conforms(children: List<Edge>) -> Bool {
 // an undeclared operation, which D13 step (b) reads as Undecided. Whether each
 // member names a declared resource, and whether two spellings name one, are facts of resolution
 // (v2.compiler.resolve), not of this pre-resolve wall.
+// THE EDGE TARGET IS READ OR THE WALL DOES NOT CLAIM IT. core_edge_target_lookup distinguishes
+// three states and each wall answers all three by name, matching arrow_body_target_conforms's
+// spelling in v2.std.node: an ABSENT edge is an undeclared operation, nothing to check here (D13
+// step (b) reads it as Undecided downstream); an AMBIGUOUS edge -- two edges sharing one core
+// marker -- has no single target to read, so the wall refuses rather than grant conformance to a
+// target it cannot name. Naming the arms keeps a lookup state added later from silently inheriting
+// "reads".
 fn arrow_resource_requirements_edge_target_reads(children: List<Edge>) -> Bool {
   match core_edge_target_lookup(children: children, marker: ArrowResourceRequirementsEdge) {
     Found { target: requirements } =>
@@ -132,20 +141,23 @@ fn arrow_resource_requirements_edge_target_reads(children: List<Edge>) -> Bool {
           ((id == ^requirements_declared_none) || (id == ^requirements_opaque)) && (count(requirements.children) == 0)
         _ => false
       }
-    _ => true
+    Absent => true
+    Ambiguous => false
   }
 }
 
 fn arrow_effect_claims_edge_target_reads(children: List<Edge>) -> Bool {
   match core_edge_target_lookup(children: children, marker: ArrowEffectClaimsEdge) {
     Found { target: claims } => arrow_effect_claims_target_conforms(claims: claims)
-    _ => true
+    Absent => true
+    Ambiguous => false
   }
 }
 
 fn arrow_execution_mode_edge_target_reads(children: List<Edge>) -> Bool {
   match core_edge_target_lookup(children: children, marker: ArrowExecutionModeClaimEdge) {
     Found { target: mode } => arrow_execution_mode_claim_target_conforms(mode: mode)
-    _ => true
+    Absent => true
+    Ambiguous => false
   }
 }