val cswap2_st:
    #t:limb_t
  -> len:size_t
  -> bit:limb t
  -> b1:lbignum t len
  -> b2:lbignum t len ->
  Stack unit
  (requires fun h -> live h b1 /\ live h b2 /\ disjoint b1 b2)
  (ensures  fun h0 _ h1 -> modifies (loc b1 |+| loc b2) h0 h1 /\
    (as_seq h1 b1, as_seq h1 b2) == S.cswap2 bit (as_seq h0 b1) (as_seq h0 b2))
let cswap2_st #t len bit b1 b2 =
  [@inline_let]
  let mask = uint #t 0 -. bit in
  [@inline_let]
  let spec h0 = S.cswap2_f mask in

  let h0 = ST.get () in
  loop2 h0 len b1 b2 spec
  (fun i ->
    Loops.unfold_repeati (v len) (spec h0) (as_seq h0 b1, as_seq h0 b2) (v i);
    let dummy = mask &. (b1.(i) ^. b2.(i)) in
    b1.(i) <- b1.(i) ^. dummy;
    b2.(i) <- b2.(i) ^. dummy
  )
val cswap2_st:
    #t:limb_t
  -> len:size_t
  -> bit:limb t
  -> b1:lbignum t len
  -> b2:lbignum t len ->
  Stack unit
  (requires fun h -> live h b1 /\ live h b2 /\ disjoint b1 b2)
  (ensures  fun h0 _ h1 -> modifies (loc b1 |+| loc b2) h0 h1 /\
    (as_seq h1 b1, as_seq h1 b2) == S.cswap2 bit (as_seq h0 b1) (as_seq h0 b2))
let cswap2_st #t len bit b1 b2 =
[@@ inline_let ]let mask = uint #t 0 -. bit in
[@@ inline_let ]let spec h0 = S.cswap2_f mask in
let h0 = ST.get () in
loop2 h0
  len
  b1
  b2
  spec
  (fun i ->
      Loops.unfold_repeati (v len) (spec h0) (as_seq h0 b1, as_seq h0 b2) (v i);
      let dummy = mask &. (b1.(i) ^. b2.(i)) in
      b1.(i) <- b1.(i) ^. dummy;
      b2.(i) <- b2.(i) ^. dummy)
Hacl.Bignum.Lib.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.Loops.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.Bignum.Lib.fst.checked Hacl.Bignum.Definitions.fst.checked Hacl.Bignum.Base.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.Lib.fst
Hacl.Bignum.Definitions.limb_t Lib.IntTypes.size_t Hacl.Bignum.Definitions.limb Hacl.Bignum.Definitions.lbignum Lib.Buffer.loop2 Prims.b2t Prims.op_LessThan Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.Buffer.op_Array_Assignment Prims.unit Lib.IntTypes.op_Hat_Dot Lib.IntTypes.SEC Lib.IntTypes.int_t Lib.Buffer.op_Array_Access Lib.Buffer.MUT Lib.IntTypes.op_Amp_Dot Lib.LoopCombinators.unfold_repeati FStar.Pervasives.Native.tuple2 Hacl.Spec.Bignum.Definitions.lbignum FStar.Pervasives.Native.Mktuple2 Lib.Buffer.as_seq FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Prims.nat Hacl.Spec.Bignum.Lib.cswap2_f Lib.IntTypes.op_Subtraction_Dot Lib.IntTypes.uint
module Hacl.Bignum.Lib

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

open Lib.IntTypes
open Lib.Buffer

open Hacl.Bignum.Base
open Hacl.Bignum.Definitions

module S = Hacl.Spec.Bignum.Lib
module ST = FStar.HyperStack.ST
module Loops = Lib.LoopCombinators
module LSeq = Lib.Sequence


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

///
///  Get and set i-th bit of a bignum
///

inline_for_extraction noextract
val bn_get_ith_bit:
    #t:limb_t
  -> len:size_t
  -> b:lbignum t len
  -> i:size_t{v i / bits t < v len} ->
  Stack (limb t)
  (requires fun h -> live h b)
  (ensures  fun h0 r h1 -> h0 == h1 /\
    r == S.bn_get_ith_bit (as_seq h0 b) (v i))

let bn_get_ith_bit #t len input ind =
  [@inline_let]
  let pbits = size (bits t) in
  let i = ind /. pbits in
  assert (v i == v ind / bits t);
  let j = ind %. pbits in
  assert (v j == v ind % bits t);
  let tmp = input.(i) in
  (tmp >>. j) &. uint #t 1


inline_for_extraction noextract
val bn_set_ith_bit:
    #t:limb_t
  -> len:size_t
  -> b:lbignum t len
  -> i:size_t{v i / bits t < v len} ->
  Stack unit
  (requires fun h -> live h b)
  (ensures  fun h0 _ h1 -> modifies (loc b) h0 h1 /\
    as_seq h1 b == S.bn_set_ith_bit (as_seq h0 b) (v i))

let bn_set_ith_bit #t len input ind =
  [@inline_let]
  let pbits = size (bits t) in
  let i = ind /. pbits in
  assert (v i == v ind / bits t);
  let j = ind %. pbits in
  assert (v j == v ind % bits t);
  input.(i) <- input.(i) |. (uint #t 1 <<. j)


inline_for_extraction noextract
val cswap2_st:
    #t:limb_t
  -> len:size_t
  -> bit:limb t
  -> b1:lbignum t len
  -> b2:lbignum t len ->
  Stack unit
  (requires fun h -> live h b1 /\ live h b2 /\ disjoint b1 b2)
  (ensures  fun h0 _ h1 -> modifies (loc b1 |+| loc b2) h0 h1 /\
    (as_seq h1 b1, as_seq h1 b2) == S.cswap2 bit (as_seq h0 b1) (as_seq h0 b2))
val cswap2_st:
    #t:limb_t
  -> len:size_t
  -> bit:limb t
  -> b1:lbignum t len
  -> b2:lbignum t len ->
  Stack unit
  (requires fun h -> live h b1 /\ live h b2 /\ disjoint b1 b2)
  (ensures  fun h0 _ h1 -> modifies (loc b1 |+| loc b2) h0 h1 /\
    (as_seq h1 b1, as_seq h1 b2) == S.cswap2 bit (as_seq h0 b1) (as_seq h0 b2))

    len: Lib.IntTypes.size_t ->
    bit: Hacl.Bignum.Definitions.limb t ->
    b1: Hacl.Bignum.Definitions.lbignum t len ->
    b2: Hacl.Bignum.Definitions.lbignum t len
  -> FStar.HyperStack.ST.Stack Prims.unit