val serialize32_flbytes32_backwards (len: asn1_int32)
    : serializer32_backwards (serialize_flbytes32 len)
val serialize32_flbytes32_backwards (len: asn1_int32)
    : serializer32_backwards (serialize_flbytes32 len)
let serialize32_flbytes32_backwards
  (len: asn1_int32)
: serializer32_backwards (serialize_flbytes32 len)
= fun (x: B32.lbytes32 len)
    #rrel #rel
    b pos
-> store_bytes x 0ul len b (pos - len);
   len
module ASN1.Low.Bytes32

open ASN1.Base
open ASN1.Spec.Bytes32
open ASN1.Low.Base
open LowParse.Low.Bytes
open FStar.Integers
module B32 = FStar.Bytes
/
prims.fst.checked LowParse.Low.Bytes.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Bytes.fsti.checked ASN1.Spec.Bytes32.fst.checked ASN1.Low.Base.fst.checked ASN1.Base.fst.checked
ASN1.Low.Bytes32.fst
len: ASN1.Base.asn1_int32
  -> ASN1.Low.Base.serializer32_backwards (ASN1.Spec.Bytes32.serialize_flbytes32 len)
ASN1.Base.asn1_int32 FStar.Bytes.lbytes32 LowStar.Monotonic.Buffer.srel ASN1.Low.Base.byte LowStar.Monotonic.Buffer.mbuffer FStar.UInt32.t Prims.unit LowParse.Low.Bytes.store_bytes FStar.UInt32.__uint_to_t FStar.Integers.op_Subtraction FStar.Integers.Unsigned FStar.Integers.W32 ASN1.Low.Base.serializer32_backwards LowParse.Spec.Base.total_constant_size_parser_kind FStar.Integers.v ASN1.Spec.Bytes32.parse_flbytes32 ASN1.Spec.Bytes32.serialize_flbytes32
let serialize32_flbytes32_backwards (len: asn1_int32)
    : serializer32_backwards (serialize_flbytes32 len) =
  
fun (x: B32.lbytes32 len) #rrel #rel b pos ->
  store_bytes x 0ul len b (pos - len);
  len