val uint128_to_uint8 (a: UInt128.t) : Tot (b: UInt8.t{UInt8.v b = UInt128.v a % pow2 8})
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})
  = Math.Lemmas.pow2_modulo_modulo_lemma_2 (UInt128.v a) 64 8;
    uint64_to_uint8 (FStar.UInt128.uint128_to_uint64 a)
module MiTLS.FStar.Old.Endianness
open MiTLS

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
/
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
MiTLS.FStar.Old.Endianness.fst
a: FStar.UInt128.t -> b: FStar.UInt8.t{FStar.UInt8.v b = FStar.UInt128.v a % Prims.pow2 8}
FStar.UInt128.t FStar.Int.Cast.uint64_to_uint8 FStar.UInt128.uint128_to_uint64 Prims.unit FStar.Math.Lemmas.pow2_modulo_modulo_lemma_2 FStar.UInt128.v FStar.UInt8.t Prims.b2t Prims.op_Equality Prims.int FStar.UInt8.v Prims.op_Modulus Prims.pow2
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)