val felem_to_list_lemma_eval: x:S.felem ->
  Lemma (as_nat5 (list_as_felem5 (felem_to_list x)) == x)
let felem_to_list_lemma_eval x =
  felem_to_list_index_lemma x;
  let x0 = x % pow52 in
  let x1 = x / pow52 % pow52 in
  let x2 = x / pow104 % pow52 in
  let x3 = x / pow156 % pow52 in
  let x4 = x / pow208 in
  let (f0, f1, f2, f3, f4) = list_as_felem5 (felem_to_list x) in
  let nat_x = as_nat5 (f0, f1, f2, f3, f4) in
  assert (nat_x == x0 + x1 * pow52 + x2 * pow104 + x3 * pow156 + x4 * pow208);
  calc (==) {
    x0 + x1 * pow52 + x2 * pow104 + x3 * pow156 + x4 * pow208;
    (==) { }
    x0 + x1 * pow52 + x2 * pow104 + (x / pow156 % pow52) * pow156 + x / pow208 * pow208;
    (==) { lemma_mod_pow2_sub x 156 52 }
    x0 + x1 * pow52 + x2 * pow104 + x % pow208 - x % pow156 + x / pow208 * pow208;
    (==) { Math.Lemmas.euclidean_division_definition x pow208 }
    x0 + x1 * pow52 + (x / pow104 % pow52) * pow104 - x % pow156 + x;
    (==) { lemma_mod_pow2_sub x 104 52 }
    x0 + (x / pow52 % pow52) * pow52 - x % pow104 + x;
    (==) { lemma_mod_pow2_sub x 52 52 }
    x;
  }
val felem_to_list_lemma_eval: x:S.felem ->
  Lemma (as_nat5 (list_as_felem5 (felem_to_list x)) == x)
let felem_to_list_lemma_eval x =
felem_to_list_index_lemma x;
let x0 = x % pow52 in
let x1 = x / pow52 % pow52 in
let x2 = x / pow104 % pow52 in
let x3 = x / pow156 % pow52 in
let x4 = x / pow208 in
let f0, f1, f2, f3, f4 = list_as_felem5 (felem_to_list x) in
let nat_x = as_nat5 (f0, f1, f2, f3, f4) in
assert (nat_x == x0 + x1 * pow52 + x2 * pow104 + x3 * pow156 + x4 * pow208);
calc ( == ) {
  x0 + x1 * pow52 + x2 * pow104 + x3 * pow156 + x4 * pow208;
  ( == ) { () }
  x0 + x1 * pow52 + x2 * pow104 + (x / pow156 % pow52) * pow156 + (x / pow208) * pow208;
  ( == ) { lemma_mod_pow2_sub x 156 52 }
  x0 + x1 * pow52 + x2 * pow104 + x % pow208 - x % pow156 + (x / pow208) * pow208;
  ( == ) { Math.Lemmas.euclidean_division_definition x pow208 }
  x0 + x1 * pow52 + (x / pow104 % pow52) * pow104 - x % pow156 + x;
  ( == ) { lemma_mod_pow2_sub x 104 52 }
  x0 + (x / pow52 % pow52) * pow52 - x % pow104 + x;
  ( == ) { lemma_mod_pow2_sub x 52 52 }
  x;
}
Hacl.Spec.K256.PrecompTable.fst.checked
Spec.K256.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Hacl.Spec.PrecompBaseTable.fsti.checked Hacl.Spec.K256.Field52.Definitions.fst.checked Hacl.Impl.K256.Point.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.List.Tot.fst.checked FStar.Calc.fsti.checked
Hacl.Spec.K256.PrecompTable.fst
Spec.K256.PointOps.felem Lib.IntTypes.uint64 FStar.Calc.calc_finish Prims.int Prims.eq2 Prims.op_Addition FStar.Mul.op_Star Hacl.Spec.K256.Field52.Definitions.pow52 Hacl.Spec.K256.Field52.Definitions.pow104 Hacl.Spec.K256.Field52.Definitions.pow156 Hacl.Spec.K256.Field52.Definitions.pow208 Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step Prims.op_Subtraction Prims.op_Modulus Prims.op_Division FStar.Calc.calc_init FStar.Calc.calc_pack Prims.squash Hacl.Spec.K256.PrecompTable.lemma_mod_pow2_sub FStar.Math.Lemmas.euclidean_division_definition Prims._assert Prims.nat Hacl.Spec.K256.Field52.Definitions.as_nat5 FStar.Pervasives.Native.Mktuple5 Hacl.Spec.K256.Field52.Definitions.felem5 Hacl.Spec.K256.PrecompTable.list_as_felem5 Hacl.Spec.K256.PrecompTable.felem_to_list Hacl.Spec.K256.PrecompTable.felem_to_list_index_lemma
module Hacl.Spec.K256.PrecompTable

