Little-endian representation of bytes. First element of the list is the Least Significant Bit.

input_bytes ~le bs returns the representation of bs that Plompiler expects as input.

constant ~le bs returns a value holding the bytes bs. le can be used to set the endianness.

constant_uint32 ~le n returns a value holding the bytes correspoding to the uint n. le can be used to set the endianness.

length b returns the length of b in bits.

concat bs returns the concatenation of the bitlists in bs.

add b1 b2 computes the addition of b1 and b2.

xor b1 b2 computes the bitwise xor between b1 and b2.

not b computes the bitwise negation of b.

band b1 b2 computes the bitwise conjunction between b1 and b2.

rotate_left bl n shifts the bits left by n positions, so that each bit is more significant. The most significant bit becomes the least significant i.e. it is "rotated". rotate_left bl (length bl) = bl

rotate_right bl n shifts the bits right by n positions. Similar to rotate_left, but to the right.

shift_left bl n shifts all bits left by n positions, so that each bit is more significant. The most signigicant bit is lost and the least significant bit is set to zero. More precisely, if we interpret the bl as an integer shift_left bl i = bl * 2^i mod 2^{length a}

shift_right bl n shifts all bits right by n positions. Similar to shift_left, but to the right.