Expand description
Composite pointer validity and dereferenceability checks. Composite pointer-safety contract checkers.
This module owns Allocated, Deref, ValidPtr, and pointer-to-reference
conversion checks. Several leaf predicates are still conservative
placeholders, but the composite APIs keep the contract structure explicit.