val lemma_subm_conditional:
    x0:nat -> x1:nat -> x2:nat -> x3:nat -> x4:nat
  -> y0:nat -> y1:nat -> y2:nat -> y3:nat -> y4:nat
  -> b0:nat -> b1:nat -> b2:nat -> b3:nat -> b4:nat ->
  Lemma (
    x0 - y0 + b0 * pow2 56 +
    (x1 - y1 - b0 + b1 * pow2 56) * pow2 56 +
    (x2 - y2 - b1 + b2 * pow2 56) * pow2 112 +
    (x3 - y3 - b2 + b3 * pow2 56) * pow2 168 +
    (x4 - y4 - b3 + b4 * pow2 56) * pow2 224 ==
    (x0 + x1 * pow2 56 + x2 * pow2 112 + x3 * pow2 168 + x4 * pow2 224) -
    (y0 + y1 * pow2 56 + y2 * pow2 112 + y3 * pow2 168 + y4 * pow2 224) + b4 * pow2 280)
let lemma_subm_conditional x0 x1 x2 x3 x4 y0 y1 y2 y3 y4 b0 b1 b2 b3 b4 =
  assert_norm (pow2 56 * pow2 56 = pow2 112);
  assert_norm (pow2 56 * pow2 112 = pow2 168);
  assert_norm (pow2 56 * pow2 168 = pow2 224);
  assert_norm (pow2 56 * pow2 224 = pow2 280)
val lemma_subm_conditional:
    x0:nat -> x1:nat -> x2:nat -> x3:nat -> x4:nat
  -> y0:nat -> y1:nat -> y2:nat -> y3:nat -> y4:nat
  -> b0:nat -> b1:nat -> b2:nat -> b3:nat -> b4:nat ->
  Lemma (
    x0 - y0 + b0 * pow2 56 +
    (x1 - y1 - b0 + b1 * pow2 56) * pow2 56 +
    (x2 - y2 - b1 + b2 * pow2 56) * pow2 112 +
    (x3 - y3 - b2 + b3 * pow2 56) * pow2 168 +
    (x4 - y4 - b3 + b4 * pow2 56) * pow2 224 ==
    (x0 + x1 * pow2 56 + x2 * pow2 112 + x3 * pow2 168 + x4 * pow2 224) -
    (y0 + y1 * pow2 56 + y2 * pow2 112 + y3 * pow2 168 + y4 * pow2 224) + b4 * pow2 280)
let lemma_subm_conditional x0 x1 x2 x3 x4 y0 y1 y2 y3 y4 b0 b1 b2 b3 b4 =
assert_norm (pow2 56 * pow2 56 = pow2 112);
assert_norm (pow2 56 * pow2 112 = pow2 168);
assert_norm (pow2 56 * pow2 168 = pow2 224);
assert_norm (pow2 56 * pow2 224 = pow2 280)
Hacl.Spec.BignumQ.Lemmas.fst.checked
Spec.Ed25519.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Hacl.Spec.BignumQ.Definitions.fst.checked FStar.UInt32.fsti.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.CanonCommSemiring.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Calc.fsti.checked
Hacl.Spec.BignumQ.Lemmas.fst
Prims.nat FStar.Pervasives.assert_norm Prims.b2t Prims.op_Equality Prims.int FStar.Mul.op_Star Prims.pow2 Prims.unit
module Hacl.Spec.BignumQ.Lemmas

open FStar.Tactics.CanonCommSemiring
open FStar.Mul
open Lib.IntTypes

module S = Spec.Ed25519

include Hacl.Spec.BignumQ.Definitions

