[move-prover] experimental modeling of a heterogeneous key-value store

language/move-model/src/intrinsics.rs

@@ -10,7 +10,10 @@ use crate::{
     ast::{Operation, PropertyBag, PropertyValue, QualifiedSymbol},
     builder::module_builder::SpecBlockContext,
     model::{IntrinsicId, QualifiedId, SpecFunId},
-    pragmas::{INTRINSIC_PRAGMA, INTRINSIC_TYPE_MAP, INTRINSIC_TYPE_MAP_ASSOC_FUNCTIONS},
+    pragmas::{
+        INTRINSIC_PRAGMA, INTRINSIC_TYPE_KVS, INTRINSIC_TYPE_KVS_ASSOC_FUNCTIONS,
+        INTRINSIC_TYPE_MAP, INTRINSIC_TYPE_MAP_ASSOC_FUNCTIONS,
+    },
     symbol::{Symbol, SymbolPool},
     FunId, GlobalEnv, Loc, ModuleBuilder, StructId,
 };
@@ -104,6 +107,7 @@ pub(crate) fn process_intrinsic_declaration(
     // obtain the associated functions map
     let associated_funs = match target.as_str() {
         INTRINSIC_TYPE_MAP => INTRINSIC_TYPE_MAP_ASSOC_FUNCTIONS.deref(),
+        INTRINSIC_TYPE_KVS => INTRINSIC_TYPE_KVS_ASSOC_FUNCTIONS.deref(),
         _ => {
             builder
                 .parent

language/move-model/src/pragmas.rs

@@ -182,6 +182,106 @@ pub static INTRINSIC_TYPE_MAP_ASSOC_FUNCTIONS: Lazy<BTreeMap<&'static str, bool>
         ])
     });
 
