val proj_g_pow2_64:S.proj_point
let proj_g_pow2_64 : S.proj_point =
  [@inline_let]
  let rX : S.felem = 0x000931f4ae428a4ad81ee0aa89cf5247ce85d4dd696c61b4bb9d4761e57b7fbe in
  [@inline_let]
  let rY : S.felem = 0x7e88e5e6a142d5c2269f21a158e82ab2c79fcecb26e397b96fd5b9fbcd0a69a5 in
  [@inline_let]
  let rZ : S.felem = 0x02626dc2dd5e06cd19de5e6afb6c5dbdd3e41dc1472e7b8ef11eb0662e41c44b in
  (rX, rY, rZ)
val proj_g_pow2_64:S.proj_point
let proj_g_pow2_64:S.proj_point =
[@@ inline_let ]let rX:S.felem =
  0x000931f4ae428a4ad81ee0aa89cf5247ce85d4dd696c61b4bb9d4761e57b7fbe
in
[@@ inline_let ]let rY:S.felem =
  0x7e88e5e6a142d5c2269f21a158e82ab2c79fcecb26e397b96fd5b9fbcd0a69a5
in
[@@ inline_let ]let rZ:S.felem =
  0x02626dc2dd5e06cd19de5e6afb6c5dbdd3e41dc1472e7b8ef11eb0662e41c44b
in
(rX, rY, rZ)
Hacl.P256.PrecompTable.fst.checked
Spec.P256.Lemmas.fsti.checked Spec.P256.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.P256.PrecompTable.fsti.checked Hacl.Impl.P256.Point.fsti.checked Hacl.Impl.P256.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.P256.PrecompTable.fst
FStar.Pervasives.Native.Mktuple3 Prims.nat Spec.P256.PointOps.felem
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
module SE = Spec.Exponentiation
module SPT = Hacl.Spec.PrecompBaseTable
module SPT256 = Hacl.Spec.PrecompBaseTable256
module SPTK = Hacl.Spec.P256.PrecompTable

module S = Spec.P256
module SL = Spec.P256.Lemmas

open Hacl.Impl.P256.Point
include Hacl.Impl.P256.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
val proj_g_pow2_64:S.proj_point
Spec.P256.PointOps.proj_point