Skip to content

Commit

Permalink
[diem-framework] improve the specs for NetworkIdentity
Browse files Browse the repository at this point in the history 
Mostly to simplify the `forall/exists i in 0..len(vec): P(vec[i])`;
with the notion that iterates over all elements of a vector:
`forall/exists e in vec: P(e);`.

Closes: aptos-labs#8867
  • Loading branch information
@meng-xu-cs @bors-libra
meng-xu-cs authored and bors-libra committed Aug 12, 2021
1 parent 2147baf commit 834439f
Show file tree
Hide file tree
Showing 4 changed files with 65 additions and 65 deletions.
46 changes: 23 additions & 23 deletions language/diem-framework/modules/NetworkIdentity.move
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,12 +53,12 @@ module DiemFramework::NetworkIdentity {
public fun get(account_addr: address): vector<vector<u8>> acquires NetworkIdentity {
assert(
exists<NetworkIdentity>(account_addr),
Errors::invalid_state(ENETWORK_ID_DOESNT_EXIST)
Errors::not_published(ENETWORK_ID_DOESNT_EXIST)
);
*&borrow_global<NetworkIdentity>(account_addr).identities
}
spec get {
aborts_if !exists<NetworkIdentity>(account_addr);
aborts_if !exists<NetworkIdentity>(account_addr) with Errors::NOT_PUBLISHED;
ensures result == global<NetworkIdentity>(account_addr).identities;
}

Expand Down Expand Up @@ -93,16 +93,17 @@ module DiemFramework::NetworkIdentity {
} else {
vec()
};
let has_change = (exists i in 0..len(to_add): !contains(prior_identities, to_add[i]));
let has_change = (exists e in to_add: !contains(prior_identities, e));

let post handle = global<NetworkIdentity>(account_addr).identity_change_events;
let post msg = NetworkIdentityChangeNotification {
identities: global<NetworkIdentity>(account_addr).identities,
time_rotated_seconds: DiemTimestamp::spec_now_seconds(),
};

aborts_if len(to_add) == 0;
aborts_if len(prior_identities) + len(to_add) > MAX_ADDR_IDENTITIES;
aborts_if len(to_add) == 0 with Errors::INVALID_ARGUMENT;
aborts_if len(prior_identities) + len(to_add) > MAX_U64;
aborts_if len(prior_identities) + len(to_add) > MAX_ADDR_IDENTITIES with Errors::LIMIT_EXCEEDED;
include has_change ==> DiemTimestamp::AbortsIfNotOperating;
include AddMembersInternalEnsures<vector<u8>> {
old_members: prior_identities,
Expand All @@ -124,7 +125,7 @@ module DiemFramework::NetworkIdentity {
let account_addr = Signer::address_of(account);
assert(
exists<NetworkIdentity>(account_addr),
Errors::invalid_state(ENETWORK_ID_DOESNT_EXIST)
Errors::not_published(ENETWORK_ID_DOESNT_EXIST)
);

let identity = borrow_global_mut<NetworkIdentity>(account_addr);
Expand All @@ -141,17 +142,17 @@ module DiemFramework::NetworkIdentity {
spec remove_identities {
let account_addr = Signer::spec_address_of(account);
let prior_identities = global<NetworkIdentity>(account_addr).identities;
let has_change = (exists i in 0..len(to_remove): contains(prior_identities, to_remove[i]));
let has_change = (exists e in to_remove: contains(prior_identities, e));

let post handle = global<NetworkIdentity>(account_addr).identity_change_events;
let post msg = NetworkIdentityChangeNotification {
identities: global<NetworkIdentity>(account_addr).identities,
time_rotated_seconds: DiemTimestamp::spec_now_seconds(),
};

aborts_if len(to_remove) == 0;
aborts_if len(to_remove) > MAX_ADDR_IDENTITIES;
aborts_if !exists<NetworkIdentity>(account_addr);
aborts_if len(to_remove) == 0 with Errors::INVALID_ARGUMENT;
aborts_if len(to_remove) > MAX_ADDR_IDENTITIES with Errors::LIMIT_EXCEEDED;
aborts_if !exists<NetworkIdentity>(account_addr) with Errors::NOT_PUBLISHED;
include has_change ==> DiemTimestamp::AbortsIfNotOperating;
include RemoveMembersInternalEnsures<vector<u8>> {
old_members: prior_identities,
Expand Down Expand Up @@ -219,18 +220,18 @@ module DiemFramework::NetworkIdentity {
// ensures that the `members` argument is and remains a set
include UniqueMembers<T>;
// returns whether a new element is added to the set
ensures result == (exists i in 0..len(to_add): !contains(old(members), to_add[i]));
ensures result == (exists e in to_add: !contains(old(members), e));
}
spec schema AddMembersInternalEnsures<T: copy> {
old_members: vector<T>;
new_members: vector<T>;
to_add: vector<T>;
// everything in the `to_add` vector must be in the updated set
ensures forall i in 0..len(to_add): contains(new_members, to_add[i]);
ensures forall e in to_add: contains(new_members, e);
// everything in the old set must remain in the updated set
ensures forall i in 0..len(old_members): contains(new_members, old_members[i]);
ensures forall e in old_members: contains(new_members, e);
// everything in the updated set must come from either the old set or the `to_add` vector
ensures forall i in 0..len(new_members): (contains(old_members, new_members[i]) || contains(to_add, new_members[i]));
ensures forall e in new_members: (contains(old_members, e) || contains(to_add, e));
}

/// Remove all elements that appear in `to_remove` from `members`.
Expand All @@ -253,8 +254,7 @@ module DiemFramework::NetworkIdentity {
// the set can never grow in size
invariant len(members) <= len(old(members));
// the current set maintains the uniqueness of the elements
invariant forall j in 0..len(members), k in 0..len(members):
members[j] == members[k] ==> j == k;
invariant forall j in 0..len(members), k in 0..len(members): members[j] == members[k] ==> j == k;
// all elements in the the current set come from the original set
invariant forall j in 0..len(members): contains(old(members), members[j]);
// the current set never contains anything from the `to_remove` vector
Expand All @@ -279,9 +279,9 @@ module DiemFramework::NetworkIdentity {
}
spec remove_members_internal {
// TODO: due to the complexity of the loop invariants and the extensive use of quantifiers in the spec, this
// function needs a bit more time to verify. We may need to investigate ways to reduce the verification time
// for this function in the future.
pragma timeout = 120;
// function takes significantly longer to verify (expect 200+ seconds). We will need to investigate ways to
// reduce the verification time for this function in the future. Until then, disable the verification for now.
pragma verify = false;

pragma opaque;
// TODO(mengxu): this is to force the prover to honor the "opaque" pragma in the ignore opaque setting
Expand All @@ -295,18 +295,18 @@ module DiemFramework::NetworkIdentity {
// ensures that the `members` argument is and remains a set
include UniqueMembers<T>;
// returns whether an element is removed from the set
ensures result == (exists i in 0..len(to_remove): contains(old(members), to_remove[i]));
ensures result == (exists e in to_remove: contains(old(members), e));
}
spec schema RemoveMembersInternalEnsures<T: drop> {
old_members: vector<T>;
new_members: vector<T>;
to_remove: vector<T>;
// everything in the `to_remove` vector must not be in the updated set
ensures forall i in 0..len(to_remove): !contains(new_members, to_remove[i]);
ensures forall e in to_remove: !contains(new_members, e);
// all members in the updated set must be in the original set
ensures forall i in 0..len(new_members): contains(old_members, new_members[i]);
ensures forall e in new_members: contains(old_members, e);
// an element from the original set that is not in the `to_remove` must be in the updated set
ensures forall i in 0..len(old_members): (contains(to_remove, old_members[i]) || contains(new_members, old_members[i]));
ensures forall e in old_members: (contains(to_remove, e) || contains(new_members, e));
}

spec schema UniqueMembers<T> {
Expand Down
42 changes: 21 additions & 21 deletions language/diem-framework/modules/doc/NetworkIdentity.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -221,7 +221,7 @@ Return the underlying <code><a href="NetworkIdentity.md#0x1_NetworkIdentity">Net
<pre><code><b>public</b> <b>fun</b> <a href="NetworkIdentity.md#0x1_NetworkIdentity_get">get</a>(account_addr: address): vector&lt;vector&lt;u8&gt;&gt; <b>acquires</b> <a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a> {
<b>assert</b>(
<b>exists</b>&lt;<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>&gt;(account_addr),
<a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_state">Errors::invalid_state</a>(<a href="NetworkIdentity.md#0x1_NetworkIdentity_ENETWORK_ID_DOESNT_EXIST">ENETWORK_ID_DOESNT_EXIST</a>)
<a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="NetworkIdentity.md#0x1_NetworkIdentity_ENETWORK_ID_DOESNT_EXIST">ENETWORK_ID_DOESNT_EXIST</a>)
);
*&borrow_global&lt;<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>&gt;(account_addr).identities
}
Expand All @@ -236,7 +236,7 @@ Return the underlying <code><a href="NetworkIdentity.md#0x1_NetworkIdentity">Net



<pre><code><b>aborts_if</b> !<b>exists</b>&lt;<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>&gt;(account_addr);
<pre><code><b>aborts_if</b> !<b>exists</b>&lt;<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>&gt;(account_addr) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>;
<b>ensures</b> result == <b>global</b>&lt;<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>&gt;(account_addr).identities;
</code></pre>

Expand Down Expand Up @@ -300,14 +300,15 @@ Update and create if not exist <code><a href="NetworkIdentity.md#0x1_NetworkIden
} <b>else</b> {
vec()
};
<b>let</b> has_change = (<b>exists</b> i in 0..len(to_add): !contains(prior_identities, to_add[i]));
<b>let</b> has_change = (<b>exists</b> e in to_add: !contains(prior_identities, e));
<b>let</b> post handle = <b>global</b>&lt;<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>&gt;(account_addr).identity_change_events;
<b>let</b> post msg = <a href="NetworkIdentity.md#0x1_NetworkIdentity_NetworkIdentityChangeNotification">NetworkIdentityChangeNotification</a> {
identities: <b>global</b>&lt;<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>&gt;(account_addr).identities,
time_rotated_seconds: <a href="DiemTimestamp.md#0x1_DiemTimestamp_spec_now_seconds">DiemTimestamp::spec_now_seconds</a>(),
};
<b>aborts_if</b> len(to_add) == 0;
<b>aborts_if</b> len(prior_identities) + len(to_add) &gt; <a href="NetworkIdentity.md#0x1_NetworkIdentity_MAX_ADDR_IDENTITIES">MAX_ADDR_IDENTITIES</a>;
<b>aborts_if</b> len(to_add) == 0 <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>;
<b>aborts_if</b> len(prior_identities) + len(to_add) &gt; MAX_U64;
<b>aborts_if</b> len(prior_identities) + len(to_add) &gt; <a href="NetworkIdentity.md#0x1_NetworkIdentity_MAX_ADDR_IDENTITIES">MAX_ADDR_IDENTITIES</a> <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_LIMIT_EXCEEDED">Errors::LIMIT_EXCEEDED</a>;
<b>include</b> has_change ==&gt; <a href="DiemTimestamp.md#0x1_DiemTimestamp_AbortsIfNotOperating">DiemTimestamp::AbortsIfNotOperating</a>;
<b>include</b> <a href="NetworkIdentity.md#0x1_NetworkIdentity_AddMembersInternalEnsures">AddMembersInternalEnsures</a>&lt;vector&lt;u8&gt;&gt; {
old_members: prior_identities,
Expand Down Expand Up @@ -348,7 +349,7 @@ Remove <code><a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a
<b>let</b> account_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(account);
<b>assert</b>(
<b>exists</b>&lt;<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>&gt;(account_addr),
<a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_state">Errors::invalid_state</a>(<a href="NetworkIdentity.md#0x1_NetworkIdentity_ENETWORK_ID_DOESNT_EXIST">ENETWORK_ID_DOESNT_EXIST</a>)
<a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="NetworkIdentity.md#0x1_NetworkIdentity_ENETWORK_ID_DOESNT_EXIST">ENETWORK_ID_DOESNT_EXIST</a>)
);

<b>let</b> identity = borrow_global_mut&lt;<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>&gt;(account_addr);
Expand All @@ -375,15 +376,15 @@ Remove <code><a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a

<pre><code><b>let</b> account_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account);
<b>let</b> prior_identities = <b>global</b>&lt;<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>&gt;(account_addr).identities;
<b>let</b> has_change = (<b>exists</b> i in 0..len(to_remove): contains(prior_identities, to_remove[i]));
<b>let</b> has_change = (<b>exists</b> e in to_remove: contains(prior_identities, e));
<b>let</b> post handle = <b>global</b>&lt;<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>&gt;(account_addr).identity_change_events;
<b>let</b> post msg = <a href="NetworkIdentity.md#0x1_NetworkIdentity_NetworkIdentityChangeNotification">NetworkIdentityChangeNotification</a> {
identities: <b>global</b>&lt;<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>&gt;(account_addr).identities,
time_rotated_seconds: <a href="DiemTimestamp.md#0x1_DiemTimestamp_spec_now_seconds">DiemTimestamp::spec_now_seconds</a>(),
};
<b>aborts_if</b> len(to_remove) == 0;
<b>aborts_if</b> len(to_remove) &gt; <a href="NetworkIdentity.md#0x1_NetworkIdentity_MAX_ADDR_IDENTITIES">MAX_ADDR_IDENTITIES</a>;
<b>aborts_if</b> !<b>exists</b>&lt;<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>&gt;(account_addr);
<b>aborts_if</b> len(to_remove) == 0 <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>;
<b>aborts_if</b> len(to_remove) &gt; <a href="NetworkIdentity.md#0x1_NetworkIdentity_MAX_ADDR_IDENTITIES">MAX_ADDR_IDENTITIES</a> <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_LIMIT_EXCEEDED">Errors::LIMIT_EXCEEDED</a>;
<b>aborts_if</b> !<b>exists</b>&lt;<a href="NetworkIdentity.md#0x1_NetworkIdentity">NetworkIdentity</a>&gt;(account_addr) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>;
<b>include</b> has_change ==&gt; <a href="DiemTimestamp.md#0x1_DiemTimestamp_AbortsIfNotOperating">DiemTimestamp::AbortsIfNotOperating</a>;
<b>include</b> <a href="NetworkIdentity.md#0x1_NetworkIdentity_RemoveMembersInternalEnsures">RemoveMembersInternalEnsures</a>&lt;vector&lt;u8&gt;&gt; {
old_members: prior_identities,
Expand Down Expand Up @@ -473,7 +474,7 @@ to be a set and hence can have duplicated elements.
new_members: members,
};
<b>include</b> <a href="NetworkIdentity.md#0x1_NetworkIdentity_UniqueMembers">UniqueMembers</a>&lt;T&gt;;
<b>ensures</b> result == (<b>exists</b> i in 0..len(to_add): !contains(<b>old</b>(members), to_add[i]));
<b>ensures</b> result == (<b>exists</b> e in to_add: !contains(<b>old</b>(members), e));
</code></pre>


Expand All @@ -486,9 +487,9 @@ to be a set and hence can have duplicated elements.
old_members: vector&lt;T&gt;;
new_members: vector&lt;T&gt;;
to_add: vector&lt;T&gt;;
<b>ensures</b> <b>forall</b> i in 0..len(to_add): contains(new_members, to_add[i]);
<b>ensures</b> <b>forall</b> i in 0..len(old_members): contains(new_members, old_members[i]);
<b>ensures</b> <b>forall</b> i in 0..len(new_members): (contains(old_members, new_members[i]) || contains(to_add, new_members[i]));
<b>ensures</b> <b>forall</b> e in to_add: contains(new_members, e);
<b>ensures</b> <b>forall</b> e in old_members: contains(new_members, e);
<b>ensures</b> <b>forall</b> e in new_members: (contains(old_members, e) || contains(to_add, e));
}
</code></pre>

Expand Down Expand Up @@ -531,8 +532,7 @@ to be a set and hence can have duplicated elements.
// the set can never grow in size
<b>invariant</b> len(members) &lt;= len(<b>old</b>(members));
// the current set maintains the uniqueness of the elements
<b>invariant</b> <b>forall</b> j in 0..len(members), k in 0..len(members):
members[j] == members[k] ==&gt; j == k;
<b>invariant</b> <b>forall</b> j in 0..len(members), k in 0..len(members): members[j] == members[k] ==&gt; j == k;
// all elements in the the current set come from the original set
<b>invariant</b> <b>forall</b> j in 0..len(members): contains(<b>old</b>(members), members[j]);
// the current set never contains anything from the `to_remove` vector
Expand Down Expand Up @@ -566,7 +566,7 @@ to be a set and hence can have duplicated elements.



<pre><code><b>pragma</b> timeout = 120;
<pre><code><b>pragma</b> verify = <b>false</b>;
<b>pragma</b> opaque;
<b>ensures</b> [concrete] <b>true</b>;
<b>aborts_if</b> <b>false</b>;
Expand All @@ -575,7 +575,7 @@ to be a set and hence can have duplicated elements.
new_members: members,
};
<b>include</b> <a href="NetworkIdentity.md#0x1_NetworkIdentity_UniqueMembers">UniqueMembers</a>&lt;T&gt;;
<b>ensures</b> result == (<b>exists</b> i in 0..len(to_remove): contains(<b>old</b>(members), to_remove[i]));
<b>ensures</b> result == (<b>exists</b> e in to_remove: contains(<b>old</b>(members), e));
</code></pre>


Expand All @@ -588,9 +588,9 @@ to be a set and hence can have duplicated elements.
old_members: vector&lt;T&gt;;
new_members: vector&lt;T&gt;;
to_remove: vector&lt;T&gt;;
<b>ensures</b> <b>forall</b> i in 0..len(to_remove): !contains(new_members, to_remove[i]);
<b>ensures</b> <b>forall</b> i in 0..len(new_members): contains(old_members, new_members[i]);
<b>ensures</b> <b>forall</b> i in 0..len(old_members): (contains(to_remove, old_members[i]) || contains(new_members, old_members[i]));
<b>ensures</b> <b>forall</b> e in to_remove: !contains(new_members, e);
<b>ensures</b> <b>forall</b> e in new_members: contains(old_members, e);
<b>ensures</b> <b>forall</b> e in old_members: (contains(to_remove, e) || contains(new_members, e));
}
</code></pre>

Expand Down
Loading

0 comments on commit 834439f

Please sign in to comment.