val table_inv_w5:BE.table_inv_t U64 15ul 32ul
let table_inv_w5 : BE.table_inv_t U64 15ul 32ul =
  [@inline_let] let len = 15ul in
  [@inline_let] let ctx_len = 0ul in
  [@inline_let] let k = mk_k256_concrete_ops in
  [@inline_let] let l = 5ul in
  [@inline_let] let table_len = 32ul in
  BE.table_inv_precomp len ctx_len k l table_len
val table_inv_w5:BE.table_inv_t U64 15ul 32ul
let table_inv_w5:BE.table_inv_t U64 15ul 32ul =
[@@ inline_let ]let len = 15ul in
[@@ inline_let ]let ctx_len = 0ul in
[@@ inline_let ]let k = mk_k256_concrete_ops in
[@@ inline_let ]let l = 5ul in
[@@ inline_let ]let table_len = 32ul in
BE.table_inv_precomp len ctx_len k l table_len
Hacl.Impl.K256.GLV.fst.checked
Spec.K256.Lemmas.fsti.checked Spec.K256.fst.checked Spec.Exponentiation.fsti.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.Exponentiation.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.K256.GLV.Lemmas.fst.checked Hacl.Spec.K256.GLV.fst.checked Hacl.Spec.K256.ECSM.Lemmas.fst.checked Hacl.K256.Scalar.fsti.checked Hacl.K256.PrecompTable.fsti.checked Hacl.K256.Field.fsti.checked Hacl.Impl.PrecompTable.fsti.checked Hacl.Impl.MultiExponentiation.fsti.checked Hacl.Impl.K256.PointMul.fsti.checked Hacl.Impl.K256.Point.fsti.checked Hacl.Impl.K256.Group.fst.checked Hacl.Impl.K256.GLV.Constants.fsti.checked Hacl.Impl.Exponentiation.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
Hacl.Impl.K256.GLV.fst
Hacl.Impl.Exponentiation.table_inv_precomp Lib.IntTypes.U64 FStar.UInt32.t FStar.UInt32.__uint_to_t Hacl.Impl.Exponentiation.Definitions.concrete_ops FStar.UInt32.uint_to_t Hacl.Impl.K256.Group.mk_k256_concrete_ops
module Hacl.Impl.K256.GLV

open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer

module ST = FStar.HyperStack.ST
module LSeq = Lib.Sequence

module LE = Lib.Exponentiation
module SE = Spec.Exponentiation
module BE = Hacl.Impl.Exponentiation
module ME = Hacl.Impl.MultiExponentiation
module PT = Hacl.Impl.PrecompTable

module S = Spec.K256
module SL = Spec.K256.Lemmas
module SG = Hacl.Spec.K256.GLV
module SGL = Hacl.Spec.K256.GLV.Lemmas
module PML = Hacl.Spec.K256.ECSM.Lemmas
module PM = Hacl.Impl.K256.PointMul

open Hacl.K256.Field
open Hacl.K256.Scalar
open Hacl.Impl.K256.Point

open Hacl.Impl.K256.GLV.Constants
include Hacl.Impl.K256.Group
include Hacl.K256.PrecompTable

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

let _: squash(pow2 5 = 32) =
  assert_norm (pow2 5 = 32)

let _: squash(pow2 128 < S.q) =
  assert_norm (pow2 128 < S.q)


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