val ideal_PNE : f:ideal_flag{b2t f <==> b2t ideal_AEAD}
let ideal_PNE = false
val ideal_PNE : f:ideal_flag{b2t f <==> b2t ideal_AEAD}
let ideal_PNE =
false
Model.Flags.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked
Model.Flags.fst
module Model.Flags

inline_for_extraction let model = false
inline_for_extraction let ideal_TS = false
val ideal_PNE : f:ideal_flag{b2t f <==> b2t ideal_AEAD}
f: Model.Flags.ideal_flag{f <==> Model.Flags.ideal_AEAD}