val honestRSAPMS : pk: MiTLS.RSAKey.pk -> cv: MiTLS.TLSConstants.protocolVersion -> pms: MiTLS.PMS.rsapms -> Prims.bool
let honestRSAPMS (pk:RSAKey.pk) (cv:TLSConstants.protocolVersion) pms =
  match pms with
  | IdealRSAPMS(s)    -> true
  | ConcreteRSAPMS(s) -> false
﻿module MiTLS.PMS

(* Split from KEF *)

open MiTLS.Mem
open FStar.Bytes
open MiTLS.TLSConstants

#reset-options "--using_facts_from '* -LowParse.Spec.Base'"

let ideal = Flags.ideal_PMS // controls idealization of PMS.

type rsarepr = bytes
(*private*)
type rsaseed = {seed: rsarepr}

// To ideally avoid collisions concerns between Honest and Coerced pms we use a sum type.
type rsapms =
//#if ideal
  | IdealRSAPMS of rsaseed
//#endif
  | ConcreteRSAPMS of rsarepr

//#if ideal
/
prims.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.RSAKey.fst.checked MiTLS.Random.fst.checked MiTLS.Mem.fst.checked MiTLS.Flags.fst.checked MiTLS.CommonDH.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.PMS.fst
pk: MiTLS.RSAKey.pk -> cv: MiTLS.TLSConstants.protocolVersion -> pms: MiTLS.PMS.rsapms -> Prims.bool
MiTLS.RSAKey.pk MiTLS.TLSConstants.protocolVersion MiTLS.PMS.rsapms MiTLS.PMS.rsaseed MiTLS.PMS.rsarepr Prims.bool
let honestRSAPMS (pk: RSAKey.pk) (cv: TLSConstants.protocolVersion) pms =
  
match pms with
| IdealRSAPMS s -> true
| ConcreteRSAPMS s -> false