val decode_u16 (b: bytes{Seq.length b == 2}) : GTot U16.t
let decode_u16
  (b: bytes { Seq.length b == 2 } )
: GTot U16.t
= E.lemma_be_to_n_is_bounded b;
  U16.uint_to_t (E.be_to_n b)
val decode_u16 (b: bytes{Seq.length b == 2}) : GTot U16.t
let decode_u16 (b: bytes{Seq.length b == 2}) : GTot U16.t =
E.lemma_be_to_n_is_bounded b;
U16.uint_to_t (E.be_to_n b)
LowParse.Spec.Int.fst.checked
prims.fst.checked LowParse.Spec.Seq.fst.checked LowParse.Spec.Combinators.fsti.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
LowParse.Spec.Int.fst
LowParse.Bytes.bytes Prims.eq2 Prims.int FStar.Seq.Base.length LowParse.Bytes.byte FStar.UInt16.uint_to_t FStar.Endianness.be_to_n Prims.unit FStar.Endianness.lemma_be_to_n_is_bounded FStar.UInt16.t
module LowParse.Spec.Int
open LowParse.Spec.Combinators

let decode_u8
  (b: bytes { Seq.length b == 1 } )
: Tot U8.t
= Seq.index b 0

let decode_u8_injective () : Lemma
  (make_total_constant_size_parser_precond 1 U8.t decode_u8)
= ()

let tot_parse_u8 =
  decode_u8_injective ();
  tot_make_total_constant_size_parser 1 U8.t decode_u8

let parse_u8_spec
  b
=
  Seq.lemma_index_slice b 0 1 0;
  E.reveal_be_to_n (Seq.slice b 0 1);
  E.reveal_be_to_n (Seq.slice (Seq.slice b 0 1) 0 0)

let parse_u8_spec' b = ()

let serialize_u8 =
  Seq.create 1

let serialize_u8_spec x = ()

let decode_u16
  (b: bytes { Seq.length b == 2 } )
val decode_u16 (b: bytes{Seq.length b == 2}) : GTot U16.t
b: LowParse.Bytes.bytes{FStar.Seq.Base.length b == 2} -> Prims.GTot FStar.UInt16.t