[Spec] add boogie native for aggregator_v2 #14881

rahxephon89 · 2024-10-05T08:10:37Z

Description

This PR adds native implementation of aggregator_v2 in the Move prover.

How Has This Been Tested?

Several tests for verification are added to aggregator_v2.move.
A spec is added to collection.move in aptos-token-objects.

Key Areas to Review

Aggregator_v2 can only be instantiated with u64 and u128 so for all other concrete types, all APIs will directly abort.
For generic type #..., only the abort_if conditions are specified, need to make sure it is correct.

Type of Change

Which Components or Systems Does This Change Impact?

Checklist

I have read and followed the CONTRIBUTING doc
I have performed a self-review of my own code
I have commented my code, particularly in hard-to-understand areas
I identified and added all stakeholders and component owners affected by this change as reviewers
I tested both happy and unhappy path of the functionality
I have made corresponding changes to the documentation

trunk-io · 2024-10-05T08:10:41Z

⏱️ 2h 4m total CI duration on this PR

Slowest 15 Jobs	Cumulative Duration	Recent Runs
rust-move-unit-coverage	16m	🟩
rust-move-unit-coverage	15m	🟩
rust-move-unit-coverage	12m	🟩
rust-move-unit-coverage	11m	🟩
rust-move-tests	9m	🟩
rust-move-tests	9m	🟩
rust-move-tests	9m	🟩
rust-move-tests	9m	🟩
rust-cargo-deny	9m	🟩 🟩 🟩 🟩 🟩
rust-move-tests	7m	⬜
rust-move-unit-coverage	7m	⬜
check-dynamic-deps	5m	🟩 🟩 🟩 🟩 🟩
general-lints	2m	🟩 🟩 🟩 🟩 🟩
semgrep/ci	2m	🟩 🟩 🟩 🟩 🟩
file_change_determinator	55s	🟩 🟩 🟩 🟩 🟩

_{settings ⋅ feedback ⋅ docs ⋅ learn more about trunk.io}

codecov · 2024-10-05T08:30:08Z

Codecov Report

Attention: Patch coverage is 93.75000% with 1 line in your changes missing coverage. Please review.

Project coverage is 59.7%. Comparing base (d9c7970) to head (bf81777).
Report is 6 commits behind head on main.

Files with missing lines	Patch %	Lines
third_party/move/move-prover/src/cli.rs	0.0%	1 Missing ⚠️

❗ There is a different number of reports uploaded between BASE (d9c7970) and HEAD (bf81777). Click for more details.

HEAD has 1 upload less than BASE

Flag BASE (d9c7970) HEAD (bf81777)

2 1

Additional details and impacted files

@@             Coverage Diff             @@
##             main   #14881       +/-   ##
===========================================
- Coverage    72.8%    59.7%    -13.1%     
===========================================
  Files        2400      853     -1547     
  Lines      485208   208289   -276919     
===========================================
- Hits       353490   124541   -228949     
+ Misses     131718    83748    -47970

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

wrwg · 2024-10-07T17:43:01Z

aptos-move/framework/aptos-token-objects/sources/collection.move

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


Can we make line breaks better here? Shouldn't be over 100 characters

wrwg · 2024-10-07T17:45:21Z

aptos-move/framework/src/aptos-natives.bpl

+      && $IsEqual'{{S}}'(s1->$max_value, s2->$max_value)
+}
+
+{% if S == "u64" -%}


Ther seems to be a bit of duplication in this if-else? Could we perhaps loop over the various types instead>

I refactored the template here to reduce duplication.

georgemitenkov · 2024-10-08T08:05:22Z

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

@@ -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 exceed 1024 bytes, ECONCAT_STRING_LENGTH_TOO_LARGE is raised.


another typo: exceed --> exceeds

georgemitenkov · 2024-10-08T08:07:36Z

third_party/move/move-prover/src/cli.rs

