[Spec] add boogie native for aggregator_v2 (#14881)

* add native for aggregator_v2

* handle comments

* refactor aptos-natives.bpl

aptos-move/framework/aptos-framework/sources/aggregator_v2/aggregator_v2.move

@@ -38,7 +38,7 @@ module aptos_framework::aggregator_v2 {
     /// The generic type supplied to the aggregator is not supported.
     const EUNSUPPORTED_AGGREGATOR_TYPE: u64 = 7;
 
-    /// Arguments passed to concat exceed max limit of 256 bytes (for prefix and suffix together).
+    /// Arguments passed to concat exceed max limit of 1024 bytes (for prefix and suffix together).
     const ECONCAT_STRING_LENGTH_TOO_LARGE: u64 = 8;
 
     /// The native aggregator function, that is in the move file, is not yet supported.
@@ -194,7 +194,7 @@ module aptos_framework::aggregator_v2 {
     /// Concatenates `before`, `snapshot` and `after` into a single string.
     /// snapshot passed needs to have integer type - currently supported types are u64 and u128.
     /// Raises EUNSUPPORTED_AGGREGATOR_SNAPSHOT_TYPE if called with another type.
-    /// If length of prefix and suffix together exceed 256 bytes, ECONCAT_STRING_LENGTH_TOO_LARGE is raised.
+    /// If length of prefix and suffix together exceeds 1024 bytes, ECONCAT_STRING_LENGTH_TOO_LARGE is raised.
     ///
     /// Parallelism info: This operation enables parallelism.
     public native fun derive_string_concat<IntElement>(before: String, snapshot: &AggregatorSnapshot<IntElement>, after: String): DerivedStringSnapshot;
@@ -209,6 +209,199 @@ module aptos_framework::aggregator_v2 {
     /// DEPRECATED, use derive_string_concat() instead. always raises EAGGREGATOR_FUNCTION_NOT_YET_SUPPORTED.
     public native fun string_concat<IntElement>(before: String, snapshot: &AggregatorSnapshot<IntElement>, after: String): AggregatorSnapshot<String>;
 
+    #[verify_only]
+    fun verify_aggregator_try_add_sub(): Aggregator<u64> {
+        let agg = create_aggregator(10);
+        spec {
+            assert spec_get_max_value(agg) == 10;
+            assert spec_get_value(agg) == 0;
+        };
+        let x = try_add(&mut agg, 5);
+        spec {
+            assert x;
+            assert is_at_least(agg, 5);
+        };
+        let y = try_sub(&mut agg, 6);
+        spec {
+            assert !y;
+            assert spec_get_value(agg) == 5;
+            assert spec_get_max_value(agg) == 10;
+        };
+        let y = try_sub(&mut agg, 4);
+        spec {
+            assert y;
+            assert spec_get_value(agg) == 1;
+            assert spec_get_max_value(agg) == 10;
+        };
+        let x = try_add(&mut agg, 11);
+        spec {
+            assert !x;
+            assert spec_get_value(agg) == 1;
+            assert spec_get_max_value(agg) == 10;
+        };
+        let x = try_add(&mut agg, 9);
+        spec {
+            assert x;
+            assert spec_get_value(agg) == 10;
+            assert spec_get_max_value(agg) == 10;
+        };
+        agg
+    }
+
+    spec verify_aggregator_try_add_sub{
+        ensures spec_get_max_value(result) == 10;
+        ensures spec_get_value(result) == 10;
+        ensures read(result) == 10;
+    }
+
+    #[verify_only]
+    fun verify_aggregator_add_sub(sub_value: u64, add_value: u64) {
+        let agg = create_aggregator(10);
+        add(&mut agg, add_value);
+        spec {
+            assert spec_get_value(agg) == add_value;
+        };
+        sub(&mut agg, sub_value);
+        spec {
+            assert spec_get_value(agg) == add_value - sub_value;
+        };
+    }
+
+    spec verify_aggregator_add_sub(sub_value: u64, add_value: u64) {
+        pragma aborts_if_is_strict;
+        aborts_if add_value > 10;
+        aborts_if sub_value > add_value;
+    }
+
+    #[verify_only]
+    fun verify_correct_read() {
+        let snapshot = create_snapshot(42);
+        spec {
+            assert spec_read_snapshot(snapshot) == 42;
+        };
+        let derived = create_derived_string(std::string::utf8(b"42"));
+        spec {
+            assert spec_read_derived_string(derived).bytes == b"42";
+        };
+    }
+
+    #[verify_only]
+    fun verify_invalid_read(aggregator: &Aggregator<u8>): u8 {
+        read(aggregator)
+    }
+    spec verify_invalid_read {
+        aborts_if true;
+    }
+
+    #[verify_only]
+    fun verify_invalid_is_least(aggregator: &Aggregator<u8>): bool {
+        is_at_least(aggregator, 0)
+    }
+    spec verify_invalid_is_least {
+        aborts_if true;
+    }
+
+    #[verify_only]
+    fun verify_copy_not_yet_supported() {
+        let snapshot = create_snapshot(42);
+        copy_snapshot(&snapshot);
+    }
+
+    spec verify_copy_not_yet_supported {
+        aborts_if true;
+    }
+
+    #[verify_only]
+    fun verify_string_concat1() {
+        let snapshot = create_snapshot(42);
+        let derived = derive_string_concat(std::string::utf8(b"before"), &snapshot, std::string::utf8(b"after"));
+        spec {
+            assert spec_read_derived_string(derived).bytes ==
+                concat(b"before", concat(spec_get_string_value(snapshot).bytes, b"after"));
+        };
+    }
+
+    #[verify_only]
+    fun verify_aggregator_generic<IntElement1: copy + drop, IntElement2: copy+drop>(): (Aggregator<IntElement1>,  Aggregator<IntElement2>){
+        let x = create_unbounded_aggregator<IntElement1>();
+        let y = create_unbounded_aggregator<IntElement2>();
+        (x, y)
+    }
+    spec verify_aggregator_generic <IntElement1: copy + drop, IntElement2: copy+drop>(): (Aggregator<IntElement1>,  Aggregator<IntElement2>) {
+        use aptos_std::type_info;
+        aborts_if type_info::type_name<IntElement1>().bytes != b"u64" && type_info::type_name<IntElement1>().bytes != b"u128";
+        aborts_if type_info::type_name<IntElement2>().bytes != b"u64" && type_info::type_name<IntElement2>().bytes != b"u128";
+    }
+
+    #[verify_only]
+    fun verify_aggregator_generic_add<IntElement: copy + drop>(aggregator: &mut Aggregator<IntElement>, value: IntElement) {
+        try_add(aggregator, value);
+        is_at_least_impl(aggregator, value);
+        // cannot specify aborts_if condition for generic `add`
+        // because comparison is not supported by IntElement
+        add(aggregator, value);
+    }
+    spec verify_aggregator_generic_add<IntElement: copy + drop>(aggregator: &mut Aggregator<IntElement>, value: IntElement) {
+        use aptos_std::type_info;
+        aborts_if type_info::type_name<IntElement>().bytes != b"u64" && type_info::type_name<IntElement>().bytes != b"u128";
+    }
+
+    #[verify_only]
+    fun verify_aggregator_generic_sub<IntElement: copy + drop>(aggregator: &mut Aggregator<IntElement>, value: IntElement) {
+        try_sub(aggregator, value);
+        // cannot specify aborts_if condition for generic `sub`
+        // because comparison is not supported by IntElement
+        sub(aggregator, value);
+    }
+    spec verify_aggregator_generic_sub<IntElement: copy + drop>(aggregator: &mut Aggregator<IntElement>, value: IntElement) {
+        use aptos_std::type_info;
+        aborts_if type_info::type_name<IntElement>().bytes != b"u64" && type_info::type_name<IntElement>().bytes != b"u128";
+    }
+
+    #[verify_only]
+    fun verify_aggregator_invalid_type1() {
+        create_unbounded_aggregator<u8>();
+    }
+    spec verify_aggregator_invalid_type1 {
+        aborts_if true;
+    }
+
+    #[verify_only]
+    fun verify_snapshot_invalid_type1() {
+        use std::option;
+        create_snapshot(option::some(42));
+    }
+    spec verify_snapshot_invalid_type1 {
+        aborts_if true;
+    }
+
+    #[verify_only]
+    fun verify_snapshot_invalid_type2() {
+        create_snapshot(vector[42]);
+    }
+
+    spec verify_snapshot_invalid_type2 {
+        aborts_if true;
+    }
+
+    #[verify_only]
+    fun verify_aggregator_valid_type() {
+        let _agg_1 = create_unbounded_aggregator<u64>();
+        spec {
+            assert spec_get_max_value(_agg_1) == MAX_U64;
+        };
+        let _agg_2 = create_unbounded_aggregator<u128>();
+        spec {
+            assert spec_get_max_value(_agg_2) == MAX_U128;
+        };
+        create_aggregator<u64>(5);
+        create_aggregator<u128>(5);
+    }
+
+    spec verify_aggregator_valid_type {
+        aborts_if false;
+    }
+
     // ========================================
 
     #[test]

aptos-move/framework/aptos-framework/sources/aggregator_v2/aggregator_v2.spec.move

@@ -1,73 +1,109 @@
 spec aptos_framework::aggregator_v2 {
-    spec create_aggregator {
-        // TODO: temporary mockup.
-        pragma opaque;
+
+    spec Aggregator {
+        pragma intrinsic;
     }
 
-    spec create_unbounded_aggregator {
-        // TODO: temporary mockup.
-        pragma opaque;
+    spec max_value<IntElement: copy + drop>(aggregator: &Aggregator<IntElement>): IntElement {
+        pragma intrinsic;
     }
 
-    spec try_add {
-        // TODO: temporary mockup.
-        pragma opaque;
+    spec create_aggregator<IntElement: copy + drop>(max_value: IntElement): Aggregator<IntElement> {
+        pragma intrinsic;
     }
 
-    spec try_sub {
-        // TODO: temporary mockup.
-        pragma opaque;
+    spec create_unbounded_aggregator<IntElement: copy + drop>(): Aggregator<IntElement> {
+        pragma intrinsic;
     }
 
-    spec is_at_least_impl {
-        // TODO: temporary mockup.
-        pragma opaque;
+    spec try_add<IntElement>(aggregator: &mut Aggregator<IntElement>, value: IntElement): bool {
+        pragma intrinsic;
     }
 
-    spec read {
-        // TODO: temporary mockup.
-        pragma opaque;
+    spec add<IntElement>(aggregator: &mut Aggregator<IntElement>, value: IntElement) {
+        pragma intrinsic;
+    }
+
+    spec try_sub<IntElement>(aggregator: &mut Aggregator<IntElement>, value: IntElement): bool {
+        pragma intrinsic;
+    }
+
+    spec sub<IntElement>(aggregator: &mut Aggregator<IntElement>, value: IntElement) {
+        pragma intrinsic;
+    }
+
+    spec is_at_least_impl<IntElement>(aggregator: &Aggregator<IntElement>, min_amount: IntElement): bool {
+        pragma intrinsic;
+    }
+
+    spec read<IntElement>(aggregator: &Aggregator<IntElement>): IntElement {
+        pragma intrinsic;
     }
 
-    spec snapshot {
-        // TODO: temporary mockup.
+    spec snapshot<IntElement>(aggregator: &Aggregator<IntElement>): AggregatorSnapshot<IntElement> {
         pragma opaque;
+        include AbortsIfIntElement<IntElement>;
+        ensures [abstract] result.value == spec_get_value(aggregator);
     }
 
-    spec create_snapshot {
-        // TODO: temporary mockup.
+    spec create_snapshot<IntElement: copy + drop>(value: IntElement): AggregatorSnapshot<IntElement> {
         pragma opaque;
+        include AbortsIfIntElement<IntElement>;
+        ensures [abstract] result.value == value;
     }
 
-    spec read_snapshot {
-        // TODO: temporary mockup.
+    spec read_snapshot<IntElement>(snapshot: &AggregatorSnapshot<IntElement>): IntElement {
         pragma opaque;
+        include AbortsIfIntElement<IntElement>;
+        ensures [abstract] result == snapshot.value;
     }
 
-    spec read_derived_string {
-        // TODO: temporary mockup.
+    spec read_derived_string(snapshot: &DerivedStringSnapshot): String {
         pragma opaque;
+        aborts_if [abstract] false;
+        ensures [abstract] result == snapshot.value;
     }
 
-    spec create_derived_string {
-        // TODO: temporary mockup.
+    spec create_derived_string(value: String): DerivedStringSnapshot {
         pragma opaque;
+        aborts_if [abstract] len(value.bytes) > 1024;
+        ensures [abstract] result.value == value;
     }
 
-    spec derive_string_concat {
-        // TODO: temporary mockup.
+    spec derive_string_concat<IntElement>(before: String, snapshot: &AggregatorSnapshot<IntElement>, after: String): DerivedStringSnapshot {
         pragma opaque;
+        include AbortsIfIntElement<IntElement>;
+        ensures [abstract] result.value.bytes == concat(before.bytes, concat(spec_get_string_value(snapshot).bytes, after.bytes));
+        aborts_if [abstract] len(before.bytes) + len(after.bytes) > 1024;
+    }
+
+    spec schema AbortsIfIntElement<IntElement> {
+        use aptos_std::type_info;
+        aborts_if [abstract] type_info::type_name<IntElement>().bytes != b"u64" && type_info::type_name<IntElement>().bytes != b"u128";
     }
 
     // deprecated
     spec copy_snapshot {
-        // TODO: temporary mockup.
         pragma opaque;
+        aborts_if [abstract] true;
     }
 
     // deprecated
     spec string_concat {
-        // TODO: temporary mockup.
         pragma opaque;
+        aborts_if [abstract] true;
+    }
+
+    // Get aggregator.value
+    spec native fun spec_get_value<IntElement>(aggregator: Aggregator<IntElement>): IntElement;
+    // Get aggregator.max_value
+    spec native fun spec_get_max_value<IntElement>(aggregator: Aggregator<IntElement>): IntElement;
+    // Uninterpreted spec function that translates the value inside aggregator into corresponding string representation
+    spec fun spec_get_string_value<IntElement>(aggregator: AggregatorSnapshot<IntElement>): String;
+    spec fun spec_read_snapshot<IntElement>(snapshot: AggregatorSnapshot<IntElement>): IntElement {
+        snapshot.value
+    }
+    spec fun spec_read_derived_string(snapshot: DerivedStringSnapshot): String {
+        snapshot.value
     }
 }