val table_inv_w5:BE.table_inv_t U64 20ul 32ul
let table_inv_w5 : BE.table_inv_t U64 20ul 32ul =
  [@inline_let] let len = 20ul in
  [@inline_let] let ctx_len = 0ul in
  [@inline_let] let k = mk_ed25519_concrete_ops in
  [@inline_let] let l = 5ul in
  [@inline_let] let table_len = 32ul in
  assert_norm (pow2 (v l) = v table_len);
  BE.table_inv_precomp len ctx_len k l table_len
val table_inv_w5:BE.table_inv_t U64 20ul 32ul
let table_inv_w5:BE.table_inv_t U64 20ul 32ul =
[@@ inline_let ]let len = 20ul in
[@@ inline_let ]let ctx_len = 0ul in
[@@ inline_let ]let k = mk_ed25519_concrete_ops in
[@@ inline_let ]let l = 5ul in
[@@ inline_let ]let table_len = 32ul in
assert_norm (pow2 (v l) = v table_len);
BE.table_inv_precomp len ctx_len k l table_len
Hacl.Impl.Ed25519.Ladder.fst.checked
Spec.Exponentiation.fsti.checked Spec.Ed25519.Lemmas.fsti.checked Spec.Ed25519.fst.checked prims.fst.checked LowStar.Ignore.fsti.checked Lib.IntTypes.fsti.checked Lib.Exponentiation.fsti.checked Lib.ByteSequence.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.PrecompBaseTable256.fsti.checked Hacl.Spec.Bignum.Definitions.fst.checked Hacl.Spec.Bignum.Convert.fst.checked Hacl.Impl.PrecompTable.fsti.checked Hacl.Impl.MultiExponentiation.fsti.checked Hacl.Impl.Exponentiation.fsti.checked Hacl.Impl.Ed25519.PointNegate.fst.checked Hacl.Impl.Ed25519.PointConstants.fst.checked Hacl.Impl.Ed25519.Group.fst.checked Hacl.Impl.Ed25519.Field51.fst.checked Hacl.Ed25519.PrecompTable.fsti.checked Hacl.Bignum25519.fsti.checked Hacl.Bignum.Definitions.fst.checked Hacl.Bignum.Convert.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked
Hacl.Impl.Ed25519.Ladder.fst
Hacl.Impl.Exponentiation.table_inv_precomp Lib.IntTypes.U64 Prims.unit FStar.Pervasives.assert_norm Prims.b2t Prims.op_Equality Prims.int Prims.l_or Prims.op_GreaterThan Lib.IntTypes.range Lib.IntTypes.U32 Prims.pow2 Lib.IntTypes.v Lib.IntTypes.PUB FStar.UInt32.t FStar.UInt32.__uint_to_t Hacl.Impl.Exponentiation.Definitions.concrete_ops FStar.UInt32.uint_to_t Hacl.Impl.Ed25519.Group.mk_ed25519_concrete_ops
module Hacl.Impl.Ed25519.Ladder

module ST = FStar.HyperStack.ST
open FStar.HyperStack.All
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer

open Hacl.Bignum25519
module F51 = Hacl.Impl.Ed25519.Field51

module BSeq = Lib.ByteSequence

module LE = Lib.Exponentiation
module SE = Spec.Exponentiation
module BE = Hacl.Impl.Exponentiation
module ME = Hacl.Impl.MultiExponentiation
module PT = Hacl.Impl.PrecompTable
module SPT256 = Hacl.Spec.PrecompBaseTable256
module BD = Hacl.Bignum.Definitions
module SD = Hacl.Spec.Bignum.Definitions

module S = Spec.Ed25519

open Hacl.Impl.Ed25519.PointConstants
include Hacl.Impl.Ed25519.Group
include Hacl.Ed25519.PrecompTable

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

inline_for_extraction noextract
let table_inv_w4 : BE.table_inv_t U64 20ul 16ul =
  [@inline_let] let len = 20ul in
  [@inline_let] let ctx_len = 0ul in
  [@inline_let] let k = mk_ed25519_concrete_ops in
  [@inline_let] let l = 4ul in
  [@inline_let] let table_len = 16ul in
  BE.table_inv_precomp len ctx_len k l table_len


inline_for_extraction noextract
val table_inv_w5:BE.table_inv_t U64 20ul 32ul
Hacl.Impl.Exponentiation.table_inv_t Lib.IntTypes.U64
  (FStar.UInt32.uint_to_t 20 <: FStar.UInt32.t)
  (FStar.UInt32.uint_to_t 32 <: FStar.UInt32.t)