pub fn collect_verify_laws(items: &[TopLevel]) -> Vec<VerifyBlock>Expand description
verify … law blocks from a module’s top-level items, in source
order. Plain example-style verify blocks (VerifyKind::Example)
are excluded — only laws are lifted into a dep’s ModuleInfo for
the cross-file law pool.
VISIBILITY gate (cross-file law pool, fail-closed at admission): a
law is lifted ONLY when its SUBJECT fn is EXPOSED by the module —
the same rule crate::visibility::collect_module_exports /
crate::visibility::SymbolRegistry::from_modules apply to fns. A
law about a private helper (_-prefixed, or absent from a non-empty
exposes [...] list) is a module-internal obligation: it is still
proved in the module’s OWN export, but it never enters a consumer’s
pool, is never emitted into a consumer’s build, and is never lowered
for a consumer. A consumer can only cite what its dependency makes
public, exactly as it can only CALL exposed fns.