Extrude uniform parameters of inner fixpoints in guard condition check (grant #16040) by herbelin · Pull Request #17986 · rocq-prover/rocq

herbelin · 2023-08-29T10:49:55Z

The PR computes the parameters of inner fixpoints that are stable across recursive calls and extrudes them for the computation of guard through these inner fixpoints, thus granting the long-standing wish described in #16040.

Closes #16040

Added / updated test-suite.
Added changelog

ppedrot · 2023-10-30T11:38:26Z

kernel/inductive.ml

+  let n = List.length l in
+  let n' = List.length l' in
+  if n < n' then List.map2 (&&) l (List.firstn n l')
+  else List.map2 (&&) (List.firstn n' l) l'


It's a weird way to write a function that can be written much more elegantly with a pattern-matching.

Indeed! [Changed]

ppedrot · 2023-11-06T09:22:26Z

Contrarily to the other tweaks to the guard condition, I think that this one is indeed innocuous. There are some dubious places in the code but I don't understand it enough to predict the consequences.

ppedrot · 2023-11-06T09:23:56Z

kernel/inductive.ml

+      if Int.equal n (nbodies + k - i) then
+        let args, extra = List.chop nargs l in
+        let new_args = snd (List.filter2 (fun uniform _ -> not uniform) argsign args) in
+        Term.applist (f, new_args @ extra)


This term could be ill-typed, couldn't it? How do we know that uniform parameters cannot depend on a non-uniform one? With SProp we lose injectivity of dependence on variables.

You're right, as in:

Inductive sTrue : SProp := sI. Parameter P : sTrue -> Prop. Check fix f a (e : P a) n := match n with | 0 => 0 | S n => f sI e n end.

And the same would typically also happen if we had η on unit.

Then we could either expect the uniform arguments to be a continuous prefix of the arguments, as that would cover the interesting cases, or to consider that definitionally-inhabited subsingleton arguments can always be extruded?

Characterizing the latter does not look so easy, so, by simplicity, I would go towards the first solution. Ok for you? (That means reducing the data argsign to just an int.)

Actually, there is nothing wrong with extruding (a copy of) the definitionally-inhabited subsingleton arguments, or more generally with uniform arguments that do not constitute a prefix of the arguments. Moreover, the code already takes this into account. Assuming an interleaving of uniform γ and γ' and non-uniform δ as in:

fix f γ δ γ' n := φ(f γ δ' γ', ..., f γ δ'' γ')

the translation is:

fun γ δ γ' => (fix f δ n := φ(f δ', ..., f δ'')) δ

