feat: added is valid

Author: andrii-a8c

crates/move-prover-boogie-backend/src/boogie_backend/bytecode_translator.rs

@@ -5371,6 +5371,10 @@ impl<'env> FunctionTranslator<'env> {
                                     srcs[0]
                                 );
                                 emitln!(self.writer(), "assume (forall i:int :: InRangeVec($quantifier_temp_vec, i) ==> ReadVec($quantifier_temp_vec, i) == (if {}({}) then 1 else 0));", fun_name, cr_args(&format!("i + $t{}", srcs[0])));
+                                emitln!(
+                                    self.writer(),
+                                    "assume $IsValid'vec'u64''($quantifier_temp_vec);"
+                                );
                                 emitln!(self.writer(), "$t{} := $0_vec_$sum'u64'($quantifier_temp_vec, 0, LenVec($quantifier_temp_vec));", dests[0]);
                             }
                             QuantifierType::SumMap => {

crates/move-prover-boogie-backend/src/boogie_backend/lib.rs

@@ -22,6 +22,7 @@ use move_stackless_bytecode::{
     dynamic_field_analysis::{self, NameValueInfo},
     function_target_pipeline::{FunctionTargetsHolder, FunctionVariant},
     mono_analysis::{self, MonoInfo, PureQuantifierHelperInfo},
+    stackless_bytecode::QuantifierHelperType,
     verification_analysis,
 };
 
@@ -514,7 +515,12 @@ impl QuantifierHelperInfo {
             "v, start, end".to_string()
         };
 
-        let dst_elem_boogie_type = if matches!(info.qht, QuantifierHelperType::FindIndices) {
+        let dst_elem_boogie_type = if matches!(
+            info.qht,
+            QuantifierHelperType::FindIndex
+                | QuantifierHelperType::FindIndices
+                | QuantifierHelperType::RangeCount
+        ) {
             &Type::Primitive(PrimitiveType::U64)
         } else if matches!(info.qht, QuantifierHelperType::Filter) {
             &params_types[info.li].skip_reference()

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

@@ -999,8 +999,9 @@ function $RangeCountQuantifierHelper_{{FN}}({{QP}}): Vec ({{RT}});
 axiom (forall {{QP}}:: {$RangeCountQuantifierHelper_{{FN}}({{QA}})}
 (
     var res := $RangeCountQuantifierHelper_{{FN}}({{QA}});
-        LenVec(res) == (if start <= end then end - start else 0) &&
-        (forall i: int :: InRangeVec(res, i) ==> ReadVec(res, i) == (if {{FN}}({{EAB}}(i + start){{EAA}}) then 1 else 0))
+        (LenVec(res) == (if start <= end then end - start else 0)) &&
+        (forall i: int :: InRangeVec(res, i) ==> ReadVec(res, i) == (if {{FN}}({{EAB}}(i + start){{EAA}}) then 1 else 0)) &&
+        $IsValid'vec'u64''(res)
     )
 );
 {%- endif %}