• Jakob Botsch Nielsen's avatar
    Prove a property for the Congress contract · 1b1c9908
    Jakob Botsch Nielsen authored
    This proves a concrete property about any Congress contract deployed to
    a blockchain. More specifically, we show that the count of transactions
    sent out by any Congress contract will always be less than or equal to
    the total number of actions it has receive in "create proposal"
    messages.
    Thus, this property is stated only over the transactions going in and
    out to the Congress contract.
    To prove this, we reason over incoming and outgoing transactions, the
    internal state of the congress and also the actions in the blockchain
    queue.
    1b1c9908
LocalBlockchain.v 18.5 KB