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 ./cast5.bend as C5
7	import ./LAWS.bend as Laws
8	
9	def swap2(b: L.LcBlock64) -> {b == L.lc.swap(L.lc.swap(b)) : L.LcBlock64}:
10	  match b:
11	    case L.LcBlock64{h, l}:
12	      {==}
13	
14	# CAST-128: its rounds, then the exchange of the halves, undone
15	
16	def Laws.cast5_round_trip(k, b):
17	  match k:
18	    case C5.LcCast5Key{+rks}:
19	      %swap2(L.lc.fe.run(~C5.LcCast5Rk, ~C5.cast5.f, rks, b)) : {L.lc.fe.unrun(~C5.LcCast5Rk, ~C5.cast5.f, rks, _) == b : L.LcBlock64}
20	      Equal.sym(L.LcBlock64, b, L.lc.fe.unrun(~C5.LcCast5Rk, ~C5.cast5.f, rks, L.lc.fe.run(~C5.LcCast5Rk, ~C5.cast5.f, rks, b)), CoreL.feistel_unrun_run(~C5.LcCast5Rk, ~C5.cast5.f, rks, b))
21	
22	def Laws.cast5_round_trip_dual(k, b):
23	  match k:
24	    case C5.LcCast5Key{+rks}:
25	      %CoreL.feistel_run_unrun(~C5.LcCast5Rk, ~C5.cast5.f, rks, L.lc.swap(b)) : {L.lc.swap(_) == b : L.LcBlock64}
26	      Equal.sym(L.LcBlock64, b, L.lc.swap(L.lc.swap(b)), swap2(b))
27	
28	# BEGIN GENERATED by gen/vectors.py: vectors
29	
30	def Laws.cast5_rfc2144():
31	  {==}
32	
33	def Laws.cast5_bad_key_length():
34	  {==}
35	# END GENERATED: vectors