val lemma_fast_mul1 (a:nat)
               (b a0 a1 a2 a3
                ba0_hi ba0_lo
                ba1_hi ba1_lo
                ba2_hi ba2_lo
                ba3_hi ba3_lo
                s1 s2 s3 s4:nat64) : Lemma
  (requires a = pow2_four a0 a1 a2 a3 /\

            pow2_64 * ba0_hi + ba0_lo == b * a0 /\
            pow2_64 * ba1_hi + ba1_lo == b * a1 /\
            pow2_64 * ba2_hi + ba2_lo == b * a2 /\
            pow2_64 * ba3_hi + ba3_lo == b * a3 /\

           (let s1', c1 = add_carry ba1_lo ba0_hi 0 in
            let s2', c2 = add_carry ba2_lo ba1_hi c1 in
            let s3', c3 = add_carry ba3_lo ba2_hi c2 in
            let s4', c4 = add_carry ba3_hi 0 c3 in
            s1 == s1' /\
            s2 == s2' /\
            s3 == s3' /\
            s4 == s4' /\
            c4 == 0)
  )
  (ensures pow2_five ba0_lo s1 s2 s3 s4 == a * b)
let lemma_fast_mul1 (a:nat)
               (b a0 a1 a2 a3
                ba0_hi ba0_lo
                ba1_hi ba1_lo
                ba2_hi ba2_lo
                ba3_hi ba3_lo
                s1 s2 s3 s4:nat64) : Lemma
  (requires a = pow2_four a0 a1 a2 a3 /\

            pow2_64 * ba0_hi + ba0_lo == b * a0 /\
            pow2_64 * ba1_hi + ba1_lo == b * a1 /\
            pow2_64 * ba2_hi + ba2_lo == b * a2 /\
            pow2_64 * ba3_hi + ba3_lo == b * a3 /\

           (let s1', c1 = add_carry ba1_lo ba0_hi 0 in
            let s2', c2 = add_carry ba2_lo ba1_hi c1 in
            let s3', c3 = add_carry ba3_lo ba2_hi c2 in
            let s4', c4 = add_carry ba3_hi 0 c3 in
            s1 == s1' /\
            s2 == s2' /\
            s3 == s3' /\
            s4 == s4' /\
            c4 == 0)
  )
  (ensures pow2_five ba0_lo s1 s2 s3 s4 == a * b)
  =
  assert_by_tactic (b * pow2_four a0 a1 a2 a3 == pow2_four (b*a0) (b*a1) (b*a2) (b*a3)) int_canon;
  //lemma_prod_bounds ba0_hi ba0_lo b a0;
  //lemma_prod_bounds ba1_hi ba1_lo b a1;
  //lemma_prod_bounds ba2_hi ba2_lo b a2;
  //lemma_prod_bounds ba3_hi ba3_lo b a3;
  ()
val lemma_fast_mul1 (a:nat)
               (b a0 a1 a2 a3
                ba0_hi ba0_lo
                ba1_hi ba1_lo
                ba2_hi ba2_lo
                ba3_hi ba3_lo
                s1 s2 s3 s4:nat64) : Lemma
  (requires a = pow2_four a0 a1 a2 a3 /\

            pow2_64 * ba0_hi + ba0_lo == b * a0 /\
            pow2_64 * ba1_hi + ba1_lo == b * a1 /\
            pow2_64 * ba2_hi + ba2_lo == b * a2 /\
            pow2_64 * ba3_hi + ba3_lo == b * a3 /\

           (let s1', c1 = add_carry ba1_lo ba0_hi 0 in
            let s2', c2 = add_carry ba2_lo ba1_hi c1 in
            let s3', c3 = add_carry ba3_lo ba2_hi c2 in
            let s4', c4 = add_carry ba3_hi 0 c3 in
            s1 == s1' /\
            s2 == s2' /\
            s3 == s3' /\
            s4 == s4' /\
            c4 == 0)
  )
  (ensures pow2_five ba0_lo s1 s2 s3 s4 == a * b)
