def bf_unrun_run

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

import Base
import bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.bend as L
import bend-osdev-legacy-ciphers@0.1.0.0/blowfish.bend as BF

1610def bf_unrun_run(os: List<&2, BF.LcBfOp>, +b: L.LcBlock64) -> {b == BF.bf.unrun(os, BF.bf.run(os, b)) : L.LcBlock64}:
1611  match os:
1612    case Nil{}:
1613      {==}
1614    case Con{+o, +t}:
1615      %bf_unrun_run(t, BF.bf.op(o, b)) : {b == BF.bf.unop(o, _) : L.LcBlock64}
1616      bf_unop_op(o, b)