val precomp_r19:
    f2:felem5{felem_fits5 f2 (9, 10, 9, 9, 9)}
  -> r19:felem5{felem_fits5 r19 (171, 190, 171, 171, 171)}
let precomp_r19 (f20, f21, f22, f23, f24) =
  [@inline_let]
  let r190 = f20 *! u64 19 in
  [@inline_let]
  let r191 = f21 *! u64 19 in
  [@inline_let]
  let r192 = f22 *! u64 19 in
  [@inline_let]
  let r193 = f23 *! u64 19 in
  [@inline_let]
  let r194 = f24 *! u64 19 in
  (r190, r191, r192, r193, r194)
val precomp_r19:
    f2:felem5{felem_fits5 f2 (9, 10, 9, 9, 9)}
  -> r19:felem5{felem_fits5 r19 (171, 190, 171, 171, 171)}
let precomp_r19 (f20, f21, f22, f23, f24) =
[@@ inline_let ]let r190 = f20 *! u64 19 in
[@@ inline_let ]let r191 = f21 *! u64 19 in
[@@ inline_let ]let r192 = f22 *! u64 19 in
[@@ inline_let ]let r193 = f23 *! u64 19 in
[@@ inline_let ]let r194 = f24 *! u64 19 in
(r190, r191, r192, r193, r194)
Hacl.Spec.Curve25519.Field51.fst.checked
Spec.Curve25519.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Hacl.Spec.Curve25519.Field51.Lemmas.fst.checked Hacl.Spec.Curve25519.Field51.Definition.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked
Hacl.Spec.Curve25519.Field51.fst
Hacl.Spec.Curve25519.Field51.Definition.felem5 Hacl.Spec.Curve25519.Field51.Definition.felem_fits5 FStar.Pervasives.Native.Mktuple5 Prims.nat Lib.IntTypes.uint64 Lib.IntTypes.int_t Lib.IntTypes.U64 Lib.IntTypes.SEC Lib.IntTypes.op_Star_Bang Lib.IntTypes.u64
module Hacl.Spec.Curve25519.Field51

open Lib.Sequence
open Lib.IntTypes
open FStar.Mul
open Spec.Curve25519

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

#reset-options "--z3rlimit 50 --fuel 0 --ifuel 0 --using_facts_from '* -FStar.Seq'"

inline_for_extraction noextract
val fadd5:
    f1:felem5{felem_fits5 f1 (1, 2, 1, 1, 1)}
  -> f2:felem5{felem_fits5 f2 (1, 2, 1, 1, 1)}
  -> out:felem5{felem_fits5 out (2, 4, 2, 2, 2) /\
      feval out == fadd (feval f1) (feval f2)}
let fadd5 (f10, f11, f12, f13, f14) (f20, f21, f22, f23, f24) =
  let o0 = f10 +! f20 in
  let o1 = f11 +! f21 in
  let o2 = f12 +! f22 in
  let o3 = f13 +! f23 in
  let o4 = f14 +! f24 in
  let out = (o0, o1, o2, o3, o4) in
  FStar.Math.Lemmas.lemma_mod_plus_distr_l
    (as_nat5 (f10, f11, f12, f13, f14)) (as_nat5 (f20, f21, f22, f23, f24)) prime;
  FStar.Math.Lemmas.lemma_mod_plus_distr_r
    ((as_nat5 (f10, f11, f12, f13, f14)) % prime) (as_nat5 (f20, f21, f22, f23, f24)) prime;
  out

inline_for_extraction noextract
val fadd_zero:
    f1:felem5{felem_fits5 f1 (1, 2, 1, 1, 1)}
  -> out:felem5{felem_fits5 out (9, 10, 9, 9, 9) /\
      feval out == feval f1}
let fadd_zero (f10, f11, f12, f13, f14) =
  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
  lemma_add_zero (f10, f11, f12, f13, f14);
  (o0, o1, o2, o3, o4)

inline_for_extraction noextract
val fsub5:
    f1:felem5{felem_fits5 f1 (1, 2, 1, 1, 1)}
  -> f2:felem5{felem_fits5 f2 (1, 2, 1, 1, 1)}
  -> out:felem5{felem_fits5 out (9, 10, 9, 9, 9) /\
    feval out == fsub (feval f1) (feval f2)}
