val one_mod : BE.lone_st U64 5ul 0ul mk_to_k256_prime_comm_monoid
let one_mod ctx one = make_u52_5 one (u64 1, u64 0, u64 0, u64 0, u64 0)
val one_mod : BE.lone_st U64 5ul 0ul mk_to_k256_prime_comm_monoid
let one_mod ctx one =
make_u52_5 one (u64 1, u64 0, u64 0, u64 0, u64 0)
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
Lib.Buffer.lbuffer Lib.IntTypes.uint_t Lib.IntTypes.U64 Lib.IntTypes.SEC FStar.UInt32.__uint_to_t Hacl.K256.Field.make_u52_5 FStar.Pervasives.Native.Mktuple5 Lib.IntTypes.uint64 Lib.IntTypes.u64 Prims.unit
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
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;
}


inline_for_extraction noextract
val one_mod : BE.lone_st U64 5ul 0ul mk_to_k256_prime_comm_monoid
Hacl.Impl.Exponentiation.Definitions.lone_st Lib.IntTypes.U64
  5ul
  0ul
  Hacl.Impl.K256.Finv.mk_to_k256_prime_comm_monoid