val g_pow2_64:S.aff_point
val g_pow2_64:S.aff_point
let g_pow2_64 : S.aff_point = pow_point (pow2 64) g_aff
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 F51 = Hacl.Impl.Ed25519.Field51

module LSeq = Lib.Sequence
module LE = Lib.Exponentiation.Definition
module SE = Spec.Exponentiation
module BE = Hacl.Impl.Exponentiation
module SPT = Hacl.Spec.PrecompBaseTable

module S = Spec.Ed25519
include Hacl.Impl.Ed25519.Group

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

inline_for_extraction noextract
val ext_point_to_list: p:S.ext_point_c
  -> x:list uint64{FStar.List.Tot.length x = 20 /\
    mk_to_ed25519_comm_monoid.BE.linv (Seq.seq_of_list x)}


val lemma_refl: x:S.ext_point_c ->
  Lemma (S.mk_ed25519_concrete_ops.SE.to.SE.refl x ==
    mk_to_ed25519_comm_monoid.BE.refl (Seq.seq_of_list (ext_point_to_list x)))


inline_for_extraction noextract
let mk_ed25519_precomp_base_table: SPT.mk_precomp_base_table S.ext_point_c U64 20ul 0ul = {
  SPT.concr_ops = S.mk_ed25519_concrete_ops;
  SPT.to_cm = mk_to_ed25519_comm_monoid;
  SPT.to_list = ext_point_to_list;
  SPT.lemma_refl = lemma_refl;
}


inline_for_extraction noextract
let g_c : S.ext_point_c =
  Spec.Ed25519.Lemmas.g_is_on_curve ();
  S.g


inline_for_extraction noextract
let pow_point (k:nat) (p:S.aff_point_c) =
  LE.pow S.mk_ed25519_comm_monoid p k

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

noextract
let g_aff : S.aff_point_c =
  Spec.Ed25519.Lemmas.g_is_on_curve ();
  S.to_aff_point S.g

// [pow2 64]G
/
Spec.Exponentiation.fsti.checked Spec.Ed25519.Lemmas.fsti.checked Spec.Ed25519.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.Exponentiation.Definition.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.PrecompBaseTable.fsti.checked Hacl.Impl.Exponentiation.fsti.checked Hacl.Impl.Ed25519.Group.fst.checked Hacl.Impl.Ed25519.Field51.fst.checked Hacl.Bignum25519.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.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
Hacl.Ed25519.PrecompTable.fsti
Spec.Ed25519.PointOps.aff_point
Hacl.Ed25519.PrecompTable.pow_point Prims.pow2 Hacl.Ed25519.PrecompTable.g_aff
let g_pow2_64:S.aff_point =
  
pow_point (pow2 64) g_aff