From ee1791adc5f6e068d75533094d9f459839eb2c87 Mon Sep 17 00:00:00 2001 From: Teng Zhang Date: Mon, 14 Oct 2024 07:47:31 +0000 Subject: [PATCH] [Spec] add boogie native for aggregator_v2 (#14881) * add native for aggregator_v2 * handle comments * refactor aptos-natives.bpl --- .../aptos-framework/doc/aggregator_v2.md | 837 +++++++++++++++++- .../sources/aggregator_v2/aggregator_v2.move | 197 ++++- .../aggregator_v2/aggregator_v2.spec.move | 100 ++- .../aptos-token-objects/doc/collection.md | 38 + .../sources/collection.move | 21 + aptos-move/framework/src/aptos-natives.bpl | 220 +++++ aptos-move/framework/src/prover.rs | 6 +- .../move-prover/boogie-backend/src/options.rs | 15 + .../move/move-prover/lab/src/benchmark.rs | 6 +- third_party/move/move-prover/src/cli.rs | 11 +- 10 files changed, 1392 insertions(+), 59 deletions(-) diff --git a/aptos-move/framework/aptos-framework/doc/aggregator_v2.md b/aptos-move/framework/aptos-framework/doc/aggregator_v2.md index 38704a60e34f2..a5073c231961b 100644 --- a/aptos-move/framework/aptos-framework/doc/aggregator_v2.md +++ b/aptos-move/framework/aptos-framework/doc/aggregator_v2.md @@ -49,11 +49,29 @@ read, read_snapshot, read_derived_string - [Function `derive_string_concat`](#0x1_aggregator_v2_derive_string_concat) - [Function `copy_snapshot`](#0x1_aggregator_v2_copy_snapshot) - [Function `string_concat`](#0x1_aggregator_v2_string_concat) +- [Function `verify_aggregator_try_add_sub`](#0x1_aggregator_v2_verify_aggregator_try_add_sub) +- [Function `verify_aggregator_add_sub`](#0x1_aggregator_v2_verify_aggregator_add_sub) +- [Function `verify_correct_read`](#0x1_aggregator_v2_verify_correct_read) +- [Function `verify_invalid_read`](#0x1_aggregator_v2_verify_invalid_read) +- [Function `verify_invalid_is_least`](#0x1_aggregator_v2_verify_invalid_is_least) +- [Function `verify_copy_not_yet_supported`](#0x1_aggregator_v2_verify_copy_not_yet_supported) +- [Function `verify_string_concat1`](#0x1_aggregator_v2_verify_string_concat1) +- [Function `verify_aggregator_generic`](#0x1_aggregator_v2_verify_aggregator_generic) +- [Function `verify_aggregator_generic_add`](#0x1_aggregator_v2_verify_aggregator_generic_add) +- [Function `verify_aggregator_generic_sub`](#0x1_aggregator_v2_verify_aggregator_generic_sub) +- [Function `verify_aggregator_invalid_type1`](#0x1_aggregator_v2_verify_aggregator_invalid_type1) +- [Function `verify_snapshot_invalid_type1`](#0x1_aggregator_v2_verify_snapshot_invalid_type1) +- [Function `verify_snapshot_invalid_type2`](#0x1_aggregator_v2_verify_snapshot_invalid_type2) +- [Function `verify_aggregator_valid_type`](#0x1_aggregator_v2_verify_aggregator_valid_type) - [Specification](#@Specification_1) + - [Struct `Aggregator`](#@Specification_1_Aggregator) + - [Function `max_value`](#@Specification_1_max_value) - [Function `create_aggregator`](#@Specification_1_create_aggregator) - [Function `create_unbounded_aggregator`](#@Specification_1_create_unbounded_aggregator) - [Function `try_add`](#@Specification_1_try_add) + - [Function `add`](#@Specification_1_add) - [Function `try_sub`](#@Specification_1_try_sub) + - [Function `sub`](#@Specification_1_sub) - [Function `is_at_least_impl`](#@Specification_1_is_at_least_impl) - [Function `read`](#@Specification_1_read) - [Function `snapshot`](#@Specification_1_snapshot) @@ -64,10 +82,23 @@ read, read_snapshot, read_derived_string - [Function `derive_string_concat`](#@Specification_1_derive_string_concat) - [Function `copy_snapshot`](#@Specification_1_copy_snapshot) - [Function `string_concat`](#@Specification_1_string_concat) + - [Function `verify_aggregator_try_add_sub`](#@Specification_1_verify_aggregator_try_add_sub) + - [Function `verify_aggregator_add_sub`](#@Specification_1_verify_aggregator_add_sub) + - [Function `verify_invalid_read`](#@Specification_1_verify_invalid_read) + - [Function `verify_invalid_is_least`](#@Specification_1_verify_invalid_is_least) + - [Function `verify_copy_not_yet_supported`](#@Specification_1_verify_copy_not_yet_supported) + - [Function `verify_aggregator_generic`](#@Specification_1_verify_aggregator_generic) + - [Function `verify_aggregator_generic_add`](#@Specification_1_verify_aggregator_generic_add) + - [Function `verify_aggregator_generic_sub`](#@Specification_1_verify_aggregator_generic_sub) + - [Function `verify_aggregator_invalid_type1`](#@Specification_1_verify_aggregator_invalid_type1) + - [Function `verify_snapshot_invalid_type1`](#@Specification_1_verify_snapshot_invalid_type1) + - [Function `verify_snapshot_invalid_type2`](#@Specification_1_verify_snapshot_invalid_type2) + - [Function `verify_aggregator_valid_type`](#@Specification_1_verify_aggregator_valid_type) 
use 0x1::error;
 use 0x1::features;
+use 0x1::option;
 use 0x1::string;
@@ -221,7 +252,7 @@ and any calls will raise this error. -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;
@@ -709,7 +740,7 @@ Useful for when object is sometimes created via string_concat(), and sometimes d
 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.
 
@@ -776,11 +807,523 @@ DEPRECATED, use derive_string_concat() instead. always raises EAGGREGATOR_FUNCTI
 
 
 
+
+
+
+
+## Function `verify_aggregator_try_add_sub`
+
+
+
+
#[verify_only]
+fun verify_aggregator_try_add_sub(): aggregator_v2::Aggregator<u64>
+

+
+
+
+

+Implementation
+
+
+
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
+}
+

