val getz (p: point)
    : Stack felem
      (requires fun h -> live h p)
      (ensures fun h0 f h1 -> f == gsub p 10ul 5ul /\ h0 == h1)
let getz (p:point) : Stack felem
  (requires fun h -> live h p)
  (ensures fun h0 f h1 -> f == gsub p 10ul 5ul /\ h0 == h1)
  = sub p 10ul 5ul
val getz (p: point)
    : Stack felem
      (requires fun h -> live h p)
      (ensures fun h0 f h1 -> f == gsub p 10ul 5ul /\ h0 == h1)
let getz (p: point)
    : Stack felem
      (requires fun h -> live h p)
      (ensures fun h0 f h1 -> f == gsub p 10ul 5ul /\ h0 == h1) =
sub p 10ul 5ul
Hacl.Impl.K256.Point.fsti.checked
Spec.K256.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.K256.Field.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.Impl.K256.Point.fsti
Hacl.Impl.K256.Point.point Lib.Buffer.sub Lib.Buffer.MUT Lib.IntTypes.uint64 FStar.UInt32.__uint_to_t Lib.Buffer.lbuffer_t Hacl.K256.Field.felem FStar.Monotonic.HyperStack.mem Lib.Buffer.live Prims.l_and Prims.eq2 Hacl.K256.Field.nlimb Lib.Buffer.gsub
module Hacl.Impl.K256.Point

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 S = Spec.K256
open Hacl.K256.Field

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

inline_for_extraction noextract
let as_felem5_lseq (s:LSeq.lseq uint64 5) : felem5 =
  let open Lib.Sequence in
  (s.[0],s.[1],s.[2],s.[3],s.[4])


///  Affine coordinates

inline_for_extraction noextract
let aff_point_seq = LSeq.lseq uint64 10

let aff_point_inv_seq (p:aff_point_seq) =
  inv_fully_reduced5 (as_felem5_lseq (LSeq.sub p 0 5)) /\
  inv_fully_reduced5 (as_felem5_lseq (LSeq.sub p 5 5))

let aff_point_eval_seq (p:aff_point_seq{aff_point_inv_seq p}) : S.aff_point =
  as_nat5 (as_felem5_lseq (LSeq.sub p 0 5)),
  as_nat5 (as_felem5_lseq (LSeq.sub p 5 5))

inline_for_extraction noextract
let aff_point = lbuffer uint64 10ul

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

noextract
let aff_point_eval (h:mem) (p:aff_point{aff_point_inv h p}) : GTot S.aff_point =
  aff_point_eval_seq (as_seq h p)


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 5ul /\ h0 == h1)
  = sub p 0ul 5ul

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 5ul 5ul /\ h0 == h1)
  = sub p 5ul 5ul


///  Projective coordinates

// (_X, _Y, _Z)
inline_for_extraction noextract
let point = lbuffer uint64 15ul

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

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

inline_for_extraction noextract
let getz (p:point) : Stack felem
  (requires fun h -> live h p)
val getz (p: point)
    : Stack felem
      (requires fun h -> live h p)
      (ensures fun h0 f h1 -> f == gsub p 10ul 5ul /\ h0 == h1)
p: Hacl.Impl.K256.Point.point -> FStar.HyperStack.ST.Stack Hacl.K256.Field.felem