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