val make_g: g:point -> Stack unit
  (requires fun h -> live h g)
  (ensures  fun h0 _ h1 -> modifies (loc g) h0 h1 /\
    point_inv h1 g /\ point_eval h1 g == S.g)
let make_g g =
  let gx, gy, gz = getx g, gety g, getz g in

  [@inline_let]
  let x =
   (u64 0x2815b16f81798,
    u64 0xdb2dce28d959f,
    u64 0xe870b07029bfc,
    u64 0xbbac55a06295c,
    u64 0x79be667ef9dc) in

  assert_norm (0x79be667ef9dc < max48);
  assert_norm (0xe1108a8fd17b4 < max52);
  assert_norm (S.g_x == as_nat5 x);
  make_u52_5 gx x;

  [@inline_let]
  let y =
   (u64 0x7d08ffb10d4b8,
    u64 0x48a68554199c4,
    u64 0xe1108a8fd17b4,
    u64 0xc4655da4fbfc0,
    u64 0x483ada7726a3) in

  assert_norm (S.g_y == as_nat5 y);
  make_u52_5 gy y;

  set_one gz
val make_g: g:point -> Stack unit
  (requires fun h -> live h g)
  (ensures  fun h0 _ h1 -> modifies (loc g) h0 h1 /\
    point_inv h1 g /\ point_eval h1 g == S.g)
let make_g g =
let gx, gy, gz = getx g, gety g, getz g in
[@@ inline_let ]let x =
  (u64 0x2815b16f81798,
    u64 0xdb2dce28d959f,
    u64 0xe870b07029bfc,
    u64 0xbbac55a06295c,
    u64 0x79be667ef9dc)
in
assert_norm (0x79be667ef9dc < max48);
assert_norm (0xe1108a8fd17b4 < max52);
assert_norm (S.g_x == as_nat5 x);
make_u52_5 gx x;
[@@ inline_let ]let y =
  (u64 0x7d08ffb10d4b8,
    u64 0x48a68554199c4,
    u64 0xe1108a8fd17b4,
    u64 0xc4655da4fbfc0,
    u64 0x483ada7726a3)
in
assert_norm (S.g_y == as_nat5 y);
make_u52_5 gy y;
set_one gz
Hacl.Impl.K256.Point.fst.checked
Spec.K256.Lemmas.fsti.checked Spec.K256.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.K256.Field52.Lemmas.fsti.checked Hacl.Spec.K256.Field52.fst.checked Hacl.K256.Field.fsti.checked Hacl.Impl.K256.Finv.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
Hacl.Impl.K256.Point.fst
Hacl.Impl.K256.Point.point Hacl.K256.Field.felem Hacl.K256.Field.set_one Prims.unit Hacl.K256.Field.make_u52_5 FStar.Pervasives.assert_norm Prims.eq2 Prims.nat Spec.K256.PointOps.g_y Hacl.Spec.K256.Field52.Definitions.as_nat5 FStar.Pervasives.Native.tuple5 Lib.IntTypes.int_t Lib.IntTypes.U64 Lib.IntTypes.SEC FStar.Pervasives.Native.Mktuple5 Lib.IntTypes.uint64 Lib.IntTypes.u64 Spec.K256.PointOps.g_x Prims.b2t Prims.op_LessThan Hacl.Spec.K256.Field52.Definitions.max52 Hacl.Spec.K256.Field52.Definitions.max48 FStar.Pervasives.Native.tuple3 FStar.Pervasives.Native.Mktuple3 Hacl.Impl.K256.Point.getz Hacl.Impl.K256.Point.gety Hacl.Impl.K256.Point.getx
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 BSeq = Lib.ByteSequence

module S = Spec.K256
module SL = Spec.K256.Lemmas
module BI = Hacl.Spec.K256.Field52
module BL = Hacl.Spec.K256.Field52.Lemmas

open Hacl.K256.Field
open Hacl.Impl.K256.Finv

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

///  Create a point

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


let create_point () =
  create (3ul *! 5ul) (u64 0)


let make_point_at_inf p =
  SL.to_aff_point_at_infinity_lemma ();
  let px, py, pz = getx p, gety p, getz p in
  set_zero px;
  set_one py;
  set_zero pz
val make_g: g:point -> Stack unit
  (requires fun h -> live h g)
  (ensures  fun h0 _ h1 -> modifies (loc g) h0 h1 /\
    point_inv h1 g /\ point_eval h1 g == S.g)
g: Hacl.Impl.K256.Point.point -> FStar.HyperStack.ST.Stack Prims.unit