val lemma_nat_r43210_mod_prime (c3 d4 d8 t3 r sum0 sum1 sum2 sum3 sum4 sum5 sum6 sum7 sum8: nat) : Lemma
  (requires
    r  = 0x1000003D10 /\
    d4 = (sum3 + r * (sum8 % pow2 64)) / pow2 52 + sum4 + r * pow2 12 * (sum8 / pow2 64) /\
    t3 = (sum3 + r * (sum8 % pow2 64)) % pow2 52 /\
    d8 = (d4 / pow2 52 + sum5) / pow2 52 + sum6 /\
    c3 = sum0 + ((d4 % pow2 52) / pow2 48 + ((d4 / pow2 52 + sum5) % pow2 52) * pow2 4) * (r / pow2 4))
  (ensures
    (c3 + (sum1 + r * d8) * pow2 52 + (sum2 + r * sum7) * pow2 104 +
    t3 * pow2 156 + (d4 % pow2 48) * pow2 208) % S.prime ==
    (sum0 + sum5 * r + (sum1 + sum6 * r) * pow2 52 + (sum2 + r * sum7) * pow2 104 +
    (sum3 + r * sum8) * pow2 156 + sum4 * pow2 208) % S.prime)
let lemma_nat_r43210_mod_prime c3 d4 d8 t3 r sum0 sum1 sum2 sum3 sum4 sum5 sum6 sum7 sum8 =
  let tmp2 = sum3 + r * (sum8 % pow2 64) in
  let tmp1 = d4 / pow2 52 + sum5 in
  let tmp0 = sum0 + (tmp1 % pow2 52 - d4 / pow2 52) * r in
  let d4mod = (d4 % pow2 48) * pow2 208 + (d4 / pow2 48) * 0x1000003D1 in

  calc (==) {
    c3 + (d4 % pow2 48) * pow2 208 + (sum1 + r * d8) * pow2 52;
    (==) { simplify_c3 d4 r sum5; assert_norm (0x1000003D10 / pow2 4 = 0x1000003D1) }
    d4mod + tmp0 + (sum1 + r * d8) * pow2 52;
    (==) { Math.Lemmas.distributivity_add_left sum1 (r * d8) (pow2 52) }
    d4mod + sum0 + (tmp1 % pow2 52 - d4 / pow2 52) * r + sum1 * pow2 52 + r * (tmp1 / pow2 52 + sum6) * pow2 52;
    (==) { Math.Lemmas.distributivity_sub_left (tmp1 % pow2 52) (d4 / pow2 52) r }
    d4mod + sum0 + (tmp1 % pow2 52) * r - d4 / pow2 52 * r + sum1 * pow2 52 + r * (tmp1 / pow2 52 + sum6) * pow2 52;
    (==) { ML.lemma_distr_eucl_mul_add r tmp1 sum6 (pow2 52) }
    d4mod + sum0 + r * (d4 / pow2 52 + sum5) - d4 / pow2 52 * r + sum1 * pow2 52 + r * sum6 * pow2 52;
    (==) { Math.Lemmas.distributivity_add_right r (d4 / pow2 52) sum5 }
    d4mod + sum0 + r * sum5 + sum1 * pow2 52 + r * sum6 * pow2 52;
    (==) { Math.Lemmas.distributivity_add_left sum1 (r * sum6) (pow2 52) }
    d4mod + sum0 + r * sum5 + (sum1 + r * sum6) * pow2 52;
    };

  calc (==) { //t3 * pow2 156 + d4 * pow2 208;
    (tmp2 % pow2 52) * pow2 156 + (tmp2 / pow2 52 + sum4 + r * pow2 12 * (sum8 / pow2 64)) * pow2 208;
    (==) { ML.lemma_distr_pow (tmp2 % pow2 52) (tmp2 / pow2 52 + sum4 + r * pow2 12 * (sum8 / pow2 64)) 52 156 }
    (tmp2 % pow2 52 + (tmp2 / pow2 52 + sum4 + r * pow2 12 * (sum8 / pow2 64)) * pow2 52) * pow2 156;
    (==) { ML.lemma_distr_eucl_mul_add 1 tmp2 (sum4 + r * pow2 12 * (sum8 / pow2 64)) (pow2 52) }
    (tmp2 + (sum4 + r * pow2 12 * (sum8 / pow2 64)) * pow2 52) * pow2 156;
    (==) { ML.lemma_swap_mul3 r (pow2 12) (sum8 / pow2 64) }
    (tmp2 + (sum4 + r * (sum8 / pow2 64) * pow2 12) * pow2 52) * pow2 156;
    (==) { ML.lemma_distr_pow sum4 (r * (sum8 / pow2 64)) 12 52 }
    (sum3 + r * (sum8 % pow2 64) + sum4 * pow2 52 + r * (sum8 / pow2 64) * pow2 64) * pow2 156;
    (==) { ML.lemma_distr_eucl_mul r sum8 (pow2 64) }
    (sum3 + r * sum8 + sum4 * pow2 52) * pow2 156;
    (==) { ML.lemma_distr_pow (sum3 + r * sum8) sum4 52 156 }
    (sum3 + r * sum8) * pow2 156 + sum4 * pow2 208;
    };

  LD.as_nat_mod_prime (sum0 + r * sum5) (sum1 + r * sum6) (sum2 + r * sum7) t3 d4