let feq (#a #b:Type) (f:(a -> b)) (x y:a) :
  Lemma (requires x == y) (ensures f x == f y) = ()

let eq_eq2 (#a:eqtype) (x y:a) :
  Lemma (requires x = y) (ensures x == y) = ()

val lemma_mul_lt:a:nat -> b:nat -> c:nat -> d:nat ->
  Lemma
  (requires a < b /\ c < d)
  (ensures  a * c < b * d)

let lemma_mul_lt a b c d = ()


val lemma_as_nat5: f:qelem5 ->
  Lemma
  (requires qelem_fits5 f (1, 1, 1, 1, 1))
  (ensures  as_nat5 f < pow2 280)

let lemma_as_nat5 f =
  //let (f0, f1, f2, f3, f4) = f in
  //assert (as_nat5 f == v f0 + v f1 * pow56 + v f2 * pow112 + v f3 * pow168 + v f4 * pow224);
  assert_norm (pow2 56 * pow2 56 = pow2 112);
  assert_norm (pow2 56 * pow2 112 = pow2 168);
  assert_norm (pow2 56 * pow2 168 = pow2 224);
  assert_norm (pow2 56 * pow2 224 = pow2 280)


val lemma_choose_step:
    bit:uint64{v bit <= 1}
  -> x:uint64
  -> y:uint64
  -> Lemma
     (let mask = bit -. u64 1 in
      let z = x ^. (mask &. (x ^. y)) in
      if v bit = 1 then z == x else z == y)

let lemma_choose_step bit p1 p2 =
  let mask = bit -. u64 1 in
  assert (v bit == 0 ==> v mask == pow2 64 - 1);
  assert (v bit == 1 ==> v mask == 0);
  let dummy = mask &. (p1 ^. p2) in
  logand_lemma mask (p1 ^. p2);
  assert (v bit == 1 ==> v dummy == 0);
  assert (v bit == 0 ==> v dummy ==  v (p1 ^. p2));
  let p1' = p1 ^. dummy in
  assert (v dummy == v (if v bit = 1 then u64 0 else (p1 ^. p2)));
  logxor_lemma p1 p2


val lemma_subm_conditional:
    x0:nat -> x1:nat -> x2:nat -> x3:nat -> x4:nat
  -> y0:nat -> y1:nat -> y2:nat -> y3:nat -> y4:nat
  -> b0:nat -> b1:nat -> b2:nat -> b3:nat -> b4:nat ->
  Lemma (
    x0 - y0 + b0 * pow2 56 +
    (x1 - y1 - b0 + b1 * pow2 56) * pow2 56 +
    (x2 - y2 - b1 + b2 * pow2 56) * pow2 112 +
    (x3 - y3 - b2 + b3 * pow2 56) * pow2 168 +
    (x4 - y4 - b3 + b4 * pow2 56) * pow2 224 ==
    (x0 + x1 * pow2 56 + x2 * pow2 112 + x3 * pow2 168 + x4 * pow2 224) -
    (y0 + y1 * pow2 56 + y2 * pow2 112 + y3 * pow2 168 + y4 * pow2 224) + b4 * pow2 280)

#push-options "--z3rlimit 50"
val lemma_subm_conditional:
    x0:nat -> x1:nat -> x2:nat -> x3:nat -> x4:nat
  -> y0:nat -> y1:nat -> y2:nat -> y3:nat -> y4:nat
  -> b0:nat -> b1:nat -> b2:nat -> b3:nat -> b4:nat ->
  Lemma (
    x0 - y0 + b0 * pow2 56 +
    (x1 - y1 - b0 + b1 * pow2 56) * pow2 56 +
    (x2 - y2 - b1 + b2 * pow2 56) * pow2 112 +
    (x3 - y3 - b2 + b3 * pow2 56) * pow2 168 +
    (x4 - y4 - b3 + b4 * pow2 56) * pow2 224 ==
    (x0 + x1 * pow2 56 + x2 * pow2 112 + x3 * pow2 168 + x4 * pow2 224) -
    (y0 + y1 * pow2 56 + y2 * pow2 112 + y3 * pow2 168 + y4 * pow2 224) + b4 * pow2 280)

    x0: Prims.nat ->
    x1: Prims.nat ->
    x2: Prims.nat ->
    x3: Prims.nat ->
    x4: Prims.nat ->
    y0: Prims.nat ->
    y1: Prims.nat ->
    y2: Prims.nat ->
    y3: Prims.nat ->
    y4: Prims.nat ->
    b0: Prims.nat ->
    b1: Prims.nat ->
    b2: Prims.nat ->
    b3: Prims.nat ->
    b4: Prims.nat
  -> FStar.Pervasives.Lemma
    (ensures
      x0 - y0 + b0 * Prims.pow2 56 + (x1 - y1 - b0 + b1 * Prims.pow2 56) * Prims.pow2 56 +
      (x2 - y2 - b1 + b2 * Prims.pow2 56) * Prims.pow2 112 +
      (x3 - y3 - b2 + b3 * Prims.pow2 56) * Prims.pow2 168 +
      (x4 - y4 - b3 + b4 * Prims.pow2 56) * Prims.pow2 224 ==
      x0 + x1 * Prims.pow2 56 + x2 * Prims.pow2 112 + x3 * Prims.pow2 168 + x4 * Prims.pow2 224 -
      (y0 + y1 * Prims.pow2 56 + y2 * Prims.pow2 112 + y3 * Prims.pow2 168 + y4 * Prims.pow2 224) +
      b4 * Prims.pow2 280)