val g_pow2_192:S.aff_point
let g_pow2_192 : S.aff_point = pow_point (pow2 192) g_aff
val g_pow2_192:S.aff_point
let g_pow2_192:S.aff_point =
pow_point (pow2 192) g_aff
Hacl.K256.PrecompTable.fsti.checked
Spec.K256.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.Impl.K256.Point.fsti.checked Hacl.Impl.K256.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.K256.PrecompTable.fsti
Hacl.K256.PrecompTable.pow_point Prims.pow2 Hacl.K256.PrecompTable.g_aff
module Hacl.K256.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.K256

open Hacl.Impl.K256.Point
include Hacl.Impl.K256.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 = 15 /\
    mk_to_k256_comm_monoid.BE.linv (Seq.seq_of_list x)}

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

inline_for_extraction noextract
let mk_k256_precomp_base_table: SPT.mk_precomp_base_table S.proj_point U64 15ul 0ul = {
  SPT.concr_ops = S.mk_k256_concrete_ops;
  SPT.to_cm = mk_to_k256_comm_monoid;
  SPT.to_list = proj_point_to_list;
  SPT.lemma_refl = lemma_refl;
}

inline_for_extraction noextract
let pow_point (k:nat) (p:S.aff_point) =
  LE.pow S.mk_k256_comm_monoid p k

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

noextract
let g_aff : S.aff_point = S.to_aff_point S.g

// [pow2 64]G
noextract
let g_pow2_64 : S.aff_point = pow_point (pow2 64) g_aff

// [pow2 128]G
noextract
let g_pow2_128 : S.aff_point = pow_point (pow2 128) g_aff

// [pow2 192]G
val g_pow2_192:S.aff_point
Spec.K256.PointOps.aff_point