def bf_unrun_run

bend-osdev-blowfish@0.1.0.0 · PROOF.bend:41

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

41def bf_unrun_run(os: List<&2, BF.LcBfOp>, +b: L.LcBlock64) -> {b == BF.bf.unrun(os, BF.bf.run(os, b)) : L.LcBlock64}:
42  match os:
43    case Nil{}:
44      {==}
45    case Con{+o, +t}:
46      %bf_unrun_run(t, BF.bf.op(o, b)) : {b == BF.bf.unop(o, _) : L.LcBlock64}
47      bf_unop_op(o, b)