Instadapp/aave-protocol-v2
1
0
Fork 0
mirror of https://github.com/Instadapp/aave-protocol-v2.git synced 2024-07-29 21:47:30 +00:00
Code Issues Packages Projects Releases Wiki Activity

Fix compilation errors

Browse Source
This commit is contained in:
pistiner 2020-12-03 17:20:11 +02:00
parent 1ce83f27af
commit 6b9bed65c4
2 changed files with 40 additions and 40 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

66
specs/UserConfiguration.spec
View File

@ -1,66 +1,66 @@
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
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(address user, uint256 reserveIndex )
isEmpty(user) => !isBorrowingAny(user) && !isUsingAsCollateralOrBorrowing(user, reserveIndex)
invariant empty(uint256 reserveIndex)
isEmpty() => !isBorrowingAny() && !isUsingAsCollateralOrBorrowing(reserveIndex)
invariant notEmpty(address user, uint256 reserveIndex )
( isBorrowingAny(user) || isUsingAsCollateral(user, reserveIndex)) => !isEmpty(user)
invariant notEmpty(uint256 reserveIndex)
(isBorrowingAny() || isUsingAsCollateral(reserveIndex)) => !isEmpty()
invariant borrowing(address user, uint256 reserveIndex )
isBorrowing(user, reserveIndex) => isBorrowingAny(user)
invariant borrowing(uint256 reserveIndex )
isBorrowing(reserveIndex) => isBorrowingAny()
invariant collateralOrBorrowing(address user, uint256 reserveIndex )
( isUsingAsCollateral(user, reserveIndex) || isBorrowing(user, reserveIndex) ) <=> isUsingAsCollateralOrBorrowing(user, reserveIndex)
invariant collateralOrBorrowing(uint256 reserveIndex )
(isUsingAsCollateral(reserveIndex) || isBorrowing(reserveIndex)) <=> isUsingAsCollateralOrBorrowing(reserveIndex)
rule setBorrowing(address user, uint256 reserveIndex, bool borrowing)
rule setBorrowing(uint256 reserveIndex, bool borrowing)
{
require reserveIndex < 128;
setBorrowing(user, reserveIndex, borrowing);
assert isBorrowing(user, reserveIndex) == borrowing, "unexpected result";
setBorrowing(reserveIndex, borrowing);
assert isBorrowing(reserveIndex) == borrowing, "unexpected result";
}
rule setBorrowingNoChangeToOther(address user, uint256 reserveIndex, uint256 reserveIndexOther, bool borrowing)
rule setBorrowingNoChangeToOther(uint256 reserveIndex, uint256 reserveIndexOther, bool borrowing)
{
require reserveIndexOther != reserveIndex;
require reserveIndexOther < 128 && reserveIndex < 128;
bool otherReserveBorrowing = isBorrowing(user, reserveIndexOther);
bool otherReserveCollateral = isUsingAsCollateral(user,reserveIndexOther);
bool otherReserveBorrowing = isBorrowing(reserveIndexOther);
bool otherReserveCollateral = isUsingAsCollateral(reserveIndexOther);
setBorrowing(user, reserveIndex, borrowing);
assert otherReserveBorrowing == isBorrowing(user, reserveIndexOther) &&
otherReserveCollateral == isUsingAsCollateral(user,reserveIndexOther), "changed to other reserve";
setBorrowing(reserveIndex, borrowing);
assert otherReserveBorrowing == isBorrowing(reserveIndexOther) &&
otherReserveCollateral == isUsingAsCollateral(reserveIndexOther), "changed to other reserve";
}
rule setUsingAsCollateral(address user, uint256 reserveIndex, bool usingAsCollateral)
rule setUsingAsCollateral(uint256 reserveIndex, bool usingAsCollateral)
{
require reserveIndex < 128;
setUsingAsCollateral(user, reserveIndex, usingAsCollateral);
assert isUsingAsCollateral(user, reserveIndex) == usingAsCollateral, "unexpected result";
setUsingAsCollateral(reserveIndex, usingAsCollateral);
assert isUsingAsCollateral(reserveIndex) == usingAsCollateral, "unexpected result";
}
rule setUsingAsCollateralNoChangeToOther(address user, uint256 reserveIndex, uint256 reserveIndexOther, bool usingAsCollateral)
rule setUsingAsCollateralNoChangeToOther(uint256 reserveIndex, uint256 reserveIndexOther, bool usingAsCollateral)
{
require reserveIndexOther != reserveIndex;
require reserveIndexOther < 128 && reserveIndex < 128;
bool otherReserveBorrowing = isBorrowing(user, reserveIndexOther);
bool otherReserveCollateral = isUsingAsCollateral(user,reserveIndexOther);
bool otherReserveBorrowing = isBorrowing(reserveIndexOther);
bool otherReserveCollateral = isUsingAsCollateral(reserveIndexOther);
setUsingAsCollateral(user, reserveIndex, usingAsCollateral);
assert otherReserveBorrowing == isBorrowing(user, reserveIndexOther) &&
otherReserveCollateral == isUsingAsCollateral(user,reserveIndexOther), "changed to other reserve";
setUsingAsCollateral(reserveIndex, usingAsCollateral);
assert otherReserveBorrowing == isBorrowing(reserveIndexOther) &&
otherReserveCollateral == isUsingAsCollateral(reserveIndexOther), "changed to other reserve";
}

14
specs/harness/UserConfigurationHarness.sol
View File

@ -2,15 +2,16 @@ pragma solidity 0.6.12;
pragma experimental ABIEncoderV2;
import {UserConfiguration} from '../../contracts/protocol/libraries/configuration/UserConfiguration.sol';
import {DataTypes} from '../../contracts/protocol/libraries/types/DataTypes.sol';
/*
A wrapper contract for calling functions from the library UserConfiguration.
*/
contract UserConfigurationHarness {
DataTypes.UserConfigurationMap internal usersConfig;
function setBorrowing(
address user,
uint256 reserveIndex,
bool borrowing
) public {
@ -18,14 +19,13 @@ contract UserConfigurationHarness {
}
function setUsingAsCollateral(
address user,
uint256 reserveIndex,
bool _usingAsCollateral
) public {
UserConfiguration.setUsingAsCollateral(usersConfig, reserveIndex, _usingAsCollateral);
}
function isUsingAsCollateralOrBorrowing(address user, uint256 reserveIndex)
function isUsingAsCollateralOrBorrowing(uint256 reserveIndex)
public
view
returns (bool)
@ -33,19 +33,19 @@ contract UserConfigurationHarness {
return UserConfiguration.isUsingAsCollateralOrBorrowing(usersConfig, reserveIndex);
}
function isBorrowing(address user, uint256 reserveIndex) public view returns (bool) {
function isBorrowing(uint256 reserveIndex) public view returns (bool) {
return UserConfiguration.isBorrowing(usersConfig, reserveIndex);
}
function isUsingAsCollateral(address user, uint256 reserveIndex) public view returns (bool) {
function isUsingAsCollateral(uint256 reserveIndex) public view returns (bool) {
return UserConfiguration.isUsingAsCollateral(usersConfig, reserveIndex);
}
function isBorrowingAny(address user) public view returns (bool) {
function isBorrowingAny() public view returns (bool) {
return UserConfiguration.isBorrowingAny(usersConfig);
}
function isEmpty(address user) public view returns (bool) {
function isEmpty() public view returns (bool) {
return UserConfiguration.isEmpty(usersConfig);
}