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)))
let lemma_refl x =
  SPTK.proj_point_to_list_lemma 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)))
let lemma_refl x =
SPTK.proj_point_to_list_lemma x
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
Spec.K256.PointOps.proj_point Hacl.Spec.K256.PrecompTable.proj_point_to_list_lemma Prims.unit
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
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)))
x: Spec.K256.PointOps.proj_point
  -> FStar.Pervasives.Lemma
    (ensures
      Mkto_comm_monoid?.refl (Mkconcrete_ops?.to Spec.K256.mk_k256_concrete_ops) x ==
      Mkto_comm_monoid?.refl Hacl.Impl.K256.Group.mk_to_k256_comm_monoid
        (FStar.Seq.Properties.seq_of_list (Hacl.K256.PrecompTable.proj_point_to_list x)))