val mk_to_k256_prime_comm_monoid:BE.to_comm_monoid U64 5ul 0ul
let mk_to_k256_prime_comm_monoid : BE.to_comm_monoid U64 5ul 0ul = {
  BE.a_spec = S.felem;
  BE.comm_monoid = SI.nat_mod_comm_monoid;
  BE.linv_ctx = linv_ctx;
  BE.linv = linv;
  BE.refl = refl;
}
val mk_to_k256_prime_comm_monoid:BE.to_comm_monoid U64 5ul 0ul
let mk_to_k256_prime_comm_monoid:BE.to_comm_monoid U64 5ul 0ul =
{
  BE.a_spec = S.felem;
  BE.comm_monoid = SI.nat_mod_comm_monoid;
  BE.linv_ctx = linv_ctx;
  BE.linv = linv;
  BE.refl = refl
}
Hacl.Impl.K256.Finv.fst.checked
Spec.K256.fst.checked Spec.Exponentiation.fsti.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.K256.Finv.fst.checked Hacl.K256.Field.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
Hacl.Impl.K256.Finv.fst
Hacl.Impl.Exponentiation.Definitions.Mkto_comm_monoid Lib.IntTypes.U64 FStar.UInt32.uint_to_t Spec.K256.PointOps.felem Hacl.Spec.K256.Finv.nat_mod_comm_monoid Hacl.Impl.K256.Finv.linv_ctx Hacl.Impl.K256.Finv.linv Hacl.Impl.K256.Finv.refl
module Hacl.Impl.K256.Finv

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

open Lib.IntTypes
open Lib.Buffer

open Hacl.K256.Field

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

module S = Spec.K256
module SI = Hacl.Spec.K256.Finv

module SE = Spec.Exponentiation
module BE = Hacl.Impl.Exponentiation

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

unfold
let linv_ctx (a:LSeq.lseq uint64 0) : Type0 = True

unfold
let linv (a:LSeq.lseq uint64 5) : Type0 =
  let open Lib.Sequence in
  inv_lazy_reduced2_5 (a.[0],a.[1],a.[2],a.[3],a.[4])

unfold
let refl (a:LSeq.lseq uint64 5{linv a}) : GTot S.felem =
  let open Lib.Sequence in
  feval5 (a.[0],a.[1],a.[2],a.[3],a.[4])


inline_for_extraction noextract
val mk_to_k256_prime_comm_monoid:BE.to_comm_monoid U64 5ul 0ul
Hacl.Impl.Exponentiation.Definitions.to_comm_monoid Lib.IntTypes.U64
  (FStar.UInt32.uint_to_t 5 <: FStar.UInt32.t)
  (FStar.UInt32.uint_to_t 0 <: FStar.UInt32.t)