val carry_round_after_last_carry_mod_prime5_lemma: m:scale64_5 -> f:felem5 -> Lemma
  (requires (let (m0,m1,m2,m3,m4) = m in
    m1 + 1 <= 4096 /\ m2 + 1 <= 4096 /\ m3 + 1 <= 4096 /\ m4 = 1 /\
    felem_fits5 f (m0,m1,m2,m3,1)))
  (ensures (let r = carry_round5 f in
    let (r0,r1,r2,r3,r4) = r in
    let (t0,t1,t2,t3,t4) = f in
    as_nat5 r == as_nat5 f /\ felem_fits5 r (1,1,1,1,2) /\
    v r4 < v t4 + pow2 12 /\ (v r4 >= pow2 48 ==> v r4 % pow2 48 < pow2 12)))
let carry_round_after_last_carry_mod_prime5_lemma m f =
  let (m0,m1,m2,m3,m4) = m in
  let (t0,t1,t2,t3,t4) = f in //(m0,m1,m2,m3,1)

  let t1' = t1 +. (t0 >>. 52ul) in let t0' = t0 &. mask52 in
  LD.lemma_carry52 m1 m0 t1 t0;
  assert (felem_fits1 t1' (m1 + 1));
  assert (felem_fits1 t0' 1);
  assert (v t0' = v t0 % pow2 52);
  assert (v t1' = v t1 + v t0 / pow2 52);

  let t2' = t2 +. (t1' >>. 52ul) in let t1'' = t1' &. mask52 in
  LD.lemma_carry52 m2 (m1 + 1) t2 t1';
  assert (felem_fits1 t2' (m2 + 1));
  assert (felem_fits1 t1'' 1);
  assert (v t1'' = v t1' % pow2 52);
  assert (v t2' = v t2 + v t1' / pow2 52);

  let t3' = t3 +. (t2' >>. 52ul) in let t2'' = t2' &. mask52 in
  LD.lemma_carry52 m3 (m2 + 1) t3 t2';
  assert (felem_fits1 t3' (m3 + 1));
  assert (felem_fits1 t2'' 1);
  assert (v t2'' = v t2' % pow2 52);
  assert (v t3' = v t3 + v t2' / pow2 52);

  let t4' = t4 +. (t3' >>. 52ul) in let t3'' = t3' &. mask52 in
  LD.lemma_carry_last52 m4 (m3 + 1) t4 t3';
  assert (felem_fits_last1 t4' (m4 + 1));
  assert (felem_fits1 t3'' 1);
  assert (v t3'' = v t3' % pow2 52);
  assert (v t4' = v t4 + v t3' / pow2 52);
  LD.carry_last_small_mod_lemma t4 t3';

  ML.lemma_simplify_carry_round (v t0) (v t1) (v t2) (v t3) (v t4);
  let r = carry_round5 f in
  assert ((t0',t1'',t2'',t3'',t4') == r);
  assert (as_nat5 r == as_nat5 f)
val carry_round_after_last_carry_mod_prime5_lemma: m:scale64_5 -> f:felem5 -> Lemma
  (requires (let (m0,m1,m2,m3,m4) = m in
    m1 + 1 <= 4096 /\ m2 + 1 <= 4096 /\ m3 + 1 <= 4096 /\ m4 = 1 /\
    felem_fits5 f (m0,m1,m2,m3,1)))
  (ensures (let r = carry_round5 f in
    let (r0,r1,r2,r3,r4) = r in
    let (t0,t1,t2,t3,t4) = f in
    as_nat5 r == as_nat5 f /\ felem_fits5 r (1,1,1,1,2) /\
    v r4 < v t4 + pow2 12 /\ (v r4 >= pow2 48 ==> v r4 % pow2 48 < pow2 12)))
let carry_round_after_last_carry_mod_prime5_lemma m f =
let m0, m1, m2, m3, m4 = m in
let t0, t1, t2, t3, t4 = f in
let t1' = t1 +. (t0 >>. 52ul) in
let t0' = t0 &. mask52 in
LD.lemma_carry52 m1 m0 t1 t0;
assert (felem_fits1 t1' (m1 + 1));
assert (felem_fits1 t0' 1);
assert (v t0' = v t0 % pow2 52);
assert (v t1' = v t1 + v t0 / pow2 52);
let t2' = t2 +. (t1' >>. 52ul) in
let t1'' = t1' &. mask52 in
LD.lemma_carry52 m2 (m1 + 1) t2 t1';
assert (felem_fits1 t2' (m2 + 1));
assert (felem_fits1 t1'' 1);
assert (v t1'' = v t1' % pow2 52);
assert (v t2' = v t2 + v t1' / pow2 52);
let t3' = t3 +. (t2' >>. 52ul) in
let t2'' = t2' &. mask52 in
LD.lemma_carry52 m3 (m2 + 1) t3 t2';
assert (felem_fits1 t3' (m3 + 1));
assert (felem_fits1 t2'' 1);
assert (v t2'' = v t2' % pow2 52);
assert (v t3' = v t3 + v t2' / pow2 52);
let t4' = t4 +. (t3' >>. 52ul) in
let t3'' = t3' &. mask52 in
LD.lemma_carry_last52 m4 (m3 + 1) t4 t3';
assert (felem_fits_last1 t4' (m4 + 1));
assert (felem_fits1 t3'' 1);
assert (v t3'' = v t3' % pow2 52);
assert (v t4' = v t4 + v t3' / pow2 52);
LD.carry_last_small_mod_lemma t4 t3';
ML.lemma_simplify_carry_round (v t0) (v t1) (v t2) (v t3) (v t4);
let r = carry_round5 f in
assert ((t0', t1'', t2'', t3'', t4') == r);
assert (as_nat5 r == as_nat5 f)
Hacl.Spec.K256.Field52.Lemmas2.fst.checked
Spec.K256.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Hacl.Spec.K256.MathLemmas.fst.checked Hacl.Spec.K256.Field52.Definitions.Lemmas.fst.checked Hacl.Spec.K256.Field52.Definitions.fst.checked Hacl.Spec.K256.Field52.fst.checked FStar.UInt32.fsti.checked FStar.UInt.fsti.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.Lemmas2.fst
Hacl.Spec.K256.Field52.Definitions.scale64_5 Hacl.Spec.K256.Field52.Definitions.felem5 Prims.nat Lib.IntTypes.uint64 Prims._assert Prims.eq2 Hacl.Spec.K256.Field52.Definitions.as_nat5 Prims.unit FStar.Pervasives.Native.tuple5 FStar.Pervasives.Native.Mktuple5 Hacl.Spec.K256.Field52.carry_round5 Hacl.Spec.K256.MathLemmas.lemma_simplify_carry_round Lib.IntTypes.v Lib.IntTypes.U64 Lib.IntTypes.SEC Hacl.Spec.K256.Field52.Definitions.Lemmas.carry_last_small_mod_lemma Prims.b2t Prims.op_Equality Prims.int Prims.op_Addition Prims.op_Division Prims.pow2 Prims.op_Modulus Hacl.Spec.K256.Field52.Definitions.felem_fits1 Hacl.Spec.K256.Field52.Definitions.felem_fits_last1 Hacl.Spec.K256.Field52.Definitions.Lemmas.lemma_carry_last52 Lib.IntTypes.int_t Lib.IntTypes.op_Amp_Dot Hacl.Spec.K256.Field52.Definitions.mask52 Lib.IntTypes.op_Plus_Dot Lib.IntTypes.op_Greater_Greater_Dot FStar.UInt32.__uint_to_t Hacl.Spec.K256.Field52.Definitions.Lemmas.lemma_carry52
module Hacl.Spec.K256.Field52.Lemmas2

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

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

///  Normalize-weak

val minus_x_mul_pow2_256_lemma: m:scale64_5 -> f:felem5 -> Lemma
  (requires felem_fits5 f m)
  (ensures
   (let x, r = minus_x_mul_pow2_256 f in
    let (r0,r1,r2,r3,r4) = r in
    let (m0,m1,m2,m3,m4) = m in
    let (t0,t1,t2,t3,t4) = f in
    v x < pow2 16 /\ v x = v t4 / pow2 48 /\
    v r4 = v t4 % pow2 48 /\
    as_nat5 r == as_nat5 f - v x * pow2 256 /\
    felem_fits5 r (m0,m1,m2,m3,1)))

let minus_x_mul_pow2_256_lemma m f =
  let (m0,m1,m2,m3,m4) = m in
  let (t0,t1,t2,t3,t4) = f in

  let x = t4 >>. 48ul in let t4' = t4 &. mask48 in
  LD.lemma_mask48 t4;

  let r = (t0,t1,t2,t3,t4') in
  calc (==) { // as_nat5 f
    v t0 + v t1 * pow52 + v t2 * pow104 + v t3 * pow156 + v t4 * pow208;
    (==) { Math.Lemmas.euclidean_division_definition (v t4) (pow2 48) }
    v t0 + v t1 * pow52 + v t2 * pow104 + v t3 * pow156 + (v t4 / pow2 48 * pow2 48 + v t4 % pow2 48) * pow208;
    (==) { Math.Lemmas.distributivity_add_left (v t4 / pow2 48 * pow2 48) (v t4 % pow2 48) pow208 }
    v t0 + v t1 * pow52 + v t2 * pow104 + v t3 * pow156 + (v t4 / pow2 48 * pow2 48) * pow208 + (v t4 % pow2 48) * pow208;
    (==) { }
    (v x * pow2 48) * pow208 + as_nat5 r;
    (==) { Math.Lemmas.paren_mul_right (v x) (pow2 48) pow208; Math.Lemmas.pow2_plus 48 208 }
    v x * pow2 256 + as_nat5 r;
  };

  Math.Lemmas.lemma_div_lt (v t4) 64 48


val carry_round_after_last_carry_mod_prime5_lemma: m:scale64_5 -> f:felem5 -> Lemma
  (requires (let (m0,m1,m2,m3,m4) = m in
    m1 + 1 <= 4096 /\ m2 + 1 <= 4096 /\ m3 + 1 <= 4096 /\ m4 = 1 /\
    felem_fits5 f (m0,m1,m2,m3,1)))
  (ensures (let r = carry_round5 f in
    let (r0,r1,r2,r3,r4) = r in
    let (t0,t1,t2,t3,t4) = f in
    as_nat5 r == as_nat5 f /\ felem_fits5 r (1,1,1,1,2) /\
    v r4 < v t4 + pow2 12 /\ (v r4 >= pow2 48 ==> v r4 % pow2 48 < pow2 12)))
val carry_round_after_last_carry_mod_prime5_lemma: m:scale64_5 -> f:felem5 -> Lemma
  (requires (let (m0,m1,m2,m3,m4) = m in
    m1 + 1 <= 4096 /\ m2 + 1 <= 4096 /\ m3 + 1 <= 4096 /\ m4 = 1 /\
    felem_fits5 f (m0,m1,m2,m3,1)))
  (ensures (let r = carry_round5 f in
    let (r0,r1,r2,r3,r4) = r in
    let (t0,t1,t2,t3,t4) = f in
    as_nat5 r == as_nat5 f /\ felem_fits5 r (1,1,1,1,2) /\
    v r4 < v t4 + pow2 12 /\ (v r4 >= pow2 48 ==> v r4 % pow2 48 < pow2 12)))
m: Hacl.Spec.K256.Field52.Definitions.scale64_5 -> f: Hacl.Spec.K256.Field52.Definitions.felem5
  -> FStar.Pervasives.Lemma
      (requires
        (let _ = m in
          (let FStar.Pervasives.Native.Mktuple5 #_ #_ #_ #_ #_ m0 m1 m2 m3 m4 = _ in
            m1 + 1 <= 4096 /\ m2 + 1 <= 4096 /\ m3 + 1 <= 4096 /\ m4 = 1 /\
            Hacl.Spec.K256.Field52.Definitions.felem_fits5 f (m0, m1, m2, m3, 1))
          <:
          Type0))
      (ensures
        (let r = Hacl.Spec.K256.Field52.carry_round5 f in
          let _ = r in
          (let FStar.Pervasives.Native.Mktuple5 #_ #_ #_ #_ #_ _ _ _ _ r4 = _ in
            let _ = f in
            (let FStar.Pervasives.Native.Mktuple5 #_ #_ #_ #_ #_ _ _ _ _ t4 = _ in
              Hacl.Spec.K256.Field52.Definitions.as_nat5 r ==
              Hacl.Spec.K256.Field52.Definitions.as_nat5 f /\
              Hacl.Spec.K256.Field52.Definitions.felem_fits5 r (1, 1, 1, 1, 2) /\
              Lib.IntTypes.v r4 < Lib.IntTypes.v t4 + Prims.pow2 12 /\
              (Lib.IntTypes.v r4 >= Prims.pow2 48 ==>
                Lib.IntTypes.v r4 % Prims.pow2 48 < Prims.pow2 12))
            <:
            Type0)
          <:
          Type0))