1	import Base
2	import bend-osdev-bytes@0.1.1.0/bytes.bend as B
3	import bend-osdev-cipher-core@0.1.0.0/cipher_core.bend as L
4	import bend-osdev-cipher-core@0.1.0.0/LAWS.bend as CoreL
5	import bend-osdev-cipher-core@0.1.0.0/PROOF.bend as CoreP
6	import ./blowfish.bend as BF
7	import ./LAWS.bend as Laws
8	
9	# Blowfish: a round and the final step, each undone by XOR whatever F is
10	
11	def 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	
26	def 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	
41	def 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	
49	def 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	
57	def 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	
62	def 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	
69	def Laws.blowfish_bad_key_length():
70	  {==}
71	# END GENERATED: vectors