system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
#### totalSupply

Total supply of tokens. It represents the maximum number of tokens that is allowed to exist.

``` js
function totalSupply() public view returns (uint256 allowed)
```
assistant
/// @notice postcondition  _totalSupply == allowed
function totalSupply() public view returns (uint256 allowed);