From 66bd5b4aab592bf23e0000506dc1082e7ac6c9e3 Mon Sep 17 00:00:00 2001
From: zoz <97761083+0xzoz@users.noreply.github.com>
Date: Fri, 16 Feb 2024 02:47:51 -0800
Subject: [PATCH] [fix] formal verification ci (#179)

---
 framework/Makefile                            | 24 ++++++++++++++-----
 .../sources/ol_sources/slow_wallet.move       |  6 ++++-
 .../sources/ol_sources/slow_wallet.spec.move  |  3 ++-
 3 files changed, 25 insertions(+), 8 deletions(-)

diff --git a/framework/Makefile b/framework/Makefile
index 79e5a9708..ca8ab4294 100644
--- a/framework/Makefile
+++ b/framework/Makefile
@@ -1,3 +1,9 @@
+# Prover Tests are WIP
+# These are the prover tests that have been written
+# and are known to pass
+PROVER_TESTS = demo ol_account slow sacred
+
+VENDOR_TESTS = chain_id guid
 
 # Formal verification of each framework using the Move prover
 prove:
@@ -10,10 +16,16 @@ prove:
 	echo "Testing vendor-stdlib" && \
 	find sources -type f -name "*.move" ! -name "*.spec.move" | sed 's/\.move$$//' | \
 	xargs -I {} sh -c 'echo "Testing file: {}"; diem move prove -f {} || echo "Error in file: {}"'
-	
+
 	@cd libra-framework && \
-	echo "Testing libra-framework" && \
-	find . -type f -name "*.move" ! -name "*.spec.move" -print0 | \
-	awk -v RS='\0' -v ORS='\0' '{sub(/^\.\//,""); print}' | \
-	sort -uz | \
-	xargs -0 -I {} sh -c 'echo "Testing file: {}"; diem move prove -f {} || echo "Error in file: {}"' 
\ No newline at end of file
+	for i in ${PROVER_TESTS} ${VENDOR_TESTS}; do \
+			diem move prove -f $$i; \
+	done
+
+#TODO: automate libra-framework verification once we have identified and fixed specifications	
+# @cd libra-framework && \
+# echo "Testing libra-framework" && \
+# find . -type f -name "*.move" ! -name "*.spec.move" -print0 | \
+# awk -v RS='\0' -v ORS='\0' '{sub(/^\.\//,""); print}' | \
+# sort -uz | \
+# xargs -0 -I {} sh -c 'echo "Testing file: {}"; diem move prove -f {} || echo "Error in file: {}"' 
\ No newline at end of file
diff --git a/framework/libra-framework/sources/ol_sources/slow_wallet.move b/framework/libra-framework/sources/ol_sources/slow_wallet.move
index 70559cdce..96fa64f6f 100644
--- a/framework/libra-framework/sources/ol_sources/slow_wallet.move
+++ b/framework/libra-framework/sources/ol_sources/slow_wallet.move
@@ -135,7 +135,7 @@ module ol_framework::slow_wallet {
       let list = get_slow_list();
       let len = vector::length<address>(&list);
       if (len == 0) return (false, 0);
-      let accounts_updated = 0;
+      let accounts_updated: u64 = 0;
       let i = 0;
       while (i < len) {
         let addr = vector::borrow<address>(&list, i);
@@ -159,6 +159,10 @@ module ol_framework::slow_wallet {
 
         // it may be that some accounts were not updated, so we can't report
         // success unless that was the case.
+        spec {
+          assume accounts_updated + 1 < MAX_U64;
+        };
+
         accounts_updated = accounts_updated + 1;
 
         i = i + 1;
diff --git a/framework/libra-framework/sources/ol_sources/slow_wallet.spec.move b/framework/libra-framework/sources/ol_sources/slow_wallet.spec.move
index aef366e0c..78b9b24d4 100644
--- a/framework/libra-framework/sources/ol_sources/slow_wallet.spec.move
+++ b/framework/libra-framework/sources/ol_sources/slow_wallet.spec.move
@@ -19,6 +19,7 @@ spec ol_framework::slow_wallet {
 
         aborts_if !exists<SacredCow<SlowDrip>>(@0x2);
 
-        aborts_if borrow_global<SacredCow<SlowDrip>>(@0x2).value != 30000 * 1000000;
+        aborts_if borrow_global<SacredCow<SlowDrip>>(@0x2).value != 35000 * 1000000;
+
     }
 }