What check_nested_fix_body is doing is to check the guard of φ(f δ', ..., f δ'') in the context γ δ γ' where γ and γ' inherit the size of their argument in the stack (if any). This implicitly means that it already considers not a fun γ γ' => ... extrusion (which might be ill-typed in general) but a fun γ δ γ' => ... δ combination of extrusion and expansion.

[Added 28/12] For the example above, the transformation is:

Check fun a (e : P a) => (fix f a n := match n with | 0 => 0 | S n => f sI n end) a.

Note: I added a clarification in the code.

I still fail to see why I (x, y, z) is a well-formed type in your comment. The z variable has not the right type as it has type C{x, y₀} rather than C{x, y} where y₀ is the outermost y variable.

Regarding typing, I'm finding a small weakness in the algorithm: the arguments could be normalized before checking their uniformity: otherwise we may find u different of y but convertible to y, and fail to extrude it in a way which respects typing.

Assuming the normalization done, we know z:C{x, y} and z:C{x, u} from the original term and thus C{x, y} and C{x, u} convertible (or more precisely C{x, y} ≦ C{x, u} with subtyping). Since u is not convertible with y, then either y and u are absent in the first place or the convertibility proof of C{x, y} ≦ C{x, u} either eventually discards y and u, or makes them convertible from some other reason (e.g. being in an SProp). In any cases, the idea is that the convertibility proof of C{x, y} ≦ C{x, u} can be modified into a proof of convertibility of C{x, y₀} ≦ C{x, y} (using then your naming convention for y and y₀).

I don't think that missing an extrusion because of some u not detected as being convertible to the y is bad as we would just be more restrictive in the guard compared to what would give the optimal (well-typed) extrusion. However, do you think e.g. it would be better to check the convertibility of u with y (thus taking into account strict propness), rather than just reasoning on the form?

either y and u are absent in the first place or the convertibility proof of C{x, y} ≦ C{x, u} either eventually discards y and u, or makes them convertible from some other reason

That doesn't really look like a formal proof to me. This kind of injectivity property is especially dubious in presence of SProp, we could end up proving UIP without realizing with this kind of feature.

Would it be wrong to do a proof by induction on the structure and the reducts of C{x, _}? Then, am I missing other base cases than when C{_,_} does not depend on its second argument and when both C{x, y} and C{x, u} are detected proof irrelevant? (I'm asking because I'm not so familiar with the rules for proof irrelevance, so I may be missing some rules.)

More generally, is your intuition telling you that the result is wrong or is it that you'd like, as a rule, that statements about Coq TT are always formalized? In the latter case, I would need help because I don't have an infrastructure such as MetaCoq at hand to do a computer-checked proof.

Alternatively, we can also renounce to non-prefix extrusion. This would still certainly cover most of the interesting cases.

I'd prefer not to implement non-prefix extrusion so as to err on the safe side.

Ok, done.

I also added more tests as well as found and fixed a residual bug (wrongly dropping the "NeedReduce" status of the uniform arguments of an inner fix by testing the need for reduction of only extra_stack in the previous version of the PR).

SkySkimmer · 2023-11-22T15:10:35Z

@herbelin if you want this merged you should undraft at some point

herbelin · 2023-11-22T16:36:36Z

I had missed @ppedrot's comment, sorry. I now answered. I wanted to add a few tests before undrafting.

herbelin · 2023-11-22T18:38:38Z

I wanted to add a few tests before undrafting.

Actually, the tests I had in mind were about a more ambitious version supporting uniform parameters across mutual fixpoints. That seems significantly more complicated (need to reason up to permutation of uniform arguments) and I renounced to it.

coqbot-app · 2023-12-08T13:45:44Z

🔴 CI failure at commit 9dd2d32 without any failure in the test-suite

✔️ Corresponding job for the base commit 2c068b8 succeeded

❔ Ask me to try to extract a minimal test case that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following target: ci-fiat_crypto

You can also pass me a specific list of targets to minimize as arguments.

herbelin · 2023-12-08T13:57:24Z

If someone wants to have a second look. At least this looks ok on my side. (The fiat-crypto failure is probably related to upstream changes made yesterday.)

SkySkimmer · 2023-12-08T13:58:45Z

cc @JasonGross

JasonGross · 2023-12-08T16:03:59Z

Looks like the Fiat Crypto job is using an outdated rewriter artifact? If you rerun the ci-rewriter job then Fiat Crypto should succeed

…oint.

…bility.

…ction". We do it at use time rather than artificially propagating it transitively to arguments that don't need reduction.

…x in guard checking. We proceed in three steps on the expansion of the relevant body of a block of fix: - first find the arguments of the recursive calls that are uniform - then drop those arguments - in addition to the main argument of the inner fix, we propagate the recursive specification of the arguments that are uniform towards the body of the fixpoints.

…refix.

coqbot-app · 2024-05-06T23:38:01Z

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]      │              CPU cycles               │           CPU instructions            │  max resident mem [KB]  │
│                                     │                         │                                       │                                       │                         │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│                       coq-equations │    7.43     7.71  -3.63 │    30979751662     31091777979  -0.36 │    50782514800     50785169545  -0.01 │  386688   386752  -0.02 │
│                          coq-stdlib │  361.32   365.45  -1.13 │  1529847933066   1544116665917  -0.92 │  1286830929329   1286721029895   0.01 │  717672   724612  -0.96 │
│               coq-mathcomp-fingroup │   30.28    30.60  -1.05 │   137848856062    139044751646  -0.86 │   208053138399    208098891167  -0.02 │  562932   562792   0.02 │
│                 coq-metacoq-erasure │  503.62   506.14  -0.50 │  2299181568829   2308623199588  -0.41 │  3589971313519   3587068986254   0.08 │ 2145268  2155420  -0.47 │
│                         coq-unimath │ 2462.86  2474.33  -0.46 │ 11216697316195  11266152227356  -0.44 │ 22196568179425  22196955338450  -0.00 │ 1254644  1254392   0.02 │
│             coq-metacoq-safechecker │  423.95   425.37  -0.33 │  1940682599112   1947039043440  -0.33 │  3196895271479   3198184985804  -0.04 │ 2071296  2067192   0.20 │
│                           coq-verdi │   48.93    49.06  -0.26 │   219711179089    220033397051  -0.15 │   340695466400    340625440525   0.02 │  531912   531708   0.04 │
│               coq-mathcomp-solvable │  118.21   118.52  -0.26 │   540030557781    540609424952  -0.11 │   859335847935    859376435694  -0.00 │  881440   882148  -0.08 │
│                             coq-vst │  880.24   882.44  -0.25 │  3999756130940   4010970206723  -0.28 │  6736779845291   6746279153516  -0.14 │ 2150396  2146588   0.18 │
│                coq-metacoq-template │  150.77   151.10  -0.22 │   669657210521    669481716888   0.03 │  1045729948941   1045766907948  -0.00 │ 1484476  1484408   0.00 │
│ coq-neural-net-interp-computed-lite │  298.63   299.14  -0.17 │  1362993825234   1366621392102  -0.27 │  3616202513327   3616176013784   0.00 │ 1126356  1128468  -0.19 │
│                       coq-fourcolor │ 1359.87  1361.54  -0.12 │  6218288259015   6225903693444  -0.12 │ 12916732545136  12916642601262   0.00 │ 2129016  2129016   0.00 │
│                            coq-core │  129.16   129.29  -0.10 │   503289323814    500466198407   0.56 │   531769251020    531379394813   0.07 │  457156   456744   0.09 │
│              coq-mathcomp-character │  109.70   109.80  -0.09 │   501043805480    501768612615  -0.14 │   793223136074    793186435089   0.00 │ 1152640  1152996  -0.03 │
│                        coq-bedrock2 │  359.92   360.23  -0.09 │  1640489112639   1641215551005  -0.04 │  3102646537872   3102625198150   0.00 │  859160   857600   0.18 │
│                        coq-compcert │  281.05   281.08  -0.01 │  1271037010065   1271931307266  -0.07 │  1940476265197   1942311886610  -0.09 │ 1118756  1122476  -0.33 │
│                coq-mathcomp-algebra │  260.97   260.94   0.01 │  1190812993011   1190406550711   0.03 │  2003836977644   2003784947340   0.00 │ 1296208  1293040   0.25 │
│                    coq-math-classes │   85.72    85.69   0.04 │   385071658923    384845182099   0.06 │   535999789073    536002652393  -0.00 │  503948   503464   0.10 │
│        coq-fiat-crypto-with-bedrock │ 6233.97  6230.73   0.05 │ 28397968956306  28384315845891   0.05 │ 51218068875448  51219277392767  -0.00 │ 3246072  3246152  -0.00 │
│                      coq-verdi-raft │  580.62   580.01   0.11 │  2642049319326   2636170624161   0.22 │  4159974913996   4159818746496   0.00 │  840112   840020   0.01 │
│                      coq-test-suite │  701.17   700.36   0.12 │  2995602306017   2990268280131   0.18 │  5390780942283   5390124220014   0.01 │ 2694712  2696160  -0.05 │
│              coq-mathcomp-odd-order │  785.78   784.76   0.13 │  3598204436640   3593696906566   0.13 │  6096399681402   6096506168094  -0.00 │ 1638764  1638480   0.02 │
│          coq-performance-tests-lite │  704.71   703.72   0.14 │  3183660717485   3180002617148   0.12 │  5685171914021   5684797137658   0.01 │ 2266368  2266188   0.01 │
│                    coq-fiat-parsers │  312.00   311.48   0.17 │  1389831743202   1389962527048  -0.01 │  2469483460585   2469431762715   0.00 │ 2399480  2400088  -0.03 │
│                        coq-rewriter │  390.90   390.05   0.22 │  1777397689229   1773276985477   0.23 │  2989836246869   2990535005371  -0.02 │ 1473464  1477740  -0.29 │
│                   coq-iris-examples │  469.92   468.89   0.22 │  2136391184854   2132772078412   0.17 │  3276696495282   3276739816708  -0.00 │ 1113956  1110872   0.28 │
│                   coq-metacoq-pcuic │  988.83   986.34   0.25 │  4436296201564   4423155301701   0.30 │  6475871614773   6476877667210  -0.02 │ 2686788  2684184   0.10 │
│               coq-engine-bench-lite │  157.10   156.68   0.27 │   666595722632    664848305951   0.26 │  1225718011790   1225364415573   0.03 │ 1234872  1236652  -0.14 │
│                  coq-mathcomp-field │  143.19   142.78   0.29 │   653605081985    651483617553   0.33 │  1077242906894   1077236514817   0.00 │ 1448996  1448356   0.04 │
│                 coq-category-theory │  695.62   693.57   0.30 │  3163616419583   3153538270740   0.32 │  5257533190359   5257499755423   0.00 │  956992   956768   0.02 │
│         coq-rewriter-perf-SuperFast │  790.89   788.46   0.31 │  3595962712037   3584693193580   0.31 │  6255369499972   6254140713914   0.02 │ 1571936  1576768  -0.31 │
│                         coq-coqutil │   42.35    42.21   0.33 │   186949403111    186322953713   0.34 │   270456516370    270414282233   0.02 │  561564   561596  -0.01 │
│                            coq-hott │  160.66   160.11   0.34 │   717477774717    716158904060   0.18 │  1142251481356   1142149773858   0.01 │  481092   478608   0.52 │
│            coq-metacoq-translations │   16.97    16.91   0.35 │    75604092002     75273175753   0.44 │   124799682993    124782539870   0.01 │  847736   846372   0.16 │
│                      coq-coquelicot │   39.85    39.70   0.38 │   177037628770    176711676177   0.18 │   249050139641    249017128764   0.01 │  855204   853300   0.22 │
│                           coq-color │  251.90   250.85   0.42 │  1133670615765   1128205020471   0.48 │  1634243370747   1634254997814  -0.00 │ 1205492  1210008  -0.37 │
│                        coq-coqprime │   48.29    48.08   0.44 │   216617318555    216322181802   0.14 │   333956781634    334016919348  -0.02 │  783632   784100  -0.06 │
│              coq-mathcomp-ssreflect │  220.58   219.37   0.55 │  1007731459329   1001952843350   0.58 │  1673746152065   1673649217154   0.01 │ 1739272  1738844   0.02 │
│                            coq-corn │  719.58   715.43   0.58 │  3268962546289   3251144549316   0.55 │  5072125935808   5071950480634   0.00 │  764668   767112  -0.32 │
│                         coq-bignums │   29.33    29.12   0.72 │   132987041931    132534551019   0.34 │   192039681535    192027214438   0.01 │  472800   474672  -0.39 │
│                       coq-fiat-core │   59.41    58.61   1.36 │   246618563454    245110088812   0.62 │   367750243995    367749881137   0.00 │  482372   482952  -0.12 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

