Skip to content

Commit

Permalink
[fix] formal verification ci (0LNetworkCommunity#179)
Browse files Browse the repository at this point in the history
  • Loading branch information
0xzoz authored and 0o-de-lally committed Feb 16, 2024
1 parent 5427b74 commit 727ff1b
Show file tree
Hide file tree
Showing 3 changed files with 25 additions and 8 deletions.
24 changes: 18 additions & 6 deletions framework/Makefile
Original file line number Diff line number Diff line change
@@ -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:
Expand All @@ -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: {}"'
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: {}"'
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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;

}
}

0 comments on commit 727ff1b

Please sign in to comment.