def des_rounds_unrounds
bend-osdev-legacy-ciphers@0.1.0.0 · PROOF.bend:191
import bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-osdev-legacy-ciphers@0.1.0.0/des.bend as D
191def des_rounds_unrounds(ks: List<&2, D.LcDesRk>, +h: D.LcDesHalves) -> {h == D.des.rounds(ks, D.des.unrounds(ks, h)) : D.LcDesHalves}:
192 match ks:
193 case Nil{}:
194 {==}
195 case Con{+k, +t}:
196 %des_step_unstep(k, D.des.unrounds(t, h)) : {h == D.des.rounds(t, _) : D.LcDesHalves}
197 des_rounds_unrounds(t, h)