val lemma_nat_r43210_mod_prime (c3 d4 d8 t3 r sum0 sum1 sum2 sum3 sum4 sum5 sum6 sum7 sum8: nat) : Lemma
  (requires
    r  = 0x1000003D10 /\
    d4 = (sum3 + r * (sum8 % pow2 64)) / pow2 52 + sum4 + r * pow2 12 * (sum8 / pow2 64) /\
    t3 = (sum3 + r * (sum8 % pow2 64)) % pow2 52 /\
    d8 = (d4 / pow2 52 + sum5) / pow2 52 + sum6 /\
    c3 = sum0 + ((d4 % pow2 52) / pow2 48 + ((d4 / pow2 52 + sum5) % pow2 52) * pow2 4) * (r / pow2 4))
  (ensures
    (c3 + (sum1 + r * d8) * pow2 52 + (sum2 + r * sum7) * pow2 104 +
    t3 * pow2 156 + (d4 % pow2 48) * pow2 208) % S.prime ==
    (sum0 + sum5 * r + (sum1 + sum6 * r) * pow2 52 + (sum2 + r * sum7) * pow2 104 +
    (sum3 + r * sum8) * pow2 156 + sum4 * pow2 208) % S.prime)
let lemma_nat_r43210_mod_prime c3 d4 d8 t3 r sum0 sum1 sum2 sum3 sum4 sum5 sum6 sum7 sum8 =
let tmp2 = sum3 + r * (sum8 % pow2 64) in
let tmp1 = d4 / pow2 52 + sum5 in
let tmp0 = sum0 + (tmp1 % pow2 52 - d4 / pow2 52) * r in
let d4mod = (d4 % pow2 48) * pow2 208 + (d4 / pow2 48) * 0x1000003D1 in
calc ( == ) {
  c3 + (d4 % pow2 48) * pow2 208 + (sum1 + r * d8) * pow2 52;
  ( == ) { (simplify_c3 d4 r sum5;
    assert_norm (0x1000003D10 / pow2 4 = 0x1000003D1)) }
  d4mod + tmp0 + (sum1 + r * d8) * pow2 52;
  ( == ) { Math.Lemmas.distributivity_add_left sum1 (r * d8) (pow2 52) }
  d4mod + sum0 + (tmp1 % pow2 52 - d4 / pow2 52) * r + sum1 * pow2 52 +
  (r * (tmp1 / pow2 52 + sum6)) * pow2 52;
  ( == ) { Math.Lemmas.distributivity_sub_left (tmp1 % pow2 52) (d4 / pow2 52) r }
  d4mod + sum0 + (tmp1 % pow2 52) * r - (d4 / pow2 52) * r + sum1 * pow2 52 +
  (r * (tmp1 / pow2 52 + sum6)) * pow2 52;
  ( == ) { ML.lemma_distr_eucl_mul_add r tmp1 sum6 (pow2 52) }
  d4mod + sum0 + r * (d4 / pow2 52 + sum5) - (d4 / pow2 52) * r + sum1 * pow2 52 +
  (r * sum6) * pow2 52;
  ( == ) { Math.Lemmas.distributivity_add_right r (d4 / pow2 52) sum5 }
  d4mod + sum0 + r * sum5 + sum1 * pow2 52 + (r * sum6) * pow2 52;
  ( == ) { Math.Lemmas.distributivity_add_left sum1 (r * sum6) (pow2 52) }
  d4mod + sum0 + r * sum5 + (sum1 + r * sum6) * pow2 52;
};
calc ( == ) {
  (tmp2 % pow2 52) * pow2 156 +
  (tmp2 / pow2 52 + sum4 + (r * pow2 12) * (sum8 / pow2 64)) * pow2 208;
  ( == ) { ML.lemma_distr_pow (tmp2 % pow2 52)
    (tmp2 / pow2 52 + sum4 + (r * pow2 12) * (sum8 / pow2 64))
    52
    156 }
  (tmp2 % pow2 52 + (tmp2 / pow2 52 + sum4 + (r * pow2 12) * (sum8 / pow2 64)) * pow2 52) * pow2 156;
  ( == ) { ML.lemma_distr_eucl_mul_add 1 tmp2 (sum4 + (r * pow2 12) * (sum8 / pow2 64)) (pow2 52) }
  (tmp2 + (sum4 + (r * pow2 12) * (sum8 / pow2 64)) * pow2 52) * pow2 156;
  ( == ) { ML.lemma_swap_mul3 r (pow2 12) (sum8 / pow2 64) }
  (tmp2 + (sum4 + (r * (sum8 / pow2 64)) * pow2 12) * pow2 52) * pow2 156;
  ( == ) { ML.lemma_distr_pow sum4 (r * (sum8 / pow2 64)) 12 52 }
  (sum3 + r * (sum8 % pow2 64) + sum4 * pow2 52 + (r * (sum8 / pow2 64)) * pow2 64) * pow2 156;
  ( == ) { ML.lemma_distr_eucl_mul r sum8 (pow2 64) }
  (sum3 + r * sum8 + sum4 * pow2 52) * pow2 156;
  ( == ) { ML.lemma_distr_pow (sum3 + r * sum8) sum4 52 156 }
  (sum3 + r * sum8) * pow2 156 + sum4 * pow2 208;
};
LD.as_nat_mod_prime (sum0 + r * sum5) (sum1 + r * sum6) (sum2 + r * sum7) t3 d4
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 Hacl.Spec.K256.Field52.Definitions.Lemmas.as_nat_mod_prime Prims.op_Addition FStar.Mul.op_Star Prims.unit FStar.Calc.calc_finish Prims.int Prims.eq2 Prims.op_Modulus Prims.pow2 Prims.op_Division Prims.Cons FStar.Preorder.relation Prims.Nil FStar.Calc.calc_step FStar.Calc.calc_init FStar.Calc.calc_pack Hacl.Spec.K256.MathLemmas.lemma_distr_pow Prims.squash Hacl.Spec.K256.MathLemmas.lemma_distr_eucl_mul_add Hacl.Spec.K256.MathLemmas.lemma_swap_mul3 Hacl.Spec.K256.MathLemmas.lemma_distr_eucl_mul Prims.op_Subtraction FStar.Pervasives.assert_norm Prims.b2t Prims.op_Equality Hacl.Spec.K256.Field52.Lemmas4.simplify_c3 FStar.Math.Lemmas.distributivity_add_left FStar.Math.Lemmas.distributivity_sub_left FStar.Math.Lemmas.distributivity_add_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))

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 lemma_nat_r43210_mod_prime (c3 d4 d8 t3 r sum0 sum1 sum2 sum3 sum4 sum5 sum6 sum7 sum8: nat) : Lemma
  (requires
    r  = 0x1000003D10 /\
    d4 = (sum3 + r * (sum8 % pow2 64)) / pow2 52 + sum4 + r * pow2 12 * (sum8 / pow2 64) /\
    t3 = (sum3 + r * (sum8 % pow2 64)) % pow2 52 /\
    d8 = (d4 / pow2 52 + sum5) / pow2 52 + sum6 /\
    c3 = sum0 + ((d4 % pow2 52) / pow2 48 + ((d4 / pow2 52 + sum5) % pow2 52) * pow2 4) * (r / pow2 4))
  (ensures
    (c3 + (sum1 + r * d8) * pow2 52 + (sum2 + r * sum7) * pow2 104 +
    t3 * pow2 156 + (d4 % pow2 48) * pow2 208) % S.prime ==
    (sum0 + sum5 * r + (sum1 + sum6 * r) * pow2 52 + (sum2 + r * sum7) * pow2 104 +
    (sum3 + r * sum8) * pow2 156 + sum4 * pow2 208) % S.prime)
