diff --git a/dag/gunbc/fleet/fleet_revision_acceptance.dag b/dag/gunbc/fleet/fleet_revision_acceptance.dag index 0f437a47391..d3bcb36035d 100644 --- a/dag/gunbc/fleet/fleet_revision_acceptance.dag +++ b/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 } diff --git a/dag/gunbc/host/managed_host_unit_hold.dag b/dag/gunbc/host/managed_host_unit_hold.dag index 9c53c47f790..7bc370ce457 100644 --- a/dag/gunbc/host/managed_host_unit_hold.dag +++ b/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"), diff --git a/dag/gunbc/machine_intake/megarac_kvm_observer_observe.dag b/dag/gunbc/machine_intake/megarac_kvm_observer_observe.dag index 7e57c27538d..3514a685993 100644 --- a/dag/gunbc/machine_intake/megarac_kvm_observer_observe.dag +++ b/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) } diff --git a/dag/gunbc/non_fold_residue.dag b/dag/gunbc/non_fold_residue.dag index 500eb5a7db8..4de3951a966 100644 --- a/dag/gunbc/non_fold_residue.dag +++ b/dag/gunbc/non_fold_residue.dag @@ -766,11 +766,8 @@ data non_fold_residue_frontier: List = [ 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 }, diff --git a/dag/gunbc/runner/runner_throughput_qualification_route.dag b/dag/gunbc/runner/runner_throughput_qualification_route.dag index 221a620a4f2..518c98f6388 100644 --- a/dag/gunbc/runner/runner_throughput_qualification_route.dag +++ b/dag/gunbc/runner/runner_throughput_qualification_route.dag @@ -362,7 +362,9 @@ fn route_control_plane_write_count(route: List) -> 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) -> Bool { route |> all(s => match stage_effect(stage: s) { @@ -414,6 +416,8 @@ fn route_deregisters_what_it_registered(route: List) -> 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, attempt: NonEmptyStr) -> Bool { route |> all(s => match s { diff --git a/dag/gunbc/spark/pair_serving_authority_log.dag b/dag/gunbc/spark/pair_serving_authority_log.dag index 958012dfe34..200e72bbbbc 100644 --- a/dag/gunbc/spark/pair_serving_authority_log.dag +++ b/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)) } } } diff --git a/dag/test/claim/fleet/fleet_desired_merge_queue_admission_witness_test.dag b/dag/test/claim/fleet/fleet_desired_merge_queue_admission_witness_test.dag index 30eb7e0bf8a..41458f1397f 100644 --- a/dag/test/claim/fleet/fleet_desired_merge_queue_admission_witness_test.dag +++ b/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)])) { diff --git a/dag/test/claim/host/managed_host_unit_hold_witness_test.dag b/dag/test/claim/host/managed_host_unit_hold_witness_test.dag index 60fff575274..0a3c5f8f069 100644 --- a/dag/test/claim/host/managed_host_unit_hold_witness_test.dag +++ b/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 +} diff --git a/dag/test/claim/spark/pair_serving_authority_log_witness_test.dag b/dag/test/claim/spark/pair_serving_authority_log_witness_test.dag index 359359cd311..929d54d0216 100644 --- a/dag/test/claim/spark/pair_serving_authority_log_witness_test.dag +++ b/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 + } +} diff --git a/src/v2/std/arrow_contract.dag b/src/v2/std/arrow_contract.dag index 8ad81a4c6a9..7cead6aabbb 100644 --- a/src/v2/std/arrow_contract.dag +++ b/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) -> 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) -> 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) -> 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) -> 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) -> 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 } } diff --git a/src/v2/test/claim/arrow_contract_edge_conformance_test.dag b/src/v2/test/claim/arrow_contract_edge_conformance_test.dag index 8e31607d72c..374c2d41504 100644 --- a/src/v2/test/claim/arrow_contract_edge_conformance_test.dag +++ b/src/v2/test/claim/arrow_contract_edge_conformance_test.dag @@ -15,6 +15,7 @@ import v2.std.node { Authored, ArrowEffectClaimsEdge, ArrowExecutionModeClaimEdge, + ArrowResourceRequirementsEdge, Node, Positional, Symbol, @@ -128,3 +129,25 @@ test fn contract_edge_identity_is_order_independent() -> Bool { && (content_hash(n: ace_arrow(extra: [ace_claims(names: [ace_readonly()]), ace_mode(mode: ace_hermetic())])) == content_hash(n: ace_arrow(extra: [ace_mode(mode: ace_hermetic()), ace_claims(names: [ace_readonly()])]))) && (content_hash(n: ace_arrow(extra: [ace_claims(names: [ace_readonly()])])) != content_hash(n: ace_arrow(extra: []))) } + +// A requirements edge whose target is a nonempty Conj of resource references -- the wall only reads +// its shape; whether members name declared resources is resolution's fact (D13 ruling B). +fn ace_requirements(children: List) -> Edge { + core_edge(marker: ArrowResourceRequirementsEdge, target: ace_conj(children: children)) +} + +// THE AMBIGUOUS EDGE DOES NOT READ, at the vocabulary wall ALONE. Each red below duplicates one +// contract edge; the vocabulary wall runs without the structural wall +// (arrow_signature_edges_conform) that refuses the same arrow at cardinality, so the wall's own +// answer for an ambiguous lookup is unmasked: with no single target to read it refuses rather than +// grant conformance, matching arrow_body_target_conforms's Ambiguous arm in v2.std.node. Before the +// three walls named Ambiguous, each answered true here. +fn ace_vocabulary_wall(extra: List) -> Bool { + type_binder_node_conforms(n: ace_arrow(extra: extra)) +} + +test fn an_ambiguous_contract_edge_does_not_read_at_the_vocabulary_wall() -> Bool { + !ace_vocabulary_wall(extra: [ace_claims(names: [ace_readonly()]), ace_claims(names: [ace_idempotent()])]) + && !ace_vocabulary_wall(extra: [ace_mode(mode: ace_hermetic()), ace_mode(mode: ace_hermetic())]) + && !ace_vocabulary_wall(extra: [ace_requirements(children: [ace_named(name: ace_readonly(), target: ace_atom(identity: ace_readonly()))]), ace_requirements(children: [ace_named(name: ace_readonly(), target: ace_atom(identity: ace_readonly()))])]) +}