[move-prover] create a choice boogie function on unique ExpData

The choice operator is currently implemented with a property that
if the same choice operator is referred multiple times, the chosen
evidence should stay the same.

This semantics is captured in the newly added
`// Semantics when the same-choice operator is referred`
section in the `choice.move` test case.

This property is implemented by converting a choice operator into
an uninterpreted function in Boogie followed by an axiom to constrain
this uninterpreted function.

However, in this translation process, there is an implicit assumption
that one choice operator will only be called with a one and only one set
of variables (e.g., function arguments/locals, free vars, and memories).
This assumption is valid in the verification of DPN given the limited
uses of the choice operator, but there are violations.

Once case is documented in the following example:

```move
    struct S has drop {
        x: u64
    }

    fun test_less_than_1(x: u64): u64 {
        x - 1
    }

    fun test_less_than_2(s: S): u64 {
        s.x - 1
    }

    spec test_less_than_1 {
        include EnsuresLessThan;
    }

    spec test_less_than_2 {
        include EnsuresLessThan { x: s.x };
    }

    spec schema EnsuresLessThan {
        x: u64;
        result: u64;
        ensures result != (choose i: u64 where i >= x);
    }
```

This choice operator is referred to in two contexts:
- in `test_less_than_1`, it is called with an argument `$t0` of type `u64`
- in `test_less_than_2`, it is called with an argument `$t0` of type `S`

Before this commit, the translation will produce a Boogie type error,
which is due to the fact that the choice operator is only translated
once with `$t0: u64` as its first argument.

Changes in this commit is simple in concept but might not be obvious
from the code:

Before this commit, we are already creating different functions for
the same choice operator if they are specialized with different types.
This is evident in
`lifted_choice_infos: Rc<RefCell<BTreeMap<NodeId, LiftedChoiceInfo>>>`
as `NodeId` being the key.

The change is:
`lifted_choice_infos: Rc<RefCell<HashMap<ExpData, LiftedChoiceInfo>>>`.
So, instead of just using `NodeId`, we use the whole `ExpData`, which
includes the `NodeId` but also the range and body `Exp` as well. If
two choice expressions share exactly the same `Exp` for range and body,
(i.e., their ASTs are exactly the same). We point them to the same
uninterpreted function in Boogie. Otherwise, we create a new
uninterpreted function for each reference to the same choice operator.

Closes: aptos-labs#9772

language/move-model/src/ast.rs

@@ -379,7 +379,7 @@ pub enum ExpData {
         Vec<Vec<Exp>>,
         /// Optional `where` clause
         Option<Exp>,
-        // Body
+        /// Body
         Exp,
     ),
     /// Represents a block which contains a set of variable bindings and an expression

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

@@ -4,7 +4,7 @@
 //! This module translates specification conditions to Boogie code.
 
 use std::{
-    collections::{BTreeMap, BTreeSet, HashMap},
+    collections::{BTreeSet, HashMap},
     rc::Rc,
 };
 
@@ -50,12 +50,14 @@ pub struct SpecTranslator<'env> {
     /// Counter for creating new variables.
     fresh_var_count: RefCell<usize>,
     /// Information about lifted choice expressions. Each choice expression in the
-    /// original program is uniquely identified by the node id. This allows us to capture
-    /// duplication of expressions and map them to the same uninterpreted choice
-    /// function. If an expression is duplicated and then later specialized by a type
+    /// original program is uniquely identified by the choice expression AST (verbatim),
+    /// which includes the node id of the expression.
+    ///
+    /// This allows us to capture duplication of expressions and map them to the same uninterpreted
+    /// choice function. If an expression is duplicated and then later specialized by a type
     /// instantiation, it will have a different node id, but again the same instantiations
     /// map to the same node id, which is the desired semantics.
-    lifted_choice_infos: Rc<RefCell<BTreeMap<NodeId, LiftedChoiceInfo>>>,
+    lifted_choice_infos: Rc<RefCell<HashMap<ExpData, LiftedChoiceInfo>>>,
 }
 
 /// A struct which contains information about a lifted choice expression (like `some x:int: p(x)`).
