Input for a Plompiler program.

Element of the native scalar field.

Representation of values.

Plompiler program.

Representation of elements.

input_bytes ~le b returns the representation of b that Plompiler expects as input. le can be used to set the endianness.

constant ~le b returns the constant b as a Plompiler value. le can be used to set the endianness.

of_scalar ~total_nb_bits b converts the scalar b of size total_nb_bits in bits into the tl representation.

to_scalar b return the scalar representing the value b.

of_bool_list b converts the list of bits in little-endian order into the tl representation.

to_bool_list b returns the list of bits in little-endian order, representing the value b.

xor a b returns the exclusive disjunction of a and b.

band a b returns the conjunction of a and b.

not b returns the negation of b.

rotate_right b n shifts the bits right by n positions, so that each bit is less significant. The least significant bit becomes the most significant i.e. it is "rotated". rotate_right bs (length bl) = bl

shift_right b n shifts all bits right by n positions, so that each bit is less significant. The least signigicant bit is lost and the most significant bit is set to zero. More precisely, if we interpret the b as an integer, shift_right b n = b / 2^n

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.

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

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}