val bytelen (g: group) : n: nat{n <= 127}
val bytelen (g: group) : n: nat{n <= 127}
let bytelen (g:group) : n:nat{n <= 127} =
  match g with
  | EverCrypt.ECC_P256 -> 32
  | EverCrypt.ECC_P384 -> 48
  | EverCrypt.ECC_P521 -> 66
  | EverCrypt.ECC_X25519 -> 32
  | EverCrypt.ECC_X448 -> 56
module MiTLS.ECGroup
open MiTLS

module B = FStar.Bytes
module HST = FStar.HyperStack.ST

type group = EverCrypt.ec_curve
/
prims.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLS.Curve25519.fst.checked MiTLS.EverCrypt.fsti.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.Bytes.fsti.checked
MiTLS.ECGroup.fsti
g: MiTLS.ECGroup.group -> n: Prims.nat{n <= 127}
MiTLS.ECGroup.group Prims.nat Prims.b2t Prims.op_LessThanOrEqual
let bytelen (g: group) : n: nat{n <= 127} =
  
match g with
| EverCrypt.ECC_P256 -> 32
| EverCrypt.ECC_P384 -> 48
| EverCrypt.ECC_P521 -> 66
| EverCrypt.ECC_X25519 -> 32
| EverCrypt.ECC_X448 -> 56