Introduce an efficient typing rule for let-bindings in Typeops.#21678
Open
ppedrot wants to merge 2 commits intorocq-prover:masterfrom
Open
Introduce an efficient typing rule for let-bindings in Typeops.#21678ppedrot wants to merge 2 commits intorocq-prover:masterfrom
ppedrot wants to merge 2 commits intorocq-prover:masterfrom
Conversation
ppedrot
added
kind: fix
coqbot-app
bot
removed
the
request: full CI
Member
Author
|
@coqbot bench |
Member
Author
Contributor
|
🏁 Bench results: INFO: failed to install 🐢 Top 25 slow downs┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 62.9 66.4 3.4971 5.56% 608 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 94.0 94.7 0.7389 0.79% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 0.724 1.39 0.6654 91.87% 813 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 0.296 0.941 0.6452 218.15% 153 rocq-mathcomp-algebra/algebra/spectral.v.html │ │ 21.6 22.1 0.5040 2.33% 651 rocq-stdlib/theories/Zmod/ZmodBase.v.html │ │ 0.497 0.946 0.4494 90.48% 586 rocq-stdlib/theories/Strings/Byte.v.html │ │ 0.480 0.899 0.4196 87.50% 816 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 0.00449 0.415 0.4108 9145.73% 72 rocq-mathcomp-algebra/algebra/spectral.v.html │ │ 6.201 6.602 0.4010 6.47% 192 coq-vst/veric/binop_lemmas5.v.html │ │ 7.92 8.31 0.3934 4.97% 1331 coq-mathcomp-odd-order/theories/PFsection9.v.html │ │ 0.564 0.954 0.3895 69.05% 7 rocq-mathcomp-solvable/solvable/all_solvable.v.html │ │ 34.681 35.055 0.3740 1.08% 97 coq-vst/veric/binop_lemmas5.v.html │ │ 32.9 33.2 0.3334 1.01% 12 coq-fourcolor/theories/proof/job439to465.v.html │ │ 0.293 0.622 0.3285 112.02% 17 rocq-stdlib/theories/micromega/Env.v.html │ │ 0.000309 0.315 0.3144 101735.28% 793 rocq-mathcomp-algebra/algebra/mxalgebra.v.html │ │ 5.84 6.15 0.3074 5.26% 196 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/HValuedSets.v.html │ │ 0.293 0.585 0.2920 99.71% 14 rocq-stdlib/theories/extraction/ExtrOcamlZBigInt.v.html │ │ 0.630 0.922 0.2914 46.25% 41 rocq-stdlib/theories/ZArith/Zdiv_facts.v.html │ │ 35.125 35.409 0.2840 0.81% 147 coq-vst/veric/expr_lemmas4.v.html │ │ 23.9 24.2 0.2800 1.17% 12 coq-fourcolor/theories/proof/job486to489.v.html │ │ 29.7 30.0 0.2765 0.93% 12 coq-fourcolor/theories/proof/job001to106.v.html │ │ 18.3 18.6 0.2639 1.44% 12 coq-fourcolor/theories/proof/job311to314.v.html │ │ 48.7 49.0 0.2493 0.51% 376 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 15.429 15.677 0.2480 1.61% 1209 coq-vst/floyd/Component.v.html │ │ 0.699 0.942 0.2427 34.72% 9 rocq-mathcomp-solvable/solvable/extremal.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 202 201 -0.8311 -0.41% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 1.03 0.502 -0.5243 -51.07% 719 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 0.424 0.00326 -0.4202 -99.23% 75 rocq-mathcomp-algebra/algebra/spectral.v.html │ │ 0.422 0.00188 -0.4198 -99.55% 171 rocq-mathcomp-field/field/finfield.v.html │ │ 0.417 0.00942 -0.4080 -97.74% 154 rocq-mathcomp-algebra/algebra/spectral.v.html │ │ 0.833 0.478 -0.3551 -42.63% 650 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 0.619 0.268 -0.3508 -56.68% 12 rocq-stdlib/theories/MSets/MSets.v.html │ │ 0.725 0.407 -0.3185 -43.90% 374 rocq-stdlib/theories/Sorting/SetoidList.v.html │ │ 0.315 0.000128 -0.3145 -99.96% 796 rocq-mathcomp-algebra/algebra/mxalgebra.v.html │ │ 24.4 24.2 -0.2777 -1.14% 550 coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │ │ 0.633 0.361 -0.2721 -42.96% 682 rocq-stdlib/theories/Numbers/DecimalFacts.v.html │ │ 25.4 25.2 -0.2255 -0.89% 12 coq-fourcolor/theories/proof/job299to302.v.html │ │ 27.7 27.5 -0.2253 -0.81% 12 coq-fourcolor/theories/proof/job287to290.v.html │ │ 20.9 20.7 -0.2206 -1.06% 479 rocq-metarocq-erasure/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v.html │ │ 0.226 0.00760 -0.2181 -96.63% 118 rocq-mathcomp-algebra/algebra/spectral.v.html │ │ 0.327 0.110 -0.2166 -66.28% 658 rocq-stdlib/theories/Numbers/DecimalFacts.v.html │ │ 0.295 0.0802 -0.2147 -72.81% 166 rocq-mathcomp-algebra/algebra/spectral.v.html │ │ 0.229 0.0180 -0.2109 -92.12% 640 rocq-mathcomp-solvable/solvable/cyclic.v.html │ │ 0.214 0.00276 -0.2108 -98.71% 422 rocq-mathcomp-solvable/solvable/cyclic.v.html │ │ 0.325 0.117 -0.2082 -64.03% 14 rocq-stdlib/theories/setoid_ring/Ncring.v.html │ │ 0.208 0.00333 -0.2050 -98.40% 763 rocq-metarocq-erasure/erasure/theories/EWcbvEval.v.html │ │ 0.576 0.372 -0.2039 -35.41% 1161 rocq-stdlib/theories/Strings/Byte.v.html │ │ 10.6 10.4 -0.2038 -1.92% 496 coq-rewriter/src/Rewriter/Rewriter/Wf.v.html │ │ 0.396 0.193 -0.2034 -51.37% 16 rocq-stdlib/theories/Numbers/HexadecimalPos.v.html │ │ 0.515 0.314 -0.2007 -38.99% 145 rocq-metarocq-pcuic/pcuic/theories/PCUICPrincipality.v.html │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
SkySkimmer
approved these changes
Mar 3, 2026
SkySkimmer
added
the
needs: progress
Contributor
|
What's going on in fiat crypto? |
Contributor
|
Seems to timeout in |
Member
Author
|
@coqbot resume ci minimize ci-fiat_crypto |
Contributor
|
I was unable to minimize any of the CI targets that you requested. |
Member
Author
Contributor
|
I was unable to minimize any of the CI targets that you requested. |
Member
Author
|
It seems that the minimizer is not able to handle timeouts properly even if we gave it a failing reproduction test... (cc @JasonGross) |
ppedrot
added
the
request: full CI
ppedrot
force-pushed
the
preserve-let-in-kernel-the-return
branch
from
8cbd4cb to
c5d5ec8
Compare
coqbot-app
bot
removed
the
request: full CI
Member
|
The bot looks at the CI log to determine the error message it is supposed to maintain. Here there was no error message, so it can't minimize. We should probably add a mode that disables this check ("coqbot resume ci overlay minimize" or something), but in the meantime, you can make a branch of fiat-crypto with the patch, add an overlay, retrigger the CI, and then trigger the minimizer on the timeout that occurs in CI logs. |
When the expand_let typing flag is set in the environment, we change
the kernel typing rule for let-bindings from
let x := t in u : T{x := t}
to
let x := t in u : let x := t in T.
We cannot do this by default since it may change the inferred type for
some expressions, which is returned when the expected type is not
provided. To work around this, we statically set the flag in expressions
for which the precise inferred type is not relevant. For now there is
no user-facing flag that would allow setting this option in a more
fine-grained way though, but it is easy to fix.
This is a revival of rocq-prover#13606 and a partial fix of rocq-prover#11838. The latter still
suffers from superlinear blowups in unrelated parts of the kernel, namely
VM and native compilation.
ppedrot
added
the
request: full CI
ppedrot
force-pushed
the
preserve-let-in-kernel-the-return
branch
from
c5d5ec8 to
18f1190
Compare
coqbot-app
bot
removed
the
request: full CI
Member
Author
|
@coqbot ci minimize |
Contributor
|
I have initiated minimization at commit 18f1190 for the suggested target ci-fiat_crypto as requested. |
Contributor
|
Error: Could not minimize file in 10m 2s (from ci-fiat_crypto) (full log on GitHub Actions, cc @JasonGross) build log (truncated to last 26KiB; full 5.4MiB file on GitHub Actions Artifacts under
|
Member
Author
|
coqbot tried to get the previous artifact for some reason and since there was none it miserably failed. I'm stubborn, so let's retry: @coqbot ci minimize ci-fiat_crypto |
Contributor
|
I am now running minimization at commit 18f1190 on requested target ci-fiat_crypto. I'll come back to you with the results once it's done. |
Contributor
|
Error: Could not minimize file in 9m 43s (from ci-fiat_crypto) (full log on GitHub Actions, cc @JasonGross) build log (truncated to last 26KiB; full 5.4MiB file on GitHub Actions Artifacts under
|
Contributor
|
@coqbot ci minimize ci-fiat_crypto |
Contributor
|
I am now running minimization at commit 18f1190 on requested target ci-fiat_crypto. I'll come back to you with the results once it's done. |
Member
Author
|
@coqbot ci minimize ci-fiat_crypto |
Contributor
|
I am now running minimization at commit 18f1190 on requested target ci-fiat_crypto. I'll come back to you with the results once it's done. |
Contributor
Minimization interrupted by timeout, being automatically continued. Partially Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/fiat_crypto/src/Assembly/WithBedrock/Proofs.v in 5h 15m 9s (from ci-fiat_crypto) (interrupted by timeout, being automatically continued) (full log on GitHub Actions - verbose log)⭐ ⏱️ Partially Minimized Coq File (timeout)(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "+implicit-core-hint-db,+implicits-in-term,+non-reversible-notation,+deprecated-intros-until-0,+deprecated-focus,+unused-intro-pattern,+variable-collision,+unexpected-implicit-declaration,+omega-is-deprecated,+deprecated-instantiate-syntax,+non-recursive,+undeclared-scope,+deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,+deprecated-typeclasses-transparency-without-locality,+fragile-hint-constr,-deprecated-since-9.0,-deprecated-since-8.20,-deprecated-from-Coq" "-w" "-notation-overridden,-native-compiler-disabled,-ambiguous-paths,-masking-absolute-name" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-coqlib" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq//" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/src" "Crypto" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Coqprime" "Coqprime" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Kami" "Kami" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Ltac2" "Ltac2" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Rewriter" "Rewriter" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Rupicola" "Rupicola" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Stdlib" "Stdlib" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/bedrock2" "bedrock2" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/bedrock2Examples" "bedrock2Examples" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/compiler" "compiler" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/coqutil" "coqutil" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/riscv" "riscv" "-top" "Crypto.Assembly.WithBedrock.Proofs") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 122 lines to 45 lines *)
(* coqc version 9.3+alpha compiled with OCaml 4.14.2
coqtop version 9.3+alpha
Expected coqc runtime on this file: 1.827 sec
Expected coqc peak memory usage on this file: 886660.0 kb *)
Require Crypto.Assembly.WithBedrock.Semantics.
Require Crypto.Assembly.EquivalenceProofs.
Import Stdlib.micromega.Lia.
Import Stdlib.ZArith.ZArith.
Import Crypto.Assembly.Syntax.
Import Crypto.Util.Option.
Import Crypto.Util.Bool.Reflect.
Import Crypto.Util.ListUtil.
Import Crypto.Util.Tactics.SpecializeBy.
Import Crypto.Assembly.EquivalenceProofs.
Definition R_regs_preserved_v rn (m : Semantics.reg_state)
:= Z.land (Tuple.nth_default 0%Z rn m) (Z.ones 64).
Definition R_regs_preserved G d G' d' (m : Semantics.reg_state) rs rs'
:= forall rn idx, Symbolic.get_reg rs' rn = Some idx -> exists idx', Symbolic.get_reg rs rn = Some idx' /\ let v := R_regs_preserved_v (N.to_nat rn) m in eval_idx_Z G d idx' v -> eval_idx_Z G' d' idx v.
Lemma R_regs_preserved_set_reg G d G' d' rs rs' ri rm v
(H : R_regs_preserved G d G' d' rm rs rs')
(H_same : (ri < N.of_nat (List.length widest_registers))%N -> exists idx, Symbolic.get_reg rs ri = Some idx /\ let v' := R_regs_preserved_v (N.to_nat ri) rm in eval_idx_Z G d idx v' -> eval_idx_Z G' d' v v')
: R_regs_preserved G d G' d' rm rs (Symbolic.set_reg rs' ri v).
Proof.
cbv [R_regs_preserved] in *.
intros rn idx; specialize (H rn).
rewrite get_reg_set_reg_full; intro.
vm_compute (length widest_registers) in *.
repeat first [ progress break_innermost_match_hyps
| progress inversion_option
| progress subst
| progress destruct_head'_and
| progress destruct_head'_or
| progress destruct_head'_ex
| progress specialize_by_assumption
| progress specialize_by lia
| rewrite @Bool.andb_true_iff in *
| rewrite @Bool.andb_false_iff in *
| solve [ eauto ]
| progress reflect_hyps
| match goal with
| [ H : forall v, ?k = Some v -> _, H' : ?k = Some _ |- _ ]
=> specialize (H _ H')
end ].
Timeout 5 Qed.🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)🛠️ 📜 Intermediate Coq File log (useful for debugging if minimization did not go as far as you wanted)📜 Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 13MiB file on GitHub Actions Artifacts under
|
Contributor
|
That may be as minimized as it will get. From there it will inline dependencies but probably have to leave a lot of them around. |
Contributor
Minimization interrupted by timeout, being automatically continued. Partially Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/fiat_crypto/src/Assembly/WithBedrock/Proofs.v in 5h 15m 11s (from ci-fiat_crypto) (interrupted by timeout, being automatically continued) (full log on GitHub Actions - verbose log)⭐ ⏱️ Partially Minimized Coq File (timeout)(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "+implicit-core-hint-db,+implicits-in-term,+non-reversible-notation,+deprecated-intros-until-0,+deprecated-focus,+unused-intro-pattern,+variable-collision,+unexpected-implicit-declaration,+omega-is-deprecated,+deprecated-instantiate-syntax,+non-recursive,+undeclared-scope,+deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,+deprecated-typeclasses-transparency-without-locality,+fragile-hint-constr,-deprecated-since-9.0,-deprecated-since-8.20,-deprecated-from-Coq" "-w" "-notation-overridden,-native-compiler-disabled,-ambiguous-paths,-masking-absolute-name" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-coqlib" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq//" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/src" "Crypto" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Coqprime" "Coqprime" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Kami" "Kami" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Ltac2" "Ltac2" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Rewriter" "Rewriter" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Rupicola" "Rupicola" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Stdlib" "Stdlib" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/bedrock2" "bedrock2" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/bedrock2Examples" "bedrock2Examples" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/compiler" "compiler" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/coqutil" "coqutil" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/riscv" "riscv" "-top" "Top.bug_01") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 122 lines to 45 lines, then from 65 lines to 45 lines *)
(* coqc version 9.3+alpha compiled with OCaml 4.14.2
coqtop version 9.3+alpha
Expected coqc runtime on this file: 1.852 sec
Expected coqc peak memory usage on this file: 888372.0 kb *)
Require Crypto.Assembly.WithBedrock.Semantics.
Require Crypto.Assembly.EquivalenceProofs.
Import Stdlib.micromega.Lia.
Import Stdlib.ZArith.ZArith.
Import Crypto.Assembly.Syntax.
Import Crypto.Util.Option.
Import Crypto.Util.Bool.Reflect.
Import Crypto.Util.ListUtil.
Import Crypto.Util.Tactics.SpecializeBy.
Import Crypto.Assembly.EquivalenceProofs.
Definition R_regs_preserved_v rn (m : Semantics.reg_state)
:= Z.land (Tuple.nth_default 0%Z rn m) (Z.ones 64).
Definition R_regs_preserved G d G' d' (m : Semantics.reg_state) rs rs'
:= forall rn idx, Symbolic.get_reg rs' rn = Some idx -> exists idx', Symbolic.get_reg rs rn = Some idx' /\ let v := R_regs_preserved_v (N.to_nat rn) m in eval_idx_Z G d idx' v -> eval_idx_Z G' d' idx v.
Lemma R_regs_preserved_set_reg G d G' d' rs rs' ri rm v
(H : R_regs_preserved G d G' d' rm rs rs')
(H_same : (ri < N.of_nat (List.length widest_registers))%N -> exists idx, Symbolic.get_reg rs ri = Some idx /\ let v' := R_regs_preserved_v (N.to_nat ri) rm in eval_idx_Z G d idx v' -> eval_idx_Z G' d' v v')
: R_regs_preserved G d G' d' rm rs (Symbolic.set_reg rs' ri v).
Proof.
cbv [R_regs_preserved] in *.
intros rn idx; specialize (H rn).
rewrite get_reg_set_reg_full; intro.
vm_compute (length widest_registers) in *.
repeat first [ progress break_innermost_match_hyps
| progress inversion_option
| progress subst
| progress destruct_head'_and
| progress destruct_head'_or
| progress destruct_head'_ex
| progress specialize_by_assumption
| progress specialize_by lia
| rewrite @Bool.andb_true_iff in *
| rewrite @Bool.andb_false_iff in *
| solve [ eauto ]
| progress reflect_hyps
| match goal with
| [ H : forall v, ?k = Some v -> _, H' : ?k = Some _ |- _ ]
=> specialize (H _ H')
end ].
Timeout 5 Qed.🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)🛠️ 📜 Intermediate Coq File log (useful for debugging if minimization did not go as far as you wanted)📜 Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 13MiB file on GitHub Actions Artifacts under
|
Contributor
Minimization interrupted by timeout, being automatically continued. Partially Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/fiat_crypto/src/Assembly/WithBedrock/Proofs.v in 5h 15m 9s (from ci-fiat_crypto) (interrupted by timeout, being automatically continued) (full log on GitHub Actions - verbose log)⭐ ⏱️ Partially Minimized Coq File (timeout)(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "+implicit-core-hint-db,+implicits-in-term,+non-reversible-notation,+deprecated-intros-until-0,+deprecated-focus,+unused-intro-pattern,+variable-collision,+unexpected-implicit-declaration,+omega-is-deprecated,+deprecated-instantiate-syntax,+non-recursive,+undeclared-scope,+deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,+deprecated-typeclasses-transparency-without-locality,+fragile-hint-constr,-deprecated-since-9.0,-deprecated-since-8.20,-deprecated-from-Coq" "-w" "-notation-overridden,-native-compiler-disabled,-ambiguous-paths,-masking-absolute-name" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-coqlib" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq//" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/src" "Crypto" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Coqprime" "Coqprime" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Kami" "Kami" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Ltac2" "Ltac2" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Rewriter" "Rewriter" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Rupicola" "Rupicola" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Stdlib" "Stdlib" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/bedrock2" "bedrock2" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/bedrock2Examples" "bedrock2Examples" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/compiler" "compiler" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/coqutil" "coqutil" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/riscv" "riscv" "-top" "Top.bug_01") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 122 lines to 45 lines, then from 65 lines to 45 lines, then from 65 lines to 45 lines *)
(* coqc version 9.3+alpha compiled with OCaml 4.14.2
coqtop version 9.3+alpha
Expected coqc runtime on this file: 1.793 sec
Expected coqc peak memory usage on this file: 886840.0 kb *)
Require Crypto.Assembly.WithBedrock.Semantics.
Require Crypto.Assembly.EquivalenceProofs.
Import Stdlib.micromega.Lia.
Import Stdlib.ZArith.ZArith.
Import Crypto.Assembly.Syntax.
Import Crypto.Util.Option.
Import Crypto.Util.Bool.Reflect.
Import Crypto.Util.ListUtil.
Import Crypto.Util.Tactics.SpecializeBy.
Import Crypto.Assembly.EquivalenceProofs.
Definition R_regs_preserved_v rn (m : Semantics.reg_state)
:= Z.land (Tuple.nth_default 0%Z rn m) (Z.ones 64).
Definition R_regs_preserved G d G' d' (m : Semantics.reg_state) rs rs'
:= forall rn idx, Symbolic.get_reg rs' rn = Some idx -> exists idx', Symbolic.get_reg rs rn = Some idx' /\ let v := R_regs_preserved_v (N.to_nat rn) m in eval_idx_Z G d idx' v -> eval_idx_Z G' d' idx v.
Lemma R_regs_preserved_set_reg G d G' d' rs rs' ri rm v
(H : R_regs_preserved G d G' d' rm rs rs')
(H_same : (ri < N.of_nat (List.length widest_registers))%N -> exists idx, Symbolic.get_reg rs ri = Some idx /\ let v' := R_regs_preserved_v (N.to_nat ri) rm in eval_idx_Z G d idx v' -> eval_idx_Z G' d' v v')
: R_regs_preserved G d G' d' rm rs (Symbolic.set_reg rs' ri v).
Proof.
cbv [R_regs_preserved] in *.
intros rn idx; specialize (H rn).
rewrite get_reg_set_reg_full; intro.
vm_compute (length widest_registers) in *.
repeat first [ progress break_innermost_match_hyps
| progress inversion_option
| progress subst
| progress destruct_head'_and
| progress destruct_head'_or
| progress destruct_head'_ex
| progress specialize_by_assumption
| progress specialize_by lia
| rewrite @Bool.andb_true_iff in *
| rewrite @Bool.andb_false_iff in *
| solve [ eauto ]
| progress reflect_hyps
| match goal with
| [ H : forall v, ?k = Some v -> _, H' : ?k = Some _ |- _ ]
=> specialize (H _ H')
end ].
Timeout 5 Qed.🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted) (truncated to 6.0KiB; full 204KiB file on GitHub Actions Artifacts under
|
Contributor
Minimization interrupted by timeout, being automatically continued. Partially Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/fiat_crypto/src/Assembly/WithBedrock/Proofs.v in 5h 15m 9s (from ci-fiat_crypto) (interrupted by timeout, being automatically continued) (full log on GitHub Actions - verbose log)⭐ ⏱️ Partially Minimized Coq File (timeout)(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "+implicit-core-hint-db,+implicits-in-term,+non-reversible-notation,+deprecated-intros-until-0,+deprecated-focus,+unused-intro-pattern,+variable-collision,+unexpected-implicit-declaration,+omega-is-deprecated,+deprecated-instantiate-syntax,+non-recursive,+undeclared-scope,+deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,+deprecated-typeclasses-transparency-without-locality,+fragile-hint-constr,-deprecated-since-9.0,-deprecated-since-8.20,-deprecated-from-Coq" "-w" "-notation-overridden,-native-compiler-disabled,-ambiguous-paths,-masking-absolute-name" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-coqlib" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq//" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/src" "Crypto" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Coqprime" "Coqprime" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Kami" "Kami" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Ltac2" "Ltac2" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Rewriter" "Rewriter" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Rupicola" "Rupicola" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Stdlib" "Stdlib" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/bedrock2" "bedrock2" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/bedrock2Examples" "bedrock2Examples" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/compiler" "compiler" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/coqutil" "coqutil" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/riscv" "riscv" "-top" "Top.bug_01") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 122 lines to 45 lines, then from 65 lines to 45 lines, then from 65 lines to 45 lines, then from 65 lines to 45 lines *)
(* coqc version 9.3+alpha compiled with OCaml 4.14.2
coqtop version 9.3+alpha
Expected coqc runtime on this file: 1.765 sec
Expected coqc peak memory usage on this file: 890168.0 kb *)
Require Crypto.Assembly.WithBedrock.Semantics.
Require Crypto.Assembly.EquivalenceProofs.
Import Stdlib.micromega.Lia.
Import Stdlib.ZArith.ZArith.
Import Crypto.Assembly.Syntax.
Import Crypto.Util.Option.
Import Crypto.Util.Bool.Reflect.
Import Crypto.Util.ListUtil.
Import Crypto.Util.Tactics.SpecializeBy.
Import Crypto.Assembly.EquivalenceProofs.
Definition R_regs_preserved_v rn (m : Semantics.reg_state)
:= Z.land (Tuple.nth_default 0%Z rn m) (Z.ones 64).
Definition R_regs_preserved G d G' d' (m : Semantics.reg_state) rs rs'
:= forall rn idx, Symbolic.get_reg rs' rn = Some idx -> exists idx', Symbolic.get_reg rs rn = Some idx' /\ let v := R_regs_preserved_v (N.to_nat rn) m in eval_idx_Z G d idx' v -> eval_idx_Z G' d' idx v.
Lemma R_regs_preserved_set_reg G d G' d' rs rs' ri rm v
(H : R_regs_preserved G d G' d' rm rs rs')
(H_same : (ri < N.of_nat (List.length widest_registers))%N -> exists idx, Symbolic.get_reg rs ri = Some idx /\ let v' := R_regs_preserved_v (N.to_nat ri) rm in eval_idx_Z G d idx v' -> eval_idx_Z G' d' v v')
: R_regs_preserved G d G' d' rm rs (Symbolic.set_reg rs' ri v).
Proof.
cbv [R_regs_preserved] in *.
intros rn idx; specialize (H rn).
rewrite get_reg_set_reg_full; intro.
vm_compute (length widest_registers) in *.
repeat first [ progress break_innermost_match_hyps
| progress inversion_option
| progress subst
| progress destruct_head'_and
| progress destruct_head'_or
| progress destruct_head'_ex
| progress specialize_by_assumption
| progress specialize_by lia
| rewrite @Bool.andb_true_iff in *
| rewrite @Bool.andb_false_iff in *
| solve [ eauto ]
| progress reflect_hyps
| match goal with
| [ H : forall v, ?k = Some v -> _, H' : ?k = Some _ |- _ ]
=> specialize (H _ H')
end ].
Timeout 5 Qed.🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted) (truncated to 6.0KiB; full 204KiB file on GitHub Actions Artifacts under
|
Member
Author
|
Indeed it didn't even inlined the modules, this is now seemingly looping. |
Member
|
That is a bit weird, presumably the issue is that Crypto.Assembly.EquivalenceProofs is so slow to build that it does not manage to make it through the initial steps that are required to verify that inlining succeeded before timing out (or the first couple of inlining strategies fail and there is not enough time to run a couple dozen variants and find the one that works) |
Member
Author
|
I'll try to hand-minimize this a bit further, but I think I've got the explanation for the timeout. Basically we're inferring a type |
Member
|
If you manually inline the file and proactively admit all Qed'd proofs (maybe I should set up the minimizer to attempt this version first?), it should be able to resume minimization from there. |
Contributor
Minimization interrupted by timeout, being automatically continued. Partially Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/fiat_crypto/src/Assembly/WithBedrock/Proofs.v in 5h 15m 10s (from ci-fiat_crypto) (interrupted by timeout, being automatically continued) (full log on GitHub Actions - verbose log)⭐ ⏱️ Partially Minimized Coq File (timeout)(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "+implicit-core-hint-db,+implicits-in-term,+non-reversible-notation,+deprecated-intros-until-0,+deprecated-focus,+unused-intro-pattern,+variable-collision,+unexpected-implicit-declaration,+omega-is-deprecated,+deprecated-instantiate-syntax,+non-recursive,+undeclared-scope,+deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,+deprecated-typeclasses-transparency-without-locality,+fragile-hint-constr,-deprecated-since-9.0,-deprecated-since-8.20,-deprecated-from-Coq" "-w" "-notation-overridden,-native-compiler-disabled,-ambiguous-paths,-masking-absolute-name" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-coqlib" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq//" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/src" "Crypto" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Coqprime" "Coqprime" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Kami" "Kami" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Ltac2" "Ltac2" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Rewriter" "Rewriter" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Rupicola" "Rupicola" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Stdlib" "Stdlib" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/bedrock2" "bedrock2" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/bedrock2Examples" "bedrock2Examples" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/compiler" "compiler" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/coqutil" "coqutil" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/riscv" "riscv" "-top" "Top.bug_01") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 122 lines to 45 lines, then from 65 lines to 45 lines, then from 65 lines to 45 lines, then from 65 lines to 45 lines, then from 65 lines to 45 lines *)
(* coqc version 9.3+alpha compiled with OCaml 4.14.2
coqtop version 9.3+alpha
Expected coqc runtime on this file: 1.750 sec
Expected coqc peak memory usage on this file: 888588.0 kb *)
Require Crypto.Assembly.WithBedrock.Semantics.
Require Crypto.Assembly.EquivalenceProofs.
Import Stdlib.micromega.Lia.
Import Stdlib.ZArith.ZArith.
Import Crypto.Assembly.Syntax.
Import Crypto.Util.Option.
Import Crypto.Util.Bool.Reflect.
Import Crypto.Util.ListUtil.
Import Crypto.Util.Tactics.SpecializeBy.
Import Crypto.Assembly.EquivalenceProofs.
Definition R_regs_preserved_v rn (m : Semantics.reg_state)
:= Z.land (Tuple.nth_default 0%Z rn m) (Z.ones 64).
Definition R_regs_preserved G d G' d' (m : Semantics.reg_state) rs rs'
:= forall rn idx, Symbolic.get_reg rs' rn = Some idx -> exists idx', Symbolic.get_reg rs rn = Some idx' /\ let v := R_regs_preserved_v (N.to_nat rn) m in eval_idx_Z G d idx' v -> eval_idx_Z G' d' idx v.
Lemma R_regs_preserved_set_reg G d G' d' rs rs' ri rm v
(H : R_regs_preserved G d G' d' rm rs rs')
(H_same : (ri < N.of_nat (List.length widest_registers))%N -> exists idx, Symbolic.get_reg rs ri = Some idx /\ let v' := R_regs_preserved_v (N.to_nat ri) rm in eval_idx_Z G d idx v' -> eval_idx_Z G' d' v v')
: R_regs_preserved G d G' d' rm rs (Symbolic.set_reg rs' ri v).
Proof.
cbv [R_regs_preserved] in *.
intros rn idx; specialize (H rn).
rewrite get_reg_set_reg_full; intro.
vm_compute (length widest_registers) in *.
repeat first [ progress break_innermost_match_hyps
| progress inversion_option
| progress subst
| progress destruct_head'_and
| progress destruct_head'_or
| progress destruct_head'_ex
| progress specialize_by_assumption
| progress specialize_by lia
| rewrite @Bool.andb_true_iff in *
| rewrite @Bool.andb_false_iff in *
| solve [ eauto ]
| progress reflect_hyps
| match goal with
| [ H : forall v, ?k = Some v -> _, H' : ?k = Some _ |- _ ]
=> specialize (H _ H')
end ].
Timeout 5 Qed.🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted) (truncated to 6.0KiB; full 204KiB file on GitHub Actions Artifacts under
|
Contributor
|
manually interrupted the auto continue |
Member
Author
|
Here is a small snippet that only depends on the stdlib. I could inline it further, but it's mostly to quickly pinpoint the culprit in the fiat-crypto dev. Require Import Stdlib.ZArith.ZArith.
Definition R_regs_preserved_v (rn : Z) := Z.land rn (Z.ones 64).
Lemma R_regs_preserved_set_reg
(rn : Z)
(b : bool) :
(if b then False else False) ->
R_regs_preserved_v rn = 0%Z.
Proof.
intros XXX.
vm_compute (length) in *.
destruct b eqn:?.
all: contradiction.
Show Proof.
(*
(fun (rn : Z) (b : bool) (XXX : if b then False else False) =>
(let b0 := b in
let Heqb0 : b = b0 := eq_refl in
(if b0 as b1 return b = b1 -> (if b1 then False else False) -> R_regs_preserved_v rn = 0%Z
then fun (_ : b = true) (XXX0 : False) => False_ind (R_regs_preserved_v rn = 0%Z) XXX0
else fun (_ : b = false) (XXX0 : False) => False_ind (R_regs_preserved_v rn = 0%Z) XXX0) Heqb0 XXX)
<:
R_regs_preserved_v rn = 0%Z)
*)
Timeout 2 Qed.The bomb is clearly Not sure what to do. I do think though it's a bit crazy that fiat-crypto leaves ticking computational bombs around without any kind of locking. |
Member
Insofar as this is an accurate representation of what's happening, I think we should replace vm_compute with compute or lazy (assuming they have the same behavior modulo the type of cast node). I believe this code probably predates the insertion of vm cast nodes, and we definitely don't want to be inserting cast nodes that demand full reduction on both sides when the proof script is only partially reducing. (It would be a different story if we were invoking vm_compute without an argument.) |
Member
I think we broadly aim for the opposite approach in fiat-crypto: we try to whitelist reduction rather then blacklist it with locking. |
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
3 participants
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.
When the expand_let typing flag is set in the environment, we change the kernel typing rule for let-bindings from
to
We cannot do this by default since it may change the inferred type for some expressions, which is returned when the expected type is not provided. To work around this, we statically set the flag in expressions for which the precise inferred type is not relevant. For now there is no user-facing flag that would allow setting this option in a more fine-grained way though, but it is easy to fix.
This is a revival of #13606 and a partial fix of #11838. The latter still suffers from superlinear blowups in unrelated parts of the kernel, namely VM and native compilation.