revise spec (#908)

Author: rahxephon89

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

@@ -810,7 +810,7 @@ impl<'env> FunctionTranslator<'env> {
                 mem_inst_seen.insert(memory);
             }
         }
-
+        let mut dup: Vec<String> = vec![];
         // Declare temporaries for debug tracing and other purposes.
         for (_, (ty, ref bv_flag, cnt)) in self.compute_needed_temps() {
             for i in 0..cnt {
@@ -819,12 +819,12 @@ impl<'env> FunctionTranslator<'env> {
                 } else {
                     boogie_type
                 };
-                emitln!(
-                    writer,
-                    "var {}: {};",
-                    boogie_temp_from_suffix(env, &boogie_type_suffix_bv(env, &ty, *bv_flag), i),
-                    bv_type(env, &ty)
-                );
+                let temp_name =
+                    boogie_temp_from_suffix(env, &boogie_type_suffix_bv(env, &ty, *bv_flag), i);
+                if !dup.contains(&temp_name) {
+                    emitln!(writer, "var {}: {};", temp_name.clone(), bv_type(env, &ty));
+                    dup.push(temp_name);
+                }
             }
         }
 
@@ -2181,7 +2181,13 @@ impl<'env> FunctionTranslator<'env> {
                         self.track_return(*i, srcs[0], bv_flag);
                     }
                     TraceAbort => self.track_abort(&str_local(srcs[0])),
-                    TraceExp(kind, node_id) => self.track_exp(*kind, *node_id, srcs[0]),
+                    TraceExp(kind, node_id) => {
+                        let bv_flag = *global_state
+                            .get_temp_index_oper(mid, fid, srcs[0], baseline_flag)
+                            .unwrap()
+                            == Bitwise;
+                        self.track_exp(*kind, *node_id, srcs[0], bv_flag)
+                    }
                     EmitEvent => {
                         let msg = srcs[0];
                         let handle = srcs[1];
@@ -2484,22 +2490,12 @@ impl<'env> FunctionTranslator<'env> {
         );
     }
 
-    fn track_exp(&self, kind: TraceKind, node_id: NodeId, temp: TempIndex) {
+    fn track_exp(&self, kind: TraceKind, node_id: NodeId, temp: TempIndex, bv_flag: bool) {
         let env = self.parent.env;
         let writer = self.parent.writer;
         let ty = self.get_local_type(temp);
-        let global_state = &self
-            .fun_target
-            .global_env()
-            .get_extension::<GlobalNumberOperationState>()
-            .expect("global number operation state");
         let temp_str = if ty.is_reference() {
-            let new_temp = boogie_temp(
-                env,
-                ty.skip_reference(),
-                0,
-                global_state.get_node_num_oper(node_id) == Bitwise,
-            );
+            let new_temp = boogie_temp(env, ty.skip_reference(), 0, bv_flag);
             emitln!(writer, "{} := $Dereference($t{});", new_temp, temp);
             new_temp
         } else {

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

@@ -24,16 +24,46 @@ module TestFeatures {
 
     spec contains {
         pragma bv=b"0";
+        pragma opaque;
         aborts_if false;
         ensures result == ((feature / 8) < len(features) && spec_contains(features, feature));
     }
 
+    fun is_enabled(feature: u64): bool acquires Features {
+        exists<Features>(@std) &&
+            contains(&borrow_global<Features>(@std).features, feature)
+    }
+
+    spec is_enabled {
+        aborts_if false;
+        pragma timeout = 120;
+        ensures result == (
+            exists<Features>(@std) // this one does not verify
+                && (((feature / 8) < len(global<Features>(@std).features)
+                && spec_contains(global<Features>(@std).features, feature)))
+        );
+    }
+
     fun set(features: &mut vector<u8>, feature: u64, include: bool) {
+        let old_n = vector::length(features); // ghost var
+        let old_features = *features; // ghost var
+        let n = old_n; // ghost var
+
         let byte_index = feature / 8;
         let bit_mask = 1 << ((feature % 8) as u8);
-        while (vector::length(features) <= byte_index) {
-            let len = vector::length(features);
-            vector::insert(features, 0, len)
+        while({
+            spec {
+                invariant n == len(features);
+                invariant n >= old_n;
+                invariant byte_index < old_n ==> len(features) == old_n;
+                invariant byte_index >= old_n ==> len(features) <= byte_index + 1;
+                invariant forall i in 0..old_n: features[i] == old_features[i];
+                invariant forall i in old_n..n: (features[i] as u8) == (0 as u8);
+            };
+            vector::length(features) <= byte_index
+        }) {
+            vector::push_back(features, 0);
+            n = n + 1;
         };
         let entry = vector::borrow_mut(features, byte_index);
         if (include)
@@ -44,6 +74,7 @@ module TestFeatures {
 
     spec set {
         pragma bv=b"0";
+        pragma timeout = 120;
         aborts_if false;
         ensures feature / 8 < len(features);
         ensures include == spec_contains(features, feature);
@@ -92,14 +123,58 @@ module TestFeatures {
         aborts_if signer::address_of(framework) != @std;
     }
 
-    fun enable_feature_flags(feature: u64) acquires Features {
+    public fun disable_feature_flags(disable: vector<u64>) acquires Features {
         let features = &mut borrow_global_mut<Features>(@std).features;
-        set(features, feature, true);
+        let i = 0;
+        let n = vector::length(&disable);
+        while ({
+            spec {
+                invariant i <= n;
+                invariant forall j in 0..i: disable[j] / 8 < len(features) && !spec_contains(features, disable[j]);
+            };
+            i < n
+        }) {
+            set(features, *vector::borrow(&disable, i), false);
+            spec {
+                assert (disable[i] / 8 < len(features) && !spec_contains(features, disable[i]));
+            };
+            i = i + 1;
+        };
+    }
+
+    spec disable_feature_flags {
+        pragma opaque;
+        pragma timeout = 120;
+        modifies global<Features>(@std);
+        let post features = global<Features>(@std).features;
+        ensures forall i in 0..len(disable): (disable[i] / 8 < len(features) && !spec_contains(features, disable[i]));
+    }
+
+    public fun enable_feature_flags(enable: vector<u64>) acquires Features {
+        let features = &mut borrow_global_mut<Features>(@std).features;
+        let i = 0;
+        let n = vector::length(&enable);
+        while ({
+            spec {
+                invariant i <= n;
+                invariant forall j in 0..i: enable[j] / 8 < len(features) && spec_contains(features, enable[j]);
+            };
+            i < n
+        }) {
+            set(features, *vector::borrow(&enable, i), true);
+            spec {
+                assert (enable[i] / 8 < len(features) && spec_contains(features, enable[i]));
+            };
+            i = i + 1;
+        };
     }
 
     spec enable_feature_flags {
-        let post features = borrow_global<Features>(@std).features;
-        ensures spec_contains(features, feature);
+        pragma opaque;
+        pragma timeout = 120;
+        modifies global<Features>(@std);
+        let post features = global<Features>(@std).features;
+        ensures forall i in 0..len(enable): (enable[i] / 8 < len(features) && spec_contains(features, enable[i]));
     }
 
 }