Accelerate some lemmas in rabbitmq proof

[euclidgame]

This PR tries to accelerate some time-consuming lemmas in the proof of rabbitmq controller. The approaches and observations are as follows:

• Break down the proof into multiple methods. Suppose we have a lemma_a which runs for $n$ seconds. We can move part of it into a new lemma lemma_b and call lemma_b inside lemma_a. Then lemma_a and lemma_b run for $n'$ and $m$ seconds separately. The interesting thing is that usually $n'+m < n$.
• Make the lemma simpler. We tend to carry multiple things using one lemma (one spec in most cases) if they can be easily proved together. However, sometimes this makes things worse. We can first prove the part that is independent of the rest and get a simpler lemma first. This lemma can be an illustration.
• Try to reduce the possible instantiations of each universal quantifiers. When proving a lemma, we use other lemmas to assist. If the lemmas to help contain universal quantifiers, we have weaken their domains to those we actually use (sometimes remove the quantifiers). Here is an example.
• Take care of the assertions and their ordering. We used to think adding more assertions would help to remind the verifier of some predicates and then make verification faster. But it poses more burden sometimes. And the order of assertions also makes a difference. About the assertions here, I swap the two assertions or change them into

assert(local_step.is_AfterKRequestStep() && local_step.get_AfterKRequestStep_0() == ActionKind::Get);
assert(local_step_prime.is_AfterKRequestStep() && local_step_prime.get_AfterKRequestStep_0() == ActionKind::Update);

or

assert(local_step.is_AfterKRequestStep());
assert(local_step_prime.is_AfterKRequestStep());

, then the time is (greatly) increased. (I don't really know why).

[marshtompsxd]

@euclidgame could you document how you improve the verification time in the description?

[tianyin]

Good point. I think it can even be something to report in the paper.

[tianyin]

The summary is fantastic! Good job @euclidgame

Could you also give some quantitative numbers so we know how much time each effort saves?

[euclidgame]

@tianyin , I am not sure how to do it. In my view, the saved time is more related to the concrete lemmas rather than the approach (effort) type. Can you elaborate on what you want?

What I can get is the running time of each lemma and the total verification time before and after this PR.

[tianyin]

What I can get is the running time of each lemma and the total verification time before and after this PR.

Yes. That's exactly what I was hoping to see! :)

[marshtompsxd]

@euclidgame Do you have more commits to push? Otherwise I will merge it