-
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