-                    "object_instances".to_string(),
-                    true,
-                )],
+                module_instance_names: vec![


Seems like module_instances can be factored out? It is duplicated across multiple files causing more changes

georgemitenkov · 2024-10-08T08:10:38Z

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

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


nit: this extra line is not needed?

georgemitenkov · 2024-10-08T08:12:06Z

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

+    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 {


nit: for consistency can also use get instead of read in these names? So we get aggregator value, get snapshot integer value, etc.

I used read here because there are corresponding APIs read_snapshot and read_derived_string.

georgemitenkov · 2024-10-08T08:15:48Z

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

        pragma opaque;
+        include AbortsIfIntElement<IntElement>;
+        ensures [abstract] result.value == spec_get_value(aggregator);


Question, why here we need to call a spec native for aggregator, and not aggregator.value? Is it because the spec is intrinsic? Cause technically for sub for example you can say: aggregator.value = old(aggregator).value - amount if no overflow, etc. or does the spec not support these kind of things because of generic types?

yeah, when the spec of a struct is intrinsic, we cannot directly get access to its field. The reason of using intrinsics for spec is because generic types do not support + and -.

georgemitenkov · 2024-10-08T08:22:13Z

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

@@ -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]


I was not aware we had these attributes, so this can be used for spec testing? Nice to know!

yeah, with this attribute, the function is only visible for verification.

georgemitenkov · 2024-10-08T08:23:17Z

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

+        let x = try_add(&mut agg, 5);
+        spec {
+            assert x;
+            assert is_at_least(agg, 5);


Curious why at least and not exact equality?

I use this assertion to test the native implementation for the API is_at_least.

rahxephon89 · 2024-10-08T17:13:11Z

[Spec] add boogie native for aggregator_v2 #14881 👈
main

This stack of pull requests is managed by Graphite. Learn more about stacking.

Join @rahxephon89 and the rest of your teammates on Graphite

add native for aggregator_v2

6536135

rahxephon89 force-pushed the teng/aggregator-spec-v2 branch from 69a1fa9 to 6536135 Compare October 5, 2024 08:18

rahxephon89 marked this pull request as ready for review October 6, 2024 02:23

rahxephon89 requested review from junkil-park, davidiw, movekevin and wrwg as code owners October 6, 2024 02:23

rahxephon89 requested review from georgemitenkov and igor-aptos October 6, 2024 02:23

rahxephon89 changed the title ~~[WIP][Spec] add native for aggregator_v2~~ [Spec] add boogie native for aggregator_v2 Oct 6, 2024

wrwg reviewed Oct 7, 2024

View reviewed changes

georgemitenkov reviewed Oct 8, 2024

View reviewed changes

handle comments

bf81777

refactor aptos-natives.bpl

da06c6d

rahxephon89 force-pushed the teng/aggregator-spec-v2 branch from 9d4bead to da06c6d Compare October 8, 2024 20:05

rahxephon89 requested review from georgemitenkov and wrwg October 8, 2024 20:06

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Spec] add boogie native for aggregator_v2 #14881

[Spec] add boogie native for aggregator_v2 #14881

rahxephon89 commented Oct 5, 2024 •

edited

Loading

trunk-io bot commented Oct 5, 2024 •

edited

Loading

codecov bot commented Oct 5, 2024 •

edited

Loading

wrwg Oct 7, 2024

rahxephon89 Oct 8, 2024

wrwg Oct 7, 2024

rahxephon89 Oct 8, 2024

georgemitenkov Oct 8, 2024

georgemitenkov Oct 8, 2024

rahxephon89 Oct 8, 2024

georgemitenkov Oct 8, 2024

rahxephon89 Oct 8, 2024

georgemitenkov Oct 8, 2024

rahxephon89 Oct 8, 2024

georgemitenkov Oct 8, 2024

rahxephon89 Oct 8, 2024

georgemitenkov Oct 8, 2024

rahxephon89 Oct 8, 2024

georgemitenkov Oct 8, 2024

rahxephon89 Oct 8, 2024

rahxephon89 commented Oct 8, 2024 •

edited

Loading

[Spec] add boogie native for aggregator_v2 #14881

Are you sure you want to change the base?

[Spec] add boogie native for aggregator_v2 #14881

Conversation

rahxephon89 commented Oct 5, 2024 • edited Loading

Description

How Has This Been Tested?

Key Areas to Review

Type of Change

Which Components or Systems Does This Change Impact?

Checklist

trunk-io bot commented Oct 5, 2024 • edited Loading

codecov bot commented Oct 5, 2024 • edited Loading

Codecov Report

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

rahxephon89 commented Oct 8, 2024 • edited Loading

rahxephon89 commented Oct 5, 2024 •

edited

Loading

trunk-io bot commented Oct 5, 2024 •

edited

Loading

codecov bot commented Oct 5, 2024 •

edited

Loading

rahxephon89 commented Oct 8, 2024 •

edited

Loading