Coercion with `as` #

Syntax #

V@[as_expr] ::= V@[spec_expr] as R@[type]

Coercions on integer types and `char` #

Any of the following types may be coerced to any of the other types:

i8, i16, i32, i64, i128, isize
u8, u16, u32, u64, u128, usize
int
nat
char

Note that this is more permissive than as in Rust exec code. For example, Rust does not permit using as to cast from a u16 to a char, but this is allowed in Verus spec code.

Definition #

Verus defines as-casting as follows:

Casting to an int is always defined and does not require truncation.
Casting to a nat is unspecified if the input value is negative.
Casting to a char is unspecified if the input value is outside the allowed char values.
Casting to any other finite-size integer type is defined as truncation — taking the lower N bits for the appropriate N, then interpreting the result as a signed or unsigned integer.

Reasoning about truncation #

The definition of truncation is not exported in Verus's default prover mode (i.e., it behaves as if it is unspecified). To reason about truncation, use the bit-vector solver or the compute solver.

Also note that the value of N for usize and isize may be configured with the global directive.

Coercions on pointers #

Pointers to integers #

You can coerce any pointer to any integer type. For a pointer ptr: *mut T or ptr: *const T, the expression ptr as INT_TYPE is equivalent to ptr.addr() as INT_TYPE.

Note

Using ptr.addr() explicitly is often clearer than an as-cast.

Note

Verus does not support casting an integer to a pointer using as. Instead, use a function like with_addr or with_exposed_provenance.

Pointers to pointers #

Verus supports some pointer-to-pointer coercions, including between *const and *mut pointers:

*mut T to *const T (identity function)
*const T to *mut T (identity function)

And other kinds of coercions:

*mut T to *mut S for any S: Sized (spec)
*mut [T; N] to *mut [T] (spec)
*mut [T] to *mut [U] (spec)
*mut [T] to *mut str (spec)
*mut str to *mut [T] (spec)

And the equivalent set of casts for *const pointers.

Coercion with as #