val print_share (#g: CommonDH.group) (s: CommonDH.share g)
    : ST unit (requires (fun h0 -> True)) (ensures (fun h0 _ h1 -> modifies_none h0 h1))
val print_share (#g: CommonDH.group) (s: CommonDH.share g)
    : ST unit (requires (fun h0 -> True)) (ensures (fun h0 _ h1 -> modifies_none h0 h1))
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)
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"
/
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
s: MiTLS.CommonDH.share g -> FStar.HyperStack.ST.ST Prims.unit
MiTLS.CommonDH.group MiTLS.CommonDH.share MiTLS.Old.KeySchedule.dbg Prims.op_Hat Prims.unit Prims.string FStar.Bytes.hex_of_bytes FStar.Bytes.bytes MiTLS.CommonDH.serialize_raw FStar.Monotonic.HyperStack.mem Prims.l_True FStar.HyperStack.ST.modifies_none
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)