val serialize_asn1_bit_string
  (l: asn1_value_length_of_type BIT_STRING)
: serializer (parse_asn1_bit_string l)
val serialize_asn1_bit_string
  (l: asn1_value_length_of_type BIT_STRING)
: serializer (parse_asn1_bit_string l)
let serialize_asn1_bit_string l
= serialize_synth
  (* p1 *) (parse_seq_flbytes l
            `parse_filter`
            filter_asn1_bit_string l)
  (* f2 *) (synth_asn1_bit_string l)
  (* s1 *) (serialize_seq_flbytes l
            `serialize_filter`
            filter_asn1_bit_string l)
  (* g1 *) (synth_asn1_bit_string_inverse l)
  (* prf*) (synth_asn1_bit_string_injective 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

module B32 = FStar.Bytes

(* 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.

let filter_asn1_bit_string l raw
= let unused_bits = raw.[0] in
  if l = 1 then
  ( unused_bits = 0uy )
  else
  ( let mask = normalize_term (pow2 (v unused_bits)) in
    0uy <= unused_bits && unused_bits <= 7uy &&
    (* x % 0b10..0 to check whether the last ... bits is 0 *)
    0 = normalize_term ((v raw.[l - 1]) % mask) )

/// Decode the valid input bytes into our representation of BIT_STRING,
/// which is a dependent tuple of `total length, unused_bits, octets`
let synth_asn1_bit_string l raw
= let unused_bits: n: asn1_int32 {0 <= v n /\ v n <= 7} = cast raw.[0] in
  let s32 = B32.hide (Seq.slice raw 1 l) in
  { bs_len         = u l;
    bs_unused_bits = unused_bits;
    bs_s           = s32 }

/// Prove our decode function is injective
#push-options "--z3rlimit 16"
noextract
let synth_asn1_bit_string_injective'
  (l: asn1_value_length_of_type BIT_STRING)
  (raw1 raw2: parse_filter_refine (filter_asn1_bit_string l))
: Lemma
  (requires synth_asn1_bit_string l raw1 == synth_asn1_bit_string l raw2)
  (ensures raw1 == raw2)
= Seq.lemma_split raw1 1;
  Seq.lemma_split raw2 1;
  assert (raw1 `Seq.equal` raw2)
#pop-options

noextract
let synth_asn1_bit_string_injective
  (l: asn1_value_length_of_type BIT_STRING)
: Lemma (
  synth_injective (synth_asn1_bit_string l)
)
= synth_injective_intro'
  (* f *) (synth_asn1_bit_string l)
  (*prf*) (synth_asn1_bit_string_injective' l)

/// Encode our representation of BIT_STRING into bytes
let synth_asn1_bit_string_inverse l value
= let raw = cast value.bs_unused_bits `Seq.cons` B32.reveal value.bs_s in
  let value' = synth_asn1_bit_string l raw in
  B32.extensionality value.bs_s value'.bs_s;
  raw

///
/// ASN1 BIT_STRING Value Parser
///
noextract
let parse_asn1_bit_string l
= synth_asn1_bit_string_injective l;
  parse_seq_flbytes l
  `parse_filter`
  filter_asn1_bit_string l
  `parse_synth`
  synth_asn1_bit_string l

///
/// ASN1 BIT_STRING Value Serialzier
/
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 FStar.Bytes.fsti.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.fst
l: ASN1.Base.asn1_value_length_of_type ASN1.Base.BIT_STRING
  -> LowParse.Spec.Base.serializer (ASN1.Spec.Value.BIT_STRING.parse_asn1_bit_string l)
ASN1.Base.asn1_value_length_of_type ASN1.Base.BIT_STRING LowParse.Spec.Combinators.serialize_synth LowParse.Spec.Combinators.parse_filter_kind LowParse.Spec.Base.total_constant_size_parser_kind LowParse.Spec.Combinators.parse_filter_refine FStar.Seq.Properties.lseq LowParse.Bytes.byte ASN1.Spec.Value.BIT_STRING.filter_asn1_bit_string ASN1.Base.datatype_of_asn1_type Prims.eq2 FStar.Integers.int_t FStar.Integers.Signed FStar.Integers.Winfinite Prims.l_or Prims.l_and Prims.b2t FStar.Integers.op_Greater_Equals ASN1.Base.asn1_value_length_inbound_of_type FStar.Integers.within_bounds FStar.Integers.Unsigned FStar.Integers.W32 FStar.Integers.v ASN1.Base.__proj__Mkbit_string_t__item__bs_len LowParse.Spec.Combinators.parse_filter LowParse.Spec.SeqBytes.Base.parse_seq_flbytes ASN1.Spec.Value.BIT_STRING.synth_asn1_bit_string LowParse.Spec.Combinators.serialize_filter LowParse.Spec.SeqBytes.Base.serialize_seq_flbytes ASN1.Spec.Value.BIT_STRING.synth_asn1_bit_string_inverse ASN1.Spec.Value.BIT_STRING.synth_asn1_bit_string_injective LowParse.Spec.Base.serializer ASN1.Spec.Value.BIT_STRING.parse_asn1_bit_string_kind ASN1.Spec.Value.BIT_STRING.parse_asn1_bit_string
let serialize_asn1_bit_string l =
  
serialize_synth ((parse_seq_flbytes l) `parse_filter` (filter_asn1_bit_string l))
  (synth_asn1_bit_string l)
  ((serialize_seq_flbytes l) `serialize_filter` (filter_asn1_bit_string l))
  (synth_asn1_bit_string_inverse l)
  (synth_asn1_bit_string_injective l)