[Spec] Update spec of code.move (aptos-labs#8888)

* init

* mock up native error

* bypass compiler error

* init PR

* fix typeo

* add comment

* fix lint error

aptos-move/framework/aptos-framework/doc/code.md

@@ -551,12 +551,15 @@ package.
     <b>let</b> allowed_deps = <a href="code.md#0x1_code_check_dependencies">check_dependencies</a>(addr, &pack);
 
     // Check package against conflicts
+    // To avoid prover compiler <a href="../../aptos-stdlib/../move-stdlib/doc/error.md#0x1_error">error</a> on <b>spec</b>
+    // the package need <b>to</b> be an immutable variable
     <b>let</b> module_names = <a href="code.md#0x1_code_get_module_names">get_module_names</a>(&pack);
-    <b>let</b> packages = &<b>mut</b> <b>borrow_global_mut</b>&lt;<a href="code.md#0x1_code_PackageRegistry">PackageRegistry</a>&gt;(addr).packages;
-    <b>let</b> len = <a href="../../aptos-stdlib/../move-stdlib/doc/vector.md#0x1_vector_length">vector::length</a>(packages);
+    <b>let</b> package_immutable = &<b>borrow_global</b>&lt;<a href="code.md#0x1_code_PackageRegistry">PackageRegistry</a>&gt;(addr).packages;
+    <b>let</b> len = <a href="../../aptos-stdlib/../move-stdlib/doc/vector.md#0x1_vector_length">vector::length</a>(package_immutable);
     <b>let</b> index = len;
     <b>let</b> upgrade_number = 0;
-    <a href="../../aptos-stdlib/../move-stdlib/doc/vector.md#0x1_vector_enumerate_ref">vector::enumerate_ref</a>(packages, |i, <b>old</b>| {
+    <a href="../../aptos-stdlib/../move-stdlib/doc/vector.md#0x1_vector_enumerate_ref">vector::enumerate_ref</a>(package_immutable
+    , |i, <b>old</b>| {
         <b>let</b> <b>old</b>: &<a href="code.md#0x1_code_PackageMetadata">PackageMetadata</a> = <b>old</b>;
         <b>if</b> (<b>old</b>.name == pack.name) {
             upgrade_number = <b>old</b>.upgrade_number + 1;
@@ -570,6 +573,7 @@ package.
     // Assign the upgrade counter.
     pack.upgrade_number = upgrade_number;
 
+    <b>let</b> packages = &<b>mut</b> <b>borrow_global_mut</b>&lt;<a href="code.md#0x1_code_PackageRegistry">PackageRegistry</a>&gt;(addr).packages;
     // Update registry
     <b>let</b> policy = pack.upgrade_policy;
     <b>if</b> (index &lt; len) {
@@ -918,7 +922,10 @@ Native function to initiate module loading, including a list of allowed dependen
 
 
 
-<pre><code><b>pragma</b> verify = <b>false</b>;
+<pre><code><b>pragma</b> aborts_if_is_partial;
+<b>let</b> addr = <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(owner);
+<b>modifies</b> <b>global</b>&lt;<a href="code.md#0x1_code_PackageRegistry">PackageRegistry</a>&gt;(addr);
+<b>aborts_if</b> pack.upgrade_policy.policy &lt;= <a href="code.md#0x1_code_upgrade_policy_arbitrary">upgrade_policy_arbitrary</a>().policy;
 </code></pre>
 
 
@@ -950,7 +957,9 @@ Native function to initiate module loading, including a list of allowed dependen
 
 
 
-<pre><code><b>pragma</b> verify = <b>false</b>;
+<pre><code><b>pragma</b> aborts_if_is_partial;
+<b>aborts_if</b> old_pack.upgrade_policy.policy &gt;= <a href="code.md#0x1_code_upgrade_policy_immutable">upgrade_policy_immutable</a>().policy;
+<b>aborts_if</b> !<a href="code.md#0x1_code_can_change_upgrade_policy_to">can_change_upgrade_policy_to</a>(old_pack.upgrade_policy, new_pack.upgrade_policy);
 </code></pre>
 
 

aptos-move/framework/aptos-framework/sources/code.move

@@ -145,12 +145,15 @@ module aptos_framework::code {
         let allowed_deps = check_dependencies(addr, &pack);
 
         // Check package against conflicts
+        // To avoid prover compiler error on spec
+        // the package need to be an immutable variable
         let module_names = get_module_names(&pack);
-        let packages = &mut borrow_global_mut<PackageRegistry>(addr).packages;
-        let len = vector::length(packages);
+        let package_immutable = &borrow_global<PackageRegistry>(addr).packages;
+        let len = vector::length(package_immutable);
         let index = len;
         let upgrade_number = 0;
-        vector::enumerate_ref(packages, |i, old| {
+        vector::enumerate_ref(package_immutable
+        , |i, old| {
             let old: &PackageMetadata = old;
             if (old.name == pack.name) {
                 upgrade_number = old.upgrade_number + 1;
@@ -164,6 +167,7 @@ module aptos_framework::code {
         // Assign the upgrade counter.
         pack.upgrade_number = upgrade_number;
 
+        let packages = &mut borrow_global_mut<PackageRegistry>(addr).packages;
         // Update registry
         let policy = pack.upgrade_policy;
         if (index < len) {

aptos-move/framework/aptos-framework/sources/code.spec.move

@@ -23,27 +23,32 @@ spec aptos_framework::code {
     }
 
     spec publish_package(owner: &signer, pack: PackageMetadata, code: vector<vector<u8>>) {
-        // TODO: Can't verify `check_upgradability` in while loop.
-        pragma verify = false;
+        // TODO: Can't verify 'vector::enumerate' loop.
+        pragma aborts_if_is_partial;
+        let addr = signer::address_of(owner);
+        modifies global<PackageRegistry>(addr);
+        aborts_if pack.upgrade_policy.policy <= upgrade_policy_arbitrary().policy;
     }
 
     spec publish_package_txn {
-        // TODO: Calls `publish_package`.`
+        // TODO: Calls `publish_package`.
         pragma verify = false;
     }
 
     spec check_upgradability(old_pack: &PackageMetadata, new_pack: &PackageMetadata, new_modules: &vector<String>) {
-        // TODO: Can't `aborts_if` in a loop.
-        pragma verify = false;
+        // TODO: Can't verify 'vector::enumerate' loop.
+        pragma aborts_if_is_partial;
+        aborts_if old_pack.upgrade_policy.policy >= upgrade_policy_immutable().policy;
+        aborts_if !can_change_upgrade_policy_to(old_pack.upgrade_policy, new_pack.upgrade_policy);
     }
 
     spec check_dependencies(publish_address: address, pack: &PackageMetadata): vector<AllowedDep> {
-        // TODO: loop too deep.
+        // TODO: Can't verify 'vector::enumerate' loop.
         pragma verify = false;
     }
 
     spec check_coexistence(old_pack: &PackageMetadata, new_modules: &vector<String>) {
-        // TODO: loop too deep.
+        // TODO: Can't verify 'vector::enumerate' loop.
         pragma verify = false;
     }