fix(oob): require an exact encoding before a constant-index OOB is Proved

Problem: OOBObserver::emit marked every constant-index array OOB as Proved,
even when the path reaching the access was over-approximated (an opaque call
or a truncated loop). The heap and UAF paths already gated on exactEncoding.

Fix: pass exactEncoding(env) into emit and require it alongside a numeral
index before assigning Proved; otherwise the finding is Heuristic.

Test: test_proved_requires_exact_model "[oob]" adds an exact control (stays
Proved) and an opaque-call path (now Heuristic; was Proved).

src/detect/oob_access.cpp

@@ -352,7 +352,8 @@ class OOBObserver : public SafetyObserver {
             if (result == z3::sat) {
                 ++stats_.sat;
                 auto bindings = detect::collectModelBindings(m, idx64, false);
-                emit(idx64, known_len, loc, idx_expr, base_var, std::move(bindings));
+                emit(idx64, known_len, loc, exactEncoding(env), idx_expr, base_var,
+                     std::move(bindings));
                 // M31 R3-oob: fuzz witness with captured model populated.
                 const std::string id = std::string("oob-access:") + loc.file + ":" +
                                        std::to_string(loc.line) + ":" + std::to_string(loc.column);
@@ -762,13 +763,15 @@ class OOBObserver : public SafetyObserver {
         out_.push_back(std::move(f));
     }
 
-    void emit(const z3::expr& idx, int known_len, const ir::SourceLoc& loc,
+    void emit(const z3::expr& idx, int known_len, const ir::SourceLoc& loc, bool exact_model,
               const clang::Expr* idx_expr = nullptr, const clang::VarDecl* base_var = nullptr,
               std::vector<std::pair<std::string, std::string>> model_bindings = {}) {
         Finding f;
         f.kind = FindingKind::OOBAccess;
+        // A constant index proves the access out of bounds only when the path
+        // that reaches it was encoded exactly (docs/research/soundness.md).
         const bool is_const = idx.is_numeral();
-        f.confidence = is_const ? Confidence::Proved : Confidence::Heuristic;
+        f.confidence = is_const && exact_model ? Confidence::Proved : Confidence::Heuristic;
         Location l = locationFromSloc(loc);
         f.locations.push_back(std::move(l));
         f.id = std::string("oob-access:") + f.locations.front().file + ":" +

tests/unit/test_proved_requires_exact_model.cpp

@@ -161,3 +161,29 @@ TEST_CASE("type-trait constants are exact for complete types only", "[proved-con
                                /*c_mode=*/true)
                     .has_value());
 }
+
+TEST_CASE("constant-index array OOB keeps Proved only on an exact encoding",
+          "[proved-contract][oob]") {
+    auto oobConfidence = [](const std::string& code) -> std::optional<fold::Confidence> {
+        auto unit = parse(code);
+        REQUIRE(unit);
+        fold::SolverBudget b;
+        fold::SolverStats s;
+        for (const auto& f : fold::detectOOBAccessInContext(unit->getASTContext(), b, s))
+            if (f.id.rfind("oob-access:", 0) == 0)
+                return f.confidence;
+        return std::nullopt;
+    };
+    SECTION("exact: stays Proved (control)") {
+        const auto c = oobConfidence("int f() { int a[4] = {0}; return a[4]; }");
+        REQUIRE(c.has_value());
+        CHECK(*c == fold::Confidence::Proved);
+    }
+    SECTION("an over-approximated operation on the path: Heuristic") {
+        const auto c = oobConfidence("extern int opaque(int);\n"
+                                     "int f(int k) { int a[4] = {0}; int n = opaque(k);"
+                                     " if (n > 2) return a[4]; return 0; }");
+        REQUIRE(c.has_value());
+        CHECK(*c == fold::Confidence::Heuristic);
+    }
+}