val simplify_c3 (d4 r sum5:nat) : Lemma
  (requires r % pow2 4 = 0)
  (ensures (let k = (d4 / pow2 52 + sum5) % pow2 52 in
    ((d4 % pow2 52) / pow2 48 + k * pow2 4) * (r / pow2 4) ==
    (d4 / pow2 48) * (r / pow2 4) + (k - (d4 / pow2 52)) * r))
let simplify_c3 d4 r sum5 =
  let k = (d4 / pow2 52 + sum5) % pow2 52 in

  calc (==) { //simplify c3
    ((d4 % pow2 52) / pow2 48 + k * pow2 4) * (r / pow2 4);
    (==) { Math.Lemmas.pow2_modulo_division_lemma_1 d4 48 52 }
    ((d4 / pow2 48) % pow2 4 + k * pow2 4) * (r / pow2 4);
    (==) { Math.Lemmas.euclidean_division_definition (d4 / pow2 48) (pow2 4) }
    (d4 / pow2 48 - (d4 / pow2 48 / pow2 4) * pow2 4 + k * pow2 4) * (r / pow2 4);
    (==) { Math.Lemmas.division_multiplication_lemma d4 (pow2 48) (pow2 4); Math.Lemmas.pow2_plus 48 4 }
    (d4 / pow2 48 - (d4 / pow2 52) * pow2 4 + k * pow2 4) * (r / pow2 4);
    (==) { Math.Lemmas.distributivity_sub_left k (d4 / pow2 52) (pow2 4) }
    (d4 / pow2 48 + (k - d4 / pow2 52) * pow2 4) * (r / pow2 4);
    (==) { Math.Lemmas.distributivity_add_left (d4 / pow2 48) ((k - d4 / pow2 52) * pow2 4) (r / pow2 4) }
    (d4 / pow2 48) * (r / pow2 4) + (k - d4 / pow2 52) * pow2 4 * (r / pow2 4);
    (==) { Math.Lemmas.paren_mul_right (k - d4 / pow2 52) (pow2 4) (r / pow2 4); Math.Lemmas.div_exact_r r (pow2 4) }
    (d4 / pow2 48) * (r / pow2 4) + (k - d4 / pow2 52) * r;
  }
val simplify_c3 (d4 r sum5:nat) : Lemma
  (requires r % pow2 4 = 0)
  (ensures (let k = (d4 / pow2 52 + sum5) % pow2 52 in
    ((d4 % pow2 52) / pow2 48 + k * pow2 4) * (r / pow2 4) ==
    (d4 / pow2 48) * (r / pow2 4) + (k - (d4 / pow2 52)) * r))