let fsub5 (f10, f11, f12, f13, f14) (f20, f21, f22, f23, f24) =
  //assert_norm (0x3fffffffffff68 == pow2 54 - 152);
  //assert_norm (0x3ffffffffffff8 == pow2 54 - 8);
  let (t0, t1, t2, t3, t4) = fadd_zero (f10, f11, f12, f13, f14) in
  let o0 = t0 -! f20 in
  let o1 = t1 -! f21 in
  let o2 = t2 -! f22 in
  let o3 = t3 -! f23 in
  let o4 = t4 -! f24 in
  let out = (o0, o1, o2, o3, o4) in
  FStar.Math.Lemmas.lemma_mod_plus_distr_l
    (as_nat5 (t0, t1, t2, t3, t4)) (- as_nat5 (f20, f21, f22, f23, f24)) prime;
  lemma_mod_sub_distr ((as_nat5 (t0, t1, t2, t3, t4)) % prime) (as_nat5 (f20, f21, f22, f23, f24)) prime;
  out

val lemma_fsub:
    f1:felem5{felem_fits5 f1 (1, 2, 1, 1, 1)}
  -> f2:felem5{felem_fits5 f2 (1, 2, 1, 1, 1)}
  -> Lemma (let (f10, f11, f12, f13, f14) = f1 in
      let (f20, f21, f22, f23, f24) = f2 in
      let o0 = f10 +! u64 0x3fffffffffff68 -! f20 in
      let o1 = f11 +! u64 0x3ffffffffffff8 -! f21 in
      let o2 = f12 +! u64 0x3ffffffffffff8 -! f22 in
      let o3 = f13 +! u64 0x3ffffffffffff8 -! f23 in
      let o4 = f14 +! u64 0x3ffffffffffff8 -! f24 in
      let out = (o0, o1, o2, o3, o4) in
      out == fsub5 (f10, f11, f12, f13, f14) (f20, f21, f22, f23, f24))
let lemma_fsub f1 f2 = ()

inline_for_extraction noextract
val mul_wide64:
    #m1:scale64
  -> #m2:scale64
  -> x:uint64{felem_fits1 x m1}
  -> y:uint64{felem_fits1 y m2 /\ m1 * m2 <= 67108864}
  -> z:uint128{uint_v z == uint_v x * uint_v y /\ felem_wide_fits1 z (m1 * m2)}
#push-options "--z3rlimit 5"
let mul_wide64 #m1 #m2 x y =
  let open FStar.Math.Lemmas in
  lemma_mult_le_left (v x) (v y) (m2 * max51);  //v x * v y <= v x * (m2 * max51)
  lemma_mult_le_right (m2 * max51) (v x) (m1 * max51); // v x * (m2 * max51) <= (m1 * max51) * (m2 * max51)
  paren_mul_right (m1 * max51) m2 max51;  //(m1 * max51) * (m2 * max51) = ((m1 * max51) * m2) * max51
  paren_mul_right m1 max51 m2;  //(m1 * max51) * m2 = m1 * (max51 * m2)
  swap_mul max51 m2;  //max51 * m2 = m2 * max51
  paren_mul_right m1 m2 max51;  //m1 * (m2 * max51) = (m1 * m2) * max51
  paren_mul_right (m1 * m2) max51 max51;  //((m1 * m2) * max51) * max51 = (m1 * m2) * (max51 * max51)
  assert (v x * v y <= m1 * max51 * m2 * max51);
  assert (v x * v y <= m1 * m2 * max51 * max51);
  mul64_wide x y
#pop-options

inline_for_extraction noextract
val smul_felem5:
    #m1:scale64
  -> #m2:scale64_5
  -> u1:uint64{felem_fits1 u1 m1}
  -> f2:felem5{felem_fits5 f2 m2 /\ m1 *^ m2 <=* s128x5 67108864}
  -> out:felem_wide5{felem_wide_fits5 out (m1 *^ m2) /\
      wide_as_nat5 out == uint_v u1 * as_nat5 f2}
