Avoid exponential partial reduction

[roconnor-blockstream]

mkVSU calls mkComponent which has a repeat apply Forall_cons. For whatever reason, when Coq applies Forall_cons it fully unfolds the filter_options fixpoint without reducing the inner match expression. Because there are two recursive call sites, this causes an exponential blow up in the the size of the (internal) goal.

To avoid that exponential blow up, I've refactored the filter_options implementation to have only one recursive call site.

I've tested this with a C program with 16 trivial functions f1 to f16 of the form

void f1(void) {}

along with the following verification file

Require Import VST.floyd.proofauto.
Require Import VST.floyd.VSU.
Require Import test.
Instance CompSpecs : compspecs. make_compspecs prog. Defined.

Section TestASI.

Definition mk_spec i : ident * funspec :=
 DECLARE i
 WITH u:unit
 PRE [ ]
    PROP () PARAMS () SEP ()
 POST [ tvoid ]
    PROP ( ) RETURN () SEP ().

Definition TestASI : funspecs := map mk_spec
 [ _f1; _f2; _f3; _f4; _f5; _f6; _f7; _f8; _f9; _f10; _f11; _f12; _f13; _f14; _f15; _f16 ].

End TestASI.

Section Test_VSU.

Definition Test_imports : funspecs := [].
Definition Test_private : funspecs := [].
Definition Test_internals : funspecs := Test_private ++ TestASI.
Definition Test_Gprog : funspecs := Test_imports ++ Test_internals.
Definition Test_Vprog : varspecs. mk_varspecs prog. Defined.

Lemma mk_body i : semax_body Test_Vprog Test_Gprog f_f1 (mk_spec i).
Proof.
start_function.
forward.
entailer.
Qed.

Existing Instance NullExtension.Espec.

Lemma TestVSU: VSU nil Test_imports ltac:(QPprog prog) TestASI emp.
Proof.
Time mkVSU prog Test_internals.
solve_SF_internal mk_body.
solve_SF_internal mk_body.
solve_SF_internal mk_body.
solve_SF_internal mk_body.
solve_SF_internal mk_body.
solve_SF_internal mk_body.
solve_SF_internal mk_body.
solve_SF_internal mk_body.
solve_SF_internal mk_body.
solve_SF_internal mk_body.
solve_SF_internal mk_body.
solve_SF_internal mk_body.
solve_SF_internal mk_body.
solve_SF_internal mk_body.
solve_SF_internal mk_body.
solve_SF_internal mk_body.
Time Qed.

End Test_VSU.

Prior to this change the timings on my machine were:

$ coqc verif_test.v
Finished transaction in 19.819 secs (19.082u,0.496s) (successful)
Finished transaction in 31.257 secs (30.668u,0.045s) (successful)

After applying this change my timings are

$ coqc verif_test.v
Finished transaction in 3.501 secs (3.444u,0.013s) (successful)
Finished transaction in 0.883 secs (0.869u,0.003s) (successful)