Module in_bound 

SMT lowering for the InBound safety property.

The current implementation handles the common slice pattern:

ptr = slice.as_ptr()
current = ptr.add(index)
guard: index < slice.len()
property: InBound(current, T, n)

The module only lowers the property to SmtObligation::InBounds. The common SMT model is responsible for matching as_ptr, ptr.add, len, and branch facts from the forward visit result.

Functions

check 🔒

Check InBound by lowering it to a common bounds obligation.

check_for_checkpoint 🔒

Check InBound at a return checkpoint for struct invariant verification.

pointer_arithmetic_obligation 🔒