let smul_felem5 #m1 #m2 u1 (f20, f21, f22, f23, f24) =
  let (m20, m21, m22, m23, m24) = m2 in
  [@inline_let]
  let o0 = mul_wide64 #m1 #m20 u1 f20 in
  [@inline_let]
  let o1 = mul_wide64 #m1 #m21 u1 f21 in
  [@inline_let]
  let o2 = mul_wide64 #m1 #m22 u1 f22 in
  [@inline_let]
  let o3 = mul_wide64 #m1 #m23 u1 f23 in
  [@inline_let]
  let o4 = mul_wide64 #m1 #m24 u1 f24 in
  [@inline_let]
  let out = (o0, o1, o2, o3, o4) in
  lemma_smul_felem5 u1 (f20, f21, f22, f23, f24);
  out

inline_for_extraction noextract
val mul_add_wide128:
    #m1:scale64
  -> #m2:scale64
  -> #m3:scale128
  -> x:uint64{felem_fits1 x m1}
  -> y:uint64{felem_fits1 y m2}
  -> z:uint128{felem_wide_fits1 z m3 /\ m3 + m1 * m2 <= 67108864}
  -> r:uint128{uint_v r == uint_v z + uint_v x * uint_v y /\ felem_wide_fits1 r (m3 + m1 * m2)}
let mul_add_wide128 #m1 #m2 #m3 x y z =
  z +! mul_wide64 #m1 #m2 x y

#push-options "--z3rlimit 100"
inline_for_extraction noextract
val smul_add_felem5:
    #m1:scale64
  -> #m2:scale64_5
  -> #m3:scale128_5
  -> u1:uint64{felem_fits1 u1 m1}
  -> f2:felem5{felem_fits5 f2 m2}
  -> acc1:felem_wide5{felem_wide_fits5 acc1 m3 /\ m3 +* m1 *^ m2 <=* s128x5 67108864}
  -> acc2:felem_wide5{
      wide_as_nat5 acc2 == wide_as_nat5 acc1 + uint_v u1 * as_nat5 f2 /\
      felem_wide_fits5 acc2 (m3 +* m1 *^ m2)}
let smul_add_felem5 #m1 #m2 #m3 u1 (f20, f21, f22, f23, f24) (o0, o1, o2, o3, o4) =
  let (m20, m21, m22, m23, m24) = m2 in
  let (m30, m31, m32, m33, m34) = m3 in
  [@inline_let]
  let o0' = mul_add_wide128 #m1 #m20 #m30 u1 f20 o0 in
  [@inline_let]
  let o1' = mul_add_wide128 #m1 #m21 #m31 u1 f21 o1 in
  [@inline_let]
  let o2' = mul_add_wide128 #m1 #m22 #m32 u1 f22 o2 in
  [@inline_let]
  let o3' = mul_add_wide128 #m1 #m23 #m33 u1 f23 o3 in
  [@inline_let]
  let o4' = mul_add_wide128 #m1 #m24 #m34 u1 f24 o4 in
  [@inline_let]
  let out = (o0', o1', o2', o3', o4') in
  lemma_smul_add_felem5 u1 (f20, f21, f22, f23, f24) (o0, o1, o2, o3, o4);
  out
#pop-options

inline_for_extraction noextract
val precomp_r19:
    f2:felem5{felem_fits5 f2 (9, 10, 9, 9, 9)}
  -> r19:felem5{felem_fits5 r19 (171, 190, 171, 171, 171)}
val precomp_r19:
    f2:felem5{felem_fits5 f2 (9, 10, 9, 9, 9)}
  -> r19:felem5{felem_fits5 r19 (171, 190, 171, 171, 171)}

    f2:
      Hacl.Spec.Curve25519.Field51.Definition.felem5
        {Hacl.Spec.Curve25519.Field51.Definition.felem_fits5 f2 (9, 10, 9, 9, 9)}
  -> r19:
    Hacl.Spec.Curve25519.Field51.Definition.felem5
      {Hacl.Spec.Curve25519.Field51.Definition.felem_fits5 r19 (171, 190, 171, 171, 171)}