1	# Generated by gen/laws.py; do not edit by hand.
2	import Base
3	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
4	import ./hashes.bend as Hs
5	import ./md4.bend as M4
6	import ./md5.bend as M5
7	import ./sha1.bend as S1
8	import ./ripemd160.bend as RM
9	import ./sm3.bend as SM
10	import ./streebog.bend as ST
11	import ./michael.bend as MI
12	import bend-osdev-bytes@0.1.0.0/LAWS.bend as BL
13	import bend-osdev-bytes@0.1.0.0/PROOF.bend as BP
14	import ./LAWS.bend as Laws
15	
16	# The engine: feeding xs ++ ys is feeding xs, then ys (induction on xs)
17	def 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	
24	def 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	# Lengths: an Octets made from a list has the list's length; the bytes of
29	# a chaining value are a list of fixed shape whatever its words are
30	def 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	
38	def 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	
43	def 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	
48	def 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	
54	def 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	
59	def 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	
65	def 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	
70	def 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	
76	def 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	
81	def 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	
87	def 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	
92	def 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	
98	def 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	
103	def 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	
109	def 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	
114	def 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	
120	def Laws.md4_streaming(s, a, b):
121	  Laws.md_streaming(~Hs.HsW4, ~M4.HsMd4.compress, ~63, s, a, b)
122	
123	def 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	
127	def 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	
132	def 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	
135	def Laws.md4_digest_length(m):
136	  Laws.md4_length(M4.HsMd4.update(M4.HsMd4.init(), m))
137	
138	def Laws.md4_rfc1320_1():
139	  {==}
140	
141	def Laws.md4_rfc1320_2():
142	  {==}
143	
144	def Laws.md4_rfc1320_3():
145	  {==}
146	
147	def Laws.md4_rfc1320_4():
148	  {==}
149	
150	def Laws.md4_rfc1320_5():
151	  {==}
152	
153	def Laws.md4_rfc1320_6():
154	  {==}
155	
156	def Laws.md4_rfc1320_7():
157	  {==}
158	
159	def Laws.md5_streaming(s, a, b):
160	  Laws.md_streaming(~Hs.HsW4, ~M5.HsMd5.compress, ~63, s, a, b)
161	
162	def 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	
166	def 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	
171	def 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	
174	def Laws.md5_digest_length(m):
175	  Laws.md5_length(M5.HsMd5.update(M5.HsMd5.init(), m))
176	
177	def Laws.md5_rfc1321_1():
178	  {==}
179	
180	def Laws.md5_rfc1321_2():
181	  {==}
182	
183	def Laws.md5_rfc1321_3():
184	  {==}
185	
186	def Laws.md5_rfc1321_4():
187	  {==}
188	
189	def Laws.md5_rfc1321_5():
190	  {==}
191	
192	def Laws.md5_rfc1321_6():
193	  {==}
194	
195	def Laws.md5_rfc1321_7():
196	  {==}
197	
198	def Laws.sha1_streaming(s, a, b):
199	  Laws.md_streaming(~Hs.HsW5, ~S1.HsSha1.compress, ~63, s, a, b)
200	
201	def 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	
205	def 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	
210	def 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	
213	def Laws.sha1_digest_length(m):
214	  Laws.sha1_length(S1.HsSha1.update(S1.HsSha1.init(), m))
215	
216	def Laws.sha1_fips_1():
217	  {==}
218	
219	def Laws.sha1_fips_2():
220	  {==}
221	
222	def Laws.ripemd160_streaming(s, a, b):
223	  Laws.md_streaming(~Hs.HsW5, ~RM.HsRipemd160.compress, ~63, s, a, b)
224	
225	def 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	
229	def 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	
234	def 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	
237	def Laws.ripemd160_digest_length(m):
238	  Laws.ripemd160_length(RM.HsRipemd160.update(RM.HsRipemd160.init(), m))
239	
240	def Laws.ripemd160_paper_1():
241	  {==}
242	
243	def Laws.ripemd160_paper_2():
244	  {==}
245	
246	def Laws.ripemd160_paper_3():
247	  {==}
248	
249	def Laws.ripemd160_paper_4():
250	  {==}
251	
252	def Laws.ripemd160_paper_5():
253	  {==}
254	
255	def Laws.ripemd160_paper_6():
256	  {==}
257	
258	def Laws.ripemd160_paper_7():
259	  {==}
260	
261	def Laws.ripemd160_paper_8():
262	  {==}
263	
264	def Laws.sm3_streaming(s, a, b):
265	  Laws.md_streaming(~Hs.HsW8, ~SM.HsSm3.compress, ~63, s, a, b)
266	
267	def 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	
271	def 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	
276	def 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	
279	def Laws.sm3_digest_length(m):
280	  Laws.sm3_length(SM.HsSm3.update(SM.HsSm3.init(), m))
281	
282	def Laws.sm3_example_1():
283	  {==}
284	
285	def Laws.sm3_example_2():
286	  {==}
287	
288	def Laws.streebog512_streaming(s, a, b):
289	  Laws.md_streaming(~ST.HsStbCv, ~ST.HsStreebog.compress, ~63, s, a, b)
290	
291	def 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	
295	def 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	
300	def Laws.streebog512_length(s):
301	  stb512_len(ST.hs.stb.finish(s))
302	
303	def Laws.streebog512_digest_length(m):
304	  Laws.streebog512_length(ST.HsStreebog.update(ST.HsStreebog.init512(), m))
305	
306	def Laws.streebog256_streaming(s, a, b):
307	  Laws.md_streaming(~ST.HsStbCv, ~ST.HsStreebog.compress, ~63, s, a, b)
308	
309	def 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	
313	def 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	
318	def Laws.streebog256_length(s):
319	  stb256_len(ST.hs.stb.finish(s))
320	
321	def Laws.streebog256_digest_length(m):
322	  Laws.streebog256_length(ST.HsStreebog.update(ST.HsStreebog.init256(), m))
323	
324	def Laws.streebog_lps_zero():
325	  {==}
326	
327	def Laws.streebog_g_example1():
328	  {==}
329	
330	def Laws.streebog_g0_example1():
331	  {==}
332	
333	def Laws.michael_streaming(s, a, b):
334	  Laws.md_streaming(~Hs.HsW2, ~MI.HsMichael.compress, ~3, s, a, b)
335	
336	def 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	
340	def 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	
343	def Laws.michael_mic_length(k, m):
344	  Laws.michael_length(MI.HsMichael.update(MI.HsMichael.init(k), m))
345	
346	def Laws.michael_short_key():
347	  {==}
348	
349	def Laws.michael_vector_1():
350	  {==}
351	
352	def Laws.michael_vector_2():
353	  {==}
354	
355	def Laws.michael_vector_3():
356	  {==}
357	
358	def Laws.michael_vector_4():
359	  {==}
360	
361	def Laws.michael_vector_5():
362	  {==}
363	
364	def Laws.michael_vector_6():
365	  {==}
366	
367	def Laws.michael_tkip_m63():
368	  {==}