Stream: Coq users

Topic: ✔ Non-terminating/super-slow unification


view this post on Zulip Sebastian Ertel (Sep 04 2022 at 19:18):

Dear Coq-ers,

I’m using Koika for one of my projects and repeatedly enter the situation where Coq seems to enter an infinite loop (or at least is very very slow).

Koika is an EDSL for hardware design and I try to give hardware designers a simple way to write tests. A simple test for example looks like this:

Example test2:
  let input := #{
   ("i1"   , bits_t _) => Bits.of_nat _ 1;
   ("i2" , bits_t _) => Bits.of_nat _ 3;
   ("i3" , bits_t _) => Bits.of_nat _ 4
                 }# in

  let (ctxt,_) := run tc_f2 input r in

  let o := Bits.to_nat ctxt.[InfiniteLoop.r1] in

  o = 1.
reflexivity.
Defined.

I reported this in more detail as an issue in Koika . Coq does not even get to the proof part but is stuck at checking the type of the Example with CPU time rising to 100%. That is why I believe that the unification algorithm of Coq could be the cause. But I’m not sure. I let it sit there for several minutes but it never terminated.

I played around with it in a fork and recorded my findings in the code and reported them in the Koika issue. I found a solution for this particular test but when writing more such tests I hit this situation over and over again.

Do you have any idea why that might happen?
What would be a proper way to debug this?

Thanks!

view this post on Zulip Paolo Giarrusso (Sep 04 2022 at 20:09):

Coq's unification algorithms (plural) don't correspond exactly with either cbn or simpl, but none of those are meant for "heavy-duty" computation (unlike vm_compute)

view this post on Zulip Paolo Giarrusso (Sep 04 2022 at 20:15):

However, if the question is about how to unwrap options safely and efficiently, following https://plv.csail.mit.edu/blog/unwrapping-options.html#unwrapping-options, take 2 mentions the option of using vm_compute.

view this post on Zulip Paolo Giarrusso (Sep 04 2022 at 20:19):

But as the issue mentions, vm_compute can't be fast on opaque proofs. Maybe ltac profiling could be helpful here? It should display which tactics take most time, and it could tell whether vm_compute or sth else is at fault.

view this post on Zulip Sebastian Ertel (Sep 04 2022 at 20:20):

I had found this blog post and replace the version on must that is present in Koika with the one proposed in the blog post. This made the unification work like a charm. But I just can't say wait, to be honest.

view this post on Zulip Paolo Giarrusso (Sep 04 2022 at 20:22):

"can't say wait"? Is wait some ill-behaved function?

view this post on Zulip Sebastian Ertel (Sep 04 2022 at 20:24):

Thanks for the hint to Ltac profiling!
How do I do that during unification though?

view this post on Zulip Sebastian Ertel (Sep 04 2022 at 20:26):

Paolo Giarrusso said:

"can't say wait"? Is wait some ill-behaved function?

I'm sorry, I did not get this?

view this post on Zulip Paolo Giarrusso (Sep 04 2022 at 20:26):

Ltac profiling doesn't apply there... unification does have debugging options, but I'm not sure they're relevant? It seems the goal should be to _never_ use unification on non-trivial problems, and to always use vm_compute first

view this post on Zulip Paolo Giarrusso (Sep 04 2022 at 20:27):

@Sebastian Ertel You wrote But I just can't say wait, to be honest. — I have no idea what that means. And I'm not sure understand what the problem is, if unwrap_dec' fixes things

view this post on Zulip Sebastian Ertel (Sep 04 2022 at 20:28):

Oh, sorry, my bad! wait should be why.

view this post on Zulip Paolo Giarrusso (Sep 04 2022 at 20:29):

what's why?

view this post on Zulip Sebastian Ertel (Sep 04 2022 at 20:30):

I mean, I do not understand why unwrap_dec' fixes things and the must(unwrap) implemented in Koika triggers this behaviour.

view this post on Zulip Sebastian Ertel (Sep 04 2022 at 20:34):

I also am not sure what you mean when you say that I should always use vm_compute first.
How would I use a tactic in a type?

