forked from yetanotherflower/mm0
-
Notifications
You must be signed in to change notification settings - Fork 1
/
x86.mm1
5047 lines (4505 loc) · 238 KB
/
x86.mm1
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
import "peano_hex.mm1";
@(add-eval @ fn (b n) (def a {(eval n) shl 1}) @ if (eval b) {a + 1} a)
@_ def consBit (b: wff) (n: nat): nat = $ if b (b1 n) (b0 n) $;
@(add-eval @ fn (n i) {{{(eval n) shr (eval i)} band 1} = 1})
@_ def bit (n i: nat): nat = $ nat (i e. n) $;
pub theorem bitT (n i: nat): $ bool (bit n i) $ = 'boolnat;
theorem bit01: $ bit 0 i = 0 $ = '(mpbir nateq0 nel0);
theorem bitb00: $ bit (b0 n) 0 = 0 $ = '(mpbir nateq0 elb00);
theorem bitb10: $ bit (b1 n) 0 = 1 $ = '(mpbir nateq1 elb10);
theorem bitb0S: $ bit (b0 n) (suc i) = bit n i $ = '(nateq elb0S);
theorem bitb1S: $ bit (b1 n) (suc i) = bit n i $ = '(nateq elb1S);
theorem bit_shr: $ bit (shr a k) i = bit a (i + k) $ = '(nateq elshr);
theorem bitb00i (h: $ a = b0 b $): $ bit a 0 = 0 $ = '(eqtr (biteq1 h) bitb00);
theorem bitb10i (h: $ a = b1 b $): $ bit a 0 = 1 $ = '(eqtr (biteq1 h) bitb10);
theorem bitb0Si (h: $ a = b0 b $) (h2: $ bit b n = c $): $ bit a (suc n) = c $ =
'(eqtr (biteq1 h) @ eqtr bitb0S h2);
theorem bitb1Si (h: $ a = b1 b $) (h2: $ bit b n = c $): $ bit a (suc n) = c $ =
'(eqtr (biteq1 h) @ eqtr bitb1S h2);
-- Adds theorems such as
-- theorem xbita3: $ bit xa 3 = 1 $;
-- which evaluate the bits of an individual hex digit.
-- Naming system is "xbit" + hex digit + index
do {
(def (xbit n i) @ atom-app "xbit" (hexstring n) (hexstring i))
(for 0 16 @ fn (n) @ for 0 4 @ fn (i)
@ letrec ([(f n i)
@ if {i = 0}
'(,(atom-app "bitb" {n % 2} "0i") ,(hexnhalf n))
'(,(atom-app "bitb" {n % 2} "Si")
,(hexnhalf n) ,(f {n // 2} {i - 1}))])
(add-tac-thm! (xbit n i) () ()
'(eq (bit (h2n (,(hexdigit n))) (,(dn i))) (,(dn {{n shr i} band 1}))) ()
@ fn () (f n i)))
};
@(add-eval @ fn (a b) {(eval a) band (eval b)})
@_ abstract def bitAnd (a b: nat): nat = $ lower (a i^i b) $;
pub theorem bitAndEq (a b: nat): $ bitAnd a b == a i^i b $ =
'(eqscom @ mpbi eqlower @ infin1 finns);
theorem elbitAnd: $ i e. bitAnd a b <-> i e. a /\ i e. b $ =
'(bitr (eleq2 bitAndEq) elin);
theorem bitAnd_sym: $ bitAnd a b = bitAnd b a $ =
'(axext @ eqstr4 bitAndEq @ eqstr4 bitAndEq incom);
theorem bitAnd_ass: $ bitAnd (bitAnd a b) c = bitAnd a (bitAnd b c) $ =
'(axext @ eqstr4 bitAndEq @ eqstr4 bitAndEq @
eqstr4 (ineq1 bitAndEq) @ eqstr4 (ineq2 bitAndEq) inass);
theorem bitAnd01 (a: nat): $ bitAnd 0 a = 0 $ = '(axext @ eqstr bitAndEq in01);
theorem bitAnd02 (a: nat): $ bitAnd a 0 = 0 $ = '(eqtr bitAnd_sym bitAnd01);
theorem bitAnd_idm (a: nat): $ bitAnd a a = a $ = '(axext @ eqstr bitAndEq inidm);
theorem bitAndb0l: $ bitAnd (b0 a) b = b0 (bitAnd a (b // 2)) $ =
(named '(axext @ ax_gen @ bitr elbitAnd @ bitr (aneq1i elb0) @
bitr4 anass @ bitr elb0 @ aneq2a @ syl5bb elbitAnd @
aneq2d @ syl5bb eldiv2 @ eleq1d @ syl sub1can ltner));
theorem bitAndb0r: $ bitAnd a (b0 b) = b0 (bitAnd (a // 2) b) $ =
'(eqtr bitAnd_sym @ eqtr4 bitAndb0l @ b0eq bitAnd_sym);
theorem bitAndb00: $ bitAnd (b0 a) (b0 b) = b0 (bitAnd a b) $ =
'(eqtr bitAndb0l @ b0eq @ bitAndeq2 b0div2);
theorem bitAndb01: $ bitAnd (b0 a) (b1 b) = b0 (bitAnd a b) $ =
'(eqtr bitAndb0l @ b0eq @ bitAndeq2 b1div2);
theorem bitAndb10: $ bitAnd (b1 a) (b0 b) = b0 (bitAnd a b) $ =
'(eqtr bitAndb0r @ b0eq @ bitAndeq1 b1div2);
theorem bitAndb11: $ bitAnd (b1 a) (b1 b) = b1 (bitAnd a b) $ =
(named '(axext @ ax_gen @ bitr elbitAnd @ bitr4 (aneq1i elb1) @
bitr elb1 @ bitr (oreq2i elbitAnd) @ bitr4 ordi @ aneq2i elb1));
@(add-eval @ fn (a b) {(eval a) bor (eval b)})
@_ abstract def bitOr (a b: nat): nat = $ lower (a u. b) $;
pub theorem bitOrEq (a b: nat): $ bitOr a b == a u. b $ =
'(eqscom @ mpbi eqlower @ unfin finns finns);
theorem elbitOr: $ i e. bitOr a b <-> i e. a \/ i e. b $ =
'(bitr (eleq2 bitOrEq) elun);
theorem bitOr_sym: $ bitOr a b = bitOr b a $ =
'(axext @ eqstr4 bitOrEq @ eqstr4 bitOrEq uncom);
theorem bitOr_ass: $ bitOr (bitOr a b) c = bitOr a (bitOr b c) $ =
'(axext @ eqstr4 bitOrEq @ eqstr4 bitOrEq @
eqstr4 (uneq1 bitOrEq) @ eqstr4 (uneq2 bitOrEq) unass);
theorem bitAnd_di: $ bitAnd a (bitOr b c) = bitOr (bitAnd a b) (bitAnd a c) $ =
'(axext @ eqstr4 bitAndEq @ eqstr4 bitOrEq @
eqstr4 (ineq2 bitOrEq) @ eqstr4 (uneq bitAndEq bitAndEq) indi);
theorem bitOr01 (a: nat): $ bitOr 0 a = a $ = '(axext @ eqstr bitOrEq un01);
theorem bitOr02 (a: nat): $ bitOr a 0 = a $ = '(eqtr bitOr_sym bitOr01);
theorem bitOr_idm (a: nat): $ bitOr a a = a $ = '(axext @ eqstr bitOrEq unidm);
theorem bitOrb1l: $ bitOr (b1 a) b = b1 (bitOr a (b // 2)) $ =
(named '(axext @ ax_gen @ bitr elbitOr @ bitr (oreq1i elb1) @
bitr4 orass @ bitr elb1 @ oreq2a @ syl5bb elbitOr @
oreq2d @ syl5bb eldiv2 @ eleq1d sub1can));
theorem bitOrb1r: $ bitOr a (b1 b) = b1 (bitOr (a // 2) b) $ =
'(eqtr bitOr_sym @ eqtr4 bitOrb1l @ b1eq bitOr_sym);
theorem bitOrb00: $ bitOr (b0 a) (b0 b) = b0 (bitOr a b) $ =
(named '(axext @ ax_gen @ bitr elbitOr @ bitr4 (oreq1i elb0) @
bitr elb0 @ bitr (aneq2i elbitOr) @ bitr4 andi @ oreq2i elb0));
theorem bitOrb01: $ bitOr (b0 a) (b1 b) = b1 (bitOr a b) $ =
'(eqtr bitOrb1r @ b1eq @ bitOreq1 b0div2);
theorem bitOrb10: $ bitOr (b1 a) (b0 b) = b1 (bitOr a b) $ =
'(eqtr bitOrb1l @ b1eq @ bitOreq2 b0div2);
theorem bitOrb11: $ bitOr (b1 a) (b1 b) = b1 (bitOr a b) $ =
'(eqtr bitOrb1l @ b1eq @ bitOreq2 b1div2);
theorem bitAnd_add_bitOr: $ bitAnd a b + bitOr a b = a + b $ =
(named @ focus
(def h '(aleqd @ eqeqd (addeqd bitAndeq1 bitOreq1) addeq1))
(def h2 '(eqeqd (addeqd bitAndeq2 bitOreq2) addeq2))
'(eale ,h2 @ trud @ !! indstr _ _ ,h ,h @ sylib (cbval ,h2) @ iald @
casesda (anwr @
eqtr4d (addeqd (syl6eq bitAnd01 @ bitAndeq1) (syl6eq bitOr01 @ bitOreq1)) addeq1) _)
(have 'hal '(rsyl anlr @ syl6 (eale ,h2) @ eale @ imeqd lteq1 ,h))
(def (f x y0 y1)
(def g @ match-fn @ (y z w1 w2 h)
'(eqtr4d (addeqd (syl6eq ,y @ bitAndeqd anlr anr) (syl6eq ,z @ bitOreqd anlr anr)) @
eqtr4d (addeqd anlr anr) @ syl5eq ,w1 @ syl6eqr ,w2
,(foldr h '(mpd (mpbird (lteq2d anlr) ,x) (anwll hal)) list)))
(split-sop '{($b0 v$ => ,(g y0)) + ($b1 v$ => ,(g y1))}))
(split-sop '{
($b0 u$ => ,(f '(sylib b0ltid @ sylib b0ne0 @ mpbid (neeq1d anlr) anllr)
'(bitAndb00 bitOrb00 addb00 addb00 (b0eqd))
'(bitAndb01 bitOrb01 addb01 addb01 (b1eqd)))) +
($b1 u$ => ,(f '(a1i b1ltid)
'(bitAndb10 bitOrb10 addb01 addb10 (b1eqd))
'(bitAndb11 bitOrb11 addb11 addb11 (b0eqd suceqd))))}));
theorem bitOr_eq_add2: $ bitAnd a b = 0 -> bitOr a b = a + b $ =
'(eqtr3g add01 bitAnd_add_bitOr @ addeq1d eqcom);
theorem bitOr_eq_add: $ a i^i b == 0 -> bitOr a b = a + b $ =
'(syl bitOr_eq_add2 @ syl axext @ syl5eqs bitAndEq id);
@(add-eval @ fn (a b) {(eval a) band (bnot (eval b))})
@_ abstract def bitDif (a b: nat): nat = $ lower (a i^i Compl b) $;
pub theorem bitDifEq (a b: nat): $ bitDif a b == a i^i Compl b $ =
'(eqscom @ mpbi eqlower @ infin1 finns);
theorem elbitDif (a b i: nat): $ i e. bitDif a b <-> (i e. a /\ ~i e. b) $ =
'(bitr (eleq2 bitDifEq) @ bitr elin @ aneq2i elcpl);
theorem bitDif01: $ bitDif 0 a = 0 $ = '(axext @ eqstr bitDifEq in01);
theorem bitDif02: $ bitDif a 0 = a $ = '(axext @ eqstr bitDifEq @ eqstr (ineq2 cpl0) inv2);
theorem bitDifid: $ bitDif a a = 0 $ = '(axext @ eqstr bitDifEq incpl2);
theorem bitDifeq0: $ bitDif a b = 0 <-> a C_ b $ =
'(bitr3 nsinj @ bitr (eqseq1 bitDifEq) incpleq0);
theorem bitDifAndss: $ a C_ c -> bitDif a (bitAnd c b) = bitDif a b $ =
'(syl axext @ !! alimi x @ bitr4g elbitDif elbitDif @
syl aneq2a @ imim2i @ noteqd @ syl5bb elbitAnd bian1);
theorem bitDifAndid: $ bitDif a (bitAnd a b) = bitDif a b $ = '(bitDifAndss ssid);
theorem bitDifAnd: $ bitDif (bitAnd a b) c = bitAnd a (bitDif b c) $ =
'(axext @ eqstr4 bitDifEq @ eqstr4 bitAndEq @
eqstr4 (ineq1 bitAndEq) @ eqstr4 (ineq2 bitDifEq) inass);
theorem bitDifadd: $ b C_ a -> bitDif a b + b = a $ =
'(syl5eqr (bitOr_eq_add @ mpbir ineq0 @ mpbir (sseq1 bitDifEq) inss2) @
sylib nsinj @ !! alimi x @ syl5bb elbitOr @ syl5bb (oreq1 elbitDif) @
syl5bb ordir @ syl5bb (bian2 emr) bior2a);
theorem bitDifsub: $ b C_ a -> bitDif a b = a - b $ =
'(syl5eqr pncan @ subeq1d bitDifadd);
theorem bitDif_upto: $ bitDif a (upto n) = shl (shr a n) n $ =
(named '(axext @ ax_gen @ bitr4 elbitDif @ bitr4 elshl @
bitr4 ancomb @ bitr (aneq2a @ syl5bb elshr @ eleq1d npcan) @
aneq1i @ con2b @ bitr elupto ltnle));
@(add-eval @ fn (a b) {(eval a) bxor (eval b)})
@_ abstract def bitXor (a b: nat): nat = $ lower {n | ~(n e. a <-> n e. b)} $;
pub theorem bitXor_mem (a b i: nat): $ i e. bitXor a b <-> ~(i e. a <-> i e. b) $ =
'(bitr (ellower @
finss (mpbi ssab1 @ !! ax_gen n @
sylibr elun @ con1 @ sylbi notor @ imp binth) @
unfin finns finns) @
elabe @ noteqd @ bieqd eleq1 eleq1);
@(add-eval 32) @_ def d32: nat = $ 2 ^ 5 $; prefix d32: $32$ prec max;
@(add-eval 64) @_ def d64: nat = $ 2 ^ 6 $; prefix d64: $64$ prec max;
@(add-eval 256) @_ def d256: nat = $ 2 ^ 8 $; prefix d256: $256$ prec max;
theorem d2mul16: $ 2 * 16 = 32 $ = '(eqtr2 powS @ muleq2 d2pow4);
theorem d2mul32: $ 2 * 32 = 64 $ = '(eqcom powS);
theorem d16mul16: $ 16 * 16 = 256 $ = '(eqcom @ pow22lem d2mul4 d2pow4);
theorem dec32: $ 32 = ,32 $ = '(eqtr3 d2mul16 ,to_hex);
do (insert! tohex-map 'd32 @ fn () '((hex (h2n (x2)) (x0)) (dec32)));
theorem d8mul4: $ 8 * 4 = 32 $ = norm_num;
theorem d32ne0: $ 32 != 0 $ = 'pow2ne0;
theorem d64ne0: $ 64 != 0 $ = 'pow2ne0;
theorem d256ne0: $ 256 != 0 $ = 'pow2ne0;
theorem dec64: $ 64 = ,64 $ = '(eqtr3 d2mul32 ,to_hex);
theorem dec256: $ 256 = ,256 $ = '(eqtr3 d16mul16 ,to_hex);
do (insert! tohex-map 'd64 @ fn () '((hex (h2n (x4)) (x0)) (dec64)));
do (insert! tohex-map 'd256 @ fn () '((hex (hex (h2n (x1)) (x0)) (x0)) (dec256)));
theorem d8mul8: $ 8 * 8 = 64 $ = norm_num;
theorem c2nlt256 (c: char): $ c < 256 $ = '(mpbi (lteq2 d16mul16) c2nlt);
theorem c2nlt256pow (c: char): $ c < 256 ^ suc k $ =
'(ltletr c2nlt256 @ mpbi (leeq1 pow12) @ lepow2a d256ne0 le11S);
theorem d8le32: $ 8 <= 32 $ = norm_num;
theorem d8le64: $ 8 <= 64 $ = norm_num;
theorem d8lt32: $ 8 < 32 $ = norm_num;
theorem d8lt64: $ 8 < 64 $ = norm_num;
theorem d16lt32: $ 16 < 32 $ = norm_num;
theorem d16lt64: $ 16 < 64 $ = norm_num;
theorem d16le64: $ 16 <= 64 $ = '(ltle d16lt64);
theorem d32le64: $ 32 <= 64 $ = norm_num;
@_ def Bits (k: nat): nat = $ upto (2 ^ k) $;
theorem Bitsle (m n v: nat): $ m <= n -> v e. Bits m -> v e. Bits n $ =
'(sylibr (imeqi elupto elupto) @ syl (com12 ltletr) @ lepow2a d2ne0);
theorem Bitsss (m n: nat): $ m <= n -> Bits m C_ Bits n $ = '(!! iald x Bitsle);
theorem Bits_eq_power: $ Bits n = power (upto n) $ = '(eqcom powerupto);
theorem elBits: $ a e. Bits n <-> a C_ upto n $ =
'(bitr (elneq2 Bits_eq_power) elpower);
theorem elBits2: $ a e. Bits n <-> a < 2 ^ n $ = 'elupto;
theorem elBitsS_el: $ a e. Bits (suc n) -> (a e. Bits n <-> ~n e. a) $ =
'(sylbi elBits @ sylbi (sseq2 @ nseq uptoS_ins) @
syl5bb elBits @ ibid (a1i @ mpi ltirr @ con3d @ syl6ib elupto @ ssel) ssins);
theorem uptoT: $ upto n e. Bits n $ = '(mpbir elBits ssid);
theorem elBits8mul: $ n e. Bits (8 * k) <-> n < 256 ^ k $ =
'(bitr elBits2 @ lteq2 powmul);
theorem Bitsle1: $ v <= w -> w e. Bits n -> v e. Bits n $ =
'(sylibr (imeqi elBits2 elBits2) lelttr);
theorem Bits_mod: $ a e. Bits n -> a % 2 ^ n = a $ = '(sylbi elBits2 modlteq);
theorem Bits_eqm: $ a e. Bits n /\ b e. Bits n -> (mod(2 ^ n): a = b <-> a = b) $ =
'(eqeqd (anwl Bits_mod) (anwr Bits_mod));
theorem Bits_zeqm: $ a e. Bits n /\ b e. Bits n -> (modZ(2 ^ n): b0 a = b0 b <-> a = b) $ =
'(syl5bb zeqmeqm Bits_eqm);
theorem elBits0: $ a e. Bits 0 <-> a = 0 $ = '(bitr elBits2 @ bitr (lteq2 pow0) lt12);
theorem elBits01: $ 0 e. Bits n $ = '(mpbir elBits ss01);
theorem elBitsx01: $ x0 e. Bits n $ = '(mpbi (eleq1 dec0) elBits01);
theorem elBits1: $ a e. Bits 1 <-> bool a $ = '(bitr elBits2 @ lteq2 pow12);
theorem elBits11: $ 1 e. Bits n <-> n != 0 $ =
'(bitr4 elBits2 @ bitr3 lt01 @ bitr (ltpow2 d1lt2) (lteq1 pow0));
theorem Bits_zeqm_02: $ a e. Bits n -> (modZ(2 ^ n): b0 a = 0 <-> a = 0) $ =
'(syl5bbr (zeqmeq3 b00) @ mpand (a1i elBits01) Bits_zeqm);
theorem eq_bitAnd1: $ a C_ b <-> bitAnd a b = a $ = '(bitr eqin1 @ bitr3 (eqseq1 bitAndEq) nsinj);
theorem eq_bitAnd2: $ a C_ b <-> bitAnd b a = a $ = '(bitr eq_bitAnd1 @ eqeq1 bitAnd_sym);
theorem bitAndT1: $ a e. Bits n -> bitAnd a b e. Bits n $ =
'(sylbi elBits @ sylibr elBits @ sylibr (sseq1 bitAndEq) @ sstr inss1);
theorem bitAndT2: $ b e. Bits n -> bitAnd a b e. Bits n $ =
'(sylbi elBits @ sylibr elBits @ sylibr (sseq1 bitAndEq) @ sstr inss2);
theorem bitOrT: $ a e. Bits n /\ b e. Bits n <-> bitOr a b e. Bits n $ =
'(bitr4 (aneq elBits elBits) @ bitr elBits @ bitr (sseq1 bitOrEq) unss);
theorem bitDifT: $ a e. Bits n -> bitDif a b e. Bits n $ =
'(sylbi elBits @ sylibr elBits @ sylibr (sseq1 bitDifEq) @ sstr inss1);
theorem mulBitsT: $ a e. Bits m /\ b e. Bits n -> a * b e. Bits (m + n) $ =
'(sylibr elBits2 @ sylibr (lteq2 powadd) @ ltmuld (sylib elBits2 anl) (sylib elBits2 anr));
theorem shladdT: $ a e. Bits n /\ c e. Bits b -> shl a b + c e. Bits (n + b) $ =
'(sylibr elBits2 @ ltletrd (sylib ltadd2 @ sylib elBits2 anr) @
sylib (leeq mulS1 @ eqcom powadd) @ syl lemul1a @
sylib elBits2 anl);
theorem shlT: $ a e. Bits n -> shl a b e. Bits (n + b) $ =
'(sylib (eleq1 add0) @ mpi elBits01 @ exp shladdT);
theorem shlT2: $ a e. Bits n -> n + b <= c -> shl a b e. Bits c $ =
'(rsyl shlT @ com12 @ syl ssel Bitsss);
theorem shrT: $ a e. Bits (n + b) -> shr a b e. Bits n $ =
'(sylibr elBits @ sylbi elBits @ !! iald x @ syl5bi elshr @
syl6ib (bitr4 elupto @ bitr elupto ltadd1) ssel);
theorem b1Bits: $ a e. Bits n <-> b1 a e. Bits (suc n) $ =
'(bitr4 elBits2 @ bitr elBits2 @ bitr (lteq2 @ eqtr powS b0mul21) b1ltb0);
theorem b0Bits: $ a e. Bits n <-> b0 a e. Bits (suc n) $ =
'(bitr4 elBits2 @ bitr elBits2 @ bitr4 (lteq2 @ eqtr powS b0mul21) b0lt);
theorem b0Bitsi (h1: $ a = b0 a2 $) (h2: $ a2 e. Bits n $): $ a e. Bits (suc n) $ =
'(mpbir (eleq1 h1) @ mpbi b0Bits h2);
theorem b1Bitsi (h1: $ a = b1 a2 $) (h2: $ a2 e. Bits n $): $ a e. Bits (suc n) $ =
'(mpbir (eleq1 h1) @ mpbi b1Bits h2);
theorem mod_el_Bits: $ a % (2 ^ k) e. Bits k $ = '(mpbir elupto @ modlt pow2ne0);
theorem h2nT (h: hex): $ h e. Bits 4 $ =
'(mpbir elBits2 @ mpbir (lteq2 d2pow4) h2nlt);
theorem hexT: $ a e. Bits k -> a :x x e. Bits (k + 4) $ =
'(sylibr (eleq1 hexshl4) @ sylan shladdT id (a1i h2nT));
theorem hex2T: $ a e. Bits k -> a :x x :x y e. Bits (k + 8) $ =
'(sylib (elneq2 @ Bitseq @ eqtr addass @ addeq2 d4add4) @ syl hexT hexT);
theorem xelBits4S (h: $ n e. Bits (4 * k) $): $ n :x a e. Bits (4 * suc k) $ =
'(mpbir (elneq2 @ Bitseq mulS) (hexT h));
theorem xelBits41: $ h2n a e. Bits (4 * suc k) $ =
'(mpbi (eleq1 hex01_) @ xelBits4S elBits01);
--| `(to-elBits4 k n)` proves `n e. Bits (4 * k)`
do (def (to-elBits4 k n) @ match k
[$suc ,k$ @ match n
[$,n :x ,a$ '(xelBits4S ,a ,k ,n ,(to-elBits4 k n))]
[$h2n ,a$ '(xelBits41 ,a ,k)]]);
theorem xelBits8S (h: $ n e. Bits (8 * k) $): $ n :x a1 :x a0 e. Bits (8 * suc k) $ =
'(mpbir (elneq2 @ Bitseq mulS) (hex2T h));
theorem xelBits82: $ h2n a1 :x a0 e. Bits (8 * suc k) $ =
'(mpbi (eleq1 @ hexeq1 hex01_) @ xelBits8S elBits01);
theorem xelBits81: $ h2n a0 e. Bits (8 * suc k) $ =
'(mpbi (eleq1 hex01) xelBits82);
--| `(to-elBits8 k n)` proves `n e. Bits (8 * k)`
do (def (to-elBits8 k n) @ match k
[$suc ,k$ @ match n
[$,n :x ,a1 :x ,a0$ '(xelBits8S ,a0 ,a1 ,k ,n ,(to-elBits8 k n))]
[$h2n ,a1 :x ,a0$ '(xelBits82 ,a0 ,a1 ,k)]
[$h2n ,a0$ '(xelBits81 ,a0 ,k)]]);
theorem xelBits7S (h: $ n e. Bits (8 * k + 7) $): $ n :x a1 :x a0 e. Bits (8 * suc k + 7) $ =
'(mpbir (elneq2 @ Bitseq @ eqtr (addeq1 mulS) addrass) (hex2T h));
theorem xelBits72S: $ h2n a1 :x a0 e. Bits (8 * suc k + 7) $ =
'(mpbi (elneq (hexeq1 hex01_) @ Bitseq @ eqtr4 addrass @ addeq1 mulS) (hex2T elBits01));
theorem xelBits720 (h: $ a1 < x8 $): $ h2n a1 :x a0 e. Bits (8 * 0 + 7) $ =
'(mpbi (elneq2 @ Bitseq {,norm_num : $ 3 + 4 = _ $})
(hexT @ mpbir elBits2 @ mpbir (lteq2 @ eqtr d2pow3 dec8) h));
theorem xelBits71: $ h2n a0 e. Bits (8 * k + 7) $ =
'(Bitsle (letr {,norm_num : $ 4 <= 7 $} leaddid2) h2nT);
--| `(to-elBits7 k n)` proves `n e. Bits (8 * k + 7)`
do (def (to-elBits7 k n) @ match n
[$,n :x ,a1 :x ,a0$ @ match k
[$suc ,k$ '(xelBits7S ,a0 ,a1 ,k ,n ,(to-elBits7 k n))]]
[$h2n ,a1 :x ,a0$ @ match k
[$suc ,k$ '(xelBits72S ,a0 ,a1 ,k)]
[$0$ '(xelBits720 ,a0 ,a1 ,(atom-app 'declt (hexstring (hex->number a1)) 8))]]
[$h2n ,a0$ '(xelBits71 ,a0 ,k)]);
@_ def u8: nat = $ Bits 8 $;
@_ def u16: nat = $ Bits 16 $;
@_ def u32: nat = $ Bits 32 $;
@_ def u64: nat = $ Bits 64 $;
theorem d0elu8: $ 0 e. u8 $ = 'elBits01;
theorem d0elu16: $ 0 e. u16 $ = 'elBits01;
theorem d0elu32: $ 0 e. u32 $ = 'elBits01;
theorem d0elu64: $ 0 e. u64 $ = 'elBits01;
theorem u32ss64: $ u32 C_ u64 $ = '(Bitsss d32le64);
theorem u16ss64: $ u16 C_ u64 $ = '(Bitsss d16le64);
theorem u8ss32: $ u8 C_ u32 $ = '(Bitsss d8le32);
theorem u8ss64: $ u8 C_ u64 $ = '(Bitsss d8le64);
theorem u8ss16: $ u8 C_ u16 $ = '(Bitsss @ ltle d8lt16);
theorem u64le1: $ v <= w -> w e. u64 -> v e. u64 $ = 'Bitsle1;
theorem elu8: $ n e. u8 <-> n < 16 * 16 $ = '(bitr elBits2 @ lteq2 d2pow8);
theorem elu8_2: $ n e. u8 <-> n < 256 $ = '(bitr elu8 @ lteq2 d16mul16);
theorem elu8_3: $ n e. u8 <-> n < 256 ^ 1 $ = '(bitr4 elu8_2 @ lteq2 pow12);
theorem c2nT (c: char): $ c e. u8 $ = '(mpbir elu8 c2nlt);
theorem elu8_lem (h: $ n < ,256 $): $ n e. u8 $ =
'(mpbir elBits2 @ mpbir (lteq2 d2pow8x) h);
theorem d1elu8: $ 1 e. u8 $ = '(elu8_lem ,norm_num);
theorem d2elu8: $ 2 e. u8 $ = '(elu8_lem ,norm_num);
theorem d1elu32: $ 1 e. u32 $ = '(ssel u8ss32 d1elu8);
theorem mod_el_u8: $ a % 256 e. u8 $ = 'mod_el_Bits;
theorem elu16: $ n e. u16 <-> n < 256 ^ 2 $ =
'(bitr (elneq2 @ Bitseq {,norm_num : $ 16 = 8 * 2 $}) elBits8mul);
theorem elu32: $ n e. u32 <-> n < 256 ^ 4 $ =
'(bitr (elneq2 @ Bitseq {,norm_num : $ 32 = 8 * 4 $}) elBits8mul);
theorem elu64: $ n e. u64 <-> n < 256 ^ 8 $ =
'(bitr (elneq2 @ Bitseq {,norm_num : $ 64 = 8 * 8 $}) elBits8mul);
theorem xu8Byte_2 (a0 a1: hex): $ ch a1 a0 = a1 :x a0 $ = 'c2nhex;
theorem xu8Byte_1 (a0: hex): $ ch x0 a0 = a0 $ = 'c2nh2n;
theorem xelu8_1 (a0: hex): $ a0 e. u8 $ = '(mpbi (eleq1 xu8Byte_1) c2nT);
theorem xelu8_2 (a0 a1: hex): $ a1 :x a0 e. u8 $ = '(mpbi (eleq1 xu8Byte_2) c2nT);
theorem xeluNlem (e: $ 8 * k = n $) (h: $ a e. Bits (8 * k) $): $ a e. Bits n $ =
'(mpbi (elneq2 @ Bitseq e) h);
theorem xelu8i (h: $ a e. Bits (8 * suc 0) $): $ a e. u8 $ = '(xeluNlem mul12 h);
theorem xelu16i (h: $ a e. Bits (8 * ,(sucs 2)) $): $ a e. u16 $ = '(xeluNlem d8mul2 h);
theorem xelu32i (h: $ a e. Bits (8 * ,(sucs 4)) $): $ a e. u32 $ = '(xeluNlem d8mul4 h);
theorem xelu64i (h: $ a e. Bits (8 * ,(sucs 8)) $): $ a e. u64 $ = '(xeluNlem d8mul8 h);
--| `(to-elu N a)` returns a proof that `a` is a hex literal in uN: `a e. uN`
--| assuming `N = 8,16,32,64`
do (def (to-elu n a)
'(,(atom-app 'xelu n 'i) ,a ,(to-elBits8 (sucs {n // 8}) a)));
theorem xelBits7b0 (h: $ a e. Bits (8 * k + 7) $): $ b0 a e. Bits (8 * suc k) $ =
'(mpbir (elneq2 @ Bitseq @ eqtr mulS addS2) @ mpbi b0Bits h);
theorem xelBits7b1 (h: $ a e. Bits (8 * k + 7) $): $ b1 a e. Bits (8 * suc k) $ =
'(mpbir (elneq2 @ Bitseq @ eqtr mulS addS2) @ mpbi b1Bits h);
theorem xelu8b0i (h: $ a e. Bits (8 * 0 + 7) $): $ b0 a e. u8 $ = '(xelu8i @ xelBits7b0 h);
theorem xelu8b1i (h: $ a e. Bits (8 * 0 + 7) $): $ b1 a e. u8 $ = '(xelu8i @ xelBits7b1 h);
theorem xelu16b0i (h: $ a e. Bits (8 * ,(sucs 1) + 7) $): $ b0 a e. u16 $ = '(xelu16i @ xelBits7b0 h);
theorem xelu16b1i (h: $ a e. Bits (8 * ,(sucs 1) + 7) $): $ b1 a e. u16 $ = '(xelu16i @ xelBits7b1 h);
theorem xelu32b0i (h: $ a e. Bits (8 * ,(sucs 3) + 7) $): $ b0 a e. u32 $ = '(xelu32i @ xelBits7b0 h);
theorem xelu32b1i (h: $ a e. Bits (8 * ,(sucs 3) + 7) $): $ b1 a e. u32 $ = '(xelu32i @ xelBits7b1 h);
theorem xelu64b0i (h: $ a e. Bits (8 * ,(sucs 7) + 7) $): $ b0 a e. u64 $ = '(xelu64i @ xelBits7b0 h);
theorem xelu64b1i (h: $ a e. Bits (8 * ,(sucs 7) + 7) $): $ b1 a e. u64 $ = '(xelu64i @ xelBits7b1 h);
--| `(to-eli N a)` returns a proof that `a` is a signed hex literal in uN: `a e. uN`
--| assuming `N = 8,16,32,64`
do (def (to-eli n a) @ match a
[$0$ '(,(atom-app 'd0elu n))]
[$b0 ,a$ '(,(atom-app 'xelu n 'b0i) ,a ,(to-elBits7 (sucs {{n // 8} - 1}) a))]
[$b1 ,a$ '(,(atom-app 'xelu n 'b1i) ,a ,(to-elBits7 (sucs {{n // 8} - 1}) a))]);
--| Get the lower bits of a number
@(add-eval @ fn (k n) {(eval n) band {{1 shl (eval k)} - 1}})
@_ def chop (k n: nat): nat = $ n % 2 ^ k $;
pub theorem chopT (k n: nat): $ chop k n e. Bits k $ = '(mpbir elupto @ modlt pow2ne0);
theorem chop01: $ chop 0 n = 0 $ = '(mpbi elBits0 chopT);
theorem chop02: $ chop k 0 = 0 $ = 'mod01;
theorem el_chop: $ a e. chop k n <-> a < k /\ a e. n $ = 'elmodpow2;
theorem bit_chop: $ a < k -> bit (chop k n) a = bit n a $ =
'(nateqd @ syl5bb el_chop bian1);
theorem bit_chop_0: $ ~a < k -> bit (chop k n) a = 0 $ =
'(sylibr nateq0 @ con3 @ sylbi el_chop anl);
theorem chopT_min: $ a e. Bits m -> chop k a e. Bits (min m k) $ =
(named '(sylibr elBits @ iald @ syl5bi el_chop @ exp @ sylibr elupto @
sylibr ltmin @ iand (sylib elupto @ sylc ssel (sylib elBits anl) anrr) anrl));
theorem bitAnd_upto: $ bitAnd (upto k) a = chop k a $ =
'(axext @ !! ax_gen x @ bitr4 elbitAnd @ bitr4 el_chop @ aneq1i elupto);
theorem chop_upto: $ m <= k <-> chop m (upto k) = upto m $ =
'(bitr3 uptoss @ bitr eq_bitAnd1 @ eqeq1 bitAnd_upto);
theorem shlshr_chop: $ shl (shr n k) k + chop k n = n $ = '(eqtr (addeq1 mulcom) divmod);
theorem chop_shl_0: $ m <= k -> chop m (shl a k) = 0 $ =
'(syl axext @ sylib ss02 @ !! iald x @ syl5bi el_chop @ impd @
syl6 (syl5bi elshl @ sylbi ltnle @ syl5 anl absurd) @ com12 ltletr);
theorem shladd_uniq: $ a e. Bits k /\ shl m k + a = n <-> shr n k = m /\ chop k n = a $ =
'(ibii (eqdivmod (sylib elBits2 anl) @ syl5eq (addeq1 mulcom) anr) @
mpbii (ian chopT shlshr_chop) ,(eqtac-with #f));
theorem chop_shladd: $ b e. Bits k -> chop k (shl a k + b) = b $ =
'(anrd @ sylib shladd_uniq @ iand id eqidd);
theorem chop4hex: $ chop 4 (a :x b) = b $ = '(eqtr (chopeq2 hexshl4) @ chop_shladd h2nT);
theorem chop_shladd2: $ chop k (shl a k + b) = chop k b $ = '(muladdmod1 pow2ne0);
theorem Bits_chop: $ a e. Bits k -> chop k a = a $ = 'Bits_mod;
theorem eqm_chop: $ mod(2 ^ k): chop k a = a $ = 'eqmmod;
theorem zeqm_chop: $ modZ(2 ^ k): b0 (chop k a) = b0 a $ = '(mpbir zeqmeqm eqm_chop);
theorem chop_eq_chop: $ chop k a = chop k b <-> mod(2 ^ k): a = b $ = 'biid;
theorem chop_eq_chop2: $ chop k a = chop k b <-> modZ(2 ^ k): b0 a = b0 b $ =
'(bitr4 chop_eq_chop zeqmeqm);
theorem chop_chop: $ m <= n -> chop m (chop n a) = chop m a $ = '(syl modmod powdvd);
theorem chop_shl: $ shl (chop n a) k = chop (n + k) (shl a k) $ =
'(eqtr4 mulmoddir @ modeq2 powadd);
theorem chop_shr: $ shr (chop (n + k) a) k = chop n (shr a k) $ =
'(eqtr4 (diveq1 @ modeq2 powadd) divmod2);
theorem chop_shr2: $ shr (chop (k + n) a) k = chop n (shr a k) $ =
'(eqtr (shreq1 @ chopeq1 addcom) chop_shr);
theorem chop_bitAnd1: $ chop m (bitAnd a b) = bitAnd (chop m a) b $ =
'(eqtr3 bitAnd_upto @ eqtr3 bitAnd_ass @ bitAndeq1 bitAnd_upto);
theorem chop_bitAnd2: $ chop m (bitAnd a b) = bitAnd a (chop m b) $ =
'(eqtr (chopeq2 bitAnd_sym) @ eqtr chop_bitAnd1 bitAnd_sym);
theorem chop_bitAnd: $ chop m (bitAnd a b) = bitAnd (chop m a) (chop m b) $ =
'(eqtr3 (chop_chop leid) @ eqtr (chopeq2 chop_bitAnd1) chop_bitAnd2);
theorem chop_bitOr: $ chop m (bitOr a b) = bitOr (chop m a) (chop m b) $ =
'(eqtr3 bitAnd_upto @ eqtr bitAnd_di @ bitOreq bitAnd_upto bitAnd_upto);
theorem chop_bitDif1: $ chop m (bitDif a b) = bitDif (chop m a) b $ =
'(eqtr3 bitAnd_upto @ eqtr3 bitDifAnd @ bitDifeq1 bitAnd_upto);
theorem chop_bitDif: $ chop m (bitDif a b) = bitDif (chop m a) (chop m b) $ =
'(eqtr4 chop_bitDif1 @ eqtr3 (bitDifeq2 bitAnd_upto) @ bitDifAndss @ mpbi elBits chopT);
theorem shl_bitAnd: $ shl (bitAnd a b) m = bitAnd (shl a m) (shl b m) $ =
'(axext @ !! ax_gen x @ bitr4 elshl @ bitr4 elbitAnd @
bitr (aneq2i elbitAnd) @ bitr4 anandi @ aneq elshl elshl);
theorem shl_bitOr: $ shl (bitOr a b) m = bitOr (shl a m) (shl b m) $ =
'(axext @ !! ax_gen x @ bitr4 elshl @ bitr4 elbitOr @
bitr (aneq2i elbitOr) @ bitr4 andi @ oreq elshl elshl);
theorem shl_bitDif: $ shl (bitDif a b) m = bitDif (shl a m) (shl b m) $ =
'(axext @ !! ax_gen x @ bitr4 elshl @ bitr4 elbitDif @
bitr4 (aneq2i elbitDif) @ bitr (aneq elshl @ noteq elshl) @
bitr anass @ aneq2a @ aneq2d @ noteqd bian1);
theorem shr_bitAnd: $ shr (bitAnd a b) m = bitAnd (shr a m) (shr b m) $ =
'(axext @ !! ax_gen x @ bitr4 elshr @ bitr4 elbitAnd @ bitr4 elbitAnd @ aneq elshr elshr);
theorem shr_bitOr: $ shr (bitOr a b) m = bitOr (shr a m) (shr b m) $ =
'(axext @ !! ax_gen x @ bitr4 elshr @ bitr4 elbitOr @ bitr4 elbitOr @ oreq elshr elshr);
theorem shr_bitDif: $ shr (bitDif a b) m = bitDif (shr a m) (shr b m) $ =
'(axext @ !! ax_gen x @ bitr4 elshr @ bitr4 elbitDif @ bitr4 elbitDif @ aneq elshr @ noteq elshr);
theorem eqm_chopd (h: $ G -> mod(2 ^ k): a = b $):
$ G -> mod(2 ^ k): chop k a = b $ = '(syl (eqmtr eqm_chop) h);
theorem zeqm_chopd (h: $ G -> modZ(2 ^ k): b0 a = b $):
$ G -> modZ(2 ^ k): b0 (chop k a) = b $ = '(syl (zeqmtr zeqm_chop) h);
theorem zeqm_chop1: $ b e. Bits n -> (modZ(2 ^ n): b0 a = b0 b <-> chop n a = b) $ =
'(syl5bbr (zeqmeqm2 zeqm_chop) @ rsyl (ian chopT) Bits_zeqm);
theorem zeqm_chop2: $ a e. Bits n -> (modZ(2 ^ n): b0 a = b0 b <-> a = chop n b) $ =
'(syl5bbr (zeqmeqm3 zeqm_chop) @ mpand (a1i chopT) Bits_zeqm);
@(add-eval @ fn (k n) {(evalZ n) band {{1 shl (eval k)} - 1}})
@_ local def chopZ (k n: nat): nat = $ n %Z 2 ^ k $;
theorem chopZT (k n: nat): $ chopZ k n e. Bits k $ = 'chopT;
theorem chopZ_b0: $ chopZ k (b0 a) = chop k a $ = 'zmodb0;
theorem zeqm_chopZ: $ modZ(2 ^ k): b0 (chopZ k a) = a $ = '(zeqmmod pow2ne0);
theorem zeqm_chopZd (h: $ G -> modZ(2 ^ k): a = b $):
$ G -> modZ(2 ^ k): b0 (chopZ k a) = b $ = '(syl (zeqmtr zeqm_chopZ) h);
theorem chopZ_eq_chopZ: $ chopZ k a = chopZ k b <-> modZ(2 ^ k): a = b $ = '(zmodeqmod pow2ne0);
theorem chopZ_b1: $ a e. Bits k -> chopZ k (b1 a) = 2 ^ k - suc a $ = '(sylbi elBits2 zmodb1);
theorem chopZ_b1_2: $ a e. Bits k -> chopZ k (b1 a) + suc a = 2 ^ k $ =
'(eqtrd (addeq1d chopZ_b1) @ sylbi elBits2 npcan);
theorem hex_divmod256:
$ (a :x b :x c) // 256 = a /\ (a :x b :x c) % 256 = b :x c $ =
'(trud @ eqdivmod (a1i @ mpbi elu8_2 @ mpbi (eleq1 c2nch) c2nT) @
a1i @ eqtr3 addass @ addeq1 @
eqtr4 (addeq1 @ eqtr4 mulcom @ eqtr mulass @ muleq2 d16mul16) addmul);
theorem xchopshr8: $ shr (a :x b :x c) 8 = a /\ chop 8 (a :x b :x c) = b :x c $ = 'hex_divmod256;
theorem s2nT (s: string): $ s e. List u8 $ =
'(mpbir elList @ mpbir (alleq1 @ !! eqab2i n elu8) s2nlt);
@(add-eval @ fn (k n) @ match (eval k) [0 #f] [k {{{(eval n) shr {k - 1}} band 1} = 1}])
@_ def bitsMSB (k n: nat): wff = $ 0 < k /\ k - 1 e. n $;
theorem bitsMSB_b0: $ bitsMSB k n <-> k e. b0 n $ = '(bicom elb0);
theorem bitsMSB_Bits: $ n e. Bits k -> (bitsMSB k n <-> ~n e. Bits (k - 1)) $ =
'(syl con2b @ casesda
(bithd (mpbiri elBits01 @ eleq1d @ sylib elBits0 @ impcom @ bi1d @ elneq2d Bitseq)
(anwr @ con2 @ sylib lt01 anl))
(bitr4d (syl elBitsS_el @ impcom @ bi2d @ elneq2d @ Bitseqd sub1can)
(noteqd @ syl bian1 @ sylibr lt01 anr)));
theorem bitsMSB_le: $ n e. Bits k -> (bitsMSB k n <-> 2 ^ (k - 1) <= n) $ =
'(syl6bbr lenlt @ syl6bb (noteq elBits2) bitsMSB_Bits);
theorem chopZ_MSB: $ a e. Bits k -> (bitsMSB k (chopZ k a) <-> odd a) $ =
(focus
(have 'h '(Bitsle1 divleid))
(def h2 '(mpbid (elneqd anr @ Bitseqd @ eqcomd @ syl sub1can anlr) anll))
'(casesda _ @ ibid _ _)
'(binthd (anwr @ con2 @ sylib lt01 anl) @ mpbiri odd0 @
noteqd @ oddeqd @ sylib elBits0 @ impcom @ bi1d @ elneq2d Bitseq)
'(syl5bi (bitsMSB_Bits chopZT) @ con1d @ syl5bi eqb0 @ exp @
mpbird (eleq1d @ eqtrd (chopZeq2d anr) @ syl5eq chopZ_b0 @ syl Bits_chop @ anwll h) @
sylibr b0Bits ,h2)
'(syl5bi eqb1 @ exp @ sylibr (bitsMSB_le chopZT) @
mpbird (leeq2d @ eqtrd (chopZeq2d anr) @ syl chopZ_b1 @ anwll h) @
sylib (leeq1 pncan) @ syl lesub1i @
mpbid (leeq2d @ syl5eqr mul21 @ syl5eqr powS @ poweq2d @ syl sub1can anlr) @
sylib leadd2 @ sylib elBits2 @ sylibr b1Bits ,h2));
theorem Bits_zeqm2: $ a e. Bits n /\ b e. Bits n -> (modZ(2 ^ n): a = b <-> a = b) $ =
(focus
(have 'h $ _ -> (odd a <-> odd b) $
'(bitr3d (rsyl anll chopZ_MSB) @ bitrd (bitsMSBeq2d anr) (rsyl anlr chopZ_MSB)))
'(syl5bbr chopZ_eq_chopZ @ ibid (exp @ casesda _ _) @ a1i chopZeq2)
(focus
(have 'h1 '(sylib eqb1 anr))
(have 'h2 '(sylib eqb1 @ imp @ bi1d h))
'(eqtr4d h1 @ eqtr4d h2 @ b1eqd @ sylib peano2 @ sylib addcan2 @
eqtr4d (syl chopZ_b1_2 @ rsyl an3l @ Bitsle1 divleid) @
eqtrd (addeq1d @ eqtr3d (chopZeq2d h1) @ eqtrd anlr (chopZeq2d h2)) @
syl chopZ_b1_2 @ rsyl anllr @ Bitsle1 divleid))
(focus
(have 'h3 '(sylib eqb0 anr))
(have 'h4 '(sylib eqb0 @ imp @ con3d @ bi2d h))
'(eqtr4d h3 @ eqtr4d h4 @ b0eqd @
mpbid (sylan Bits_eqm (rsyl an3l @ Bitsle1 divleid) (rsyl anllr @ Bitsle1 divleid)) @
eqtr3g chopZ_b0 chopZ_b0 @ eqtr3d (chopZeq2d h3) @ eqtrd anlr (chopZeq2d h4))));
--| Sign extend `(v: bitvec m)` to length `n`
@_ def sExt (m n v: nat): nat = $ if (bitsMSB m v) (2 ^ n - 2 ^ m + v) v $;
@_ def sExtq (n v: nat): nat = $ sExt n 64 v $;
pub theorem sExtT (m n v: nat): $ m <= n /\ v e. Bits m -> sExt m n v e. Bits n $ =
'(casesda
(mpbird (eleq1d @ anwr ifpos) @
sylibr elupto @ mpbid (lteq2d @ syl npcan @ anwll @ lepow2a d2ne0) @
sylib ltadd2 @ sylib elupto anlr)
(mpbird (eleq1d @ anwr ifneg) @ anwl @ imp Bitsle));
pub theorem sExtqT (n v: nat): $ n <= 64 /\ v e. Bits n -> sExtq n v e. u64 $ = 'sExtT;
theorem sExt_chopZ: $ m <= n /\ a e. Bits m -> sExt m n (chopZ m a) = chopZ n a $ =
(focus
(have 'h0 '(anwr @ Bitsle1 b0leid))
(have 'h1 '(anwr @ Bitsle1 b1leid))
'(imp ,(split-sop 'a (fn (x) '(syl5ibrcom ,eqtac @ exp ,x)) '{
($b0 x$ => (eqtrd (syl ifneg @ mpbiri b0odd @ noteqd @ anwr chopZ_MSB) @
eqtr4g chopZ_b0 chopZ_b0 @
eqtr4d (syl Bits_chop h0) (syl Bits_chop @ sylc Bitsle anl h0))) +
($b1 x$ => (eqtrd (syl ifpos @ mpbiri b1odd @ anwr chopZ_MSB) @
eqtr4d (addeq2d @ syl chopZ_b1 h1) @ eqtr4d (syl chopZ_b1 @ sylc Bitsle anl h1) @
eqcomd @ syl eqsub1 @ syl5eq addass @
eqtrd (addeq2d @ syl npcan @ sylib elBits2 h1) @
anwl @ syl npcan @ lepow2a d2ne0))})));
--| Write `a e. Bits m` to bits `k` thru `k+m-1` of `n`
@_ def bitsUpdate (k m a n: nat): nat = $ bitDif n (shl (upto m) k) + shl a k $;
pub theorem bitsUpdateT (k m l a n: nat):
$ k + m <= l /\ a e. Bits m /\ n e. Bits l -> bitsUpdate k m a n e. Bits l $ =
'(mpbid (eleq1d @ syl bitOr_eq_add @ sylibr ineq0 @
sylibr (sseq1 bitDifEq) @ syl (sstr inss2) @
sylib sscpl @ sylib shlss @ sylib elBits anlr) @
sylib bitOrT @ iand (anwr bitDifT) (sylc shlT2 anlr @ sylib (leeq1 addcom) anll));
theorem bitsUpdate_or: $ a e. Bits m ->
bitsUpdate k m a n = bitOr (bitDif n (shl (upto m) k)) (shl a k) $ =
'(eqcomd @ syl bitOr_eq_add @ sylibr ineq0 @ sylibr (sseq1 bitDifEq) @
sylbi elBits @ sylbi shlss @ sylbi sscpl @ sstr inss2);
theorem shr_bitsUpdate:
$ shr (bitsUpdate (k + i) m a n) i = bitsUpdate k m a (shr n i) $ =
'(eqtr (shreq1 @ eqtr4 addcom @ addeq1 shlshl) @ eqtr shrshladd @
eqtr addcom @ addeq1 @ eqtr shr_bitDif @
bitDifeq2 @ eqtr3 (shreq1 shlshl) shrshlid);
theorem chop_bitsUpdate_2: $ k + i = j -> a e. Bits m ->
chop j (bitsUpdate k m a n) = bitsUpdate k m (chop i a) (chop j n) $ =
'(exp @ eqtr4d (chopeq2d @ anwr bitsUpdate_or) @
eqtr4d (syl bitsUpdate_or @ anwr @ rsyl chopT_min @ ssel @ Bitsss minle1) @
syl5eq chop_bitOr @ bitOreqd (a1i chop_bitDif1) @
eqcomd @ syl5eq chop_shl @ chopeq1d @ syl5eq addcom anl);
theorem chop_bitsUpdate_id:
$ chop k (bitsUpdate k m a n) = chop k n $ =
'(eqtr (chopeq2 addcom) @ eqtr chop_shladd2 @ eqtr chop_bitDif @
eqtr (bitDifeq2 @ chop_shl_0 leid) bitDif02);
theorem chop_bitsUpdate_1: $ i <= k -> chop i (bitsUpdate k m a n) = chop i n $ =
'(eqtr3d chop_chop @ syl5eq (chopeq2 chop_bitsUpdate_id) chop_chop);
theorem bitsUpdate01: $ bitsUpdate 0 m a n = bitDif n (upto m) + a $ =
'(addeq (bitDifeq2 shl02) shl02);
theorem bitsUpdate01_: $ bitsUpdate 0 m a n = shl (shr n m) m + a $ =
'(eqtr bitsUpdate01 @ addeq1 bitDif_upto);
theorem el_bitsUpdate_1: $ i < k -> (i e. bitsUpdate k m a n <-> i e. n) $ =
'(bitr3d bian1 @ syl5bb (bitr3 el_chop @ bitr (elneq2 chop_bitsUpdate_id) el_chop) bian1);
theorem el_bitsUpdate_2: $ i < m -> (k + i e. bitsUpdate k m a n <-> i e. a) $ =
'(syl5bb (eleq1 addcom) @ syl5bbr elshr @
syl5bb (elneq2 @ eqtr3 (shreq1 @ bitsUpdateeq1 add01) @ eqtr shr_bitsUpdate bitsUpdate01_) @
bitr3d bian1 @ syl5bbr el_chop @ syl5bb (elneq2 chop_shladd2) @ syl5bb el_chop bian1);
theorem el_bitsUpdate_3: $ a e. Bits m /\ k + m <= i ->
(i e. bitsUpdate k m a n <-> i e. n) $ =
(focus
(def (f x) '(imp @ con2d @ syl5bi elshl @ exp @ sylib ltnle @
mpbid (syl ltsubadd2 anrl) @ sylib elupto @ sylc ssel (sylib elBits ,x) anrr))
'(bitrd (elneq2d @ anwl bitsUpdate_or) @ syl5bb elbitOr @
bitrd (syl bior2 ,(f 'anl)) @ syl5bb elbitDif @ syl bian2 ,(f '(a1i uptoT))));
theorem el_bitsUpdate1_eq: $ k e. bitsUpdate k 1 (nat p) n <-> p $ =
'(bitr3 (eleq1 add0) @ bitr (el_bitsUpdate_2 d0lt1) @ bitr el01 oddnat);
theorem el_bitsUpdate1_ne: $ i != k -> (i e. bitsUpdate k 1 (nat p) n <-> i e. n) $ =
'(sylbi neltlt @ eor el_bitsUpdate_1 @ sylbir (leeq1 add12) @
exp el_bitsUpdate_3 @ mpbir elBits1 boolnat);
@(add-eval @ fn (n v) @ match (eval k) [0 #f] [k {{{(eval n) shr {k - 1}} band 1} = 1}])
@_ def bitsNot (k n: nat): nat = $ bitDif (upto k) n $;
pub theorem bitsNot_mem (k n i: nat): $ i e. bitsNot k n <-> i < k /\ ~i e. n $ =
'(bitr elbitDif @ aneq1i elupto);
pub theorem bitsNotT (k n: nat): $ bitsNot k n e. Bits k $ = '(bitDifT uptoT);
theorem bitsNot_chop: $ bitsNot k (chop k n) = bitsNot k n $ =
'(eqtr3 (bitsNoteq2 bitAnd_upto) bitDifAndid);
theorem bitsNot_add: $ n e. Bits k -> bitsNot k n + n = upto k $ = '(sylbi elBits bitDifadd);
theorem bitsNot_sub: $ n e. Bits k -> bitsNot k n = upto k - n $ = '(sylbi elBits bitDifsub);
theorem bitsNot0: $ bitsNot k 0 = upto k $ = '(eqtr (bitsNot_sub elBits01) sub02);
theorem bitsNot01: $ bitsNot 0 n = 0 $ = '(eqtr (bitDifeq1 upto0) bitDif01);
theorem chop_bitsNot: $ m <= k -> chop m (bitsNot k n) = bitsNot m n $ =
'(syl5eq chop_bitDif1 @ sylbi chop_upto bitDifeq1);
theorem shl_bitsNot: $ shl (bitsNot k a) m + upto m = bitsNot (k + m) (shl a m) $ =
'(eqtr3 (addeq1 @ shleq1 bitsNot_chop) @ eqtr (mpbi addcan1 @
eqtr4 addrass @ eqtr4 (eqtr4 (bitsNot_add chopT) shlupto) @ addeq1 @
eqtr3 (addeq2 chop_shl) @ eqtr3 shladd @ shleq1 @ bitsNot_add chopT) bitsNot_chop);
theorem shr_bitsNot: $ shr (bitsNot k a) m = bitsNot (k - m) (shr a m) $ =
'(eqtr shr_bitDif @ bitDifeq1 shrupto);
theorem zeqm_bitsNot: $ modZ(2 ^ k): b0 (bitsNot k n) = -uZ b0 (suc n) $ =
'(zeqmtr
(mpbi zeqmsub @ mpbir (zeqmeq2 @ eqtr zsubneg2 @ eqtr zaddb0 @
b0eq @ eqtr addS @ eqtr (suceq @ eqtr3 (addeq1 bitsNot_chop) @ bitsNot_add chopT) @
sucupto) zeqmid0)
(mpbir zeqmneg @ mpbir zeqmeqm @ mpbir eqmsuc eqm_chop));
theorem zeqm_bitsNot2: $ modZ(2 ^ k): b0 (bitsNot k n) = b1 n $ =
'(zeqmtr zeqm_bitsNot @ eqzeqm znegb0S);
theorem chopZ_b1_bitsNot: $ chopZ k (b1 n) = bitsNot k n $ =
'(mpbi (Bits_zeqm @ ian chopZT bitsNotT) @ zeqmtr zeqm_chopZ @ zeqmcom zeqm_bitsNot2);
theorem zeqm_bitsNotd
(h1: $ G -> modZ(2 ^ k): b0 a = x $):
$ G -> modZ(2 ^ k): b0 (bitsNot k a) = -uZ (x +Z b0 1) $ =
'(syl (zeqmtr zeqm_bitsNot) @ sylibr zeqmneg @
sylib (zeqmeq2 @ eqtr zaddb0 @ b0eq add12) @ zeqmadd1d h1);
theorem bitsNot4_h2n (a: hex): $ bitsNot 4 a + a = xf $ =
'(eqtr (bitsNot_add h2nT) @ upto4);
theorem bitsNot4_hex: $ bitsNot 4 (a :x b) + b = xf $ =
'(eqtr (addeq1 @ eqtr3 bitsNot_chop @ bitsNoteq2 chop4hex) bitsNot4_h2n);
theorem bitsNot_hex: $ b + c = xf -> bitsNot (k + 4) (a :x b) = bitsNot k a :x c $ =
'(syl5eqr shlshr_chop @ syl6eqr hexshl4 @
addeqd (a1i @ shleq1 @ eqtr shr_bitsNot @ bitsNoteq pncan shrhex4)
(syl5eq (chop_bitsNot leaddid2) @ sylib addcan1 @ syl6eq addcom @
eqtr4d (a1i bitsNot4_hex) id));
theorem xbitNotS (h0: $ a + b = xf $) (h1: $ c = bitsNot k n $):
$ c :x b = bitsNot (k + 4) (n :x a) $ = '(eqtr4 (hexeq1 h1) (bitsNot_hex h0));
theorem xbitNot1 (h0: $ a + h2n b = xf $): $ b = bitsNot 4 (n :x a) $ =
'(eqtr3 hex01_ @ eqtr (xbitNotS h0 @ eqcom bitsNot01) @ bitsNoteq1 add01);
theorem xbitNot_ch (h0: $ a0 + c0 = xf $) (h1: $ a1 + c1 = xf $):
$ c2n (ch c1 c0) = bitsNot 8 (n :x a1 :x a0) $ =
'(eqtr c2nch @ eqtr (xbitNotS h0 @ xbitNot1 h1) @ bitsNoteq1 d4add4);
@(add-eval @ fn (k a b) {{(eval a) + (eval b)} band {{1 shl (eval k)} - 1}})
@_ def bitsAdd (k a b: nat): nat = $ chop k (a + b) $;
pub theorem bitsAddT (k a b: nat): $ bitsAdd k a b e. Bits k $ = 'chopT;
theorem bitsAdd_eqid: $ a + b e. Bits k -> bitsAdd k a b = a + b $ = 'Bits_chop;
theorem eqm_bitsAdd: $ mod(2 ^ k): bitsAdd k a b = a + b $ = 'eqm_chop;
theorem zeqm_bitsAdd: $ modZ(2 ^ k): b0 (bitsAdd k a b) = b0 a +Z b0 b $ =
'(mpbir (zeqmeq3 zaddb0) @ mpbir zeqmeqm eqm_bitsAdd);
theorem eqm_bitsAddd
(h1: $ G -> mod(2 ^ k): a = x $) (h2: $ G -> mod(2 ^ k): b = y $):
$ G -> mod(2 ^ k): bitsAdd k a b = x + y $ =
'(syl (eqmtr eqm_bitsAdd) @ eqmaddd h1 h2);
theorem zeqm_bitsAddd
(h1: $ G -> modZ(2 ^ k): b0 a = x $) (h2: $ G -> modZ(2 ^ k): b0 b = y $):
$ G -> modZ(2 ^ k): b0 (bitsAdd k a b) = x +Z y $ =
'(syl (zeqmtr zeqm_bitsAdd) @ zeqmaddd h1 h2);
theorem bitsAdd02: $ bitsAdd k 0 a = chop k a $ = '(chopeq2 add01);
theorem bitsAdd03: $ bitsAdd k a 0 = chop k a $ = '(chopeq2 add0);
@(add-eval @ fn (k n) {(- (eval n)) band {{1 shl (eval k)} - 1}})
@_ def bitsNeg (k n: nat): nat = $ bitsAdd k (bitsNot k n) 1 $;
pub theorem bitsNegT (k n: nat): $ bitsNeg k n e. Bits k $ = 'bitsAddT;
theorem zeqm_bitsNegd
(h1: $ G -> modZ(2 ^ k): b0 a = x $):
$ G -> modZ(2 ^ k): b0 (bitsNeg k a) = -uZ x $ =
'(sylib (zeqmeq3 @ eqtr (zaddeq1 znegadd) znpcan) @
zeqm_bitsAddd (zeqm_bitsNotd h1) (a1i zeqmid));
theorem zeqm_bitsNeg: $ modZ(2 ^ k): b0 (bitsNeg k n) = -uZ b0 n $ =
'(trud @ zeqm_bitsNegd @ a1i zeqmid);
theorem bitsNeg0: $ bitsNeg k 0 = 0 $ =
'(mpbi (Bits_zeqm_02 bitsNegT) @
mpbi (zeqmeq3 @ eqtr (znegeq b00) zneg0) zeqm_bitsNeg);
theorem bitsNeg1: $ bitsNeg k 1 = upto k $ =
'(mpbi (Bits_zeqm @ ian bitsNegT uptoT) @
zeqmtr zeqm_bitsNeg @ zeqmcom @ mpbi zeqmsub @
mpbir (zeqmeq2 @ eqtr zsubneg2 @ eqtr zaddb0 @ b0eq uptoadd1) zeqmid0);
@(add-eval @ fn (k a b) {{(eval a) - (eval b)} band {{1 shl (eval k)} - 1}})
@_ def bitsSub (k a b: nat): nat = $ bitsAdd k a (bitsNeg k b) $;
pub theorem bitsSubT (k a b: nat): $ bitsSub k a b e. Bits k $ = 'bitsAddT;
theorem zeqm_bitsSubd
(h1: $ G -> modZ(2 ^ k): b0 a = x $) (h2: $ G -> modZ(2 ^ k): b0 b = y $):
$ G -> modZ(2 ^ k): b0 (bitsSub k a b) = x -Z y $ =
'(zeqm_bitsAddd h1 @ zeqm_bitsNegd h2);
theorem zeqm_bitsSub2: $ modZ(2 ^ k): b0 (bitsSub k a b) = b0 a -Z b0 b $ =
'(trud @ zeqm_bitsSubd (a1i zeqmid) (a1i zeqmid));
theorem zeqm_bitsSub: $ modZ(2 ^ k): b0 (bitsSub k a b) = a -ZN b $ =
'(mpbi (zeqmeq3 zsubb0) zeqm_bitsSub2);
theorem bitsSub_eq_sub: $ b <= a -> a e. Bits k -> bitsSub k a b = a - b $ =
'(exp @ mpbid (sylan Bits_zeqm (a1i bitsSubT) @ anwr @ Bitsle1 subleid) @
mpbii zeqm_bitsSub @ zeqmeq3d @ anwl znsubpos);
theorem bitsSub03: $ bitsSub k a 0 = chop k a $ = '(eqtr (bitsAddeq3 bitsNeg0) bitsAdd03);
theorem bits_npcan: $ bitsAdd k (bitsSub k a b) b = chop k a $ =
'(mpbi (zeqm_chop2 bitsAddT) @ mpbi (zeqmeq3 znpcan) @
trud @ zeqm_bitsAddd (a1i zeqm_bitsSub2) (a1i zeqmid));
theorem bits_pncan: $ bitsSub k (bitsAdd k a b) b = chop k a $ =
'(mpbi (zeqm_chop2 bitsAddT) @ mpbi (zeqmeq3 zpncan) @
trud @ zeqm_bitsSubd (a1i zeqm_bitsAdd) (a1i zeqmid));
@_ def bitsSar (k a b: nat): nat =
$ nat (bitsMSB k a) * (upto k - upto (k - b)) + shr a b $;
pub theorem bitsSarT (k a b: nat):
$ a e. Bits k /\ b <= k -> bitsSar k a b e. Bits k $ =
'(sylibr elBits2 @
sylibr (lteq2 @ eqtr3 uptoadd1 @
eqtr3 (addeq1 @ npcan @ mpbi leupto subleid) @ eqtr addass @ addeq2 uptoadd1) @
leltaddd (a1i @ mpbi (leeq2 mul11) (lemul1a natle1)) @
sylib elBits2 @ syl shrT @ mpbird (elneq2d @ Bitseqd @ anwr npcan) anl);
@(add-eval @ fn (a b) {{(eval a) + (eval b)} band {{1 shl 64} - 1}})
@_ def add64 (a b: nat): nat = $ bitsAdd 64 a b $; infixl add64: $+_64$ prec 64;
pub theorem add64T (a b: nat): $ a +_64 b e. u64 $ = 'bitsAddT;
theorem add64_eqid: $ a + b e. u64 -> a +_64 b = a + b $ = 'bitsAdd_eqid;
theorem add64S_eqid: $ suc a e. u64 -> a +_64 1 = suc a $ =
'(sylbir (eleq1 add12) @ syl6eq add12 add64_eqid);
@(add-eval @ fn (a b) {{(eval a) - (eval b)} band {{1 shl 64} - 1}})
@_ def sub64 (a b: nat): nat = $ bitsSub 64 a b $; infixl sub64: $-_64$ prec 64;
pub theorem sub64T (a b: nat): $ a -_64 b e. u64 $ = 'bitsSubT;
theorem sub64_eqid: $ b <= a -> a e. u64 -> a -_64 b = a - b $ = 'bitsSub_eq_sub;
theorem sub02_64: $ a -_64 0 = chop 64 a $ = 'bitsSub03;
theorem npcan64: $ a -_64 b +_64 b = chop 64 a $ = 'bits_npcan;
theorem pncan64: $ a +_64 b -_64 b = chop 64 a $ = 'bits_pncan;
@_ local def toBytesAux (k n .a: nat): nat = $ rec 0 (\ a,
\. i e. upto (suc n), (i % 256) : a @ (i // 256)) k $;
theorem toBytesAux0: $ toBytesAux 0 n = 0 $ = (named 'rec0);
theorem toBytesAux0_app: $ toBytesAux 0 n @ i = 0 $ =
'(eqtr (appneq1 toBytesAux0) app01);
theorem toBytesAuxS: $ toBytesAux (suc k) n =
\. i e. upto (suc n), (i % 256) : toBytesAux k n @ (i // 256) $ =
'(eqtr {recS : $ _ = _ @ toBytesAux k n $} @
!! applame a @ lowereqd @ reseq1d @ lameqd @ conseq2d @ appeq1d nseq);
theorem toBytesAuxS_app: $ a <= n ->
toBytesAux (suc k) n @ a = (a % 256) : toBytesAux k n @ (a // 256) $ =
'(syl5eq (appneq1 toBytesAuxS) @
sylbi leltsuc @ sylbir elupto @ !! apprlame x @ conseqd modeq1 @ appeq2d diveq1);
--| Little endian encoding
@_ abstract def toBytes (k n: nat): nat = $ toBytesAux k n @ n $;
pub theorem toBytes0 (n: nat): $ toBytes 0 n = 0 $ = 'toBytesAux0_app;
theorem toBytesAuxS_eq: $ a <= n -> toBytesAux k n @ a = toBytes k a $ =
(named @ focus
'(!! eale x (imeqd leeq1 @ imeqd leeq1 @ eqeqd appeq2 appeq2)
,(induct '(ind) 'k
'(ax_gen @ a1i @ a1i @ eqtr4 toBytesAux0_app toBytesAux0_app)
'(sylbi (cbval ,eqtac) @
ialda @ exp @ eqtr4d (anwr toBytesAuxS_app) @
eqtr4d (syl toBytesAuxS_app anlr) @
conseq2d @
mpd (letrd (a1i divleid) anr) @ mpd (letrd (a1i divleid) anlr) @
anwll @ eale ,eqtac))
leid));
pub theorem toBytesS (k n: nat):
$ toBytes (suc k) n = (n % 256) : toBytes k (n // 256) $ =
'(eqtr (toBytesAuxS_app leid) @ conseq2 @ toBytesAuxS_eq divleid);
theorem toBytesS2: $ toBytes (suc k) n = chop 8 n : toBytes k (shr n 8) $ = 'toBytesS;
theorem toBytes02: $ toBytes k 0 = repeat 0 k $ =
(named @ induct '(ind) 'k
'(eqtr4 toBytes0 repeat0)
'(syl5eq toBytesS @ syl5eq (conseq mod01 @ toByteseq2 div01) @
syl6eqr repeatS conseq2));
pub theorem toBytesT (k n: nat): $ toBytes k n e. Array u8 k $ =
'(!! eale x (eleq1d toByteseq2) ,(induct '(!! ind y z) 'k
'(ax_gen @ mpbir (eleq1 toBytes0) elArray0)
'(sylbi (!! cbval _ y @ eleq1d toByteseq2) @ iald @
sylibr (eleq1 toBytesS) @ syl (sylibr elArrayS @ ian mod_el_u8) @
eale @ eleq1d toByteseq2)));
theorem toBytesT2: $ toBytes k n e. List u8 $ = '(elArrayList toBytesT);
theorem toBytes_len: $ len (toBytes k n) = k $ = '(elArraylen toBytesT);
theorem toBytes1: $ toBytes 1 n = chop 8 n : 0 $ =
'(eqtr toBytesS @ conseq2 toBytes0);
theorem toBytes_chop: $ toBytes k (chop (8 * k) n) = toBytes k n $ =
(named '(ax_mp (!! eale x ,(eqtac-gen 'n)) ,(induct '(ind) 'k
'(ax_gen @ eqtr4 toBytes0 toBytes0)
'(sylbi (cbval ,eqtac) @ iald @ eqtr4g toBytesS2 toBytesS2 @ conseqd
(a1i @ chop_chop @ mpbi (leeq1 mul12) @ lemul2a le11S)
(sylibr (eqeq1 @ toByteseq2 @ eqtr (shreq1 @ chopeq1 mulS) chop_shr) @
eale ,eqtac)))));
theorem toBytes_inj2: $ toBytes k a = toBytes k b <-> chop (8 * k) a = chop (8 * k) b $ =
(named @ focus
'(ibii _ @ eqtr3g toBytes_chop toBytes_chop toByteseq2)
'(ax_mp (!! eale y ,(eqtac-gen 'b)) @ ax_mp (!! eale x ,(eqtac-gen 'a)) _)
(induct '(ind) 'k
'(ax_gen @ ax_gen @ eqtr4g (chopeq1 mul02) (chopeq1 mul02) @ a1i @ eqtr4 chop01 chop01)
'(sylbi (cbval @ cbvald ,eqtac) @ iald @ iald @
ealie @ ealde @ syl6 _ @ bi1d ,eqtac))
'(syl5bi (eqeq toBytesS2 toBytesS2) @ syl5bi consinj @
impd @ com12 @ imim2d @ exp @ eqtr4g (chopeq1 mulS) (chopeq1 mulS) @
eqtr3g shlshr_chop shlshr_chop @ addeqd (shleq1d @ eqtr4g chop_shr chop_shr anr) @
eqtr4g (chop_chop leaddid2) (chop_chop leaddid2) anl));
theorem toBytes_inj: $ toBytes k a = toBytes k b <-> mod(2 ^ (8 * k)): a = b $ =
'(bitr toBytes_inj2 chop_eq_chop);
theorem toBytesS_bitsNot: $ toBytes (suc k) (bitsNot (8 * suc k) n) =
bitsNot 8 n : toBytes k (bitsNot (8 * k) (shr n 8)) $ =
'(eqtr toBytesS2 @ conseq
(chop_bitsNot @ mpbi (leeq1 mul12) @ lemul2a le11S)
(toByteseq2 @ eqtr shr_bitsNot @ bitsNoteq1 @ eqtr (subeq1 mulS2) pncan));
theorem s2n_toBytesS0 (h: $ c = a $) (h2: $ s = repeat 0 k $):
$ c ': s = toBytes (suc k) a $ =
'(eqtr (s2n_S (eqcom @ modltid @ mpbi elu8_2 c2nT) @
eqtr4 h2 @ eqtr (toByteseq2 @ divlteq0 @ mpbi elu8_2 c2nT) toBytes02) @
eqtr3 toBytesS @ toByteseq2 h);
theorem xtoBytes0: $ s0 = toBytes 0 a $ = '(eqtr4 s2ns0 toBytes0);
theorem xtoBytesS (h: $ s = toBytes k n $): $ ch a1 a0 ': s = toBytes (suc k) (n :x a1 :x a0) $ =
'(eqtr4 (s2n_S (eqtr4 c2nhex @ anr hex_divmod256) @
eqtr4 h @ toByteseq2 @ anl hex_divmod256) toBytesS);
theorem xtoBytesS2 (h: $ s = toBytes k x0 $): $ ch a1 a0 ': s = toBytes (suc k) (a1 :x a0) $ =
'(eqtr (xtoBytesS h) @ toByteseq2 @ hexeq1 hex01);
theorem xtoBytesS1 (h: $ s = toBytes k x0 $): $ ch x0 a0 ': s = toBytes (suc k) a0 $ =
'(eqtr (xtoBytesS2 h) @ toByteseq2 hex01);
theorem xtoBytes1S: $ s1 (ch a1 a0) = toBytes (suc 0) (n :x a1 :x a0) $ =
'(eqtr3 s2nscons0 @ xtoBytesS xtoBytes0);
theorem xtoBytes12: $ s1 (ch a1 a0) = toBytes (suc 0) (a1 :x a0) $ =
'(eqtr3 s2nscons0 @ xtoBytesS2 xtoBytes0);
theorem xtoBytes11: $ s1 (ch x0 a0) = toBytes (suc 0) a0 $ =
'(eqtr xtoBytes12 @ toByteseq2 hex01);
--| `(to-toBytes k n)` returns `(s p)` where `p: s2n s = toBytes k n`.
--| Note that `k` should be a unary numeral constructed by `(sucs)`
do (def (to-toBytes k n) @ match k
[$suc ,k$ @ match k
[$0$ @ match n
[$,n :x ,a1 :x ,a0$ '($s1 (ch ,a1 ,a0)$ (xtoBytes1S ,a0 ,a1 ,n))]
[$h2n ,a1 :x ,a0$ '($s1 (ch ,a1 ,a0)$ (xtoBytes12 ,a0 ,a1))]
[$h2n ,a0$ '($s1 (ch ,'(x0) ,a0)$ (xtoBytes11 ,a0))]]
[_ @ match n
[$,n :x ,a1 :x ,a0$ @ match (to-toBytes k n) @ (s p)
'($ch ,a1 ,a0 ': ,s$ (xtoBytesS ,a0 ,a1 ,k ,n ,s ,p))]
[$h2n ,a1 :x ,a0$ @ match (to-toBytes k '(h2n @ x0)) @ (s p)
'($ch ,a1 ,a0 ': ,s$ (xtoBytesS2 ,a0 ,a1 ,k ,s ,p))]
[$h2n ,a0$ @ match (to-toBytes k '(h2n @ x0)) @ (s p)
'($ch ,'(x0) ,a0 ': ,s$ (xtoBytesS1 ,a0 ,k ,s ,p))]]]
[$0$ '($s0$ (xtoBytesS1 ,n))]);
@_ def u16Bytes (n: nat): nat = $ toBytes 2 n $;
@_ def u32Bytes (n: nat): nat = $ toBytes 4 n $;
@_ def u64Bytes (n: nat): nat = $ toBytes 8 n $;
theorem u16BytesT: $ u16Bytes n e. Array u8 2 $ = 'toBytesT;
theorem u32BytesT: $ u32Bytes n e. Array u8 4 $ = 'toBytesT;
theorem u64BytesT: $ u64Bytes n e. Array u8 8 $ = 'toBytesT;
theorem u16BytesList: $ u16Bytes n e. List u8 $ = '(elArrayList u16BytesT);
theorem u32BytesList: $ u32Bytes n e. List u8 $ = '(elArrayList u32BytesT);
theorem u64BytesList: $ u64Bytes n e. List u8 $ = '(elArrayList u64BytesT);
theorem u16Bytes_len: $ len (u16Bytes n) = 2 $ = 'toBytes_len;
theorem u32Bytes_len: $ len (u32Bytes n) = 4 $ = 'toBytes_len;
theorem u64Bytes_len: $ len (u64Bytes n) = 8 $ = 'toBytes_len;
theorem xu16Bytes (h: $ s2n s = toBytes ,(sucs 2) n $): $ s = u16Bytes n $ = 'h;
theorem xu32Bytes (h: $ s2n s = toBytes ,(sucs 4) n $): $ s = u32Bytes n $ = 'h;
theorem xu64Bytes (h: $ s2n s = toBytes ,(sucs 8) n $): $ s = u64Bytes n $ = 'h;
--| `(to-uNBytes N a)` returns a pair `(s p)` where `p: s2n s = uNBytes a`
--| assuming `N = 16,32,64`
do (def (to-uNBytes n a)
(def k (sucs {n // 8}))
@ match (to-toBytes k a) @ (s p)
'(,s (,(atom-app 'xu n 'Bytes) ,a ,s ,p)));
@_ local def toIBytes (k n: nat): nat = $ toBytes k (chopZ (8 * k) n) $;
@_ local def i8Bytes (n: nat): nat = $ toIBytes 1 n $;
@_ local def i16Bytes (n: nat): nat = $ toIBytes 2 n $;
@_ local def i32Bytes (n: nat): nat = $ toIBytes 4 n $;
@_ local def i64Bytes (n: nat): nat = $ toIBytes 8 n $;
theorem i8Bytes_val2: $ i8Bytes n = toBytes 1 (chopZ 8 n) $ = '(toByteseq2 @ chopZeq1 mul12);
theorem i16Bytes_val: $ i16Bytes n = toBytes 2 (chopZ 16 n) $ = '(toByteseq2 @ chopZeq1 d8mul2);
theorem i32Bytes_val: $ i32Bytes n = toBytes 4 (chopZ 32 n) $ = '(toByteseq2 @ chopZeq1 d8mul4);
theorem i64Bytes_val: $ i64Bytes n = toBytes 8 (chopZ 64 n) $ = '(toByteseq2 @ chopZeq1 d8mul8);
theorem i8Bytes_val (n: nat): $ i8Bytes n = chopZ 8 n : 0 $ =