val refl (p: LSeq.lseq uint64 15 {point_inv_lseq p}) : GTot S.aff_point
let refl (p:LSeq.lseq uint64 15{point_inv_lseq p}) : GTot S.aff_point =
  S.to_aff_point (point_eval_lseq p)
val refl (p: LSeq.lseq uint64 15 {point_inv_lseq p}) : GTot S.aff_point
let refl (p: LSeq.lseq uint64 15 {point_inv_lseq p}) : GTot S.aff_point =
S.to_aff_point (point_eval_lseq p)
Hacl.Impl.K256.Group.fst.checked
Spec.K256.Lemmas.fsti.checked Spec.K256.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Impl.K256.PointDouble.fst.checked Hacl.Impl.K256.PointAdd.fst.checked Hacl.Impl.K256.Point.fsti.checked Hacl.Impl.Exponentiation.Definitions.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.Impl.K256.Group.fst
Lib.Sequence.lseq Lib.IntTypes.uint64 Hacl.Impl.K256.Point.point_inv_lseq Spec.K256.PointOps.to_aff_point Hacl.Impl.K256.Point.point_eval_lseq Spec.K256.PointOps.aff_point
module Hacl.Impl.K256.Group

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 BE = Hacl.Impl.Exponentiation.Definitions

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

open Hacl.Impl.K256.Point

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

unfold
let linv_ctx (a:LSeq.lseq uint64 0) : Type0 = True

unfold
val refl (p: LSeq.lseq uint64 15 {point_inv_lseq p}) : GTot S.aff_point
p: Lib.Sequence.lseq Lib.IntTypes.uint64 15 {Hacl.Impl.K256.Point.point_inv_lseq p}
  -> Prims.GTot Spec.K256.PointOps.aff_point