let pow2_256 = 0x10000000000000000000000000000000000000000000000000000000000000000
let pow2_256 =
0x10000000000000000000000000000000000000000000000000000000000000000
Vale.Curve25519.Fast_defs.fst.checked
Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Curve25519.Fast_lemmas_internal.fsti.checked Vale.Arch.Types.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Curve25519.Fast_defs.fst
module Vale.Curve25519.Fast_defs

open Vale.Def.Words_s
open Vale.Def.Types_s
open FStar.Mul

unfold let pow2_192 = 0x1000000000000000000000000000000000000000000000000
val pow2_256 : Prims.int
Prims.int