feat: rich external loop invariant error messages (#342)

* feat: rich error messages

* cleanup

* cleanup

* feat: added types and 1 more test

Author: andrii-a8c

crates/move-stackless-bytecode/src/move_loop_invariants.rs

@@ -8,6 +8,7 @@ use std::{
 
 use move_model::{
     model::{FunId, FunctionEnv, GlobalEnv, QualifiedId},
+    symbol::Symbol,
     ty::{PrimitiveType, Type},
 };
 
@@ -170,6 +171,15 @@ impl MoveLoopInvariantsProcessor {
         !env.has_errors()
     }
 
+    fn parse_var_name(name: &Symbol, builder: &FunctionDataBuilder) -> String {
+        let name_str = builder.fun_env.symbol_pool().string(*name);
+        if name_str.contains('#') {
+            name_str.split('#').next().unwrap().to_string()
+        } else {
+            name_str.to_string()
+        }
+    }
+
     fn match_invariant_arguments(
         builder: &FunctionDataBuilder,
         loop_inv_env: &FunctionEnv,
@@ -187,12 +197,9 @@ impl MoveLoopInvariantsProcessor {
                 // Note: builder.data.name_to_index usually looks like
                 // n -> 0, i#1#0 -> 1, s#1#0 -> 2
                 for (name, &idx) in &builder.data.name_to_index {
-                    let name_str = builder.fun_env.symbol_pool().string(*name);
-                    if let Some(base_name) = name_str.split('#').next() {
-                        if base_name == param_name_str.as_ref() {
-                            found_idx = Some(idx);
-                            break;
-                        }
+                    if Self::parse_var_name(name, builder) == *param_name_str {
+                        found_idx = Some(idx);
+                        break;
                     }
                 }
             }
@@ -217,10 +224,22 @@ impl MoveLoopInvariantsProcessor {
                     Severity::Error,
                     &builder.fun_env.get_loc(),
                     &format!(
-                        "Loop invariant function {} expects parameter '{}' which is not found in function {}",
+                        "Loop invariant function {} expects parameter '{}' which is not found in function {}.\nAvailable variables: ( {} )",
                         loop_inv_env.get_full_name_str(),
                         param_name_str,
-                        builder.fun_env.get_full_name_str()
+                        builder.fun_env.get_full_name_str(),
+                        builder.data.name_to_index
+                        .iter()
+                        .map(|(name, idx)|
+                            format!(
+                                "{}: {}",
+                                Self::parse_var_name(name, builder),
+                                builder
+                                    .get_local_type(*idx)
+                                    .display(&builder.fun_env.module_env.env.get_type_display_ctx())
+                                    .to_string()
+                            )
+                        ).join(", ")
                     ),
                 );
             }

crates/sui-prover/tests/inputs/loop_invariant/external_invalid_arg_name_macro.move

@@ -0,0 +1,27 @@
+module 0x42::loop_invariant_external_invalid_arg_name_macro_fail;
+
+use prover::prover::ensures;
+
+macro fun test_loop($n: u64): u128 {
+    let mut s: u128 = 0;
+    let mut i = 0;
+
+    while (i < $n) {
+        i = i + 1;
+        s = s + (i as u128);
+    };
+    s
+}
+
+#[spec_only(loop_inv(target = test_spec))]
+#[ext(no_abort)]
+fun loop_inv(i: u64, n: u64, compare: u128): bool {
+    i <= n && (compare == (i as u128) * ((i as u128) + 1) / 2)
+}
+
+#[spec(prove)]
+fun test_spec(n: u64): u128 {
+    let res = test_loop!(n);
+    ensures(res == (n as u128) * ((n as u128) + 1) / 2);
+    res
+}

crates/sui-prover/tests/snapshots/loop_invariant/external_invalid_arg_name.move.snap

@@ -1,10 +1,11 @@
 ---
 source: crates/sui-prover/tests/integration.rs
-assertion_line: 262
+assertion_line: 271
 expression: output
 ---
 exiting with bytecode transformation errors
-error: Loop invariant function loop_invariant_external_invalid_arg_name_fail::loop_inv expects parameter 'compare' which is not found in function loop_invariant_external_invalid_arg_name_fail::test_spec
+error: Loop invariant function loop_invariant_external_invalid_arg_name_fail::loop_inv expects parameter 'compare' which is not found in function loop_invariant_external_invalid_arg_name_fail::test_spec.
+Available variables: ( n: u64, i: u64, s: u128 )
    ┌─ tests/inputs/loop_invariant/external_invalid_arg_name.move:12:1
    │  
 12 │ ╭ fun test_spec(n: u64): u128 {

crates/sui-prover/tests/snapshots/loop_invariant/external_invalid_arg_name_macro.move.snap

@@ -0,0 +1,16 @@
+---
+source: crates/sui-prover/tests/integration.rs
+assertion_line: 271
+expression: output
+---
+exiting with bytecode transformation errors
+error: Loop invariant function loop_invariant_external_invalid_arg_name_macro_fail::loop_inv expects parameter 'compare' which is not found in function loop_invariant_external_invalid_arg_name_macro_fail::test_spec.
+Available variables: ( n: u64, i: u64, res: u128, s: u128 )
+   ┌─ tests/inputs/loop_invariant/external_invalid_arg_name_macro.move:23:1
+   │  
+23 │ ╭ fun test_spec(n: u64): u128 {
+24 │ │     let res = test_loop!(n);
+25 │ │     ensures(res == (n as u128) * ((n as u128) + 1) / 2);
+26 │ │     res
+27 │ │ }
+   │ ╰─^