val lemma_proj_g_pow2_128_eval : unit ->
  Lemma (SE.exp_pow2 S.mk_k256_concrete_ops proj_g_pow2_64 64 == proj_g_pow2_128)
let lemma_proj_g_pow2_128_eval () =
  SPT256.exp_pow2_rec_is_exp_pow2 S.mk_k256_concrete_ops proj_g_pow2_64 64;
  let qX, qY, qZ = normalize_term (SPT256.exp_pow2_rec S.mk_k256_concrete_ops proj_g_pow2_64 64) in
  normalize_term_spec (SPT256.exp_pow2_rec S.mk_k256_concrete_ops proj_g_pow2_64 64);
  let rX : S.felem = 0x98299efbc8e459915404ae015b48cac3b929e0158665f3c7fa5489fbd25c4297 in
  let rY : S.felem = 0xf1e5cbc9579e7d11a31681e947c2959ae0298a006d1c06ab1ad93d6716ea50cc in
  let rZ : S.felem = 0x5c53ffe15001674a2eacb60c9327a8b0ddbd93a0fa6d90309de6cc124133938b in
  assert_norm (qX == rX /\ qY == rY /\ qZ == rZ)
val lemma_proj_g_pow2_128_eval : unit ->
  Lemma (SE.exp_pow2 S.mk_k256_concrete_ops proj_g_pow2_64 64 == proj_g_pow2_128)
let lemma_proj_g_pow2_128_eval () =
SPT256.exp_pow2_rec_is_exp_pow2 S.mk_k256_concrete_ops proj_g_pow2_64 64;
let qX, qY, qZ = normalize_term (SPT256.exp_pow2_rec S.mk_k256_concrete_ops proj_g_pow2_64 64) in
normalize_term_spec (SPT256.exp_pow2_rec S.mk_k256_concrete_ops proj_g_pow2_64 64);
let rX:S.felem = 0x98299efbc8e459915404ae015b48cac3b929e0158665f3c7fa5489fbd25c4297 in
let rY:S.felem = 0xf1e5cbc9579e7d11a31681e947c2959ae0298a006d1c06ab1ad93d6716ea50cc in
let rZ:S.felem = 0x5c53ffe15001674a2eacb60c9327a8b0ddbd93a0fa6d90309de6cc124133938b in
assert_norm (qX == rX /\ qY == rY /\ qZ == rZ)
Hacl.K256.PrecompTable.fst.checked
Spec.K256.Lemmas.fsti.checked Spec.K256.fst.checked Spec.Exponentiation.fsti.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.Exponentiation.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.PrecompBaseTable256.fsti.checked Hacl.Spec.PrecompBaseTable.fsti.checked Hacl.Spec.K256.PrecompTable.fsti.checked Hacl.Impl.K256.Point.fsti.checked Hacl.Impl.K256.Group.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.K256.PrecompTable.fst
Prims.unit Spec.K256.PointOps.felem FStar.Pervasives.assert_norm Prims.l_and Prims.eq2 FStar.Pervasives.normalize_term_spec Spec.K256.PointOps.proj_point Hacl.Spec.PrecompBaseTable256.exp_pow2_rec Spec.K256.mk_k256_concrete_ops Hacl.K256.PrecompTable.proj_g_pow2_64 FStar.Pervasives.Native.tuple3 FStar.Pervasives.normalize_term Hacl.Spec.PrecompBaseTable256.exp_pow2_rec_is_exp_pow2
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
module SE = Spec.Exponentiation
module SPT = Hacl.Spec.PrecompBaseTable
module SPT256 = Hacl.Spec.PrecompBaseTable256
module SPTK = Hacl.Spec.K256.PrecompTable

module S = Spec.K256
module SL = Spec.K256.Lemmas

open Hacl.Impl.K256.Point
include Hacl.Impl.K256.Group

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

let proj_point_to_list p =
  SPTK.proj_point_to_list_lemma p;
  SPTK.proj_point_to_list p

let lemma_refl x =
  SPTK.proj_point_to_list_lemma x

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

inline_for_extraction noextract
let proj_g_pow2_64 : S.proj_point =
  [@inline_let]
  let rX : S.felem = 0x46ec0aa60b0b98c37b29371784676ad967b7beb1a941ddb6fbbff95b44cb788b in
  [@inline_let]
  let rY : S.felem = 0x6b946755bbc6b677576579c990a1ccf14a710545251a1428fabbf02f40268e63 in
  [@inline_let]
  let rZ : S.felem = 0x3c114b2ac17c199ec9eba9f7cc64dc459ca2e53f5bbead2b4e618b318ffcc00e in
  (rX, rY, rZ)

val lemma_proj_g_pow2_64_eval : unit ->
  Lemma (SE.exp_pow2 S.mk_k256_concrete_ops S.g 64 == proj_g_pow2_64)

let lemma_proj_g_pow2_64_eval () =
  SPT256.exp_pow2_rec_is_exp_pow2 S.mk_k256_concrete_ops S.g 64;
  let qX, qY, qZ = normalize_term (SPT256.exp_pow2_rec S.mk_k256_concrete_ops S.g 64) in
  normalize_term_spec (SPT256.exp_pow2_rec S.mk_k256_concrete_ops S.g 64);
  let rX : S.felem = 0x46ec0aa60b0b98c37b29371784676ad967b7beb1a941ddb6fbbff95b44cb788b in
  let rY : S.felem = 0x6b946755bbc6b677576579c990a1ccf14a710545251a1428fabbf02f40268e63 in
  let rZ : S.felem = 0x3c114b2ac17c199ec9eba9f7cc64dc459ca2e53f5bbead2b4e618b318ffcc00e in
  assert_norm (qX == rX /\ qY == rY /\ qZ == rZ)


inline_for_extraction noextract
let proj_g_pow2_128 : S.proj_point =
  [@inline_let]
  let rX : S.felem = 0x98299efbc8e459915404ae015b48cac3b929e0158665f3c7fa5489fbd25c4297 in
  [@inline_let]
  let rY : S.felem = 0xf1e5cbc9579e7d11a31681e947c2959ae0298a006d1c06ab1ad93d6716ea50cc in
  [@inline_let]
  let rZ : S.felem = 0x5c53ffe15001674a2eacb60c9327a8b0ddbd93a0fa6d90309de6cc124133938b in
  (rX, rY, rZ)

val lemma_proj_g_pow2_128_eval : unit ->
  Lemma (SE.exp_pow2 S.mk_k256_concrete_ops proj_g_pow2_64 64 == proj_g_pow2_128)
val lemma_proj_g_pow2_128_eval : unit ->
  Lemma (SE.exp_pow2 S.mk_k256_concrete_ops proj_g_pow2_64 64 == proj_g_pow2_128)
_: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures
      Spec.Exponentiation.exp_pow2 Spec.K256.mk_k256_concrete_ops
        Hacl.K256.PrecompTable.proj_g_pow2_64
        64 ==
      Hacl.K256.PrecompTable.proj_g_pow2_128)