val uint128_to_uint8 (a: UInt128.t) : Tot (b: UInt8.t{UInt8.v b == UInt128.v a % pow2 8})
let uint128_to_uint8 (a:UInt128.t) : Tot (b:UInt8.t{UInt8.v b == UInt128.v a % pow2 8})
  = uint64_to_uint8 (uint128_to_uint64 a)
val uint128_to_uint8 (a: UInt128.t) : Tot (b: UInt8.t{UInt8.v b == UInt128.v a % pow2 8})
let uint128_to_uint8 (a: UInt128.t) : Tot (b: UInt8.t{UInt8.v b == UInt128.v a % pow2 8}) =
uint64_to_uint8 (uint128_to_uint64 a)
Crypto.Symmetric.Bytes.fst.checked
prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt128.fsti.checked FStar.UInt.fsti.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Old.Endianness.fst.checked FStar.Mul.fst.checked FStar.Math.Lib.fst.checked FStar.Math.Lemmas.fst.checked FStar.IO.fst.checked FStar.Int.Cast.Full.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked FStar.Buffer.fst.checked Buffer.Utils.fst.checked
Crypto.Symmetric.Bytes.fst
FStar.UInt128.t FStar.Int.Cast.uint64_to_uint8 FStar.Int.Cast.Full.uint128_to_uint64 FStar.UInt8.t Prims.eq2 Prims.int FStar.UInt8.v Prims.op_Modulus FStar.UInt128.v Prims.pow2
(*--build-config
options:--trace_error --max_fuel 4 --initial_fuel 0 --max_ifuel 2 --initial_ifuel 0 --z3rlimit 20 --use_hints --include ../../code/bignum --include ../../code/experimental/aesgcm --include ../../code/lib/karamel --include ../../code/poly1305 --include ../../code/salsa-family --include ../../secure_api/aead --include ../../secure_api/prf --include ../../secure_api/vale --include ../../secure_api/uf1cma --include ../../secure_api/utils --include ../../specs --include ../../../karamel/krmllib
--*)
module Crypto.Symmetric.Bytes

module ST = FStar.HyperStack.ST

open FStar.HyperStack.All

open FStar.HyperStack
open FStar.UInt32
open FStar.Ghost
open FStar.Buffer
open FStar.Mul
open FStar.Int.Cast.Full

module U8 = FStar.UInt8

open Buffer.Utils

type mem = FStar.HyperStack.mem

let u8  = UInt8.t
let u32 = UInt32.t
let u64 = UInt64.t


(** TODO: Move. Used only in AEAD.EnxorDexor, much faster to prove here *)
val eq_snoc_slice: #a:Type -> s_0:Seq.seq a -> s_1:Seq.seq a -> x:a -> Lemma
  (requires (Seq.length s_1 == Seq.length s_0 + 1 /\
            Seq.index s_1 (Seq.length s_0) == x /\
            Seq.equal (Seq.slice s_1 0 (Seq.length s_0)) s_0))
  (ensures  (Seq.equal s_1 (Seq.snoc s_0 x)))
let eq_snoc_slice #a s_0 s_1 x = ()

// TODO: rename and move to FStar.Buffer
// bytes  -> uint8_s; lbytes  -> uint8_sl
// buffer -> uint8_p; lbuffer -> uint8_sl

type bytes = Seq.seq UInt8.t // Currently, Buffer.Utils redefines this as buffer
type buffer = Buffer.buffer UInt8.t

type lbytes  (l:nat) = b:bytes  {Seq.length b == l}
type lbuffer (l:nat) = b:buffer {Buffer.length b == l}
val uint128_to_uint8 (a: UInt128.t) : Tot (b: UInt8.t{UInt8.v b == UInt128.v a % pow2 8})
a: FStar.UInt128.t -> b: FStar.UInt8.t{FStar.UInt8.v b == FStar.UInt128.v a % Prims.pow2 8}