let hex1 (x:UInt8.t {FStar.UInt8.(x <^ 16uy)}) =
  FStar.UInt8.(
    if x <^ 10uy then UInt8.to_string x else
    if x = 10uy then "a" else
    if x = 11uy then "b" else
    if x = 12uy then "c" else
    if x = 13uy then "d" else
    if x = 14uy then "e" else "f")
let hex1 (x: UInt8.t{let open FStar.UInt8 in x <^ 16uy}) =
let open FStar.UInt8 in
if x <^ 10uy
then UInt8.to_string x
else
  if x = 10uy
  then "a"
  else
    if x = 11uy
    then "b"
    else if x = 12uy then "c" else if x = 13uy then "d" else if x = 14uy then "e" else "f"
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.UInt8.t Prims.b2t FStar.UInt8.op_Less_Hat FStar.UInt8.__uint_to_t FStar.UInt8.to_string Prims.bool Prims.op_Equality Prims.string
(*--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}

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 hex1 : x: FStar.UInt8.t{x <^ 16uy} -> Prims.string
x: FStar.UInt8.t{x <^ 16uy} -> Prims.string