Problems reusing proofs proven by contract_induction
Closed this issue · 9 comments
In ConCert the contract_induction lemma lets us prove statements of the form
forall bstate caddr (trace : ChainTrace empty_state bstate),
env_contracts bstate caddr = Some (contract : WeakContract) ->
exists dep cstate inc_calls,
deployment_info Setup trace caddr = Some dep /\
contract_state bstate caddr = Some cstate /\
incoming_calls Msg trace caddr = Some inc_calls /\
P (chain_height bstate)
(current_slot bstate)
(finalized_height bstate)
caddr
dep
cstate
(env_account_balances bstate caddr)
(outgoing_acts bstate caddr)
inc_calls
(outgoing_txs trace caddr).
However it is not always possible to reuse proofs on this form inside another proof proven by contract_induction. Let's say that I have already proven a lemma for some property Q which was proved using contract_induction and to prove the property P above I need the information in Q, since I have already proven Q I would like to simply apply that lemma in my proof however to apply I will need to know
reachable bstate /\
env_contracts bstate caddr = Some (contract : WeakContract) /\
deployment_info Setup trace caddr = Some dep /\
contract_state bstate caddr = Some cstate /\
incoming_calls Msg trace caddr = Some inc_calls /\
This information is not available in the goals that are produced by contract_induction so you cannot apply the lemma for Q.
As far as I can tell the CallFacts, DeployFacts and AddBlockFacts used in contract_induction were intended for this purpose and it is possible to use e.g. CallFacts if Q only need cstate. However these facts cannot be used in general to introduce any lemma in this format since none of the facts gives you both cstate, dep, inc_calls and bstate at the same time.
So if contract_induction should allow reuse of proofs it either need to change how the facts work or give the needed information in the goals produced.
@jakobbotsch did you ever run into this?
@4ever2 Could you state your suggested form (or forms) for an improved contract induction?
What would the statement look like?
In addition to what Bas said, do you have an example where this ends up being a problem?
It's been a while, so I don't exactly remember how the proof of this principle goes through, and I don't know if we can allow the other goals access to that information.
however to apply I will need to know
env_contracts bstate caddr = Some (contract : WeakContract) /\ deployment_info Setup trace caddr = Some dep /\ contract_state bstate caddr = Some cstate /\ incoming_calls Msg trace caddr = Some inc_calls /\
Will you? The precondition of the statement is weaker than what you put here, it shows existence and that P holds, not that P holds under that precondition. It probably means you will not be able to connect parts of the statement to the goal you are proving, but only the parts that the particular goal is not depending on anyway.
I could be wrong -- an example would be good. I remember having to expand some of the information at one point to be able to apply this lemma below:
ConCert/execution/examples/Escrow.v
Lines 146 to 152 in daae096
@jakobbotsch did you ever run into this?
Only to a certain degree, see the example in the link above.
@jakobbotsch You are right to apply the lemma I only need to know that the ChainState is reachable and there is a contract deployed in it under the address.
I don't have any specific examples, and I am not entirely sure if it is a problem. My main worry was that it was not possible to reuse any proofs about deploy_info or inc_calls because no goals give sufficient information to connect that part of the statements to the goal. However as you pointed out none of the goals really depend on deploy_info or inc_calls so maybe it is not a problem since you would never need to use a lemma stating something about deploy_info or inc_calls.
@spitters @jakobbotsch
I now have a concrete example where a useful lemma cannot be used in contract_induction.
Lemma contract_balance_bound : forall bstate caddr (trace : ChainTrace empty_state bstate),
let effective_balance := (env_account_balances bstate caddr -
(sumZ (fun act => act_body_amount act) (outgoing_acts bstate caddr)))%Z in
env_contracts bstate caddr = Some (contract : WeakContract) ->
exists cstate,
contract_state bstate caddr = Some cstate
/\ (P cstate -> effective_balance = 0).While proving the non-recursive call goal in contract_induction there will be some entrypoint which will produce a transfer action transfering the entire contract balance to another address which means that we have to prove that
(ctx_contract_balance ctx - (ctx_contract_balance ctx + sumZ (fun act : ActionBody => act_body_amount act) prev_out_queue))%Z = 0%Z, i.e. sumZ (fun act : ActionBody => act_body_amount act) prev_out_queue = 0%Z.
I have already proved Q cstate -> outgoing_acts bstate caddr = [] in another lemma, this would be enough to prove above however it is not possible to instantiate CallFacts with this because outgoing acts not is an input to CallFacts, it is also not possible to apply the lemma directly where needed.
I have opened a pull request #111 with my suggested change. The change does not break any proofs or require changing the contract_induction lemma proof and allows proving the above example.
I think it's reasonable to add outgoing_actions to CallFacts.
I have a general comment, however. contract_induction is an induction principle that helps to organise proofs and give some convenience. Of course, it might be not general enough (which is, to some extent is its purpose), and adding missing things to it might be a good idea. We just should be careful that we don't make it too general, defeating the purpose of making a convenient induction principle.
PS: I think the title of the issue is a bit confusing. At first, I thought that lemmas proved by contract_induction cannot be used in some cases, but this depends on how you stated these lemmas. It seems the problem is that contract_induction is not general enough for certain cases and generates goals that does not allow for using other lemmas.