proofs/crypto/poly1305/final.bend
bend-collections-laws-crypto@1.0.0.0 · 573 lines · 48 definitions
1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/poly1305.bend as R
4import bend-collections-laws-crypto@1.0.0.0/src/crypto/poly1305/limbs.bend as Li
5import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
6import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend as AR
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U3
9import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend as UA
10import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
11import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
12import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64mul.bend as WM
13import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64sh.bend as SH
14import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/shrn.bend as SHN
15import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/f64bits.bend as FB
16import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
17import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/arith.bend as A
18import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/value.bend as V
19import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/step.bend as ST
20
21
22
23
24
25
26def wones(n: Nat) -> Word(n):
27 match n:
28 case 0n: WNil{}
29 case 1n+p: WCon{True{}, wones(p)}
30
31law wand0:
32 for +n: Nat
33 for +w: Word(n)
34 {Word.and(n, Word.zero(n), w) == Word.zero(n) : Word(n)}
35
36def wand0(n, w):
37 match n:
38 case 0n:
39 match w:
40 case WNil{}: {==}
41 case 1n+p:
42 match w:
43 case WCon{b, t}: Equal.cong(Word(p), Word(1n+p), x => WCon{False{}, x}, Word.and(p, Word.zero(p), t), Word.zero(p), wand0(p, t))
44
45law wand1:
46 for +n: Nat
47 for +w: Word(n)
48 {Word.and(n, wones(n), w) == w : Word(n)}
49
50def wand1(n, w):
51 match n:
52 case 0n:
53 match w:
54 case WNil{}: {==}
55 case 1n+p:
56 match w:
57 case WCon{b, t}: Equal.cong(Word(p), Word(1n+p), x => WCon{b, x}, Word.and(p, wones(p), t), t, wand1(p, t))
58
59law wxor0:
60 for +n: Nat
61 for +w: Word(n)
62 {Word.xor(n, w, Word.zero(n)) == w : Word(n)}
63
64def wxor0(n, w):
65 match n:
66 case 0n:
67 match w:
68 case WNil{}: {==}
69 case 1n+p:
70 match w:
71 case WCon{b, t}:
72 match b:
73 case False{}: Equal.cong(Word(p), Word(1n+p), x => WCon{False{}, x}, Word.xor(p, t, Word.zero(p)), t, wxor0(p, t))
74 case True{}: Equal.cong(Word(p), Word(1n+p), x => WCon{True{}, x}, Word.xor(p, t, Word.zero(p)), t, wxor0(p, t))
75
76law wxor2:
77 for +n: Nat
78 for +x: Word(n)
79 for +y: Word(n)
80 {Word.xor(n, x, Word.xor(n, x, y)) == y : Word(n)}
81
82def wxor2(n, x, y):
83 match n:
84 case 0n:
85 match x y:
86 case WNil{} WNil{}: {==}
87 case 1n+p:
88 match x y:
89 case WCon{False{}, s} WCon{False{}, t}: Equal.cong(Word(p), Word(1n+p), z => WCon{False{}, z}, Word.xor(p, s, Word.xor(p, s, t)), t, wxor2(p, s, t))
90 case WCon{False{}, s} WCon{True{}, t}: Equal.cong(Word(p), Word(1n+p), z => WCon{True{}, z}, Word.xor(p, s, Word.xor(p, s, t)), t, wxor2(p, s, t))
91 case WCon{True{}, s} WCon{False{}, t}: Equal.cong(Word(p), Word(1n+p), z => WCon{False{}, z}, Word.xor(p, s, Word.xor(p, s, t)), t, wxor2(p, s, t))
92 case WCon{True{}, s} WCon{True{}, t}: Equal.cong(Word(p), Word(1n+p), z => WCon{True{}, z}, Word.xor(p, s, Word.xor(p, s, t)), t, wxor2(p, s, t))
93
94def pick0(+x: U32, +y: U32) -> {Li.pick(0, x, y) == x : U32}:
95 match x y:
96 case U32{a} U32{b}:
97 Equal.trans(U32, U32{Word.xor(32n, a, Word.and(32n, Word.zero(32n), Word.xor(32n, a, b)))}, U32{Word.xor(32n, a, Word.zero(32n))}, U32{a},
98 Equal.cong(Word(32n), U32, w => U32{Word.xor(32n, a, w)}, Word.and(32n, Word.zero(32n), Word.xor(32n, a, b)), Word.zero(32n), wand0(32n, Word.xor(32n, a, b))),
99 Equal.cong(Word(32n), U32, w => U32{w}, Word.xor(32n, a, Word.zero(32n)), a, wxor0(32n, a)))
100
101def pick1(+x: U32, +y: U32) -> {Li.pick(4294967295, x, y) == y : U32}:
102 match x y:
103 case U32{a} U32{b}:
104 Equal.trans(U32, U32{Word.xor(32n, a, Word.and(32n, wones(32n), Word.xor(32n, a, b)))}, U32{Word.xor(32n, a, Word.xor(32n, a, b))}, U32{b},
105 Equal.cong(Word(32n), U32, w => U32{Word.xor(32n, a, w)}, Word.and(32n, wones(32n), Word.xor(32n, a, b)), Word.xor(32n, a, b), wand1(32n, Word.xor(32n, a, b))),
106 Equal.cong(Word(32n), U32, w => U32{w}, Word.xor(32n, a, Word.xor(32n, a, b)), b, wxor2(32n, a, b)))
107
108law sel0:
109 for +a: List<&2, U32>
110 for +b: List<&2, U32>
111 for +h: {V.len(a) == V.len(b) : Nat}
112 {Li.select(0, a, b) == a : List<&2, U32>}
113
114def sel0(a, b, h):
115 match a b:
116 case Nil{} Nil{}: {==}
117 case Nil{} y <> bt: Empty.absurd({Li.select(0, [], y <> bt) == [] : List<&2, U32>}, N.zero_succ(V.len(bt), h))
118 case x <> at Nil{}: Empty.absurd({Li.select(0, x <> at, []) == x <> at : List<&2, U32>}, N.succ_zero(V.len(at), h))
119 case x <> at y <> bt:
120 Equal.trans(List<&2, U32>, Li.pick(0, x, y) <> Li.select(0, at, bt), x <> Li.select(0, at, bt), x <> at,
121 Equal.cong(U32, List<&2, U32>, z => z <> Li.select(0, at, bt), Li.pick(0, x, y), x, pick0(x, y)),
122 Equal.cong(List<&2, U32>, List<&2, U32>, z => x <> z, Li.select(0, at, bt), at, sel0(at, bt, N.succ_inj(V.len(at), V.len(bt), h))))
123
124law sel1:
125 for +a: List<&2, U32>
126 for +b: List<&2, U32>
127 for +h: {V.len(a) == V.len(b) : Nat}
128 {Li.select(4294967295, a, b) == b : List<&2, U32>}
129
130def sel1(a, b, h):
131 match a b:
132 case Nil{} Nil{}: {==}
133 case Nil{} y <> bt: Empty.absurd({Li.select(4294967295, [], y <> bt) == y <> bt : List<&2, U32>}, N.zero_succ(V.len(bt), h))
134 case x <> at Nil{}: Empty.absurd({Li.select(4294967295, x <> at, []) == [] : List<&2, U32>}, N.succ_zero(V.len(at), h))
135 case x <> at y <> bt:
136 Equal.trans(List<&2, U32>, Li.pick(4294967295, x, y) <> Li.select(4294967295, at, bt), y <> Li.select(4294967295, at, bt), y <> bt,
137 Equal.cong(U32, List<&2, U32>, z => z <> Li.select(4294967295, at, bt), Li.pick(4294967295, x, y), y, pick1(x, y)),
138 Equal.cong(List<&2, U32>, List<&2, U32>, z => y <> z, Li.select(4294967295, at, bt), bt, sel1(at, bt, N.succ_inj(V.len(at), V.len(bt), h))))
139
140law len_take_eq:
141 for +n: Nat
142 for +xs: List<&2, U32>
143 for +h: {Nat.is_le(n, V.len(xs)) == True{} : Bool}
144 {V.len(Li.take(n, xs)) == n : Nat}
145
146def len_take_eq(n, xs, h):
147 match n xs:
148 case 0n _: {==}
149 case 1n+k Nil{}: Empty.absurd({V.len(Li.take(1n+k, [])) == 1n+k : Nat}, L.false_true(h))
150 case 1n+k x <> t: Equal.cong(Nat, Nat, z => 1n+z, V.len(Li.take(k, t)), k, len_take_eq(k, t, h))
151
152
153
154
155def lt_dbl(+x: Nat, +h: {Nat.is_le(1n, x) == True{} : Bool}) -> {Nat.is_lt(x, Nat.double(x)) == True{} : Bool}:
156 A.lt_subst(x, Nat.add(x, x), Nat.double(x), A.sy(Nat.double(x), Nat.add(x, x), NA.double_self(x)),
157 A.lt_substl(Nat.add(x, 0n), x, Nat.add(x, x), N.add_zero(x), N.lt_add_left(0n, x, x, N.succ_le_lt(0n, x, h))))
158
159
160def hval(+h: List<&2, U32>) -> Nat:
161 V.ev(h)
162
163def gg(+h: List<&2, U32>) -> List<&2, U32>:
164 Li.carry(16n, Li.add(h, [5]), 0)
165
166def qq(+h: List<&2, U32>) -> Nat:
167 C.high(130n, Nat.add(V.ev(h), 5n))
168
169law g_ev:
170 for +one: Nat
171 for +h1: {one == 1n : Nat}
172 for +h: List<&2, U32>
173 for +hh: {ST.inv(h) == True{} : Bool}
174 {V.ev(gg(h)) == Nat.add(V.ev(h), 5n) : Nat}
175
176def g_ev(one, h1, h, hh):
177 +s8 = C.shift(8n, one)
178 +hl = N.eq_from_is_eq(V.len(h), 17n, L.and_left(Nat.is_eq(V.len(h), 17n), Bool.and(V.fit_all(h, 8n), Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n)), hh))
179 +hr2 = L.and_right(Nat.is_eq(V.len(h), 17n), Bool.and(V.fit_all(h, 8n), Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n)), hh)
180 +hf = L.and_left(V.fit_all(h, 8n), Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n), hr2)
181 +a = Li.add(h, [5])
182 +h5 = V.cons_le(5, [], s8, L.subst(Nat, z => {Nat.is_le(5n, C.shift(8n, z)) == True{} : Bool}, 1n, one, A.sy(one, 1n, h1), {==}), {==})
183 +hf1 = ST.s8fit(one, h1)
184 +ea = V.add_ev(h, [5], s8, s8, V.fit_le(h, 8n, one, h1, hf), h5, hf1)
185 +s9 = C.shift(9n, one)
186 +l10 = A.lt_substl(s9, Nat.add(s8, s8), Nat.double(s9), NA.double_self(s8), lt_dbl(s9, A.one_le_shift(9n, one, h1)))
187 +ha = V.le_fit(a, Nat.add(s8, s8), 10n, one, h1, l10, V.add_le(h, [5], s8, s8, V.fit_le(h, 8n, one, h1, hf), h5, hf1))
188 +hal = V.len_add(h, [5], 17n, N.eq_le(V.len(h), 17n, hl), {==})
189 +ce = V.carry_ev(16n, a, 0, 2n, {==}, ha, {==})
190 +sk = V.skip_long(17n, a, hal)
191 A.tr(V.ev(gg(h)), Nat.add(V.ev(gg(h)), V.pos(17n, V.ev(Li.skip(17n, a)))), Nat.add(V.ev(h), 5n),
192 A.tr(V.ev(gg(h)), Nat.add(V.ev(gg(h)), 0n), Nat.add(V.ev(gg(h)), V.pos(17n, V.ev(Li.skip(17n, a)))), A.sy(Nat.add(V.ev(gg(h)), 0n), V.ev(gg(h)), N.add_zero(V.ev(gg(h)))),
193 Equal.cong(List<&2, U32>, Nat, l => Nat.add(V.ev(gg(h)), V.pos(17n, V.ev(l))), [], Li.skip(17n, a), Equal.sym(List<&2, U32>, Li.skip(17n, a), [], sk))),
194 A.tr(Nat.add(V.ev(gg(h)), V.pos(17n, V.ev(Li.skip(17n, a)))), V.ev(a), Nat.add(V.ev(h), 5n), ce, ea))
195
196def lenh(+h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}) -> {V.len(h) == 17n : Nat}:
197 N.eq_from_is_eq(V.len(h), 17n, L.and_left(Nat.is_eq(V.len(h), 17n), Bool.and(V.fit_all(h, 8n), Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n)), hh))
198
199def fith(+h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}) -> {V.fit_all(h, 8n) == True{} : Bool}:
200 L.and_left(V.fit_all(h, 8n), Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n), L.and_right(Nat.is_eq(V.len(h), 17n), Bool.and(V.fit_all(h, 8n), Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n)), hh))
201
202def toph(+h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}) -> {Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n) == True{} : Bool}:
203 L.and_right(V.fit_all(h, 8n), Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n), L.and_right(Nat.is_eq(V.len(h), 17n), Bool.and(V.fit_all(h, 8n), Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n)), hh))
204
205def len16(+h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}) -> {V.len(Li.take(16n, h)) == 16n : Nat}:
206 len_take_eq(16n, h, A.le_subst(16n, 17n, V.len(h), A.sy(V.len(h), 17n, lenh(h, hh)), {==}))
207
208law hsplit:
209 for +h: List<&2, U32>
210 for +hh: {ST.inv(h) == True{} : Bool}
211 {V.ev(h) == Nat.add(V.ev(Li.take(16n, h)), V.pos(16n, V.v(Li.hd0(Li.skip(16n, h))))) : Nat}
212
213def hsplit(h, hh):
214 +sk = Li.skip(16n, h)
215 A.tr(V.ev(h), Nat.add(V.ev(Li.take(16n, h)), V.pos(16n, V.ev(sk))), Nat.add(V.ev(Li.take(16n, h)), V.pos(16n, V.v(Li.hd0(sk)))), V.ts_ev(16n, h),
216 WM.cong_r(V.ev(Li.take(16n, h)), V.pos(16n, V.ev(sk)), V.pos(16n, V.v(Li.hd0(sk))), Equal.cong(Nat, Nat, z => V.pos(16n, z), V.ev(sk), V.v(Li.hd0(sk)),
217 V.ev_one(sk, V.len_skip(16n, h, 1n, N.eq_le(V.len(h), 17n, lenh(h, hh)))))))
218
219
220law hlt:
221 for +one: Nat
222 for +h1: {one == 1n : Nat}
223 for +h: List<&2, U32>
224 for +hh: {ST.inv(h) == True{} : Bool}
225 {Nat.is_lt(V.ev(h), Nat.add(V.pos(16n, one), C.shift(130n, one))) == True{} : Bool}
226
227def hlt(one, h1, h, hh):
228 +lh = V.ev(Li.take(16n, h))
229 +vt = V.v(Li.hd0(Li.skip(16n, h)))
230 +u = V.pos(16n, one)
231 +l1 = A.lt_subst(lh, V.pos(V.len(Li.take(16n, h)), one), u, Equal.cong(Nat, Nat, z => V.pos(z, one), V.len(Li.take(16n, h)), 16n, len16(h, hh)), V.ev_lt(Li.take(16n, h), one, h1, V.fit_take(16n, h, 8n, fith(h, hh))))
232 +e4 = A.sy(C.shift(2n, one), 4n, Equal.cong(Nat, Nat, z => C.shift(2n, z), one, 1n, h1))
233 +l2 = WW.shift_mono(128n, vt, C.shift(2n, one), A.le_subst(vt, 4n, C.shift(2n, one), e4, toph(h, hh)))
234 A.lt_substl(Nat.add(lh, V.pos(16n, vt)), V.ev(h), Nat.add(u, C.shift(130n, one)), A.sy(V.ev(h), Nat.add(lh, V.pos(16n, vt)), hsplit(h, hh)), A.lt_le_add(lh, V.pos(16n, vt), u, C.shift(130n, one), l1, l2))
235
236def lg(+h: List<&2, U32>) -> Nat:
237 V.ev(Li.take(16n, gg(h)))
238
239def tg(+h: List<&2, U32>) -> Nat:
240 Nat.add(V.v(Li.hd0(Li.skip(16n, gg(h)))), 0n)
241
242law gsplit:
243 for +one: Nat
244 for +h1: {one == 1n : Nat}
245 for +h: List<&2, U32>
246 for +hh: {ST.inv(h) == True{} : Bool}
247 {Nat.add(V.ev(h), 5n) == Nat.add(lg(h), C.shift(128n, tg(h))) : Nat}
248
249def gsplit(one, h1, h, hh):
250 A.tr(Nat.add(V.ev(h), 5n), V.ev(gg(h)), Nat.add(lg(h), C.shift(128n, tg(h))), A.sy(V.ev(gg(h)), Nat.add(V.ev(h), 5n), g_ev(one, h1, h, hh)), V.ts_ev(16n, gg(h)))
251
252def flg(+one: Nat, +h1: {one == 1n : Nat}, +h: List<&2, U32>) -> {C.fits(128n, lg(h)) == True{} : Bool}:
253 WW.fits_one(128n, one, h1, lg(h), V.ev_lt(Li.take(16n, gg(h)), one, h1, V.carry_lo(16n, Li.add(h, [5]), 0)))
254
255def bb(+h: List<&2, U32>) -> U32:
256 U32.shrn(Li.hd0(Li.skip(16n, gg(h))), 2n)
257
258law bval:
259 for +one: Nat
260 for +h1: {one == 1n : Nat}
261 for +h: List<&2, U32>
262 for +hh: {ST.inv(h) == True{} : Bool}
263 {V.v(bb(h)) == qq(h) : Nat}
264
265def bval(one, h1, h, hh):
266 +x = Nat.add(V.ev(h), 5n)
267 +tp = V.v(Li.hd0(Li.skip(16n, gg(h))))
268 +ehi = A.tr(C.high(128n, x), C.high(128n, Nat.add(lg(h), C.shift(128n, tg(h)))), tg(h), Equal.cong(Nat, Nat, z => C.high(128n, z), x, Nat.add(lg(h), C.shift(128n, tg(h))), gsplit(one, h1, h, hh)), WW.high_u(128n, lg(h), tg(h), flg(one, h1, h)))
269 A.tr(V.v(bb(h)), C.high(2n, tp), qq(h), SHN.shrn_high(Li.hd0(Li.skip(16n, gg(h))), 2n),
270 A.tr(C.high(2n, tp), C.high(2n, C.high(128n, x)), qq(h), Equal.cong(Nat, Nat, z => C.high(2n, z), tp, C.high(128n, x), A.tr(tp, tg(h), C.high(128n, x), A.sy(tg(h), tp, N.add_zero(tp)), A.sy(C.high(128n, x), tg(h), ehi))),
271 A.sy(qq(h), C.high(2n, C.high(128n, x)), WW.high_comp(2n, 128n, x))))
272
273
274def u16(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(16n, V.pos(16n, one)) == True{} : Bool}:
275 N.le_trans(16n, C.shift(4n, one), V.pos(16n, one), L.subst(Nat, z => {Nat.is_le(16n, C.shift(4n, z)) == True{} : Bool}, 1n, one, A.sy(one, 1n, h1), {==}), WW.shift_ge(124n, C.shift(4n, one)))
276
277def uu(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(Nat.add(V.pos(16n, one), V.pos(16n, one)), C.shift(130n, one)) == True{} : Bool}:
278 +u = V.pos(16n, one)
279 A.le_substl(Nat.double(u), Nat.add(u, u), C.shift(130n, one), NA.double_self(u), WW.shift_ge(1n, Nat.double(u)))
280
281law qlt2:
282 for +one: Nat
283 for +h1: {one == 1n : Nat}
284 for +h: List<&2, U32>
285 for +hh: {ST.inv(h) == True{} : Bool}
286 {Nat.is_lt(qq(h), 2n) == True{} : Bool}
287
288def qlt2(one, h1, h, hh):
289 +u = V.pos(16n, one)
290 +s = C.shift(130n, one)
291 +x = Nat.add(V.ev(h), 5n)
292 +l1 = N.lt_add_r2(V.ev(h), Nat.add(u, s), 5n, hlt(one, h1, h, hh))
293 +e1 = A.tr(Nat.add(Nat.add(u, s), 5n), Nat.add(u, Nat.add(s, 5n)), Nat.add(s, Nat.add(u, 5n)), N.add_assoc(u, s, 5n), A.tr(Nat.add(u, Nat.add(s, 5n)), Nat.add(u, Nat.add(5n, s)), Nat.add(s, Nat.add(u, 5n)), WM.cong_r(u, Nat.add(s, 5n), Nat.add(5n, s), N.add_comm(s, 5n)), A.tr(Nat.add(u, Nat.add(5n, s)), Nat.add(Nat.add(u, 5n), s), Nat.add(s, Nat.add(u, 5n)), A.sy(Nat.add(Nat.add(u, 5n), s), Nat.add(u, Nat.add(5n, s)), N.add_assoc(u, 5n, s)), N.add_comm(Nat.add(u, 5n), s))))
294 +l2 = N.le_add_left(Nat.add(u, 5n), s, s, N.le_trans(Nat.add(u, 5n), Nat.add(u, u), s, N.le_add_left(5n, u, u, N.le_trans(5n, 16n, u, {==}, u16(one, h1))), uu(one, h1)))
295 +l3 = N.lt_le_trans(x, Nat.add(s, Nat.add(u, 5n)), Nat.add(s, s), A.lt_subst(x, Nat.add(Nat.add(u, s), 5n), Nat.add(s, Nat.add(u, 5n)), e1, l1), l2)
296 +f131 = WW.fits_one(131n, one, h1, x, A.lt_subst(x, Nat.add(s, s), Nat.double(s), A.sy(Nat.double(s), Nat.add(s, s), NA.double_self(s)), l3))
297 WW.lt_of_fits(1n, qq(h), SH.fits_high(130n, 1n, x, f131))
298
299def heqlen(+h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}) -> {V.len(Li.take(16n, h)) == V.len(Li.take(16n, gg(h))) : Nat}:
300 A.tr(V.len(Li.take(16n, h)), 16n, V.len(Li.take(16n, gg(h))), len16(h, hh), {==})
301
302def qone(+one: Nat, +h1: {one == 1n : Nat}, +h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}, +hc: {Nat.is_eq(qq(h), 0n) == False{} : Bool}) -> {qq(h) == 1n : Nat}:
303 N.le_antisym(qq(h), 1n, N.lt_succ_le(qq(h), 1n, qlt2(one, h1, h, hh)), N.lt_succ_le_succ(0n, qq(h), N.lt_or_eq(0n, qq(h), N.zero_le(qq(h)), N.is_eq_sym_false(qq(h), 0n, hc))))
304
305def which0(+one: Nat, +h1: {one == 1n : Nat}, +h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}, +hc: {Nat.is_eq(qq(h), 0n) == True{} : Bool}) -> {Li.freeze(h) == Li.take(16n, h) : List<&2, U32>}:
306 +eb = U3.injective(bb(h), 0, A.tr(V.v(bb(h)), qq(h), 0n, bval(one, h1, h, hh), N.eq_from_is_eq(qq(h), 0n, hc)))
307 Equal.trans(List<&2, U32>, Li.freeze(h), Li.select(U32.sub(0, 0), Li.take(16n, h), Li.take(16n, gg(h))), Li.take(16n, h),
308 Equal.cong(U32, List<&2, U32>, w => Li.select(U32.sub(0, w), Li.take(16n, h), Li.take(16n, gg(h))), bb(h), 0, eb),
309 sel0(Li.take(16n, h), Li.take(16n, gg(h)), heqlen(h, hh)))
310
311def which1(+one: Nat, +h1: {one == 1n : Nat}, +h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}, +hc: {Nat.is_eq(qq(h), 0n) == False{} : Bool}) -> {Li.freeze(h) == Li.take(16n, gg(h)) : List<&2, U32>}:
312 +eb = U3.injective(bb(h), 1, A.tr(V.v(bb(h)), qq(h), 1n, bval(one, h1, h, hh), qone(one, h1, h, hh, hc)))
313 Equal.trans(List<&2, U32>, Li.freeze(h), Li.select(U32.sub(0, 1), Li.take(16n, h), Li.take(16n, gg(h))), Li.take(16n, gg(h)),
314 Equal.cong(U32, List<&2, U32>, w => Li.select(U32.sub(0, w), Li.take(16n, h), Li.take(16n, gg(h))), bb(h), 1, eb),
315 sel1(Li.take(16n, h), Li.take(16n, gg(h)), heqlen(h, hh)))
316
317def which_c(+one: Nat, +h1: {one == 1n : Nat}, +h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(qq(h), 0n) == c : Bool}) -> Or({Li.freeze(h) == Li.take(16n, h) : List<&2, U32>}, {Li.freeze(h) == Li.take(16n, gg(h)) : List<&2, U32>}):
318 match c:
319 case True{}: Inl{which0(one, h1, h, hh, hc)}
320 case False{}: Inr{which1(one, h1, h, hh, hc)}
321
322def fz_fit_o(+h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}, o: Or({Li.freeze(h) == Li.take(16n, h) : List<&2, U32>}, {Li.freeze(h) == Li.take(16n, gg(h)) : List<&2, U32>})) -> {V.fit_all(Li.freeze(h), 8n) == True{} : Bool}:
323 match o:
324 case Inl{e}: L.subst(List<&2, U32>, l => {V.fit_all(l, 8n) == True{} : Bool}, Li.take(16n, h), Li.freeze(h), Equal.sym(List<&2, U32>, Li.freeze(h), Li.take(16n, h), e), V.fit_take(16n, h, 8n, fith(h, hh)))
325 case Inr{e}: L.subst(List<&2, U32>, l => {V.fit_all(l, 8n) == True{} : Bool}, Li.take(16n, gg(h)), Li.freeze(h), Equal.sym(List<&2, U32>, Li.freeze(h), Li.take(16n, gg(h)), e), V.carry_lo(16n, Li.add(h, [5]), 0))
326
327law freeze_fit:
328 for +one: Nat
329 for +h1: {one == 1n : Nat}
330 for +h: List<&2, U32>
331 for +hh: {ST.inv(h) == True{} : Bool}
332 {V.fit_all(Li.freeze(h), 8n) == True{} : Bool}
333
334def freeze_fit(one, h1, h, hh):
335 fz_fit_o(h, hh, which_c(one, h1, h, hh, Nat.is_eq(qq(h), 0n), {==}))
336
337law freeze_len:
338 for +one: Nat
339 for +h1: {one == 1n : Nat}
340 for +h: List<&2, U32>
341 for +hh: {ST.inv(h) == True{} : Bool}
342 {Nat.is_le(V.len(Li.freeze(h)), 16n) == True{} : Bool}
343
344def fz_len_o(+h: List<&2, U32>, o: Or({Li.freeze(h) == Li.take(16n, h) : List<&2, U32>}, {Li.freeze(h) == Li.take(16n, gg(h)) : List<&2, U32>})) -> {Nat.is_le(V.len(Li.freeze(h)), 16n) == True{} : Bool}:
345 match o:
346 case Inl{e}: L.subst(List<&2, U32>, l => {Nat.is_le(V.len(l), 16n) == True{} : Bool}, Li.take(16n, h), Li.freeze(h), Equal.sym(List<&2, U32>, Li.freeze(h), Li.take(16n, h), e), V.len_take(16n, h))
347 case Inr{e}: L.subst(List<&2, U32>, l => {Nat.is_le(V.len(l), 16n) == True{} : Bool}, Li.take(16n, gg(h)), Li.freeze(h), Equal.sym(List<&2, U32>, Li.freeze(h), Li.take(16n, gg(h)), e), V.len_take(16n, gg(h)))
348
349def freeze_len(one, h1, h, hh):
350 fz_len_o(h, which_c(one, h1, h, hh, Nat.is_eq(qq(h), 0n), {==}))
351
352
353
354
355law elg_k:
356 for +k: Nat
357 for +x: Nat
358 for +lgv: Nat
359 for +tgv: Nat
360 for +d: Nat
361 for +s2: Nat
362 for +hs: {x == Nat.add(lgv, C.shift(k, tgv)) : Nat}
363 for +hf: {C.fits(k, lgv) == True{} : Bool}
364 for +hx: {x == Nat.add(d, C.shift(k, s2)) : Nat}
365 {lgv == C.low(k, d) : Nat}
366
367def elg_k(k, x, lgv, tgv, d, s2, hs, hf, hx):
368 A.tr(lgv, C.low(k, x), C.low(k, d),
369 A.sy(C.low(k, x), lgv, A.tr(C.low(k, x), C.low(k, Nat.add(lgv, C.shift(k, tgv))), lgv, Equal.cong(Nat, Nat, z => C.low(k, z), x, Nat.add(lgv, C.shift(k, tgv)), hs), WW.low_u(k, lgv, tgv, hf))),
370 A.tr(C.low(k, x), C.low(k, Nat.add(d, C.shift(k, s2))), C.low(k, d), Equal.cong(Nat, Nat, z => C.low(k, z), x, Nat.add(d, C.shift(k, s2)), hx), WW.low_add_shift(k, d, s2)))
371
372law fin_k:
373 for +k: Nat
374 for +a: Nat
375 for +b: Nat
376 for +c: Nat
377 for +m: Nat
378 for +e1: {a == b : Nat}
379 for +e2: {b == C.low(k, c) : Nat}
380 for +e3: {m == c : Nat}
381 {a == C.low(k, m) : Nat}
382
383def fin_k(k, a, b, c, m, e1, e2, e3):
384 A.tr(a, b, C.low(k, m), e1, A.tr(b, C.low(k, c), C.low(k, m), e2, Equal.cong(Nat, Nat, z => C.low(k, z), c, m, A.sy(m, c, e3))))
385
386law fe_k:
387 for +k: Nat
388 for +x: Nat
389 for +lgv: Nat
390 for +tgv: Nat
391 for +d: Nat
392 for +s2: Nat
393 for +a: Nat
394 for +m: Nat
395 for +hs: {x == Nat.add(lgv, C.shift(k, tgv)) : Nat}
396 for +hf: {C.fits(k, lgv) == True{} : Bool}
397 for +hx: {x == Nat.add(d, C.shift(k, s2)) : Nat}
398 for +e1: {a == lgv : Nat}
399 for +e3: {m == d : Nat}
400 {a == C.low(k, m) : Nat}
401
402def fe_k(k, x, lgv, tgv, d, s2, a, m, hs, hf, hx, e1, e3):
403 fin_k(k, a, lgv, d, m, e1, elg_k(k, x, lgv, tgv, d, s2, hs, hf, hx), e3)
404
405def frz_c(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +h5: {Nat.add(1n+bp, 5n) == C.shift(130n, one) : Nat}, +h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(qq(h), 0n) == c : Bool}) -> {V.ev(Li.freeze(h)) == C.low(128n, Nat.mod(V.ev(h), 1n+bp)) : Nat}:
406 match c:
407 case True{}:
408 +pp = {1n+bp : Nat}
409 +x = Nat.add(V.ev(h), 5n)
410 +lh = V.ev(Li.take(16n, h))
411 +vt = V.v(Li.hd0(Li.skip(16n, h)))
412 +ef = Equal.cong(List<&2, U32>, Nat, l => V.ev(l), Li.freeze(h), Li.take(16n, h), which0(one, h1, h, hh, hc))
413 +lx = A.lt_subst(x, C.shift(130n, one), Nat.add(pp, 5n), A.sy(Nat.add(pp, 5n), C.shift(130n, one), h5), WW.lt_one(130n, one, h1, x, hc))
414 +lp = A.btrue(Nat.is_lt(V.ev(h), pp), Nat.is_lt(x, Nat.add(pp, 5n)), Equal.sym(Bool, Nat.is_lt(x, Nat.add(pp, 5n)), Nat.is_lt(V.ev(h), pp), WW.lt_cancel_r(V.ev(h), pp, 5n)), lx)
415 +em = NR.mod_of(0n, bp, V.ev(h), lp)
416 +flh = WW.fits_one(128n, one, h1, lh, A.lt_subst(lh, V.pos(V.len(Li.take(16n, h)), one), V.pos(16n, one), Equal.cong(Nat, Nat, z => V.pos(z, one), V.len(Li.take(16n, h)), 16n, len16(h, hh)), V.ev_lt(Li.take(16n, h), one, h1, V.fit_take(16n, h, 8n, fith(h, hh)))))
417 +el = A.tr(C.low(128n, V.ev(h)), C.low(128n, Nat.add(lh, V.pos(16n, vt))), lh, Equal.cong(Nat, Nat, z => C.low(128n, z), V.ev(h), Nat.add(lh, V.pos(16n, vt)), hsplit(h, hh)), WW.low_u(128n, lh, vt, flh))
418 A.tr(V.ev(Li.freeze(h)), lh, C.low(128n, Nat.mod(V.ev(h), pp)), ef,
419 A.sy(C.low(128n, Nat.mod(V.ev(h), pp)), lh, A.tr(C.low(128n, Nat.mod(V.ev(h), pp)), C.low(128n, V.ev(h)), lh, Equal.cong(Nat, Nat, z => C.low(128n, z), Nat.mod(V.ev(h), pp), V.ev(h), em), el)))
420 case False{}:
421 +pp = {1n+bp : Nat}
422 +s = C.shift(130n, one)
423 +u = V.pos(16n, one)
424 +x = Nat.add(V.ev(h), 5n)
425 +d = C.low(130n, x)
426 +q = qq(h)
427 +ef = Equal.cong(List<&2, U32>, Nat, l => V.ev(l), Li.freeze(h), Li.take(16n, gg(h)), which1(one, h1, h, hh, hc))
428 +eq1 = qone(one, h1, h, hh, hc)
429 +es = A.tr(C.shift(130n, q), Nat.mul(q, s), s, WW.shift_mul_one(130n, one, h1, q), A.tr(Nat.mul(q, s), Nat.mul(1n, s), s, Equal.cong(Nat, Nat, z => Nat.mul(z, s), q, 1n, eq1), AR.one_mul(s)))
430 +ex = A.tr(x, Nat.add(d, C.shift(130n, q)), Nat.add(d, s), WW.low_high(130n, x), WM.cong_r(d, C.shift(130n, q), s, es))
431 +ex2 = A.tr(Nat.add(V.ev(h), 5n), Nat.add(d, Nat.add(pp, 5n)), Nat.add(Nat.add(d, pp), 5n), A.tr(x, Nat.add(d, s), Nat.add(d, Nat.add(pp, 5n)), ex, WM.cong_r(d, s, Nat.add(pp, 5n), A.sy(Nat.add(pp, 5n), s, h5))), A.sy(Nat.add(Nat.add(d, pp), 5n), Nat.add(d, Nat.add(pp, 5n)), N.add_assoc(d, pp, 5n)))
432 +eh = UA.add_cancel_r(V.ev(h), Nat.add(d, pp), 5n, ex2)
433
434 +l1 = N.lt_add_r2(V.ev(h), Nat.add(u, s), 5n, hlt(one, h1, h, hh))
435 +e1 = A.tr(Nat.add(Nat.add(u, s), 5n), Nat.add(u, Nat.add(s, 5n)), Nat.add(Nat.add(u, 5n), s), N.add_assoc(u, s, 5n), A.tr(Nat.add(u, Nat.add(s, 5n)), Nat.add(u, Nat.add(5n, s)), Nat.add(Nat.add(u, 5n), s), WM.cong_r(u, Nat.add(s, 5n), Nat.add(5n, s), N.add_comm(s, 5n)), A.sy(Nat.add(Nat.add(u, 5n), s), Nat.add(u, Nat.add(5n, s)), N.add_assoc(u, 5n, s))))
436 +l2 = A.lt_substl(x, Nat.add(d, s), Nat.add(Nat.add(u, 5n), s), ex, A.lt_subst(x, Nat.add(Nat.add(u, s), 5n), Nat.add(Nat.add(u, 5n), s), e1, l1))
437 +ld = A.btrue(Nat.is_lt(d, Nat.add(u, 5n)), Nat.is_lt(Nat.add(d, s), Nat.add(Nat.add(u, 5n), s)), Equal.sym(Bool, Nat.is_lt(Nat.add(d, s), Nat.add(Nat.add(u, 5n), s)), Nat.is_lt(d, Nat.add(u, 5n)), WW.lt_cancel_r(d, Nat.add(u, 5n), s)), l2)
438 +l9 = N.lt_le_trans(Nat.add(u, 9n), Nat.add(u, u), s, N.lt_add_left(9n, u, u, N.lt_le_trans(9n, 16n, u, {==}, u16(one, h1))), uu(one, h1))
439 +l9b = A.lt_substl(Nat.add(u, 9n), Nat.add(Nat.add(u, 4n), 5n), Nat.add(pp, 5n), A.sy(Nat.add(Nat.add(u, 4n), 5n), Nat.add(u, 9n), N.add_assoc(u, 4n, 5n)), A.lt_subst(Nat.add(u, 9n), s, Nat.add(pp, 5n), A.sy(Nat.add(pp, 5n), s, h5), l9))
440 +l4 = A.btrue(Nat.is_lt(Nat.add(u, 4n), pp), Nat.is_lt(Nat.add(Nat.add(u, 4n), 5n), Nat.add(pp, 5n)), Equal.sym(Bool, Nat.is_lt(Nat.add(Nat.add(u, 4n), 5n), Nat.add(pp, 5n)), Nat.is_lt(Nat.add(u, 4n), pp), WW.lt_cancel_r(Nat.add(u, 4n), pp, 5n)), l9b)
441 +l5 = A.le_substl(1n+Nat.add(u, 4n), Nat.add(u, 5n), pp, A.sy(Nat.add(u, 5n), 1n+Nat.add(u, 4n), N.add_succ(u, 4n)), N.lt_succ_le_succ(Nat.add(u, 4n), pp, l4))
442 +ldp = N.lt_le_trans(d, Nat.add(u, 5n), pp, ld, l5)
443 +em = A.tr(Nat.mod(V.ev(h), pp), Nat.mod(Nat.add(Nat.mul(1n, pp), d), pp), d,
444 Equal.cong(Nat, Nat, z => Nat.mod(z, pp), V.ev(h), Nat.add(Nat.mul(1n, pp), d), A.tr(V.ev(h), Nat.add(d, pp), Nat.add(Nat.mul(1n, pp), d), eh, A.tr(Nat.add(d, pp), Nat.add(pp, d), Nat.add(Nat.mul(1n, pp), d), N.add_comm(d, pp), WM.cong_l(pp, Nat.mul(1n, pp), d, A.sy(Nat.mul(1n, pp), pp, AR.one_mul(pp)))))),
445 NR.mod_of(1n, bp, d, ldp))
446 fe_k(128n, x, lg(h), tg(h), d, C.shift(2n, one), V.ev(Li.freeze(h)), Nat.mod(V.ev(h), pp), gsplit(one, h1, h, hh), flg(one, h1, h), ex, ef, em)
447
448law freeze_ev:
449 for +one: Nat
450 for +h1: {one == 1n : Nat}
451 for +bp: Nat
452 for +h5: {Nat.add(1n+bp, 5n) == C.shift(130n, one) : Nat}
453 for +h: List<&2, U32>
454 for +hh: {ST.inv(h) == True{} : Bool}
455 {V.ev(Li.freeze(h)) == C.low(128n, Nat.mod(V.ev(h), 1n+bp)) : Nat}
456
457def freeze_ev(one, h1, bp, h5, h, hh):
458 frz_c(one, h1, bp, h5, h, hh, Nat.is_eq(qq(h), 0n), {==})
459
460
461
462law bytes_le:
463 for +n: Nat
464 for +ds: List<&2, U32>
465 for +u: U32
466 for +k: Nat
467 for +j: Nat
468 for +hj: {Nat.is_le(Nat.add(9n, j), 32n) == True{} : Bool}
469 for +hd: {V.fit_all(ds, Nat.add(8n, j)) == True{} : Bool}
470 for +hu: {C.fits(Nat.add(8n, j), V.v(u)) == True{} : Bool}
471 {Li.bytes(n, ds, u) == R.le_bytes(n, Nat.add(Nat.add(V.v(u), V.ev(ds)), V.pos(n, k))) : List<&2, U32>}
472
473def bytes_le(n, ds, u, k, j, hj, hd, hu):
474 match n:
475 case 0n: {==}
476 case 1n+m:
477 +h = Li.hd0(ds)
478 +s = U32.add(u, h)
479 +vs = V.v(s)
480 +u2 = U32.shrn(s, 8n)
481 +et = V.ev(Li.tl(ds))
482 +pk = V.pos(m, k)
483 +y = Nat.add(Nat.add(V.v(u), V.ev(ds)), C.shift(8n, pk))
484 +y2 = Nat.add(vs, C.shift(8n, Nat.add(et, pk)))
485 +es = V.step_ev(ds, u, j, hj, hd, hu)
486 +ey = A.tr(y, Nat.add(Nat.add(V.v(u), Nat.add(V.v(h), C.shift(8n, et))), C.shift(8n, pk)), y2,
487 WM.cong_l(Nat.add(V.v(u), V.ev(ds)), Nat.add(V.v(u), Nat.add(V.v(h), C.shift(8n, et))), C.shift(8n, pk), WM.cong_r(V.v(u), V.ev(ds), Nat.add(V.v(h), C.shift(8n, et)), V.hd_tl_ev(ds))),
488 A.tr(Nat.add(Nat.add(V.v(u), Nat.add(V.v(h), C.shift(8n, et))), C.shift(8n, pk)), Nat.add(Nat.add(Nat.add(V.v(u), V.v(h)), C.shift(8n, et)), C.shift(8n, pk)), y2,
489 WM.cong_l(Nat.add(V.v(u), Nat.add(V.v(h), C.shift(8n, et))), Nat.add(Nat.add(V.v(u), V.v(h)), C.shift(8n, et)), C.shift(8n, pk), A.sy(Nat.add(Nat.add(V.v(u), V.v(h)), C.shift(8n, et)), Nat.add(V.v(u), Nat.add(V.v(h), C.shift(8n, et))), N.add_assoc(V.v(u), V.v(h), C.shift(8n, et)))),
490 A.tr(Nat.add(Nat.add(Nat.add(V.v(u), V.v(h)), C.shift(8n, et)), C.shift(8n, pk)), Nat.add(Nat.add(V.v(u), V.v(h)), C.shift(8n, Nat.add(et, pk))), y2,
491 V.sh3(Nat.add(V.v(u), V.v(h)), et, pk),
492 WM.cong_l(Nat.add(V.v(u), V.v(h)), vs, C.shift(8n, Nat.add(et, pk)), A.sy(vs, Nat.add(V.v(u), V.v(h)), es)))))
493 +elo = WW.low_add_shift(8n, vs, Nat.add(et, pk))
494 +ehi = A.tr(C.high(8n, y2), Nat.add(C.high(8n, vs), Nat.add(et, pk)), Nat.add(Nat.add(V.v(u2), et), pk), WW.high_add_shift(8n, vs, Nat.add(et, pk)),
495 A.tr(Nat.add(C.high(8n, vs), Nat.add(et, pk)), Nat.add(V.v(u2), Nat.add(et, pk)), Nat.add(Nat.add(V.v(u2), et), pk), WM.cong_l(C.high(8n, vs), V.v(u2), Nat.add(et, pk), A.sy(V.v(u2), C.high(8n, vs), SHN.shrn_high(s, 8n))), A.sy(Nat.add(Nat.add(V.v(u2), et), pk), Nat.add(V.v(u2), Nat.add(et, pk)), N.add_assoc(V.v(u2), et, pk))))
496 +lo8 = C.low(8n, vs)
497 +eb = U3.injective(U32.and(s, 255), U32.from_nat(lo8), A.tr(V.v(U32.and(s, 255)), lo8, V.v(U32.from_nat(lo8)), FB.andm(s, 8n, 255, {==}), A.sy(V.v(U32.from_nat(lo8)), lo8, U3.to_nat_from_nat(lo8, 8n, {==}, WW.low_lt(8n, vs)))))
498 +ih = bytes_le(m, Li.tl(ds), u2, k, j, hj, V.tl_fit(ds, Nat.add(8n, j), hd), V.next_fit(ds, u, j, hj, hd, hu))
499 Equal.trans(List<&2, U32>, U32.and(s, 255) <> Li.bytes(m, Li.tl(ds), u2), R.le_bytes(1n+m, y2), R.le_bytes(1n+m, y),
500 Equal.trans(List<&2, U32>, U32.and(s, 255) <> Li.bytes(m, Li.tl(ds), u2), U32.from_nat(lo8) <> R.le_bytes(m, Nat.add(Nat.add(V.v(u2), et), pk)), R.le_bytes(1n+m, y2),
501 Equal.trans(List<&2, U32>, U32.and(s, 255) <> Li.bytes(m, Li.tl(ds), u2), U32.from_nat(lo8) <> Li.bytes(m, Li.tl(ds), u2), U32.from_nat(lo8) <> R.le_bytes(m, Nat.add(Nat.add(V.v(u2), et), pk)),
502 Equal.cong(U32, List<&2, U32>, z => z <> Li.bytes(m, Li.tl(ds), u2), U32.and(s, 255), U32.from_nat(lo8), eb),
503 Equal.cong(List<&2, U32>, List<&2, U32>, z => U32.from_nat(lo8) <> z, Li.bytes(m, Li.tl(ds), u2), R.le_bytes(m, Nat.add(Nat.add(V.v(u2), et), pk)), ih)),
504 Equal.trans(List<&2, U32>, U32.from_nat(lo8) <> R.le_bytes(m, Nat.add(Nat.add(V.v(u2), et), pk)), U32.from_nat(C.low(8n, y2)) <> R.le_bytes(m, Nat.add(Nat.add(V.v(u2), et), pk)), R.le_bytes(1n+m, y2),
505 Equal.cong(Nat, List<&2, U32>, z => U32.from_nat(z) <> R.le_bytes(m, Nat.add(Nat.add(V.v(u2), et), pk)), lo8, C.low(8n, y2), A.sy(C.low(8n, y2), lo8, elo)),
506 Equal.cong(Nat, List<&2, U32>, z => U32.from_nat(C.low(8n, y2)) <> R.le_bytes(m, z), Nat.add(Nat.add(V.v(u2), et), pk), C.high(8n, y2), A.sy(C.high(8n, y2), Nat.add(Nat.add(V.v(u2), et), pk), ehi)))),
507 Equal.cong(Nat, List<&2, U32>, z => R.le_bytes(1n+m, z), y2, y, A.sy(y, y2, ey)))
508
509
510
511law bytes_le_to:
512 for +n: Nat
513 for +ds: List<&2, U32>
514 for +k: Nat
515 for +t: Nat
516 for +hb: {Li.bytes(n, ds, 0) == R.le_bytes(n, Nat.add(Nat.add(V.v(0), V.ev(ds)), V.pos(n, k))) : List<&2, U32>}
517 for +ht: {Nat.add(V.ev(ds), V.pos(n, k)) == t : Nat}
518 {Li.bytes(n, ds, 0) == R.le_bytes(n, t) : List<&2, U32>}
519
520def bytes_le_to(n, ds, k, t, hb, ht):
521 Equal.trans(List<&2, U32>, Li.bytes(n, ds, 0), R.le_bytes(n, Nat.add(V.ev(ds), V.pos(n, k))), R.le_bytes(n, t), hb,
522 Equal.cong(Nat, List<&2, U32>, z => R.le_bytes(n, z), Nat.add(V.ev(ds), V.pos(n, k)), t, ht))
523
524
525law tag_eq:
526 for +one: Nat
527 for +h1: {one == 1n : Nat}
528 for +bp: Nat
529 for +h5: {Nat.add(1n+bp, 5n) == C.shift(130n, one) : Nat}
530 for +h: List<&2, U32>
531 for +hh: {ST.inv(h) == True{} : Bool}
532 for +s: List<&2, U32>
533 for +hs: {V.fit_all(s, 8n) == True{} : Bool}
534 {Li.bytes(16n, Li.add(Li.freeze(h), s), 0) == R.le_bytes(16n, Nat.add(Nat.mod(V.ev(h), 1n+bp), V.ev(s))) : List<&2, U32>}
535
536def tag_eq(one, h1, bp, h5, h, hh, s, hs):
537 +s8 = C.shift(8n, one)
538 +s9 = C.shift(9n, one)
539 +fz = Li.freeze(h)
540 +a = Nat.mod(V.ev(h), 1n+bp)
541 +lo = C.low(128n, a)
542 +kk = C.high(128n, a)
543 +ds = Li.add(fz, s)
544 +hf = freeze_fit(one, h1, h, hh)
545 +hf1 = ST.s8fit(one, h1)
546 +ed = V.add_ev(fz, s, s8, s8, V.fit_le(fz, 8n, one, h1, hf), V.fit_le(s, 8n, one, h1, hs), hf1)
547 +l10 = A.lt_substl(s9, Nat.add(s8, s8), Nat.double(s9), NA.double_self(s8), lt_dbl(s9, A.one_le_shift(9n, one, h1)))
548 +hd = V.le_fit(ds, Nat.add(s8, s8), 10n, one, h1, l10, V.add_le(fz, s, s8, s8, V.fit_le(fz, 8n, one, h1, hf), V.fit_le(s, 8n, one, h1, hs), hf1))
549 +bl = bytes_le(16n, ds, 0, kk, 2n, {==}, hd, {==})
550
551 +e1 = A.tr(Nat.add(V.ev(ds), V.pos(16n, kk)), Nat.add(Nat.add(lo, V.ev(s)), V.pos(16n, kk)), Nat.add(a, V.ev(s)),
552 WM.cong_l(V.ev(ds), Nat.add(lo, V.ev(s)), V.pos(16n, kk), A.tr(V.ev(ds), Nat.add(V.ev(fz), V.ev(s)), Nat.add(lo, V.ev(s)), ed, WM.cong_l(V.ev(fz), lo, V.ev(s), freeze_ev(one, h1, bp, h5, h, hh)))),
553 A.tr(Nat.add(Nat.add(lo, V.ev(s)), V.pos(16n, kk)), Nat.add(Nat.add(lo, V.pos(16n, kk)), V.ev(s)), Nat.add(a, V.ev(s)),
554 A.tr(Nat.add(Nat.add(lo, V.ev(s)), V.pos(16n, kk)), Nat.add(lo, Nat.add(V.ev(s), V.pos(16n, kk))), Nat.add(Nat.add(lo, V.pos(16n, kk)), V.ev(s)), N.add_assoc(lo, V.ev(s), V.pos(16n, kk)), ST.rot(lo, V.ev(s), V.pos(16n, kk))),
555 WM.cong_l(Nat.add(lo, V.pos(16n, kk)), a, V.ev(s), A.sy(a, Nat.add(lo, V.pos(16n, kk)), WW.low_high(128n, a)))))
556 bytes_le_to(16n, ds, kk, Nat.add(a, V.ev(s)), bl, e1)
557
558
559law fin_eq:
560 for +one: Nat
561 for +h1: {one == 1n : Nat}
562 for +bp: Nat
563 for +h5: {Nat.add(1n+bp, 5n) == C.shift(130n, one) : Nat}
564 for +h: List<&2, U32>
565 for +hh: {ST.inv(h) == True{} : Bool}
566 for +s: List<&2, U32>
567 for +hs: {V.fit_all(s, 8n) == True{} : Bool}
568 {Li.fin(h, s) == R.le_bytes(16n, Nat.add(Nat.mod(V.ev(h), 1n+bp), V.ev(s))) : List<&2, U32>}
569
570def fin_eq(one, h1, bp, h5, h, hh, s, hs):
571 match s:
572 case Nil{}: tag_eq(one, h1, bp, h5, h, hh, Nil{}, hs)
573 case y <> ys: tag_eq(one, h1, bp, h5, h, hh, y <> ys, hs)