val pow153:(pow153: pos{pow2 153 == pow153 /\ pow153 = pow51 * pow51 * pow51})
let pow153: (pow153:pos{pow2 153 == pow153 /\ pow153 = pow51 * pow51 * pow51}) =
  let pow153:pos = normalize_term (pow2 153) in
  normalize_term_spec (pow2 153);
  Math.Lemmas.pow2_plus 51 51;
  Math.Lemmas.pow2_plus 102 51;
  pow153
val pow153:(pow153: pos{pow2 153 == pow153 /\ pow153 = pow51 * pow51 * pow51})
let pow153:(pow153: pos{pow2 153 == pow153 /\ pow153 = pow51 * pow51 * pow51}) =
let pow153:pos = normalize_term (pow2 153) in
normalize_term_spec (pow2 153);
Math.Lemmas.pow2_plus 51 51;
Math.Lemmas.pow2_plus 102 51;
pow153
Hacl.Spec.Ed25519.PrecompTable.fsti.checked
Spec.Ed25519.fst.checked Spec.Curve25519.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Hacl.Spec.Curve25519.Field51.Definition.fst.checked Hacl.Impl.Ed25519.Field51.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.List.Tot.fst.checked
Hacl.Spec.Ed25519.PrecompTable.fsti
Prims.unit FStar.Math.Lemmas.pow2_plus FStar.Pervasives.normalize_term_spec Prims.pos Prims.pow2 FStar.Pervasives.normalize_term
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

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

unfold
let create5 (x0 x1 x2 x3 x4:uint64) : list uint64 = [x0; x1; x2; x3; x4]

inline_for_extraction noextract
let felem_list = x:list uint64{FL.length x == 5}
inline_for_extraction noextract
let point_list = x:list uint64{FL.length x == 20}

inline_for_extraction noextract
let pow51 = SF51.pow51

[@"opaque_to_smt"]
let pow102: (pow102:pos{pow2 102 == pow102 /\ pow102 = pow51 * pow51}) =
  let pow102:pos = normalize_term (pow2 102) in
  normalize_term_spec (pow2 102);
  Math.Lemmas.pow2_plus 51 51;
  pow102
val pow153:(pow153: pos{pow2 153 == pow153 /\ pow153 = pow51 * pow51 * pow51})
pow153:
Prims.pos
  { Prims.pow2 153 == pow153 /\
    pow153 =
    (Hacl.Spec.Ed25519.PrecompTable.pow51 * Hacl.Spec.Ed25519.PrecompTable.pow51) *
    Hacl.Spec.Ed25519.PrecompTable.pow51 }