TON Masterchain Contracts Formal Verification

The function `process_new_stake` has a test that the submitted stake is larger than `min_stake`. ```func if (msg_value < min_stake) { ;; stake too small, return it return return_stake(s_addr, query_id, 5); } ``` However, nothing prevents a user from submitting a bid larger that `max_stake`. The function `try_elect` will then restrict the bid to be less than `max_stake`: ```func var (stake, _, pubkey) = (min(key~load_uint(128), max_stake), key~load_uint(32), key.preload_uint(256)); ``` If the user submitted more than `max_stake`, then at this point the contract will forget about the excess part, which will become unretrievably locked in the contract balance. Note that `max_stake` is a configuration parameter which can be changed at any time by the owner of the config contract. This makes the situation potentially more error prone, because such a change could happen between the user's bid submission and the next election. So if the limit was lowered, the user could submit a bid which was valid at the time time of submission but triggered this bug at the time of election.

The `conduct_elections` function computes the next validator set and then stores it in the `past_elect` dictionary. The key it is stored under is the `elect_at` field, the time at which the election takes place. If there somehow was already a past validator set stored under the same key, the past set would be overwritten and all the stakes in it lost. The `elect_at` field is chosen in `announce_new_elections` to be a time in the future (`now() + elect_begin_before`), so intuitively it will be distinct from other election times in the past. However, there is some extra logic that can move it to a slightly earlier time ("pretend that the elections started at t0"). Exactly which time `t0` would be depends on configuration parameters which are set and changed outside the elector contract, which makes it hard to formally prove that there can never be a clash. The likelihood of this going wrong may seem remote, but another check would make the contract more self-contained.

There are two cases in the elector contract when it sends a message and includes approximately 1 Gram of value in order to pay for the message processing costs. These are in `process_new_stake` (the call to `send_confirmation`) and in `conduct_elections` (the call to `send_validator_set_to_config`). In `process_new_stake` this cost is deducted from the posted stake, so that the accounting is correct: ```func msg_value -= 1000000000; ;; deduct GR$1 for sending confirmation ``` However, there is no logic in `conduct_elections` which explains where the value of the message should be deducted from, which breaks the invariant that data structures reflect the current balance of the contract.

The function `announce_new_elections` takes an argument `elect` despite declaring a local variable with the same name which is used in the function body. The argument is redundant.