Open ehildenb opened 4 years ago
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'
<accountList>
as convenience for proving.EntryAction < Action
which will be decided by #54.accountsValid
which asserts that the <accountList>
and <accounts>
cell stay in sync.sumBalances
which is used to state the property that TOTAL_ISSUANCE
remains correct.
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.