PROOF.bend
bend-osdev-blowfish@0.1.0.0 · 71 lines · 0 definitions
1import Base
2import bend-osdev-bytes@0.1.1.0/bytes.bend as B
3import bend-osdev-cipher-core@0.1.0.0/cipher_core.bend as L
4import bend-osdev-cipher-core@0.1.0.0/LAWS.bend as CoreL
5import bend-osdev-cipher-core@0.1.0.0/PROOF.bend as CoreP
6import bend-osdev-blowfish@0.1.0.0/blowfish.bend as BF
7import bend-osdev-blowfish@0.1.0.0/LAWS.bend as Laws
8
9# Blowfish: a round and the final step, each undone by XOR whatever F is
10
11def bf_unop_op(o: BF.LcBfOp, b: L.LcBlock64) -> {b == BF.bf.unop(o, BF.bf.op(o, b)) : L.LcBlock64}:
12 match o:
13 case BF.LcBfRound{+p, +t}:
14 match b:
15 case L.LcBlock64{+l, +r}:
16 %CoreL.u32_xor_cancel(l, p) : {L.LcBlock64{l, r} == L.LcBlock64{_, U32.xor(U32.xor(r, BF.bf.f(t, U32.xor(l, p))), BF.bf.f(t, U32.xor(l, p)))} : L.LcBlock64}
17 %CoreL.u32_xor_cancel(r, BF.bf.f(t, U32.xor(l, p))) : {L.LcBlock64{l, r} == L.LcBlock64{l, _} : L.LcBlock64}
18 {==}
19 case BF.LcBfFinal{+p17, +p18}:
20 match b:
21 case L.LcBlock64{+l, +r}:
22 %CoreL.u32_xor_cancel(l, p17) : {L.LcBlock64{l, r} == L.LcBlock64{_, U32.xor(U32.xor(r, p18), p18)} : L.LcBlock64}
23 %CoreL.u32_xor_cancel(r, p18) : {L.LcBlock64{l, r} == L.LcBlock64{l, _} : L.LcBlock64}
24 {==}
25
26def bf_op_unop(o: BF.LcBfOp, b: L.LcBlock64) -> {b == BF.bf.op(o, BF.bf.unop(o, b)) : L.LcBlock64}:
27 match o:
28 case BF.LcBfRound{+p, +t}:
29 match b:
30 case L.LcBlock64{+x, +y}:
31 %CoreL.u32_xor_cancel(y, p) : {L.LcBlock64{x, y} == L.LcBlock64{U32.xor(U32.xor(x, BF.bf.f(t, y)), BF.bf.f(t, _)), _} : L.LcBlock64}
32 %CoreL.u32_xor_cancel(x, BF.bf.f(t, y)) : {L.LcBlock64{x, y} == L.LcBlock64{_, y} : L.LcBlock64}
33 {==}
34 case BF.LcBfFinal{+p17, +p18}:
35 match b:
36 case L.LcBlock64{+x, +y}:
37 %CoreL.u32_xor_cancel(x, p18) : {L.LcBlock64{x, y} == L.LcBlock64{_, U32.xor(U32.xor(y, p17), p17)} : L.LcBlock64}
38 %CoreL.u32_xor_cancel(y, p17) : {L.LcBlock64{x, y} == L.LcBlock64{x, _} : L.LcBlock64}
39 {==}
40
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)
48
49def bf_run_unrun(os: List<&2, BF.LcBfOp>, +b: L.LcBlock64) -> {b == BF.bf.run(os, BF.bf.unrun(os, b)) : L.LcBlock64}:
50 match os:
51 case Nil{}:
52 {==}
53 case Con{+o, +t}:
54 %bf_op_unop(o, BF.bf.unrun(t, b)) : {b == BF.bf.run(t, _) : L.LcBlock64}
55 bf_run_unrun(t, b)
56
57def Laws.blowfish_round_trip(k, b):
58 match k:
59 case BF.LcBlowfishKey{+ops}:
60 Equal.sym(L.LcBlock64, b, BF.bf.unrun(ops, BF.bf.run(ops, b)), bf_unrun_run(ops, b))
61
62def Laws.blowfish_round_trip_dual(k, b):
63 match k:
64 case BF.LcBlowfishKey{+ops}:
65 Equal.sym(L.LcBlock64, b, BF.bf.run(ops, BF.bf.unrun(ops, b)), bf_run_unrun(ops, b))
66
67# BEGIN GENERATED by gen/vectors.py: vectors
68
69def Laws.blowfish_bad_key_length():
70 {==}
71# END GENERATED: vectors