val get_iv:
  a:Spec.alg
  -> s: size_t{size_v s < 8} ->
  Stack (word_t a)
    (requires (fun h -> True))
    (ensures  (fun h0 z h1 -> h0 == h1 /\
      v z == v (Seq.index (Spec.ivTable a) (v s))))
let get_iv a s =
  recall_contents #(Spec.pub_word_t Spec.Blake2S) #8ul ivTable_S (Spec.ivTable Spec.Blake2S);
  recall_contents #(Spec.pub_word_t Spec.Blake2B) #8ul ivTable_B (Spec.ivTable Spec.Blake2B);
  [@inline_let]
  let ivTable: (x:glbuffer (Spec.pub_word_t a) 8ul{witnessed x (Spec.ivTable a) /\ recallable x}) =
    match a with
    | Spec.Blake2S -> ivTable_S
    | Spec.Blake2B -> ivTable_B
  in
  let r = index ivTable s in
  secret #(Spec.wt a) r
val get_iv:
  a:Spec.alg
  -> s: size_t{size_v s < 8} ->
  Stack (word_t a)
    (requires (fun h -> True))
    (ensures  (fun h0 z h1 -> h0 == h1 /\
      v z == v (Seq.index (Spec.ivTable a) (v s))))
let get_iv a s =
recall_contents #(Spec.pub_word_t Spec.Blake2S) #8ul ivTable_S (Spec.ivTable Spec.Blake2S);
recall_contents #(Spec.pub_word_t Spec.Blake2B) #8ul ivTable_B (Spec.ivTable Spec.Blake2B);
[@@ inline_let ]let ivTable:(x:
  glbuffer (Spec.pub_word_t a) 8ul {witnessed x (Spec.ivTable a) /\ recallable x}) =
  match a with
  | Spec.Blake2S -> ivTable_S
  | Spec.Blake2B -> ivTable_B
in
let r = index ivTable s in
secret #(Spec.wt a) r
Hacl.Impl.Blake2.Generic.fst.checked
Spec.Blake2.fst.checked prims.fst.checked LowStar.Modifies.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked Hacl.Impl.Blake2.Core.fsti.checked Hacl.Impl.Blake2.Constants.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
Hacl.Impl.Blake2.Generic.fst
Spec.Blake2.alg Lib.IntTypes.size_t Prims.b2t Prims.op_LessThan Lib.IntTypes.size_v Lib.IntTypes.secret Spec.Blake2.wt Hacl.Impl.Blake2.Core.word_t Spec.Blake2.pub_word_t Lib.Buffer.index Lib.Buffer.CONST FStar.UInt32.uint_to_t Lib.Buffer.lbuffer_t FStar.UInt32.t Prims.eq2 LowStar.ConstBuffer.qual LowStar.ConstBuffer.qual_of LowStar.ConstBuffer.IMMUTABLE Prims.l_and Lib.Buffer.witnessed Spec.Blake2.ivTable Lib.Buffer.recallable Hacl.Impl.Blake2.Constants.ivTable_S Hacl.Impl.Blake2.Constants.ivTable_B Prims.unit Lib.Buffer.recall_contents Spec.Blake2.Blake2B FStar.UInt32.__uint_to_t Spec.Blake2.Blake2S
module Hacl.Impl.Blake2.Generic

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

open Lib.IntTypes
open Lib.Buffer
open Lib.ByteBuffer
open Lib.LoopCombinators

module ST = FStar.HyperStack.ST
module Seq = Lib.Sequence
module Loops = Lib.LoopCombinators
module Spec = Spec.Blake2

open Hacl.Impl.Blake2.Constants
open Hacl.Impl.Blake2.Core

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

noextract
let is_valid_blake2_config (a : Spec.alg) (m : m_spec) =
  match a, m with
  | Spec.Blake2S, M32 | Spec.Blake2S, M128
  | Spec.Blake2B, M32 | Spec.Blake2B, M256 -> true
  | _ -> false

inline_for_extraction noextract
let valid_m_spec (a : Spec.alg) = m:m_spec{is_valid_blake2_config a m}

/// Accessors for constants

inline_for_extraction noextract
val get_iv:
  a:Spec.alg
  -> s: size_t{size_v s < 8} ->
  Stack (word_t a)
    (requires (fun h -> True))
    (ensures  (fun h0 z h1 -> h0 == h1 /\
      v z == v (Seq.index (Spec.ivTable a) (v s))))
val get_iv:
  a:Spec.alg
  -> s: size_t{size_v s < 8} ->
  Stack (word_t a)
    (requires (fun h -> True))
    (ensures  (fun h0 z h1 -> h0 == h1 /\
      v z == v (Seq.index (Spec.ivTable a) (v s))))
a: Spec.Blake2.alg -> s: Lib.IntTypes.size_t{Lib.IntTypes.size_v s < 8}
  -> FStar.HyperStack.ST.Stack (Hacl.Impl.Blake2.Core.word_t a)