fix spec

starcoinorg · May 22, 2022 · 08285aa · 08285aa
1 parent 95ab521
commit 08285aa
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 3 deletions.
diff --git a/sources/Account.move b/sources/Account.move
@@ -1003,8 +1003,8 @@ module Account {
 
     spec remove_zero_balance {
         let addr = Signer::address_of(account);
-        aborts_if !old(exists<Balance<TokenType>>(addr));
-        ensures !exists<Balance<CoinType>>(addr);
+        aborts_if !exists<Balance<TokenType>>(addr);
+        ensures !exists<Balance<TokenType>>(addr);
     }
 }
 

diff --git a/sources/NFT.move b/sources/NFT.move
@@ -892,10 +892,11 @@ module NFTGallery {
 
     spec remove_empty_gallery {
         let sender_addr = Signer::address_of(sender);
-        aborts_if !old(exists<NFTGallery<NFTMeta, NFTBody>>(sender_addr));
+        aborts_if !exists<NFTGallery<NFTMeta, NFTBody>>(sender_addr);
 
         let gallery = global<NFTGallery<NFTMeta, NFTBody>>(sender_addr);
         aborts_if Vector::length<NFT<NFTMeta, NFTBody>>(gallery.items) > 0;
+
         ensures !exists<NFTGallery<NFTMeta, NFTBody>>(sender_addr);
     }