def bf_op_unop

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

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

1595def bf_op_unop(o: BF.LcBfOp, b: L.LcBlock64) -> {b == BF.bf.op(o, BF.bf.unop(o, b)) : L.LcBlock64}:
1596  match o:
1597    case BF.LcBfRound{+p, +t}:
1598      match b:
1599        case L.LcBlock64{+x, +y}:
1600          %u32_xx(y, p) : {L.LcBlock64{x, y} == L.LcBlock64{U32.xor(U32.xor(x, BF.bf.f(t, y)), BF.bf.f(t, _)), _} : L.LcBlock64}
1601          %u32_xx(x, BF.bf.f(t, y)) : {L.LcBlock64{x, y} == L.LcBlock64{_, y} : L.LcBlock64}
1602          {==}
1603    case BF.LcBfFinal{+p17, +p18}:
1604      match b:
1605        case L.LcBlock64{+x, +y}:
1606          %u32_xx(x, p18) : {L.LcBlock64{x, y} == L.LcBlock64{_, U32.xor(U32.xor(y, p17), p17)} : L.LcBlock64}
1607          %u32_xx(y, p17) : {L.LcBlock64{x, y} == L.LcBlock64{x, _} : L.LcBlock64}
1608          {==}