1use oxilean_kernel::{BinderInfo, Declaration, Environment, Expr, Level, Name};
6
7use super::functions::*;
8use super::types::*;
9
10#[allow(dead_code)]
30#[allow(clippy::too_many_lines)]
31pub fn register_bitvec_extended_axioms(env: &mut Environment) {
32 let mut add = |name: &str, ty: Expr| {
33 let _ = add_axiom(env, name, vec![], ty);
34 };
35 add("BitVec.arithShiftRight", bvx_ext_arith_shift_right_ty());
36 add(
37 "BitVec.shiftLeft_zero_amount",
38 bvx_ext_forall_one(|| {
39 mk_bv_eq(
40 bvar(1),
41 app2(cst("BitVec.shiftLeft"), bvar(0), cst("Nat.zero")),
42 bvar(0),
43 )
44 }),
45 );
46 add(
47 "BitVec.shiftRight_zero_amount",
48 bvx_ext_forall_one(|| {
49 mk_bv_eq(
50 bvar(1),
51 app2(cst("BitVec.shiftRight"), bvar(0), cst("Nat.zero")),
52 bvar(0),
53 )
54 }),
55 );
56 add(
57 "BitVec.arithShiftRight_zero_amount",
58 bvx_ext_forall_one(|| {
59 mk_bv_eq(
60 bvar(1),
61 app2(cst("BitVec.arithShiftRight"), bvar(0), cst("Nat.zero")),
62 bvar(0),
63 )
64 }),
65 );
66 add(
67 "BitVec.shiftLeft_ge_width",
68 bvx_ext_forall_bv_nat(|| {
69 arrow(
70 app3(
71 cst("Eq"),
72 bool_ty(),
73 app2(cst("Nat.ble"), bvar(2), bvar(0)),
74 cst("true"),
75 ),
76 mk_bv_eq(
77 bvar(2),
78 app2(cst("BitVec.shiftLeft"), bvar(1), bvar(0)),
79 app(cst("BitVec.zero"), bvar(2)),
80 ),
81 )
82 }),
83 );
84 add(
85 "BitVec.add_mod",
86 pi(
87 BinderInfo::Implicit,
88 "n",
89 nat_ty(),
90 pi(
91 BinderInfo::Default,
92 "a",
93 mk_bitvec(bvar(0)),
94 pi(
95 BinderInfo::Default,
96 "b",
97 mk_bitvec(bvar(1)),
98 mk_nat_eq(
99 app(
100 cst("BitVec.toNat"),
101 app2(cst("BitVec.add"), bvar(1), bvar(0)),
102 ),
103 app2(
104 cst("Nat.mod"),
105 app2(
106 cst("Nat.add"),
107 app(cst("BitVec.toNat"), bvar(1)),
108 app(cst("BitVec.toNat"), bvar(0)),
109 ),
110 app2(
111 cst("Nat.pow"),
112 app(cst("Nat.succ"), app(cst("Nat.succ"), cst("Nat.zero"))),
113 bvar(2),
114 ),
115 ),
116 ),
117 ),
118 ),
119 ),
120 );
121 add(
122 "BitVec.add_neg_cancel",
123 bvx_ext_forall_one(|| {
124 mk_bv_eq(
125 bvar(1),
126 app2(cst("BitVec.add"), bvar(0), app(cst("BitVec.neg"), bvar(0))),
127 app(cst("BitVec.zero"), bvar(1)),
128 )
129 }),
130 );
131 add(
132 "BitVec.mul_comm",
133 pi(
134 BinderInfo::Implicit,
135 "n",
136 nat_ty(),
137 pi(
138 BinderInfo::Default,
139 "a",
140 mk_bitvec(bvar(0)),
141 pi(
142 BinderInfo::Default,
143 "b",
144 mk_bitvec(bvar(1)),
145 mk_bv_eq(
146 bvar(2),
147 app2(cst("BitVec.mul"), bvar(1), bvar(0)),
148 app2(cst("BitVec.mul"), bvar(0), bvar(1)),
149 ),
150 ),
151 ),
152 ),
153 );
154 add(
155 "BitVec.mul_assoc",
156 pi(
157 BinderInfo::Implicit,
158 "n",
159 nat_ty(),
160 pi(
161 BinderInfo::Default,
162 "a",
163 mk_bitvec(bvar(0)),
164 pi(
165 BinderInfo::Default,
166 "b",
167 mk_bitvec(bvar(1)),
168 pi(
169 BinderInfo::Default,
170 "c",
171 mk_bitvec(bvar(2)),
172 mk_bv_eq(
173 bvar(3),
174 app2(
175 cst("BitVec.mul"),
176 app2(cst("BitVec.mul"), bvar(2), bvar(1)),
177 bvar(0),
178 ),
179 app2(
180 cst("BitVec.mul"),
181 bvar(2),
182 app2(cst("BitVec.mul"), bvar(1), bvar(0)),
183 ),
184 ),
185 ),
186 ),
187 ),
188 ),
189 );
190 add(
191 "BitVec.mul_mod",
192 pi(
193 BinderInfo::Implicit,
194 "n",
195 nat_ty(),
196 pi(
197 BinderInfo::Default,
198 "a",
199 mk_bitvec(bvar(0)),
200 pi(
201 BinderInfo::Default,
202 "b",
203 mk_bitvec(bvar(1)),
204 mk_nat_eq(
205 app(
206 cst("BitVec.toNat"),
207 app2(cst("BitVec.mul"), bvar(1), bvar(0)),
208 ),
209 app2(
210 cst("Nat.mod"),
211 app2(
212 cst("Nat.mul"),
213 app(cst("BitVec.toNat"), bvar(1)),
214 app(cst("BitVec.toNat"), bvar(0)),
215 ),
216 app2(
217 cst("Nat.pow"),
218 app(cst("Nat.succ"), app(cst("Nat.succ"), cst("Nat.zero"))),
219 bvar(2),
220 ),
221 ),
222 ),
223 ),
224 ),
225 ),
226 );
227 add(
228 "BitVec.ult_irrefl",
229 bvx_ext_forall_one(|| {
230 mk_eq(
231 bool_ty(),
232 app2(cst("BitVec.ult"), bvar(0), bvar(0)),
233 cst("false"),
234 )
235 }),
236 );
237 add(
238 "BitVec.ule_refl",
239 bvx_ext_forall_one(|| {
240 mk_eq(
241 bool_ty(),
242 app2(cst("BitVec.ule"), bvar(0), bvar(0)),
243 cst("true"),
244 )
245 }),
246 );
247 add(
248 "BitVec.ult_ule",
249 pi(
250 BinderInfo::Implicit,
251 "n",
252 nat_ty(),
253 pi(
254 BinderInfo::Default,
255 "a",
256 mk_bitvec(bvar(0)),
257 pi(
258 BinderInfo::Default,
259 "b",
260 mk_bitvec(bvar(1)),
261 arrow(
262 mk_eq(
263 bool_ty(),
264 app2(cst("BitVec.ult"), bvar(1), bvar(0)),
265 cst("true"),
266 ),
267 mk_eq(
268 bool_ty(),
269 app2(cst("BitVec.ule"), bvar(1), bvar(0)),
270 cst("true"),
271 ),
272 ),
273 ),
274 ),
275 ),
276 );
277 add(
278 "BitVec.slt_irrefl",
279 bvx_ext_forall_one(|| {
280 mk_eq(
281 bool_ty(),
282 app2(cst("BitVec.slt"), bvar(0), bvar(0)),
283 cst("false"),
284 )
285 }),
286 );
287 add(
288 "BitVec.sle_refl",
289 bvx_ext_forall_one(|| {
290 mk_eq(
291 bool_ty(),
292 app2(cst("BitVec.sle"), bvar(0), bvar(0)),
293 cst("true"),
294 )
295 }),
296 );
297 add(
298 "BitVec.append_assoc",
299 pi(
300 BinderInfo::Implicit,
301 "n",
302 nat_ty(),
303 pi(
304 BinderInfo::Implicit,
305 "m",
306 nat_ty(),
307 pi(
308 BinderInfo::Implicit,
309 "k",
310 nat_ty(),
311 pi(
312 BinderInfo::Default,
313 "a",
314 mk_bitvec(bvar(2)),
315 pi(
316 BinderInfo::Default,
317 "b",
318 mk_bitvec(bvar(2)),
319 pi(
320 BinderInfo::Default,
321 "c",
322 mk_bitvec(bvar(2)),
323 mk_bv_eq(
324 app2(
325 cst("Nat.add"),
326 app2(cst("Nat.add"), bvar(5), bvar(4)),
327 bvar(3),
328 ),
329 app2(
330 cst("BitVec.append"),
331 app2(cst("BitVec.append"), bvar(2), bvar(1)),
332 bvar(0),
333 ),
334 app2(
335 cst("BitVec.append"),
336 bvar(2),
337 app2(cst("BitVec.append"), bvar(1), bvar(0)),
338 ),
339 ),
340 ),
341 ),
342 ),
343 ),
344 ),
345 ),
346 );
347 add(
348 "BitVec.extractLsb_full",
349 bvx_ext_forall_nat_bv(|| {
350 mk_bv_eq(
351 bvar(1),
352 app3(
353 cst("BitVec.extractLsb"),
354 app2(
355 cst("Nat.sub"),
356 bvar(1),
357 app(cst("Nat.succ"), cst("Nat.zero")),
358 ),
359 cst("Nat.zero"),
360 bvar(0),
361 ),
362 app2(cst("BitVec.setWidth"), bvar(1), bvar(0)),
363 )
364 }),
365 );
366 add("BitVec.zeroExtend", bvx_ext_zero_extend_ty());
367 add(
368 "BitVec.zeroExtend_ge_id",
369 bvx_ext_forall_nat_bv(|| {
370 mk_bv_eq(
371 bvar(1),
372 app2(cst("BitVec.zeroExtend"), bvar(1), bvar(0)),
373 bvar(0),
374 )
375 }),
376 );
377 add(
378 "BitVec.signExtend_ge_id",
379 bvx_ext_forall_nat_bv(|| {
380 mk_bv_eq(
381 bvar(1),
382 app2(cst("BitVec.signExtend"), bvar(1), bvar(0)),
383 bvar(0),
384 )
385 }),
386 );
387 add(
388 "BitVec.toFin",
389 pi(
390 BinderInfo::Implicit,
391 "n",
392 nat_ty(),
393 arrow(mk_bitvec(bvar(0)), bvx_ext_fin2n(bvar(0))),
394 ),
395 );
396 add(
397 "BitVec.ofFin",
398 pi(
399 BinderInfo::Implicit,
400 "n",
401 nat_ty(),
402 arrow(bvx_ext_fin2n(bvar(0)), mk_bitvec(bvar(0))),
403 ),
404 );
405 add(
406 "BitVec.toFin_ofFin",
407 pi(
408 BinderInfo::Implicit,
409 "n",
410 nat_ty(),
411 pi(
412 BinderInfo::Default,
413 "f",
414 bvx_ext_fin2n(bvar(0)),
415 mk_eq(
416 bvx_ext_fin2n(bvar(1)),
417 app(cst("BitVec.toFin"), app(cst("BitVec.ofFin"), bvar(0))),
418 bvar(0),
419 ),
420 ),
421 ),
422 );
423 add(
424 "BitVec.ofFin_toFin",
425 bvx_ext_forall_one(|| {
426 mk_bv_eq(
427 bvar(1),
428 app(cst("BitVec.ofFin"), app(cst("BitVec.toFin"), bvar(0))),
429 bvar(0),
430 )
431 }),
432 );
433 add(
434 "BitVec.toNat_lt",
435 pi(
436 BinderInfo::Default,
437 "n",
438 nat_ty(),
439 pi(
440 BinderInfo::Default,
441 "a",
442 mk_bitvec(bvar(0)),
443 mk_eq(
444 bool_ty(),
445 app2(
446 cst("Nat.lt"),
447 app(cst("BitVec.toNat"), bvar(0)),
448 app2(
449 cst("Nat.pow"),
450 app(cst("Nat.succ"), app(cst("Nat.succ"), cst("Nat.zero"))),
451 bvar(1),
452 ),
453 ),
454 cst("true"),
455 ),
456 ),
457 ),
458 );
459 add(
460 "BitVec.toInt_ofInt",
461 pi(
462 BinderInfo::Default,
463 "n",
464 nat_ty(),
465 pi(
466 BinderInfo::Default,
467 "i",
468 int_ty(),
469 mk_eq(
470 int_ty(),
471 app(
472 cst("BitVec.toInt"),
473 app2(cst("BitVec.ofInt"), bvar(1), bvar(0)),
474 ),
475 bvar(0),
476 ),
477 ),
478 ),
479 );
480 add(
481 "BitVec.rotateLeft_zero",
482 bvx_ext_forall_one(|| {
483 mk_bv_eq(
484 bvar(1),
485 app2(cst("BitVec.rotateLeft"), bvar(0), cst("Nat.zero")),
486 bvar(0),
487 )
488 }),
489 );
490 add(
491 "BitVec.rotateRight_zero",
492 bvx_ext_forall_one(|| {
493 mk_bv_eq(
494 bvar(1),
495 app2(cst("BitVec.rotateRight"), bvar(0), cst("Nat.zero")),
496 bvar(0),
497 )
498 }),
499 );
500 add(
501 "BitVec.rotateLeft_rotateRight_cancel",
502 bvx_ext_forall_bv_nat(|| {
503 mk_bv_eq(
504 bvar(2),
505 app2(
506 cst("BitVec.rotateLeft"),
507 app2(cst("BitVec.rotateRight"), bvar(1), bvar(0)),
508 bvar(0),
509 ),
510 bvar(1),
511 )
512 }),
513 );
514 add(
515 "BitVec.rotateRight_rotateLeft_cancel",
516 bvx_ext_forall_bv_nat(|| {
517 mk_bv_eq(
518 bvar(2),
519 app2(
520 cst("BitVec.rotateRight"),
521 app2(cst("BitVec.rotateLeft"), bvar(1), bvar(0)),
522 bvar(0),
523 ),
524 bvar(1),
525 )
526 }),
527 );
528 add(
529 "BitVec.setBit",
530 pi(
531 BinderInfo::Implicit,
532 "n",
533 nat_ty(),
534 arrow(
535 mk_bitvec(bvar(0)),
536 arrow(nat_ty(), arrow(bool_ty(), mk_bitvec(bvar(1)))),
537 ),
538 ),
539 );
540 add(
541 "BitVec.getLsb_setBit_same",
542 pi(
543 BinderInfo::Implicit,
544 "n",
545 nat_ty(),
546 pi(
547 BinderInfo::Default,
548 "a",
549 mk_bitvec(bvar(0)),
550 pi(
551 BinderInfo::Default,
552 "i",
553 nat_ty(),
554 pi(
555 BinderInfo::Default,
556 "v",
557 bool_ty(),
558 mk_eq(
559 bool_ty(),
560 app2(
561 cst("BitVec.getLsb"),
562 app3(cst("BitVec.setBit"), bvar(2), bvar(1), bvar(0)),
563 bvar(1),
564 ),
565 bvar(0),
566 ),
567 ),
568 ),
569 ),
570 ),
571 );
572 add("BitVec.popcount", bvx_ext_popcount_ty());
573 add(
574 "BitVec.popcount_zero",
575 pi(
576 BinderInfo::Default,
577 "n",
578 nat_ty(),
579 mk_nat_eq(
580 app(cst("BitVec.popcount"), app(cst("BitVec.zero"), bvar(0))),
581 cst("Nat.zero"),
582 ),
583 ),
584 );
585 add(
586 "BitVec.popcount_allOnes",
587 pi(
588 BinderInfo::Default,
589 "n",
590 nat_ty(),
591 mk_nat_eq(
592 app(cst("BitVec.popcount"), app(cst("BitVec.allOnes"), bvar(0))),
593 bvar(0),
594 ),
595 ),
596 );
597 add(
598 "BitVec.popcount_or_add",
599 pi(
600 BinderInfo::Implicit,
601 "n",
602 nat_ty(),
603 pi(
604 BinderInfo::Default,
605 "a",
606 mk_bitvec(bvar(0)),
607 pi(
608 BinderInfo::Default,
609 "b",
610 mk_bitvec(bvar(1)),
611 mk_nat_eq(
612 app2(
613 cst("Nat.add"),
614 app(
615 cst("BitVec.popcount"),
616 app2(cst("BitVec.or"), bvar(1), bvar(0)),
617 ),
618 app(
619 cst("BitVec.popcount"),
620 app2(cst("BitVec.and"), bvar(1), bvar(0)),
621 ),
622 ),
623 app2(
624 cst("Nat.add"),
625 app(cst("BitVec.popcount"), bvar(1)),
626 app(cst("BitVec.popcount"), bvar(0)),
627 ),
628 ),
629 ),
630 ),
631 ),
632 );
633 add("BitVec.countLeadingZeros", bvx_ext_count_zeros_ty());
634 add("BitVec.countTrailingZeros", bvx_ext_count_zeros_ty());
635 add(
636 "BitVec.clz_zero",
637 pi(
638 BinderInfo::Default,
639 "n",
640 nat_ty(),
641 mk_nat_eq(
642 app(
643 cst("BitVec.countLeadingZeros"),
644 app(cst("BitVec.zero"), bvar(0)),
645 ),
646 bvar(0),
647 ),
648 ),
649 );
650 add(
651 "BitVec.ctz_zero",
652 pi(
653 BinderInfo::Default,
654 "n",
655 nat_ty(),
656 mk_nat_eq(
657 app(
658 cst("BitVec.countTrailingZeros"),
659 app(cst("BitVec.zero"), bvar(0)),
660 ),
661 bvar(0),
662 ),
663 ),
664 );
665 add(
666 "BitVec.clz_allOnes",
667 pi(
668 BinderInfo::Default,
669 "n",
670 nat_ty(),
671 mk_nat_eq(
672 app(
673 cst("BitVec.countLeadingZeros"),
674 app(cst("BitVec.allOnes"), bvar(0)),
675 ),
676 cst("Nat.zero"),
677 ),
678 ),
679 );
680 add("BitVec.reverse", bvx_ext_reverse_ty());
681 add(
682 "BitVec.reverse_reverse",
683 bvx_ext_forall_one(|| {
684 mk_bv_eq(
685 bvar(1),
686 app(cst("BitVec.reverse"), app(cst("BitVec.reverse"), bvar(0))),
687 bvar(0),
688 )
689 }),
690 );
691 add(
692 "BitVec.reverse_zero",
693 pi(
694 BinderInfo::Default,
695 "n",
696 nat_ty(),
697 mk_bv_eq(
698 bvar(0),
699 app(cst("BitVec.reverse"), app(cst("BitVec.zero"), bvar(0))),
700 app(cst("BitVec.zero"), bvar(0)),
701 ),
702 ),
703 );
704 add("BitVec.byteSwap", bitvec_unop_ty());
705 add(
706 "BitVec.byteSwap_byteSwap",
707 bvx_ext_forall_one(|| {
708 mk_bv_eq(
709 bvar(1),
710 app(cst("BitVec.byteSwap"), app(cst("BitVec.byteSwap"), bvar(0))),
711 bvar(0),
712 )
713 }),
714 );
715 add(
716 "BitVec.smt_bvadd_comm",
717 pi(
718 BinderInfo::Implicit,
719 "n",
720 nat_ty(),
721 pi(
722 BinderInfo::Default,
723 "a",
724 mk_bitvec(bvar(0)),
725 pi(
726 BinderInfo::Default,
727 "b",
728 mk_bitvec(bvar(1)),
729 mk_bv_eq(
730 bvar(2),
731 app2(cst("BitVec.add"), bvar(1), bvar(0)),
732 app2(cst("BitVec.add"), bvar(0), bvar(1)),
733 ),
734 ),
735 ),
736 ),
737 );
738 add(
739 "BitVec.smt_bvnot_bvadd_neg",
740 bvx_ext_forall_one(|| {
741 mk_bv_eq(
742 bvar(1),
743 app2(
744 cst("BitVec.add"),
745 app(cst("BitVec.not"), bvar(0)),
746 app2(
747 cst("BitVec.ofNat"),
748 bvar(1),
749 app(cst("Nat.succ"), cst("Nat.zero")),
750 ),
751 ),
752 app(cst("BitVec.neg"), bvar(0)),
753 )
754 }),
755 );
756 add(
757 "BitVec.smt_bvxor_comm",
758 pi(
759 BinderInfo::Implicit,
760 "n",
761 nat_ty(),
762 pi(
763 BinderInfo::Default,
764 "a",
765 mk_bitvec(bvar(0)),
766 pi(
767 BinderInfo::Default,
768 "b",
769 mk_bitvec(bvar(1)),
770 mk_bv_eq(
771 bvar(2),
772 app2(cst("BitVec.xor"), bvar(1), bvar(0)),
773 app2(cst("BitVec.xor"), bvar(0), bvar(1)),
774 ),
775 ),
776 ),
777 ),
778 );
779 add(
780 "BitVec.add_overflow_wrap",
781 pi(
782 BinderInfo::Default,
783 "n",
784 nat_ty(),
785 mk_nat_eq(
786 app(
787 cst("BitVec.toNat"),
788 app2(
789 cst("BitVec.add"),
790 app(cst("BitVec.allOnes"), bvar(0)),
791 app2(
792 cst("BitVec.ofNat"),
793 bvar(0),
794 app(cst("Nat.succ"), cst("Nat.zero")),
795 ),
796 ),
797 ),
798 cst("Nat.zero"),
799 ),
800 ),
801 );
802 add(
803 "BitVec.sub_underflow_wrap",
804 pi(
805 BinderInfo::Default,
806 "n",
807 nat_ty(),
808 mk_bv_eq(
809 bvar(0),
810 app2(
811 cst("BitVec.sub"),
812 app(cst("BitVec.zero"), bvar(0)),
813 app2(
814 cst("BitVec.ofNat"),
815 bvar(0),
816 app(cst("Nat.succ"), cst("Nat.zero")),
817 ),
818 ),
819 app(cst("BitVec.allOnes"), bvar(0)),
820 ),
821 ),
822 );
823 add("BitVec.isolateLowestBit", bitvec_unop_ty());
824 add(
825 "BitVec.isolateLowestBit_def",
826 bvx_ext_forall_one(|| {
827 mk_bv_eq(
828 bvar(1),
829 app(cst("BitVec.isolateLowestBit"), bvar(0)),
830 app2(cst("BitVec.and"), bvar(0), app(cst("BitVec.neg"), bvar(0))),
831 )
832 }),
833 );
834 add("BitVec.clearLowestBit", bitvec_unop_ty());
835 add(
836 "BitVec.clearLowestBit_def",
837 bvx_ext_forall_one(|| {
838 mk_bv_eq(
839 bvar(1),
840 app(cst("BitVec.clearLowestBit"), bvar(0)),
841 app2(
842 cst("BitVec.and"),
843 bvar(0),
844 app2(
845 cst("BitVec.sub"),
846 bvar(0),
847 app2(
848 cst("BitVec.ofNat"),
849 bvar(1),
850 app(cst("Nat.succ"), cst("Nat.zero")),
851 ),
852 ),
853 ),
854 )
855 }),
856 );
857 add(
858 "BitVec.clearLowestBit_zero",
859 bvx_ext_forall_one(|| {
860 arrow(
861 mk_bv_eq(bvar(1), bvar(0), app(cst("BitVec.zero"), bvar(1))),
862 mk_bv_eq(
863 bvar(1),
864 app(cst("BitVec.clearLowestBit"), bvar(0)),
865 app(cst("BitVec.zero"), bvar(1)),
866 ),
867 )
868 }),
869 );
870 add(
871 "BitVec.simdAdd",
872 pi(
873 BinderInfo::Implicit,
874 "n",
875 nat_ty(),
876 pi(
877 BinderInfo::Default,
878 "lanes",
879 nat_ty(),
880 arrow(
881 mk_bitvec(app2(cst("Nat.mul"), bvar(1), bvar(0))),
882 arrow(
883 mk_bitvec(app2(cst("Nat.mul"), bvar(2), bvar(1))),
884 mk_bitvec(app2(cst("Nat.mul"), bvar(3), bvar(2))),
885 ),
886 ),
887 ),
888 ),
889 );
890 add(
891 "BitVec.simdAnd",
892 pi(
893 BinderInfo::Implicit,
894 "n",
895 nat_ty(),
896 pi(
897 BinderInfo::Default,
898 "lanes",
899 nat_ty(),
900 arrow(
901 mk_bitvec(app2(cst("Nat.mul"), bvar(1), bvar(0))),
902 arrow(
903 mk_bitvec(app2(cst("Nat.mul"), bvar(2), bvar(1))),
904 mk_bitvec(app2(cst("Nat.mul"), bvar(3), bvar(2))),
905 ),
906 ),
907 ),
908 ),
909 );
910 add(
911 "BitVec.simdOr",
912 pi(
913 BinderInfo::Implicit,
914 "n",
915 nat_ty(),
916 pi(
917 BinderInfo::Default,
918 "lanes",
919 nat_ty(),
920 arrow(
921 mk_bitvec(app2(cst("Nat.mul"), bvar(1), bvar(0))),
922 arrow(
923 mk_bitvec(app2(cst("Nat.mul"), bvar(2), bvar(1))),
924 mk_bitvec(app2(cst("Nat.mul"), bvar(3), bvar(2))),
925 ),
926 ),
927 ),
928 ),
929 );
930 add(
931 "BitVec.simdXor",
932 pi(
933 BinderInfo::Implicit,
934 "n",
935 nat_ty(),
936 pi(
937 BinderInfo::Default,
938 "lanes",
939 nat_ty(),
940 arrow(
941 mk_bitvec(app2(cst("Nat.mul"), bvar(1), bvar(0))),
942 arrow(
943 mk_bitvec(app2(cst("Nat.mul"), bvar(2), bvar(1))),
944 mk_bitvec(app2(cst("Nat.mul"), bvar(3), bvar(2))),
945 ),
946 ),
947 ),
948 ),
949 );
950 add(
951 "BitVec.simdAdd_comm",
952 pi(
953 BinderInfo::Implicit,
954 "n",
955 nat_ty(),
956 pi(
957 BinderInfo::Default,
958 "lanes",
959 nat_ty(),
960 pi(
961 BinderInfo::Default,
962 "a",
963 mk_bitvec(app2(cst("Nat.mul"), bvar(1), bvar(0))),
964 pi(
965 BinderInfo::Default,
966 "b",
967 mk_bitvec(app2(cst("Nat.mul"), bvar(2), bvar(1))),
968 mk_bv_eq(
969 app2(cst("Nat.mul"), bvar(3), bvar(2)),
970 app3(cst("BitVec.simdAdd"), bvar(2), bvar(1), bvar(0)),
971 app3(cst("BitVec.simdAdd"), bvar(2), bvar(0), bvar(1)),
972 ),
973 ),
974 ),
975 ),
976 ),
977 );
978 add(
979 "BitVec.xor_comm",
980 pi(
981 BinderInfo::Implicit,
982 "n",
983 nat_ty(),
984 pi(
985 BinderInfo::Default,
986 "a",
987 mk_bitvec(bvar(0)),
988 pi(
989 BinderInfo::Default,
990 "b",
991 mk_bitvec(bvar(1)),
992 mk_bv_eq(
993 bvar(2),
994 app2(cst("BitVec.xor"), bvar(1), bvar(0)),
995 app2(cst("BitVec.xor"), bvar(0), bvar(1)),
996 ),
997 ),
998 ),
999 ),
1000 );
1001 add(
1002 "BitVec.xor_assoc",
1003 pi(
1004 BinderInfo::Implicit,
1005 "n",
1006 nat_ty(),
1007 pi(
1008 BinderInfo::Default,
1009 "a",
1010 mk_bitvec(bvar(0)),
1011 pi(
1012 BinderInfo::Default,
1013 "b",
1014 mk_bitvec(bvar(1)),
1015 pi(
1016 BinderInfo::Default,
1017 "c",
1018 mk_bitvec(bvar(2)),
1019 mk_bv_eq(
1020 bvar(3),
1021 app2(
1022 cst("BitVec.xor"),
1023 app2(cst("BitVec.xor"), bvar(2), bvar(1)),
1024 bvar(0),
1025 ),
1026 app2(
1027 cst("BitVec.xor"),
1028 bvar(2),
1029 app2(cst("BitVec.xor"), bvar(1), bvar(0)),
1030 ),
1031 ),
1032 ),
1033 ),
1034 ),
1035 ),
1036 );
1037 add(
1038 "BitVec.and_distrib_or",
1039 pi(
1040 BinderInfo::Implicit,
1041 "n",
1042 nat_ty(),
1043 pi(
1044 BinderInfo::Default,
1045 "a",
1046 mk_bitvec(bvar(0)),
1047 pi(
1048 BinderInfo::Default,
1049 "b",
1050 mk_bitvec(bvar(1)),
1051 pi(
1052 BinderInfo::Default,
1053 "c",
1054 mk_bitvec(bvar(2)),
1055 mk_bv_eq(
1056 bvar(3),
1057 app2(
1058 cst("BitVec.and"),
1059 bvar(2),
1060 app2(cst("BitVec.or"), bvar(1), bvar(0)),
1061 ),
1062 app2(
1063 cst("BitVec.or"),
1064 app2(cst("BitVec.and"), bvar(2), bvar(1)),
1065 app2(cst("BitVec.and"), bvar(2), bvar(0)),
1066 ),
1067 ),
1068 ),
1069 ),
1070 ),
1071 ),
1072 );
1073 add(
1074 "BitVec.or_distrib_and",
1075 pi(
1076 BinderInfo::Implicit,
1077 "n",
1078 nat_ty(),
1079 pi(
1080 BinderInfo::Default,
1081 "a",
1082 mk_bitvec(bvar(0)),
1083 pi(
1084 BinderInfo::Default,
1085 "b",
1086 mk_bitvec(bvar(1)),
1087 pi(
1088 BinderInfo::Default,
1089 "c",
1090 mk_bitvec(bvar(2)),
1091 mk_bv_eq(
1092 bvar(3),
1093 app2(
1094 cst("BitVec.or"),
1095 bvar(2),
1096 app2(cst("BitVec.and"), bvar(1), bvar(0)),
1097 ),
1098 app2(
1099 cst("BitVec.and"),
1100 app2(cst("BitVec.or"), bvar(2), bvar(1)),
1101 app2(cst("BitVec.or"), bvar(2), bvar(0)),
1102 ),
1103 ),
1104 ),
1105 ),
1106 ),
1107 ),
1108 );
1109 add(
1110 "BitVec.and_or_absorb",
1111 pi(
1112 BinderInfo::Implicit,
1113 "n",
1114 nat_ty(),
1115 pi(
1116 BinderInfo::Default,
1117 "a",
1118 mk_bitvec(bvar(0)),
1119 pi(
1120 BinderInfo::Default,
1121 "b",
1122 mk_bitvec(bvar(1)),
1123 mk_bv_eq(
1124 bvar(2),
1125 app2(
1126 cst("BitVec.and"),
1127 bvar(1),
1128 app2(cst("BitVec.or"), bvar(1), bvar(0)),
1129 ),
1130 bvar(1),
1131 ),
1132 ),
1133 ),
1134 ),
1135 );
1136 add(
1137 "BitVec.or_and_absorb",
1138 pi(
1139 BinderInfo::Implicit,
1140 "n",
1141 nat_ty(),
1142 pi(
1143 BinderInfo::Default,
1144 "a",
1145 mk_bitvec(bvar(0)),
1146 pi(
1147 BinderInfo::Default,
1148 "b",
1149 mk_bitvec(bvar(1)),
1150 mk_bv_eq(
1151 bvar(2),
1152 app2(
1153 cst("BitVec.or"),
1154 bvar(1),
1155 app2(cst("BitVec.and"), bvar(1), bvar(0)),
1156 ),
1157 bvar(1),
1158 ),
1159 ),
1160 ),
1161 ),
1162 );
1163 add(
1164 "BitVec.and_allOnes",
1165 bvx_ext_forall_one(|| {
1166 mk_bv_eq(
1167 bvar(1),
1168 app2(
1169 cst("BitVec.and"),
1170 bvar(0),
1171 app(cst("BitVec.allOnes"), bvar(1)),
1172 ),
1173 bvar(0),
1174 )
1175 }),
1176 );
1177 add(
1178 "BitVec.and_zero",
1179 bvx_ext_forall_one(|| {
1180 mk_bv_eq(
1181 bvar(1),
1182 app2(cst("BitVec.and"), bvar(0), app(cst("BitVec.zero"), bvar(1))),
1183 app(cst("BitVec.zero"), bvar(1)),
1184 )
1185 }),
1186 );
1187 add(
1188 "BitVec.or_zero",
1189 bvx_ext_forall_one(|| {
1190 mk_bv_eq(
1191 bvar(1),
1192 app2(cst("BitVec.or"), bvar(0), app(cst("BitVec.zero"), bvar(1))),
1193 bvar(0),
1194 )
1195 }),
1196 );
1197 add(
1198 "BitVec.or_allOnes",
1199 bvx_ext_forall_one(|| {
1200 mk_bv_eq(
1201 bvar(1),
1202 app2(
1203 cst("BitVec.or"),
1204 bvar(0),
1205 app(cst("BitVec.allOnes"), bvar(1)),
1206 ),
1207 app(cst("BitVec.allOnes"), bvar(1)),
1208 )
1209 }),
1210 );
1211 add(
1212 "BitVec.xor_zero",
1213 bvx_ext_forall_one(|| {
1214 mk_bv_eq(
1215 bvar(1),
1216 app2(cst("BitVec.xor"), bvar(0), app(cst("BitVec.zero"), bvar(1))),
1217 bvar(0),
1218 )
1219 }),
1220 );
1221 add(
1222 "BitVec.not_zero",
1223 pi(
1224 BinderInfo::Default,
1225 "n",
1226 nat_ty(),
1227 mk_bv_eq(
1228 bvar(0),
1229 app(cst("BitVec.not"), app(cst("BitVec.zero"), bvar(0))),
1230 app(cst("BitVec.allOnes"), bvar(0)),
1231 ),
1232 ),
1233 );
1234 add(
1235 "BitVec.not_allOnes",
1236 pi(
1237 BinderInfo::Default,
1238 "n",
1239 nat_ty(),
1240 mk_bv_eq(
1241 bvar(0),
1242 app(cst("BitVec.not"), app(cst("BitVec.allOnes"), bvar(0))),
1243 app(cst("BitVec.zero"), bvar(0)),
1244 ),
1245 ),
1246 );
1247 add(
1248 "BitVec.ext",
1249 pi(
1250 BinderInfo::Implicit,
1251 "n",
1252 nat_ty(),
1253 pi(
1254 BinderInfo::Default,
1255 "a",
1256 mk_bitvec(bvar(0)),
1257 pi(
1258 BinderInfo::Default,
1259 "b",
1260 mk_bitvec(bvar(1)),
1261 arrow(
1262 pi(
1263 BinderInfo::Default,
1264 "i",
1265 nat_ty(),
1266 mk_eq(
1267 bool_ty(),
1268 app2(cst("BitVec.getLsb"), bvar(2), bvar(0)),
1269 app2(cst("BitVec.getLsb"), bvar(2), bvar(0)),
1270 ),
1271 ),
1272 mk_bv_eq(bvar(2), bvar(1), bvar(0)),
1273 ),
1274 ),
1275 ),
1276 ),
1277 );
1278}
1279#[cfg(test)]
1280mod tests_ext {
1281 use super::*;
1282 fn setup_ext_env() -> Environment {
1283 let mut env = Environment::new();
1284 for (name, ty) in &[
1285 ("Nat", type1()),
1286 ("Int", type1()),
1287 ("Bool", type1()),
1288 ("Fin", type1()),
1289 ("Eq", prop()),
1290 ("Iff", prop()),
1291 ] {
1292 env.add(Declaration::Axiom {
1293 name: Name::str(*name),
1294 univ_params: vec![],
1295 ty: ty.clone(),
1296 })
1297 .expect("operation should succeed");
1298 }
1299 for name in &[
1300 "Nat.zero", "Nat.succ", "Nat.add", "Nat.mul", "Nat.sub", "Nat.mod", "Nat.pow",
1301 "Nat.lt", "Nat.ble",
1302 ] {
1303 env.add(Declaration::Axiom {
1304 name: Name::str(*name),
1305 univ_params: vec![],
1306 ty: nat_ty(),
1307 })
1308 .expect("operation should succeed");
1309 }
1310 for name in &["true", "false"] {
1311 env.add(Declaration::Axiom {
1312 name: Name::str(*name),
1313 univ_params: vec![],
1314 ty: bool_ty(),
1315 })
1316 .expect("operation should succeed");
1317 }
1318 build_bitvec_env(&mut env).expect("build_bitvec_env should succeed");
1319 register_bitvec_extended_axioms(&mut env);
1320 env
1321 }
1322 #[test]
1323 fn test_ext_arith_shift_right_present() {
1324 let env = setup_ext_env();
1325 assert!(env.contains(&Name::str("BitVec.arithShiftRight")));
1326 }
1327 #[test]
1328 fn test_ext_shift_zero_laws() {
1329 let env = setup_ext_env();
1330 assert!(env.contains(&Name::str("BitVec.shiftLeft_zero_amount")));
1331 assert!(env.contains(&Name::str("BitVec.shiftRight_zero_amount")));
1332 assert!(env.contains(&Name::str("BitVec.arithShiftRight_zero_amount")));
1333 }
1334 #[test]
1335 fn test_ext_add_mod_present() {
1336 let env = setup_ext_env();
1337 assert!(env.contains(&Name::str("BitVec.add_mod")));
1338 }
1339 #[test]
1340 fn test_ext_mul_laws() {
1341 let env = setup_ext_env();
1342 assert!(env.contains(&Name::str("BitVec.mul_comm")));
1343 assert!(env.contains(&Name::str("BitVec.mul_assoc")));
1344 assert!(env.contains(&Name::str("BitVec.mul_mod")));
1345 }
1346 #[test]
1347 fn test_ext_comparison_laws() {
1348 let env = setup_ext_env();
1349 assert!(env.contains(&Name::str("BitVec.ult_irrefl")));
1350 assert!(env.contains(&Name::str("BitVec.ule_refl")));
1351 assert!(env.contains(&Name::str("BitVec.slt_irrefl")));
1352 assert!(env.contains(&Name::str("BitVec.sle_refl")));
1353 }
1354 #[test]
1355 fn test_ext_concat_extract() {
1356 let env = setup_ext_env();
1357 assert!(env.contains(&Name::str("BitVec.append_assoc")));
1358 assert!(env.contains(&Name::str("BitVec.extractLsb_full")));
1359 }
1360 #[test]
1361 fn test_ext_zero_sign_extend() {
1362 let env = setup_ext_env();
1363 assert!(env.contains(&Name::str("BitVec.zeroExtend")));
1364 assert!(env.contains(&Name::str("BitVec.zeroExtend_ge_id")));
1365 assert!(env.contains(&Name::str("BitVec.signExtend_ge_id")));
1366 }
1367 #[test]
1368 fn test_ext_fin_iso() {
1369 let env = setup_ext_env();
1370 assert!(env.contains(&Name::str("BitVec.toFin")));
1371 assert!(env.contains(&Name::str("BitVec.ofFin")));
1372 assert!(env.contains(&Name::str("BitVec.toFin_ofFin")));
1373 assert!(env.contains(&Name::str("BitVec.ofFin_toFin")));
1374 }
1375 #[test]
1376 fn test_ext_nat_int_conv() {
1377 let env = setup_ext_env();
1378 assert!(env.contains(&Name::str("BitVec.toNat_lt")));
1379 assert!(env.contains(&Name::str("BitVec.toInt_ofInt")));
1380 }
1381 #[test]
1382 fn test_ext_rotation_laws() {
1383 let env = setup_ext_env();
1384 assert!(env.contains(&Name::str("BitVec.rotateLeft_zero")));
1385 assert!(env.contains(&Name::str("BitVec.rotateRight_zero")));
1386 assert!(env.contains(&Name::str("BitVec.rotateLeft_rotateRight_cancel")));
1387 assert!(env.contains(&Name::str("BitVec.rotateRight_rotateLeft_cancel")));
1388 }
1389 #[test]
1390 fn test_ext_bit_access() {
1391 let env = setup_ext_env();
1392 assert!(env.contains(&Name::str("BitVec.setBit")));
1393 assert!(env.contains(&Name::str("BitVec.getLsb_setBit_same")));
1394 }
1395 #[test]
1396 fn test_ext_popcount() {
1397 let env = setup_ext_env();
1398 assert!(env.contains(&Name::str("BitVec.popcount")));
1399 assert!(env.contains(&Name::str("BitVec.popcount_zero")));
1400 assert!(env.contains(&Name::str("BitVec.popcount_allOnes")));
1401 assert!(env.contains(&Name::str("BitVec.popcount_or_add")));
1402 }
1403 #[test]
1404 fn test_ext_count_zeros() {
1405 let env = setup_ext_env();
1406 assert!(env.contains(&Name::str("BitVec.countLeadingZeros")));
1407 assert!(env.contains(&Name::str("BitVec.countTrailingZeros")));
1408 assert!(env.contains(&Name::str("BitVec.clz_zero")));
1409 assert!(env.contains(&Name::str("BitVec.ctz_zero")));
1410 assert!(env.contains(&Name::str("BitVec.clz_allOnes")));
1411 }
1412 #[test]
1413 fn test_ext_reversal() {
1414 let env = setup_ext_env();
1415 assert!(env.contains(&Name::str("BitVec.reverse")));
1416 assert!(env.contains(&Name::str("BitVec.reverse_reverse")));
1417 assert!(env.contains(&Name::str("BitVec.reverse_zero")));
1418 assert!(env.contains(&Name::str("BitVec.byteSwap")));
1419 assert!(env.contains(&Name::str("BitVec.byteSwap_byteSwap")));
1420 }
1421 #[test]
1422 fn test_ext_smt_axioms() {
1423 let env = setup_ext_env();
1424 assert!(env.contains(&Name::str("BitVec.smt_bvadd_comm")));
1425 assert!(env.contains(&Name::str("BitVec.smt_bvnot_bvadd_neg")));
1426 assert!(env.contains(&Name::str("BitVec.smt_bvxor_comm")));
1427 }
1428 #[test]
1429 fn test_ext_overflow_behavior() {
1430 let env = setup_ext_env();
1431 assert!(env.contains(&Name::str("BitVec.add_overflow_wrap")));
1432 assert!(env.contains(&Name::str("BitVec.sub_underflow_wrap")));
1433 }
1434 #[test]
1435 fn test_ext_bit_tricks() {
1436 let env = setup_ext_env();
1437 assert!(env.contains(&Name::str("BitVec.isolateLowestBit")));
1438 assert!(env.contains(&Name::str("BitVec.isolateLowestBit_def")));
1439 assert!(env.contains(&Name::str("BitVec.clearLowestBit")));
1440 assert!(env.contains(&Name::str("BitVec.clearLowestBit_def")));
1441 assert!(env.contains(&Name::str("BitVec.clearLowestBit_zero")));
1442 }
1443 #[test]
1444 fn test_ext_simd() {
1445 let env = setup_ext_env();
1446 assert!(env.contains(&Name::str("BitVec.simdAdd")));
1447 assert!(env.contains(&Name::str("BitVec.simdAnd")));
1448 assert!(env.contains(&Name::str("BitVec.simdOr")));
1449 assert!(env.contains(&Name::str("BitVec.simdXor")));
1450 assert!(env.contains(&Name::str("BitVec.simdAdd_comm")));
1451 }
1452 #[test]
1453 fn test_ext_distributivity() {
1454 let env = setup_ext_env();
1455 assert!(env.contains(&Name::str("BitVec.and_distrib_or")));
1456 assert!(env.contains(&Name::str("BitVec.or_distrib_and")));
1457 assert!(env.contains(&Name::str("BitVec.xor_comm")));
1458 assert!(env.contains(&Name::str("BitVec.xor_assoc")));
1459 }
1460 #[test]
1461 fn test_ext_absorption() {
1462 let env = setup_ext_env();
1463 assert!(env.contains(&Name::str("BitVec.and_or_absorb")));
1464 assert!(env.contains(&Name::str("BitVec.or_and_absorb")));
1465 }
1466 #[test]
1467 fn test_ext_identity_annihilator() {
1468 let env = setup_ext_env();
1469 assert!(env.contains(&Name::str("BitVec.and_allOnes")));
1470 assert!(env.contains(&Name::str("BitVec.and_zero")));
1471 assert!(env.contains(&Name::str("BitVec.or_zero")));
1472 assert!(env.contains(&Name::str("BitVec.or_allOnes")));
1473 assert!(env.contains(&Name::str("BitVec.xor_zero")));
1474 assert!(env.contains(&Name::str("BitVec.not_zero")));
1475 assert!(env.contains(&Name::str("BitVec.not_allOnes")));
1476 }
1477 #[test]
1478 fn test_ext_extensionality() {
1479 let env = setup_ext_env();
1480 assert!(env.contains(&Name::str("BitVec.ext")));
1481 }
1482 #[test]
1483 fn test_bitvecfixed_struct_size() {
1484 let _bv: BitVecFixed<64> = BitVecFixed { data: 0xDEAD_BEEF };
1485 assert_eq!(std::mem::size_of::<BitVecFixed<64>>(), 8);
1486 }
1487}