fstar 2025.02.17 · OCaml Package

module U8 = FStar_UInt8

module U16 = FStar_UInt16

module U32 = FStar_UInt32

type u8 = U8.t

type u16 = U16.t

type u32 = U32.t

type byte = u8

type bytes = string

type cbytes = string

val len : bytes -> U32.t

val length : bytes -> Z.t

val reveal : bytes -> unit

val length_reveal : bytes -> unit

val hide : 'a -> unit

val hide_reveal : bytes -> unit

val reveal_hide : 'a -> unit

type 'a lbytes = bytes

type 'a lbytes32 = bytes

type kbytes = bytes

val empty_bytes : string

val empty_unique : bytes -> unit

val get : bytes -> u32 -> int

val op_String_Access : bytes -> u32 -> int

type ('b1, 'b2) equal = unit

val extensionality : bytes -> bytes -> unit

val create : u32 -> byte -> string

val create_ : Z.t -> byte -> string

val init : u32 -> (u32 -> byte) -> string

val twobytes : (byte * byte) -> string

val append : bytes -> bytes -> string

val op_At_Bar : bytes -> bytes -> string

val slice : bytes -> u32 -> u32 -> string

val slice_ : bytes -> Z.t -> Z.t -> string

val sub : bytes -> u32 -> u32 -> string

val split : bytes -> u32 -> string * string

val split_ : bytes -> Z.t -> string * string

val fits_in_k_bytes : Z.t -> Z.t -> bool

type 'a uint_k = Z.t

val repr_bytes : Z.t -> Z.t

val lemma_repr_bytes_values : Z.t -> unit

val repr_bytes_size : Z.t -> 'a uint_k -> unit

val int_of_bytes : bytes -> Z.t

val bytes_of_int : Z.t -> Z.t -> string

val int_of_bytes_of_int : Z.t -> 'a uint_k -> unit

val bytes_of_int_of_bytes : bytes -> unit

val int32_of_bytes : bytes -> int

val int16_of_bytes : bytes -> int

val int8_of_bytes : bytes -> int

val bytes_of_int32 : U32.t -> string

val bytes_of_int16 : U32.t -> string

val bytes_of_int8 : U32.t -> string

type 'a minbytes = bytes

val xor : U32.t -> 'a minbytes -> 'b minbytes -> bytes

val xor_ : Z.t -> bytes -> bytes -> bytes

val xor_commutative : U32.t -> 'a minbytes -> 'b minbytes -> unit

val xor_append : bytes -> bytes -> bytes -> bytes -> unit

val xor_idempotent : U32.t -> bytes -> bytes -> unit

val utf8 : string -> bytes

val utf8_encode : string -> bytes

val iutf8 : bytes -> string

val iutf8_opt : bytes -> string option

val digit_to_int : char -> int

val hex_to_char : char -> char -> char

val char_to_hex : char -> char * char

val string_of_hex : string -> bytes

val bytes_of_hex : string -> string

val hex_of_string : string -> string

val hex_of_bytes : string -> string

val print_bytes : bytes -> string

val string_of_bytes : 'a -> 'a

val bytes_of_string : 'a -> 'a

val cbyte : bytes -> int

val cbyte2 : bytes -> int * int

val index : bytes -> Z.t -> int

val get_cbytes : bytes -> bytes

val abytes : cbytes -> cbytes

val abyte : byte -> string

val abyte2 : (int * int) -> string

val split_eq : bytes -> u32 -> string * string

val createBytes : Z.t -> int -> bytes

val initBytes : Z.t -> (Z.t -> int) -> bytes

val equalBytes : bytes -> bytes -> bool

val split2 : bytes -> u32 -> u32 -> bytes * bytes * bytes

val byte_of_int : Z.t -> int

package fstar