aave-protocol-v2/specs/UserConfiguration.spec
2020-10-15 00:59:12 +03:00

67 lines
2.6 KiB
Ruby

methods {
setBorrowing(address, uint256, bool) envfree
setUsingAsCollateral(address, uint256, bool) envfree
isUsingAsCollateralOrBorrowing(address, uint256) returns bool envfree
isBorrowing(address, uint256) returns bool envfree
isUsingAsCollateral(address, uint256) returns bool envfree
isBorrowingAny(address ) returns bool envfree
isEmpty(address ) returns bool envfree
}
invariant empty(address user, uint256 reserveIndex )
isEmpty(user) => !isBorrowingAny(user) && !isUsingAsCollateralOrBorrowing(user, reserveIndex)
invariant notEmpty(address user, uint256 reserveIndex )
( isBorrowingAny(user) || isUsingAsCollateral(user, reserveIndex)) => !isEmpty(user)
invariant borrowing(address user, uint256 reserveIndex )
isBorrowing(user, reserveIndex) => isBorrowingAny(user)
invariant collateralOrBorrowing(address user, uint256 reserveIndex )
( isUsingAsCollateral(user, reserveIndex) || isBorrowing(user, reserveIndex) ) <=> isUsingAsCollateralOrBorrowing(user, reserveIndex)
rule setBorrowing(address user, uint256 reserveIndex, bool borrowing)
{
require reserveIndex < 128;
setBorrowing(user, reserveIndex, borrowing);
assert isBorrowing(user, reserveIndex) == borrowing, "unexpected result";
}
rule setBorrowingNoChangeToOther(address user, uint256 reserveIndex, uint256 reserveIndexOther, bool borrowing)
{
require reserveIndexOther != reserveIndex;
require reserveIndexOther < 128 && reserveIndex < 128;
bool otherReserveBorrowing = isBorrowing(user, reserveIndexOther);
bool otherReserveCollateral = isUsingAsCollateral(user,reserveIndexOther);
setBorrowing(user, reserveIndex, borrowing);
assert otherReserveBorrowing == isBorrowing(user, reserveIndexOther) &&
otherReserveCollateral == isUsingAsCollateral(user,reserveIndexOther), "changed to other reserve";
}
rule setUsingAsCollateral(address user, uint256 reserveIndex, bool usingAsCollateral)
{
require reserveIndex < 128;
setUsingAsCollateral(user, reserveIndex, usingAsCollateral);
assert isUsingAsCollateral(user, reserveIndex) == usingAsCollateral, "unexpected result";
}
rule setUsingAsCollateralNoChangeToOther(address user, uint256 reserveIndex, uint256 reserveIndexOther, bool usingAsCollateral)
{
require reserveIndexOther != reserveIndex;
require reserveIndexOther < 128 && reserveIndex < 128;
bool otherReserveBorrowing = isBorrowing(user, reserveIndexOther);
bool otherReserveCollateral = isUsingAsCollateral(user,reserveIndexOther);
setUsingAsCollateral(user, reserveIndex, usingAsCollateral);
assert otherReserveBorrowing == isBorrowing(user, reserveIndexOther) &&
otherReserveCollateral == isUsingAsCollateral(user,reserveIndexOther), "changed to other reserve";
}