use shell to fix aptos move test

deps/aptos-framework/multisig_account.spec.move

@@ -0,0 +1,6 @@
+spec aptos_framework::multisig_account {
+    spec module {
+        // TODO: verification disabled until this module is specified.
+        pragma verify = false;
+    }
+}

deps/aptos-framework/sources/aggregator/README.md

@@ -0,0 +1,47 @@
+# Design Rationale
+
+## Aggregators
+
+Aggregator is a parallelizable integer that supports addition and subtraction.
+Unlike integer, aggregator has a user-defined `limit` which specifies when
+the value of aggregator overflows. Similarly to unsigned integers, the value
+of an aggregator underflows when going below zero.
+
+Both additions and subtractions are executed speculatively, and thus can be
+easily parallelized. On underflow or overflow, these operations are guaranteed
+to abort. Using these operations is encouraged.
+
+Reading an aggregator's value "materializes" the speculative value, and it
+can involve reading from the storage or checking for underflow or overflow.
+In general, using this operation is discouraged, or at least it should be used
+as rarely as possible.
+
+## Aggregator factory
+
+Unfortunately, aggregators cannot be part of a resource. At the moment, Move
+does not allow fine-grained access to resource fields, which ruins performance
+benefits aggregators can provide. In addition, getting the value of the field of
+a resource from storage is not possible without hardcoding the struct layout.
+For example, given a struct
+
+```move
+struct Foo<A> has key {
+    a: A,
+    b: u128,
+}
+```
+
+there is no clean way of getting the value of `Foo::a` without knowing that the
+offset is 0.
+
+To mitigate the problem, we store aggregators as table items. Recall that every
+item stored in the table is uniquely identified by `(handle, key)` pair: `handle` 
+identifies a table instance, and `key` identifies an item within the table. Now,
+if aggregator is a table item, it can be easily queried from storage and has a
+fine-grained access.
+
+To create an aggregator, one can use an `AggregatorFactory`. It is a resource
+which contains a single `phantom_table` field. When the factory is initialized,
+this field is used to generate a unique table `handle` which is passed to all
+new aggregators. When a new aggregator instance is created, it has a unique
+`key` which together with the `handle` is stored in `Aggregator` struct.

deps/aptos-framework/sources/aggregator/aggregator.move

