Consider re-writing private state as internal to allow invariants over private state

[cd1m0]

As described in #163 we changed the scribble type-checker to reject annotations that talk about private state variables of base contracts. So for example it would reject samples such as this:

contract Base {
    uint private x;
}

contract Child is Base {
     /// if_succeeds x == 42;
     function foo() public {}
}

One common case where this occurs is a token contract inheriting from https://github.com/OpenZeppelin's ERC20 contract. A lot of invariants that talk about ERC20's private state (e.g. _balances, _totalSupply, _approvals) can be re-phrased using the ERC20's public getters (e.g. balanceOf(), totalSupply(), allowance()). However some invariants do require talking about the underlying state (e.g. talking about the sum of balances - unchecked_sum(_balances)).

This issue is here to track user demand for talking about private state. With cases of invariants that cannot be expressed without private state, we will reconsider scribble re-writing private state as internal.

We didn't immediately go with re-writing private state as internal, as in some cases that may create code that doesnt compile. Specifically when a child contract has a state variable with the same name as a private state variable of the parent contract, re-writing the parent contract's state variable to internal will cause a compilation error.