fix: three Boogie prelude bugs

1. Unsound axiom in $IndexOfVecMap (native.bpl:588).
   The inner forall referenced ReadVec(v, i) (the found index) instead of
   ReadVec(v, j). Since the outer body forces v[i].key == k, the inner
   !$IsEqual(v[i].key, k) is always false, so the forall becomes
   (j < i ==> false), forcing i == 0. For any vec_map whose target key is
   at index > 0, the axiom is inconsistent — Z3 derives UNSAT and any
   ensures verifies vacuously. Two vec_map tests (get_idx_ok, get_idx_opt_ok)
   had ensures that were only true for empty-pre-insert maps, but verified
   anyway due to this bug. Tests updated to assert the correct post-insert
   index using old_m.length().

2. Mismatched endmacro tag (native.bpl:1548).
   bcs_module opens at line 1516, closed with {% endmacro hash_module %}.
   Tera ignores the name, but it's a clear copy-paste artifact.

3. Drift in vector-array-intern-theory.bpl.
   Sibling vector-array-theory.bpl:117-119 documents that InRangeVec must
   stay non-inlined — it guards many quantifiers and needs to be uninterpreted
   for triggering. Intern version had it {:inline}, plus inlined the range
   check in ContainsVec bypassing InRangeVec entirely. Fixed both.

Not included: the count/sum_map split guard relaxation (proposed as fix #3
in the audit). Empirically caused a matching-pressure regression in
quantifiers_multi_arg_count_loop_ok — the 0 <= start && end <= LenVec(v)
guard was serving as a useful trigger gate. Leaving as-is.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: andreistefanescu

crates/move-prover-boogie-backend/src/boogie_backend/prelude/native.bpl

@@ -585,7 +585,7 @@ axiom (forall v: Vec ($2_vec_map_Entry{{S}}), k: {{K}} :: {$IndexOfVecMap{{S}}(v
     (var i := $IndexOfVecMap{{S}}(v, k);
      if (!$ContainsVecMap{{S}}(v, k)) then i == -1
      else $IsValid'u64'(i) && InRangeVec(v, i) && $IsEqual{{K_S}}(ReadVec(v, i)->$key, k) &&
-        (forall j: int :: $IsValid'u64'(j) && j >= 0 && j < i ==> !$IsEqual{{K_S}}(ReadVec(v, i)->$key, k))));
+        (forall j: int :: $IsValid'u64'(j) && j >= 0 && j < i ==> !$IsEqual{{K_S}}(ReadVec(v, j)->$key, k))));
 
 function $VecMapKeys{{S}}(v: Vec ($2_vec_map_Entry{{S}})): Vec ({{K}});
 axiom (forall v: Vec ($2_vec_map_Entry{{S}}) :: {$VecMapKeys{{S}}(v)}
@@ -1545,7 +1545,7 @@ const $serialized_address_len: int;
 axiom (forall v: int :: {$1_bcs_serialize'address'(v)}
      ( var r := $1_bcs_serialize'address'(v); LenVec(r) == $serialized_address_len));
 {% endif %}
-{% endmacro hash_module %}
+{% endmacro bcs_module %}
 {# Event Module
    ============
 #}

crates/move-prover-boogie-backend/src/boogie_backend/prelude/vector-array-intern-theory.bpl

@@ -126,8 +126,7 @@ function {:inline} SwapVec<T>(v: Vec T, i: int, j: int): Vec T {
 }
 
 function {:inline} ContainsVec<T>(v: Vec T, e: T): bool {
-    (var l := v->l;
-    (exists i: int :: i >= 0 && i < l && v->v[i] == e))
+    (exists i: int :: InRangeVec(v, i) && v->v[i] == e)
 }
 
 function IndexOfVec<T>(v: Vec T, e: T): int;
@@ -137,6 +136,9 @@ axiom {:ctor "Vec"} (forall<T> v: Vec T, e: T :: {IndexOfVec(v, e)}
      else InRangeVec(v, i) && ReadVec(v, i) == e &&
         (forall j: int :: j >= 0 && j < i ==> ReadVec(v, j) != e)));
 
-function {:inline} InRangeVec<T>(v: Vec T, i: int): bool {
+// This function should stay non-inlined as it guards many quantifiers
+// over vectors. It appears important to have this uninterpreted for
+// quantifier triggering.
+function InRangeVec<T>(v: Vec T, i: int): bool {
     i >= 0 && i < LenVec(v)
 }

crates/sui-prover/tests/inputs/vec_map/get_idx_ok.move

@@ -1,6 +1,6 @@
 module 0x42::foo;
 
-use prover::prover::{requires, ensures};
+use prover::prover::{requires, ensures, clone};
 
 use sui::vec_map;
 
@@ -11,7 +11,8 @@ fun foo(m: &mut vec_map::VecMap<u64, u8>) {
 #[spec(prove)]
 fun bar_spec(m: &mut vec_map::VecMap<u64, u8>) {
   requires(!m.contains(&10));
+  let old_m = clone!(m);
   foo(m);
-  ensures(m.get_idx(&10) == 0);
+  ensures(m.get_idx(&10) == old_m.length());
 }
 

crates/sui-prover/tests/inputs/vec_map/get_idx_opt_ok.move

@@ -1,6 +1,6 @@
 module 0x42::foo;
 
-use prover::prover::{requires, ensures};
+use prover::prover::{requires, ensures, clone};
 
 use sui::vec_map;
 
@@ -11,7 +11,8 @@ fun foo(m: &mut vec_map::VecMap<u64, u8>) {
 #[spec(prove)]
 fun bar_spec(m: &mut vec_map::VecMap<u64, u8>) {
   requires(!m.contains(&10));
+  let old_m = clone!(m);
   foo(m);
   ensures(m.get(&10) == 0);
-  ensures(m.get_idx_opt(&10) == option::some(0));
+  ensures(m.get_idx_opt(&10) == option::some(old_m.length()));
 }