def xtsp.tweak

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:1477

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

1477def 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>}:
1478  %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>}
1479  {==}