let failwith = LowStar.Failure.failwith
let failwith =
LowStar.Failure.failwith
Test.NoHeap.fst.checked
TestLib.fsti.checked Test.Vectors.Poly1305.fst.checked Test.Vectors.Curve25519.fst.checked Test.Vectors.Chacha20Poly1305.fst.checked Test.Vectors.fst.checked Test.Lowstarize.fst.checked Spec.Hash.Definitions.fst.checked Spec.Agile.HMAC.fsti.checked Spec.Agile.Hash.fsti.checked prims.fst.checked LowStar.Failure.fsti.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Lib.IntTypes.fst.checked Hacl.Hash.Definitions.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Int32.fsti.checked FStar.HyperStack.ST.fsti.checked EverCrypt.Poly1305.fsti.checked EverCrypt.HMAC.fsti.checked EverCrypt.HKDF.fsti.checked EverCrypt.Hash.Incremental.fst.checked EverCrypt.Hash.fsti.checked EverCrypt.Curve25519.fsti.checked EverCrypt.Cipher.fsti.checked EverCrypt.Chacha20Poly1305.fsti.checked C.String.fsti.checked C.Loops.fst.checked
Test.NoHeap.fst
LowStar.Failure.failwith Prims.string FStar.Monotonic.HyperStack.mem Prims.l_True Prims.l_False
module Test.NoHeap

module B = LowStar.Buffer
module L = Test.Lowstarize
module U32 = FStar.UInt32

open FStar.HyperStack.ST
open FStar.Integers
open LowStar.BufferOps
open Test.Lowstarize

let string_of_alg: Spec.Agile.Hash.hash_alg -> C.String.t =
  let open C.String in
  let open Spec.Agile.Hash in
  function
  | MD5 -> !$"MD5"
  | SHA1 -> !$"SHA1"
  | SHA2_224 -> !$"SHA2_224"
  | SHA2_256 -> !$"SHA2_256"
  | SHA2_384 -> !$"SHA2_384"
  | SHA2_512 -> !$"SHA2_512"
  | SHA3_224 -> !$"SHA3_224"
  | SHA3_256 -> !$"SHA3_256"
  | SHA3_384 -> !$"SHA3_384"
  | SHA3_512 -> !$"SHA3_512"
  | Blake2S -> !$"Blake2S"
  | Blake2B -> !$"Blake2B"
  | Shake128 -> !$"Shake128"
  | Shake256 -> !$"Shake256"

/// A module that contains stack-only tests, suitable for both C and Wasm. Other
/// tests that may make arbitrary use of the heap are in Test and Test.Hash.
///
/// .. note::
///   Tests in this module are *VERIFIED*. Please keep it this way.

noextract unfold inline_for_extraction
let (!$) = C.String.((!$))
val failwith : _: Prims.string -> FStar.HyperStack.ST.Stack _
_: Prims.string -> FStar.HyperStack.ST.Stack _