val to_aff_point_negate_lemma (p:proj_point) :
  Lemma (to_aff_point (point_negate p) == aff_point_negate (to_aff_point p))
let to_aff_point_negate_lemma p =
  let px, py, pz = p in
  let qx, qy = to_aff_point (point_negate p) in
  assert (qx == px /% pz /\ qy == (- py) % prime /% pz);
  let ax, ay = aff_point_negate (to_aff_point p) in
  assert (ax == px /% pz /\ ay == (- py /% pz) % prime);
  let pz_inv = M.pow_mod #prime pz (prime - 2) in

  calc (==) { // (-py) % prime /% pz;
    ((- py) % prime * pz_inv) % prime;
    (==) { Math.Lemmas.lemma_mod_mul_distr_l (- py) pz_inv prime }
    (- py * pz_inv) % prime;
    (==) { Math.Lemmas.neg_mul_left py pz_inv }
    (- (py * pz_inv)) % prime;
    (==) { Math.Lemmas.lemma_mod_sub_distr 0 (py * pz_inv) prime }
    (- (py * pz_inv) % prime) % prime; // (- py /% pz) % prime;
  }
val to_aff_point_negate_lemma (p:proj_point) :
  Lemma (to_aff_point (point_negate p) == aff_point_negate (to_aff_point p))
let to_aff_point_negate_lemma p =
let px, py, pz = p in
let qx, qy = to_aff_point (point_negate p) in
assert (qx == px /% pz /\ qy == (- py) % prime /% pz);
let ax, ay = aff_point_negate (to_aff_point p) in
assert (ax == px /% pz /\ ay == (- py /% pz) % prime);
let pz_inv = M.pow_mod #prime pz (prime - 2) in
calc ( == ) {
  (((- py) % prime) * pz_inv) % prime;
  ( == ) { Math.Lemmas.lemma_mod_mul_distr_l (- py) pz_inv prime }
  (- py * pz_inv) % prime;
  ( == ) { Math.Lemmas.neg_mul_left py pz_inv }
  (- (py * pz_inv)) % prime;
  ( == ) { Math.Lemmas.lemma_mod_sub_distr 0 (py * pz_inv) prime }
  (- (py * pz_inv) % prime) % prime;
}
Spec.K256.Lemmas.fst.checked
Spec.K256.PointOps.fst.checked prims.fst.checked Lib.NatMod.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Math.Euclid.fsti.checked FStar.Calc.fsti.checked
Spec.K256.Lemmas.fst
Spec.K256.PointOps.proj_point Spec.K256.PointOps.felem FStar.Calc.calc_finish Prims.int Prims.eq2 Prims.op_Modulus FStar.Mul.op_Star Prims.op_Minus Spec.K256.PointOps.prime Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step FStar.Calc.calc_init FStar.Calc.calc_pack FStar.Math.Lemmas.lemma_mod_mul_distr_l Prims.squash FStar.Math.Lemmas.neg_mul_left FStar.Math.Lemmas.lemma_mod_sub_distr Lib.NatMod.nat_mod Lib.NatMod.pow_mod Prims.op_Subtraction Prims._assert Prims.l_and Spec.K256.PointOps.op_Slash_Percent Spec.K256.PointOps.aff_point Spec.K256.PointOps.aff_point_negate Spec.K256.PointOps.to_aff_point Spec.K256.PointOps.point_negate
module Spec.K256.Lemmas

open FStar.Mul

open Spec.K256.PointOps

module Euclid = FStar.Math.Euclid
module M = Lib.NatMod

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

assume val prime_lemma: unit -> Lemma (Euclid.is_prime prime)

let lemma_aff_is_point_at_inf p =
  prime_lemma ();
  let (px, py, pz) = p in
  M.lemma_div_mod_prime_is_zero #prime px pz;
  M.lemma_div_mod_prime_is_zero #prime py pz


let lemma_proj_aff_id p =
  let (px, py) = p in
  let (pX, pY, pZ) = to_proj_point p in
  assert (pX = px /\ pY = pY /\ pZ = one);
  let (rx, ry) = to_aff_point (pX, pY, pZ) in
  assert (rx = (pX /% pZ) /\ ry = (pY /% pZ));
  M.lemma_div_mod_prime_one #prime pX;
  M.lemma_div_mod_prime_one #prime pY;
  assert (rx = pX /\ ry = pY)

let aff_point_at_inf_lemma p = ()

let aff_point_add_assoc_lemma p q s = admit()

let aff_point_add_comm_lemma p q = admit()

let aff_point_negate_lemma p =
  let p_neg = aff_point_negate p in
  let px, py = p in
  let qx, qy = p_neg in
  assert (qx = px /\ qy = (-py) % prime);
  assert (aff_point_add p_neg p == aff_point_at_inf)


let to_aff_point_at_infinity_lemma () =
  let px, py = to_aff_point point_at_inf in
  assert (px == zero /% zero /\ py == one /% zero);
  assert (px == zero *% M.pow_mod #prime zero (prime - 2));
  M.lemma_pow_mod #prime zero (prime - 2);
  assert (px == zero *% (M.pow zero (prime - 2) % prime));
  M.lemma_pow_zero (prime - 2);
  assert (px == zero /\ py == zero)

let to_aff_point_add_lemma p q = admit()

let to_aff_point_double_lemma p = admit()
val to_aff_point_negate_lemma (p:proj_point) :
  Lemma (to_aff_point (point_negate p) == aff_point_negate (to_aff_point p))
p: Spec.K256.PointOps.proj_point
  -> FStar.Pervasives.Lemma
    (ensures
      Spec.K256.PointOps.to_aff_point (Spec.K256.PointOps.point_negate p) ==
      Spec.K256.PointOps.aff_point_negate (Spec.K256.PointOps.to_aff_point p))