val pre_wellformed_id: pre_id -> Type0
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
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.)
///
/
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
_: MiTLS.Idx.pre_id -> Type0
MiTLS.Idx.pre_id MiTLS.Idx.kdfa MiTLS.Idx.id_psk Prims.l_True MiTLS.Idx.label MiTLS.TLSInfo.logInfo MiTLS.Hashing.Spec.anyTag Prims.l_and MiTLS.Idx.pre_wellformed_id MiTLS.Idx.digest_info MiTLS.Idx.ha_of_id MiTLS.Idx.context
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 -> pre_wellformed_id i