Module `L.Bytes`

Representation of bytes.

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

type 'a input = 'a Input.t

Input for a Plompiler program.

type scalar = scalar

Element of the native scalar field.

type 'a repr = 'a repr

Representation of values.

type 'a t = 'a t

Plompiler program.

type tl = bool list

Representation of elements.

val input_bytes : le:bool -> bytes -> tl input

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

val constant : le:bool -> bytes -> tl repr t

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

val of_scalar : total_nb_bits:int -> scalar repr -> tl repr t

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

val to_scalar : tl repr -> scalar repr t

to_scalar b return the scalar representing the value b.

val of_bool_list : bool list repr -> tl repr t

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

val to_bool_list : tl repr -> bool list repr t

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

val xor : tl repr -> tl repr -> tl repr t

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

val band : tl repr -> tl repr -> tl repr t

band a b returns the conjunction of a and b.

val not : tl repr -> tl repr t

not b returns the negation of b.

val rotate_right : tl repr -> int -> tl repr t

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

val shift_right : tl repr -> int -> tl repr t

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

val constant_uint32 : le:bool -> Stdint.uint32 -> tl repr t

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

val length : tl repr -> int

length b returns the length of b in bits.

val concat : tl repr array -> tl repr

concat bs returns the concatenation of the bitlists in bs.

val add : ?ignore_carry:bool -> tl repr -> tl repr -> tl repr t

add b1 b2 computes the addition of b1 and b2.

val rotate_left : tl repr -> int -> tl repr t

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

val shift_left : tl repr -> int -> tl repr t

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}

Install

Dune Dependency

Authors

Maintainers

Sources

doc/octez-libs.plompiler/Plompiler/Bounded/Make/V/argument-1-L/Bytes/index.html

Module `L.Bytes`

package octez-libs

Install

Dune Dependency

Authors

Maintainers

Sources

doc/octez-libs.plompiler/Plompiler/Bounded/Make/V/argument-1-L/Bytes/index.html

Module L.Bytes

Module `L.Bytes`