let real = b:bool {b ==> ~model}
let real =
b: bool{b ==> ~model}
Flags.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked
Flags.fst
Prims.bool Prims.l_imp Prims.b2t Prims.l_not Flags.model
module Flags

assume val model: bool // scaffolding

let t = b:bool {b ==> model} 
assume val ideal_KEF: t
assume val ideal_Nonce: t
assume val ideal_Sig: t
assume val ideal_PMS: t
assume val ideal_PRF: t
assume val ideal_AEAD: t
assume val ideal_HMAC: t // see HMAC.UFCMA

assume val flag_Raw:  b:bool{b ==> model}
assume val flag_KDF:  d:nat -> b:bool{b ==> model}
assume val flag_KEF0: d:nat -> b:bool{b ==> model /\ flag_KDF d ==> b}
assume val flag_PRF1: d:nat -> b:bool{flag_KEF0 d ==> b /\ b ==> model}
assume val flag_ODH:  d:nat -> b:bool {flag_PRF1 d ==> b /\ b ==> model}
assume val flag_KEF2: d:nat -> b:bool{flag_KDF d ==> b /\ b ==> model}

// debug printing flags, one per module; 
// the refinement enables us to leak secrets for printing.
val real : Type0
Type0