let simplify_c3 d4 r sum5 =
let k = (d4 / pow2 52 + sum5) % pow2 52 in
calc ( == ) {
  ((d4 % pow2 52) / pow2 48 + k * pow2 4) * (r / pow2 4);
  ( == ) { Math.Lemmas.pow2_modulo_division_lemma_1 d4 48 52 }
  ((d4 / pow2 48) % pow2 4 + k * pow2 4) * (r / pow2 4);
  ( == ) { Math.Lemmas.euclidean_division_definition (d4 / pow2 48) (pow2 4) }
  (d4 / pow2 48 - (d4 / pow2 48 / pow2 4) * pow2 4 + k * pow2 4) * (r / pow2 4);
  ( == ) { (Math.Lemmas.division_multiplication_lemma d4 (pow2 48) (pow2 4);
    Math.Lemmas.pow2_plus 48 4) }
  (d4 / pow2 48 - (d4 / pow2 52) * pow2 4 + k * pow2 4) * (r / pow2 4);
  ( == ) { Math.Lemmas.distributivity_sub_left k (d4 / pow2 52) (pow2 4) }
  (d4 / pow2 48 + (k - d4 / pow2 52) * pow2 4) * (r / pow2 4);
  ( == ) { Math.Lemmas.distributivity_add_left (d4 / pow2 48)
    ((k - d4 / pow2 52) * pow2 4)
    (r / pow2 4) }
  (d4 / pow2 48) * (r / pow2 4) + ((k - d4 / pow2 52) * pow2 4) * (r / pow2 4);
  ( == ) { (Math.Lemmas.paren_mul_right (k - d4 / pow2 52) (pow2 4) (r / pow2 4);
    Math.Lemmas.div_exact_r r (pow2 4)) }
  (d4 / pow2 48) * (r / pow2 4) + (k - d4 / pow2 52) * r;
}
Hacl.Spec.K256.Field52.Lemmas4.fst.checked
Spec.K256.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Hacl.Spec.K256.MathLemmas.fst.checked Hacl.Spec.K256.Field52.Definitions.Lemmas.fst.checked Hacl.Spec.K256.Field52.Definitions.fst.checked Hacl.Spec.K256.Field52.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Calc.fsti.checked
Hacl.Spec.K256.Field52.Lemmas4.fst
Prims.nat FStar.Calc.calc_finish Prims.int Prims.eq2 FStar.Mul.op_Star Prims.op_Addition Prims.op_Division Prims.op_Modulus Prims.pow2 Prims.op_Subtraction Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step FStar.Calc.calc_init FStar.Calc.calc_pack FStar.Math.Lemmas.pow2_modulo_division_lemma_1 Prims.squash FStar.Math.Lemmas.euclidean_division_definition FStar.Math.Lemmas.pow2_plus FStar.Math.Lemmas.division_multiplication_lemma FStar.Math.Lemmas.distributivity_sub_left FStar.Math.Lemmas.distributivity_add_left FStar.Math.Lemmas.div_exact_r FStar.Math.Lemmas.paren_mul_right
module Hacl.Spec.K256.Field52.Lemmas4

open FStar.Mul
open Lib.IntTypes

module S = Spec.K256

include Hacl.Spec.K256.Field52.Definitions
include Hacl.Spec.K256.Field52

module ML = Hacl.Spec.K256.MathLemmas
module LD = Hacl.Spec.K256.Field52.Definitions.Lemmas

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

val lemma_nat_r432 (r2 r3 r4 c9 c11 d4 d11 t3 r:nat) : Lemma
  (requires
    r2 = c9 % pow2 52 /\ c11 = c9 / pow2 52 + r * pow2 12 * d11 + t3 /\
    r3 = c11 % pow2 52 /\ r4 = c11 / pow2 52 + (d4 % pow2 52) % pow2 48)
  (ensures
    (r4 * pow2 52 + r3) * pow2 52 + r2 =
    c9 + r * d11 * pow2 64 + t3 * pow2 52 + (d4 % pow2 48) * pow2 104)

let lemma_nat_r432 r2 r3 r4 c9 c11 d4 d11 t3 r =
  let k = d4 % pow2 48 in
  calc (==) {
    (r4 * pow2 52 + r3) * pow2 52 + r2;
    (==) { Math.Lemmas.pow2_modulo_modulo_lemma_1 d4 48 52 }
    ((c11 / pow2 52 + k) * pow2 52 + c11 % pow2 52) * pow2 52 + r2;
    (==) { ML.lemma_distr_eucl c11 k }
    (c9 / pow2 52 + r * pow2 12 * d11 + t3 + k * pow2 52) * pow2 52 + c9 % pow2 52;
    (==) { ML.lemma_distr_eucl c9 (r * pow2 12 * d11 + t3 + k * pow2 52) }
    c9 + (r * pow2 12 * d11 + t3 + k * pow2 52) * pow2 52;
    (==) { ML.lemma_distr_pow (r * pow2 12 * d11 + t3) k 52 52 }
    c9 + (r * pow2 12 * d11 + t3) * pow2 52 + k * pow2 104;
    (==) { ML.lemma_swap_mul3 r (pow2 12) d11 }
    c9 + (r * d11 * pow2 12 + t3) * pow2 52 + k * pow2 104;
    (==) { ML.lemma_distr_pow t3 (r * d11) 12 52 }
    c9 + r * d11 * pow2 64 + t3 * pow2 52 + k * pow2 104;
    }