+
+
+
+

+
+
+
+## Function `verify_aggregator_add_sub`
+
+
+
+
#[verify_only]
+fun verify_aggregator_add_sub(sub_value: u64, add_value: u64)
+

+
+
+
+

+Implementation
+
+
+
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;
+    };
+}
+

+
+
+
+

+
+
+
+## Function `verify_correct_read`
+
+
+
+
#[verify_only]
+fun verify_correct_read()
+

+
+
+
+

+Implementation
+
+
+
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";
+    };
+}
+

+
+
+
+

+
+
+
+## Function `verify_invalid_read`
+
+
+
+
#[verify_only]
+fun verify_invalid_read(aggregator: &aggregator_v2::Aggregator<u8>): u8
+

+
+
+
+

+Implementation
+
+
+
fun verify_invalid_read(aggregator: &Aggregator<u8>): u8 {
+    read(aggregator)
+}
+

+
+
+
+

+
+
+
+## Function `verify_invalid_is_least`
+
+
+
+
#[verify_only]
+fun verify_invalid_is_least(aggregator: &aggregator_v2::Aggregator<u8>): bool
+

+
+
+
+

+Implementation
+
+
+
fun verify_invalid_is_least(aggregator: &Aggregator<u8>): bool {
+    is_at_least(aggregator, 0)
+}
+

+
+
+
+

+
+
+
+## Function `verify_copy_not_yet_supported`
+
+
+
+
#[verify_only]
+fun verify_copy_not_yet_supported()
+

+
+
+
+

+Implementation
+
+
+
fun verify_copy_not_yet_supported() {
+    let snapshot = create_snapshot(42);
+    copy_snapshot(&snapshot);
+}
+

+
+
+
+

+
+
+
+## Function `verify_string_concat1`
+
+
+
+
#[verify_only]
+fun verify_string_concat1()
+

+
+
+
+

+Implementation
+
+
+
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"));
+    };
+}
+

+
+
+
+

+
+
+
+## Function `verify_aggregator_generic`
+
+
+
+
#[verify_only]
+fun verify_aggregator_generic<IntElement1: copy, drop, IntElement2: copy, drop>(): (aggregator_v2::Aggregator<IntElement1>, aggregator_v2::Aggregator<IntElement2>)
+

+
+
+
+

+Implementation
+
+
+
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)
+}
+

+
+
+
+

+
+
+
+## Function `verify_aggregator_generic_add`
+
+
+
+
#[verify_only]
+fun verify_aggregator_generic_add<IntElement: copy, drop>(aggregator: &mut aggregator_v2::Aggregator<IntElement>, value: IntElement)
+

+
+
+
+

+Implementation
+
+
+
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);
+}
+

+
+
+
+

+
+
+
+## Function `verify_aggregator_generic_sub`
+
+
+
+
#[verify_only]
+fun verify_aggregator_generic_sub<IntElement: copy, drop>(aggregator: &mut aggregator_v2::Aggregator<IntElement>, value: IntElement)
+

+
+
+
+

+Implementation
+
+
+
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);
+}
+

+
+
+
+

+
+
+
+## Function `verify_aggregator_invalid_type1`
+
+
+
+
#[verify_only]
+fun verify_aggregator_invalid_type1()
+

+
+
+
+

+Implementation
+
+
+
fun verify_aggregator_invalid_type1() {
+    create_unbounded_aggregator<u8>();
+}
+

+
+
+
+

+
+
+
+## Function `verify_snapshot_invalid_type1`
+
+
+
+
#[verify_only]
+fun verify_snapshot_invalid_type1()
+

+
+
+
+

+Implementation
+
+
+
fun verify_snapshot_invalid_type1() {
+    use std::option;
+    create_snapshot(option::some(42));
+}
+

+
+
+
+

+
+
+
+## Function `verify_snapshot_invalid_type2`
+
+
+
+
#[verify_only]
+fun verify_snapshot_invalid_type2()
+

+
+
+
+

+Implementation
+
+
+
fun verify_snapshot_invalid_type2() {
+    create_snapshot(vector[42]);
+}
+

+
+
+
+

+
+
+
+## Function `verify_aggregator_valid_type`
+
+
+
+
#[verify_only]
+fun verify_aggregator_valid_type()
+

+
+
+
+

+Implementation
+
+
+
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);
+}
+

+
+
+
 

 
 
 
-## Specification
+## Specification
+
+
+
+
+
+
+
native fun spec_get_max_value<IntElement>(aggregator: Aggregator<IntElement>): IntElement;
+

+
+
+
+
+
+
+
+
fun spec_get_string_value<IntElement>(aggregator: AggregatorSnapshot<IntElement>): String;
+

+
+
+
+
+
+
+
+
fun spec_read_snapshot<IntElement>(snapshot: AggregatorSnapshot<IntElement>): IntElement {
+   snapshot.value
+}
+

+
+
+
+
+
+
+
+
fun spec_read_derived_string(snapshot: DerivedStringSnapshot): String {
+   snapshot.value
+}
+

+
+
+
+
+
+### Struct `Aggregator`
+
+
+
struct Aggregator<IntElement> has drop, store
+

+
+
+
+

+

+value: IntElement
+

