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.Bignum25519.fsti.checked
Spec.Ed25519.fst.checked Spec.Curve25519.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.Curve25519.Finv.fst.checked Hacl.Spec.Curve25519.Field51.Definition.fst.checked Hacl.Impl.Ed25519.Field51.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked
Hacl.Bignum25519.fsti
Hacl.Bignum25519.point Lib.Buffer.sub Lib.Buffer.MUT Lib.IntTypes.uint64 FStar.UInt32.__uint_to_t Lib.Buffer.lbuffer_t Hacl.Bignum25519.felem FStar.Monotonic.HyperStack.mem Lib.Buffer.live Prims.l_and Prims.eq2 Lib.Buffer.gsub
module Hacl.Bignum25519

module ST = FStar.HyperStack.ST
open FStar.HyperStack.All

open Lib.IntTypes
open Lib.Buffer

module BSeq = Lib.ByteSequence
module S51 = Hacl.Spec.Curve25519.Field51.Definition
module F51 = Hacl.Impl.Ed25519.Field51

module SC = Spec.Curve25519

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

(* Type abbreviations *)
inline_for_extraction noextract
let felem = lbuffer uint64 5ul

(* A point is buffer of size 20, that is 4 consecutive buffers of size 5 *)
inline_for_extraction noextract
let point = lbuffer uint64 20ul

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.Bignum25519.point -> FStar.HyperStack.ST.Stack Hacl.Bignum25519.felem