Module valid_num 

SMT lowering for the ValidNum safety property.

ValidNum carries one or more numeric predicates, for example:

ValidNum(i < len)
ValidNum(size_of(T) * len <= isize::MAX)

This module only rebinds callee-side contract expressions to the concrete checkpoint arguments and converts them to common SMT predicates. The shared backend discharges the query by checking whether the negated predicate is satisfiable under the forward path facts.

Functions

check 🔒

Check ValidNum by lowering all predicates to a common predicate obligation.