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;
  }
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;
}
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 FStar.Calc.calc_finish Prims.int Prims.eq2 Prims.op_Modulus Prims.op_Addition FStar.Mul.op_Star Hacl.Spec.K256.GLV.lambda Spec.K256.PointOps.q Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step Hacl.Spec.K256.GLV.minus_lambda FStar.Calc.calc_init FStar.Calc.calc_pack FStar.Math.Lemmas.lemma_mod_plus_distr_r Prims.squash FStar.Math.Lemmas.lemma_mod_plus_distr_l FStar.Math.Lemmas.distributivity_add_right FStar.Math.Lemmas.lemma_mod_mul_distr_r FStar.Math.Lemmas.small_mod Prims._assert Prims.b2t Prims.op_Equality Spec.K256.PointOps.op_Plus_Hat Spec.K256.PointOps.op_Star_Hat FStar.Pervasives.Native.tuple2 Hacl.Spec.K256.GLV.scalar_split_lambda FStar.Pervasives.assert_norm
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))
val lemma_scalar_split_lambda_eval (k:S.qelem) :
  Lemma (let r1, r2 = scalar_split_lambda k in k == S.(r1 +^ r2 *^ lambda))
k: Spec.K256.PointOps.qelem
  -> FStar.Pervasives.Lemma
    (ensures
      (let _ = Hacl.Spec.K256.GLV.scalar_split_lambda k in
        (let FStar.Pervasives.Native.Mktuple2 #_ #_ r1 r2 = _ in
          k == r1 +^ r2 *^ Hacl.Spec.K256.GLV.lambda)
        <:
        Type0))