1	import Base
2	import ../LAWS.bend as L
3	import ../libs/AES256GCM.bend as AES
4	
5	# Transport fixture aliases before entering the encryption or decryption code.
6	# Equal fixtures must not force a fresh evaluation of the entire cipher.
7	def encrypt_inputs(+key: AES.SecretKey, +nonce: AES.Nonce,
8	    +aad: List<&2, U32>, +fixture_aad: List<&2, U32>,
9	    +plaintext: List<&2, U32>, +fixture_plaintext: List<&2, U32>,
10	    +expected: List<&2, U32>,
11	    aad_matches: {aad == fixture_aad : List<&2, U32>},
12	    plaintext_matches: {plaintext == fixture_plaintext : List<&2, U32>},
13	    computed: {L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, fixture_aad, fixture_plaintext)) == expected : List<&2, U32>}) ->
14	    {L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, aad, plaintext)) == expected : List<&2, U32>}:
15	    Equal.trans(List<&2, U32>,
16	        L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, aad, plaintext)),
17	        L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, fixture_aad, plaintext)), expected,
18	        Equal.cong(List<&2, U32>, List<&2, U32>, value =>
19	            L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, value, plaintext)),
20	            aad, fixture_aad, aad_matches),
21	        Equal.trans(List<&2, U32>,
22	            L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, fixture_aad, plaintext)),
23	            L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, fixture_aad, fixture_plaintext)), expected,
24	            Equal.cong(List<&2, U32>, List<&2, U32>, value =>
25	                L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, fixture_aad, value)),
26	                plaintext, fixture_plaintext, plaintext_matches), computed))
27	
28	def decrypt_inputs(+key: AES.SecretKey, +fixture_key: AES.SecretKey,
29	    +aad: List<&2, U32>, +fixture_aad: List<&2, U32>,
30	    +envelope: AES.Envelope, +fixture_envelope: AES.Envelope,
31	    +expected: Result<&2, &2, AES.Error, List<&2, U32>>,
32	    key_matches: {key == fixture_key : AES.SecretKey},
33	    aad_matches: {aad == fixture_aad : List<&2, U32>},
34	    envelope_matches: {envelope == fixture_envelope : AES.Envelope},
35	    computed: {AES.decrypt(fixture_key, fixture_aad, fixture_envelope) == expected : Result<&2, &2, AES.Error, List<&2, U32>>}) ->
36	    {AES.decrypt(key, aad, envelope) == expected : Result<&2, &2, AES.Error, List<&2, U32>>}:
37	    Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
38	        AES.decrypt(key, aad, envelope), AES.decrypt(fixture_key, aad, envelope), expected,
39	        Equal.cong(AES.SecretKey, Result<&2, &2, AES.Error, List<&2, U32>>,
40	            value => AES.decrypt(value, aad, envelope), key, fixture_key, key_matches),
41	        Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
42	            AES.decrypt(fixture_key, aad, envelope), AES.decrypt(fixture_key, fixture_aad, envelope), expected,
43	            Equal.cong(List<&2, U32>, Result<&2, &2, AES.Error, List<&2, U32>>,
44	                value => AES.decrypt(fixture_key, value, envelope), aad, fixture_aad, aad_matches),
45	            Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
46	                AES.decrypt(fixture_key, fixture_aad, envelope), AES.decrypt(fixture_key, fixture_aad, fixture_envelope), expected,
47	                Equal.cong(AES.Envelope, Result<&2, &2, AES.Error, List<&2, U32>>,
48	                    value => AES.decrypt(fixture_key, fixture_aad, value), envelope, fixture_envelope, envelope_matches), computed)))