val ext_g_pow2_128:S.ext_point
let ext_g_pow2_128 : S.ext_point =
  [@inline_let]
  let rX : SC.elem = 0x38569441a1f5cd408a120bf398c05f4d98921fc59796c50c2af9fb1690e8727e in
  [@inline_let]
  let rY : SC.elem = 0x0a97dfad58fa26197529d9296502368db1c0513ba4c45512f239db96f78d2e7c in
  [@inline_let]
  let rZ : SC.elem = 0x78d98ebac33bd94604a2ce24527eb73c2cba4d3b1e5f55b8444bb5e513a54540 in
  [@inline_let]
  let rT : SC.elem = 0x3dc4d80a0c809ab67253c9cae46b0a2fdbfca8ca0f515475b21d1e95fb8d9add in
  (rX, rY, rZ, rT)
val ext_g_pow2_128:S.ext_point
let ext_g_pow2_128:S.ext_point =
[@@ inline_let ]let rX:SC.elem =
  0x38569441a1f5cd408a120bf398c05f4d98921fc59796c50c2af9fb1690e8727e
in
[@@ inline_let ]let rY:SC.elem =
  0x0a97dfad58fa26197529d9296502368db1c0513ba4c45512f239db96f78d2e7c
in
[@@ inline_let ]let rZ:SC.elem =
  0x78d98ebac33bd94604a2ce24527eb73c2cba4d3b1e5f55b8444bb5e513a54540
in
[@@ inline_let ]let rT:SC.elem =
  0x3dc4d80a0c809ab67253c9cae46b0a2fdbfca8ca0f515475b21d1e95fb8d9add
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
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)

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 ext_g_pow2_64_zinv: unit -> Lemma (let (rX, rY, rZ, rT) = ext_g_pow2_64 in
  SC.finv rZ = 0x32435c2ae3ace33871119d9346f332af7d025740cdca88b087ec408e4b7b1c76)

let ext_g_pow2_64_zinv () =
  let rZ = 0x424da3d215aef3b7967274a7d81d8d30e7a51756922ebd07058c9d04ac8405e0 in
  let rZ_comp = normalize_term (LM.pow_mod_ #SC.prime rZ (SC.prime - 2)) in
  normalize_term_spec (LM.pow_mod_ #SC.prime rZ (SC.prime - 2));
  assert_norm (rZ_comp ==
    0x32435c2ae3ace33871119d9346f332af7d025740cdca88b087ec408e4b7b1c76);

  let (_, _, qZ, _) = ext_g_pow2_64 in
  assert (qZ == rZ);
  LM.pow_mod_def #SC.prime rZ (SC.prime - 2)


val lemma_ext_g_pow2_64_point_inv: unit -> Lemma (S.point_inv ext_g_pow2_64)
let lemma_ext_g_pow2_64_point_inv () =
  let open Spec.Curve25519 in
  let open Spec.Ed25519 in
  let rX : SC.elem = 0x5a8a5a58bef144743ef0a14ef1bad8b169be613a4f82d2c418c00c5507edf10d in
  let rY : SC.elem = 0x1ad2dd576455f6786b43640245cf64fae933ffc7ecabc74b63ce54790e453f73 in
  let rZ : SC.elem = 0x424da3d215aef3b7967274a7d81d8d30e7a51756922ebd07058c9d04ac8405e0 in
  let rT : SC.elem = 0x75e4cec7f1c8417c2268c6cff4e4f9d94dd599649b949e8e19cf23c11f401586 in
  let zinv : SC.elem = 0x32435c2ae3ace33871119d9346f332af7d025740cdca88b087ec408e4b7b1c76 in
  ext_g_pow2_64_zinv ();
  let (x, y) = (rX *% zinv, rY *% zinv) in
  assert (x = 0x6222bd88bf2df9d5d44b60cfb4a08a960078db7ed51a35eb3e0b6b8ff4eda202);
  assert (y = 0x325bb42ea4ed025dd6bdaed261b7c4f5410b608ba902b068f1efa5782e45313);
  lemma_is_on_curve x y;
  assert ((y * y - x * x) % SC.prime =
    0x44b4161cc56730b0c4ddd3ee61af107f6ec87d11e0da287cb1dc61a07d10842a);
  assert ((1 + d * (x * x) * (y * y)) % SC.prime =
    0x44b4161cc56730b0c4ddd3ee61af107f6ec87d11e0da287cb1dc61a07d10842a);
  assert (S.is_on_curve (x, y));
  assert (rX *% rY *% zinv =
    0x75e4cec7f1c8417c2268c6cff4e4f9d94dd599649b949e8e19cf23c11f401586);
  assert (S.is_ext ext_g_pow2_64)


inline_for_extraction noextract
let ext_g_pow2_64_c : S.ext_point_c =
  lemma_ext_g_pow2_64_point_inv ();
  ext_g_pow2_64


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