Stream: Coq devs & plugin devs

Topic: Performance of coqchk on instantiated functors

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.

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.

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.

Pierre-Marie Pédrot (Jun 07 2022 at 10:51):

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

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

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?

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

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

Paolo Giarrusso (Jun 07 2022 at 12:07):

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

Gaëtan Gilbert (Jun 07 2022 at 12:08):

A is already typechecked

Paolo Giarrusso (Jun 07 2022 at 12:09):

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

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.

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

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

Paolo Giarrusso (Jun 07 2022 at 12:12):

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

Paolo Giarrusso (Jun 07 2022 at 12:13):

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

Paolo Giarrusso (Jun 07 2022 at 12:13):

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

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

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.

Gaëtan Gilbert (Jun 07 2022 at 12:17):

I think that won't work for coqchk

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

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?

Paolo Giarrusso (Jun 07 2022 at 12:27):

in any case, I wonder:

• can we classify causes of coqchk slowdowns on functor applications? Are they all of this form, or is there something else?
• would manual use of Opaque help @Jason Gross 's problem? Or would one need to add stronger sealing mechanisms?
• could coqchk gain better heuristics? writing Opaque M.n is more work than Opaque X.n, which is more work than coqchk generating that.

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)?

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

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)

Paolo Giarrusso (Jun 07 2022 at 13:55):

I wonder if some intermediate Opaquer command could help

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

Gaëtan Gilbert (Jun 07 2022 at 13:57):

what would Opaquer even do?

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: May 28 2023 at 13:30 UTC