def des_unstep_step

bend-osdev-legacy-ciphers@0.1.0.0 · PROOF.bend:171

import Base
import bend-osdev-legacy-ciphers@0.1.0.0/des.bend as D

171def des_unstep_step(+k: D.LcDesRk, h: D.LcDesHalves) -> {h == D.des.unstep(k, D.des.step(k, h)) : D.LcDesHalves}:
172  match h:
173    case D.LcDesHalves{l, +r}:
174      %u32_xx(l, D.des.f(k, r)) : {D.LcDesHalves{l, r} == D.LcDesHalves{_, r} : D.LcDesHalves}
175      {==}