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!

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)

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.

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.

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.

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

Thanks for the hint to Ltac profiling!

How do I do that during unification though?

Paolo Giarrusso said:

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

I'm sorry, I did not get this?

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

@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

Oh, sorry, my bad! `wait`

should be `why`

.

what's `why`

?

I mean, I do not understand why `unwrap_dec'`

fixes things and the `must(unwrap)`

implemented in Koika triggers this behaviour.

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?

Also, how do I understand when a problem is trivial?

To me, the type of the `Example`

given above seems pretty trivial.

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)

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.

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)

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/.
```

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

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?

pretty much — or to use `vm_compute`

to do all the computation, so that unification's left with `1 = 1`

or such

I can use `vm_compute`

just like that in a term?

`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...

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...

(Well, I guess so)

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...

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

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

@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.

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.

Paolo Giarrusso said:

... papers by

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

Thanks again for that pointer.

Sebastian Ertel has marked this topic as resolved.

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

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.

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

Of course smaller _all other things being equal_

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.

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