let rsapss_sign_msg_to_bn_st (t:limb_t) (a:Hash.hash_alg{S.hash_is_supported a}) (modBits:modBits_t t) =
  let len = blocks modBits (size (bits t)) in
    saltLen:size_t
  -> salt:lbuffer uint8 saltLen
  -> msgLen:size_t
  -> msg:lbuffer uint8 msgLen
  -> m:lbignum t len ->
  Stack unit
  (requires fun h ->
    live h salt /\ live h msg /\ live h m /\
    disjoint salt msg /\ disjoint m msg /\ disjoint m salt /\
    as_seq h m == LSeq.create (v len) (uint #t 0) /\
    LS.rsapss_sign_pre a (v modBits) (v saltLen) (as_seq h salt) (v msgLen) (as_seq h msg))
  (ensures  fun h0 _ h1 -> modifies (loc m) h0 h1 /\
    as_seq h1 m == LS.rsapss_sign_msg_to_bn a (v modBits) (v saltLen) (as_seq h0 salt) (v msgLen) (as_seq h0 msg))
let rsapss_sign_msg_to_bn_st
      (t: limb_t)
      (a: Hash.hash_alg{S.hash_is_supported a})
      (modBits: modBits_t t)
     =
let len = blocks modBits (size (bits t)) in

    saltLen: size_t ->
    salt: lbuffer uint8 saltLen ->
    msgLen: size_t ->
    msg: lbuffer uint8 msgLen ->
    m: lbignum t len
  -> Stack unit
      (requires
        fun h ->
          live h salt /\ live h msg /\ live h m /\ disjoint salt msg /\ disjoint m msg /\
          disjoint m salt /\ as_seq h m == LSeq.create (v len) (uint #t 0) /\
          LS.rsapss_sign_pre a (v modBits) (v saltLen) (as_seq h salt) (v msgLen) (as_seq h msg))
      (ensures
        fun h0 _ h1 ->
          modifies (loc m) h0 h1 /\
          as_seq h1 m ==
          LS.rsapss_sign_msg_to_bn a
            (v modBits)
            (v saltLen)
            (as_seq h0 salt)
            (v msgLen)
            (as_seq h0 msg))
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 Spec.Hash.Definitions.hash_alg Prims.b2t Spec.RSAPSS.hash_is_supported Hacl.Impl.RSAPSS.modBits_t Lib.IntTypes.size_t Lib.Buffer.lbuffer Lib.IntTypes.uint8 Hacl.Bignum.Definitions.lbignum Prims.unit FStar.Monotonic.HyperStack.mem Prims.l_and Lib.Buffer.live Lib.Buffer.MUT Hacl.Bignum.Definitions.limb Lib.Buffer.disjoint Prims.eq2 Lib.Sequence.lseq Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.Buffer.as_seq Lib.Sequence.create Lib.IntTypes.uint Lib.IntTypes.SEC Hacl.Spec.RSAPSS.rsapss_sign_pre Lib.Buffer.modifies Lib.Buffer.loc Lib.Sequence.seq Prims.l_or Prims.nat FStar.Seq.Base.length Hacl.Spec.Bignum.Definitions.limb Hacl.Spec.Bignum.Definitions.blocks Lib.IntTypes.bits Hacl.Spec.RSAPSS.rsapss_sign_msg_to_bn Lib.IntTypes.int_t Prims.int Lib.IntTypes.range Prims.op_GreaterThan Prims.op_LessThanOrEqual Prims.op_Subtraction Prims.pow2 Prims.op_Multiply Lib.IntTypes.mk_int Hacl.Bignum.Definitions.blocks Lib.IntTypes.size
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}


inline_for_extraction noextract
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))


inline_for_extraction noextract
val rsapss_sign_bn: #t:limb_t -> ke:BE.exp t -> modBits:modBits_t t -> rsapss_sign_bn_st t ke modBits
let rsapss_sign_bn #t ke modBits eBits dBits skey m m' s =
  [@inline_let] let bits : size_pos = bits t in
  let nLen = blocks modBits (size bits) in
  let eLen = blocks eBits (size bits) in
  let dLen = blocks dBits (size bits) in

  let n  = sub skey 0ul nLen in
  let r2 = sub skey nLen nLen in
  let e  = sub skey (nLen +! nLen) eLen in
  let d  = sub skey (nLen +! nLen +! eLen) dLen in

  Math.Lemmas.pow2_le_compat (bits * v nLen) (v modBits);
  let h0 = ST.get () in
  SM.bn_precomp_r2_mod_n_lemma (v modBits - 1) (as_seq h0 n);
  BE.mk_bn_mod_exp_precompr2 nLen ke.BE.exp_ct_precomp n r2 m dBits d s;
  BE.mk_bn_mod_exp_precompr2 nLen ke.BE.exp_vt_precomp n r2 s eBits e m';
  let h1 = ST.get () in
  SD.bn_eval_inj (v nLen) (as_seq h1 s)
    (SE.bn_mod_exp_consttime_precompr2 (v nLen) (as_seq h0 n) (as_seq h0 r2)
    (as_seq h0 m) (v dBits) (as_seq h0 d));
  SD.bn_eval_inj (v nLen) (as_seq h1 m')
    (SE.bn_mod_exp_vartime_precompr2 (v nLen) (as_seq h0 n) (as_seq h0 r2)
    (as_seq h1 s) (v eBits) (as_seq h0 e));
  let eq_m = BN.bn_eq_mask nLen m m' in
  mapT nLen s (logand eq_m) s;
  BB.unsafe_bool_of_limb eq_m
val rsapss_sign_msg_to_bn_st : t: Hacl.Bignum.Definitions.limb_t ->
    a: Spec.Hash.Definitions.hash_alg{Spec.RSAPSS.hash_is_supported a} ->
    modBits: Hacl.Impl.RSAPSS.modBits_t t
  -> Type0

    t: Hacl.Bignum.Definitions.limb_t ->
    a: Spec.Hash.Definitions.hash_alg{Spec.RSAPSS.hash_is_supported a} ->
    modBits: Hacl.Impl.RSAPSS.modBits_t t
  -> Type0