diff --git a/aptos-move/framework/aptos-framework/doc/aggregator.md b/aptos-move/framework/aptos-framework/doc/aggregator.md index 4d2bfca013199..be20daf6b83c1 100644 --- a/aptos-move/framework/aptos-framework/doc/aggregator.md +++ b/aptos-move/framework/aptos-framework/doc/aggregator.md @@ -330,10 +330,9 @@ Destroys an aggregator and removes it from its AggregatorFactory. -
pragma opaque;
+
pragma intrinsic;
 // This enforces high-level requirement 1:
-aborts_if false;
-ensures [abstract] result == spec_get_limit(aggregator);
+aborts_if [abstract] false;
 
diff --git a/aptos-move/framework/aptos-framework/sources/aggregator/aggregator.spec.move b/aptos-move/framework/aptos-framework/sources/aggregator/aggregator.spec.move index 76f00feba3f7e..d29b6cb1bb8a6 100644 --- a/aptos-move/framework/aptos-framework/sources/aggregator/aggregator.spec.move +++ b/aptos-move/framework/aptos-framework/sources/aggregator/aggregator.spec.move @@ -59,10 +59,9 @@ spec aptos_framework::aggregator { } spec limit { - pragma opaque; + pragma intrinsic; /// [high-level-req-1.2] - aborts_if false; - ensures [abstract] result == spec_get_limit(aggregator); + aborts_if [abstract] false; } spec native fun spec_read(aggregator: Aggregator): u128; diff --git a/aptos-move/framework/src/aptos-natives.bpl b/aptos-move/framework/src/aptos-natives.bpl index 717b510391fdb..e2c34cf5f21a0 100644 --- a/aptos-move/framework/src/aptos-natives.bpl +++ b/aptos-move/framework/src/aptos-natives.bpl @@ -266,6 +266,13 @@ function {:inline} $IsEqual'$1_aggregator_Aggregator'(s1: $1_aggregator_Aggregat function {:inline} $1_aggregator_spec_get_limit(s: $1_aggregator_Aggregator): int { s->$limit } +function {:inline} $1_aggregator_limit(s: $1_aggregator_Aggregator): int { + s->$limit +} +procedure {:inline 1} $1_aggregator_limit(s: $1_aggregator_Aggregator) returns (res: int) { + res := s->$limit; + return; +} function {:inline} $1_aggregator_spec_get_handle(s: $1_aggregator_Aggregator): int { s->$handle } diff --git a/crates/aptos/CHANGELOG.md b/crates/aptos/CHANGELOG.md index b9cf75816b2ce..7ac2acca203f4 100644 --- a/crates/aptos/CHANGELOG.md +++ b/crates/aptos/CHANGELOG.md @@ -4,6 +4,7 @@ All notable changes to the Aptos CLI will be captured in this file. This project ## Unreleased - Fix typos in `aptos move compile` help text. +- Update the default version of `movefmt` to be installed from 1.0.5 to 1.0.6 ## [4.3.0] - 2024/10/30 - Allow for setting large-packages module for chunking publish mode with `--large-packages-module-address` diff --git a/crates/aptos/src/update/movefmt.rs b/crates/aptos/src/update/movefmt.rs index 2dd229a430271..d6889379defe0 100644 --- a/crates/aptos/src/update/movefmt.rs +++ b/crates/aptos/src/update/movefmt.rs @@ -13,7 +13,7 @@ use self_update::update::ReleaseUpdate; use std::path::PathBuf; const FORMATTER_BINARY_NAME: &str = "movefmt"; -const TARGET_FORMATTER_VERSION: &str = "1.0.5"; +const TARGET_FORMATTER_VERSION: &str = "1.0.6"; const FORMATTER_EXE_ENV: &str = "FORMATTER_EXE"; #[cfg(target_os = "windows")]