Module deref 

SMT lowering for the Deref safety property.

Deref(p, T, n) is the range-level part of pointer validity:

Deref(p, T, n) = Allocated(p, T, n, *) && InBound(p, T, n)

The star in Allocated represents the current allocation object/provenance abstraction. This module keeps Deref as a composite SP and delegates the object and bounds checks to their existing lowerings.

Functions

check 🔒

Check Deref by proving both allocation and bounds obligations.