[move framework][move-prover] Some specs from LIP-6, refactoring of initialization in Genesis #5997

DavidLDill · 2020-09-11T18:21:11Z

Changes to a bunch of .move files related to LibraAccount and LibraSystem.

Added specification that every account has a role in LibraAccount.
Refactored Genesis and LibraAccount some to make this easier to prove,
and to clean up initialization. Specifically, roles for libra root
and treasury compliance were added in Genesis separately from the
account creation functions. So, I moved role creation into the account creation functions. Genesis was also creating the libra root and treasury compliance accounts directly, so I moved those into LibraAccount::initialize, which simplifies the Genesis code and eliminates some dependencies.

In various places, I renamed accounts to reflect their roles, if
known. I also added some assertion checks in SlidingNonce, which was
getting errors from unchecked aborts.

Motivation

(Write your motivation for proposed changes here.)

Have you read the Contributing Guidelines on pull requests?

(Write your answer here.)

Test Plan

(Share your test plan here. If you changed code, please provide us with clear instructions for verifying that your changes work.)

Related PRs

(If this PR adds or changes functionality, please take some time to update the docs at https://github.com/libra/website, and link to your PR here.)

bob-wilson · 2020-09-14T19:58:51Z

language/stdlib/modules/LibraSystem.move

-    //    to update, and only completes successfully if the signer is the validator operator
-    //    for that validator.
-    // set_libra_system_config is a private function, so it does not have to preserve the property.
+    /// Testricts the set of functions that can modify the validator set config.


"Testricts"?

tzakian

Overall looks good on the Move side! Only a couple cleanup comments.

tzakian · 2020-09-14T19:38:28Z

language/stdlib/modules/Genesis.move

    use 0x1::LibraVMConfig;

    fun initialize(
        lr_account: &signer,
        tc_account: &signer,
        lr_auth_key: vector<u8>,
-        tc_addr: address,
+        _tc_addr: address,


Nit: can you remove this argument? You'll need to update the call to this in language/tools/vm-genesis/src/lib.rs

I tried it, but debugging the resulting crashes in Rust were a nightmare. So, I'm going to try to land this and fix it later.

language/stdlib/modules/LibraAccount.move

language/stdlib/modules/LibraSystem.move

language/stdlib/modules/ValidatorConfig.move

language/stdlib/transaction_scripts/peer_to_peer_with_metadata.move

bob-wilson · 2020-09-14T20:22:48Z

Is this a breaking change? It certainly changes genesis a bit, but I'm not sure if anything needs to change if you don't rebuild genesis.

DavidLDill · 2020-09-15T03:35:34Z

/land

Changes to a bunch of .move files related to LibraAccount and LibraSystem. Added specification that every account has a role in LibraAccount. Refactored Genesis and LibraAccount some to make this easier to prove, and to clean up initialization. Specifically, roles for libra root and treasury compliance were added in Genesis separately from the account creation functions. So, I moved role creation into the account creation functions. Genesis was also creating the libra root and treasury compliance accounts directly, so I moved those into LibraAccount::initialize, which simplifies the Genesis code and eliminates some dependencies. In various places, I renamed accounts to reflect their roles, if known. I also added some assertion checks in SlidingNonce, which was getting errors from unchecked aborts. A fair number of files were touched for this purpose. I experimented in couple of places with cross references. Closes: #5997

bors-libra · 2020-09-15T03:38:05Z

💔 Test Failed - commit-workflow

github-actions · 2020-09-15T04:01:10Z

Cluster Test Result

Cluster setup failed: `Nodes did not become healthy after deployment`
Logs: http://kibana.ct-2-k8s-testnet.aws.hlw3truzy4ls.com/app/kibana#/discover?_g=(time:(from:'2020-09-15T03:48:59Z',to:'2020-09-15T04:01:09Z'))
Dashboard: http://grafana.ct-2-k8s-testnet.aws.hlw3truzy4ls.com/d/2XqUIhnWz/performance?from=1600141739000&to=1600142469000
Validator 1 logs: http://kibana.ct-2-k8s-testnet.aws.hlw3truzy4ls.com/app/kibana#/discover?_g=(time:(from:'2020-09-15T03:48:59Z',to:'2020-09-15T04:01:09Z'))&_a=(columns:!(log),query:(language:kuery,query:'kubernetes.pod_name:"val-1"'),sort:!(!('@timestamp',desc)))

❗ Cluster Test failed - non-zero exit code for cti

Repro cmd:

./scripts/cti --tag land_74e660b5 --cluster-test-tag land_97a7554b -E RUST_LOG=debug -E BATCH_SIZE=15 -E UPDATE_TO_TAG=land_97a7554b --report report.json --suite land_blocking_compat

wrwg · 2020-09-16T03:04:09Z

language/stdlib/modules/LibraSystem.move

+        /// LIP-6 property: validator has validator role. The code does not check this explicitly,
+        /// but it is implied by the assert ValidatorConfig::is_valid, since
+        /// a published ValidatorConfig has a ValidatorRole is an invariant (in ValidatorConfig).
+        ensures Roles::spec_has_validator_role_addr(validator_address);


This sounds like the same as the last ensures. What's the difference?

If you mean ensures(is_valid....), that implies that it address has a validator role, via another invariant, but doesn't say so directly. This ensures directly specifies the desired property, and I'm sure it's proved by combining the invariant and is_valid.

wrwg · 2020-09-16T03:06:25Z

language/stdlib/modules/LibraSystem.move

@@ -374,10 +372,13 @@ module LibraSystem {
    // This function should never throw an assertion.
    fun update_ith_validator_info_(validators: &mut vector<ValidatorInfo>, i: u64): bool {
        let size = Vector::length(validators);
+        // TODO (dd): This provably cannot happen


It is an interesting question whether we should remove the code in such cases. I would say no, for robustness. If you agree, I would remove the TODO but instead just add a comment like "Provably does not happen, but here for sanity".

wrwg · 2020-09-16T03:08:09Z

language/stdlib/modules/LibraSystem.move

@@ -394,10 +395,16 @@ module LibraSystem {
        pragma opaque;
        aborts_if false;
        let new_validator_config = ValidatorConfig::spec_get_config(validators[i].addr);
+        // Amazingly, it is able to prove this because get_validator_index_ ensures it


Use /// (here and elsewhere) and don't use expression like "amazingly"? This is documentation part of the artifact, not a note paper.

wrwg · 2020-09-16T03:10:16Z

language/stdlib/modules/LibraSystem.move

+        requires 0 <= i && i < len(validators);
+        // TODO (dd): Should be able to prove this, but it times out.
+        // Every member of validators is valid.
+        // requires ValidatorConfig::is_valid(validators[i].addr);


There is a new way how to keep such properties type checked but not verified. Use requires [deactivated] P.

wrwg · 2020-09-16T03:11:43Z

language/stdlib/modules/LibraSystem.move

+    // This also implies that every member has a validator role.
+    // TODO (dd): Times out.  I think it should not be hard, so don't know why.
+    // spec module {
+    //   let validators = spec_get_validators();


Addd [deactivated]?

wrwg · 2020-09-16T03:12:28Z

language/stdlib/modules/LibraSystem.move

+    // This also implies that every member has a validator role.
+    // TODO (dd): Times out.  I think it should not be hard, so don't know why.
+    // spec module {
+    //   let validators = spec_get_validators();


Remove let? Doesn't buy a lot.

wrwg · 2020-09-16T03:14:01Z

language/stdlib/modules/Roles.move

@@ -179,14 +179,15 @@ module Roles {
    spec fun grant_role {
        pragma opaque;
        include GrantRole;
+        let addr = Signer::spec_address_of(account);
+        // Requires to satisfy global invariants.
+        requires role_id == LIBRA_ROOT_ROLE_ID ==> addr == CoreAddresses::LIBRA_ROOT_ADDRESS();


I think this should be assertions in the code and aborts_if in the specs.

As I understand this comment, you're suggesting that I add an assert to grant_role that role_id is libra root. But this seems to me exactly the kind of situation where we would want to use "requires".

grant_role is private and every calling context has an assert that the role_id is libra root. So, this seemed right to me, since it's checked in all calling contexts and helps to prove the invariant.

wrwg · 2020-09-16T03:15:00Z

language/stdlib/modules/SlidingNonce.move

@@ -21,6 +21,8 @@ module SlidingNonce {
    const ENONCE_TOO_NEW: u64 = 2;
    /// The nonce was already recorded previously
    const ENONCE_ALREADY_RECORDED: u64 = 3;
+    /// Nonce


Please make a sentence out of this. This documentation is dumped by a debugging tool @tzakian wrote/is writing.

wrwg · 2020-09-16T03:15:45Z

language/stdlib/modules/ValidatorConfig.move

+    /// in LibraSystem so we don't have to check whether every validator address has a validator role.
+    /// <a name="ValidatorConfigImpliesValidatorRole"></a>
+    spec module {
+        invariant [global] forall addr1:address where exists_config(addr1):


Nit: spec after addr1:

runtian-zhou · 2020-09-18T00:19:27Z

There's probably some trailing whitespace issue that needs to be resolved XD

DavidLDill · 2020-09-18T16:26:51Z

/land

bors-libra · 2020-09-18T18:03:35Z

🔒 Merge Conflict

DavidLDill · 2020-09-18T19:46:45Z

/help

bors-libra · 2020-09-18T19:46:46Z

Bors help and documentation

Bors is a Github App used to manage merging of PRs in order to ensure that CI is always green. It does so by maintaining a Merge Queue. Once a PR reaches the head of the Merge Queue it is rebased on top of the latest version of the PR's base-branch (generally master) and then triggers CI. If CI comes back green the PR is then merged into the base-branch. Regardless of the outcome, the next PR is the queue is then processed.

General

This project's Merge Queue can be found here.
This project requires PRs to be Reviewed and Approved before they can be queued for merging.
Before PR's can be merged they must be configured with "Allow edits from maintainers" enabled. This is needed for Bors to be able to update PR's in-place so that Github can properly recognize and mark them as "merged" once they've been merged into the upstream branch.

Commands

Bors actions can be triggered by posting a comment which includes a line of the form /<action>.

Command	Action	Description
Land	`land`, `merge`	attempt to land or merge a PR
Canary	`canary`, `try`	canary a PR by performing all checks without merging
Cancel	`cancel`, `stop`	stop an in-progress land
Cherry Pick	`cherry-pick <target>`	cherry-pick a PR into `<target>` branch
Priority	`priority`	set the priority level for a PR (`high`, `normal`, `low`)
Help	`help`, `h`	show this help message

Options

Options for Pull Requests are configured through the application of labels.

Option	Description
	Indicates that the PR is high-priority. When queued the PR will be placed at the head of the merge queue.
	Indicates that the PR is low-priority. When queued the PR will be placed at the back of the merge queue.
	Before merging the PR will be squashed down to a single commit, only retaining the commit message of the first commit in the PR.

DavidLDill · 2020-09-18T20:50:46Z

/priority high
/land

DavidLDill · 2020-09-18T21:33:48Z

/priority high

DavidLDill · 2020-09-18T22:31:05Z

/land

…esis a bit. Potential breaking change: I'm actually not sure if this is a breaking change. I changed the order of some initialization functions in Genesis.move and it turns out the event handle generator has a counter that is incremented for each new event handle, and that this becomes part of the guid for the event handle. The resulting serialized string appears as *-event-key in the json records in json-rpc. I don't know whether clients depend on the counter values in the guids (it would better to use some other means to identify event streams, if one exists). If clients do depend on these, they might see the names event-keys change when genesis is rebuilt. For example, "received_events_key": "0000000000000000000000000000000000000000000000dd", might become "received_events_key": "0300000000000000000000000000000000000000000000dd", General comments on changes: Changes to a bunch of .move files related to LibraAccount and LibraSystem. Added specification that every account has a role in LibraAccount. Refactored Genesis and LibraAccount some to make this easier to prove, and to clean up initialization. Specifically, roles for libra root and treasury compliance were added in Genesis separately from the account creation functions. So, I moved role creation into the account creation functions. Genesis was also creating the libra root and treasury compliance accounts directly, so I moved those into LibraAccount::initialize, which simplifies the Genesis code and eliminates some dependencies. In various places, I renamed accounts to reflect their roles, if known. I also added some assertion checks in SlidingNonce, which was getting errors from unchecked aborts. A fair number of files were touched for this purpose. I experimented in couple of places with cross references. Closes: #5997

bors-libra · 2020-09-19T00:02:57Z

💔 Test Failed - commit-workflow

github-actions · 2020-09-19T00:06:23Z

Cluster Test Result

all up : 1008 TPS, 4485 ms latency, 5650 ms p99 latency, no expired txns
Logs: http://kibana.ct-2-k8s-testnet.aws.hlw3truzy4ls.com/app/kibana#/discover?_g=(time:(from:'2020-09-18T23:53:15Z',to:'2020-09-19T00:06:22Z'))
Dashboard: http://grafana.ct-2-k8s-testnet.aws.hlw3truzy4ls.com/d/2XqUIhnWz/performance?from=1600473195000&to=1600473982000
Validator 1 logs: http://kibana.ct-2-k8s-testnet.aws.hlw3truzy4ls.com/app/kibana#/discover?_g=(time:(from:'2020-09-18T23:53:15Z',to:'2020-09-19T00:06:22Z'))&_a=(columns:!(log),query:(language:kuery,query:'kubernetes.pod_name:"val-1"'),sort:!(!('@timestamp',desc)))

Repro cmd:

./scripts/cti --tag land_ca8e32a6 -E RUST_LOG=debug --report report.json --suite land_blocking

🎉 Land-blocking cluster test passed! 👌

DavidLDill · 2020-09-19T03:09:29Z

/priority high

DavidLDill · 2020-09-19T16:09:29Z

/land

…esis a bit. Potential breaking change: I'm actually not sure if this is a breaking change. I changed the order of some initialization functions in Genesis.move and it turns out the event handle generator has a counter that is incremented for each new event handle, and that this becomes part of the guid for the event handle. The resulting serialized string appears as *-event-key in the json records in json-rpc. I don't know whether clients depend on the counter values in the guids (it would better to use some other means to identify event streams, if one exists). If clients do depend on these, they might see the names event-keys change when genesis is rebuilt. For example, "received_events_key": "0000000000000000000000000000000000000000000000dd", might become "received_events_key": "0300000000000000000000000000000000000000000000dd", General comments on changes: Changes to a bunch of .move files related to LibraAccount and LibraSystem. Added specification that every account has a role in LibraAccount. Refactored Genesis and LibraAccount some to make this easier to prove, and to clean up initialization. Specifically, roles for libra root and treasury compliance were added in Genesis separately from the account creation functions. So, I moved role creation into the account creation functions. Genesis was also creating the libra root and treasury compliance accounts directly, so I moved those into LibraAccount::initialize, which simplifies the Genesis code and eliminates some dependencies. In various places, I renamed accounts to reflect their roles, if known. I also added some assertion checks in SlidingNonce, which was getting errors from unchecked aborts. A fair number of files were touched for this purpose. I experimented in couple of places with cross references. Closes: diem#5997

github-actions · 2020-09-19T16:34:05Z

Cluster Test Result

all up : 1016 TPS, 4459 ms latency, 5300 ms p99 latency, no expired txns
Logs: http://kibana.ct-1-k8s-testnet.aws.hlw3truzy4ls.com/app/kibana#/discover?_g=(time:(from:'2020-09-19T16:22:51Z',to:'2020-09-19T16:34:03Z'))
Dashboard: http://grafana.ct-1-k8s-testnet.aws.hlw3truzy4ls.com/d/2XqUIhnWz/performance?from=1600532571000&to=1600533243000
Validator 1 logs: http://kibana.ct-1-k8s-testnet.aws.hlw3truzy4ls.com/app/kibana#/discover?_g=(time:(from:'2020-09-19T16:22:51Z',to:'2020-09-19T16:34:03Z'))&_a=(columns:!(log),query:(language:kuery,query:'kubernetes.pod_name:"val-1"'),sort:!(!('@timestamp',desc)))

Repro cmd:

./scripts/cti --tag land_837052ef -E RUST_LOG=debug --report report.json --suite land_blocking

🎉 Land-blocking cluster test passed! 👌

DavidLDill requested a review from tzakian September 11, 2020 18:21

bors-libra added this to In Review in bors Sep 11, 2020

diem-cla-bot bot added the cla-signed label Sep 11, 2020

DavidLDill force-pushed the every_account_has_role branch from b7bee58 to cff02ba Compare September 11, 2020 18:27

DavidLDill changed the title ~~[move framework][move-prover] DRAFT: Move role creation from Genesis to LibraAccount~~ [move framework][move-prover] Some specs from LIP-6, refactoring of initialization in Genesis Sep 13, 2020

DavidLDill force-pushed the every_account_has_role branch from cff02ba to e82e323 Compare September 14, 2020 17:57

DavidLDill marked this pull request as ready for review September 14, 2020 17:58

DavidLDill requested review from junkil-park, emmazzz and wrwg September 14, 2020 17:59

bob-wilson reviewed Sep 14, 2020

View reviewed changes

tzakian approved these changes Sep 14, 2020

View reviewed changes

DavidLDill force-pushed the every_account_has_role branch from e82e323 to abb0a61 Compare September 15, 2020 03:34

bors-libra moved this from In Review to Queued in bors Sep 15, 2020

bors-libra moved this from Queued to Testing in bors Sep 15, 2020

bors-libra moved this from Testing to In Review in bors Sep 15, 2020

DavidLDill force-pushed the every_account_has_role branch from abb0a61 to 042f3fb Compare September 15, 2020 17:33

wrwg approved these changes Sep 16, 2020

View reviewed changes

DavidLDill force-pushed the every_account_has_role branch from 042f3fb to 10456de Compare September 16, 2020 17:04

xli approved these changes Sep 16, 2020

View reviewed changes

runtian-zhou mentioned this pull request Sep 16, 2020

[breaking][libra-framework] Refactor writeset prologue and epilogue #6042

Merged

DavidLDill force-pushed the every_account_has_role branch from 10456de to 1aeb35c Compare September 18, 2020 00:16

DavidLDill requested a review from thefallentree as a code owner September 18, 2020 00:16

DavidLDill force-pushed the every_account_has_role branch from 1aeb35c to cf4f1fa Compare September 18, 2020 00:52

bors-libra moved this from Testing to In Review in bors Sep 18, 2020

DavidLDill force-pushed the every_account_has_role branch from 1c541a2 to e28476c Compare September 18, 2020 16:26

bors-libra moved this from In Review to Queued in bors Sep 18, 2020

bors-libra moved this from Queued to In Review in bors Sep 18, 2020

DavidLDill force-pushed the every_account_has_role branch from e28476c to abde1f7 Compare September 18, 2020 20:49

bors-libra added the bors-high-priority label Sep 18, 2020

bors-libra moved this from In Review to Queued in bors Sep 18, 2020

bors-libra moved this from Queued to Testing in bors Sep 18, 2020

bors-libra moved this from Testing to In Review in bors Sep 19, 2020

DavidLDill force-pushed the every_account_has_role branch from abde1f7 to 9849164 Compare September 19, 2020 03:04

bors-libra moved this from In Review to Queued in bors Sep 19, 2020

bors-libra moved this from Queued to Testing in bors Sep 19, 2020

bors-libra force-pushed the every_account_has_role branch from 9849164 to 837052e Compare September 19, 2020 16:34

bors-libra removed this from Testing in bors Sep 19, 2020

bors-libra closed this in 837052e Sep 19, 2020

bors-libra merged commit 837052e into diem:master Sep 19, 2020

[move framework][move-prover] Some specs from LIP-6, refactoring of initialization in Genesis #5997

[move framework][move-prover] Some specs from LIP-6, refactoring of initialization in Genesis #5997

Conversation

DavidLDill commented Sep 11, 2020

Motivation

Have you read the Contributing Guidelines on pull requests?

Test Plan

Related PRs

Choose a reason for hiding this comment

tzakian left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bob-wilson commented Sep 14, 2020

DavidLDill commented Sep 15, 2020

bors-libra commented Sep 15, 2020

github-actions bot commented Sep 15, 2020

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

runtian-zhou commented Sep 18, 2020

DavidLDill commented Sep 18, 2020

bors-libra commented Sep 18, 2020

DavidLDill commented Sep 18, 2020

bors-libra commented Sep 18, 2020

General

Commands

Options

DavidLDill commented Sep 18, 2020

DavidLDill commented Sep 18, 2020

DavidLDill commented Sep 18, 2020

bors-libra commented Sep 19, 2020

github-actions bot commented Sep 19, 2020

DavidLDill commented Sep 19, 2020

DavidLDill commented Sep 19, 2020

github-actions bot commented Sep 19, 2020