val lemma_sum_a1b
      (a0 a1:nat64)
      (a0b:nat) (a0b_0 a0b_1 a0b_2 a0b_3 a0b_4:nat64)
      (a1b:nat) (a1b_0 a1b_1 a1b_2 a1b_3 a1b_4:nat64)
      (b:nat)   (b0 b1 b2 b3:nat64)
      (s1 s2 s3 s4 s5
      c:nat64) : Lemma
  (requires a0b = pow2_five a0b_0 a0b_1 a0b_2 a0b_3 a0b_4 /\
            a1b = pow2_five a1b_0 a1b_1 a1b_2 a1b_3 a1b_4 /\
            b = pow2_four b0 b1 b2 b3 /\
            a0b = mul_nats a0 b /\
            a1b = mul_nats a1 b /\
           (let s1', c1 = add_carry a0b_1 a1b_0 0 in
            let s2', c2 = add_carry a0b_2 a1b_1 c1 in
            let s3', c3 = add_carry a0b_3 a1b_2 c2 in
            let s4', c4 = add_carry a0b_4 a1b_3 c3 in
            let s5', c5 = add_carry 0 a1b_4 c4 in
            s1 == s1' /\
            s2 == s2' /\
            s3 == s3' /\
            s4 == s4' /\
            s5 == s5' /\
            c5 == c))
  (ensures (pow2_two a0 a1) * b ==
           pow2_seven a0b_0 s1 s2 s3 s4 s5 c)
let lemma_sum_a1b
      (a0 a1:nat64)
      (a0b:nat) (a0b_0 a0b_1 a0b_2 a0b_3 a0b_4:nat64)
      (a1b:nat) (a1b_0 a1b_1 a1b_2 a1b_3 a1b_4:nat64)
      (b:nat)   (b0 b1 b2 b3:nat64)
      (s1 s2 s3 s4 s5
      c:nat64) : Lemma
  (requires a0b = pow2_five a0b_0 a0b_1 a0b_2 a0b_3 a0b_4 /\
            a1b = pow2_five a1b_0 a1b_1 a1b_2 a1b_3 a1b_4 /\
            b = pow2_four b0 b1 b2 b3 /\
            a0b = mul_nats a0 b /\
            a1b = mul_nats a1 b /\
           (let s1', c1 = add_carry a0b_1 a1b_0 0 in
            let s2', c2 = add_carry a0b_2 a1b_1 c1 in
            let s3', c3 = add_carry a0b_3 a1b_2 c2 in
            let s4', c4 = add_carry a0b_4 a1b_3 c3 in
            let s5', c5 = add_carry 0 a1b_4 c4 in
            s1 == s1' /\
            s2 == s2' /\
            s3 == s3' /\
            s4 == s4' /\
            s5 == s5' /\
            c5 == c))
  (ensures (pow2_two a0 a1) * b ==
           pow2_seven a0b_0 s1 s2 s3 s4 s5 c)
  =
  assert_by_tactic (
    (pow2_two a0 a1) * b ==
    pow2_two (mul_nats a0 b) (mul_nats a1 b)) int_canon;
  assert (
    pow2_two (mul_nats a0 b) (mul_nats a1 b) ==
    pow2_two a0b a1b);
  lemma_offset_sum a0b a0b_0 a0b_1 a0b_2 a0b_3 a0b_4
                   a1b a1b_0 a1b_1 a1b_2 a1b_3 a1b_4;
  assert (
    pow2_two a0b a1b ==
    pow2_six a0b_0 (a0b_1 + a1b_0) (a0b_2 + a1b_1) (a0b_3 + a1b_2) (a0b_4 + a1b_3) a1b_4);
  lemma_partial_sum a0b_0 a0b_1 a0b_2 a0b_3 a0b_4
                    a1b_0 a1b_1 a1b_2 a1b_3 a1b_4
                    s1 s2 s3 s4 s5 c;
  ()
val lemma_sum_a1b
      (a0 a1:nat64)
      (a0b:nat) (a0b_0 a0b_1 a0b_2 a0b_3 a0b_4:nat64)
      (a1b:nat) (a1b_0 a1b_1 a1b_2 a1b_3 a1b_4:nat64)
      (b:nat)   (b0 b1 b2 b3:nat64)
      (s1 s2 s3 s4 s5
      c:nat64) : Lemma
  (requires a0b = pow2_five a0b_0 a0b_1 a0b_2 a0b_3 a0b_4 /\
            a1b = pow2_five a1b_0 a1b_1 a1b_2 a1b_3 a1b_4 /\
            b = pow2_four b0 b1 b2 b3 /\
            a0b = mul_nats a0 b /\
            a1b = mul_nats a1 b /\
           (let s1', c1 = add_carry a0b_1 a1b_0 0 in
            let s2', c2 = add_carry a0b_2 a1b_1 c1 in
            let s3', c3 = add_carry a0b_3 a1b_2 c2 in
            let s4', c4 = add_carry a0b_4 a1b_3 c3 in
            let s5', c5 = add_carry 0 a1b_4 c4 in
            s1 == s1' /\
            s2 == s2' /\
            s3 == s3' /\
            s4 == s4' /\
            s5 == s5' /\
            c5 == c))
  (ensures (pow2_two a0 a1) * b ==
           pow2_seven a0b_0 s1 s2 s3 s4 s5 c)
let lemma_sum_a1b
      (a0 a1: nat64)
      (a0b: nat)
      (a0b_0 a0b_1 a0b_2 a0b_3 a0b_4: nat64)
      (a1b: nat)
      (a1b_0 a1b_1 a1b_2 a1b_3 a1b_4: nat64)
      (b: nat)
      (b0 b1 b2 b3 s1 s2 s3 s4 s5 c: nat64)
    : Lemma
      (requires
        a0b = pow2_five a0b_0 a0b_1 a0b_2 a0b_3 a0b_4 /\
        a1b = pow2_five a1b_0 a1b_1 a1b_2 a1b_3 a1b_4 /\ b = pow2_four b0 b1 b2 b3 /\
        a0b = mul_nats a0 b /\ a1b = mul_nats a1 b /\
        (let s1', c1 = add_carry a0b_1 a1b_0 0 in
          let s2', c2 = add_carry a0b_2 a1b_1 c1 in
          let s3', c3 = add_carry a0b_3 a1b_2 c2 in
          let s4', c4 = add_carry a0b_4 a1b_3 c3 in
          let s5', c5 = add_carry 0 a1b_4 c4 in
          s1 == s1' /\ s2 == s2' /\ s3 == s3' /\ s4 == s4' /\ s5 == s5' /\ c5 == c))
      (ensures (pow2_two a0 a1) * b == pow2_seven a0b_0 s1 s2 s3 s4 s5 c) =
assert_by_tactic ((pow2_two a0 a1) * b == pow2_two (mul_nats a0 b) (mul_nats a1 b)) int_canon;
assert (pow2_two (mul_nats a0 b) (mul_nats a1 b) == pow2_two a0b a1b);
lemma_offset_sum a0b a0b_0 a0b_1 a0b_2 a0b_3 a0b_4 a1b a1b_0 a1b_1 a1b_2 a1b_3 a1b_4;
assert (pow2_two a0b a1b ==
    pow2_six a0b_0 (a0b_1 + a1b_0) (a0b_2 + a1b_1) (a0b_3 + a1b_2) (a0b_4 + a1b_3) a1b_4);
lemma_partial_sum a0b_0 a0b_1 a0b_2 a0b_3 a0b_4 a1b_0 a1b_1 a1b_2 a1b_3 a1b_4 s1 s2 s3 s4 s5 c;
()
Vale.Curve25519.FastMul_helpers.fst.checked
Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Curve25519.Fast_lemmas_internal.fsti.checked Vale.Curve25519.Fast_defs.fst.checked prims.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.CanonCommSemiring.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Calc.fsti.checked
Vale.Curve25519.FastMul_helpers.fst
Vale.Def.Types_s.nat64 Prims.nat Prims.unit Vale.Curve25519.FastMul_helpers.lemma_partial_sum Prims._assert Prims.eq2 Vale.Curve25519.Fast_defs.pow2_two Vale.Curve25519.Fast_defs.pow2_six Prims.op_Addition Vale.Curve25519.FastMul_helpers.lemma_offset_sum Vale.Curve25519.Fast_defs.mul_nats FStar.Tactics.Effect.assert_by_tactic Prims.int FStar.Mul.op_Star Vale.Curve25519.FastMul_helpers.int_canon Prims.l_and Prims.b2t Prims.op_Equality Vale.Curve25519.Fast_defs.pow2_five Vale.Curve25519.Fast_defs.pow2_four Prims.op_BarBar Prims.l_or Prims.op_LessThan Vale.Def.Words_s.pow2_64 Prims.logical FStar.Pervasives.Native.tuple2 Vale.Def.Words_s.nat64 Vale.Curve25519.Fast_defs.add_carry Prims.squash Vale.Curve25519.Fast_defs.pow2_seven Prims.Nil FStar.Pervasives.pattern
module Vale.Curve25519.FastMul_helpers

open Vale.Def.Words_s
open Vale.Def.Types_s
open FStar.Mul
open FStar.Tactics
open FStar.Tactics.CanonCommSemiring
open Vale.Curve25519.Fast_defs
open Vale.Curve25519.Fast_lemmas_internal
open FStar.Math.Lemmas
#reset-options "--using_facts_from '* -FStar.Tactics -FStar.Reflection'"

#push-options "--z3rlimit 10"
let lemma_mul_pow2_bound (b:nat{b > 1}) (x y:natN (pow2 b))
  : Lemma (x * y < pow2 (2*b) - 1 /\
           x * y <= pow2 (2*b) - 2*pow2(b) + 1)
  = lemma_mul_bounds_le x (pow2 b - 1) y (pow2 b -1);
    pow2_plus b b;
    assert ( (pow2 b - 1) * (pow2 b -1) = pow2 (2*b) - 2*pow2(b) + 1)
#pop-options

let lemma_mul_bound64 (x y:nat64)
  : Lemma (x * y < pow2_128 - 1 /\ x * y <= pow2_128 - 2*pow2_64 + 1)
  = assert_norm (pow2 64 == pow2_64);
    assert_norm (pow2 128 == pow2_128);
    lemma_mul_pow2_bound 64 x y

(* Intel manual mentions this fact *)
let lemma_intel_prod_sum_bound (w x y z:nat64)
  : Lemma (w * x + y + z < pow2_128)
  = lemma_mul_bound64 w x

let lemma_prod_bounds (dst_hi dst_lo x y:nat64)
  : Lemma
    (requires
      pow2_64 * dst_hi + dst_lo == x * y)
    (ensures
      dst_hi < pow2_64 - 1 /\
      (dst_hi < pow2_64 - 2 \/
       dst_lo <= 1))
  = let result = x * y in
    lemma_div_mod result pow2_64;
    //assert (result = pow2_64 * (result / pow2_64) + result % pow2_64);
    //assert (result % pow2_64 == dst_lo);
    //assert (result / pow2_64 == dst_hi);
    lemma_mul_bound64 x y

let lemma_double_bound (x:nat64)
  : Lemma (add_wrap x x < pow2_64 - 1)
  = ()

type bit = b:nat { b <= 1 }

let lemma_offset_sum (a_agg:nat) (a0 a1 a2 a3 a4:nat64)
                     (b_agg:nat) (b0 b1 b2 b3 b4:nat64)
  : Lemma
    (requires
      a_agg = pow2_five a0 a1 a2 a3 a4 /\
      b_agg = pow2_five b0 b1 b2 b3 b4)
    (ensures
      a_agg + pow2_64 * b_agg =
      pow2_six a0 (a1 + b0) (a2 + b1) (a3 + b2) (a4 + b3) b4)
  = let lhs = a_agg + pow2_64 * b_agg in
    let rhs = pow2_six a0 (a1 + b0) (a2 + b1) (a3 + b2) (a4 + b3) b4 in
    assert_by_tactic (lhs == rhs) int_canon

#push-options "--z3rlimit 60"
let lemma_partial_sum
     (a0 a1 a2 a3 a4
      b0 b1 b2 b3 b4
      s1 s2 s3 s4 s5 c:nat64)
  : Lemma
    (requires
      (let s1', c1 = add_carry a1 b0 0 in
       let s2', c2 = add_carry a2 b1 c1 in
       let s3', c3 = add_carry a3 b2 c2 in
       let s4', c4 = add_carry a4 b3 c3 in
       let s5', c5 = add_carry 0 b4 c4 in
       s1 == s1' /\
       s2 == s2' /\
       s3 == s3' /\
       s4 == s4' /\
       s5 == s5' /\
       c == c5))
  (ensures
    pow2_six a0 (a1 + b0) (a2 + b1) (a3 + b2) (a4 + b3) b4 =
    pow2_seven a0 s1 s2 s3 s4 s5 c)
  = ()

let lemma_partial_sum_a2b
     (a0 a1 a2 a3 a4 a5
      b0 b1 b2 b3 b4
      s1 s2 s3 s4 s5:nat64)
  : Lemma
    (requires
      (let s1', c1 = add_carry a2 b0 0 in
       let s2', c2 = add_carry a3 b1 c1 in
       let s3', c3 = add_carry a4 b2 c2 in
       let s4', c4 = add_carry a5 b3 c3 in
       let s5', c5 = add_carry 0 b4 c4 in
       s1 == s1' /\
       s2 == s2' /\
       s3 == s3' /\
       s4 == s4' /\
       s5 == s5' /\
       0 == c5))
  (ensures
    pow2_seven a0 a1 (a2 + b0) (a3 + b1) (a4 + b2) (a5 + b3) b4 =
    pow2_seven a0 a1 s1 s2 s3 s4 s5)
  = ()

let lemma_partial_sum_a3b (
      a0 a1 a2 a3 a4 a5 a6
      b0 b1 b2 b3 b4
      s1 s2 s3 s4 s5:nat64) : Lemma
  (requires(let s1', c1 = add_carry a3 b0 0 in
            let s2', c2 = add_carry a4 b1 c1 in
            let s3', c3 = add_carry a5 b2 c2 in
            let s4', c4 = add_carry a6 b3 c3 in
            let s5', c5 = add_carry 0 b4 c4 in
            s1 == s1' /\
            s2 == s2' /\
            s3 == s3' /\
            s4 == s4' /\
            s5 == s5' /\
            0 == c5))
  (ensures pow2_eight a0 a1 a2 (a3 + b0) (a4 + b1) (a5 + b2) (a6 + b3) b4 =
           pow2_eight a0 a1 a2 s1 s2 s3 s4 s5)
  =
  ()
#pop-options

let lemma_sum_a1b
      (a0 a1:nat64)
      (a0b:nat) (a0b_0 a0b_1 a0b_2 a0b_3 a0b_4:nat64)
      (a1b:nat) (a1b_0 a1b_1 a1b_2 a1b_3 a1b_4:nat64)
      (b:nat)   (b0 b1 b2 b3:nat64)
      (s1 s2 s3 s4 s5
      c:nat64) : Lemma
  (requires a0b = pow2_five a0b_0 a0b_1 a0b_2 a0b_3 a0b_4 /\
            a1b = pow2_five a1b_0 a1b_1 a1b_2 a1b_3 a1b_4 /\
            b = pow2_four b0 b1 b2 b3 /\
            a0b = mul_nats a0 b /\
            a1b = mul_nats a1 b /\
           (let s1', c1 = add_carry a0b_1 a1b_0 0 in
            let s2', c2 = add_carry a0b_2 a1b_1 c1 in
            let s3', c3 = add_carry a0b_3 a1b_2 c2 in
            let s4', c4 = add_carry a0b_4 a1b_3 c3 in
            let s5', c5 = add_carry 0 a1b_4 c4 in
            s1 == s1' /\
            s2 == s2' /\
            s3 == s3' /\
            s4 == s4' /\
            s5 == s5' /\
            c5 == c))
  (ensures (pow2_two a0 a1) * b ==
           pow2_seven a0b_0 s1 s2 s3 s4 s5 c)
val lemma_sum_a1b
      (a0 a1:nat64)
      (a0b:nat) (a0b_0 a0b_1 a0b_2 a0b_3 a0b_4:nat64)
      (a1b:nat) (a1b_0 a1b_1 a1b_2 a1b_3 a1b_4:nat64)
      (b:nat)   (b0 b1 b2 b3:nat64)
      (s1 s2 s3 s4 s5
      c:nat64) : Lemma
  (requires a0b = pow2_five a0b_0 a0b_1 a0b_2 a0b_3 a0b_4 /\
            a1b = pow2_five a1b_0 a1b_1 a1b_2 a1b_3 a1b_4 /\
            b = pow2_four b0 b1 b2 b3 /\
            a0b = mul_nats a0 b /\
            a1b = mul_nats a1 b /\
           (let s1', c1 = add_carry a0b_1 a1b_0 0 in
            let s2', c2 = add_carry a0b_2 a1b_1 c1 in
            let s3', c3 = add_carry a0b_3 a1b_2 c2 in
            let s4', c4 = add_carry a0b_4 a1b_3 c3 in
            let s5', c5 = add_carry 0 a1b_4 c4 in
            s1 == s1' /\
            s2 == s2' /\
            s3 == s3' /\
            s4 == s4' /\
            s5 == s5' /\
            c5 == c))
  (ensures (pow2_two a0 a1) * b ==
           pow2_seven a0b_0 s1 s2 s3 s4 s5 c)

    a0: Vale.Def.Types_s.nat64 ->
    a1: Vale.Def.Types_s.nat64 ->
    a0b: Prims.nat ->
    a0b_0: Vale.Def.Types_s.nat64 ->
    a0b_1: Vale.Def.Types_s.nat64 ->
    a0b_2: Vale.Def.Types_s.nat64 ->
    a0b_3: Vale.Def.Types_s.nat64 ->
    a0b_4: Vale.Def.Types_s.nat64 ->
    a1b: Prims.nat ->
    a1b_0: Vale.Def.Types_s.nat64 ->
    a1b_1: Vale.Def.Types_s.nat64 ->
    a1b_2: Vale.Def.Types_s.nat64 ->
    a1b_3: Vale.Def.Types_s.nat64 ->
    a1b_4: Vale.Def.Types_s.nat64 ->
    b: Prims.nat ->
    b0: Vale.Def.Types_s.nat64 ->
    b1: Vale.Def.Types_s.nat64 ->
    b2: Vale.Def.Types_s.nat64 ->
    b3: Vale.Def.Types_s.nat64 ->
    s1: Vale.Def.Types_s.nat64 ->
    s2: Vale.Def.Types_s.nat64 ->
    s3: Vale.Def.Types_s.nat64 ->
    s4: Vale.Def.Types_s.nat64 ->
    s5: Vale.Def.Types_s.nat64 ->
    c: Vale.Def.Types_s.nat64
  -> FStar.Pervasives.Lemma
      (requires
        a0b = Vale.Curve25519.Fast_defs.pow2_five a0b_0 a0b_1 a0b_2 a0b_3 a0b_4 /\
        a1b = Vale.Curve25519.Fast_defs.pow2_five a1b_0 a1b_1 a1b_2 a1b_3 a1b_4 /\
        b = Vale.Curve25519.Fast_defs.pow2_four b0 b1 b2 b3 /\
        a0b = Vale.Curve25519.Fast_defs.mul_nats a0 b /\
        a1b = Vale.Curve25519.Fast_defs.mul_nats a1 b /\
        (let _ = Vale.Curve25519.Fast_defs.add_carry a0b_1 a1b_0 0 in
          (let FStar.Pervasives.Native.Mktuple2 #_ #_ s1' c1 = _ in
            let _ = Vale.Curve25519.Fast_defs.add_carry a0b_2 a1b_1 c1 in
            (let FStar.Pervasives.Native.Mktuple2 #_ #_ s2' c2 = _ in
              let _ = Vale.Curve25519.Fast_defs.add_carry a0b_3 a1b_2 c2 in
              (let FStar.Pervasives.Native.Mktuple2 #_ #_ s3' c3 = _ in
                let _ = Vale.Curve25519.Fast_defs.add_carry a0b_4 a1b_3 c3 in
                (let FStar.Pervasives.Native.Mktuple2 #_ #_ s4' c4 = _ in
                  let _ = Vale.Curve25519.Fast_defs.add_carry 0 a1b_4 c4 in
                  (let FStar.Pervasives.Native.Mktuple2 #_ #_ s5' c5 = _ in
                    s1 == s1' /\ s2 == s2' /\ s3 == s3' /\ s4 == s4' /\ s5 == s5' /\ c5 == c)
                  <:
                  Prims.logical)
                <:
                Prims.logical)
              <:
              Prims.logical)
            <:
            Prims.logical)
          <:
          Prims.logical))
      (ensures
        Vale.Curve25519.Fast_defs.pow2_two a0 a1 * b ==
        Vale.Curve25519.Fast_defs.pow2_seven a0b_0 s1 s2 s3 s4 s5 c)