val list_as_felem5 (f: felem_list) : SF51.felem5
let list_as_felem5 (f:felem_list) : SF51.felem5 =
  let x = Seq.seq_of_list f <: lseq uint64 5 in
  F51.lseq_as_felem x
val list_as_felem5 (f: felem_list) : SF51.felem5
let list_as_felem5 (f: felem_list) : SF51.felem5 =
let x = Seq.seq_of_list f <: lseq uint64 5 in
F51.lseq_as_felem x
Hacl.Spec.Ed25519.PrecompTable.fst.checked
Spec.Ed25519.fst.checked Spec.Curve25519.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Hacl.Spec.PrecompBaseTable.fsti.checked Hacl.Spec.Curve25519.Field51.Definition.fst.checked Hacl.Impl.Ed25519.Field51.fst.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.Ed25519.PrecompTable.fst
Hacl.Spec.Ed25519.PrecompTable.felem_list Hacl.Impl.Ed25519.Field51.lseq_as_felem Lib.Sequence.lseq Lib.IntTypes.int_t Lib.IntTypes.U64 Lib.IntTypes.SEC FStar.Seq.Properties.seq_of_list Lib.IntTypes.uint64 Hacl.Spec.Curve25519.Field51.Definition.felem5
module Hacl.Spec.Ed25519.PrecompTable

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

module F51 = Hacl.Impl.Ed25519.Field51
module SF51 = Hacl.Spec.Curve25519.Field51.Definition

module S = Spec.Ed25519
module SC = Spec.Curve25519
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]

//-----------------------------------
val list_as_felem5 (f: felem_list) : SF51.felem5
f: Hacl.Spec.Ed25519.PrecompTable.felem_list -> Hacl.Spec.Curve25519.Field51.Definition.felem5