PROOF.bend

bend-osdev-aead@0.1.0.0 · 394 lines · 41 definitions

1import Base
2import bend-osdev-bytes@0.1.0.0/bytes.bend as B
3import bend-osdev-bytes@0.1.0.0/LAWS.bend as BL
4import bend-osdev-bytes@0.1.0.0/PROOF.bend as BP
5import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
6import bend-osdev-aead@0.1.0.0/aead.bend as Ad
7import bend-osdev-aead@0.1.0.0/aesround.bend as R
8import bend-osdev-aead@0.1.0.0/aegis128.bend as G
9import bend-osdev-aead@0.1.0.0/authenc.bend as Au
10import bend-osdev-aead@0.1.0.0/essiv.bend as Es
11import bend-osdev-aead@0.1.0.0/seqiv.bend as Sq
12import bend-osdev-aead@0.1.0.0/echainiv.bend as Ec
13import bend-osdev-aead@0.1.0.0/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
17def 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
23def 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
29def 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
38def 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
49def 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
62def 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
68def 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
75def 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
83def 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
91def nat_sub_zero(x: Nat) -> {x == Nat.sub(x, 0n) : Nat}:
92  match x:
93    case 0n:
94      {==}
95    case 1n+p:
96      {==}
97
98def 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
107def 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
114def 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
125def 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
133def 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
142def 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
148def 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
157def 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
166def 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
171def Laws.aesround_rfc10032():
172  {==}
173
174# ESSIV: what it wraps, at the derived IV
175
176def Laws.essiv_round_trip_if(KD, KS, Blk, enc, blk_of, blk_to, cenc, cdec, kd, ks, iv, m, h):
177  h
178
179def 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
185def 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
194def 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
197def 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
206def 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
211def 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
225def 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
231def 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
241def 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
244def 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
252def 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
259def 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
268def 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
276def 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
286def 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
295def 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
304def 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
317def 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
322def 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
327def 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
331def 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
335def 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
339def 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
345def 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
349def 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
359def 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
368def 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
386def Laws.aegis128_round_trip(k, n, a, p):
387  aegis_rt(Nat.is_eq(B.Octets.len(n), 16n), k, n, a, p, {==}, {==})
388
389def 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  {==}