val is_ffdhe (ng: namedGroup) : Tot bool
val is_ffdhe (ng: namedGroup) : Tot bool
let is_ffdhe (ng:namedGroup): Tot bool = List.mem ng [ Ffdhe2048; Ffdhe3072; Ffdhe4096; Ffdhe6144; Ffdhe8192 ]
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)) = ()
let print s = discard (IO.debug_print_string ("CDH| "^s^"\n"))
unfold let dbg : string -> ST unit (requires (fun _ -> True))
  (ensures (fun h0 _ h1 -> h0 == h1)) =
  if DebugFlags.debug_CDH then print else (fun _ -> ())

type group' =
  | FFDH of DHGroup.group
  | ECDH of ECGroup.group

let group = group'
let is_ec g = ECDH? g

#set-options "--z3rlimit 100"
let string_of_group = function
  | FFDH g ->
    begin
    let open MiTLS.DHGroup in
    match g with
    | Named FFDHE2048 -> "FFDHE2048"
    | Named FFDHE3072 -> "FFDHE3072"
    | Named FFDHE4096 -> "FFDHE4096"
    | Named FFDHE6144 -> "FFDHE6144"
    | Named FFDHE8192 -> "FFDHE8192"
    | Explicit _      -> "Explicit group"
    end
  | ECDH g ->
    begin
    match g with
    | EC.ECC_P256    -> "P256"
    | EC.ECC_P384    -> "P384"
    | EC.ECC_P521    -> "P521"
    | EC.ECC_X25519  -> "X255519"
    | EC.ECC_X448    -> "X448"
    end

private type pre_keyshare' =
  | KS_FF: g:DHGroup.group -> DHGroup.keyshare g -> pre_keyshare'
  | KS_EC: g:ECGroup.group -> ECGroup.keyshare g -> pre_keyshare'

let pre_keyshare (g:group) =
  ks:pre_keyshare'{(match g with
  | FFDH dhg -> KS_FF? ks /\ KS_FF?.g ks = dhg
  | ECDH ecg -> KS_EC? ks /\ KS_EC?.g ks = ecg)}

private type pre_share' =
  | S_FF: g:DHGroup.group -> DHGroup.share g -> pre_share'
  | S_EC: g:ECGroup.group -> ECGroup.share g -> pre_share'

let pre_share (g:group) =
  s:pre_share'{(match g with
  | FFDH dhg -> S_FF? s /\ S_FF?.g s = dhg
  | ECDH ecg -> S_EC? s /\ S_EC?.g s = ecg)}

let pre_pubshare #g ks =
  match g with
  | FFDH dhg -> let KS_FF _ ks = ks in S_FF dhg (DHGroup.pubshare #dhg ks)
  | ECDH ecg -> let KS_EC _ ks = ks in S_EC ecg (ECGroup.pubshare #ecg ks)

let namedGroup_of_group (g:group): Tot (option namedGroup) =
  match g with
  | ECDH EC.ECC_P256 -> Some Secp256r1
  | ECDH EC.ECC_P384 -> Some Secp384r1
  | ECDH EC.ECC_P521 -> Some Secp521r1
  | ECDH EC.ECC_X25519 -> Some X25519
  | ECDH EC.ECC_X448 -> Some X448
  | FFDH (DHGroup.Named DHGroup.FFDHE2048) -> Some Ffdhe2048
  | FFDH (DHGroup.Named DHGroup.FFDHE3072) -> Some Ffdhe3072
  | FFDH (DHGroup.Named DHGroup.FFDHE4096) -> Some Ffdhe4096
  | FFDH (DHGroup.Named DHGroup.FFDHE6144) -> Some Ffdhe6144
  | FFDH (DHGroup.Named DHGroup.FFDHE8192) -> Some Ffdhe8192
  | _ -> None

let lemma_namedGroup_of_group (g:group)
  : Lemma (Some? (namedGroup_of_group g) <==> (ECDH? g \/ (FFDH? g /\ DHGroup.Named? (FFDH?._0 g))))
  [SMTPat (namedGroup_of_group g)]
  = ()

let group_of_namedGroup (ng:namedGroup): Tot (option group) =
  match ng with
  | Secp256r1 -> Some (ECDH EC.ECC_P256)
  | Secp384r1 -> Some (ECDH EC.ECC_P384)
  | Secp521r1 -> Some (ECDH EC.ECC_P521)
  | X25519    -> Some (ECDH EC.ECC_X25519)
  | X448      -> Some (ECDH EC.ECC_X448)
  | Ffdhe2048 -> Some (FFDH (DHGroup.Named DHGroup.FFDHE2048))
  | Ffdhe3072 -> Some (FFDH (DHGroup.Named DHGroup.FFDHE3072))
  | Ffdhe4096 -> Some (FFDH (DHGroup.Named DHGroup.FFDHE4096))
  | Ffdhe6144 -> Some (FFDH (DHGroup.Named DHGroup.FFDHE6144))
  | Ffdhe8192 -> Some (FFDH (DHGroup.Named DHGroup.FFDHE8192))
  | _         -> None

let is_ecdhe (ng:namedGroup): Tot bool = List.mem ng [ Secp256r1; Secp384r1; Secp521r1; X25519; X448 ]
/
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
ng: MiTLS.Parsers.NamedGroup.namedGroup -> Prims.bool
MiTLS.Parsers.NamedGroup.namedGroup FStar.List.Tot.Base.mem Prims.Cons MiTLS.Parsers.NamedGroup.Ffdhe2048 MiTLS.Parsers.NamedGroup.Ffdhe3072 MiTLS.Parsers.NamedGroup.Ffdhe4096 MiTLS.Parsers.NamedGroup.Ffdhe6144 MiTLS.Parsers.NamedGroup.Ffdhe8192 Prims.Nil Prims.bool
let is_ffdhe (ng: namedGroup) : Tot bool =
  
List.mem ng [Ffdhe2048; Ffdhe3072; Ffdhe4096; Ffdhe6144; Ffdhe8192]