fix

aptos-labs · Nov 4, 2024 · d20a091 · d20a091
1 parent 9baf39b
commit d20a091
Show file tree

Hide file tree

Showing 5 changed files with 13 additions and 7 deletions.
diff --git 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 <code>AggregatorFactory</code>.
 
 
 
-<pre><code><b>pragma</b> opaque;
+<pre><code><b>pragma</b> intrinsic;
 // This enforces <a id="high-level-req-1.2" href="#high-level-req">high-level requirement 1</a>:
-<b>aborts_if</b> <b>false</b>;
-<b>ensures</b> [abstract] result == <a href="aggregator.md#0x1_aggregator_spec_get_limit">spec_get_limit</a>(<a href="aggregator.md#0x1_aggregator">aggregator</a>);
+<b>aborts_if</b> [abstract] <b>false</b>;
 </code></pre>
 
 

diff --git 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
@@ -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
@@ -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
@@ -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")]