val pubshare (k: keyshare) : Tot point
val pubshare (k: keyshare) : Tot point
let pubshare (k:keyshare) : Tot point = fst k
module MiTLS.TLS.Curve25519
open MiTLS

open FStar.Bytes
open FStar.Error

open FStar.HyperStack.ST

module B = FStar.Bytes
module LB = LowStar.Buffer

type scalar = lbytes 32
type point = lbytes 32
type keyshare = point * scalar
/
prims.fst.checked MiTLS.Random.fst.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked EverCrypt.Curve25519.fsti.checked
MiTLS.TLS.Curve25519.fst
k: MiTLS.TLS.Curve25519.keyshare -> MiTLS.TLS.Curve25519.point
MiTLS.TLS.Curve25519.keyshare FStar.Pervasives.Native.fst MiTLS.TLS.Curve25519.point MiTLS.TLS.Curve25519.scalar
let pubshare (k: keyshare) : Tot point =
  
fst k