let point_seq = LSeq.lseq uint64 12
let point_seq =
LSeq.lseq uint64 12
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
Lib.Sequence.lseq Lib.IntTypes.uint64
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)

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


inline_for_extraction noextract
let aff_point = lbuffer uint64 8ul

noextract
let as_aff_point_nat (h:mem) (p:aff_point) =
  as_aff_point_nat_seq (as_seq h p)

noextract
let aff_point_inv (h:mem) (p:aff_point) =
  aff_point_inv_seq (as_seq h p)

noextract
let aff_point_x_as_nat (h:mem) (p:aff_point) : GTot nat =
  as_nat h (gsub p 0ul 4ul)

noextract
let aff_point_y_as_nat (h:mem) (p:aff_point) : GTot nat =
  as_nat h (gsub p 4ul 4ul)

inline_for_extraction noextract
let aff_getx (p:aff_point) : Stack felem
  (requires fun h -> live h p)
  (ensures fun h0 f h1 -> f == gsub p 0ul 4ul /\ h0 == h1)
  = sub p 0ul 4ul

inline_for_extraction noextract
let aff_gety (p:aff_point) : Stack felem
  (requires fun h -> live h p)
  (ensures fun h0 f h1 -> f == gsub p 4ul 4ul /\ h0 == h1)
  = sub p 4ul 4ul


///  Projective coordinates
val point_seq : Type0
Type0