val known_cipherSuite_repr (v: U16.t) : bool
val known_cipherSuite_repr (v: U16.t) : bool
let known_cipherSuite_repr (v:U16.t) : bool = v `cipherSuite_repr_eq` 0us || (v `cipherSuite_repr_eq` 1us || (v `cipherSuite_repr_eq` 2us || (v `cipherSuite_repr_eq` 4us || (v `cipherSuite_repr_eq` 5us || (v `cipherSuite_repr_eq` 10us || (v `cipherSuite_repr_eq` 19us || (v `cipherSuite_repr_eq` 22us || (v `cipherSuite_repr_eq` 24us || (v `cipherSuite_repr_eq` 27us || (v `cipherSuite_repr_eq` 47us || (v `cipherSuite_repr_eq` 50us || (v `cipherSuite_repr_eq` 51us || (v `cipherSuite_repr_eq` 52us || (v `cipherSuite_repr_eq` 53us || (v `cipherSuite_repr_eq` 56us || (v `cipherSuite_repr_eq` 57us || (v `cipherSuite_repr_eq` 58us || (v `cipherSuite_repr_eq` 59us || (v `cipherSuite_repr_eq` 60us || (v `cipherSuite_repr_eq` 61us || (v `cipherSuite_repr_eq` 64us || (v `cipherSuite_repr_eq` 103us || (v `cipherSuite_repr_eq` 106us || (v `cipherSuite_repr_eq` 107us || (v `cipherSuite_repr_eq` 108us || (v `cipherSuite_repr_eq` 109us || (v `cipherSuite_repr_eq` 156us || (v `cipherSuite_repr_eq` 157us || (v `cipherSuite_repr_eq` 158us || (v `cipherSuite_repr_eq` 159us || (v `cipherSuite_repr_eq` 160us || (v `cipherSuite_repr_eq` 161us || (v `cipherSuite_repr_eq` 162us || (v `cipherSuite_repr_eq` 163us || (v `cipherSuite_repr_eq` 164us || (v `cipherSuite_repr_eq` 165us || (v `cipherSuite_repr_eq` 166us || (v `cipherSuite_repr_eq` 167us || (v `cipherSuite_repr_eq` 4865us || (v `cipherSuite_repr_eq` 4866us || (v `cipherSuite_repr_eq` 4867us || (v `cipherSuite_repr_eq` 4868us || (v `cipherSuite_repr_eq` 4869us || (v `cipherSuite_repr_eq` 49169us || (v `cipherSuite_repr_eq` 49170us || (v `cipherSuite_repr_eq` 49171us || (v `cipherSuite_repr_eq` 49172us || (v `cipherSuite_repr_eq` 49191us || (v `cipherSuite_repr_eq` 49192us || (v `cipherSuite_repr_eq` 49195us || (v `cipherSuite_repr_eq` 49196us || (v `cipherSuite_repr_eq` 49199us || (v `cipherSuite_repr_eq` 49200us || (v `cipherSuite_repr_eq` 52392us || (v `cipherSuite_repr_eq` 52393us || (v `cipherSuite_repr_eq` 52394us || (v `cipherSuite_repr_eq` 52395us || (v `cipherSuite_repr_eq` 52396us || (v `cipherSuite_repr_eq` 52397us || (false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
module MiTLS.Parsers.CipherSuite

(* This file has been automatically generated by EverParse. *)
open FStar.Bytes
module U8 = FStar.UInt8
module U16 = FStar.UInt16
module U32 = FStar.UInt32
module U64 = FStar.UInt64
module LP = LowParse.Spec.Base
module LS = LowParse.SLow.Base
module LSZ = LowParse.SLow.Base
module LPI = LowParse.Spec.AllIntegers
module LL = LowParse.Low.Base
module L = FStar.List.Tot
module B = LowStar.Buffer
module BY = FStar.Bytes
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST


let cipherSuite_repr = U16.t
/
prims.fst.checked LowStar.Buffer.fst.checked LowParse.Spec.Base.fsti.checked LowParse.Spec.AllIntegers.fst.checked LowParse.SLow.Base.fst.checked LowParse.Low.Base.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Bytes.fsti.checked
MiTLS.Parsers.CipherSuite.fsti
v: FStar.UInt16.t -> Prims.bool
FStar.UInt16.t Prims.op_BarBar MiTLS.Parsers.CipherSuite.cipherSuite_repr_eq FStar.UInt16.__uint_to_t Prims.bool
let known_cipherSuite_repr (v: U16.t) : bool =
  
v
`cipherSuite_repr_eq`
0us ||
(v
  `cipherSuite_repr_eq`
  1us ||
  (v
    `cipherSuite_repr_eq`
    2us ||
    (v
      `cipherSuite_repr_eq`
      4us ||
      (v
        `cipherSuite_repr_eq`
        5us ||
        (v
          `cipherSuite_repr_eq`
          10us ||
          (v
            `cipherSuite_repr_eq`
            19us ||
            (v
              `cipherSuite_repr_eq`
              22us ||
              (v
                `cipherSuite_repr_eq`
                24us ||
                (v
                  `cipherSuite_repr_eq`
                  27us ||
                  (v
                    `cipherSuite_repr_eq`
                    47us ||
                    (v
                      `cipherSuite_repr_eq`
                      50us ||
                      (v
                        `cipherSuite_repr_eq`
                        51us ||
                        (v
                          `cipherSuite_repr_eq`
                          52us ||
                          (v
                            `cipherSuite_repr_eq`
                            53us ||
                            (v
                              `cipherSuite_repr_eq`
                              56us ||
                              (v
                                `cipherSuite_repr_eq`
                                57us ||
                                (v
                                  `cipherSuite_repr_eq`
                                  58us ||
                                  (v
                                    `cipherSuite_repr_eq`
                                    59us ||
                                    (v
                                      `cipherSuite_repr_eq`
                                      60us ||
                                      (v
                                        `cipherSuite_repr_eq`
                                        61us ||
                                        (v
                                          `cipherSuite_repr_eq`
                                          64us ||
                                          (v
                                            `cipherSuite_repr_eq`
                                            103us ||
                                            (v
                                              `cipherSuite_repr_eq`
                                              106us ||
                                              (v
                                                `cipherSuite_repr_eq`
                                                107us ||
                                                (v
                                                  `cipherSuite_repr_eq`
                                                  108us ||
                                                  (v
                                                    `cipherSuite_repr_eq`
                                                    109us ||
                                                    (v
                                                      `cipherSuite_repr_eq`
                                                      156us ||
                                                      (v
                                                        `cipherSuite_repr_eq`
                                                        157us ||
                                                        (v
                                                          `cipherSuite_repr_eq`
                                                          158us ||
                                                          (v
                                                            `cipherSuite_repr_eq`
                                                            159us ||
                                                            (v
                                                              `cipherSuite_repr_eq`
                                                              160us ||
                                                              (v
                                                                `cipherSuite_repr_eq`
                                                                161us ||
                                                                (v
                                                                  `cipherSuite_repr_eq`
                                                                  162us ||
                                                                  (v
                                                                    `cipherSuite_repr_eq`
                                                                    163us ||
                                                                    (v
                                                                      `cipherSuite_repr_eq`
                                                                      164us ||
                                                                      (v
                                                                        `cipherSuite_repr_eq`
                                                                        165us ||
                                                                        (v
                                                                          `cipherSuite_repr_eq`
                                                                          166us ||
                                                                          (v
                                                                            `cipherSuite_repr_eq`
                                                                            167us ||
                                                                            (v
                                                                              `cipherSuite_repr_eq`
                                                                              4865us ||
                                                                              (v
                                                                                `cipherSuite_repr_eq`
                                                                                4866us ||
                                                                                (v
                                                                                  `cipherSuite_repr_eq`
                                                                                  4867us ||
                                                                                  (v
                                                                                    `cipherSuite_repr_eq`
                                                                                    4868us ||
                                                                                    (v
                                                                                      `cipherSuite_repr_eq`
                                                                                      4869us ||
                                                                                      (v
                                                                                        `cipherSuite_repr_eq`
                                                                                        49169us ||
                                                                                        (v
                                                                                          `cipherSuite_repr_eq`
                                                                                          49170us ||
                                                                                          (v
                                                                                            `cipherSuite_repr_eq`
                                                                                            49171us ||
                                                                                            (v
                                                                                              `cipherSuite_repr_eq`
                                                                                              49172us ||
                                                                                              (v
                                                                                                `cipherSuite_repr_eq`
                                                                                                49191us ||
                                                                                                (v
                                                                                                  `cipherSuite_repr_eq`
                                                                                                  49192us ||
                                                                                                  (v
                                                                                                    `cipherSuite_repr_eq`
                                                                                                    49195us ||
                                                                                                    (
                                                                                                      v
                                                                                                      `cipherSuite_repr_eq`
                                                                                                      49196us ||
                                                                                                      (
                                                                                                        v
                                                                                                        `cipherSuite_repr_eq`
                                                                                                        49199us ||
                                                                                                        (
                                                                                                          v
                                                                                                          `cipherSuite_repr_eq`
                                                                                                          49200us ||
                                                                                                          (
                                                                                                            v
                                                                                                            `cipherSuite_repr_eq`
                                                                                                            52392us ||
                                                                                                            (
                                                                                                              v
                                                                                                              `cipherSuite_repr_eq`
                                                                                                              52393us ||
                                                                                                              (
                                                                                                                v
                                                                                                                `cipherSuite_repr_eq`
                                                                                                                52394us ||
                                                                                                                (
                                                                                                                  v
                                                                                                                  `cipherSuite_repr_eq`
                                                                                                                  52395us ||
                                                                                                                  (
                                                                                                                    v
                                                                                                                    `cipherSuite_repr_eq`
                                                                                                                    52396us ||
                                                                                                                    (
                                                                                                                      v
                                                                                                                      `cipherSuite_repr_eq`
                                                                                                                      52397us ||
                                                                                                                      (
                                                                                                                        false
                                                                                                                      )
                                                                                                                    )
                                                                                                                  )
                                                                                                                )
                                                                                                              )
                                                                                                            )
                                                                                                          )
                                                                                                        )
                                                                                                      )
                                                                                                    )
                                                                                                  ))
                                                                                              ))))))
                                                                                  ))))))))))))))))))
                                              ))))))))))))))))))))))))