val ideal : MiTLS.Flags.t
let ideal = Flags.ideal_PMS
﻿module MiTLS.PMS

(* Split from KEF *)

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

#reset-options "--using_facts_from '* -LowParse.Spec.Base'"
/
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
MiTLS.Flags.t
MiTLS.Flags.ideal_PMS
let ideal =
  
Flags.ideal_PMS