+

+
+

+

+max_value: IntElement
+

+

+
+

+

+
+
+
+
pragma intrinsic;
+

+
+
+
+
+
+### Function `max_value`
+
+
+
public fun max_value<IntElement: copy, drop>(aggregator: &aggregator_v2::Aggregator<IntElement>): IntElement
+

+
+
+
+
+
pragma intrinsic;
+

+
 
 
 
@@ -794,7 +1337,7 @@ DEPRECATED, use derive_string_concat() instead. always raises EAGGREGATOR_FUNCTI
 
 
 
-
pragma opaque;
+
pragma intrinsic;
 

 
 
@@ -810,7 +1353,7 @@ DEPRECATED, use derive_string_concat() instead. always raises EAGGREGATOR_FUNCTI
 
 
 
-
pragma opaque;
+
pragma intrinsic;
 

 
 
@@ -826,7 +1369,23 @@ DEPRECATED, use derive_string_concat() instead. always raises EAGGREGATOR_FUNCTI
 
 
 
-
pragma opaque;
+
pragma intrinsic;
+

+
+
+
+
+
+### Function `add`
+
+
+
public fun add<IntElement>(aggregator: &mut aggregator_v2::Aggregator<IntElement>, value: IntElement)
+

+
+
+
+
+
pragma intrinsic;
 

 
 
@@ -842,7 +1401,23 @@ DEPRECATED, use derive_string_concat() instead. always raises EAGGREGATOR_FUNCTI
 
 
 
-
pragma opaque;
+
pragma intrinsic;
+

+
+
+
+
+
+### Function `sub`
+
+
+
public fun sub<IntElement>(aggregator: &mut aggregator_v2::Aggregator<IntElement>, value: IntElement)
+

+
+
+
+
+
pragma intrinsic;
 

 
 
@@ -858,7 +1433,7 @@ DEPRECATED, use derive_string_concat() instead. always raises EAGGREGATOR_FUNCTI
 
 
 
-
pragma opaque;
+
pragma intrinsic;
 

 
 
@@ -874,7 +1449,7 @@ DEPRECATED, use derive_string_concat() instead. always raises EAGGREGATOR_FUNCTI
 
 
 
-
pragma opaque;
+
pragma intrinsic;
 

 
 
@@ -891,6 +1466,8 @@ DEPRECATED, use derive_string_concat() instead. always raises EAGGREGATOR_FUNCTI
 
 
 
pragma opaque;
+include AbortsIfIntElement<IntElement>;
+ensures [abstract] result.value == spec_get_value(aggregator);
 

 
 
@@ -907,6 +1484,8 @@ DEPRECATED, use derive_string_concat() instead. always raises EAGGREGATOR_FUNCTI
 
 
 
pragma opaque;
+include AbortsIfIntElement<IntElement>;
+ensures [abstract] result.value == value;
 

 
 
@@ -923,6 +1502,8 @@ DEPRECATED, use derive_string_concat() instead. always raises EAGGREGATOR_FUNCTI
 
 
 
pragma opaque;
+include AbortsIfIntElement<IntElement>;
+ensures [abstract] result == snapshot.value;
 

 
 
@@ -939,6 +1520,8 @@ DEPRECATED, use derive_string_concat() instead. always raises EAGGREGATOR_FUNCTI
 
 
 
pragma opaque;
+aborts_if [abstract] false;
+ensures [abstract] result == snapshot.value;
 

 
 
@@ -955,6 +1538,8 @@ DEPRECATED, use derive_string_concat() instead. always raises EAGGREGATOR_FUNCTI
 
 
 
pragma opaque;
+aborts_if [abstract] len(value.bytes) > 1024;
+ensures [abstract] result.value == value;
 

 
 
@@ -971,6 +1556,20 @@ DEPRECATED, use derive_string_concat() instead. always raises EAGGREGATOR_FUNCTI
 
 
 
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;
+

+
+
+
+
+
+
+
+
schema AbortsIfIntElement<IntElement> {
+    aborts_if [abstract] type_info::type_name<IntElement>().bytes != b"u64" && type_info::type_name<IntElement>().bytes != b"u128";
+}
 

 
 
@@ -988,6 +1587,7 @@ DEPRECATED, use derive_string_concat() instead. always raises EAGGREGATOR_FUNCTI
 
 
 
pragma opaque;
+aborts_if [abstract] true;
 

 
 
@@ -1005,6 +1605,225 @@ DEPRECATED, use derive_string_concat() instead. always raises EAGGREGATOR_FUNCTI
 
 
 
pragma opaque;
+aborts_if [abstract] true;
+

+
+
+
+
+
+
+
+
native fun spec_get_value<IntElement>(aggregator: Aggregator<IntElement>): IntElement;
+

+
+
+
+
+
+### Function `verify_aggregator_try_add_sub`
+
+
+
#[verify_only]
+fun verify_aggregator_try_add_sub(): aggregator_v2::Aggregator<u64>
+

+
+
+
+
+
ensures spec_get_max_value(result) == 10;
+ensures spec_get_value(result) == 10;
+ensures read(result) == 10;
+

+
+
+
+
+
+### Function `verify_aggregator_add_sub`
+
+
+
#[verify_only]
+fun 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;
+

+
+
+
+
+
+### Function `verify_invalid_read`
+
+
+
#[verify_only]
+fun verify_invalid_read(aggregator: &aggregator_v2::Aggregator<u8>): u8
+

+
+
+
+
+
aborts_if true;
+

+
+
+
+
+
+### Function `verify_invalid_is_least`
+
+
+
#[verify_only]
+fun verify_invalid_is_least(aggregator: &aggregator_v2::Aggregator<u8>): bool
+

+
+
+
+
+
aborts_if true;
+

