val pow2_63:nat
let pow2_63:nat = 0x8000000000000000
val pow2_63:nat
let pow2_63:nat =
0x8000000000000000
Vale.Curve25519.FastHybrid_helpers.fsti.checked
Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Curve25519.Fast_defs.fst.checked prims.fst.checked FStar.Tactics.CanonCommSemiring.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Calc.fsti.checked
Vale.Curve25519.FastHybrid_helpers.fsti
module Vale.Curve25519.FastHybrid_helpers

open Vale.Def.Words_s
open Vale.Def.Types_s
open FStar.Mul
open FStar.Tactics
open FStar.Tactics.CanonCommSemiring
open Vale.Curve25519.Fast_defs
open FStar.Calc

let int_canon = fun _ -> norm [delta; zeta; iota]; int_semiring () //; dump "Final"
val pow2_63:nat
Prims.nat