val shake256_4x:
    input_len:size_t
  -> input0:lbuffer uint8 input_len
  -> input1:lbuffer uint8 input_len
  -> input2:lbuffer uint8 input_len
  -> input3:lbuffer uint8 input_len
  -> output_len:size_t
  -> output0:lbuffer uint8 output_len
  -> output1:lbuffer uint8 output_len
  -> output2:lbuffer uint8 output_len
  -> output3:lbuffer uint8 output_len
  -> Stack unit
    (requires fun h ->
      live h input0 /\ live h input1 /\ live h input2 /\ live h input3 /\
      live h output0 /\ live h output1 /\ live h output2 /\ live h output3 /\
      loc_pairwise_disjoint
        [loc input0; loc input1; loc input2; loc input3;
         loc output0; loc output1; loc output2; loc output3])
    (ensures  fun h0 _ h1 ->
      modifies (loc_union (loc_union (loc output0) (loc output1))
                          (loc_union (loc output2) (loc output3))) h0 h1 /\
      as_seq h1 output0 == S.shake256 (v input_len) (as_seq h0 input0) (v output_len) /\
      as_seq h1 output1 == S.shake256 (v input_len) (as_seq h0 input1) (v output_len) /\
      as_seq h1 output2 == S.shake256 (v input_len) (as_seq h0 input2) (v output_len) /\
      as_seq h1 output3 == S.shake256 (v input_len) (as_seq h0 input3) (v output_len))
let shake256_4x input_len input0 input1 input2 input3 output_len output0 output1 output2 output3 =
  SHA3.shake256_hacl input_len input0 output_len output0;
  SHA3.shake256_hacl input_len input1 output_len output1;
  SHA3.shake256_hacl input_len input2 output_len output2;
  SHA3.shake256_hacl input_len input3 output_len output3
val shake256_4x:
    input_len:size_t
  -> input0:lbuffer uint8 input_len
  -> input1:lbuffer uint8 input_len
  -> input2:lbuffer uint8 input_len
  -> input3:lbuffer uint8 input_len
  -> output_len:size_t
  -> output0:lbuffer uint8 output_len
  -> output1:lbuffer uint8 output_len
  -> output2:lbuffer uint8 output_len
  -> output3:lbuffer uint8 output_len
  -> Stack unit
    (requires fun h ->
      live h input0 /\ live h input1 /\ live h input2 /\ live h input3 /\
      live h output0 /\ live h output1 /\ live h output2 /\ live h output3 /\
      loc_pairwise_disjoint
        [loc input0; loc input1; loc input2; loc input3;
         loc output0; loc output1; loc output2; loc output3])
    (ensures  fun h0 _ h1 ->
      modifies (loc_union (loc_union (loc output0) (loc output1))
                          (loc_union (loc output2) (loc output3))) h0 h1 /\
      as_seq h1 output0 == S.shake256 (v input_len) (as_seq h0 input0) (v output_len) /\
      as_seq h1 output1 == S.shake256 (v input_len) (as_seq h0 input1) (v output_len) /\
      as_seq h1 output2 == S.shake256 (v input_len) (as_seq h0 input2) (v output_len) /\
      as_seq h1 output3 == S.shake256 (v input_len) (as_seq h0 input3) (v output_len))
let shake256_4x input_len input0 input1 input2 input3 output_len output0 output1 output2 output3 =
SHA3.shake256_hacl input_len input0 output_len output0;
SHA3.shake256_hacl input_len input1 output_len output1;
SHA3.shake256_hacl input_len input2 output_len output2;
SHA3.shake256_hacl input_len input3 output_len output3
Hacl.Keccak.fst.checked
prims.fst.checked LowStar.Buffer.fst.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.SHA3.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.All.fst.checked
Hacl.Keccak.fst
Lib.IntTypes.size_t Lib.Buffer.lbuffer Lib.IntTypes.uint8 Hacl.SHA3.shake256_hacl Prims.unit
module Hacl.Keccak

open FStar.HyperStack.All

open LowStar.Buffer

open Lib.IntTypes
open Lib.Buffer

module SHA3 = Hacl.SHA3

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

(* This is a stub non-vectorized implementation intended to be replaced by a real
   vectorized implementation like the one in fips202.c for x64
*)

let shake128_4x input_len input0 input1 input2 input3 output_len output0 output1 output2 output3 =
  SHA3.shake128_hacl input_len input0 output_len output0;
  SHA3.shake128_hacl input_len input1 output_len output1;
  SHA3.shake128_hacl input_len input2 output_len output2;
  SHA3.shake128_hacl input_len input3 output_len output3
val shake256_4x:
    input_len:size_t
  -> input0:lbuffer uint8 input_len
  -> input1:lbuffer uint8 input_len
  -> input2:lbuffer uint8 input_len
  -> input3:lbuffer uint8 input_len
  -> output_len:size_t
  -> output0:lbuffer uint8 output_len
  -> output1:lbuffer uint8 output_len
  -> output2:lbuffer uint8 output_len
  -> output3:lbuffer uint8 output_len
  -> Stack unit
    (requires fun h ->
      live h input0 /\ live h input1 /\ live h input2 /\ live h input3 /\
      live h output0 /\ live h output1 /\ live h output2 /\ live h output3 /\
      loc_pairwise_disjoint
        [loc input0; loc input1; loc input2; loc input3;
         loc output0; loc output1; loc output2; loc output3])
    (ensures  fun h0 _ h1 ->
      modifies (loc_union (loc_union (loc output0) (loc output1))
                          (loc_union (loc output2) (loc output3))) h0 h1 /\
      as_seq h1 output0 == S.shake256 (v input_len) (as_seq h0 input0) (v output_len) /\
      as_seq h1 output1 == S.shake256 (v input_len) (as_seq h0 input1) (v output_len) /\
      as_seq h1 output2 == S.shake256 (v input_len) (as_seq h0 input2) (v output_len) /\
      as_seq h1 output3 == S.shake256 (v input_len) (as_seq h0 input3) (v output_len))

    input_len: Lib.IntTypes.size_t ->
    input0: Lib.Buffer.lbuffer Lib.IntTypes.uint8 input_len ->
    input1: Lib.Buffer.lbuffer Lib.IntTypes.uint8 input_len ->
    input2: Lib.Buffer.lbuffer Lib.IntTypes.uint8 input_len ->
    input3: Lib.Buffer.lbuffer Lib.IntTypes.uint8 input_len ->
    output_len: Lib.IntTypes.size_t ->
    output0: Lib.Buffer.lbuffer Lib.IntTypes.uint8 output_len ->
    output1: Lib.Buffer.lbuffer Lib.IntTypes.uint8 output_len ->
    output2: Lib.Buffer.lbuffer Lib.IntTypes.uint8 output_len ->
    output3: Lib.Buffer.lbuffer Lib.IntTypes.uint8 output_len
  -> FStar.HyperStack.ST.Stack Prims.unit