🐢 Top 25 slow downs

┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                              TOP 25 SLOW DOWNS                                                               │
│                                                                                                                                              │
│   OLD       NEW      DIFF   %DIFF    Ln                     FILE                                                                             │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   2.3820    2.9110  0.5290  22.21%   487  coq-stdlib/Numbers/HexadecimalFacts.v.html                                                         │
│  94.8160   95.3230  0.5070   0.53%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                    │
│  94.8030   95.2370  0.4340   0.46%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                    │
│  62.4270   62.8180  0.3910   0.63%   609  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html      │
│  80.8680   81.2580  0.3900   0.48%    48  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                            │
│  47.2380   47.5880  0.3500   0.74%   558  coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html                                    │
│ 241.6060  241.9550  0.3490   0.14%   141  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                         │
│   0.5500    0.8700  0.3200  58.18%   736  coq-stdlib/Reals/Cauchy/ConstructiveCauchyReals.v.html                                             │
│  33.3230   33.6150  0.2920   0.88%  1333  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html   │
│   6.4060    6.6730  0.2670   4.17%  3024  coq-fiat-crypto-with-bedrock/src/Assembly/EquivalenceProofs.v.html                                 │
│  25.4110   25.6720  0.2610   1.03%   345  coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html                                 │
│   0.0000    0.2550  0.2550    inf%   476  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/New/Signature.v.html                      │
│   8.0550    8.3070  0.2520   3.13%  2854  coq-fiat-crypto-with-bedrock/src/Assembly/EquivalenceProofs.v.html                                 │
│  15.8430   16.0920  0.2490   1.57%   828  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html                            │
│  36.4620   36.7060  0.2440   0.67%   548  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html                   │
│ 137.9620  138.1910  0.2290   0.17%   155  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                         │
│  22.5150   22.7380  0.2230   0.99%  1073  coq-metacoq-safechecker/safechecker/theories/PCUICSafeReduce.v.html                                │
│   7.3020    7.5220  0.2200   3.01%   604  coq-unimath/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v.html │
│  17.4150   17.6300  0.2150   1.23%   607  coq-mathcomp-odd-order/theories/PFsection9.v.html                                                  │
│   0.5540    0.7680  0.2140  38.63%   422  coq-stdlib/MSets/MSetList.v.html                                                                   │
│  17.8010   18.0110  0.2100   1.18%    32  coq-performance-tests-lite/src/pattern.v.html                                                      │
│  37.3950   37.6000  0.2050   0.55%     3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html                   │
│   8.0480    8.2470  0.1990   2.47%  1133  coq-metacoq-erasure/erasure/theories/ErasureFunction.v.html                                        │
│   0.5850    0.7780  0.1930  32.99%   816  coq-stdlib/MSets/MSetRBT.v.html                                                                    │
│  17.1780   17.3660  0.1880   1.09%   481  coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html                                  │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                   TOP 25 SPEED UPS                                                                   │
│                                                                                                                                                      │
│   OLD       NEW      DIFF     %DIFF     Ln                      FILE                                                                                 │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 182.1250  180.3930  -1.7320    -0.95%   233  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│ 220.9070  219.5110  -1.3960    -0.63%   103  coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html                                     │
│ 155.8050  154.5760  -1.2290    -0.79%  1190  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                           │
│ 257.5000  256.3240  -1.1760    -0.46%  1629  coq-metacoq-pcuic/pcuic/theories/PCUICSR.v.html                                                         │
│  67.8680   66.9460  -0.9220    -1.36%    27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                                │
│   3.9210    3.1790  -0.7420   -18.92%   153  coq-vst/veric/binop_lemmas2.v.html                                                                      │
│ 257.6860  256.9680  -0.7180    -0.28%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html           │
│  36.5180   35.9270  -0.5910    -1.62%     2  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html                                 │
│  27.6420   27.1030  -0.5390    -1.95%    35  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html                    │
│  29.4820   28.9660  -0.5160    -1.75%    32  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html                    │
│ 101.5690  101.0770  -0.4920    -0.48%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                             │
│   3.9240    3.4410  -0.4830   -12.31%   490  coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html                                              │
│  74.0610   73.5940  -0.4670    -0.63%   905  coq-unimath/UniMath/ModelCategories/Generated/LNWFSCocomplete.v.html                                    │
│   3.5090    3.1090  -0.4000   -11.40%   857  coq-vst/veric/expr_lemmas.v.html                                                                        │
│  24.6700   24.3510  -0.3190    -1.29%    49  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                                 │
│  41.6970   41.3910  -0.3060    -0.73%   139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                            │
│  34.0720   33.7810  -0.2910    -0.85%   839  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                           │
│  62.6020   62.3130  -0.2890    -0.46%   609  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                             │
│  25.6350   25.3570  -0.2780    -1.08%    24  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/MultiRetSplit.v.html                                   │
│  27.9450   27.6700  -0.2750    -0.98%    12  coq-fourcolor/theories/job563to588.v.html                                                               │
│ 131.8780  131.6030  -0.2750    -0.21%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                                  │
│   0.8390    0.5650  -0.2740   -32.66%   200  coq-stdlib/Numbers/HexadecimalNat.v.html                                                                │
│  18.1130   17.8410  -0.2720    -1.50%    12  coq-fourcolor/theories/job315to318.v.html                                                               │
│   5.7200    5.4540  -0.2660    -4.65%    19  coq-fiat-crypto-with-bedrock/src/Language/IdentifiersBasicGENERATED.v.html                              │
│   0.2540    0.0000  -0.2540  -100.00%   476  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/New/Signature.v.html                           │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