view this post on Zulip Sebastian Ertel (Sep 04 2022 at 20:37):

Also, how do I understand when a problem is trivial?
To me, the type of the Example given above seems pretty trivial.

view this post on Zulip Paolo Giarrusso (Sep 04 2022 at 20:39):

Hmmm. I was thinking of this variant of unwrap_dec' — as the blog post hints, this should use vm_compute to reduce is_some:

Notation unwrap_dec'' o := (unwrap_dec o (@eq_refl bool true <: is_some o = true)).

OTOH, you say unwrap_dec' is already good enough, so maybe that's not the ideal suggestion. unwrap_dec' also uses unification, but with a different problem (link for onlookers: https://github.com/mit-plv/koika/blob/8a42a5d4b13890838d9c1c878b25ba4ebae52a5e/coq/Common.v#L192-L196)

view this post on Zulip Paolo Giarrusso (Sep 04 2022 at 20:57):

How would I use a tactic in a type?

For debugging, You can use the refine tactic to give a partial term with holes, and obtain a goal that you can refine further, with refine or other tactics. Tactics-in-terms (e.g. function ltac:(tactic_producing_argument)) lets you do similar things non-interactively.

Also, how do I understand when a problem is trivial? To me, the type of the Example given above seems pretty trivial.

Computing your example is apparently easy and vm_compute does it — but unification is not allowed to just normalize the results in general (because it's used in many other cases), so it tries hard to _not_ compute results, and is much slower.

view this post on Zulip Paolo Giarrusso (Sep 04 2022 at 20:59):

I haven't seen many ways to speed-up unification (beyond telling it to never unfold certain constants — which doesn't seem likely to help you)

view this post on Zulip Sebastian Ertel (Sep 04 2022 at 21:04):

Paolo Giarrusso said:

Hmmm. I was thinking of this variant of unwrap_dec' — as the blog post hints, this should use vm_compute to reduce is_some:

Notation unwrap_dec'' o := (unwrap_dec o (@eq_refl bool true <: is_some o = true)).

OTOH, you say unwrap_dec' is already good enough, so maybe that's not the ideal suggestion. unwrap_dec' also uses unification, but with a different problem (link for onlookers: https://github.com/mit-plv/koika/blob/8a42a5d4b13890838d9c1c878b25ba4ebae52a5e/coq/Common.v#L192-L196)

Thanks for that pointer. I tried it out.
When I use vm_compute via <: I get
Error: Cannot check cast with vm: unresolved arguments remain.
When I use native_compute via <<: I get

Anomaly "File "kernel/vconv.ml", line 199, characters 18-24: Assertion failed."
Please report at http://coq.inria.fr/bugs/.

view this post on Zulip Paolo Giarrusso (Sep 04 2022 at 21:07):

oh, that probably means the computation problem has some unresolved evar left

view this post on Zulip Sebastian Ertel (Sep 04 2022 at 21:08):

Paolo Giarrusso said:

