let pow_point (k:nat) (p:S.aff_point) =
  LE.pow S.mk_p256_comm_monoid p k
let pow_point (k: nat) (p: S.aff_point) =
LE.pow S.mk_p256_comm_monoid p k
Hacl.P256.PrecompTable.fsti.checked
Spec.P256.fst.checked Spec.Exponentiation.fsti.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.Spec.P256.Montgomery.fsti.checked Hacl.Impl.P256.Point.fsti.checked Hacl.Impl.P256.Group.fst.checked Hacl.Impl.Exponentiation.Definitions.fst.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.fst.checked
Hacl.P256.PrecompTable.fsti
Prims.nat Spec.P256.PointOps.aff_point Lib.Exponentiation.Definition.pow Spec.P256.mk_p256_comm_monoid
module Hacl.P256.PrecompTable

open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer

module ST = FStar.HyperStack.ST
module LSeq = Lib.Sequence

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

module S = Spec.P256
module SM = Hacl.Spec.P256.Montgomery

open Hacl.Impl.P256.Point
include Hacl.Impl.P256.Group

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

inline_for_extraction noextract
val proj_point_to_list: p:S.proj_point
  -> x:list uint64{FStar.List.Tot.length x = 12 /\
    mk_to_p256_comm_monoid.BE.linv (Seq.seq_of_list x)}

val lemma_refl: x:S.proj_point ->
  Lemma (S.mk_p256_concrete_ops.SE.to.SE.refl x ==
    mk_to_p256_comm_monoid.BE.refl (Seq.seq_of_list (proj_point_to_list x)))

inline_for_extraction noextract
let mk_p256_precomp_base_table: SPT.mk_precomp_base_table S.proj_point U64 12ul 0ul = {
  SPT.concr_ops = S.mk_p256_concrete_ops;
  SPT.to_cm = mk_to_p256_comm_monoid;
  SPT.to_list = proj_point_to_list;
  SPT.lemma_refl = lemma_refl;
}

inline_for_extraction noextract
val pow_point : k: Prims.nat -> p: Spec.P256.PointOps.aff_point -> Spec.P256.PointOps.aff_point
k: Prims.nat -> p: Spec.P256.PointOps.aff_point -> Spec.P256.PointOps.aff_point