Bit operators

Syntax

bit_expr ::= spec_expr  &  spec_expr
           | spec_expr  |  spec_expr
           | spec_expr  ^  spec_expr
           | spec_expr  << spec_expr
           | spec_expr  >> spec_expr

Typing

Semantics

&, |, and ^.

These have the usual meaning: bitwise-OR, bitwise-AND, and bitwise-XOR. Verus, like Rust, requires the input operands to be the same type, even in specification code. However, as binary operators defined over the integers, ℤ x ℤ → ℤ, these operations are independent of bitwidth. This is true even for negative operands, as a result of the way two’s complement sign-extension works.

>> and <<.

Verus specifications (like Rust’s) do not require the left and right sides of a shift operator to be the same type. Shift is unspecified when the right-hand side is negative. Unlike in executable code, however, there is no upper bound on the right-hand side.

a << b and and a >> b both have the same type as a.

Right shifts can be defined over the integers ℤ x ℤ → ℤ independently of the input bitwidth.

For <<, however, the result does depend on the input type because a left shift may involve truncation if some bits get shifted “off to the left”. There is no widening to an int (unlike, say, Verus specification +).

Reasoning about bit operators

In Verus’s default prover mode, the definitions of these bitwise operators are not exported. To prove nontrivial facts about bitwise operators, use the bit-vector solver or the compute solver.