1	# Generated by gen/laws.py; do not edit by hand.
2	#
3	# The laws of the hashes, for every input where they are proved:
4	# streaming (update over a ++ b is update over a, then b, from every
5	# state), the digest in any pieces equals the one-shot digest, and the
6	# digest's length; then the specifications' vectors. The engine's streaming
7	# law is stated once, for every chaining value and compression function;
8	# each hash's is that law at its own defs.
9	import Base
10	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
11	import ./hashes.bend as Hs
12	import ./md4.bend as M4
13	import ./md5.bend as M5
14	import ./sha1.bend as S1
15	import ./ripemd160.bend as RM
16	import ./sm3.bend as SM
17	import ./streebog.bend as ST
18	import ./michael.bend as MI
19	
20	# The engine (hashes.bend), for every chaining value type, compression
21	# function and block size: a ++ b is a, then b, from every state
22	law md_streaming:
23	  for ~C: Data
24	  for ~compress: C -> List<&2, U32> -> C
25	  for ~last: U32
26	  for s: Hs.HsMdState<C>
27	  for +a: B.Octets
28	  for +b: B.Octets
29	  {Hs.HsMd.update(~C, ~compress, ~last, s, B.Octets.append(a, b)) == Hs.HsMd.update(~C, ~compress, ~last, Hs.HsMd.update(~C, ~compress, ~last, s, a), b) : Hs.HsMdState<C>}
30	
31	# MD4 (RFC 1320) (md4.bend)
32	
33	# MD4 (RFC 1320): update over a ++ b is update over a, then b, from every state
34	law md4_streaming:
35	  for s: Hs.HsMdState<Hs.HsW4>
36	  for +a: B.Octets
37	  for +b: B.Octets
38	  {M4.HsMd4.update(s, B.Octets.append(a, b)) == M4.HsMd4.update(M4.HsMd4.update(s, a), b) : Hs.HsMdState<Hs.HsW4>}
39	
40	# MD4 (RFC 1320): the digest in two pieces is the one-shot digest, for every split
41	law md4_split:
42	  for +a: B.Octets
43	  for +b: B.Octets
44	  {M4.HsMd4.final(M4.HsMd4.update(M4.HsMd4.update(M4.HsMd4.init(), a), b)) == M4.HsMd4.digest(B.Octets.append(a, b)) : B.Octets}
45	
46	# MD4 (RFC 1320): and in three pieces
47	law md4_split3:
48	  for +a: B.Octets
49	  for +b: B.Octets
50	  for +c: B.Octets
51	  {M4.HsMd4.final(M4.HsMd4.update(M4.HsMd4.update(M4.HsMd4.update(M4.HsMd4.init(), a), b), c)) == M4.HsMd4.digest(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
52	
53	# MD4 (RFC 1320): the digest of every state has 16 bytes
54	law md4_length:
55	  for +s: Hs.HsMdState<Hs.HsW4>
56	  {B.Octets.len(M4.HsMd4.final(s)) == 16n : Nat}
57	
58	# MD4 (RFC 1320): the digest of every message has 16 bytes
59	law md4_digest_length:
60	  for +m: B.Octets
61	  {B.Octets.len(M4.HsMd4.digest(m)) == 16n : Nat}
62	
63	# MD4 (RFC 1320): RFC 1320, appendix A.5 (the test suite)
64	law md4_rfc1320_1:
65	  {M4.HsMd4.digest(B.Octets.of_string("")) == B.Octets.of_list([49, 214, 207, 224, 209, 106, 233, 49, 183, 60, 89, 215, 224, 192, 137, 192]) : B.Octets}
66	
67	# MD4 (RFC 1320): RFC 1320, appendix A.5 (the test suite)
68	law md4_rfc1320_2:
69	  {M4.HsMd4.digest(B.Octets.of_string("a")) == B.Octets.of_list([189, 229, 44, 179, 29, 227, 62, 70, 36, 94, 5, 251, 219, 214, 251, 36]) : B.Octets}
70	
71	# MD4 (RFC 1320): RFC 1320, appendix A.5 (the test suite)
72	law md4_rfc1320_3:
73	  {M4.HsMd4.digest(B.Octets.of_string("abc")) == B.Octets.of_list([164, 72, 1, 122, 175, 33, 216, 82, 95, 193, 10, 232, 122, 166, 114, 157]) : B.Octets}
74	
75	# MD4 (RFC 1320): RFC 1320, appendix A.5 (the test suite)
76	law md4_rfc1320_4:
77	  {M4.HsMd4.digest(B.Octets.of_string("message digest")) == B.Octets.of_list([217, 19, 10, 129, 100, 84, 159, 232, 24, 135, 72, 6, 225, 199, 1, 75]) : B.Octets}
78	
79	# MD4 (RFC 1320): RFC 1320, appendix A.5 (the test suite)
80	law md4_rfc1320_5:
81	  {M4.HsMd4.digest(B.Octets.of_string("abcdefghijklmnopqrstuvwxyz")) == B.Octets.of_list([215, 158, 28, 48, 138, 165, 187, 205, 238, 168, 237, 99, 223, 65, 45, 169]) : B.Octets}
82	
83	# MD4 (RFC 1320): RFC 1320, appendix A.5 (the test suite)
84	law md4_rfc1320_6:
85	  {M4.HsMd4.digest(B.Octets.of_string("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789")) == B.Octets.of_list([4, 63, 133, 130, 242, 65, 219, 53, 28, 230, 39, 225, 83, 231, 240, 228]) : B.Octets}
86	
87	# MD4 (RFC 1320): RFC 1320, appendix A.5 (the test suite)
88	law md4_rfc1320_7:
89	  {M4.HsMd4.digest(B.Octets.of_string("12345678901234567890123456789012345678901234567890123456789012345678901234567890")) == B.Octets.of_list([227, 59, 77, 220, 156, 56, 242, 25, 156, 62, 123, 22, 79, 204, 5, 54]) : B.Octets}
90	
91	# MD5 (RFC 1321) (md5.bend)
92	
93	# MD5 (RFC 1321): update over a ++ b is update over a, then b, from every state
94	law md5_streaming:
95	  for s: Hs.HsMdState<Hs.HsW4>
96	  for +a: B.Octets
97	  for +b: B.Octets
98	  {M5.HsMd5.update(s, B.Octets.append(a, b)) == M5.HsMd5.update(M5.HsMd5.update(s, a), b) : Hs.HsMdState<Hs.HsW4>}
99	
100	# MD5 (RFC 1321): the digest in two pieces is the one-shot digest, for every split
101	law md5_split:
102	  for +a: B.Octets
103	  for +b: B.Octets
104	  {M5.HsMd5.final(M5.HsMd5.update(M5.HsMd5.update(M5.HsMd5.init(), a), b)) == M5.HsMd5.digest(B.Octets.append(a, b)) : B.Octets}
105	
106	# MD5 (RFC 1321): and in three pieces
107	law md5_split3:
108	  for +a: B.Octets
109	  for +b: B.Octets
110	  for +c: B.Octets
111	  {M5.HsMd5.final(M5.HsMd5.update(M5.HsMd5.update(M5.HsMd5.update(M5.HsMd5.init(), a), b), c)) == M5.HsMd5.digest(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
112	
113	# MD5 (RFC 1321): the digest of every state has 16 bytes
114	law md5_length:
115	  for +s: Hs.HsMdState<Hs.HsW4>
116	  {B.Octets.len(M5.HsMd5.final(s)) == 16n : Nat}
117	
118	# MD5 (RFC 1321): the digest of every message has 16 bytes
119	law md5_digest_length:
120	  for +m: B.Octets
121	  {B.Octets.len(M5.HsMd5.digest(m)) == 16n : Nat}
122	
123	# MD5 (RFC 1321): RFC 1321, appendix A.5 (the test suite)
124	law md5_rfc1321_1:
125	  {M5.HsMd5.digest(B.Octets.of_string("")) == B.Octets.of_list([212, 29, 140, 217, 143, 0, 178, 4, 233, 128, 9, 152, 236, 248, 66, 126]) : B.Octets}
126	
127	# MD5 (RFC 1321): RFC 1321, appendix A.5 (the test suite)
128	law md5_rfc1321_2:
129	  {M5.HsMd5.digest(B.Octets.of_string("a")) == B.Octets.of_list([12, 193, 117, 185, 192, 241, 182, 168, 49, 195, 153, 226, 105, 119, 38, 97]) : B.Octets}
130	
131	# MD5 (RFC 1321): RFC 1321, appendix A.5 (the test suite)
132	law md5_rfc1321_3:
133	  {M5.HsMd5.digest(B.Octets.of_string("abc")) == B.Octets.of_list([144, 1, 80, 152, 60, 210, 79, 176, 214, 150, 63, 125, 40, 225, 127, 114]) : B.Octets}
134	
135	# MD5 (RFC 1321): RFC 1321, appendix A.5 (the test suite)
136	law md5_rfc1321_4:
137	  {M5.HsMd5.digest(B.Octets.of_string("message digest")) == B.Octets.of_list([249, 107, 105, 125, 124, 183, 147, 141, 82, 90, 47, 49, 170, 241, 97, 208]) : B.Octets}
138	
139	# MD5 (RFC 1321): RFC 1321, appendix A.5 (the test suite)
140	law md5_rfc1321_5:
141	  {M5.HsMd5.digest(B.Octets.of_string("abcdefghijklmnopqrstuvwxyz")) == B.Octets.of_list([195, 252, 211, 215, 97, 146, 228, 0, 125, 251, 73, 108, 202, 103, 225, 59]) : B.Octets}
142	
143	# MD5 (RFC 1321): RFC 1321, appendix A.5 (the test suite)
144	law md5_rfc1321_6:
145	  {M5.HsMd5.digest(B.Octets.of_string("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789")) == B.Octets.of_list([209, 116, 171, 152, 210, 119, 217, 245, 165, 97, 28, 44, 159, 65, 157, 159]) : B.Octets}
146	
147	# MD5 (RFC 1321): RFC 1321, appendix A.5 (the test suite)
148	law md5_rfc1321_7:
149	  {M5.HsMd5.digest(B.Octets.of_string("12345678901234567890123456789012345678901234567890123456789012345678901234567890")) == B.Octets.of_list([87, 237, 244, 162, 43, 227, 201, 85, 172, 73, 218, 46, 33, 7, 182, 122]) : B.Octets}
150	
151	# SHA-1 (FIPS 180-4) (sha1.bend)
152	
153	# SHA-1 (FIPS 180-4): update over a ++ b is update over a, then b, from every state
154	law sha1_streaming:
155	  for s: Hs.HsMdState<Hs.HsW5>
156	  for +a: B.Octets
157	  for +b: B.Octets
158	  {S1.HsSha1.update(s, B.Octets.append(a, b)) == S1.HsSha1.update(S1.HsSha1.update(s, a), b) : Hs.HsMdState<Hs.HsW5>}
159	
160	# SHA-1 (FIPS 180-4): the digest in two pieces is the one-shot digest, for every split
161	law sha1_split:
162	  for +a: B.Octets
163	  for +b: B.Octets
164	  {S1.HsSha1.final(S1.HsSha1.update(S1.HsSha1.update(S1.HsSha1.init(), a), b)) == S1.HsSha1.digest(B.Octets.append(a, b)) : B.Octets}
165	
166	# SHA-1 (FIPS 180-4): and in three pieces
167	law sha1_split3:
168	  for +a: B.Octets
169	  for +b: B.Octets
170	  for +c: B.Octets
171	  {S1.HsSha1.final(S1.HsSha1.update(S1.HsSha1.update(S1.HsSha1.update(S1.HsSha1.init(), a), b), c)) == S1.HsSha1.digest(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
172	
173	# SHA-1 (FIPS 180-4): the digest of every state has 20 bytes
174	law sha1_length:
175	  for +s: Hs.HsMdState<Hs.HsW5>
176	  {B.Octets.len(S1.HsSha1.final(s)) == 20n : Nat}
177	
178	# SHA-1 (FIPS 180-4): the digest of every message has 20 bytes
179	law sha1_digest_length:
180	  for +m: B.Octets
181	  {B.Octets.len(S1.HsSha1.digest(m)) == 20n : Nat}
182	
183	# SHA-1 (FIPS 180-4): FIPS 180-4's examples (NIST's SHA-1 example values): "abc" and the 448-bit message
184	law sha1_fips_1:
185	  {S1.HsSha1.digest(B.Octets.of_string("abc")) == B.Octets.of_list([169, 153, 62, 54, 71, 6, 129, 106, 186, 62, 37, 113, 120, 80, 194, 108, 156, 208, 216, 157]) : B.Octets}
186	
187	# SHA-1 (FIPS 180-4): FIPS 180-4's examples (NIST's SHA-1 example values): "abc" and the 448-bit message
188	law sha1_fips_2:
189	  {S1.HsSha1.digest(B.Octets.of_string("abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq")) == B.Octets.of_list([132, 152, 62, 68, 28, 59, 210, 110, 186, 174, 74, 161, 249, 81, 41, 229, 229, 70, 112, 241]) : B.Octets}
190	
191	# RIPEMD-160 (ripemd160.bend)
192	
193	# RIPEMD-160: update over a ++ b is update over a, then b, from every state
194	law ripemd160_streaming:
195	  for s: Hs.HsMdState<Hs.HsW5>
196	  for +a: B.Octets
197	  for +b: B.Octets
198	  {RM.HsRipemd160.update(s, B.Octets.append(a, b)) == RM.HsRipemd160.update(RM.HsRipemd160.update(s, a), b) : Hs.HsMdState<Hs.HsW5>}
199	
200	# RIPEMD-160: the digest in two pieces is the one-shot digest, for every split
201	law ripemd160_split:
202	  for +a: B.Octets
203	  for +b: B.Octets
204	  {RM.HsRipemd160.final(RM.HsRipemd160.update(RM.HsRipemd160.update(RM.HsRipemd160.init(), a), b)) == RM.HsRipemd160.digest(B.Octets.append(a, b)) : B.Octets}
205	
206	# RIPEMD-160: and in three pieces
207	law ripemd160_split3:
208	  for +a: B.Octets
209	  for +b: B.Octets
210	  for +c: B.Octets
211	  {RM.HsRipemd160.final(RM.HsRipemd160.update(RM.HsRipemd160.update(RM.HsRipemd160.update(RM.HsRipemd160.init(), a), b), c)) == RM.HsRipemd160.digest(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
212	
213	# RIPEMD-160: the digest of every state has 20 bytes
214	law ripemd160_length:
215	  for +s: Hs.HsMdState<Hs.HsW5>
216	  {B.Octets.len(RM.HsRipemd160.final(s)) == 20n : Nat}
217	
218	# RIPEMD-160: the digest of every message has 20 bytes
219	law ripemd160_digest_length:
220	  for +m: B.Octets
221	  {B.Octets.len(RM.HsRipemd160.digest(m)) == 20n : Nat}
222	
223	# RIPEMD-160: the test values of Dobbertin, Bosselaers and Preneel (the RIPEMD-160 page)
224	law ripemd160_paper_1:
225	  {RM.HsRipemd160.digest(B.Octets.of_string("")) == B.Octets.of_list([156, 17, 133, 165, 197, 233, 252, 84, 97, 40, 8, 151, 126, 232, 245, 72, 178, 37, 141, 49]) : B.Octets}
226	
227	# RIPEMD-160: the test values of Dobbertin, Bosselaers and Preneel (the RIPEMD-160 page)
228	law ripemd160_paper_2:
229	  {RM.HsRipemd160.digest(B.Octets.of_string("a")) == B.Octets.of_list([11, 220, 157, 45, 37, 107, 62, 233, 218, 174, 52, 123, 230, 244, 220, 131, 90, 70, 127, 254]) : B.Octets}
230	
231	# RIPEMD-160: the test values of Dobbertin, Bosselaers and Preneel (the RIPEMD-160 page)
232	law ripemd160_paper_3:
233	  {RM.HsRipemd160.digest(B.Octets.of_string("abc")) == B.Octets.of_list([142, 178, 8, 247, 224, 93, 152, 122, 155, 4, 74, 142, 152, 198, 176, 135, 241, 90, 11, 252]) : B.Octets}
234	
235	# RIPEMD-160: the test values of Dobbertin, Bosselaers and Preneel (the RIPEMD-160 page)
236	law ripemd160_paper_4:
237	  {RM.HsRipemd160.digest(B.Octets.of_string("message digest")) == B.Octets.of_list([93, 6, 137, 239, 73, 210, 250, 229, 114, 184, 129, 177, 35, 168, 95, 250, 33, 89, 95, 54]) : B.Octets}
238	
239	# RIPEMD-160: the test values of Dobbertin, Bosselaers and Preneel (the RIPEMD-160 page)
240	law ripemd160_paper_5:
241	  {RM.HsRipemd160.digest(B.Octets.of_string("abcdefghijklmnopqrstuvwxyz")) == B.Octets.of_list([247, 28, 39, 16, 156, 105, 44, 27, 86, 187, 220, 235, 91, 157, 40, 101, 179, 112, 141, 188]) : B.Octets}
242	
243	# RIPEMD-160: the test values of Dobbertin, Bosselaers and Preneel (the RIPEMD-160 page)
244	law ripemd160_paper_6:
245	  {RM.HsRipemd160.digest(B.Octets.of_string("abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq")) == B.Octets.of_list([18, 160, 83, 56, 74, 156, 12, 136, 228, 5, 160, 108, 39, 220, 244, 154, 218, 98, 235, 43]) : B.Octets}
246	
247	# RIPEMD-160: the test values of Dobbertin, Bosselaers and Preneel (the RIPEMD-160 page)
248	law ripemd160_paper_7:
249	  {RM.HsRipemd160.digest(B.Octets.of_string("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789")) == B.Octets.of_list([176, 226, 11, 110, 49, 22, 100, 2, 134, 237, 58, 135, 165, 113, 48, 121, 178, 31, 81, 137]) : B.Octets}
250	
251	# RIPEMD-160: the test values of Dobbertin, Bosselaers and Preneel (the RIPEMD-160 page)
252	law ripemd160_paper_8:
253	  {RM.HsRipemd160.digest(B.Octets.of_string("12345678901234567890123456789012345678901234567890123456789012345678901234567890")) == B.Octets.of_list([155, 117, 46, 69, 87, 61, 75, 57, 244, 219, 211, 50, 60, 171, 130, 191, 99, 50, 107, 251]) : B.Octets}
254	
255	# SM3 (GB/T 32905) (sm3.bend)
256	
257	# SM3 (GB/T 32905): update over a ++ b is update over a, then b, from every state
258	law sm3_streaming:
259	  for s: Hs.HsMdState<Hs.HsW8>
260	  for +a: B.Octets
261	  for +b: B.Octets
262	  {SM.HsSm3.update(s, B.Octets.append(a, b)) == SM.HsSm3.update(SM.HsSm3.update(s, a), b) : Hs.HsMdState<Hs.HsW8>}
263	
264	# SM3 (GB/T 32905): the digest in two pieces is the one-shot digest, for every split
265	law sm3_split:
266	  for +a: B.Octets
267	  for +b: B.Octets
268	  {SM.HsSm3.final(SM.HsSm3.update(SM.HsSm3.update(SM.HsSm3.init(), a), b)) == SM.HsSm3.digest(B.Octets.append(a, b)) : B.Octets}
269	
270	# SM3 (GB/T 32905): and in three pieces
271	law sm3_split3:
272	  for +a: B.Octets
273	  for +b: B.Octets
274	  for +c: B.Octets
275	  {SM.HsSm3.final(SM.HsSm3.update(SM.HsSm3.update(SM.HsSm3.update(SM.HsSm3.init(), a), b), c)) == SM.HsSm3.digest(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
276	
277	# SM3 (GB/T 32905): the digest of every state has 32 bytes
278	law sm3_length:
279	  for +s: Hs.HsMdState<Hs.HsW8>
280	  {B.Octets.len(SM.HsSm3.final(s)) == 32n : Nat}
281	
282	# SM3 (GB/T 32905): the digest of every message has 32 bytes
283	law sm3_digest_length:
284	  for +m: B.Octets
285	  {B.Octets.len(SM.HsSm3.digest(m)) == 32n : Nat}
286	
287	# SM3 (GB/T 32905): draft-shen-sm3-hash-01, examples 1 and 2
288	law sm3_example_1:
289	  {SM.HsSm3.digest(B.Octets.of_string("abc")) == B.Octets.of_list([102, 199, 240, 244, 98, 238, 237, 217, 209, 242, 212, 107, 220, 16, 228, 226, 65, 103, 196, 135, 92, 242, 247, 162, 41, 125, 160, 43, 143, 75, 168, 224]) : B.Octets}
290	
291	# SM3 (GB/T 32905): draft-shen-sm3-hash-01, examples 1 and 2
292	law sm3_example_2:
293	  {SM.HsSm3.digest(B.Octets.of_string("abcdabcdabcdabcdabcdabcdabcdabcdabcdabcdabcdabcdabcdabcdabcdabcd")) == B.Octets.of_list([222, 190, 159, 249, 34, 117, 184, 161, 56, 96, 72, 137, 193, 142, 90, 77, 111, 219, 112, 229, 56, 126, 87, 101, 41, 61, 203, 163, 156, 12, 87, 50]) : B.Octets}
294	
295	# Streebog-512 (RFC 6986) (streebog.bend)
296	
297	# Streebog-512 (RFC 6986): update over a ++ b is update over a, then b, from every state
298	law streebog512_streaming:
299	  for s: Hs.HsMdState<ST.HsStbCv>
300	  for +a: B.Octets
301	  for +b: B.Octets
302	  {ST.HsStreebog.update(s, B.Octets.append(a, b)) == ST.HsStreebog.update(ST.HsStreebog.update(s, a), b) : Hs.HsMdState<ST.HsStbCv>}
303	
304	# Streebog-512 (RFC 6986): the digest in two pieces is the one-shot digest, for every split
305	law streebog512_split:
306	  for +a: B.Octets
307	  for +b: B.Octets
308	  {ST.HsStreebog.final512(ST.HsStreebog.update(ST.HsStreebog.update(ST.HsStreebog.init512(), a), b)) == ST.HsStreebog.digest512(B.Octets.append(a, b)) : B.Octets}
309	
310	# Streebog-512 (RFC 6986): and in three pieces
311	law streebog512_split3:
312	  for +a: B.Octets
313	  for +b: B.Octets
314	  for +c: B.Octets
315	  {ST.HsStreebog.final512(ST.HsStreebog.update(ST.HsStreebog.update(ST.HsStreebog.update(ST.HsStreebog.init512(), a), b), c)) == ST.HsStreebog.digest512(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
316	
317	# Streebog-512 (RFC 6986): the digest of every state has 64 bytes
318	law streebog512_length:
319	  for +s: Hs.HsMdState<ST.HsStbCv>
320	  {B.Octets.len(ST.HsStreebog.final512(s)) == 64n : Nat}
321	
322	# Streebog-512 (RFC 6986): the digest of every message has 64 bytes
323	law streebog512_digest_length:
324	  for +m: B.Octets
325	  {B.Octets.len(ST.HsStreebog.digest512(m)) == 64n : Nat}
326	
327	# Streebog-256 (RFC 6986) (streebog.bend)
328	
329	# Streebog-256 (RFC 6986): update over a ++ b is update over a, then b, from every state
330	law streebog256_streaming:
331	  for s: Hs.HsMdState<ST.HsStbCv>
332	  for +a: B.Octets
333	  for +b: B.Octets
334	  {ST.HsStreebog.update(s, B.Octets.append(a, b)) == ST.HsStreebog.update(ST.HsStreebog.update(s, a), b) : Hs.HsMdState<ST.HsStbCv>}
335	
336	# Streebog-256 (RFC 6986): the digest in two pieces is the one-shot digest, for every split
337	law streebog256_split:
338	  for +a: B.Octets
339	  for +b: B.Octets
340	  {ST.HsStreebog.final256(ST.HsStreebog.update(ST.HsStreebog.update(ST.HsStreebog.init256(), a), b)) == ST.HsStreebog.digest256(B.Octets.append(a, b)) : B.Octets}
341	
342	# Streebog-256 (RFC 6986): and in three pieces
343	law streebog256_split3:
344	  for +a: B.Octets
345	  for +b: B.Octets
346	  for +c: B.Octets
347	  {ST.HsStreebog.final256(ST.HsStreebog.update(ST.HsStreebog.update(ST.HsStreebog.update(ST.HsStreebog.init256(), a), b), c)) == ST.HsStreebog.digest256(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
348	
349	# Streebog-256 (RFC 6986): the digest of every state has 32 bytes
350	law streebog256_length:
351	  for +s: Hs.HsMdState<ST.HsStbCv>
352	  {B.Octets.len(ST.HsStreebog.final256(s)) == 32n : Nat}
353	
354	# Streebog-256 (RFC 6986): the digest of every message has 32 bytes
355	law streebog256_digest_length:
356	  for +m: B.Octets
357	  {B.Octets.len(ST.HsStreebog.digest256(m)) == 32n : Nat}
358	
359	# Streebog's transformations (streebog.bend): RFC 6986, section 10.1, example 1
360	
361	# Streebog-512, K = LPS(h xor N) = LPS(0^512) (RFC 6986 prints it most significant byte first)
362	law streebog_lps_zero:
363	  {ST.HsStreebog.lps(B.Octets.zeros(64n)) == B.Octets.of_list([116, 165, 212, 206, 46, 252, 131, 179, 116, 165, 212, 206, 46, 252, 131, 179, 116, 165, 212, 206, 46, 252, 131, 179, 116, 165, 212, 206, 46, 252, 131, 179, 116, 165, 212, 206, 46, 252, 131, 179, 116, 165, 212, 206, 46, 252, 131, 179, 116, 165, 212, 206, 46, 252, 131, 179, 116, 165, 212, 206, 46, 252, 131, 179]) : B.Octets}
364	
365	# Streebog-512, the first compression, g_N(h, m) with h = N = 0 and m the padded M1 (RFC 6986 prints it most significant byte first)
366	law streebog_g_example1:
367	  {ST.HsStreebog.g(B.Octets.zeros(64n), B.Octets.zeros(64n), B.Octets.of_list([48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 48, 49, 50, 1])) == B.Octets.of_list([226, 218, 59, 107, 115, 228, 254, 5, 217, 245, 177, 63, 121, 53, 65, 149, 92, 129, 80, 44, 82, 15, 237, 211, 197, 186, 187, 140, 144, 246, 84, 39, 189, 142, 115, 51, 219, 138, 72, 38, 166, 169, 90, 68, 65, 102, 168, 23, 56, 79, 57, 33, 175, 52, 234, 145, 17, 203, 44, 129, 248, 44, 16, 253]) : B.Octets}
368	
369	# Streebog-512, g_0(h, N) after it, N = 504 (RFC 6986 prints it most significant byte first)
370	law streebog_g0_example1:
371	  {ST.HsStreebog.g(B.Octets.zeros(64n), B.Octets.of_list([226, 218, 59, 107, 115, 228, 254, 5, 217, 245, 177, 63, 121, 53, 65, 149, 92, 129, 80, 44, 82, 15, 237, 211, 197, 186, 187, 140, 144, 246, 84, 39, 189, 142, 115, 51, 219, 138, 72, 38, 166, 169, 90, 68, 65, 102, 168, 23, 56, 79, 57, 33, 175, 52, 234, 145, 17, 203, 44, 129, 248, 44, 16, 253]), B.Octets.of_list([248, 1])) == B.Octets.of_list([124, 29, 119, 231, 93, 26, 144, 168, 1, 69, 211, 98, 214, 225, 55, 144, 127, 110, 166, 25, 79, 161, 71, 33, 98, 148, 55, 109, 157, 182, 45, 61, 82, 151, 213, 212, 103, 112, 187, 170, 235, 22, 23, 11, 42, 111, 2, 66, 182, 20, 13, 194, 254, 228, 194, 150, 241, 92, 105, 36, 217, 31, 136, 92]) : B.Octets}
372	
373	# Michael (michael.bend): the same laws, under every key
374	
375	# Michael (IEEE 802.11i): update over a ++ b is update over a, then b, from every state
376	law michael_streaming:
377	  for s: Hs.HsMdState<Hs.HsW2>
378	  for +a: B.Octets
379	  for +b: B.Octets
380	  {MI.HsMichael.update(s, B.Octets.append(a, b)) == MI.HsMichael.update(MI.HsMichael.update(s, a), b) : Hs.HsMdState<Hs.HsW2>}
381	
382	# Michael (IEEE 802.11i): the tag in two pieces is the one-call tag, for every key and split
383	law michael_split:
384	  for +k: Hs.HsW2
385	  for +a: B.Octets
386	  for +b: B.Octets
387	  {MI.HsMichael.final(MI.HsMichael.update(MI.HsMichael.update(MI.HsMichael.init(k), a), b)) == MI.HsMichael.mic(k, B.Octets.append(a, b)) : B.Octets}
388	
389	# Michael (IEEE 802.11i): the tag of every state has 8 bytes
390	law michael_length:
391	  for +s: Hs.HsMdState<Hs.HsW2>
392	  {B.Octets.len(MI.HsMichael.final(s)) == 8n : Nat}
393	
394	# Michael (IEEE 802.11i): the tag of every message under every key has 8 bytes
395	law michael_mic_length:
396	  for +k: Hs.HsW2
397	  for +m: B.Octets
398	  {B.Octets.len(MI.HsMichael.mic(k, m)) == 8n : Nat}
399	
400	# Michael (IEEE 802.11i): a key of 7 bytes is refused
401	law michael_short_key:
402	  {Result.map(&2, &2, Hs.HsError, Hs.HsW2, Unit, k => Unit{}, MI.HsMichael.key(B.Octets.zeros(7n))) == Fail{Hs.HsBadKeyLength{7n}} : Result<&2, &2, Hs.HsError, Unit>}
403	
404	# Michael (IEEE 802.11i): test vector 1 as recalled from IEEE 802.11i's Annex H.2 (each key the previous tag), not checked against a published copy (README.md)
405	law michael_vector_1:
406	  {Result.map(&2, &2, Hs.HsError, Hs.HsW2, B.Octets, k => MI.HsMichael.mic(k, B.Octets.of_string("")), MI.HsMichael.key(B.Octets.of_list([0, 0, 0, 0, 0, 0, 0, 0]))) == Done{B.Octets.of_list([130, 146, 92, 28, 161, 209, 48, 184])} : Result<&2, &2, Hs.HsError, B.Octets>}
407	
408	# Michael (IEEE 802.11i): test vector 2 as recalled from IEEE 802.11i's Annex H.2 (each key the previous tag), not checked against a published copy (README.md)
409	law michael_vector_2:
410	  {Result.map(&2, &2, Hs.HsError, Hs.HsW2, B.Octets, k => MI.HsMichael.mic(k, B.Octets.of_string("M")), MI.HsMichael.key(B.Octets.of_list([130, 146, 92, 28, 161, 209, 48, 184]))) == Done{B.Octets.of_list([67, 71, 33, 202, 64, 99, 155, 63])} : Result<&2, &2, Hs.HsError, B.Octets>}
411	
412	# Michael (IEEE 802.11i): test vector 3 as recalled from IEEE 802.11i's Annex H.2 (each key the previous tag), not checked against a published copy (README.md)
413	law michael_vector_3:
414	  {Result.map(&2, &2, Hs.HsError, Hs.HsW2, B.Octets, k => MI.HsMichael.mic(k, B.Octets.of_string("Mi")), MI.HsMichael.key(B.Octets.of_list([67, 71, 33, 202, 64, 99, 155, 63]))) == Done{B.Octets.of_list([232, 249, 190, 202, 233, 126, 93, 41])} : Result<&2, &2, Hs.HsError, B.Octets>}
415	
416	# Michael (IEEE 802.11i): test vector 4 as recalled from IEEE 802.11i's Annex H.2 (each key the previous tag), not checked against a published copy (README.md)
417	law michael_vector_4:
418	  {Result.map(&2, &2, Hs.HsError, Hs.HsW2, B.Octets, k => MI.HsMichael.mic(k, B.Octets.of_string("Mic")), MI.HsMichael.key(B.Octets.of_list([232, 249, 190, 202, 233, 126, 93, 41]))) == Done{B.Octets.of_list([144, 3, 143, 198, 207, 19, 193, 219])} : Result<&2, &2, Hs.HsError, B.Octets>}
419	
420	# Michael (IEEE 802.11i): test vector 5 as recalled from IEEE 802.11i's Annex H.2 (each key the previous tag), not checked against a published copy (README.md)
421	law michael_vector_5:
422	  {Result.map(&2, &2, Hs.HsError, Hs.HsW2, B.Octets, k => MI.HsMichael.mic(k, B.Octets.of_string("Mich")), MI.HsMichael.key(B.Octets.of_list([144, 3, 143, 198, 207, 19, 193, 219]))) == Done{B.Octets.of_list([213, 94, 16, 5, 16, 18, 137, 134])} : Result<&2, &2, Hs.HsError, B.Octets>}
423	
424	# Michael (IEEE 802.11i): test vector 6 as recalled from IEEE 802.11i's Annex H.2 (each key the previous tag), not checked against a published copy (README.md)
425	law michael_vector_6:
426	  {Result.map(&2, &2, Hs.HsError, Hs.HsW2, B.Octets, k => MI.HsMichael.mic(k, B.Octets.of_string("Michael")), MI.HsMichael.key(B.Octets.of_list([213, 94, 16, 5, 16, 18, 137, 134]))) == Done{B.Octets.of_list([10, 148, 43, 18, 78, 202, 165, 70])} : Result<&2, &2, Hs.HsError, B.Octets>}
427	
428	# Michael (IEEE 802.11i): IEEE Std 802.11-2012, M.6.3 (the TKIP test vector, as hostap's BSD-licensed wlantest/test_vectors.c reproduces it): the MIC of its MSDU (DA, SA, priority 0 and three zero bytes, then the data) under TK bytes 16 to 23
429	law michael_tkip_m63:
430	  {Result.map(&2, &2, Hs.HsError, Hs.HsW2, B.Octets, k => MI.HsMichael.mic(k, B.Octets.of_list([2, 3, 4, 5, 6, 8, 2, 3, 4, 5, 6, 7, 0, 0, 0, 0, 170, 170, 3, 0, 0, 0, 8, 0, 69, 0, 0, 84, 0, 0, 64, 0, 64, 1, 165, 85, 192, 168, 10, 2, 192, 168, 10, 1, 8, 0, 58, 176, 0, 0, 0, 0, 205, 76, 5, 0, 0, 0, 0, 0, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55])), MI.HsMichael.key(B.Octets.of_list([52, 86, 120, 144, 18, 52, 86, 120]))) == Done{B.Octets.of_list([104, 129, 163, 243, 214, 72, 208, 60])} : Result<&2, &2, Hs.HsError, B.Octets>}