Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Format move code using aptos movefmt #115

Open
wants to merge 1 commit into
base: dev
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
560 changes: 358 additions & 202 deletions aptos-move/framework/supra-framework/sources/account.move

Large diffs are not rendered by default.

440 changes: 281 additions & 159 deletions aptos-move/framework/supra-framework/sources/account.spec.move

Large diffs are not rendered by default.

Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ module supra_framework::aggregator {
struct Aggregator has store {
handle: address,
key: address,
limit: u128,
limit: u128
}

/// Returns `limit` exceeding which aggregator overflows.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -28,20 +28,27 @@ spec supra_framework::aggregator {

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
> spec_get_limit(aggregator);
/// [high-level-req-2]
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);
ensures aggregator
== spec_aggregator_set_val(
old(aggregator),
spec_aggregator_get_val(old(aggregator)) + value
);
}

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);
ensures aggregator
== spec_aggregator_set_val(
old(aggregator),
spec_aggregator_get_val(old(aggregator)) - value
);
}

spec read(aggregator: &Aggregator): u128 {
Expand All @@ -66,9 +73,14 @@ spec supra_framework::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;
}
Original file line number Diff line number Diff line change
Expand Up @@ -20,20 +20,22 @@ module supra_framework::aggregator_factory {
/// system and who can create them. At the moment, only Supra Framework (0x1)
/// account can.
struct AggregatorFactory has key {
phantom_table: Table<address, u128>,
phantom_table: Table<address, u128>
}

/// Creates a new factory for aggregators. Can only be called during genesis.
public(friend) fun initialize_aggregator_factory(supra_framework: &signer) {
public(friend) fun initialize_aggregator_factory(
supra_framework: &signer
) {
system_addresses::assert_supra_framework(supra_framework);
let aggregator_factory = AggregatorFactory {
phantom_table: table::new()
};
let aggregator_factory = AggregatorFactory { phantom_table: table::new() };
move_to(supra_framework, aggregator_factory);
}

/// Creates a new aggregator instance which overflows on exceeding a `limit`.
public(friend) fun create_aggregator_internal(limit: u128): Aggregator acquires AggregatorFactory {
public(friend) fun create_aggregator_internal(
limit: u128
): Aggregator acquires AggregatorFactory {
assert!(
exists<AggregatorFactory>(@supra_framework),
error::not_found(EAGGREGATOR_FACTORY_NOT_FOUND)
Expand All @@ -52,10 +54,14 @@ module supra_framework::aggregator_factory {
}

/// Returns a new aggregator.
native fun new_aggregator(aggregator_factory: &mut AggregatorFactory, limit: u128): Aggregator;
native fun new_aggregator(
aggregator_factory: &mut AggregatorFactory, limit: u128
): Aggregator;

#[test_only]
public fun initialize_aggregator_factory_for_test(supra_framework: &signer) {
public fun initialize_aggregator_factory_for_test(
supra_framework: &signer
) {
initialize_aggregator_factory(supra_framework);
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,7 @@ spec supra_framework::aggregator_factory {
ensures aggregator::spec_get_limit(result) == limit;
ensures aggregator::spec_aggregator_get_val(result) == 0;
}

spec schema CreateAggregatorInternalAbortsIf {
aborts_if !exists<AggregatorFactory>(@supra_framework);
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -19,15 +19,12 @@ module supra_framework::optional_aggregator {
/// Wrapper around integer with a custom overflow limit. Supports add, subtract and read just like `Aggregator`.
struct Integer has store {
value: u128,
limit: u128,
limit: u128
}

/// Creates a new integer which overflows on exceeding a `limit`.
fun new_integer(limit: u128): Integer {
Integer {
value: 0,
limit,
}
Integer { value: 0, limit }
}

/// Adds `value` to integer. Aborts on overflowing the limit.
Expand Down Expand Up @@ -65,20 +62,22 @@ module supra_framework::optional_aggregator {
// Parallelizable.
aggregator: Option<Aggregator>,
// Non-parallelizable.
integer: Option<Integer>,
integer: Option<Integer>
}

/// Creates a new optional aggregator.
public(friend) fun new(limit: u128, parallelizable: bool): OptionalAggregator {
if (parallelizable) {
OptionalAggregator {
aggregator: option::some(aggregator_factory::create_aggregator_internal(limit)),
integer: option::none(),
aggregator: option::some(
aggregator_factory::create_aggregator_internal(limit)
),
integer: option::none()
}
} else {
OptionalAggregator {
aggregator: option::none(),
integer: option::some(new_integer(limit)),
integer: option::some(new_integer(limit))
}
}
}
Expand Down Expand Up @@ -136,7 +135,9 @@ module supra_framework::optional_aggregator {
}

/// Destroys parallelizable optional aggregator and returns its limit.
fun destroy_optional_aggregator(optional_aggregator: OptionalAggregator): u128 {
fun destroy_optional_aggregator(
optional_aggregator: OptionalAggregator
): u128 {
let OptionalAggregator { aggregator, integer } = optional_aggregator;
let limit = aggregator::limit(option::borrow(&aggregator));
aggregator::destroy(option::destroy_some(aggregator));
Expand All @@ -154,7 +155,9 @@ module supra_framework::optional_aggregator {
}

/// Adds `value` to optional aggregator, aborting on exceeding the `limit`.
public fun add(optional_aggregator: &mut OptionalAggregator, value: u128) {
public fun add(
optional_aggregator: &mut OptionalAggregator, value: u128
) {
if (option::is_some(&optional_aggregator.aggregator)) {
let aggregator = option::borrow_mut(&mut optional_aggregator.aggregator);
aggregator::add(aggregator, value);
Expand All @@ -165,7 +168,9 @@ module supra_framework::optional_aggregator {
}

/// Subtracts `value` from optional aggregator, aborting on going below zero.
public fun sub(optional_aggregator: &mut OptionalAggregator, value: u128) {
public fun sub(
optional_aggregator: &mut OptionalAggregator, value: u128
) {
if (option::is_some(&optional_aggregator.aggregator)) {
let aggregator = option::borrow_mut(&mut optional_aggregator.aggregator);
aggregator::sub(aggregator, value);
Expand Down
Loading