val 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 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
val 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 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;
lemma_mul_bound64 x y
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 Vale.Curve25519.FastMul_helpers.lemma_mul_bound64 Prims.unit FStar.Math.Lemmas.lemma_div_mod Vale.Def.Words_s.pow2_64 Prims.int FStar.Mul.op_Star Prims.eq2 Prims.op_Addition Prims.squash Prims.l_and Prims.b2t Prims.op_LessThan Prims.op_Subtraction Prims.l_or Prims.op_LessThanOrEqual 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 \/
val 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))

    dst_hi: Vale.Def.Types_s.nat64 ->
    dst_lo: Vale.Def.Types_s.nat64 ->
    x: Vale.Def.Types_s.nat64 ->
    y: Vale.Def.Types_s.nat64
  -> FStar.Pervasives.Lemma (requires Vale.Def.Words_s.pow2_64 * dst_hi + dst_lo == x * y)
      (ensures
        dst_hi < Vale.Def.Words_s.pow2_64 - 1 /\
        (dst_hi < Vale.Def.Words_s.pow2_64 - 2 \/ dst_lo <= 1))