val serialize_big_integer_as_octet_string_V
      (tag: (the_asn1_tag INTEGER & asn1_value_int32_of_big_integer))
    : serializer (parse_big_integer_as_octet_string_V tag)
val serialize_big_integer_as_octet_string_V
      (tag: (the_asn1_tag INTEGER & asn1_value_int32_of_big_integer))
    : serializer (parse_big_integer_as_octet_string_V tag)
let serialize_big_integer_as_octet_string_V
  (tag: (the_asn1_tag INTEGER & asn1_value_int32_of_big_integer))
: serializer (parse_big_integer_as_octet_string_V tag)
= serialize_synth
  (* p1 *) (weak_kind_of_big_integer
            `weaken`
            parse_big_integer_as_octet_string (snd tag))
  (* f2 *) (synth_big_integer_as_octet_string_V tag)
  (* s1 *) (weak_kind_of_big_integer
            `serialize_weaken`
            serialize_big_integer_as_octet_string (snd tag))
  (* g1 *) (synth_big_integer_as_octet_string_V_inverse tag)
  (* prf*) ()
module ASN1.Spec.Value.BigInteger

open ASN1.Spec.Base

open ASN1.Base
open ASN1.Spec.Tag
open ASN1.Spec.Length
open ASN1.Spec.Bytes32

open FStar.Integers

module B32 = FStar.Bytes

