chore(acir_formal_proofs): fix and re-run shl/shr (#21938)

Resolves #21845

Author: AztecBot

barretenberg/cpp/src/barretenberg/acir_formal_proofs/README.md

@@ -41,10 +41,10 @@ The verifier uses SMT (Satisfiability Modulo Theories) solving to formally verif
 | Binary::Or  | Unsigned_32   | Unsigned_32   | 5.3          | 0.25      | ✓ | TermType::BVTerm | -      | 20.03.2026 |
 | Binary::Or  | Unsigned_128  | Unsigned_128  | 124          | 0.88      | ✓ | TermType::BVTerm | -      | 20.03.2026 |
 | Binary::Or  | Signed_64     | Signed_64     | 20.7         | -         | ✓ | TermType::BVTerm | -      | 20.03.2026 |
-| Binary::Shl | Unsigned_64   | Unsigned_8    | 43.9         | 2.53      | ✓ | TermType::BVTerm | -      | 20.03.2026 |
-| Binary::Shl | Unsigned_32   | Unsigned_8    | FAILED       | -         | ✗ | TermType::BVTerm | ACIR changed in noir, see [#21845](https://github.com/AztecProtocol/aztec-packages/issues/21845) | 20.03.2026 |
+| Binary::Shl | Unsigned_64   | Unsigned_64   | 5000         | 12        | ✓ | TermType::BVTerm | -      | 20.03.2026 |
+| Binary::Shl | Signed_64     | Signed_64     | 1116         | 6         | ✗ | TermType::BVTerm | - | 20.03.2026 |
 | Binary::Shl | Signed_8      | Signed_8      | 49.6         | 2.54      | ✓ | TermType::BVTerm | -      | 20.03.2026 |
-| Binary::Shr | Unsigned_64   | Unsigned_8    | FAILED       | -         | ✗ | TermType::BVTerm | ACIR changed in noir, see [#21845](https://github.com/AztecProtocol/aztec-packages/issues/21845) | 20.03.2026 |
+| Binary::Shr | Unsigned_64   | Unsigned_64   | 4981         | ~10       | ✓ | TermType::BVTerm | -      | 20.03.2026 |
 | Binary::Shr | Signed_8      | Signed_8      | 235          | -         | ✓ | TermType::BVTerm | -      | 20.03.2026 |
 | Binary::Sub | Unsigned_128  | Unsigned_128  | 4.1          | 0.23      | ✓ | TermType::BVTerm | -      | 20.03.2026 |
 | Binary::Sub | Signed_64     | Signed_64     | 81.6         | 2.86      | ✓ | TermType::BVTerm | -      | 20.03.2026 |

barretenberg/cpp/src/barretenberg/acir_formal_proofs/acir_loader.test.cpp

@@ -287,7 +287,7 @@ TEST(acir_formal_proofs, uint_terms_shl8)
  */
 TEST(acir_formal_proofs, uint_terms_shl32)
 {
-    std::string TESTNAME = "Binary::Shl_Unsigned_32_Unsigned_8";
+    std::string TESTNAME = "Binary::Shl_Unsigned_32_Unsigned_32";
     AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
     smt_solver::Solver solver = loader.get_smt_solver();
     smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver);
@@ -306,7 +306,7 @@ TEST(acir_formal_proofs, uint_terms_shl32)
  */
 TEST(acir_formal_proofs, uint_terms_shr)
 {
-    std::string TESTNAME = "Binary::Shr_Unsigned_64_Unsigned_8";
+    std::string TESTNAME = "Binary::Shr_Unsigned_64_Unsigned_64";
     AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
     smt_solver::Solver solver = loader.get_smt_solver();
     smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver);
@@ -652,6 +652,23 @@ TEST(AcirFormalProofs, SignedShl)
     }
 }
 
+/**
+ * @brief Test for i64 << i64
+ *
+ */
+TEST(AcirFormalProofs, SignedShl64)
+{
+    std::string TESTNAME = "Binary::Shl_Signed_64_Signed_64";
+    AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
+    smt_solver::Solver solver = loader.get_smt_solver();
+    smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver);
+    bool res = verify_shl64(&solver, circuit);
+    EXPECT_FALSE(res);
+    if (res) {
+        save_buggy_witness(TESTNAME, circuit);
+    }
+}
+
 /**
  * @brief Test for i8 >> i8
  *
@@ -669,6 +686,23 @@ TEST(AcirFormalProofs, SignedShr)
     }
 }
 
+/**
+ * @brief Test for i64 >> i64
+ *
+ */
+TEST(AcirFormalProofs, SignedShr64)
+{
+    std::string TESTNAME = "Binary::Shr_Signed_64_Signed_64";
+    AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
+    smt_solver::Solver solver = loader.get_smt_solver();
+    smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver);
+    bool res = verify_shr(&solver, circuit);
+    EXPECT_FALSE(res);
+    if (res) {
+        save_buggy_witness(TESTNAME, circuit);
+    }
+}
+
 /**
  * @brief Test for i64 - i64
  *