Compare for equality.

Create a tuple from a list of fields

Extract the value out of a tuple.

Extracts an element at given constant index from vector

Sets an element at given constant in vector.

Given a m-bit bitvector and a natural number n less than m, this returns the bitvector with the n least significant bits.

Given a m-bit bitvector x and a natural number n greater than m, this returns the bitvector with the same m least signficant bits, and where the new bits are the same as the most significant bit in x.

Given a m-bit bitvector x and a natural number n greater than m, this returns the bitvector with the same m least signficant bits, and where the new bits are all false.

This casts an expression from one type to another that should use the same number of bytes in memory.

BVAdd w x y denotes x + y.

BVAdc w x y c denotes x + y + (c ? 1 : 0).

BVSub w x y denotes x - y.

BVSbb w x y b denotes (x - y) - (b ? 1 : 0).

Left shift (e.g. `BVShl x y` denotes `fromUnsigned (toUnsigned x * 2 ^ toUnsigned y)`

Unsigned right shift (e.g. `BVShr x y` denotes `fromUnsigned (toUnsigned x / 2 ^ toUnsigned y)`

Arithmetic right shift (e.g. `BVSar x y` denotes `fromUnsigned (toSigned x / 2 ^ toUnsigned y)`

Add two values and a carry bit to determine if they have an unsigned overflow.

This is the sum of three three values cannot be represented as an unsigned number.

Add two values and a carry bit to determine if they have a signed overflow.

SadcOverflows w x y c should be true iff the result toNat x + toNat y + (c ? 1 : 0) is greater than 2^w-1.

Unsigned subtract with borrow overflow

UsbbOverflows w x y c should be true iff the result (toNat x - toNat y) - (c ? 1 : 0) is non-negative. Since everything is unsigned, this is equivalent to x unsignedLt (y + (c ? 1 : 0).

Signed subtract with borrow overflow.

SsbbOverflows w x y c should be true iff the result (toInt x - toInt y) - (c ? 1 : 0) is not between -2^(w-1) and 2^(w-1)-1. An equivalent way to express this is that x and y should have opposite signs and the sign of the result should differ from the sign of x.

This returns the number of true bits in the input.

Reverse the bytes in a bitvector expression.

bsf "bit scan forward" returns the index of the least-significant bit that is 1. An equivalent way of stating this is that it returns the number zero-bits starting from the least significant bit. This returns n if the value is zero.

bsr "bit scan reverse" returns the index of the most-significant bit that is 1. An equivalent way of stating this is that it returns the number zero-bits starting from the most-significant bit location. This returns n if the value is zero.

Convert between vector types that are equivalent.

Type is equal to itself.

Allows transitivity composing proofs.