def sp.join_split
bend-osdev-mode-core@0.1.0.0 · PROOF.bend:206
import bend-osdev-mode-core@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
206
207def sp.join_split(ys: List<&2, U32>) -> {M.cm.join_onto(M.cm.split.blocks(M.cm.split(B.mask(ys))), M.cm.split.tail(M.cm.split(B.mask(ys)))) == B.mask(ys) : List<&2, U32>}:
208 match ys:
209 case Nil{}:
210 {==}
211 case Con{+y0, +r0}:
212 match r0:
213 case Nil{}:
214 {==}
215 case Con{+y1, +r1}:
216 match r1:
217 case Nil{}:
218 {==}
219 case Con{+y2, +r2}:
220 match r2:
221 case Nil{}:
222 {==}
223 case Con{+y3, +r3}:
224 match r3:
225 case Nil{}:
226 {==}
227 case Con{+y4, +r4}:
228 match r4:
229 case Nil{}:
230 {==}
231 case Con{+y5, +r5}:
232 match r5:
233 case Nil{}:
234 {==}
235 case Con{+y6, +r6}:
236 match r6:
237 case Nil{}:
238 {==}
239 case Con{+y7, +r7}:
240 match r7:
241 case Nil{}:
242 {==}
243 case Con{+y8, +r8}:
244 match r8:
245 case Nil{}:
246 {==}
247 case Con{+y9, +r9}:
248 match r9:
249 case Nil{}:
250 {==}
251 case Con{+y10, +r10}:
252 match r10:
253 case Nil{}:
254 {==}
255 case Con{+y11, +r11}:
256 match r11:
257 case Nil{}:
258 {==}
259 case Con{+y12, +r12}:
260 match r12:
261 case Nil{}:
262 {==}
263 case Con{+y13, +r13}:
264 match r13:
265 case Nil{}:
266 {==}
267 case Con{+y14, +r14}:
268 match r14:
269 case Nil{}:
270 {==}
271 case Con{+y15, +t}:
272 %Equal.sym(List<&2, M.CmBlock>, M.cm.split.blocks(M.cm.split.cons(M.cm.block16(B.byte(y0), B.byte(y1), B.byte(y2), B.byte(y3), B.byte(y4), B.byte(y5), B.byte(y6), B.byte(y7), B.byte(y8), B.byte(y9), B.byte(y10), B.byte(y11), B.byte(y12), B.byte(y13), B.byte(y14), B.byte(y15)), M.cm.split(B.mask(t)))), Con{M.cm.block16(B.byte(y0), B.byte(y1), B.byte(y2), B.byte(y3), B.byte(y4), B.byte(y5), B.byte(y6), B.byte(y7), B.byte(y8), B.byte(y9), B.byte(y10), B.byte(y11), B.byte(y12), B.byte(y13), B.byte(y14), B.byte(y15)), M.cm.split.blocks(M.cm.split(B.mask(t)))}, sp.cons_blocks(M.cm.block16(B.byte(y0), B.byte(y1), B.byte(y2), B.byte(y3), B.byte(y4), B.byte(y5), B.byte(y6), B.byte(y7), B.byte(y8), B.byte(y9), B.byte(y10), B.byte(y11), B.byte(y12), B.byte(y13), B.byte(y14), B.byte(y15)), M.cm.split(B.mask(t)))) : {M.cm.join_onto(_, M.cm.split.tail(M.cm.split.cons(M.cm.block16(B.byte(y0), B.byte(y1), B.byte(y2), B.byte(y3), B.byte(y4), B.byte(y5), B.byte(y6), B.byte(y7), B.byte(y8), B.byte(y9), B.byte(y10), B.byte(y11), B.byte(y12), B.byte(y13), B.byte(y14), B.byte(y15)), M.cm.split(B.mask(t))))) == Con{B.byte(y0), Con{B.byte(y1), Con{B.byte(y2), Con{B.byte(y3), Con{B.byte(y4), Con{B.byte(y5), Con{B.byte(y6), Con{B.byte(y7), Con{B.byte(y8), Con{B.byte(y9), Con{B.byte(y10), Con{B.byte(y11), Con{B.byte(y12), Con{B.byte(y13), Con{B.byte(y14), Con{B.byte(y15), B.mask(t)}}}}}}}}}}}}}}}} : List<&2, U32>}
273 %Equal.sym(List<&2, U32>, M.cm.split.tail(M.cm.split.cons(M.cm.block16(B.byte(y0), B.byte(y1), B.byte(y2), B.byte(y3), B.byte(y4), B.byte(y5), B.byte(y6), B.byte(y7), B.byte(y8), B.byte(y9), B.byte(y10), B.byte(y11), B.byte(y12), B.byte(y13), B.byte(y14), B.byte(y15)), M.cm.split(B.mask(t)))), M.cm.split.tail(M.cm.split(B.mask(t))), sp.cons_tail(M.cm.block16(B.byte(y0), B.byte(y1), B.byte(y2), B.byte(y3), B.byte(y4), B.byte(y5), B.byte(y6), B.byte(y7), B.byte(y8), B.byte(y9), B.byte(y10), B.byte(y11), B.byte(y12), B.byte(y13), B.byte(y14), B.byte(y15)), M.cm.split(B.mask(t)))) : {M.cm.join_onto(Con{M.cm.block16(B.byte(y0), B.byte(y1), B.byte(y2), B.byte(y3), B.byte(y4), B.byte(y5), B.byte(y6), B.byte(y7), B.byte(y8), B.byte(y9), B.byte(y10), B.byte(y11), B.byte(y12), B.byte(y13), B.byte(y14), B.byte(y15)), M.cm.split.blocks(M.cm.split(B.mask(t)))}, _) == Con{B.byte(y0), Con{B.byte(y1), Con{B.byte(y2), Con{B.byte(y3), Con{B.byte(y4), Con{B.byte(y5), Con{B.byte(y6), Con{B.byte(y7), Con{B.byte(y8), Con{B.byte(y9), Con{B.byte(y10), Con{B.byte(y11), Con{B.byte(y12), Con{B.byte(y13), Con{B.byte(y14), Con{B.byte(y15), B.mask(t)}}}}}}}}}}}}}}}} : List<&2, U32>}
274 %Equal.sym(List<&2, U32>, M.cm.join_onto(M.cm.split.blocks(M.cm.split(B.mask(t))), M.cm.split.tail(M.cm.split(B.mask(t)))), B.mask(t), sp.join_split(t)) : {M.cm.bytes_onto(M.cm.block16(B.byte(y0), B.byte(y1), B.byte(y2), B.byte(y3), B.byte(y4), B.byte(y5), B.byte(y6), B.byte(y7), B.byte(y8), B.byte(y9), B.byte(y10), B.byte(y11), B.byte(y12), B.byte(y13), B.byte(y14), B.byte(y15)), _) == Con{B.byte(y0), Con{B.byte(y1), Con{B.byte(y2), Con{B.byte(y3), Con{B.byte(y4), Con{B.byte(y5), Con{B.byte(y6), Con{B.byte(y7), Con{B.byte(y8), Con{B.byte(y9), Con{B.byte(y10), Con{B.byte(y11), Con{B.byte(y12), Con{B.byte(y13), Con{B.byte(y14), Con{B.byte(y15), B.mask(t)}}}}}}}}}}}}}}}} : List<&2, U32>}
275 sp.blk16(y0, y1, y2, y3, y4, y5, y6, y7, y8, y9, y10, y11, y12, y13, y14, y15, B.mask(t))