def des_step_unstep

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

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

177def des_step_unstep(+k: D.LcDesRk, h: D.LcDesHalves) -> {h == D.des.step(k, D.des.unstep(k, h)) : D.LcDesHalves}:
178  match h:
179    case D.LcDesHalves{+a, b}:
180      %u32_xx(b, D.des.f(k, a)) : {D.LcDesHalves{a, b} == D.LcDesHalves{a, _} : D.LcDesHalves}
181      {==}