Stream: Coq users

Topic: Reducing kernel verification time


view this post on Zulip Benjamin Bonneau (Jul 10 2023 at 15:00):

Hello,
I have a (rather complex) tactic (ltac1) that solves automatically some goal of interest (a kind of program refinement). I managed to have the tactic run in an acceptable time but the kernel takes significantly more time to check the generated proof term (on some instance the tactic runs in 1.2s and the kernel in 5s).
I do not know if I can hope to improve this, I don't know how to retrieve useful informations about what the kernel is doing.
Currently I only have access to:

Would there be other way to figure out what the kernel is doing ? For instance I know that the proof term is quadratic in the size of the program I consider (but I think that the tactics still do a linear work because the quadratic part comes from duplicated terms which are seen as evars by the tactics). I expect this part to be easily type checkable but I do not know if it is really the case or if the long verification time comes from this part.
I though that having some informations like the number of reduction performed in the conversions could be useful.
I know that guard checking can be quite long but only a few simple fix operators are visible in the proof term (but again there are ellipses).
I found this thread that suggest a way to debug the kernel, could something like this be useful here ?
Also I had a few questions about the kernel and reduction:

Finally I noticed that cbn generates a cast in the proof term ?proof : original_goal, not generating this cast at some points (using eval and change) improved the kernel checking time (by almost 20% on some examples). So if there are other simple tricks like this I would be happy to try them :)

view this post on Zulip Janno (Jul 10 2023 at 15:33):

I'll try to answer some of the easier questions:

view this post on Zulip Michael Soegtrop (Jul 10 2023 at 15:35):

There is a lengthy thread on the topic with various good hints which might also be helpful:

https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/How.20to.20Debug.20slow.20QED.3F

view this post on Zulip Benjamin Bonneau (Jul 10 2023 at 17:14):

Janno said:

This does not seems to work in Coqtail but I it works when calling coqc :+1: .

I rechecked my exemples and it seems that it indeed only influence the time of cbn.

view this post on Zulip Gaëtan Gilbert (Jul 10 2023 at 17:14):

I there any kind of sharing in the kernel ? For instance if an evar occurs several times, is it (the term it is unified to) type checked multiple times ?

Yes it gets checked multiple times

Except for the conversions and guards, is the kernel checking linear in the size of the proof term ?

I think so (meaning size without considering sharing)

view this post on Zulip Gaëtan Gilbert (Jul 10 2023 at 17:16):

you can use Time around a command (eg Time Qed.) or coqc -time to get more precise timings, although Time Qed can be missing some of the time (it is the time spent preparing the data to be sent to the kernel, which involves a few term traversals)

view this post on Zulip Wolf Honore (Jul 10 2023 at 17:33):

This does not seems to work in Coqtail

I haven't looked into it much but I expect it's the same issue as https://github.com/coq/coq/issues/13971

view this post on Zulip Emilio Jesús Gallego Arias (Jul 10 2023 at 17:54):

@Wolf Honore do you render Pp.t -> string in Coqtail? If not that's a separate issue from the one in CoqIDE.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 10 2023 at 17:57):

So there are likely 2 issues, depending where the rendering of Coq's pretty printing type happens:

view this post on Zulip Emilio Jesús Gallego Arias (Jul 10 2023 at 18:08):

https://github.com/coq/coq/pull/17840 should fix this problem for VsCoq 1 and Coqtail if my interpretation is correct

view this post on Zulip Wolf Honore (Jul 10 2023 at 18:53):

You may be right @Emilio Jesús Gallego Arias, I'll try to look more closely when I have time

view this post on Zulip Benjamin Bonneau (Jul 13 2023 at 08:52):

Gaëtan Gilbert said:

you can use Time around a command (eg Time Qed.) or coqc -time to get more precise timings, although Time Qed can be missing some of the time (it is the time spent preparing the data to be sent to the kernel, which involves a few term traversals)