@@ -1,75 +1,28 @@
-/// This module provides an API for aggregatable integers that allow addition,
-/// subtraction, and reading.
-///
-/// Design rationale (V1)
-/// =====================
-/// Aggregator can be seen as a parellizable integer that supports addition,
-/// subtraction and reading. The first version (V1) of aggregator has the
-/// the following specification.
-///
-/// add(value: u128)
-///   Speculatively adds a `value` to aggregator. This is a cheap operation
-///   which is parallelizable. If the result of addition overflows a `limit`
-///   (one of aggregator's fields), an error is produced and the execution
-///   aborts.
-///
-/// sub(value: u128)
-///   Speculatively subtracts a `value` from aggregator. This is a cheap
-///   operation which is parallelizable. If the result goes below zero, an
-///   error is produced and the execution aborts.
-///
-/// read(): u128
-///   Reads (materializes) the value of an aggregator. This is an expensive
-///   operation which usually involves reading from the storage.
-///
-/// destroy()
-///   Destroys and aggregator, also cleaning up storage if necessary.
-///
-/// Note that there is no constructor in `Aggregator` API. This is done on purpose.
-/// For every aggregator, we need to know where its value is stored on chain.
-/// Currently, Move does not allow fine grained access to struct fields. For
-/// example, given a struct
-///
-///   struct Foo<A> has key {
-///       a: A,
-///       b: u128,
-///   }
-///
-/// there is no way of getting a value of `Foo::a` without hardcoding the layout
-/// of `Foo` and the field offset. To mitigate this problem, one can use a table.
-/// Every item stored in the table is uniqely identified by (handle, key) pair:
-/// `handle` identifies a table instance, `key` identifies an item within the table.
-///
-/// So how is this related to aggregator? Well, aggregator can reuse the table's
-/// approach for fine-grained storage. However, since native functions only see a
-/// reference to aggregator, we must ensure that both `handle` and `key` are
-/// included as fields. Therefore, the struct looks like
-///
-///  struct Aggregator {
-///      handle: u128,
-///      key: u128,
-///      ..
-///  }
-///
-/// Remaining question is how to generate this (handle, key) pair. For that, we have
-/// a dedicated struct called `AggregatorFactory` which is responsible for constructing
-/// aggregators. See `aggregator_factory.move` for more details.
-///
-/// Advice to users (V1)
-/// ====================
-/// Users are encouraged to use "cheap" operations (e.g. additions) to exploit the
-/// parallelism in execution.
+/// This module provides an interface for aggregators. Aggregators are similar to
+/// unsigned integers and support addition and subtraction (aborting on underflow
+/// or on overflowing a custom upper limit). The difference from integers is that
+/// aggregators allow to perform both additions and subtractions in parallel across
+/// multiple transactions, enabling parallel execution. For example, if the first
+/// transaction is doing `add(X, 1)` for aggregator resource `X`, and the second
+/// is doing `sub(X,3)`, they can be executed in parallel avoiding a read-modify-write
+/// dependency.
+/// However, reading the aggregator value (i.e. calling `read(X)`) is an expensive
+/// operation and should be avoided as much as possible because it reduces the
+/// parallelism. Moreover, **aggregators can only be created by Aptos Framework (0x1)
+/// at the moment.**
 module aptos_framework::aggregator {
 
-    /// When the value of aggregator (actual or accumulated) overflows (raised by native code).
+    /// The value of aggregator overflows. Raised by native code.
     const EAGGREGATOR_OVERFLOW: u64 = 1;
 
-    /// When the value of aggregator (actual or accumulated) underflows, i.e goes below zero (raised by native code).
+    /// The value of aggregator underflows (goes below zero). Raised by native code.
     const EAGGREGATOR_UNDERFLOW: u64 = 2;
 
-    /// When aggregator feature is not supported (raised by native code).
+    /// Aggregator feature is not supported. Raised by native code.
     const ENOT_SUPPORTED: u64 = 3;
 
+    /// Represents an integer which supports parallel additions and subtractions
+    /// across multiple transactions. See the module description for more details.
     struct Aggregator has store {
         handle: address,
         key: address,

deps/aptos-framework/sources/aggregator/aggregator.spec.move

@@ -1,25 +1,47 @@
 spec aptos_framework::aggregator {
-    spec module {
-        pragma verify = false;
+    spec Aggregator {
+        pragma intrinsic;
     }
 
-    spec add {
-        // TODO: temporary mockup.
+    spec add(aggregator: &mut Aggregator, value: u128) {
         pragma opaque;
+        aborts_if spec_aggregator_get_val(aggregator) + value > spec_get_limit(aggregator);
+        aborts_if spec_aggregator_get_val(aggregator) + value > MAX_U128;
+        ensures spec_get_limit(aggregator) == spec_get_limit(old(aggregator));
+        ensures aggregator == spec_aggregator_set_val(old(aggregator),
+            spec_aggregator_get_val(old(aggregator)) + value);
     }
 
-    spec sub {
-        // TODO: temporary mockup.
+    spec sub(aggregator: &mut Aggregator, value: u128) {
         pragma opaque;
+        aborts_if spec_aggregator_get_val(aggregator) < value;
+        ensures spec_get_limit(aggregator) == spec_get_limit(old(aggregator));
+        ensures aggregator == spec_aggregator_set_val(old(aggregator),
+            spec_aggregator_get_val(old(aggregator)) - value);
     }
 
-    spec read {
-        // TODO: temporary mockup.
+    spec read(aggregator: &Aggregator): u128 {
         pragma opaque;
+        aborts_if false;
+        ensures result == spec_read(aggregator);
+        ensures result <= spec_get_limit(aggregator);
     }
 
-    spec destroy {
-        // TODO: temporary mockup.
+    spec destroy(aggregator: Aggregator) {
         pragma opaque;
+        aborts_if false;
     }
+
+    spec limit {
+        pragma opaque;
+        aborts_if false;
+        ensures [abstract] result == spec_get_limit(aggregator);
+    }
+
+    spec native fun spec_read(aggregator: Aggregator): u128;
+    spec native fun spec_get_limit(a: Aggregator): u128;
+    spec native fun spec_get_handle(a: Aggregator): u128;
+    spec native fun spec_get_key(a: Aggregator): u128;
+    spec native fun spec_aggregator_set_val(a: Aggregator, v: u128): Aggregator;
+    spec native fun spec_aggregator_get_val(a: Aggregator): u128;
 }

deps/aptos-framework/sources/aggregator/aggregator_factory.move

@@ -1,51 +1,29 @@
-/// This module provides foundations to create aggregators in the system.
-///
-/// Design rationale (V1)
-/// =====================
-/// First, we encourage the reader to see rationale of `Aggregator` in
-/// `aggregator.move`.
-///
-/// Recall that the value of any aggregator can be identified in storage by
-/// (handle, key) pair. How this pair can be generated? Short answer: with
-/// `AggregatorFactory`!
-///
-/// `AggregatorFactory` is a struct that can be stored as a resource on some
-/// account and which contains a `phantom_table` field. When the factory is
-/// initialized, we initialize this table. Importantly, table initialization
-/// only generates a uniue table `handle` - something we can reuse.
-///
-/// When the user wants to create a new aggregator, he/she calls a constructor
-/// provided by the factory (`create_aggregator(..)`). This constructor generates
-/// a unique key, which with the handle is used to initialize `Aggregator` struct.
-///
-/// Use cases
-/// =========
-/// We limit the usage of `AggregatorFactory` by only storing it on the core
-/// account.
-///
-/// When something whants to use an aggregator, the factory is queried and an
-/// aggregator instance is created. Once aggregator is no longer in use, it
-/// should be destroyed by the user.
+/// This module provides foundations to create aggregators. Currently only
+/// Aptos Framework (0x1) can create them, so this module helps to wrap
+/// the constructor of `Aggregator` struct so that only a system account
+/// can initialize one. In the future, this might change and aggregators
+/// can be enabled for the public.
 module aptos_framework::aggregator_factory {
     use std::error;
 
     use aptos_framework::system_addresses;
-    use aptos_std::aggregator::Aggregator;
+    use aptos_framework::aggregator::Aggregator;
     use aptos_std::table::{Self, Table};
 
     friend aptos_framework::genesis;
     friend aptos_framework::optional_aggregator;
 
-    /// When aggregator factory is not published yet.
+    /// Aggregator factory is not published yet.
     const EAGGREGATOR_FACTORY_NOT_FOUND: u64 = 1;
 
-    /// Struct that creates aggregators.
+    /// Creates new aggregators. Used to control the numbers of aggregators in the
+    /// system and who can create them. At the moment, only Aptos Framework (0x1)
+    /// account can.
     struct AggregatorFactory has key {
         phantom_table: Table<address, u128>,
     }
 
-    /// Can only be called during genesis.
-    /// Creates a new factory for aggregators.
+    /// Creates a new factory for aggregators. Can only be called during genesis.
     public(friend) fun initialize_aggregator_factory(aptos_framework: &signer) {
         system_addresses::assert_aptos_framework(aptos_framework);
         let aggregator_factory = AggregatorFactory {
@@ -73,6 +51,7 @@ module aptos_framework::aggregator_factory {
         create_aggregator_internal(limit)
     }
 
+    /// Returns a new aggregator.
     native fun new_aggregator(aggregator_factory: &mut AggregatorFactory, limit: u128): Aggregator;
 
     #[test_only]

deps/aptos-framework/sources/aggregator/aggregator_factory.spec.move

@@ -1,10 +1,44 @@
 spec aptos_framework::aggregator_factory {
+    use aptos_framework::aggregator;
     spec module {
-        pragma verify = false;
+        pragma aborts_if_is_strict;
     }
 
-    spec new_aggregator {
-        // TODO: temporary mockup.
+    spec new_aggregator(aggregator_factory: &mut AggregatorFactory, limit: u128): Aggregator {
         pragma opaque;
+        aborts_if false;
+        ensures result == spec_new_aggregator(limit);
+        ensures aggregator::spec_get_limit(result) == limit;
     }
+
+    /// Make sure the caller is @aptos_framework.
+    /// AggregatorFactory is not under the caller before creating the resource.
+    spec initialize_aggregator_factory(aptos_framework: &signer) {
+        use std::signer;
+        let addr = signer::address_of(aptos_framework);
+        aborts_if addr != @aptos_framework;
+        aborts_if exists<AggregatorFactory>(addr);
+        ensures exists<AggregatorFactory>(addr);
+    }
+
+    spec create_aggregator_internal(limit: u128): Aggregator {
+        include CreateAggregatorInternalAbortsIf;
+        ensures aggregator::spec_get_limit(result) == limit;
+        ensures aggregator::spec_aggregator_get_val(result) == 0;
+    }
+    spec schema CreateAggregatorInternalAbortsIf {
+        aborts_if !exists<AggregatorFactory>(@aptos_framework);
+    }
+
+    /// Make sure the caller is @aptos_framework.
+    /// AggregatorFactory existed under the @aptos_framework when Creating a new aggregator.
+    spec create_aggregator(account: &signer, limit: u128): Aggregator {
+        use std::signer;
+        let addr = signer::address_of(account);
+        aborts_if addr != @aptos_framework;
+        aborts_if !exists<AggregatorFactory>(@aptos_framework);
+    }
+
+    spec native fun spec_new_aggregator(limit: u128): Aggregator;
+
 }