Lending contracts having state invariants depending on call stack.

lending.sol

// Simple lending contract demostrating complex call-stack
// dependant state invariants.
// @author Remco Bloemen <remco@0xproject.com>

pragma solidity ^0.4.25;

// Simple non-reentrant version. (Or actually, the innermost call is responsible for paying back everyone.)
contract Lending1 {
    
    constructor () public payable {
        require(address(this).balance == 100 ether);
    }
    
    function borrowAndCall(uint256 amount, address target) public {
        require(target.call.value(amount)(), "Call failed");
        require(address(this).balance == 100 ether, "Did not pay back loan");
    }
    
    function checkBalance() public view {
        // TODO: Proof that this assertion never fails unless re-entrantly
        //       called through `borrowAndCall`
        assert(address(this).balance == 100 ether);
    }
}

// Strict reentrant version. Every call needs to repay its loan.
contract Lending2 {
  
    constructor () public payable {
        require(address(this).balance == 100 ether);
    }
    
    function borrowAndCall(uint256 amount, address target) public {
        uint256 before = address(this).balance;
        require(target.call.value(amount)(), "Call failed");
        require(address(this).balance == before, "Did not pay back loan");
    }
    
    function checkBalance() public view {
        // TODO: Proof that this assertion never fails unless re-entrantly
        //       called through `borrowAndCall`
        assert(address(this).balance == 100 ether);
    }
}

// Nonstrict reentrant version. Outermost call needs to repay remainder.
contract Lending3 {
  
    uint256 internal depth;
    
    constructor () public payable {
        require(address(this).balance == 100 ether);
        depth = 0;
    }
    
    function borrowAndCall(uint256 amount, address target) public {
        ++depth;
        require(target.call.value(amount)(), "Call failed");
        --depth;
        if (depth == 0) {
            require(
              address(this).balance == 100 ether,
              "Did not pay back loan");
        }
    }
    
    function checkBalance() public view {
        // TODO: Proof that this assertion never fails unless re-entrantly
        //       called through `borrowAndCall`
        assert(address(this).balance == 100 ether);
    }
}


// Bug 1: The contracts actually do not accept repayments.
// Solution: Add this fallback function
//
//    function() public payable { } 
//
// Bug 2: If the fallback is called on its own with payment,
//        the contract balance exceeds 100 ether and `checkBalance` will fail. // Solution: 
//
//    function() public payable {
//        require(address(this).balance <= 100 ether, "No donations accepted.");
//    } 
//
// Bug 3: Contract can still receive donations by forcing a selfdestruct payment
//        making the assertion in `checkBalance` fail.
// Solution: Change the assertion in `checkBalance` to exclude forced payments,
//           but how?
//