Stream: Coq devs & plugin devs

Topic: Performance of coqchk on instantiated functors


view this post on Zulip Jason Gross (Jun 05 2022 at 16:25):

Is there anything that can be done about how slow coqchk is when there are lots of instantiated module functors floating around? I have an commit that added about 4s of coqc time and instantiated 3 functors, adding over 1.5h of coqchk time (https://github.com/mit-plv/fiat-crypto/runs/6742237434?check_suite_focus=true / https://github.com/mit-plv/fiat-crypto/pull/1274/files / https://github.com/mit-plv/fiat-crypto/commit/f3ef38805173110dd150c6de71f6fdaffd042c6d over https://github.com/mit-plv/fiat-crypto/runs/6742072165?check_suite_focus=true).
I suspect the issue is that the functor has a bunch of conversion problems buried in opaque proofs that become much harder when the functor arguments are instantiated. The only thing I can think of to do is replicate the functor arguments as a record and move all the proofs and definitions outside the functor (using functors because FMapInterface), but it would be nice if coqchk could handle this automatically.

view this post on Zulip Pierre-Marie Pédrot (Jun 07 2022 at 08:29):

The handling of functors in coqchk is very wobbly. I'm not sure if there is a universal solution to your kind of performance issues.

view this post on Zulip Ali Caglayan (Jun 07 2022 at 10:38):

Correct me if I am wrong, but don't most issues arising from functors come up because their specification is just so general? Perhaps it would be possible to restrict to a sane subset of functors for which we can fix performance/soundness issues. I know there have been informal discussions about reducing the complexity of the functor mechanism, but if Jason's use case is not pathological, it should definitely be a part of the sane fragment. Of course, I could also be wrong and it could be precisely this fragment that is problematic.

view this post on Zulip Pierre-Marie Pédrot (Jun 07 2022 at 10:51):

coqchk trying to be safe is likely to be the issue here

view this post on Zulip Pierre-Marie Pédrot (Jun 07 2022 at 10:52):

i.e. it expands fully applied functors to check that the result is still well-typed

view this post on Zulip Paolo Giarrusso (Jun 07 2022 at 12:02):

when coqchk typechecks the result of F A instead of F and A separately, does it regard members of A as at least Opaque?

view this post on Zulip Paolo Giarrusso (Jun 07 2022 at 12:04):

otherwise, “pathological functors" will include any functor F that relies on its argument being abstract for performance

view this post on Zulip Gaëtan Gilbert (Jun 07 2022 at 12:05):

it does not
fields of F A get the same unfolding oracle as fields of F

view this post on Zulip Paolo Giarrusso (Jun 07 2022 at 12:07):

that is fine, the question is on fields of A itself _when typechecking the applied functor_

view this post on Zulip Gaëtan Gilbert (Jun 07 2022 at 12:08):

A is already typechecked

view this post on Zulip Paolo Giarrusso (Jun 07 2022 at 12:09):

that is not relevant, so let me spell out what I mean

view this post on Zulip Gaëtan Gilbert (Jun 07 2022 at 12:10):

consider

Module Type AT.
  Parameter n : nat.
End AT.

Definition ignore (x:nat) := 0.

Module F(X:AT).
  Definition foo : ignore X.n = ignore 100 := eq_refl.
End F.

Module M.
  Definition n := 101.
End M.

Module FM := F M.

view this post on Zulip Gaëtan Gilbert (Jun 07 2022 at 12:11):

while checking FM.foo coqchk sees eq_refl : ignore M.n = ignore 100 with M.n Defined

view this post on Zulip Gaëtan Gilbert (Jun 07 2022 at 12:11):

so it will compare 101 == 100 100 == 99 99 == 98 etc until failing and falling back to unfolding ignore

view this post on Zulip Paolo Giarrusso (Jun 07 2022 at 12:12):

yep, so could coqchk treat M.n as Opaque (even if Defined) when typechecking FM.foo?

view this post on Zulip Paolo Giarrusso (Jun 07 2022 at 12:13):

also wondering if you can even write Opaque M.n by hand here...

view this post on Zulip Paolo Giarrusso (Jun 07 2022 at 12:13):

even if, of course, that's useless for coqc

view this post on Zulip Gaëtan Gilbert (Jun 07 2022 at 12:14):

if you move the definition of M before F you can put Opaque M.n and I think coqchk would respect it

view this post on Zulip Paolo Giarrusso (Jun 07 2022 at 12:16):

hm, this is also accepted, no idea with what semantics:

Module F(X:AT).
  Opaque X.n.

view this post on Zulip Gaëtan Gilbert (Jun 07 2022 at 12:17):

I think that won't work for coqchk

view this post on Zulip Gaëtan Gilbert (Jun 07 2022 at 12:19):

I think you can make definitions where treating functor arguments as Opaque in coqchk is the wrong thing but maybe it would work more often than the current system

view this post on Zulip Paolo Giarrusso (Jun 07 2022 at 12:22):

I agree that Opaque gives less opacity than the source program, but what are those examples, and are those rare enough to be pathological? Maybe showing such examples would help the discussion?

view this post on Zulip Paolo Giarrusso (Jun 07 2022 at 12:27):

in any case, I wonder:

view this post on Zulip Paolo Giarrusso (Jun 07 2022 at 12:28):

Semi-OT: does coqchk also erase module sealing via opaque ascriptions (which is otherwise the strongest sealing available)?

view this post on Zulip Gaëtan Gilbert (Jun 07 2022 at 12:40):

actually Opaque M.n isn't strong enough here, because it's getting unfolded in a Constant vs Constructor conversion Opaque is ignored

view this post on Zulip Gaëtan Gilbert (Jun 07 2022 at 12:41):

and treating M.n as Qed is just incorrect, because you can write stuff like Definition n_def : M.n = 100 := eq_refl in F (moving the definition of M before F)

view this post on Zulip Paolo Giarrusso (Jun 07 2022 at 13:55):

I wonder if some intermediate Opaquer command could help

view this post on Zulip Paolo Giarrusso (Jun 07 2022 at 13:56):

otherwise I'm wondering if coqchk -trust-functor-soundness that doesn't expand functors could be useful

view this post on Zulip Gaëtan Gilbert (Jun 07 2022 at 13:57):

what would Opaquer even do?

view this post on Zulip Paolo Giarrusso (Jun 07 2022 at 14:03):

it's getting unfolded in a Constant vs Constructor conversion — Opaque is ignored

could you implement delayed unfolding even in this scenario (and have a different command just for bwd compat), or is this too hard to implement, and maybe this is too naive a Q.


Last updated: Feb 01 2023 at 16:03 UTC