val lemma_mul_inv:
    f:felem5{felem_fits5 f (1, 1, 1, 1, 1)}
  -> cin:uint64{v cin < pow2 51}
  -> Lemma
    (let (i0, i1, i2, i3, i4) = f in
    assert_norm (pow51 = pow2 51);
     let i1' = i1 +! cin in
     let out = (i0, i1', i2, i3, i4) in
     if (v i1 + v cin) / pow2 51 > 0 then
       felem_fits5 out (1, 2, 1, 1, 1) /\
       (v i1 + v cin) % pow2 51 < v cin
     else felem_fits5 out (1, 1, 1, 1, 1))
let lemma_mul_inv f cin =
  assert_norm (pow51 = pow2 51)
val lemma_mul_inv:
    f:felem5{felem_fits5 f (1, 1, 1, 1, 1)}
  -> cin:uint64{v cin < pow2 51}
  -> Lemma
    (let (i0, i1, i2, i3, i4) = f in
    assert_norm (pow51 = pow2 51);
     let i1' = i1 +! cin in
     let out = (i0, i1', i2, i3, i4) in
     if (v i1 + v cin) / pow2 51 > 0 then
       felem_fits5 out (1, 2, 1, 1, 1) /\
       (v i1 + v cin) % pow2 51 < v cin
     else felem_fits5 out (1, 1, 1, 1, 1))
let lemma_mul_inv f cin =
assert_norm (pow51 = pow2 51)
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 Prims.b2t Prims.op_LessThan Lib.IntTypes.v Lib.IntTypes.U64 Lib.IntTypes.SEC Prims.pow2 FStar.Pervasives.assert_norm Prims.op_Equality Prims.pos Hacl.Spec.Curve25519.Field51.Definition.pow51 Prims.unit
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)}
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)

inline_for_extraction noextract
val mul_felem5:
    f1:felem5{felem_fits5 f1 (9, 10, 9, 9, 9)}
  -> r:felem5{felem_fits5 r (9, 10, 9, 9, 9)}
  -> r19:felem5{felem_fits5 r19 (171, 190, 171, 171, 171) /\ r19 == precomp_r19 r}
  -> out:felem_wide5{felem_wide_fits5 out (6579, 4797, 3340, 1881, 423) /\
      feval_wide out == fmul (feval f1) (feval r)}
let mul_felem5 (f10, f11, f12, f13, f14) (r0, r1, r2, r3, r4) (r190, r191, r192, r193, r194) =
  let (o0, o1, o2, o3, o4) = smul_felem5 #9 #(9, 10, 9, 9, 9) f10 (r0, r1, r2, r3, r4) in
  let (o0, o1, o2, o3, o4) = smul_add_felem5 #10 #(171, 9, 10, 9, 9) #(81, 90, 81, 81, 81)
    f11 (r194, r0, r1, r2, r3) (o0, o1, o2, o3, o4) in
  let (o0, o1, o2, o3, o4) = smul_add_felem5 #9 #(171, 171, 9, 10, 9) #(1791, 180, 181, 171, 171)
    f12 (r193, r194, r0, r1, r2) (o0, o1, o2, o3, o4) in
  let (o0, o1, o2, o3, o4) = smul_add_felem5 #9 #(171, 171, 171, 9, 10) #(3330, 1719, 262, 261, 252)
    f13 (r192, r193, r194, r0, r1) (o0, o1, o2, o3, o4) in
  let (o0, o1, o2, o3, o4) = smul_add_felem5 #9 #(190, 171, 171, 171, 9) #(4869, 3258, 1801, 342, 342)
    f14 (r191, r192, r193, r194, r0) (o0, o1, o2, o3, o4) in
  lemma_fmul5 (f10, f11, f12, f13, f14) (r0, r1, r2, r3, r4);
  (o0, o1, o2, o3, o4)