let lemma_fast_mul1
      (a: nat)
      (b a0 a1 a2 a3 ba0_hi ba0_lo ba1_hi ba1_lo ba2_hi ba2_lo ba3_hi ba3_lo s1 s2 s3 s4: nat64)
    : Lemma
      (requires
        a = pow2_four a0 a1 a2 a3 /\ pow2_64 * ba0_hi + ba0_lo == b * a0 /\
        pow2_64 * ba1_hi + ba1_lo == b * a1 /\ pow2_64 * ba2_hi + ba2_lo == b * a2 /\
        pow2_64 * ba3_hi + ba3_lo == b * a3 /\
        (let s1', c1 = add_carry ba1_lo ba0_hi 0 in
          let s2', c2 = add_carry ba2_lo ba1_hi c1 in
          let s3', c3 = add_carry ba3_lo ba2_hi c2 in
          let s4', c4 = add_carry ba3_hi 0 c3 in
          s1 == s1' /\ s2 == s2' /\ s3 == s3' /\ s4 == s4' /\ c4 == 0))
      (ensures pow2_five ba0_lo s1 s2 s3 s4 == a * b) =
assert_by_tactic (b * pow2_four a0 a1 a2 a3 == pow2_four (b * a0) (b * a1) (b * a2) (b * a3))
  int_canon;
()
Vale.Curve25519.FastHybrid_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.FastHybrid_helpers.fst
Prims.nat Vale.Def.Types_s.nat64 Prims.unit FStar.Tactics.Effect.assert_by_tactic Prims.eq2 Prims.int FStar.Mul.op_Star Vale.Curve25519.Fast_defs.pow2_four Vale.Curve25519.FastHybrid_helpers.int_canon Prims.l_and Prims.b2t Prims.op_Equality Prims.op_Addition Vale.Def.Words_s.pow2_64 Prims.op_BarBar Prims.logical FStar.Pervasives.Native.tuple2 Vale.Def.Words_s.nat64 Vale.Curve25519.Fast_defs.add_carry Prims.squash Vale.Curve25519.Fast_defs.pow2_five Prims.Nil FStar.Pervasives.pattern
module Vale.Curve25519.FastHybrid_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

#reset-options "--max_fuel 0 --max_ifuel 0 --using_facts_from '* -FStar.Tactics -FStar.Reflection'"

