val serialize_flbytes32_correct (len: asn1_int32)
    : Lemma (serializer_correct (parse_flbytes (v len)) (serialize_flbytes32' len))
val serialize_flbytes32_correct (len: asn1_int32)
    : Lemma (serializer_correct (parse_flbytes (v len)) (serialize_flbytes32' len))
let serialize_flbytes32_correct
  (len: asn1_int32)
: Lemma
  (serializer_correct (parse_flbytes (v len)) (serialize_flbytes32' len))
= let prf
    (input: B32.lbytes32 len)
  : Lemma
    (
      let ser = serialize_flbytes32' len input in
      Seq.length ser == v len /\
      parse (parse_flbytes32 len) ser == Some (input, (v len))
    )
  = ()
  in
  Classical.forall_intro prf
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

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)

let serialize_flbytes32'
  (len: asn1_int32)
: Tot (bare_serializer (B32.lbytes32 len))
= fun (x: B32.lbytes32 len) -> (
    lt_pow2_32 (v len);
    B32.reveal x
  )
/
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
  -> FStar.Pervasives.Lemma
    (ensures
      LowParse.Spec.Base.serializer_correct (LowParse.Spec.Bytes.parse_flbytes (FStar.Integers.v len
            ))
        (ASN1.Spec.Bytes32.serialize_flbytes32' len))
ASN1.Base.asn1_int32 FStar.Classical.forall_intro FStar.Bytes.lbytes32 Prims.l_and 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 LowParse.Bytes.byte ASN1.Spec.Bytes32.serialize_flbytes32' FStar.Integers.v FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple2 LowParse.Spec.Base.consumed_length LowParse.Spec.Base.parse ASN1.Spec.Bytes32.parse_flbytes32 FStar.Pervasives.Native.Some FStar.Pervasives.Native.Mktuple2 Prims.unit Prims.l_True Prims.squash FStar.Pervasives.norm Prims.Cons FStar.Pervasives.norm_step FStar.Pervasives.iota FStar.Pervasives.delta_attr Prims.string Prims.Nil FStar.Integers.signed_width FStar.Integers.nat_of_width FStar.Integers.width_of_sw FStar.Integers.width FStar.Int.size FStar.Integers.fixed_width FStar.UInt.size FStar.UInt32.v FStar.Pervasives.pattern LowParse.Bytes.bytes LowParse.Spec.Base.serializer_correct LowParse.Spec.Base.total_constant_size_parser_kind FStar.Bytes.lbytes LowParse.Spec.Bytes.parse_flbytes
let serialize_flbytes32_correct (len: asn1_int32)
    : Lemma (serializer_correct (parse_flbytes (v len)) (serialize_flbytes32' len)) =
  
let prf (input: B32.lbytes32 len)
    : Lemma
    (let ser = serialize_flbytes32' len input in
      Seq.length ser == v len /\ parse (parse_flbytes32 len) ser == Some (input, (v len))) =
  ()
in
Classical.forall_intro prf