let cswap2 (sw:uint64) (nq:proj_point) (nqp1:proj_point) =
  let open Lib.RawIntTypes in
  if uint_to_nat sw = 1 then (nqp1, nq) else (nq, nqp1)
let cswap2 (sw: uint64) (nq nqp1: proj_point) =
let open Lib.RawIntTypes in if uint_to_nat sw = 1 then (nqp1, nq) else (nq, nqp1)
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
Lib.IntTypes.uint64 Spec.Curve25519.proj_point Prims.op_Equality Prims.int Lib.RawIntTypes.uint_to_nat Lib.IntTypes.U64 Lib.IntTypes.SEC FStar.Pervasives.Native.Mktuple2 Prims.bool FStar.Pervasives.Native.tuple2
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

let decodePoint (u:serialized_point) =
  (nat_from_bytes_le u % pow2 255) % prime

let encodePoint (p:proj_point) : Tot serialized_point =
  let x, z = p in
  let p = x /% z in
  nat_to_bytes_le 32 p

let add_and_double q nq nqp1 =
  let x_1, z_1 = q in
  let x_2, z_2 = nq in
  let x_3, z_3 = nqp1 in
  let a = x_2 +% z_2 in
  let b = x_2 -% z_2 in
  let c = x_3 +% z_3 in
  let d = x_3 -% z_3 in
  let da = d *% a in
  let cb = c *% b in
  let x_3 = da +% cb in
  let z_3 = da -% cb in
  let aa = a *% a in
  let bb = b *% b in
  let x_3 = x_3 *% x_3 in
  let z_3 = z_3 *% z_3 in
  let e = aa -% bb in
  let e121665 = e *% 121665 in
  let aa_e121665 = e121665 +% aa in
  let x_2 = aa *% bb in
  let z_2 = e *% aa_e121665 in
  let z_3 = z_3 *% x_1 in
  (x_2, z_2), (x_3, z_3)

let double nq =
  let x_2, z_2 = nq in
  let a = x_2 +% z_2 in
  let b = x_2 -% z_2 in
  let aa = a *% a in
  let bb = b *% b in
  let e = aa -% bb in
  let e121665 = e *% 121665 in
  let aa_e121665 = e121665 +% aa in
  let x_2 = aa *% bb in
  let z_2 = e *% aa_e121665 in
  x_2, z_2
val cswap2 : sw: Lib.IntTypes.uint64 -> nq: Spec.Curve25519.proj_point -> nqp1: Spec.Curve25519.proj_point
  -> Spec.Curve25519.proj_point * Spec.Curve25519.proj_point
sw: Lib.IntTypes.uint64 -> nq: Spec.Curve25519.proj_point -> nqp1: Spec.Curve25519.proj_point
  -> Spec.Curve25519.proj_point * Spec.Curve25519.proj_point