val lemma_mul_sub (mc:nat) (a b c:uint64) : Lemma
  (requires
    v a <= max52 /\ max52 <= v a * 2 /\ v c <= mc * max52 /\
    mc <= v b /\ 2 * v b <= 4096)
  (ensures (let r = a *. u64 2 *. b -. c in
    v r = v a * 2 * v b - v c /\
    felem_fits1 r (2 * v b)))
let lemma_mul_sub mc a b c =
  let r = a *. u64 2 *. b -. c in
  assert (v c <= mc * max52);
  ML.lemma_ab_le_cd mc max52 (v b) (v a * 2);
  assert (v c <= v a * 2 * v b);

  assert (v a * 2 * v b - v c <= v a * 2 * v b);
  Math.Lemmas.paren_mul_right (v a) 2 (v b);
  ML.lemma_ab_le_cd (v a) (2 * v b) max52 4096;
  assert_norm (4096 * max52 < pow2 64);
  Math.Lemmas.small_mod (v a * 2 * v b - v c) (pow2 64);
  assert (v r = v a * 2 * v b - v c);

  ML.lemma_ab_le_cd (v a) (2 * v b) max52 (2 * v b);
  assert (felem_fits1 r (2 * v b))
val lemma_mul_sub (mc:nat) (a b c:uint64) : Lemma
  (requires
    v a <= max52 /\ max52 <= v a * 2 /\ v c <= mc * max52 /\
    mc <= v b /\ 2 * v b <= 4096)
  (ensures (let r = a *. u64 2 *. b -. c in
    v r = v a * 2 * v b - v c /\
    felem_fits1 r (2 * v b)))
let lemma_mul_sub mc a b c =
let r = a *. u64 2 *. b -. c in
assert (v c <= mc * max52);
ML.lemma_ab_le_cd mc max52 (v b) (v a * 2);
assert (v c <= (v a * 2) * v b);
assert ((v a * 2) * v b - v c <= (v a * 2) * v b);
Math.Lemmas.paren_mul_right (v a) 2 (v b);
ML.lemma_ab_le_cd (v a) (2 * v b) max52 4096;
assert_norm (4096 * max52 < pow2 64);
Math.Lemmas.small_mod ((v a * 2) * v b - v c) (pow2 64);
assert (v r = (v a * 2) * v b - v c);
ML.lemma_ab_le_cd (v a) (2 * v b) max52 (2 * v b);
assert (felem_fits1 r (2 * v b))
Hacl.Spec.K256.Field52.Lemmas.fst.checked
Spec.K256.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Hacl.Spec.K256.MathLemmas.fst.checked Hacl.Spec.K256.Field52.Lemmas3.fst.checked Hacl.Spec.K256.Field52.Lemmas2.fst.checked Hacl.Spec.K256.Field52.Lemmas1.fst.checked Hacl.Spec.K256.Field52.Definitions.Lemmas.fst.checked Hacl.Spec.K256.Field52.Definitions.fst.checked Hacl.Spec.K256.Field52.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.K256.Field52.Lemmas.fst
Prims.nat Lib.IntTypes.uint64 Prims._assert Prims.b2t Hacl.Spec.K256.Field52.Definitions.felem_fits1 FStar.Mul.op_Star Lib.IntTypes.v Lib.IntTypes.U64 Lib.IntTypes.SEC Prims.unit Hacl.Spec.K256.MathLemmas.lemma_ab_le_cd Hacl.Spec.K256.Field52.Definitions.max52 Prims.op_Equality Prims.int Prims.op_Subtraction FStar.Math.Lemmas.small_mod Prims.pow2 FStar.Pervasives.assert_norm Prims.op_LessThan FStar.Math.Lemmas.paren_mul_right Prims.op_LessThanOrEqual Lib.IntTypes.int_t Lib.IntTypes.op_Subtraction_Dot Lib.IntTypes.op_Star_Dot Lib.IntTypes.u64
module Hacl.Spec.K256.Field52.Lemmas

open FStar.Mul
open Lib.IntTypes

module S = Spec.K256

include Hacl.Spec.K256.Field52.Definitions
include Hacl.Spec.K256.Field52

module ML = Hacl.Spec.K256.MathLemmas
module LD = Hacl.Spec.K256.Field52.Definitions.Lemmas
module L1 = Hacl.Spec.K256.Field52.Lemmas1
module L2 = Hacl.Spec.K256.Field52.Lemmas2
module L3 = Hacl.Spec.K256.Field52.Lemmas3

#set-options "--z3rlimit 100 --fuel 0 --ifuel 0"

let load_felem5_lemma s =
  L1.load_felem5_lemma s


let store_felem5_lemma f =
  L1.store_felem5_lemma f


let add5_lemma m1 m2 f1 f2 =
  L1.add5_lemma m1 m2 f1 f2


