PROOF.bend
1import Base
2import bend-osdev-bytes@0.1.1.0/bytes.bend as B
3import bend-osdev-bytes@0.1.1.0/LAWS.bend as BL
4import bend-osdev-bytes@0.1.1.0/PROOF.bend as BP
5import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
6import bend-osdev-pkcs7@0.1.0.0/pkcs7.bend as P
7import bend-osdev-pkcs7@0.1.0.0/LAWS.bend as Laws
8import bend-osdev-u32@0.1.0.0/LAWS.bend as UL
9import bend-osdev-u32@0.1.0.0/PROOF.bend as UP
10
11# How the proofs go. Padding m (L bytes) to blocks of bs = 1 + q bytes
12# appends p = bs - (L mod bs) bytes of value p. The arithmetic: L mod bs is
13# at most q, so p = 1 + (q - L mod bs) is 1 to bs, and L + p is a multiple
14# of bs (pk.mod_pad, on Base's Nat.divmod.go, as kmath's division lemmas
15# are). Unpadding reads the last byte back: p is at most 255, and U32's
16# value of the byte of p is p (pk.u8, every value checked by computation:
17# U32.from_nat builds a word by increments, so no general lemma is needed);
18# the last p bytes are all p, so their XOR difference is 0 (pk.diff_fill:
19# each byte XOR itself is 0, bit by bit); and the first L bytes are m (the
20# bytes interface laws on take, drop and at of an append). Nothing looks
21# inside Octets.
22
23# Booleans: False is not True
24
25def pk.disc(b: Bool) -> Type:
26 match b:
27 case False{}:
28 Unit
29 case True{}:
30 Empty
31
32def pk.empty(h: {False{} == True{} : Bool}) -> Empty:
33 %h : pk.disc(_)
34 Unit{}
35
36def pk.absurd(-A: Type, h: {False{} == True{} : Bool}) -> A:
37 Empty.absurd(A, pk.empty(h))
38
39# Naturals
40
41def pk.sub_zero(+a: Nat) -> {Nat.sub(a, 0n) == a : Nat}:
42 match a:
43 case 0n:
44 {==}
45 case 1n+p:
46 {==}
47
48# (L + k) - k is L
49def pk.add_sub(+l: Nat, +k: Nat) -> {Nat.sub(Nat.add(l, k), k) == l : Nat}:
50 match k:
51 case 0n:
52 %UL.nat_add_zero(l) : {Nat.sub(Nat.add(l, 0n), 0n) == _ : Nat}
53 pk.sub_zero(Nat.add(l, 0n))
54 case 1n+kp:
55 %Equal.sym(Nat, Nat.add(l, 1n+kp), 1n+Nat.add(l, kp), UL.nat_add_succ(l, kp)) : {Nat.sub(_, 1n+kp) == l : Nat}
56 pk.add_sub(l, kp)
57
58def pk.le_step(+x: Nat, +y: Nat) -> {Nat.is_le(x, y) == True{} : Bool} -> {Nat.is_le(x, 1n+y) == True{} : Bool}:
59 match x y:
60 case 0n _:
61 h => {==}
62 case 1n+xp 0n:
63 h => pk.absurd({Nat.is_le(1n+xp, 1n) == True{} : Bool}, h)
64 case 1n+xp 1n+yp:
65 h => pk.le_step(xp, yp)(h)
66
67# q - r <= q
68def pk.le_sub(+q: Nat, +r: Nat) -> {Nat.is_le(Nat.sub(q, r), q) == True{} : Bool}:
69 match q r:
70 case 0n _:
71 {==}
72 case 1n+qp 0n:
73 UL.nat_le_refl(qp)
74 case 1n+qp 1n+rp:
75 pk.le_step(Nat.sub(qp, rp), qp)(pk.le_sub(qp, rp))
76
77# r <= q gives (1 + q) - r = 1 + (q - r)
78def pk.sub_succ(+r: Nat, +q: Nat) -> {Nat.is_le(r, q) == True{} : Bool} -> {Nat.sub(1n+q, r) == 1n+Nat.sub(q, r) : Nat}:
79 match r q:
80 case 0n _:
81 h => %Equal.sym(Nat, Nat.sub(q, 0n), q, pk.sub_zero(q)) : {1n+q == 1n+_ : Nat}
82 {==}
83 case 1n+rp 0n:
84 h => pk.absurd({Nat.sub(1n, 1n+rp) == 1n+Nat.sub(0n, 1n+rp) : Nat}, h)
85 case 1n+rp 1n+qp:
86 h => pk.sub_succ(rp, qp)(h)
87
88def pk.le_trans(+a: Nat, +b: Nat, +c: Nat) -> {Nat.is_le(a, b) == True{} : Bool} -> {Nat.is_le(b, c) == True{} : Bool} -> {Nat.is_le(a, c) == True{} : Bool}:
89 match a b c:
90 case 0n _ 0n:
91 h1 => h2 => {==}
92 case 0n _ 1n+cp:
93 h1 => h2 => {==}
94 case 1n+ap 0n _:
95 h1 => h2 => pk.absurd({Nat.is_le(1n+ap, c) == True{} : Bool}, h1)
96 case 1n+ap 1n+bp 0n:
97 h1 => h2 => pk.absurd({Nat.is_le(1n+ap, 0n) == True{} : Bool}, h2)
98 case 1n+ap 1n+bp 1n+cp:
99 h1 => h2 => pk.le_trans(ap, bp, cp)(h1)(h2)
100
101def pk.le0(+y: Nat) -> {Nat.is_le(0n, y) == True{} : Bool}:
102 match y:
103 case 0n:
104 {==}
105 case 1n+yp:
106 {==}
107
108def pk.lt0(+x: Nat) -> {Nat.is_lt(x, 0n) == True{} : Bool} -> {False{} == True{} : Bool}:
109 match x:
110 case 0n:
111 h => h
112 case 1n+xp:
113 h => h
114
115def pk.lt_le(+x: Nat, +y: Nat) -> {Nat.is_lt(x, 1n+y) == True{} : Bool} -> {Nat.is_le(x, y) == True{} : Bool}:
116 match x:
117 case 0n:
118 h => pk.le0(y)
119 case 1n+xp:
120 match y:
121 case 0n:
122 h => pk.absurd({Nat.is_le(1n+xp, 0n) == True{} : Bool}, pk.lt0(xp)(h))
123 case 1n+yp:
124 h => pk.lt_le(xp, yp)(h)
125
126# Base's division: n counts down the dividend, m the steps left before the
127# remainder wraps, d the quotient, r the remainder so far (m + r = q, for a
128# divisor 1 + q)
129
130# 1 + m + x steps from (m, d, r) take one wrap and leave x
131def pk.go_skip(+m: Nat, +x: Nat, +d: Nat, +r: Nat) -> {Nat.divmod.go(1n+Nat.add(m, x), m, d, r) == Nat.divmod.go(x, Nat.add(m, r), 1n+d, 0n) : Nat & Nat}:
132 match m:
133 case 0n:
134 {==}
135 case 1n+mp:
136 Equal.trans(Nat & Nat, Nat.divmod.go(1n+Nat.add(mp, x), mp, d, 1n+r), Nat.divmod.go(x, Nat.add(mp, 1n+r), 1n+d, 0n), Nat.divmod.go(x, 1n+Nat.add(mp, r), 1n+d, 0n), pk.go_skip(mp, x, d, 1n+r), Equal.cong(Nat, Nat & Nat, z => Nat.divmod.go(x, z, 1n+d, 0n), Nat.add(mp, 1n+r), 1n+Nat.add(mp, r), UL.nat_add_succ(mp, r)))
137
138# (1 + m + r) - r = 1 + m
139def pk.sub_add_r(+m: Nat, +r: Nat) -> {Nat.sub(1n+Nat.add(m, r), r) == 1n+m : Nat}:
140 match r:
141 case 0n:
142 %UL.nat_add_zero(m) : {Nat.sub(1n+Nat.add(m, 0n), 0n) == 1n+_ : Nat}
143 {==}
144 case 1n+rp:
145 %Equal.sym(Nat, Nat.add(m, 1n+rp), 1n+Nat.add(m, rp), UL.nat_add_succ(m, rp)) : {Nat.sub(1n+_, 1n+rp) == 1n+m : Nat}
146 pk.sub_add_r(m, rp)
147
148# the remainder is at most q
149def pk.mod_le(+a: Nat, +m: Nat, +d: Nat, +r: Nat, +q: Nat) -> {Nat.add(m, r) == q : Nat} -> {Nat.is_le(Pair.snd(Nat, Nat, Nat.divmod.go(a, m, d, r)), q) == True{} : Bool}:
150 match a:
151 case 0n:
152 inv => %inv : {Nat.is_le(r, _) == True{} : Bool}
153 UL.nat_le_add(r, m)
154 case 1n+ap:
155 match m:
156 case 0n:
157 inv => pk.mod_le(ap, r, 1n+d, 0n, q)(Equal.trans(Nat, Nat.add(r, 0n), r, q, UL.nat_add_zero(r), inv))
158 case 1n+mp:
159 inv => pk.mod_le(ap, mp, d, 1n+r, q)(Equal.trans(Nat, Nat.add(mp, 1n+r), 1n+Nat.add(mp, r), q, UL.nat_add_succ(mp, r), inv))
160
161# a + (1 + q - (a mod (1 + q))) is a multiple of 1 + q
162def pk.mod_pad(+a: Nat, +m: Nat, +d: Nat, +r: Nat, +q: Nat) -> {Nat.add(m, r) == q : Nat} -> {Pair.snd(Nat, Nat, Nat.divmod.go(Nat.add(a, Nat.sub(1n+q, Pair.snd(Nat, Nat, Nat.divmod.go(a, m, d, r)))), m, d, r)) == 0n : Nat}:
163 match a:
164 case 0n:
165 inv => %inv : {Pair.snd(Nat, Nat, Nat.divmod.go(Nat.sub(1n+_, r), m, d, r)) == 0n : Nat}
166 %Equal.sym(Nat, Nat.sub(1n+Nat.add(m, r), r), 1n+m, pk.sub_add_r(m, r)) : {Pair.snd(Nat, Nat, Nat.divmod.go(_, m, d, r)) == 0n : Nat}
167 %UL.nat_add_zero(m) : {Pair.snd(Nat, Nat, Nat.divmod.go(1n+_, m, d, r)) == 0n : Nat}
168 %Equal.sym(Nat & Nat, Nat.divmod.go(1n+Nat.add(m, 0n), m, d, r), Nat.divmod.go(0n, Nat.add(m, r), 1n+d, 0n), pk.go_skip(m, 0n, d, r)) : {Pair.snd(Nat, Nat, _) == 0n : Nat}
169 {==}
170 case 1n+ap:
171 match m:
172 case 0n:
173 inv => pk.mod_pad(ap, r, 1n+d, 0n, q)(Equal.trans(Nat, Nat.add(r, 0n), r, q, UL.nat_add_zero(r), inv))
174 case 1n+mp:
175 inv => pk.mod_pad(ap, mp, d, 1n+r, q)(Equal.trans(Nat, Nat.add(mp, 1n+r), 1n+Nat.add(mp, r), q, UL.nat_add_succ(mp, r), inv))
176
177# The padding bytes
178
179def pk.fill_len(+n: Nat, +v: U32) -> {B.len(P.pkcs7.fill(n, v)) == n : Nat}:
180 match n:
181 case 0n:
182 {==}
183 case 1n+p:
184 %pk.fill_len(p, v) : {1n+B.len(P.pkcs7.fill(p, v)) == 1n+_ : Nat}
185 {==}
186
187def pk.mask_fill(+n: Nat, +v: U32) -> {B.mask(P.pkcs7.fill(n, v)) == P.pkcs7.fill(n, B.byte(v)) : List<&2, U32>}:
188 match n:
189 case 0n:
190 {==}
191 case 1n+p:
192 %pk.mask_fill(p, v) : {Con{B.byte(v), B.mask(P.pkcs7.fill(p, v))} == Con{B.byte(v), _} : List<&2, U32>}
193 {==}
194
195def pk.drop_fill(+k: Nat, +v: U32) -> {B.drop(k, P.pkcs7.fill(1n+k, v)) == Con{v, Nil{}} : List<&2, U32>}:
196 match k:
197 case 0n:
198 {==}
199 case 1n+kp:
200 pk.drop_fill(kp, v)
201
202# BEGIN GENERATED by gen/pkcs7_proof.py: bits
203# a byte's byte is itself
204def pk.bb(u: U32) -> {B.byte(B.byte(u)) == B.byte(u) : U32}:
205 match u:
206 case U32{WCon{u0, WCon{u1, WCon{u2, WCon{u3, WCon{u4, WCon{u5, WCon{u6, WCon{u7, WCon{u8, WCon{u9, WCon{u10, WCon{u11, WCon{u12, WCon{u13, WCon{u14, WCon{u15, WCon{u16, WCon{u17, WCon{u18, WCon{u19, WCon{u20, WCon{u21, WCon{u22, WCon{u23, WCon{u24, WCon{u25, WCon{u26, WCon{u27, WCon{u28, WCon{u29, WCon{u30, WCon{u31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
207 {==}
208# END GENERATED: bits
209
210# a word XOR itself is zero, bit by bit
211def pk.wself(+n: Nat, w: Word(n)) -> {Word.xor(n, w, w) == Word.zero(n) : Word(n)}:
212 match n:
213 case 0n:
214 match w:
215 case WNil{}:
216 {==}
217 case 1n+p:
218 match w:
219 case WCon{h, t}:
220 match h:
221 case False{}:
222 %pk.wself(p, t) : {WCon{False{}, Word.xor(p, t, t)} == WCon{False{}, _} : Word(1n+p)}
223 {==}
224 case True{}:
225 %pk.wself(p, t) : {WCon{False{}, Word.xor(p, t, t)} == WCon{False{}, _} : Word(1n+p)}
226 {==}
227
228def pk.xor_self(+a: U32) -> {U32.xor(a, a) == 0 : U32}:
229 match a:
230 case U32{x}:
231 %Equal.sym(Word(32n), Word.xor(32n, x, x), Word.zero(32n), pk.wself(32n, x)) : {U32{_} == 0 : U32}
232 {==}
233
234# the padding's difference from its own byte is 0
235def pk.diff_fill(+n: Nat, +u: U32) -> {P.pkcs7.diff(P.pkcs7.fill(n, B.byte(u)), B.byte(u), 0) == 0 : U32}:
236 match n:
237 case 0n:
238 {==}
239 case 1n+p:
240 %Equal.sym(U32, B.byte(B.byte(u)), B.byte(u), pk.bb(u)) : {P.pkcs7.diff(P.pkcs7.fill(p, B.byte(u)), B.byte(u), U32.or(0, U32.xor(_, B.byte(u)))) == 0 : U32}
241 %Equal.sym(U32, U32.xor(B.byte(u), B.byte(u)), 0, pk.xor_self(B.byte(u))) : {P.pkcs7.diff(P.pkcs7.fill(p, B.byte(u)), B.byte(u), U32.or(0, _)) == 0 : U32}
242 pk.diff_fill(p, u)
243
244# BEGIN GENERATED by gen/pkcs7_proof.py: u8
245# the values 224 to 255
246def pk.u8.c7(r: Nat) -> {Nat.is_le(224n+r, 255n) == True{} : Bool} -> {U32.to_nat(B.byte(U32.from_nat(224n+r))) == 224n+r : Nat}:
247 match r:
248 case 0n:
249 h => {==}
250 case 1n+r1:
251 match r1:
252 case 0n:
253 h => {==}
254 case 1n+r2:
255 match r2:
256 case 0n:
257 h => {==}
258 case 1n+r3:
259 match r3:
260 case 0n:
261 h => {==}
262 case 1n+r4:
263 match r4:
264 case 0n:
265 h => {==}
266 case 1n+r5:
267 match r5:
268 case 0n:
269 h => {==}
270 case 1n+r6:
271 match r6:
272 case 0n:
273 h => {==}
274 case 1n+r7:
275 match r7:
276 case 0n:
277 h => {==}
278 case 1n+r8:
279 match r8:
280 case 0n:
281 h => {==}
282 case 1n+r9:
283 match r9:
284 case 0n:
285 h => {==}
286 case 1n+r10:
287 match r10:
288 case 0n:
289 h => {==}
290 case 1n+r11:
291 match r11:
292 case 0n:
293 h => {==}
294 case 1n+r12:
295 match r12:
296 case 0n:
297 h => {==}
298 case 1n+r13:
299 match r13:
300 case 0n:
301 h => {==}
302 case 1n+r14:
303 match r14:
304 case 0n:
305 h => {==}
306 case 1n+r15:
307 match r15:
308 case 0n:
309 h => {==}
310 case 1n+r16:
311 match r16:
312 case 0n:
313 h => {==}
314 case 1n+r17:
315 match r17:
316 case 0n:
317 h => {==}
318 case 1n+r18:
319 match r18:
320 case 0n:
321 h => {==}
322 case 1n+r19:
323 match r19:
324 case 0n:
325 h => {==}
326 case 1n+r20:
327 match r20:
328 case 0n:
329 h => {==}
330 case 1n+r21:
331 match r21:
332 case 0n:
333 h => {==}
334 case 1n+r22:
335 match r22:
336 case 0n:
337 h => {==}
338 case 1n+r23:
339 match r23:
340 case 0n:
341 h => {==}
342 case 1n+r24:
343 match r24:
344 case 0n:
345 h => {==}
346 case 1n+r25:
347 match r25:
348 case 0n:
349 h => {==}
350 case 1n+r26:
351 match r26:
352 case 0n:
353 h => {==}
354 case 1n+r27:
355 match r27:
356 case 0n:
357 h => {==}
358 case 1n+r28:
359 match r28:
360 case 0n:
361 h => {==}
362 case 1n+r29:
363 match r29:
364 case 0n:
365 h => {==}
366 case 1n+r30:
367 match r30:
368 case 0n:
369 h => {==}
370 case 1n+r31:
371 match r31:
372 case 0n:
373 h => {==}
374 case 1n+r32:
375 h => pk.absurd({U32.to_nat(B.byte(U32.from_nat(256n+r32))) == 256n+r32 : Nat}, h)
376
377# the values 192 to 223
378def pk.u8.c6(r: Nat) -> {Nat.is_le(192n+r, 255n) == True{} : Bool} -> {U32.to_nat(B.byte(U32.from_nat(192n+r))) == 192n+r : Nat}:
379 match r:
380 case 0n:
381 h => {==}
382 case 1n+r1:
383 match r1:
384 case 0n:
385 h => {==}
386 case 1n+r2:
387 match r2:
388 case 0n:
389 h => {==}
390 case 1n+r3:
391 match r3:
392 case 0n:
393 h => {==}
394 case 1n+r4:
395 match r4:
396 case 0n:
397 h => {==}
398 case 1n+r5:
399 match r5:
400 case 0n:
401 h => {==}
402 case 1n+r6:
403 match r6:
404 case 0n:
405 h => {==}
406 case 1n+r7:
407 match r7:
408 case 0n:
409 h => {==}
410 case 1n+r8:
411 match r8:
412 case 0n:
413 h => {==}
414 case 1n+r9:
415 match r9:
416 case 0n:
417 h => {==}
418 case 1n+r10:
419 match r10:
420 case 0n:
421 h => {==}
422 case 1n+r11:
423 match r11:
424 case 0n:
425 h => {==}
426 case 1n+r12:
427 match r12:
428 case 0n:
429 h => {==}
430 case 1n+r13:
431 match r13:
432 case 0n:
433 h => {==}
434 case 1n+r14:
435 match r14:
436 case 0n:
437 h => {==}
438 case 1n+r15:
439 match r15:
440 case 0n:
441 h => {==}
442 case 1n+r16:
443 match r16:
444 case 0n:
445 h => {==}
446 case 1n+r17:
447 match r17:
448 case 0n:
449 h => {==}
450 case 1n+r18:
451 match r18:
452 case 0n:
453 h => {==}
454 case 1n+r19:
455 match r19:
456 case 0n:
457 h => {==}
458 case 1n+r20:
459 match r20:
460 case 0n:
461 h => {==}
462 case 1n+r21:
463 match r21:
464 case 0n:
465 h => {==}
466 case 1n+r22:
467 match r22:
468 case 0n:
469 h => {==}
470 case 1n+r23:
471 match r23:
472 case 0n:
473 h => {==}
474 case 1n+r24:
475 match r24:
476 case 0n:
477 h => {==}
478 case 1n+r25:
479 match r25:
480 case 0n:
481 h => {==}
482 case 1n+r26:
483 match r26:
484 case 0n:
485 h => {==}
486 case 1n+r27:
487 match r27:
488 case 0n:
489 h => {==}
490 case 1n+r28:
491 match r28:
492 case 0n:
493 h => {==}
494 case 1n+r29:
495 match r29:
496 case 0n:
497 h => {==}
498 case 1n+r30:
499 match r30:
500 case 0n:
501 h => {==}
502 case 1n+r31:
503 match r31:
504 case 0n:
505 h => {==}
506 case 1n+r32:
507 pk.u8.c7(r32)
508
509# the values 160 to 191
510def pk.u8.c5(r: Nat) -> {Nat.is_le(160n+r, 255n) == True{} : Bool} -> {U32.to_nat(B.byte(U32.from_nat(160n+r))) == 160n+r : Nat}:
511 match r:
512 case 0n:
513 h => {==}
514 case 1n+r1:
515 match r1:
516 case 0n:
517 h => {==}
518 case 1n+r2:
519 match r2:
520 case 0n:
521 h => {==}
522 case 1n+r3:
523 match r3:
524 case 0n:
525 h => {==}
526 case 1n+r4:
527 match r4:
528 case 0n:
529 h => {==}
530 case 1n+r5:
531 match r5:
532 case 0n:
533 h => {==}
534 case 1n+r6:
535 match r6:
536 case 0n:
537 h => {==}
538 case 1n+r7:
539 match r7:
540 case 0n:
541 h => {==}
542 case 1n+r8:
543 match r8:
544 case 0n:
545 h => {==}
546 case 1n+r9:
547 match r9:
548 case 0n:
549 h => {==}
550 case 1n+r10:
551 match r10:
552 case 0n:
553 h => {==}
554 case 1n+r11:
555 match r11:
556 case 0n:
557 h => {==}
558 case 1n+r12:
559 match r12:
560 case 0n:
561 h => {==}
562 case 1n+r13:
563 match r13:
564 case 0n:
565 h => {==}
566 case 1n+r14:
567 match r14:
568 case 0n:
569 h => {==}
570 case 1n+r15:
571 match r15:
572 case 0n:
573 h => {==}
574 case 1n+r16:
575 match r16:
576 case 0n:
577 h => {==}
578 case 1n+r17:
579 match r17:
580 case 0n:
581 h => {==}
582 case 1n+r18:
583 match r18:
584 case 0n:
585 h => {==}
586 case 1n+r19:
587 match r19:
588 case 0n:
589 h => {==}
590 case 1n+r20:
591 match r20:
592 case 0n:
593 h => {==}
594 case 1n+r21:
595 match r21:
596 case 0n:
597 h => {==}
598 case 1n+r22:
599 match r22:
600 case 0n:
601 h => {==}
602 case 1n+r23:
603 match r23:
604 case 0n:
605 h => {==}
606 case 1n+r24:
607 match r24:
608 case 0n:
609 h => {==}
610 case 1n+r25:
611 match r25:
612 case 0n:
613 h => {==}
614 case 1n+r26:
615 match r26:
616 case 0n:
617 h => {==}
618 case 1n+r27:
619 match r27:
620 case 0n:
621 h => {==}
622 case 1n+r28:
623 match r28:
624 case 0n:
625 h => {==}
626 case 1n+r29:
627 match r29:
628 case 0n:
629 h => {==}
630 case 1n+r30:
631 match r30:
632 case 0n:
633 h => {==}
634 case 1n+r31:
635 match r31:
636 case 0n:
637 h => {==}
638 case 1n+r32:
639 pk.u8.c6(r32)
640
641# the values 128 to 159
642def pk.u8.c4(r: Nat) -> {Nat.is_le(128n+r, 255n) == True{} : Bool} -> {U32.to_nat(B.byte(U32.from_nat(128n+r))) == 128n+r : Nat}:
643 match r:
644 case 0n:
645 h => {==}
646 case 1n+r1:
647 match r1:
648 case 0n:
649 h => {==}
650 case 1n+r2:
651 match r2:
652 case 0n:
653 h => {==}
654 case 1n+r3:
655 match r3:
656 case 0n:
657 h => {==}
658 case 1n+r4:
659 match r4:
660 case 0n:
661 h => {==}
662 case 1n+r5:
663 match r5:
664 case 0n:
665 h => {==}
666 case 1n+r6:
667 match r6:
668 case 0n:
669 h => {==}
670 case 1n+r7:
671 match r7:
672 case 0n:
673 h => {==}
674 case 1n+r8:
675 match r8:
676 case 0n:
677 h => {==}
678 case 1n+r9:
679 match r9:
680 case 0n:
681 h => {==}
682 case 1n+r10:
683 match r10:
684 case 0n:
685 h => {==}
686 case 1n+r11:
687 match r11:
688 case 0n:
689 h => {==}
690 case 1n+r12:
691 match r12:
692 case 0n:
693 h => {==}
694 case 1n+r13:
695 match r13:
696 case 0n:
697 h => {==}
698 case 1n+r14:
699 match r14:
700 case 0n:
701 h => {==}
702 case 1n+r15:
703 match r15:
704 case 0n:
705 h => {==}
706 case 1n+r16:
707 match r16:
708 case 0n:
709 h => {==}
710 case 1n+r17:
711 match r17:
712 case 0n:
713 h => {==}
714 case 1n+r18:
715 match r18:
716 case 0n:
717 h => {==}
718 case 1n+r19:
719 match r19:
720 case 0n:
721 h => {==}
722 case 1n+r20:
723 match r20:
724 case 0n:
725 h => {==}
726 case 1n+r21:
727 match r21:
728 case 0n:
729 h => {==}
730 case 1n+r22:
731 match r22:
732 case 0n:
733 h => {==}
734 case 1n+r23:
735 match r23:
736 case 0n:
737 h => {==}
738 case 1n+r24:
739 match r24:
740 case 0n:
741 h => {==}
742 case 1n+r25:
743 match r25:
744 case 0n:
745 h => {==}
746 case 1n+r26:
747 match r26:
748 case 0n:
749 h => {==}
750 case 1n+r27:
751 match r27:
752 case 0n:
753 h => {==}
754 case 1n+r28:
755 match r28:
756 case 0n:
757 h => {==}
758 case 1n+r29:
759 match r29:
760 case 0n:
761 h => {==}
762 case 1n+r30:
763 match r30:
764 case 0n:
765 h => {==}
766 case 1n+r31:
767 match r31:
768 case 0n:
769 h => {==}
770 case 1n+r32:
771 pk.u8.c5(r32)
772
773# the values 96 to 127
774def pk.u8.c3(r: Nat) -> {Nat.is_le(96n+r, 255n) == True{} : Bool} -> {U32.to_nat(B.byte(U32.from_nat(96n+r))) == 96n+r : Nat}:
775 match r:
776 case 0n:
777 h => {==}
778 case 1n+r1:
779 match r1:
780 case 0n:
781 h => {==}
782 case 1n+r2:
783 match r2:
784 case 0n:
785 h => {==}
786 case 1n+r3:
787 match r3:
788 case 0n:
789 h => {==}
790 case 1n+r4:
791 match r4:
792 case 0n:
793 h => {==}
794 case 1n+r5:
795 match r5:
796 case 0n:
797 h => {==}
798 case 1n+r6:
799 match r6:
800 case 0n:
801 h => {==}
802 case 1n+r7:
803 match r7:
804 case 0n:
805 h => {==}
806 case 1n+r8:
807 match r8:
808 case 0n:
809 h => {==}
810 case 1n+r9:
811 match r9:
812 case 0n:
813 h => {==}
814 case 1n+r10:
815 match r10:
816 case 0n:
817 h => {==}
818 case 1n+r11:
819 match r11:
820 case 0n:
821 h => {==}
822 case 1n+r12:
823 match r12:
824 case 0n:
825 h => {==}
826 case 1n+r13:
827 match r13:
828 case 0n:
829 h => {==}
830 case 1n+r14:
831 match r14:
832 case 0n:
833 h => {==}
834 case 1n+r15:
835 match r15:
836 case 0n:
837 h => {==}
838 case 1n+r16:
839 match r16:
840 case 0n:
841 h => {==}
842 case 1n+r17:
843 match r17:
844 case 0n:
845 h => {==}
846 case 1n+r18:
847 match r18:
848 case 0n:
849 h => {==}
850 case 1n+r19:
851 match r19:
852 case 0n:
853 h => {==}
854 case 1n+r20:
855 match r20:
856 case 0n:
857 h => {==}
858 case 1n+r21:
859 match r21:
860 case 0n:
861 h => {==}
862 case 1n+r22:
863 match r22:
864 case 0n:
865 h => {==}
866 case 1n+r23:
867 match r23:
868 case 0n:
869 h => {==}
870 case 1n+r24:
871 match r24:
872 case 0n:
873 h => {==}
874 case 1n+r25:
875 match r25:
876 case 0n:
877 h => {==}
878 case 1n+r26:
879 match r26:
880 case 0n:
881 h => {==}
882 case 1n+r27:
883 match r27:
884 case 0n:
885 h => {==}
886 case 1n+r28:
887 match r28:
888 case 0n:
889 h => {==}
890 case 1n+r29:
891 match r29:
892 case 0n:
893 h => {==}
894 case 1n+r30:
895 match r30:
896 case 0n:
897 h => {==}
898 case 1n+r31:
899 match r31:
900 case 0n:
901 h => {==}
902 case 1n+r32:
903 pk.u8.c4(r32)
904
905# the values 64 to 95
906def pk.u8.c2(r: Nat) -> {Nat.is_le(64n+r, 255n) == True{} : Bool} -> {U32.to_nat(B.byte(U32.from_nat(64n+r))) == 64n+r : Nat}:
907 match r:
908 case 0n:
909 h => {==}
910 case 1n+r1:
911 match r1:
912 case 0n:
913 h => {==}
914 case 1n+r2:
915 match r2:
916 case 0n:
917 h => {==}
918 case 1n+r3:
919 match r3:
920 case 0n:
921 h => {==}
922 case 1n+r4:
923 match r4:
924 case 0n:
925 h => {==}
926 case 1n+r5:
927 match r5:
928 case 0n:
929 h => {==}
930 case 1n+r6:
931 match r6:
932 case 0n:
933 h => {==}
934 case 1n+r7:
935 match r7:
936 case 0n:
937 h => {==}
938 case 1n+r8:
939 match r8:
940 case 0n:
941 h => {==}
942 case 1n+r9:
943 match r9:
944 case 0n:
945 h => {==}
946 case 1n+r10:
947 match r10:
948 case 0n:
949 h => {==}
950 case 1n+r11:
951 match r11:
952 case 0n:
953 h => {==}
954 case 1n+r12:
955 match r12:
956 case 0n:
957 h => {==}
958 case 1n+r13:
959 match r13:
960 case 0n:
961 h => {==}
962 case 1n+r14:
963 match r14:
964 case 0n:
965 h => {==}
966 case 1n+r15:
967 match r15:
968 case 0n:
969 h => {==}
970 case 1n+r16:
971 match r16:
972 case 0n:
973 h => {==}
974 case 1n+r17:
975 match r17:
976 case 0n:
977 h => {==}
978 case 1n+r18:
979 match r18:
980 case 0n:
981 h => {==}
982 case 1n+r19:
983 match r19:
984 case 0n:
985 h => {==}
986 case 1n+r20:
987 match r20:
988 case 0n:
989 h => {==}
990 case 1n+r21:
991 match r21:
992 case 0n:
993 h => {==}
994 case 1n+r22:
995 match r22:
996 case 0n:
997 h => {==}
998 case 1n+r23:
999 match r23:
1000 case 0n:
1001 h => {==}
1002 case 1n+r24:
1003 match r24:
1004 case 0n:
1005 h => {==}
1006 case 1n+r25:
1007 match r25:
1008 case 0n:
1009 h => {==}
1010 case 1n+r26:
1011 match r26:
1012 case 0n:
1013 h => {==}
1014 case 1n+r27:
1015 match r27:
1016 case 0n:
1017 h => {==}
1018 case 1n+r28:
1019 match r28:
1020 case 0n:
1021 h => {==}
1022 case 1n+r29:
1023 match r29:
1024 case 0n:
1025 h => {==}
1026 case 1n+r30:
1027 match r30:
1028 case 0n:
1029 h => {==}
1030 case 1n+r31:
1031 match r31:
1032 case 0n:
1033 h => {==}
1034 case 1n+r32:
1035 pk.u8.c3(r32)
1036
1037# the values 32 to 63
1038def pk.u8.c1(r: Nat) -> {Nat.is_le(32n+r, 255n) == True{} : Bool} -> {U32.to_nat(B.byte(U32.from_nat(32n+r))) == 32n+r : Nat}:
1039 match r:
1040 case 0n:
1041 h => {==}
1042 case 1n+r1:
1043 match r1:
1044 case 0n:
1045 h => {==}
1046 case 1n+r2:
1047 match r2:
1048 case 0n:
1049 h => {==}
1050 case 1n+r3:
1051 match r3:
1052 case 0n:
1053 h => {==}
1054 case 1n+r4:
1055 match r4:
1056 case 0n:
1057 h => {==}
1058 case 1n+r5:
1059 match r5:
1060 case 0n:
1061 h => {==}
1062 case 1n+r6:
1063 match r6:
1064 case 0n:
1065 h => {==}
1066 case 1n+r7:
1067 match r7:
1068 case 0n:
1069 h => {==}
1070 case 1n+r8:
1071 match r8:
1072 case 0n:
1073 h => {==}
1074 case 1n+r9:
1075 match r9:
1076 case 0n:
1077 h => {==}
1078 case 1n+r10:
1079 match r10:
1080 case 0n:
1081 h => {==}
1082 case 1n+r11:
1083 match r11:
1084 case 0n:
1085 h => {==}
1086 case 1n+r12:
1087 match r12:
1088 case 0n:
1089 h => {==}
1090 case 1n+r13:
1091 match r13:
1092 case 0n:
1093 h => {==}
1094 case 1n+r14:
1095 match r14:
1096 case 0n:
1097 h => {==}
1098 case 1n+r15:
1099 match r15:
1100 case 0n:
1101 h => {==}
1102 case 1n+r16:
1103 match r16:
1104 case 0n:
1105 h => {==}
1106 case 1n+r17:
1107 match r17:
1108 case 0n:
1109 h => {==}
1110 case 1n+r18:
1111 match r18:
1112 case 0n:
1113 h => {==}
1114 case 1n+r19:
1115 match r19:
1116 case 0n:
1117 h => {==}
1118 case 1n+r20:
1119 match r20:
1120 case 0n:
1121 h => {==}
1122 case 1n+r21:
1123 match r21:
1124 case 0n:
1125 h => {==}
1126 case 1n+r22:
1127 match r22:
1128 case 0n:
1129 h => {==}
1130 case 1n+r23:
1131 match r23:
1132 case 0n:
1133 h => {==}
1134 case 1n+r24:
1135 match r24:
1136 case 0n:
1137 h => {==}
1138 case 1n+r25:
1139 match r25:
1140 case 0n:
1141 h => {==}
1142 case 1n+r26:
1143 match r26:
1144 case 0n:
1145 h => {==}
1146 case 1n+r27:
1147 match r27:
1148 case 0n:
1149 h => {==}
1150 case 1n+r28:
1151 match r28:
1152 case 0n:
1153 h => {==}
1154 case 1n+r29:
1155 match r29:
1156 case 0n:
1157 h => {==}
1158 case 1n+r30:
1159 match r30:
1160 case 0n:
1161 h => {==}
1162 case 1n+r31:
1163 match r31:
1164 case 0n:
1165 h => {==}
1166 case 1n+r32:
1167 pk.u8.c2(r32)
1168
1169# the values 0 to 31
1170def pk.u8(r: Nat) -> {Nat.is_le(r, 255n) == True{} : Bool} -> {U32.to_nat(B.byte(U32.from_nat(r))) == r : Nat}:
1171 match r:
1172 case 0n:
1173 h => {==}
1174 case 1n+r1:
1175 match r1:
1176 case 0n:
1177 h => {==}
1178 case 1n+r2:
1179 match r2:
1180 case 0n:
1181 h => {==}
1182 case 1n+r3:
1183 match r3:
1184 case 0n:
1185 h => {==}
1186 case 1n+r4:
1187 match r4:
1188 case 0n:
1189 h => {==}
1190 case 1n+r5:
1191 match r5:
1192 case 0n:
1193 h => {==}
1194 case 1n+r6:
1195 match r6:
1196 case 0n:
1197 h => {==}
1198 case 1n+r7:
1199 match r7:
1200 case 0n:
1201 h => {==}
1202 case 1n+r8:
1203 match r8:
1204 case 0n:
1205 h => {==}
1206 case 1n+r9:
1207 match r9:
1208 case 0n:
1209 h => {==}
1210 case 1n+r10:
1211 match r10:
1212 case 0n:
1213 h => {==}
1214 case 1n+r11:
1215 match r11:
1216 case 0n:
1217 h => {==}
1218 case 1n+r12:
1219 match r12:
1220 case 0n:
1221 h => {==}
1222 case 1n+r13:
1223 match r13:
1224 case 0n:
1225 h => {==}
1226 case 1n+r14:
1227 match r14:
1228 case 0n:
1229 h => {==}
1230 case 1n+r15:
1231 match r15:
1232 case 0n:
1233 h => {==}
1234 case 1n+r16:
1235 match r16:
1236 case 0n:
1237 h => {==}
1238 case 1n+r17:
1239 match r17:
1240 case 0n:
1241 h => {==}
1242 case 1n+r18:
1243 match r18:
1244 case 0n:
1245 h => {==}
1246 case 1n+r19:
1247 match r19:
1248 case 0n:
1249 h => {==}
1250 case 1n+r20:
1251 match r20:
1252 case 0n:
1253 h => {==}
1254 case 1n+r21:
1255 match r21:
1256 case 0n:
1257 h => {==}
1258 case 1n+r22:
1259 match r22:
1260 case 0n:
1261 h => {==}
1262 case 1n+r23:
1263 match r23:
1264 case 0n:
1265 h => {==}
1266 case 1n+r24:
1267 match r24:
1268 case 0n:
1269 h => {==}
1270 case 1n+r25:
1271 match r25:
1272 case 0n:
1273 h => {==}
1274 case 1n+r26:
1275 match r26:
1276 case 0n:
1277 h => {==}
1278 case 1n+r27:
1279 match r27:
1280 case 0n:
1281 h => {==}
1282 case 1n+r28:
1283 match r28:
1284 case 0n:
1285 h => {==}
1286 case 1n+r29:
1287 match r29:
1288 case 0n:
1289 h => {==}
1290 case 1n+r30:
1291 match r30:
1292 case 0n:
1293 h => {==}
1294 case 1n+r31:
1295 match r31:
1296 case 0n:
1297 h => {==}
1298 case 1n+r32:
1299 pk.u8.c1(r32)
1300# END GENERATED: u8
1301
1302# The round trip
1303
1304# Pkcs7.unpad's checks and its unpad.oct, with what they compute as
1305# arguments, so that each can be rewritten on its own
1306def pk.ug(+bs: Nat, +m: B.Octets, +n: Nat, +md: Nat) -> Result<&2, &2, M.CmError, B.Octets>:
1307 do Result<&2, &2, M.CmError, B.Octets>:
1308 M.cm.check(Nat.is_lt(0n, n), M.CmTooShort{n})
1309 M.cm.check(Nat.is_eq(md, 0n), M.CmNotBlockMultiple{n})
1310 P.pkcs7.unpad.oct(bs, m, n)
1311
1312def pk.k2(+bs: Nat, +m: B.Octets, +n: Nat, +p: Nat, le: Bool, +d: U32) -> Result<&2, &2, M.CmError, B.Octets>:
1313 P.pkcs7.strip(Bool.and(Nat.is_lt(0n, p), Bool.and(le, U32.is_eq(d, 0))), n, p, m)
1314
1315def pk.k(+bs: Nat, +m: B.Octets, +n: Nat, +v: U32, +p: Nat) -> Result<&2, &2, M.CmError, B.Octets>:
1316 pk.k2(bs, m, n, p, Nat.is_le(p, bs), P.pkcs7.diff(B.Octets.to_list(B.Octets.drop(Nat.sub(n, p), m)), v, 0))
1317
1318# the padding of 1 + p1 bytes
1319def pk.pad(+p1: Nat) -> B.Octets:
1320 B.Octets.of_list(P.pkcs7.fill(1n+p1, U32.from_nat(1n+p1)))
1321
1322# its last byte, at L + p1 of m and it
1323def pk.at(+m: B.Octets, +p1: Nat) -> {B.Octets.at(B.Octets.append(m, pk.pad(p1)), Nat.add(B.Octets.len(m), p1)) == Some{B.byte(U32.from_nat(1n+p1))} : Maybe<&2, U32>}:
1324 %Equal.sym(Maybe<&2, U32>, B.Octets.at(B.Octets.append(m, pk.pad(p1)), Nat.add(B.Octets.len(m), p1)), B.Octets.at(pk.pad(p1), p1), BL.octets_at_append_add(m, pk.pad(p1), p1)) : {_ == Some{B.byte(U32.from_nat(1n+p1))} : Maybe<&2, U32>}
1325 %Equal.sym(Maybe<&2, U32>, B.Octets.at(pk.pad(p1), p1), B.at(B.Octets.to_list(pk.pad(p1)), p1), BL.octets_at_list(pk.pad(p1), p1)) : {_ == Some{B.byte(U32.from_nat(1n+p1))} : Maybe<&2, U32>}
1326 %Equal.sym(List<&2, U32>, B.Octets.to_list(pk.pad(p1)), B.mask(P.pkcs7.fill(1n+p1, U32.from_nat(1n+p1))), BL.octets_to_of(P.pkcs7.fill(1n+p1, U32.from_nat(1n+p1)))) : {B.at(_, p1) == Some{B.byte(U32.from_nat(1n+p1))} : Maybe<&2, U32>}
1327 %Equal.sym(List<&2, U32>, B.mask(P.pkcs7.fill(1n+p1, U32.from_nat(1n+p1))), P.pkcs7.fill(1n+p1, B.byte(U32.from_nat(1n+p1))), pk.mask_fill(1n+p1, U32.from_nat(1n+p1))) : {B.at(_, p1) == Some{B.byte(U32.from_nat(1n+p1))} : Maybe<&2, U32>}
1328 %Equal.sym(List<&2, U32>, B.drop(p1, P.pkcs7.fill(1n+p1, B.byte(U32.from_nat(1n+p1)))), Con{B.byte(U32.from_nat(1n+p1)), Nil{}}, pk.drop_fill(p1, B.byte(U32.from_nat(1n+p1)))) : {B.at.head(_) == Some{B.byte(U32.from_nat(1n+p1))} : Maybe<&2, U32>}
1329 %pk.bb(U32.from_nat(1n+p1)) : {Some{B.byte(B.byte(U32.from_nat(1n+p1)))} == Some{_} : Maybe<&2, U32>}
1330 {==}
1331
1332# the padded message's length
1333def pk.len(+m: B.Octets, +p1: Nat) -> {B.Octets.len(B.Octets.append(m, pk.pad(p1))) == 1n+Nat.add(B.Octets.len(m), p1) : Nat}:
1334 %Equal.sym(Nat, B.Octets.len(B.Octets.append(m, pk.pad(p1))), Nat.add(B.Octets.len(m), B.Octets.len(pk.pad(p1))), BL.octets_len_append(m, pk.pad(p1))) : {_ == 1n+Nat.add(B.Octets.len(m), p1) : Nat}
1335 %Equal.sym(Nat, B.Octets.len(pk.pad(p1)), B.len(P.pkcs7.fill(1n+p1, U32.from_nat(1n+p1))), BL.octets_len_of_list(P.pkcs7.fill(1n+p1, U32.from_nat(1n+p1)))) : {Nat.add(B.Octets.len(m), _) == 1n+Nat.add(B.Octets.len(m), p1) : Nat}
1336 %Equal.sym(Nat, B.len(P.pkcs7.fill(1n+p1, U32.from_nat(1n+p1))), 1n+p1, pk.fill_len(1n+p1, U32.from_nat(1n+p1))) : {Nat.add(B.Octets.len(m), _) == 1n+Nat.add(B.Octets.len(m), p1) : Nat}
1337 UL.nat_add_succ(B.Octets.len(m), p1)
1338
1339# unpad.oct on m and a padding of 1 + p1 bytes (p1 below 255) gives m
1340def pk.oct(+bs: Nat, +m: B.Octets, +p1: Nat, hle: {Nat.is_le(1n+p1, bs) == True{} : Bool}, hb: {Nat.is_le(1n+p1, 255n) == True{} : Bool}) -> {P.pkcs7.unpad.oct(bs, B.Octets.append(m, pk.pad(p1)), 1n+Nat.add(B.Octets.len(m), p1)) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}:
1341 +el = pk.add_sub(B.Octets.len(m), p1)
1342 # the last byte is the byte of 1 + p1
1343 %Equal.sym(Nat, Nat.sub(Nat.add(B.Octets.len(m), p1), 0n), Nat.add(B.Octets.len(m), p1), pk.sub_zero(Nat.add(B.Octets.len(m), p1))) : {pk.k(bs, B.Octets.append(m, pk.pad(p1)), 1n+Nat.add(B.Octets.len(m), p1), P.pkcs7.last(B.Octets.at(B.Octets.append(m, pk.pad(p1)), _), 0), U32.to_nat(P.pkcs7.last(B.Octets.at(B.Octets.append(m, pk.pad(p1)), _), 0))) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
1344 %Equal.sym(Maybe<&2, U32>, B.Octets.at(B.Octets.append(m, pk.pad(p1)), Nat.add(B.Octets.len(m), p1)), Some{B.byte(U32.from_nat(1n+p1))}, pk.at(m, p1)) : {pk.k(bs, B.Octets.append(m, pk.pad(p1)), 1n+Nat.add(B.Octets.len(m), p1), P.pkcs7.last(_, 0), U32.to_nat(P.pkcs7.last(_, 0))) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
1345 # whose value is 1 + p1
1346 %Equal.sym(Nat, U32.to_nat(B.byte(U32.from_nat(1n+p1))), 1n+p1, pk.u8(1n+p1)(hb)) : {pk.k(bs, B.Octets.append(m, pk.pad(p1)), 1n+Nat.add(B.Octets.len(m), p1), B.byte(U32.from_nat(1n+p1)), _) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
1347 # at most the block size
1348 %Equal.sym(Bool, Nat.is_le(1n+p1, bs), True{}, hle) : {pk.k2(bs, B.Octets.append(m, pk.pad(p1)), 1n+Nat.add(B.Octets.len(m), p1), 1n+p1, _, P.pkcs7.diff(B.Octets.to_list(B.Octets.drop(Nat.sub(Nat.add(B.Octets.len(m), p1), p1), B.Octets.append(m, pk.pad(p1)))), B.byte(U32.from_nat(1n+p1)), 0)) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
1349 # the last 1 + p1 bytes are the padding
1350 %Equal.sym(Nat, Nat.sub(Nat.add(B.Octets.len(m), p1), p1), B.Octets.len(m), el) : {pk.k2(bs, B.Octets.append(m, pk.pad(p1)), 1n+Nat.add(B.Octets.len(m), p1), 1n+p1, True{}, P.pkcs7.diff(B.Octets.to_list(B.Octets.drop(_, B.Octets.append(m, pk.pad(p1)))), B.byte(U32.from_nat(1n+p1)), 0)) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
1351 %Equal.sym(B.Octets, B.Octets.drop(B.Octets.len(m), B.Octets.append(m, pk.pad(p1))), pk.pad(p1), BL.octets_drop_append(m, pk.pad(p1))) : {pk.k2(bs, B.Octets.append(m, pk.pad(p1)), 1n+Nat.add(B.Octets.len(m), p1), 1n+p1, True{}, P.pkcs7.diff(B.Octets.to_list(_), B.byte(U32.from_nat(1n+p1)), 0)) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
1352 %Equal.sym(List<&2, U32>, B.Octets.to_list(pk.pad(p1)), B.mask(P.pkcs7.fill(1n+p1, U32.from_nat(1n+p1))), BL.octets_to_of(P.pkcs7.fill(1n+p1, U32.from_nat(1n+p1)))) : {pk.k2(bs, B.Octets.append(m, pk.pad(p1)), 1n+Nat.add(B.Octets.len(m), p1), 1n+p1, True{}, P.pkcs7.diff(_, B.byte(U32.from_nat(1n+p1)), 0)) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
1353 %Equal.sym(List<&2, U32>, B.mask(P.pkcs7.fill(1n+p1, U32.from_nat(1n+p1))), P.pkcs7.fill(1n+p1, B.byte(U32.from_nat(1n+p1))), pk.mask_fill(1n+p1, U32.from_nat(1n+p1))) : {pk.k2(bs, B.Octets.append(m, pk.pad(p1)), 1n+Nat.add(B.Octets.len(m), p1), 1n+p1, True{}, P.pkcs7.diff(_, B.byte(U32.from_nat(1n+p1)), 0)) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
1354 # all of them the byte
1355 %Equal.sym(U32, P.pkcs7.diff(P.pkcs7.fill(1n+p1, B.byte(U32.from_nat(1n+p1))), B.byte(U32.from_nat(1n+p1)), 0), 0, pk.diff_fill(1n+p1, U32.from_nat(1n+p1))) : {pk.k2(bs, B.Octets.append(m, pk.pad(p1)), 1n+Nat.add(B.Octets.len(m), p1), 1n+p1, True{}, _) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
1356 # so the first L bytes are kept
1357 %Equal.sym(Nat, Nat.sub(Nat.add(B.Octets.len(m), p1), p1), B.Octets.len(m), el) : {Done{B.Octets.take(_, B.Octets.append(m, pk.pad(p1)))} == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
1358 %Equal.sym(B.Octets, B.Octets.take(B.Octets.len(m), B.Octets.append(m, pk.pad(p1))), m, BL.octets_take_append(m, pk.pad(p1))) : {Done{_} == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
1359 {==}
1360
1361# the round trip for a block size 1 + q (q below 255) and a padding of
1362# 1 + p1 bytes, p1 <= q, that makes whole blocks
1363def pk.main2(+q: Nat, +m: B.Octets, +p1: Nat, +hle: {Nat.is_le(p1, q) == True{} : Bool}, hb: {Nat.is_le(1n+q, 255n) == True{} : Bool}, hm: {Nat.mod(1n+Nat.add(B.Octets.len(m), p1), 1n+q) == 0n : Nat}) -> {P.Pkcs7.unpad.go(True{}, 1n+q, B.Octets.append(m, pk.pad(p1))) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}:
1364 %Equal.sym(Nat, B.Octets.len(B.Octets.append(m, pk.pad(p1))), 1n+Nat.add(B.Octets.len(m), p1), pk.len(m, p1)) : {pk.ug(1n+q, B.Octets.append(m, pk.pad(p1)), _, Nat.mod(_, 1n+q)) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
1365 %Equal.sym(Nat, Nat.mod(1n+Nat.add(B.Octets.len(m), p1), 1n+q), 0n, hm) : {pk.ug(1n+q, B.Octets.append(m, pk.pad(p1)), 1n+Nat.add(B.Octets.len(m), p1), _) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
1366 pk.oct(1n+q, m, p1, hle, pk.le_trans(1n+p1, 1n+q, 255n)(hle)(hb))
1367
1368# 1 + L + (q - L mod (1 + q)) is a multiple of 1 + q
1369def pk.hm(+q: Nat, +m: B.Octets) -> {Nat.mod(1n+Nat.add(B.Octets.len(m), Nat.sub(q, Nat.mod(B.Octets.len(m), 1n+q))), 1n+q) == 0n : Nat}:
1370 +hs = pk.sub_succ(Nat.mod(B.Octets.len(m), 1n+q), q)(pk.mod_le(B.Octets.len(m), q, 0n, 0n, q)(UL.nat_add_zero(q)))
1371 %UL.nat_add_succ(B.Octets.len(m), Nat.sub(q, Nat.mod(B.Octets.len(m), 1n+q))) : {Nat.mod(_, 1n+q) == 0n : Nat}
1372 %hs : {Nat.mod(Nat.add(B.Octets.len(m), _), 1n+q) == 0n : Nat}
1373 pk.mod_pad(B.Octets.len(m), q, 0n, 0n, q)(UL.nat_add_zero(q))
1374
1375def pk.main(+q: Nat, +m: B.Octets, +e: {Nat.is_lt(1n+q, 256n) == True{} : Bool}) -> {P.Pkcs7.unpad(1n+q, P.pkcs7.pad.oct(1n+q, m)) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}:
1376 +hs = pk.sub_succ(Nat.mod(B.Octets.len(m), 1n+q), q)(pk.mod_le(B.Octets.len(m), q, 0n, 0n, q)(UL.nat_add_zero(q)))
1377 # the padding is 1 + (q - L mod (1 + q)) bytes
1378 %Equal.sym(Nat, Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q)), 1n+Nat.sub(q, Nat.mod(B.Octets.len(m), 1n+q)), hs) : {P.Pkcs7.unpad(1n+q, B.Octets.append(m, B.Octets.of_list(P.pkcs7.fill(_, U32.from_nat(_))))) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
1379 # the block size is one the padding takes
1380 %Equal.sym(Bool, Nat.is_lt(1n+q, 256n), True{}, e) : {P.Pkcs7.unpad.go(_, 1n+q, B.Octets.append(m, pk.pad(Nat.sub(q, Nat.mod(B.Octets.len(m), 1n+q))))) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
1381 # and the padded length is a multiple of it (pk.hm)
1382 pk.main2(q, m, Nat.sub(q, Nat.mod(B.Octets.len(m), 1n+q)), pk.le_sub(q, Nat.mod(B.Octets.len(m), 1n+q)), pk.lt_le(1n+q, 255n)(e), pk.hm(q, m))
1383
1384def pk.rt(ok: Bool, +bs: Nat, +m: B.Octets) -> {P.pkcs7.size_ok(bs) == ok : Bool} -> {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, P.Pkcs7.pad.go(ok, bs, m), c => P.Pkcs7.unpad(bs, c)) == Result.map(&2, &2, M.CmError, B.Octets, B.Octets, c => m, P.Pkcs7.pad.go(ok, bs, m)) : Result<&2, &2, M.CmError, B.Octets>}:
1385 match ok:
1386 case False{}:
1387 e => {==}
1388 case True{}:
1389 match bs:
1390 case 0n:
1391 e => pk.absurd({P.Pkcs7.unpad(0n, P.pkcs7.pad.oct(0n, m)) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}, e)
1392 case 1n+q:
1393 e => pk.main(q, m, e)
1394
1395def Laws.pkcs7_round_trip(bs, m):
1396 pk.rt(P.pkcs7.size_ok(bs), bs, m)({==})
1397
1398# Padding gives whole blocks: L + p, p = 1 + q - L mod (1 + q), is a
1399# multiple of 1 + q (pk.mod_pad)
1400
1401def pk.blocks(ok: Bool, +bs: Nat, +m: B.Octets) -> {P.pkcs7.size_ok(bs) == ok : Bool} -> {Result.map(&2, &2, M.CmError, B.Octets, Nat, c => Nat.mod(B.Octets.len(c), bs), P.Pkcs7.pad.go(ok, bs, m)) == Result.map(&2, &2, M.CmError, B.Octets, Nat, c => 0n, P.Pkcs7.pad.go(ok, bs, m)) : Result<&2, &2, M.CmError, Nat>}:
1402 match ok:
1403 case False{}:
1404 e => {==}
1405 case True{}:
1406 match bs:
1407 case 0n:
1408 e => pk.absurd({Done{Nat.mod(B.Octets.len(P.pkcs7.pad.oct(0n, m)), 0n)} == Done{0n} : Result<&2, &2, M.CmError, Nat>}, e)
1409 case 1n+q:
1410 e => %Equal.sym(Nat, B.Octets.len(P.pkcs7.pad.oct(1n+q, m)), Nat.add(B.Octets.len(m), B.Octets.len(B.Octets.of_list(P.pkcs7.fill(Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q)), U32.from_nat(Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q))))))), BL.octets_len_append(m, B.Octets.of_list(P.pkcs7.fill(Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q)), U32.from_nat(Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q))))))) : {Done{Nat.mod(_, 1n+q)} == Done{0n} : Result<&2, &2, M.CmError, Nat>}
1411 %Equal.sym(Nat, B.Octets.len(B.Octets.of_list(P.pkcs7.fill(Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q)), U32.from_nat(Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q)))))), B.len(P.pkcs7.fill(Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q)), U32.from_nat(Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q))))), BL.octets_len_of_list(P.pkcs7.fill(Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q)), U32.from_nat(Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q)))))) : {Done{Nat.mod(Nat.add(B.Octets.len(m), _), 1n+q)} == Done{0n} : Result<&2, &2, M.CmError, Nat>}
1412 %Equal.sym(Nat, B.len(P.pkcs7.fill(Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q)), U32.from_nat(Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q))))), Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q)), pk.fill_len(Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q)), U32.from_nat(Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q))))) : {Done{Nat.mod(Nat.add(B.Octets.len(m), _), 1n+q)} == Done{0n} : Result<&2, &2, M.CmError, Nat>}
1413 %Equal.sym(Nat, Nat.mod(Nat.add(B.Octets.len(m), Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q))), 1n+q), 0n, pk.mod_pad(B.Octets.len(m), q, 0n, 0n, q)(UL.nat_add_zero(q))) : {Done{_} == Done{0n} : Result<&2, &2, M.CmError, Nat>}
1414 {==}
1415
1416def Laws.pkcs7_pad_blocks(bs, m):
1417 pk.blocks(P.pkcs7.size_ok(bs), bs, m)({==})
1418
1419# Vectors
1420
1421def Laws.pkcs7_pad_empty():
1422 {==}
1423
1424def Laws.pkcs7_pad_15():
1425 {==}
1426
1427def Laws.pkcs7_unpad_15():
1428 {==}
1429
1430def Laws.pkcs7_unpad_zero():
1431 {==}
1432
1433def Laws.pkcs7_unpad_mixed():
1434 {==}