PROOF.xtsp.tweak: 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 1477-1479 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=1477&end_line=1479

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
import bend-osdev-cipher-modes@0.1.0.0/xts.bend as T

def xtsp.tweak(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k2: K, +i: B.Octets, h: {B.Octets.len(i) == 16n : Nat}) -> {T.xts.tweak(~K, ~enc, k2, i) == Done{enc(k2, M.cm.block_of(B.Octets.to_list(i)))} : Result<&2, &2, M.CmError, M.CmBlock>}:
  %Equal.sym(Nat, B.len(B.Octets.to_list(i)), 16n, oc.len(i, 16n, h)) : {T.xts.tweak.go(~K, ~enc, k2, M.cm.need_block.pick(Nat.is_eq(_, 16n), B.Octets.to_list(i), M.CmBadTweakLength{B.len(B.Octets.to_list(i))})) == Done{enc(k2, M.cm.block_of(B.Octets.to_list(i)))} : Result<&2, &2, M.CmError, M.CmBlock>}
  {==}

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.len
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.to_list
  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-cipher-modes@0.1.0.0/PROOF.bend&name=oc.len
  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=CmError
  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.need_block.pick
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/xts.bend&name=xts.tweak
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/xts.bend&name=xts.tweak.go