mirror of
https://github.com/Instadapp/aave-protocol-v2.git
synced 2024-07-29 21:47:30 +00:00
67 lines
2.3 KiB
Ruby
67 lines
2.3 KiB
Ruby
methods {
|
|
setBorrowing(uint256, bool) envfree
|
|
setUsingAsCollateral(uint256, bool) envfree
|
|
isUsingAsCollateralOrBorrowing(uint256) returns bool envfree
|
|
isBorrowing(uint256) returns bool envfree
|
|
isUsingAsCollateral(uint256) returns bool envfree
|
|
isBorrowingAny() returns bool envfree
|
|
isEmpty() returns bool envfree
|
|
}
|
|
|
|
invariant empty(uint256 reserveIndex)
|
|
isEmpty() => !isBorrowingAny() && !isUsingAsCollateralOrBorrowing(reserveIndex)
|
|
|
|
invariant notEmpty(uint256 reserveIndex)
|
|
(isBorrowingAny() || isUsingAsCollateral(reserveIndex)) => !isEmpty()
|
|
|
|
|
|
invariant borrowing(uint256 reserveIndex )
|
|
isBorrowing(reserveIndex) => isBorrowingAny()
|
|
|
|
invariant collateralOrBorrowing(uint256 reserveIndex )
|
|
(isUsingAsCollateral(reserveIndex) || isBorrowing(reserveIndex)) <=> isUsingAsCollateralOrBorrowing(reserveIndex)
|
|
|
|
|
|
|
|
rule setBorrowing(uint256 reserveIndex, bool borrowing)
|
|
{
|
|
require reserveIndex < 128;
|
|
|
|
setBorrowing(reserveIndex, borrowing);
|
|
assert isBorrowing(reserveIndex) == borrowing, "unexpected result";
|
|
}
|
|
|
|
rule setBorrowingNoChangeToOther(uint256 reserveIndex, uint256 reserveIndexOther, bool borrowing)
|
|
{
|
|
require reserveIndexOther != reserveIndex;
|
|
require reserveIndexOther < 128 && reserveIndex < 128;
|
|
bool otherReserveBorrowing = isBorrowing(reserveIndexOther);
|
|
bool otherReserveCollateral = isUsingAsCollateral(reserveIndexOther);
|
|
|
|
setBorrowing(reserveIndex, borrowing);
|
|
assert otherReserveBorrowing == isBorrowing(reserveIndexOther) &&
|
|
otherReserveCollateral == isUsingAsCollateral(reserveIndexOther), "changed to other reserve";
|
|
}
|
|
|
|
|
|
rule setUsingAsCollateral(uint256 reserveIndex, bool usingAsCollateral)
|
|
{
|
|
require reserveIndex < 128;
|
|
|
|
setUsingAsCollateral(reserveIndex, usingAsCollateral);
|
|
assert isUsingAsCollateral(reserveIndex) == usingAsCollateral, "unexpected result";
|
|
}
|
|
|
|
|
|
rule setUsingAsCollateralNoChangeToOther(uint256 reserveIndex, uint256 reserveIndexOther, bool usingAsCollateral)
|
|
{
|
|
require reserveIndexOther != reserveIndex;
|
|
require reserveIndexOther < 128 && reserveIndex < 128;
|
|
bool otherReserveBorrowing = isBorrowing(reserveIndexOther);
|
|
bool otherReserveCollateral = isUsingAsCollateral(reserveIndexOther);
|
|
|
|
setUsingAsCollateral(reserveIndex, usingAsCollateral);
|
|
assert otherReserveBorrowing == isBorrowing(reserveIndexOther) &&
|
|
otherReserveCollateral == isUsingAsCollateral(reserveIndexOther), "changed to other reserve";
|
|
}
|