val keygen: Prims.unit
  -> ST keyshare (requires (fun h0 -> True)) (ensures (fun h0 _ h1 -> modifies_none h0 h1))
val keygen: Prims.unit
  -> ST keyshare (requires (fun h0 -> True)) (ensures (fun h0 _ h1 -> modifies_none h0 h1))
let keygen () : ST keyshare
  (requires (fun h0 -> True))
  (ensures (fun h0 _ h1 -> modifies_none h0 h1))
  =
  let s : lbytes 32 = Random.sample32 32ul in
  let base_point = Bytes.create 1ul 9uy @| Bytes.create 31ul 0uy in
  scalarmult s base_point, s
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

let pubshare (k:keyshare) : Tot point = fst k

let scalarmult (secret:Bytes.lbytes 32) (point:Bytes.lbytes 32)
  : ST (lbytes 32)
  (requires (fun h -> True))
  (ensures (fun h0 _ h1 -> modifies_none h0 h1)) =
  push_frame ();
  let lp = B.len point in
  let ls = B.len secret in
  let pb = LB.alloca 0uy lp in
  let sb = LB.alloca 0uy ls in
  let out = LB.alloca 0uy 32ul in
  B.store_bytes point pb;
  B.store_bytes secret sb;
  assume false;
  ignore (EverCrypt.Curve25519.ecdh out sb pb);
  pop_frame (); B.of_buffer 32ul out
/
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
_: Prims.unit -> FStar.HyperStack.ST.ST MiTLS.TLS.Curve25519.keyshare
Prims.unit FStar.Pervasives.Native.Mktuple2 MiTLS.TLS.Curve25519.point MiTLS.TLS.Curve25519.scalar MiTLS.TLS.Curve25519.keyshare MiTLS.TLS.Curve25519.scalarmult FStar.Bytes.lbytes FStar.Bytes.bytes FStar.Bytes.op_At_Bar FStar.Bytes.create FStar.UInt32.__uint_to_t FStar.UInt8.__uint_to_t MiTLS.Random.sample32 FStar.UInt32.v FStar.Monotonic.HyperStack.mem Prims.l_True FStar.HyperStack.ST.modifies_none
let keygen ()
    : ST keyshare (requires (fun h0 -> True)) (ensures (fun h0 _ h1 -> modifies_none h0 h1)) =
  
let s:lbytes 32 = Random.sample32 32ul in
let base_point = Bytes.create 1ul 9uy @| Bytes.create 31ul 0uy in
scalarmult s base_point, s