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()
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 ()
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.compute_st Lib.IntTypes.size_t Lib.Buffer.lbuffer Lib.IntTypes.uint8 Hacl.HMAC_DRBG.hash_len FStar.HyperStack.ST.pop_frame Prims.unit Lib.Buffer.copy Lib.Buffer.MUT Spec.HMAC_DRBG.hmac_input_bound Prims._assert FStar.Seq.Base.equal Lib.Buffer.as_seq FStar.Seq.Base.append FStar.Seq.Properties.cons FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Lib.Buffer.op_Array_Assignment Prims.op_disEquality FStar.UInt32.t FStar.UInt32.__uint_to_t Lib.Buffer.lbuffer_t Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.Buffer.sub Lib.IntTypes.op_Plus_Bang Lib.IntTypes.U32 Lib.IntTypes.PUB Prims.bool Hacl.Hash.Definitions.hash_len Lib.Buffer.create Lib.IntTypes.u8 FStar.HyperStack.ST.push_frame
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)
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)

    hmac: Hacl.HMAC.compute_st a ->
    len: Lib.IntTypes.size_t ->
    data: Lib.Buffer.lbuffer Lib.IntTypes.uint8 len ->
    n: Lib.IntTypes.uint8 ->
    k: Lib.Buffer.lbuffer Lib.IntTypes.uint8 (Hacl.HMAC_DRBG.hash_len a) ->
    v: Lib.Buffer.lbuffer Lib.IntTypes.uint8 (Hacl.HMAC_DRBG.hash_len a)
  -> FStar.HyperStack.ST.Stack Prims.unit