val dbg: string -> ST unit (requires (fun _ -> True)) (ensures (fun h0 _ h1 -> h0 == h1))
val dbg: string -> ST unit (requires (fun _ -> True)) (ensures (fun h0 _ h1 -> h0 == h1))
let dbg : string -> ST unit (requires (fun _ -> True))
  (ensures (fun h0 _ h1 -> h0 == h1)) =
  if DebugFlags.debug_CDH then print else (fun _ -> ())
module MiTLS.CommonDH
open MiTLS

(**
An abstract interface for Diffie-Hellman operations

When the key extraction stack is idealized (Flag.model), this module
records the honesty of shares using two layers of types: pre_share
is for syntactically valid shares (used in parsing modules) while
share is for registered shares (for which is_honest is defined).
*)

open FStar.Bytes
open FStar.Error

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

module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module MDM = FStar.Monotonic.DependentMap
module DM = FStar.DependentMap
module EC = MiTLS.EverCrypt

(* A flag for runtime debugging of cDH data.
   The F* normalizer will erase debug prints at extraction
   when this flag is set to false. *)
let discard (b:bool): ST unit (requires (fun _ -> True))
 (ensures (fun h0 _ h1 -> h0 == h1)) = ()
/
prims.fst.checked MiTLS.TLSError.fst.checked MiTLS.Parsers.NamedGroup.fsti.checked MiTLS.Parse.fst.checked MiTLS.Mem.fst.checked MiTLS.Format.KeyShareEntry.fsti.checked MiTLS.Flags.fst.checked MiTLS.EverCrypt.fsti.checked MiTLS.ECGroup.fsti.checked MiTLS.DHGroup.fsti.checked MiTLS.DebugFlags.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.DependentMap.fsti.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.IO.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Error.fst.checked FStar.DependentMap.fsti.checked FStar.Bytes.fsti.checked
MiTLS.CommonDH.fst
_: Prims.string -> FStar.HyperStack.ST.ST Prims.unit
MiTLS.DebugFlags.debug_CDH MiTLS.CommonDH.print Prims.bool Prims.string Prims.unit FStar.Monotonic.HyperStack.mem Prims.l_True Prims.eq2
let dbg: string -> ST unit (requires (fun _ -> True)) (ensures (fun h0 _ h1 -> h0 == h1)) =
  
if DebugFlags.debug_CDH then print else (fun _ -> ())