1	import Base
2	import ../../../src/crypto/sha3/sha3_256.bend as SHA3
3	import ../../../spec/crypto/sha3.bend as FIPS
4	
5	# SHA3-256: the public API against the FIPS 202 specification
6	# spec/crypto/sha3.bend (sponge on the specification's Keccak-p[1600, 24]).
7	
8	# The digest of every byte list is the specification's.
9	law sha3_256_correct:
10	  for +bytes: List<&2, U32>
11	  {SHA3.sha3_256(bytes) == FIPS.sha3_256(bytes) : List<&2, U32>}
12	
13	# Every digest is 32 bytes.
14	law sha3_256_length:
15	  for +bytes: List<&2, U32>
16	  {List.length(&2, U32, SHA3.sha3_256(bytes)) == 32n : Nat}