val footprint: #a:supported_alg -> st:state a -> GTot B.loc
let footprint #a st =
  let k:B.buffer uint8 = st.k in
  let v:B.buffer uint8 = st.v in
  let ctr:B.buffer size_t = st.reseed_counter in
  B.loc_addr_of_buffer k |+| B.loc_addr_of_buffer v |+| B.loc_addr_of_buffer ctr
val footprint: #a:supported_alg -> st:state a -> GTot B.loc
let footprint #a st =
let k:B.buffer uint8 = st.k in
let v:B.buffer uint8 = st.v in
let ctr:B.buffer size_t = st.reseed_counter in
B.loc_addr_of_buffer k |+| B.loc_addr_of_buffer v |+| B.loc_addr_of_buffer ctr
Hacl.HMAC_DRBG.fst.checked
Spec.HMAC_DRBG.fst.checked Spec.HMAC_DRBG.fst.checked Spec.Hash.Definitions.fst.checked Spec.Agile.HMAC.fsti.checked prims.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.HMAC.fsti.checked Hacl.Hash.Definitions.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.HMAC_DRBG.fst
Hacl.HMAC_DRBG.supported_alg Hacl.HMAC_DRBG.state Lib.Buffer.op_Bar_Plus_Bar LowStar.Monotonic.Buffer.loc_addr_of_buffer Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC LowStar.Buffer.trivial_preorder Lib.IntTypes.U32 Lib.IntTypes.PUB LowStar.Buffer.buffer Hacl.HMAC_DRBG.__proj__State__item__reseed_counter Hacl.HMAC_DRBG.__proj__State__item__v Hacl.HMAC_DRBG.__proj__State__item__k LowStar.Monotonic.Buffer.loc
module Hacl.HMAC_DRBG

open FStar.HyperStack.ST
module ST = FStar.HyperStack.ST

open Spec.Hash.Definitions

open Lib.IntTypes
open Lib.Buffer

module HS = FStar.HyperStack
module B = LowStar.Buffer
module LSeq = Lib.Sequence

module HMAC = Hacl.HMAC
module S = Spec.HMAC_DRBG

friend Spec.HMAC_DRBG

unfold
let hash_len (a:supported_alg) = Hacl.Hash.Definitions.hash_len a

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

inline_for_extraction noextract
val update_round: #a:supported_alg
  -> hmac:HMAC.compute_st a
  -> len:size_t
  -> data:lbuffer uint8 len
  -> n:uint8
  -> k:lbuffer uint8 (hash_len a)
  -> v:lbuffer uint8 (hash_len a)
  -> Stack unit
  (requires fun h0 ->
    live h0 k /\ live h0 v /\ live h0 data /\
    disjoint k v /\
    // HMAC input length must fit in size_t
    hash_length a + 1 + uint_v len + block_length a < pow2 32)
  (ensures  fun h0 _ h1 ->
    S.hmac_input_bound a;
    as_seq h1 k == Spec.Agile.HMAC.hmac a
      (as_seq h0 k)
      (Seq.append (as_seq h0 v) (Seq.cons n (as_seq h0 data))) /\
    as_seq h1 v == Spec.Agile.HMAC.hmac a (as_seq h1 k) (as_seq h0 v) /\
    modifies2 k v h0 h1)

let update_round #a hmac len data n k v =
  let h0 = ST.get() in
  push_frame();
  let input_len = hash_len a +! 1ul +! len in
  let input = create input_len (u8 0) in
  let k' = sub input 0ul (hash_len a) in
  copy k' v;
  if len <> 0ul then copy (sub input (hash_len a +! 1ul) len) data;
  input.(hash_len a) <- n;
  let h1 = ST.get() in
  assert (Seq.equal (as_seq h1 input)
                    (Seq.append (as_seq h0 v) (Seq.cons n (as_seq h0 data))));
  S.hmac_input_bound a;
  hmac k' k (hash_len a) input input_len;
  hmac v k' (hash_len a) v (hash_len a);
  copy k k';
  pop_frame()


inline_for_extraction noextract
val update: #a:supported_alg
  -> hmac:HMAC.compute_st a
  -> len:size_t
  -> data:lbuffer uint8 len
  -> k:lbuffer uint8 (hash_len a)
  -> v:lbuffer uint8 (hash_len a)
  -> Stack unit
  (requires fun h0 ->
    live h0 data /\ live h0 k /\ live h0 v /\
    disjoint k v /\ disjoint k data /\ disjoint v data /\
    hash_length a + 1 + uint_v len + block_length a < pow2 32)
  (ensures  fun h0 _ h1 ->
    S.hmac_input_bound a;
    let k', v' = S.update #a (as_seq h0 data) (as_seq h0 k) (as_seq h0 v) in
    modifies2 k v h0 h1 /\
    as_seq h1 k == k' /\
    as_seq h1 v == v')

let update #a hmac len data k v  =
  update_round hmac len data (u8 0) k v;
  if len <> 0ul then
    update_round hmac len data (u8 1) k v


noeq
type state (a:supported_alg) =
| State:
    k:lbuffer uint8 (hash_len a)
  -> v:lbuffer uint8 (hash_len a)
  -> reseed_counter:lbuffer size_t 1ul
    {disjoint k v /\ disjoint k reseed_counter /\ disjoint v reseed_counter}
  -> state a

let freeable #a st =
  let k:B.buffer uint8 = st.k in
  let v:B.buffer uint8 = st.v in
  let ctr:B.buffer size_t = st.reseed_counter in
  B.freeable k /\ B.freeable v /\ B.freeable ctr
val footprint: #a:supported_alg -> st:state a -> GTot B.loc
st: Hacl.HMAC_DRBG.state a -> Prims.GTot LowStar.Monotonic.Buffer.loc