val point_z_as_nat (h: mem) (e: point) : GTot nat
let point_z_as_nat (h:mem) (e:point) : GTot nat =
  as_nat h (gsub e 8ul 4ul)
val point_z_as_nat (h: mem) (e: point) : GTot nat
let point_z_as_nat (h: mem) (e: point) : GTot nat =
as_nat h (gsub e 8ul 4ul)
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
FStar.Monotonic.HyperStack.mem Hacl.Impl.P256.Point.point Hacl.Impl.P256.Bignum.as_nat Lib.Buffer.gsub Lib.Buffer.MUT Lib.IntTypes.uint64 FStar.UInt32.__uint_to_t Prims.nat
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

inline_for_extraction noextract
let point_seq = LSeq.lseq uint64 12

let as_point_nat_seq (p:point_seq) =
  BD.bn_v (LSeq.sub p 0 4),
  BD.bn_v (LSeq.sub p 4 4),
  BD.bn_v (LSeq.sub p 8 4)

let point_inv_seq (p:point_seq) =
  let x, y, z = as_point_nat_seq p in
  x < S.prime /\ y < S.prime /\ z < S.prime


inline_for_extraction noextract
let point = lbuffer uint64 12ul

noextract
let as_point_nat (h:mem) (p:point) =
  as_point_nat_seq (as_seq h p)

noextract
let point_inv (h:mem) (p:point) =
  point_inv_seq (as_seq h p)

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

noextract
let point_y_as_nat (h:mem) (e:point) : GTot nat =
  as_nat h (gsub e 4ul 4ul)

noextract
val point_z_as_nat (h: mem) (e: point) : GTot nat
h: FStar.Monotonic.HyperStack.mem -> e: Hacl.Impl.P256.Point.point -> Prims.GTot Prims.nat