[move-prover] Fixes a bug in the choose operator.

The implementation of the choose operator attempts to reuse the generated uninterpreted function for the choice if the same source level choice is duplicated. This is needed to ensure that the choice result is the same if the expression is cloned, which happens e.g. if conditions of opaque functions are inserted at caller side, or if choices appear in schemas.

Consider

```
schema S { ensures result == choose i: int: i > 0; }
spec f { include S; include S; }
```
We require that the choice delivers the same value in both inclusions of `S` (otherwise we would create an inconsistency). While the logic for this was there, it was buggy before this PR.

The bug was that temporaries or variables used in the choice may substitute to different values in the insertion context. This PR fixes this bug by computing temporaries and vars again for each application point of the choice.

Closes: aptos-labs#8865

language/move-model/src/ast.rs

@@ -438,8 +438,9 @@ impl ExpData {
     }
 
     /// Returns the free local variables, inclusive their types, used in this expression.
-    pub fn free_vars(&self, env: &GlobalEnv) -> BTreeMap<Symbol, Type> {
-        let mut vars = BTreeMap::new();
+    /// Result is ordered by occurrence.
+    pub fn free_vars(&self, env: &GlobalEnv) -> Vec<(Symbol, Type)> {
+        let mut vars = vec![];
         let mut shadowed = vec![]; // Should be multiset but don't have this
         let mut visitor = |up: bool, e: &ExpData| {
             use ExpData::*;
@@ -461,8 +462,8 @@ impl ExpData {
                     }
                 }
                 if let LocalVar(id, sym) = e {
-                    if !shadowed.contains(sym) {
-                        vars.insert(*sym, env.get_node_type(*id));
+                    if !shadowed.contains(sym) && !vars.iter().any(|(s, _)| s == sym) {
+                        vars.push((*sym, env.get_node_type(*id)));
                     }
                 }
             }
@@ -504,12 +505,14 @@ impl ExpData {
         result
     }
 
-    /// Returns the temporaries used in this expression.
-    pub fn temporaries(&self, env: &GlobalEnv) -> BTreeMap<TempIndex, Type> {
-        let mut temps = BTreeMap::new();
+    /// Returns the temporaries used in this expression. Result is ordered by occurrence.
+    pub fn temporaries(&self, env: &GlobalEnv) -> Vec<(TempIndex, Type)> {
+        let mut temps = vec![];
         let mut visitor = |e: &ExpData| {
             if let ExpData::Temporary(id, idx) = e {
-                temps.insert(*idx, env.get_node_type(*id));
+                if !temps.iter().any(|(i, _)| i == idx) {
+                    temps.push((*idx, env.get_node_type(*id)));
+                }
             }
         };
         self.visit(&mut visitor);
@@ -567,7 +570,10 @@ impl ExpData {
             }
             Lambda(_, _, body) => body.visit_pre_post(visitor),
             Quant(_, _, ranges, triggers, condition, body) => {
-                for (_, range) in ranges {
+                for (decl, range) in ranges {
+                    if let Some(binding) = &decl.binding {
+                        binding.visit_pre_post(visitor);
+                    }
                     range.visit_pre_post(visitor);
                 }
                 for trigger in triggers {

language/move-model/src/builder/module_builder.rs

@@ -1344,8 +1344,8 @@ impl<'env, 'translator> ModuleBuilder<'env, 'translator> {
             // Check whether the inclusion is correct regards usage of post state.
 
             // First check for lets.
-            for name in cond.exp.free_vars(self.parent.env).keys() {
-                if let Some((true, id)) = self.spec_block_lets.get(name) {
+            for (name, _) in cond.exp.free_vars(self.parent.env) {
+                if let Some((true, id)) = self.spec_block_lets.get(&name) {
                     let label_cond = (cond.loc.clone(), "not allowed to use post state".to_owned());
                     let label_let = (
                         self.parent.env.get_node_loc(*id),

language/move-prover/boogie-backend/src/spec_translator.rs

@@ -1213,35 +1213,58 @@ impl<'env> SpecTranslator<'env> {
         range: &(LocalVarDecl, Exp),
         body: &Exp,
     ) {
+        // Reconstruct the choice so we can easily determine used locals and temps.
+        let range_and_body = ExpData::Quant(
+            node_id,
+            kind,
+            vec![range.clone()],
+            vec![],
+            None,
+            body.clone(),
+        );
+        let some_var = range.0.name;
+        let free_vars = range_and_body
+            .free_vars(self.env)
+            .into_iter()
+            .filter(|(s, _)| *s != some_var)
+            .collect_vec();
+        let used_temps = range_and_body
+            .temporaries(self.env)
+            .into_iter()
+            .collect_vec();
+
+        // Create a new uninterpreted function and choice info only if it does not
+        // stem from the same original source than an existing one. This needs to be done to
+        // avoid non-determinism in reasoning with choices resulting from duplication
+        // of the same expressions. Consider a user has written `ensures choose i: ..`.
+        // This expression might be duplicated many times e.g. via opaque function caller
+        // sites. We want that the choice consistently returns the same value in each case;
+        // we can only guarantee this if we use the same uninterpreted function for each instance.
         let mut choice_infos = self.lifted_choice_infos.borrow_mut();
         let choice_count = choice_infos.len();
         let info = choice_infos.entry(node_id).or_insert_with(|| {
-            let some_var = range.0.name;
-            let free_vars = body
-                .free_vars(self.env)
-                .into_iter()
-                .filter(|(s, _)| *s != some_var)
-                .collect_vec();
-            let used_temps = body.temporaries(self.env).into_iter().collect_vec();
             let used_memory = body.used_memory(self.env).into_iter().collect_vec();
             LiftedChoiceInfo {
                 id: choice_count,
                 node_id,
                 kind,
-                free_vars,
-                used_temps,
+                free_vars: free_vars.clone(),
+                used_temps: used_temps.clone(),
                 used_memory,
                 var: some_var,
                 range: range.1.clone(),
                 condition: body.clone(),
             }
         });
         let fun_name = boogie_choice_fun_name(info.id);
-        let args = info
-            .free_vars
+
+        // Construct the arguments. Notice that those might be different for each call of
+        // the choice function, resulting from the choice being injected into multiple contexts
+        // with different substitutions.
+        let args = free_vars
             .iter()
             .map(|(s, _)| s.display(self.env.symbol_pool()).to_string())
-            .chain(info.used_temps.iter().map(|(t, _)| format!("$t{}", t)))
+            .chain(used_temps.iter().map(|(t, _)| format!("$t{}", t)))
             .chain(
                 info.used_memory
                     .iter()

language/move-prover/tests/sources/functional/choice.cvc4_exp

@@ -34,6 +34,21 @@ error: post-condition does not hold
    =     at tests/sources/functional/choice.move:21
    =         `TRACE(choose x: u64 where x >= 4 && x <= 5)` = <redacted>
 
+error: post-condition does not hold
+   ┌─ tests/sources/functional/choice.move:98:9
+   │
+98 │         ensures result == TRACE(choose y: u64 where y > x);
+   │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   │
+   =     at tests/sources/functional/choice.move:98
+   =     at tests/sources/functional/choice.move:93: test_choice_dup_expected_fail
+   =         x = <redacted>
+   =     at tests/sources/functional/choice.move:94: test_choice_dup_expected_fail
+   =         result = <redacted>
+   =     at tests/sources/functional/choice.move:95: test_choice_dup_expected_fail
+   =     at tests/sources/functional/choice.move:98
+   =         `TRACE(choose y: u64 where y > x)` = <redacted>
+
 error: post-condition does not hold
    ┌─ tests/sources/functional/choice.move:70:9
    │

language/move-prover/tests/sources/functional/choice.exp

@@ -34,6 +34,21 @@ error: post-condition does not hold
    =     at tests/sources/functional/choice.move:21
    =         `TRACE(choose x: u64 where x >= 4 && x <= 5)` = <redacted>
 
+error: post-condition does not hold
+   ┌─ tests/sources/functional/choice.move:98:9
+   │
+98 │         ensures result == TRACE(choose y: u64 where y > x);
+   │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   │
+   =     at tests/sources/functional/choice.move:98
+   =     at tests/sources/functional/choice.move:93: test_choice_dup_expected_fail
+   =         x = <redacted>
+   =     at tests/sources/functional/choice.move:94: test_choice_dup_expected_fail
+   =         result = <redacted>
+   =     at tests/sources/functional/choice.move:95: test_choice_dup_expected_fail
+   =     at tests/sources/functional/choice.move:98
+   =         `TRACE(choose y: u64 where y > x)` = <redacted>
+
 error: post-condition does not hold
    ┌─ tests/sources/functional/choice.move:85:9
    │

language/move-prover/tests/sources/functional/choice.move

@@ -85,4 +85,26 @@ module 0x42::TestSome {
         ensures TRACE(choose i in 0..len(result) where result[i] == 2) == 1;
     }
 
+    // Testing choice duplication
+    // ==========================
+
+    // This is only a compilation test. It fails verification.
+
+    fun test_choice_dup_expected_fail(x: u64): u64 {
+        x + 1
+    }
+    spec test_choice_dup_expected_fail {
+        pragma opaque; // making this opaque lets the choice be injected at each call
+        ensures result == TRACE(choose y: u64 where y > x);
+    }
+
+    fun test_choice_use1(a: u64): u64 {
+        test_choice_dup_expected_fail(a)
+    }
+
+    fun test_choice_use2(_a: vector<u64>, b: u64): u64 {
+        // with incorrect use of parameters, this would use $t0 as a parameter to the choice
+        // function, which leads to a type error in boogie.
+        test_choice_dup_expected_fail(b)
+    }
 }