val parse_asn1_integer_kind : l: ASN1.Base.asn1_value_length_of_type ASN1.Base.INTEGER -> LowParse.Spec.Base.parser_kind
let parse_asn1_integer_kind (l: asn1_value_length_of_type INTEGER) = constant_size_parser_kind l
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)

/// Length computation function/specification for a `INTEGER` value's serialization
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 )

(* NOTE: Why this function signature will not pass type check when
         `datatype_of_asn1_type` is marked as `unfold`? *)
(* NOTE: Why I must explicitly provide #(Signed W32) everywhere? *)

/// Decode the valid input bytes to our represenation of ASN1 `INTEGER` value,
/// which is a _positive_ _signed_ 32-bit integer
/// 1) If the first byte is less then 0x80uy, then just decode it as an integer (in Big-Endian)
/// 2) If the first byte is a leading zero, then truncate it and decode the rest bytes as an
///    integer (in Big-Endian)
#restart-solver
noextract
val synth_asn1_integer
  (l: asn1_value_length_of_type INTEGER)
  (s: parse_filter_refine (filter_asn1_integer l))
: GTot (value: datatype_of_asn1_type INTEGER { l == length_of_asn1_integer value })


/// Encode an integre accoding to the encoding rule
noextract
val synth_asn1_integer_inverse
  (l: asn1_value_length_of_type INTEGER)
  (value: datatype_of_asn1_type INTEGER { l == length_of_asn1_integer value } )
: GTot (s: parse_filter_refine (filter_asn1_integer l) { value == synth_asn1_integer l s })

/// Prove that the our decoding function is injective when there is a leading zero
/// in the input bytes

val synth_asn1_integer_injective_with_leading_zero
  (l: asn1_value_length_of_type INTEGER)
  (s1 s2: parse_filter_refine (filter_asn1_integer l))
: Lemma
  (requires synth_asn1_integer l s1 == synth_asn1_integer l s2 /\
            s1.[0] == 0x00uy)
  (ensures  s2.[0] == 0x00uy /\ s1 `Seq.equal` s2)

/// Prove that the our decoding function is injective when there is no leading zero
/// in the input bytes
val synth_asn1_integer_injective_without_leading_zero
  (l: asn1_value_length_of_type INTEGER)
  (s1 s2: parse_filter_refine (filter_asn1_integer l))
: Lemma
  (requires synth_asn1_integer l s1 == synth_asn1_integer l s2 /\
            s1.[0] <> 0x00uy /\ s2.[0] <> 0x00uy)
  (ensures  s1 `Seq.equal` s2)

/// Prove that the our decoding function is injective
val synth_asn1_integer_injective'
  (l: asn1_value_length_of_type INTEGER)
  (s1 s2: parse_filter_refine (filter_asn1_integer l))
: Lemma
  (requires synth_asn1_integer l s1 == synth_asn1_integer l s2)
  (ensures s1 `Seq.equal` s2)

val synth_asn1_integer_injective
  (l: asn1_value_length_of_type INTEGER)
: Lemma (synth_injective (synth_asn1_integer l))
/
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
l: ASN1.Base.asn1_value_length_of_type ASN1.Base.INTEGER -> LowParse.Spec.Base.parser_kind
ASN1.Base.asn1_value_length_of_type ASN1.Base.INTEGER LowParse.Spec.Combinators.constant_size_parser_kind LowParse.Spec.Base.parser_kind
let parse_asn1_integer_kind (l: asn1_value_length_of_type INTEGER) =
  
constant_size_parser_kind l