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_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
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 Hacl.Spec.Bignum.Base.unsafe_bool_of_limb Prims.bool Prims.unit Lib.Buffer.mapT Lib.Buffer.MUT Hacl.Bignum.Definitions.limb Lib.IntTypes.logand Lib.IntTypes.SEC Hacl.Bignum.bn_eq_mask Hacl.Spec.Bignum.Definitions.bn_eval_inj Lib.Buffer.as_seq Hacl.Spec.Bignum.Exponentiation.bn_mod_exp_vartime_precompr2 Hacl.Spec.Bignum.Exponentiation.bn_mod_exp_consttime_precompr2 FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Hacl.Bignum.Exponentiation.mk_bn_mod_exp_precompr2 Hacl.Bignum.Exponentiation.__proj__Mkexp__item__exp_vt_precomp Hacl.Bignum.Exponentiation.__proj__Mkexp__item__exp_ct_precomp Hacl.Spec.Bignum.Montgomery.bn_precomp_r2_mod_n_lemma Prims.op_Subtraction FStar.Math.Lemmas.pow2_le_compat FStar.Mul.op_Star Lib.Buffer.lbuffer_t Lib.Buffer.sub Lib.IntTypes.int_t Prims.eq2 Prims.int Prims.l_or Lib.IntTypes.range Prims.l_and Prims.b2t Prims.op_GreaterThan Prims.op_LessThanOrEqual Prims.pow2 Prims.op_Multiply Lib.IntTypes.mk_int Hacl.Spec.Bignum.Definitions.blocks Prims.pos
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
val rsapss_sign_bn: #t:limb_t -> ke:BE.exp t -> modBits:modBits_t t -> rsapss_sign_bn_st t ke modBits
ke: Hacl.Bignum.Exponentiation.exp t -> modBits: Hacl.Impl.RSAPSS.modBits_t t
  -> Hacl.Impl.RSAPSS.rsapss_sign_bn_st t ke modBits