Proof (Invariant): <totalIssuance> being the sum of balances in the state

[ehildenb]

After #54, let's write a simple high-level property of the set-balance.md module which proves the invariant that the <totalIssuance> remains the sum of the balances in the account storage.

[ehildenb]

    rule 
      <set-balance> 
        <k> ANY_ACTION:EntryAction => . ... </k> 
        <now> _ => _ </now> 
        <events> _ => _ </events> 
        <return-value> _ => _ </return-value> 
        <call-stack> _ => _ </call-stack> 
        <existentialDeposit> _ </existentialDeposit> 
        <creationFee> _ </creationFee> 
        <transferFee> _ </transferFee> 
        <totalIssuance> TOTAL_ISSUANCE => TOTAL_ISSUANCE' </totalIssuance> 
        <accountList> ACCOUNT_LIST => ACCOUNT_LIST' </accountList>
        <accounts> ACCOUNTS => ACCOUNTS' </accounts>
      </set-balance> 
      requires accountsValid(ACCOUNT_LIST, ACCOUNTS)
       andBool accountsValid(ACCOUNT_LIST', ACCOUNTS')
       andBool sumBalances(ACCOUNT_LIST) ==Int TOTAL_ISSUANCE
       andBool sumBalances(ACCOUNT_LIST') ==Int TOTAL_ISSUANCE'

• Added <accountList> as convenience for proving.
• Added subsort EntryAction < Action which will be decided by Define which entrypoints are interesting for high-level properties/invariants #54.
• Added accountsValid which asserts that the <accountList> and <accounts> cell stay in sync.
• Added sumBalances which is used to state the property that TOTAL_ISSUANCE remains correct.