val parse_flbytes32_gen (len: asn1_int32) (s: bytes{Seq.length s == v len})
    : GTot (B32.lbytes32 len)
val parse_flbytes32_gen (len: asn1_int32) (s: bytes{Seq.length s == v len})
    : GTot (B32.lbytes32 len)
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
module ASN1.Spec.Bytes32

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

open FStar.Integers
module B32 = FStar.Bytes
/
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 -> s: ASN1.Base.bytes{FStar.Seq.Base.length s == FStar.Integers.v len}
  -> Prims.GTot (FStar.Bytes.lbytes32 len)
ASN1.Base.asn1_int32 ASN1.Base.bytes Prims.eq2 Prims.int Prims.l_or Prims.b2t Prims.op_GreaterThanOrEqual FStar.Integers.within_bounds FStar.Integers.Unsigned FStar.Integers.W32 FStar.Seq.Base.length ASN1.Base.byte FStar.Integers.v FStar.Bytes.hide Prims.unit LowParse.Spec.Bytes.lt_pow2_32 FStar.Bytes.lbytes32
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