inst_sha2.bend
1# SHA-256 and SHA-512 (FIPS 180-4) as hashes: bend-collections' hashes,
2# adapted to Octets. The code is bend-collections@1.0.0.0's src/crypto
3# (hash.bend and the sha, sha512 and keccak files it imports), imported from
4# bend-collections-laws-crypto@1.0.0.0, which ships the same files with
5# their proofs: Bend names a def by the package it comes from, so those
6# proofs (Split.sha256, Incremental.sha256, Sha256.length, ...) are about
7# that package's copy, and this adapter uses it so that LAWS.bend can cite
8# them. No other file of bend-osdev sees bend-collections' types: the state
9# is wrapped in CrSha2State, and bytes cross as Octets.
10#
11# The instances (block size 64 and 128 bytes, digest 32 and 64):
12# ~CrSha2State, ~64n, ~32n, ~CrSha2.init256(), ~CrSha2.update,
13# ~CrSha2.final, ~CrSha2.sha256
14# ~CrSha2State, ~128n, ~64n, ~CrSha2.init512(), ~CrSha2.update,
15# ~CrSha2.final, ~CrSha2.sha512
16import Base
17import bend-osdev-bytes@0.1.0.0/bytes.bend as B
18import bend-collections-laws-crypto@1.0.0.0/src/crypto/hash.bend as Hc
19
20# A hash state (opaque): which hash, its chaining value, the bytes of the
21# unfinished block, and the length so far
22type CrSha2State is Data:
23 CrSha2State{h: Hc.Hasher}
24
25def CrSha2.init256() -> CrSha2State:
26 CrSha2State{Hc.new_sha256()}
27
28def CrSha2.init512() -> CrSha2State:
29 CrSha2State{Hc.new_sha512()}
30
31# the state after more bytes (either hash: the state knows which it is)
32def CrSha2.update(s: CrSha2State, o: B.Octets) -> CrSha2State:
33 match s:
34 case CrSha2State{h}:
35 CrSha2State{Hc.update(h, B.Octets.to_list(o))}
36
37# the digest of the bytes so far
38def CrSha2.final(s: CrSha2State) -> B.Octets:
39 match s:
40 case CrSha2State{h}:
41 B.Octets.of_list(Hc.digest(h))
42
43# The digests in one call
44def CrSha2.sha256(o: B.Octets) -> B.Octets:
45 B.Octets.of_list(Hc.sha256(B.Octets.to_list(o)))
46
47def CrSha2.sha512(o: B.Octets) -> B.Octets:
48 B.Octets.of_list(Hc.sha512(B.Octets.to_list(o)))