Alloy model of Rust orphan rule

orphanrule.als

-- Simplified Rust crate model
--
-- Crates form a dependency DAG, starting from single top-level target (Binary) 
-- Traits implemented for Types
-- Simple impls (no blanket/parameterized impls)
-- Orphan rule
-- assertion that implementations are globally coherent

-- Trait is define in exactly one crate
sig Trait {
	tr_crate: one Crate
}

-- Type is defined in exactly one crate
sig Type {
	ty_crate: one Crate
}

-- Orphan rule - either type or trait must be local,
-- and the other must either local or a dependency
-- NOTE: A non-local type/trait can't be in *any* other crate,
-- it must be in a dependency for the invariant to hold. This
-- also relies on the dep graph being acyclic.
pred orphan_rule[crate: Crate] {
	crate.impls in
		(crate[tr_crate] -> (crate + crate.deps)[ty_crate]) + -- local trait
		((crate+crate.deps)[tr_crate] -> crate[ty_crate]) -- local type
}

-- Dependency adoptions
-- May impl traits & types in dependencies
-- INVALID: needs dominator checking
pred adopt_deps[crate: Crate] {
	crate.impls in (crate + crate.deps)[tr_crate] -> (crate + crate.deps)[ty_crate]
}

-- Crate has deps and impls
sig Crate {
	deps : set Crate, -- dependencies
	impls: Trait -> Type -- set of imples of traits for types
} {
	orphan_rule[this]
	-- adopt_deps[this]
}

-- Unique top level crate which all other crates are transitive deps of
one sig Binary extends Crate {}

fact {
	-- nothing depends on Binary
	no deps.Binary
	-- dep graph is DAG
	no c: Crate | c in c.^deps
	-- all crates reachable from binary (incl Binary)
	Crate in Binary.*deps 
}

-- Impls are coherent if an implementation of a trait for a type appears in at most one crate
assert CoherentImpls {
    all tr: Trait, ty: Type | lone impls.ty.tr
}

check CoherentImpls

run example {
	-- at least one other crate
	some Crate - Binary
} for 4 Crate, 2 Trait, 2 Type