def sp.tail_masked
bend-osdev-mode-core@0.1.0.0 · PROOF.bend:352
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
352
353def sp.tail_masked(ys: List<&2, U32>) -> {B.mask(M.cm.split.tail(M.cm.split(B.mask(ys)))) == M.cm.split.tail(M.cm.split(B.mask(ys))) : List<&2, U32>}:
354 match ys:
355 case Nil{}:
356 li.mask_mask(Nil{})
357 case Con{+y0, +r0}:
358 match r0:
359 case Nil{}:
360 li.mask_mask(Con{y0, Nil{}})
361 case Con{+y1, +r1}:
362 match r1:
363 case Nil{}:
364 li.mask_mask(Con{y0, Con{y1, Nil{}}})
365 case Con{+y2, +r2}:
366 match r2:
367 case Nil{}:
368 li.mask_mask(Con{y0, Con{y1, Con{y2, Nil{}}}})
369 case Con{+y3, +r3}:
370 match r3:
371 case Nil{}:
372 li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Nil{}}}}})
373 case Con{+y4, +r4}:
374 match r4:
375 case Nil{}:
376 li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Nil{}}}}}})
377 case Con{+y5, +r5}:
378 match r5:
379 case Nil{}:
380 li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Nil{}}}}}}})
381 case Con{+y6, +r6}:
382 match r6:
383 case Nil{}:
384 li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Nil{}}}}}}}})
385 case Con{+y7, +r7}:
386 match r7:
387 case Nil{}:
388 li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Nil{}}}}}}}}})
389 case Con{+y8, +r8}:
390 match r8:
391 case Nil{}:
392 li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Nil{}}}}}}}}}})
393 case Con{+y9, +r9}:
394 match r9:
395 case Nil{}:
396 li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Nil{}}}}}}}}}}})
397 case Con{+y10, +r10}:
398 match r10:
399 case Nil{}:
400 li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Nil{}}}}}}}}}}}})
401 case Con{+y11, +r11}:
402 match r11:
403 case Nil{}:
404 li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Con{y11, Nil{}}}}}}}}}}}}})
405 case Con{+y12, +r12}:
406 match r12:
407 case Nil{}:
408 li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Con{y11, Con{y12, Nil{}}}}}}}}}}}}}})
409 case Con{+y13, +r13}:
410 match r13:
411 case Nil{}:
412 li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Con{y11, Con{y12, Con{y13, Nil{}}}}}}}}}}}}}}})
413 case Con{+y14, +r14}:
414 match r14:
415 case Nil{}:
416 li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Con{y11, Con{y12, Con{y13, Con{y14, Nil{}}}}}}}}}}}}}}}})
417 case Con{+y15, +t}:
418 %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)))) : {B.mask(_) == _ : List<&2, U32>}
419 sp.tail_masked(t)