let fadd5_lemma m1 m2 f1 f2 =
  let r = add5 f1 f2 in
  add5_lemma m1 m2 f1 f2;
  assert (as_nat5 r == as_nat5 f1 + as_nat5 f2);
  Math.Lemmas.modulo_distributivity (as_nat5 f1) (as_nat5 f2) S.prime


let mul15_lemma m1 m2 f c =
  L1.mul15_lemma m1 m2 f c


let fmul15_lemma m1 m2 f c =
  let r = mul15 f c in
  mul15_lemma m1 m2 f c;
  assert (as_nat5 r == v c * as_nat5 f);
  Math.Lemmas.lemma_mod_mul_distr_r (v c) (as_nat5 f) S.prime


#push-options "--ifuel 1"
let is_felem_zero_vartime5_lemma f = ()


let is_felem_ge_prime_vartime5_lemma f =
  let p =
   (u64 0xffffefffffc2f,
    u64 0xfffffffffffff,
    u64 0xfffffffffffff,
    u64 0xfffffffffffff,
    u64 0xffffffffffff) in
  assert_norm (S.prime = as_nat5 p);
  assert_norm (0xffffefffffc2f <= max52);
  assert_norm (0xfffffffffffff = max52);
  assert_norm (0xffffffffffff = max48);
  assert (felem_fits5 p (1,1,1,1,1));
  //LD.lemma_as_nat_decompose f;
  //LD.lemma_as_nat_decompose p;
  LD.lemma_as_nat_bound f;
  LD.lemma_as_nat_bound p


let is_felem_lt_prime_minus_order_vartime5_lemma f =
  assert_norm (S.prime - S.q =
    0xda1722fc9baee + 0x1950b75fc4402 * pow52 + 0x1455123 * pow104)


let is_felem_eq_vartime5_lemma f1 f2 =
  if as_nat5 f1 = as_nat5 f2 then LD.as_nat_inj f1 f2
#pop-options


let normalize_weak5_lemma m f =
  let r = normalize_weak5 f in
  let (t0,t1,t2,t3,t4) = f in
  L2.normalize_weak5_lemma m f;
  assert (as_nat5 r == as_nat5 f - v t4 / pow2 48 * S.prime);
  Math.Lemmas.lemma_mod_sub (as_nat5 f) S.prime (v t4 / pow2 48)


let normalize5_lemma m f =
  L2.normalize5_lemma m f


let fmul5_lemma a b =
  L3.fmul5_lemma a b

let fmul5_lemma1 a b =
  let r = fmul5 a b in
  L3.fmul5_lemma a b;
  assert (as_nat5 r % S.prime == as_nat5 a * as_nat5 b % S.prime);
  ML.lemma_mod_mul_distr (as_nat5 a) (as_nat5 b) S.prime


let fsqr5_lemma a =
  L3.fsqr5_lemma a

let fsqr5_lemma1 a =
  let r = fsqr5 a in
  L3.fsqr5_lemma a;
  assert (as_nat5 r % S.prime == as_nat5 a * as_nat5 a % S.prime);
  ML.lemma_mod_mul_distr (as_nat5 a) (as_nat5 a) S.prime


val lemma_mul_sub (mc:nat) (a b c:uint64) : Lemma
  (requires
    v a <= max52 /\ max52 <= v a * 2 /\ v c <= mc * max52 /\
    mc <= v b /\ 2 * v b <= 4096)
  (ensures (let r = a *. u64 2 *. b -. c in
    v r = v a * 2 * v b - v c /\
    felem_fits1 r (2 * v b)))
val lemma_mul_sub (mc:nat) (a b c:uint64) : Lemma
  (requires
    v a <= max52 /\ max52 <= v a * 2 /\ v c <= mc * max52 /\
    mc <= v b /\ 2 * v b <= 4096)
  (ensures (let r = a *. u64 2 *. b -. c in
    v r = v a * 2 * v b - v c /\
    felem_fits1 r (2 * v b)))
mc: Prims.nat -> a: Lib.IntTypes.uint64 -> b: Lib.IntTypes.uint64 -> c: Lib.IntTypes.uint64
  -> FStar.Pervasives.Lemma
      (requires
        Lib.IntTypes.v a <= Hacl.Spec.K256.Field52.Definitions.max52 /\
        Hacl.Spec.K256.Field52.Definitions.max52 <= Lib.IntTypes.v a * 2 /\
        Lib.IntTypes.v c <= mc * Hacl.Spec.K256.Field52.Definitions.max52 /\ mc <= Lib.IntTypes.v b /\
        2 * Lib.IntTypes.v b <= 4096)
      (ensures
        (let r = a *. Lib.IntTypes.u64 2 *. b -. c in
          Lib.IntTypes.v r = (Lib.IntTypes.v a * 2) * Lib.IntTypes.v b - Lib.IntTypes.v c /\
          Hacl.Spec.K256.Field52.Definitions.felem_fits1 r (2 * Lib.IntTypes.v b)))