val len_of_asn1_integer (value: datatype_of_asn1_type INTEGER)
    : (len: asn1_value_int32_of_type INTEGER {v len == length_of_asn1_integer value})
val len_of_asn1_integer (value: datatype_of_asn1_type INTEGER)
    : (len: asn1_value_int32_of_type INTEGER {v len == length_of_asn1_integer value})
let len_of_asn1_integer
  (value: datatype_of_asn1_type INTEGER)
: (len: asn1_value_int32_of_type INTEGER { v len == length_of_asn1_integer value } )
= if      0l         <= value && value <= 0x7Fl      then
  ( 1ul )
  else if 0x7Fl       < value && value <= 0xFFl       then
  ( 2ul )
  else if 0xFFl       < value && value <= 0x7FFFl     then
  ( 2ul )
  else if 0x7FFFl     < value && value <= 0xFFFFl     then
  ( 3ul )
  else if 0xFFFFl     < value && value <= 0x7FFFFFl   then
  ( 3ul )
  else if 0x7FFFFFl   < value && value <= 0xFFFFFFl   then
  ( 4ul )
  else // if 0xFFFFFFl   < value && value <= 0x7FFFFFFFl then
  ( 4ul )
module ASN1.Low.Value.INTEGER

open ASN1.Base
open ASN1.Spec.Value.INTEGER
open ASN1.Low.Base

open FStar.Integers

(* NOTE: Read after `ASN1.Spec.Tag`, `ASN1.Spec.Length` *)

/// Implementation of length computation of `INTEGER` value's serialization
/
prims.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Int32.fsti.checked ASN1.Spec.Value.INTEGER.fsti.checked ASN1.Low.Base.fst.checked ASN1.Base.fst.checked
ASN1.Low.Value.INTEGER.fsti
value: ASN1.Base.datatype_of_asn1_type ASN1.Base.INTEGER
  -> len:
    ASN1.Base.asn1_value_int32_of_type ASN1.Base.INTEGER
      {FStar.Integers.v len == ASN1.Spec.Value.INTEGER.length_of_asn1_integer value}
ASN1.Base.datatype_of_asn1_type ASN1.Base.INTEGER Prims.op_AmpAmp FStar.Integers.op_Less_Equals FStar.Integers.Signed FStar.Integers.W32 FStar.Int32.__int_to_t FStar.UInt32.__uint_to_t Prims.bool FStar.Integers.op_Less ASN1.Base.asn1_value_int32_of_type Prims.eq2 FStar.Integers.int_t FStar.Integers.Winfinite Prims.l_or FStar.Integers.within_bounds FStar.Integers.Unsigned Prims.l_and Prims.b2t FStar.Integers.op_Greater_Equals ASN1.Base.asn1_value_length_inbound_of_type FStar.Integers.v ASN1.Spec.Value.INTEGER.length_of_asn1_integer
let len_of_asn1_integer (value: datatype_of_asn1_type INTEGER)
    : (len: asn1_value_int32_of_type INTEGER {v len == length_of_asn1_integer value}) =
  
if 0l <= value && value <= 0x7Fl
then (1ul)
else
  if 0x7Fl < value && value <= 0xFFl
  then (2ul)
  else
    if 0xFFl < value && value <= 0x7FFFl
    then (2ul)
    else
      if 0x7FFFl < value && value <= 0xFFFFl
      then (3ul)
      else
        if 0xFFFFl < value && value <= 0x7FFFFFl
        then (3ul)
        else if 0x7FFFFFl < value && value <= 0xFFFFFFl then (4ul) else (4ul)