Module typed 

Path-local checking for the Typed safety property.

Typed(p, T) is not a pure numeric SMT fact. The first verifier model proves it by following the path-local provenance facts produced by the forward visitor: references and slices carry their Rust element type, pointer arithmetic preserves the base pointee type, same-type casts preserve typedness, and ptr.write(value) establishes one initialized T element.

Structs

TypedContext 🔒

Constants

MAX_TYPED_TRACE_DEPTH 🔒

Functions

check 🔒

Check Typed using path-local provenance and initialization facts.

field_ty 🔒

Resolve one field projection through an aggregate type.

payload_ty 🔒

Return the Rust payload type carried by references, pointers, slices, and arrays.

place_debug 🔒

Return a compact label for a verifier place.