open FStar.Mul
open Lib.IntTypes
open Lib.Sequence

open Hacl.Spec.K256.Field52.Definitions
open Hacl.Impl.K256.Point

module S = Spec.K256
module FL = FStar.List.Tot
module SPT = Hacl.Spec.PrecompBaseTable

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

let create5_lseq (x0 x1 x2 x3 x4:uint64) : lseq uint64 5 =
  let l = [x0; x1; x2; x3; x4] in
  assert_norm (FL.length l = 5);
  Seq.seq_of_list l


val create5_lemma (x0 x1 x2 x3 x4:uint64) :
  Lemma (let s = create5_lseq x0 x1 x2 x3 x4 in
    s.[0] == x0 /\ s.[1] == x1 /\ s.[2] == x2 /\ s.[3] == x3 /\ s.[4] == x4)
let create5_lemma x0 x1 x2 x3 x4 =
  Seq.elim_of_list [x0; x1; x2; x3; x4]

//-----------------------------------

noextract
let list_as_felem5 (f:felem_list) : felem5 =
  let x = Seq.seq_of_list f <: lseq uint64 5 in
  as_felem5_lseq x


val felem_to_list_index_lemma: x:S.felem ->
  Lemma (let (f0, f1, f2, f3, f4) = list_as_felem5 (felem_to_list x) in
    let x0 = x % pow52 in
    let x1 = x / pow52 % pow52 in
    let x2 = x / pow104 % pow52 in
    let x3 = x / pow156 % pow52 in
    let x4 = x / pow208 in
    v f0 == x0 /\ v f1 == x1 /\ v f2 == x2 /\ v f3 == x3 /\ v f4 == x4)

let felem_to_list_index_lemma x =
  let x0 = x % pow52 in
  let x1 = x / pow52 % pow52 in
  let x2 = x / pow104 % pow52 in
  let x3 = x / pow156 % pow52 in
  let x4 = x / pow208 in
  let f = felem_to_list x in

  let (f0, f1, f2, f3, f4) = list_as_felem5 f in
  create5_lemma (u64 x0) (u64 x1) (u64 x2) (u64 x3) (u64 x4);
  assert (v f0 == x0 /\ v f1 == x1 /\ v f2 == x2 /\ v f3 == x3 /\ v f4 == x4)


val felem_to_list_lemma_fits: x:S.felem ->
  Lemma (felem_fits5 (list_as_felem5 (felem_to_list x)) (1, 1, 1, 1, 1))

let felem_to_list_lemma_fits x =
  felem_to_list_index_lemma x;
  let x0 = x % pow52 in
  let x1 = x / pow52 % pow52 in
  let x2 = x / pow104 % pow52 in
  let x3 = x / pow156 % pow52 in
  let x4 = x / pow208 in
  assert (felem_fits1 (u64 x0) 1);
  assert (felem_fits1 (u64 x1) 1);
  assert (felem_fits1 (u64 x2) 1);
  assert (felem_fits1 (u64 x3) 1);
  Math.Lemmas.lemma_div_lt_nat x 256 208;
  assert (felem_fits_last1 (u64 x4) 1)


val lemma_mod_pow2_sub: x:nat -> a:nat -> b:nat ->
  Lemma (x / pow2 a % pow2 b * pow2 a == x % pow2 (a + b) - x % pow2 a)

let lemma_mod_pow2_sub x a b =
  calc (==) {
    x / pow2 a % pow2 b * pow2 a;
    (==) { Math.Lemmas.pow2_modulo_division_lemma_1 x a (a + b) }
    x % pow2 (a + b) / pow2 a * pow2 a;
    (==) { Math.Lemmas.euclidean_division_definition (x % pow2 (a + b)) (pow2 a) }
    x % pow2 (a + b) - x % pow2 (a + b) % pow2 a;
    (==) { Math.Lemmas.pow2_modulo_modulo_lemma_1 x a (a + b) }
    x % pow2 (a + b) - x % pow2 a;
  }


val felem_to_list_lemma_eval: x:S.felem ->
  Lemma (as_nat5 (list_as_felem5 (felem_to_list x)) == x)
val felem_to_list_lemma_eval: x:S.felem ->
  Lemma (as_nat5 (list_as_felem5 (felem_to_list x)) == x)
x: Spec.K256.PointOps.felem
  -> FStar.Pervasives.Lemma
    (ensures
      Hacl.Spec.K256.Field52.Definitions.as_nat5 (Hacl.Spec.K256.PrecompTable.list_as_felem5 (Hacl.Spec.K256.PrecompTable.felem_to_list
                x)) ==
      x)