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.

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.

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.

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

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

when coqchk typechecks the result of `F A`

instead of `F`

and `A`

separately, does it regard members of `A`

as at least `Opaque`

?

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

it does not

fields of `F A`

get the same unfolding oracle as fields of `F`

that is fine, the question is on fields of `A`

itself _when typechecking the applied functor_

A is already typechecked

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

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

while checking `FM.foo`

coqchk sees `eq_refl : ignore M.n = ignore 100`

with `M.n`

Defined

so it will compare `101 == 100`

`100 == 99`

`99 == 98`

etc until failing and falling back to unfolding `ignore`

yep, so could `coqchk`

treat `M.n`

as `Opaque`

(even if `Defined`

) when typechecking `FM.foo`

?

also wondering if you can even write `Opaque M.n`

by hand here...

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

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

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

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

I think that won't work for coqchk

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

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?

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.

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

actually `Opaque M.n`

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

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)

I wonder if some intermediate `Opaquer`

command could help

otherwise I'm wondering if `coqchk -trust-functor-soundness`

that doesn't expand functors could be useful

what would Opaquer even do?

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: Oct 13 2024 at 01:02 UTC