def xtsp.ppY
bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:1516
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
1516def 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>}:
1517 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))