LAWS.aria_rfc5794: law of bend-osdev-legacy-ciphers@0.1.0.0
Import: import bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend as LAWS
Lines 310-314 of bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&start_line=310&end_line=314

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-legacy-ciphers@0.1.0.0/legacy_ciphers.bend as L
import bend-osdev-legacy-ciphers@0.1.0.0/aria.bend as A

# RFC 5794, Appendix A.1: ARIA-128, key 000102030405060708090A0B0C0D0E0F,
# plaintext 00112233445566778899AABBCCDDEEFF, ciphertext
# D718FBD6AB644C739DA95F3BE6451778
law aria_rfc5794:
  {Result.map(&2, &2, L.LcError, A.LcAriaKey, M.CmBlock, k => A.LcAria.encrypt(k, M.CmBlock{1122867, 1146447479, 2291772091, 3437096703}), A.LcAria.key(B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]))) == Done{M.CmBlock{3608738774, 2875477107, 2645122875, 3863287672}} : Result<&2, &2, L.LcError, M.CmBlock>}

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result.map
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.of_list
  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/aria.bend&name=LcAria.encrypt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/aria.bend&name=LcAria.key
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/aria.bend&name=LcAriaKey
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.bend&name=LcError