val parse_flbytes32 (len: asn1_int32)
    : Tot (parser (total_constant_size_parser_kind (v len)) (B32.lbytes32 len))
val parse_flbytes32 (len: asn1_int32)
    : Tot (parser (total_constant_size_parser_kind (v len)) (B32.lbytes32 len))
let parse_flbytes32
  (len: asn1_int32 )
: Tot (parser (total_constant_size_parser_kind (v len)) (B32.lbytes32 len))
= make_total_constant_size_parser (v len) (B32.lbytes32 len) (parse_flbytes32_gen len)
module ASN1.Spec.Bytes32

open LowParse.Spec.Base
open LowParse.Spec.Bytes
open ASN1.Base

open FStar.Integers
module B32 = FStar.Bytes

let parse_flbytes32_gen
  (len: asn1_int32 )
  (s: bytes { Seq.length s == v len } )
: GTot (B32.lbytes32 len)
= lt_pow2_32 (v len);
  B32.hide s
/
prims.fst.checked LowParse.Spec.Bytes.fst.checked LowParse.Spec.Base.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Classical.fsti.checked FStar.Bytes.fsti.checked ASN1.Base.fst.checked
ASN1.Spec.Bytes32.fst
len: ASN1.Base.asn1_int32
  -> LowParse.Spec.Base.parser (LowParse.Spec.Base.total_constant_size_parser_kind (FStar.Integers.v
              len))
      (FStar.Bytes.lbytes32 len)
ASN1.Base.asn1_int32 LowParse.Spec.Combinators.make_total_constant_size_parser FStar.Integers.v FStar.Integers.Unsigned FStar.Integers.W32 FStar.Bytes.lbytes32 ASN1.Spec.Bytes32.parse_flbytes32_gen LowParse.Spec.Base.parser LowParse.Spec.Base.total_constant_size_parser_kind
let parse_flbytes32 (len: asn1_int32)
    : Tot (parser (total_constant_size_parser_kind (v len)) (B32.lbytes32 len)) =
  
make_total_constant_size_parser (v len) (B32.lbytes32 len) (parse_flbytes32_gen len)