def des_unrounds_rounds

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

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

183def des_unrounds_rounds(ks: List<&2, D.LcDesRk>, +h: D.LcDesHalves) -> {h == D.des.unrounds(ks, D.des.rounds(ks, h)) : D.LcDesHalves}:
184  match ks:
185    case Nil{}:
186      {==}
187    case Con{+k, +t}:
188      %des_unrounds_rounds(t, D.des.step(k, h)) : {h == D.des.unstep(k, _) : D.LcDesHalves}
189      des_unstep_step(k, h)