1	import Base
2	import ../libs/AES256GCM.bend as AES
3	import ../libs/AES256GCMCore.bend as Core
4	
5	def output_ciphertext(output: Core.GcmOutput) -> List<&2, U32>:
6	    match output:
7	        case Core.GcmOutput{ciphertext, ciphertext_valid,
8	            tag_bytes, tag_valid, tag_size, tag_words, tag_nonce, tag_aad,
9	            tag_matches}:
10	            ciphertext
11	
12	def output_tag(output: Core.GcmOutput) -> List<&2, U32>:
13	    match output:
14	        case Core.GcmOutput{ciphertext, ciphertext_valid,
15	            tag_bytes, tag_valid, tag_size, tag_words, tag_nonce, tag_aad,
16	            tag_matches}:
17	            tag_bytes
18	
19	def output_tag_words(output: Core.GcmOutput) -> List<&2, U32>:
20	    match output:
21	        case Core.GcmOutput{ciphertext, ciphertext_valid, tag_bytes,
22	            tag_valid, tag_size, tag_words, tag_nonce, tag_aad, tag_matches}:
23	            tag_words
24	
25	def output_tag_nonce(output: Core.GcmOutput) -> List<&2, U32>:
26	    match output:
27	        case Core.GcmOutput{ciphertext, ciphertext_valid, tag_bytes,
28	            tag_valid, tag_size, tag_words, tag_nonce, tag_aad, tag_matches}:
29	            tag_nonce
30	
31	def output_tag_aad(output: Core.GcmOutput) -> List<&2, U32>:
32	    match output:
33	        case Core.GcmOutput{ciphertext, ciphertext_valid, tag_bytes,
34	            tag_valid, tag_size, tag_words, tag_nonce, tag_aad, tag_matches}:
35	            tag_aad
36	
37	def output_tag_ciphertext(output: Core.GcmOutput) -> List<&2, U32>:
38	    match output:
39	        case Core.GcmOutput{ciphertext, ciphertext_valid, tag_bytes,
40	            tag_valid, tag_size, tag_words, tag_nonce, tag_aad, tag_matches}:
41	            ciphertext
42	
43	def output_from_ciphertext_matches(+words: List<&2, U32>,
44	    +nonce: List<&2, U32>, +aad: List<&2, U32>,
45	    +cipher_output: Core.GcmCiphertext) ->
46	    {output_ciphertext(Core.gcm_output_from_ciphertext(words, nonce, aad,
47	        cipher_output)) == Core.gcm_ciphertext_bytes(cipher_output) :
48	        List<&2, U32>}:
49	    match cipher_output:
50	        case Core.GcmCiphertext{bytes, valid}: {==}
51	
52	
53	
54	def output_ciphertext_valid(+output: Core.GcmOutput) ->
55	    {Core.gcm_bytes_valid(output_ciphertext(output)) == True{} : Bool}:
56	    match output:
57	        case Core.GcmOutput{ciphertext, ciphertext_valid,
58	            tag_bytes, tag_valid, tag_size, tag_words, tag_nonce, tag_aad,
59	            tag_matches}:
60	            ciphertext_valid
61	
62	def output_tag_valid(+output: Core.GcmOutput) ->
63	    {Core.gcm_bytes_valid(output_tag(output)) == True{} : Bool}:
64	    match output:
65	        case Core.GcmOutput{ciphertext, ciphertext_valid,
66	            tag_bytes, tag_valid, tag_size, tag_words, tag_nonce, tag_aad,
67	            tag_matches}:
68	            tag_valid
69	
70	def envelope_gcm_ciphertext(nonce: AES.Nonce,
71	    output: Core.GcmOutput) ->
72	    {AES.ciphertext(AES.envelope_from_gcm_checked(nonce, output)) ==
73	     output_ciphertext(output) : List<&2, U32>}:
74	    match output:
75	        case Core.GcmOutput{ciphertext, ciphertext_valid,
76	            tag_bytes, tag_valid, tag_size, tag_words, tag_nonce, tag_aad,
77	            tag_matches}: {==}
78	
79	def envelope_gcm_tag(nonce: AES.Nonce,
80	    output: Core.GcmOutput) ->
81	    {AES.tag_bytes(AES.envelope_tag(
82	        AES.envelope_from_gcm_checked(nonce, output))) ==
83	     output_tag(output) : List<&2, U32>}:
84	    match output:
85	        case Core.GcmOutput{ciphertext, ciphertext_valid,
86	            tag_bytes, tag_valid, tag_size, tag_words, tag_nonce, tag_aad,
87	            tag_matches}: {==}
88	
89	def envelope_gcm_nonce(nonce: AES.Nonce,
90	    output: Core.GcmOutput) ->
91	    {AES.raw_nonce_bytes(AES.envelope_nonce(
92	        AES.envelope_from_gcm_checked(nonce, output))) ==
93	     AES.raw_nonce_bytes(nonce) : List<&2, U32>}:
94	    match output:
95	        case Core.GcmOutput{ciphertext, ciphertext_valid,
96	            tag_bytes, tag_valid, tag_size, tag_words, tag_nonce, tag_aad,
97	            tag_matches}: {==}
98	
99	def raw_encrypt_output_ciphertext(+key: List<&2, U32>,
100	    +nonce: List<&2, U32>, +aad: List<&2, U32>,
101	    +plaintext: List<&2, U32>) ->
102	    {output_ciphertext(Core.gcm_encrypt_raw(key, nonce, aad, plaintext)) ==
103	     Core.gcm_zip_xor(plaintext,
104	        Core.gcm_ctr_stream_exact(List.length(&2, U32, plaintext),
105	            Core.aes256_expand(key),
106	            Core.gcm_inc32(Core.gcm_j0(nonce)))) : List<&2, U32>}:
107	    Equal.trans(List<&2, U32>,
108	        output_ciphertext(Core.gcm_encrypt_raw(key, nonce, aad, plaintext)),
109	        Core.gcm_ciphertext_bytes(Core.gcm_ctr_encrypt(
110	            Core.aes256_expand(key), nonce, plaintext)),
111	        Core.gcm_zip_xor(plaintext,
112	            Core.gcm_ctr_stream_exact(List.length(&2, U32, plaintext),
113	                Core.aes256_expand(key),
114	                Core.gcm_inc32(Core.gcm_j0(nonce)))),
115	        output_from_ciphertext_matches(Core.aes256_expand(key), nonce, aad,
116	            Core.gcm_ctr_encrypt(Core.aes256_expand(key), nonce, plaintext)),
117	        {==})