I tried using Time Qed on my exemple . It gives me a smaller time than what I was calculating using time coqc: I obtain 1.2s for the tactics (with the time tactic or coqc -time), 3.5s for Qed (using Time or coqc -time) and a total of 6.2s for coqc (using time coqc). It seems that Time Qed is missing a significant amount of time (1.5s). So I guess that it means that it is a problem with the size of the proof term ?

view this post on Zulip Gaëtan Gilbert (Jul 13 2023 at 08:54):

probably
you already said the size is quadratic so that makes it especially likely to be the problem

view this post on Zulip Paolo Giarrusso (Jul 13 2023 at 09:35):

Could you use abstract to lift the duplicated terms into separate constants?

view this post on Zulip Paolo Giarrusso (Jul 13 2023 at 09:44):

Abstract requires an evar-free goal, but there might be ways around that.

view this post on Zulip Benjamin Bonneau (Jul 13 2023 at 12:19):

Paolo Giarrusso said:

Could you use abstract to lift the duplicated terms into separate constants?

To be concrete, the goal I'm solving is something like:

prog_refines p0 ?p1

where, p0 is the input program, ?p1 is a program generated by the tactic and prog_refines is a soundness property. The tactic is solving this goal inductively on p0 and generates a corresponding ?p1. The problem arise with combinators. For instance a sequence operator would be handled by applying a lemma:

Lemma refines_Seq p0a p0b p1a p1b
  (Ha : prog_refines p0a p1a)
  (Hb : prog_refines p0b p1b):
  prog_refines (Seq p0a p0b) (Seq p1a p1b).

Now I think that the problem is that the sub-programs p0a, p0b, p1a andp1b appears as parameters of the lemma, which makes the proof term quadratic in the size of the program.
The generated program p1 is larger (by a constant factor) than p0 so reducing the size of the corresponding terms (by some kind of factorisation maybe ?) could be enough. However those terms are not directly generated but rather inductively instantiated so I don't know if abstract would work here.
I'm considering instead solving a goal:

{p1 | prog_refines p0 p1}

and then reducing the proj1_sig of the proof to obtain the generated program. But it requires a significant refactoring and I'm not sure how well this reduction would be handled by the tactics and the kernel since the term will contain the full proof.

view this post on Zulip Benjamin Bonneau (Jul 27 2023 at 13:39):

I was able to reduce enough the kernel verification time by using transparent_abstract to factorise into separate lemmas the subterms of the generated program.
I'm using something like:

Inductive MyGoal (n : nat) := MyGoalI.

Lemma change_MyGoal_arg (n0 n1 : nat)
  (H : MyGoal n0)
  (E : n0 = n1):
  MyGoal n1.
Proof.
  case E; exact H.
Qed.

Ltac abstract_refl :=
  lazymatch goal with |- ?x0 = _ =>
    (* See https://github.com/coq/coq/issues/16534#issuecomment-1256930507 *)
    let x0 := eval cbv beta in x0 in
    is_ground x0;
    unshelve instantiate (1 := _);
    [ transparent_abstract (exact x0) |]
  end;
  lazymatch goal with |- @eq ?T _ ?x1 =>
    exact (@eq_refl T x1)
  end.

Goal exists (n : nat), MyGoal n /\ n = 0.
Proof.
  do 2 esplit. {
    (* at each step *)
    refine (change_MyGoal_arg _ _ _ _).
    - (* solves the goal, unify the argument *) exact (MyGoalI O).
    - (* abstracts the argument in a transparent lemma *) abstract_refl.
  }
  (* ..._subterm = 0 *)
  cbv.
  (* 0 = 0 *)
  reflexivity.
Qed.

(where in my case MyGoal is a program refinement property and the argument n is the generated program).
This modification slightly increases the time taken by my tactics but greatly reduces the verification time of the kernel:

Original Modified
Tactic 1.229s 1.499s
Kernel (Time Qed) 2.355s 0.873s
Total (coqc) 4.60s 2.62s

As commented, there were indeed some issues with evars, but there was already a known workaround.


Last updated: Jun 23 2024 at 04:03 UTC