md5.bend

bend-osdev-hashes@0.1.0.0 · 129 lines · 12 definitions

1# MD5 (RFC 1321, R. Rivest, "The MD5 Message-Digest Algorithm", 1992): a
2# 128-bit digest of 64-byte blocks, four rounds of sixteen steps (the table
3# T[i] = floor(2^32 abs(sin i)), the shifts and the word order of section
4# 3.4, unrolled by gen/rounds.py). Little-endian words; the length in bits
5# is padded in little-endian. MD5 is broken for collisions: use it for
6# checksums and the formats that require it, not for security.
7#
8# The hash, as the crypto package's hash interface takes it:
9#   ~Hs.HsMdState<Hs.HsW4>, ~64n, ~16n, ~HsMd5.init(), ~HsMd5.update,
10#   ~HsMd5.final, ~HsMd5.digest
11import Base
12import bend-osdev-bytes@0.1.0.0/bytes.bend as B
13import bend-osdev-hashes@0.1.0.0/hashes.bend as Hs
14
15# the auxiliary functions F, G, H and I (section 3.4)
16def hs.md5.f(+x: U32, y: U32, z: U32) -> U32:
17  U32.or(U32.and(x, y), U32.and(U32.not(x), z))
18
19def hs.md5.g(x: U32, y: U32, +z: U32) -> U32:
20  U32.or(U32.and(x, z), U32.and(y, U32.not(z)))
21
22def hs.md5.h(x: U32, y: U32, z: U32) -> U32:
23  U32.xor(U32.xor(x, y), z)
24
25def hs.md5.i(x: U32, y: U32, z: U32) -> U32:
26  U32.xor(y, U32.or(x, U32.not(z)))
27
28# one step: b + ((a + f + X[k] + T[i]) <<< s)
29def hs.md5.step(a: U32, b: U32, f: U32, x: U32, t: U32, +s: Nat) -> U32:
30  U32.add(b, Hs.hs.rotl(U32.add(U32.add(a, f), U32.add(x, t)), s))
31
32# BEGIN GENERATED by gen/rounds.py: md5
33def hs.md5.rounds(x: Hs.HsW16, cv: Hs.HsW4) -> Hs.HsW4:
34  match x cv:
35    case Hs.HsW16{+x0, +x1, +x2, +x3, +x4, +x5, +x6, +x7, +x8, +x9, +x10, +x11, +x12, +x13, +x14, +x15} Hs.HsW4{+a0, +b0, +c0, +d0}:
36      # round 1
37      +v1 = hs.md5.step(a0, b0, hs.md5.f(b0, c0, d0), x0, 3614090360, 7n)
38      +v2 = hs.md5.step(d0, v1, hs.md5.f(v1, b0, c0), x1, 3905402710, 12n)
39      +v3 = hs.md5.step(c0, v2, hs.md5.f(v2, v1, b0), x2, 606105819, 17n)
40      +v4 = hs.md5.step(b0, v3, hs.md5.f(v3, v2, v1), x3, 3250441966, 22n)
41      +v5 = hs.md5.step(v1, v4, hs.md5.f(v4, v3, v2), x4, 4118548399, 7n)
42      +v6 = hs.md5.step(v2, v5, hs.md5.f(v5, v4, v3), x5, 1200080426, 12n)
43      +v7 = hs.md5.step(v3, v6, hs.md5.f(v6, v5, v4), x6, 2821735955, 17n)
44      +v8 = hs.md5.step(v4, v7, hs.md5.f(v7, v6, v5), x7, 4249261313, 22n)
45      +v9 = hs.md5.step(v5, v8, hs.md5.f(v8, v7, v6), x8, 1770035416, 7n)
46      +v10 = hs.md5.step(v6, v9, hs.md5.f(v9, v8, v7), x9, 2336552879, 12n)
47      +v11 = hs.md5.step(v7, v10, hs.md5.f(v10, v9, v8), x10, 4294925233, 17n)
48      +v12 = hs.md5.step(v8, v11, hs.md5.f(v11, v10, v9), x11, 2304563134, 22n)
49      +v13 = hs.md5.step(v9, v12, hs.md5.f(v12, v11, v10), x12, 1804603682, 7n)
50      +v14 = hs.md5.step(v10, v13, hs.md5.f(v13, v12, v11), x13, 4254626195, 12n)
51      +v15 = hs.md5.step(v11, v14, hs.md5.f(v14, v13, v12), x14, 2792965006, 17n)
52      +v16 = hs.md5.step(v12, v15, hs.md5.f(v15, v14, v13), x15, 1236535329, 22n)
53      # round 2
54      +v17 = hs.md5.step(v13, v16, hs.md5.g(v16, v15, v14), x1, 4129170786, 5n)
55      +v18 = hs.md5.step(v14, v17, hs.md5.g(v17, v16, v15), x6, 3225465664, 9n)
56      +v19 = hs.md5.step(v15, v18, hs.md5.g(v18, v17, v16), x11, 643717713, 14n)
57      +v20 = hs.md5.step(v16, v19, hs.md5.g(v19, v18, v17), x0, 3921069994, 20n)
58      +v21 = hs.md5.step(v17, v20, hs.md5.g(v20, v19, v18), x5, 3593408605, 5n)
59      +v22 = hs.md5.step(v18, v21, hs.md5.g(v21, v20, v19), x10, 38016083, 9n)
60      +v23 = hs.md5.step(v19, v22, hs.md5.g(v22, v21, v20), x15, 3634488961, 14n)
61      +v24 = hs.md5.step(v20, v23, hs.md5.g(v23, v22, v21), x4, 3889429448, 20n)
62      +v25 = hs.md5.step(v21, v24, hs.md5.g(v24, v23, v22), x9, 568446438, 5n)
63      +v26 = hs.md5.step(v22, v25, hs.md5.g(v25, v24, v23), x14, 3275163606, 9n)
64      +v27 = hs.md5.step(v23, v26, hs.md5.g(v26, v25, v24), x3, 4107603335, 14n)
65      +v28 = hs.md5.step(v24, v27, hs.md5.g(v27, v26, v25), x8, 1163531501, 20n)
66      +v29 = hs.md5.step(v25, v28, hs.md5.g(v28, v27, v26), x13, 2850285829, 5n)
67      +v30 = hs.md5.step(v26, v29, hs.md5.g(v29, v28, v27), x2, 4243563512, 9n)
68      +v31 = hs.md5.step(v27, v30, hs.md5.g(v30, v29, v28), x7, 1735328473, 14n)
69      +v32 = hs.md5.step(v28, v31, hs.md5.g(v31, v30, v29), x12, 2368359562, 20n)
70      # round 3
71      +v33 = hs.md5.step(v29, v32, hs.md5.h(v32, v31, v30), x5, 4294588738, 4n)
72      +v34 = hs.md5.step(v30, v33, hs.md5.h(v33, v32, v31), x8, 2272392833, 11n)
73      +v35 = hs.md5.step(v31, v34, hs.md5.h(v34, v33, v32), x11, 1839030562, 16n)
74      +v36 = hs.md5.step(v32, v35, hs.md5.h(v35, v34, v33), x14, 4259657740, 23n)
75      +v37 = hs.md5.step(v33, v36, hs.md5.h(v36, v35, v34), x1, 2763975236, 4n)
76      +v38 = hs.md5.step(v34, v37, hs.md5.h(v37, v36, v35), x4, 1272893353, 11n)
77      +v39 = hs.md5.step(v35, v38, hs.md5.h(v38, v37, v36), x7, 4139469664, 16n)
78      +v40 = hs.md5.step(v36, v39, hs.md5.h(v39, v38, v37), x10, 3200236656, 23n)
79      +v41 = hs.md5.step(v37, v40, hs.md5.h(v40, v39, v38), x13, 681279174, 4n)
80      +v42 = hs.md5.step(v38, v41, hs.md5.h(v41, v40, v39), x0, 3936430074, 11n)
81      +v43 = hs.md5.step(v39, v42, hs.md5.h(v42, v41, v40), x3, 3572445317, 16n)
82      +v44 = hs.md5.step(v40, v43, hs.md5.h(v43, v42, v41), x6, 76029189, 23n)
83      +v45 = hs.md5.step(v41, v44, hs.md5.h(v44, v43, v42), x9, 3654602809, 4n)
84      +v46 = hs.md5.step(v42, v45, hs.md5.h(v45, v44, v43), x12, 3873151461, 11n)
85      +v47 = hs.md5.step(v43, v46, hs.md5.h(v46, v45, v44), x15, 530742520, 16n)
86      +v48 = hs.md5.step(v44, v47, hs.md5.h(v47, v46, v45), x2, 3299628645, 23n)
87      # round 4
88      +v49 = hs.md5.step(v45, v48, hs.md5.i(v48, v47, v46), x0, 4096336452, 6n)
89      +v50 = hs.md5.step(v46, v49, hs.md5.i(v49, v48, v47), x7, 1126891415, 10n)
90      +v51 = hs.md5.step(v47, v50, hs.md5.i(v50, v49, v48), x14, 2878612391, 15n)
91      +v52 = hs.md5.step(v48, v51, hs.md5.i(v51, v50, v49), x5, 4237533241, 21n)
92      +v53 = hs.md5.step(v49, v52, hs.md5.i(v52, v51, v50), x12, 1700485571, 6n)
93      +v54 = hs.md5.step(v50, v53, hs.md5.i(v53, v52, v51), x3, 2399980690, 10n)
94      +v55 = hs.md5.step(v51, v54, hs.md5.i(v54, v53, v52), x10, 4293915773, 15n)
95      +v56 = hs.md5.step(v52, v55, hs.md5.i(v55, v54, v53), x1, 2240044497, 21n)
96      +v57 = hs.md5.step(v53, v56, hs.md5.i(v56, v55, v54), x8, 1873313359, 6n)
97      +v58 = hs.md5.step(v54, v57, hs.md5.i(v57, v56, v55), x15, 4264355552, 10n)
98      +v59 = hs.md5.step(v55, v58, hs.md5.i(v58, v57, v56), x6, 2734768916, 15n)
99      +v60 = hs.md5.step(v56, v59, hs.md5.i(v59, v58, v57), x13, 1309151649, 21n)
100      +v61 = hs.md5.step(v57, v60, hs.md5.i(v60, v59, v58), x4, 4149444226, 6n)
101      +v62 = hs.md5.step(v58, v61, hs.md5.i(v61, v60, v59), x11, 3174756917, 10n)
102      +v63 = hs.md5.step(v59, v62, hs.md5.i(v62, v61, v60), x2, 718787259, 15n)
103      +v64 = hs.md5.step(v60, v63, hs.md5.i(v63, v62, v61), x9, 3951481745, 21n)
104      Hs.HsW4{U32.add(a0, v61), U32.add(b0, v64), U32.add(c0, v63), U32.add(d0, v62)}
105# END GENERATED: md5
106
107# The chaining value before any block (section 3.3)
108def HsMd5.iv() -> Hs.HsW4:
109  Hs.HsW4{1732584193, 4023233417, 2562383102, 271733878}
110
111# One 64-byte block (a list of another length is read as zero words: the
112# engine passes only whole blocks)
113def HsMd5.compress(cv: Hs.HsW4, blk: List<&2, U32>) -> Hs.HsW4:
114  hs.md5.rounds(Hs.hs.block.le(blk), cv)
115
116def HsMd5.init() -> Hs.HsMdState<Hs.HsW4>:
117  Hs.HsMd.start(~Hs.HsW4, HsMd5.iv())
118
119def HsMd5.update(s: Hs.HsMdState<Hs.HsW4>, o: B.Octets) -> Hs.HsMdState<Hs.HsW4>:
120  Hs.HsMd.update(~Hs.HsW4, ~HsMd5.compress, ~63, s, o)
121
122# the digest of the bytes so far: the padding and the length, then the four
123# words little-endian
124def HsMd5.final(s: Hs.HsMdState<Hs.HsW4>) -> B.Octets:
125  Hs.HsMd.final_md(~Hs.HsW4, ~HsMd5.compress, ~63, ~Hs.hs.len.le, ~Hs.HsW4.le, s)
126
127# The digest in one call
128def HsMd5.digest(o: B.Octets) -> B.Octets:
129  HsMd5.final(HsMd5.update(HsMd5.init(), o))