Skip to content

Commit

Permalink
Format move code using aptos movefmt
Browse files Browse the repository at this point in the history
  • Loading branch information
axiongsupra committed Oct 26, 2024
1 parent d2c4977 commit 40c2002
Show file tree
Hide file tree
Showing 101 changed files with 13,799 additions and 7,921 deletions.
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

0 comments on commit 40c2002

Please sign in to comment.