val felem_to_list_lemma_eval: x:S.felem ->
  Lemma (BD.bn_v (list_as_felem4 (felem_to_list x)) == x)
let felem_to_list_lemma_eval x =
  let x0 = x % pow2 64 in
  let x1 = x / pow2 64 % pow2 64 in
  let x2 = x / pow2 128 % pow2 64 in
  let x3 = x / pow2 192 % pow2 64 in
  let bn_x = list_as_felem4 (felem_to_list x) in
  create4_lemma (u64 x0) (u64 x1) (u64 x2) (u64 x3);
  assert (v bn_x.[0] == x0 /\ v bn_x.[1] == x1 /\ v bn_x.[2] == x2 /\ v bn_x.[3] == x3);
  Hacl.Impl.P256.Bignum.bn_v_is_as_nat bn_x;
  assert (BD.bn_v bn_x = x0 + x1 * pow2 64 + x2 * pow2 128 + x3 * pow2 192);
  Hacl.Spec.PrecompBaseTable256.lemma_decompose_nat256_as_four_u64 x
val felem_to_list_lemma_eval: x:S.felem ->
  Lemma (BD.bn_v (list_as_felem4 (felem_to_list x)) == x)
let felem_to_list_lemma_eval x =
let x0 = x % pow2 64 in
let x1 = x / pow2 64 % pow2 64 in
let x2 = x / pow2 128 % pow2 64 in
let x3 = x / pow2 192 % pow2 64 in
let bn_x = list_as_felem4 (felem_to_list x) in
create4_lemma (u64 x0) (u64 x1) (u64 x2) (u64 x3);
assert (v bn_x.[ 0 ] == x0 /\ v bn_x.[ 1 ] == x1 /\ v bn_x.[ 2 ] == x2 /\ v bn_x.[ 3 ] == x3);
Hacl.Impl.P256.Bignum.bn_v_is_as_nat bn_x;
assert (BD.bn_v bn_x = x0 + x1 * pow2 64 + x2 * pow2 128 + x3 * pow2 192);
Hacl.Spec.PrecompBaseTable256.lemma_decompose_nat256_as_four_u64 x
Hacl.Spec.P256.PrecompTable.fst.checked
Spec.P256.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Hacl.Spec.PrecompBaseTable256.fsti.checked Hacl.Spec.PrecompBaseTable.fsti.checked Hacl.Spec.P256.Montgomery.fsti.checked Hacl.Spec.Bignum.Definitions.fst.checked Hacl.Impl.P256.Point.fsti.checked Hacl.Impl.P256.Bignum.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked
Hacl.Spec.P256.PrecompTable.fst
Spec.P256.PointOps.felem Hacl.Spec.PrecompBaseTable256.lemma_decompose_nat256_as_four_u64 Prims.unit Prims._assert Prims.b2t Prims.op_Equality Prims.int Hacl.Spec.Bignum.Definitions.bn_v Lib.IntTypes.U64 Prims.op_Addition FStar.Mul.op_Star Prims.pow2 Hacl.Impl.P256.Bignum.bn_v_is_as_nat Prims.l_and Prims.eq2 Lib.IntTypes.v Lib.IntTypes.SEC Lib.Sequence.op_String_Access Lib.IntTypes.uint64 Hacl.Spec.P256.PrecompTable.create4_lemma Lib.IntTypes.u64 Lib.Sequence.lseq Lib.IntTypes.int_t Hacl.Spec.P256.PrecompTable.list_as_felem4 Hacl.Spec.P256.PrecompTable.felem_to_list Prims.op_Modulus Prims.op_Division
module Hacl.Spec.P256.PrecompTable

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

open Hacl.Impl.P256.Point

module S = Spec.P256
module SM = Hacl.Spec.P256.Montgomery
module BD = Hacl.Spec.Bignum.Definitions
module FL = FStar.List.Tot
module SPT = Hacl.Spec.PrecompBaseTable

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

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


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

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

noextract
let list_as_felem4 (f:felem_list) : lseq uint64 4 =
  Seq.seq_of_list f <: lseq uint64 4


val felem_to_list_lemma_eval: x:S.felem ->
  Lemma (BD.bn_v (list_as_felem4 (felem_to_list x)) == x)
val felem_to_list_lemma_eval: x:S.felem ->
  Lemma (BD.bn_v (list_as_felem4 (felem_to_list x)) == x)
x: Spec.P256.PointOps.felem
  -> FStar.Pervasives.Lemma
    (ensures
      Hacl.Spec.Bignum.Definitions.bn_v (Hacl.Spec.P256.PrecompTable.list_as_felem4 (Hacl.Spec.P256.PrecompTable.felem_to_list
                x)) ==
      x)