Skip to main content

Some refactoring, some profiling and some optimization

· 6 min read
Natasha Klaus

During our work on verification of Tezos source code, we faced a problem: some proofs were taking too long time to execute. For example, function which proves equality of parse_ty_aux and dep_parse_ty_aux was executing about 5 minutes, according to CI (Not acceptable! We couldn't even merge this proof!).

For the information why we actually needed to prove the equality of parse_ty_aux and dep_parse_ty_aux, and why we had to create a function-simulation dep_parse_ty_aux, please check this article: Simulations - dependently-typed version

What is the reason of such a long execution period? First of all the length of original parse_ty_aux is about 500 lines of code. So the term itself is rather big, and each step of its reduction is a time-taking procedure.

Many other functions that also need to be verified are even longer, for example the Fixpoint parse_data_aux is having 4932 lines of code. Therefore, it is very important that the proofs for such a long functions are optimized.

One-step reduction​

From the very beginning of the proof building it became obvious that big numbers used in both functions may be the essence of the problem:

in dep_parse_ty we have 10 000 in nat - natural numbers,

fuel <= 10 000

and in parse_ty_aux we have same big number in Z - integers represented in a binary way

stack_depth <= 10 000

Tactics like simpl, cbn, cbv, unfold would reduce as much as they can, trying to simplify 10 000, so we had to force Coq to perform just one-step reduction in many cases.

Ways of one-step reduction we used:

  • limitation of tactic unfold by giving it a precise string reference
unfold "let? _ := _ in _"
  • building a special-case tactics for each piece of code, for example tactic simpl can be forced to work only in the very precise area:
| |- context [match ?e with _ => _ end] =>
          match e with
          | Script_typed_ir.Type_size.(Script_typed_ir.TYPE_SIZE.compound1) _ _ =>
              simpl e
          end
  • simpl, cbn, cbv are customizable, for some of them debugging info can be printed

Execution time​

To find out what are the most expensive parts of our code, we also used the command Time, which executes sentence and displays the time needed to execute it.

Command Time helped us a lot in picking the right order for tactics application. For example tactic lia should go after all the simpler tactics, like reflexivity and others. The reason is the next: tactic lia works slowly, it tries many variants on the same goal, while reflexivity either solves or reports inability to resolve goals faster. So in the sequence of the tactics, we should suggest reflexivity to solve all it can, and all remaining goals we should give lia.

Changing order of these tactics on the bunch of goals can notably accelerate calculations:

 try lia; try reflexivity   (** not recommended*)
 
 try reflexivity; try lia   (** recommended *)

Also, we had to get rid of such tactics as easy in some sequences of tactics, and replace easy by the more simpl and precise tactics, consider this example below: p is the node.Prim, when we destruct it, we receive more than 150 subgoals.

This code takes 53.2 seconds:

Time (destruct p eqn:TP;
       simpl; try reflexivity; destruct l0 eqn:L0; simpl; try easy;
       destruct Script_ir_annot.check_type_annot eqn:CTA; simpl;
       try easy).

This code takes 6.3 seconds! Quite a difference! Here try easy replaced with try (split; reflexivity): 

Time (destruct p eqn:TP;
      simpl; try reflexivity; destruct l0 eqn:L0; simpl; try (split; reflexivity);
      destruct Script_ir_annot.check_type_annot eqn:CTA; simpl;
      try (split; reflexivity)).

Replacing 10000 to 10 and calculating execution time​

After all the manipulations described above, it was not clear what was causing the slow work of prover. We were thinking that one-step reduction applied to all problem areas should have solved the problem with large numbers. But still the numbers 10000 and 10001 were on the list of suspects, it was too early to delete them. We will not describe here who from this list turned out to be innocent, instead, we will tell you how we managed to catch the criminal red-handed.

We replaced 10000 and 10001 in dep_parse_ty_aux from Simulations folder and in parse_ty_aux from Proto_alpha everywhere they occured with 10 and 11 respectively. When we measured time of updated equality proof, difference was the next: 5 minutes versus 1 minute. Experiment has shown that the speed of calculations accelerated by 5 times.

Opaque and Transparent​

We can make our numbers Opaque, this will prevent them from unfolding and simplifying, see the code below:

Definition number_10001 : Z.t := 10001.
Opaque number_10001.

Definition number_10000 : Z.t := 10000.
Opaque number_10000.

And if we need them to be transparent (we do in many cases, we actually use these numbers in calculations), we can make them transparent before usage, like this:

Transparent number_10001.

In the code we have several such number definitions (all required for calculations)

Definition number_10001 : Z.t := 10001.
Opaque number_10001.

Definition number_10000 : Z.t := 10000.
Opaque number_10000.

Definition nat_number_10001 : nat := 10001.
Opaque nat_number_10001.

Definition nat_number_10000 : nat := 10000.
Opaque nat_number_10000.

Definition positive_number_10001 : positive := 10001.
Opaque positive_number_10001.

Definition positive_number_10000 : positive := 10000.
Opaque positive_number_10000.

We also need to switch between them inside proof (make transparent / make opaque), and this is getting tiresome. But we are lucky, because we are dealing with Coq. In the example below, with_strategy will make all our opaque numbers transparent just for lia tactic where we need it.

Ltac tr_lia := with_strategy transparent
      [nat_number_10000
       nat_number_10001
       number_10000
       number_10001
       positive_number_10000
       positive_number_10001] lia.

"This can be useful for guarding calls to reduction in tactic automation to ensure that certain constants are never unfolded by tactics like simpl and cbn or to ensure that unfolding does not fail..." says the coq reference manual. Exactly what we need!

Here are some particularly notable results: without Opaque solution, this line of code below (which calls quite voluminous tactic basic), works 2 minutes:

all : repeat (basic Y' parse_ty_aux_dep_parse_ty_aux_eq).

With Opaque solution this line works 2 seconds!

We are, of course, very satisfied with the result. That was educational. Thanks for reading!