val lemma_nat_r4321 (r1 r2 r3 r4 c6 c9 c11 d4 d10 d11 t3 r sum2:nat) : Lemma
  (requires
    d11 = d10 / pow2 64 /\
    r1 = c6 % pow2 52 /\ c9 = c6 / pow2 52 + sum2 + r * (d10 % pow2 64) /\
    r2 = c9 % pow2 52 /\ c11 = c9 / pow2 52 + r * pow2 12 * d11 + t3 /\
    r3 = c11 % pow2 52 /\ r4 = c11 / pow2 52 + (d4 % pow2 52) % pow2 48)
  (ensures
    ((r4 * pow2 52 + r3) * pow2 52 + r2) * pow2 52 + r1 =
    c6 + sum2 * pow2 52 + r * d10 * pow2 52 + t3 * pow2 104 + (d4 % pow2 48) * pow2 156)

let lemma_nat_r4321 r1 r2 r3 r4 c6 c9 c11 d4 d10 d11 t3 r sum2 =
  let k = d4 % pow2 48 in
  let tmp1 = t3 * pow2 52 + k * pow2 104 in

  calc (==) {
    ((r4 * pow2 52 + r3) * pow2 52 + r2) * pow2 52 + r1;
    (==) { lemma_nat_r432 r2 r3 r4 c9 c11 d4 d11 t3 r }
    (c9 + r * d11 * pow2 64 + tmp1) * pow2 52 + r1;
    (==) { }
    (c6 / pow2 52 + sum2 + r * (d10 % pow2 64) + r * d11 * pow2 64 + tmp1) * pow2 52 + c6 % pow2 52;
    (==) { ML.lemma_distr_eucl_mul r d10 (pow2 64) }
    (c6 / pow2 52 + sum2 + r * d10 + tmp1) * pow2 52 + c6 % pow2 52;
    (==) { ML.lemma_distr_eucl c6 (sum2 + r * d10 + tmp1) }
    c6 + (sum2 + r * d10 + tmp1) * pow2 52;
    (==) { Math.Lemmas.distributivity_add_left (sum2 + r * d10) tmp1 (pow2 52) }
    c6 + (sum2 + r * d10) * pow2 52 + tmp1 * pow2 52;
    (==) { Math.Lemmas.distributivity_add_left sum2 (r * d10) (pow2 52) }
    c6 + sum2 * pow2 52 + r * d10 * pow2 52 + tmp1 * pow2 52;
    (==) { ML.lemma_distr_pow_pow t3 52 k 104 52 }
    c6 + sum2 * pow2 52 + r * d10 * pow2 52 + t3 * pow2 104 + k * pow2 156;
    }


val lemma_nat_r43210 (r0 r1 r2 r3 r4 c3 c6 c9 c11 d4 d8 d10 d11 t3 r sum1 sum2 sum7:nat) : Lemma
  (requires
    d10 == d8 / pow2 52 + sum7 /\
    r0 = c3 % pow2 52 /\ c6 = c3 / pow2 52 + sum1 + d8 % pow2 52 * r /\
    d11 = d10 / pow2 64 /\
    r1 = c6 % pow2 52 /\ c9 = c6 / pow2 52 + sum2 + r * (d10 % pow2 64) /\
    r2 = c9 % pow2 52 /\ c11 = c9 / pow2 52 + r * pow2 12 * d11 + t3 /\
    r3 = c11 % pow2 52 /\ r4 = c11 / pow2 52 + (d4 % pow2 52) % pow2 48)
  (ensures
    r0 + r1 * pow52 + r2 * pow104 + r3 * pow156 + r4 * pow208 =
    c3 + (sum1 + r * d8) * pow2 52 + (sum2 + r * sum7) * pow2 104 + t3 * pow2 156 + (d4 % pow2 48) * pow2 208)

