val lemma_glv : p:S.proj_point ->
  Lemma (S.to_aff_point (point_mul_lambda p) == aff_point_mul lambda (S.to_aff_point p))
let lemma_glv p =
  let (pX, pY, pZ) = p in
  let (px, py) = S.to_aff_point p in
  assert (px = S.(pX /% pZ) /\ py = S.(pY /% pZ));
  let (qx, qy) = aff_point_mul lambda (px, py) in
  lemma_glv_aff (px, py);
  assert (qx = S.(beta *% px) /\ qy = py);
  assert (qx = S.(beta *% (pX /% pZ)) /\ qy = S.(pY /% pZ));

  let (rX, rY, rZ) = point_mul_lambda p in
  assert (rX = S.(beta *% pX) /\ rY = pY /\ rZ = pZ);
  let (rx, ry) = S.to_aff_point (rX, rY, rZ) in
  assert (rx = S.(rX /% rZ) /\ ry = S.(rY /% rZ));
  assert (rx = S.(beta *% pX /% pZ) /\ ry = S.(pY /% pZ));
  assert (qy = ry);
  // S.(beta *% pX /% rZ) = S.(beta *% (pX /% pZ))
  assert (S.(beta *% pX /% pZ) = S.(beta *% pX *% S.finv pZ));
  assert (S.(beta *% (pX /% pZ)) = S.(beta *% (pX *% S.finv pZ)));
  M.lemma_mul_mod_assoc #S.prime beta pX (S.finv pZ);
  assert (S.(beta *% pX *% S.finv pZ) = S.(beta *% (pX *% S.finv pZ)))
val lemma_glv : p:S.proj_point ->
  Lemma (S.to_aff_point (point_mul_lambda p) == aff_point_mul lambda (S.to_aff_point p))
let lemma_glv p =
let pX, pY, pZ = p in
let px, py = S.to_aff_point p in
assert (px = S.(pX /% pZ) /\ py = S.(pY /% pZ));
let qx, qy = aff_point_mul lambda (px, py) in
lemma_glv_aff (px, py);
assert (qx = S.(beta *% px) /\ qy = py);
assert (qx = S.(beta *% (pX /% pZ)) /\ qy = S.(pY /% pZ));
let rX, rY, rZ = point_mul_lambda p in
assert (rX = S.(beta *% pX) /\ rY = pY /\ rZ = pZ);
let rx, ry = S.to_aff_point (rX, rY, rZ) in
assert (rx = S.(rX /% rZ) /\ ry = S.(rY /% rZ));
assert (rx = S.(beta *% pX /% pZ) /\ ry = S.(pY /% pZ));
assert (qy = ry);
assert (S.(beta *% pX /% pZ) = S.(beta *% pX *% S.finv pZ));
assert (S.(beta *% (pX /% pZ)) = S.(beta *% (pX *% S.finv pZ)));
M.lemma_mul_mod_assoc #S.prime beta pX (S.finv pZ);
assert (S.(beta *% pX *% S.finv pZ) = S.(beta *% (pX *% S.finv pZ)))
Hacl.Spec.K256.GLV.Lemmas.fst.checked
Spec.K256.Lemmas.fsti.checked Spec.K256.fst.checked Spec.Exponentiation.fsti.checked prims.fst.checked Lib.NatMod.fsti.checked Lib.Exponentiation.fsti.checked Hacl.Spec.K256.GLV.fst.checked Hacl.Spec.K256.ECSM.Lemmas.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Calc.fsti.checked
Hacl.Spec.K256.GLV.Lemmas.fst
Spec.K256.PointOps.proj_point Spec.K256.PointOps.felem Prims._assert Prims.b2t Prims.op_Equality Spec.K256.PointOps.op_Star_Percent Hacl.Spec.K256.GLV.beta Spec.K256.PointOps.finv Prims.unit Lib.NatMod.lemma_mul_mod_assoc Spec.K256.PointOps.prime Spec.K256.PointOps.op_Slash_Percent Prims.l_and Spec.K256.PointOps.aff_point Spec.K256.PointOps.to_aff_point FStar.Pervasives.Native.Mktuple3 Hacl.Spec.K256.GLV.point_mul_lambda Hacl.Spec.K256.GLV.Lemmas.lemma_glv_aff FStar.Pervasives.Native.Mktuple2 Hacl.Spec.K256.GLV.aff_point_mul Hacl.Spec.K256.GLV.lambda
module Hacl.Spec.K256.GLV.Lemmas

open FStar.Mul

module M = Lib.NatMod
module LE = Lib.Exponentiation
module SE = Spec.Exponentiation

module S = Spec.K256
module LS = Spec.K256.Lemmas
module SM = Hacl.Spec.K256.ECSM.Lemmas

open Hacl.Spec.K256.GLV

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

// [lambda](px, py) = (beta * px, py)
assume
val lemma_glv_aff : p:S.aff_point -> Lemma (aff_point_mul lambda p == aff_point_mul_lambda p)

val lemma_glv : p:S.proj_point ->
  Lemma (S.to_aff_point (point_mul_lambda p) == aff_point_mul lambda (S.to_aff_point p))
val lemma_glv : p:S.proj_point ->
  Lemma (S.to_aff_point (point_mul_lambda p) == aff_point_mul lambda (S.to_aff_point p))
p: Spec.K256.PointOps.proj_point
  -> FStar.Pervasives.Lemma
    (ensures
      Spec.K256.PointOps.to_aff_point (Hacl.Spec.K256.GLV.point_mul_lambda p) ==
      Hacl.Spec.K256.GLV.aff_point_mul Hacl.Spec.K256.GLV.lambda (Spec.K256.PointOps.to_aff_point p)
    )