+
+
+
+
+
+### Function `verify_copy_not_yet_supported`
+
+
+
#[verify_only]
+fun verify_copy_not_yet_supported()
+

+
+
+
+
+
aborts_if true;
+

+
+
+
+
+
+### Function `verify_aggregator_generic`
+
+
+
#[verify_only]
+fun verify_aggregator_generic<IntElement1: copy, drop, IntElement2: copy, drop>(): (aggregator_v2::Aggregator<IntElement1>, aggregator_v2::Aggregator<IntElement2>)
+

+
+
+
+
+
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";
+

+
+
+
+
+
+### Function `verify_aggregator_generic_add`
+
+
+
#[verify_only]
+fun verify_aggregator_generic_add<IntElement: copy, drop>(aggregator: &mut aggregator_v2::Aggregator<IntElement>, value: IntElement)
+

+
+
+
+
+
aborts_if type_info::type_name<IntElement>().bytes != b"u64" && type_info::type_name<IntElement>().bytes != b"u128";
+

+
+
+
+
+
+### Function `verify_aggregator_generic_sub`
+
+
+
#[verify_only]
+fun verify_aggregator_generic_sub<IntElement: copy, drop>(aggregator: &mut aggregator_v2::Aggregator<IntElement>, value: IntElement)
+

+
+
+
+
+
aborts_if type_info::type_name<IntElement>().bytes != b"u64" && type_info::type_name<IntElement>().bytes != b"u128";
+

+
+
+
+
+
+### Function `verify_aggregator_invalid_type1`
+
+
+
#[verify_only]
+fun verify_aggregator_invalid_type1()
+

+
+
+
+
+
aborts_if true;
+

+
+
+
+
+
+### Function `verify_snapshot_invalid_type1`
+
+
+
#[verify_only]
+fun verify_snapshot_invalid_type1()
+

+
+
+
+
+
aborts_if true;
+

+
+
+
+
+
+### Function `verify_snapshot_invalid_type2`
+
+
+
#[verify_only]
+fun verify_snapshot_invalid_type2()
+

+
+
+
+
+
aborts_if true;
+

+
+
+
+
+
+### Function `verify_aggregator_valid_type`
+
+
+
#[verify_only]
+fun verify_aggregator_valid_type()
+

+
+
+
+
+
aborts_if false;
 

 
 
