val mod_inv_limb_:
    #t:limb_t
  -> alpha:limb t
  -> beta:limb t
  -> ub:lbignum t 1ul
  -> vb:lbignum t 1ul ->
  Stack unit
  (requires fun h -> live h ub /\ live h vb /\ disjoint ub vb)
  (ensures  fun h0 _ h1 -> modifies (loc ub |+| loc vb) h0 h1 /\
    (let (us, vs) =
      Loops.repeat_gen (bits t)
	(S.mod_inv_limb_t t)
	(S.mod_inv_limb_f alpha beta)
	(LSeq.index (as_seq h0 ub) 0, LSeq.index (as_seq h0 vb) 0) in
    LSeq.index (as_seq h1 ub) 0 == us /\ LSeq.index (as_seq h1 vb) 0 == vs))
let mod_inv_limb_ #t alpha beta ub vb =
  [@inline_let]
  let refl h i : GTot (S.mod_inv_limb_t t i) = LSeq.index (as_seq h ub) 0, LSeq.index (as_seq h vb) 0 in
  [@inline_let]
  let footprint i = loc ub |+| loc vb in
  [@inline_let]
  let spec h0 = S.mod_inv_limb_f alpha beta in
  let h0 = ST.get () in
  loop h0 (size (bits t)) (S.mod_inv_limb_t t) refl footprint spec
  (fun i ->
    Loops.unfold_repeat_gen (bits t) (S.mod_inv_limb_t t) (spec h0) (refl h0 0) (v i);
    let us = ub.(0ul) in
    let vs = vb.(0ul) in
    let u_is_odd = uint #t 0 -. (us &. uint #t 1) in
    let beta_if_u_is_odd = beta &. u_is_odd in
    ub.(0ul) <- ((us ^. beta_if_u_is_odd) >>. 1ul) +. (us &. beta_if_u_is_odd);

    let alpha_if_u_is_odd = alpha &. u_is_odd in
    vb.(0ul) <- (vs >>. 1ul) +. alpha_if_u_is_odd
  )
val mod_inv_limb_:
    #t:limb_t
  -> alpha:limb t
  -> beta:limb t
  -> ub:lbignum t 1ul
  -> vb:lbignum t 1ul ->
  Stack unit
  (requires fun h -> live h ub /\ live h vb /\ disjoint ub vb)
  (ensures  fun h0 _ h1 -> modifies (loc ub |+| loc vb) h0 h1 /\
    (let (us, vs) =
      Loops.repeat_gen (bits t)
	(S.mod_inv_limb_t t)
	(S.mod_inv_limb_f alpha beta)
	(LSeq.index (as_seq h0 ub) 0, LSeq.index (as_seq h0 vb) 0) in
    LSeq.index (as_seq h1 ub) 0 == us /\ LSeq.index (as_seq h1 vb) 0 == vs))
let mod_inv_limb_ #t alpha beta ub vb =
[@@ inline_let ]let refl h i : GTot (S.mod_inv_limb_t t i) =
  LSeq.index (as_seq h ub) 0, LSeq.index (as_seq h vb) 0
in
[@@ inline_let ]let footprint i = loc ub |+| loc vb in
[@@ inline_let ]let spec h0 = S.mod_inv_limb_f alpha beta in
let h0 = ST.get () in
loop h0
  (size (bits t))
  (S.mod_inv_limb_t t)
  refl
  footprint
  spec
  (fun i ->
      Loops.unfold_repeat_gen (bits t) (S.mod_inv_limb_t t) (spec h0) (refl h0 0) (v i);
      let us = ub.(0ul) in
      let vs = vb.(0ul) in
      let u_is_odd = uint #t 0 -. (us &. uint #t 1) in
      let beta_if_u_is_odd = beta &. u_is_odd in
      ub.(0ul) <- ((us ^. beta_if_u_is_odd) >>. 1ul) +. (us &. beta_if_u_is_odd);
      let alpha_if_u_is_odd = alpha &. u_is_odd in
      vb.(0ul) <- (vs >>. 1ul) +. alpha_if_u_is_odd)
