PROOF.xtsp.steal: 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 1519-1536 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=1519&end_line=1536

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-bytes@0.1.0.0/LAWS.bend as BL
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
import bend-osdev-cipher-modes@0.1.0.0/xts.bend as T

# Ciphertext stealing undoes itself: the last whole block p and a tail tl
# (masked, fewer than 16 bytes), encrypted by steal_c and steal_t and
# decrypted by dsteal, come back as p's bytes and then tl
def xtsp.steal(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, ~dec: K -> M.CmBlock -> M.CmBlock, ~inv: @k: K -> @b: M.CmBlock -> {dec(k, enc(k, b)) == b : M.CmBlock}, +k: K, +p: M.CmBlock, tl: List<&2, U32>, +t: M.CmBlock) -> {B.mask(tl) == tl : List<&2, U32>} -> {Nat.is_lt(B.len(tl), 16n) == True{} : Bool} -> {T.xts.dsteal(~K, ~dec, k, T.xts.steal_c(~K, ~enc, k, p, tl, t), T.xts.steal_t(~K, ~enc, k, p, tl, t), t) == M.cm.bytes_onto(p, tl) : List<&2, U32>}:
  match tl:
    case Nil{}:
      hm => hl => %Equal.sym(M.CmBlock, T.xts.bdec(~K, ~dec, k, T.xts.benc(~K, ~enc, k, p, t), t), p, xtsp.blk(~K, ~enc, ~dec, ~inv, k, p, t)) : {M.cm.bytes_of(_) == M.cm.bytes_onto(p, Nil{}) : List<&2, U32>}
        {==}
    case Con{+h, +r}:
      +hm => +hl => %Equal.sym(M.CmBlock, T.xts.bdec(~K, ~dec, k, T.xts.benc(~K, ~enc, k, M.cm.block_of(B.append(Con{h, r}, B.drop(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))))), T.Xts.mul_alpha(t)), T.Xts.mul_alpha(t)), M.cm.block_of(B.append(Con{h, r}, B.drop(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))))), xtsp.blk(~K, ~enc, ~dec, ~inv, k, M.cm.block_of(B.append(Con{h, r}, B.drop(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))))), T.Xts.mul_alpha(t))) : {M.cm.bytes_onto(T.xts.bdec(~K, ~dec, k, M.cm.block_of(B.append(B.take(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))), B.drop(B.len(B.take(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t)))), M.cm.bytes_of(_)))), t), B.take(B.len(B.take(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t)))), M.cm.bytes_of(_))) == M.cm.bytes_onto(p, Con{h, r}) : List<&2, U32>}
              %Equal.sym(Nat, B.len(B.take(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t)))), B.len(Con{h, r}), li.len_take(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t)))(na.lt_le(B.len(Con{h, r}), 16n)(hl))) : {M.cm.bytes_onto(T.xts.bdec(~K, ~dec, k, M.cm.block_of(B.append(B.take(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))), B.drop(_, M.cm.bytes_of(M.cm.block_of(B.append(Con{h, r}, B.drop(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))))))))), t), B.take(_, M.cm.bytes_of(M.cm.block_of(B.append(Con{h, r}, B.drop(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t)))))))) == M.cm.bytes_onto(p, Con{h, r}) : List<&2, U32>}
              %Equal.sym(List<&2, U32>, M.cm.bytes_of(M.cm.block_of(B.append(Con{h, r}, B.drop(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t)))))), B.append(Con{h, r}, B.drop(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t)))), xtsp.ppY(Con{h, r}, T.xts.benc(~K, ~enc, k, p, t), hm, hl)) : {M.cm.bytes_onto(T.xts.bdec(~K, ~dec, k, M.cm.block_of(B.append(B.take(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))), B.drop(B.len(Con{h, r}), _))), t), B.take(B.len(Con{h, r}), _)) == M.cm.bytes_onto(p, Con{h, r}) : List<&2, U32>}
              %Equal.sym(List<&2, U32>, B.take(B.len(Con{h, r}), B.append(Con{h, r}, B.drop(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))))), Con{h, r}, li.take_append(Con{h, r}, B.drop(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))))) : {M.cm.bytes_onto(T.xts.bdec(~K, ~dec, k, M.cm.block_of(B.append(B.take(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))), B.drop(B.len(Con{h, r}), B.append(Con{h, r}, B.drop(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))))))), t), _) == M.cm.bytes_onto(p, Con{h, r}) : List<&2, U32>}
              %Equal.sym(List<&2, U32>, B.drop(B.len(Con{h, r}), B.append(Con{h, r}, B.drop(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))))), B.drop(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))), li.drop_append(Con{h, r}, B.drop(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))))) : {M.cm.bytes_onto(T.xts.bdec(~K, ~dec, k, M.cm.block_of(B.append(B.take(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))), _)), t), Con{h, r}) == M.cm.bytes_onto(p, Con{h, r}) : List<&2, U32>}
              %Equal.sym(List<&2, U32>, B.append(B.take(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))), B.drop(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t)))), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t)), BL.take_drop(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t)))) : {M.cm.bytes_onto(T.xts.bdec(~K, ~dec, k, M.cm.block_of(_), t), Con{h, r}) == M.cm.bytes_onto(p, Con{h, r}) : List<&2, U32>}
              %Equal.sym(M.CmBlock, M.cm.block_of(M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))), T.xts.benc(~K, ~enc, k, p, t), sp.block_bytes(T.xts.benc(~K, ~enc, k, p, t))) : {M.cm.bytes_onto(T.xts.bdec(~K, ~dec, k, _, t), Con{h, r}) == M.cm.bytes_onto(p, Con{h, r}) : List<&2, U32>}
              %Equal.sym(M.CmBlock, T.xts.bdec(~K, ~dec, k, T.xts.benc(~K, ~enc, k, p, t), t), p, xtsp.blk(~K, ~enc, ~dec, ~inv, k, p, t)) : {M.cm.bytes_onto(_, Con{h, r}) == M.cm.bytes_onto(p, Con{h, r}) : List<&2, U32>}
        {==}

Uses (29):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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/LAWS.bend&name=take_drop
  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-bytes@0.1.1.0/bytes.bend&name=take
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=li.drop_append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=li.len_take
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=li.take_append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=na.lt_le
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=sp.block_bytes
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=xtsp.blk
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=xtsp.ppY
  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
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend&name=cm.bytes_onto
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/xts.bend&name=Xts.mul_alpha
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/xts.bend&name=xts.bdec
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/xts.bend&name=xts.benc
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/xts.bend&name=xts.dsteal
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/xts.bend&name=xts.steal_c
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/xts.bend&name=xts.steal_t