val lemma_nat_r43210_mod_prime (c3 d4 d8 t3 r sum0 sum1 sum2 sum3 sum4 sum5 sum6 sum7 sum8: nat) : Lemma
  (requires
    r  = 0x1000003D10 /\
    d4 = (sum3 + r * (sum8 % pow2 64)) / pow2 52 + sum4 + r * pow2 12 * (sum8 / pow2 64) /\
    t3 = (sum3 + r * (sum8 % pow2 64)) % pow2 52 /\
    d8 = (d4 / pow2 52 + sum5) / pow2 52 + sum6 /\
    c3 = sum0 + ((d4 % pow2 52) / pow2 48 + ((d4 / pow2 52 + sum5) % pow2 52) * pow2 4) * (r / pow2 4))
  (ensures
    (c3 + (sum1 + r * d8) * pow2 52 + (sum2 + r * sum7) * pow2 104 +
    t3 * pow2 156 + (d4 % pow2 48) * pow2 208) % S.prime ==
    (sum0 + sum5 * r + (sum1 + sum6 * r) * pow2 52 + (sum2 + r * sum7) * pow2 104 +
    (sum3 + r * sum8) * pow2 156 + sum4 * pow2 208) % S.prime)

    c3: Prims.nat ->
    d4: Prims.nat ->
    d8: Prims.nat ->
    t3: Prims.nat ->
    r: Prims.nat ->
    sum0: Prims.nat ->
    sum1: Prims.nat ->
    sum2: Prims.nat ->
    sum3: Prims.nat ->
    sum4: Prims.nat ->
    sum5: Prims.nat ->
    sum6: Prims.nat ->
    sum7: Prims.nat ->
    sum8: Prims.nat
  -> FStar.Pervasives.Lemma
      (requires
        r = 0x1000003D10 /\
        d4 =
        (sum3 + r * (sum8 % Prims.pow2 64)) / Prims.pow2 52 + sum4 +
        (r * Prims.pow2 12) * (sum8 / Prims.pow2 64) /\
        t3 = (sum3 + r * (sum8 % Prims.pow2 64)) % Prims.pow2 52 /\
        d8 = (d4 / Prims.pow2 52 + sum5) / Prims.pow2 52 + sum6 /\
        c3 =
        sum0 +
        (d4 % Prims.pow2 52 / Prims.pow2 48 +
          ((d4 / Prims.pow2 52 + sum5) % Prims.pow2 52) * Prims.pow2 4) *
        (r / Prims.pow2 4))
      (ensures
        (c3 + (sum1 + r * d8) * Prims.pow2 52 + (sum2 + r * sum7) * Prims.pow2 104 +
          t3 * Prims.pow2 156 +
          (d4 % Prims.pow2 48) * Prims.pow2 208) %
        Spec.K256.PointOps.prime ==
        (sum0 + sum5 * r + (sum1 + sum6 * r) * Prims.pow2 52 + (sum2 + r * sum7) * Prims.pow2 104 +
          (sum3 + r * sum8) * Prims.pow2 156 +
          sum4 * Prims.pow2 208) %
        Spec.K256.PointOps.prime)