Sebastian Ertel (Sep 04 2022 at 19:18): 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!
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)
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.
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.
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.
Paolo Giarrusso (Sep 04 2022 at 20:22):"can't say wait"? Is wait some ill-behaved function?
Sebastian Ertel (Sep 04 2022 at 20:24):Thanks for the hint to Ltac profiling!
How do I do that during unification though?
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?
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
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
Sebastian Ertel (Sep 04 2022 at 20:28):Oh, sorry, my bad! wait should be why.
Paolo Giarrusso (Sep 04 2022 at 20:29):what's why?
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.
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?
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.
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)
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.
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)
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 usevm_computeto reduceis_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/.
oh, that probably means the computation problem has some unresolved evar left
Sebastian Ertel (Sep 04 2022 at 21:08):Paolo Giarrusso said:
Computing your example is apparently easy and
vm_computedoes 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?
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
Sebastian Ertel (Sep 04 2022 at 21:13):I can use vm_compute just like that in a term?
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...
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...
Sebastian Ertel (Sep 04 2022 at 21:15):(Well, I guess so)
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...
Sebastian Ertel (Sep 04 2022 at 21:16):Well, thanks a lot for taking the time to help me out on this.
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.
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.
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.
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.
Notification Bot (Sep 08 2022 at 20:04):Sebastian Ertel has marked this topic as resolved.
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
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.
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
Paolo Giarrusso (Sep 08 2022 at 20:30):Of course smaller _all other things being equal_
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.
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: Sep 25 2023 at 12:01 UTC