val lemma_add_zero:
  f1:felem5{felem_fits5 f1 (1, 2, 1, 1, 1)}
  -> Lemma (
    let (f10, f11, f12, f13, f14) = f1 in
    let o0 = f10 +! u64 0x3fffffffffff68 in
    let o1 = f11 +! u64 0x3ffffffffffff8 in
    let o2 = f12 +! u64 0x3ffffffffffff8 in
    let o3 = f13 +! u64 0x3ffffffffffff8 in
    let o4 = f14 +! u64 0x3ffffffffffff8 in
    let out = (o0, o1, o2, o3, o4) in
    feval out == feval f1)
let lemma_add_zero f1 =
  let (f10, f11, f12, f13, f14) = f1 in
  let o0 = f10 +! u64 0x3fffffffffff68 in
  let o1 = f11 +! u64 0x3ffffffffffff8 in
  let o2 = f12 +! u64 0x3ffffffffffff8 in
  let o3 = f13 +! u64 0x3ffffffffffff8 in
  let o4 = f14 +! u64 0x3ffffffffffff8 in
  let out = (o0, o1, o2, o3, o4) in
  assert (feval out ==
    (v f10 + 0x3fffffffffff68 +
    (v f11 + 0x3ffffffffffff8) * pow51 +
    (v f12 + 0x3ffffffffffff8) * pow51 * pow51 +
    (v f13 + 0x3ffffffffffff8) * pow51 * pow51 * pow51 +
    (v f14 + 0x3ffffffffffff8) * pow51 * pow51 * pow51 * pow51) % prime);
  FStar.Math.Lemmas.distributivity_add_left (v f11) 0x3ffffffffffff8 pow51;
  FStar.Math.Lemmas.distributivity_add_left (v f12) 0x3ffffffffffff8 (pow51 * pow51);
  FStar.Math.Lemmas.distributivity_add_left (v f13) 0x3ffffffffffff8 (pow51 * pow51 * pow51);
  FStar.Math.Lemmas.distributivity_add_left (v f14) 0x3ffffffffffff8 (pow51 * pow51 * pow51 * pow51);
  assert_norm (
    0x3fffffffffff68 +
    0x3ffffffffffff8 * pow51 +
    0x3ffffffffffff8 * pow51 * pow51 +
    0x3ffffffffffff8 * pow51 * pow51 * pow51 +
    0x3ffffffffffff8 * pow51 * pow51 * pow51 * pow51 = 8 * prime);
  assert (feval out == (v f10 + v f11 * pow51 +
    v f12 * pow51 * pow51 + v f13 * pow51 * pow51 * pow51 +
    v f14 * pow51 * pow51 * pow51 * pow51 + 8 * prime) % prime);
  FStar.Math.Lemmas.lemma_mod_plus (as_nat5 f1) 8 prime;
  assert (feval out == (v f10 + v f11 * pow51 +
    v f12 * pow51 * pow51 + v f13 * pow51 * pow51 * pow51 +
    v f14 * pow51 * pow51 * pow51 * pow51) % prime)
val lemma_add_zero:
  f1:felem5{felem_fits5 f1 (1, 2, 1, 1, 1)}
  -> Lemma (
    let (f10, f11, f12, f13, f14) = f1 in
    let o0 = f10 +! u64 0x3fffffffffff68 in
    let o1 = f11 +! u64 0x3ffffffffffff8 in
    let o2 = f12 +! u64 0x3ffffffffffff8 in
    let o3 = f13 +! u64 0x3ffffffffffff8 in
    let o4 = f14 +! u64 0x3ffffffffffff8 in
    let out = (o0, o1, o2, o3, o4) in
    feval out == feval f1)
let lemma_add_zero f1 =
let f10, f11, f12, f13, f14 = f1 in
let o0 = f10 +! u64 0x3fffffffffff68 in
let o1 = f11 +! u64 0x3ffffffffffff8 in
let o2 = f12 +! u64 0x3ffffffffffff8 in
let o3 = f13 +! u64 0x3ffffffffffff8 in
let o4 = f14 +! u64 0x3ffffffffffff8 in
let out = (o0, o1, o2, o3, o4) in
assert (feval out ==
    (v f10 + 0x3fffffffffff68 + (v f11 + 0x3ffffffffffff8) * pow51 +
      ((v f12 + 0x3ffffffffffff8) * pow51) * pow51 +
      (((v f13 + 0x3ffffffffffff8) * pow51) * pow51) * pow51 +
      ((((v f14 + 0x3ffffffffffff8) * pow51) * pow51) * pow51) * pow51) %
    prime);
