1	import Base
2	import ../../../src/crypto/sha3/core.bend as C
3	import ./conformance.bend as Conformance
4	import ./laws.bend as Laws
5	
6	# Gate for the SHA3-256 package: `bend proofs/crypto/sha3/proof.bend` prints
7	# ALL PROOFS CHECK when every law of laws.bend holds. The conformance is
8	# proved for every round count; SHA3-256 instantiates 24.
9	
10	def Laws.sha3_256_correct(bytes):
11	  Conformance.keccak_correct(bytes, 24n)
12	
13	def Laws.sha3_256_length(bytes):
14	  Conformance.digest_length(C.absorb(C.lanes(List.append(&2, U32, bytes,
15	    C.suffix(List.length(&2, U32, bytes)))), 24n, C.zero()))