1	# Laws about Blowfish (blowfish.bend): for every key and block, decryption
2	# undoes encryption and encryption undoes decryption; and a refused key,
3	# proved by computation.
4	import Base
5	import bend-osdev-bytes@0.1.1.0/bytes.bend as B
6	import bend-osdev-cipher-core@0.1.0.0/cipher_core.bend as L
7	import ./blowfish.bend as BF
8	
9	# Blowfish (Schneier), every key
10	
11	law blowfish_round_trip:
12	  for k: BF.LcBlowfishKey
13	  for +b: L.LcBlock64
14	  {BF.LcBlowfish.decrypt(k, BF.LcBlowfish.encrypt(k, b)) == b : L.LcBlock64}
15	
16	law blowfish_round_trip_dual:
17	  for k: BF.LcBlowfishKey
18	  for +b: L.LcBlock64
19	  {BF.LcBlowfish.encrypt(k, BF.LcBlowfish.decrypt(k, b)) == b : L.LcBlock64}
20	
21	# A refusal, proved by computation (gen/vectors.py); Schneier's vectors run
22	# in check.bend (README.md, Laws)
23	
24	# BEGIN GENERATED by gen/vectors.py: vectors
25	# a Blowfish key of 3 bytes is refused (32 bits at least)
26	law blowfish_bad_key_length:
27	  {Result.map(&2, &2, L.LcError, BF.LcBlowfishKey, Unit, k => Unit{}, BF.LcBlowfish.key(B.Octets.of_list([0, 0, 0]))) == Fail{L.LcBadKeyLength{3n}} : Result<&2, &2, L.LcError, Unit>}
28	
29	# END GENERATED: vectors