val 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)
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;
  };
  ()
val 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)
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;
  ( == ) { FStar.Tactics.Effect.synth_by_tactic (fun _ -> (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);
    ( == ) { FStar.Tactics.Effect.synth_by_tactic (fun _ -> (int_canon ())) }
    pow2_four (a0' + carry * 38) a1' a2' a3';
  } }
  (pow2_four (a0' + carry * 38) a1' a2' a3') % prime;
};
()
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
Vale.Def.Types_s.nat64 Vale.Curve25519.Fast_defs.bit Prims.unit FStar.Calc.calc_finish Prims.int Prims.eq2 Prims.op_Modulus Prims.op_Addition Vale.Curve25519.Fast_defs.pow2_four FStar.Mul.op_Star Vale.Curve25519.Fast_defs.pow2_256 Vale.Curve25519.Fast_defs.prime Prims.Cons FStar.Preorder.relation Prims.Nil FStar.Calc.calc_step Vale.Curve25519.Fast_defs.pow2_five FStar.Calc.calc_init FStar.Calc.calc_pack Vale.Curve25519.FastHybrid_helpers.lemma_mul_pow256_add Prims.squash FStar.Tactics.CanonCommSemiring.semiring_reflect FStar.Tactics.CanonCommSemiring.int_cr FStar.Pervasives.Native.Mktuple2 Prims.list FStar.Pervasives.Native.tuple2 Prims.nat FStar.Pervasives.Native.snd Prims.b2t Prims.op_GreaterThanOrEqual Prims.op_Multiply FStar.Reflection.V2.Data.var FStar.Tactics.CanonCommSemiring.Pvar FStar.Tactics.CanonCommSemiring.Pplus FStar.Tactics.CanonCommSemiring.Pmult FStar.Tactics.CanonCommSemiring.Pconst Prims._assert Prims.op_LessThan Vale.Def.Words_s.pow2_64 Prims.l_and Prims.op_Subtraction 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)
val 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)

    a0: Vale.Def.Types_s.nat64 ->
    a1: Vale.Def.Types_s.nat64 ->
    a2: Vale.Def.Types_s.nat64 ->
    a3: 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 ->
    carry_in: Vale.Def.Types_s.nat64 ->
    carry: Vale.Curve25519.Fast_defs.bit
  -> FStar.Pervasives.Lemma
      (requires
        Vale.Curve25519.Fast_defs.pow2_five a0' a1' a2' a3' carry ==
        Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2 a3 + carry_in * 38 /\
        carry_in * 38 - 1 + 38 < Vale.Def.Words_s.pow2_64)
      (ensures
        a0' + carry * 38 < Vale.Def.Words_s.pow2_64 /\
        Vale.Curve25519.Fast_defs.pow2_four (a0' + carry * 38) a1' a2' a3' %
        Vale.Curve25519.Fast_defs.prime ==
        (Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2 a3 +
          carry_in * Vale.Curve25519.Fast_defs.pow2_256) %
        Vale.Curve25519.Fast_defs.prime)