Repository: aptos-labs/aptos-core (language: python)

Issue:
[Bug][prover] Bitvector not working in context of aborts_if with clause
Drop the following into the prover functional test dir:

```
module 0x42::test {
    use std::error;

    spec module {
        pragma verify = true;
    }

    fun assert_no_spec(x: u64) {
        assert!(x > 815);
    }

    fun assert_with_spec(x: u64) {
        assert!(x > 815);
    }
    spec assert_with_spec  {
        aborts_if x > 815 with std::error::internal(0) | (0xCA26CBD9BE << 24);
    }
}

```

Boogie error:

```
Move prover returns: [internal] boogie exited with compilation errors:
aborts_if_compiler_codes.bpl(3672,47): Error: invalid type for argument 0 in application of $Or'Bv64': int (expected: bv64)
aborts_if_compiler_codes.bpl(3672,70): Error: invalid type for argument 1 in application of $Or'Bv64': int (expected: bv64)
aborts_if_compiler_codes.bpl(3675,4): Error: mismatched types in assignment command (cannot assign bv64 to int)
3 type checking errors detected in aborts_if_compiler_codes.bpl
```


Discussion / hints:
Automatic type inference and conversion between bv and int type is not complete but we can express this property in an awkward way by using the builtin function `bv2int` and `int2bv`: 

```
    spec assert_with_spec  {
        aborts_if x > 815 with bv2int(int2bv(std::error::internal(0) as u64) | int2bv((0xCA26CBD9BE << 24) as u64));
    }
```

Could there be a better error message which hints to use the conversion functions explicitly, then the errors on boogie level? 
> Could there be a better error message which hints to use the conversion functions explicitly, then the errors on boogie level?

Yes, it is possible but the fix would not be trivial because in some cases constants/variables/temporaries in an expression are automatically converted into a bv type so we need to know when and where we need to insert the conversion and then give hints to users. Will come back to this issue later.


Fix patch:
diff --git a/third_party/move/move-prover/boogie-backend/src/bytecode_translator.rs b/third_party/move/move-prover/boogie-backend/src/bytecode_translator.rs
index d7cfdb3cc53d8..661c782d8aac8 100644
--- a/third_party/move/move-prover/boogie-backend/src/bytecode_translator.rs
+++ b/third_party/move/move-prover/boogie-backend/src/bytecode_translator.rs
@@ -2550,8 +2550,19 @@ impl<'env> FunctionTranslator<'env> {
                     writer.indent();
                     *last_tracked_loc = None;
                     self.track_loc(last_tracked_loc, &loc);
+                    let num_oper_code = global_state
+                        .get_temp_index_oper(mid, fid, *code, baseline_flag)
+                        .unwrap();
+                    let bv2int_str = if *num_oper_code == Bitwise {
+                        format!(
+                            "$int2bv.{}($abort_code)",
+                            boogie_num_type_base(&self.get_local_type(*code))
+                        )
+                    } else {
+                        "$abort_code".to_string()
+                    };
                     let code_str = str_local(*code);
-                    emitln!(writer, "{} := $abort_code;", code_str);
+                    emitln!(writer, "{} := {};", code_str, bv2int_str);
                     self.track_abort(&code_str);
                     emitln!(writer, "goto L{};", target.as_usize());
                     writer.unindent();
@@ -2559,7 +2570,19 @@ impl<'env> FunctionTranslator<'env> {
                 }
             },
             Abort(_, src) => {
-                emitln!(writer, "$abort_code := {};", str_local(*src));
+                let num_oper_code = global_state
+                    .get_temp_index_oper(mid, fid, *src, baseline_flag)
+                    .unwrap();
+                let int2bv_str = if *num_oper_code == Bitwise {
+                    format!(
+                        "$bv2int.{}({})",
+                        boogie_num_type_base(&self.get_local_type(*src)),
+                        str_local(*src)
+                    )
+                } else {
+                    str_local(*src)
+                };
+                emitln!(writer, "$abort_code := {};", int2bv_str);
                 emitln!(writer, "$abort_flag := true;");
                 emitln!(writer, "return;")
             },
