Module goal 

Same-resource mutual exclusion. Detection is kernel’s; arbitration is not — reading statements and judging intent belongs to models (collab::arbiter) and humans. The part crates/kernel/spec/Goal.lean specifies this module.

Structs

GoalEntry

GoalId

Non-empty goal identity; uniqueness bookkeeping is the caller’s.

Enums

GoalResource

What a goal claims. Paths conflict on prefix overlap either way; external names conflict on equality; the two kinds never conflict with each other.

GoalVerdict

Deliberately exhaustive verdict.

Functions

detect_conflict

First conflict wins, in the registered slice’s order (deterministic: the caller’s table order is the clock). A candidate re-submitting its own id is idempotent, not a conflict.