Further automation of data_encoding proofs with CoqHammer

This post is a continuation of the previous blog post on proof automation for the data_encoding proofs.

data_encoding is a library used in the Tezos codebase to define binary and JSON encodings, by using some primitives and then combining these primitives with combinators.

As said in the previous post, we defined a custom tactic for automating data_encoding proofs. These proofs are usually mechanical at the beginning, for each combinator we have a lemma or axiom that verify the outer term and generates a subgoal for each of the inner terms, and for primitives we have axioms to eliminate them. The subgoals remaining are regarding the combinators injections and projections, which are distinct for each encoding.

The data_encoding_auto tactic can eliminate all the combinators and primitives terms, but we still have to finish the last subgoals by hand, at last we did. Now we can use CoqHammer to finish some proofs increasing even more the our level of automation.

Here is a proof using only data_encoding_auto:

Lemma ratio_encoding_is_valid
  : Data_encoding.Valid.t Ratio.Valid.t Constants_repr.ratio_encoding.
  Data_encoding.Valid.data_encoding_auto.
  intros x H; intuition; try apply H.
  destruct H as [numerator [denominator dgt0]].
  assert (x.(Constants_repr.ratio.denominator) >? 0 = true) by lia.
  now rewrite H.
Qed.

And here is a proof using combination of data_encoding_auto and CoqHammer:

Lemma ratio_encoding_is_valid
  : Data_encoding.Valid.t Ratio.Valid.t Constants_repr.ratio_encoding.
  Data_encoding.Valid.data_encoding_auto; scrush.
Qed.

The usual usage of CoqHammer is: you import it with From Hammer Require Import Tactics., this puts best tactic into the scope. Whenever you fell that CoqHammer can solve the current go you fire the best tactic. CoqHammer will try to find multiple solutions for the current subgoal and it will print the best one in the standard output, you then replace the best with the tactic suggested by it, these include sauto, scrush, sfirstorder and much more.

best tactic will try to use the lemmas in the scope to solve the subgoal but you can also parameterize it to use other lemmas, here is another encoding verification example:

Lemma origination_result_list_encoding_is_valid : 
  Data_encoding.Valid.t Valid.t Migration_repr.origination_result_list_encoding.
  Data_encoding.Valid.data_encoding_auto.
  best use: Forall_True.
Qed.

In this case the last subgoal is something like this:

forall x : list Migration_repr.origination_result,
Valid.t x ->
Forall
  (fun v_a : Migration_repr.origination_result =>
  ...

In subgoals like this we usually apply Forall_True lemma and continue the proof of the remaining subgoals. By parameterizing best with use: Forall_True it can finds its way up to the completion of the proof. Also, CoqHammer can help us with other proofs not involving data_encoding as this is a generic automation mechanism for Coq.

Automation is important not only because it boosts our productivity but also because it generalizes the proofs so that they become easier to maintain and more robust to changes in the code.