val h_table : Type0
let h_table = if model then i_honesty_table else unit
module MiTLS.Idx
open MiTLS

open MiTLS.Mem
//open Pkg

module DM = FStar.DependentMap
module MDM = FStar.Monotonic.DependentMap

type info = TLSInfo.logInfo

// 17-12-08 we considered separating "honesty" from the more ad hoc parts of this file.

/// TLS-SPECIFIC KEY INDICES
/// --------------------------------------------------------------------------------------------------
///
/// We provide an instance of ipkg to track key derivation (here using constant labels)
/// these labels are specific to HKDF, for now strings e.g. "e exp master".
type label = s:string{Bytes.length (Bytes.bytes_of_string s) < 250}

/// the middle extraction takes an optional DH secret, identified by this triple
/// we use our own datatype to simplify typechecking
type id_dhe =
  | NoIDH
  | IDH:
    gX: CommonDH.dhi ->
    gY: CommonDH.dhr gX -> id_dhe

// The "ciphersuite hash algorithms" eligible for TLS 1.3 key derivation.
// We will be more restrictive.
type kdfa = a:EverCrypt.HMAC.supported_alg { Spec.Hash.Definitions.is_md a }

/// Runtime key-derivation parameters, to be adjusted.
///
/// HKDF defines an injective function from label * context to bytes, to be used as KDF indexes.
///
type context =
  | Extract: context // TLS extractions have no label and no context; we may separate Extract0 and Extract2
  | ExtractDH: v:id_dhe -> context // This is Extract1 (the middle extraction)
  | Expand: context // TLS expansion with default hash value
  | ExpandLog: // TLS expansion using hash of the handshake log
    info: TLSInfo.logInfo (* ghost, abstract summary of the transcript *) ->
    hv: Hashing.Spec.anyTag (* requires stratification *) -> context
// 18-09-25 should info be HandshakeLog.hs_transcript? 


/// Underneath, HKDF takes a "context" and a required length, with
/// disjoint internal encodings of the context:
/// [HKDF.format #ha label digest len]

type id_psk = nat // external application PSKs only; we may also set the usage's maximal recursive depth here.

// The `[@ Gc]` attribute instructs KaRaMeL to translate the `pre_id` field as a pointer,
// otherwise it would generate an invalid type definition.
[@ Gc]
type pre_id =
  | Preshared:
      a: kdfa (* fixing the hash algorithm *) ->
      id_psk  ->
      pre_id
  | Derive:
      i:pre_id (* parent index *) ->
      l:label (* static part of the derivation label *) ->
      context (* dynamic part of the derivation label *) ->
      pre_id

// always bound by the index (and also passed concretely at creation-time).
val ha_of_id: i:pre_id -> kdfa
let rec ha_of_id = function
  | Preshared a _ -> a
  | Derive i lbl ctx -> ha_of_id i

// placeholders
assume val idh_of_log: TLSInfo.logInfo -> id_dhe
assume val summary: Bytes.bytes -> TLSInfo.logInfo

// concrete transcript digest
let digest_info (a:kdfa) (info:TLSInfo.logInfo) (hv: Hashing.Spec.anyTag) =
  exists (transcript: Hashing.hashable a).
    // Bytes.length hv = hash_len a /\
    hv = Hashing.h a transcript /\
    Hashing.CRF.hashed a transcript /\
    info = summary transcript

/// stratified definition of id required.
///
/// we will enforce
/// * consistency on the hash algorithm
/// * monotonicity of the log infos (recursively including earlier resumption logs).
/// * usage restriction: the log after DH must include the DH identifier of the parent.
///   (Hence, we should either forbid successive DHs or authenticate them all.)
///
val pre_wellformed_id: pre_id -> Type0
let rec pre_wellformed_id = function
  | Preshared a _ -> True
  | Derive i l (ExpandLog info hv) -> pre_wellformed_id i /\ digest_info (ha_of_id i) info hv
  | Derive i lbl ctx ->
      //TODO "ctx either extends the parent's, or includes its idh" /\
      pre_wellformed_id i

/// Indexes are used concretely in model code, so we
/// erase them conditionally on model
type id = 
  (if model then i:pre_id {pre_wellformed_id i}
  else unit)

unfold type wellformed_id (i:id) =
  (if model then pre_wellformed_id i else True)

unfold let wellformed_derive (i:id) (l:label) (ctx:context) =
  (if model then pre_wellformed_id (Derive i l ctx) else True)

unfold let derive (i:id) (l:label) (ctx:context{wellformed_derive i l ctx}) : id =
  (if model then Derive i l ctx else ())

type honest_idh (c:context) =
  ExtractDH? c /\ IDH? (ExtractDH?.v c) /\
  (let ExtractDH (IDH gX gY) = c in CommonDH.honest_dhr gY)

/// We use a global honesty table for all indexes. Inside ipkg, we
/// assume all index types are defined in the table below. We assume
/// write access to this table is public, but the following global
/// invariant must be enforced: if i is corrupt then all indexes
/// derived from i are also corrupt
/// ---EXCEPT if ctx is ExtractDH g gx gy with CommonDH.honest_dhr gy
///
type honesty_invariant (m:DM.t id (MDM.opt (fun _ -> bool))) =
  (forall (i:id) (l:label) (c:context{wellformed_derive i l c}).
  {:pattern (DM.sel m (Derive i l c))}
  Some? (DM.sel m (derive i l c)) ==> Some? (DM.sel m i) /\
  (DM.sel m i = Some false ==> (honest_idh c \/ DM.sel m (derive i l c) = Some false)))

//17-12-08 removed [private] twice, as we need to recall it in ODH :(
type i_honesty_table =
/
Spec.Hash.Definitions.fst.checked prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.Pkg.fst.checked MiTLS.Mem.fst.checked MiTLS.Hashing.Spec.fst.checked MiTLS.Hashing.CRF.fsti.checked MiTLS.Hashing.fsti.checked MiTLS.CommonDH.fsti.checked FStar.Squash.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.DependentMap.fsti.checked FStar.DependentMap.fsti.checked FStar.Bytes.fsti.checked EverCrypt.HMAC.fsti.checked
MiTLS.Idx.fst
Type0
MiTLS.Mem.model MiTLS.Idx.i_honesty_table Prims.bool Prims.unit
let h_table =
  
if model then i_honesty_table else unit