diff --git a/language/move-model/src/intrinsics.rs b/language/move-model/src/intrinsics.rs index b71246b9ae..de4d4efbf6 100644 --- a/language/move-model/src/intrinsics.rs +++ b/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 diff --git a/language/move-model/src/pragmas.rs b/language/move-model/src/pragmas.rs index bf68a32054..a7caf81127 100644 --- a/language/move-model/src/pragmas.rs +++ b/language/move-model/src/pragmas.rs @@ -182,6 +182,106 @@ pub static INTRINSIC_TYPE_MAP_ASSOC_FUNCTIONS: Lazy ]) }); +/// # 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(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(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(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(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(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(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(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(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(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(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(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(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> = + 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,13 +325,12 @@ 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, }, @@ -239,6 +338,19 @@ pub fn is_pragma_valid_for_block( } } +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"; diff --git a/language/move-prover/boogie-backend/src/prelude/native.bpl b/language/move-prover/boogie-backend/src/prelude/native.bpl index 85969bde4e..7828d82e44 100644 --- a/language/move-prover/boogie-backend/src/prelude/native.bpl +++ b/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 ==== #} diff --git a/language/move-prover/boogie-backend/src/spec_translator.rs b/language/move-prover/boogie-backend/src/spec_translator.rs index 527cfcfd9d..ebc698bf2e 100644 --- a/language/move-prover/boogie-backend/src/spec_translator.rs +++ b/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], @@ -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"); } diff --git a/language/move-prover/bytecode/src/data_invariant_instrumentation.rs b/language/move-prover/bytecode/src/data_invariant_instrumentation.rs index d3b5b9d9dc..2a838178f1 100644 --- a/language/move-prover/bytecode/src/data_invariant_instrumentation.rs +++ b/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) }