val length_of_asn1_integer (value: datatype_of_asn1_type INTEGER)
    : GTot (asn1_value_length_of_type INTEGER)
val length_of_asn1_integer (value: datatype_of_asn1_type INTEGER)
    : GTot (asn1_value_length_of_type INTEGER)
let length_of_asn1_integer
  (value: datatype_of_asn1_type INTEGER)
: GTot (asn1_value_length_of_type INTEGER)
= let vx = v #(Signed W32) value in
  if      0         <= vx && vx <= 0x7F      then
  ( 1 )
  else if 0x7F       < vx && vx <= 0xFF       then
  ( 2 )
  else if 0xFF       < vx && vx <= 0x7FFF     then
  ( 2 )
  else if 0x7FFF     < vx && vx <= 0xFFFF     then
  ( 3 )
  else if 0xFFFF     < vx && vx <= 0x7FFFFF   then
  ( 3 )
  else if 0x7FFFFF   < vx && vx <= 0xFFFFFF   then
  ( 4 )
  else if 0xFFFFFF   < vx && vx <= 0x7FFFFFFF then
  ( 4 )
module ASN1.Spec.Value.INTEGER

open ASN1.Spec.Base
open LowParse.Spec.SeqBytes.Base

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

open FStar.Integers

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

(* NOTE: This module defines:
         1) The ASN1 `INTEGER` Value Parser and Serializer
         2) The ASN1 `INTEGER` TLV Parser and Serializer

         And each part is organized as:
         1) Aux (ghost) functions with prefix `filter_` to filter out invalid input bytes
         2) Aux (ghost) functions with prefix `synth_` to decode the valid input bytes into our
            representation of INTEGER values. These functions are injective.
         3) Aux (ghost) functions with prefix `synth_` and suffix `_inverse` to encode our
            representation of INTEGER into bytes. These functions are the inverse of
            corresponding synth functions.
         4) Functions with the prefix `parse_` are parsers constructed using parser combinators and
            aux functions.
         5) Functions with the prefix `serialize_` are serializers constructed using serializer
            combinators and aux functions.
         6) Lemma with suffix `_unfold` reveals the computation of parser/serialzier.
         7) Lemma with suffix `_size` reveals the length of a serialization.
*)

(*
NOTE: 1. Negative: `**p & 0x80 == 0`, reject
      2. Zero    : as `[0x02; 0x01; 0x00]` for INTEGER or `[0x0A; 0x01; 0x00]` fir ENUMERATED tags
      3. Positive: if the most significant bit of a positive integer is `1`, then add a leading zero.

NOTE: MbedTLS's implementation seems allow arbitrary leading zeros. We only allow one leading zero for now.
NOTE: We only allow at most 4-byte positive integers ([0, 0x7FFFFFFF]). If an integer is encoded into 5 bytes with a leading
      zero, then it must be a negative integer.
*)

//////////////////////////////////////////////////////////////////////
////       ASN1 `INTEGER` Value Parser/Serializer
//////////////////////////////////////////////////////////////////////

/// filters the valid input bytes accoring to the encoding rule
/// 1. valid length of input bytes is [1, 4]
/// 2. only positive integers, whether
///    a) the most significant bit is `0` (the first byte is less than 0x80uy/0b10000000uy), or
///    b) the first byte is a leading zero 0x00uy and the second byte's most significant bit is `1`
///       (the second byte is greater then or equal to 0x80uy/0b10000000uy)
noextract
val filter_asn1_integer
  (l: asn1_value_length_of_type INTEGER) (* 1 <= l <= 4*)
  (s: lbytes l)
: GTot (bool)
/
prims.fst.checked LowParse.Spec.SeqBytes.Base.fst.checked FStar.UInt8.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked ASN1.Spec.Tag.fsti.checked ASN1.Spec.Length.fsti.checked ASN1.Spec.Base.fst.checked ASN1.Base.fst.checked
ASN1.Spec.Value.INTEGER.fsti
value: ASN1.Base.datatype_of_asn1_type ASN1.Base.INTEGER
  -> Prims.GTot (ASN1.Base.asn1_value_length_of_type ASN1.Base.INTEGER)
ASN1.Base.datatype_of_asn1_type ASN1.Base.INTEGER Prims.op_AmpAmp FStar.Integers.op_Less_Equals FStar.Integers.Signed FStar.Integers.Winfinite Prims.bool FStar.Integers.op_Less ASN1.Base.asn1_value_length_of_type FStar.Integers.int_t FStar.Pervasives.norm Prims.Cons FStar.Pervasives.norm_step FStar.Pervasives.iota FStar.Pervasives.delta_attr Prims.string Prims.Nil FStar.Pervasives.Native.Mktuple2 FStar.Integers.signed_width FStar.Pervasives.Native.option Prims.int FStar.Integers.W32 FStar.Integers.nat_of_width FStar.Integers.width_of_sw FStar.Integers.width Prims.l_True FStar.Int.size FStar.Integers.fixed_width FStar.UInt.size FStar.Integers.v
let length_of_asn1_integer (value: datatype_of_asn1_type INTEGER)
    : GTot (asn1_value_length_of_type INTEGER) =
  
let vx = v #(Signed W32) value in
if 0 <= vx && vx <= 0x7F
then (1)
else
  if 0x7F < vx && vx <= 0xFF
  then (2)
  else
    if 0xFF < vx && vx <= 0x7FFF
    then (2)
    else
      if 0x7FFF < vx && vx <= 0xFFFF
      then (3)
      else
        if 0xFFFF < vx && vx <= 0x7FFFFF
        then (3)
        else
          if 0x7FFFFF < vx && vx <= 0xFFFFFF
          then (4)
          else if 0xFFFFFF < vx && vx <= 0x7FFFFFFF then (4)