Bit operators #

Syntax #

V@[bit_expr] ::= V@[spec_expr]  &  V@[spec_expr]
           | V@[spec_expr]  |  V@[spec_expr]
           | V@[spec_expr]  ^  V@[spec_expr]
           | V@[spec_expr]  << V@[spec_expr]
           | V@[spec_expr]  >> V@[spec_expr]

Typing #

operation	LHS type	RHS type	result type
& | ^	t	t	t
<< >>	t1	t2	t1

Semantics #

&, |, and ^.

These have the usual meaning: bitwise-AND, bitwise-OR, 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 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.