val point_double : BE.lsqr_st U64 20ul 0ul mk_to_ed25519_comm_monoid
let point_double ctx x xx =
  let h0 = ST.get () in
  Spec.Ed25519.Lemmas.to_aff_point_double_lemma (F51.refl_ext_point (as_seq h0 x));
  Hacl.Impl.Ed25519.PointDouble.point_double xx x
val point_double : BE.lsqr_st U64 20ul 0ul mk_to_ed25519_comm_monoid
let point_double ctx x xx =
let h0 = ST.get () in
Spec.Ed25519.Lemmas.to_aff_point_double_lemma (F51.refl_ext_point (as_seq h0 x));
Hacl.Impl.Ed25519.PointDouble.point_double xx x
Hacl.Impl.Ed25519.Group.fst.checked
Spec.Ed25519.Lemmas.fsti.checked Spec.Ed25519.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Impl.Exponentiation.Definitions.fst.checked Hacl.Impl.Ed25519.PointDouble.fst.checked Hacl.Impl.Ed25519.PointConstants.fst.checked Hacl.Impl.Ed25519.PointAdd.fst.checked Hacl.Impl.Ed25519.Field51.fst.checked Hacl.Bignum25519.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked
Hacl.Impl.Ed25519.Group.fst
Lib.Buffer.lbuffer Lib.IntTypes.uint_t Lib.IntTypes.U64 Lib.IntTypes.SEC FStar.UInt32.__uint_to_t Hacl.Impl.Ed25519.PointDouble.point_double Prims.unit Spec.Ed25519.Lemmas.to_aff_point_double_lemma Hacl.Impl.Ed25519.Field51.refl_ext_point Lib.Buffer.as_seq Lib.Buffer.MUT FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get
module Hacl.Impl.Ed25519.Group

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

open Lib.IntTypes
open Lib.Buffer

open Hacl.Bignum25519
open Hacl.Impl.Ed25519.PointConstants

module LSeq = Lib.Sequence
module F51 = Hacl.Impl.Ed25519.Field51
module BE = Hacl.Impl.Exponentiation.Definitions
module S = Spec.Ed25519

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

unfold
let a_spec = S.aff_point_c

unfold
let refl (a:LSeq.lseq uint64 20{F51.linv a}) : GTot a_spec =
  S.to_aff_point (F51.refl_ext_point a)

unfold
let linv_ctx (a:LSeq.lseq uint64 0) : Type0 = True

inline_for_extraction noextract
let mk_to_ed25519_comm_monoid : BE.to_comm_monoid U64 20ul 0ul = {
  BE.a_spec = a_spec;
  BE.comm_monoid = S.mk_ed25519_comm_monoid;
  BE.linv_ctx = linv_ctx;
  BE.linv = F51.linv;
  BE.refl = refl;
}


inline_for_extraction noextract
val point_add : BE.lmul_st U64 20ul 0ul mk_to_ed25519_comm_monoid
let point_add ctx x y xy =
  let h0 = ST.get () in
  Spec.Ed25519.Lemmas.to_aff_point_add_lemma
    (F51.refl_ext_point (as_seq h0 x)) (F51.refl_ext_point (as_seq h0 y));
  Hacl.Impl.Ed25519.PointAdd.point_add xy x y


inline_for_extraction noextract
val point_double : BE.lsqr_st U64 20ul 0ul mk_to_ed25519_comm_monoid
Hacl.Impl.Exponentiation.Definitions.lsqr_st Lib.IntTypes.U64
  20ul
  0ul
  Hacl.Impl.Ed25519.Group.mk_to_ed25519_comm_monoid