diff --git a/aptos-move/framework/aptos-framework/sources/aggregator_v2/aggregator_v2.move b/aptos-move/framework/aptos-framework/sources/aggregator_v2/aggregator_v2.move
index 7e26548bc0abd..c72777051d45d 100644
--- a/aptos-move/framework/aptos-framework/sources/aggregator_v2/aggregator_v2.move
+++ b/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(before: String, snapshot: &AggregatorSnapshot, 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(before: String, snapshot: &AggregatorSnapshot, after: String): AggregatorSnapshot;
 
+    #[verify_only]
+    fun verify_aggregator_try_add_sub(): Aggregator {
+        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 {
+        read(aggregator)
+    }
+    spec verify_invalid_read {
+        aborts_if true;
+    }
+
+    #[verify_only]
+    fun verify_invalid_is_least(aggregator: &Aggregator): 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(): (Aggregator,  Aggregator){
+        let x = create_unbounded_aggregator();
+        let y = create_unbounded_aggregator();
+        (x, y)
+    }
+    spec verify_aggregator_generic (): (Aggregator,  Aggregator) {
+        use aptos_std::type_info;
+        aborts_if type_info::type_name().bytes != b"u64" && type_info::type_name().bytes != b"u128";
+        aborts_if type_info::type_name().bytes != b"u64" && type_info::type_name().bytes != b"u128";
+    }
+
+    #[verify_only]
+    fun verify_aggregator_generic_add(aggregator: &mut Aggregator, 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(aggregator: &mut Aggregator, value: IntElement) {
+        use aptos_std::type_info;
+        aborts_if type_info::type_name().bytes != b"u64" && type_info::type_name().bytes != b"u128";
+    }
+
+    #[verify_only]
+    fun verify_aggregator_generic_sub(aggregator: &mut Aggregator, 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(aggregator: &mut Aggregator, value: IntElement) {
+        use aptos_std::type_info;
+        aborts_if type_info::type_name().bytes != b"u64" && type_info::type_name().bytes != b"u128";
+    }
+
+    #[verify_only]
+    fun verify_aggregator_invalid_type1() {
+        create_unbounded_aggregator();
+    }
+    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();
+        spec {
+            assert spec_get_max_value(_agg_1) == MAX_U64;
+        };
+        let _agg_2 = create_unbounded_aggregator();
+        spec {
+            assert spec_get_max_value(_agg_2) == MAX_U128;
+        };
+        create_aggregator(5);
+        create_aggregator(5);
+    }
+
+    spec verify_aggregator_valid_type {
+        aborts_if false;
+    }
+
     // ========================================
 
     #[test]
diff --git a/aptos-move/framework/aptos-framework/sources/aggregator_v2/aggregator_v2.spec.move b/aptos-move/framework/aptos-framework/sources/aggregator_v2/aggregator_v2.spec.move
index 2395ebed63388..3fabb0fc2c8d3 100644
--- a/aptos-move/framework/aptos-framework/sources/aggregator_v2/aggregator_v2.spec.move
+++ b/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(aggregator: &Aggregator): IntElement {
+        pragma intrinsic;
     }
 
-    spec try_add {
-        // TODO: temporary mockup.
-        pragma opaque;
+    spec create_aggregator(max_value: IntElement): Aggregator {
+        pragma intrinsic;
     }
 
-    spec try_sub {
-        // TODO: temporary mockup.
-        pragma opaque;
+    spec create_unbounded_aggregator(): Aggregator {
+        pragma intrinsic;
     }
 
-    spec is_at_least_impl {
-        // TODO: temporary mockup.
-        pragma opaque;
+    spec try_add(aggregator: &mut Aggregator, value: IntElement): bool {
+        pragma intrinsic;
     }
 
-    spec read {
-        // TODO: temporary mockup.
-        pragma opaque;
+    spec add(aggregator: &mut Aggregator, value: IntElement) {
+        pragma intrinsic;
+    }
+
+    spec try_sub(aggregator: &mut Aggregator, value: IntElement): bool {
+        pragma intrinsic;
+    }
+
+    spec sub(aggregator: &mut Aggregator, value: IntElement) {
+        pragma intrinsic;
+    }
+
+    spec is_at_least_impl(aggregator: &Aggregator, min_amount: IntElement): bool {
+        pragma intrinsic;
+    }
+
+    spec read(aggregator: &Aggregator): IntElement {
+        pragma intrinsic;
     }
 
-    spec snapshot {
-        // TODO: temporary mockup.
+    spec snapshot(aggregator: &Aggregator): AggregatorSnapshot {
         pragma opaque;
+        include AbortsIfIntElement;
+        ensures [abstract] result.value == spec_get_value(aggregator);
     }
 
-    spec create_snapshot {
-        // TODO: temporary mockup.
+    spec create_snapshot(value: IntElement): AggregatorSnapshot {
         pragma opaque;
+        include AbortsIfIntElement;
+        ensures [abstract] result.value == value;
     }
 
-    spec read_snapshot {
-        // TODO: temporary mockup.
+    spec read_snapshot(snapshot: &AggregatorSnapshot): IntElement {
         pragma opaque;
+        include AbortsIfIntElement;
+        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(before: String, snapshot: &AggregatorSnapshot, after: String): DerivedStringSnapshot {
         pragma opaque;
+        include AbortsIfIntElement;
+        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 {
+        use aptos_std::type_info;
+        aborts_if [abstract] type_info::type_name().bytes != b"u64" && type_info::type_name().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(aggregator: Aggregator): IntElement;
+    // Get aggregator.max_value
+    spec native fun spec_get_max_value(aggregator: Aggregator): IntElement;
+    // Uninterpreted spec function that translates the value inside aggregator into corresponding string representation
+    spec fun spec_get_string_value(aggregator: AggregatorSnapshot): String;
+    spec fun spec_read_snapshot(snapshot: AggregatorSnapshot): IntElement {
+        snapshot.value
+    }
+    spec fun spec_read_derived_string(snapshot: DerivedStringSnapshot): String {
+        snapshot.value
     }
 }
diff --git a/aptos-move/framework/aptos-token-objects/doc/collection.md b/aptos-move/framework/aptos-token-objects/doc/collection.md
index 3193210b619f8..0416df35f7d72 100644
--- a/aptos-move/framework/aptos-token-objects/doc/collection.md
+++ b/aptos-move/framework/aptos-token-objects/doc/collection.md
@@ -63,6 +63,8 @@ require adding the field original_name.
 -  [Function `set_description`](#0x4_collection_set_description)
 -  [Function `set_uri`](#0x4_collection_set_uri)
 -  [Function `set_max_supply`](#0x4_collection_set_max_supply)
+-  [Specification](#@Specification_1)
+    -  [Function `increment_supply`](#@Specification_1_increment_supply)
 
 
 
use 0x1::aggregator_v2;
@@ -1824,5 +1826,41 @@ After changing the collection's name, to create tokens - only call functions tha
 
 
 
+
+
+## Specification
+
+
+
+
+### Function `increment_supply`
+
+
+
public(friend) fun increment_supply(collection: &object::Object<collection::Collection>, token: address): option::Option<aggregator_v2::AggregatorSnapshot<u64>>
+

+
+
+
+
+
pragma aborts_if_is_partial;
+let collection_addr = object::object_address(collection);
+let supply = global<ConcurrentSupply>(collection_addr);
+let post supply_post = global<ConcurrentSupply>(collection_addr);
+aborts_if exists<ConcurrentSupply>(collection_addr) &&
+    aggregator_v2::spec_get_value(supply.current_supply) + 1
+        > aggregator_v2::spec_get_max_value(supply.current_supply);
+aborts_if exists<ConcurrentSupply>(collection_addr) &&
+    aggregator_v2::spec_get_value(supply.total_minted) + 1
+        > aggregator_v2::spec_get_max_value(supply.total_minted);
+ensures
+    aggregator_v2::spec_get_max_value(supply.current_supply)
+        == aggregator_v2::spec_get_max_value(supply_post.current_supply);
+ensures exists<ConcurrentSupply>(collection_addr) &&
+    aggregator_v2::spec_get_value(supply.current_supply) + 1
+        <= aggregator_v2::spec_get_max_value(supply.current_supply) ==>
+    aggregator_v2::spec_get_value(supply.current_supply) + 1
+        == aggregator_v2::spec_get_value(supply_post.current_supply);
+

+
 
 [move-book]: https://aptos.dev/move/book/SUMMARY
diff --git a/aptos-move/framework/aptos-token-objects/sources/collection.move b/aptos-move/framework/aptos-token-objects/sources/collection.move
index ae545b241d606..ff81e64d1ea57 100644
--- a/aptos-move/framework/aptos-token-objects/sources/collection.move
+++ b/aptos-move/framework/aptos-token-objects/sources/collection.move
@@ -440,6 +440,27 @@ module aptos_token_objects::collection {
         }
     }
 
+    spec increment_supply {
+        pragma aborts_if_is_partial;
+        let collection_addr = object::object_address(collection);
+        let supply = global(collection_addr);
+        let post supply_post = global(collection_addr);
+        aborts_if exists(collection_addr) &&
+            aggregator_v2::spec_get_value(supply.current_supply) + 1
+                > aggregator_v2::spec_get_max_value(supply.current_supply);
+        aborts_if exists(collection_addr) &&
+            aggregator_v2::spec_get_value(supply.total_minted) + 1
+                > aggregator_v2::spec_get_max_value(supply.total_minted);
+        ensures
+            aggregator_v2::spec_get_max_value(supply.current_supply)
+                == aggregator_v2::spec_get_max_value(supply_post.current_supply);
+        ensures exists(collection_addr) &&
+            aggregator_v2::spec_get_value(supply.current_supply) + 1
+                <= aggregator_v2::spec_get_max_value(supply.current_supply) ==>
+            aggregator_v2::spec_get_value(supply.current_supply) + 1
+                == aggregator_v2::spec_get_value(supply_post.current_supply);
+    }
+
     /// Called by token on burn to decrement supply if there's an appropriate Supply struct.
     public(friend) fun decrement_supply(
         collection: &Object,
diff --git a/aptos-move/framework/src/aptos-natives.bpl b/aptos-move/framework/src/aptos-natives.bpl
index f31f51181e25e..717b510391fdb 100644
--- a/aptos-move/framework/src/aptos-natives.bpl
+++ b/aptos-move/framework/src/aptos-natives.bpl
@@ -16,6 +16,226 @@ procedure {:inline 1} $1_object_exists_at{{S}}(object: int) returns (res: bool)
 
 {%- endfor %}
 
+
+
+
+{%- for instance in aggregator_v2_instances %}
+{%- set S = instance.suffix  -%}
+{%- set T = instance.name -%}
+
+// ==================================================================================
+// Intrinsic implementation of aggregator_v2 for element type `{{instance.suffix}}`
+
+
+datatype $1_aggregator_v2_Aggregator'{{S}}' {
+    $1_aggregator_v2_Aggregator'{{S}}'($value: {{T}}, $max_value: {{T}})
+}
+function {:inline} $Update'$1_aggregator_v2_Aggregator'{{S}}''_value(s: $1_aggregator_v2_Aggregator'{{S}}', x: {{T}}): $1_aggregator_v2_Aggregator'{{S}}' {
+    $1_aggregator_v2_Aggregator'{{S}}'(x, s->$max_value)
+}
+function {:inline} $Update'$1_aggregator_v2_Aggregator'{{S}}''_max_value(s: $1_aggregator_v2_Aggregator'{{S}}', x: {{T}}): $1_aggregator_v2_Aggregator'{{S}}' {
+    $1_aggregator_v2_Aggregator'{{S}}'(s->$value, x)
+}
+function $IsValid'$1_aggregator_v2_Aggregator'{{S}}''(s: $1_aggregator_v2_Aggregator'{{S}}'): bool {
+    $IsValid'{{S}}'(s->$value)
+      && $IsValid'{{S}}'(s->$max_value)
+}
+function {:inline} $IsEqual'$1_aggregator_v2_Aggregator'{{S}}''(s1: $1_aggregator_v2_Aggregator'{{S}}', s2: $1_aggregator_v2_Aggregator'{{S}}'): bool {
+    $IsEqual'{{S}}'(s1->$value, s2->$value)
+      && $IsEqual'{{S}}'(s1->$max_value, s2->$max_value)
+}
+
+procedure {:inline 1} $1_aggregator_v2_create_unbounded_aggregator'{{S}}'() returns (res: $1_aggregator_v2_Aggregator'{{S}}')
+{
+    {% if S == "u64" -%}
+    res := $1_aggregator_v2_Aggregator'{{S}}'(0, $MAX_U64);
+    {% elif S == "u128" -%}
+    res := $1_aggregator_v2_Aggregator'{{S}}'(0, $MAX_U128);
+    {% elif "#" in S -%}
+    if (!$IsEqual'vec'u8''($TypeName({{S}}_info), MakeVec3(117, 54, 52)) && !$IsEqual'vec'u8''($TypeName({{S}}_info), MakeVec4(117, 49, 50, 56))) {
+        call $ExecFailureAbort();
+        return;
+    }
+    {% else -%}
+        call $ExecFailureAbort();
+        return;
+    {% endif -%}
+}
+
+
+    procedure {:inline 1} $1_aggregator_v2_create_aggregator'{{S}}'($max_value: {{T}}) returns (res: $1_aggregator_v2_Aggregator'{{S}}')
+    {
+        {% if S == "u64" or S == "u128"  -%}
+        res := $1_aggregator_v2_Aggregator'{{S}}'(0, $max_value);
+        {% elif "#" in S -%}
+        if (!$IsEqual'vec'u8''($TypeName({{S}}_info), MakeVec3(117, 54, 52)) && !$IsEqual'vec'u8''($TypeName({{S}}_info), MakeVec4(117, 49, 50, 56))) {
+            call $ExecFailureAbort();
+            return;
+        }
+        {% else -%}
+        call $ExecFailureAbort();
+        return;
+        {% endif -%}
+    }
+
+
+    procedure {:inline 1} $1_aggregator_v2_try_add'{{S}}'(aggregator: $Mutation ($1_aggregator_v2_Aggregator'{{S}}'), value: {{T}}) returns (res: bool, aggregator_updated: $Mutation ($1_aggregator_v2_Aggregator'{{S}}'))
+    {
+        {% if S == "u64" or S == "u128"  -%}
+        if ($Dereference(aggregator)->$max_value < value + $Dereference(aggregator)->$value) {
+            res := false;
+            aggregator_updated:= aggregator;
+        } else {
+            res := true;
+            aggregator_updated:= $UpdateMutation(aggregator, $1_aggregator_v2_Aggregator'{{S}}'(value + $Dereference(aggregator)->$value, $Dereference(aggregator)->$max_value));
+        }
+        {% elif "#" in S -%}
+              if (!$IsEqual'vec'u8''($TypeName({{S}}_info), MakeVec3(117, 54, 52)) && !$IsEqual'vec'u8''($TypeName({{S}}_info), MakeVec4(117, 49, 50, 56))) {
+                  call $ExecFailureAbort();
+                  return;
+              }
+        {% else -%}
+            call $ExecFailureAbort();
+            return;
+        {% endif -%}
+    }
+
+    procedure {:inline 1} $1_aggregator_v2_try_sub'{{S}}'(aggregator: $Mutation ($1_aggregator_v2_Aggregator'{{S}}'), value: {{T}}) returns (res: bool, aggregator_updated: $Mutation ($1_aggregator_v2_Aggregator'{{S}}'))
+    {
+        {% if S == "u64" or S == "u128"  -%}
+        if ($Dereference(aggregator)->$value < value) {
+            res := false;
+            aggregator_updated:= aggregator;
+            return;
+        } else {
+            res := true;
+            aggregator_updated:= $UpdateMutation(aggregator, $1_aggregator_v2_Aggregator'{{S}}'($Dereference(aggregator)->$value - value, $Dereference(aggregator)->$max_value));
+            return;
+        }
+        {% elif "#" in S -%}
+         if (!$IsEqual'vec'u8''($TypeName({{S}}_info), MakeVec3(117, 54, 52)) && !$IsEqual'vec'u8''($TypeName({{S}}_info), MakeVec4(117, 49, 50, 56))) {
+             call $ExecFailureAbort();
+             return;
+         }
+        {% else -%}
+            call $ExecFailureAbort();
+            return;
+        {% endif -%}
+    }
+
+    procedure {:inline 1} $1_aggregator_v2_add'{{S}}'(aggregator: $Mutation ($1_aggregator_v2_Aggregator'{{S}}'), value: {{T}}) returns (aggregator_updated: $Mutation ($1_aggregator_v2_Aggregator'{{S}}'))
+    {
+       {% if S == "u64" or S == "u128"  -%}
+       var try_result: bool;
+       var try_aggregator: $Mutation $1_aggregator_v2_Aggregator'{{S}}';
+       call try_result, try_aggregator := $1_aggregator_v2_try_add'{{S}}'(aggregator, value);
+       if (!try_result) {
+           call $ExecFailureAbort();
+           return;
+       }
+       aggregator_updated := try_aggregator;
+       return;
+       {% elif "#" in S -%}
+          var try_result: bool;
+          var try_aggregator: $Mutation $1_aggregator_v2_Aggregator'{{S}}';
+          call try_result, try_aggregator := $1_aggregator_v2_try_add'{{S}}'(aggregator, value);
+          return;
+       {% else -%}
+        call $ExecFailureAbort();
+        return;
+       {% endif -%}
+   }
+
+   procedure {:inline 1} $1_aggregator_v2_sub'{{S}}'(aggregator: $Mutation ($1_aggregator_v2_Aggregator'{{S}}'), value: {{T}}) returns (aggregator_updated: $Mutation ($1_aggregator_v2_Aggregator'{{S}}'))
+   {
+       {% if S == "u64" or S == "u128"  -%}
+          var try_result: bool;
+          var try_aggregator: $Mutation $1_aggregator_v2_Aggregator'{{S}}';
+          call try_result, try_aggregator := $1_aggregator_v2_try_sub'{{S}}'(aggregator, value);
+          if (!try_result) {
+              call $ExecFailureAbort();
+              return;
+          }
+          aggregator_updated := try_aggregator;
+         return;
+       {% elif "#" in S -%}
+          var try_result: bool;
+          var try_aggregator: $Mutation $1_aggregator_v2_Aggregator'{{S}}';
+          call try_result, try_aggregator := $1_aggregator_v2_try_add'{{S}}'(aggregator, value);
+          return;
+       {% else -%}
+        call $ExecFailureAbort();
+        return;
+       {% endif -%}
+   }
+
+   procedure {:inline 1} $1_aggregator_v2_read'{{S}}'(aggregator: $1_aggregator_v2_Aggregator'{{S}}') returns (res: {{T}}) {
+       {% if S == "u64" or S == "u128"  -%}
+       res := aggregator->$value;
+       {% elif "#" in S -%}
+         if (!$IsEqual'vec'u8''($TypeName({{S}}_info), MakeVec3(117, 54, 52)) && !$IsEqual'vec'u8''($TypeName({{S}}_info), MakeVec4(117, 49, 50, 56))) {
+             call $ExecFailureAbort();
+             return;
+         }
+       {% else -%}
+        call $ExecFailureAbort();
+        return;
+       {% endif -%}
+   }
+
+   procedure {:inline 1} $1_aggregator_v2_max_value'{{S}}'(aggregator: $1_aggregator_v2_Aggregator'{{S}}') returns (res: {{T}}) {
+       {% if S == "u64" or S == "u128"  -%}
+       res := aggregator->$max_value;
+       {% elif "#" in S -%}
+         if (!$IsEqual'vec'u8''($TypeName({{S}}_info), MakeVec3(117, 54, 52)) && !$IsEqual'vec'u8''($TypeName({{S}}_info), MakeVec4(117, 49, 50, 56))) {
+             call $ExecFailureAbort();
+             return;
+         }
+       {% else -%}
+        call $ExecFailureAbort();
+        return;
+       {% endif -%}
+   }
+
+   procedure {:inline 1} $1_aggregator_v2_is_at_least_impl'{{S}}'(aggregator: $1_aggregator_v2_Aggregator'{{S}}', min_amount: {{T}}) returns (res: bool)
+   {
+       {% if S == "u64" or S == "u128"  -%}
+          res := aggregator->$value >= min_amount;
+          return;
+       {% elif "#" in S -%}
+         if (!$IsEqual'vec'u8''($TypeName({{S}}_info), MakeVec3(117, 54, 52)) && !$IsEqual'vec'u8''($TypeName({{S}}_info), MakeVec4(117, 49, 50, 56))) {
+             call $ExecFailureAbort();
+             return;
+         }
+       {% else -%}
+        call $ExecFailureAbort();
+        return;
+       {% endif -%}
+   }
+
+function {:inline} $1_aggregator_v2_spec_get_value'{{S}}'(s: $1_aggregator_v2_Aggregator'{{S}}'): {{T}} {
+    s->$value
+}
+
+function {:inline} $1_aggregator_v2_spec_get_max_value'{{S}}'(s: $1_aggregator_v2_Aggregator'{{S}}'): {{T}} {
+    s->$max_value
+}
+
+function {:inline} $1_aggregator_v2_$read'{{S}}'(s: $1_aggregator_v2_Aggregator'{{S}}'): {{T}} {
+    s->$value
+}
+
+{% if S == "u64" or S == "u128" -%}
+   function {:inline} $1_aggregator_v2_$is_at_least_impl'{{S}}'(aggregator: $1_aggregator_v2_Aggregator'{{S}}', min_amount: int): bool
+   {
+       aggregator->$value >= min_amount
+   }
+{% else -%}
+   function $1_aggregator_v2_$is_at_least_impl'{{S}}'(aggregator: $1_aggregator_v2_Aggregator'{{S}}', min_amount: {{T}}): bool;
+{% endif -%}
+
+{%- endfor %}
+
 // ==================================================================================
 // Intrinsic implementation of aggregator and aggregator factory
 
diff --git a/aptos-move/framework/src/prover.rs b/aptos-move/framework/src/prover.rs
index c88b04596f094..fbe8a7fed97a1 100644
--- a/aptos-move/framework/src/prover.rs
+++ b/aptos-move/framework/src/prover.rs
@@ -161,11 +161,7 @@ impl ProverOptions {
         options.backend.custom_natives =
             Some(move_prover_boogie_backend::options::CustomNativeOptions {
                 template_bytes: include_bytes!("aptos-natives.bpl").to_vec(),
-                module_instance_names: vec![(
-                    "0x1::object".to_string(),
-                    "object_instances".to_string(),
-                    true,
-                )],
+                module_instance_names: move_prover_boogie_backend::options::custom_native_options(),
             });
         let mut writer = StandardStream::stderr(ColorChoice::Auto);
         if compiler_version.unwrap_or_default() == CompilerVersion::V1 {
diff --git a/third_party/move/move-prover/boogie-backend/src/options.rs b/third_party/move/move-prover/boogie-backend/src/options.rs
index 5c16b9faa66fd..989095b5659f3 100644
--- a/third_party/move/move-prover/boogie-backend/src/options.rs
+++ b/third_party/move/move-prover/boogie-backend/src/options.rs
@@ -58,6 +58,21 @@ pub struct CustomNativeOptions {
     pub module_instance_names: Vec<(String, String, bool)>,
 }
 
+pub fn custom_native_options() -> Vec<(String, String, bool)> {
+    vec![
+        (
+            "0x1::object".to_string(),
+            "object_instances".to_string(),
+            true,
+        ),
+        (
+            "0x1::aggregator_v2".to_string(),
+            "aggregator_v2_instances".to_string(),
+            true,
+        ),
+    ]
+}
+
 /// Contains information about a native method implementing mutable borrow semantics for a given
 /// type in an alternative storage model (returning &mut without taking appropriate &mut as a
 /// parameter, much like vector::borrow_mut)
diff --git a/third_party/move/move-prover/lab/src/benchmark.rs b/third_party/move/move-prover/lab/src/benchmark.rs
index 6e4ba638f8bca..b05b6515083a4 100644
--- a/third_party/move/move-prover/lab/src/benchmark.rs
+++ b/third_party/move/move-prover/lab/src/benchmark.rs
@@ -178,11 +178,7 @@ fn run_benchmark(
                     "../../../../../aptos-move/framework/src/aptos-natives.bpl"
                 )
                 .to_vec(),
-                module_instance_names: vec![(
-                    "0x1::object".to_string(),
-                    "object_instances".to_string(),
-                    true,
-                )],
+                module_instance_names: move_prover_boogie_backend::options::custom_native_options(),
             });
     }
     // Do not allow any benchmark to run longer than 60s. If this is exceeded it usually
diff --git a/third_party/move/move-prover/src/cli.rs b/third_party/move/move-prover/src/cli.rs
index 6cb2af7d2ba76..1a34a4de84003 100644
--- a/third_party/move/move-prover/src/cli.rs
+++ b/third_party/move/move-prover/src/cli.rs
@@ -20,7 +20,10 @@ use move_model::{
     model::VerificationScope,
     options::ModelBuilderOptions,
 };
-use move_prover_boogie_backend::options::{BoogieOptions, CustomNativeOptions, VectorTheory};
+use move_prover_boogie_backend::{
+    options,
+    options::{BoogieOptions, CustomNativeOptions, VectorTheory},
+};
 use move_prover_bytecode_pipeline::options::{AutoTraceLevel, ProverOptions};
 use once_cell::sync::Lazy;
 use serde::{Deserialize, Serialize};
@@ -808,11 +811,7 @@ impl Options {
                     "../../../../aptos-move/framework/src/aptos-natives.bpl"
                 )
                 .to_vec(),
-                module_instance_names: vec![(
-                    "0x1::object".to_string(),
-                    "object_instances".to_string(),
-                    true,
-                )],
+                module_instance_names: options::custom_native_options(),
             });
             options
                 .move_named_address_values