hashes.bend

bend-osdev-hashes@0.1.0.0 · 191 lines · 32 definitions

1# bend-osdev-hashes: the Merkle-Damgard engine every hash of this package
2# streams through, and the word types and byte orders they share.
3#
4# A hash of this shape keeps a chaining value (any type C) and compresses
5# the message a block at a time (~compress: C -> the block's bytes -> C).
6# The engine holds the bytes of the unfinished block, how many there are,
7# and how many blocks it has compressed; its update takes bytes one at a
8# time, and compresses when a block is full. Because update is a fold over
9# the bytes, feeding a ++ b is feeding a and then b, from every state
10# (LAWS.bend: md_streaming), whatever the compression function; each hash's
11# split law (streaming in any pieces equals the one-shot digest) follows.
12#
13# Each algorithm's file supplies its chaining value, compression function,
14# and final step (the padding, and the digest from the chaining value):
15#   md4.bend (RFC 1320), md5.bend (RFC 1321), sha1.bend (FIPS 180-4),
16#   ripemd160.bend (Dobbertin, Bosselaers, Preneel), sm3.bend (GB/T 32905),
17#   streebog.bend (RFC 6986), michael.bend (IEEE 802.11i's MIC).
18# The block size is a parameter (~last: the block size less one, a power of
19# two less one for HsMd.md_pad), so 64-byte blocks (all the hashes) and the
20# 4-byte words of Michael run through the same engine.
21import Base
22import bend-osdev-bytes@0.1.0.0/bytes.bend as B
23import bend-osdev-word64@0.1.0.0/word64.bend as W
24
25# The package's errors: a key of a length the algorithm does not take
26type HsError is Data:
27  HsBadKeyLength{got: Nat}
28
29# The engine's state (opaque): the chaining value, the bytes of the
30# unfinished block (last first), how many there are, and the number of
31# blocks compressed
32type HsMdState<-C: Data> is Data:
33  HsMdState{cv: C, buf: List<&2, U32>, cnt: U32, nb: W.W64}
34
35# Chaining values of two, four, five and eight 32-bit words (open types)
36type HsW2 is Data:
37  HsW2{a: U32, b: U32}
38
39type HsW4 is Data:
40  HsW4{a: U32, b: U32, c: U32, d: U32}
41
42type HsW5 is Data:
43  HsW5{a: U32, b: U32, c: U32, d: U32, e: U32}
44
45type HsW8 is Data:
46  HsW8{a: U32, b: U32, c: U32, d: U32, e: U32, f: U32, g: U32, h: U32}
47
48# The sixteen words of a 64-byte block (internal to the package)
49type HsW16 is Data:
50  HsW16{x0: U32, x1: U32, x2: U32, x3: U32, x4: U32, x5: U32, x6: U32, x7: U32, x8: U32, x9: U32, x10: U32, x11: U32, x12: U32, x13: U32, x14: U32, x15: U32}
51
52# Words, natively (bulk data: bytes' field readers are for headers)
53
54# x rotated left by n (1 to 31)
55def hs.rotl(+x: U32, +n: Nat) -> U32:
56  U32.or(U32.shln(x, n), U32.shrn(x, Nat.sub(32n, n)))
57
58# the word with bytes a (least significant), b, c, d
59def hs.le(a: U32, b: U32, c: U32, d: U32) -> U32:
60  U32.or(U32.or(a, U32.shln(b, 8n)), U32.or(U32.shln(c, 16n), U32.shln(d, 24n)))
61
62# the word with bytes a (most significant), b, c, d
63def hs.be(a: U32, b: U32, c: U32, d: U32) -> U32:
64  hs.le(d, c, b, a)
65
66# A block's sixteen words, little-endian (MD4, MD5, RIPEMD-160) or
67# big-endian (SHA-1, SM3); a block of another length gives zeros (the engine
68# passes only whole blocks)
69def hs.block.le(blk: List<&2, U32>) -> HsW16:
70  match blk:
71    case Con{b0, Con{b1, Con{b2, Con{b3, Con{b4, Con{b5, Con{b6, Con{b7, Con{b8, Con{b9, Con{b10, Con{b11, Con{b12, Con{b13, Con{b14, Con{b15, Con{b16, Con{b17, Con{b18, Con{b19, Con{b20, Con{b21, Con{b22, Con{b23, Con{b24, Con{b25, Con{b26, Con{b27, Con{b28, Con{b29, Con{b30, Con{b31, Con{b32, Con{b33, Con{b34, Con{b35, Con{b36, Con{b37, Con{b38, Con{b39, Con{b40, Con{b41, Con{b42, Con{b43, Con{b44, Con{b45, Con{b46, Con{b47, Con{b48, Con{b49, Con{b50, Con{b51, Con{b52, Con{b53, Con{b54, Con{b55, Con{b56, Con{b57, Con{b58, Con{b59, Con{b60, Con{b61, Con{b62, Con{b63, Nil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
72      HsW16{hs.le(b0, b1, b2, b3), hs.le(b4, b5, b6, b7), hs.le(b8, b9, b10, b11), hs.le(b12, b13, b14, b15), hs.le(b16, b17, b18, b19), hs.le(b20, b21, b22, b23), hs.le(b24, b25, b26, b27), hs.le(b28, b29, b30, b31), hs.le(b32, b33, b34, b35), hs.le(b36, b37, b38, b39), hs.le(b40, b41, b42, b43), hs.le(b44, b45, b46, b47), hs.le(b48, b49, b50, b51), hs.le(b52, b53, b54, b55), hs.le(b56, b57, b58, b59), hs.le(b60, b61, b62, b63)}
73    case _:
74      HsW16{0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0}
75
76def hs.block.be(blk: List<&2, U32>) -> HsW16:
77  match blk:
78    case Con{b0, Con{b1, Con{b2, Con{b3, Con{b4, Con{b5, Con{b6, Con{b7, Con{b8, Con{b9, Con{b10, Con{b11, Con{b12, Con{b13, Con{b14, Con{b15, Con{b16, Con{b17, Con{b18, Con{b19, Con{b20, Con{b21, Con{b22, Con{b23, Con{b24, Con{b25, Con{b26, Con{b27, Con{b28, Con{b29, Con{b30, Con{b31, Con{b32, Con{b33, Con{b34, Con{b35, Con{b36, Con{b37, Con{b38, Con{b39, Con{b40, Con{b41, Con{b42, Con{b43, Con{b44, Con{b45, Con{b46, Con{b47, Con{b48, Con{b49, Con{b50, Con{b51, Con{b52, Con{b53, Con{b54, Con{b55, Con{b56, Con{b57, Con{b58, Con{b59, Con{b60, Con{b61, Con{b62, Con{b63, Nil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
79      HsW16{hs.be(b0, b1, b2, b3), hs.be(b4, b5, b6, b7), hs.be(b8, b9, b10, b11), hs.be(b12, b13, b14, b15), hs.be(b16, b17, b18, b19), hs.be(b20, b21, b22, b23), hs.be(b24, b25, b26, b27), hs.be(b28, b29, b30, b31), hs.be(b32, b33, b34, b35), hs.be(b36, b37, b38, b39), hs.be(b40, b41, b42, b43), hs.be(b44, b45, b46, b47), hs.be(b48, b49, b50, b51), hs.be(b52, b53, b54, b55), hs.be(b56, b57, b58, b59), hs.be(b60, b61, b62, b63)}
80    case _:
81      HsW16{0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0}
82
83# The digest bytes of a chaining value: each word little-endian (MD4, MD5,
84# RIPEMD-160, Michael) or big-endian (SHA-1, SM3), in order
85
86def HsW2.le(x: HsW2) -> B.Octets:
87  match x:
88    case HsW2{a, b}:
89      B.Octets.of_list(B.append(B.le32(a), B.le32(b)))
90
91def HsW4.le(x: HsW4) -> B.Octets:
92  match x:
93    case HsW4{a, b, c, d}:
94      B.Octets.of_list(B.append(B.le32(a), B.append(B.le32(b), B.append(B.le32(c), B.le32(d)))))
95
96def HsW5.le(x: HsW5) -> B.Octets:
97  match x:
98    case HsW5{a, b, c, d, e}:
99      B.Octets.of_list(B.append(B.le32(a), B.append(B.le32(b), B.append(B.le32(c), B.append(B.le32(d), B.le32(e))))))
100
101def HsW5.be(x: HsW5) -> B.Octets:
102  match x:
103    case HsW5{a, b, c, d, e}:
104      B.Octets.of_list(B.append(B.be32(a), B.append(B.be32(b), B.append(B.be32(c), B.append(B.be32(d), B.be32(e))))))
105
106def HsW8.be(x: HsW8) -> B.Octets:
107  match x:
108    case HsW8{a, b, c, d, e, f, g, h}:
109      B.Octets.of_list(B.append(B.be32(a), B.append(B.be32(b), B.append(B.be32(c), B.append(B.be32(d), B.append(B.be32(e), B.append(B.be32(f), B.append(B.be32(g), B.be32(h)))))))))
110
111# The engine
112
113# the state before any byte, from the initial chaining value
114def HsMd.start(~C: Data, cv: C) -> HsMdState<C>:
115  HsMdState{cv, Nil{}, 0, W.W64.zero()}
116
117def hs.md.push(~C: Data, ~compress: C -> List<&2, U32> -> C, full: Bool, cv: C, buf: List<&2, U32>, cnt: U32, nb: W.W64) -> HsMdState<C>:
118  match full:
119    case True{}:
120      HsMdState{compress(cv, B.rev(buf)), Nil{}, 0, W.W64.add(nb, W.W64.one())}
121    case False{}:
122      HsMdState{cv, buf, U32.add(cnt, 1), nb}
123
124# one byte in: a block of last + 1 bytes is compressed when it is full
125def hs.md.step(~C: Data, ~compress: C -> List<&2, U32> -> C, ~last: U32, s: HsMdState<C>, b: U32) -> HsMdState<C>:
126  match s:
127    case HsMdState{cv, buf, +cnt, nb}:
128      hs.md.push(~C, ~compress, U32.is_eq(cnt, last), cv, Con{b, buf}, cnt, nb)
129
130def hs.md.feed(~C: Data, ~compress: C -> List<&2, U32> -> C, ~last: U32, xs: List<&2, U32>, s: HsMdState<C>) -> HsMdState<C>:
131  match xs:
132    case Nil{}:
133      s
134    case Con{x, t}:
135      hs.md.feed(~C, ~compress, ~last, t, hs.md.step(~C, ~compress, ~last, s, x))
136
137# the state after more bytes
138def HsMd.update(~C: Data, ~compress: C -> List<&2, U32> -> C, ~last: U32, s: HsMdState<C>, o: B.Octets) -> HsMdState<C>:
139  hs.md.feed(~C, ~compress, ~last, B.Octets.to_list(o), s)
140
141# the same, for bytes as a list (each element is taken as it is: callers
142# pass bytes)
143def HsMd.update_list(~C: Data, ~compress: C -> List<&2, U32> -> C, ~last: U32, s: HsMdState<C>, xs: List<&2, U32>) -> HsMdState<C>:
144  hs.md.feed(~C, ~compress, ~last, xs, s)
145
146# The state's parts: the chaining value, the bytes of the unfinished block
147# (first first), how many there are, and the number of blocks compressed
148def HsMd.cv(~C: Data, s: HsMdState<C>) -> C:
149  match s:
150    case HsMdState{cv, buf, cnt, nb}:
151      cv
152
153def HsMd.pending(~C: Data, s: HsMdState<C>) -> List<&2, U32>:
154  match s:
155    case HsMdState{cv, buf, cnt, nb}:
156      B.rev(buf)
157
158def HsMd.count(~C: Data, s: HsMdState<C>) -> U32:
159  match s:
160    case HsMdState{cv, buf, cnt, nb}:
161      cnt
162
163def HsMd.blocks(~C: Data, s: HsMdState<C>) -> W.W64:
164  match s:
165    case HsMdState{cv, buf, cnt, nb}:
166      nb
167
168# The length so far in bits, modulo 2^64 (blocks of last + 1 bytes)
169def HsMd.bits(~C: Data, ~last: U32, +s: HsMdState<C>) -> W.W64:
170  W.W64.add(W.W64.mul(HsMd.blocks(~C, s), W.W64.from_u32(U32.shln(U32.add(last, 1), 3n))), W.W64.from_u32(U32.shln(HsMd.count(~C, s), 3n)))
171
172# The length field: eight bytes, little-endian (MD4, MD5, RIPEMD-160) or
173# big-endian (SHA-1, SM3)
174def hs.len.le(v: W.W64) -> List<&2, U32>:
175  B.le64(v)
176
177def hs.len.be(v: W.W64) -> List<&2, U32>:
178  B.be64(v)
179
180# The Merkle-Damgard padding after cnt bytes of an unfinished block: the
181# byte 0x80, zeros, then the length field, so that the whole is a number of
182# blocks (the block size last + 1 a power of two)
183def HsMd.md_pad(~last: U32, +cnt: U32, +field: List<&2, U32>) -> List<&2, U32>:
184  +k = U32.and(U32.sub(U32.sub(last, U32.from_nat(B.len(field))), cnt), last)
185  Con{128, B.append(B.zeros(U32.to_nat(k)), field)}
186
187# The final step of a Merkle-Damgard hash: the padding with the length in
188# bits (~field writes it: eight bytes, little- or big-endian), through the
189# engine, then the digest of the chaining value (~out)
190def HsMd.final_md(~C: Data, ~compress: C -> List<&2, U32> -> C, ~last: U32, ~field: W.W64 -> List<&2, U32>, ~out: C -> B.Octets, +s: HsMdState<C>) -> B.Octets:
191  out(HsMd.cv(~C, hs.md.feed(~C, ~compress, ~last, HsMd.md_pad(~last, HsMd.count(~C, s), field(HsMd.bits(~C, ~last, s))), s)))