Proof (Invariant): EntryAction does not allow balances between 0 and <existentialDeposit>

[ehildenb]

Sketch:

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

• Subsort EntryAction
• Function nonDustBalances which cycles through the accounts and checks their respective balances and verifies that they are not dusty (either they are 0 or they are > EXISTENTIAL_DEPOSIT)