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_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;
}
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 Prims.op_Addition FStar.Mul.op_Star Prims.pow2 Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step Prims.op_Division Prims.op_Modulus FStar.Calc.calc_init FStar.Calc.calc_pack Hacl.Spec.K256.Field52.Lemmas4.lemma_nat_r432 Prims.squash Hacl.Spec.K256.MathLemmas.lemma_distr_eucl_mul Hacl.Spec.K256.MathLemmas.lemma_distr_eucl FStar.Math.Lemmas.distributivity_add_left Hacl.Spec.K256.MathLemmas.lemma_distr_pow_pow
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)
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)

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