val coerce (k: bytes) : key
val coerce (k: bytes) : key
let coerce (k:bytes) : key = k
﻿(* Copyright (C) 2012--2015 Microsoft Research and INRIA *)
(* STATUS : JK : assumed two arrays because, has to be fixed *)
module MiTLS.TLSPRF
open MiTLS
module HS = FStar.HyperStack //Added automatically

(* Low-level (bytes -> byte) PRF implementations for TLS
   used by Handshake, Handshake.Secret, KEF, and PRF.
*)

open FStar.HyperStack.ST

open MiTLS.Mem
open MiTLS.Hashing.Spec
open FStar.Bytes
open MiTLS.TLSConstants
open MiTLS.TLSInfo

module U32 = FStar.UInt32
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Mem.fst.checked MiTLS.HMAC.fsti.checked MiTLS.Hashing.Spec.fst.checked MiTLS.Hashing.fsti.checked FStar.UInt32.fsti.checked FStar.Set.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.TLSPRF.fst
k: FStar.Bytes.bytes -> MiTLS.TLSPRF.key
FStar.Bytes.bytes MiTLS.TLSPRF.key
let coerce (k: bytes) : key =
  
k