let lemma_synth_big_integer_as_octet_string_injective'
  (len: asn1_value_int32_of_big_integer)
  (s32 s32': parse_filter_refine (filter_big_integer_as_octet_string len))
: Lemma
  (requires synth_big_integer_as_octet_string len s32 == synth_big_integer_as_octet_string len s32')
  (ensures s32 == s32')
= if (v len = 1) then
  ( () )
  else if (s32 `B32.index` 0 = 0x00uy) then
  ( assert (B32.length s32 == B32.length s32');
    assert (s32' `B32.index` 0 == 0x00uy);
    assert (s32 `B32.index` 0 == s32' `B32.index` 0);
    assert (B32.slice s32 1ul len `B32.equal` B32.slice s32' 1ul len);
    assert (forall (i: UInt32.t { 1 <= v i /\ v i < v (B32.length s32 )}). s32  `B32.get` i == B32.slice s32  1ul len `B32.get` (i - 1ul) );
    assert (forall (i: UInt32.t { 1 <= v i /\ v i < v (B32.length s32')}). s32' `B32.get` i == B32.slice s32' 1ul len `B32.get` (i - 1ul) );
    assert (s32 `B32.equal` s32');
    B32.extensionality s32 s32' )
  else
  ( () )

let lemma_synth_big_integer_as_octet_string_injective len
= synth_injective_intro'
  (* f *) (synth_big_integer_as_octet_string len)
  (*prf*) (lemma_synth_big_integer_as_octet_string_injective' len)

let parse_big_integer_as_octet_string len
= lemma_synth_big_integer_as_octet_string_injective len;
  parse_flbytes32 len
  `parse_filter`
  filter_big_integer_as_octet_string len
  `parse_synth`
  synth_big_integer_as_octet_string len

let serialize_big_integer_as_octet_string len
= serialize_synth
  (* p1 *) (parse_flbytes32 len
            `parse_filter`
            filter_big_integer_as_octet_string len)
  (* f2 *) (synth_big_integer_as_octet_string len)
  (* s1 *) (serialize_flbytes32 len
            `serialize_filter`
            filter_big_integer_as_octet_string len)
  (* g1 *) (synth_big_integer_as_octet_string_inverse len)
  (* Prf*) (lemma_synth_big_integer_as_octet_string_injective len)

let lemma_serialize_big_integer_as_octet_string_unfold len value
= serialize_synth_eq
  (* p1 *) (parse_flbytes32 len
            `parse_filter`
            filter_big_integer_as_octet_string len)
  (* f2 *) (synth_big_integer_as_octet_string len)
  (* s1 *) (serialize_flbytes32 len
            `serialize_filter`
            filter_big_integer_as_octet_string len)
  (* g1 *) (synth_big_integer_as_octet_string_inverse len)
  (* Prf*) (lemma_synth_big_integer_as_octet_string_injective len)
  (* in *) (value)

let lemma_serialize_big_integer_as_octet_string_size len value
= lemma_serialize_big_integer_as_octet_string_unfold len value

noextract
let synth_big_integer_as_octet_string_V
  (tag: (the_asn1_tag INTEGER & asn1_value_int32_of_big_integer))
  (value: big_integer_as_octet_string_t
         { valid_big_integer_as_octet_string_prop (snd tag) value })
: GTot (refine_with_tag parser_tag_of_big_integer_as_octet_string tag)
= value

noextract inline_for_extraction
let synth_big_integer_as_octet_string_V_inverse
  (tag: (the_asn1_tag INTEGER & asn1_value_int32_of_big_integer))
  (value': refine_with_tag parser_tag_of_big_integer_as_octet_string tag)
: Tot (value: big_integer_as_octet_string_t
               { valid_big_integer_as_octet_string_prop (snd tag) value /\
                 value' == synth_big_integer_as_octet_string_V tag value})
= value'


///
/// Aux parser
///
noextract
let parse_big_integer_as_octet_string_V
  (tag: (the_asn1_tag INTEGER & asn1_value_int32_of_big_integer))
: parser (weak_kind_of_big_integer) (refine_with_tag parser_tag_of_big_integer_as_octet_string tag)
= weak_kind_of_big_integer
  `weaken`
  parse_big_integer_as_octet_string (snd tag)
  `parse_synth`
  synth_big_integer_as_octet_string_V tag

///
/// Aux serializer
///
/
prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Bytes.fsti.checked ASN1.Spec.Tag.fsti.checked ASN1.Spec.Length.fsti.checked ASN1.Spec.Bytes32.fst.checked ASN1.Spec.Base.fst.checked ASN1.Base.fst.checked
ASN1.Spec.Value.BigInteger.fst

    tag:
      (ASN1.Base.the_asn1_tag ASN1.Base.INTEGER *
        ASN1.Spec.Value.BigInteger.asn1_value_int32_of_big_integer)
  -> LowParse.Spec.Base.serializer (ASN1.Spec.Value.BigInteger.parse_big_integer_as_octet_string_V tag
        )
FStar.Pervasives.Native.tuple2 ASN1.Base.the_asn1_tag ASN1.Base.INTEGER ASN1.Spec.Value.BigInteger.asn1_value_int32_of_big_integer LowParse.Spec.Combinators.serialize_synth ASN1.Spec.Value.BigInteger.weak_kind_of_big_integer ASN1.Spec.Value.BigInteger.big_integer_as_octet_string_t ASN1.Spec.Value.BigInteger.valid_big_integer_as_octet_string_prop FStar.Pervasives.Native.snd LowParse.Spec.Base.refine_with_tag ASN1.Spec.Value.BigInteger.parser_tag_of_big_integer_as_octet_string LowParse.Spec.Base.weaken ASN1.Spec.Value.BigInteger.parse_big_integer_as_octet_string_kind ASN1.Spec.Value.BigInteger.parse_big_integer_as_octet_string ASN1.Spec.Value.BigInteger.synth_big_integer_as_octet_string_V LowParse.Spec.Combinators.serialize_weaken ASN1.Spec.Value.BigInteger.serialize_big_integer_as_octet_string ASN1.Spec.Value.BigInteger.synth_big_integer_as_octet_string_V_inverse LowParse.Spec.Base.serializer ASN1.Spec.Value.BigInteger.parse_big_integer_as_octet_string_V
let serialize_big_integer_as_octet_string_V
      (tag: (the_asn1_tag INTEGER & asn1_value_int32_of_big_integer))
    : serializer (parse_big_integer_as_octet_string_V tag) =
  
serialize_synth (weak_kind_of_big_integer `weaken` (parse_big_integer_as_octet_string (snd tag)))
  (synth_big_integer_as_octet_string_V tag)
  (weak_kind_of_big_integer `serialize_weaken` (serialize_big_integer_as_octet_string (snd tag)))
  (synth_big_integer_as_octet_string_V_inverse tag)
  ()