PROOF.xtsp.ppY: def of bend-osdev-cipher-modes@0.1.0.0
Import: import bend-osdev-cipher-modes@0.1.0.0/PROOF.bend as PROOF
Lines 1516-1517 of bend-osdev-cipher-modes@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&start_line=1516&end_line=1517

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

def xtsp.ppY(+tl: List<&2, U32>, +b: M.CmBlock, hm: {B.mask(tl) == tl : List<&2, U32>}, hl: {Nat.is_lt(B.len(tl), 16n) == True{} : Bool}) -> {M.cm.bytes_of(M.cm.block_of(B.append(tl, B.drop(B.len(tl), M.cm.bytes_of(b))))) == B.append(tl, B.drop(B.len(tl), M.cm.bytes_of(b))) : List<&2, U32>}:
  Equal.trans(List<&2, U32>, M.cm.bytes_of(M.cm.block_of(B.append(tl, B.drop(B.len(tl), M.cm.bytes_of(b))))), B.mask(B.append(tl, B.drop(B.len(tl), M.cm.bytes_of(b)))), B.append(tl, B.drop(B.len(tl), M.cm.bytes_of(b))), sp.bb16(B.append(tl, B.drop(B.len(tl), M.cm.bytes_of(b))))(xtsp.len16(tl, b, hl)), xtsp.maskY(tl, b, hm))

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=drop
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=len
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=mask
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=sp.bb16
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=xtsp.len16
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=xtsp.maskY
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend&name=CmBlock
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend&name=cm.block_of
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend&name=cm.bytes_of