val eea_pow2_odd_k_lemma_d: a:pos -> n:pos -> k1:pos -> Lemma
  (requires n * k1 % pow2 (a - 1) == 1 /\ n % 2 = 1)
  (ensures (let d = n * k1 / pow2 (a - 1) in
    d % 2 == (if n * k1 % pow2 a < pow2 (a - 1) then 0 else 1)))
let eea_pow2_odd_k_lemma_d a n k1 =
  let d = n * k1 / pow2 (a - 1) in
  Math.Lemmas.pow2_modulo_division_lemma_1 (n * k1) (a - 1) a;
  assert (d % 2 == n * k1 % pow2 a / pow2 (a - 1));
  if d % 2 = 0 then begin
    Math.Lemmas.small_division_lemma_2 (n * k1 % pow2 a) (pow2 (a - 1));
    assert (n * k1 % pow2 a < pow2 (a - 1));
    () end
val eea_pow2_odd_k_lemma_d: a:pos -> n:pos -> k1:pos -> Lemma
  (requires n * k1 % pow2 (a - 1) == 1 /\ n % 2 = 1)
  (ensures (let d = n * k1 / pow2 (a - 1) in
    d % 2 == (if n * k1 % pow2 a < pow2 (a - 1) then 0 else 1)))
let eea_pow2_odd_k_lemma_d a n k1 =
let d = n * k1 / pow2 (a - 1) in
Math.Lemmas.pow2_modulo_division_lemma_1 (n * k1) (a - 1) a;
assert (d % 2 == n * k1 % pow2 a / pow2 (a - 1));
if d % 2 = 0
then
  (Math.Lemmas.small_division_lemma_2 (n * k1 % pow2 a) (pow2 (a - 1));
    assert (n * k1 % pow2 a < pow2 (a - 1));
    ())
Hacl.Spec.Montgomery.Lemmas.fst.checked
prims.fst.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.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.Montgomery.Lemmas.fst
Prims.pos Prims.op_Equality Prims.int Prims.op_Modulus Prims.unit Prims._assert Prims.b2t Prims.op_LessThan FStar.Mul.op_Star Prims.pow2 Prims.op_Subtraction FStar.Math.Lemmas.small_division_lemma_2 Prims.bool Prims.eq2 Prims.op_Division FStar.Math.Lemmas.pow2_modulo_division_lemma_1
module Hacl.Spec.Montgomery.Lemmas

open FStar.Mul

open Lib.IntTypes
open Lib.LoopCombinators


(**
https://members.loria.fr/PZimmermann/mca/mca-cup-0.5.9.pdf
https://eprint.iacr.org/2011/239.pdf
https://eprint.iacr.org/2017/1057.pdf *)

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

val eea_pow2_odd_k_lemma_d: a:pos -> n:pos -> k1:pos -> Lemma
  (requires n * k1 % pow2 (a - 1) == 1 /\ n % 2 = 1)
  (ensures (let d = n * k1 / pow2 (a - 1) in
    d % 2 == (if n * k1 % pow2 a < pow2 (a - 1) then 0 else 1)))
val eea_pow2_odd_k_lemma_d: a:pos -> n:pos -> k1:pos -> Lemma
  (requires n * k1 % pow2 (a - 1) == 1 /\ n % 2 = 1)
  (ensures (let d = n * k1 / pow2 (a - 1) in
    d % 2 == (if n * k1 % pow2 a < pow2 (a - 1) then 0 else 1)))
a: Prims.pos -> n: Prims.pos -> k1: Prims.pos
  -> FStar.Pervasives.Lemma (requires n * k1 % Prims.pow2 (a - 1) == 1 /\ n % 2 = 1)
      (ensures
        (let d = n * k1 / Prims.pow2 (a - 1) in
          d % 2 ==
          (match n * k1 % Prims.pow2 a < Prims.pow2 (a - 1) with
            | true -> 0
            | _ -> 1)))