Drop useless content from module parameter types. - #22402
Draft
ppedrot wants to merge 2 commits into
Draft
Conversation
In theory, some parts of what we store in module types are not used by the system. The two principal examples are opaque proof bodies and sealed module implementations, as they are never accessed when typechecking modules. In both cases we only ever care about the type of the corresponding object, not its implementation. In practice, we do want to keep them for one single use case, namely the infamous ability to include module types into plain modules. While we could interpret this operation as adding axioms with opaque proofs and modules, users typically expect that it keeps the underlying body instead. This pattern is unfortunately used in several places in the standard library to work around user syntax limitations. Instead of doing it this violently, in this commit we go for a slightly more refined approach. We drop the opaque content of the parameters of functors only. There is no easy way to include the type of module parameters, hence one cannot rely on the aforementioned hack. To easily keep track of which modules are assumed to have no opaque content, we introduce a new type and carefully add wrappers that drop this content at the right place.
ppedrot
added
kind: performance
coqbot-app
Bot
removed
the
request: full CI
Member
Author
|
@coqbot bench |
Contributor
|
🏁 Bench results: INFO: failed to install rocq-mathcomp-boot (dependency rocq-elpi failed) 🐢 Top 25 slow downs┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 203 204 1.2957 0.64% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 57.3 58.6 1.2719 2.22% 782 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 13.0 14.0 1.0701 8.26% 548 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 61.1 62.2 1.0484 1.72% 788 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 65.7 66.3 0.6410 0.98% 794 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 18.8 19.4 0.5901 3.14% 32 coq-performance-tests-lite/src/pattern.v.html │ │ 50.8 51.4 0.5896 1.16% 27 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html │ │ 47.0 47.6 0.5746 1.22% 244 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html │ │ 38.8 39.3 0.5226 1.35% 762 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 9.90 10.3 0.4241 4.28% 703 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 43.1 43.5 0.3844 0.89% 539 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 31.5 31.9 0.3713 1.18% 656 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 6.66 7.00 0.3404 5.11% 165 coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html │ │ 20.3 20.6 0.3083 1.52% 722 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 23.5 23.8 0.3055 1.30% 672 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 53.2 53.5 0.2915 0.55% 567 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 53.5 53.8 0.2798 0.52% 776 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 44.7 45.0 0.2706 0.60% 578 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html │ │ 23.2 23.5 0.2671 1.15% 743 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 0.0333 0.292 0.2587 775.84% 95 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html │ │ 7.54 7.79 0.2503 3.32% 792 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 0.0905 0.316 0.2254 248.99% 97 coq-fiat-crypto-with-bedrock/src/SlowPrimeSynthesisExamples.v.html │ │ 97.6 97.8 0.2122 0.22% 296 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/Addchain.v.html │ │ 0.0909 0.295 0.2044 224.98% 62 coq-fiat-crypto-with-bedrock/src/Assembly/WithBedrock/SymbolicProofs.v.html │ │ 1.12 1.32 0.1996 17.77% 12 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 107 107 -0.7718 -0.72% 255 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 5.47 4.78 -0.6861 -12.55% 1828 rocq-metarocq-safechecker/safechecker/theories/PCUICSafeReduce.v.html │ │ 85.4 84.7 -0.6177 -0.72% 48 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 7.092 6.536 -0.5560 -7.84% 192 coq-vst/veric/binop_lemmas5.v.html │ │ 41.9 41.5 -0.4831 -1.15% 269 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 18.8 18.3 -0.4822 -2.57% 31 coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html │ │ 47.0 46.6 -0.3953 -0.84% 2 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html │ │ 15.0 14.6 -0.3936 -2.63% 672 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ │ 50.6 50.2 -0.3535 -0.70% 376 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 48.5 48.2 -0.3454 -0.71% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v.html │ │ 2.77 2.50 -0.2727 -9.85% 597 coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/SetGroupoidComprehension.v.html │ │ 48.5 48.3 -0.2709 -0.56% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html │ │ 0.282 0.0257 -0.2563 -90.90% 96 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html │ │ 1.42 1.166 -0.2540 -17.89% 937 coq-vst/veric/binop_lemmas2.v.html │ │ 16.3 16.0 -0.2329 -1.43% 57 coq-category-theory/Instance/Fact.v.html │ │ 0.261 0.0315 -0.2300 -87.95% 98 coq-fiat-crypto-with-bedrock/src/SlowPrimeSynthesisExamples.v.html │ │ 0.217 0.00109 -0.2162 -99.50% 66 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html │ │ 37.8 37.6 -0.1962 -0.52% 139 coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html │ │ 22.2 22.0 -0.1911 -0.86% 516 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 29.444 29.253 -0.1910 -0.65% 194 coq-vst/veric/expr_lemmas4.v.html │ │ 7.93 7.74 -0.1875 -2.36% 7 coq-fiat-crypto-with-bedrock/src/PerfTesting/PerfTestSearchPattern.v.html │ │ 2.934 2.747 -0.1870 -6.37% 167 coq-vst/veric/binop_lemmas6.v.html │ │ 2.344 2.158 -0.1860 -7.94% 290 coq-vst/veric/extend_tc.v.html │ │ 20.2 20.0 -0.1802 -0.89% 79 coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v.html │ │ 1.27 1.09 -0.1793 -14.13% 6 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeI64.v.html │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
Member
Author
|
Some effect on some module-heavy constructions: This is uncommon though, all other vo files from the bench have a diff < 1%. |
ppedrot
added
the
request: full CI
coqbot-app
Bot
removed
the
request: full CI
Member
Author
|
Let's retry with a backwards compatible API: @coqbot bench. |
Contributor
|
🏁 Bench results: INFO: failed to install 🐢 Top 25 slow downs┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 62.9 65.4 2.4629 3.91% 608 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 200 202 2.1316 1.07% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 236 237 1.2264 0.52% 141 coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html │ │ 12.8 13.7 0.9864 7.74% 548 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 133 134 0.8976 0.68% 155 coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html │ │ 49.6 50.5 0.8935 1.80% 27 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html │ │ 44.6 45.1 0.5471 1.23% 578 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html │ │ 39.7 40.2 0.5468 1.38% 81 coq-fiat-crypto-with-bedrock/rupicola/src/Rupicola/Examples/Utf8/Utf8.v.html │ │ 38.731 39.173 0.4420 1.14% 834 coq-vst/veric/binop_lemmas4.v.html │ │ 44.7 45.1 0.4240 0.95% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html │ │ 22.4 22.8 0.3930 1.75% 1073 rocq-metarocq-safechecker/safechecker/theories/PCUICSafeReduce.v.html │ │ 27.4 27.7 0.3245 1.18% 13 coq-fourcolor/theories/proof/job287to290.v.html │ │ 44.6 45.0 0.3130 0.70% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v.html │ │ 36.4 36.7 0.2782 0.76% 139 coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html │ │ 126 126 0.2775 0.22% 659 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ │ 25.4 25.7 0.2744 1.08% 13 coq-fourcolor/theories/proof/job223to226.v.html │ │ 12.1 12.4 0.2742 2.26% 800 rocq-metarocq-safechecker/safechecker/theories/PCUICSafeRetyping.v.html │ │ 67.4 67.6 0.2715 0.40% 596 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ │ 1.31 1.58 0.2643 20.13% 4 rocq-mathcomp-analysis/theories/pi_irrational.v.html │ │ 5.082 5.345 0.2630 5.18% 888 coq-vst/veric/binop_lemmas4.v.html │ │ 0.0330 0.293 0.2596 786.01% 95 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html │ │ 103 103 0.2536 0.25% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 31.0 31.2 0.2434 0.79% 13 coq-fourcolor/theories/proof/job254to270.v.html │ │ 17.5 17.7 0.2432 1.39% 243 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 4.30 4.54 0.2418 5.63% 162 coq-category-theory/Instance/Coq/Par.v.html │ └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 41.2 39.6 -1.5704 -3.81% 1423 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 36.3 35.0 -1.3485 -3.71% 898 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 5.37 4.69 -0.6810 -12.68% 1828 rocq-metarocq-safechecker/safechecker/theories/PCUICSafeReduce.v.html │ │ 65.0 64.3 -0.6183 -0.95% 794 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 16.5 15.9 -0.5864 -3.56% 898 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 29.1 28.5 -0.5591 -1.92% 31 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html │ │ 27.1 26.6 -0.5483 -2.02% 34 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html │ │ 50.0 49.5 -0.4936 -0.99% 376 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 105 104 -0.4870 -0.46% 255 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 42.7 42.2 -0.4867 -1.14% 115 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html │ │ 18.6 18.1 -0.4175 -2.25% 31 coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html │ │ 0.683 0.273 -0.4108 -60.10% 398 coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html │ │ 6.414 6.022 -0.3920 -6.11% 192 coq-vst/veric/binop_lemmas5.v.html │ │ 41.0 40.6 -0.3739 -0.91% 269 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 15.9 15.6 -0.3684 -2.31% 57 coq-category-theory/Instance/Fact.v.html │ │ 24.5 24.2 -0.3597 -1.47% 13 coq-fourcolor/theories/proof/job486to489.v.html │ │ 57.3 56.9 -0.3454 -0.60% 512 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 64.8 64.5 -0.3073 -0.47% 305 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/Addchain.v.html │ │ 23.2 22.9 -0.3025 -1.30% 85 coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/AffineProofs.v.html │ │ 0.296 0.000447 -0.2951 -99.85% 64 rocq-mathcomp-analysis/theories/topology_theory/connected.v.html │ │ 1.399 1.113 -0.2860 -20.44% 937 coq-vst/veric/binop_lemmas2.v.html │ │ 4.37 4.10 -0.2729 -6.24% 5 coq-fiat-crypto-with-bedrock/src/Assembly/Parse/Examples/fiat_p256_mul_optimised_seed11.v.html │ │ 0.284 0.0254 -0.2585 -91.07% 96 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html │ │ 54.0 53.8 -0.2541 -0.47% 276 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 15.1 14.9 -0.2502 -1.65% 841 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
In theory, some parts of what we store in module types are not used by the system. The two principal examples are opaque proof bodies and sealed module implementations, as they are never accessed when typechecking modules. In both cases we only ever care about the type of the corresponding object, not its implementation.
In practice, we do want to keep them for one single use case, namely the infamous ability to include module types into plain modules. While we could interpret this operation as adding axioms with opaque proofs and modules, users typically expect that it keeps the underlying body instead. This pattern is unfortunately used in several places in the standard library to work around user syntax limitations.
Instead of doing it this violently, in this commit we go for a slightly more refined approach. We drop the opaque content of the parameters of functors only. There is no easy way to include the type of module parameters, hence one cannot rely on the aforementioned hack.
To easily keep track of which modules are assumed to have no opaque content, we introduce a new type and carefully add wrappers that drop this content at the right place.