1	import Base
2	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
3	import bend-osdev-bytes@0.1.0.0/LAWS.bend as BL
4	import bend-osdev-bytes@0.1.0.0/PROOF.bend as BP
5	import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
6	import ./aead.bend as Ad
7	import ./aesround.bend as R
8	import ./aegis128.bend as G
9	import ./authenc.bend as Au
10	import ./essiv.bend as Es
11	import ./seqiv.bend as Sq
12	import ./echainiv.bend as Ec
13	import ./LAWS.bend as Laws
14	
15	# BEGIN GENERATED by gen/proof.py: bits
16	# the low byte of a XOR depends only on the low byte of its first operand
17	def byte_xor_byte(z: U32, k: U32) -> {B.byte(U32.xor(z, k)) == B.byte(U32.xor(B.byte(z), k)) : U32}:
18	  match z k:
19	    case U32{WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, WCon{a8, WCon{a9, WCon{a10, WCon{a11, WCon{a12, WCon{a13, WCon{a14, WCon{a15, WCon{a16, WCon{a17, WCon{a18, WCon{a19, WCon{a20, WCon{a21, WCon{a22, WCon{a23, WCon{a24, WCon{a25, WCon{a26, WCon{a27, WCon{a28, WCon{a29, WCon{a30, WCon{a31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
20	      {==}
21	
22	# a word's big-endian bytes are four
23	def be32_len(v: U32) -> {4n == B.len(B.be32(v)) : Nat}:
24	  match v:
25	    case U32{WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, WCon{a8, WCon{a9, WCon{a10, WCon{a11, WCon{a12, WCon{a13, WCon{a14, WCon{a15, WCon{a16, WCon{a17, WCon{a18, WCon{a19, WCon{a20, WCon{a21, WCon{a22, WCon{a23, WCon{a24, WCon{a25, WCon{a26, WCon{a27, WCon{a28, WCon{a29, WCon{a30, WCon{a31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
26	      {==}
27	
28	# a byte masked again is itself
29	def byte_byte(h: U32) -> {B.byte(h) == B.byte(B.byte(h)) : U32}:
30	  match h:
31	    case U32{WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, WCon{a8, WCon{a9, WCon{a10, WCon{a11, WCon{a12, WCon{a13, WCon{a14, WCon{a15, WCon{a16, WCon{a17, WCon{a18, WCon{a19, WCon{a20, WCon{a21, WCon{a22, WCon{a23, WCon{a24, WCon{a25, WCon{a26, WCon{a27, WCon{a28, WCon{a29, WCon{a30, WCon{a31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
32	      {==}
33	# END GENERATED: bits
34	
35	# XOR undone: a == (a xor b) xor b, for every bit and word, and on a byte.
36	# Each lemma is stated simple side first, the form a rewrite (%e : P) takes.
37	
38	def bool_xx(a: Bool, b: Bool) -> {a == Bool.xor(Bool.xor(a, b), b) : Bool}:
39	  match a b:
40	    case True{} True{}:
41	      {==}
42	    case True{} False{}:
43	      {==}
44	    case False{} True{}:
45	      {==}
46	    case False{} False{}:
47	      {==}
48	
49	def word_xx(n: Nat, a: Word(n), b: Word(n)) -> {a == Word.xor(n, Word.xor(n, a, b), b) : Word(n)}:
50	  match n:
51	    case 0n:
52	      match a b:
53	        case WNil{} WNil{}:
54	          {==}
55	    case 1n+p:
56	      match a b:
57	        case WCon{ah, at} WCon{bh, bt}:
58	          %bool_xx(ah, bh) : {WCon{ah, at} == WCon{_, Word.xor(p, Word.xor(p, at, bt), bt)} : Word(1n+p)}
59	          %word_xx(p, at, bt) : {WCon{ah, at} == WCon{ah, _} : Word(1n+p)}
60	          {==}
61	
62	def u32_xx(a: U32, b: U32) -> {a == U32.xor(U32.xor(a, b), b) : U32}:
63	  match a b:
64	    case U32{x} U32{y}:
65	      %word_xx(32n, x, y) : {U32{x} == U32{_} : U32}
66	      {==}
67	
68	def byte_xx(+h: U32, +k: U32) -> {B.byte(h) == B.byte(U32.xor(B.byte(U32.xor(h, k)), k)) : U32}:
69	  %byte_xor_byte(U32.xor(h, k), k) : {B.byte(h) == _ : U32}
70	  %u32_xx(h, k) : {B.byte(h) == B.byte(_) : U32}
71	  {==}
72	
73	# Natural numbers
74	
75	def nat_add_zero(x: Nat) -> {x == Nat.add(x, 0n) : Nat}:
76	  match x:
77	    case 0n:
78	      {==}
79	    case 1n+p:
80	      %nat_add_zero(p) : {1n+p == 1n+_ : Nat}
81	      {==}
82	
83	def nat_add_succ(x: Nat, +t: Nat) -> {1n+Nat.add(x, t) == Nat.add(x, 1n+t) : Nat}:
84	  match x:
85	    case 0n:
86	      {==}
87	    case 1n+p:
88	      %nat_add_succ(p, t) : {1n+1n+Nat.add(p, t) == 1n+_ : Nat}
89	      {==}
90	
91	def nat_sub_zero(x: Nat) -> {x == Nat.sub(x, 0n) : Nat}:
92	  match x:
93	    case 0n:
94	      {==}
95	    case 1n+p:
96	      {==}
97	
98	def nat_sub_add(+x: Nat, t: Nat) -> {x == Nat.sub(Nat.add(x, t), t) : Nat}:
99	  match t:
100	    case 0n:
101	      %nat_add_zero(x) : {x == Nat.sub(_, 0n) : Nat}
102	      nat_sub_zero(x)
103	    case 1n+(+u):
104	      %nat_add_succ(x, u) : {x == Nat.sub(_, 1n+u) : Nat}
105	      nat_sub_add(x, u)
106	
107	def nat_lt_zero(x: Nat) -> {False{} == Nat.is_lt(x, 0n) : Bool}:
108	  match x:
109	    case 0n:
110	      {==}
111	    case 1n+p:
112	      {==}
113	
114	def nat_lt_add(+x: Nat, t: Nat) -> {False{} == Nat.is_lt(Nat.add(x, t), t) : Bool}:
115	  match t:
116	    case 0n:
117	      %nat_add_zero(x) : {False{} == Nat.is_lt(_, 0n) : Bool}
118	      nat_lt_zero(x)
119	    case 1n+(+u):
120	      %nat_add_succ(x, u) : {False{} == Nat.is_lt(_, 1n+u) : Bool}
121	      nat_lt_add(x, u)
122	
123	# Lists and Octets
124	
125	def len_append(xs: List<&2, U32>, +ys: List<&2, U32>) -> {Nat.add(B.len(xs), B.len(ys)) == B.len(B.append(xs, ys)) : Nat}:
126	  match xs:
127	    case Nil{}:
128	      {==}
129	    case Con{h, t}:
130	      %len_append(t, ys) : {1n+Nat.add(B.len(t), B.len(ys)) == 1n+_ : Nat}
131	      {==}
132	
133	def mask_len(xs: List<&2, U32>) -> {B.len(xs) == B.len(B.mask(xs)) : Nat}:
134	  match xs:
135	    case Nil{}:
136	      {==}
137	    case Con{h, t}:
138	      %mask_len(t) : {1n+B.len(t) == 1n+_ : Nat}
139	      {==}
140	
141	# the length of a list made Octets
142	def olen_of(+xs: List<&2, U32>) -> {B.len(xs) == B.Octets.len(B.Octets.of_list(xs)) : Nat}:
143	  %Equal.sym(Nat, B.Octets.len(B.Octets.of_list(xs)), B.len(B.Octets.to_list(B.Octets.of_list(xs))), BL.octets_len_list(B.Octets.of_list(xs))) : {B.len(xs) == _ : Nat}
144	  %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.of_list(xs)), B.mask(xs), BL.octets_to_of(xs)) : {B.len(xs) == B.len(_) : Nat}
145	  mask_len(xs)
146	
147	# the length of a joined string
148	def olen_append(+a: B.Octets, +b: B.Octets) -> {Nat.add(B.Octets.len(a), B.Octets.len(b)) == B.Octets.len(B.Octets.append(a, b)) : Nat}:
149	  %Equal.sym(Nat, B.Octets.len(B.Octets.append(a, b)), B.len(B.Octets.to_list(B.Octets.append(a, b))), BL.octets_len_list(B.Octets.append(a, b))) : {Nat.add(B.Octets.len(a), B.Octets.len(b)) == _ : Nat}
150	  %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.append(a, b)), B.append(B.Octets.to_list(a), B.Octets.to_list(b)), BL.octets_append_list(a, b)) : {Nat.add(B.Octets.len(a), B.Octets.len(b)) == B.len(_) : Nat}
151	  %len_append(B.Octets.to_list(a), B.Octets.to_list(b)) : {Nat.add(B.Octets.len(a), B.Octets.len(b)) == _ : Nat}
152	  %BL.octets_len_list(a) : {Nat.add(B.Octets.len(a), B.Octets.len(b)) == Nat.add(_, B.len(B.Octets.to_list(b))) : Nat}
153	  %BL.octets_len_list(b) : {Nat.add(B.Octets.len(a), B.Octets.len(b)) == Nat.add(B.Octets.len(a), _) : Nat}
154	  {==}
155	
156	# A ciphertext joined with its tag splits back into the two
157	def split_join(+c: B.Octets, +t: B.Octets) -> {Done{Ad.AdSplit{c, t}} == Ad.AdTag.split(B.Octets.len(t), B.Octets.append(c, t)) : Result<&2, &2, Cr.CrError, Ad.AdSplit>}:
158	  %olen_append(c, t) : {Done{Ad.AdSplit{c, t}} == Ad.ad.split.pick(Nat.is_lt(_, B.Octets.len(t)), B.Octets.len(t), B.Octets.append(c, t)) : Result<&2, &2, Cr.CrError, Ad.AdSplit>}
159	  %nat_lt_add(B.Octets.len(c), B.Octets.len(t)) : {Done{Ad.AdSplit{c, t}} == Ad.ad.split.pick(_, B.Octets.len(t), B.Octets.append(c, t)) : Result<&2, &2, Cr.CrError, Ad.AdSplit>}
160	  %olen_append(c, t) : {Done{Ad.AdSplit{c, t}} == Done{Ad.AdSplit{B.Octets.take(Nat.sub(_, B.Octets.len(t)), B.Octets.append(c, t)), B.Octets.drop(Nat.sub(_, B.Octets.len(t)), B.Octets.append(c, t))}} : Result<&2, &2, Cr.CrError, Ad.AdSplit>}
161	  %nat_sub_add(B.Octets.len(c), B.Octets.len(t)) : {Done{Ad.AdSplit{c, t}} == Done{Ad.AdSplit{B.Octets.take(_, B.Octets.append(c, t)), B.Octets.drop(_, B.Octets.append(c, t))}} : Result<&2, &2, Cr.CrError, Ad.AdSplit>}
162	  %Equal.sym(B.Octets, B.Octets.take(B.Octets.len(c), B.Octets.append(c, t)), c, BL.octets_take_append(c, t)) : {Done{Ad.AdSplit{c, t}} == Done{Ad.AdSplit{_, B.Octets.drop(B.Octets.len(c), B.Octets.append(c, t))}} : Result<&2, &2, Cr.CrError, Ad.AdSplit>}
163	  %Equal.sym(B.Octets, B.Octets.drop(B.Octets.len(c), B.Octets.append(c, t)), t, BL.octets_drop_append(c, t)) : {Done{Ad.AdSplit{c, t}} == Done{Ad.AdSplit{c, _}} : Result<&2, &2, Cr.CrError, Ad.AdSplit>}
164	  {==}
165	
166	def is_eq_refl(+o: B.Octets) -> {True{} == Ad.AdTag.is_eq(o, o) : Bool}:
167	  Equal.sym(Bool, B.Octets.is_eq(o, o), True{}, BL.octets_is_eq_refl(o))
168	
169	# AESRound: RFC 10032's vector
170	
171	def Laws.aesround_rfc10032():
172	  {==}
173	
174	# ESSIV: what it wraps, at the derived IV
175	
176	def Laws.essiv_round_trip_if(KD, KS, Blk, enc, blk_of, blk_to, cenc, cdec, kd, ks, iv, m, h):
177	  h
178	
179	def Laws.essiv_aead_round_trip_if(KD, KS, Blk, enc, blk_of, blk_to, seal, open, kd, ks, iv, aad, p, h):
180	  h
181	
182	# seqiv and echainiv: the IV, ivlen bytes long (hl), splits back off the
183	# front, and the wrapped AEAD opens what it sealed (h)
184	
185	def seqiv_r(~KA: Data, ~open: KA -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, ~ivlen: Nat, +ka: KA, +salt: B.Octets, +seq: B.Octets, +iv: B.Octets, +aad: B.Octets, +p: B.Octets, r: Result<&2, &2, Cr.CrError, B.Octets>, hl: {B.Octets.len(iv) == ivlen : Nat}, h: {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, r, c => open(ka, iv, B.Octets.append(aad, iv), c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, r) : Result<&2, &2, Cr.CrError, B.Octets>}) -> {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => B.Octets.append(iv, c), r), c => Sq.AdSeqiv.open(~KA, ~open, ~ivlen, Sq.AdSeqivKey{ka, salt}, seq, aad, c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => B.Octets.append(iv, c), r)) : Result<&2, &2, Cr.CrError, B.Octets>}:
186	  match r:
187	    case Fail{e}:
188	      {==}
189	    case Done{+c}:
190	      %hl : {Sq.ad.sq.open.go(~KA, ~open, Sq.AdSeqivKey{ka, salt}, aad, B.Octets.len(B.Octets.append(iv, c)), B.Octets.split_at(_, B.Octets.append(iv, c))) == Done{p} : Result<&2, &2, Cr.CrError, B.Octets>}
191	      %Equal.sym(Maybe<&2, B.OctetsSplit>, B.Octets.split_at(B.Octets.len(iv), B.Octets.append(iv, c)), Some{B.OctetsSplit{iv, c}}, BL.octets_split_at_append(iv, c)) : {Sq.ad.sq.open.go(~KA, ~open, Sq.AdSeqivKey{ka, salt}, aad, B.Octets.len(B.Octets.append(iv, c)), _) == Done{p} : Result<&2, &2, Cr.CrError, B.Octets>}
192	      h
193	
194	def Laws.seqiv_round_trip_if(KA, seal, open, ivlen, ka, salt, seq, aad, p, hl, h):
195	  seqiv_r(~KA, ~open, ~ivlen, ka, salt, seq, Sq.AdSeqiv.iv(~KA, Sq.AdSeqivKey{ka, salt}, seq), aad, p, seal(ka, Sq.AdSeqiv.iv(~KA, Sq.AdSeqivKey{ka, salt}, seq), B.Octets.append(aad, Sq.AdSeqiv.iv(~KA, Sq.AdSeqivKey{ka, salt}, seq)), p), hl, h)
196	
197	def echainiv_r(~KA: Data, ~KC: Data, ~open: KA -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, ~ivlen: Nat, +ka: KA, +kc: KC, +salt: B.Octets, +seq: B.Octets, +iv: B.Octets, +aad: B.Octets, +p: B.Octets, r: Result<&2, &2, Cr.CrError, B.Octets>, hl: {B.Octets.len(iv) == ivlen : Nat}, h: {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, r, c => open(ka, iv, B.Octets.append(aad, iv), c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, r) : Result<&2, &2, Cr.CrError, B.Octets>}) -> {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => B.Octets.append(iv, c), r), c => Ec.AdEchainiv.open(~KA, ~KC, ~open, ~ivlen, Ec.AdEchainivKey{ka, kc, salt}, seq, aad, c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => B.Octets.append(iv, c), r)) : Result<&2, &2, Cr.CrError, B.Octets>}:
198	  match r:
199	    case Fail{e}:
200	      {==}
201	    case Done{+c}:
202	      %hl : {Ec.ad.ec.open.go(~KA, ~KC, ~open, Ec.AdEchainivKey{ka, kc, salt}, aad, B.Octets.len(B.Octets.append(iv, c)), B.Octets.split_at(_, B.Octets.append(iv, c))) == Done{p} : Result<&2, &2, Cr.CrError, B.Octets>}
203	      %Equal.sym(Maybe<&2, B.OctetsSplit>, B.Octets.split_at(B.Octets.len(iv), B.Octets.append(iv, c)), Some{B.OctetsSplit{iv, c}}, BL.octets_split_at_append(iv, c)) : {Ec.ad.ec.open.go(~KA, ~KC, ~open, Ec.AdEchainivKey{ka, kc, salt}, aad, B.Octets.len(B.Octets.append(iv, c)), _) == Done{p} : Result<&2, &2, Cr.CrError, B.Octets>}
204	      h
205	
206	def Laws.echainiv_round_trip_if(KA, KC, Blk, enc, blk_of, blk_to, seal, open, ivlen, ka, kc, salt, seq, aad, p, hl, h):
207	  echainiv_r(~KA, ~KC, ~open, ~ivlen, ka, kc, salt, seq, Ec.AdEchainiv.iv(~KA, ~KC, ~Blk, ~enc, ~blk_of, ~blk_to, Ec.AdEchainivKey{ka, kc, salt}, seq), aad, p, seal(ka, Ec.AdEchainiv.iv(~KA, ~KC, ~Blk, ~enc, ~blk_of, ~blk_to, Ec.AdEchainivKey{ka, kc, salt}, seq), B.Octets.append(aad, Ec.AdEchainiv.iv(~KA, ~KC, ~Blk, ~enc, ~blk_of, ~blk_to, Ec.AdEchainivKey{ka, kc, salt}, seq)), p), hl, h)
208	
209	# Encrypt-then-MAC
210	
211	def fit_len(n: Nat, xs: List<&2, U32>) -> {B.len(Au.ad.au.fit(n, xs)) == n : Nat}:
212	  match n:
213	    case 0n:
214	      {==}
215	    case 1n+m:
216	      match xs:
217	        case Nil{}:
218	          %fit_len(m, Nil{}) : {1n+B.len(Au.ad.au.fit(m, Nil{})) == 1n+_ : Nat}
219	          {==}
220	        case Con{h, t}:
221	          %fit_len(m, t) : {1n+B.len(Au.ad.au.fit(m, t)) == 1n+_ : Nat}
222	          {==}
223	
224	# every tag has tlen bytes
225	def au_tag_len(~KE: Data, ~KM: Data, ~mac: KM -> B.Octets -> B.Octets, ~input: B.Octets -> B.Octets -> B.Octets -> B.Octets, ~tlen: Nat, k: Au.AdAuthencKey<KE, KM>, +aad: B.Octets, +iv: B.Octets, +c: B.Octets) -> {B.Octets.len(Au.AdAuthenc.tag(~KE, ~KM, ~mac, ~input, ~tlen, k, aad, iv, c)) == tlen : Nat}:
226	  match k:
227	    case Au.AdAuthencKey{ke, +km}:
228	      %olen_of(Au.ad.au.fit(tlen, B.Octets.to_list(mac(km, input(aad, iv, c))))) : {_ == tlen : Nat}
229	      fit_len(tlen, B.Octets.to_list(mac(km, input(aad, iv, c))))
230	
231	def authenc_r(~KE: Data, ~KM: Data, ~enc: KE -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, ~dec: KE -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, ~mac: KM -> B.Octets -> B.Octets, ~input: B.Octets -> B.Octets -> B.Octets -> B.Octets, ~tlen: Nat, +ke: KE, +km: KM, +iv: B.Octets, +aad: B.Octets, +p: B.Octets, r: Result<&2, &2, Cr.CrError, B.Octets>, h: {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, r, c => dec(ke, iv, c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, r) : Result<&2, &2, Cr.CrError, B.Octets>}) -> {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => Au.ad.au.sealed(~KE, ~KM, ~mac, ~input, ~tlen, Au.AdAuthencKey{ke, km}, aad, iv, c), r), c => Au.AdAuthenc.open(~KE, ~KM, ~dec, ~mac, ~input, ~tlen, Au.AdAuthencKey{ke, km}, iv, aad, c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => Au.ad.au.sealed(~KE, ~KM, ~mac, ~input, ~tlen, Au.AdAuthencKey{ke, km}, aad, iv, c), r)) : Result<&2, &2, Cr.CrError, B.Octets>}:
232	  match r:
233	    case Fail{e}:
234	      {==}
235	    case Done{+c}:
236	      %au_tag_len(~KE, ~KM, ~mac, ~input, ~tlen, Au.AdAuthencKey{ke, km}, aad, iv, c) : {Result.bind(&2, &2, Cr.CrError, Ad.AdSplit, B.Octets, Ad.AdTag.split(_, B.Octets.append(c, Au.AdAuthenc.tag(~KE, ~KM, ~mac, ~input, ~tlen, Au.AdAuthencKey{ke, km}, aad, iv, c))), s => Au.ad.au.open.go(~KE, ~KM, ~dec, ~mac, ~input, ~tlen, Au.AdAuthencKey{ke, km}, iv, aad, s)) == Done{p} : Result<&2, &2, Cr.CrError, B.Octets>}
237	      %split_join(c, Au.AdAuthenc.tag(~KE, ~KM, ~mac, ~input, ~tlen, Au.AdAuthencKey{ke, km}, aad, iv, c)) : {Result.bind(&2, &2, Cr.CrError, Ad.AdSplit, B.Octets, _, s => Au.ad.au.open.go(~KE, ~KM, ~dec, ~mac, ~input, ~tlen, Au.AdAuthencKey{ke, km}, iv, aad, s)) == Done{p} : Result<&2, &2, Cr.CrError, B.Octets>}
238	      %is_eq_refl(Au.AdAuthenc.tag(~KE, ~KM, ~mac, ~input, ~tlen, Au.AdAuthencKey{ke, km}, aad, iv, c)) : {Result.bind(&2, &2, Cr.CrError, Unit, B.Octets, Au.ad.au.check(_), u => dec(ke, iv, c)) == Done{p} : Result<&2, &2, Cr.CrError, B.Octets>}
239	      h
240	
241	def Laws.authenc_round_trip_if(KE, KM, enc, dec, mac, input, tlen, ke, km, iv, aad, p, h):
242	  authenc_r(~KE, ~KM, ~enc, ~dec, ~mac, ~input, ~tlen, ke, km, iv, aad, p, enc(ke, iv, p), h)
243	
244	def Laws.authenc_tamper(KE, KM, dec, mac, input, tlen, k, iv, aad, c, t, hl, ht):
245	  %hl : {Result.bind(&2, &2, Cr.CrError, Ad.AdSplit, B.Octets, Ad.AdTag.split(_, B.Octets.append(c, t)), s => Au.ad.au.open.go(~KE, ~KM, ~dec, ~mac, ~input, ~tlen, k, iv, aad, s)) == Fail{Cr.CrTagMismatch{}} : Result<&2, &2, Cr.CrError, B.Octets>}
246	  %split_join(c, t) : {Result.bind(&2, &2, Cr.CrError, Ad.AdSplit, B.Octets, _, s => Au.ad.au.open.go(~KE, ~KM, ~dec, ~mac, ~input, ~tlen, k, iv, aad, s)) == Fail{Cr.CrTagMismatch{}} : Result<&2, &2, Cr.CrError, B.Octets>}
247	  %Equal.sym(Bool, Ad.AdTag.is_eq(Au.AdAuthenc.tag(~KE, ~KM, ~mac, ~input, ~tlen, k, aad, iv, c), t), False{}, ht) : {Result.bind(&2, &2, Cr.CrError, Unit, B.Octets, Au.ad.au.check(_), u => dec(Au.ad.au.ke(~KE, ~KM, k), iv, c)) == Fail{Cr.CrTagMismatch{}} : Result<&2, &2, Cr.CrError, B.Octets>}
248	  {==}
249	
250	# AEGIS-128: the loops that run are the structural forms
251	
252	def ego_ref(xs: List<&2, U32>, +sb: R.AdSbox, +r: G.AdAegisRun, +acc: List<&2, U32>) -> {G.AdAegisOut{G.ad.ae.eafter(xs, sb, r), G.ad.ae.rev(acc, G.ad.ae.eout(xs, sb, r))} == G.ad.ae.ego(xs, sb, r, acc) : G.AdAegisOut}:
253	  match xs:
254	    case Nil{}:
255	      {==}
256	    case Con{+x, t}:
257	      ego_ref(t, sb, G.ad.ae.step(sb, r, B.byte(x)), Con{B.byte(U32.xor(x, G.ad.ae.zhead(r))), acc})
258	
259	def dgo_ref(ys: List<&2, U32>, +sb: R.AdSbox, +r: G.AdAegisRun, +acc: List<&2, U32>) -> {G.AdAegisOut{G.ad.ae.dafter(ys, sb, r), G.ad.ae.rev(acc, G.ad.ae.dout(ys, sb, r))} == G.ad.ae.dgo(ys, sb, r, acc) : G.AdAegisOut}:
260	  match ys:
261	    case Nil{}:
262	      {==}
263	    case Con{+y, t}:
264	      dgo_ref(t, sb, G.ad.ae.step(sb, r, B.byte(U32.xor(y, G.ad.ae.zhead(r)))), Con{B.byte(U32.xor(y, G.ad.ae.zhead(r))), acc})
265	
266	# decryption runs through the states encryption ran through, and gives the
267	# message's bytes back
268	def dec_enc_after(xs: List<&2, U32>, +sb: R.AdSbox, +r: G.AdAegisRun) -> {G.ad.ae.eafter(xs, sb, r) == G.ad.ae.dafter(G.ad.ae.eout(xs, sb, r), sb, r) : G.AdAegisRun}:
269	  match xs:
270	    case Nil{}:
271	      {==}
272	    case Con{+x, t}:
273	      %byte_xx(x, G.ad.ae.zhead(r)) : {G.ad.ae.eafter(t, sb, G.ad.ae.step(sb, r, B.byte(x))) == G.ad.ae.dafter(G.ad.ae.eout(t, sb, G.ad.ae.step(sb, r, B.byte(x))), sb, G.ad.ae.step(sb, r, _)) : G.AdAegisRun}
274	      dec_enc_after(t, sb, G.ad.ae.step(sb, r, B.byte(x)))
275	
276	def dec_enc_out(xs: List<&2, U32>, +sb: R.AdSbox, +r: G.AdAegisRun) -> {B.mask(xs) == G.ad.ae.dout(G.ad.ae.eout(xs, sb, r), sb, r) : List<&2, U32>}:
277	  match xs:
278	    case Nil{}:
279	      {==}
280	    case Con{+x, t}:
281	      %byte_xx(x, G.ad.ae.zhead(r)) : {Con{B.byte(x), B.mask(t)} == Con{_, G.ad.ae.dout(G.ad.ae.eout(t, sb, G.ad.ae.step(sb, r, B.byte(x))), sb, G.ad.ae.step(sb, r, _))} : List<&2, U32>}
282	      %dec_enc_out(t, sb, G.ad.ae.step(sb, r, B.byte(x))) : {Con{B.byte(x), B.mask(t)} == Con{B.byte(x), _} : List<&2, U32>}
283	      {==}
284	
285	# the ciphertext's bytes are bytes, and as many as the message's
286	def mask_eout(xs: List<&2, U32>, +sb: R.AdSbox, +r: G.AdAegisRun) -> {G.ad.ae.eout(xs, sb, r) == B.mask(G.ad.ae.eout(xs, sb, r)) : List<&2, U32>}:
287	  match xs:
288	    case Nil{}:
289	      {==}
290	    case Con{+x, t}:
291	      %byte_byte(U32.xor(x, G.ad.ae.zhead(r))) : {Con{B.byte(U32.xor(x, G.ad.ae.zhead(r))), G.ad.ae.eout(t, sb, G.ad.ae.step(sb, r, B.byte(x)))} == Con{_, B.mask(G.ad.ae.eout(t, sb, G.ad.ae.step(sb, r, B.byte(x))))} : List<&2, U32>}
292	      %mask_eout(t, sb, G.ad.ae.step(sb, r, B.byte(x))) : {Con{B.byte(U32.xor(x, G.ad.ae.zhead(r))), G.ad.ae.eout(t, sb, G.ad.ae.step(sb, r, B.byte(x)))} == Con{B.byte(U32.xor(x, G.ad.ae.zhead(r))), _} : List<&2, U32>}
293	      {==}
294	
295	def len_eout(xs: List<&2, U32>, +sb: R.AdSbox, +r: G.AdAegisRun) -> {B.len(xs) == B.len(G.ad.ae.eout(xs, sb, r)) : Nat}:
296	  match xs:
297	    case Nil{}:
298	      {==}
299	    case Con{+x, t}:
300	      %len_eout(t, sb, G.ad.ae.step(sb, r, B.byte(x))) : {1n+B.len(t) == 1n+_ : Nat}
301	      {==}
302	
303	# every tag has 16 bytes
304	def blk_len(b: R.AdBlk) -> {16n == B.Octets.len(R.AdBlk.to_octets(b)) : Nat}:
305	  match b:
306	    case R.AdBlk{+w0, +w1, +w2, +w3}:
307	      %olen_of(R.AdBlk.to_list(R.AdBlk{w0, w1, w2, w3})) : {16n == _ : Nat}
308	      %len_append(B.be32(w0), B.append(B.be32(w1), B.append(B.be32(w2), B.be32(w3)))) : {16n == _ : Nat}
309	      %len_append(B.be32(w1), B.append(B.be32(w2), B.be32(w3))) : {16n == Nat.add(B.len(B.be32(w0)), _) : Nat}
310	      %len_append(B.be32(w2), B.be32(w3)) : {16n == Nat.add(B.len(B.be32(w0)), Nat.add(B.len(B.be32(w1)), _)) : Nat}
311	      %be32_len(w0) : {16n == Nat.add(_, Nat.add(B.len(B.be32(w1)), Nat.add(B.len(B.be32(w2)), B.len(B.be32(w3))))) : Nat}
312	      %be32_len(w1) : {16n == Nat.add(4n, Nat.add(_, Nat.add(B.len(B.be32(w2)), B.len(B.be32(w3))))) : Nat}
313	      %be32_len(w2) : {16n == Nat.add(4n, Nat.add(4n, Nat.add(_, B.len(B.be32(w3))))) : Nat}
314	      %be32_len(w3) : {16n == Nat.add(4n, Nat.add(4n, Nat.add(4n, _))) : Nat}
315	      {==}
316	
317	def tag_len(st: G.AdAegisSt) -> {16n == B.Octets.len(G.ad.ae.tag(st)) : Nat}:
318	  match st:
319	    case G.AdAegisSt{a0, a1, a2, a3, a4}:
320	      blk_len(R.AdBlk.xor(R.AdBlk.xor(R.AdBlk.xor(a0, a1), R.AdBlk.xor(a2, a3)), a4))
321	
322	def fin_len(+sb: R.AdSbox, +st: G.AdAegisSt, +al: Nat, +ml: Nat) -> {16n == B.Octets.len(G.ad.ae.final(sb, st, al, ml)) : Nat}:
323	  tag_len(G.ad.ae.fin.go(7n, sb, R.AdBlk.xor(G.ad.ae.s3(st), R.AdBlk.of_list(B.append(G.ad.ae.bits(al), G.ad.ae.bits(ml)))), st))
324	
325	# seal and open under a nonce of 16 bytes or another length
326	
327	def seal_ok(+kk: G.AdAegisKey, +n: B.Octets, +a: B.Octets, +p: B.Octets, e: {Nat.is_eq(B.Octets.len(n), 16n) == True{} : Bool}) -> {Done{G.ad.ae.seal.go(kk, n, a, p)} == G.AdAegis128.seal(kk, n, a, p) : Result<&2, &2, Cr.CrError, B.Octets>}:
328	  %Equal.sym(Bool, Nat.is_eq(B.Octets.len(n), 16n), True{}, e) : {Done{G.ad.ae.seal.go(kk, n, a, p)} == Result.map(&2, &2, Cr.CrError, Unit, B.Octets, u => G.ad.ae.seal.go(kk, n, a, p), Cr.CrError.check(_, Cr.CrBadNonceLength{B.Octets.len(n)})) : Result<&2, &2, Cr.CrError, B.Octets>}
329	  {==}
330	
331	def seal_bad(+kk: G.AdAegisKey, +n: B.Octets, +a: B.Octets, +p: B.Octets, e: {Nat.is_eq(B.Octets.len(n), 16n) == False{} : Bool}) -> {Fail{Cr.CrBadNonceLength{B.Octets.len(n)}} == G.AdAegis128.seal(kk, n, a, p) : Result<&2, &2, Cr.CrError, B.Octets>}:
332	  %Equal.sym(Bool, Nat.is_eq(B.Octets.len(n), 16n), False{}, e) : {Fail{Cr.CrBadNonceLength{B.Octets.len(n)}} == Result.map(&2, &2, Cr.CrError, Unit, B.Octets, u => G.ad.ae.seal.go(kk, n, a, p), Cr.CrError.check(_, Cr.CrBadNonceLength{B.Octets.len(n)})) : Result<&2, &2, Cr.CrError, B.Octets>}
333	  {==}
334	
335	def open_ok(+kk: G.AdAegisKey, +n: B.Octets, +a: B.Octets, +c: B.Octets, e: {Nat.is_eq(B.Octets.len(n), 16n) == True{} : Bool}) -> {Result.bind(&2, &2, Cr.CrError, Ad.AdSplit, B.Octets, Ad.AdTag.split(16n, c), s => G.ad.ae.open.go(kk, n, a, s)) == G.AdAegis128.open(kk, n, a, c) : Result<&2, &2, Cr.CrError, B.Octets>}:
336	  %Equal.sym(Bool, Nat.is_eq(B.Octets.len(n), 16n), True{}, e) : {Result.bind(&2, &2, Cr.CrError, Ad.AdSplit, B.Octets, Ad.AdTag.split(16n, c), s => G.ad.ae.open.go(kk, n, a, s)) == Result.bind(&2, &2, Cr.CrError, Unit, B.Octets, Cr.CrError.check(_, Cr.CrBadNonceLength{B.Octets.len(n)}), u => Result.bind(&2, &2, Cr.CrError, Ad.AdSplit, B.Octets, Ad.AdTag.split(16n, c), s => G.ad.ae.open.go(kk, n, a, s))) : Result<&2, &2, Cr.CrError, B.Octets>}
337	  {==}
338	
339	def nonce_ok(+n: B.Octets, hn: {B.Octets.len(n) == 16n : Nat}) -> {Nat.is_eq(B.Octets.len(n), 16n) == True{} : Bool}:
340	  %Equal.sym(Nat, B.Octets.len(n), 16n, hn) : {Nat.is_eq(_, 16n) == True{} : Bool}
341	  {==}
342	
343	# what seal produces, what open expects of it, and what open gives back
344	
345	def seal_go_eq(+k: R.AdBlk, +sb: R.AdSbox, +n: B.Octets, +a: B.Octets, +p: B.Octets) -> {B.Octets.append(B.Octets.of_list(G.ad.ae.eout(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), G.ad.ae.final(sb, G.ad.ae.flush(sb, G.ad.ae.eafter(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), B.Octets.len(a), B.Octets.len(p))) == G.ad.ae.seal.go(G.AdAegisKey{k, sb}, n, a, p) : B.Octets}:
346	  %ego_ref(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a), Nil{}) : {B.Octets.append(B.Octets.of_list(G.ad.ae.eout(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), G.ad.ae.final(sb, G.ad.ae.flush(sb, G.ad.ae.eafter(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), B.Octets.len(a), B.Octets.len(p))) == G.ad.ae.sealed(sb, a, p, _) : B.Octets}
347	  {==}
348	
349	def tag_of_eq(+k: R.AdBlk, +sb: R.AdSbox, +n: B.Octets, +a: B.Octets, +p: B.Octets) -> {G.ad.ae.final(sb, G.ad.ae.flush(sb, G.ad.ae.eafter(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), B.Octets.len(a), B.Octets.len(p)) == G.AdAegis128.tag_of(G.AdAegisKey{k, sb}, n, a, B.Octets.of_list(G.ad.ae.eout(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a)))) : B.Octets}:
350	  %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.of_list(G.ad.ae.eout(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a)))), B.mask(G.ad.ae.eout(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), BL.octets_to_of(G.ad.ae.eout(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a)))) : {G.ad.ae.final(sb, G.ad.ae.flush(sb, G.ad.ae.eafter(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), B.Octets.len(a), B.Octets.len(p)) == G.ad.ae.tag_of.of(sb, a, B.Octets.of_list(G.ad.ae.eout(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), G.ad.ae.dgo(_, sb, G.ad.ae.start(sb, k, n, a), Nil{})) : B.Octets}
351	  %mask_eout(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a)) : {G.ad.ae.final(sb, G.ad.ae.flush(sb, G.ad.ae.eafter(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), B.Octets.len(a), B.Octets.len(p)) == G.ad.ae.tag_of.of(sb, a, B.Octets.of_list(G.ad.ae.eout(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), G.ad.ae.dgo(_, sb, G.ad.ae.start(sb, k, n, a), Nil{})) : B.Octets}
352	  %dgo_ref(G.ad.ae.eout(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a)), sb, G.ad.ae.start(sb, k, n, a), Nil{}) : {G.ad.ae.final(sb, G.ad.ae.flush(sb, G.ad.ae.eafter(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), B.Octets.len(a), B.Octets.len(p)) == G.ad.ae.tag_of.of(sb, a, B.Octets.of_list(G.ad.ae.eout(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), _) : B.Octets}
353	  %dec_enc_after(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a)) : {G.ad.ae.final(sb, G.ad.ae.flush(sb, G.ad.ae.eafter(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), B.Octets.len(a), B.Octets.len(p)) == G.ad.ae.final(sb, G.ad.ae.flush(sb, _), B.Octets.len(a), B.Octets.len(B.Octets.of_list(G.ad.ae.eout(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))))) : B.Octets}
354	  %olen_of(G.ad.ae.eout(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))) : {G.ad.ae.final(sb, G.ad.ae.flush(sb, G.ad.ae.eafter(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), B.Octets.len(a), B.Octets.len(p)) == G.ad.ae.final(sb, G.ad.ae.flush(sb, G.ad.ae.eafter(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), B.Octets.len(a), _) : B.Octets}
355	  %len_eout(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a)) : {G.ad.ae.final(sb, G.ad.ae.flush(sb, G.ad.ae.eafter(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), B.Octets.len(a), B.Octets.len(p)) == G.ad.ae.final(sb, G.ad.ae.flush(sb, G.ad.ae.eafter(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), B.Octets.len(a), _) : B.Octets}
356	  %BL.octets_len_list(p) : {G.ad.ae.final(sb, G.ad.ae.flush(sb, G.ad.ae.eafter(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), B.Octets.len(a), B.Octets.len(p)) == G.ad.ae.final(sb, G.ad.ae.flush(sb, G.ad.ae.eafter(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), B.Octets.len(a), _) : B.Octets}
357	  {==}
358	
359	def plain_eq(+k: R.AdBlk, +sb: R.AdSbox, +n: B.Octets, +a: B.Octets, +p: B.Octets) -> {p == G.ad.ae.plain(G.AdAegisKey{k, sb}, n, a, B.Octets.of_list(G.ad.ae.eout(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a)))) : B.Octets}:
360	  %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.of_list(G.ad.ae.eout(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a)))), B.mask(G.ad.ae.eout(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), BL.octets_to_of(G.ad.ae.eout(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a)))) : {p == G.ad.ae.plain.of(G.ad.ae.dgo(_, sb, G.ad.ae.start(sb, k, n, a), Nil{})) : B.Octets}
361	  %mask_eout(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a)) : {p == G.ad.ae.plain.of(G.ad.ae.dgo(_, sb, G.ad.ae.start(sb, k, n, a), Nil{})) : B.Octets}
362	  %dgo_ref(G.ad.ae.eout(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a)), sb, G.ad.ae.start(sb, k, n, a), Nil{}) : {p == G.ad.ae.plain.of(_) : B.Octets}
363	  %dec_enc_out(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a)) : {p == B.Octets.of_list(_) : B.Octets}
364	  %BL.octets_to_of(B.Octets.to_list(p)) : {p == B.Octets.of_list(_) : B.Octets}
365	  %Equal.sym(B.Octets, B.Octets.of_list(B.Octets.to_list(B.Octets.of_list(B.Octets.to_list(p)))), B.Octets.of_list(B.Octets.to_list(p)), BL.octets_of_to(B.Octets.of_list(B.Octets.to_list(p)))) : {p == _ : B.Octets}
366	  Equal.sym(B.Octets, B.Octets.of_list(B.Octets.to_list(p)), p, BL.octets_of_to(p))
367	
368	def aegis_rt(b: Bool, +kk: G.AdAegisKey, +n: B.Octets, +a: B.Octets, +p: B.Octets, e: {Nat.is_eq(B.Octets.len(n), 16n) == b : Bool}, e2: {Nat.is_eq(B.Octets.len(n), 16n) == b : Bool}) -> {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, G.AdAegis128.seal(kk, n, a, p), c => G.AdAegis128.open(kk, n, a, c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, G.AdAegis128.seal(kk, n, a, p)) : Result<&2, &2, Cr.CrError, B.Octets>}:
369	  match b:
370	    case True{}:
371	      match kk:
372	        case G.AdAegisKey{+k, +sb}:
373	          %seal_ok(G.AdAegisKey{k, sb}, n, a, p, e) : {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, _, c => G.AdAegis128.open(G.AdAegisKey{k, sb}, n, a, c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, _) : Result<&2, &2, Cr.CrError, B.Octets>}
374	          %open_ok(G.AdAegisKey{k, sb}, n, a, G.ad.ae.seal.go(G.AdAegisKey{k, sb}, n, a, p), e2) : {_ == Done{p} : Result<&2, &2, Cr.CrError, B.Octets>}
375	          %seal_go_eq(k, sb, n, a, p) : {Result.bind(&2, &2, Cr.CrError, Ad.AdSplit, B.Octets, Ad.AdTag.split(16n, _), s => G.ad.ae.open.go(G.AdAegisKey{k, sb}, n, a, s)) == Done{p} : Result<&2, &2, Cr.CrError, B.Octets>}
376	          %Equal.sym(Nat, 16n, B.Octets.len(G.ad.ae.final(sb, G.ad.ae.flush(sb, G.ad.ae.eafter(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), B.Octets.len(a), B.Octets.len(p))), fin_len(sb, G.ad.ae.flush(sb, G.ad.ae.eafter(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), B.Octets.len(a), B.Octets.len(p))) : {Result.bind(&2, &2, Cr.CrError, Ad.AdSplit, B.Octets, Ad.AdTag.split(_, B.Octets.append(B.Octets.of_list(G.ad.ae.eout(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), G.ad.ae.final(sb, G.ad.ae.flush(sb, G.ad.ae.eafter(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), B.Octets.len(a), B.Octets.len(p)))), s => G.ad.ae.open.go(G.AdAegisKey{k, sb}, n, a, s)) == Done{p} : Result<&2, &2, Cr.CrError, B.Octets>}
377	          %split_join(B.Octets.of_list(G.ad.ae.eout(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), G.ad.ae.final(sb, G.ad.ae.flush(sb, G.ad.ae.eafter(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), B.Octets.len(a), B.Octets.len(p))) : {Result.bind(&2, &2, Cr.CrError, Ad.AdSplit, B.Octets, _, s => G.ad.ae.open.go(G.AdAegisKey{k, sb}, n, a, s)) == Done{p} : Result<&2, &2, Cr.CrError, B.Octets>}
378	          %tag_of_eq(k, sb, n, a, p) : {G.ad.ae.check(Ad.AdTag.is_eq(_, G.ad.ae.final(sb, G.ad.ae.flush(sb, G.ad.ae.eafter(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), B.Octets.len(a), B.Octets.len(p))), G.ad.ae.plain(G.AdAegisKey{k, sb}, n, a, B.Octets.of_list(G.ad.ae.eout(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))))) == Done{p} : Result<&2, &2, Cr.CrError, B.Octets>}
379	          %is_eq_refl(G.ad.ae.final(sb, G.ad.ae.flush(sb, G.ad.ae.eafter(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), B.Octets.len(a), B.Octets.len(p))) : {G.ad.ae.check(_, G.ad.ae.plain(G.AdAegisKey{k, sb}, n, a, B.Octets.of_list(G.ad.ae.eout(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))))) == Done{p} : Result<&2, &2, Cr.CrError, B.Octets>}
380	          %plain_eq(k, sb, n, a, p) : {G.ad.ae.check(True{}, _) == Done{p} : Result<&2, &2, Cr.CrError, B.Octets>}
381	          {==}
382	    case False{}:
383	      %seal_bad(kk, n, a, p, e) : {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, _, c => G.AdAegis128.open(kk, n, a, c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, _) : Result<&2, &2, Cr.CrError, B.Octets>}
384	      {==}
385	
386	def Laws.aegis128_round_trip(k, n, a, p):
387	  aegis_rt(Nat.is_eq(B.Octets.len(n), 16n), k, n, a, p, {==}, {==})
388	
389	def Laws.aegis128_tamper(k, n, a, c, t, hn, hl, ht):
390	  %open_ok(k, n, a, B.Octets.append(c, t), nonce_ok(n, hn)) : {_ == Fail{Cr.CrTagMismatch{}} : Result<&2, &2, Cr.CrError, B.Octets>}
391	  %hl : {Result.bind(&2, &2, Cr.CrError, Ad.AdSplit, B.Octets, Ad.AdTag.split(_, B.Octets.append(c, t)), s => G.ad.ae.open.go(k, n, a, s)) == Fail{Cr.CrTagMismatch{}} : Result<&2, &2, Cr.CrError, B.Octets>}
392	  %split_join(c, t) : {Result.bind(&2, &2, Cr.CrError, Ad.AdSplit, B.Octets, _, s => G.ad.ae.open.go(k, n, a, s)) == Fail{Cr.CrTagMismatch{}} : Result<&2, &2, Cr.CrError, B.Octets>}
393	  %Equal.sym(Bool, Ad.AdTag.is_eq(G.AdAegis128.tag_of(k, n, a, c), t), False{}, ht) : {G.ad.ae.check(_, G.ad.ae.plain(k, n, a, c)) == Fail{Cr.CrTagMismatch{}} : Result<&2, &2, Cr.CrError, B.Octets>}
394	  {==}