Computing your example is apparently easy and vm_compute does it — but unification is not allowed to just normalize the results in general (because it's used in many other cases), so it tries hard to _not_ compute results, and is much slower.

I see. So the solution would be to help the unification by telling it how to reduce the term via tactics in terms?

view this post on Zulip Paolo Giarrusso (Sep 04 2022 at 21:09):

pretty much — or to use vm_compute to do all the computation, so that unification's left with 1 = 1 or such

view this post on Zulip Sebastian Ertel (Sep 04 2022 at 21:13):

I can use vm_compute just like that in a term?

view this post on Zulip Paolo Giarrusso (Sep 04 2022 at 21:15):

ltac:() lets you call tactics in terms, and if you have an evar-free term, you can use <: as above. But getting the evar-free term might require more fiddling...

view this post on Zulip Paolo Giarrusso (Sep 04 2022 at 21:15):

in the example I tried and that didn't work, might be is_some's implicit argument, or something uninferred in the term. Hard to tell without trying, and it's late here...

view this post on Zulip Sebastian Ertel (Sep 04 2022 at 21:15):

(Well, I guess so)

view this post on Zulip Paolo Giarrusso (Sep 04 2022 at 21:16):

And the problem is trickier than I initially thought — so sorry this wasn't too helpful! Hope I gave some idea of what to expect...

view this post on Zulip Sebastian Ertel (Sep 04 2022 at 21:16):

Well, thanks a lot for taking the time to help me out on this.

view this post on Zulip Sebastian Ertel (Sep 04 2022 at 21:18):

Yes, thanks again for your pointers. I will give it another try using tactics in terms then.

view this post on Zulip Sebastian Ertel (Sep 08 2022 at 18:29):

@Paolo Giarrusso, thanks again for your help! Using tactics in terms and removing some burden on unification by specifying more types, I made my program work.

I do have one more question though before I close this stream:
As far as I understand tactics in terms are side-stepping the Coq's type checking algorithm (more precisely the part responsible for term reductions). Does that mean, whenever I use tactics in terms I'm basically enlarging the TCB by the tactics I'm using?

I think: yes. But I wanted to make sure that I got this right.

view this post on Zulip Paolo Giarrusso (Sep 08 2022 at 18:45):

No, these tactics do not enlarge your TCB, they just produce terms which
are easier to typecheck.

Generally, tactics in proofs aren't trusted, it's the kernel's job to
validate their result. Any typechecking done by tactics is almost entirely
a matter of convenience.
(Tactics that apply postulates technically extend the TCB, but in a very
different sense; using coqchk is advised).

There's a different matter, that's generating parts of your statements
using tactics (or even fancy inference techniques like typeclasses or
canonical structures): it's a good idea to double-check that your top-level
statement is really the one you meant, as far as possible; papers by
Gonthier's team on his major development describe this step explicitly.

view this post on Zulip Sebastian Ertel (Sep 08 2022 at 20:04):

Paolo Giarrusso said:

... papers by
Gonthier's team on his major development describe this step explicitly.

Thanks again for that pointer.

view this post on Zulip Notification Bot (Sep 08 2022 at 20:04):

Sebastian Ertel has marked this topic as resolved.

view this post on Zulip Karl Palmskog (Sep 08 2022 at 20:05):

hm, if anyone wonders most of those papers are listed here: https://math-comp.github.io/papers.html

view this post on Zulip Paolo Giarrusso (Sep 08 2022 at 20:21):

Thanks for adding the link. I was thinking especially of this quote from http://www2.tcs.ifi.lmu.de/~abel/lehre/WS07-08/CAFR/4colproof.pdf (Sec. 2, pages 3-4):

these few lines,
definition of the real numbers in file real.v (about 200 lines in total) are all that one needs to read and understand in order to ascertain that the statement below in file fourcolor.v is indeed a proof of the Four Colour Theorem: [...]
The other 60,000 or so lines of the proof can be read for insight or even entertainment, but need not be reviewed for correctness. That is the job of the the Coq proof assistant, a job for computers.

view this post on Zulip Karl Palmskog (Sep 08 2022 at 20:23):

maybe a bit OT, but it's not always that "smaller" means "more understandable". For example, in PL theory, your operational semantics of a language could take a couple of hundred lines to define from scratch, and your theorem a few lines to state, but to figure out what the semantics and theorem (e.g., subject reduction) means might be a multi-day/week task

view this post on Zulip Paolo Giarrusso (Sep 08 2022 at 20:30):

Of course smaller _all other things being equal_

view this post on Zulip Paolo Giarrusso (Sep 08 2022 at 20:35):

I think the assumption (if you're reviewing such a proof) is that you already understand the involved maths, but you want to confirm whether the formalization gets it right. And potentially you want to double-check what elaboration did.

view this post on Zulip Karl Palmskog (Sep 08 2022 at 20:39):

one document I usually recommend to Coq paper/code reviewers: https://www.ssi.gouv.fr/uploads/2014/11/anssi-requirements-on-the-use-of-coq-in-the-context-of-common-criteria-evaluations-v1.1-en.pdf ("Coq requirements in Common Criteria evaluations")


Last updated: Mar 28 2024 at 13:01 UTC