@@ -338,8 +340,12 @@ impl<'env> SpecTranslator<'env> {
     /// Translate lifted functions for choice expressions.
     fn translate_choice_functions(&self) {
         let env = self.env;
-        let infos = self.lifted_choice_infos.borrow();
-        for (_, info) in infos.iter() {
+        let infos_ref = self.lifted_choice_infos.borrow();
+        // need the sorting here because `lifted_choice_infos` is a hashmap while we want
+        // deterministic ordering of the output. Sorting uses the `.id` field, which represents the
+        // insertion order.
+        let infos_sorted = infos_ref.values().sorted_by(|v1, v2| v1.id.cmp(&v2.id));
+        for info in infos_sorted {
             let fun_name = boogie_choice_fun_name(info.id);
             let result_ty = &env.get_node_type(info.node_id);
             let exp_loc = env.get_node_loc(info.node_id);
@@ -1195,6 +1201,10 @@ impl<'env> SpecTranslator<'env> {
             .temporaries(self.env)
             .into_iter()
             .collect_vec();
+        let used_memory = range_and_body
+            .used_memory(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
@@ -1205,20 +1215,19 @@ impl<'env> SpecTranslator<'env> {
         // 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 used_memory = body.used_memory(self.env).into_iter().collect_vec();
-            LiftedChoiceInfo {
+        let info = choice_infos
+            .entry(range_and_body)
+            .or_insert_with(|| LiftedChoiceInfo {
                 id: choice_count,
                 node_id,
                 kind,
                 free_vars: free_vars.clone(),
                 used_temps: used_temps.clone(),
-                used_memory,
+                used_memory: used_memory.clone(),
                 var: some_var,
                 range: range.1.clone(),
                 condition: body.clone(),
-            }
-        });
+            });
         let fun_name = boogie_choice_fun_name(info.id);
 
         // Construct the arguments. Notice that those might be different for each call of
@@ -1229,7 +1238,7 @@ impl<'env> SpecTranslator<'env> {
             .map(|(s, _)| s.display(self.env.symbol_pool()).to_string())
             .chain(used_temps.iter().map(|(t, _)| format!("$t{}", t)))
             .chain(
-                info.used_memory
+                used_memory
                     .iter()
                     .map(|(m, l)| boogie_resource_memory_name(self.env, m, l)),
             )

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

@@ -47,6 +47,26 @@ error: post-condition does not hold
    =     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:156:9
+    │
+156 │         ensures evidence1 == evidence2;
+    │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+    │
+    =     at tests/sources/functional/choice.move:154
+    =     at tests/sources/functional/choice.move:155
+    =     at tests/sources/functional/choice.move:152: test_different_choice_via_let
+    =     at tests/sources/functional/choice.move:156
+
+error: post-condition does not hold
+    ┌─ tests/sources/functional/choice.move:180:9
+    │
+180 │         ensures choose_some_positive_u64() == choose_another_positive_u64();
+    │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+    │
+    =     at tests/sources/functional/choice.move:178: test_different_choice_via_spec_fun
+    =     at tests/sources/functional/choice.move:180
+
 error: post-condition does not hold
    ┌─ tests/sources/functional/choice.move:70:9
    │
@@ -86,3 +106,29 @@ error: post-condition does not hold
    =     at tests/sources/functional/choice.move:82: test_not_using_min_incorrect
    =     at tests/sources/functional/choice.move:85
    =         `TRACE(choose i in 0..len(result) where result[i] == 2)` = <redacted>
+
+error: post-condition does not hold
+    ┌─ tests/sources/functional/choice.move:217:9
+    │
+217 │         ensures result != (choose i: u64 where i >= k);
+    │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+    │
+    =     at tests/sources/functional/choice.move:234: test_same_choice_different_args_via_schema_2
+    =         result = <redacted>
+    =     at tests/sources/functional/choice.move:235: test_same_choice_different_args_via_schema_2
+    =     at tests/sources/functional/choice.move:217
+
+error: post-condition does not hold
+    ┌─ tests/sources/functional/choice.move:208:9
+    │
+208 │         ensures evidence1 == evidence2;
+    │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+    │
+    =     at tests/sources/functional/choice.move:204: test_same_choice_different_args_via_spec_fun
+    =     at tests/sources/functional/choice.move:206
+    =     at tests/sources/functional/choice.move:207
+    =     at tests/sources/functional/choice.move:204: test_same_choice_different_args_via_spec_fun
+    =         x = <redacted>
+    =         y = <redacted>
+    =         result = <redacted>
+    =     at tests/sources/functional/choice.move:208

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

@@ -47,6 +47,26 @@ error: post-condition does not hold
    =     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:156:9
+    │
+156 │         ensures evidence1 == evidence2;
+    │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+    │
+    =     at tests/sources/functional/choice.move:154
+    =     at tests/sources/functional/choice.move:155
+    =     at tests/sources/functional/choice.move:152: test_different_choice_via_let
+    =     at tests/sources/functional/choice.move:156
+
+error: post-condition does not hold
+    ┌─ tests/sources/functional/choice.move:180:9
+    │
+180 │         ensures choose_some_positive_u64() == choose_another_positive_u64();
+    │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+    │
+    =     at tests/sources/functional/choice.move:178: test_different_choice_via_spec_fun
+    =     at tests/sources/functional/choice.move:180
+
 error: post-condition does not hold
    ┌─ tests/sources/functional/choice.move:85:9
    │
@@ -67,3 +87,29 @@ error: post-condition does not hold
    =     at tests/sources/functional/choice.move:82: test_not_using_min_incorrect
    =     at tests/sources/functional/choice.move:85
    =         `TRACE(choose i in 0..len(result) where result[i] == 2)` = <redacted>
+
+error: post-condition does not hold
+    ┌─ tests/sources/functional/choice.move:217:9
+    │
+217 │         ensures result != (choose i: u64 where i >= k);
+    │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+    │
+    =     at tests/sources/functional/choice.move:234: test_same_choice_different_args_via_schema_2
+    =         result = <redacted>
+    =     at tests/sources/functional/choice.move:235: test_same_choice_different_args_via_schema_2
+    =     at tests/sources/functional/choice.move:217
+
+error: post-condition does not hold
+    ┌─ tests/sources/functional/choice.move:208:9
+    │
+208 │         ensures evidence1 == evidence2;
+    │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+    │
+    =     at tests/sources/functional/choice.move:204: test_same_choice_different_args_via_spec_fun
+    =     at tests/sources/functional/choice.move:206
+    =     at tests/sources/functional/choice.move:207
+    =     at tests/sources/functional/choice.move:204: test_same_choice_different_args_via_spec_fun
+    =         x = <redacted>
+    =         y = <redacted>
+    =         result = <redacted>
+    =     at tests/sources/functional/choice.move:208

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

@@ -107,4 +107,135 @@ module 0x42::TestSome {
         // function, which leads to a type error in boogie.
         test_choice_dup_expected_fail(b)
     }
+
+    // Testing using the same choice in multiple verification targets
+    // ==============================================================
+
+    struct S has drop {
+        x: u64
+    }
+
+    fun test_less_than_1(x: u64): u64 {
+        x - 1
+    }
+
+    fun test_less_than_2(s: S): u64 {
+        s.x - 1
+    }
+
+    spec test_less_than_1 {
+        include EnsuresLessThan;
+    }
+
+    spec test_less_than_2 {
+        include EnsuresLessThan { x: s.x };
+    }
+
+    spec schema EnsuresLessThan {
+        x: u64;
+        result: u64;
+        ensures result != (choose i: u64 where i >= x);
+    }
+
+    // Semantics when the same-choice operator is referred
+    // ===================================================
+
+    // Refer to choice operators via let
+
+    fun test_same_choice_via_let() {}
+    spec test_same_choice_via_let {
+        let evidence = (choose i: u64 where i > 0);
+        ensures evidence == evidence;
+        // expect to pass
+    }
+
+    fun test_different_choice_via_let() {}
+    spec test_different_choice_via_let {
+        let evidence1 = (choose i: u64 where i > 0);
+        let evidence2 = (choose i: u64 where i > 0);
+        ensures evidence1 == evidence2;
+        // expect to fail, even though the choices are the same text-wise
+    }
+
+    // Refer to choice operators via spec fun
+
+    spec fun choose_some_positive_u64(): u64 {
+        choose i: u64 where i > 0
+    }
+    spec fun choose_another_positive_u64(): u64 {
+        choose i: u64 where i > 0
+    }
+    spec fun choose_some_positive_u64_indirect(): u64 {
+        choose_some_positive_u64()
+    }
+
+    fun test_same_choice_via_spec_fun() {}
+    spec test_same_choice_via_spec_fun {
+        ensures choose_some_positive_u64() == choose_some_positive_u64();
+        // expect to pass
+    }
+
+    fun test_different_choice_via_spec_fun() {}
+    spec test_different_choice_via_spec_fun {
+        ensures choose_some_positive_u64() == choose_another_positive_u64();
+        // expect to fail
+    }
+
+    fun test_same_choice_via_spec_fun_indirect() {}
+    spec test_same_choice_via_spec_fun_indirect {
+        ensures choose_some_positive_u64() == choose_some_positive_u64_indirect();
+        // expect to pass
+    }
+
+    // Refer to choice operators w/ arguments via spec fun
+
+    spec fun choose_a_larger_num(n: u64): u64 {
+        choose i: u64 where i > n
+    }
+
+    fun test_same_choice_same_args_via_spec_fun(n: u64): bool { n == 0 }
+    spec test_same_choice_same_args_via_spec_fun {
+        let evidence1 = choose_a_larger_num(n);
+        let evidence2 = choose_a_larger_num(n);
+        ensures evidence1 == evidence2;
+        // expect to pass
+    }
+
+    fun test_same_choice_different_args_via_spec_fun(x: u64, y: u64): bool { x == y }
+    spec test_same_choice_different_args_via_spec_fun {
+        let evidence1 = choose_a_larger_num(x);
+        let evidence2 = choose_a_larger_num(y);
+        ensures evidence1 == evidence2;
+        // expect to fail
+    }
+
+    // Refer to choice operators w/ arguments via schema
+
+    spec schema ResultLessThanK {
+        k: u64;
+        result: u64;
+        ensures result != (choose i: u64 where i >= k);
+    }
+
+    fun test_same_choice_different_args_via_schema(x: u64, y: u64): u64 {
+        if (x >= y) {
+            y - 1
+        } else {
+            x - 1
+        }
+    }
+    spec test_same_choice_different_args_via_schema {
+        include ResultLessThanK {k: x};
+        include ResultLessThanK {k: y};
+        // expect to pass
+    }
+
+    fun test_same_choice_different_args_via_schema_2(): u64 {
+        42
+    }
+    spec test_same_choice_different_args_via_schema_2 {
+        include ResultLessThanK { k: 100 };
+        include ResultLessThanK { k: 10 };
+        // expect to fail
+    }
 }