val rsapss_sign_msg_to_bn:
    #t:limb_t
  -> a:Hash.hash_alg{S.hash_is_supported a}
  -> modBits:modBits_t t ->
  rsapss_sign_msg_to_bn_st t a modBits
let rsapss_sign_msg_to_bn #t a modBits saltLen salt msgLen msg m =
  push_frame ();
  [@inline_let] let bits : size_pos = bits t in
  [@inline_let] let numb : size_pos = numbytes t in
  let nLen = blocks modBits (size bits) in

  let emBits = modBits -! 1ul in
  let emLen = blocks emBits 8ul in
  [@inline_let] let mLen = blocks emLen (size numb) in

  let em = create emLen (u8 0) in
  RP.pss_encode a saltLen salt msgLen msg emBits em;
  LS.blocks_bits_lemma t (v emBits);
  LS.blocks_numb_lemma t (v emBits);
  assert (SD.blocks (v emBits) bits = v mLen);
  assert (numb * v mLen <= max_size_t);
  assert (v mLen <= v nLen);

  let h' = ST.get () in
  update_sub_f h' m 0ul mLen
    (fun h -> SB.bn_from_bytes_be (v emLen) (as_seq h' em))
    (fun _ -> BN.bn_from_bytes_be emLen em (sub m 0ul mLen));
  pop_frame ()
val rsapss_sign_msg_to_bn:
    #t:limb_t
  -> a:Hash.hash_alg{S.hash_is_supported a}
  -> modBits:modBits_t t ->
  rsapss_sign_msg_to_bn_st t a modBits
let rsapss_sign_msg_to_bn #t a modBits saltLen salt msgLen msg m =
push_frame ();
[@@ inline_let ]let bits:size_pos = bits t in
[@@ inline_let ]let numb:size_pos = numbytes t in
let nLen = blocks modBits (size bits) in
let emBits = modBits -! 1ul in
let emLen = blocks emBits 8ul in
[@@ inline_let ]let mLen = blocks emLen (size numb) in
let em = create emLen (u8 0) in
RP.pss_encode a saltLen salt msgLen msg emBits em;
LS.blocks_bits_lemma t (v emBits);
LS.blocks_numb_lemma t (v emBits);
assert (SD.blocks (v emBits) bits = v mLen);
assert (numb * v mLen <= max_size_t);
assert (v mLen <= v nLen);
let h' = ST.get () in
update_sub_f h'
  m
  0ul
  mLen
  (fun h -> SB.bn_from_bytes_be (v emLen) (as_seq h' em))
  (fun _ -> BN.bn_from_bytes_be emLen em (sub m 0ul mLen));
pop_frame ()
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 Hacl.Bignum.Definitions.blocks Lib.IntTypes.size Lib.IntTypes.bits FStar.HyperStack.ST.pop_frame Prims.unit Lib.Buffer.update_sub_f Hacl.Bignum.Definitions.limb FStar.UInt32.__uint_to_t FStar.Monotonic.HyperStack.mem Hacl.Spec.Bignum.bn_from_bytes_be Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.Buffer.as_seq Lib.Buffer.MUT Lib.Sequence.lseq Hacl.Bignum.bn_from_bytes_be Lib.IntTypes.mk_int Lib.IntTypes.numbytes Lib.Buffer.sub Lib.Buffer.lbuffer_t FStar.HyperStack.ST.get Prims._assert Prims.op_LessThanOrEqual FStar.Mul.op_Star Lib.IntTypes.max_size_t Prims.op_Equality Prims.int Prims.l_or Prims.l_and Prims.op_GreaterThan Lib.IntTypes.range Hacl.Spec.Bignum.Definitions.blocks Hacl.Spec.RSAPSS.blocks_numb_lemma Hacl.Spec.RSAPSS.blocks_bits_lemma Hacl.Impl.RSAPSS.Padding.pss_encode Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.Buffer.create Lib.IntTypes.u8 Prims.eq2 Prims.op_Subtraction Prims.pow2 Prims.op_Multiply FStar.UInt32.uint_to_t FStar.UInt32.t Lib.IntTypes.op_Subtraction_Bang Prims.pos FStar.HyperStack.ST.push_frame
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


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


inline_for_extraction noextract
val rsapss_sign_msg_to_bn:
    #t:limb_t
  -> a:Hash.hash_alg{S.hash_is_supported a}
  -> modBits:modBits_t t ->
  rsapss_sign_msg_to_bn_st t a modBits
val rsapss_sign_msg_to_bn:
    #t:limb_t
  -> a:Hash.hash_alg{S.hash_is_supported a}
  -> modBits:modBits_t t ->
  rsapss_sign_msg_to_bn_st t a modBits

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