val print_buffer: s:buffer -> i:UInt32.t{UInt32.v i <= length s} -> len:UInt32.t{UInt32.v len <= length s} -> Stack unit
  (requires (fun h -> live h s))
  (ensures (fun h0 _ h1 -> h0 == h1))
let rec print_buffer s i len =
  let open FStar.UInt32 in
  if i <^ len then
    let b = Buffer.index s i in
    let sep = if i %^ 16ul =^ 15ul || i +^ 1ul = len then "\n" else " " in
    let _ = IO.debug_print_string (hex2 b ^ sep) in
    let _ = print_buffer s (i +^ 1ul) len in
    ()
val print_buffer: s:buffer -> i:UInt32.t{UInt32.v i <= length s} -> len:UInt32.t{UInt32.v len <= length s} -> Stack unit
  (requires (fun h -> live h s))
  (ensures (fun h0 _ h1 -> h0 == h1))
let rec print_buffer s i len =
let open FStar.UInt32 in
if i <^ len
then
  let b = Buffer.index s i in
  let sep = if i %^ 16ul =^ 15ul || i +^ 1ul = len then "\n" else " " in
  let _ = IO.debug_print_string (hex2 b ^ sep) in
  let _ = print_buffer s (i +^ 1ul) len in
  ()
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
Crypto.Symmetric.Bytes.buffer FStar.UInt32.t Prims.b2t Prims.op_LessThanOrEqual FStar.UInt32.v FStar.Buffer.length FStar.UInt8.t FStar.UInt32.op_Less_Hat Prims.unit Crypto.Symmetric.Bytes.print_buffer FStar.UInt32.op_Plus_Hat FStar.UInt32.__uint_to_t Prims.bool FStar.IO.debug_print_string Prims.op_Hat Crypto.Symmetric.Bytes.hex2 Prims.string Prims.op_BarBar FStar.UInt32.op_Equals_Hat FStar.UInt32.op_Percent_Hat Prims.op_Equality FStar.Buffer.index
(*--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)

private 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")
private let hex2 x =
  FStar.UInt8.(hex1 (x /^ 16uy) ^ hex1 (x %^ 16uy))

val print_buffer: s:buffer -> i:UInt32.t{UInt32.v i <= length s} -> len:UInt32.t{UInt32.v len <= length s} -> Stack unit
  (requires (fun h -> live h s))
  (ensures (fun h0 _ h1 -> h0 == h1))
val print_buffer: s:buffer -> i:UInt32.t{UInt32.v i <= length s} -> len:UInt32.t{UInt32.v len <= length s} -> Stack unit
  (requires (fun h -> live h s))
  (ensures (fun h0 _ h1 -> h0 == h1))

    s: Crypto.Symmetric.Bytes.buffer ->
    i: FStar.UInt32.t{FStar.UInt32.v i <= FStar.Buffer.length s} ->
    len: FStar.UInt32.t{FStar.UInt32.v len <= FStar.Buffer.length s}
  -> FStar.HyperStack.ST.Stack Prims.unit