val db_zero:
    len:size_t{v len > 0}
  -> db:lbuffer uint8 len
  -> emBits:size_t ->
  Stack unit
  (requires fun h -> live h db)
  (ensures  fun h0 _ h1 -> modifies (loc db) h0 h1 /\
    as_seq h1 db == S.db_zero #(v len) (as_seq h0 db) (v emBits))
let db_zero len db emBits =
  let msBits = emBits %. 8ul in
  if msBits >. 0ul then
    db.(0ul) <- db.(0ul) &. (u8 0xff >>. (8ul -. msBits))
val db_zero:
    len:size_t{v len > 0}
  -> db:lbuffer uint8 len
  -> emBits:size_t ->
  Stack unit
  (requires fun h -> live h db)
  (ensures  fun h0 _ h1 -> modifies (loc db) h0 h1 /\
    as_seq h1 db == S.db_zero #(v len) (as_seq h0 db) (v emBits))
let db_zero len db emBits =
let msBits = emBits %. 8ul in
if msBits >. 0ul then db.(0ul) <- db.(0ul) &. (u8 0xff >>. (8ul -. msBits))
Hacl.Impl.RSAPSS.Padding.fst.checked
Spec.RSAPSS.fst.checked Spec.Hash.Definitions.fst.checked Spec.Agile.Hash.fsti.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked Hacl.Impl.RSAPSS.MGF.fst.checked Hacl.Bignum.Definitions.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.Impl.RSAPSS.Padding.fst
Lib.IntTypes.size_t Prims.b2t Prims.op_GreaterThan Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.Buffer.lbuffer Lib.IntTypes.uint8 Lib.IntTypes.op_Greater_Dot FStar.UInt32.__uint_to_t Lib.Buffer.op_Array_Assignment Prims.unit Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.IntTypes.op_Amp_Dot Lib.IntTypes.op_Greater_Greater_Dot Lib.IntTypes.u8 Lib.IntTypes.op_Subtraction_Dot Lib.Buffer.op_Array_Access Lib.Buffer.MUT Prims.bool Lib.IntTypes.op_Percent_Dot
module Hacl.Impl.RSAPSS.Padding

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

open Lib.IntTypes
open Lib.Buffer

open Hacl.Impl.RSAPSS.MGF

module ST = FStar.HyperStack.ST
module LSeq = Lib.Sequence

module Hash = Spec.Agile.Hash
module S = Spec.RSAPSS
module BD = Hacl.Bignum.Definitions


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

inline_for_extraction noextract
let less_than_max_input_length = Spec.Hash.Definitions.less_than_max_input_length

inline_for_extraction noextract
let salt_len_t (a:Hash.fixed_len_alg) =
  saltLen:size_t{8 + Hash.hash_length a + v saltLen <= max_size_t /\ (8 + Hash.hash_length a + v saltLen) `less_than_max_input_length` a}

inline_for_extraction noextract
let msg_len_t (a:Hash.fixed_len_alg) =
  msgLen:size_t{v msgLen `less_than_max_input_length` a}

inline_for_extraction noextract
let em_len_t (a:Hash.fixed_len_alg) (saltLen:salt_len_t a) =
  emBits:size_t{0 < v emBits /\ Hash.hash_length a + v saltLen + 2 <= S.blocks (v emBits) 8}


inline_for_extraction noextract
val xor_bytes:
    len:size_t{v len > 0}
  -> b1:lbuffer uint8 len
  -> b2:lbuffer uint8 len ->
  Stack unit
  (requires fun h -> live h b1 /\ live h b2 /\ disjoint b1 b2)
  (ensures  fun h0 _ h1 -> modifies (loc b1) h0 h1 /\
    as_seq h1 b1 == S.xor_bytes (as_seq h0 b1) (as_seq h0 b2))

let xor_bytes len b1 b2 =
  map2T len b1 (fun x y -> x ^. y) b1 b2


inline_for_extraction noextract
val db_zero:
    len:size_t{v len > 0}
  -> db:lbuffer uint8 len
  -> emBits:size_t ->
  Stack unit
  (requires fun h -> live h db)
  (ensures  fun h0 _ h1 -> modifies (loc db) h0 h1 /\
    as_seq h1 db == S.db_zero #(v len) (as_seq h0 db) (v emBits))
val db_zero:
    len:size_t{v len > 0}
  -> db:lbuffer uint8 len
  -> emBits:size_t ->
  Stack unit
  (requires fun h -> live h db)
  (ensures  fun h0 _ h1 -> modifies (loc db) h0 h1 /\
    as_seq h1 db == S.db_zero #(v len) (as_seq h0 db) (v emBits))

    len: Lib.IntTypes.size_t{Lib.IntTypes.v len > 0} ->
    db: Lib.Buffer.lbuffer Lib.IntTypes.uint8 len ->
    emBits: Lib.IntTypes.size_t
  -> FStar.HyperStack.ST.Stack Prims.unit