inst_sha3.bend
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
13import Base
14import bend-osdev-bytes@0.1.0.0/bytes.bend as B
15import 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
19type CrSha3State is Data:
20 CrSha3State{h: Hc.Hasher}
21
22def CrSha3.init() -> CrSha3State:
23 CrSha3State{Hc.new_sha3_256()}
24
25# the state after more bytes
26def 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
32def 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
38def CrSha3.sha3_256(o: B.Octets) -> B.Octets:
39 B.Octets.of_list(Hc.sha3_256(B.Octets.to_list(o)))