Module type_invariants 

Standard-library type-invariant generation.

Type invariants are synthesized obligations that a value of a given type must satisfy. Unlike user-written #[rapx::invariant] struct invariants, these are generated automatically from the bundled std-type-invariants.json database, keyed by a normalized type path (e.g. core::num::NonZero) or by the built-in [T] slice key.

The results feed the type_invariants field of a [FunctionTarget] (see super::target), whose entry facts are synthesized by the VM’s init_parameters and re-proved at return by VerifyDriver::verify_type_invariants.

Constants

SLICE_ELEM_PLACEHOLDER 🔒

Placeholder type name substituted for the $elem token before parsing. The JSON $elem is a bare type argument (e.g. Align($self, $elem)), and the real element type — which can be a composite like [T; N] that has no resolvable name — is injected afterwards by replace_ty_args. Any primitive placeholder resolves cleanly through the name-based type parser.

Functions

build_type_invariants_from_params 🔒

For each function parameter (and the return type), look up the type’s invariants from std-type-invariants.json and create preconditions.

collect_type_invariants 🔒

Look up the type path in the DB and add instantiated invariants to results.

instantiate_entry 🔒

Instantiate a single (non-any) type invariant entry.

instantiate_type_invariant 🔒

Create properties from a type invariant entry, substituting the parameter name (and, for the slice entry, the element type). An entry with an any field expands to a single disjunctive Property::Or; otherwise it yields the properties denoted by its tag.

is_numeric_field_access 🔒

Check if a string looks like a numeric field access (e.g. “0”).

replace_expr_ty 🔒

Replace size_of/align_of type arguments inside a contract expression.

replace_pred_ty 🔒

Replace size_of/align_of type arguments inside a numeric predicate.

replace_ty_args 🔒

Replace every type argument in a property tree with the slice element type.

type_path_key 🔒

Generate a normalised type path key for lookups in the type-invariants DB, together with the element type for the built-in slice entry.