val ext_g_pow2_64:S.ext_point
let ext_g_pow2_64 : S.ext_point =
  [@inline_let]
  let rX : SC.elem = 0x5a8a5a58bef144743ef0a14ef1bad8b169be613a4f82d2c418c00c5507edf10d in
  [@inline_let]
  let rY : SC.elem = 0x1ad2dd576455f6786b43640245cf64fae933ffc7ecabc74b63ce54790e453f73 in
  [@inline_let]
  let rZ : SC.elem = 0x424da3d215aef3b7967274a7d81d8d30e7a51756922ebd07058c9d04ac8405e0 in
  [@inline_let]
  let rT : SC.elem = 0x75e4cec7f1c8417c2268c6cff4e4f9d94dd599649b949e8e19cf23c11f401586 in
  (rX, rY, rZ, rT)
val ext_g_pow2_64:S.ext_point
let ext_g_pow2_64:S.ext_point =
[@@ inline_let ]let rX:SC.elem =
  0x5a8a5a58bef144743ef0a14ef1bad8b169be613a4f82d2c418c00c5507edf10d
in
[@@ inline_let ]let rY:SC.elem =
  0x1ad2dd576455f6786b43640245cf64fae933ffc7ecabc74b63ce54790e453f73
in
[@@ inline_let ]let rZ:SC.elem =
  0x424da3d215aef3b7967274a7d81d8d30e7a51756922ebd07058c9d04ac8405e0
in
[@@ inline_let ]let rT:SC.elem =
  0x75e4cec7f1c8417c2268c6cff4e4f9d94dd599649b949e8e19cf23c11f401586
in
(rX, rY, rZ, rT)
Hacl.Ed25519.PrecompTable.fst.checked
Spec.Exponentiation.fsti.checked Spec.Ed25519.fst.checked Spec.Curve25519.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.NatMod.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.PrecompBaseTable256.fsti.checked Hacl.Spec.PrecompBaseTable.fsti.checked Hacl.Spec.Ed25519.PrecompTable.fsti.checked Hacl.Impl.Ed25519.Group.fst.checked Hacl.Bignum25519.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.List.Tot.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.Calc.fsti.checked
Hacl.Ed25519.PrecompTable.fst
FStar.Pervasives.Native.Mktuple4 Spec.Curve25519.elem
module Hacl.Ed25519.PrecompTable

module ST = FStar.HyperStack.ST
open FStar.HyperStack.All
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer

open Hacl.Bignum25519

module LSeq = Lib.Sequence
module LM = Lib.NatMod
module SE = Spec.Exponentiation
module SPT = Hacl.Spec.PrecompBaseTable
module SPT256 = Hacl.Spec.PrecompBaseTable256
module SPTE = Hacl.Spec.Ed25519.PrecompTable
module S = Spec.Ed25519
module SC = Spec.Curve25519

include Hacl.Impl.Ed25519.Group

#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"

let ext_point_to_list p =
  SPTE.ext_point_to_list_lemma p;
  SPTE.ext_point_to_list p

let lemma_refl x =
  SPTE.ext_point_to_list_lemma x

//-----------------

val lemma_is_on_curve: x:SC.elem -> y:SC.elem ->
  Lemma (Spec.Curve25519.(y *% y -% x *% x) == (y * y - x * x) % SC.prime /\
  Spec.Curve25519.(1 +% S.d *% (x *% x) *% (y *% y)) == (1 + S.d * (x * x) * (y * y)) % SC.prime)

let lemma_is_on_curve x y =
  let open Spec.Curve25519 in
  let open Spec.Ed25519 in
  calc (==) {
    y *% y -% x *% x;
    (==) { }
    ((y * y) % prime - (x * x) % prime) % prime;
    (==) { Math.Lemmas.lemma_mod_plus_distr_l (y * y) (- (x * x) % prime) prime }
    (y * y - (x * x) % prime) % prime;
    (==) { Math.Lemmas.lemma_mod_sub_distr (y * y) (x * x) prime }
    (y * y - x * x) % prime;
    };

  calc (==) {
    1 +% S.d *% (x *% x) *% (y *% y);
    (==) { }
    (1 + (S.d * (x * x % prime) % prime) * (y * y % prime) % prime) % prime;
    (==) { Math.Lemmas.lemma_mod_mul_distr_r S.d (x * x) prime }
    (1 + (S.d * (x * x) % prime) * (y * y % prime) % prime) % prime;
    (==) { Math.Lemmas.lemma_mod_mul_distr_l (S.d * (x * x)) (y * y % prime) prime }
    (1 + (S.d * (x * x)) * (y * y % prime) % prime) % prime;
    (==) { Math.Lemmas.lemma_mod_mul_distr_r (S.d * (x * x)) (y * y) prime }
    (1 + (S.d * (x * x)) * (y * y) % prime) % prime;
    (==) { Math.Lemmas.lemma_mod_plus_distr_r 1 ((S.d * (x * x)) * (y * y)) prime }
    (1 + (S.d * (x * x)) * (y * y)) % prime;
    }

//--------------

inline_for_extraction noextract
val ext_g_pow2_64:S.ext_point
Spec.Ed25519.PointOps.ext_point