val test: DH.group -> St bool
val test: DH.group -> St bool
let test group =
  let initiator_key_and_share = DH.keygen group in
  let gx = DH.ipubshare initiator_key_and_share in
  let gy, gxy = DH.dh_responder group gx in
  let gxy' = DH.dh_initiator group initiator_key_and_share gy in
  let gxy  = hex_of_bytes gxy in
  let gxy' = hex_of_bytes gxy' in
  if gxy = gxy' then true
  else
    begin
      print ("Unexpected output: output = " ^ gxy' ^ "\nexpected = " ^ gxy);
      false
    end
module MiTLS.Test.CommonDH
open MiTLS

open FStar.Bytes
open FStar.Error
open FStar.Printf
open FStar.HyperStack
open FStar.HyperStack.ST

open MiTLS.TLSError
open MiTLS.TLSConstants
open MiTLS.Parsers.NamedGroup
open MiTLS.Parsers.NamedGroupList

module DH = MiTLS.CommonDH

#set-options "--admit_smt_queries true"

let prefix = "Test.CommonDH"

val discard: bool -> ST unit
  (requires (fun _ -> True))
  (ensures (fun h0 _ h1 -> h0 == h1))
let discard _ = ()
let print s = discard (IO.debug_print_string (prefix^": "^s^".\n"))
// let print = C.String,print
// let print = FStar.HyperStack.IO.print_string
/
prims.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Parsers.NamedGroupList.fsti.checked MiTLS.Parsers.NamedGroup.fsti.checked MiTLS.CommonDH.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.fsti.checked FStar.IO.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked C.fst.checked
MiTLS.Test.CommonDH.fst
group: MiTLS.CommonDH.group -> FStar.HyperStack.ST.St Prims.bool
MiTLS.CommonDH.group MiTLS.CommonDH.rshare MiTLS.CommonDH.secret Prims.op_Equality Prims.string Prims.bool Prims.unit MiTLS.Test.CommonDH.print Prims.op_Hat FStar.Bytes.hex_of_bytes MiTLS.CommonDH.dh_initiator FStar.Pervasives.Native.tuple2 MiTLS.CommonDH.dh_responder MiTLS.CommonDH.ishare Prims.eq2 MiTLS.CommonDH.pre_share MiTLS.CommonDH.pre_pubshare MiTLS.CommonDH.ipubshare MiTLS.CommonDH.ikeyshare MiTLS.CommonDH.keygen
let test group =
  
let initiator_key_and_share = DH.keygen group in
let gx = DH.ipubshare initiator_key_and_share in
let gy, gxy = DH.dh_responder group gx in
let gxy' = DH.dh_initiator group initiator_key_and_share gy in
let gxy = hex_of_bytes gxy in
let gxy' = hex_of_bytes gxy' in
if gxy = gxy'
then true
else
  (print ("Unexpected output: output = " ^ gxy' ^ "\nexpected = " ^ gxy);
    false)