FStar.Math.Lemmas.distributivity_add_left (v f11) 0x3ffffffffffff8 pow51;
FStar.Math.Lemmas.distributivity_add_left (v f12) 0x3ffffffffffff8 (pow51 * pow51);
FStar.Math.Lemmas.distributivity_add_left (v f13) 0x3ffffffffffff8 ((pow51 * pow51) * pow51);
FStar.Math.Lemmas.distributivity_add_left (v f14)
  0x3ffffffffffff8
  (((pow51 * pow51) * pow51) * pow51);
assert_norm (0x3fffffffffff68 + 0x3ffffffffffff8 * pow51 + (0x3ffffffffffff8 * pow51) * pow51 +
    ((0x3ffffffffffff8 * pow51) * pow51) * pow51 +
    (((0x3ffffffffffff8 * pow51) * pow51) * pow51) * pow51 =
    8 * prime);
assert (feval out ==
    (v f10 + v f11 * pow51 + (v f12 * pow51) * pow51 + ((v f13 * pow51) * pow51) * pow51 +
      (((v f14 * pow51) * pow51) * pow51) * pow51 +
      8 * prime) %
    prime);
FStar.Math.Lemmas.lemma_mod_plus (as_nat5 f1) 8 prime;
assert (feval out ==
    (v f10 + v f11 * pow51 + (v f12 * pow51) * pow51 + ((v f13 * pow51) * pow51) * pow51 +
      (((v f14 * pow51) * pow51) * pow51) * pow51) %
    prime)
Hacl.Spec.Curve25519.Field51.Lemmas.fst.checked
Spec.Curve25519.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Hacl.Spec.Curve25519.Field51.Definition.fst.checked Hacl.Impl.Curve25519.Lemmas.fst.checked FStar.UInt32.fsti.checked FStar.Tactics.Canon.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked
Hacl.Spec.Curve25519.Field51.Lemmas.fst
Hacl.Spec.Curve25519.Field51.Definition.felem5 Hacl.Spec.Curve25519.Field51.Definition.felem_fits5 FStar.Pervasives.Native.Mktuple5 Prims.nat Lib.IntTypes.uint64 Prims._assert Prims.eq2 Prims.int Hacl.Spec.Curve25519.Field51.Definition.feval Prims.op_Modulus Prims.op_Addition Lib.IntTypes.v Lib.IntTypes.U64 Lib.IntTypes.SEC FStar.Mul.op_Star Hacl.Spec.Curve25519.Field51.Definition.pow51 Spec.Curve25519.prime Prims.unit FStar.Math.Lemmas.lemma_mod_plus Hacl.Spec.Curve25519.Field51.Definition.as_nat5 FStar.Pervasives.assert_norm Prims.b2t Prims.op_Equality FStar.Math.Lemmas.distributivity_add_left FStar.Pervasives.Native.tuple5 Lib.IntTypes.int_t Lib.IntTypes.op_Plus_Bang Lib.IntTypes.u64
module Hacl.Spec.Curve25519.Field51.Lemmas

open FStar.Mul
open Lib.Sequence
open Lib.IntTypes

open FStar.Tactics
open FStar.Tactics.Canon

open Spec.Curve25519
open Hacl.Spec.Curve25519.Field51.Definition

module BSeq = Lib.ByteSequence
module LSeq = Lib.Sequence

#reset-options "--z3rlimit 50 --using_facts_from '* -FStar.Seq -FStar.Tactics'"

val lemma_mod_sub_distr: a:int -> b:int -> n:pos ->
  Lemma ((a - b % n) % n = (a - b) % n)
let lemma_mod_sub_distr a b n =
  FStar.Math.Lemmas.lemma_div_mod b n;
  FStar.Math.Lemmas.distributivity_sub_left 0 (b / n) n;
  // (a - b) % n == (a - (b % n) - (b / n) * n) % n
  FStar.Math.Lemmas.lemma_mod_plus (a - (b % n)) (-(b / n)) n

