From 630614dc32b745676950197dea677ec1fdb757df Mon Sep 17 00:00:00 2001 From: JakeSilverman Date: Fri, 10 Oct 2025 14:18:13 -0700 Subject: [PATCH] [Specs] ordered_map and big_ordered_map specs for get and get_and_map --- .../datastructures/big_ordered_map.move | 50 +++++++++++++++++++ .../datastructures/big_ordered_map.spec.move | 19 +++++++ .../sources/datastructures/ordered_map.move | 30 +++++++++++ .../datastructures/ordered_map.spec.move | 15 ++++++ 4 files changed, 114 insertions(+) diff --git a/aptos-move/framework/aptos-framework/sources/datastructures/big_ordered_map.move b/aptos-move/framework/aptos-framework/sources/datastructures/big_ordered_map.move index 7fbd1feac6f60..008ad80f8e293 100644 --- a/aptos-move/framework/aptos-framework/sources/datastructures/big_ordered_map.move +++ b/aptos-move/framework/aptos-framework/sources/datastructures/big_ordered_map.move @@ -2668,4 +2668,54 @@ module aptos_std::big_ordered_map { aborts_if !spec_contains_key(map, 1); } + #[verify_only] + fun test_verify_get() { + let keys: vector = vector[1, 2, 3]; + let values: vector = vector[4, 5, 6]; + let map = new_from(keys, values); + let res1 = map.get(&1); + let res2 = map.get(&4); + spec { + assert keys[0] == 1; + assert keys[1] == 2; + assert keys[2] == 3; + assert res1 == option::spec_some(4 as u64); + assert res2 == option::spec_none(); + assert spec_len(map) == 3; + }; + map.remove(&1); + map.remove(&2); + map.remove(&3); + map.destroy_empty(); + } + + spec test_verify_get { + pragma verify = true; + aborts_if false; + } + + #[verify_only] + fun test_verify_get_and_map() { + let keys: vector = vector[1, 2, 3]; + let values: vector = vector[4, 5, 6]; + let map = new_from(keys, values); + let res1 = map.get_and_map(&1, |x : &u64| *x + 1); + let res2 = map.get_and_map(&4, |x : &u64| *x + 1); + spec { + assert keys[0] == 1; + assert false; + assert res1 == option::spec_some(2 as u64); + assert res2 == option::spec_none(); + assert spec_len(map) == 3; + }; + map.remove(&1); + map.remove(&2); + map.remove(&3); + map.destroy_empty(); + } + + spec test_verify_get_and_map { + pragma verify = true; + } + } diff --git a/aptos-move/framework/aptos-framework/sources/datastructures/big_ordered_map.spec.move b/aptos-move/framework/aptos-framework/sources/datastructures/big_ordered_map.spec.move index 86e4aa195ff1d..f0bdc658fdbc0 100644 --- a/aptos-move/framework/aptos-framework/sources/datastructures/big_ordered_map.spec.move +++ b/aptos-move/framework/aptos-framework/sources/datastructures/big_ordered_map.spec.move @@ -220,6 +220,20 @@ spec aptos_std::big_ordered_map { std::cmp::compare(option::spec_borrow(result), k) == std::cmp::Ordering::Less); } + spec get { + pragma opaque; + pragma verify = false; + aborts_if [abstract] false; + ensures [abstract] spec_contains_key(self, key) ==> result == option::spec_some(spec_get(self, key)); + ensures [abstract] !spec_contains_key(self, key) ==> result == option::spec_none(); + } + + spec get_and_map { + pragma opaque; + pragma verify = false; + ensures [abstract] spec_contains_key(self, key) ==> result == option::spec_some(f(spec_get(self, key))); + ensures [abstract] !spec_contains_key(self, key) ==> result == option::spec_none(); + } spec internal_find { pragma opaque; @@ -246,6 +260,11 @@ spec aptos_std::big_ordered_map { pragma verify = false; } + spec iter_modify { + pragma opaque; + pragma verify = false; + } + spec compute_length { pragma verify = false; pragma opaque; diff --git a/aptos-move/framework/aptos-framework/sources/datastructures/ordered_map.move b/aptos-move/framework/aptos-framework/sources/datastructures/ordered_map.move index 6e8b504b618f8..23f48723ccac1 100644 --- a/aptos-move/framework/aptos-framework/sources/datastructures/ordered_map.move +++ b/aptos-move/framework/aptos-framework/sources/datastructures/ordered_map.move @@ -1506,4 +1506,34 @@ module aptos_std::ordered_map { aborts_if !spec_contains_key(map, 1); } + #[verify_only] + fun test_verify_get() { + let keys: vector = vector[1, 2, 3]; + let values: vector = vector[4, 5, 6]; + let map = new_from(keys, values); + let res1 = map.get(&1); + let res2 = map.get(&4); + spec { + assert keys[0] == 1; + assert res1 == option::spec_some(4 as u64); + assert res2 == option::spec_none(); + assert spec_len(map) == 3; + }; + } + + #[verify_only] + fun test_verify_get_and_map() { + let keys: vector = vector[1, 2, 3]; + let values: vector = vector[4, 5, 6]; + let map = new_from(keys, values); + let res1 = map.get_and_map(&1, |x : &u64| *x + 1); + let res2 = map.get_and_map(&4, |x : &u64| *x + 1); + spec { + assert keys[0] == 1; + assert res1 == option::spec_some(5 as u64); + assert res2 == option::spec_none(); + assert spec_len(map) == 3; + }; + } + } diff --git a/aptos-move/framework/aptos-framework/sources/datastructures/ordered_map.spec.move b/aptos-move/framework/aptos-framework/sources/datastructures/ordered_map.spec.move index 8e7d64ab75f92..3ba2d66d25ac5 100644 --- a/aptos-move/framework/aptos-framework/sources/datastructures/ordered_map.spec.move +++ b/aptos-move/framework/aptos-framework/sources/datastructures/ordered_map.spec.move @@ -51,6 +51,21 @@ spec aptos_std::ordered_map { pragma intrinsic; } + spec get { + pragma opaque; + pragma verify = false; + aborts_if [abstract] false; + ensures [abstract] spec_contains_key(self, key) ==> result == option::spec_some(spec_get(self, key)); + ensures [abstract] !spec_contains_key(self, key) ==> result == option::spec_none(); + } + + spec get_and_map { + pragma opaque; + pragma verify = false; + ensures [abstract] spec_contains_key(self, key) ==> result == option::spec_some(f(spec_get(self, key))); + ensures [abstract] !spec_contains_key(self, key) ==> result == option::spec_none(); + } + spec remove { pragma opaque; pragma verify = false;