pub(crate) fn subsumption_closure<'tcx>(
atom: &AtomProperty<'tcx>,
) -> Vec<AtomProperty<'tcx>>Expand description
Apply the builtin subsumption rules to an asserted fact: a stronger
primitive also asserts its weaker consequences — a one-way weakening, unlike
the ≡ compound equivalences above. The rules are declared declaratively
in std-subsumption.rs with the same Name(params) { body } syntax; the
head is an existing primitive tag and the body a pure conjunction of weaker
primitive calls whose parameters map positionally to the head’s arguments
(e.g. Init(p, T, n) ⇒ Typed(p, T)). Pointer-validity primitives
(NonNull/Allocated/InBound) are deliberately not implied: they are
orthogonal requirements stated explicitly by contracts.
Returns the transitive closure of the subsumption relation applied to
atom, deduplicated: each weaker consequence appears exactly once.