1	# SHA3-256 (FIPS 202) as a hash: bend-collections' SHA3-256, adapted to
2	# Octets, as inst_sha2.bend adapts SHA-256 and SHA-512. The code is
3	# bend-collections@1.0.0.0's src/crypto (hash.bend and the keccak and sha3
4	# files it imports), imported from bend-collections-laws-crypto@1.0.0.0,
5	# which ships the same files with their proofs (Split.sha3_256,
6	# Incremental.sha3_256, Sha3_256.length, Sha3_256.value); LAWS.bend cites
7	# them. The state is wrapped in CrSha3State, and bytes cross as Octets.
8	#
9	# The instance (block size 136 bytes, the SHA3-256 rate, which is HMAC's
10	# B for SHA3-256; digest 32):
11	#   ~CrSha3State, ~136n, ~32n, ~CrSha3.init(), ~CrSha3.update,
12	#   ~CrSha3.final, ~CrSha3.sha3_256
13	import Base
14	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
15	import bend-collections-laws-crypto@1.0.0.0/src/crypto/hash.bend as Hc
16	
17	# A hash state (opaque): the Keccak state, the bytes of the unfinished
18	# block, and the length so far
19	type CrSha3State is Data:
20	  CrSha3State{h: Hc.Hasher}
21	
22	def CrSha3.init() -> CrSha3State:
23	  CrSha3State{Hc.new_sha3_256()}
24	
25	# the state after more bytes
26	def CrSha3.update(s: CrSha3State, o: B.Octets) -> CrSha3State:
27	  match s:
28	    case CrSha3State{h}:
29	      CrSha3State{Hc.update(h, B.Octets.to_list(o))}
30	
31	# the digest of the bytes so far
32	def CrSha3.final(s: CrSha3State) -> B.Octets:
33	  match s:
34	    case CrSha3State{h}:
35	      B.Octets.of_list(Hc.digest(h))
36	
37	# the digest in one call
38	def CrSha3.sha3_256(o: B.Octets) -> B.Octets:
39	  B.Octets.of_list(Hc.sha3_256(B.Octets.to_list(o)))