+/// # Pragmas for intrinsic key-value store (KVS) declaration
+
+/// The intrinsic type for key-value store
+pub const INTRINSIC_TYPE_KVS: &str = "kvs";
+
+/// Create a new store with an empty content
+/// `[spec] fun kvs_new(): Store`
+pub const INTRINSIC_FUN_KVS_SPEC_NEW: &str = "kvs_spec_new";
+
+/// Get the value associated with key `k`.
+/// The behavior is undefined
+/// - if `k` does not exist in the map or
+/// - if the value associated with `k` is not of type `V`
+/// `[spec] fun kvs_get<K, V>(s: Store, k: K): V`
+pub const INTRINSIC_FUN_KVS_SPEC_GET: &str = "kvs_spec_get";
+
+/// Set the value associated with key `k` to be `v` and return the new store.
+/// `[spec] fun kvs_set<K, V>(s: Store, k: K, v: V): Store`
+pub const INTRINSIC_FUN_KVS_SPEC_SET: &str = "kvs_spec_set";
+
+/// Remove the entry associated with key `k`
+/// The behavior is undefined
+/// - if `k` does not exist in the store
+/// `[spec] fun kvs_del<K>(s: Store, k: K): Store`
+pub const INTRINSIC_FUN_KVS_SPEC_DEL: &str = "kvs_spec_del";
+
+/// Get the number of entries in the store
+/// `[spec] fun kvs_len(s: Store): num`
+pub const INTRINSIC_FUN_KVS_SPEC_LEN: &str = "kvs_spec_len";
+
+/// Check if the store has an entry associated with key `k`
+/// `[spec] fun kvs_has_key<K>(s: Store, k: K): bool`
+pub const INTRINSIC_FUN_KVS_SPEC_HAS_KEY: &str = "kvs_spec_has_key";
+
+/// Check if the store has an entry associated with key `k` with value type `V`
+/// `[spec] fun kvs_has_key_with_value_type<K, V>(s: Store, k: K): bool`
+pub const INTRINSIC_FUN_KVS_SPEC_HAS_KEY_WITH_VALUE_TYPE: &str = "kvs_spec_has_key_with_value_type";
+
+/// Create a new store with an empty content
+/// `[move] fun kvs_new(): Store`
+pub const INTRINSIC_FUN_KVS_NEW: &str = "kvs_new";
+
+/// Add a new entry to the store, aborts if the key already exists
+/// `[move] fun kvs_add_no_override<K, V>(s: &mut Store, k: K, v: V)`
+pub const INTRINSIC_FUN_KVS_ADD_NO_OVERRIDE: &str = "kvs_add_no_override";
+
+/// Remove an entry from the store, aborts if the key does not exists
+/// `[move] fun kvs_del_must_exist<K>(s: &mut Store, k: K)`
+pub const INTRINSIC_FUN_KVS_DEL_MUST_EXIST: &str = "kvs_add_no_override";
+
+/// Remove an entry from the store, aborts if the key does not exists.
+/// Also aborts if the value type mismatches with existing value.
+/// `[move] fun kvs_del_return_value<K, V>(s: &mut Store, k: K): V`
+pub const INTRINSIC_FUN_KVS_DEL_RETURN_VALUE: &str = "kvs_del_return_value";
+
+/// Immutable borrow of a value from the store, aborts if the key does not exist.
+/// Also aborts if the value type mismatches with existing value.
+/// `[move] fun kvs_borrow<K, V>(s: &Store, k: K): &V`
+pub const INTRINSIC_FUN_KVS_BORROW: &str = "kvs_borrow";
+
+/// Mutable borrow of a value from the store, aborts if the key does not exist.
+/// Also aborts if the value type mismatches with existing value.
+/// `[move] fun kvs_borrow_mut<K, V>(s: &mut Store, k: K): &mut V`
+pub const INTRINSIC_FUN_KVS_BORROW_MUT: &str = "kvs_borrow_mut";
+
+/// Check if the store has an entry associated with key `k`
+/// `[move] fun kvs_has_key<K>(s: &Store, k: K): bool`
+pub const INTRINSIC_FUN_KVS_HAS_KEY: &str = "kvs_has_key";
+
+/// Check if the store has an entry associated with key `k` with value type `V`
+/// `[move] fun kvs_has_key_with_value_type<K, V>(s: &Store, k: K): bool`
+pub const INTRINSIC_FUN_KVS_HAS_KEY_WITH_VALUE_TYPE: &str = "kvs_has_key_with_value_type";
+
+/// Get the number of entries in the store
+/// `[move] fun kvs_len(s: &Store): u64`
+pub const INTRINSIC_FUN_KVS_LEN: &str = "kvs_len";
+
+/// All intrinsic functions associated with the key-value store type
+pub static INTRINSIC_TYPE_KVS_ASSOC_FUNCTIONS: Lazy<BTreeMap<&'static str, bool>> =
+    Lazy::new(|| {
+        BTreeMap::from([
+            (INTRINSIC_FUN_KVS_SPEC_NEW, false),
+            (INTRINSIC_FUN_KVS_SPEC_GET, false),
+            (INTRINSIC_FUN_KVS_SPEC_SET, false),
+            (INTRINSIC_FUN_KVS_SPEC_DEL, false),
+            (INTRINSIC_FUN_KVS_SPEC_LEN, false),
+            (INTRINSIC_FUN_KVS_SPEC_HAS_KEY, false),
+            (INTRINSIC_FUN_KVS_SPEC_HAS_KEY_WITH_VALUE_TYPE, false),
+            (INTRINSIC_FUN_KVS_NEW, true),
+            (INTRINSIC_FUN_KVS_ADD_NO_OVERRIDE, true),
+            (INTRINSIC_FUN_KVS_DEL_MUST_EXIST, true),
+            (INTRINSIC_FUN_KVS_DEL_RETURN_VALUE, true),
+            (INTRINSIC_FUN_KVS_BORROW, true),
+            (INTRINSIC_FUN_KVS_BORROW_MUT, true),
+            (INTRINSIC_FUN_KVS_HAS_KEY, true),
+            (INTRINSIC_FUN_KVS_HAS_KEY_WITH_VALUE_TYPE, true),
+            (INTRINSIC_FUN_KVS_LEN, true),
+        ])
+    });
+
 /// Checks whether a pragma is valid in a specific spec block.
 pub fn is_pragma_valid_for_block(
     symbols: &SymbolPool,
@@ -225,20 +325,32 @@ pub fn is_pragma_valid_for_block(
         ),
         Struct(..) => match pragma {
             INTRINSIC_PRAGMA | BV_PARAM_PROP => true,
-            _ if INTRINSIC_TYPE_MAP_ASSOC_FUNCTIONS.contains_key(pragma) => bag
-                .get(&symbols.make(INTRINSIC_PRAGMA))
-                .map(|v| match v {
-                    PropertyValue::Symbol(s) => symbols.string(*s).as_str() == INTRINSIC_TYPE_MAP,
-                    _ => false,
-                })
-                .unwrap_or(false),
+            _ if INTRINSIC_TYPE_MAP_ASSOC_FUNCTIONS.contains_key(pragma) => {
+                is_intrinsic_type_declared(symbols, bag, INTRINSIC_TYPE_MAP)
+            }
+            _ if INTRINSIC_TYPE_KVS_ASSOC_FUNCTIONS.contains_key(pragma) => {
+                is_intrinsic_type_declared(symbols, bag, INTRINSIC_TYPE_KVS)
+            }
             // all other cases
             _ => false,
         },
         _ => false,
     }
 }
 
+fn is_intrinsic_type_declared(
+    symbols: &SymbolPool,
+    bag: &PropertyBag,
+    intrinsic_type: &str,
+) -> bool {
+    bag.get(&symbols.make(INTRINSIC_PRAGMA))
+        .map(|v| match v {
+            PropertyValue::Symbol(s) => symbols.string(*s).as_str() == intrinsic_type,
+            _ => false,
+        })
+        .unwrap_or(false)
+}
+
 /// Internal property attached to conditions if they are injected via an apply or a module
 /// invariant.
 pub const CONDITION_INJECTED_PROP: &str = "$injected";

