val prime:pos
let prime : pos = pow2 255 - 19
val prime:pos
let prime:pos =
pow2 255 - 19
Spec.Curve25519.fst.checked
Spec.Curve25519.Lemmas.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.NatMod.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.UInt8.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked
Spec.Curve25519.fst
Prims.op_Subtraction Prims.pow2
module Spec.Curve25519

open FStar.Mul
open Lib.IntTypes
open Lib.Sequence
open Lib.ByteSequence

open Spec.Curve25519.Lemmas

#set-options "--z3rlimit 30 --ifuel 0 --fuel 0"
val prime:pos
Prims.pos