val fresh_dhr: #i:dhi -> j:pre_dhr i -> mem -> GTot Type0
val fresh_dhr: #i:dhi -> j:pre_dhr i -> mem -> GTot Type0
let fresh_dhr #i j h =
  (if Flags.model then
    let log: i_ilog = ilog in
    honest_dhi_st log i h
    /\ (let Some (Honest log') = MDM.sel (sel h log) i in
        None? (MDM.sel (sel h log') j))
  else False)
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 ]

let is_ffdhe (ng:namedGroup): Tot bool = List.mem ng [ Ffdhe2048; Ffdhe3072; Ffdhe4096; Ffdhe6144; Ffdhe8192 ]

// let lemma_group_of_namedGroup (ng:namedGroup)
//   : Lemma (Some? (group_of_namedGroup ng) <==> (SEC? ng \/ FFDHE? ng))
//   [SMTPat (group_of_namedGroup ng)]
//   = ()

let default_group = ECDH (EC.ECC_X25519)



noextract
let dh_region = new_region tls_tables_region

noeq type ilog_entry (i:pre_dhi) =
  | Honest of MDM.t dh_region (pre_dhr i) (fun j -> bool) (fun _ -> True)
  | Corrupt

private type i_ilog = MDM.t dh_region pre_dhi ilog_entry (fun _ -> True)
private type ishare_table = (if Flags.model then i_ilog else unit)
let ilog: ishare_table =
  if Flags.model then MDM.alloc () <: i_ilog else ()

type registered_dhi i =
  (if Flags.model then
    let log: i_ilog = ilog in
    witnessed (MDM.defined log i)
  else True)

type fresh_dhi i h =
  (if Flags.model then
    let log: i_ilog = ilog in MDM.fresh log i h
  else False)

type honest_dhi_st (log:i_ilog) (i:pre_dhi) (h:mem) =
  Some? (MDM.sel (sel h log) i) /\ Honest? (Some?.v (MDM.sel (sel h log) i))

let lemma_honest_dhi_stable (log:i_ilog) (i:pre_dhi)
  : Lemma (stable_on_t log (honest_dhi_st log i))
  = admit()

type honest_dhi i =
  (if Flags.model then
    let log: i_ilog = ilog in
    witnessed (honest_dhi_st log i)
  else False)

type corrupt_dhi_st (log:i_ilog) (i:pre_dhi) (h:mem) =
  Some? (MDM.sel (sel h log) i) /\ Corrupt? (Some?.v (MDM.sel (sel h log) i))

let lemma_corrupt_dhi_stable (log:i_ilog) (i:pre_dhi)
  : Lemma (stable_on_t log (corrupt_dhi_st log i))
  = admit()

type corrupt_dhi i =
  (if Flags.model then
    let log: i_ilog = ilog in
    witnessed (corrupt_dhi_st log i)
   else True)

// cwinter: quic2c
// abstract let share_log: share_table =
//   (if Flags.ideal_KEF then
//     MDM.alloc () <: ideal_log
//   else
//     ())

// let registered i =
//   (if Flags.ideal_KEF then
//     let log : ideal_log = share_log in
//     HST.witnessed (MDM.defined log i)
//   else
//     True)

// let honest_share i =
//   (if Flags.ideal_KEF then
//     let log : ideal_log = share_log in
//     HST.witnessed (MDM.contains log i true)
//   else False)

// let dishonest_share i =
//   (if Flags.ideal_KEF then
//     let log : ideal_log = share_log in
//     HST.witnessed (MDM.contains log i false)
//   else True)

let lemma_honest_corrupt (i:pre_dhi{registered_dhi i})
  : Lemma (honest_dhi i <==> ~(corrupt_dhi i))
  = admit()

let is_honest_dhi i =
  if Flags.model then
    let log: i_ilog = ilog in
    recall log;
    testify (MDM.defined log i);
    lemma_honest_corrupt i;
    match MDM.lookup log i with
    | Some (Corrupt) ->
      lemma_corrupt_dhi_stable log i;
      mr_witness log (corrupt_dhi_st log i);
      false
    | Some (Honest _) ->
      lemma_honest_dhi_stable log i;
      mr_witness log (honest_dhi_st log i);
      true
  else false

let ipubshare #g gx = pre_pubshare gx

let registered_dhr_st (#i:dhi) (log:i_ilog) (j:pre_dhr i) (h:mem) =
  corrupt_dhi_st log i h \/
  (honest_dhi_st log i h /\
    (let Some (Honest log') = MDM.sel (sel h log) i in
      Some? (MDM.sel (sel h log') j)))

let registered_dhr #i j =
  (if Flags.model then
    let log: i_ilog = ilog in
    witnessed (registered_dhr_st log j)
  else True)
/
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
j: MiTLS.CommonDH.pre_dhr i -> h: FStar.Monotonic.HyperStack.mem -> Prims.GTot Type0
MiTLS.CommonDH.dhi MiTLS.CommonDH.pre_dhr FStar.Monotonic.HyperStack.mem MiTLS.Flags.model Prims.l_and MiTLS.CommonDH.honest_dhi_st FStar.Monotonic.DependentMap.t MiTLS.CommonDH.dh_region Prims.bool FStar.DependentMap.t FStar.Monotonic.DependentMap.opt Prims.l_True Prims.b2t FStar.Pervasives.Native.uu___is_None FStar.Monotonic.DependentMap.sel FStar.Monotonic.HyperStack.sel FStar.Monotonic.DependentMap.imap FStar.Monotonic.DependentMap.grows Prims.logical FStar.Pervasives.Native.option MiTLS.CommonDH.ilog_entry MiTLS.CommonDH.pre_dhi MiTLS.CommonDH.i_ilog MiTLS.CommonDH.ilog Prims.l_False
let fresh_dhr #i j h =
  
(if Flags.model
  then
    let log:i_ilog = ilog in
    honest_dhi_st log i h /\
    (let Some (Honest log') = MDM.sel (sel h log) i in
      None? (MDM.sel (sel h log') j))
  else False)