[prover] Update MSL doc (#784)

* update MSL doc

* update link

* revise example

Author: rahxephon89

apps/nextra/pages/en/build/smart-contracts/error-codes.mdx

@@ -14,7 +14,7 @@ For the sources of these errors, see:
 
 - [vm_status.rs](https://github.com/aptos-labs/aptos-core/blob/main/third_party/move/move-core/types/src/vm_status.rs)
 - [error.move](https://github.com/aptos-labs/aptos-core/blob/main/aptos-move/framework/move-stdlib/sources/error.move)
-- [account.move](https://github.com/aptos-labs/aptos-core/blob/main/aptos-move/framework/aptos-framework/sources/account.move)
+- [account.move](https://github.com/aptos-labs/aptos-core/blob/main/aptos-move/framework/aptos-framework/sources/account/account.move)
 - [coin.move](https://github.com/aptos-labs/aptos-core/blob/main/aptos-move/framework/aptos-framework/sources/coin.move)
 - [token.move](https://github.com/aptos-labs/aptos-core/blob/main/aptos-move/framework/aptos-token/sources/token.move)
 - [token_transfers.move](https://github.com/aptos-labs/aptos-core/blob/main/aptos-move/framework/aptos-token/sources/token_transfers.move)

apps/nextra/pages/en/build/smart-contracts/prover/spec-lang.mdx

@@ -136,12 +136,6 @@ exists <binding>, ..., <binding> [ where <exp> ] : <exp>
 - The optional constraint `where <exp>` allows to restrict the quantified range. `forall x: T where p: q`
   is equivalent to `forall x: T : p ==> q` and `exists x: T where p: q` is equivalent to `exists x: T : p && q`.
 
-Notice that it is possible to quantify over types. For example:
-
-```move
-forall t: type, addr: address where exists<R<t>>(addr): exists<T<t>>(addr)
-```
-
 ## Choice operator
 
 The choice operator allows selecting a value that satisfies a predicate:
@@ -658,20 +652,6 @@ module 0x42::m {
 }
 ```
 
-If this is not wanted, and the `aborts_with` should be independent of `aborts_if`, one can use the
-property `[check]`:
-
-```move
-module 0x42::m {
-  spec get_one_off {
-    aborts_if !exists<Counter>(addr) with 3;
-    aborts_if global<Counter>(addr) == 0 with EXECUTION_FAILURE;
-
-    aborts_with [check] 3, EXECUTION_FAILURE;
-  }
-}
-```
-
 ## Requires condition
 
 The `requires` condition is a spec block member that postulates a pre-condition for a function. The
@@ -857,6 +837,14 @@ module 0x42::m {
 }
 ```
 
+Notice that type parameters are supported in global invariants. For example, the invariant above can be rewritten into the below one if `Counter` is generic:
+
+```move
+module addr::M {
+    invariant<T> forall a: addr where exists<Counter<T>>(a): global<Counter<T>>(a).value > 0;
+}
+```
+
 #### Disabling invariants
 
 There are times when a global invariant holds almost everywhere, except for a brief interval inside a function. In current Move code, this often occurs when something (e.g. an account) is being set up and

apps/nextra/pages/en/build/smart-contracts/resource-accounts.mdx

@@ -83,4 +83,4 @@ For an example, see the `SignerCapability` employed by the `mint_nft` function
 in [`minting.move`](https://github.com/aptos-labs/aptos-core/blob/2e9d8ee759fcd3f6e831034f05c1656b1c48efc4/aptos-move/move-examples/mint_nft/sources/minting.move#L143-L181).
 
 For more details, see the "resource account" references in [`resource_account.move`](https://github.com/aptos-labs/aptos-core/blob/main/aptos-move/framework/aptos-framework/sources/resource_account.move)
-and [`account.move`](https://github.com/aptos-labs/aptos-core/blob/main/aptos-move/framework/aptos-framework/sources/account.move).
+and [`account.move`](https://github.com/aptos-labs/aptos-core/blob/main/aptos-move/framework/aptos-framework/sources/account/account.move).

apps/nextra/pages/ja/build/smart-contracts/error-codes.mdx

@@ -10,7 +10,7 @@ title: "Aptosのエラーコード"
 
 - [vm_status.rs](https://github.com/aptos-labs/aptos-core/blob/main/third_party/move/move-core/types/src/vm_status.rs)
 - [error.move](https://github.com/aptos-labs/aptos-core/blob/main/aptos-move/framework/move-stdlib/sources/error.move)
-- [account.move](https://github.com/aptos-labs/aptos-core/blob/main/aptos-move/framework/aptos-framework/sources/account.move)
+- [account.move](https://github.com/aptos-labs/aptos-core/blob/main/aptos-move/framework/aptos-framework/sources/account/account.move)
 - [coin.move](https://github.com/aptos-labs/aptos-core/blob/main/aptos-move/framework/aptos-framework/sources/coin.move)
 - [token.move](https://github.com/aptos-labs/aptos-core/blob/main/aptos-move/framework/aptos-token/sources/token.move)
 - [token_transfers.move](https://github.com/aptos-labs/aptos-core/blob/main/aptos-move/framework/aptos-token/sources/token_transfers.move)

apps/nextra/pages/ja/build/smart-contracts/resource-accounts.mdx

@@ -42,4 +42,4 @@ Aptosでは、リソースアカウントはソースアドレスと追加のシ
 
 例として、[`minting.move`](https://github.com/aptos-labs/aptos-core/blob/2e9d8ee759fcd3f6e831034f05c1656b1c48efc4/aptos-move/move-examples/mint_nft/sources/minting.move#L143-L181)の`mint_nft`関数で使用される`SignerCapability`を参照してください。
 
-詳細については、[`resource_account.move`](https://github.com/aptos-labs/aptos-core/blob/main/aptos-move/framework/aptos-framework/sources/resource_account.move)と[`account.move`](https://github.com/aptos-labs/aptos-core/blob/main/aptos-move/framework/aptos-framework/sources/account.move)の「リソースアカウント」に関する参照を参照してください。
+詳細については、[`resource_account.move`](https://github.com/aptos-labs/aptos-core/blob/main/aptos-move/framework/aptos-framework/sources/resource_account.move)と[`account.move`](https://github.com/aptos-labs/aptos-core/blob/main/aptos-move/framework/aptos-framework/sources/account/account.move)の「リソースアカウント」に関する参照を参照してください。