val valid_big_integer_as_octet_string_prop
      (len: asn1_value_int32_of_big_integer)
      (x: big_integer_as_octet_string_t)
    : Type0
val valid_big_integer_as_octet_string_prop
      (len: asn1_value_int32_of_big_integer)
      (x: big_integer_as_octet_string_t)
    : Type0
let valid_big_integer_as_octet_string_prop
  (len: asn1_value_int32_of_big_integer)
  (x: big_integer_as_octet_string_t)
: Type0
= let (.[]) = B32.get in
  v (x.len) > 0 /\
  ( if v len = 1 then
    ( v (x.len) == v len /\ (x.s).[0ul] < 0x80uy )
    else if ((x.s).[0ul] >= 0x80uy) then
    ( v (x.len) == v len - 1 )
    else
    ( v (x.len) == v len /\ (x.s).[0ul] > 0x00uy ) )
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 LowParse.Spec.DER

open FStar.Integers

module U32 = FStar.UInt32
module B32 = FStar.Bytes

(*

  encoded -----parse------>  decoded
   bytes  <---serialize--- octet string
*)

unfold
[@@ "opaque_to_smt"]
let asn1_value_length_of_big_integer
= l: asn1_length_t { 1 <= l /\ l <= asn1_length_max - 6}

unfold
[@@ "opaque_to_smt"]
let asn1_value_int32_of_big_integer
= n: U32.t {asn1_int32_inbounds 1 (asn1_length_max - 6) n}

unfold
[@@ "opaque_to_smt"]
let asn1_TLV_length_of_big_integer
= l: asn1_length_t { 3 <= l /\ l <= asn1_length_max }

unfold
[@@ "opaque_to_smt"]
let asn1_TLV_int32_of_big_integer
= n: U32.t {asn1_int32_inbounds 3 asn1_length_max n}

let valid_big_integer_as_octet_string
  (len: asn1_value_int32_of_type OCTET_STRING)
  (s32: B32.lbytes32 len)
= let (.[]) = B32.get in
(* no nil *)
  v len > 0 /\
(* no leading zero byte if length > 1 *)
  (if v len > 1 then s32.[0ul] =!= 0x00uy else True) /\
(* leave one space for leading zero byte *)
  (if s32.[0ul] >= 0x80uy then v len <= asn1_length_max - 7 else True)

let big_integer_as_octet_string_t
= x: datatype_of_asn1_type OCTET_STRING
  { valid_big_integer_as_octet_string (x.len) (x.s) }
/
prims.fst.checked LowParse.Spec.DER.fsti.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.Low.Length.fsti.checked ASN1.Base.fst.checked
ASN1.Spec.Value.BigInteger.fsti

    len: ASN1.Spec.Value.BigInteger.asn1_value_int32_of_big_integer ->
    x: ASN1.Spec.Value.BigInteger.big_integer_as_octet_string_t
  -> Type0
ASN1.Spec.Value.BigInteger.asn1_value_int32_of_big_integer ASN1.Spec.Value.BigInteger.big_integer_as_octet_string_t Prims.l_and Prims.b2t FStar.Integers.op_Greater FStar.Integers.Signed FStar.Integers.Winfinite FStar.Integers.v FStar.Integers.Unsigned FStar.Integers.W32 ASN1.Base.__proj__Mkoctet_string_t__item__len Prims.op_Equality Prims.int Prims.eq2 FStar.Integers.int_t Prims.l_or FStar.Integers.within_bounds FStar.Integers.op_Less FStar.Integers.W8 ASN1.Base.__proj__Mkoctet_string_t__item__s FStar.UInt32.__uint_to_t FStar.UInt8.__uint_to_t Prims.bool FStar.Integers.op_Greater_Equals FStar.Integers.op_Subtraction Prims.logical FStar.Bytes.bytes FStar.UInt32.t Prims.op_LessThan FStar.UInt32.v FStar.Bytes.len FStar.UInt8.t Prims.l_True FStar.Seq.Base.index FStar.Bytes.reveal FStar.Bytes.get
let valid_big_integer_as_octet_string_prop
      (len: asn1_value_int32_of_big_integer)
      (x: big_integer_as_octet_string_t)
    : Type0 =
  
let ( .[] ) = B32.get in
v (x.len) > 0 /\
(if v len = 1
  then (v (x.len) == v len /\ (x.s).[ 0ul ] < 0x80uy)
  else
    if ((x.s).[ 0ul ] >= 0x80uy)
    then (v (x.len) == v len - 1)
    else (v (x.len) == v len /\ (x.s).[ 0ul ] > 0x00uy))