ppedrot

This change to the guard lies in the likely reasonable territory.

ppedrot · 2024-05-07T06:25:07Z

@coqbot merge now

coqbot-app · 2024-05-07T06:25:09Z

@ppedrot: You cannot merge this PR because:

There is still a needs: benchmarking label.

ppedrot · 2024-05-07T06:26:56Z

@coqbot merge now

…tch. Commit 140908d (PR rocq-prover#17986, about the extrusion of uniform parameters) was passing the wrong extra arguments of a match.

…tch. Commit 140908d (PR rocq-prover#17986, about the extrusion of uniform parameters) was passing the wrong extra arguments of a match. (cherry picked from commit 1338fea)

As evidenced by the flurry of LLM-discovered soundness issues with the guard check, this commit was clearly not analyzed enough. In this commit we simply revert the part that introduced the uniform parameter support and leave the cleanups. It invalidates at least one concrete test from the test-suite, but the next commit should reinstall the same feature in a way that is much more robust.

herbelin added kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: inductives Inductive types, fixpoints, etc. labels Aug 29, 2023

herbelin added this to the 8.19+rc1 milestone Aug 29, 2023

coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Aug 29, 2023

herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 3, 2023

herbelin force-pushed the master+fix16040-guard-extrude-fix-parameter branch from 43d5435 to d3e7d63 Compare September 3, 2023 15:44

coqbot-app bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Sep 3, 2023

herbelin changed the title ~~Extrude uniform parameters of inner fixpoints in guard condition check (grant #16040) + support for mutually defined inner fixpoints~~ Extrude uniform parameters of inner fixpoints in guard condition check (grant #16040) Sep 3, 2023

ppedrot reviewed Oct 30, 2023

View reviewed changes

ppedrot reviewed Nov 6, 2023

View reviewed changes

SkySkimmer removed this from the 8.19+rc1 milestone Nov 22, 2023

herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label Nov 22, 2023

herbelin force-pushed the master+fix16040-guard-extrude-fix-parameter branch from d3e7d63 to db8af2e Compare November 22, 2023 18:09

coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Nov 22, 2023

herbelin added a commit to herbelin/github-coq that referenced this pull request Nov 22, 2023

Change log for rocq-prover#17986

9dd2d32

herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label Nov 22, 2023

herbelin force-pushed the master+fix16040-guard-extrude-fix-parameter branch from db8af2e to 9dd2d32 Compare November 22, 2023 18:36

coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Nov 22, 2023

herbelin marked this pull request as ready for review November 22, 2023 18:40

herbelin requested review from a team as code owners November 22, 2023 18:40

Typo in specification of CList.interval.

0eb955e

herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label May 6, 2024

herbelin added 7 commits May 6, 2024 11:11

Renaming CList.skipn_at_least into CList.skipn_at_best, more to the p…

e519aa8

…oint.

Inductive.ml: extend lift_stack to any integer.

c930313

Guard checking: isolate the code dealing with lambdas for later reusa…

eaabad5

…bility.

Guard: More natural way to test for "at least one argument needs redu…

77aa57b

…ction". We do it at use time rather than artificially propagating it transitively to arguments that don't need reduction.

Extrusion of uniform arguments of a fix: restriction to the maximal p…

49bb2cc

…refix.

Change log for rocq-prover#17986

1830851

herbelin force-pushed the master+fix16040-guard-extrude-fix-parameter branch from af7a654 to 1830851 Compare May 6, 2024 09:16

ppedrot added this to the 8.20+rc1 milestone May 7, 2024

ppedrot approved these changes May 7, 2024

View reviewed changes

ppedrot removed the needs: benchmarking Performance testing is required. label May 7, 2024

coqbot-app bot merged commit 98b6978 into rocq-prover:master May 7, 2024

herbelin mentioned this pull request Oct 9, 2024

Fixes #19661: incorrect reduction of inner fixpoints with extra arguments in fixpoint guard checker #19671

Merged

2 tasks

This was referenced Feb 28, 2026

Guard checker soundness bug: cross-calls in nested mutual fixpoints #21682

Closed

Guard checker soundness bug: higher-order recursive call through fixpoint #21683

Closed

ppedrot mentioned this pull request Feb 28, 2026

Implement extruded uniform parameters in the dumbest possible way. #21686

Closed

Conversation

herbelin commented Aug 29, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

herbelin Nov 22, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ppedrot commented Nov 6, 2023

Uh oh!

Choose a reason for hiding this comment

Uh oh!

herbelin Nov 22, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

herbelin Nov 22, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

herbelin Dec 9, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

SkySkimmer commented Nov 22, 2023

Uh oh!

herbelin commented Nov 22, 2023

Uh oh!

herbelin commented Nov 22, 2023

Uh oh!

coqbot-app bot commented Dec 8, 2023

Uh oh!

herbelin commented Dec 8, 2023

Uh oh!

SkySkimmer commented Dec 8, 2023

Uh oh!

JasonGross commented Dec 8, 2023

Uh oh!

coqbot-app bot commented May 6, 2024

Uh oh!

ppedrot left a comment

Choose a reason for hiding this comment

Uh oh!

ppedrot commented May 7, 2024

Uh oh!

coqbot-app bot commented May 7, 2024

Uh oh!

ppedrot commented May 7, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

herbelin commented Aug 29, 2023 •

edited

Loading

herbelin Nov 22, 2023 •

edited

Loading

herbelin Nov 22, 2023 •

edited

Loading

herbelin Nov 22, 2023 •

edited

Loading

herbelin Dec 9, 2023 •

edited

Loading