test: add new files from grosser group

Eval/fail.txt

@@ -13,3 +13,29 @@ bitvec_InstCombineShift__497'''.lean
 bitvec_InstCombineShift__497.lean
 bitvec_InstCombineShift__582.lean
 bitvec_InstCombineShift__724.lean
+g2008h02h16hSDivOverflow2_proof.lean
+g2008h02h23hMulSub_proof.lean
+gadd2_proof.lean
+gadd4_proof.lean
+gaddhshlhsdivhtohsrem_proof.lean
+gand2_proof.lean
+gapinthsub_proof.lean
+gashrhdemand_proof.lean
+gdistribute_proof.lean
+gexact_proof.lean
+gfoldhinchofhaddhofhnothxhandhyhtohsubhxhfromhy_proof.lean
+gfoldhsubhofhnothtohinchofhadd_proof.lean
+glshr_proof.lean
+gmul_fold_proof.lean
+gnot_proof.lean
+gpr14365_proof.lean
+greassociatehnuw_proof.lean
+grem_proof.lean
+gsdivhexacthbyhnegativehpowerhofhtwo_proof.lean
+gsdivhexacthbyhpowerhofhtwo_proof.lean
+gsubhandhorhneghxor_proof.lean
+gsubhofhnegatible_proof.lean
+gsubhofhnegatiblehinseltpoison_proof.lean
+gsubhorhandhxor_proof.lean
+gsubhxorhorhneghand_proof.lean
+gxor_proof.lean

Eval/g2008h02h16hSDivOverflow2_proof.lean

@@ -0,0 +1,7 @@
+import LeanSAT.Tactics.BVDecide
+
+open Std (BitVec)
+theorem i_thm (x : _root_.BitVec 8) :
+    (x.sdiv 253#8).sdiv 253#8 = x.sdiv 9#8 := by
+  bv_decide
+

Eval/g2008h02h23hMulSub_proof.lean

@@ -0,0 +1,9 @@
+import LeanSAT.Tactics.BVDecide
+
+-- Currently times out
+set_option sat.timeout 1
+open Std (BitVec)
+theorem test_thm (x : _root_.BitVec 26) :
+    x * 2885#26 + x * 67105980#26 = x := by
+  bv_decide
+

Eval/gadd2_proof.lean

@@ -0,0 +1,127 @@
+import LeanSAT.Tactics.BVDecide
+
+open Std (BitVec)
+theorem test2_thm (x : _root_.BitVec 32) :
+    (x &&& 7#32) + (x &&& 32#32) = x &&& 39#32 := by
+  bv_decide
+
+theorem test3_thm (x : _root_.BitVec 32) :
+    (x &&& 128#32) + x >>> 30 = x &&& 128#32 ||| x >>> 30 := by
+  bv_decide
+
+theorem test4_thm (x : _root_.BitVec 32) :
+    x * 2#32 = x <<< 1 := by
+  bv_decide
+
+set_option sat.timeout 1
+theorem test9_thm (x : _root_.BitVec 16) :
+    x * 2#16 + x * 32767#16 = x * 32769#16 := by
+  bv_decide
+
+#exit
+
+theorem test10_thm (x x_1 : _root_.BitVec 32) :
+  x_1 + 1#32 + ((x.sshiftRight 3 ||| 2863311530#32) ^^^ 1431655765#32) =
+    x_1 + (x.sshiftRight 3 &&& 1431655765#32) * 4294967295#32 := by
+  bv_decide
+
+theorem test11_thm (x x_1 : _root_.BitVec 32) :
+  x_1 + 1#32 + ((x ||| 2863311530#32) ^^^ 1431655765#32) = x_1 + (x &&& 1431655765#32) * 4294967295#32 := by
+  bv_decide
+
+theorem test12_thm (x x_1 : _root_.BitVec 32) :
+  x_1 + 1#32 + ((x ||| 2863311530#32) ^^^ 1431655765#32) = x_1 + (x &&& 1431655765#32) * 4294967295#32 := by
+  bv_decide
+
+theorem test13_thm (x x_1 : _root_.BitVec 32) :
+  x_1 + 1#32 + ((x ||| 2863311529#32) ^^^ 1431655766#32) = x_1 + (x &&& 1431655766#32) * 4294967295#32 := by
+  bv_decide
+
+theorem test14_thm (x x_1 : _root_.BitVec 32) :
+  x_1 + 1#32 + ((x ||| 2863311529#32) ^^^ 1431655766#32) = x_1 + (x &&& 1431655766#32) * 4294967295#32 := by
+  bv_decide
+
+theorem test15_thm (x x_1 : _root_.BitVec 32) :
+  x_1 + 1#32 + (x &&& 2863311529#32 ^^^ 2863311529#32) = x_1 + (x ||| 1431655766#32) * 4294967295#32 := by
+  bv_decide
+
+theorem test16_thm (x x_1 : _root_.BitVec 32) :
+  x_1 + 1#32 + (x &&& 2863311529#32 ^^^ 2863311529#32) = x_1 + (x ||| 1431655766#32) * 4294967295#32 := by
+  bv_decide
+
+theorem test17_thm (x x_1 : _root_.BitVec 32) :
+  (x_1 &&& 2863311530#32 ^^^ 2863311531#32) + x = x + (x_1 ||| 1431655765#32) * 4294967295#32 := by
+  bv_decide
+
+theorem test18_thm (x x_1 : _root_.BitVec 32) :
+  x_1 + 1#32 + (x &&& 2863311530#32 ^^^ 2863311530#32) = x_1 + (x ||| 1431655765#32) * 4294967295#32 := by
+  bv_decide
+
+theorem mul_add_to_mul_1_thm (x : _root_.BitVec 16) : 
+    x + x * 8#16 = x * 9#16 := by
+  bv_decide
+
+theorem mul_add_to_mul_2_thm (x : _root_.BitVec 16) : 
+    x + x * 8#16 = x * 9#16 := by
+  bv_decide
+
+theorem mul_add_to_mul_3_thm (x : _root_.BitVec 16) : 
+    x * 2#16 + x * 3#16 = x * 5#16 := by
+  bv_decide
+
+theorem mul_add_to_mul_4_thm (x : _root_.BitVec 16) : 
+    x * 2#16 + x * 7#16 = x * 9#16 := by
+  bv_decide
+
+theorem mul_add_to_mul_5_thm (x : _root_.BitVec 16) : 
+    x * 3#16 + x * 7#16 = x * 10#16 := by
+  bv_decide
+
+theorem mul_add_to_mul_6_thm (x x_1 : _root_.BitVec 32) : 
+    x_1 * x + x_1 * x * 5#32 = x_1 * x * 6#32 := by
+  bv_decide
+
+theorem mul_add_to_mul_7_thm (x : _root_.BitVec 16) : 
+    x + x * 32767#16 = x <<< 15 := by
+  bv_decide
+
+theorem mul_add_to_mul_8_thm (x : _root_.BitVec 16) : 
+    x * 16383#16 + x * 16384#16 = x * 32767#16 := by
+  bv_decide
+
+theorem mul_add_to_mul_9_thm (x : _root_.BitVec 16) : 
+    x * 32768#16 = x <<< 15 := by
+  bv_decide
+
+theorem add_or_and_thm (x x_1 : _root_.BitVec 32) : 
+    (x_1 ||| x) + (x_1 &&& x) = x_1 + x := by
+  bv_decide
+
+theorem add_or_and_commutative_thm (x x_1 : _root_.BitVec 32) : 
+    (x_1 ||| x) + (x &&& x_1) = x_1 + x := by
+  bv_decide
+
+theorem add_and_or_commutative_thm (x x_1 : _root_.BitVec 32) : 
+    (x_1 &&& x) + (x ||| x_1) = x + x_1 := by
+  bv_decide
+
+theorem add_nsw_or_and_thm (x x_1 : _root_.BitVec 32) : 
+    (x_1 ||| x) + (x_1 &&& x) = x_1 + x := by
+  bv_decide
+
+theorem add_nuw_or_and_thm (x x_1 : _root_.BitVec 32) : 
+    (x_1 ||| x) + (x_1 &&& x) = x_1 + x := by
+  bv_decide
+
+theorem add_nuw_nsw_or_and_thm (x x_1 : _root_.BitVec 32) : 
+    (x_1 ||| x) + (x_1 &&& x) = x_1 + x := by
+  bv_decide
+
+theorem add_undemanded_low_bits_thm (x : _root_.BitVec 32) : 
+    ((x ||| 15#32) + 1616#32) >>> 4 = (1616#32 + x) >>> 4 := by
+  bv_decide
+
+theorem sub_undemanded_low_bits_thm (x : _root_.BitVec 32) : 
+    ((x ||| 15#32) + 4294965680#32) >>> 4 = (4294965680#32 + x) >>> 4 := by
+  bv_decide
+

Eval/gadd4_proof.lean

@@ -0,0 +1,17 @@
+import LeanSAT.Tactics.BVDecide
+
+open Std (BitVec)
+theorem match_andAsRem_lshrAsDiv_shlAsMul_thm (x : _root_.BitVec 64) :
+  (x &&& 63#64) + BitVec.ofNat 64 (x.toNat >>> 6 % 9) <<< 6 = BitVec.ofNat 64 (x.toNat % 576) := by
+  bv_decide
+
+theorem match_signed_thm (x : _root_.BitVec 64) :
+  x + 299#64 * (x.sdiv 299#64).sdiv 64#64 * 18446744073709551552#64 + x.sdiv 19136#64 * 19136#64 +
+      (x.sdiv 19136#64).sdiv 9#64 * 18446744073709379392#64 =
+    x + x.sdiv 172224#64 * 18446744073709379392#64 := by
+  bv_decide
+
+theorem not_match_inconsistent_signs_thm (x : _root_.BitVec 64) :
+  BitVec.ofNat 64 ((x.sdiv 299#64).toNat % 64) * 299#64 = 299#64 * (x.sdiv 299#64 &&& 63#64) := by
+  bv_decide
+

Eval/gaddhshlhsdivhtohsrem_proof.lean

@@ -0,0 +1,15 @@
+import LeanSAT.Tactics.BVDecide
+
+open Std (BitVec)
+
+theorem addhshlhsdivhscalar0_thm (x : _root_.BitVec 8) :
+    x.sdiv 252#8 <<< 2 + x = x + x.sdiv 4#8 * 252#8 := by
+  bv_decide
+
+theorem addhshlhsdivhscalar1_thm (x : _root_.BitVec 8) :
+    x.sdiv 192#8 <<< 6 + x = x + x.sdiv 64#8 * 192#8 := by
+  bv_decide
+
+theorem addhshlhsdivhscalar2_thm (x : _root_.BitVec 32) :
+  x.sdiv 3221225472#32 <<< 30 + x = x + x.sdiv 1073741824#32 * 3221225472#32 := by
+  bv_decide

Eval/gand2_proof.lean

@@ -0,0 +1,28 @@
+import LeanSAT.Tactics.BVDecide
+
+open Std (BitVec)
+theorem test9_thm (x : _root_.BitVec 64) :
+    x * 18446744073709551615#64 &&& 1#64 = x &&& 1#64 := by
+  bv_decide
+
+set_option sat.timeout 1
+theorem test10_thm (x : _root_.BitVec 64) :
+  x * 18446744073709551615#64 + (x * 18446744073709551615#64 &&& 1#64) =
+    18446744073709551615#64 * (x &&& 18446744073709551614#64) := by
+  bv_decide
+
+theorem test11_thm (x x_1 : _root_.BitVec 32) :
+  x_1 <<< 8 * (x_1 <<< 8 + x &&& 128#32) = x_1 <<< 8 * (x &&& 128#32) := by
+  bv_decide
+
+theorem test12_thm (x x_1 : _root_.BitVec 32) :
+  x <<< 8 * (x_1 + x <<< 8 &&& 128#32) = x <<< 8 * (x_1 &&& 128#32) := by
+  bv_decide
+
+theorem test13_thm (x x_1 : _root_.BitVec 32) :
+  x <<< 8 * (x_1 + x <<< 8 * 4294967295#32 &&& 128#32) = x <<< 8 * (x_1 &&& 128#32) := by
+  bv_decide
+
+theorem test14_thm (x x_1 : _root_.BitVec 32) :
+  x_1 <<< 8 * (x_1 <<< 8 + x * 4294967295#32 &&& 128#32) = x_1 <<< 8 * (x * 4294967295#32 &&& 128#32) := by
+  bv_decide

Eval/gapinthsub_proof.lean

@@ -0,0 +1,32 @@
+import LeanSAT.Tactics.BVDecide
+
+set_option sat.timeout 1
+open Std (BitVec)
+theorem test6_thm (x x_1 : _root_.BitVec 57) :
+  x_1 + (x_1 &&& x) * 144115188075855871#57 = (x ^^^ 144115188075855871#57) &&& x_1 := by
+  bv_decide
+
+theorem test7_thm (x : _root_.BitVec 77) :
+  151115727451828646838271#77 + 151115727451828646838271#77 * x = x ^^^ 151115727451828646838271#77 := by
+  bv_decide
+#exit
+theorem test8_thm (x : _root_.BitVec 27) :
+    9#27 * x + x * 134217727#27 = x <<< 3 := by
+  bv_decide
+
+theorem test9_thm (x : _root_.BitVec 42) :
+    x + x * 4398046511101#42 = x * 4398046511102#42 := by
+  bv_decide
+
+theorem test12_thm (x : _root_.BitVec 43) :
+    x.sshiftRight 42 * 8796093022207#43 = x >>> 42 := by
+  bv_decide
+
+theorem test13_thm (x : _root_.BitVec 79) :
+    x >>> 78 * 604462909807314587353087#79 = x.sshiftRight 78 := by
+  bv_decide
+
+theorem test16_thm (x : _root_.BitVec 51) :
+    x.sdiv 1123#51 * 2251799813685247#51 = x.sdiv 2251799813684125#51 := by
+  bv_decide
+

Eval/gashrhdemand_proof.lean

@@ -0,0 +1,6 @@
+import LeanSAT.Tactics.BVDecide
+
+open Std (BitVec)
+theorem srem2_ashr_mask_thm (x : _root_.BitVec 32) :
+  (x + x.sdiv 2#32 * 4294967294#32).sshiftRight 31 &&& 2#32 = x + x.sdiv 2#32 * 4294967294#32 &&& 2#32 := by
+  bv_decide

Eval/gdistribute_proof.lean

@@ -0,0 +1,24 @@
+import LeanSAT.Tactics.BVDecide
+
+open Std (BitVec)
+theorem factorize_thm (x : _root_.BitVec 32) :
+    (x ||| 1#32) &&& (x ||| 2#32) = x := by
+  bv_decide
+
+set_option sat.timeout 1
+theorem factorize2_thm (x : _root_.BitVec 32) :
+    3#32 * x + x * 4294967294#32 = x := by
+  bv_decide
+#exit
+theorem factorize4_thm (x x_1 : _root_.BitVec 32) :
+    x_1 <<< 1 * x + x * x_1 * 4294967295#32 = x * x_1 := by
+  bv_decide
+
+theorem factorize5_thm (x x_1 : _root_.BitVec 32) :
+    x_1 * 2#32 * x + x_1 * x * 4294967295#32 = x_1 * x := by
+  bv_decide
+
+theorem expand_thm (x : _root_.BitVec 32) :
+    (x &&& 1#32 ||| 2#32) &&& 1#32 = x &&& 1#32 := by
+  bv_decide
+

Eval/gexact_proof.lean

@@ -0,0 +1,19 @@
+import LeanSAT.Tactics.BVDecide
+
+open Std (BitVec)
+theorem sdiv2_thm (x : _root_.BitVec 32) :
+    x.sdiv 8#32 = x.sshiftRight 3 := by
+  bv_decide
+
+theorem sdiv4_thm (x : _root_.BitVec 32) :
+    x.sdiv 3#32 * 3#32 = x := by
+  bv_decide
+
+theorem sdiv6_thm (x : _root_.BitVec 32) :
+    x.sdiv 3#32 * 4294967293#32 = x * 4294967295#32 := by
+  bv_decide
+
+theorem mul_of_sdiv_fail_ub_thm (x : _root_.BitVec 8) :
+    x.sdiv 6#8 * 250#8 = x * 255#8 := by
+  bv_decide
+

Eval/gfoldhinchofhaddhofhnothxhandhyhtohsubhxhfromhy_proof.lean

@@ -0,0 +1,7 @@
+import LeanSAT.Tactics.BVDecide
+
+set_option sat.timeout 1
+open Std (BitVec)
+theorem t0_thm (x x_1 : _root_.BitVec 32) :
+    (x_1 ^^^ 4294967295#32) + x + 1#32 = x + x_1 * 4294967295#32 := by
+  bv_decide

Eval/gfoldhsubhofhnothtohinchofhadd_proof.lean

@@ -0,0 +1,8 @@
+import LeanSAT.Tactics.BVDecide
+
+open Std (BitVec)
+set_option sat.timeout 1
+theorem p0_scalar_thm (x x_1 : _root_.BitVec 32) :
+    x_1 + (x ^^^ 4294967295#32) * 4294967295#32 = x_1 + x + 1#32 := by
+  bv_decide
+

Eval/glshr_proof.lean

@@ -0,0 +1,15 @@
+import LeanSAT.Tactics.BVDecide
+
+open Std (BitVec)
+theorem lshr_exact_thm (x : _root_.BitVec 8) :
+    (x <<< 2 + 4#8) >>> 2 = x + 1#8 &&& 63#8 := by
+  bv_decide
+
+theorem shl_add_thm (x x_1 : _root_.BitVec 8) :
+    (x_1 <<< 2 + x) >>> 2 = x >>> 2 + x_1 &&& 63#8 := by
+  bv_decide
+
+theorem negative_and_odd_thm (x : _root_.BitVec 32) :
+    (x + x.sdiv 2#32 * 4294967294#32) >>> 31 = x >>> 31 &&& x := by
+  bv_decide
+

Eval/gmul_fold_proof.lean

@@ -0,0 +1,16 @@
+import LeanSAT.Tactics.BVDecide
+
+set_option sat.timeout 1
+open Std (BitVec)
+theorem mul8_low_A0_B0_thm (x x_1 : _root_.BitVec 8) :
+  (x_1 >>> 4 * x + x >>> 4 * x_1) <<< 4 + (x_1 &&& 15#8) * (x &&& 15#8) = x * x_1 := by
+  bv_decide
+
+theorem mul8_low_thm (x x_1 : _root_.BitVec 8) :
+  (x &&& 15#8) * (x_1 &&& 15#8) + (x_1 >>> 4 * (x &&& 15#8) + (x_1 &&& 15#8) * x >>> 4) <<< 4 = x * x_1 := by
+  bv_decide
+
+theorem mul16_low_thm (x x_1 : _root_.BitVec 16) :
+  (x &&& 255#16) * (x_1 &&& 255#16) + (x_1 >>> 8 * (x &&& 255#16) + (x_1 &&& 255#16) * x >>> 8) <<< 8 = x * x_1 := by
+  bv_decide
+

Eval/gnot_proof.lean

@@ -0,0 +1,16 @@
+import LeanSAT.Tactics.BVDecide
+
+set_option sat.timeout 1
+open Std (BitVec)
+theorem not_sub_thm (x : _root_.BitVec 32) :
+    123#32 + x * 4294967295#32 ^^^ 4294967295#32 = x + 4294967172#32 := by
+  bv_decide
+#exit
+theorem not_add_thm (x : _root_.BitVec 32) :
+    x + 123#32 ^^^ 4294967295#32 = x * 4294967295#32 + 4294967172#32 := by
+  bv_decide
+
+theorem not_or_neg_thm (x x_1 : _root_.BitVec 8) :
+    (x_1 * 255#8 ||| x) ^^^ 255#8 = x_1 + 255#8 &&& (x ^^^ 255#8) := by
+  bv_decide
+