PROOF.bend
bend-osdev-hashes@0.1.0.0 · 368 lines · 17 definitions
1
2import Base
3import bend-osdev-bytes@0.1.0.0/bytes.bend as B
4import bend-osdev-hashes@0.1.0.0/hashes.bend as Hs
5import bend-osdev-hashes@0.1.0.0/md4.bend as M4
6import bend-osdev-hashes@0.1.0.0/md5.bend as M5
7import bend-osdev-hashes@0.1.0.0/sha1.bend as S1
8import bend-osdev-hashes@0.1.0.0/ripemd160.bend as RM
9import bend-osdev-hashes@0.1.0.0/sm3.bend as SM
10import bend-osdev-hashes@0.1.0.0/streebog.bend as ST
11import bend-osdev-hashes@0.1.0.0/michael.bend as MI
12import bend-osdev-bytes@0.1.0.0/LAWS.bend as BL
13import bend-osdev-bytes@0.1.0.0/PROOF.bend as BP
14import bend-osdev-hashes@0.1.0.0/LAWS.bend as Laws
15
16
17def feed_append(~C: Data, ~compress: C -> List<&2, U32> -> C, ~last: U32, xs: List<&2, U32>, +ys: List<&2, U32>, s: Hs.HsMdState<C>) -> {Hs.hs.md.feed(~C, ~compress, ~last, B.append(xs, ys), s) == Hs.hs.md.feed(~C, ~compress, ~last, ys, Hs.hs.md.feed(~C, ~compress, ~last, xs, s)) : Hs.HsMdState<C>}:
18 match xs:
19 case Nil{}:
20 {==}
21 case Con{x, t}:
22 feed_append(~C, ~compress, ~last, t, ys, Hs.hs.md.step(~C, ~compress, ~last, s, x))
23
24def Laws.md_streaming(C, compress, last, s, a, b):
25 %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.append(a, b)), B.append(B.Octets.to_list(a), B.Octets.to_list(b)), BL.octets_append_list(a, b)) : {Hs.hs.md.feed(~C, ~compress, ~last, _, s) == Hs.HsMd.update(~C, ~compress, ~last, Hs.HsMd.update(~C, ~compress, ~last, s, a), b) : Hs.HsMdState<C>}
26 feed_append(~C, ~compress, ~last, B.Octets.to_list(a), B.Octets.to_list(b), s)
27
28
29
30def mask_len(xs: List<&2, U32>) -> {B.len(B.mask(xs)) == B.len(xs) : Nat}:
31 match xs:
32 case Nil{}:
33 {==}
34 case Con{h, t}:
35 %mask_len(t) : {B.len(B.mask(Con{h, t})) == 1n+_ : Nat}
36 {==}
37
38def octets_len_of(+xs: List<&2, U32>) -> {B.Octets.len(B.Octets.of_list(xs)) == B.len(xs) : Nat}:
39 %Equal.sym(Nat, B.Octets.len(B.Octets.of_list(xs)), B.len(B.Octets.to_list(B.Octets.of_list(xs))), BL.octets_len_list(B.Octets.of_list(xs))) : {_ == B.len(xs) : Nat}
40 %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.of_list(xs)), B.mask(xs), BL.octets_to_of(xs)) : {B.len(_) == B.len(xs) : Nat}
41 mask_len(xs)
42
43def w2le_len_list(a0: U32, a1: U32) -> {B.len(B.append(B.le32(a0), B.le32(a1))) == 8n : Nat}:
44 match a0 a1:
45 case U32{wa0} U32{wa1}:
46 {==}
47
48def w2le_len(x: Hs.HsW2) -> {B.Octets.len(Hs.HsW2.le(x)) == 8n : Nat}:
49 match x:
50 case Hs.HsW2{+a0, +a1}:
51 %Equal.sym(Nat, B.Octets.len(B.Octets.of_list(B.append(B.le32(a0), B.le32(a1)))), B.len(B.append(B.le32(a0), B.le32(a1))), octets_len_of(B.append(B.le32(a0), B.le32(a1)))) : {_ == 8n : Nat}
52 w2le_len_list(a0, a1)
53
54def w4le_len_list(a0: U32, a1: U32, a2: U32, a3: U32) -> {B.len(B.append(B.le32(a0), B.append(B.le32(a1), B.append(B.le32(a2), B.le32(a3))))) == 16n : Nat}:
55 match a0 a1 a2 a3:
56 case U32{wa0} U32{wa1} U32{wa2} U32{wa3}:
57 {==}
58
59def w4le_len(x: Hs.HsW4) -> {B.Octets.len(Hs.HsW4.le(x)) == 16n : Nat}:
60 match x:
61 case Hs.HsW4{+a0, +a1, +a2, +a3}:
62 %Equal.sym(Nat, B.Octets.len(B.Octets.of_list(B.append(B.le32(a0), B.append(B.le32(a1), B.append(B.le32(a2), B.le32(a3)))))), B.len(B.append(B.le32(a0), B.append(B.le32(a1), B.append(B.le32(a2), B.le32(a3))))), octets_len_of(B.append(B.le32(a0), B.append(B.le32(a1), B.append(B.le32(a2), B.le32(a3)))))) : {_ == 16n : Nat}
63 w4le_len_list(a0, a1, a2, a3)
64
65def w5le_len_list(a0: U32, a1: U32, a2: U32, a3: U32, a4: U32) -> {B.len(B.append(B.le32(a0), B.append(B.le32(a1), B.append(B.le32(a2), B.append(B.le32(a3), B.le32(a4)))))) == 20n : Nat}:
66 match a0 a1 a2 a3 a4:
67 case U32{wa0} U32{wa1} U32{wa2} U32{wa3} U32{wa4}:
68 {==}
69
70def w5le_len(x: Hs.HsW5) -> {B.Octets.len(Hs.HsW5.le(x)) == 20n : Nat}:
71 match x:
72 case Hs.HsW5{+a0, +a1, +a2, +a3, +a4}:
73 %Equal.sym(Nat, B.Octets.len(B.Octets.of_list(B.append(B.le32(a0), B.append(B.le32(a1), B.append(B.le32(a2), B.append(B.le32(a3), B.le32(a4))))))), B.len(B.append(B.le32(a0), B.append(B.le32(a1), B.append(B.le32(a2), B.append(B.le32(a3), B.le32(a4)))))), octets_len_of(B.append(B.le32(a0), B.append(B.le32(a1), B.append(B.le32(a2), B.append(B.le32(a3), B.le32(a4))))))) : {_ == 20n : Nat}
74 w5le_len_list(a0, a1, a2, a3, a4)
75
76def w5be_len_list(a0: U32, a1: U32, a2: U32, a3: U32, a4: U32) -> {B.len(B.append(B.be32(a0), B.append(B.be32(a1), B.append(B.be32(a2), B.append(B.be32(a3), B.be32(a4)))))) == 20n : Nat}:
77 match a0 a1 a2 a3 a4:
78 case U32{wa0} U32{wa1} U32{wa2} U32{wa3} U32{wa4}:
79 {==}
80
81def w5be_len(x: Hs.HsW5) -> {B.Octets.len(Hs.HsW5.be(x)) == 20n : Nat}:
82 match x:
83 case Hs.HsW5{+a0, +a1, +a2, +a3, +a4}:
84 %Equal.sym(Nat, B.Octets.len(B.Octets.of_list(B.append(B.be32(a0), B.append(B.be32(a1), B.append(B.be32(a2), B.append(B.be32(a3), B.be32(a4))))))), B.len(B.append(B.be32(a0), B.append(B.be32(a1), B.append(B.be32(a2), B.append(B.be32(a3), B.be32(a4)))))), octets_len_of(B.append(B.be32(a0), B.append(B.be32(a1), B.append(B.be32(a2), B.append(B.be32(a3), B.be32(a4))))))) : {_ == 20n : Nat}
85 w5be_len_list(a0, a1, a2, a3, a4)
86
87def w8be_len_list(a0: U32, a1: U32, a2: U32, a3: U32, a4: U32, a5: U32, a6: U32, a7: U32) -> {B.len(B.append(B.be32(a0), B.append(B.be32(a1), B.append(B.be32(a2), B.append(B.be32(a3), B.append(B.be32(a4), B.append(B.be32(a5), B.append(B.be32(a6), B.be32(a7))))))))) == 32n : Nat}:
88 match a0 a1 a2 a3 a4 a5 a6 a7:
89 case U32{wa0} U32{wa1} U32{wa2} U32{wa3} U32{wa4} U32{wa5} U32{wa6} U32{wa7}:
90 {==}
91
92def w8be_len(x: Hs.HsW8) -> {B.Octets.len(Hs.HsW8.be(x)) == 32n : Nat}:
93 match x:
94 case Hs.HsW8{+a0, +a1, +a2, +a3, +a4, +a5, +a6, +a7}:
95 %Equal.sym(Nat, B.Octets.len(B.Octets.of_list(B.append(B.be32(a0), B.append(B.be32(a1), B.append(B.be32(a2), B.append(B.be32(a3), B.append(B.be32(a4), B.append(B.be32(a5), B.append(B.be32(a6), B.be32(a7)))))))))), B.len(B.append(B.be32(a0), B.append(B.be32(a1), B.append(B.be32(a2), B.append(B.be32(a3), B.append(B.be32(a4), B.append(B.be32(a5), B.append(B.be32(a6), B.be32(a7))))))))), octets_len_of(B.append(B.be32(a0), B.append(B.be32(a1), B.append(B.be32(a2), B.append(B.be32(a3), B.append(B.be32(a4), B.append(B.be32(a5), B.append(B.be32(a6), B.be32(a7)))))))))) : {_ == 32n : Nat}
96 w8be_len_list(a0, a1, a2, a3, a4, a5, a6, a7)
97
98def stb512_len_list(a0: U32, a1: U32, a2: U32, a3: U32, a4: U32, a5: U32, a6: U32, a7: U32, a8: U32, a9: U32, a10: U32, a11: U32, a12: U32, a13: U32, a14: U32, a15: U32) -> {B.len(B.append(B.le32(a0), B.append(B.le32(a1), B.append(B.le32(a2), B.append(B.le32(a3), B.append(B.le32(a4), B.append(B.le32(a5), B.append(B.le32(a6), B.append(B.le32(a7), B.append(B.le32(a8), B.append(B.le32(a9), B.append(B.le32(a10), B.append(B.le32(a11), B.append(B.le32(a12), B.append(B.le32(a13), B.append(B.le32(a14), B.le32(a15))))))))))))))))) == 64n : Nat}:
99 match a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15:
100 case U32{wa0} U32{wa1} U32{wa2} U32{wa3} U32{wa4} U32{wa5} U32{wa6} U32{wa7} U32{wa8} U32{wa9} U32{wa10} U32{wa11} U32{wa12} U32{wa13} U32{wa14} U32{wa15}:
101 {==}
102
103def stb512_len(x: Hs.HsW16) -> {B.Octets.len(ST.hs.stb.out512(x)) == 64n : Nat}:
104 match x:
105 case Hs.HsW16{+a0, +a1, +a2, +a3, +a4, +a5, +a6, +a7, +a8, +a9, +a10, +a11, +a12, +a13, +a14, +a15}:
106 %Equal.sym(Nat, B.Octets.len(B.Octets.of_list(B.append(B.le32(a0), B.append(B.le32(a1), B.append(B.le32(a2), B.append(B.le32(a3), B.append(B.le32(a4), B.append(B.le32(a5), B.append(B.le32(a6), B.append(B.le32(a7), B.append(B.le32(a8), B.append(B.le32(a9), B.append(B.le32(a10), B.append(B.le32(a11), B.append(B.le32(a12), B.append(B.le32(a13), B.append(B.le32(a14), B.le32(a15)))))))))))))))))), B.len(B.append(B.le32(a0), B.append(B.le32(a1), B.append(B.le32(a2), B.append(B.le32(a3), B.append(B.le32(a4), B.append(B.le32(a5), B.append(B.le32(a6), B.append(B.le32(a7), B.append(B.le32(a8), B.append(B.le32(a9), B.append(B.le32(a10), B.append(B.le32(a11), B.append(B.le32(a12), B.append(B.le32(a13), B.append(B.le32(a14), B.le32(a15))))))))))))))))), octets_len_of(B.append(B.le32(a0), B.append(B.le32(a1), B.append(B.le32(a2), B.append(B.le32(a3), B.append(B.le32(a4), B.append(B.le32(a5), B.append(B.le32(a6), B.append(B.le32(a7), B.append(B.le32(a8), B.append(B.le32(a9), B.append(B.le32(a10), B.append(B.le32(a11), B.append(B.le32(a12), B.append(B.le32(a13), B.append(B.le32(a14), B.le32(a15)))))))))))))))))) : {_ == 64n : Nat}
107 stb512_len_list(a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15)
108
109def stb256_len_list(a8: U32, a9: U32, a10: U32, a11: U32, a12: U32, a13: U32, a14: U32, a15: U32) -> {B.len(B.append(B.le32(a8), B.append(B.le32(a9), B.append(B.le32(a10), B.append(B.le32(a11), B.append(B.le32(a12), B.append(B.le32(a13), B.append(B.le32(a14), B.le32(a15))))))))) == 32n : Nat}:
110 match a8 a9 a10 a11 a12 a13 a14 a15:
111 case U32{wa8} U32{wa9} U32{wa10} U32{wa11} U32{wa12} U32{wa13} U32{wa14} U32{wa15}:
112 {==}
113
114def stb256_len(x: Hs.HsW16) -> {B.Octets.len(ST.hs.stb.out256(x)) == 32n : Nat}:
115 match x:
116 case Hs.HsW16{a0, a1, a2, a3, a4, a5, a6, a7, +a8, +a9, +a10, +a11, +a12, +a13, +a14, +a15}:
117 %Equal.sym(Nat, B.Octets.len(B.Octets.of_list(B.append(B.le32(a8), B.append(B.le32(a9), B.append(B.le32(a10), B.append(B.le32(a11), B.append(B.le32(a12), B.append(B.le32(a13), B.append(B.le32(a14), B.le32(a15)))))))))), B.len(B.append(B.le32(a8), B.append(B.le32(a9), B.append(B.le32(a10), B.append(B.le32(a11), B.append(B.le32(a12), B.append(B.le32(a13), B.append(B.le32(a14), B.le32(a15))))))))), octets_len_of(B.append(B.le32(a8), B.append(B.le32(a9), B.append(B.le32(a10), B.append(B.le32(a11), B.append(B.le32(a12), B.append(B.le32(a13), B.append(B.le32(a14), B.le32(a15)))))))))) : {_ == 32n : Nat}
118 stb256_len_list(a8, a9, a10, a11, a12, a13, a14, a15)
119
120def Laws.md4_streaming(s, a, b):
121 Laws.md_streaming(~Hs.HsW4, ~M4.HsMd4.compress, ~63, s, a, b)
122
123def Laws.md4_split(a, b):
124 %Laws.md4_streaming(M4.HsMd4.init(), a, b) : {M4.HsMd4.final(_) == M4.HsMd4.digest(B.Octets.append(a, b)) : B.Octets}
125 {==}
126
127def Laws.md4_split3(a, b, c):
128 %Laws.md4_streaming(M4.HsMd4.update(M4.HsMd4.init(), a), b, c) : {M4.HsMd4.final(_) == M4.HsMd4.digest(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
129 %Laws.md4_streaming(M4.HsMd4.init(), a, B.Octets.append(b, c)) : {M4.HsMd4.final(_) == M4.HsMd4.digest(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
130 {==}
131
132def Laws.md4_length(s):
133 w4le_len(Hs.HsMd.cv(~Hs.HsW4, Hs.hs.md.feed(~Hs.HsW4, ~M4.HsMd4.compress, ~63, Hs.HsMd.md_pad(~63, Hs.HsMd.count(~Hs.HsW4, s), Hs.hs.len.le(Hs.HsMd.bits(~Hs.HsW4, ~63, s))), s)))
134
135def Laws.md4_digest_length(m):
136 Laws.md4_length(M4.HsMd4.update(M4.HsMd4.init(), m))
137
138def Laws.md4_rfc1320_1():
139 {==}
140
141def Laws.md4_rfc1320_2():
142 {==}
143
144def Laws.md4_rfc1320_3():
145 {==}
146
147def Laws.md4_rfc1320_4():
148 {==}
149
150def Laws.md4_rfc1320_5():
151 {==}
152
153def Laws.md4_rfc1320_6():
154 {==}
155
156def Laws.md4_rfc1320_7():
157 {==}
158
159def Laws.md5_streaming(s, a, b):
160 Laws.md_streaming(~Hs.HsW4, ~M5.HsMd5.compress, ~63, s, a, b)
161
162def Laws.md5_split(a, b):
163 %Laws.md5_streaming(M5.HsMd5.init(), a, b) : {M5.HsMd5.final(_) == M5.HsMd5.digest(B.Octets.append(a, b)) : B.Octets}
164 {==}
165
166def Laws.md5_split3(a, b, c):
167 %Laws.md5_streaming(M5.HsMd5.update(M5.HsMd5.init(), a), b, c) : {M5.HsMd5.final(_) == M5.HsMd5.digest(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
168 %Laws.md5_streaming(M5.HsMd5.init(), a, B.Octets.append(b, c)) : {M5.HsMd5.final(_) == M5.HsMd5.digest(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
169 {==}
170
171def Laws.md5_length(s):
172 w4le_len(Hs.HsMd.cv(~Hs.HsW4, Hs.hs.md.feed(~Hs.HsW4, ~M5.HsMd5.compress, ~63, Hs.HsMd.md_pad(~63, Hs.HsMd.count(~Hs.HsW4, s), Hs.hs.len.le(Hs.HsMd.bits(~Hs.HsW4, ~63, s))), s)))
173
174def Laws.md5_digest_length(m):
175 Laws.md5_length(M5.HsMd5.update(M5.HsMd5.init(), m))
176
177def Laws.md5_rfc1321_1():
178 {==}
179
180def Laws.md5_rfc1321_2():
181 {==}
182
183def Laws.md5_rfc1321_3():
184 {==}
185
186def Laws.md5_rfc1321_4():
187 {==}
188
189def Laws.md5_rfc1321_5():
190 {==}
191
192def Laws.md5_rfc1321_6():
193 {==}
194
195def Laws.md5_rfc1321_7():
196 {==}
197
198def Laws.sha1_streaming(s, a, b):
199 Laws.md_streaming(~Hs.HsW5, ~S1.HsSha1.compress, ~63, s, a, b)
200
201def Laws.sha1_split(a, b):
202 %Laws.sha1_streaming(S1.HsSha1.init(), a, b) : {S1.HsSha1.final(_) == S1.HsSha1.digest(B.Octets.append(a, b)) : B.Octets}
203 {==}
204
205def Laws.sha1_split3(a, b, c):
206 %Laws.sha1_streaming(S1.HsSha1.update(S1.HsSha1.init(), a), b, c) : {S1.HsSha1.final(_) == S1.HsSha1.digest(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
207 %Laws.sha1_streaming(S1.HsSha1.init(), a, B.Octets.append(b, c)) : {S1.HsSha1.final(_) == S1.HsSha1.digest(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
208 {==}
209
210def Laws.sha1_length(s):
211 w5be_len(Hs.HsMd.cv(~Hs.HsW5, Hs.hs.md.feed(~Hs.HsW5, ~S1.HsSha1.compress, ~63, Hs.HsMd.md_pad(~63, Hs.HsMd.count(~Hs.HsW5, s), Hs.hs.len.be(Hs.HsMd.bits(~Hs.HsW5, ~63, s))), s)))
212
213def Laws.sha1_digest_length(m):
214 Laws.sha1_length(S1.HsSha1.update(S1.HsSha1.init(), m))
215
216def Laws.sha1_fips_1():
217 {==}
218
219def Laws.sha1_fips_2():
220 {==}
221
222def Laws.ripemd160_streaming(s, a, b):
223 Laws.md_streaming(~Hs.HsW5, ~RM.HsRipemd160.compress, ~63, s, a, b)
224
225def Laws.ripemd160_split(a, b):
226 %Laws.ripemd160_streaming(RM.HsRipemd160.init(), a, b) : {RM.HsRipemd160.final(_) == RM.HsRipemd160.digest(B.Octets.append(a, b)) : B.Octets}
227 {==}
228
229def Laws.ripemd160_split3(a, b, c):
230 %Laws.ripemd160_streaming(RM.HsRipemd160.update(RM.HsRipemd160.init(), a), b, c) : {RM.HsRipemd160.final(_) == RM.HsRipemd160.digest(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
231 %Laws.ripemd160_streaming(RM.HsRipemd160.init(), a, B.Octets.append(b, c)) : {RM.HsRipemd160.final(_) == RM.HsRipemd160.digest(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
232 {==}
233
234def Laws.ripemd160_length(s):
235 w5le_len(Hs.HsMd.cv(~Hs.HsW5, Hs.hs.md.feed(~Hs.HsW5, ~RM.HsRipemd160.compress, ~63, Hs.HsMd.md_pad(~63, Hs.HsMd.count(~Hs.HsW5, s), Hs.hs.len.le(Hs.HsMd.bits(~Hs.HsW5, ~63, s))), s)))
236
237def Laws.ripemd160_digest_length(m):
238 Laws.ripemd160_length(RM.HsRipemd160.update(RM.HsRipemd160.init(), m))
239
240def Laws.ripemd160_paper_1():
241 {==}
242
243def Laws.ripemd160_paper_2():
244 {==}
245
246def Laws.ripemd160_paper_3():
247 {==}
248
249def Laws.ripemd160_paper_4():
250 {==}
251
252def Laws.ripemd160_paper_5():
253 {==}
254
255def Laws.ripemd160_paper_6():
256 {==}
257
258def Laws.ripemd160_paper_7():
259 {==}
260
261def Laws.ripemd160_paper_8():
262 {==}
263
264def Laws.sm3_streaming(s, a, b):
265 Laws.md_streaming(~Hs.HsW8, ~SM.HsSm3.compress, ~63, s, a, b)
266
267def Laws.sm3_split(a, b):
268 %Laws.sm3_streaming(SM.HsSm3.init(), a, b) : {SM.HsSm3.final(_) == SM.HsSm3.digest(B.Octets.append(a, b)) : B.Octets}
269 {==}
270
271def Laws.sm3_split3(a, b, c):
272 %Laws.sm3_streaming(SM.HsSm3.update(SM.HsSm3.init(), a), b, c) : {SM.HsSm3.final(_) == SM.HsSm3.digest(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
273 %Laws.sm3_streaming(SM.HsSm3.init(), a, B.Octets.append(b, c)) : {SM.HsSm3.final(_) == SM.HsSm3.digest(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
274 {==}
275
276def Laws.sm3_length(s):
277 w8be_len(Hs.HsMd.cv(~Hs.HsW8, Hs.hs.md.feed(~Hs.HsW8, ~SM.HsSm3.compress, ~63, Hs.HsMd.md_pad(~63, Hs.HsMd.count(~Hs.HsW8, s), Hs.hs.len.be(Hs.HsMd.bits(~Hs.HsW8, ~63, s))), s)))
278
279def Laws.sm3_digest_length(m):
280 Laws.sm3_length(SM.HsSm3.update(SM.HsSm3.init(), m))
281
282def Laws.sm3_example_1():
283 {==}
284
285def Laws.sm3_example_2():
286 {==}
287
288def Laws.streebog512_streaming(s, a, b):
289 Laws.md_streaming(~ST.HsStbCv, ~ST.HsStreebog.compress, ~63, s, a, b)
290
291def Laws.streebog512_split(a, b):
292 %Laws.streebog512_streaming(ST.HsStreebog.init512(), a, b) : {ST.HsStreebog.final512(_) == ST.HsStreebog.digest512(B.Octets.append(a, b)) : B.Octets}
293 {==}
294
295def Laws.streebog512_split3(a, b, c):
296 %Laws.streebog512_streaming(ST.HsStreebog.update(ST.HsStreebog.init512(), a), b, c) : {ST.HsStreebog.final512(_) == ST.HsStreebog.digest512(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
297 %Laws.streebog512_streaming(ST.HsStreebog.init512(), a, B.Octets.append(b, c)) : {ST.HsStreebog.final512(_) == ST.HsStreebog.digest512(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
298 {==}
299
300def Laws.streebog512_length(s):
301 stb512_len(ST.hs.stb.finish(s))
302
303def Laws.streebog512_digest_length(m):
304 Laws.streebog512_length(ST.HsStreebog.update(ST.HsStreebog.init512(), m))
305
306def Laws.streebog256_streaming(s, a, b):
307 Laws.md_streaming(~ST.HsStbCv, ~ST.HsStreebog.compress, ~63, s, a, b)
308
309def Laws.streebog256_split(a, b):
310 %Laws.streebog256_streaming(ST.HsStreebog.init256(), a, b) : {ST.HsStreebog.final256(_) == ST.HsStreebog.digest256(B.Octets.append(a, b)) : B.Octets}
311 {==}
312
313def Laws.streebog256_split3(a, b, c):
314 %Laws.streebog256_streaming(ST.HsStreebog.update(ST.HsStreebog.init256(), a), b, c) : {ST.HsStreebog.final256(_) == ST.HsStreebog.digest256(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
315 %Laws.streebog256_streaming(ST.HsStreebog.init256(), a, B.Octets.append(b, c)) : {ST.HsStreebog.final256(_) == ST.HsStreebog.digest256(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
316 {==}
317
318def Laws.streebog256_length(s):
319 stb256_len(ST.hs.stb.finish(s))
320
321def Laws.streebog256_digest_length(m):
322 Laws.streebog256_length(ST.HsStreebog.update(ST.HsStreebog.init256(), m))
323
324def Laws.streebog_lps_zero():
325 {==}
326
327def Laws.streebog_g_example1():
328 {==}
329
330def Laws.streebog_g0_example1():
331 {==}
332
333def Laws.michael_streaming(s, a, b):
334 Laws.md_streaming(~Hs.HsW2, ~MI.HsMichael.compress, ~3, s, a, b)
335
336def Laws.michael_split(k, a, b):
337 %Laws.michael_streaming(MI.HsMichael.init(k), a, b) : {MI.HsMichael.final(_) == MI.HsMichael.mic(k, B.Octets.append(a, b)) : B.Octets}
338 {==}
339
340def Laws.michael_length(s):
341 w2le_len(Hs.HsMd.cv(~Hs.HsW2, Hs.HsMd.update_list(~Hs.HsW2, ~MI.HsMichael.compress, ~3, s, MI.hs.michael.pad(Hs.HsMd.count(~Hs.HsW2, s)))))
342
343def Laws.michael_mic_length(k, m):
344 Laws.michael_length(MI.HsMichael.update(MI.HsMichael.init(k), m))
345
346def Laws.michael_short_key():
347 {==}
348
349def Laws.michael_vector_1():
350 {==}
351
352def Laws.michael_vector_2():
353 {==}
354
355def Laws.michael_vector_3():
356 {==}
357
358def Laws.michael_vector_4():
359 {==}
360
361def Laws.michael_vector_5():
362 {==}
363
364def Laws.michael_vector_6():
365 {==}
366
367def Laws.michael_tkip_m63():
368 {==}