		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Shift-operations

Leo shift operations.

These are arithmetic shift left and shift right operations, in regular and wrapped variants.

The left operand can be any signed or unsigned integer type; the right operand can only be u8, u16, or u32. The return type is the same as the left operand type.

For the regular shift left and shift right operations, it is an error if the right operand is larger than the number of bits of the left operand's type.

For the wrapped shift left and shift right operations, instead of getting an error when the right operand is too large, only the low log_2(N) bits are used when deciding how far to shift, where N is the bit size of the left operand's type. In other words, the shift amount is first reduced modulo N.

Arithmetic shift is best thought of as multiplication (left shift) or division (right shift) by a power of two. The right operand is the power of two. In the case of division, fractions are rounded towards negative infinity.

For example -3i8 >> 1u8 becomes -3/2 which is rounded to -2i8.

For regular left shift, if the result of multiplying by the power of two is not representable in the return type, it is an error. For example, 64i8 << 1u8 and -65i8 << 1u8 are errors.

For wrapped left shift, if the result of multiplying by the power of two is not representable in the return type, then the low N bits are interpreted as a value of the return type. For example, consider 127i8.shl_wrapped(2u8). The bits 0111 1111 are shifted left by two places: 1 1111 1100; the low 8 bits are 1111 1100, which represents the returned value -4i8.

Subtopics

Op-shl-wrapped: Leo wrapped left shift operation.
Op-shr-wrapped: Leo wrapped right shift operation.
Op-shr: Leo right shift operation.
Op-shl: Leo left shift operation.