PROOF.aria_xor2: def of bend-osdev-legacy-ciphers@0.1.0.0
Import: import bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend as PROOF
Lines 7915-7935 of bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&start_line=7915&end_line=7935

import Base
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
import bend-osdev-legacy-ciphers@0.1.0.0/aria.bend as A

# a round key XORed twice
def aria_xor2(s: A.LcAriaSt, k: M.CmBlock) -> {s == A.aria.xor(A.aria.xor(s, k), k) : A.LcAriaSt}:
  match s k:
    case A.LcAriaSt{+x0, +x1, +x2, +x3, +x4, +x5, +x6, +x7, +x8, +x9, +x10, +x11, +x12, +x13, +x14, +x15} M.CmBlock{U32{+k0}, U32{+k1}, U32{+k2}, U32{+k3}}:
      %word_xx(8n, x0, A.aria.byte0(k0)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{_, Word.xor(8n, Word.xor(8n, x1, A.aria.byte1(k0)), A.aria.byte1(k0)), Word.xor(8n, Word.xor(8n, x2, A.aria.byte2(k0)), A.aria.byte2(k0)), Word.xor(8n, Word.xor(8n, x3, A.aria.byte3(k0)), A.aria.byte3(k0)), Word.xor(8n, Word.xor(8n, x4, A.aria.byte0(k1)), A.aria.byte0(k1)), Word.xor(8n, Word.xor(8n, x5, A.aria.byte1(k1)), A.aria.byte1(k1)), Word.xor(8n, Word.xor(8n, x6, A.aria.byte2(k1)), A.aria.byte2(k1)), Word.xor(8n, Word.xor(8n, x7, A.aria.byte3(k1)), A.aria.byte3(k1)), Word.xor(8n, Word.xor(8n, x8, A.aria.byte0(k2)), A.aria.byte0(k2)), Word.xor(8n, Word.xor(8n, x9, A.aria.byte1(k2)), A.aria.byte1(k2)), Word.xor(8n, Word.xor(8n, x10, A.aria.byte2(k2)), A.aria.byte2(k2)), Word.xor(8n, Word.xor(8n, x11, A.aria.byte3(k2)), A.aria.byte3(k2)), Word.xor(8n, Word.xor(8n, x12, A.aria.byte0(k3)), A.aria.byte0(k3)), Word.xor(8n, Word.xor(8n, x13, A.aria.byte1(k3)), A.aria.byte1(k3)), Word.xor(8n, Word.xor(8n, x14, A.aria.byte2(k3)), A.aria.byte2(k3)), Word.xor(8n, Word.xor(8n, x15, A.aria.byte3(k3)), A.aria.byte3(k3))} : A.LcAriaSt}
      %word_xx(8n, x1, A.aria.byte1(k0)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{x0, _, Word.xor(8n, Word.xor(8n, x2, A.aria.byte2(k0)), A.aria.byte2(k0)), Word.xor(8n, Word.xor(8n, x3, A.aria.byte3(k0)), A.aria.byte3(k0)), Word.xor(8n, Word.xor(8n, x4, A.aria.byte0(k1)), A.aria.byte0(k1)), Word.xor(8n, Word.xor(8n, x5, A.aria.byte1(k1)), A.aria.byte1(k1)), Word.xor(8n, Word.xor(8n, x6, A.aria.byte2(k1)), A.aria.byte2(k1)), Word.xor(8n, Word.xor(8n, x7, A.aria.byte3(k1)), A.aria.byte3(k1)), Word.xor(8n, Word.xor(8n, x8, A.aria.byte0(k2)), A.aria.byte0(k2)), Word.xor(8n, Word.xor(8n, x9, A.aria.byte1(k2)), A.aria.byte1(k2)), Word.xor(8n, Word.xor(8n, x10, A.aria.byte2(k2)), A.aria.byte2(k2)), Word.xor(8n, Word.xor(8n, x11, A.aria.byte3(k2)), A.aria.byte3(k2)), Word.xor(8n, Word.xor(8n, x12, A.aria.byte0(k3)), A.aria.byte0(k3)), Word.xor(8n, Word.xor(8n, x13, A.aria.byte1(k3)), A.aria.byte1(k3)), Word.xor(8n, Word.xor(8n, x14, A.aria.byte2(k3)), A.aria.byte2(k3)), Word.xor(8n, Word.xor(8n, x15, A.aria.byte3(k3)), A.aria.byte3(k3))} : A.LcAriaSt}
      %word_xx(8n, x2, A.aria.byte2(k0)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{x0, x1, _, Word.xor(8n, Word.xor(8n, x3, A.aria.byte3(k0)), A.aria.byte3(k0)), Word.xor(8n, Word.xor(8n, x4, A.aria.byte0(k1)), A.aria.byte0(k1)), Word.xor(8n, Word.xor(8n, x5, A.aria.byte1(k1)), A.aria.byte1(k1)), Word.xor(8n, Word.xor(8n, x6, A.aria.byte2(k1)), A.aria.byte2(k1)), Word.xor(8n, Word.xor(8n, x7, A.aria.byte3(k1)), A.aria.byte3(k1)), Word.xor(8n, Word.xor(8n, x8, A.aria.byte0(k2)), A.aria.byte0(k2)), Word.xor(8n, Word.xor(8n, x9, A.aria.byte1(k2)), A.aria.byte1(k2)), Word.xor(8n, Word.xor(8n, x10, A.aria.byte2(k2)), A.aria.byte2(k2)), Word.xor(8n, Word.xor(8n, x11, A.aria.byte3(k2)), A.aria.byte3(k2)), Word.xor(8n, Word.xor(8n, x12, A.aria.byte0(k3)), A.aria.byte0(k3)), Word.xor(8n, Word.xor(8n, x13, A.aria.byte1(k3)), A.aria.byte1(k3)), Word.xor(8n, Word.xor(8n, x14, A.aria.byte2(k3)), A.aria.byte2(k3)), Word.xor(8n, Word.xor(8n, x15, A.aria.byte3(k3)), A.aria.byte3(k3))} : A.LcAriaSt}
      %word_xx(8n, x3, A.aria.byte3(k0)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{x0, x1, x2, _, Word.xor(8n, Word.xor(8n, x4, A.aria.byte0(k1)), A.aria.byte0(k1)), Word.xor(8n, Word.xor(8n, x5, A.aria.byte1(k1)), A.aria.byte1(k1)), Word.xor(8n, Word.xor(8n, x6, A.aria.byte2(k1)), A.aria.byte2(k1)), Word.xor(8n, Word.xor(8n, x7, A.aria.byte3(k1)), A.aria.byte3(k1)), Word.xor(8n, Word.xor(8n, x8, A.aria.byte0(k2)), A.aria.byte0(k2)), Word.xor(8n, Word.xor(8n, x9, A.aria.byte1(k2)), A.aria.byte1(k2)), Word.xor(8n, Word.xor(8n, x10, A.aria.byte2(k2)), A.aria.byte2(k2)), Word.xor(8n, Word.xor(8n, x11, A.aria.byte3(k2)), A.aria.byte3(k2)), Word.xor(8n, Word.xor(8n, x12, A.aria.byte0(k3)), A.aria.byte0(k3)), Word.xor(8n, Word.xor(8n, x13, A.aria.byte1(k3)), A.aria.byte1(k3)), Word.xor(8n, Word.xor(8n, x14, A.aria.byte2(k3)), A.aria.byte2(k3)), Word.xor(8n, Word.xor(8n, x15, A.aria.byte3(k3)), A.aria.byte3(k3))} : A.LcAriaSt}
      %word_xx(8n, x4, A.aria.byte0(k1)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{x0, x1, x2, x3, _, Word.xor(8n, Word.xor(8n, x5, A.aria.byte1(k1)), A.aria.byte1(k1)), Word.xor(8n, Word.xor(8n, x6, A.aria.byte2(k1)), A.aria.byte2(k1)), Word.xor(8n, Word.xor(8n, x7, A.aria.byte3(k1)), A.aria.byte3(k1)), Word.xor(8n, Word.xor(8n, x8, A.aria.byte0(k2)), A.aria.byte0(k2)), Word.xor(8n, Word.xor(8n, x9, A.aria.byte1(k2)), A.aria.byte1(k2)), Word.xor(8n, Word.xor(8n, x10, A.aria.byte2(k2)), A.aria.byte2(k2)), Word.xor(8n, Word.xor(8n, x11, A.aria.byte3(k2)), A.aria.byte3(k2)), Word.xor(8n, Word.xor(8n, x12, A.aria.byte0(k3)), A.aria.byte0(k3)), Word.xor(8n, Word.xor(8n, x13, A.aria.byte1(k3)), A.aria.byte1(k3)), Word.xor(8n, Word.xor(8n, x14, A.aria.byte2(k3)), A.aria.byte2(k3)), Word.xor(8n, Word.xor(8n, x15, A.aria.byte3(k3)), A.aria.byte3(k3))} : A.LcAriaSt}
      %word_xx(8n, x5, A.aria.byte1(k1)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{x0, x1, x2, x3, x4, _, Word.xor(8n, Word.xor(8n, x6, A.aria.byte2(k1)), A.aria.byte2(k1)), Word.xor(8n, Word.xor(8n, x7, A.aria.byte3(k1)), A.aria.byte3(k1)), Word.xor(8n, Word.xor(8n, x8, A.aria.byte0(k2)), A.aria.byte0(k2)), Word.xor(8n, Word.xor(8n, x9, A.aria.byte1(k2)), A.aria.byte1(k2)), Word.xor(8n, Word.xor(8n, x10, A.aria.byte2(k2)), A.aria.byte2(k2)), Word.xor(8n, Word.xor(8n, x11, A.aria.byte3(k2)), A.aria.byte3(k2)), Word.xor(8n, Word.xor(8n, x12, A.aria.byte0(k3)), A.aria.byte0(k3)), Word.xor(8n, Word.xor(8n, x13, A.aria.byte1(k3)), A.aria.byte1(k3)), Word.xor(8n, Word.xor(8n, x14, A.aria.byte2(k3)), A.aria.byte2(k3)), Word.xor(8n, Word.xor(8n, x15, A.aria.byte3(k3)), A.aria.byte3(k3))} : A.LcAriaSt}
      %word_xx(8n, x6, A.aria.byte2(k1)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{x0, x1, x2, x3, x4, x5, _, Word.xor(8n, Word.xor(8n, x7, A.aria.byte3(k1)), A.aria.byte3(k1)), Word.xor(8n, Word.xor(8n, x8, A.aria.byte0(k2)), A.aria.byte0(k2)), Word.xor(8n, Word.xor(8n, x9, A.aria.byte1(k2)), A.aria.byte1(k2)), Word.xor(8n, Word.xor(8n, x10, A.aria.byte2(k2)), A.aria.byte2(k2)), Word.xor(8n, Word.xor(8n, x11, A.aria.byte3(k2)), A.aria.byte3(k2)), Word.xor(8n, Word.xor(8n, x12, A.aria.byte0(k3)), A.aria.byte0(k3)), Word.xor(8n, Word.xor(8n, x13, A.aria.byte1(k3)), A.aria.byte1(k3)), Word.xor(8n, Word.xor(8n, x14, A.aria.byte2(k3)), A.aria.byte2(k3)), Word.xor(8n, Word.xor(8n, x15, A.aria.byte3(k3)), A.aria.byte3(k3))} : A.LcAriaSt}
      %word_xx(8n, x7, A.aria.byte3(k1)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, _, Word.xor(8n, Word.xor(8n, x8, A.aria.byte0(k2)), A.aria.byte0(k2)), Word.xor(8n, Word.xor(8n, x9, A.aria.byte1(k2)), A.aria.byte1(k2)), Word.xor(8n, Word.xor(8n, x10, A.aria.byte2(k2)), A.aria.byte2(k2)), Word.xor(8n, Word.xor(8n, x11, A.aria.byte3(k2)), A.aria.byte3(k2)), Word.xor(8n, Word.xor(8n, x12, A.aria.byte0(k3)), A.aria.byte0(k3)), Word.xor(8n, Word.xor(8n, x13, A.aria.byte1(k3)), A.aria.byte1(k3)), Word.xor(8n, Word.xor(8n, x14, A.aria.byte2(k3)), A.aria.byte2(k3)), Word.xor(8n, Word.xor(8n, x15, A.aria.byte3(k3)), A.aria.byte3(k3))} : A.LcAriaSt}
      %word_xx(8n, x8, A.aria.byte0(k2)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, _, Word.xor(8n, Word.xor(8n, x9, A.aria.byte1(k2)), A.aria.byte1(k2)), Word.xor(8n, Word.xor(8n, x10, A.aria.byte2(k2)), A.aria.byte2(k2)), Word.xor(8n, Word.xor(8n, x11, A.aria.byte3(k2)), A.aria.byte3(k2)), Word.xor(8n, Word.xor(8n, x12, A.aria.byte0(k3)), A.aria.byte0(k3)), Word.xor(8n, Word.xor(8n, x13, A.aria.byte1(k3)), A.aria.byte1(k3)), Word.xor(8n, Word.xor(8n, x14, A.aria.byte2(k3)), A.aria.byte2(k3)), Word.xor(8n, Word.xor(8n, x15, A.aria.byte3(k3)), A.aria.byte3(k3))} : A.LcAriaSt}
      %word_xx(8n, x9, A.aria.byte1(k2)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, _, Word.xor(8n, Word.xor(8n, x10, A.aria.byte2(k2)), A.aria.byte2(k2)), Word.xor(8n, Word.xor(8n, x11, A.aria.byte3(k2)), A.aria.byte3(k2)), Word.xor(8n, Word.xor(8n, x12, A.aria.byte0(k3)), A.aria.byte0(k3)), Word.xor(8n, Word.xor(8n, x13, A.aria.byte1(k3)), A.aria.byte1(k3)), Word.xor(8n, Word.xor(8n, x14, A.aria.byte2(k3)), A.aria.byte2(k3)), Word.xor(8n, Word.xor(8n, x15, A.aria.byte3(k3)), A.aria.byte3(k3))} : A.LcAriaSt}
      %word_xx(8n, x10, A.aria.byte2(k2)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, _, Word.xor(8n, Word.xor(8n, x11, A.aria.byte3(k2)), A.aria.byte3(k2)), Word.xor(8n, Word.xor(8n, x12, A.aria.byte0(k3)), A.aria.byte0(k3)), Word.xor(8n, Word.xor(8n, x13, A.aria.byte1(k3)), A.aria.byte1(k3)), Word.xor(8n, Word.xor(8n, x14, A.aria.byte2(k3)), A.aria.byte2(k3)), Word.xor(8n, Word.xor(8n, x15, A.aria.byte3(k3)), A.aria.byte3(k3))} : A.LcAriaSt}
      %word_xx(8n, x11, A.aria.byte3(k2)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, _, Word.xor(8n, Word.xor(8n, x12, A.aria.byte0(k3)), A.aria.byte0(k3)), Word.xor(8n, Word.xor(8n, x13, A.aria.byte1(k3)), A.aria.byte1(k3)), Word.xor(8n, Word.xor(8n, x14, A.aria.byte2(k3)), A.aria.byte2(k3)), Word.xor(8n, Word.xor(8n, x15, A.aria.byte3(k3)), A.aria.byte3(k3))} : A.LcAriaSt}
      %word_xx(8n, x12, A.aria.byte0(k3)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, _, Word.xor(8n, Word.xor(8n, x13, A.aria.byte1(k3)), A.aria.byte1(k3)), Word.xor(8n, Word.xor(8n, x14, A.aria.byte2(k3)), A.aria.byte2(k3)), Word.xor(8n, Word.xor(8n, x15, A.aria.byte3(k3)), A.aria.byte3(k3))} : A.LcAriaSt}
      %word_xx(8n, x13, A.aria.byte1(k3)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, _, Word.xor(8n, Word.xor(8n, x14, A.aria.byte2(k3)), A.aria.byte2(k3)), Word.xor(8n, Word.xor(8n, x15, A.aria.byte3(k3)), A.aria.byte3(k3))} : A.LcAriaSt}
      %word_xx(8n, x14, A.aria.byte2(k3)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, _, Word.xor(8n, Word.xor(8n, x15, A.aria.byte3(k3)), A.aria.byte3(k3))} : A.LcAriaSt}
      %word_xx(8n, x15, A.aria.byte3(k3)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, _} : A.LcAriaSt}
      {==}

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.xor
  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-legacy-ciphers@0.1.0.0/PROOF.bend&name=word_xx
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/aria.bend&name=LcAriaSt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/aria.bend&name=aria.byte0
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/aria.bend&name=aria.byte1
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/aria.bend&name=aria.byte2
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/aria.bend&name=aria.byte3
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/aria.bend&name=aria.xor