val test_shake256:
     msg_len:size_t
  -> msg:lbuffer uint8 msg_len
  -> out_len:size_t{v out_len > 0}
  -> expected:lbuffer uint8 out_len
  -> Stack unit
    (requires fun h -> live h msg /\ live h expected)
    (ensures  fun h0 r h1 -> modifies0 h0 h1)
let test_shake256 msg_len msg out_len expected =
  push_frame ();
  let test = create out_len (u8 0) in
  shake256_hacl msg_len msg out_len test;
  if not (result_compare_display out_len (to_const test) (to_const expected)) then C.exit 255l;
  pop_frame ()
val test_shake256:
     msg_len:size_t
  -> msg:lbuffer uint8 msg_len
  -> out_len:size_t{v out_len > 0}
  -> expected:lbuffer uint8 out_len
  -> Stack unit
    (requires fun h -> live h msg /\ live h expected)
    (ensures  fun h0 r h1 -> modifies0 h0 h1)
let test_shake256 msg_len msg out_len expected =
push_frame ();
let test = create out_len (u8 0) in
shake256_hacl msg_len msg out_len test;
if not (result_compare_display out_len (to_const test) (to_const expected)) then C.exit 255l;
pop_frame ()
Hacl.Test.SHA3.fst.checked
prims.fst.checked Lib.RawIntTypes.fsti.checked Lib.PrintBuffer.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.SHA3.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.Int32.fsti.checked FStar.HyperStack.All.fst.checked C.String.fsti.checked C.fst.checked
Hacl.Test.SHA3.fst
Lib.IntTypes.size_t Lib.Buffer.lbuffer Lib.IntTypes.uint8 Prims.b2t Prims.op_GreaterThan Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB FStar.HyperStack.ST.pop_frame Prims.unit C.exit FStar.Int32.__int_to_t Prims.bool Prims.op_Negation Lib.PrintBuffer.result_compare_display Lib.Buffer.to_const Lib.Buffer.MUT Hacl.SHA3.shake256_hacl Lib.Buffer.lbuffer_t Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.Buffer.create Lib.IntTypes.u8 FStar.HyperStack.ST.push_frame
module Hacl.Test.SHA3

open FStar.HyperStack.All
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer
open Lib.PrintBuffer
open Hacl.SHA3

#reset-options "--z3rlimit 100 --fuel 0 --ifuel 0"

val test_sha3:
    msg_len:size_t
  -> msg:lbuffer uint8 msg_len
  -> expected224:lbuffer uint8 28ul
  -> expected256:lbuffer uint8 32ul
  -> expected384:lbuffer uint8 48ul
  -> expected512:lbuffer uint8 64ul
  -> Stack unit
    (requires fun h ->
      live h msg /\ live h expected224 /\ live h expected256 /\
      live h expected384 /\ live h expected512)
    (ensures  fun h0 r h1 -> True)

let test_sha3 msg_len msg expected224 expected256 expected384 expected512 =
  push_frame();
  let test224 = create 28ul (u8 0) in
  let test256 = create 32ul (u8 0) in
  let test384 = create 48ul (u8 0) in
  let test512 = create 64ul (u8 0) in

  sha3_224 msg_len msg test224;
  sha3_256 msg_len msg test256;
  sha3_384 msg_len msg test384;
  sha3_512 msg_len msg test512;

  if not (result_compare_display 28ul (to_const test224) (to_const expected224)) then C.exit 255l;
  if not (result_compare_display 32ul (to_const test256) (to_const expected256)) then C.exit 255l;
  if not (result_compare_display 48ul (to_const test384) (to_const expected384)) then C.exit 255l;
  if not (result_compare_display 64ul (to_const test512) (to_const expected512)) then C.exit 255l;
  pop_frame()


val test_shake128:
     msg_len:size_t
  -> msg:lbuffer uint8 msg_len
  -> out_len:size_t{v out_len > 0}
  -> expected:lbuffer uint8 out_len
  -> Stack unit
    (requires fun h -> live h msg /\ live h expected)
    (ensures  fun h0 r h1 -> modifies0 h0 h1)

let test_shake128 msg_len msg out_len expected =
  push_frame ();
  let test = create out_len (u8 0) in
  shake128_hacl msg_len msg out_len test;
  if not (result_compare_display out_len (to_const test) (to_const expected)) then C.exit 255l;
  pop_frame ()


val test_shake256:
     msg_len:size_t
  -> msg:lbuffer uint8 msg_len
  -> out_len:size_t{v out_len > 0}
  -> expected:lbuffer uint8 out_len
  -> Stack unit
    (requires fun h -> live h msg /\ live h expected)
    (ensures  fun h0 r h1 -> modifies0 h0 h1)
val test_shake256:
     msg_len:size_t
  -> msg:lbuffer uint8 msg_len
  -> out_len:size_t{v out_len > 0}
  -> expected:lbuffer uint8 out_len
  -> Stack unit
    (requires fun h -> live h msg /\ live h expected)
    (ensures  fun h0 r h1 -> modifies0 h0 h1)

    msg_len: Lib.IntTypes.size_t ->
    msg: Lib.Buffer.lbuffer Lib.IntTypes.uint8 msg_len ->
    out_len: Lib.IntTypes.size_t{Lib.IntTypes.v out_len > 0} ->
    expected: Lib.Buffer.lbuffer Lib.IntTypes.uint8 out_len
  -> FStar.HyperStack.ST.Stack Prims.unit