let rsapss_sign_bn_st (t:limb_t) (ke:BE.exp t) (modBits:modBits_t t) =
  let len = blocks modBits (size (bits t)) in
    eBits:size_t
  -> dBits:size_t{LS.skey_len_pre t (v modBits) (v eBits) (v dBits)}
  -> skey:lbignum t (2ul *! len +! blocks eBits (size (bits t)) +! blocks dBits (size (bits t)))
  -> m:lbignum t len
  -> m':lbignum t len
  -> s:lbignum t len ->
  Stack bool
  (requires fun h -> len == ke.BE.bn.BN.len /\
    live h skey /\ live h m /\ live h s /\ live h m' /\
    disjoint s m /\ disjoint s skey /\ disjoint m skey /\
    disjoint m m' /\ disjoint m' s /\ disjoint m' skey /\
    LS.rsapss_skey_pre (v modBits) (v eBits) (v dBits) (as_seq h skey) /\
    bn_v h m < bn_v h (gsub skey 0ul len))
  (ensures  fun h0 r h1 -> modifies (loc s |+| loc m') h0 h1 /\
    (r, as_seq h1 s) == LS.rsapss_sign_bn (v modBits) (v eBits) (v dBits) (as_seq h0 skey) (as_seq h0 m))
let rsapss_sign_bn_st (t: limb_t) (ke: BE.exp t) (modBits: modBits_t t) =
let len = blocks modBits (size (bits t)) in

    eBits: size_t ->
    dBits: size_t{LS.skey_len_pre t (v modBits) (v eBits) (v dBits)} ->
    skey: lbignum t (2ul *! len +! blocks eBits (size (bits t)) +! blocks dBits (size (bits t))) ->
    m: lbignum t len ->
    m': lbignum t len ->
    s: lbignum t len
  -> Stack bool
      (requires
        fun h ->
          len == ke.BE.bn.BN.len /\ live h skey /\ live h m /\ live h s /\ live h m' /\ disjoint s m /\
          disjoint s skey /\ disjoint m skey /\ disjoint m m' /\ disjoint m' s /\ disjoint m' skey /\
          LS.rsapss_skey_pre (v modBits) (v eBits) (v dBits) (as_seq h skey) /\
          bn_v h m < bn_v h (gsub skey 0ul len))
      (ensures
        fun h0 r h1 ->
          modifies (loc s |+| loc m') h0 h1 /\
          (r, as_seq h1 s) ==
          LS.rsapss_sign_bn (v modBits) (v eBits) (v dBits) (as_seq h0 skey) (as_seq h0 m))
Hacl.Impl.RSAPSS.fst.checked
Spec.RSAPSS.fst.checked Spec.Agile.Hash.fsti.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.RSAPSS.fst.checked Hacl.Spec.Bignum.Montgomery.fsti.checked Hacl.Spec.Bignum.Exponentiation.fsti.checked Hacl.Spec.Bignum.Definitions.fst.checked Hacl.Spec.Bignum.Base.fst.checked Hacl.Spec.Bignum.fsti.checked Hacl.Impl.RSAPSS.Padding.fst.checked Hacl.Impl.RSAPSS.MGF.fst.checked Hacl.Impl.RSAPSS.Keys.fst.checked Hacl.Bignum.Montgomery.fsti.checked Hacl.Bignum.Exponentiation.fsti.checked Hacl.Bignum.Definitions.fst.checked Hacl.Bignum.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.Impl.RSAPSS.fst
Hacl.Bignum.Definitions.limb_t Hacl.Bignum.Exponentiation.exp Hacl.Impl.RSAPSS.modBits_t Lib.IntTypes.size_t Hacl.Spec.RSAPSS.skey_len_pre Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Hacl.Bignum.Definitions.lbignum Lib.IntTypes.op_Plus_Bang Lib.IntTypes.op_Star_Bang FStar.UInt32.__uint_to_t Hacl.Bignum.Definitions.blocks Lib.IntTypes.size Lib.IntTypes.bits Prims.bool FStar.Monotonic.HyperStack.mem Prims.l_and Prims.eq2 Prims.l_or Prims.int Lib.IntTypes.range Prims.b2t Prims.op_GreaterThan Prims.op_LessThanOrEqual Lib.IntTypes.max_size_t FStar.Mul.op_Star Hacl.Spec.Bignum.Definitions.blocks Prims.op_LessThan Hacl.Bignum.__proj__Mkbn__item__len Hacl.Bignum.Exponentiation.__proj__Mkexp__item__bn Lib.Buffer.live Lib.Buffer.MUT Hacl.Bignum.Definitions.limb Lib.Buffer.disjoint Hacl.Spec.RSAPSS.rsapss_skey_pre Lib.Buffer.as_seq Hacl.Bignum.Definitions.bn_v Lib.Buffer.gsub Lib.Buffer.modifies Lib.Buffer.op_Bar_Plus_Bar Lib.Buffer.loc FStar.Pervasives.Native.tuple2 Hacl.Spec.Bignum.Definitions.lbignum FStar.Pervasives.Native.Mktuple2 Hacl.Spec.RSAPSS.rsapss_sign_bn Lib.IntTypes.int_t Prims.op_Subtraction Prims.pow2 Prims.op_Multiply Lib.IntTypes.mk_int
module Hacl.Impl.RSAPSS

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 Hash = Spec.Agile.Hash
module SB = Hacl.Spec.Bignum
module BB = Hacl.Spec.Bignum.Base
module SD = Hacl.Spec.Bignum.Definitions
module SM = Hacl.Spec.Bignum.Montgomery
module SE = Hacl.Spec.Bignum.Exponentiation

module BN = Hacl.Bignum
module BE = Hacl.Bignum.Exponentiation
module BM = Hacl.Bignum.Montgomery

module S = Spec.RSAPSS
module LS = Hacl.Spec.RSAPSS
module LSeq = Lib.Sequence

module RP = Hacl.Impl.RSAPSS.Padding
module RM = Hacl.Impl.RSAPSS.MGF
module RK = Hacl.Impl.RSAPSS.Keys

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

inline_for_extraction noextract
let modBits_t (t:limb_t) = modBits:size_t{1 < v modBits /\ 2 * bits t * SD.blocks (v modBits) (bits t) <= max_size_t}
val rsapss_sign_bn_st : t: Hacl.Bignum.Definitions.limb_t ->
    ke: Hacl.Bignum.Exponentiation.exp t ->
    modBits: Hacl.Impl.RSAPSS.modBits_t t
  -> Type0

    t: Hacl.Bignum.Definitions.limb_t ->
    ke: Hacl.Bignum.Exponentiation.exp t ->
    modBits: Hacl.Impl.RSAPSS.modBits_t t
  -> Type0