let lemma_nat_r43210 r0 r1 r2 r3 r4 c3 c6 c9 c11 d4 d8 d10 d11 t3 r sum1 sum2 sum7 =
  let k = d4 % pow2 48 in
  let tmp1 = sum2 * pow2 52 + t3 * pow2 104 + k * pow2 156 in

  calc (==) { // tmp1 * pow2 52
    (sum2 * pow2 52 + t3 * pow2 104 + k * pow2 156) * pow2 52;
    (==) { ML.lemma_distr_pow (sum2 * pow2 52 + t3 * pow2 104) k 156 52 }
    (sum2 * pow2 52 + t3 * pow2 104) * pow2 52 + k * pow2 208;
    (==) { ML.lemma_distr_pow_pow sum2 52 t3 104 52 }
    sum2 * pow2 104 + t3 * pow2 156 + k * pow2 208;
  };

  calc (==) {
    r0 + r1 * pow52 + r2 * pow104 + r3 * pow156 + r4 * pow208;
    (==) { ML.lemma_as_nat_horner r0 r1 r2 r3 r4 }
    (((r4 * pow2 52 + r3) * pow2 52 + r2) * pow2 52 + r1) * pow2 52 + r0;
    (==) { lemma_nat_r4321 r1 r2 r3 r4 c6 c9 c11 d4 d10 d11 t3 r sum2 }
    (c3 / pow2 52 + sum1 + d8 % pow2 52 * r + r * (d8 / pow2 52 + sum7) * pow2 52 + tmp1) * pow2 52 + c3 % pow2 52;
    (==) { ML.lemma_distr_eucl_mul_add r d8 sum7 (pow2 52) }
    (c3 / pow2 52 + sum1 + r * d8 + r * sum7 * pow2 52 + tmp1) * pow2 52 + c3 % pow2 52;
    (==) { ML.lemma_distr_eucl c3 (sum1 + r * d8 + r * sum7 * pow2 52 + tmp1) }
    c3 + (sum1 + r * d8 + r * sum7 * pow2 52 + tmp1) * pow2 52;
    (==) { ML.lemma_distr_pow (sum1 + r * d8 + tmp1) (r * sum7) 52 52 }
    c3 + (sum1 + r * d8 + tmp1) * pow2 52 + r * sum7 * pow2 104;
    (==) { Math.Lemmas.distributivity_add_left (sum1 + r * d8) tmp1 (pow2 52) }
    c3 + (sum1 + r * d8) * pow2 52 + sum2 * pow2 104 + t3 * pow2 156 + k * pow2 208 + r * sum7 * pow2 104;
    (==) { Math.Lemmas.distributivity_add_left sum2 (r * sum7) (pow2 104) }
    c3 + (sum1 + r * d8) * pow2 52 + (sum2 + r * sum7) * pow2 104 + t3 * pow2 156 + k * pow2 208;
    }


val simplify_c3 (d4 r sum5:nat) : Lemma
  (requires r % pow2 4 = 0)
  (ensures (let k = (d4 / pow2 52 + sum5) % pow2 52 in
    ((d4 % pow2 52) / pow2 48 + k * pow2 4) * (r / pow2 4) ==
    (d4 / pow2 48) * (r / pow2 4) + (k - (d4 / pow2 52)) * r))
val simplify_c3 (d4 r sum5:nat) : Lemma
  (requires r % pow2 4 = 0)
  (ensures (let k = (d4 / pow2 52 + sum5) % pow2 52 in
    ((d4 % pow2 52) / pow2 48 + k * pow2 4) * (r / pow2 4) ==
    (d4 / pow2 48) * (r / pow2 4) + (k - (d4 / pow2 52)) * r))
d4: Prims.nat -> r: Prims.nat -> sum5: Prims.nat
  -> FStar.Pervasives.Lemma (requires r % Prims.pow2 4 = 0)
      (ensures
        (let k = (d4 / Prims.pow2 52 + sum5) % Prims.pow2 52 in
          (d4 % Prims.pow2 52 / Prims.pow2 48 + k * Prims.pow2 4) * (r / Prims.pow2 4) ==
          (d4 / Prims.pow2 48) * (r / Prims.pow2 4) + (k - d4 / Prims.pow2 52) * r))