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_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)
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 Prims._assert Prims.l_and Prims.eq2 Prims.int Lib.IntTypes.v Lib.IntTypes.U64 Lib.IntTypes.SEC Prims.unit Hacl.Spec.K256.PrecompTable.create5_lemma Lib.IntTypes.u64 Hacl.Spec.K256.Field52.Definitions.felem5 Hacl.Spec.K256.PrecompTable.list_as_felem5 Hacl.Spec.K256.PrecompTable.felem_list Hacl.Spec.K256.PrecompTable.felem_to_list Prims.op_Division Hacl.Spec.K256.Field52.Definitions.pow208 Prims.op_Modulus Hacl.Spec.K256.Field52.Definitions.pow156 Hacl.Spec.K256.Field52.Definitions.pow52 Hacl.Spec.K256.Field52.Definitions.pow104
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)
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)
x: Spec.K256.PointOps.felem
  -> FStar.Pervasives.Lemma
    (ensures
      (let _ =
          Hacl.Spec.K256.PrecompTable.list_as_felem5 (Hacl.Spec.K256.PrecompTable.felem_to_list x)
        in
        (let FStar.Pervasives.Native.Mktuple5 #_ #_ #_ #_ #_ f0 f1 f2 f3 f4 = _ in
          let x0 = x % Hacl.Spec.K256.Field52.Definitions.pow52 in
          let x1 =
            x / Hacl.Spec.K256.Field52.Definitions.pow52 % Hacl.Spec.K256.Field52.Definitions.pow52
          in
          let x2 =
            x / Hacl.Spec.K256.Field52.Definitions.pow104 % Hacl.Spec.K256.Field52.Definitions.pow52
          in
          let x3 =
            x / Hacl.Spec.K256.Field52.Definitions.pow156 % Hacl.Spec.K256.Field52.Definitions.pow52
          in
          let x4 = x / Hacl.Spec.K256.Field52.Definitions.pow208 in
          Lib.IntTypes.v f0 == x0 /\ Lib.IntTypes.v f1 == x1 /\ Lib.IntTypes.v f2 == x2 /\
          Lib.IntTypes.v f3 == x3 /\ Lib.IntTypes.v f4 == x4)
        <:
        Type0))