val is_point_at_inf_vartime: p:point -> Stack bool
  (requires fun h -> live h p /\ point_inv h p)
  (ensures  fun h0 r h1 -> modifies0 h0 h1 /\
    r == S.is_point_at_inf (as_point_nat h0 p) /\
    r == S.is_point_at_inf (from_mont_point (as_point_nat h0 p)))
let is_point_at_inf_vartime p =
  let h0 = ST.get () in
  lemma_mont_is_point_at_inf (as_point_nat h0 p);
  let pz = getz p in
  bn_is_zero_vartime4 pz
val is_point_at_inf_vartime: p:point -> Stack bool
  (requires fun h -> live h p /\ point_inv h p)
  (ensures  fun h0 r h1 -> modifies0 h0 h1 /\
    r == S.is_point_at_inf (as_point_nat h0 p) /\
    r == S.is_point_at_inf (from_mont_point (as_point_nat h0 p)))
let is_point_at_inf_vartime p =
let h0 = ST.get () in
lemma_mont_is_point_at_inf (as_point_nat h0 p);
let pz = getz p in
bn_is_zero_vartime4 pz
Hacl.Impl.P256.Point.fst.checked
Spec.P256.fst.checked prims.fst.checked Lib.RawIntTypes.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.P256.Montgomery.fsti.checked Hacl.Impl.P256.Finv.fsti.checked Hacl.Impl.P256.Field.fsti.checked Hacl.Impl.P256.Constants.fst.checked Hacl.Impl.P256.Bignum.fsti.checked Hacl.Bignum.Base.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Hacl.Impl.P256.Point.fst
Hacl.Impl.P256.Point.point Hacl.Impl.P256.Bignum.bn_is_zero_vartime4 Prims.bool Hacl.Impl.P256.Bignum.felem Hacl.Impl.P256.Point.getz Prims.unit Hacl.Impl.P256.Point.lemma_mont_is_point_at_inf Hacl.Impl.P256.Point.as_point_nat FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get
module Hacl.Impl.P256.Point

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

open Lib.IntTypes
open Lib.Buffer

open Hacl.Impl.P256.Bignum
open Hacl.Impl.P256.Field
open Hacl.Impl.P256.Constants

module S = Spec.P256
module SM = Hacl.Spec.P256.Montgomery
module FI = Hacl.Impl.P256.Finv

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

///  Create a point

let create_aff_point () =
  create 8ul (u64 0)


let create_point () =
  create 12ul (u64 0)


[@CInline]
let make_base_point p =
  let x = getx p in
  let y = gety p in
  let z = getz p in
  make_g_x x;
  make_g_y y;
  make_fone z


[@CInline]
let make_point_at_inf p =
  let x = getx p in
  let y = gety p in
  let z = getz p in
  make_fzero x;
  make_fone y;
  make_fzero z


///  Check if a point is a point-at-infinity

(* https://crypto.stackexchange.com/questions/43869/point-at-infinity-and-error-handling*)
val lemma_mont_is_point_at_inf: p:S.proj_point{let (_, _, z) = p in z < S.prime} ->
  Lemma (S.is_point_at_inf p == S.is_point_at_inf (from_mont_point p))

let lemma_mont_is_point_at_inf p =
  let px, py, pz = p in
  SM.lemma_from_mont_zero pz


[@CInline]
let is_point_at_inf p =
  let h0 = ST.get () in
  lemma_mont_is_point_at_inf (as_point_nat h0 p);
  let pz = getz p in
  bn_is_zero_mask4 pz
val is_point_at_inf_vartime: p:point -> Stack bool
  (requires fun h -> live h p /\ point_inv h p)
  (ensures  fun h0 r h1 -> modifies0 h0 h1 /\
    r == S.is_point_at_inf (as_point_nat h0 p) /\
    r == S.is_point_at_inf (from_mont_point (as_point_nat h0 p)))
p: Hacl.Impl.P256.Point.point -> FStar.HyperStack.ST.Stack Prims.bool