fixup! fixup! fixup! [libra-framework] Refactor writeset prologue and…

… epilogue
diem · Sep 16, 2020 · 63cc29b · 63cc29b
1 parent 984bbcb
commit 63cc29b
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 0 deletions.
diff --git a/language/stdlib/modules/LibraAccount.move b/language/stdlib/modules/LibraAccount.move
@@ -1173,6 +1173,8 @@ module LibraAccount {
     }
 
     spec fun writeset_prologue {
+        include CoreAddresses::AbortsIfNotLibraRoot{account: sender};
+
         /// Must abort if the signer does not have the LibraRoot role [B18].
         aborts_if !Roles::spec_has_libra_root_role_addr(Signer::address_of(sender));
     }

diff --git a/language/stdlib/modules/doc/LibraAccount.md b/language/stdlib/modules/doc/LibraAccount.md
@@ -3348,6 +3348,11 @@ Can only rotate the authentication_key of cap.account_address [B26].
 
 
 
+
+<pre><code><b>include</b> <a href="CoreAddresses.md#0x1_CoreAddresses_AbortsIfNotLibraRoot">CoreAddresses::AbortsIfNotLibraRoot</a>{account: sender};
+</code></pre>
+
+
 Must abort if the signer does not have the LibraRoot role [B18].