language/move-prover/boogie-backend/src/prelude/native.bpl

@@ -451,6 +451,31 @@ function {:inline} {{impl.fun_spec_new}}{{S}}(): {{Self}} {
 {% endmacro table_module %}
 
 
+{# Key-Value Stores
+   =======
+#}
+
+{% macro kvs_type_coding(instance) %}
+{%- set T = instance.name -%}
+{%- set S = "'" ~ instance.suffix ~ "'" -%}
+
+function $EncodeTypedValue{{S}}(v: {{T}}): int;
+axiom (
+  forall v1, v2: {{T}} :: {$EncodeTypedValue{{S}}(v1), $EncodeTypedValue{{S}}(v2)}
+    $IsEqual{{S}}(v1, v2) <==> $EncodeTypedValue{{S}}(v1) == $EncodeTypedValue{{S}}(v2)
+);
+
+function $DecodeTypedValue{{S}}(i: int): {{T}};
+axiom (
+  forall i: int, v: {{T}} :: {$EncodeTypedValue{{S}}(v), $DecodeTypedValue{{S}}(v)}
+    $EncodeTypedValue{{S}}(v) == i <==> $DecodeTypedValue{{S}}(i) == v
+);
+
+function $TestTypedValue{{S}}(i: int): bool;
+
+{% endmacro table_key_encoding %}
+
+
 {# BCS
    ====
 #}

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

@@ -25,7 +25,7 @@ use move_model::{
         FieldId, GlobalEnv, Loc, ModuleEnv, ModuleId, NodeId, QualifiedInstId, SpecFunId,
         SpecVarId, StructId,
     },
-    pragmas::INTRINSIC_TYPE_MAP,
+    pragmas::{INTRINSIC_TYPE_KVS, INTRINSIC_TYPE_MAP},
     symbol::Symbol,
     ty::{PrimitiveType, Type},
     well_known::{TYPE_INFO_SPEC, TYPE_NAME_GET_SPEC, TYPE_NAME_SPEC, TYPE_SPEC_IS_STRUCT},
@@ -1215,7 +1215,7 @@ impl<'env> SpecTranslator<'env> {
 
     fn translate_quant(
         &self,
-        _node_id: NodeId,
+        node_id: NodeId,
         kind: QuantKind,
         ranges: &[(LocalVarDecl, Exp)],
         triggers: &[Vec<Exp>],
@@ -1236,6 +1236,7 @@ impl<'env> SpecTranslator<'env> {
                 Type::Struct(mid, sid, ..) => {
                     let struct_env = self.env.get_struct(mid.qualified(*sid));
                     struct_env.is_intrinsic_of(INTRINSIC_TYPE_MAP)
+                        || struct_env.is_intrinsic_of(INTRINSIC_TYPE_KVS)
                 }
                 Type::Primitive(_)
                 | Type::Tuple(_)
@@ -1279,6 +1280,13 @@ impl<'env> SpecTranslator<'env> {
                     let struct_env = self.env.get_struct(mid.qualified(*sid));
                     if struct_env.is_intrinsic_of(INTRINSIC_TYPE_MAP) {
                         emit!(self.writer, "{}{}: {}", comma, var_name, ty_str(&targs[0]));
+                    } else if struct_env.is_intrinsic_of(INTRINSIC_TYPE_KVS) {
+                        // TODO(mengxu): support quantification over all keys of kv-stores
+                        self.error(
+                            &self.env.get_node_loc(node_id),
+                            "quantification over intrinsic kv-store is not supported yet",
+                        );
+                        return;
                     } else {
                         panic!("unexpected type");
                     }

language/move-prover/bytecode/src/data_invariant_instrumentation.rs

@@ -16,7 +16,7 @@ use move_model::{
     ast::{ConditionKind, Exp, ExpData, QuantKind, TempIndex},
     exp_generator::ExpGenerator,
     model::{FunctionEnv, Loc, NodeId, StructEnv},
-    pragmas::{INTRINSIC_FUN_MAP_SPEC_GET, INTRINSIC_TYPE_MAP},
+    pragmas::{INTRINSIC_FUN_MAP_SPEC_GET, INTRINSIC_TYPE_KVS, INTRINSIC_TYPE_MAP},
     ty::Type,
 };
 
@@ -204,6 +204,13 @@ impl<'a> Instrumenter<'a> {
                     } else {
                         vec![]
                     }
+                } else if struct_env.is_intrinsic_of(INTRINSIC_TYPE_KVS) {
+                    // TODO(mengxu): translate invariants of keys and values in kv-store
+                    env.error(
+                        &env.get_node_loc(value.node_id()),
+                        "data invariants in intrinsic kv-store is not supported yet",
+                    );
+                    vec![]
                 } else {
                     self.translate_invariant_for_struct(deep, value, struct_env, targs)
                 }