def sp.mod_tail
bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:408
import bend-osdev-cipher-modes@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
408
409def sp.mod_tail(ys: List<&2, U32>) -> {Nat.mod(B.len(ys), 16n) == 0n : Nat} -> {M.cm.split.tail(M.cm.split(B.mask(ys))) == Nil{} : List<&2, U32>}:
410 match ys:
411 case Nil{}:
412 h => {==}
413 case Con{+y0, +r0}:
414 match r0:
415 case Nil{}:
416 h => sp.absurd_tail(0n, Con{y0, Nil{}}, h)
417 case Con{+y1, +r1}:
418 match r1:
419 case Nil{}:
420 h => sp.absurd_tail(1n, Con{y0, Con{y1, Nil{}}}, h)
421 case Con{+y2, +r2}:
422 match r2:
423 case Nil{}:
424 h => sp.absurd_tail(2n, Con{y0, Con{y1, Con{y2, Nil{}}}}, h)
425 case Con{+y3, +r3}:
426 match r3:
427 case Nil{}:
428 h => sp.absurd_tail(3n, Con{y0, Con{y1, Con{y2, Con{y3, Nil{}}}}}, h)
429 case Con{+y4, +r4}:
430 match r4:
431 case Nil{}:
432 h => sp.absurd_tail(4n, Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Nil{}}}}}}, h)
433 case Con{+y5, +r5}:
434 match r5:
435 case Nil{}:
436 h => sp.absurd_tail(5n, Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Nil{}}}}}}}, h)
437 case Con{+y6, +r6}:
438 match r6:
439 case Nil{}:
440 h => sp.absurd_tail(6n, Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Nil{}}}}}}}}, h)
441 case Con{+y7, +r7}:
442 match r7:
443 case Nil{}:
444 h => sp.absurd_tail(7n, Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Nil{}}}}}}}}}, h)
445 case Con{+y8, +r8}:
446 match r8:
447 case Nil{}:
448 h => sp.absurd_tail(8n, Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Nil{}}}}}}}}}}, h)
449 case Con{+y9, +r9}:
450 match r9:
451 case Nil{}:
452 h => sp.absurd_tail(9n, Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Nil{}}}}}}}}}}}, h)
453 case Con{+y10, +r10}:
454 match r10:
455 case Nil{}:
456 h => sp.absurd_tail(10n, Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Nil{}}}}}}}}}}}}, h)
457 case Con{+y11, +r11}:
458 match r11:
459 case Nil{}:
460 h => sp.absurd_tail(11n, 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{}}}}}}}}}}}}}, h)
461 case Con{+y12, +r12}:
462 match r12:
463 case Nil{}:
464 h => sp.absurd_tail(12n, 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{}}}}}}}}}}}}}}, h)
465 case Con{+y13, +r13}:
466 match r13:
467 case Nil{}:
468 h => sp.absurd_tail(13n, 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{}}}}}}}}}}}}}}}, h)
469 case Con{+y14, +r14}:
470 match r14:
471 case Nil{}:
472 h => sp.absurd_tail(14n, 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{}}}}}}}}}}}}}}}}, h)
473 case Con{+y15, +t}:
474 h => %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)))) : {_ == Nil{} : List<&2, U32>}
475 sp.mod_tail(t)(Equal.trans(Nat, Nat.mod(B.len(t), 16n), Nat.mod(Nat.add(16n, B.len(t)), 16n), 0n, Equal.sym(Nat, Nat.mod(Nat.add(16n, B.len(t)), 16n), Nat.mod(B.len(t), 16n), sp.mod16(B.len(t))), h))