val mul15_lemma1: ma:scale64 -> mb:nat -> a:uint64 -> b:uint64 -> Lemma
  (requires felem_fits1 a ma /\ v b <= mb /\ ma * mb <= 4096)
  (ensures  v (a *. b) == v a * v b /\ felem_fits1 (a *. b) (ma * mb))
let mul15_lemma1 ma mb a b =
  assert (v a * v b <= (ma * mb) * max52);
  Math.Lemmas.lemma_mult_le_right max52 (ma * mb) 4096;
  assert (v a * v b <= 4096 * max52);
  assert_norm (4096 * max52 < pow2 64);
  Math.Lemmas.small_mod (v a * v b) (pow2 64)
val mul15_lemma1: ma:scale64 -> mb:nat -> a:uint64 -> b:uint64 -> Lemma
  (requires felem_fits1 a ma /\ v b <= mb /\ ma * mb <= 4096)
  (ensures  v (a *. b) == v a * v b /\ felem_fits1 (a *. b) (ma * mb))
let mul15_lemma1 ma mb a b =
assert (v a * v b <= (ma * mb) * max52);
Math.Lemmas.lemma_mult_le_right max52 (ma * mb) 4096;
assert (v a * v b <= 4096 * max52);
assert_norm (4096 * max52 < pow2 64);
Math.Lemmas.small_mod (v a * v b) (pow2 64)
Hacl.Spec.K256.Field52.Lemmas1.fst.checked
Spec.K256.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Hacl.Spec.K256.MathLemmas.fst.checked Hacl.Spec.K256.Field52.Definitions.fst.checked Hacl.Spec.K256.Field52.fst.checked FStar.UInt32.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.Lemmas1.fst
Hacl.Spec.K256.Field52.Definitions.scale64 Prims.nat Lib.IntTypes.uint64 FStar.Math.Lemmas.small_mod FStar.Mul.op_Star Lib.IntTypes.v Lib.IntTypes.U64 Lib.IntTypes.SEC Prims.pow2 Prims.unit FStar.Pervasives.assert_norm Prims.b2t Prims.op_LessThan Hacl.Spec.K256.Field52.Definitions.max52 Prims._assert Prims.op_LessThanOrEqual FStar.Math.Lemmas.lemma_mult_le_right
module Hacl.Spec.K256.Field52.Lemmas1

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

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

///  Load and store functions

val load_felem5_lemma_as_nat: s:felem4 -> f:felem5 -> Lemma
  (requires
   (let (s0,s1,s2,s3) = s in
    let (f0,f1,f2,f3,f4) = f in
    v f0 == v s0 % pow2 52 /\
    v f1 == v s0 / pow2 52 + v s1 % pow2 40 * pow2 12 /\
    v f2 == v s1 / pow2 40 + v s2 % pow2 28 * pow2 24 /\
    v f3 == v s2 / pow2 28 + v s3 % pow2 16 * pow2 36 /\
    v f4 == v s3 / pow2 16))
  (ensures as_nat5 f == as_nat4 s)

let load_felem5_lemma_as_nat s f =
  let (s0,s1,s2,s3) = s in
  let (f0,f1,f2,f3,f4) = f in
  Math.Lemmas.euclidean_division_definition (v s0) (pow2 52);
  assert_norm (pow2 12 * pow2 52 = pow2 64);
  assert_norm (pow2 52 * pow2 52 = pow2 40 * pow2 64);
  Math.Lemmas.euclidean_division_definition (v s1) (pow2 40);
  assert_norm (pow2 24 * pow2 52 * pow2 52 = pow2 128);
  assert_norm (pow2 52 * pow2 52 * pow2 52 = pow2 28 * pow2 128);
  Math.Lemmas.euclidean_division_definition (v s2) (pow2 25);
  assert_norm (pow2 36 * pow2 52 * pow2 52 * pow2 52 = pow2 192);
  assert_norm (pow2 52 * pow2 52 * pow2 52 * pow2 52 = pow2 16 * pow2 192);
  Math.Lemmas.euclidean_division_definition (v s3) (pow2 16);
  assert (as_nat5 f == v s0 + v s1 * pow2 64 + v s2 * pow2 128 + v s3 * pow2 192)


val load_felem5_lemma_fits: s:felem4 -> f:felem5 -> Lemma
  (requires
   (let (s0,s1,s2,s3) = s in
    let (f0,f1,f2,f3,f4) = f in
    v f0 == v s0 % pow2 52 /\
    v f1 == v s0 / pow2 52 + v s1 % pow2 40 * pow2 12 /\
    v f2 = v s1 / pow2 40 + v s2 % pow2 28 * pow2 24 /\
    v f3 = v s2 / pow2 28 + v s3 % pow2 16 * pow2 36 /\
    v f4 = v s3 / pow2 16))
  (ensures felem_fits5 f (1,1,1,1,1))

