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 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
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
Math.Lemmas.lemma_div_lt (v s0) 64 52;
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;
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
Math.Lemmas.lemma_div_lt (v s1) 64 40;
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;
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
Math.Lemmas.lemma_div_lt (v s2) 64 28;
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;
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
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
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.felem4 Lib.IntTypes.uint64 Hacl.Spec.K256.Field52.Lemmas1.load_felem5_lemma_fits Prims.unit Hacl.Spec.K256.Field52.Lemmas1.load_felem5_lemma_as_nat FStar.Pervasives.Native.tuple5 Lib.IntTypes.int_t Lib.IntTypes.U64 Lib.IntTypes.SEC FStar.Pervasives.Native.Mktuple5 Prims._assert Prims.b2t Prims.op_Equality Prims.int Lib.IntTypes.v Prims.op_Division Prims.pow2 Lib.IntTypes.op_Greater_Greater_Dot FStar.UInt32.__uint_to_t Prims.op_Addition FStar.Mul.op_Star Prims.op_Modulus Lib.IntTypes.logor_disjoint FStar.Math.Lemmas.cancel_mul_mod Hacl.Spec.K256.MathLemmas.lemma_a_mod_b_mul_c_mod_d Prims.eq2 Lib.IntTypes.mod_mask Lib.IntTypes.mod_mask_lemma FStar.Math.Lemmas.lemma_div_lt Lib.IntTypes.op_Bar_Dot Lib.IntTypes.op_Less_Less_Dot Lib.IntTypes.op_Amp_Dot Lib.IntTypes.u64 Lib.IntTypes.range_t Hacl.Spec.K256.Field52.Definitions.mask52 FStar.Pervasives.assert_norm Prims.op_Subtraction
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)
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)
s: Hacl.Spec.K256.Field52.Definitions.felem4
  -> FStar.Pervasives.Lemma
    (ensures
      (let f = Hacl.Spec.K256.Field52.load_felem5 s in
        Hacl.Spec.K256.Field52.Definitions.felem_fits5 f (1, 1, 1, 1, 1) /\
        Hacl.Spec.K256.Field52.Definitions.as_nat5 f == Hacl.Spec.K256.Field52.Definitions.as_nat4 s
      ))