law tea_round_trip

bend-osdev-legacy-ciphers@0.1.0.0 · LAWS.bend:156

import Base
import bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.bend as L
import bend-osdev-legacy-ciphers@0.1.0.0/tea.bend as TE

156law tea_round_trip:
157  for k: TE.LcTeaKey
158  for +b: L.LcBlock64
159  {TE.LcTea.decrypt(k, TE.LcTea.encrypt(k, b)) == b : L.LcBlock64}