src/crypto/sha512/sha512.bend

bend-collections-laws-crypto@1.0.0.0 · 35 lines · 5 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/types.bend as T
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/core.bend as Core
4
5# SHA-512 (FIPS 180-4). Bytes are U32 values, each < 256; the digest is the
6# 64 bytes of H0..H7, most significant first. Proved equal to the executable
7# specification spec/crypto/sha512.bend for every input:
8# proofs/crypto/sha512/laws.bend.
9def sha512(bytes: List<&2, U32>) -> List<&2, U32>:
10  Core.sha512(bytes)
11
12def ascii(s: String) -> List<&2, U32>:
13  match s:
14    case SNil{}:
15      Nil{}
16    case SCon{Chr{c}, t}:
17      c <> ascii(t)
18
19def hex_digit_if(x: U32, small: Bool) -> Char:
20  match small:
21    case True{}:
22      Chr{(48 + x : U32)}
23    case False{}:
24      Chr{(87 + x : U32)}
25
26def hex_digit(+x: U32) -> Char:
27  hex_digit_if(x, U32.is_lt(x, 10))
28
29# Lowercase hex of a byte list.
30def hex(bytes: List<&2, U32>) -> String:
31  match bytes:
32    case Nil{}:
33      ""
34    case +b <> t:
35      SCon{hex_digit(U32.and(U32.shrn(b, 4n), 15)), SCon{hex_digit(U32.and(b, 15)), hex(t)}}