let aff_point_inv_seq (p:aff_point_seq) =
  let x, y = as_aff_point_nat_seq p in
  x < S.prime /\ y < S.prime
let aff_point_inv_seq (p: aff_point_seq) =
let x, y = as_aff_point_nat_seq p in
x < S.prime /\ y < S.prime
Hacl.Impl.P256.Point.fsti.checked
Spec.P256.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.P256.Montgomery.fsti.checked Hacl.Spec.Bignum.Definitions.fst.checked Hacl.Impl.P256.Bignum.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Hacl.Impl.P256.Point.fsti
Hacl.Impl.P256.Point.aff_point_seq Prims.nat Prims.l_and Prims.b2t Prims.op_LessThan Spec.P256.PointOps.prime Prims.logical FStar.Pervasives.Native.tuple2 Hacl.Impl.P256.Point.as_aff_point_nat_seq
module Hacl.Impl.P256.Point

open FStar.Mul
open FStar.HyperStack.All
open FStar.HyperStack

open Lib.IntTypes
open Lib.Buffer

open Hacl.Impl.P256.Bignum

module S = Spec.P256
module SM = Hacl.Spec.P256.Montgomery
module BD = Hacl.Spec.Bignum.Definitions
module LSeq = Lib.Sequence

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

let from_mont_point (a:tuple3 nat nat nat) : S.proj_point =
  let x, y, z = a in SM.from_mont x, SM.from_mont y, SM.from_mont z


///  Affine coordinates

inline_for_extraction noextract
let aff_point_seq = LSeq.lseq uint64 8

let as_aff_point_nat_seq (p:aff_point_seq) =
  BD.bn_v (LSeq.sub p 0 4),
  BD.bn_v (LSeq.sub p 4 4)
val aff_point_inv_seq : p: Hacl.Impl.P256.Point.aff_point_seq -> Prims.logical
p: Hacl.Impl.P256.Point.aff_point_seq -> Prims.logical