val ecdh (pk: publickey) (sk: secretkey) : option secretkey
let ecdh (pk:publickey) (sk:secretkey) : option secretkey =
  let shared = Spec.Curve25519.scalarmult sk pk in
  if not (lbytes_eq shared (create 32 (u8 0))) then
    Some shared
  else None
val ecdh (pk: publickey) (sk: secretkey) : option secretkey
let ecdh (pk: publickey) (sk: secretkey) : option secretkey =
let shared = Spec.Curve25519.scalarmult sk pk in
if not (lbytes_eq shared (create 32 (u8 0))) then Some shared else None
Spec.Box.fst.checked
Spec.SecretBox.fst.checked Spec.Salsa20.fst.checked Spec.Curve25519.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Spec.Box.fst
Spec.Box.publickey Spec.Box.secretkey Prims.op_Negation Lib.ByteSequence.lbytes_eq Lib.Sequence.create Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.IntTypes.u8 FStar.Pervasives.Native.Some Prims.bool FStar.Pervasives.Native.None FStar.Pervasives.Native.option Spec.Curve25519.serialized_point Spec.Curve25519.scalarmult
module Spec.Box

open FStar.Mul
open Lib.IntTypes
open Lib.Sequence
open Lib.ByteSequence

open Spec.SecretBox

#set-options "--z3rlimit 20 --max_fuel 0 --max_ifuel 0"

(* Constants *)
let size_publickey = 32 (* in bytes *)
let size_secretkey = 32 (* in bytes *)

type publickey = lbytes size_publickey
type secretkey = lbytes size_secretkey
val ecdh (pk: publickey) (sk: secretkey) : option secretkey
pk: Spec.Box.publickey -> sk: Spec.Box.secretkey
  -> FStar.Pervasives.Native.option Spec.Box.secretkey