it's short (~160 lines and only ~100 lines if you exclude declaration code)
it involves reasoning over maps which has historically been tricky for us
there are 6 entrypoints, 3 of which don't produce any callbacks and only update internal state and 3 of which don't update any internal state and send a single callback with a value
because callbacks here are typed, from what I can tell, you cannot pass an entrypoint of this contract as a callback to itself
the contract authorizes transactions by the immediate sender, not by source address that was responsible for initiating the call that led to this contract being called
Aside from functional correctness properties, what other properties do want to prove? Some thoughts:
the variable total_supply should always be equal to Σₐ tokenHolderBalance[a] for each address a
the only way to change the balance of an account is to either:
call transfer from account a to some account b with a != b
call mintOrBurn with target account a with quantity != 0 and tokenHolderBalance[a] + quantity >= 0
Here are some initial thoughts:
Aside from functional correctness properties, what other properties do want to prove? Some thoughts:
total_supplyshould always be equal toΣₐ tokenHolderBalance[a]for each addressatransferfrom accountato some accountbwitha != bmintOrBurnwith target accountawithquantity != 0andtokenHolderBalance[a] + quantity >= 0