Hacl.Bignum.ModInvLimb.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.Bignum.ModInvLimb.fst.checked Hacl.Spec.Bignum.ModInvLimb.fst.checked Hacl.Bignum.Definitions.fst.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.Bignum.ModInvLimb.fst
Hacl.Bignum.Definitions.limb_t Hacl.Bignum.Definitions.limb Hacl.Bignum.Definitions.lbignum FStar.UInt32.__uint_to_t Lib.Buffer.loop Lib.IntTypes.size Lib.IntTypes.bits Hacl.Spec.Bignum.ModInvLimb.mod_inv_limb_t Lib.IntTypes.size_t Prims.b2t Prims.op_LessThan Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.Buffer.op_Array_Assignment Lib.IntTypes.op_Plus_Dot Lib.IntTypes.SEC Lib.IntTypes.op_Greater_Greater_Dot Prims.unit Lib.IntTypes.int_t Lib.IntTypes.op_Amp_Dot Lib.IntTypes.op_Hat_Dot Lib.IntTypes.op_Subtraction_Dot Lib.IntTypes.uint Lib.Buffer.op_Array_Access Lib.Buffer.MUT Lib.LoopCombinators.unfold_repeat_gen FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Prims.nat FStar.Pervasives.Native.tuple2 Hacl.Spec.Bignum.Definitions.limb Hacl.Spec.Bignum.ModInvLimb.mod_inv_limb_f Prims.op_LessThanOrEqual Prims.op_Subtraction Prims.pow2 Lib.IntTypes.mk_int LowStar.Monotonic.Buffer.loc Lib.IntTypes.size_nat Lib.Buffer.op_Bar_Plus_Bar Lib.Buffer.loc FStar.Pervasives.Native.Mktuple2 Lib.Sequence.index Lib.Buffer.as_seq
module Hacl.Bignum.ModInvLimb

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

open Lib.IntTypes
open Lib.Buffer

open Hacl.Bignum.Definitions

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

module S = Hacl.Spec.Bignum.ModInvLimb

friend Hacl.Spec.Bignum.ModInvLimb

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


inline_for_extraction noextract
val mod_inv_limb_:
    #t:limb_t
  -> alpha:limb t
  -> beta:limb t
  -> ub:lbignum t 1ul
  -> vb:lbignum t 1ul ->
  Stack unit
  (requires fun h -> live h ub /\ live h vb /\ disjoint ub vb)
  (ensures  fun h0 _ h1 -> modifies (loc ub |+| loc vb) h0 h1 /\
    (let (us, vs) =
      Loops.repeat_gen (bits t)
	(S.mod_inv_limb_t t)
	(S.mod_inv_limb_f alpha beta)
	(LSeq.index (as_seq h0 ub) 0, LSeq.index (as_seq h0 vb) 0) in
    LSeq.index (as_seq h1 ub) 0 == us /\ LSeq.index (as_seq h1 vb) 0 == vs))
val mod_inv_limb_:
    #t:limb_t
  -> alpha:limb t
  -> beta:limb t
  -> ub:lbignum t 1ul
  -> vb:lbignum t 1ul ->
  Stack unit
  (requires fun h -> live h ub /\ live h vb /\ disjoint ub vb)
  (ensures  fun h0 _ h1 -> modifies (loc ub |+| loc vb) h0 h1 /\
    (let (us, vs) =
      Loops.repeat_gen (bits t)
	(S.mod_inv_limb_t t)
	(S.mod_inv_limb_f alpha beta)
	(LSeq.index (as_seq h0 ub) 0, LSeq.index (as_seq h0 vb) 0) in
    LSeq.index (as_seq h1 ub) 0 == us /\ LSeq.index (as_seq h1 vb) 0 == vs))

    alpha: Hacl.Bignum.Definitions.limb t ->
    beta: Hacl.Bignum.Definitions.limb t ->
    ub: Hacl.Bignum.Definitions.lbignum t 1ul ->
    vb: Hacl.Bignum.Definitions.lbignum t 1ul
  -> FStar.HyperStack.ST.Stack Prims.unit