val lemma_aff_point_mul_endo_split: k:S.qelem -> p:S.aff_point ->
  Lemma (aff_point_mul_endo_split k p == aff_point_mul k p)
let lemma_aff_point_mul_endo_split k p =
  let r10, r20 = scalar_split_lambda k in
  let lambda_p = aff_point_mul_lambda p in
  let r1, p1 = aff_negate_point_and_scalar_cond r10 p in
  let r2, p2 = aff_negate_point_and_scalar_cond r20 lambda_p in
  assert ((r1, p1, r2, p2) == aff_ecmult_endo_split k p);
  let is_high1 = S.scalar_is_high r10 in
  let is_high2 = S.scalar_is_high r20 in

  if is_high1 && is_high2 then begin
    SM.lemma_aff_point_mul_neg r10 p;
    SM.lemma_aff_point_mul_neg r20 lambda_p;
    lemma_aff_point_mul_split_lambda k p end
  else begin
    if is_high1 && not is_high2 then begin
      SM.lemma_aff_point_mul_neg r10 p;
      lemma_aff_point_mul_split_lambda k p end
    else begin
      if not is_high1 && is_high2 then begin
      SM.lemma_aff_point_mul_neg r20 lambda_p;
      lemma_aff_point_mul_split_lambda k p end
      else lemma_aff_point_mul_split_lambda k p
    end
  end
val lemma_aff_point_mul_endo_split: k:S.qelem -> p:S.aff_point ->
  Lemma (aff_point_mul_endo_split k p == aff_point_mul k p)
let lemma_aff_point_mul_endo_split k p =
let r10, r20 = scalar_split_lambda k in
let lambda_p = aff_point_mul_lambda p in
let r1, p1 = aff_negate_point_and_scalar_cond r10 p in
let r2, p2 = aff_negate_point_and_scalar_cond r20 lambda_p in
assert ((r1, p1, r2, p2) == aff_ecmult_endo_split k p);
let is_high1 = S.scalar_is_high r10 in
let is_high2 = S.scalar_is_high r20 in
if is_high1 && is_high2
then
  (SM.lemma_aff_point_mul_neg r10 p;
    SM.lemma_aff_point_mul_neg r20 lambda_p;
    lemma_aff_point_mul_split_lambda k p)
else
  if is_high1 && not is_high2
  then
    (SM.lemma_aff_point_mul_neg r10 p;
      lemma_aff_point_mul_split_lambda k p)
  else
    if not is_high1 && is_high2
    then
      (SM.lemma_aff_point_mul_neg r20 lambda_p;
        lemma_aff_point_mul_split_lambda k p)
    else lemma_aff_point_mul_split_lambda k p
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.qelem Spec.K256.PointOps.aff_point Prims.op_AmpAmp Hacl.Spec.K256.GLV.Lemmas.lemma_aff_point_mul_split_lambda Prims.unit Hacl.Spec.K256.ECSM.Lemmas.lemma_aff_point_mul_neg Prims.bool Prims.op_Negation Spec.K256.PointOps.scalar_is_high Prims._assert Prims.eq2 FStar.Pervasives.Native.tuple4 FStar.Pervasives.Native.Mktuple4 Hacl.Spec.K256.GLV.aff_ecmult_endo_split FStar.Pervasives.Native.tuple2 Hacl.Spec.K256.GLV.aff_negate_point_and_scalar_cond Hacl.Spec.K256.GLV.aff_point_mul_lambda Hacl.Spec.K256.GLV.scalar_split_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))

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_scalar_split_lambda_eval (k:S.qelem) :
  Lemma (let r1, r2 = scalar_split_lambda k in k == S.(r1 +^ r2 *^ lambda))

