val parse_asn1_bit_string_kind : l: ASN1.Base.asn1_value_length_of_type ASN1.Base.BIT_STRING -> LowParse.Spec.Base.parser_kind
let parse_asn1_bit_string_kind (l: asn1_value_length_of_type BIT_STRING) = constant_size_parser_kind l
module ASN1.Spec.Value.BIT_STRING

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`, `ASN1.Spec.Value.BIT_STRING` *)

(* NOTE: This module defines:
         1) The ASN1 `BIT_STRING` Value Parser and Serializer
         2) The ASN1 `BIT_STRING` 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 BIT_STRING values. These functions are injective.
         3) Aux (ghost) functions with prefix `synth_` and suffix `_inverse` to encode our
            representation of BIT_STRING 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.
*)

/// TEST
///

// let bs_empty   : datatype_of_asn1_type BIT_STRING = (|1ul, 0ul, B32.empty_bytes |)
// let bs_0_unused: datatype_of_asn1_type BIT_STRING = (|2ul, 0ul, B32.create 1ul 0b1uy|)
// let bs_1_unused: datatype_of_asn1_type BIT_STRING = (|2ul, 1ul, B32.create 1ul 0b10uy|)
// let bs_2_unused: datatype_of_asn1_type BIT_STRING = (|2ul, 2ul, B32.create 1ul 0b100uy|)
// let bs_3_unused: datatype_of_asn1_type BIT_STRING = (|2ul, 3ul, B32.create 1ul 0b1000uy|)
// let bs_4_unused: datatype_of_asn1_type BIT_STRING = (|2ul, 4ul, B32.create 1ul 0b10000uy|)
// let bs_5_unused: datatype_of_asn1_type BIT_STRING = (|2ul, 5ul, B32.create 1ul 0b100000uy|)
// let bs_6_unused: datatype_of_asn1_type BIT_STRING = (|2ul, 6ul, B32.create 1ul 0b1000000uy|)
// let bs_7_unused: datatype_of_asn1_type BIT_STRING = (|2ul, 7ul, B32.create 1ul 0b10000000uy|)

(*
   Len = 1, unused = 0, bytes = []
   Len = 2, unused = x, bytes = [_]
*)

// let (.[]) = B32.index

/// filter valid input bytes
/// 1) if the length of input bytes is 1 (the minimal length), then the first and
///    the only byte, which represents the `unused_bits`, must be 0x00uy
/// 2) otherwise, the `unused_bits` must be in [0, 7] and the last byte's last
/// `unused_bits` bits must be zero.

val filter_asn1_bit_string
  (l: asn1_value_length_of_type BIT_STRING)
  (raw: lbytes l)
: GTot (bool)

/// Decode the valid input bytes into our representation of BIT_STRING,
/// which is a dependent tuple of `total length, unused_bits, octets`
val synth_asn1_bit_string
  (l: asn1_value_length_of_type BIT_STRING)
  (raw: parse_filter_refine (filter_asn1_bit_string l))
: GTot (value: datatype_of_asn1_type BIT_STRING {
               l == v value.bs_len })


/// Encode our representation of BIT_STRING into bytes
val synth_asn1_bit_string_inverse
  (l: asn1_value_length_of_type BIT_STRING)
  (value: datatype_of_asn1_type BIT_STRING {
          l == v value.bs_len })
: GTot (raw: parse_filter_refine (filter_asn1_bit_string l) { value == synth_asn1_bit_string l raw })
/
prims.fst.checked LowParse.Spec.SeqBytes.Base.fst.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.BIT_STRING.fsti
l: ASN1.Base.asn1_value_length_of_type ASN1.Base.BIT_STRING -> LowParse.Spec.Base.parser_kind
ASN1.Base.asn1_value_length_of_type ASN1.Base.BIT_STRING LowParse.Spec.Combinators.constant_size_parser_kind LowParse.Spec.Base.parser_kind
let parse_asn1_bit_string_kind (l: asn1_value_length_of_type BIT_STRING) =
  
constant_size_parser_kind l