let state_p (a:Spec.alg) (m:m_spec) =
  lbuffer (element_t a m) (4ul *. row_len a m)
let state_p (a: Spec.alg) (m: m_spec) =
lbuffer (element_t a m) (4ul *. row_len a m)
Hacl.Impl.Blake2.Core.fsti.checked
Spec.Blake2.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntVector.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Hacl.Impl.Blake2.Core.fsti
Spec.Blake2.alg Hacl.Impl.Blake2.Core.m_spec Lib.Buffer.lbuffer Hacl.Impl.Blake2.Core.element_t Lib.IntTypes.op_Star_Dot Lib.IntTypes.U32 Lib.IntTypes.PUB FStar.UInt32.__uint_to_t Hacl.Impl.Blake2.Core.row_len
module Hacl.Impl.Blake2.Core
module ST = FStar.HyperStack.ST
open FStar.HyperStack
open FStar.HyperStack.All
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer
open Lib.ByteBuffer
open Lib.IntVector

module Spec = Spec.Blake2

#set-options "--max_fuel 0 --max_ifuel 1"

type m_spec =
  | M32
  | M128
  | M256

noextract inline_for_extraction
type word_t (a:Spec.alg) = Spec.word_t a

noextract inline_for_extraction
let element_t (a:Spec.alg) (m:m_spec) =
  match a,m with
  | Spec.Blake2S,M128 -> (vec_t U32 4)
  | Spec.Blake2S,M256 -> (vec_t U32 4)
  | Spec.Blake2B,M256 -> (vec_t U64 4)
  | _ -> (word_t a)

noextract inline_for_extraction
val zero_element: a:Spec.alg -> m:m_spec -> element_t a m

noextract inline_for_extraction
let row_len (a:Spec.alg) (m:m_spec) : size_t =
  match a,m with
  | Spec.Blake2S,M128 -> 1ul
  | Spec.Blake2S,M256 -> 1ul
  | Spec.Blake2B,M256 -> 1ul
  | _ -> 4ul

noextract inline_for_extraction
unfold let row_p (a:Spec.alg) (m:m_spec) =
  lbuffer (element_t a m) (row_len a m)

noextract inline_for_extraction
val row_v: #a:Spec.alg -> #m:m_spec -> h:mem -> row_p a m -> GTot (Spec.row a)

noextract
val row_v_lemma: #a:Spec.alg -> #m:m_spec -> h0:mem -> h1:mem -> r1:row_p a m -> r2:row_p a m ->
  Lemma (ensures (as_seq h0 r1 == as_seq h1 r2 ==>
		  row_v h0 r1 == row_v h1 r2))
	[SMTPat (row_v h0 r1); SMTPat (row_v h1 r2)]

noextract inline_for_extraction
val state_p : a: Spec.Blake2.alg -> m: Hacl.Impl.Blake2.Core.m_spec -> Type0
a: Spec.Blake2.alg -> m: Hacl.Impl.Blake2.Core.m_spec -> Type0