val pubshare: #g:group -> keyshare g -> Tot (share g)
val pubshare: #g:group -> keyshare g -> Tot (share g)
let pubshare #g k =
  match k with
  | KS_CC p _ -> S_CC p
  | KS_X25519 k -> S_X25519 (TLS.Curve25519.pubshare k)
  | KS_X448 p _ -> S_X448 p
module MiTLS.ECGroup
open MiTLS

open FStar.Error
open MiTLS.TLSError
open MiTLS.Mem
module Parse = MiTLS.Parse
open MiTLS.Parse

module B = FStar.Bytes
module LB = LowStar.Buffer
module EC = MiTLS.EverCrypt
module LP = LowParse.SLow.Base

type ec_all_curve =
  | EC_CORE of group
  | EC_UNKNOWN of (n:nat{B.repr_bytes n <= 2})
  | EC_EXPLICIT_PRIME
  | EC_EXPLICIT_BINARY

// FIXME eqtype is a lie but the idealization needs equality of keyshares
let _key g = assume false; EC.ecdh_state
/
prims.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLS.Curve25519.fst.checked MiTLS.Random.fst.checked MiTLS.Parsers.NamedGroup.fsti.checked MiTLS.Parsers.ECCurveType.fsti.checked MiTLS.Parse.fst.checked MiTLS.Mem.fst.checked MiTLS.Format.UncompressedPointRepresentation.fsti.checked MiTLS.EverCrypt.fsti.checked LowStar.Buffer.fst.checked LowParse.SLow.Base.fst.checked LowParse.SLow.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.ECGroup.fst
k: MiTLS.ECGroup.keyshare g -> MiTLS.ECGroup.share g
MiTLS.ECGroup.group MiTLS.ECGroup.keyshare MiTLS.ECGroup.point MiTLS.ECGroup._key MiTLS.ECGroup.S_CC MiTLS.TLS.Curve25519.keyshare MiTLS.ECGroup.S_X25519 MiTLS.TLS.Curve25519.pubshare FStar.Bytes.lbytes MiTLS.ECGroup.S_X448 MiTLS.ECGroup.share
let pubshare #g k =
  
match k with
| KS_CC p _ -> S_CC p
| KS_X25519 k -> S_X25519 (TLS.Curve25519.pubshare k)
| KS_X448 p _ -> S_X448 p