let load_felem5_lemma_fits s f =
  let (s0,s1,s2,s3) = s in
  let (f0,f1,f2,f3,f4) = f in
  assert (v f0 < pow2 52);

  Math.Lemmas.lemma_div_lt (v s0) 64 52;
  ML.lemma_a_div_b_plus_c_mod_d_mul_e (v s0) 52 (v s1) 40 12;
  assert (v f1 < pow2 52);

  Math.Lemmas.lemma_div_lt (v s1) 64 40;
  ML.lemma_a_div_b_plus_c_mod_d_mul_e (v s1) 40 (v s2) 28 24;
  assert (v f2 < pow2 52);

  Math.Lemmas.lemma_div_lt (v s2) 64 28;
  ML.lemma_a_div_b_plus_c_mod_d_mul_e (v s2) 28 (v s3) 16 36;
  assert (v f3 < pow2 52);

  assert (v f4 = v s3 / pow2 16);
  Math.Lemmas.lemma_div_lt (v s3) 64 16;
  assert (v f4 < pow2 48)


val load_felem5_lemma: s:felem4 ->
  Lemma (let f = load_felem5 s in
    felem_fits5 f (1,1,1,1,1) /\ as_nat5 f == as_nat4 s)

let load_felem5_lemma s =
  assert_norm (v mask52 = pow2 52 - 1);
  assert_norm (0xffffffffff = pow2 40 - 1);
  assert_norm (0xfffffff = pow2 28 - 1);
  assert_norm (0xffff = pow2 16 - 1);

  let (s0,s1,s2,s3) = s in
  let f0 = s0 &. mask52 in // s0 % pow2 52
  mod_mask_lemma s0 52ul;
  assert (v (mod_mask #U64 #SEC 52ul) == v mask52);
  assert (v f0 = v s0 % pow2 52);

  let f11 = s0 >>. 52ul in
  let f12 = (s1 &. u64 0xffffffffff) <<. 12ul in
  let f1 = f11 |. f12 in // s0 / pow2 52 + (s1 % pow2 40) * pow2 12
  Math.Lemmas.lemma_div_lt (v s0) 64 52;
  //assert (v f11 < pow2 12);
  mod_mask_lemma s1 40ul;
  assert (v (mod_mask #U64 #SEC 40ul) == 0xffffffffff);
  ML.lemma_a_mod_b_mul_c_mod_d (v s1) 40 12 64;
  //assert (v f12 == v s1 % pow2 40 * pow2 12);
  Math.Lemmas.cancel_mul_mod (v s1 % pow2 40) (pow2 12);
  logor_disjoint f11 f12 12;
  assert (v f1 = v s0 / pow2 52 + v s1 % pow2 40 * pow2 12);

  let f21 = s1 >>. 40ul in
  let f22 = (s2 &. u64 0xfffffff) <<. 24ul in
  let f2 = f21 |. f22 in // s1 / pow2 40 + (s2 % pow2 28) * pow2 24
  Math.Lemmas.lemma_div_lt (v s1) 64 40;
  //assert (v f21 < pow2 24);
  mod_mask_lemma s2 28ul;
  assert (v (mod_mask #U64 #SEC 28ul) == 0xfffffff);
  ML.lemma_a_mod_b_mul_c_mod_d (v s2) 28 24 64;
  //assert (v f22 == v s2 % pow2 28 * pow2 24);
  Math.Lemmas.cancel_mul_mod (v s2 % pow2 28) (pow2 24);
  logor_disjoint f21 f22 24;
  assert (v f2 = v s1 / pow2 40 + v s2 % pow2 28 * pow2 24);

  let f31 = s2 >>. 28ul in
  let f32 = (s3 &. u64 0xffff) <<. 36ul in
  let f3 = f31 |. f32 in // s2 / pow2 28 + (s3 % pow2 16) * pow2 36
  Math.Lemmas.lemma_div_lt (v s2) 64 28;
  //assert (v f31 < pow2 36);
  mod_mask_lemma s3 16ul;
  assert (v (mod_mask #U64 #SEC 16ul) == 0xffff);
  ML.lemma_a_mod_b_mul_c_mod_d (v s3) 16 36 64;
  //assert (v f32 == v s3 % pow2 16 * pow2 36);
  Math.Lemmas.cancel_mul_mod (v s3 % pow2 16) (pow2 36);
  logor_disjoint f31 f32 36;
  assert (v f3 = v s2 / pow2 28 + v s3 % pow2 16 * pow2 36);

  let f4 = s3 >>. 16ul in // s3 / pow2 16
  assert (v f4 = v s3 / pow2 16);

  let f = (f0,f1,f2,f3,f4) in
  load_felem5_lemma_as_nat s f;
  load_felem5_lemma_fits s f


val store_felem5_lemma_as_nat: f:felem5 -> s:felem4 -> Lemma
  (requires
   (let (f0,f1,f2,f3,f4) = f in
    let (s0,s1,s2,s3) = s in
    felem_fits5 f (1,1,1,1,1) /\
    v s0 == v f0 + v f1 % pow2 12 * pow2 52 /\
    v s1 == v f1 / pow2 12 + v f2 % pow2 24 * pow2 40 /\
    v s2 == v f2 / pow2 24 + v f3 % pow2 36 * pow2 28 /\
    v s3 == v f3 / pow2 36 + v f4 % pow2 48 * pow2 16))
  (ensures as_nat4 s == as_nat5 f)

let store_felem5_lemma_as_nat f s =
  let (f0,f1,f2,f3,f4) = f in
  let (s0,s1,s2,s3) = s in
  assert (as_nat4 s == v s0 + v s1 * pow2 64 + v s2 * pow2 128 + v s3 * pow2 192);

  calc (==) {
    v s0 + v s1 * pow2 64 + v s2 * pow2 128 + v s3 * pow2 192;
    (==) { }
    v f0 + v f1 % pow2 12 * pow2 52 + (v f1 / pow2 12 + v f2 % pow2 24 * pow2 40) * pow2 64 + v s2 * pow2 128 + v s3 * pow2 192;
    (==) { ML.lemma_a_mul_c_plus_d_mod_e_mul_f_g (v f1) 12 52 (v f2 % pow2 24) 40 64 }
    v f0 + v f1 * pow2 52 + v f2 % pow2 24 * pow2 104 + (v f2 / pow2 24 + v f3 % pow2 36 * pow2 28) * pow2 128 + v s3 * pow2 192;
    (==) { ML.lemma_a_mul_c_plus_d_mod_e_mul_f_g (v f2) 24 104 (v f3 % pow2 36) 28 128 }
    v f0 + v f1 * pow2 52 + v f2 * pow2 104 + v f3 % pow2 36 * pow2 156 + (v f3 / pow2 36 + v f4 % pow2 48 * pow2 16) * pow2 192;
    (==) { ML.lemma_a_mul_c_plus_d_mod_e_mul_f_g (v f3) 36 156 (v f4 % pow2 48) 16 192 }
    v f0 + v f1 * pow2 52 + v f2 * pow2 104 + v f3 * pow2 156 + (v f4 % pow2 48) * pow2 208;
    (==) { Math.Lemmas.small_mod (v f4) (pow2 48) }
    v f0 + v f1 * pow2 52 + v f2 * pow2 104 + v f3 * pow2 156 + v f4 * pow2 208;
    }


val store_felem5_lemma: f:felem5 -> Lemma
  (requires felem_fits5 f (1,1,1,1,1))
  (ensures  as_nat4 (store_felem5 f) == as_nat5 f)

let store_felem5_lemma f =
  let (f0,f1,f2,f3,f4) = f in
  let o0 = f0 |. (f1 <<. 52ul) in
  //assert (v (f1 <<. 52ul) == v f1 * pow2 52 % pow2 64);
  Math.Lemmas.pow2_multiplication_modulo_lemma_2 (v f1) 64 52;
  //assert (v (f1 <<. 52ul) == v f1 % pow2 12 * pow2 52);
  Math.Lemmas.cancel_mul_mod (v f1 % pow2 12) (pow2 52);
  logor_disjoint f0 (f1 <<. 52ul) 52;
  assert (v o0 == v f0 + v f1 % pow2 12 * pow2 52);

  let o1 = (f1 >>. 12ul) |. (f2 <<. 40ul) in
  //assert (v (f1 >>. 12ul) == v f1 / pow2 12);
  Math.Lemmas.lemma_div_lt (v f1) 52 12;
  //assert (v (f2 <<. 40ul) == v f2 * pow2 40 % pow2 64);
  Math.Lemmas.pow2_multiplication_modulo_lemma_2 (v f2) 64 40;
  assert (v (f2 <<. 40ul) == v f2 % pow2 24 * pow2 40);
  Math.Lemmas.cancel_mul_mod (v f2 % pow2 24) (pow2 40);
  logor_disjoint (f1 >>. 12ul) (f2 <<. 40ul) 40;
  assert (v o1 == v f1 / pow2 12 + v f2 % pow2 24 * pow2 40);

  let o2 = (f2 >>. 24ul) |. (f3 <<. 28ul) in
  Math.Lemmas.lemma_div_lt (v f2) 52 24;
  Math.Lemmas.pow2_multiplication_modulo_lemma_2 (v f3) 64 28;
  //assert (v (f3 <<. 28ul) == v f3 % pow2 36 * pow2 28);
  Math.Lemmas.cancel_mul_mod (v f3 % pow2 36) (pow2 28);
  logor_disjoint (f2 >>. 24ul) (f3 <<. 28ul) 28;
  assert (v o2 == v f2 / pow2 24 + v f3 % pow2 36 * pow2 28);

  let o3 = (f3 >>. 36ul) |. (f4 <<. 16ul) in
  Math.Lemmas.lemma_div_lt (v f3) 52 36;
  Math.Lemmas.pow2_multiplication_modulo_lemma_2 (v f4) 64 16;
  //assert (v (f4 <<. 16ul) == v f4 % pow2 48 * pow2 16);
  Math.Lemmas.cancel_mul_mod (v f4 % pow2 48) (pow2 16);
  logor_disjoint (f3 >>. 36ul) (f4 <<. 16ul) 16;
  assert (v o3 == v f3 / pow2 36 + v f4 % pow2 48 * pow2 16);
  store_felem5_lemma_as_nat f (o0,o1,o2,o3)


///  Addition and multiplication by a digit

val add5_lemma1: ma:scale64 -> mb:scale64 -> a:uint64 -> b:uint64 -> Lemma
  (requires felem_fits1 a ma /\ felem_fits1 b mb /\ ma + mb <= 4096)
  (ensures  v (a +. b) == v a + v b /\ felem_fits1 (a +. b) (ma + mb))

let add5_lemma1 ma mb a b =
  assert (v a + v b <= (ma + mb) * max52);
  Math.Lemmas.lemma_mult_le_right max52 (ma + mb) 4096;
  assert (v a + v b <= 4096 * max52);
  assert_norm (4096 * max52 < pow2 64);
  Math.Lemmas.small_mod (v a + v b) (pow2 64)


val add5_lemma_last1: ma:scale64_last -> mb:scale64_last -> a:uint64 -> b:uint64 -> Lemma
  (requires felem_fits_last1 a ma /\ felem_fits_last1 b mb /\ ma + mb <= 65536)
  (ensures  v (a +. b) == v a + v b /\ felem_fits_last1 (a +. b) (ma + mb))

let add5_lemma_last1 ma mb a b =
  assert (v a + v b <= (ma + mb) * max48);
  Math.Lemmas.lemma_mult_le_right max48 (ma + mb) 65536;
  assert (v a + v b <= 65536 * max48);
  assert_norm (65536 * max48 < pow2 64);
  Math.Lemmas.small_mod (v a + v b) (pow2 64)


val add5_lemma: m1:scale64_5 -> m2:scale64_5 -> f1:felem5 -> f2:felem5 -> Lemma
  (requires felem_fits5 f1 m1 /\ felem_fits5 f2 m2 /\ m1 +* m2 <=* (4096,4096,4096,4096,65536))
  (ensures (let r = add5 f1 f2 in
    as_nat5 r == as_nat5 f1 + as_nat5 f2 /\ felem_fits5 r (m1 +* m2)))

let add5_lemma m1 m2 f1 f2 =
  let (a0,a1,a2,a3,a4) = f1 in
  let (b0,b1,b2,b3,b4) = f2 in
  let (ma0,ma1,ma2,ma3,ma4) = m1 in
  let (mb0,mb1,mb2,mb3,mb4) = m2 in
  add5_lemma1 ma0 mb0 a0 b0;
  add5_lemma1 ma1 mb1 a1 b1;
  add5_lemma1 ma2 mb2 a2 b2;
  add5_lemma1 ma3 mb3 a3 b3;
  add5_lemma_last1 ma4 mb4 a4 b4


val mul15_lemma1: ma:scale64 -> mb:nat -> a:uint64 -> b:uint64 -> Lemma
  (requires felem_fits1 a ma /\ v b <= mb /\ ma * mb <= 4096)
  (ensures  v (a *. b) == v a * v b /\ felem_fits1 (a *. b) (ma * mb))
val mul15_lemma1: ma:scale64 -> mb:nat -> a:uint64 -> b:uint64 -> Lemma
  (requires felem_fits1 a ma /\ v b <= mb /\ ma * mb <= 4096)
  (ensures  v (a *. b) == v a * v b /\ felem_fits1 (a *. b) (ma * mb))

    ma: Hacl.Spec.K256.Field52.Definitions.scale64 ->
    mb: Prims.nat ->
    a: Lib.IntTypes.uint64 ->
    b: Lib.IntTypes.uint64
  -> FStar.Pervasives.Lemma
      (requires
        Hacl.Spec.K256.Field52.Definitions.felem_fits1 a ma /\ Lib.IntTypes.v b <= mb /\
        ma * mb <= 4096)
      (ensures
        Lib.IntTypes.v (a *. b) == Lib.IntTypes.v a * Lib.IntTypes.v b /\
        Hacl.Spec.K256.Field52.Definitions.felem_fits1 (a *. b) (ma * mb))