law feistel_unrun_run

bend-osdev-cipher-core@0.1.0.0 · LAWS.bend:63

import Base
import bend-osdev-cipher-core@0.1.0.0/cipher_core.bend as L

63# Feistel rounds over any round function f and any round keys: the rounds
64# undone last to first undo the rounds, and the other way round
65law feistel_unrun_run:
66  for ~RK: Data
67  for ~f: RK -> U32 -> U32
68  for ks: List<&2, RK>
69  for +b: L.LcBlock64
70  {b == L.lc.fe.unrun(~RK, ~f, ks, L.lc.fe.run(~RK, ~f, ks, b)) : L.LcBlock64}