@@ -2929,8 +2952,6 @@ impl<'env> FunctionTranslator<'env> {
                     _ => {},
                 },
                 Prop(_, PropKind::Modifies, exp) => {
-                    // global_state.exp_operation_map.get(exp.node_id()) == Bitwise;
-                    //let bv_flag = env.get_node_num_oper(exp.node_id()) == Bitwise;
                     let bv_flag = global_state.get_node_num_oper(exp.node_id()) == Bitwise;
                     need(&BOOL_TYPE, false, 1);
                     need(&self.inst(&env.get_node_type(exp.node_id())), bv_flag, 1)
diff --git a/third_party/move/move-prover/boogie-backend/src/spec_translator.rs b/third_party/move/move-prover/boogie-backend/src/spec_translator.rs
index 7541577b532da..48bac0b40d94c 100644
--- a/third_party/move/move-prover/boogie-backend/src/spec_translator.rs
+++ b/third_party/move/move-prover/boogie-backend/src/spec_translator.rs
@@ -1765,7 +1765,9 @@ impl<'env> SpecTranslator<'env> {
             .env
             .get_extension::<GlobalNumberOperationState>()
             .expect("global number operation state");
-        let oper_base = match self.env.get_node_type(args[0].node_id()).skip_reference() {
+        let binding = self.env.get_node_type(args[0].node_id());
+        let common_type = binding.skip_reference();
+        let oper_base = match common_type {
             Type::Primitive(PrimitiveType::U8) => "Bv8",
             Type::Primitive(PrimitiveType::U16) => "Bv16",
             Type::Primitive(PrimitiveType::U32) => "Bv32",
@@ -1780,7 +1782,18 @@ impl<'env> SpecTranslator<'env> {
             let num_oper_e = global_state.get_node_num_oper(e.node_id());
             let ty_e = self.env.get_node_type(e.node_id());
             if num_oper_e != Bitwise {
-                emit!(self.writer, "$int2bv.{}(", boogie_num_type_base(&ty_e));
+                if matches!(ty_e, Type::Primitive(PrimitiveType::Num)) || ty_e == *common_type {
+                    emit!(
+                        self.writer,
+                        "$int2bv.{}(",
+                        boogie_num_type_base(common_type)
+                    );
+                } else {
+                    self.env.error(
+                        &self.env.get_node_loc(e.node_id()),
+                        "arguments of bit operations must have the same data type",
+                    );
+                }
             }
             self.translate_exp(e);
             if num_oper_e != Bitwise {
diff --git a/third_party/move/move-prover/bytecode-pipeline/src/number_operation_analysis.rs b/third_party/move/move-prover/bytecode-pipeline/src/number_operation_analysis.rs
index b5d52ed6b1aed..64630cdd50d5e 100644
--- a/third_party/move/move-prover/bytecode-pipeline/src/number_operation_analysis.rs
+++ b/third_party/move/move-prover/bytecode-pipeline/src/number_operation_analysis.rs
@@ -16,7 +16,7 @@ use crate::{
 use itertools::Either;
 use move_binary_format::file_format::CodeOffset;
 use move_model::{
-    ast::{Exp, ExpData, TempIndex},
+    ast::{Exp, ExpData, Operation as ASTOperation, TempIndex},
     model::{FieldId, FunId, GlobalEnv, ModuleId, Parameter, StructId},
     ty::{PrimitiveType, Type},
 };
@@ -460,16 +460,42 @@ impl<'a> NumberOperationAnalysis<'a> {
 
                                 for (arg, arg_oper) in args.iter().zip(arg_oper.iter()) {
                                     if merged != *arg_oper {
-                                        // propagate to arg if necessary
-                                        global_state.update_node_oper(
-                                            arg.node_id(),
-                                            merged,
-                                            allow_merge,
-                                        );
-                                        update_temporary(arg, &merged, global_state, state);
+                                        // need to update the num_oper type to avoid insertion of int2bv conversion
+                                        // which is inefficient during SMT solving
+                                        let update_flag = match arg.clone().into() {
+                                            ExpData::Temporary(..)
+                                            | ExpData::LocalVar(..)
+                                            | ExpData::Value(..)
+                                            | ExpData::Call(_, ASTOperation::Cast, _) => true,
+                                            ExpData::Call(
+                                                _,
+                                                ASTOperation::SpecFunction(mid, sid, _),
+                                                _,
+                                            ) => {
+                                                // if the current argument is a call to a recursive spec function
+                                                // we need to update num_oper type, otherwise the boogie generator
+                                                // will incorrectly insert inv2bv conversion
+                                                let module_env =
+                                                    &self.func_target.global_env().get_module(mid);
+                                                let spec_f = module_env.get_spec_fun(sid);
+                                                !spec_f.is_move_fun
+                                                    && self
+                                                        .func_target
+                                                        .global_env()
+                                                        .is_spec_fun_recursive(mid.qualified(sid))
+                                            },
+                                            _ => false,
+                                        };
+                                        if update_flag {
+                                            global_state.update_node_oper(
+                                                arg.node_id(),
+                                                merged,
+                                                allow_merge,
+                                            );
+                                            update_temporary(arg, &merged, global_state, state);
+                                        }
                                     }
                                 }
-
                                 global_state.update_node_oper(*id, merged, allow_merge);
                             }
                         },


Test patch:
diff --git a/.github/workflows/lint-test.yaml b/.github/workflows/lint-test.yaml
index 67c046d6a2b79..a70b517ec7b9b 100644
--- a/.github/workflows/lint-test.yaml
+++ b/.github/workflows/lint-test.yaml
@@ -164,20 +164,7 @@ jobs:
           ref: ${{ github.event.pull_request.head.sha }}
           fetch-depth: 0 # Fetch all git history for accurate target determination
 
-      - name: Check if dev_setup.sh has changed
-        id: check_changes
-        run: |
-          git fetch origin ${{ github.event.pull_request.base.sha }}
-          if git diff --name-only ${{ github.event.pull_request.base.sha }} ${{ github.event.pull_request.head.sha }} | grep -q 'scripts/dev_setup.sh'; then
-            echo "scripts/dev_setup.sh has changed"
-            echo "dev_setup_changed=true" >> $GITHUB_ENV
-          else
-            echo "scripts/dev_setup.sh has not changed"
-            echo "dev_setup_changed=false" >> $GITHUB_ENV
-          fi
-
       - name: Run dev_setup.sh
-        if: env.dev_setup_changed == 'true'
         run: |
           scripts/dev_setup.sh -b -p -r -y -P -t
 
diff --git a/third_party/move/move-prover/tests/sources/functional/bv_aborts.exp b/third_party/move/move-prover/tests/sources/functional/bv_aborts.exp
new file mode 100644
index 0000000000000..1b3d4da31caec
--- /dev/null
+++ b/third_party/move/move-prover/tests/sources/functional/bv_aborts.exp
@@ -0,0 +1,30 @@
+Move prover returns: exiting with model building errors
+error: unsupported language construct
+  ┌─ tests/sources/functional/bv_aborts.move:8:9
+  │
+8 │         assert!(x > 815);
+  │         ^^^^^^ single-parameter assert! macro not supported by this compiler
+
+error: too few arguments
+  ┌─ tests/sources/functional/bv_aborts.move:8:9
+  │
+8 │         assert!(x > 815);
+  │         ^^^^^^^^^^^^^^^^
+  │         │      │
+  │         │      Found 1 argument(s) here
+  │         Invalid call of 'assert'. The call expected 2 argument(s) but got 1
+
+error: unsupported language construct
+   ┌─ tests/sources/functional/bv_aborts.move:12:9
+   │
+12 │         assert!(x > 815);
+   │         ^^^^^^ single-parameter assert! macro not supported by this compiler
+
+error: too few arguments
+   ┌─ tests/sources/functional/bv_aborts.move:12:9
+   │
+12 │         assert!(x > 815);
+   │         ^^^^^^^^^^^^^^^^
+   │         │      │
+   │         │      Found 1 argument(s) here
+   │         Invalid call of 'assert'. The call expected 2 argument(s) but got 1
diff --git a/third_party/move/move-prover/tests/sources/functional/bv_aborts.move b/third_party/move/move-prover/tests/sources/functional/bv_aborts.move
new file mode 100644
index 0000000000000..8fb5c59953cbb
--- /dev/null
+++ b/third_party/move/move-prover/tests/sources/functional/bv_aborts.move
@@ -0,0 +1,18 @@
+module 0x42::test {
+
+    spec module {
+        pragma verify = true;
+    }
+
+    fun assert_no_spec(x: u64) {
+        assert!(x > 815);
+    }
+
+    fun assert_with_spec(x: u64) {
+        assert!(x > 815);
+    }
+    spec assert_with_spec  {
+        // This will fail
+        aborts_if x > 815 with std::error::internal(0) | (0xCA26CBD9BE << 24);
+    }
+}
diff --git a/third_party/move/move-prover/tests/sources/functional/bv_aborts.v2_exp b/third_party/move/move-prover/tests/sources/functional/bv_aborts.v2_exp
new file mode 100644
index 0000000000000..bcdb810526eb5
--- /dev/null
+++ b/third_party/move/move-prover/tests/sources/functional/bv_aborts.v2_exp
@@ -0,0 +1,29 @@
+Move prover returns: exiting with verification errors
+error: function does not abort under this condition
+   ┌─ tests/sources/functional/bv_aborts.move:16:9
+   │
+16 │         aborts_if x > 815 with std::error::internal(0) | (0xCA26CBD9BE << 24);
+   │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   │
+   =     at tests/sources/functional/bv_aborts.move:11: assert_with_spec
+   =         x = <redacted>
+   =     at tests/sources/functional/bv_aborts.move:12: assert_with_spec
+   =     at tests/sources/functional/bv_aborts.move:13: assert_with_spec
+   =     at tests/sources/functional/bv_aborts.move:16: assert_with_spec (spec)
+
+error: abort not covered by any of the `aborts_if` clauses
+   ┌─ tests/sources/functional/bv_aborts.move:14:5
+   │
+12 │           assert!(x > 815);
+   │           ------ abort happened here
+13 │       }
+14 │ ╭     spec assert_with_spec  {
+15 │ │         // This will fail
+16 │ │         aborts_if x > 815 with std::error::internal(0) | (0xCA26CBD9BE << 24);
+17 │ │     }
+   │ ╰─────^
+   │
+   =     at tests/sources/functional/bv_aborts.move:11: assert_with_spec
+   =         x = <redacted>
+   =     at tests/sources/functional/bv_aborts.move:12: assert_with_spec
+   =         ABORTED