val serialize32_u8 : serializer32 serialize_u8
let serialize32_u8
= (fun (input: U8.t) ->
    let b = B32.create 1ul input in
    B32.b32_reveal_create 1ul input;
    (b <: (res: bytes32 { serializer32_correct #_ #_ #parse_u8 serialize_u8 input res } )))
val serialize32_u8 : serializer32 serialize_u8
let serialize32_u8 =
(fun (input: U8.t) ->
    let b = B32.create 1ul input in
    B32.b32_reveal_create 1ul input;
    (b <: (res: bytes32{serializer32_correct #_ #_ #parse_u8 serialize_u8 input res})))
LowParse.SLow.Int.fst.checked
prims.fst.checked LowParse.Spec.Int.fst.checked LowParse.Spec.Endianness.Instances.fst.checked LowParse.SLow.Endianness.fst.checked LowParse.SLow.Combinators.fst.checked LowParse.Bytes32.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
LowParse.SLow.Int.fst
FStar.UInt8.t LowParse.SLow.Base.bytes32 LowParse.SLow.Base.serializer32_correct LowParse.Spec.Int.parse_u8_kind LowParse.Spec.Int.parse_u8 LowParse.Spec.Int.serialize_u8 Prims.unit LowParse.Bytes32.b32_reveal_create FStar.UInt32.__uint_to_t FStar.Bytes.lbytes FStar.UInt32.v FStar.UInt32.uint_to_t FStar.UInt32.t Prims.l_Forall Prims.b2t FStar.UInt32.lt Prims.eq2 FStar.Bytes.get FStar.Bytes.create
module LowParse.SLow.Int
open LowParse.SLow.Combinators

module Seq = FStar.Seq
module U8  = FStar.UInt8
module U16 = FStar.UInt16
module U32 = FStar.UInt32
module U64 = FStar.UInt64
module B32 = LowParse.Bytes32

friend LowParse.Spec.Int

let parse32_u8 =
  decode_u8_injective ();
  make_total_constant_size_parser32 1 1ul
    decode_u8
    ()
    (fun (b: B32.lbytes 1) ->
      let r = B32.get b 0ul in
      assert (r == Seq.index (B32.reveal b) 0);
      B32.b32_index_reveal b 0;
      (r <: (y: U8.t { y == decode_u8 (B32.reveal b) })))
val serialize32_u8 : serializer32 serialize_u8
LowParse.SLow.Base.serializer32 LowParse.Spec.Int.serialize_u8