What properties do we want to verify about set_free_balance?

[ehildenb]

An initial attempt at high-level description of properties is developed here: https://github.com/runtimeverification/polkadot-verification/pull/15/files

Going to merge it if it builds correctly, but let's discuss if these properties make sense, and if they are likely to be true.

We may be able to define a refinement relation between this simple configuration and the KWasm configuration (which would encode things like the heap-folding/unfolding), which would mean we can use KEQ to facilitate verifying the high-level stated transitions over the low-level Wasm executions. @daejunpark, do you think it's possible?

[daejunpark]

Yes, it should be possible once we have a refinement relation between two configurations.

[ehildenb]

As pointed out in #19 (comment), we need to check whether the side condition 0 <Int RESERVED_BALANCE in account-reaped rule actually should be EXISTENTIAL_DEPOSIT <Int RESERVED_BALANCE.

[ehildenb]

It looks to me that comparing with 0 is what the code does, not comparing with EXISTENTIAL_DEPOSIT.

set_free_balance calls on_free_too_low, which looks like this:

    /// Account's free balance has dropped below existential deposit. Kill its
    /// free side and the account completely if its reserved size is already dead.
    ///
    /// Will maintain total issuance.
    fn on_free_too_low(who: &T::AccountId) {
        let dust = <FreeBalance<T, I>>::take(who);
        <Locks<T, I>>::remove(who);

        // underflow should never happen, but if it does, there's not much we can do about it.
        if !dust.is_zero() {
            T::DustRemoval::on_unbalanced(NegativeImbalance::new(dust));
        }  

        T::OnFreeBalanceZero::on_free_balance_zero(who);

        if Self::reserved_balance(who).is_zero() {
            Self::reap_account(who);
        }
    }

which calls _.is_zero(), which is defined:

core/sr-primitives/src/lib.rs:  pub fn is_zero(&self) -> bool { self.0 == 0 }

[ehildenb]

We have ironed out the set_free_balance properties, so I'm closing this.