proofs/crypto/aes/api.bend

bend-collections-laws-crypto@1.0.0.0 · 569 lines · 22 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/types.bend as T
5import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/aes.bend as A
6import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/gcm.bend as GI
7import bend-collections-laws-crypto@1.0.0.0/src/crypto/aesgcm.bend as GCM
8import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend as S
9import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend as G
10import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/gcm.bend as GP
11import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend as AD
12
13# The AES-128-GCM / AES-256-GCM API clauses of laws.bend (Api128/Api256
14# encrypt, decrypt, roundtrip, forgery) as plain lemmas: proof.bend fills the
15# laws with them, and the AEAD facade (proofs/crypto/aead) imports them
16# (importing proof.bend would stop it being the aes package's root). The
17# *_l versions take the nonce and tag as lists of the right length.
18
19def valid_of(+key: List<&2, U32>, +w: Nat, +h: {List.length(&2, U32, key) == w : Nat}, +v: {A.valid_length(w) == True{} : Bool}) -> {A.valid_length(List.length(&2, U32, key)) == True{} : Bool}:
20  %Equal.sym(Nat, List.length(&2, U32, key), w, h) : {A.valid_length(_) == True{} : Bool}
21  v
22
23# Decrypt what an encryption returned (None stays None).
24def open128(+key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, m: Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, U32>>:
25  match m:
26    case None{}:
27      None{}
28    case Some{ct}:
29      GCM.aes128_gcm_decrypt(key, nonce, aad, ct)
30
31def open256(+key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, m: Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, U32>>:
32  match m:
33    case None{}:
34      None{}
35    case Some{ct}:
36      GCM.aes256_gcm_decrypt(key, nonce, aad, ct)
37
38law aes128_encrypt:
39  for +key: List<&2, U32>
40  for +h: {List.length(&2, U32, key) == 16n : Nat}
41  for +n0: U32
42  for +n1: U32
43  for +n2: U32
44  for +n3: U32
45  for +n4: U32
46  for +n5: U32
47  for +n6: U32
48  for +n7: U32
49  for +n8: U32
50  for +n9: U32
51  for +n10: U32
52  for +n11: U32
53  for +aad: List<&2, U32>
54  for +pt: List<&2, U32>
55  {GCM.aes128_gcm_encrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt) == Some{G.aes_seal(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt)} : Maybe<&2, List<&2, U32>>}
56
57def aes128_encrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt):
58  %Equal.sym(Nat, List.length(&2, U32, key), 16n, h) : {GI.seal_key(GI.schedule_if(Nat.is_eq(_, 16n), key), [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt) == Some{G.aes_seal(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt)} : Maybe<&2, List<&2, U32>>}
59  %Equal.sym(Bool, A.valid_length(List.length(&2, U32, key)), True{}, valid_of(key, 16n, h, {==})) : {GI.seal_key(A.schedule_if(_, Nat.div(List.length(&2, U32, key), 4n), key), [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt) == Some{G.aes_seal(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt)} : Maybe<&2, List<&2, U32>>}
60  %GP.seal_ok(S.nk(key), S.nr(key), key, T.W{n0, n1, n2, n3}, T.W{n4, n5, n6, n7}, T.W{n8, n9, n10, n11}, aad, pt) : {Some{GI.seal_core(A.Schedule{S.nr(key), A.expand(S.nk(key), S.nr(key), key)}, T.W{n0, n1, n2, n3}, T.W{n4, n5, n6, n7}, T.W{n8, n9, n10, n11}, aad, pt)} == Some{_} : Maybe<&2, List<&2, U32>>}
61  {==}
62
63law aes128_decrypt:
64  for +key: List<&2, U32>
65  for +h: {List.length(&2, U32, key) == 16n : Nat}
66  for +n0: U32
67  for +n1: U32
68  for +n2: U32
69  for +n3: U32
70  for +n4: U32
71  for +n5: U32
72  for +n6: U32
73  for +n7: U32
74  for +n8: U32
75  for +n9: U32
76  for +n10: U32
77  for +n11: U32
78  for +aad: List<&2, U32>
79  for +ct: List<&2, U32>
80  {GCM.aes128_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, ct) == G.aes_open(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, ct) : Maybe<&2, List<&2, U32>>}
81
82def aes128_decrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, ct):
83  %Equal.sym(Nat, List.length(&2, U32, key), 16n, h) : {GI.open_key(GI.schedule_if(Nat.is_eq(_, 16n), key), [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, ct) == G.aes_open(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, ct) : Maybe<&2, List<&2, U32>>}
84  %Equal.sym(Bool, A.valid_length(List.length(&2, U32, key)), True{}, valid_of(key, 16n, h, {==})) : {GI.open_key(A.schedule_if(_, Nat.div(List.length(&2, U32, key), 4n), key), [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, ct) == G.aes_open(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, ct) : Maybe<&2, List<&2, U32>>}
85  GP.open_ok(S.nk(key), S.nr(key), key, T.W{n0, n1, n2, n3}, T.W{n4, n5, n6, n7}, T.W{n8, n9, n10, n11}, aad, ct)
86
87law aes128_roundtrip:
88  for +key: List<&2, U32>
89  for +h: {List.length(&2, U32, key) == 16n : Nat}
90  for +n0: U32
91  for +n1: U32
92  for +n2: U32
93  for +n3: U32
94  for +n4: U32
95  for +n5: U32
96  for +n6: U32
97  for +n7: U32
98  for +n8: U32
99  for +n9: U32
100  for +n10: U32
101  for +n11: U32
102  for +aad: List<&2, U32>
103  for +pt: List<&2, U32>
104  {open128(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, GCM.aes128_gcm_encrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}
105
106def aes128_roundtrip(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt):
107  %Equal.sym(Maybe<&2, List<&2, U32>>, GCM.aes128_gcm_encrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt), Some{G.aes_seal(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt)}, aes128_encrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt)) : {open128(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, _) == Some{pt} : Maybe<&2, List<&2, U32>>}
108  %Equal.sym(Maybe<&2, List<&2, U32>>, GCM.aes128_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, G.aes_seal(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt)), G.aes_open(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, G.aes_seal(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt)), aes128_decrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, G.aes_seal(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt))) : {_ == Some{pt} : Maybe<&2, List<&2, U32>>}
109  AD.roundtrip(S.nk(key), S.nr(key), key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt)
110
111law aes128_forgery:
112  for +key: List<&2, U32>
113  for +h: {List.length(&2, U32, key) == 16n : Nat}
114  for +n0: U32
115  for +n1: U32
116  for +n2: U32
117  for +n3: U32
118  for +n4: U32
119  for +n5: U32
120  for +n6: U32
121  for +n7: U32
122  for +n8: U32
123  for +n9: U32
124  for +n10: U32
125  for +n11: U32
126  for +aad: List<&2, U32>
127  for +c: List<&2, U32>
128  for +t0: U32
129  for +t1: U32
130  for +t2: U32
131  for +t3: U32
132  for +t4: U32
133  for +t5: U32
134  for +t6: U32
135  for +t7: U32
136  for +t8: U32
137  for +t9: U32
138  for +t10: U32
139  for +t11: U32
140  for +t12: U32
141  for +t13: U32
142  for +t14: U32
143  for +t15: U32
144  for ne: {[t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15] != G.aes_tag(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, c) : List<&2, U32>}
145  {GCM.aes128_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, [t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15])) == None{} : Maybe<&2, List<&2, U32>>}
146
147def aes128_forgery(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, c, t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, ne):
148  %Equal.sym(Maybe<&2, List<&2, U32>>, GCM.aes128_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, [t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15])), G.aes_open(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, [t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15])), aes128_decrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, List.append(&2, U32, c, [t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15]))) : {_ == None{} : Maybe<&2, List<&2, U32>>}
149  AD.forgery(S.nk(key), S.nr(key), key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, c, t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, ne)
150
151law aes256_encrypt:
152  for +key: List<&2, U32>
153  for +h: {List.length(&2, U32, key) == 32n : Nat}
154  for +n0: U32
155  for +n1: U32
156  for +n2: U32
157  for +n3: U32
158  for +n4: U32
159  for +n5: U32
160  for +n6: U32
161  for +n7: U32
162  for +n8: U32
163  for +n9: U32
164  for +n10: U32
165  for +n11: U32
166  for +aad: List<&2, U32>
167  for +pt: List<&2, U32>
168  {GCM.aes256_gcm_encrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt) == Some{G.aes_seal(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt)} : Maybe<&2, List<&2, U32>>}
169
170def aes256_encrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt):
171  %Equal.sym(Nat, List.length(&2, U32, key), 32n, h) : {GI.seal_key(GI.schedule_if(Nat.is_eq(_, 32n), key), [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt) == Some{G.aes_seal(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt)} : Maybe<&2, List<&2, U32>>}
172  %Equal.sym(Bool, A.valid_length(List.length(&2, U32, key)), True{}, valid_of(key, 32n, h, {==})) : {GI.seal_key(A.schedule_if(_, Nat.div(List.length(&2, U32, key), 4n), key), [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt) == Some{G.aes_seal(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt)} : Maybe<&2, List<&2, U32>>}
173  %GP.seal_ok(S.nk(key), S.nr(key), key, T.W{n0, n1, n2, n3}, T.W{n4, n5, n6, n7}, T.W{n8, n9, n10, n11}, aad, pt) : {Some{GI.seal_core(A.Schedule{S.nr(key), A.expand(S.nk(key), S.nr(key), key)}, T.W{n0, n1, n2, n3}, T.W{n4, n5, n6, n7}, T.W{n8, n9, n10, n11}, aad, pt)} == Some{_} : Maybe<&2, List<&2, U32>>}
174  {==}
175
176law aes256_decrypt:
177  for +key: List<&2, U32>
178  for +h: {List.length(&2, U32, key) == 32n : Nat}
179  for +n0: U32
180  for +n1: U32
181  for +n2: U32
182  for +n3: U32
183  for +n4: U32
184  for +n5: U32
185  for +n6: U32
186  for +n7: U32
187  for +n8: U32
188  for +n9: U32
189  for +n10: U32
190  for +n11: U32
191  for +aad: List<&2, U32>
192  for +ct: List<&2, U32>
193  {GCM.aes256_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, ct) == G.aes_open(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, ct) : Maybe<&2, List<&2, U32>>}
194
195def aes256_decrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, ct):
196  %Equal.sym(Nat, List.length(&2, U32, key), 32n, h) : {GI.open_key(GI.schedule_if(Nat.is_eq(_, 32n), key), [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, ct) == G.aes_open(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, ct) : Maybe<&2, List<&2, U32>>}
197  %Equal.sym(Bool, A.valid_length(List.length(&2, U32, key)), True{}, valid_of(key, 32n, h, {==})) : {GI.open_key(A.schedule_if(_, Nat.div(List.length(&2, U32, key), 4n), key), [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, ct) == G.aes_open(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, ct) : Maybe<&2, List<&2, U32>>}
198  GP.open_ok(S.nk(key), S.nr(key), key, T.W{n0, n1, n2, n3}, T.W{n4, n5, n6, n7}, T.W{n8, n9, n10, n11}, aad, ct)
199
200law aes256_roundtrip:
201  for +key: List<&2, U32>
202  for +h: {List.length(&2, U32, key) == 32n : Nat}
203  for +n0: U32
204  for +n1: U32
205  for +n2: U32
206  for +n3: U32
207  for +n4: U32
208  for +n5: U32
209  for +n6: U32
210  for +n7: U32
211  for +n8: U32
212  for +n9: U32
213  for +n10: U32
214  for +n11: U32
215  for +aad: List<&2, U32>
216  for +pt: List<&2, U32>
217  {open256(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, GCM.aes256_gcm_encrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}
218
219def aes256_roundtrip(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt):
220  %Equal.sym(Maybe<&2, List<&2, U32>>, GCM.aes256_gcm_encrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt), Some{G.aes_seal(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt)}, aes256_encrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt)) : {open256(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, _) == Some{pt} : Maybe<&2, List<&2, U32>>}
221  %Equal.sym(Maybe<&2, List<&2, U32>>, GCM.aes256_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, G.aes_seal(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt)), G.aes_open(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, G.aes_seal(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt)), aes256_decrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, G.aes_seal(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt))) : {_ == Some{pt} : Maybe<&2, List<&2, U32>>}
222  AD.roundtrip(S.nk(key), S.nr(key), key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt)
223
224law aes256_forgery:
225  for +key: List<&2, U32>
226  for +h: {List.length(&2, U32, key) == 32n : Nat}
227  for +n0: U32
228  for +n1: U32
229  for +n2: U32
230  for +n3: U32
231  for +n4: U32
232  for +n5: U32
233  for +n6: U32
234  for +n7: U32
235  for +n8: U32
236  for +n9: U32
237  for +n10: U32
238  for +n11: U32
239  for +aad: List<&2, U32>
240  for +c: List<&2, U32>
241  for +t0: U32
242  for +t1: U32
243  for +t2: U32
244  for +t3: U32
245  for +t4: U32
246  for +t5: U32
247  for +t6: U32
248  for +t7: U32
249  for +t8: U32
250  for +t9: U32
251  for +t10: U32
252  for +t11: U32
253  for +t12: U32
254  for +t13: U32
255  for +t14: U32
256  for +t15: U32
257  for ne: {[t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15] != G.aes_tag(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, c) : List<&2, U32>}
258  {GCM.aes256_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, [t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15])) == None{} : Maybe<&2, List<&2, U32>>}
259
260def aes256_forgery(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, c, t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, ne):
261  %Equal.sym(Maybe<&2, List<&2, U32>>, GCM.aes256_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, [t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15])), G.aes_open(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, [t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15])), aes256_decrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, List.append(&2, U32, c, [t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15]))) : {_ == None{} : Maybe<&2, List<&2, U32>>}
262  AD.forgery(S.nk(key), S.nr(key), key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, c, t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, ne)
263
264
265# ---- the same for any nonce (and tag) list of the right length
266
267def no_len(-G: Type, +n: Nat, +m: Nat, +h: {n == m : Nat}, +hf: {Nat.is_eq(n, m) == False{} : Bool}) -> G:
268  Empty.absurd(G, L.false_true(Equal.trans(Bool, False{}, Nat.is_eq(n, m), True{}, Equal.sym(Bool, Nat.is_eq(n, m), False{}, hf),
269    Equal.trans(Bool, Nat.is_eq(n, m), Nat.is_eq(m, m), True{}, Equal.cong(Nat, Bool, x => Nat.is_eq(x, m), n, m, h), N.is_eq_refl(m)))))
270
271law aes128_encrypt_l:
272  for +key: List<&2, U32>
273  for +h: {List.length(&2, U32, key) == 16n : Nat}
274  for +nonce: List<&2, U32>
275  for +hn: {List.length(&2, U32, nonce) == 12n : Nat}
276  for +aad: List<&2, U32>
277  for +pt: List<&2, U32>
278  {GCM.aes128_gcm_encrypt(key, nonce, aad, pt) == Some{G.aes_seal(key, nonce, aad, pt)} : Maybe<&2, List<&2, U32>>}
279
280def aes128_encrypt_l(key, h, nonce, hn, aad, pt):
281  match nonce:
282    case Nil{}: no_len({GCM.aes128_gcm_encrypt(key, {Nil{} : List<&2, U32>}, aad, pt) == Some{G.aes_seal(key, {Nil{} : List<&2, U32>}, aad, pt)} : Maybe<&2, List<&2, U32>>}, 0n, 12n, hn, {==})
283    case n0 <> Nil{}: no_len({GCM.aes128_gcm_encrypt(key, {[n0] : List<&2, U32>}, aad, pt) == Some{G.aes_seal(key, {[n0] : List<&2, U32>}, aad, pt)} : Maybe<&2, List<&2, U32>>}, 1n, 12n, hn, {==})
284    case n0 <> n1 <> Nil{}: no_len({GCM.aes128_gcm_encrypt(key, {[n0, n1] : List<&2, U32>}, aad, pt) == Some{G.aes_seal(key, {[n0, n1] : List<&2, U32>}, aad, pt)} : Maybe<&2, List<&2, U32>>}, 2n, 12n, hn, {==})
285    case n0 <> n1 <> n2 <> Nil{}: no_len({GCM.aes128_gcm_encrypt(key, {[n0, n1, n2] : List<&2, U32>}, aad, pt) == Some{G.aes_seal(key, {[n0, n1, n2] : List<&2, U32>}, aad, pt)} : Maybe<&2, List<&2, U32>>}, 3n, 12n, hn, {==})
286    case n0 <> n1 <> n2 <> n3 <> Nil{}: no_len({GCM.aes128_gcm_encrypt(key, {[n0, n1, n2, n3] : List<&2, U32>}, aad, pt) == Some{G.aes_seal(key, {[n0, n1, n2, n3] : List<&2, U32>}, aad, pt)} : Maybe<&2, List<&2, U32>>}, 4n, 12n, hn, {==})
287    case n0 <> n1 <> n2 <> n3 <> n4 <> Nil{}: no_len({GCM.aes128_gcm_encrypt(key, {[n0, n1, n2, n3, n4] : List<&2, U32>}, aad, pt) == Some{G.aes_seal(key, {[n0, n1, n2, n3, n4] : List<&2, U32>}, aad, pt)} : Maybe<&2, List<&2, U32>>}, 5n, 12n, hn, {==})
288    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> Nil{}: no_len({GCM.aes128_gcm_encrypt(key, {[n0, n1, n2, n3, n4, n5] : List<&2, U32>}, aad, pt) == Some{G.aes_seal(key, {[n0, n1, n2, n3, n4, n5] : List<&2, U32>}, aad, pt)} : Maybe<&2, List<&2, U32>>}, 6n, 12n, hn, {==})
289    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> Nil{}: no_len({GCM.aes128_gcm_encrypt(key, {[n0, n1, n2, n3, n4, n5, n6] : List<&2, U32>}, aad, pt) == Some{G.aes_seal(key, {[n0, n1, n2, n3, n4, n5, n6] : List<&2, U32>}, aad, pt)} : Maybe<&2, List<&2, U32>>}, 7n, 12n, hn, {==})
290    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> Nil{}: no_len({GCM.aes128_gcm_encrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7] : List<&2, U32>}, aad, pt) == Some{G.aes_seal(key, {[n0, n1, n2, n3, n4, n5, n6, n7] : List<&2, U32>}, aad, pt)} : Maybe<&2, List<&2, U32>>}, 8n, 12n, hn, {==})
291    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> Nil{}: no_len({GCM.aes128_gcm_encrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8] : List<&2, U32>}, aad, pt) == Some{G.aes_seal(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8] : List<&2, U32>}, aad, pt)} : Maybe<&2, List<&2, U32>>}, 9n, 12n, hn, {==})
292    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> Nil{}: no_len({GCM.aes128_gcm_encrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8, n9] : List<&2, U32>}, aad, pt) == Some{G.aes_seal(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8, n9] : List<&2, U32>}, aad, pt)} : Maybe<&2, List<&2, U32>>}, 10n, 12n, hn, {==})
293    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> Nil{}: no_len({GCM.aes128_gcm_encrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10] : List<&2, U32>}, aad, pt) == Some{G.aes_seal(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10] : List<&2, U32>}, aad, pt)} : Maybe<&2, List<&2, U32>>}, 11n, 12n, hn, {==})
294    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> Nil{}: aes128_encrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt)
295    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> nx <> nrest: no_len({GCM.aes128_gcm_encrypt(key, {n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> nx <> nrest : List<&2, U32>}, aad, pt) == Some{G.aes_seal(key, {n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> nx <> nrest : List<&2, U32>}, aad, pt)} : Maybe<&2, List<&2, U32>>}, 13n+List.length(&2, U32, nrest), 12n, hn, {==})
296
297law aes128_decrypt_l:
298  for +key: List<&2, U32>
299  for +h: {List.length(&2, U32, key) == 16n : Nat}
300  for +nonce: List<&2, U32>
301  for +hn: {List.length(&2, U32, nonce) == 12n : Nat}
302  for +aad: List<&2, U32>
303  for +ct: List<&2, U32>
304  {GCM.aes128_gcm_decrypt(key, nonce, aad, ct) == G.aes_open(key, nonce, aad, ct) : Maybe<&2, List<&2, U32>>}
305
306def aes128_decrypt_l(key, h, nonce, hn, aad, ct):
307  match nonce:
308    case Nil{}: no_len({GCM.aes128_gcm_decrypt(key, {Nil{} : List<&2, U32>}, aad, ct) == G.aes_open(key, {Nil{} : List<&2, U32>}, aad, ct) : Maybe<&2, List<&2, U32>>}, 0n, 12n, hn, {==})
309    case n0 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, {[n0] : List<&2, U32>}, aad, ct) == G.aes_open(key, {[n0] : List<&2, U32>}, aad, ct) : Maybe<&2, List<&2, U32>>}, 1n, 12n, hn, {==})
310    case n0 <> n1 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, {[n0, n1] : List<&2, U32>}, aad, ct) == G.aes_open(key, {[n0, n1] : List<&2, U32>}, aad, ct) : Maybe<&2, List<&2, U32>>}, 2n, 12n, hn, {==})
311    case n0 <> n1 <> n2 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, {[n0, n1, n2] : List<&2, U32>}, aad, ct) == G.aes_open(key, {[n0, n1, n2] : List<&2, U32>}, aad, ct) : Maybe<&2, List<&2, U32>>}, 3n, 12n, hn, {==})
312    case n0 <> n1 <> n2 <> n3 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, {[n0, n1, n2, n3] : List<&2, U32>}, aad, ct) == G.aes_open(key, {[n0, n1, n2, n3] : List<&2, U32>}, aad, ct) : Maybe<&2, List<&2, U32>>}, 4n, 12n, hn, {==})
313    case n0 <> n1 <> n2 <> n3 <> n4 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, {[n0, n1, n2, n3, n4] : List<&2, U32>}, aad, ct) == G.aes_open(key, {[n0, n1, n2, n3, n4] : List<&2, U32>}, aad, ct) : Maybe<&2, List<&2, U32>>}, 5n, 12n, hn, {==})
314    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, {[n0, n1, n2, n3, n4, n5] : List<&2, U32>}, aad, ct) == G.aes_open(key, {[n0, n1, n2, n3, n4, n5] : List<&2, U32>}, aad, ct) : Maybe<&2, List<&2, U32>>}, 6n, 12n, hn, {==})
315    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, {[n0, n1, n2, n3, n4, n5, n6] : List<&2, U32>}, aad, ct) == G.aes_open(key, {[n0, n1, n2, n3, n4, n5, n6] : List<&2, U32>}, aad, ct) : Maybe<&2, List<&2, U32>>}, 7n, 12n, hn, {==})
316    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7] : List<&2, U32>}, aad, ct) == G.aes_open(key, {[n0, n1, n2, n3, n4, n5, n6, n7] : List<&2, U32>}, aad, ct) : Maybe<&2, List<&2, U32>>}, 8n, 12n, hn, {==})
317    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8] : List<&2, U32>}, aad, ct) == G.aes_open(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8] : List<&2, U32>}, aad, ct) : Maybe<&2, List<&2, U32>>}, 9n, 12n, hn, {==})
318    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8, n9] : List<&2, U32>}, aad, ct) == G.aes_open(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8, n9] : List<&2, U32>}, aad, ct) : Maybe<&2, List<&2, U32>>}, 10n, 12n, hn, {==})
319    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10] : List<&2, U32>}, aad, ct) == G.aes_open(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10] : List<&2, U32>}, aad, ct) : Maybe<&2, List<&2, U32>>}, 11n, 12n, hn, {==})
320    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> Nil{}: aes128_decrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, ct)
321    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> nx <> nrest: no_len({GCM.aes128_gcm_decrypt(key, {n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> nx <> nrest : List<&2, U32>}, aad, ct) == G.aes_open(key, {n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> nx <> nrest : List<&2, U32>}, aad, ct) : Maybe<&2, List<&2, U32>>}, 13n+List.length(&2, U32, nrest), 12n, hn, {==})
322
323law aes128_roundtrip_l:
324  for +key: List<&2, U32>
325  for +h: {List.length(&2, U32, key) == 16n : Nat}
326  for +nonce: List<&2, U32>
327  for +hn: {List.length(&2, U32, nonce) == 12n : Nat}
328  for +aad: List<&2, U32>
329  for +pt: List<&2, U32>
330  {open128(key, nonce, aad, GCM.aes128_gcm_encrypt(key, nonce, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}
331
332def aes128_roundtrip_l(key, h, nonce, hn, aad, pt):
333  match nonce:
334    case Nil{}: no_len({open128(key, {Nil{} : List<&2, U32>}, aad, GCM.aes128_gcm_encrypt(key, {Nil{} : List<&2, U32>}, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}, 0n, 12n, hn, {==})
335    case n0 <> Nil{}: no_len({open128(key, {[n0] : List<&2, U32>}, aad, GCM.aes128_gcm_encrypt(key, {[n0] : List<&2, U32>}, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}, 1n, 12n, hn, {==})
336    case n0 <> n1 <> Nil{}: no_len({open128(key, {[n0, n1] : List<&2, U32>}, aad, GCM.aes128_gcm_encrypt(key, {[n0, n1] : List<&2, U32>}, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}, 2n, 12n, hn, {==})
337    case n0 <> n1 <> n2 <> Nil{}: no_len({open128(key, {[n0, n1, n2] : List<&2, U32>}, aad, GCM.aes128_gcm_encrypt(key, {[n0, n1, n2] : List<&2, U32>}, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}, 3n, 12n, hn, {==})
338    case n0 <> n1 <> n2 <> n3 <> Nil{}: no_len({open128(key, {[n0, n1, n2, n3] : List<&2, U32>}, aad, GCM.aes128_gcm_encrypt(key, {[n0, n1, n2, n3] : List<&2, U32>}, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}, 4n, 12n, hn, {==})
339    case n0 <> n1 <> n2 <> n3 <> n4 <> Nil{}: no_len({open128(key, {[n0, n1, n2, n3, n4] : List<&2, U32>}, aad, GCM.aes128_gcm_encrypt(key, {[n0, n1, n2, n3, n4] : List<&2, U32>}, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}, 5n, 12n, hn, {==})
340    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> Nil{}: no_len({open128(key, {[n0, n1, n2, n3, n4, n5] : List<&2, U32>}, aad, GCM.aes128_gcm_encrypt(key, {[n0, n1, n2, n3, n4, n5] : List<&2, U32>}, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}, 6n, 12n, hn, {==})
341    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> Nil{}: no_len({open128(key, {[n0, n1, n2, n3, n4, n5, n6] : List<&2, U32>}, aad, GCM.aes128_gcm_encrypt(key, {[n0, n1, n2, n3, n4, n5, n6] : List<&2, U32>}, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}, 7n, 12n, hn, {==})
342    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> Nil{}: no_len({open128(key, {[n0, n1, n2, n3, n4, n5, n6, n7] : List<&2, U32>}, aad, GCM.aes128_gcm_encrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7] : List<&2, U32>}, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}, 8n, 12n, hn, {==})
343    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> Nil{}: no_len({open128(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8] : List<&2, U32>}, aad, GCM.aes128_gcm_encrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8] : List<&2, U32>}, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}, 9n, 12n, hn, {==})
344    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> Nil{}: no_len({open128(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8, n9] : List<&2, U32>}, aad, GCM.aes128_gcm_encrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8, n9] : List<&2, U32>}, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}, 10n, 12n, hn, {==})
345    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> Nil{}: no_len({open128(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10] : List<&2, U32>}, aad, GCM.aes128_gcm_encrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10] : List<&2, U32>}, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}, 11n, 12n, hn, {==})
346    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> Nil{}: aes128_roundtrip(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt)
347    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> nx <> nrest: no_len({open128(key, {n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> nx <> nrest : List<&2, U32>}, aad, GCM.aes128_gcm_encrypt(key, {n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> nx <> nrest : List<&2, U32>}, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}, 13n+List.length(&2, U32, nrest), 12n, hn, {==})
348
349law aes128_forgery_t:
350  for +key: List<&2, U32>
351  for +h: {List.length(&2, U32, key) == 16n : Nat}
352  for +n0: U32
353  for +n1: U32
354  for +n2: U32
355  for +n3: U32
356  for +n4: U32
357  for +n5: U32
358  for +n6: U32
359  for +n7: U32
360  for +n8: U32
361  for +n9: U32
362  for +n10: U32
363  for +n11: U32
364  for +aad: List<&2, U32>
365  for +c: List<&2, U32>
366  for +t: List<&2, U32>
367  for +ht: {List.length(&2, U32, t) == 16n : Nat}
368  for ne: {t != G.aes_tag(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, c) : List<&2, U32>}
369  {GCM.aes128_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}
370
371def aes128_forgery_t(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, c, t, ht, ne):
372  match t:
373    case Nil{}: no_len({GCM.aes128_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {Nil{} : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 0n, 16n, ht, {==})
374    case t0 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {[t0] : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 1n, 16n, ht, {==})
375    case t0 <> t1 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {[t0, t1] : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 2n, 16n, ht, {==})
376    case t0 <> t1 <> t2 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {[t0, t1, t2] : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 3n, 16n, ht, {==})
377    case t0 <> t1 <> t2 <> t3 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {[t0, t1, t2, t3] : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 4n, 16n, ht, {==})
378    case t0 <> t1 <> t2 <> t3 <> t4 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {[t0, t1, t2, t3, t4] : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 5n, 16n, ht, {==})
379    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {[t0, t1, t2, t3, t4, t5] : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 6n, 16n, ht, {==})
380    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {[t0, t1, t2, t3, t4, t5, t6] : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 7n, 16n, ht, {==})
381    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {[t0, t1, t2, t3, t4, t5, t6, t7] : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 8n, 16n, ht, {==})
382    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {[t0, t1, t2, t3, t4, t5, t6, t7, t8] : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 9n, 16n, ht, {==})
383    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {[t0, t1, t2, t3, t4, t5, t6, t7, t8, t9] : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 10n, 16n, ht, {==})
384    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {[t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10] : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 11n, 16n, ht, {==})
385    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {[t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11] : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 12n, 16n, ht, {==})
386    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {[t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12] : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 13n, 16n, ht, {==})
387    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {[t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13] : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 14n, 16n, ht, {==})
388    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {[t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14] : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 15n, 16n, ht, {==})
389    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> Nil{}: aes128_forgery(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, c, t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, ne)
390    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> tx <> trest: no_len({GCM.aes128_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> tx <> trest : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 17n+List.length(&2, U32, trest), 16n, ht, {==})
391
392law aes128_forgery_l:
393  for +key: List<&2, U32>
394  for +h: {List.length(&2, U32, key) == 16n : Nat}
395  for +nonce: List<&2, U32>
396  for +hn: {List.length(&2, U32, nonce) == 12n : Nat}
397  for +aad: List<&2, U32>
398  for +c: List<&2, U32>
399  for +t: List<&2, U32>
400  for +ht: {List.length(&2, U32, t) == 16n : Nat}
401  for ne: {t != G.aes_tag(key, nonce, aad, c) : List<&2, U32>}
402  {GCM.aes128_gcm_decrypt(key, nonce, aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}
403
404def aes128_forgery_l(key, h, nonce, hn, aad, c, t, ht, ne):
405  match nonce:
406    case Nil{}: no_len({GCM.aes128_gcm_decrypt(key, {Nil{} : List<&2, U32>}, aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}, 0n, 12n, hn, {==})
407    case n0 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, {[n0] : List<&2, U32>}, aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}, 1n, 12n, hn, {==})
408    case n0 <> n1 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, {[n0, n1] : List<&2, U32>}, aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}, 2n, 12n, hn, {==})
409    case n0 <> n1 <> n2 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, {[n0, n1, n2] : List<&2, U32>}, aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}, 3n, 12n, hn, {==})
410    case n0 <> n1 <> n2 <> n3 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, {[n0, n1, n2, n3] : List<&2, U32>}, aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}, 4n, 12n, hn, {==})
411    case n0 <> n1 <> n2 <> n3 <> n4 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, {[n0, n1, n2, n3, n4] : List<&2, U32>}, aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}, 5n, 12n, hn, {==})
412    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, {[n0, n1, n2, n3, n4, n5] : List<&2, U32>}, aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}, 6n, 12n, hn, {==})
413    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, {[n0, n1, n2, n3, n4, n5, n6] : List<&2, U32>}, aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}, 7n, 12n, hn, {==})
414    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7] : List<&2, U32>}, aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}, 8n, 12n, hn, {==})
415    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8] : List<&2, U32>}, aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}, 9n, 12n, hn, {==})
416    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8, n9] : List<&2, U32>}, aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}, 10n, 12n, hn, {==})
417    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> Nil{}: no_len({GCM.aes128_gcm_decrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10] : List<&2, U32>}, aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}, 11n, 12n, hn, {==})
418    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> Nil{}: aes128_forgery_t(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, c, t, ht, ne)
419    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> nx <> nrest: no_len({GCM.aes128_gcm_decrypt(key, {n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> nx <> nrest : List<&2, U32>}, aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}, 13n+List.length(&2, U32, nrest), 12n, hn, {==})
420
421law aes256_encrypt_l:
422  for +key: List<&2, U32>
423  for +h: {List.length(&2, U32, key) == 32n : Nat}
424  for +nonce: List<&2, U32>
425  for +hn: {List.length(&2, U32, nonce) == 12n : Nat}
426  for +aad: List<&2, U32>
427  for +pt: List<&2, U32>
428  {GCM.aes256_gcm_encrypt(key, nonce, aad, pt) == Some{G.aes_seal(key, nonce, aad, pt)} : Maybe<&2, List<&2, U32>>}
429
430def aes256_encrypt_l(key, h, nonce, hn, aad, pt):
431  match nonce:
432    case Nil{}: no_len({GCM.aes256_gcm_encrypt(key, {Nil{} : List<&2, U32>}, aad, pt) == Some{G.aes_seal(key, {Nil{} : List<&2, U32>}, aad, pt)} : Maybe<&2, List<&2, U32>>}, 0n, 12n, hn, {==})
433    case n0 <> Nil{}: no_len({GCM.aes256_gcm_encrypt(key, {[n0] : List<&2, U32>}, aad, pt) == Some{G.aes_seal(key, {[n0] : List<&2, U32>}, aad, pt)} : Maybe<&2, List<&2, U32>>}, 1n, 12n, hn, {==})
434    case n0 <> n1 <> Nil{}: no_len({GCM.aes256_gcm_encrypt(key, {[n0, n1] : List<&2, U32>}, aad, pt) == Some{G.aes_seal(key, {[n0, n1] : List<&2, U32>}, aad, pt)} : Maybe<&2, List<&2, U32>>}, 2n, 12n, hn, {==})
435    case n0 <> n1 <> n2 <> Nil{}: no_len({GCM.aes256_gcm_encrypt(key, {[n0, n1, n2] : List<&2, U32>}, aad, pt) == Some{G.aes_seal(key, {[n0, n1, n2] : List<&2, U32>}, aad, pt)} : Maybe<&2, List<&2, U32>>}, 3n, 12n, hn, {==})
436    case n0 <> n1 <> n2 <> n3 <> Nil{}: no_len({GCM.aes256_gcm_encrypt(key, {[n0, n1, n2, n3] : List<&2, U32>}, aad, pt) == Some{G.aes_seal(key, {[n0, n1, n2, n3] : List<&2, U32>}, aad, pt)} : Maybe<&2, List<&2, U32>>}, 4n, 12n, hn, {==})
437    case n0 <> n1 <> n2 <> n3 <> n4 <> Nil{}: no_len({GCM.aes256_gcm_encrypt(key, {[n0, n1, n2, n3, n4] : List<&2, U32>}, aad, pt) == Some{G.aes_seal(key, {[n0, n1, n2, n3, n4] : List<&2, U32>}, aad, pt)} : Maybe<&2, List<&2, U32>>}, 5n, 12n, hn, {==})
438    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> Nil{}: no_len({GCM.aes256_gcm_encrypt(key, {[n0, n1, n2, n3, n4, n5] : List<&2, U32>}, aad, pt) == Some{G.aes_seal(key, {[n0, n1, n2, n3, n4, n5] : List<&2, U32>}, aad, pt)} : Maybe<&2, List<&2, U32>>}, 6n, 12n, hn, {==})
439    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> Nil{}: no_len({GCM.aes256_gcm_encrypt(key, {[n0, n1, n2, n3, n4, n5, n6] : List<&2, U32>}, aad, pt) == Some{G.aes_seal(key, {[n0, n1, n2, n3, n4, n5, n6] : List<&2, U32>}, aad, pt)} : Maybe<&2, List<&2, U32>>}, 7n, 12n, hn, {==})
440    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> Nil{}: no_len({GCM.aes256_gcm_encrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7] : List<&2, U32>}, aad, pt) == Some{G.aes_seal(key, {[n0, n1, n2, n3, n4, n5, n6, n7] : List<&2, U32>}, aad, pt)} : Maybe<&2, List<&2, U32>>}, 8n, 12n, hn, {==})
441    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> Nil{}: no_len({GCM.aes256_gcm_encrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8] : List<&2, U32>}, aad, pt) == Some{G.aes_seal(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8] : List<&2, U32>}, aad, pt)} : Maybe<&2, List<&2, U32>>}, 9n, 12n, hn, {==})
442    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> Nil{}: no_len({GCM.aes256_gcm_encrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8, n9] : List<&2, U32>}, aad, pt) == Some{G.aes_seal(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8, n9] : List<&2, U32>}, aad, pt)} : Maybe<&2, List<&2, U32>>}, 10n, 12n, hn, {==})
443    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> Nil{}: no_len({GCM.aes256_gcm_encrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10] : List<&2, U32>}, aad, pt) == Some{G.aes_seal(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10] : List<&2, U32>}, aad, pt)} : Maybe<&2, List<&2, U32>>}, 11n, 12n, hn, {==})
444    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> Nil{}: aes256_encrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt)
445    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> nx <> nrest: no_len({GCM.aes256_gcm_encrypt(key, {n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> nx <> nrest : List<&2, U32>}, aad, pt) == Some{G.aes_seal(key, {n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> nx <> nrest : List<&2, U32>}, aad, pt)} : Maybe<&2, List<&2, U32>>}, 13n+List.length(&2, U32, nrest), 12n, hn, {==})
446
447law aes256_decrypt_l:
448  for +key: List<&2, U32>
449  for +h: {List.length(&2, U32, key) == 32n : Nat}
450  for +nonce: List<&2, U32>
451  for +hn: {List.length(&2, U32, nonce) == 12n : Nat}
452  for +aad: List<&2, U32>
453  for +ct: List<&2, U32>
454  {GCM.aes256_gcm_decrypt(key, nonce, aad, ct) == G.aes_open(key, nonce, aad, ct) : Maybe<&2, List<&2, U32>>}
455
456def aes256_decrypt_l(key, h, nonce, hn, aad, ct):
457  match nonce:
458    case Nil{}: no_len({GCM.aes256_gcm_decrypt(key, {Nil{} : List<&2, U32>}, aad, ct) == G.aes_open(key, {Nil{} : List<&2, U32>}, aad, ct) : Maybe<&2, List<&2, U32>>}, 0n, 12n, hn, {==})
459    case n0 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, {[n0] : List<&2, U32>}, aad, ct) == G.aes_open(key, {[n0] : List<&2, U32>}, aad, ct) : Maybe<&2, List<&2, U32>>}, 1n, 12n, hn, {==})
460    case n0 <> n1 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, {[n0, n1] : List<&2, U32>}, aad, ct) == G.aes_open(key, {[n0, n1] : List<&2, U32>}, aad, ct) : Maybe<&2, List<&2, U32>>}, 2n, 12n, hn, {==})
461    case n0 <> n1 <> n2 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, {[n0, n1, n2] : List<&2, U32>}, aad, ct) == G.aes_open(key, {[n0, n1, n2] : List<&2, U32>}, aad, ct) : Maybe<&2, List<&2, U32>>}, 3n, 12n, hn, {==})
462    case n0 <> n1 <> n2 <> n3 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, {[n0, n1, n2, n3] : List<&2, U32>}, aad, ct) == G.aes_open(key, {[n0, n1, n2, n3] : List<&2, U32>}, aad, ct) : Maybe<&2, List<&2, U32>>}, 4n, 12n, hn, {==})
463    case n0 <> n1 <> n2 <> n3 <> n4 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, {[n0, n1, n2, n3, n4] : List<&2, U32>}, aad, ct) == G.aes_open(key, {[n0, n1, n2, n3, n4] : List<&2, U32>}, aad, ct) : Maybe<&2, List<&2, U32>>}, 5n, 12n, hn, {==})
464    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, {[n0, n1, n2, n3, n4, n5] : List<&2, U32>}, aad, ct) == G.aes_open(key, {[n0, n1, n2, n3, n4, n5] : List<&2, U32>}, aad, ct) : Maybe<&2, List<&2, U32>>}, 6n, 12n, hn, {==})
465    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, {[n0, n1, n2, n3, n4, n5, n6] : List<&2, U32>}, aad, ct) == G.aes_open(key, {[n0, n1, n2, n3, n4, n5, n6] : List<&2, U32>}, aad, ct) : Maybe<&2, List<&2, U32>>}, 7n, 12n, hn, {==})
466    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7] : List<&2, U32>}, aad, ct) == G.aes_open(key, {[n0, n1, n2, n3, n4, n5, n6, n7] : List<&2, U32>}, aad, ct) : Maybe<&2, List<&2, U32>>}, 8n, 12n, hn, {==})
467    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8] : List<&2, U32>}, aad, ct) == G.aes_open(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8] : List<&2, U32>}, aad, ct) : Maybe<&2, List<&2, U32>>}, 9n, 12n, hn, {==})
468    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8, n9] : List<&2, U32>}, aad, ct) == G.aes_open(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8, n9] : List<&2, U32>}, aad, ct) : Maybe<&2, List<&2, U32>>}, 10n, 12n, hn, {==})
469    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10] : List<&2, U32>}, aad, ct) == G.aes_open(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10] : List<&2, U32>}, aad, ct) : Maybe<&2, List<&2, U32>>}, 11n, 12n, hn, {==})
470    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> Nil{}: aes256_decrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, ct)
471    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> nx <> nrest: no_len({GCM.aes256_gcm_decrypt(key, {n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> nx <> nrest : List<&2, U32>}, aad, ct) == G.aes_open(key, {n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> nx <> nrest : List<&2, U32>}, aad, ct) : Maybe<&2, List<&2, U32>>}, 13n+List.length(&2, U32, nrest), 12n, hn, {==})
472
473law aes256_roundtrip_l:
474  for +key: List<&2, U32>
475  for +h: {List.length(&2, U32, key) == 32n : Nat}
476  for +nonce: List<&2, U32>
477  for +hn: {List.length(&2, U32, nonce) == 12n : Nat}
478  for +aad: List<&2, U32>
479  for +pt: List<&2, U32>
480  {open256(key, nonce, aad, GCM.aes256_gcm_encrypt(key, nonce, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}
481
482def aes256_roundtrip_l(key, h, nonce, hn, aad, pt):
483  match nonce:
484    case Nil{}: no_len({open256(key, {Nil{} : List<&2, U32>}, aad, GCM.aes256_gcm_encrypt(key, {Nil{} : List<&2, U32>}, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}, 0n, 12n, hn, {==})
485    case n0 <> Nil{}: no_len({open256(key, {[n0] : List<&2, U32>}, aad, GCM.aes256_gcm_encrypt(key, {[n0] : List<&2, U32>}, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}, 1n, 12n, hn, {==})
486    case n0 <> n1 <> Nil{}: no_len({open256(key, {[n0, n1] : List<&2, U32>}, aad, GCM.aes256_gcm_encrypt(key, {[n0, n1] : List<&2, U32>}, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}, 2n, 12n, hn, {==})
487    case n0 <> n1 <> n2 <> Nil{}: no_len({open256(key, {[n0, n1, n2] : List<&2, U32>}, aad, GCM.aes256_gcm_encrypt(key, {[n0, n1, n2] : List<&2, U32>}, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}, 3n, 12n, hn, {==})
488    case n0 <> n1 <> n2 <> n3 <> Nil{}: no_len({open256(key, {[n0, n1, n2, n3] : List<&2, U32>}, aad, GCM.aes256_gcm_encrypt(key, {[n0, n1, n2, n3] : List<&2, U32>}, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}, 4n, 12n, hn, {==})
489    case n0 <> n1 <> n2 <> n3 <> n4 <> Nil{}: no_len({open256(key, {[n0, n1, n2, n3, n4] : List<&2, U32>}, aad, GCM.aes256_gcm_encrypt(key, {[n0, n1, n2, n3, n4] : List<&2, U32>}, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}, 5n, 12n, hn, {==})
490    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> Nil{}: no_len({open256(key, {[n0, n1, n2, n3, n4, n5] : List<&2, U32>}, aad, GCM.aes256_gcm_encrypt(key, {[n0, n1, n2, n3, n4, n5] : List<&2, U32>}, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}, 6n, 12n, hn, {==})
491    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> Nil{}: no_len({open256(key, {[n0, n1, n2, n3, n4, n5, n6] : List<&2, U32>}, aad, GCM.aes256_gcm_encrypt(key, {[n0, n1, n2, n3, n4, n5, n6] : List<&2, U32>}, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}, 7n, 12n, hn, {==})
492    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> Nil{}: no_len({open256(key, {[n0, n1, n2, n3, n4, n5, n6, n7] : List<&2, U32>}, aad, GCM.aes256_gcm_encrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7] : List<&2, U32>}, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}, 8n, 12n, hn, {==})
493    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> Nil{}: no_len({open256(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8] : List<&2, U32>}, aad, GCM.aes256_gcm_encrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8] : List<&2, U32>}, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}, 9n, 12n, hn, {==})
494    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> Nil{}: no_len({open256(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8, n9] : List<&2, U32>}, aad, GCM.aes256_gcm_encrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8, n9] : List<&2, U32>}, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}, 10n, 12n, hn, {==})
495    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> Nil{}: no_len({open256(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10] : List<&2, U32>}, aad, GCM.aes256_gcm_encrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10] : List<&2, U32>}, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}, 11n, 12n, hn, {==})
496    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> Nil{}: aes256_roundtrip(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt)
497    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> nx <> nrest: no_len({open256(key, {n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> nx <> nrest : List<&2, U32>}, aad, GCM.aes256_gcm_encrypt(key, {n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> nx <> nrest : List<&2, U32>}, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}, 13n+List.length(&2, U32, nrest), 12n, hn, {==})
498
499law aes256_forgery_t:
500  for +key: List<&2, U32>
501  for +h: {List.length(&2, U32, key) == 32n : Nat}
502  for +n0: U32
503  for +n1: U32
504  for +n2: U32
505  for +n3: U32
506  for +n4: U32
507  for +n5: U32
508  for +n6: U32
509  for +n7: U32
510  for +n8: U32
511  for +n9: U32
512  for +n10: U32
513  for +n11: U32
514  for +aad: List<&2, U32>
515  for +c: List<&2, U32>
516  for +t: List<&2, U32>
517  for +ht: {List.length(&2, U32, t) == 16n : Nat}
518  for ne: {t != G.aes_tag(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, c) : List<&2, U32>}
519  {GCM.aes256_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}
520
521def aes256_forgery_t(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, c, t, ht, ne):
522  match t:
523    case Nil{}: no_len({GCM.aes256_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {Nil{} : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 0n, 16n, ht, {==})
524    case t0 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {[t0] : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 1n, 16n, ht, {==})
525    case t0 <> t1 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {[t0, t1] : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 2n, 16n, ht, {==})
526    case t0 <> t1 <> t2 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {[t0, t1, t2] : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 3n, 16n, ht, {==})
527    case t0 <> t1 <> t2 <> t3 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {[t0, t1, t2, t3] : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 4n, 16n, ht, {==})
528    case t0 <> t1 <> t2 <> t3 <> t4 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {[t0, t1, t2, t3, t4] : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 5n, 16n, ht, {==})
529    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {[t0, t1, t2, t3, t4, t5] : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 6n, 16n, ht, {==})
530    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {[t0, t1, t2, t3, t4, t5, t6] : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 7n, 16n, ht, {==})
531    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {[t0, t1, t2, t3, t4, t5, t6, t7] : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 8n, 16n, ht, {==})
532    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {[t0, t1, t2, t3, t4, t5, t6, t7, t8] : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 9n, 16n, ht, {==})
533    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {[t0, t1, t2, t3, t4, t5, t6, t7, t8, t9] : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 10n, 16n, ht, {==})
534    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {[t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10] : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 11n, 16n, ht, {==})
535    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {[t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11] : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 12n, 16n, ht, {==})
536    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {[t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12] : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 13n, 16n, ht, {==})
537    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {[t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13] : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 14n, 16n, ht, {==})
538    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {[t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14] : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 15n, 16n, ht, {==})
539    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> Nil{}: aes256_forgery(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, c, t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, ne)
540    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> tx <> trest: no_len({GCM.aes256_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, {t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> tx <> trest : List<&2, U32>})) == None{} : Maybe<&2, List<&2, U32>>}, 17n+List.length(&2, U32, trest), 16n, ht, {==})
541
542law aes256_forgery_l:
543  for +key: List<&2, U32>
544  for +h: {List.length(&2, U32, key) == 32n : Nat}
545  for +nonce: List<&2, U32>
546  for +hn: {List.length(&2, U32, nonce) == 12n : Nat}
547  for +aad: List<&2, U32>
548  for +c: List<&2, U32>
549  for +t: List<&2, U32>
550  for +ht: {List.length(&2, U32, t) == 16n : Nat}
551  for ne: {t != G.aes_tag(key, nonce, aad, c) : List<&2, U32>}
552  {GCM.aes256_gcm_decrypt(key, nonce, aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}
553
554def aes256_forgery_l(key, h, nonce, hn, aad, c, t, ht, ne):
555  match nonce:
556    case Nil{}: no_len({GCM.aes256_gcm_decrypt(key, {Nil{} : List<&2, U32>}, aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}, 0n, 12n, hn, {==})
557    case n0 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, {[n0] : List<&2, U32>}, aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}, 1n, 12n, hn, {==})
558    case n0 <> n1 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, {[n0, n1] : List<&2, U32>}, aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}, 2n, 12n, hn, {==})
559    case n0 <> n1 <> n2 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, {[n0, n1, n2] : List<&2, U32>}, aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}, 3n, 12n, hn, {==})
560    case n0 <> n1 <> n2 <> n3 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, {[n0, n1, n2, n3] : List<&2, U32>}, aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}, 4n, 12n, hn, {==})
561    case n0 <> n1 <> n2 <> n3 <> n4 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, {[n0, n1, n2, n3, n4] : List<&2, U32>}, aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}, 5n, 12n, hn, {==})
562    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, {[n0, n1, n2, n3, n4, n5] : List<&2, U32>}, aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}, 6n, 12n, hn, {==})
563    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, {[n0, n1, n2, n3, n4, n5, n6] : List<&2, U32>}, aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}, 7n, 12n, hn, {==})
564    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7] : List<&2, U32>}, aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}, 8n, 12n, hn, {==})
565    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8] : List<&2, U32>}, aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}, 9n, 12n, hn, {==})
566    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8, n9] : List<&2, U32>}, aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}, 10n, 12n, hn, {==})
567    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> Nil{}: no_len({GCM.aes256_gcm_decrypt(key, {[n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10] : List<&2, U32>}, aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}, 11n, 12n, hn, {==})
568    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> Nil{}: aes256_forgery_t(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, c, t, ht, ne)
569    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> nx <> nrest: no_len({GCM.aes256_gcm_decrypt(key, {n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> nx <> nrest : List<&2, U32>}, aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}, 13n+List.length(&2, U32, nrest), 12n, hn, {==})