val random_init_post : _: _ -> _: _ -> _: _ -> Prims.logical
let random_init_post = fun _ _ _ -> True
module MiTLS.EverCrypt.Specs
open MiTLS

let curve_x25519_pre = fun _ -> False
let curve_x25519_post = fun _ _ _ -> True
/
prims.fst.checked FStar.Pervasives.fsti.checked
MiTLS.EverCrypt.Specs.fsti
_: _ -> _: _ -> _: _ -> Prims.logical
Prims.l_True Prims.logical
let random_init_post =
  
fun _ _ _ -> True