def xtsp.mask_steal_t

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

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

1481# the final partial ciphertext block is masked, and splits into no blocks
1482def xtsp.mask_steal_t(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +p: M.CmBlock, tl: List<&2, U32>, +t: M.CmBlock) -> {B.mask(T.xts.steal_t(~K, ~enc, k, p, tl, t)) == T.xts.steal_t(~K, ~enc, k, p, tl, t) : List<&2, U32>}:
1483  match tl:
1484    case Nil{}:
1485      {==}
1486    case Con{+h, +r}:
1487      %Equal.sym(List<&2, U32>, B.mask(B.take(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t)))), B.take(B.len(Con{h, r}), B.mask(M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t)))), li.mask_take(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t)))) : {_ == B.take(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))) : List<&2, U32>}
1488      %Equal.sym(List<&2, U32>, B.mask(M.cm.bytes_onto(T.xts.benc(~K, ~enc, k, p, t), Nil{})), M.cm.bytes_onto(T.xts.benc(~K, ~enc, k, p, t), B.mask(Nil{})), sp.mask_blk(T.xts.benc(~K, ~enc, k, p, t), Nil{})) : {B.take(B.len(Con{h, r}), _) == B.take(B.len(Con{h, r}), M.cm.bytes_of(T.xts.benc(~K, ~enc, k, p, t))) : List<&2, U32>}
1489      {==}