def bx.rblock

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

import Base
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M

1361def bx.rblock(+a: M.CmBlock, +b: M.CmBlock) -> {M.CmBlock.xor(M.CmBlock.xor(a, b), b) == a : M.CmBlock}:
1362  match a b:
1363    case M.CmBlock{a0, a1, a2, a3} M.CmBlock{b0, b1, b2, b3}:
1364      %bx.ru32(a0, b0) : {M.CmBlock.xor(M.CmBlock.xor(M.CmBlock{a0, a1, a2, a3}, M.CmBlock{b0, b1, b2, b3}), M.CmBlock{b0, b1, b2, b3}) == M.CmBlock{_, a1, a2, a3} : M.CmBlock}
1365      %bx.ru32(a1, b1) : {M.CmBlock.xor(M.CmBlock.xor(M.CmBlock{a0, a1, a2, a3}, M.CmBlock{b0, b1, b2, b3}), M.CmBlock{b0, b1, b2, b3}) == M.CmBlock{U32.xor(U32.xor(a0, b0), b0), _, a2, a3} : M.CmBlock}
1366      %bx.ru32(a2, b2) : {M.CmBlock.xor(M.CmBlock.xor(M.CmBlock{a0, a1, a2, a3}, M.CmBlock{b0, b1, b2, b3}), M.CmBlock{b0, b1, b2, b3}) == M.CmBlock{U32.xor(U32.xor(a0, b0), b0), U32.xor(U32.xor(a1, b1), b1), _, a3} : M.CmBlock}
1367      %bx.ru32(a3, b3) : {M.CmBlock.xor(M.CmBlock.xor(M.CmBlock{a0, a1, a2, a3}, M.CmBlock{b0, b1, b2, b3}), M.CmBlock{b0, b1, b2, b3}) == M.CmBlock{U32.xor(U32.xor(a0, b0), b0), U32.xor(U32.xor(a1, b1), b1), U32.xor(U32.xor(a2, b2), b2), _} : M.CmBlock}
1368      {==}