val lemma_mul5_distr_r:
  a:nat -> b:nat -> c:nat -> d:nat -> e:nat -> f:nat ->
  Lemma ((a + b + c + d + e) * f == a * f + b * f + c * f + d * f + e * f)
let lemma_mul5_distr_r a b c d e f = ()

val lemma_mul5_distr_l:
  a:nat -> b:nat -> c:nat -> d:nat -> e:nat -> f:nat ->
  Lemma (a * (b + c + d + e + f) == a * b + a * c + a * d + a * e + a * f)
let lemma_mul5_distr_l a b c d e f = ()

val lemma_mul_assos_3:
  a:nat -> b:nat -> c:nat ->
  Lemma (a * b * c == a * (b * c))
let lemma_mul_assos_3 a b c = ()

val lemma_mul_assos_4:
  a:nat -> b:nat -> c:nat -> d:nat ->
  Lemma (a * b * c * d == a * (b * c * d))
let lemma_mul_assos_4 a b c d = ()

val lemma_mul_assos_5:
  a:nat -> b:nat -> c:nat -> d:nat -> e:nat ->
  Lemma (a * b * c * d * e == a * (b * c * d * e))
let lemma_mul_assos_5 a b c d e = ()

val lemma_mul_assos_6:
  a:nat -> b:nat -> c:nat -> d:nat -> e:nat -> f:nat ->
  Lemma (a * b * c * d * e * f == a * (b * c * d * e * f))
let lemma_mul_assos_6 a b c d e f = ()

val lemma_add_le:a:nat -> b:nat -> c:nat -> d:nat ->
  Lemma
  (requires a <= b /\ c <= d)
  (ensures  a + c <= b + d)
let lemma_add_le a b c d = ()

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

val lemma_prime: unit ->
  Lemma (pow2 255 % prime = 19)
let lemma_prime () =
  assert_norm (pow2 255 % prime = 19 % prime);
  assert_norm (19 < prime);
  FStar.Math.Lemmas.modulo_lemma 19 prime

val lemma_add_zero:
  f1:felem5{felem_fits5 f1 (1, 2, 1, 1, 1)}
  -> Lemma (
    let (f10, f11, f12, f13, f14) = f1 in
    let o0 = f10 +! u64 0x3fffffffffff68 in
    let o1 = f11 +! u64 0x3ffffffffffff8 in
    let o2 = f12 +! u64 0x3ffffffffffff8 in
    let o3 = f13 +! u64 0x3ffffffffffff8 in
    let o4 = f14 +! u64 0x3ffffffffffff8 in
    let out = (o0, o1, o2, o3, o4) in
val lemma_add_zero:
  f1:felem5{felem_fits5 f1 (1, 2, 1, 1, 1)}
  -> Lemma (
    let (f10, f11, f12, f13, f14) = f1 in
    let o0 = f10 +! u64 0x3fffffffffff68 in
    let o1 = f11 +! u64 0x3ffffffffffff8 in
    let o2 = f12 +! u64 0x3ffffffffffff8 in
    let o3 = f13 +! u64 0x3ffffffffffff8 in
    let o4 = f14 +! u64 0x3ffffffffffff8 in
    let out = (o0, o1, o2, o3, o4) in
    feval out == feval f1)

    f1:
      Hacl.Spec.Curve25519.Field51.Definition.felem5
        {Hacl.Spec.Curve25519.Field51.Definition.felem_fits5 f1 (1, 2, 1, 1, 1)}
  -> FStar.Pervasives.Lemma
    (ensures
      (let _ = f1 in
        (let FStar.Pervasives.Native.Mktuple5 #_ #_ #_ #_ #_ f10 f11 f12 f13 f14 = _ in
          let o0 = f10 +! Lib.IntTypes.u64 0x3fffffffffff68 in
          let o1 = f11 +! Lib.IntTypes.u64 0x3ffffffffffff8 in
          let o2 = f12 +! Lib.IntTypes.u64 0x3ffffffffffff8 in
          let o3 = f13 +! Lib.IntTypes.u64 0x3ffffffffffff8 in
          let o4 = f14 +! Lib.IntTypes.u64 0x3ffffffffffff8 in
          let out = o0, o1, o2, o3, o4 in
          Hacl.Spec.Curve25519.Field51.Definition.feval out ==
          Hacl.Spec.Curve25519.Field51.Definition.feval f1)
        <:
        Type0))