val little_endian_null: len:nat{len < 16} -> Lemma
  (little_endian (Seq.create len 0uy) == 0)
let rec little_endian_null len =
  if len = 0 then ()
  else
    begin
    Seq.lemma_eq_intro (Seq.slice (Seq.create len 0uy) 1 len)
		       (Seq.create (len - 1) 0uy);
    assert (little_endian (Seq.create len 0uy) ==
      0 + pow2 8 * little_endian (Seq.slice (Seq.create len 0uy) 1 len));
    little_endian_null (len - 1)
    end
val little_endian_null: len:nat{len < 16} -> Lemma
  (little_endian (Seq.create len 0uy) == 0)
let rec little_endian_null len =
if len = 0
then ()
else
  (Seq.lemma_eq_intro (Seq.slice (Seq.create len 0uy) 1 len) (Seq.create (len - 1) 0uy);
    assert (little_endian (Seq.create len 0uy) ==
        0 + pow2 8 * little_endian (Seq.slice (Seq.create len 0uy) 1 len));
    little_endian_null (len - 1))
FStar.Old.Endianness.fst.checked
prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt128.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lib.fst.checked FStar.Math.Lemmas.fst.checked FStar.Int.Cast.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.Ghost.fsti.checked
FStar.Old.Endianness.fst
Prims.nat Prims.b2t Prims.op_LessThan Prims.op_Equality Prims.int Prims.bool FStar.Old.Endianness.little_endian_null Prims.op_Subtraction Prims.unit Prims._assert Prims.eq2 FStar.Old.Endianness.little_endian FStar.Seq.Base.create FStar.UInt8.t FStar.UInt8.__uint_to_t Prims.op_Addition FStar.Mul.op_Star Prims.pow2 FStar.Seq.Base.slice FStar.Seq.Base.lemma_eq_intro
module FStar.Old.Endianness

module ST = FStar.HyperStack.ST

open FStar.HyperStack.All

open FStar.UInt32
open FStar.Ghost
open FStar.Mul
open FStar.Int.Cast

module U8 = FStar.UInt8

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

#set-options "--initial_fuel 0 --max_fuel 0"

type bytes  = Seq.seq U8.t // Pure sequence of bytes

type  lbytes  (l:nat) = b:bytes   {Seq.length b == l}

(* type lbuffer (l:nat) = b:buffer {Buffer.length b == l} *)

#reset-options

let uint128_to_uint8 (a:UInt128.t) : Tot (b:UInt8.t{UInt8.v b = UInt128.v a % pow2 8})
  = Math.Lemmas.pow2_modulo_modulo_lemma_2 (UInt128.v a) 64 8;
    uint64_to_uint8 (FStar.UInt128.uint128_to_uint64 a)

#reset-options "--z3rlimit 20 --initial_fuel 0 --max_fuel 0"


open FStar.Seq

(* Little endian integer value of a sequence of bytes *)
let rec little_endian (b:bytes) : Tot (n:nat) (decreases (Seq.length b)) =
  if Seq.length b = 0 then 0
  else
    UInt8.v (head b) + pow2 8 * little_endian (tail b)

(* Big endian integer value of a sequence of bytes *)
let rec big_endian (b:bytes) : Tot (n:nat) (decreases (Seq.length b)) = 
  if Seq.length b = 0 then 0 
  else
    UInt8.v (last b) + pow2 8 * big_endian (Seq.slice b 0 (Seq.length b - 1))

#reset-options "--initial_fuel 1 --max_fuel 1"

val little_endian_null: len:nat{len < 16} -> Lemma
  (little_endian (Seq.create len 0uy) == 0)
val little_endian_null: len:nat{len < 16} -> Lemma
  (little_endian (Seq.create len 0uy) == 0)
len: Prims.nat{len < 16}
  -> FStar.Pervasives.Lemma
    (ensures FStar.Old.Endianness.little_endian (FStar.Seq.Base.create len 0uy) == 0)