inline_for_extraction noextract
val carry51:
    l:uint64
  -> cin:uint64
  -> Pure (uint64 & uint64)
    (requires felem_fits1 l 2 /\ felem_fits1 cin 8190)
    (ensures fun (l0, l1) ->
      v l + v cin == v l1 * pow2 51 + v l0 /\
      felem_fits1 l0 1 /\ uint_v l1 < pow2 13)
let carry51 l cin =
  let l' = l +! cin in
  lemma_carry51 l cin;
  (l' &. mask51, l' >>. 51ul)

inline_for_extraction noextract
val carry51_wide:
    #m:scale64{m < 8192}
  -> l:uint128{felem_wide_fits1 l m}
  -> cin:uint64
  -> Pure (uint64 & uint64)
    (requires True)
    (ensures fun (l0, l1) ->
      v l + v cin == v l1 * pow2 51 + v l0 /\
      felem_fits1 l0 1 /\ felem_fits1 l1 (m + 1))
let carry51_wide #m l cin =
  let l' = l +! to_u128 cin in
  lemma_carry51_wide #m l cin;
  ((to_u64 l') &. mask51, to_u64 (l' >>. 51ul))

let mul_inv_t (f:felem5) =
  let (o0, o1, o2, o3, o4) = f in
  if v o1 >= pow2 51 then
    felem_fits5 f (1, 2, 1, 1, 1) /\ v o1 % pow2 51 < 8192
  else felem_fits5 f (1, 1, 1, 1, 1)

#push-options "--ifuel 1"
val lemma_mul_inv:
    f:felem5{felem_fits5 f (1, 1, 1, 1, 1)}
  -> cin:uint64{v cin < pow2 51}
  -> Lemma
    (let (i0, i1, i2, i3, i4) = f in
    assert_norm (pow51 = pow2 51);
     let i1' = i1 +! cin in
     let out = (i0, i1', i2, i3, i4) in
     if (v i1 + v cin) / pow2 51 > 0 then
       felem_fits5 out (1, 2, 1, 1, 1) /\
       (v i1 + v cin) % pow2 51 < v cin
     else felem_fits5 out (1, 1, 1, 1, 1))
val lemma_mul_inv:
    f:felem5{felem_fits5 f (1, 1, 1, 1, 1)}
  -> cin:uint64{v cin < pow2 51}
  -> Lemma
    (let (i0, i1, i2, i3, i4) = f in
    assert_norm (pow51 = pow2 51);
     let i1' = i1 +! cin in
     let out = (i0, i1', i2, i3, i4) in
     if (v i1 + v cin) / pow2 51 > 0 then
       felem_fits5 out (1, 2, 1, 1, 1) /\
       (v i1 + v cin) % pow2 51 < v cin
     else felem_fits5 out (1, 1, 1, 1, 1))

    f:
      Hacl.Spec.Curve25519.Field51.Definition.felem5
        {Hacl.Spec.Curve25519.Field51.Definition.felem_fits5 f (1, 1, 1, 1, 1)} ->
    cin: Lib.IntTypes.uint64{Lib.IntTypes.v cin < Prims.pow2 51}
  -> FStar.Pervasives.Lemma
    (ensures
      (let _ = f in
        (let FStar.Pervasives.Native.Mktuple5 #_ #_ #_ #_ #_ i0 i1 i2 i3 i4 = _ in
          FStar.Pervasives.assert_norm (Hacl.Spec.Curve25519.Field51.Definition.pow51 =
              Prims.pow2 51);
          let i1' = i1 +! cin in
          let out = i0, i1', i2, i3, i4 in
          (match (Lib.IntTypes.v i1 + Lib.IntTypes.v cin) / Prims.pow2 51 > 0 with
            | true ->
              Hacl.Spec.Curve25519.Field51.Definition.felem_fits5 out (1, 2, 1, 1, 1) /\
              (Lib.IntTypes.v i1 + Lib.IntTypes.v cin) % Prims.pow2 51 < Lib.IntTypes.v cin
            | _ -> Hacl.Spec.Curve25519.Field51.Definition.felem_fits5 out (1, 1, 1, 1, 1))
          <:
          Type0)
        <:
        Type0))