The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

Is this paper about the current implementation of fiat-crypto?

Would there be any benefits from combining it when certicoq?

On Thu, Jul 30, 2020 at 4:52 AM Jason Gross <jasongross9 AT gmail.com> wrote:
>
> This is actually the topic of a recent draft of mine, recently 
> (re)submitted to POPL 2021.
>
> Some background: One of the biggest bottlenecks in the rewrite tactics is 
> the allocation of evars (in particular, the allocation of evar contexts) 
> when instantiating lemmas.  This shows up mostly when you have a large 
> context or many binders in the goal, and issues such as #12524 
> (setoid_rewrite and rewrite_strat are cubic in the number of binders even 
> when there are no matches) and #12510 are about this.  Separately, even 
> when there are no matches and no binders, autorewrite, rewrite, rewrite!, 
> and rewrite? are all quadratic in the size of the goal (#12600).  So I 
> would not say that autorewrite is already optimized, and I believe there 
> are a number of relatively low-hanging fruit.
>
> Second: Getting a proof term that does not incur overhead which is 
> quadratic (or worse) in the number of rewrites is highly non-trivial; you 
> may find the "Performance Bottlenecks of Proof-Producing Rewriting" section 
> (Appendix A) of the aforementioned paper enlightening.
>
> Given this, there is reason (and evidence) to expect that using a 
> reflective procedure will speed things up for you.  I believe Rtac (see, 
> e.g., Gregory Malecha's thesis) has a general reflective rewriter (though I 
> was not able to make it work in recent versions of Coq, and development 
> seems to be abandoned), and the rewriting engine that I created for 
> fiat-crypto, which is the subject of the aforementioned POPL submission, is 
> another example of such a general engine.  Unfortunately, I cannot in good 
> conscience suggest that you use the framework that I built as anything 
> other than an example; it suffers from a number of restrictions that could 
> be lifted with engineering work (such as the fact that while any type 
> without arguments is supported, the only type families supported are option 
> and prod), and, more importantly, it's unmaintainable in its current form 
> and should be rewritten from scratch.
>
> Hope this helps,
> Jason
>
>
> On Wed, Jul 29, 2020 at 7:14 PM jonikelee AT gmail.com <jonikelee AT gmail.com> 
> wrote:
>>
>> Using Ltac profiling, it looks like about 40% of time spent in one
>> project I have is within autorewrite, the remainder primarily doing
>> proof search. The particular autorewrite hint dbs are not large (10 or
>> so rules each, one has only 3 rules) and the addition of rules ends
>> before the hint dbs are used. In such cases, would it be advantageous to
>> create a reflective procedure to replace use of autorewrite by a
>> particular hint db?  Or is this unlikely to improve performance,
>> considering that autorewrite is already optimized (presumably)?  I do
>> not beleive that Qeds are significantly time consuming in this project,
>> so I don't think shrinking the proof terms will have much benefit.
>>