val parse_u8_spec
  (b: bytes)
: Lemma
  (requires (Seq.length b >= 1))
  (ensures (
    let pp = parse parse_u8 b in
    Some? pp /\ (
    let (Some (v, consumed)) = pp in
    U8.v v == E.be_to_n (Seq.slice b 0 1)
  )))
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)
val parse_u8_spec
  (b: bytes)
: Lemma
  (requires (Seq.length b >= 1))
  (ensures (
    let pp = parse parse_u8 b in
    Some? pp /\ (
    let (Some (v, consumed)) = pp in
    U8.v v == E.be_to_n (Seq.slice b 0 1)
  )))
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)
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 FStar.Endianness.reveal_be_to_n FStar.Seq.Base.slice LowParse.Bytes.byte Prims.unit FStar.Seq.Base.lemma_index_slice
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
val parse_u8_spec
  (b: bytes)
: Lemma
  (requires (Seq.length b >= 1))
  (ensures (
    let pp = parse parse_u8 b in
    Some? pp /\ (
    let (Some (v, consumed)) = pp in
    U8.v v == E.be_to_n (Seq.slice b 0 1)
  )))
b: LowParse.Bytes.bytes
  -> FStar.Pervasives.Lemma (requires FStar.Seq.Base.length b >= 1)
      (ensures
        (let pp = LowParse.Spec.Base.parse LowParse.Spec.Int.parse_u8 b in
          Some? pp /\
          (let _ = pp in
            (let FStar.Pervasives.Native.Some #_ (FStar.Pervasives.Native.Mktuple2 #_ #_ v _) = _ in
              FStar.UInt8.v v == FStar.Endianness.be_to_n (FStar.Seq.Base.slice b 0 1))
            <:
            Prims.logical)))