val len_of_asn1_boolean (b: bool)
    : Tot (l: size_t{v l == Seq.length (serialize serialize_asn1_boolean b) /\ v l == 1})
val len_of_asn1_boolean (b: bool)
    : Tot (l: size_t{v l == Seq.length (serialize serialize_asn1_boolean b) /\ v l == 1})
let len_of_asn1_boolean
  (b: bool)
: Tot (l: size_t{
  v l == Seq.length (serialize serialize_asn1_boolean b) /\
  v l == 1})
= lemma_serialize_asn1_boolean_unfold b;
  lemma_serialize_asn1_boolean_size b;
  1ul
module ASN1.Low.Value.BOOLEAN
///
/// ASN.1 Low
///
open LowParse.Low.Base
open LowParse.Low.Combinators
open LowParse.Low.Int

open ASN1.Base
open ASN1.Spec.Value.BOOLEAN
open ASN1.Low.Base

module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module B = LowStar.Buffer
open FStar.Integers

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

friend ASN1.Spec.Value.BOOLEAN

///
/// Encoding a tag into bytes at low-level, implementation of `synth_..._inverse`

///
inline_for_extraction
let encode_asn1_boolean
  (x: bool)
: Tot (b: byte{b == synth_asn1_boolean_inverse x})
= match x with
  | true  -> 0xFFuy
  | false -> 0x00uy

///
/// Low-level function to be used to compute the length of a value's serialization
///
/
prims.fst.checked LowStar.Buffer.fst.checked LowParse.Low.Int.fsti.checked LowParse.Low.Combinators.fsti.checked LowParse.Low.Base.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked ASN1.Spec.Value.BOOLEAN.fst.checked ASN1.Spec.Value.BOOLEAN.fst.checked ASN1.Spec.Tag.fsti.checked ASN1.Spec.Length.fsti.checked ASN1.Low.Tag.fsti.checked ASN1.Low.Length.fsti.checked ASN1.Low.Base.fst.checked ASN1.Base.fst.checked
ASN1.Low.Value.BOOLEAN.fst
b: Prims.bool
  -> l:
    ASN1.Low.Base.size_t
      { FStar.Integers.v l ==
        FStar.Seq.Base.length (LowParse.Spec.Base.serialize ASN1.Spec.Value.BOOLEAN.serialize_asn1_boolean
              b) /\ FStar.Integers.v l == 1 }
Prims.bool FStar.UInt32.__uint_to_t Prims.unit ASN1.Spec.Value.BOOLEAN.lemma_serialize_asn1_boolean_size ASN1.Spec.Value.BOOLEAN.lemma_serialize_asn1_boolean_unfold ASN1.Low.Base.size_t Prims.l_and Prims.eq2 Prims.int Prims.l_or Prims.b2t Prims.op_GreaterThanOrEqual FStar.Integers.within_bounds FStar.Integers.Unsigned FStar.Integers.W32 FStar.Integers.v FStar.Seq.Base.length LowParse.Bytes.byte LowParse.Spec.Base.serialize ASN1.Spec.Value.BOOLEAN.parse_asn1_boolean_kind ASN1.Base.datatype_of_asn1_type ASN1.Base.BOOLEAN ASN1.Spec.Value.BOOLEAN.parse_asn1_boolean ASN1.Spec.Value.BOOLEAN.serialize_asn1_boolean
let len_of_asn1_boolean (b: bool)
    : Tot (l: size_t{v l == Seq.length (serialize serialize_asn1_boolean b) /\ v l == 1}) =
  
lemma_serialize_asn1_boolean_unfold b;
lemma_serialize_asn1_boolean_size b;
1ul