let decodePoint (u:serialized_point) =
  (nat_from_bytes_le u % pow2 255) % prime
let decodePoint (u: serialized_point) =
(nat_from_bytes_le u % pow2 255) % prime
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
Spec.Curve25519.serialized_point Prims.op_Modulus Lib.ByteSequence.nat_from_bytes_le Lib.IntTypes.SEC Prims.pow2 Spec.Curve25519.prime Prims.int
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"

(* Field types and parameters *)
let prime : pos = pow2 255 - 19

type elem = x:nat{x < prime}
let zero : elem = 0
let one  : elem = 1

let fadd (x:elem) (y:elem) : elem = (x + y) % prime
let fsub (x:elem) (y:elem) : elem = (x - y) % prime
let fmul (x:elem) (y:elem) : elem = (x * y) % prime

let ( +% ) = fadd
let ( -% ) = fsub
let ( *% ) = fmul

let fpow (x:elem) (b:nat) : elem = Lib.NatMod.pow_mod #prime x b
let ( **% ) = fpow
  
let finv (x:elem) : elem = x **% (prime - 2)
let ( /% ) (x:elem) (y:elem) = x *% finv y

(* Type aliases *)
type scalar = lbytes 32
type serialized_point = lbytes 32
type proj_point = elem & elem

let ith_bit (k:scalar) (i:nat{i < 256}) : uint64 =
  let q = i / 8 in let r = size (i % 8) in
  to_u64 ((k.[q] >>. r) &. u8 1)

let decodeScalar (k:scalar) =
  let k : scalar = k.[0] <- (k.[0] &. u8 248) in
  let k : scalar = k.[31] <- (k.[31] &. u8 127) in
  let k : scalar = k.[31] <- (k.[31] |. u8 64) in k
val decodePoint : u23: Spec.Curve25519.serialized_point -> Prims.int
u23: Spec.Curve25519.serialized_point -> Prims.int