val xor_bytes_inplace:
  a: B.buffer uint8 ->
  b: B.buffer uint8 ->
  len: UInt32.t {v len = B.length a /\ v len = B.length b} ->
  Stack unit
  (requires fun h0 -> B.disjoint a b /\ B.live h0 a /\ B.live h0 b)
  (ensures fun h0 _ h1 ->
    B.(modifies (loc_buffer a) h0 h1) /\
    B.as_seq h1 a == Spec.Loops.seq_map2 ( ^. ) (B.as_seq h0 a) (B.as_seq h0 b))
let xor_bytes_inplace a b len =
  C.Loops.in_place_map2 a b len ( ^. )
val xor_bytes_inplace:
  a: B.buffer uint8 ->
  b: B.buffer uint8 ->
  len: UInt32.t {v len = B.length a /\ v len = B.length b} ->
  Stack unit
  (requires fun h0 -> B.disjoint a b /\ B.live h0 a /\ B.live h0 b)
  (ensures fun h0 _ h1 ->
    B.(modifies (loc_buffer a) h0 h1) /\
    B.as_seq h1 a == Spec.Loops.seq_map2 ( ^. ) (B.as_seq h0 a) (B.as_seq h0 b))
let xor_bytes_inplace a b len =
C.Loops.in_place_map2 a b len ( ^. )
Hacl.HMAC.fst.checked
Spec.Loops.fst.checked Spec.Hash.Lemmas.fsti.checked Spec.Hash.Incremental.Definitions.fst.checked Spec.Hash.Incremental.fsti.checked Spec.Hash.Definitions.fst.checked Spec.Agile.HMAC.fst.checked Spec.Agile.HMAC.fst.checked Spec.Agile.Hash.fst.checked Spec.Agile.Hash.fst.checked prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowStar.Ignore.fsti.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Lib.UpdateMulti.fst.checked Hacl.Streaming.SHA2.fst.checked Hacl.Impl.Blake2.Core.fsti.checked Hacl.Hash.SHA2.fsti.checked Hacl.Hash.SHA1.fsti.checked Hacl.Hash.Definitions.fst.checked Hacl.Hash.Blake2.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt128.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Int.Cast.Full.fst.checked FStar.Int.Cast.fst.checked FStar.HyperStack.ST.fsti.checked FStar.Ghost.fsti.checked FStar.Calc.fsti.checked C.Loops.fst.checked
Hacl.HMAC.fst
LowStar.Buffer.buffer Lib.IntTypes.uint8 FStar.UInt32.t Prims.l_and Prims.b2t Prims.op_Equality Prims.int Prims.l_or Prims.op_GreaterThanOrEqual Lib.IntTypes.range Lib.IntTypes.U32 Lib.IntTypes.v Lib.IntTypes.PUB LowStar.Monotonic.Buffer.length LowStar.Buffer.trivial_preorder C.Loops.in_place_map2 Lib.IntTypes.op_Hat_Dot Lib.IntTypes.U8 Lib.IntTypes.SEC Prims.unit
module Hacl.HMAC

module S = FStar.Seq
module D = Hacl.Hash.Definitions
module ST = FStar.HyperStack.ST
module B = LowStar.Buffer
module MB = LowStar.Monotonic.Buffer
module C = Hacl.Impl.Blake2.Core

open FStar.HyperStack.ST
open LowStar.BufferOps

open Spec.Hash.Definitions
open Spec.Agile.HMAC
open Spec.Agile.Hash
open Spec.Hash.Incremental
open Spec.Hash.Incremental.Definitions
open Spec.Hash.Lemmas
friend Spec.Agile.HMAC
friend Spec.Agile.Hash

let _: squash (inversion hash_alg) = allow_inversion hash_alg

#set-options "--max_fuel 0 --max_ifuel 0 --z3rlimit 50"

/// Helpers

inline_for_extraction
val xor_bytes_inplace:
  a: B.buffer uint8 ->
  b: B.buffer uint8 ->
  len: UInt32.t {v len = B.length a /\ v len = B.length b} ->
  Stack unit
  (requires fun h0 -> B.disjoint a b /\ B.live h0 a /\ B.live h0 b)
  (ensures fun h0 _ h1 ->
    B.(modifies (loc_buffer a) h0 h1) /\
    B.as_seq h1 a == Spec.Loops.seq_map2 ( ^. ) (B.as_seq h0 a) (B.as_seq h0 b))
inline_for_extraction
val xor_bytes_inplace:
  a: B.buffer uint8 ->
  b: B.buffer uint8 ->
  len: UInt32.t {v len = B.length a /\ v len = B.length b} ->
  Stack unit
  (requires fun h0 -> B.disjoint a b /\ B.live h0 a /\ B.live h0 b)
  (ensures fun h0 _ h1 ->
    B.(modifies (loc_buffer a) h0 h1) /\
    B.as_seq h1 a == Spec.Loops.seq_map2 ( ^. ) (B.as_seq h0 a) (B.as_seq h0 b))

    a: LowStar.Buffer.buffer Lib.IntTypes.uint8 ->
    b: LowStar.Buffer.buffer Lib.IntTypes.uint8 ->
    len:
      FStar.UInt32.t
        { Lib.IntTypes.v len = LowStar.Monotonic.Buffer.length a /\
          Lib.IntTypes.v len = LowStar.Monotonic.Buffer.length b }
  -> FStar.HyperStack.ST.Stack Prims.unit