val trivial : _: FStar.Bytes.bytes -> Prims.logical
let trivial (_: bytes) = True
module MiTLS.Old.KeySchedule
open MiTLS

open FStar.Heap
open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Seq
open FStar.Bytes
open FStar.Error
//open FStar.Integers 

open MiTLS.TLSError
open MiTLS.TLSConstants
open MiTLS.Extensions
open MiTLS.TLSInfo
open MiTLS.Range
open MiTLS.StatefulLHAE
open MiTLS.HKDF
open MiTLS.PSK

module MDM = FStar.Monotonic.DependentMap
module HS = FStar.HyperStack
module ST = FStar.HyperStack.ST
module H = MiTLS.Hashing.Spec

module HMAC_UFCMA = MiTLS.Old.HMAC.UFCMA

type finishedId = HMAC_UFCMA.finishedId

(* A flag for runtime debugging of computed keys.
   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 ("KS | "^s^"\n"))
unfold let dbg : string -> ST unit (requires (fun _ -> True))
  (ensures (fun h0 _ h1 -> h0 == h1)) =
  if DebugFlags.debug_KS then print else (fun _ -> ())

#set-options "--admit_smt_queries true"

let print_share (#g:CommonDH.group) (s:CommonDH.share g) : ST unit
  (requires (fun h0 -> True))
  (ensures (fun h0 _ h1 -> modifies_none h0 h1))
  =
  let kb = CommonDH.serialize_raw #g s in
  let kh = FStar.Bytes.hex_of_bytes kb in
  dbg ("Share: "^kh)

(********************************************
*    Resumption PSK is disabled for now     *
*********************************************

abstract type res_psk (i:rmsId) =
  b:bytes{exists i.{:pattern index b i} index b i <> 0z}

abstract type res_context (i:rmsId) =
  b:bytes{length b = CoreCrypto.H.hash_len (rmsId_hash i)}

private type res_psk_entry (i:rmsId) =
  (res_psk i) * (res_context i) * ctx:psk_context * leaked:(rref tls_tables_region bool)

let res_psk_injective (m:MDM.map' rmsId res_psk_entry) =
  forall i1 i2.{:pattern (MDM.sel m i1); (MDM.sel m i2)}
       i1 = i2 <==> (match MDM.sel m i1, MDM.sel m i2 with
                  | Some (psk1, _, _, _), Some (psk2, _, _, _) -> b2t (equalBytes psk1 psk2)
                  | _ -> True)

let res_psk_table : MDM.t tls_tables_region rmsId res_psk_entry res_psk_injective =
  MDM.alloc #TLSConstants.tls_tables_region #rmsId #res_psk_entry #res_psk_injective

let registered_res_psk (i:rmsId) (h:HH.t) =
  b2t (Some? (MDM.sel (HS.sel h res_psk_table) i))

let res_psk_context (i:rmsId{registered_res_psk i}) =
  let (_, _, c, _) = Some.v (MDM.sel res_psk_table i) in c

private let res_psk_value (i:rmsId{registered_res_psk i}) =
  let (psk, _, _, _) = Some.v (MDM.sel res_psk_table i) in psk

**)

// PSK (internal/external multiplex, abstract)
// Note that application PSK is externally defined but should
// be idealized together with KS
val psk (i:esId) : Type0

let read_psk (i:PSK.pskid)
  : ST (esId * pskInfo * PSK.app_psk i)
  (requires fun h -> True)
  (ensures fun h0 _ h1 -> modifies_none h0 h1)
  =
  let c = PSK.psk_info i in
  let id =
    if Some? c.ticket_nonce then
      let (| li, rmsid |) = Ticket.dummy_rmsid c.early_ae c.early_hash in
      ResumptionPSK #li rmsid
    else
      ApplicationPSK #(c.early_hash) #(c.early_ae) i
    in
  (id, c, PSK.psk_value i)

type binderId = i:pre_binderId{valid (I_BINDER i)}
type hsId = i:TLSInfo.pre_hsId{valid (I_HS i)}
type asId = i:pre_asId{valid (I_AS i)}

// Resumption context
let rec esId_rc : (esId -> St bytes) =
  function
  | NoPSK h -> H.zeroHash h

and hsId_rc : (hsId -> St bytes) = function
  | HSID_DHE (Salt i) _ _ _ -> secretId_rc i
  | HSID_PSK (Salt i) -> secretId_rc i

and asId_rc : (asId -> St bytes) = function
  | ASID (Salt i) -> secretId_rc i

and secretId_rc : (secretId -> St bytes) = function
  | EarlySecretID i -> esId_rc i
  | HandshakeSecretID i -> hsId_rc i
  | ApplicationSecretID i -> asId_rc i

// miTLS 0.9:
// ==========
// PRF (type pms) -> TLSInfo (type id) -> KEF (extract pms)
//                     \ StatefulLHAE (coerce id) /
// TODO rework old 1.2 types
type ms = bytes
type pms = bytes

// Early secret (abstract)
val es (i:esId) : Type0

// Handshake secret (abstract)
val hs (i:hsId) : Type0
/
prims.fst.checked MiTLS.TLSPRF.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Ticket.fst.checked MiTLS.StatefulLHAE.fst.checked MiTLS.StAE.fst.checked MiTLS.RSAKey.fst.checked MiTLS.Range.fst.checked MiTLS.PSK.fst.checked MiTLS.Old.HMAC.UFCMA.fsti.checked MiTLS.Nonce.fsti.checked MiTLS.HKDF.fsti.checked MiTLS.Hashing.Spec.fst.checked MiTLS.Extensions.fsti.checked MiTLS.EverCrypt.fsti.checked MiTLS.DebugFlags.fst.checked MiTLS.CommonDH.fsti.checked Hacl.Hash.Definitions.fst.checked FStar.UInt32.fsti.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.DependentMap.fsti.checked FStar.List.Tot.fst.checked FStar.IO.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Heap.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.Old.KeySchedule.fsti
_: FStar.Bytes.bytes -> Prims.logical
FStar.Bytes.bytes Prims.l_True Prims.logical
let trivial (_: bytes) =
  
True