val prf (i: id) : Tot bool
val prf (i: id) : Tot bool
let prf (i: id): Tot bool = safeHS i && cipher_prf(cipherAlg_of_id i)
module MiTLS.Flag
open MiTLS

module ST = FStar.HyperStack.ST

open FStar.HyperStack.All

open MiTLS.Crypto.Indexing

(* All the idealization flags that we use for the cryptographic argument *)

// TODO check that the real implementation normalizes fully.


(* CRYPTOGRAPHIC SECURITY ASSUMPTIONS.
   These are not conditioned by i. 
   They suffice to select every intermediate game in our proof.
   They are ordered as successive idealization steps in our proof.
   We used to refer to those as "algorithmic strength predicates".
*) 

// controls idealization of each cipher as a perfect random function
assume 
val cipher_prf: cipherAlg -> Tot bool 

// controls existence of logs for all MACs
assume
val mac_log: bool                

// idealizes each one-time MAC as perfectly INT-1CMA.
assume
val mac_int1cma: macAlg -> Tot bool  

// controls 2nd, perfect idealization step in enxor/dexor for all PRFs.
assume
val prf_cpa: bool


(* CONDITIONAL IDEALIZATION *) 

// guarantees fresh record keys (to be defined by TLS Handshake)
assume
val safeHS: i:id -> Tot bool
/
prims.fst.checked MiTLS.Crypto.Indexing.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked
MiTLS.Flag.fst
i: MiTLS.Crypto.Indexing.id -> Prims.bool
MiTLS.Crypto.Indexing.id Prims.op_AmpAmp MiTLS.Flag.safeHS MiTLS.Flag.cipher_prf MiTLS.Crypto.Indexing.cipherAlg_of_id Prims.bool
let prf (i: id) : Tot bool =
  
safeHS i && cipher_prf (cipherAlg_of_id i)