val proj_g_pow2_192:S.proj_point
let proj_g_pow2_192 : S.proj_point =
  [@inline_let]
  let rX : S.felem = 0xbd382b67d20492b1480ca58a6d7d617ba413a9bc7c2f1cff51301ef960fb245c in
  [@inline_let]
  let rY : S.felem = 0x0b232afcf692673aa714357c524c07867a64ea3b9dfab53f0e74622159e86b0d in
  [@inline_let]
  let rZ : S.felem = 0x028a1380449aede5df8219420b458d464a6a4773ac91e8305237878cef1cffa6 in
  (rX, rY, rZ)
val proj_g_pow2_192:S.proj_point
let proj_g_pow2_192:S.proj_point =
[@@ inline_let ]let rX:S.felem =
  0xbd382b67d20492b1480ca58a6d7d617ba413a9bc7c2f1cff51301ef960fb245c
in
[@@ inline_let ]let rY:S.felem =
  0x0b232afcf692673aa714357c524c07867a64ea3b9dfab53f0e74622159e86b0d
in
[@@ inline_let ]let rZ:S.felem =
  0x028a1380449aede5df8219420b458d464a6a4773ac91e8305237878cef1cffa6
in
(rX, rY, 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
FStar.Pervasives.Native.Mktuple3 Spec.K256.PointOps.felem
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)

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)


inline_for_extraction noextract
val proj_g_pow2_192:S.proj_point
Spec.K256.PointOps.proj_point