val lemma_ext_g_pow2_64_eval : unit ->
  Lemma (SE.exp_pow2 S.mk_ed25519_concrete_ops g_c 64 == ext_g_pow2_64)
let lemma_ext_g_pow2_64_eval () =
  let co = S.mk_ed25519_concrete_ops in
  SPT256.exp_pow2_rec_is_exp_pow2 co g_c 64;
  let qX, qY, qZ, qT = normalize_term (SPT256.exp_pow2_rec co g_c 64) in
  normalize_term_spec (SPT256.exp_pow2_rec co g_c 64);
  let rX : SC.elem = 0x5a8a5a58bef144743ef0a14ef1bad8b169be613a4f82d2c418c00c5507edf10d in
  let rY : SC.elem = 0x1ad2dd576455f6786b43640245cf64fae933ffc7ecabc74b63ce54790e453f73 in
  let rZ : SC.elem = 0x424da3d215aef3b7967274a7d81d8d30e7a51756922ebd07058c9d04ac8405e0 in
  let rT : SC.elem = 0x75e4cec7f1c8417c2268c6cff4e4f9d94dd599649b949e8e19cf23c11f401586 in
  assert_norm (qX == rX /\ qY == rY /\ qZ == rZ /\ qT == rT)
val lemma_ext_g_pow2_64_eval : unit ->
  Lemma (SE.exp_pow2 S.mk_ed25519_concrete_ops g_c 64 == ext_g_pow2_64)
let lemma_ext_g_pow2_64_eval () =
let co = S.mk_ed25519_concrete_ops in
SPT256.exp_pow2_rec_is_exp_pow2 co g_c 64;
let qX, qY, qZ, qT = normalize_term (SPT256.exp_pow2_rec co g_c 64) in
normalize_term_spec (SPT256.exp_pow2_rec co g_c 64);
let rX:SC.elem = 0x5a8a5a58bef144743ef0a14ef1bad8b169be613a4f82d2c418c00c5507edf10d in
let rY:SC.elem = 0x1ad2dd576455f6786b43640245cf64fae933ffc7ecabc74b63ce54790e453f73 in
let rZ:SC.elem = 0x424da3d215aef3b7967274a7d81d8d30e7a51756922ebd07058c9d04ac8405e0 in
let rT:SC.elem = 0x75e4cec7f1c8417c2268c6cff4e4f9d94dd599649b949e8e19cf23c11f401586 in
assert_norm (qX == rX /\ qY == rY /\ qZ == rZ /\ qT == 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
Prims.unit Spec.Curve25519.elem FStar.Pervasives.assert_norm Prims.l_and Prims.eq2 FStar.Pervasives.normalize_term_spec Spec.Ed25519.ext_point_c Hacl.Spec.PrecompBaseTable256.exp_pow2_rec Hacl.Ed25519.PrecompTable.g_c FStar.Pervasives.Native.tuple4 FStar.Pervasives.normalize_term Hacl.Spec.PrecompBaseTable256.exp_pow2_rec_is_exp_pow2 Spec.Exponentiation.concrete_ops Spec.Ed25519.mk_ed25519_concrete_ops
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
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 lemma_ext_g_pow2_64_eval : unit ->
  Lemma (SE.exp_pow2 S.mk_ed25519_concrete_ops g_c 64 == ext_g_pow2_64)
val lemma_ext_g_pow2_64_eval : unit ->
  Lemma (SE.exp_pow2 S.mk_ed25519_concrete_ops g_c 64 == ext_g_pow2_64)
_: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures
      Spec.Exponentiation.exp_pow2 Spec.Ed25519.mk_ed25519_concrete_ops
        Hacl.Ed25519.PrecompTable.g_c
        64 ==
      Hacl.Ed25519.PrecompTable.ext_g_pow2_64)