let lemma_carry_prime (a0 a1 a2 a3 a0' a1' a2' a3' carry_in:nat64) (carry:bit) : Lemma
  (requires pow2_five a0' a1' a2' a3' carry == pow2_four a0 a1 a2 a3 + carry_in * 38 /\
            carry_in * 38 - 1 + 38 < pow2_64)
  (ensures a0' + carry * 38 < pow2_64 /\
           (pow2_four (a0' + carry * 38) a1' a2' a3') % prime == (pow2_four a0 a1 a2 a3 + carry_in * pow2_256) % prime)
  =
  assert (a0' + carry * 38 < pow2_64);

  calc (==) {
    (pow2_four a0 a1 a2 a3 + carry_in * pow2_256) % prime;
    == { lemma_mul_pow256_add (pow2_four a0 a1 a2 a3) carry_in }
    (pow2_four a0 a1 a2 a3 + carry_in * 38) % prime;
    == {}
    (pow2_five a0' a1' a2' a3' carry) % prime;
    == { _ by (int_canon()) }
    (pow2_four a0' a1' a2' a3' + (carry * pow2_256)) % prime;
    == { lemma_mul_pow256_add (pow2_four a0' a1' a2' a3') carry }
    (pow2_four a0' a1' a2' a3' + (carry * 38)) % prime;
    == {  calc (==) {
            (pow2_four a0' a1' a2' a3') + (carry * 38);
            == { _ by (int_canon()) }
            pow2_four (a0' + carry * 38) a1' a2' a3';
          }
       }
    (pow2_four (a0' + carry * 38) a1' a2' a3') % prime;
  };
  ()

#reset-options "--z3rlimit 30 --max_fuel 0 --max_ifuel 0 --using_facts_from '* -FStar.Tactics -FStar.Reflection'"
let lemma_fast_mul1 (a:nat)
               (b a0 a1 a2 a3
                ba0_hi ba0_lo
                ba1_hi ba1_lo
                ba2_hi ba2_lo
                ba3_hi ba3_lo
                s1 s2 s3 s4:nat64) : Lemma
  (requires a = pow2_four a0 a1 a2 a3 /\

            pow2_64 * ba0_hi + ba0_lo == b * a0 /\
            pow2_64 * ba1_hi + ba1_lo == b * a1 /\
            pow2_64 * ba2_hi + ba2_lo == b * a2 /\
            pow2_64 * ba3_hi + ba3_lo == b * a3 /\

           (let s1', c1 = add_carry ba1_lo ba0_hi 0 in
            let s2', c2 = add_carry ba2_lo ba1_hi c1 in
            let s3', c3 = add_carry ba3_lo ba2_hi c2 in
            let s4', c4 = add_carry ba3_hi 0 c3 in
            s1 == s1' /\
            s2 == s2' /\
            s3 == s3' /\
            s4 == s4' /\
            c4 == 0)
  )
  (ensures pow2_five ba0_lo s1 s2 s3 s4 == a * b)
val lemma_fast_mul1 (a:nat)
               (b a0 a1 a2 a3
                ba0_hi ba0_lo
                ba1_hi ba1_lo
                ba2_hi ba2_lo
                ba3_hi ba3_lo
                s1 s2 s3 s4:nat64) : Lemma
  (requires a = pow2_four a0 a1 a2 a3 /\

            pow2_64 * ba0_hi + ba0_lo == b * a0 /\
            pow2_64 * ba1_hi + ba1_lo == b * a1 /\
            pow2_64 * ba2_hi + ba2_lo == b * a2 /\
            pow2_64 * ba3_hi + ba3_lo == b * a3 /\

           (let s1', c1 = add_carry ba1_lo ba0_hi 0 in
            let s2', c2 = add_carry ba2_lo ba1_hi c1 in
            let s3', c3 = add_carry ba3_lo ba2_hi c2 in
            let s4', c4 = add_carry ba3_hi 0 c3 in
            s1 == s1' /\
            s2 == s2' /\
            s3 == s3' /\
            s4 == s4' /\
            c4 == 0)
  )
  (ensures pow2_five ba0_lo s1 s2 s3 s4 == a * b)

    a: Prims.nat ->
    b: Vale.Def.Types_s.nat64 ->
    a0: Vale.Def.Types_s.nat64 ->
    a1: Vale.Def.Types_s.nat64 ->
    a2: Vale.Def.Types_s.nat64 ->
    a3: Vale.Def.Types_s.nat64 ->
    ba0_hi: Vale.Def.Types_s.nat64 ->
    ba0_lo: Vale.Def.Types_s.nat64 ->
    ba1_hi: Vale.Def.Types_s.nat64 ->
    ba1_lo: Vale.Def.Types_s.nat64 ->
    ba2_hi: Vale.Def.Types_s.nat64 ->
    ba2_lo: Vale.Def.Types_s.nat64 ->
    ba3_hi: Vale.Def.Types_s.nat64 ->
    ba3_lo: 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
  -> FStar.Pervasives.Lemma
      (requires
        a = Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2 a3 /\
        Vale.Def.Words_s.pow2_64 * ba0_hi + ba0_lo == b * a0 /\
        Vale.Def.Words_s.pow2_64 * ba1_hi + ba1_lo == b * a1 /\
        Vale.Def.Words_s.pow2_64 * ba2_hi + ba2_lo == b * a2 /\
        Vale.Def.Words_s.pow2_64 * ba3_hi + ba3_lo == b * a3 /\
        (let _ = Vale.Curve25519.Fast_defs.add_carry ba1_lo ba0_hi 0 in
          (let FStar.Pervasives.Native.Mktuple2 #_ #_ s1' c1 = _ in
            let _ = Vale.Curve25519.Fast_defs.add_carry ba2_lo ba1_hi c1 in
            (let FStar.Pervasives.Native.Mktuple2 #_ #_ s2' c2 = _ in
              let _ = Vale.Curve25519.Fast_defs.add_carry ba3_lo ba2_hi c2 in
              (let FStar.Pervasives.Native.Mktuple2 #_ #_ s3' c3 = _ in
                let _ = Vale.Curve25519.Fast_defs.add_carry ba3_hi 0 c3 in
                (let FStar.Pervasives.Native.Mktuple2 #_ #_ s4' c4 = _ in
                  s1 == s1' /\ s2 == s2' /\ s3 == s3' /\ s4 == s4' /\ c4 == 0)
                <:
                Prims.logical)
              <:
              Prims.logical)
            <:
            Prims.logical)
          <:
          Prims.logical)) (ensures Vale.Curve25519.Fast_defs.pow2_five ba0_lo s1 s2 s3 s4 == a * b)