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)}
let ext_point_to_list p =
  SPTE.ext_point_to_list_lemma p;
  SPTE.ext_point_to_list p
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)}
let ext_point_to_list p =
SPTE.ext_point_to_list_lemma p;
SPTE.ext_point_to_list p
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
Spec.Ed25519.ext_point_c Hacl.Spec.Ed25519.PrecompTable.ext_point_to_list Prims.unit Hacl.Spec.Ed25519.PrecompTable.ext_point_to_list_lemma Prims.list Lib.IntTypes.uint64 Prims.l_and Prims.b2t Prims.op_Equality Prims.int FStar.List.Tot.Base.length Hacl.Impl.Exponentiation.Definitions.__proj__Mkto_comm_monoid__item__linv Lib.IntTypes.U64 FStar.UInt32.uint_to_t Hacl.Impl.Ed25519.Group.mk_to_ed25519_comm_monoid FStar.Seq.Properties.seq_of_list
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"
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)}
p: Spec.Ed25519.ext_point_c
  -> x:
    Prims.list Lib.IntTypes.uint64
      { FStar.List.Tot.Base.length x = 20 /\
        Mkto_comm_monoid?.linv Hacl.Impl.Ed25519.Group.mk_to_ed25519_comm_monoid
          (FStar.Seq.Properties.seq_of_list x) }