Specified more transaction scripts

Specified the following transaction scripts:
- burn.move
- publish_shared_ed25519_public_key.move
- rotate_dual_attestation_info.move
- rotate_shared_ed25519_public_key.move

Specified the SharedEd25519PublicKey module

Added the following governance spec to DualAttestation:
- the resource `Credential` is not transferrable.
- the invariant that only PareantVASP or DD can have `Credential`

Added the spec function & test cases for the native functions in Signature

Closes: aptos-labs#6093

language/move-prover/tests/sources/functional/verify_lcs.move

@@ -1,6 +1,6 @@
 // This file is created to verify the native function in the standard LCS module.
 
-module VerifyVector {
+module VerifyLCS {
     use 0x1::LCS;
 
     public fun verify_to_bytes<MoveValue>(v: &MoveValue): vector<u8>

language/move-prover/tests/sources/functional/verify_signature.move

@@ -0,0 +1,23 @@
+// This file is created to verify the native function in the standard LCS module.
+
+module VerifySignature {
+    use 0x1::Signature;
+
+    public fun verify_ed25519_validate_pubkey(public_key: vector<u8>): bool {
+        Signature::ed25519_validate_pubkey(public_key)
+    }
+    spec fun verify_ed25519_validate_pubkey {
+        ensures result == Signature::ed25519_validate_pubkey(public_key);
+    }
+
+    public fun verify_ed25519_verify(
+        signature: vector<u8>,
+        public_key: vector<u8>,
+        message: vector<u8>
+    ): bool {
+        Signature::ed25519_verify(signature, public_key, message)
+    }
+    spec fun verify_ed25519_verify {
+        ensures result == Signature::ed25519_verify(signature, public_key, message);
+    }
+}

language/stdlib/modules/Authenticator.move

@@ -62,6 +62,13 @@ module Authenticator {
         Vector::push_back(&mut public_key, SINGLE_ED25519_SCHEME_ID);
         Hash::sha3_256(public_key)
     }
+    spec fun ed25519_authentication_key {
+        pragma opaque = true;
+        pragma verify = false;
+        aborts_if false;
+        ensures result == spec_ed25519_authentication_key(public_key);
+    }
+    spec define spec_ed25519_authentication_key(public_key: vector<u8>): vector<u8>;
 
     /// Compute a multied25519 account authentication key for the policy `k`
     public fun multi_ed25519_authentication_key(k: &MultiEd25519PublicKey): vector<u8> {

language/stdlib/modules/DualAttestation.move

@@ -129,14 +129,24 @@ module DualAttestation {
         });
     }
     spec fun rotate_base_url {
+        include RotateBaseUrlAbortsIf;
+        include RotateBaseUrlEnsures;
+    }
+    spec schema RotateBaseUrlAbortsIf {
+        account: signer;
         let sender = Signer::spec_address_of(account);
 
         /// Must abort if the account does not have the resource Credential [B25].
         include AbortsIfNoCredential{addr: sender};
 
         include LibraTimestamp::AbortsIfNotOperating;
-        ensures global<Credential>(sender).base_url == new_url;
+    }
+    spec schema RotateBaseUrlEnsures {
+        account: signer;
+        new_url: vector<u8>;
+        let sender = Signer::spec_address_of(account);
 
+        ensures global<Credential>(sender).base_url == new_url;
         /// The sender can only rotate its own base url [B25].
         ensures forall addr:address where addr != sender:
             global<Credential>(addr).base_url == old(global<Credential>(addr).base_url);
@@ -163,13 +173,25 @@ module DualAttestation {
 
     }
     spec fun rotate_compliance_public_key {
-        let sender = Signer::spec_address_of(account);
+        include RotateCompliancePublicKeyAbortsIf;
+        include RotateCompliancePublicKeyEnsures;
+    }
+    spec schema RotateCompliancePublicKeyAbortsIf {
+        account: signer;
+        new_key: vector<u8>;
 
+        let sender = Signer::spec_address_of(account);
         /// Must abort if the account does not have the resource Credential [B25].
         include AbortsIfNoCredential{addr: sender};
 
         include LibraTimestamp::AbortsIfNotOperating;
         aborts_if !Signature::ed25519_validate_pubkey(new_key) with Errors::INVALID_ARGUMENT;
+    }
+    spec schema RotateCompliancePublicKeyEnsures {
+        account: signer;
+        new_key: vector<u8>;
+
+        let sender = Signer::spec_address_of(account);
         ensures global<Credential>(sender).compliance_public_key == new_key;
         /// The sender only rotates its own compliance_public_key [B25].
         ensures forall addr:address where addr != sender:
@@ -487,6 +509,32 @@ module DualAttestation {
         }
     }
 
+    spec schema PreserveCredentialExistence {
+        /// The existence of Preburn is preserved.
+        ensures forall addr1: address:
+            old(exists<Credential>(addr1)) ==>
+                exists<Credential>(addr1);
+    }
+    spec schema PreserveCredentialAbsence {
+        /// The absence of Preburn is preserved.
+        ensures forall addr1: address:
+            old(!exists<Credential>(addr1)) ==>
+                !exists<Credential>(addr1);
+    }
+    spec module {
+        /// The permission "RotateDualAttestationInfo(addr)" is not transferred [D25].
+        apply PreserveCredentialExistence to *;
+
+        /// The permission "RotateDualAttestationInfo(addr)" is only granted to ParentVASP or DD [B25].
+        /// "Credential" resources are only published under ParentVASP or DD accounts.
+        apply PreserveCredentialAbsence to * except publish_credential;
+        apply Roles::AbortsIfNotParentVaspOrDesignatedDealer{account: created} to publish_credential;
+        invariant [global] forall addr1: address:
+            exists<Credential>(addr1) ==>
+                (Roles::spec_has_parent_VASP_role_addr(addr1) ||
+                Roles::spec_has_designated_dealer_role_addr(addr1));
+    }
+
     /// Only set_microlibra_limit can change the limit [B15].
     spec schema DualAttestationLimitRemainsSame {
         /// The DualAttestation limit stays constant.

language/stdlib/modules/Libra.move

@@ -276,11 +276,24 @@ module Libra {
         )
     }
     spec fun burn {
+        include BurnAbortsIf<CoinType>;
+        include BurnEnsures<CoinType>;
+    }
+    spec schema BurnAbortsIf<CoinType> {
+        account: signer;
+        preburn_address: address;
+
         /// Must abort if the account does not have the BurnCapability [B12].
         aborts_if !exists<BurnCapability<CoinType>>(Signer::spec_address_of(account)) with Errors::REQUIRES_CAPABILITY;
 
         aborts_if !exists<Preburn<CoinType>>(preburn_address) with Errors::NOT_PUBLISHED;
-        include BurnAbortsIf<CoinType>{preburn: global<Preburn<CoinType>>(preburn_address)};
+        include BurnWithResourceCapAbortsIf<CoinType>{preburn: global<Preburn<CoinType>>(preburn_address)};
+    }
+    spec schema BurnEnsures<CoinType> {
+        account: signer;
+        preburn_address: address;
+
+        include BurnWithResourceCapEnsures<CoinType>{preburn: global<Preburn<CoinType>>(preburn_address)};
     }
 
     /// Cancels the current burn request in the `Preburn` resource held
@@ -504,8 +517,8 @@ module Libra {
     }
     spec fun burn_with_capability {
         aborts_if !exists<Preburn<CoinType>>(preburn_address) with Errors::NOT_PUBLISHED;
-        include BurnAbortsIf<CoinType>{preburn: global<Preburn<CoinType>>(preburn_address)};
-        include BurnEnsures<CoinType>{preburn: global<Preburn<CoinType>>(preburn_address)};
+        include BurnWithResourceCapAbortsIf<CoinType>{preburn: global<Preburn<CoinType>>(preburn_address)};
+        include BurnWithResourceCapEnsures<CoinType>{preburn: global<Preburn<CoinType>>(preburn_address)};
     }
 
     /// Permanently removes the coins held in the `Preburn` resource (in to_burn field)
@@ -545,11 +558,11 @@ module Libra {
         };
     }
     spec fun burn_with_resource_cap {
-        include BurnAbortsIf<CoinType>;
-        include BurnEnsures<CoinType>;
+        include BurnWithResourceCapAbortsIf<CoinType>;
+        include BurnWithResourceCapEnsures<CoinType>;
     }
 
-    spec schema BurnAbortsIf<CoinType> {
+    spec schema BurnWithResourceCapAbortsIf<CoinType> {
         preburn: Preburn<CoinType>;
         include AbortsIfNoCurrency<CoinType>;
         let to_burn = preburn.to_burn.value;
@@ -559,7 +572,7 @@ module Libra {
         aborts_if info.preburn_value < to_burn with Errors::LIMIT_EXCEEDED;
     }
 
-    spec schema BurnEnsures<CoinType> {
+    spec schema BurnWithResourceCapEnsures<CoinType> {
         preburn: Preburn<CoinType>;
         ensures spec_currency_info<CoinType>().total_value
                 == old(spec_currency_info<CoinType>().total_value) - old(preburn.to_burn.value);
@@ -1158,11 +1171,10 @@ module Libra {
         /// required. MintCapability must be only granted to a TreasuryCompliance account [B11].
         /// Only `register_SCS_currency` creates MintCapability, which must abort if the account
         /// does not have the TreasuryCompliance role [B17].
-        // TODO(jkpark): This kind of spec needs to be rewritten later. The problem of this spec is
-        // that it is in the form of the schema application, so verified against all the functions
-        // only in this module. Even though this is verified, there might be a function in an other
-        // module that violates this property (by obtaining a MintCapability from `register_currency`
-        // and publishing it somewhere inappropriate).
+        // TODO(jkpark): this spec does not cover the following two scenarios:
+        // a function (possibly in an other module) obtains a MintCapability from `register_currency`, and
+        // (1) uses the MintCapability for minting without publishing it, and/or
+        // (2) stashes the MintCapability inside of an other struct in the global memory.
         apply PreserveMintCapAbsence<CoinType> to *<CoinType> except register_SCS_currency<CoinType>;
         apply Roles::AbortsIfNotTreasuryCompliance{account: tc_account} to register_SCS_currency<CoinType>;
 

language/stdlib/modules/SharedEd25519PublicKey.move

@@ -38,6 +38,32 @@ module SharedEd25519PublicKey {
         assert(!exists<SharedEd25519PublicKey>(Signer::address_of(account)), Errors::already_published(ESHARED_KEY));
         move_to(account, t);
     }
+    spec fun publish {
+        include PublishAbortsIf;
+        include PublishEnsures;
+    }
+    spec schema PublishAbortsIf {
+        account: signer;
+        key: vector<u8>;
+        let addr = Signer::spec_address_of(account);
+        include LibraAccount::ExtractKeyRotationCapabilityAbortsIf;
+        include RotateKey_AbortsIf {
+                shared_key: SharedEd25519PublicKey {
+                    key: x"",
+                    rotation_cap: LibraAccount::spec_get_key_rotation_cap(addr)
+                },
+                new_public_key: key
+        };
+        aborts_if exists<SharedEd25519PublicKey>(addr) with Errors::ALREADY_PUBLISHED;
+    }
+    spec schema PublishEnsures {
+        account: signer;
+        key: vector<u8>;
+        let addr = Signer::spec_address_of(account);
+
+        ensures exists<SharedEd25519PublicKey>(addr);
+        include RotateKey_Ensures { shared_key: global<SharedEd25519PublicKey>(addr), new_public_key: key};
+    }
 
     fun rotate_key_(shared_key: &mut SharedEd25519PublicKey, new_public_key: vector<u8>) {
         // Cryptographic check of public key validity
@@ -51,6 +77,24 @@ module SharedEd25519PublicKey {
         );
         shared_key.key = new_public_key;
     }
+    spec fun rotate_key_ {
+        include RotateKey_AbortsIf;
+        include RotateKey_Ensures;
+    }
+    spec schema RotateKey_AbortsIf {
+        shared_key: SharedEd25519PublicKey;
+        new_public_key: vector<u8>;
+        aborts_if !Signature::ed25519_validate_pubkey(new_public_key) with Errors::INVALID_ARGUMENT;
+        include LibraAccount::RotateAuthenticationKeyAbortsIf {
+            cap: shared_key.rotation_cap,
+            new_authentication_key: Authenticator::spec_ed25519_authentication_key(new_public_key)
+        };
+    }
+    spec schema RotateKey_Ensures {
+        shared_key: SharedEd25519PublicKey;
+        new_public_key: vector<u8>;
+        ensures shared_key.key == new_public_key;
+    }
 
     /// (1) rotate the public key stored `account`'s `SharedEd25519PublicKey` resource to
     /// `new_public_key`
@@ -63,6 +107,23 @@ module SharedEd25519PublicKey {
         assert(exists<SharedEd25519PublicKey>(addr), Errors::not_published(ESHARED_KEY));
         rotate_key_(borrow_global_mut<SharedEd25519PublicKey>(addr), new_public_key);
     }
+    spec fun rotate_key {
+        include RotateKeyAbortsIf;
+        include RotateKeyEnsures;
+    }
+    spec schema RotateKeyAbortsIf {
+        account: signer;
+        new_public_key: vector<u8>;
+        let addr = Signer::spec_address_of(account);
+        aborts_if !exists<SharedEd25519PublicKey>(addr) with Errors::NOT_PUBLISHED;
+        include RotateKey_AbortsIf {shared_key: global<SharedEd25519PublicKey>(addr)};
+    }
+    spec schema RotateKeyEnsures {
+        account: signer;
+        new_public_key: vector<u8>;
+        let addr = Signer::spec_address_of(account);
+        include RotateKey_Ensures {shared_key: global<SharedEd25519PublicKey>(addr)};
+    }
 
     /// Return the public key stored under `addr`.
     /// Aborts if `addr` does not hold a `SharedEd25519PublicKey` resource.

language/stdlib/modules/doc/Authenticator.md

@@ -17,6 +17,8 @@
 -  [Function `multi_ed25519_authentication_key`](#0x1_Authenticator_multi_ed25519_authentication_key)
 -  [Function `public_keys`](#0x1_Authenticator_public_keys)
 -  [Function `threshold`](#0x1_Authenticator_threshold)
+-  [Specification](#0x1_Authenticator_Specification)
+    -  [Function `ed25519_authentication_key`](#0x1_Authenticator_Specification_ed25519_authentication_key)
 
 Move representation of the authenticator types used in Libra:
 - Ed25519 (single-sig)
@@ -288,3 +290,34 @@ Return the threshold for the multisig policy <code>k</code>
 
 
 </details>
+
+<a name="0x1_Authenticator_Specification"></a>
+
+## Specification
+
+
+
+<a name="0x1_Authenticator_spec_ed25519_authentication_key"></a>
+
+
+<pre><code><b>define</b> <a href="#0x1_Authenticator_spec_ed25519_authentication_key">spec_ed25519_authentication_key</a>(public_key: vector&lt;u8&gt;): vector&lt;u8&gt;;
+</code></pre>
+
+
+
+<a name="0x1_Authenticator_Specification_ed25519_authentication_key"></a>
+
+### Function `ed25519_authentication_key`
+
+
+<pre><code><b>public</b> <b>fun</b> <a href="#0x1_Authenticator_ed25519_authentication_key">ed25519_authentication_key</a>(public_key: vector&lt;u8&gt;): vector&lt;u8&gt;
+</code></pre>
+
+
+
+
+<pre><code>pragma opaque = <b>true</b>;
+pragma verify = <b>false</b>;
+<b>aborts_if</b> <b>false</b>;
+<b>ensures</b> result == <a href="#0x1_Authenticator_spec_ed25519_authentication_key">spec_ed25519_authentication_key</a>(public_key);
+</code></pre>