val fsquare_times (out a:felem) (b:size_t) : Stack unit
  (requires fun h ->
    live h out /\ live h a /\ disjoint out a /\
    inv_lazy_reduced2 h a)
  (ensures  fun h0 _ h1 -> modifies (loc out) h0 h1 /\ inv_lazy_reduced2 h1 out /\
    feval h1 out == SI.fsquare_times (feval h0 a) (v b))
let fsquare_times out a b =
  let h0 = ST.get () in
  SE.exp_pow2_lemma SI.mk_nat_mod_concrete_ops (feval h0 a) (v b);
  BE.lexp_pow2 5ul 0ul mk_k256_prime_concrete_ops (null uint64) a b out
val fsquare_times (out a:felem) (b:size_t) : Stack unit
  (requires fun h ->
    live h out /\ live h a /\ disjoint out a /\
    inv_lazy_reduced2 h a)
  (ensures  fun h0 _ h1 -> modifies (loc out) h0 h1 /\ inv_lazy_reduced2 h1 out /\
    feval h1 out == SI.fsquare_times (feval h0 a) (v b))
let fsquare_times out a b =
let h0 = ST.get () in
SE.exp_pow2_lemma SI.mk_nat_mod_concrete_ops (feval h0 a) (v b);
BE.lexp_pow2 5ul 0ul mk_k256_prime_concrete_ops (null uint64) a b out
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.K256.Field.felem Lib.IntTypes.size_t Hacl.Impl.Exponentiation.lexp_pow2 Lib.IntTypes.U64 FStar.UInt32.__uint_to_t Hacl.Impl.K256.Finv.mk_k256_prime_concrete_ops Lib.Buffer.null Lib.Buffer.MUT Lib.IntTypes.uint64 Prims.unit Spec.Exponentiation.exp_pow2_lemma Spec.K256.PointOps.felem Hacl.Spec.K256.Finv.mk_nat_mod_concrete_ops Hacl.K256.Field.feval Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get
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
let one_mod ctx one = make_u52_5 one (u64 1, u64 0, u64 0, u64 0, u64 0)


inline_for_extraction noextract
val mul_mod : BE.lmul_st U64 5ul 0ul mk_to_k256_prime_comm_monoid
let mul_mod ctx x y xy = fmul xy x y


inline_for_extraction noextract
val sqr_mod : BE.lsqr_st U64 5ul 0ul mk_to_k256_prime_comm_monoid
let sqr_mod ctx x xx = fsqr xx x


inline_for_extraction noextract
let mk_k256_prime_concrete_ops : BE.concrete_ops U64 5ul 0ul = {
  BE.to = mk_to_k256_prime_comm_monoid;
  BE.lone = one_mod;
  BE.lmul = mul_mod;
  BE.lsqr = sqr_mod;
}


val fsquare_times_in_place (out:felem) (b:size_t) : Stack unit
  (requires fun h ->
    live h out /\ inv_lazy_reduced2 h out)
  (ensures  fun h0 _ h1 -> modifies (loc out) h0 h1 /\ inv_lazy_reduced2 h1 out /\
    feval h1 out == SI.fsquare_times (feval h0 out) (v b))

[@CInline]
let fsquare_times_in_place out b =
  let h0 = ST.get () in
  SE.exp_pow2_lemma SI.mk_nat_mod_concrete_ops (feval h0 out) (v b);
  BE.lexp_pow2_in_place 5ul 0ul mk_k256_prime_concrete_ops (null uint64) out b


val fsquare_times (out a:felem) (b:size_t) : Stack unit
  (requires fun h ->
    live h out /\ live h a /\ disjoint out a /\
    inv_lazy_reduced2 h a)
  (ensures  fun h0 _ h1 -> modifies (loc out) h0 h1 /\ inv_lazy_reduced2 h1 out /\
    feval h1 out == SI.fsquare_times (feval h0 a) (v b))
val fsquare_times (out a:felem) (b:size_t) : Stack unit
  (requires fun h ->
    live h out /\ live h a /\ disjoint out a /\
    inv_lazy_reduced2 h a)
  (ensures  fun h0 _ h1 -> modifies (loc out) h0 h1 /\ inv_lazy_reduced2 h1 out /\
    feval h1 out == SI.fsquare_times (feval h0 a) (v b))
out: Hacl.K256.Field.felem -> a: Hacl.K256.Field.felem -> b: Lib.IntTypes.size_t
  -> FStar.HyperStack.ST.Stack Prims.unit