let lemma_scalar_split_lambda_eval k =
  assert_norm ((minus_lambda + lambda) % S.q = 0);

  let r1, r2 = scalar_split_lambda k in
  assert (r1 = S.(k +^ r2 *^ minus_lambda));
  calc (==) {
    (r1 + (r2 * lambda % S.q)) % S.q;
    (==) { Math.Lemmas.lemma_mod_plus_distr_r r1 (r2 * lambda) S.q }
    (r1 + r2 * lambda) % S.q;
    (==) { }
    ((k + (r2 * minus_lambda % S.q)) % S.q + r2 * lambda) % S.q;
    (==) { Math.Lemmas.lemma_mod_plus_distr_r k (r2 * minus_lambda) S.q }
    ((k + r2 * minus_lambda) % S.q + r2 * lambda) % S.q;
    (==) { Math.Lemmas.lemma_mod_plus_distr_l (k + r2 * minus_lambda) (r2 * lambda) S.q }
    (k + r2 * minus_lambda + r2 * lambda) % S.q;
    (==) { Math.Lemmas.distributivity_add_right r2 minus_lambda lambda }
    (k + r2 * (minus_lambda + lambda)) % S.q;
    (==) { Math.Lemmas.lemma_mod_plus_distr_r k (r2 * (minus_lambda + lambda)) S.q }
    (k + (r2 * (minus_lambda + lambda) % S.q)) % S.q;
    (==) { Math.Lemmas.lemma_mod_mul_distr_r r2 (minus_lambda + lambda) S.q }
    (k + (r2 * ((minus_lambda + lambda) % S.q) % S.q)) % S.q;
    (==) { }
    k % S.q;
    (==) { Math.Lemmas.small_mod k S.q }
    k;
  }

//--------------------------------------------

(**
 Fast computation of [k]P in affine coordinates
*)

val lemma_aff_point_mul_split_lambda: k:S.qelem -> p:S.aff_point ->
  Lemma (let r1, r2 = scalar_split_lambda k in aff_point_mul k p ==
    S.aff_point_add (aff_point_mul r1 p) (aff_point_mul r2 (aff_point_mul_lambda p)))

let lemma_aff_point_mul_split_lambda k p =
  let r1, r2 = scalar_split_lambda k in
  calc (==) {
    aff_point_mul k p;
    (==) { lemma_scalar_split_lambda_eval k }
    aff_point_mul S.(r1 +^ r2 *^ lambda) p;
    (==) { Math.Lemmas.lemma_mod_plus_distr_r r1 (r2 * lambda) S.q }
    aff_point_mul ((r1 + r2 * lambda) % S.q) p;
    (==) { SM.lemma_aff_point_mul_neg_modq (r1 + r2 * lambda) p }
    aff_point_mul (r1 + r2 * lambda) p;
    (==) { SM.lemma_aff_point_mul_neg_mul_add lambda r2 r1 p }
    S.aff_point_add (aff_point_mul r2 (aff_point_mul lambda p)) (aff_point_mul r1 p);
    (==) { lemma_glv_aff p }
    S.aff_point_add (aff_point_mul r2 (aff_point_mul_lambda p)) (aff_point_mul r1 p);
    (==) { LS.aff_point_add_comm_lemma (aff_point_mul r2 (aff_point_mul_lambda p)) (aff_point_mul r1 p) }
    S.aff_point_add (aff_point_mul r1 p) (aff_point_mul r2 (aff_point_mul_lambda p));
  }


val lemma_aff_point_mul_endo_split: k:S.qelem -> p:S.aff_point ->
  Lemma (aff_point_mul_endo_split k p == aff_point_mul k p)
val lemma_aff_point_mul_endo_split: k:S.qelem -> p:S.aff_point ->
  Lemma (aff_point_mul_endo_split k p == aff_point_mul k p)
k: Spec.K256.PointOps.qelem -> p: Spec.K256.PointOps.aff_point
  -> FStar.Pervasives.Lemma
    (ensures Hacl.Spec.K256.GLV.aff_point_mul_endo_split k p == Hacl.Spec.K256.GLV.aff_point_mul k p
    )