Ltac1 and Ltac2: don't normalize evars for open_constr:() #17704
Conversation
This file contains 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
SkySkimmer
added
the
request: full CI
coqbot-app
bot
removed
the
request: full CI
|
@coqbot bench |
|
🏁 Bench results: INFO: failed to install 🐢 Top 25 slow downs┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 141.2530 142.3930 1.1400 0.81% 1190 coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html │ │ 61.9490 62.8900 0.9410 1.52% 139 coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html │ │ 129.7010 130.4230 0.7220 0.56% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 2.2310 2.8690 0.6380 28.60% 122 coq-stdlib/setoid_ring/Ncring_initial.v.html │ │ 1.8510 2.4850 0.6340 34.25% 209 coq-stdlib/setoid_ring/Ncring_tac.v.html │ │ 130.0100 130.5930 0.5830 0.45% 968 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 2.9820 3.5430 0.5610 18.81% 487 coq-stdlib/Numbers/HexadecimalFacts.v.html │ │ 40.2460 40.7830 0.5370 1.33% 224 coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html │ │ 0.0050 0.5210 0.5160 10320.00% 753 coq-metacoq-pcuic/pcuic/theories/PCUICTyping.v.html │ │ 1.1080 1.4720 0.3640 32.85% 566 coq-stdlib/setoid_ring/Ncring_polynom.v.html │ │ 0.3510 0.6910 0.3400 96.87% 870 coq-stdlib/MSets/MSetRBT.v.html │ │ 0.0390 0.3690 0.3300 846.15% 1423 coq-perennial/src/program_proof/aof/proof.v.html │ │ 1.2420 1.5670 0.3250 26.17% 316 coq-stdlib/Strings/Byte.v.html │ │ 31.1520 31.4540 0.3020 0.97% 839 coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html │ │ 3.2430 3.5420 0.2990 9.22% 477 coq-perennial/src/program_proof/memkv/bank_proof.v.html │ │ 10.1030 10.3930 0.2900 2.87% 603 coq-unimath/UniMath/Algebra/GroupAction.v.html │ │ 16.0450 16.3330 0.2880 1.79% 31 coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html │ │ 4.3600 4.6030 0.2430 5.57% 102 coq-engine-bench-lite/coq/PerformanceDemos/rewrite_strat_repeated_app.v.html │ │ 2.6740 2.9140 0.2400 8.98% 1824 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Examples/KleisliEnriched.v.html │ │ 2.0180 2.2560 0.2380 11.79% 486 coq-perennial/src/program_proof/memkv/memkv_shard_clerk_proof.v.html │ │ 19.1300 19.3660 0.2360 1.23% 214 coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html │ │ 41.3810 41.6160 0.2350 0.57% 236 coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html │ │ 41.0940 41.3260 0.2320 0.56% 236 coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html │ │ 3.9300 4.1610 0.2310 5.88% 4414 coq-unimath/UniMath/HomologicalAlgebra/MappingCone.v.html │ │ 19.1350 19.3640 0.2290 1.20% 325 coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 20.3150 18.3780 -1.9370 -9.53% 808 coq-perennial/src/program_proof/wal/logger_proof.v.html │ │ 46.9470 45.5810 -1.3660 -2.91% 558 coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │ │ 81.0810 79.9060 -1.1750 -1.45% 618 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 35.9790 34.9060 -1.0730 -2.98% 12 coq-fourcolor/theories/job254to270.v.html │ │ 29.1460 28.5690 -0.5770 -1.98% 12 coq-fourcolor/theories/job517to530.v.html │ │ 34.4610 33.9670 -0.4940 -1.43% 12 coq-fourcolor/theories/job165to189.v.html │ │ 24.3280 23.8440 -0.4840 -1.99% 12 coq-fourcolor/theories/job542to545.v.html │ │ 5.8800 5.4350 -0.4450 -7.57% 167 coq-vst/veric/binop_lemmas6.v.html │ │ 33.3460 32.9080 -0.4380 -1.31% 12 coq-fourcolor/theories/job589to610.v.html │ │ 28.4760 28.0490 -0.4270 -1.50% 12 coq-fourcolor/theories/job291to294.v.html │ │ 1.4250 1.0210 -0.4040 -28.35% 372 coq-stdlib/setoid_ring/Ncring_polynom.v.html │ │ 21.2170 20.8380 -0.3790 -1.79% 12 coq-fourcolor/theories/job311to314.v.html │ │ 2.1770 1.8070 -0.3700 -17.00% 6 coq-mathcomp-algebra/mathcomp/algebra/intdiv.v.html │ │ 4.5380 4.1690 -0.3690 -8.13% 130 coq-category-theory/Functor/Strong/Product.v.html │ │ 27.3320 26.9660 -0.3660 -1.34% 12 coq-fourcolor/theories/job486to489.v.html │ │ 3.2230 2.8740 -0.3490 -10.83% 1409 coq-perennial/src/program_proof/wal/installer_proof.v.html │ │ 0.3340 0.0020 -0.3320 -99.40% 1451 coq-perennial/src/program_proof/aof/proof.v.html │ │ 30.1360 29.8110 -0.3250 -1.08% 12 coq-fourcolor/theories/job190to206.v.html │ │ 40.3780 40.0830 -0.2950 -0.73% 827 coq-vst/veric/binop_lemmas4.v.html │ │ 0.9180 0.6280 -0.2900 -31.59% 877 coq-metacoq-pcuic/pcuic/theories/PCUICTyping.v.html │ │ 27.3700 27.0830 -0.2870 -1.05% 12 coq-fourcolor/theories/job231to234.v.html │ │ 22.0920 21.8120 -0.2800 -1.27% 667 coq-perennial/src/program_proof/simplepb/pb_roapply_proof.v.html │ │ 11.1180 10.8580 -0.2600 -2.34% 88 coq-rewriter/src/Rewriter/Rewriter/Examples.v.html │ │ 32.4730 32.2150 -0.2580 -0.79% 12 coq-fourcolor/theories/job563to588.v.html │ │ 3.5630 3.3170 -0.2460 -6.90% 274 coq-perennial/src/program_proof/examples/dir_proof.v.html │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
|
🔴 CI failure at commit cecd173 without any failure in the test-suite ✔️ Corresponding job for the base commit 6e739ce succeeded ❔ Ask me to try to extract a minimal test case that can be added to the test-suite 🏃
|
|
@coqbot ci minimize |
|
I have initiated minimization at commit cecd173 for the suggested target ci-fiat_crypto as requested. |
|
Minimized File /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/src/PushButtonSynthesis/Primitives.v (from ci-fiat_crypto) (interrupted by timeout, being automatically continued) (full log on GitHub Actions) 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,unsupported-attributes" "-w" "-notation-overridden,-deprecated-hint-constr,-fragile-hint-constr,-native-compiler-disabled,-ambiguous-paths,-masking-absolute-name" "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" "-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/_build_ci/fiat_crypto/rupicola/bedrock2/deps/coqutil/src/coqutil" "coqutil" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/src/Rupicola" "Rupicola" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2" "bedrock2" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples" "bedrock2Examples" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/compiler/src/compiler" "compiler" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv" "riscv" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Bignums" "Bignums" "-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/Ltac2" "Ltac2" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Rewriter" "Rewriter" "-top" "Crypto.PushButtonSynthesis.Primitives") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 1498 lines to 11 lines, then from 24 lines to 324 lines, then from 329 lines to 52 lines, then from 65 lines to 384 lines, then from 389 lines to 57 lines, then from 70 lines to 840 lines, then from 845 lines to 118 lines, then from 131 lines to 380 lines, then from 385 lines to 130 lines, then from 143 lines to 339 lines, then from 344 lines to 132 lines *)
(* coqc version 8.18+alpha compiled with OCaml 4.14.1
coqtop version runner-vxtc-u6t-project-6138686-concurrent-0:/builds/coq/coq/_build/default,(HEAD detached at d7ce6d9) (d7ce6d9deac92848bd8420d857a18a96a87da88b)
Expected coqc runtime on this file: 10.177 sec *)
Require Crypto.Util.Tactics.SubstEvars.
Require Crypto.Util.ListUtil.Filter.
Require Crypto.Language.IdentifierParameters.
Require Rewriter.Util.plugins.RewriterBuildRegistry.
Declare ML Module "coq-rewriter.rewriter_build".
Import Crypto.Language.PreExtra.
Import Crypto.Language.IdentifierParameters.
Import Crypto.Util.ListUtil.Filter.
Module Export Compilers.
Import IdentifiersBasicGenerate.Compilers.Basic.
Rewriter Emit Inductives From Scraped
{| ScrapedData.base_type_list_named := base_type_list_named ; ScrapedData.all_ident_named_interped := all_ident_named_interped |}
As base ident raw_ident pattern_ident.
Definition package : GoalType.package_with_args scraped_data var_like_idents base ident.
Proof.
Tactic.make_package.
Defined.
Module Export APINotations.
Import Ltac2.Ltac2.
Module Export Compilers.
Export Reify.Compilers.
Import IdentifiersBasicGenerate.Compilers.Basic.Tactic.
Definition exprInfo : Classes.ExprInfoT := Eval hnf in GoalType.exprInfo package.
Global Existing Instances
baseHasNat
baseHasNatCorrect
try_make_base_transport_cps_correct
buildEagerIdent
buildInterpEagerIdentCorrect
toRestrictedIdent
toFromRestrictedIdent
buildInterpIdentCorrect
invertIdent
buildInvertIdentCorrect
base_default
exprInfo
.
Ltac2 mk_reify_base_type () :=
let package := reify_package_of_package 'package in
reify_base_type_via_reify_package package.
Ltac2 mk_reify_type () :=
let package := reify_package_of_package 'package in
reify_type_via_reify_package package.
Ltac2 mk_reify_ident_opt () :=
let package := reify_package_of_package 'package in
reify_ident_via_reify_package_opt package.
Ltac2 reify_type (ty : constr) : constr := mk_reify_type () ty.
#[deprecated(since="8.15",note="Use Ltac2 instead.")]
Ltac reify_type term :=
let f := ltac2:(term
|- Control.refine (fun () => reify_type (Option.get (Ltac1.to_constr term)))) in
constr:(ltac:(f term)).
Module Export base.
Notation type := (@base.type base) (only parsing).
Notation base_interp := Compilers.base_interp (only parsing).
Notation interp := (base.interp Compilers.base_interp) (only parsing).
End base.
Ltac2 _Reify_rhs () : unit :=
let reify_base_type := mk_reify_base_type () in
let reify_ident_opt := mk_reify_ident_opt () in
expr._Reify_rhs 'base.type 'ident reify_base_type reify_ident_opt '@base.interp '@ident_interp ().
Ltac Reify_rhs _ :=
ltac2:(_Reify_rhs ()).
Module Import invert_expr.
End invert_expr.
End Compilers.
End APINotations.
Notation Expr := (@expr.Expr base.type ident).
Notation Interp := (@expr.Interp base.type ident base.interp (@ident_interp)).
Notation reify_type t := (ltac:(let rt := reify_type t in exact rt)) (only parsing).
Notation reify_type_of e := (reify_type ((fun t (_ : t) => t) _ e)) (only parsing).
Import Coq.Relations.Relation_Definitions.
Import Crypto.Util.Tactics.SubstEvars.
Import Language.Wf.Compilers.
Fixpoint pointwise_equal {t} : relation (type.interp base.interp t)
:= match t with
| type.base t => Logic.eq
| type.arrow s d
=> fun (f g : type.interp base.interp s -> type.interp base.interp d)
=> forall x, pointwise_equal (f x) (g x)
end.
Definition is_reification_of' {t} (e : Expr t) (v : type.interp base.interp t) : Prop.
exact (pointwise_equal (Interp e) v /\ Wf e).
Defined.
Notation is_reification_of rop op
:= (match @is_reification_of' (reify_type_of op) rop op with
| T
=> ltac:(
let T := (eval cbv [pointwise_equal is_reification_of' T] in T) in
let T := (eval cbn [type.interp base.interp base.base_interp] in T) in
exact T)
end)
(only parsing).
Ltac cache_reify _ :=
split;
[ intros;
etransitivity;
[
| repeat match goal with |- _ = ?f' ?x => is_var x; apply (f_equal (fun f => f _)) end;
Reify_rhs ();
reflexivity ];
subst_evars;
reflexivity
| prove_Wf () ].
Import Coq.ZArith.ZArith.
Derive reified_id_gen
SuchThat (is_reification_of reified_id_gen (@id (list Z)))
As reified_id_gen_correct.
Proof.
Time cache_reify ().Intermediate Coq File (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 7.4MiB file on GitHub Actions Artifacts under
|
|
Minimized File /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/src/PushButtonSynthesis/Primitives.v (from ci-fiat_crypto) (interrupted by timeout, being automatically continued) (full log on GitHub Actions) Partially Minimized Coq File (could not inline Rewriter.Util.plugins.RewriterBuildRegistry) (truncated to 32KiB; full 35KiB file on GitHub Actions Artifacts under
|
|
Minimized File /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/src/PushButtonSynthesis/Primitives.v (from ci-fiat_crypto) (interrupted by timeout, being automatically continued) (full log on GitHub Actions) Partially Minimized Coq File (could not inline Rewriter.Util.plugins.RewriterBuildRegistry) (truncated to 32KiB; full 145KiB file on GitHub Actions Artifacts under
|
|
Minimized File /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/src/PushButtonSynthesis/Primitives.v (from ci-fiat_crypto) (interrupted by timeout, being automatically continued) (full log on GitHub Actions) Partially Minimized Coq File (could not inline Rewriter.Util.plugins.RewriterBuildRegistry)(* -*- 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,unsupported-attributes" "-w" "-notation-overridden,-deprecated-hint-constr,-fragile-hint-constr,-native-compiler-disabled,-ambiguous-paths,-masking-absolute-name" "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" "-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/_build_ci/fiat_crypto/rupicola/bedrock2/deps/coqutil/src/coqutil" "coqutil" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/src/Rupicola" "Rupicola" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2" "bedrock2" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples" "bedrock2Examples" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/compiler/src/compiler" "compiler" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv" "riscv" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Bignums" "Bignums" "-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/Ltac2" "Ltac2" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Rewriter" "Rewriter" "-top" "Top.bug_01") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 1498 lines to 11 lines, then from 24 lines to 324 lines, then from 329 lines to 52 lines, then from 65 lines to 384 lines, then from 389 lines to 57 lines, then from 70 lines to 840 lines, then from 845 lines to 118 lines, then from 131 lines to 380 lines, then from 385 lines to 130 lines, then from 143 lines to 339 lines, then from 344 lines to 132 lines, then from 150 lines to 132 lines, then from 145 lines to 478 lines, then from 484 lines to 255 lines, then from 269 lines to 501 lines, then from 506 lines to 351 lines, then from 365 lines to 694 lines, then from 699 lines to 825 lines, then from 833 lines to 357 lines, then from 370 lines to 564 lines, then from 570 lines to 377 lines, then from 391 lines to 987 lines, then from 992 lines to 377 lines, then from 391 lines to 3948 lines, then from 3948 lines to 4401 lines, then from 4405 lines to 389 lines, then from 402 lines to 615 lines, then from 621 lines to 464 lines *)
(* coqc version 8.18+alpha compiled with OCaml 4.14.1
coqtop version runner-vxtc-u6t-project-6138686-concurrent-0:/builds/coq/coq/_build/default,(HEAD detached at d7ce6d9) (d7ce6d9deac92848bd8420d857a18a96a87da88b)
Modules that could not be inlined: Rewriter.Util.plugins.RewriterBuildRegistry
Expected coqc runtime on this file: 9.060 sec *)
Require Coq.Init.Ltac.
Require Crypto.Util.Tactics.SubstEvars.
Require Coq.micromega.Lia.
Require Coq.Arith.Arith.
Require Coq.Lists.List.
Require Coq.Classes.Morphisms.
Require Crypto.Util.GlobalSettings.
Require Crypto.Util.FixCoqMistakes.
Require Crypto.Util.ListUtil.Filter.
Require Coq.Logic.Eqdep_dec.
Require Coq.NArith.BinNat.
Require Coq.Relations.Relation_Definitions.
Require Crypto.Util.ZUtil.Notations.
Require Crypto.Util.LetIn.
Require Crypto.Util.Decidable.
Require Rewriter.Util.plugins.RewriterBuildRegistry.
Import Coq.ZArith.ZArith.
Import Crypto.Util.Decidable.
Import Crypto.Util.ZUtil.Notations.
Import Crypto.Util.LetIn.
Local Open Scope Z_scope.
Module Export Z.
Definition zselect (cond zero_case nonzero_case : Z) :=
if cond =? 0 then zero_case else nonzero_case.
Definition add_modulo x y modulus :=
if (modulus <=? x + y) then (x + y) - modulus else (x + y).
Definition lnot_modulo (v : Z) (modulus : Z) : Z. exact (Z.lnot v mod modulus). Defined.
Definition bneg (v : Z) : Z. exact (if dec (v = 0) then 1 else 0). Defined.
Definition cc_m s x := if dec (2 ^ (Z.log2 s) = s) then x >> (Z.log2 s - 1) else x / (s / 2).
Definition rshi s hi lo n :=
let k := Z.log2 s in
if dec (2 ^ k = s)
then ((lo + (hi << k)) >> n) &' (Z.ones k)
else ((lo + hi * s) >> n) mod s.
Definition truncating_shiftl bw x n := (x << n) mod (2^bw).
Definition get_carry (bitwidth : Z) (v : Z) : Z * Z. exact ((v mod 2^bitwidth, v / 2^bitwidth)). Defined.
Definition add_with_carry (c : Z) (x y : Z) : Z. exact (c + x + y). Defined.
Definition add_with_get_carry (bitwidth : Z) (c : Z) (x y : Z) : Z * Z. exact (dlet v := add_with_carry c x y in get_carry bitwidth v). Defined.
Definition add_get_carry (bitwidth : Z) (x y : Z) : Z * Z. exact (add_with_get_carry bitwidth 0 x y). Defined.
Definition get_borrow (bitwidth : Z) (v : Z) : Z * Z. exact (let '(v, c) := get_carry bitwidth v in
(v, -c)). Defined.
Definition sub_with_borrow (c : Z) (x y : Z) : Z. exact (add_with_carry (-c) x (-y)). Defined.
Definition sub_with_get_borrow (bitwidth : Z) (c : Z) (x y : Z) : Z * Z. exact (dlet v := sub_with_borrow c x y in get_borrow bitwidth v). Defined.
Definition sub_get_borrow (bitwidth : Z) (x y : Z) : Z * Z. exact (sub_with_get_borrow bitwidth 0 x y). Defined.
Definition add_get_carry_full (bound : Z) (x y : Z) : Z * Z. exact (if 2 ^ (Z.log2 bound) =? bound
then add_get_carry (Z.log2 bound) x y
else ((x + y) mod bound, (x + y) / bound)). Defined.
Definition add_with_get_carry_full (bound : Z) (c x y : Z) : Z * Z. exact (if 2 ^ (Z.log2 bound) =? bound
then add_with_get_carry (Z.log2 bound) c x y
else ((c + x + y) mod bound, (c + x + y) / bound)). Defined.
Definition sub_get_borrow_full (bound : Z) (x y : Z) : Z * Z. exact (if 2 ^ (Z.log2 bound) =? bound
then sub_get_borrow (Z.log2 bound) x y
else ((x - y) mod bound, -((x - y) / bound))). Defined.
Definition sub_with_get_borrow_full (bound : Z) (c x y : Z) : Z * Z. exact (if 2 ^ (Z.log2 bound) =? bound
then sub_with_get_borrow (Z.log2 bound) c x y
else ((x - y - c) mod bound, -((x - y - c) / bound))). Defined.
Definition mul_split_at_bitwidth (bitwidth : Z) (x y : Z) : Z * Z. exact (dlet xy := x * y in
(if Z.geb bitwidth 0
then xy &' Z.ones bitwidth
else xy mod 2^bitwidth,
if Z.geb bitwidth 0
then xy >> bitwidth
else xy / 2^bitwidth)). Defined.
Definition mul_split (s x y : Z) : Z * Z. exact (if s =? 2^Z.log2 s
then mul_split_at_bitwidth (Z.log2 s) x y
else ((x * y) mod s, (x * y) / s)). Defined.
Definition mul_high (s x y : Z) : Z. exact (snd (mul_split s x y)). Defined.
Definition ltz (x y : Z) : Z. exact (if x <? y then 1 else 0). Defined.
Definition combine_at_bitwidth (bitwidth lo hi : Z) : Z. exact (lo + (hi << bitwidth)). Defined.
Definition value_barrier (x : Z) := x.
Import Coq.Lists.List.
Fixpoint update_nth {T} n f (xs:list T) {struct n} :=
match n with
| O => match xs with
| nil => nil
| x'::xs' => f x'::xs'
end
| S n' => match xs with
| nil => nil
| x'::xs' => x'::update_nth n' f xs'
end
end.
Import Coq.Bool.Bool.
Notation reflect_rel P b := (forall x y, reflect (P x y) (b x y)).
Module Export Crypto_DOT_Util_DOT_ZRange_WRAPPED.
Module Export ZRange.
Import Coq.ZArith.ZArith.
Declare Scope zrange_scope.
Record zrange := { lower : Z ; upper : Z }.
Bind Scope zrange_scope with zrange.
Scheme Minimality for zrange Sort Type.
Definition zrange_beq (x y : zrange) : bool.
Admitted.
Global Instance reflect_zrange_eq : reflect_rel (@eq zrange) zrange_beq | 10.
Admitted.
End ZRange.
End Crypto_DOT_Util_DOT_ZRange_WRAPPED.
Import Coq.ZArith.ZArith.
Module Export ZRange.
Definition normalize (v : zrange) : zrange.
Admitted.
Definition opp (v : zrange) : zrange.
Admitted.
Notation "- x" := (opp x) : zrange_scope.
Export Rewriter.Language.Pre.
Local Open Scope Z_scope.
Module Export ident.
Section cast.
Definition is_more_pos_than_neg (r : zrange) (v : BinInt.Z) : bool.
Admitted.
Let cast_outside_of_range (r : zrange) (v : BinInt.Z) : BinInt.Z.
Admitted.
Definition cast (r : zrange) (x : BinInt.Z)
:= let r := ZRange.normalize r in
if (lower r <=? x) && (x <=? upper r)
then x
else if is_more_pos_than_neg r x
then cast_outside_of_range r x
else -cast_outside_of_range (-r) (-x).
Definition cast2 (r : zrange * zrange) (x : BinInt.Z * BinInt.Z)
:= (cast (Datatypes.fst r) (Datatypes.fst x),
cast (Datatypes.snd r) (Datatypes.snd x)).
End cast.
Section comment.
Definition comment {A} (x : A) := tt.
Definition comment_no_keep {A} (x : A) := tt.
End comment.
Module Export fancy.
Module Export with_wordmax.
Section with_wordmax.
Context (log2wordmax : BinInt.Z).
Definition add (imm : Z) : Z * Z -> Z * Z.
Admitted.
Definition addc (imm : Z) : Z * Z * Z -> Z * Z.
Admitted.
Definition sub (imm : Z) : Z * Z -> Z * Z.
Admitted.
Definition subb (imm : Z) : Z * Z * Z -> Z * Z.
Admitted.
Definition mulll : Z * Z -> Z.
Admitted.
Definition mullh : Z * Z -> Z.
Admitted.
Definition mulhl : Z * Z -> Z.
Admitted.
Definition mulhh : Z * Z -> Z.
Admitted.
Definition selm : Z * Z * Z -> Z.
Admitted.
Definition rshi (n : Z) : Z * Z -> Z.
Admitted.
End with_wordmax.
End with_wordmax.
Definition add : (Z * Z) * (Z * Z) -> Z * Z
:= Eval cbv [with_wordmax.add] in fun x => with_wordmax.add (fst (fst x)) (snd (fst x)) (snd x).
Definition addc : (Z * Z) * (Z * Z * Z) -> Z * Z
:= Eval cbv [with_wordmax.addc] in fun x => with_wordmax.addc (fst (fst x)) (snd (fst x)) (snd x).
Definition sub : (Z * Z) * (Z * Z) -> Z * Z
:= Eval cbv [with_wordmax.sub] in fun x => with_wordmax.sub (fst (fst x)) (snd (fst x)) (snd x).
Definition subb : (Z * Z) * (Z * Z * Z) -> Z * Z
:= Eval cbv [with_wordmax.subb] in fun x => with_wordmax.subb (fst (fst x)) (snd (fst x)) (snd x).
Definition mulll : Z * (Z * Z) -> Z
:= Eval cbv [with_wordmax.mulll] in fun x => with_wordmax.mulll (fst x) (snd x).
Definition mullh : Z * (Z * Z) -> Z
:= Eval cbv [with_wordmax.mullh] in fun x => with_wordmax.mullh (fst x) (snd x).
Definition mulhl : Z * (Z * Z) -> Z
:= Eval cbv [with_wordmax.mulhl] in fun x => with_wordmax.mulhl (fst x) (snd x).
Definition mulhh : Z * (Z * Z) -> Z
:= Eval cbv [with_wordmax.mulhh] in fun x => with_wordmax.mulhh (fst x) (snd x).
Definition selm : Z * (Z * Z * Z) -> Z
:= Eval cbv [with_wordmax.selm] in fun x => with_wordmax.selm (fst x) (snd x).
Definition rshi : (Z * Z) * (Z * Z) -> Z
:= Eval cbv [with_wordmax.rshi] in fun x => with_wordmax.rshi (fst (fst x)) (snd (fst x)) (snd x).
Definition selc : Z * Z * Z -> Z.
Admitted.
Definition sell : Z * Z * Z -> Z.
Admitted.
Definition addm : Z * Z * Z -> Z.
Admitted.
Notation prod_rect_nodep := Rewriter.Util.Prod.prod_rect_nodep (only parsing).
Notation nat_rect_arrow_nodep := Rewriter.Util.NatUtil.nat_rect_arrow_nodep (only parsing).
Notation list_rect_arrow_nodep := Rewriter.Util.ListUtil.list_rect_arrow_nodep (only parsing).
Notation bool_rect_nodep := Rewriter.Util.Bool.bool_rect_nodep (only parsing).
Module Export Thunked.
Notation bool_rect := Rewriter.Util.Bool.Thunked.bool_rect (only parsing).
Notation list_rect := Rewriter.Util.ListUtil.Thunked.list_rect (only parsing).
Notation list_case := Rewriter.Util.ListUtil.Thunked.list_case (only parsing).
Notation nat_rect := Rewriter.Util.NatUtil.Thunked.nat_rect (only parsing).
Notation option_rect := Rewriter.Util.Option.Thunked.option_rect (only parsing).
Definition var_like_idents : InductiveHList.hlist.
Admitted.
Definition base_type_list_named : InductiveHList.hlist.
exact ([with_name Z BinInt.Z
; with_name bool Datatypes.bool
; with_name nat Datatypes.nat
; with_name zrange ZRange.zrange
; with_name string String.string]%hlist).
Defined.
Definition all_ident_named_interped : InductiveHList.hlist.
exact ([with_name ident_Literal (@ident.literal)
; with_name ident_comment (@ident.comment)
; with_name ident_comment_no_keep (@ident.comment_no_keep)
; with_name ident_value_barrier (@Z.value_barrier)
; with_name ident_Nat_succ Nat.succ
; with_name ident_Nat_pred Nat.pred
; with_name ident_Nat_max Nat.max
; with_name ident_Nat_mul Nat.mul
; with_name ident_Nat_add Nat.add
; with_name ident_Nat_sub Nat.sub
; with_name ident_Nat_eqb Nat.eqb
; with_name ident_nil (@Datatypes.nil)
; with_name ident_cons (@Datatypes.cons)
; with_name ident_tt Datatypes.tt
; with_name ident_pair (@Datatypes.pair)
; with_name ident_fst (@Datatypes.fst)
; with_name ident_snd (@Datatypes.snd)
; with_name ident_prod_rect (@prod_rect_nodep)
; with_name ident_bool_rect (@Thunked.bool_rect)
; with_name ident_bool_rect_nodep (@bool_rect_nodep)
; with_name ident_nat_rect (@Thunked.nat_rect)
; with_name ident_eager_nat_rect (ident.eagerly (@Thunked.nat_rect))
; with_name ident_nat_rect_arrow (@nat_rect_arrow_nodep)
; with_name ident_eager_nat_rect_arrow (ident.eagerly (@nat_rect_arrow_nodep))
; with_name ident_list_rect (@Thunked.list_rect)
; with_name ident_eager_list_rect (ident.eagerly (@Thunked.list_rect))
; with_name ident_list_rect_arrow (@list_rect_arrow_nodep)
; with_name ident_eager_list_rect_arrow (ident.eagerly (@list_rect_arrow_nodep))
; with_name ident_list_case (@Thunked.list_case)
; with_name ident_List_length (@List.length)
; with_name ident_List_seq (@List.seq)
; with_name ident_List_firstn (@List.firstn)
; with_name ident_List_skipn (@List.skipn)
; with_name ident_List_repeat (@repeat)
; with_name ident_List_combine (@List.combine)
; with_name ident_List_map (@List.map)
; with_name ident_List_app (@List.app)
; with_name ident_List_rev (@List.rev)
; with_name ident_List_flat_map (@List.flat_map)
; with_name ident_List_partition (@List.partition)
; with_name ident_List_filter (@List.filter)
; with_name ident_List_fold_right (@List.fold_right)
; with_name ident_List_update_nth (@update_nth)
; with_name ident_List_nth_default (@nth_default)
; with_name ident_eager_List_nth_default (ident.eagerly (@nth_default))
; with_name ident_Z_add Z.add
; with_name ident_Z_mul Z.mul
; with_name ident_Z_pow Z.pow
; with_name ident_Z_sub Z.sub
; with_name ident_Z_opp Z.opp
; with_name ident_Z_div Z.div
; with_name ident_Z_modulo Z.modulo
; with_name ident_Z_eqb Z.eqb
; with_name ident_Z_leb Z.leb
; with_name ident_Z_ltb Z.ltb
; with_name ident_Z_geb Z.geb
; with_name ident_Z_gtb Z.gtb
; with_name ident_Z_log2 Z.log2
; with_name ident_Z_log2_up Z.log2_up
; with_name ident_Z_of_nat Z.of_nat
; with_name ident_Z_to_nat Z.to_nat
; with_name ident_Z_shiftr Z.shiftr
; with_name ident_Z_shiftl Z.shiftl
; with_name ident_Z_land Z.land
; with_name ident_Z_lor Z.lor
; with_name ident_Z_min Z.min
; with_name ident_Z_max Z.max
; with_name ident_Z_mul_split Z.mul_split
; with_name ident_Z_mul_high Z.mul_high
; with_name ident_Z_add_get_carry Z.add_get_carry_full
; with_name ident_Z_add_with_carry Z.add_with_carry
; with_name ident_Z_add_with_get_carry Z.add_with_get_carry_full
; with_name ident_Z_sub_get_borrow Z.sub_get_borrow_full
; with_name ident_Z_sub_with_get_borrow Z.sub_with_get_borrow_full
; with_name ident_Z_ltz Z.ltz
; with_name ident_Z_zselect Z.zselect
; with_name ident_Z_add_modulo Z.add_modulo
; with_name ident_Z_truncating_shiftl Z.truncating_shiftl
; with_name ident_Z_bneg Z.bneg
; with_name ident_Z_lnot_modulo Z.lnot_modulo
; with_name ident_Z_lxor Z.lxor
; with_name ident_Z_rshi Z.rshi
; with_name ident_Z_cc_m Z.cc_m
; with_name ident_Z_combine_at_bitwidth Z.combine_at_bitwidth
; with_name ident_Z_cast ident.cast
; with_name ident_Z_cast2 ident.cast2
; with_name ident_Some (@Datatypes.Some)
; with_name ident_None (@Datatypes.None)
; with_name ident_option_rect (@Thunked.option_rect)
; with_name ident_Build_zrange ZRange.Build_zrange
; with_name ident_zrange_rect (@ZRange.zrange_rect_nodep)
; with_name ident_fancy_add ident.fancy.add
; with_name ident_fancy_addc ident.fancy.addc
; with_name ident_fancy_sub ident.fancy.sub
; with_name ident_fancy_subb ident.fancy.subb
; with_name ident_fancy_mulll ident.fancy.mulll
; with_name ident_fancy_mullh ident.fancy.mullh
; with_name ident_fancy_mulhl ident.fancy.mulhl
; with_name ident_fancy_mulhh ident.fancy.mulhh
; with_name ident_fancy_rshi ident.fancy.rshi
; with_name ident_fancy_selc ident.fancy.selc
; with_name ident_fancy_selm ident.fancy.selm
; with_name ident_fancy_sell ident.fancy.sell
; with_name ident_fancy_addm ident.fancy.addm
]%hlist).
Defined.
Definition scraped_data : ScrapedData.t.
exact ({| ScrapedData.base_type_list_named := base_type_list_named
; ScrapedData.all_ident_named_interped := all_ident_named_interped |}).
Defined.
Declare ML Module "coq-rewriter.rewriter_build".
Import Crypto.Util.ListUtil.Filter.
Module Export Compilers.
Import IdentifiersBasicGenerate.Compilers.Basic.
Rewriter Emit Inductives From Scraped
{| ScrapedData.base_type_list_named := base_type_list_named ; ScrapedData.all_ident_named_interped := all_ident_named_interped |}
As base ident raw_ident pattern_ident.
Definition package : GoalType.package_with_args scraped_data var_like_idents base ident.
Proof.
Tactic.make_package.
Defined.
Module Export APINotations.
Import Ltac2.Ltac2.
Module Export Compilers.
Export Reify.Compilers.
Import IdentifiersBasicGenerate.Compilers.Basic.Tactic.
Definition exprInfo : Classes.ExprInfoT := Eval hnf in GoalType.exprInfo package.
Global Existing Instances
baseHasNat
baseHasNatCorrect
try_make_base_transport_cps_correct
buildEagerIdent
buildInterpEagerIdentCorrect
toRestrictedIdent
toFromRestrictedIdent
buildInterpIdentCorrect
invertIdent
buildInvertIdentCorrect
base_default
exprInfo
.
Ltac2 mk_reify_base_type () :=
let package := reify_package_of_package 'package in
reify_base_type_via_reify_package package.
Ltac2 mk_reify_type () :=
let package := reify_package_of_package 'package in
reify_type_via_reify_package package.
Ltac2 mk_reify_ident_opt () :=
let package := reify_package_of_package 'package in
reify_ident_via_reify_package_opt package.
Ltac2 reify_type (ty : constr) : constr := mk_reify_type () ty.
#[deprecated(since="8.15",note="Use Ltac2 instead.")]
Ltac reify_type term :=
let f := ltac2:(term
|- Control.refine (fun () => reify_type (Option.get (Ltac1.to_constr term)))) in
constr:(ltac:(f term)).
Module Export base.
Notation type := (@base.type base) (only parsing).
Notation base_interp := Compilers.base_interp (only parsing).
Notation interp := (base.interp Compilers.base_interp) (only parsing).
End base.
Ltac2 _Reify_rhs () : unit :=
let reify_base_type := mk_reify_base_type () in
let reify_ident_opt := mk_reify_ident_opt () in
expr._Reify_rhs 'base.type 'ident reify_base_type reify_ident_opt '@base.interp '@ident_interp ().
Ltac Reify_rhs _ :=
ltac2:(_Reify_rhs ()).
Module Import invert_expr.
End invert_expr.
End Compilers.
End APINotations.
Notation Expr := (@expr.Expr base.type ident).
Notation Interp := (@expr.Interp base.type ident base.interp (@ident_interp)).
Notation reify_type t := (ltac:(let rt := reify_type t in exact rt)) (only parsing).
Notation reify_type_of e := (reify_type ((fun t (_ : t) => t) _ e)) (only parsing).
Import Coq.Relations.Relation_Definitions.
Import Crypto.Util.Tactics.SubstEvars.
Import Language.Wf.Compilers.
Fixpoint pointwise_equal {t} : relation (type.interp base.interp t)
:= match t with
| type.base t => Logic.eq
| type.arrow s d
=> fun (f g : type.interp base.interp s -> type.interp base.interp d)
=> forall x, pointwise_equal (f x) (g x)
end.
Definition is_reification_of' {t} (e : Expr t) (v : type.interp base.interp t) : Prop.
exact (pointwise_equal (Interp e) v /\ Wf e).
Defined.
Notation is_reification_of rop op
:= (match @is_reification_of' (reify_type_of op) rop op with
| T
=> ltac:(
let T := (eval cbv [pointwise_equal is_reification_of' T] in T) in
let T := (eval cbn [type.interp base.interp base.base_interp] in T) in
exact T)
end)
(only parsing).
Ltac cache_reify _ :=
split;
[ intros;
etransitivity;
[
| repeat match goal with |- _ = ?f' ?x => is_var x; apply (f_equal (fun f => f _)) end;
Reify_rhs ();
reflexivity ];
subst_evars;
reflexivity
| prove_Wf () ].
Import Coq.ZArith.ZArith.
Derive reified_id_gen
SuchThat (is_reification_of reified_id_gen (@id (list Z)))
As reified_id_gen_correct.
Proof.
Time cache_reify ().Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted) (truncated to 8.0KiB; full 26KiB file on GitHub Actions Artifacts under
|
|
Minimized File /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/src/PushButtonSynthesis/Primitives.v (from ci-fiat_crypto) (interrupted by timeout, being automatically continued) (full log on GitHub Actions) Partially Minimized Coq File (could not inline Rewriter.Util.plugins.RewriterBuildRegistry)(* -*- 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,unsupported-attributes" "-w" "-notation-overridden,-deprecated-hint-constr,-fragile-hint-constr,-native-compiler-disabled,-ambiguous-paths,-masking-absolute-name" "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" "-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/_build_ci/fiat_crypto/rupicola/bedrock2/deps/coqutil/src/coqutil" "coqutil" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/src/Rupicola" "Rupicola" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2" "bedrock2" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples" "bedrock2Examples" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/compiler/src/compiler" "compiler" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv" "riscv" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Bignums" "Bignums" "-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/Ltac2" "Ltac2" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Rewriter" "Rewriter" "-top" "Top.bug_01") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 1498 lines to 11 lines, then from 24 lines to 324 lines, then from 329 lines to 52 lines, then from 65 lines to 384 lines, then from 389 lines to 57 lines, then from 70 lines to 840 lines, then from 845 lines to 118 lines, then from 131 lines to 380 lines, then from 385 lines to 130 lines, then from 143 lines to 339 lines, then from 344 lines to 132 lines, then from 150 lines to 132 lines, then from 145 lines to 478 lines, then from 484 lines to 255 lines, then from 269 lines to 501 lines, then from 506 lines to 351 lines, then from 365 lines to 694 lines, then from 699 lines to 825 lines, then from 833 lines to 357 lines, then from 370 lines to 564 lines, then from 570 lines to 377 lines, then from 391 lines to 987 lines, then from 992 lines to 377 lines, then from 391 lines to 3948 lines, then from 3948 lines to 4401 lines, then from 4405 lines to 389 lines, then from 402 lines to 615 lines, then from 621 lines to 464 lines, then from 478 lines to 431 lines, then from 444 lines to 700 lines, then from 706 lines to 435 lines, then from 449 lines to 476 lines, then from 482 lines to 549 lines *)
(* coqc version 8.18+alpha compiled with OCaml 4.14.1
coqtop version runner-vxtc-u6t-project-6138686-concurrent-0:/builds/coq/coq/_build/default,(HEAD detached at d7ce6d9) (d7ce6d9deac92848bd8420d857a18a96a87da88b)
Modules that could not be inlined: Rewriter.Util.plugins.RewriterBuildRegistry
Expected coqc runtime on this file: 10.096 sec *)
Require Coq.Init.Ltac.
Require Crypto.Util.Tactics.SubstEvars.
Require Coq.micromega.Lia.
Require Coq.Arith.Arith.
Require Coq.Lists.List.
Require Coq.Classes.Morphisms.
Require Crypto.Util.GlobalSettings.
Require Crypto.Util.FixCoqMistakes.
Require Crypto.Util.ListUtil.Filter.
Require Coq.ZArith.BinInt.
Require Crypto.Util.Notations.
Require Rewriter.Util.GlobalSettings.
Require Rewriter.Util.FixCoqMistakes.
Require Rewriter.Util.Notations.
Require Ltac2.Init.
Require Coq.Classes.RelationClasses.
Require Rewriter.Util.IffT.
Require Rewriter.Util.Isomorphism.
Require Rewriter.Util.HProp.
Require Rewriter.Util.Equality.
Require Rewriter.Util.PrimitiveProd.
Require Rewriter.Util.PrimitiveHList.
Require Rewriter.Util.InductiveHList.
Require Rewriter.Language.PreCommon.
Require Rewriter.Language.Pre.
Require Coq.Bool.Bool.
Require Rewriter.Util.Bool.
Require Coq.Logic.Eqdep_dec.
Require Coq.NArith.NArith.
Require Coq.Numbers.Natural.Peano.NPeano.
Require Coq.Relations.Relation_Definitions.
Require Rewriter.Util.NatUtil.
Require Coq.Lists.SetoidList.
Require Coq.Arith.Peano_dec.
Require Coq.ZArith.ZArith.
Require Coq.Numbers.BinNums.
Require Rewriter.Util.Pointed.
Require Coq.Setoids.Setoid.
Require Rewriter.Util.Prod.
Require Rewriter.Util.Sigma.
Require Coq.ZArith.ZArith_dec.
Require Coq.NArith.BinNat.
Require Rewriter.Util.Decidable.
Require Rewriter.Util.Tactics.Head.
Require Rewriter.Util.Tactics.BreakMatch.
Require Rewriter.Util.Tactics.DestructHyps.
Require Rewriter.Util.Tactics.DestructHead.
Require Rewriter.Util.Option.
Require Rewriter.Util.Tactics.SpecializeBy.
Require Rewriter.Util.Tactics.Test.
Require Rewriter.Util.Tactics.Not.
Require Rewriter.Util.Tactics.DoWithHyp.
Require Rewriter.Util.Tactics.RewriteHyp.
Require Rewriter.Util.Tactics.ConstrFail.
Require Rewriter.Util.Tactics.SplitInContext.
Require Rewriter.Util.ListUtil.
Require Rewriter.Language.PreLemmas.
Require Ltac2.Int.
Require Ltac2.Message.
Require Ltac2.Control.
Require Ltac2.Bool.
Require Ltac2.Array.
Require Ltac2.Char.
Require Ltac2.Constant.
Require Ltac2.Constr.
Require Ltac2.Constructor.
Require Ltac2.Std.
Require Ltac2.Env.
Require Ltac2.Evar.
Require Ltac2.Float.
Require Ltac2.List.
Require Ltac2.Fresh.
Require Ltac2.Ident.
Require Ltac2.Ind.
Require Ltac2.Ltac1.
Require Ltac2.Meta.
Require Ltac2.Option.
Require Ltac2.Pattern.
Require Ltac2.Printf.
Require Ltac2.Proj.
Require Ltac2.String.
Require Ltac2.Uint63.
Require Ltac2.FSet.
Require Ltac2.FMap.
Require Ltac2.Notations.
Require Ltac2.Ltac2.
Require Coq.FSets.FMapPositive.
Require Rewriter.Util.Tactics.GetGoal.
Require Rewriter.Util.LetIn.
Require Rewriter.Util.OptionList.
Require Rewriter.Util.CPSNotations.
Require Coq.Classes.CMorphisms.
Require Coq.Strings.String.
Require Coq.Strings.Ascii.
Require Rewriter.Util.ListUtil.SetoidList.
Require Rewriter.Util.Tactics.Contains.
Require Rewriter.Util.Tactics.SetoidSubst.
Require Rewriter.Util.Sum.
Require Rewriter.Util.Comparison.
Require Rewriter.Util.Bool.Reflect.
Require Rewriter.Language.Language.
Require Rewriter.Language.UnderLets.
Require Rewriter.Language.UnderLetsCacheProofs.
Require Rewriter.Util.Tactics.RunTacticAsConstr.
Require Rewriter.Util.Tactics.DebugPrint.
Require Rewriter.Util.Tactics2.List.
Require Rewriter.Util.Tactics2.Ltac1.
Require Rewriter.Util.Tactics2.Message.
Require Rewriter.Util.Tactics2.Ident.
Require Rewriter.Util.Tactics2.Char.
Require Rewriter.Util.Tactics2.String.
Require Rewriter.Util.Tactics2.Array.
Require Rewriter.Util.plugins.RewriterBuildRegistry.
Import Coq.ZArith.BinInt.
Import Crypto.Util.Notations.
Infix ">>" := Z.shiftr : Z_scope.
Infix "<<" := Z.shiftl : Z_scope.
Infix "&'" := Z.land : Z_scope.
Import Coq.ZArith.BinInt.
Class Decidable (P : Prop) := dec : {P} + {~P}.
Arguments dec _%type_scope {_}.
Notation DecidableRel R := (forall x y, Decidable (R x y)).
Global Instance dec_eq_Z : DecidableRel (@eq Z) | 10.
Admitted.
Local Open Scope Z_scope.
Module Export Z.
Definition zselect (cond zero_case nonzero_case : Z) :=
if cond =? 0 then zero_case else nonzero_case.
Definition add_modulo x y modulus :=
if (modulus <=? x + y) then (x + y) - modulus else (x + y).
Definition lnot_modulo (v : Z) (modulus : Z) : Z.
Admitted.
Definition bneg (v : Z) : Z.
Admitted.
Definition cc_m s x := if dec (2 ^ (Z.log2 s) = s) then x >> (Z.log2 s - 1) else x / (s / 2).
Definition rshi s hi lo n :=
let k := Z.log2 s in
if dec (2 ^ k = s)
then ((lo + (hi << k)) >> n) &' (Z.ones k)
else ((lo + hi * s) >> n) mod s.
Definition truncating_shiftl bw x n := (x << n) mod (2^bw).
Definition add_with_carry (c : Z) (x y : Z) : Z.
Admitted.
Definition add_get_carry_full (bound : Z) (x y : Z) : Z * Z.
Admitted.
Definition add_with_get_carry_full (bound : Z) (c x y : Z) : Z * Z.
Admitted.
Definition sub_get_borrow_full (bound : Z) (x y : Z) : Z * Z.
Admitted.
Definition sub_with_get_borrow_full (bound : Z) (c x y : Z) : Z * Z.
Admitted.
Definition mul_split (s x y : Z) : Z * Z.
Admitted.
Definition mul_high (s x y : Z) : Z.
Admitted.
Definition ltz (x y : Z) : Z.
Admitted.
Definition combine_at_bitwidth (bitwidth lo hi : Z) : Z.
Admitted.
Definition value_barrier (x : Z) := x.
Import Coq.Lists.List.
Fixpoint update_nth {T} n f (xs:list T) {struct n} :=
match n with
| O => match xs with
| nil => nil
| x'::xs' => f x'::xs'
end
| S n' => match xs with
| nil => nil
| x'::xs' => x'::update_nth n' f xs'
end
end.
Import Coq.Bool.Bool.
Notation reflect_rel P b := (forall x y, reflect (P x y) (b x y)).
Module Export Crypto_DOT_Util_DOT_ZRange_WRAPPED.
Module Export ZRange.
Declare Scope zrange_scope.
Record zrange := { lower : Z ; upper : Z }.
Bind Scope zrange_scope with zrange.
Scheme Minimality for zrange Sort Type.
Definition zrange_beq (x y : zrange) : bool.
Admitted.
Global Instance reflect_zrange_eq : reflect_rel (@eq zrange) zrange_beq | 10.
Admitted.
End ZRange.
End Crypto_DOT_Util_DOT_ZRange_WRAPPED.
Module Export ZRange.
Definition normalize (v : zrange) : zrange.
Admitted.
Definition opp (v : zrange) : zrange.
Admitted.
Notation "- x" := (opp x) : zrange_scope.
Export Rewriter.Language.Pre.
Module Export ident.
Section cast.
Definition is_more_pos_than_neg (r : zrange) (v : BinInt.Z) : bool.
Admitted.
Let cast_outside_of_range (r : zrange) (v : BinInt.Z) : BinInt.Z.
Admitted.
Definition cast (r : zrange) (x : BinInt.Z)
:= let r := ZRange.normalize r in
if (lower r <=? x) && (x <=? upper r)
then x
else if is_more_pos_than_neg r x
then cast_outside_of_range r x
else -cast_outside_of_range (-r) (-x).
Definition cast2 (r : zrange * zrange) (x : BinInt.Z * BinInt.Z)
:= (cast (Datatypes.fst r) (Datatypes.fst x),
cast (Datatypes.snd r) (Datatypes.snd x)).
End cast.
Section comment.
Definition comment {A} (x : A) := tt.
Definition comment_no_keep {A} (x : A) := tt.
End comment.
Module Export fancy.
Module Export with_wordmax.
Section with_wordmax.
Context (log2wordmax : BinInt.Z).
Definition add (imm : Z) : Z * Z -> Z * Z.
Admitted.
Definition addc (imm : Z) : Z * Z * Z -> Z * Z.
Admitted.
Definition sub (imm : Z) : Z * Z -> Z * Z.
Admitted.
Definition subb (imm : Z) : Z * Z * Z -> Z * Z.
Admitted.
Definition mulll : Z * Z -> Z.
Admitted.
Definition mullh : Z * Z -> Z.
Admitted.
Definition mulhl : Z * Z -> Z.
Admitted.
Definition mulhh : Z * Z -> Z.
Admitted.
Definition selm : Z * Z * Z -> Z.
Admitted.
Definition rshi (n : Z) : Z * Z -> Z.
Admitted.
End with_wordmax.
End with_wordmax.
Definition add : (Z * Z) * (Z * Z) -> Z * Z
:= Eval cbv [with_wordmax.add] in fun x => with_wordmax.add (fst (fst x)) (snd (fst x)) (snd x).
Definition addc : (Z * Z) * (Z * Z * Z) -> Z * Z
:= Eval cbv [with_wordmax.addc] in fun x => with_wordmax.addc (fst (fst x)) (snd (fst x)) (snd x).
Definition sub : (Z * Z) * (Z * Z) -> Z * Z
:= Eval cbv [with_wordmax.sub] in fun x => with_wordmax.sub (fst (fst x)) (snd (fst x)) (snd x).
Definition subb : (Z * Z) * (Z * Z * Z) -> Z * Z
:= Eval cbv [with_wordmax.subb] in fun x => with_wordmax.subb (fst (fst x)) (snd (fst x)) (snd x).
Definition mulll : Z * (Z * Z) -> Z
:= Eval cbv [with_wordmax.mulll] in fun x => with_wordmax.mulll (fst x) (snd x).
Definition mullh : Z * (Z * Z) -> Z
:= Eval cbv [with_wordmax.mullh] in fun x => with_wordmax.mullh (fst x) (snd x).
Definition mulhl : Z * (Z * Z) -> Z
:= Eval cbv [with_wordmax.mulhl] in fun x => with_wordmax.mulhl (fst x) (snd x).
Definition mulhh : Z * (Z * Z) -> Z
:= Eval cbv [with_wordmax.mulhh] in fun x => with_wordmax.mulhh (fst x) (snd x).
Definition selm : Z * (Z * Z * Z) -> Z
:= Eval cbv [with_wordmax.selm] in fun x => with_wordmax.selm (fst x) (snd x).
Definition rshi : (Z * Z) * (Z * Z) -> Z
:= Eval cbv [with_wordmax.rshi] in fun x => with_wordmax.rshi (fst (fst x)) (snd (fst x)) (snd x).
Definition selc : Z * Z * Z -> Z.
Admitted.
Definition sell : Z * Z * Z -> Z.
Admitted.
Definition addm : Z * Z * Z -> Z.
Admitted.
Notation prod_rect_nodep := Rewriter.Util.Prod.prod_rect_nodep (only parsing).
Notation nat_rect_arrow_nodep := Rewriter.Util.NatUtil.nat_rect_arrow_nodep (only parsing).
Notation list_rect_arrow_nodep := Rewriter.Util.ListUtil.list_rect_arrow_nodep (only parsing).
Notation bool_rect_nodep := Rewriter.Util.Bool.bool_rect_nodep (only parsing).
Module Export Thunked.
Notation bool_rect := Rewriter.Util.Bool.Thunked.bool_rect (only parsing).
Notation list_rect := Rewriter.Util.ListUtil.Thunked.list_rect (only parsing).
Notation list_case := Rewriter.Util.ListUtil.Thunked.list_case (only parsing).
Notation nat_rect := Rewriter.Util.NatUtil.Thunked.nat_rect (only parsing).
Notation option_rect := Rewriter.Util.Option.Thunked.option_rect (only parsing).
Definition var_like_idents : InductiveHList.hlist.
Admitted.
Definition base_type_list_named : InductiveHList.hlist.
exact ([with_name Z BinInt.Z
; with_name bool Datatypes.bool
; with_name nat Datatypes.nat
; with_name zrange ZRange.zrange
; with_name string String.string]%hlist).
Defined.
Definition all_ident_named_interped : InductiveHList.hlist.
exact ([with_name ident_Literal (@ident.literal)
; with_name ident_comment (@ident.comment)
; with_name ident_comment_no_keep (@ident.comment_no_keep)
; with_name ident_value_barrier (@Z.value_barrier)
; with_name ident_Nat_succ Nat.succ
; with_name ident_Nat_pred Nat.pred
; with_name ident_Nat_max Nat.max
; with_name ident_Nat_mul Nat.mul
; with_name ident_Nat_add Nat.add
; with_name ident_Nat_sub Nat.sub
; with_name ident_Nat_eqb Nat.eqb
; with_name ident_nil (@Datatypes.nil)
; with_name ident_cons (@Datatypes.cons)
; with_name ident_tt Datatypes.tt
; with_name ident_pair (@Datatypes.pair)
; with_name ident_fst (@Datatypes.fst)
; with_name ident_snd (@Datatypes.snd)
; with_name ident_prod_rect (@prod_rect_nodep)
; with_name ident_bool_rect (@Thunked.bool_rect)
; with_name ident_bool_rect_nodep (@bool_rect_nodep)
; with_name ident_nat_rect (@Thunked.nat_rect)
; with_name ident_eager_nat_rect (ident.eagerly (@Thunked.nat_rect))
; with_name ident_nat_rect_arrow (@nat_rect_arrow_nodep)
; with_name ident_eager_nat_rect_arrow (ident.eagerly (@nat_rect_arrow_nodep))
; with_name ident_list_rect (@Thunked.list_rect)
; with_name ident_eager_list_rect (ident.eagerly (@Thunked.list_rect))
; with_name ident_list_rect_arrow (@list_rect_arrow_nodep)
; with_name ident_eager_list_rect_arrow (ident.eagerly (@list_rect_arrow_nodep))
; with_name ident_list_case (@Thunked.list_case)
; with_name ident_List_length (@List.length)
; with_name ident_List_seq (@List.seq)
; with_name ident_List_firstn (@List.firstn)
; with_name ident_List_skipn (@List.skipn)
; with_name ident_List_repeat (@repeat)
; with_name ident_List_combine (@List.combine)
; with_name ident_List_map (@List.map)
; with_name ident_List_app (@List.app)
; with_name ident_List_rev (@List.rev)
; with_name ident_List_flat_map (@List.flat_map)
; with_name ident_List_partition (@List.partition)
; with_name ident_List_filter (@List.filter)
; with_name ident_List_fold_right (@List.fold_right)
; with_name ident_List_update_nth (@update_nth)
; with_name ident_List_nth_default (@nth_default)
; with_name ident_eager_List_nth_default (ident.eagerly (@nth_default))
; with_name ident_Z_add Z.add
; with_name ident_Z_mul Z.mul
; with_name ident_Z_pow Z.pow
; with_name ident_Z_sub Z.sub
; with_name ident_Z_opp Z.opp
; with_name ident_Z_div Z.div
; with_name ident_Z_modulo Z.modulo
; with_name ident_Z_eqb Z.eqb
; with_name ident_Z_leb Z.leb
; with_name ident_Z_ltb Z.ltb
; with_name ident_Z_geb Z.geb
; with_name ident_Z_gtb Z.gtb
; with_name ident_Z_log2 Z.log2
; with_name ident_Z_log2_up Z.log2_up
; with_name ident_Z_of_nat Z.of_nat
; with_name ident_Z_to_nat Z.to_nat
; with_name ident_Z_shiftr Z.shiftr
; with_name ident_Z_shiftl Z.shiftl
; with_name ident_Z_land Z.land
; with_name ident_Z_lor Z.lor
; with_name ident_Z_min Z.min
; with_name ident_Z_max Z.max
; with_name ident_Z_mul_split Z.mul_split
; with_name ident_Z_mul_high Z.mul_high
; with_name ident_Z_add_get_carry Z.add_get_carry_full
; with_name ident_Z_add_with_carry Z.add_with_carry
; with_name ident_Z_add_with_get_carry Z.add_with_get_carry_full
; with_name ident_Z_sub_get_borrow Z.sub_get_borrow_full
; with_name ident_Z_sub_with_get_borrow Z.sub_with_get_borrow_full
; with_name ident_Z_ltz Z.ltz
; with_name ident_Z_zselect Z.zselect
; with_name ident_Z_add_modulo Z.add_modulo
; with_name ident_Z_truncating_shiftl Z.truncating_shiftl
; with_name ident_Z_bneg Z.bneg
; with_name ident_Z_lnot_modulo Z.lnot_modulo
; with_name ident_Z_lxor Z.lxor
; with_name ident_Z_rshi Z.rshi
; with_name ident_Z_cc_m Z.cc_m
; with_name ident_Z_combine_at_bitwidth Z.combine_at_bitwidth
; with_name ident_Z_cast ident.cast
; with_name ident_Z_cast2 ident.cast2
; with_name ident_Some (@Datatypes.Some)
; with_name ident_None (@Datatypes.None)
; with_name ident_option_rect (@Thunked.option_rect)
; with_name ident_Build_zrange ZRange.Build_zrange
; with_name ident_zrange_rect (@ZRange.zrange_rect_nodep)
; with_name ident_fancy_add ident.fancy.add
; with_name ident_fancy_addc ident.fancy.addc
; with_name ident_fancy_sub ident.fancy.sub
; with_name ident_fancy_subb ident.fancy.subb
; with_name ident_fancy_mulll ident.fancy.mulll
; with_name ident_fancy_mullh ident.fancy.mullh
; with_name ident_fancy_mulhl ident.fancy.mulhl
; with_name ident_fancy_mulhh ident.fancy.mulhh
; with_name ident_fancy_rshi ident.fancy.rshi
; with_name ident_fancy_selc ident.fancy.selc
; with_name ident_fancy_selm ident.fancy.selm
; with_name ident_fancy_sell ident.fancy.sell
; with_name ident_fancy_addm ident.fancy.addm
]%hlist).
Defined.
Definition scraped_data : ScrapedData.t.
exact ({| ScrapedData.base_type_list_named := base_type_list_named
; ScrapedData.all_ident_named_interped := all_ident_named_interped |}).
Defined.
Declare ML Module "coq-rewriter.rewriter_build".
Import Crypto.Util.ListUtil.Filter.
Module Export Compilers.
Import IdentifiersBasicGenerate.Compilers.Basic.
Rewriter Emit Inductives From Scraped
{| ScrapedData.base_type_list_named := base_type_list_named ; ScrapedData.all_ident_named_interped := all_ident_named_interped |}
As base ident raw_ident pattern_ident.
Definition package : GoalType.package_with_args scraped_data var_like_idents base ident.
Proof.
Tactic.make_package.
Defined.
Module Export APINotations.
Import Ltac2.Ltac2.
Module Export Compilers.
Export Reify.Compilers.
Import IdentifiersBasicGenerate.Compilers.Basic.Tactic.
Definition exprInfo : Classes.ExprInfoT := Eval hnf in GoalType.exprInfo package.
Global Existing Instances
baseHasNat
baseHasNatCorrect
try_make_base_transport_cps_correct
buildEagerIdent
buildInterpEagerIdentCorrect
toRestrictedIdent
toFromRestrictedIdent
buildInterpIdentCorrect
invertIdent
buildInvertIdentCorrect
base_default
exprInfo
.
Ltac2 mk_reify_base_type () :=
let package := reify_package_of_package 'package in
reify_base_type_via_reify_package package.
Ltac2 mk_reify_type () :=
let package := reify_package_of_package 'package in
reify_type_via_reify_package package.
Ltac2 mk_reify_ident_opt () :=
let package := reify_package_of_package 'package in
reify_ident_via_reify_package_opt package.
Ltac2 reify_type (ty : constr) : constr := mk_reify_type () ty.
#[deprecated(since="8.15",note="Use Ltac2 instead.")]
Ltac reify_type term :=
let f := ltac2:(term
|- Control.refine (fun () => reify_type (Option.get (Ltac1.to_constr term)))) in
constr:(ltac:(f term)).
Module Export base.
Notation type := (@base.type base) (only parsing).
Notation base_interp := Compilers.base_interp (only parsing).
Notation interp := (base.interp Compilers.base_interp) (only parsing).
End base.
Ltac2 _Reify_rhs () : unit :=
let reify_base_type := mk_reify_base_type () in
let reify_ident_opt := mk_reify_ident_opt () in
expr._Reify_rhs 'base.type 'ident reify_base_type reify_ident_opt '@base.interp '@ident_interp ().
Ltac Reify_rhs _ :=
ltac2:(_Reify_rhs ()).
Module Import invert_expr.
End invert_expr.
End Compilers.
End APINotations.
Notation Expr := (@expr.Expr base.type ident).
Notation Interp := (@expr.Interp base.type ident base.interp (@ident_interp)).
Notation reify_type t := (ltac:(let rt := reify_type t in exact rt)) (only parsing).
Notation reify_type_of e := (reify_type ((fun t (_ : t) => t) _ e)) (only parsing).
Import Coq.Relations.Relation_Definitions.
Import Crypto.Util.Tactics.SubstEvars.
Import Language.Wf.Compilers.
Fixpoint pointwise_equal {t} : relation (type.interp base.interp t)
:= match t with
| type.base t => Logic.eq
| type.arrow s d
=> fun (f g : type.interp base.interp s -> type.interp base.interp d)
=> forall x, pointwise_equal (f x) (g x)
end.
Definition is_reification_of' {t} (e : Expr t) (v : type.interp base.interp t) : Prop.
exact (pointwise_equal (Interp e) v /\ Wf e).
Defined.
Notation is_reification_of rop op
:= (match @is_reification_of' (reify_type_of op) rop op with
| T
=> ltac:(
let T := (eval cbv [pointwise_equal is_reification_of' T] in T) in
let T := (eval cbn [type.interp base.interp base.base_interp] in T) in
exact T)
end)
(only parsing).
Ltac cache_reify _ :=
split;
[ intros;
etransitivity;
[
| repeat match goal with |- _ = ?f' ?x => is_var x; apply (f_equal (fun f => f _)) end;
Reify_rhs ();
reflexivity ];
subst_evars;
reflexivity
| prove_Wf () ].
Import Coq.ZArith.ZArith.
Derive reified_id_gen
SuchThat (is_reification_of reified_id_gen (@id (list Z)))
As reified_id_gen_correct.
Proof.
Time cache_reify ().Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted) (truncated to 8.0KiB; full 28KiB file on GitHub Actions Artifacts under
|
|
Minimized File /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/src/PushButtonSynthesis/Primitives.v (from ci-fiat_crypto) (interrupted by timeout, being automatically continued) (full log on GitHub Actions) Partially Minimized Coq File (could not inline Rewriter.Util.plugins.RewriterBuildRegistry)(* -*- 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,unsupported-attributes" "-w" "-notation-overridden,-deprecated-hint-constr,-fragile-hint-constr,-native-compiler-disabled,-ambiguous-paths,-masking-absolute-name" "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" "-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/_build_ci/fiat_crypto/rupicola/bedrock2/deps/coqutil/src/coqutil" "coqutil" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/src/Rupicola" "Rupicola" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2" "bedrock2" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples" "bedrock2Examples" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/compiler/src/compiler" "compiler" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv" "riscv" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Bignums" "Bignums" "-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/Ltac2" "Ltac2" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Rewriter" "Rewriter" "-top" "Top.bug_01") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 1498 lines to 11 lines, then from 24 lines to 324 lines, then from 329 lines to 52 lines, then from 65 lines to 384 lines, then from 389 lines to 57 lines, then from 70 lines to 840 lines, then from 845 lines to 118 lines, then from 131 lines to 380 lines, then from 385 lines to 130 lines, then from 143 lines to 339 lines, then from 344 lines to 132 lines, then from 150 lines to 132 lines, then from 145 lines to 478 lines, then from 484 lines to 255 lines, then from 269 lines to 501 lines, then from 506 lines to 351 lines, then from 365 lines to 694 lines, then from 699 lines to 825 lines, then from 833 lines to 357 lines, then from 370 lines to 564 lines, then from 570 lines to 377 lines, then from 391 lines to 987 lines, then from 992 lines to 377 lines, then from 391 lines to 3948 lines, then from 3948 lines to 4401 lines, then from 4405 lines to 389 lines, then from 402 lines to 615 lines, then from 621 lines to 464 lines, then from 478 lines to 431 lines, then from 444 lines to 700 lines, then from 706 lines to 435 lines, then from 449 lines to 476 lines, then from 482 lines to 549 lines, then from 567 lines to 439 lines, then from 452 lines to 668 lines, then from 674 lines to 440 lines, then from 454 lines to 524 lines, then from 530 lines to 442 lines, then from 456 lines to 475 lines, then from 481 lines to 475 lines *)
(* coqc version 8.18+alpha compiled with OCaml 4.14.1
coqtop version runner-vxtc-u6t-project-6138686-concurrent-0:/builds/coq/coq/_build/default,(HEAD detached at d7ce6d9) (d7ce6d9deac92848bd8420d857a18a96a87da88b)
Modules that could not be inlined: Rewriter.Util.plugins.RewriterBuildRegistry
Expected coqc runtime on this file: 7.475 sec *)
Require Coq.Init.Ltac.
Require Coq.Classes.Morphisms.
Require Rewriter.Util.GlobalSettings.
Require Rewriter.Util.FixCoqMistakes.
Require Rewriter.Util.Notations.
Require Ltac2.Init.
Require Coq.Lists.List.
Require Coq.Classes.RelationClasses.
Require Rewriter.Util.IffT.
Require Rewriter.Util.Isomorphism.
Require Rewriter.Util.HProp.
Require Rewriter.Util.Equality.
Require Rewriter.Util.PrimitiveProd.
Require Rewriter.Util.PrimitiveHList.
Require Rewriter.Util.InductiveHList.
Require Rewriter.Language.PreCommon.
Require Rewriter.Language.Pre.
Require Coq.Bool.Bool.
Require Rewriter.Util.Bool.
Require Coq.Logic.Eqdep_dec.
Require Coq.NArith.NArith.
Require Coq.Arith.Arith.
Require Coq.Numbers.Natural.Peano.NPeano.
Require Coq.Relations.Relation_Definitions.
Require Coq.micromega.Lia.
Require Rewriter.Util.NatUtil.
Require Coq.Lists.SetoidList.
Require Coq.Arith.Peano_dec.
Require Coq.ZArith.ZArith.
Require Coq.Numbers.BinNums.
Require Rewriter.Util.Pointed.
Require Rewriter.Util.plugins.RewriterBuildRegistry.
Ltac subst_evars :=
repeat match goal with
| [ e := ?E |- _ ] => is_evar E; subst e
end.
Import Coq.Lists.List.
Import Coq.Classes.Morphisms.
#[export] Instance Proper_filter_eq {A} : Proper ((eq ==> eq) ==> eq ==> eq) (@filter A).
Admitted.
Reserved Infix "<<" (at level 30, no associativity).
Reserved Infix ">>" (at level 30, no associativity).
Reserved Infix "&'" (at level 50).
Import Coq.ZArith.BinInt.
Infix ">>" := Z.shiftr : Z_scope.
Infix "<<" := Z.shiftl : Z_scope.
Infix "&'" := Z.land : Z_scope.
Class Decidable (P : Prop) := dec : {P} + {~P}.
Arguments dec _%type_scope {_}.
Notation DecidableRel R := (forall x y, Decidable (R x y)).
Global Instance dec_eq_Z : DecidableRel (@eq Z) | 10.
Admitted.
Local Open Scope Z_scope.
Module Export Z.
Definition zselect (cond zero_case nonzero_case : Z) :=
if cond =? 0 then zero_case else nonzero_case.
Definition add_modulo x y modulus :=
if (modulus <=? x + y) then (x + y) - modulus else (x + y).
Definition lnot_modulo (v : Z) (modulus : Z) : Z.
Admitted.
Definition bneg (v : Z) : Z.
Admitted.
Definition cc_m s x := if dec (2 ^ (Z.log2 s) = s) then x >> (Z.log2 s - 1) else x / (s / 2).
Definition rshi s hi lo n :=
let k := Z.log2 s in
if dec (2 ^ k = s)
then ((lo + (hi << k)) >> n) &' (Z.ones k)
else ((lo + hi * s) >> n) mod s.
Definition truncating_shiftl bw x n := (x << n) mod (2^bw).
Definition add_with_carry (c : Z) (x y : Z) : Z.
Admitted.
Definition add_get_carry_full (bound : Z) (x y : Z) : Z * Z.
Admitted.
Definition add_with_get_carry_full (bound : Z) (c x y : Z) : Z * Z.
Admitted.
Definition sub_get_borrow_full (bound : Z) (x y : Z) : Z * Z.
Admitted.
Definition sub_with_get_borrow_full (bound : Z) (c x y : Z) : Z * Z.
Admitted.
Definition mul_split (s x y : Z) : Z * Z.
Admitted.
Definition mul_high (s x y : Z) : Z.
Admitted.
Definition ltz (x y : Z) : Z.
Admitted.
Definition combine_at_bitwidth (bitwidth lo hi : Z) : Z.
Admitted.
Definition value_barrier (x : Z) := x.
Fixpoint update_nth {T} n f (xs:list T) {struct n} :=
match n with
| O => match xs with
| nil => nil
| x'::xs' => f x'::xs'
end
| S n' => match xs with
| nil => nil
| x'::xs' => x'::update_nth n' f xs'
end
end.
Import Coq.Bool.Bool.
Notation reflect_rel P b := (forall x y, reflect (P x y) (b x y)).
Module Export Crypto_DOT_Util_DOT_ZRange_WRAPPED.
Module Export ZRange.
Declare Scope zrange_scope.
Record zrange := { lower : Z ; upper : Z }.
Bind Scope zrange_scope with zrange.
Scheme Minimality for zrange Sort Type.
Definition zrange_beq (x y : zrange) : bool.
Admitted.
Global Instance reflect_zrange_eq : reflect_rel (@eq zrange) zrange_beq | 10.
Admitted.
End ZRange.
End Crypto_DOT_Util_DOT_ZRange_WRAPPED.
Module Export ZRange.
Definition normalize (v : zrange) : zrange.
Admitted.
Definition opp (v : zrange) : zrange.
Admitted.
Notation "- x" := (opp x) : zrange_scope.
Export Rewriter.Language.Pre.
Module Export ident.
Section cast.
Definition is_more_pos_than_neg (r : zrange) (v : BinInt.Z) : bool.
Admitted.
Let cast_outside_of_range (r : zrange) (v : BinInt.Z) : BinInt.Z.
Admitted.
Definition cast (r : zrange) (x : BinInt.Z)
:= let r := ZRange.normalize r in
if (lower r <=? x) && (x <=? upper r)
then x
else if is_more_pos_than_neg r x
then cast_outside_of_range r x
else -cast_outside_of_range (-r) (-x).
Definition cast2 (r : zrange * zrange) (x : BinInt.Z * BinInt.Z)
:= (cast (Datatypes.fst r) (Datatypes.fst x),
cast (Datatypes.snd r) (Datatypes.snd x)).
End cast.
Section comment.
Definition comment {A} (x : A) := tt.
Definition comment_no_keep {A} (x : A) := tt.
End comment.
Module Export fancy.
Module Export with_wordmax.
Section with_wordmax.
Context (log2wordmax : BinInt.Z).
Definition add (imm : Z) : Z * Z -> Z * Z.
Admitted.
Definition addc (imm : Z) : Z * Z * Z -> Z * Z.
Admitted.
Definition sub (imm : Z) : Z * Z -> Z * Z.
Admitted.
Definition subb (imm : Z) : Z * Z * Z -> Z * Z.
Admitted.
Definition mulll : Z * Z -> Z.
Admitted.
Definition mullh : Z * Z -> Z.
Admitted.
Definition mulhl : Z * Z -> Z.
Admitted.
Definition mulhh : Z * Z -> Z.
Admitted.
Definition selm : Z * Z * Z -> Z.
Admitted.
Definition rshi (n : Z) : Z * Z -> Z.
Admitted.
End with_wordmax.
End with_wordmax.
Definition add : (Z * Z) * (Z * Z) -> Z * Z
:= Eval cbv [with_wordmax.add] in fun x => with_wordmax.add (fst (fst x)) (snd (fst x)) (snd x).
Definition addc : (Z * Z) * (Z * Z * Z) -> Z * Z
:= Eval cbv [with_wordmax.addc] in fun x => with_wordmax.addc (fst (fst x)) (snd (fst x)) (snd x).
Definition sub : (Z * Z) * (Z * Z) -> Z * Z
:= Eval cbv [with_wordmax.sub] in fun x => with_wordmax.sub (fst (fst x)) (snd (fst x)) (snd x).
Definition subb : (Z * Z) * (Z * Z * Z) -> Z * Z
:= Eval cbv [with_wordmax.subb] in fun x => with_wordmax.subb (fst (fst x)) (snd (fst x)) (snd x).
Definition mulll : Z * (Z * Z) -> Z
:= Eval cbv [with_wordmax.mulll] in fun x => with_wordmax.mulll (fst x) (snd x).
Definition mullh : Z * (Z * Z) -> Z
:= Eval cbv [with_wordmax.mullh] in fun x => with_wordmax.mullh (fst x) (snd x).
Definition mulhl : Z * (Z * Z) -> Z
:= Eval cbv [with_wordmax.mulhl] in fun x => with_wordmax.mulhl (fst x) (snd x).
Definition mulhh : Z * (Z * Z) -> Z
:= Eval cbv [with_wordmax.mulhh] in fun x => with_wordmax.mulhh (fst x) (snd x).
Definition selm : Z * (Z * Z * Z) -> Z
:= Eval cbv [with_wordmax.selm] in fun x => with_wordmax.selm (fst x) (snd x).
Definition rshi : (Z * Z) * (Z * Z) -> Z
:= Eval cbv [with_wordmax.rshi] in fun x => with_wordmax.rshi (fst (fst x)) (snd (fst x)) (snd x).
Definition selc : Z * Z * Z -> Z.
Admitted.
Definition sell : Z * Z * Z -> Z.
Admitted.
Definition addm : Z * Z * Z -> Z.
Admitted.
Notation prod_rect_nodep := Rewriter.Util.Prod.prod_rect_nodep (only parsing).
Notation nat_rect_arrow_nodep := Rewriter.Util.NatUtil.nat_rect_arrow_nodep (only parsing).
Notation list_rect_arrow_nodep := Rewriter.Util.ListUtil.list_rect_arrow_nodep (only parsing).
Notation bool_rect_nodep := Rewriter.Util.Bool.bool_rect_nodep (only parsing).
Module Export Thunked.
Notation bool_rect := Rewriter.Util.Bool.Thunked.bool_rect (only parsing).
Notation list_rect := Rewriter.Util.ListUtil.Thunked.list_rect (only parsing).
Notation list_case := Rewriter.Util.ListUtil.Thunked.list_case (only parsing).
Notation nat_rect := Rewriter.Util.NatUtil.Thunked.nat_rect (only parsing).
Notation option_rect := Rewriter.Util.Option.Thunked.option_rect (only parsing).
Definition var_like_idents : InductiveHList.hlist.
Admitted.
Definition base_type_list_named : InductiveHList.hlist.
exact ([with_name Z BinInt.Z
; with_name bool Datatypes.bool
; with_name nat Datatypes.nat
; with_name zrange ZRange.zrange
; with_name string String.string]%hlist).
Defined.
Definition all_ident_named_interped : InductiveHList.hlist.
exact ([with_name ident_Literal (@ident.literal)
; with_name ident_comment (@ident.comment)
; with_name ident_comment_no_keep (@ident.comment_no_keep)
; with_name ident_value_barrier (@Z.value_barrier)
; with_name ident_Nat_succ Nat.succ
; with_name ident_Nat_pred Nat.pred
; with_name ident_Nat_max Nat.max
; with_name ident_Nat_mul Nat.mul
; with_name ident_Nat_add Nat.add
; with_name ident_Nat_sub Nat.sub
; with_name ident_Nat_eqb Nat.eqb
; with_name ident_nil (@Datatypes.nil)
; with_name ident_cons (@Datatypes.cons)
; with_name ident_tt Datatypes.tt
; with_name ident_pair (@Datatypes.pair)
; with_name ident_fst (@Datatypes.fst)
; with_name ident_snd (@Datatypes.snd)
; with_name ident_prod_rect (@prod_rect_nodep)
; with_name ident_bool_rect (@Thunked.bool_rect)
; with_name ident_bool_rect_nodep (@bool_rect_nodep)
; with_name ident_nat_rect (@Thunked.nat_rect)
; with_name ident_eager_nat_rect (ident.eagerly (@Thunked.nat_rect))
; with_name ident_nat_rect_arrow (@nat_rect_arrow_nodep)
; with_name ident_eager_nat_rect_arrow (ident.eagerly (@nat_rect_arrow_nodep))
; with_name ident_list_rect (@Thunked.list_rect)
; with_name ident_eager_list_rect (ident.eagerly (@Thunked.list_rect))
; with_name ident_list_rect_arrow (@list_rect_arrow_nodep)
; with_name ident_eager_list_rect_arrow (ident.eagerly (@list_rect_arrow_nodep))
; with_name ident_list_case (@Thunked.list_case)
; with_name ident_List_length (@List.length)
; with_name ident_List_seq (@List.seq)
; with_name ident_List_firstn (@List.firstn)
; with_name ident_List_skipn (@List.skipn)
; with_name ident_List_repeat (@repeat)
; with_name ident_List_combine (@List.combine)
; with_name ident_List_map (@List.map)
; with_name ident_List_app (@List.app)
; with_name ident_List_rev (@List.rev)
; with_name ident_List_flat_map (@List.flat_map)
; with_name ident_List_partition (@List.partition)
; with_name ident_List_filter (@List.filter)
; with_name ident_List_fold_right (@List.fold_right)
; with_name ident_List_update_nth (@update_nth)
; with_name ident_List_nth_default (@nth_default)
; with_name ident_eager_List_nth_default (ident.eagerly (@nth_default))
; with_name ident_Z_add Z.add
; with_name ident_Z_mul Z.mul
; with_name ident_Z_pow Z.pow
; with_name ident_Z_sub Z.sub
; with_name ident_Z_opp Z.opp
; with_name ident_Z_div Z.div
; with_name ident_Z_modulo Z.modulo
; with_name ident_Z_eqb Z.eqb
; with_name ident_Z_leb Z.leb
; with_name ident_Z_ltb Z.ltb
; with_name ident_Z_geb Z.geb
; with_name ident_Z_gtb Z.gtb
; with_name ident_Z_log2 Z.log2
; with_name ident_Z_log2_up Z.log2_up
; with_name ident_Z_of_nat Z.of_nat
; with_name ident_Z_to_nat Z.to_nat
; with_name ident_Z_shiftr Z.shiftr
; with_name ident_Z_shiftl Z.shiftl
; with_name ident_Z_land Z.land
; with_name ident_Z_lor Z.lor
; with_name ident_Z_min Z.min
; with_name ident_Z_max Z.max
; with_name ident_Z_mul_split Z.mul_split
; with_name ident_Z_mul_high Z.mul_high
; with_name ident_Z_add_get_carry Z.add_get_carry_full
; with_name ident_Z_add_with_carry Z.add_with_carry
; with_name ident_Z_add_with_get_carry Z.add_with_get_carry_full
; with_name ident_Z_sub_get_borrow Z.sub_get_borrow_full
; with_name ident_Z_sub_with_get_borrow Z.sub_with_get_borrow_full
; with_name ident_Z_ltz Z.ltz
; with_name ident_Z_zselect Z.zselect
; with_name ident_Z_add_modulo Z.add_modulo
; with_name ident_Z_truncating_shiftl Z.truncating_shiftl
; with_name ident_Z_bneg Z.bneg
; with_name ident_Z_lnot_modulo Z.lnot_modulo
; with_name ident_Z_lxor Z.lxor
; with_name ident_Z_rshi Z.rshi
; with_name ident_Z_cc_m Z.cc_m
; with_name ident_Z_combine_at_bitwidth Z.combine_at_bitwidth
; with_name ident_Z_cast ident.cast
; with_name ident_Z_cast2 ident.cast2
; with_name ident_Some (@Datatypes.Some)
; with_name ident_None (@Datatypes.None)
; with_name ident_option_rect (@Thunked.option_rect)
; with_name ident_Build_zrange ZRange.Build_zrange
; with_name ident_zrange_rect (@ZRange.zrange_rect_nodep)
; with_name ident_fancy_add ident.fancy.add
; with_name ident_fancy_addc ident.fancy.addc
; with_name ident_fancy_sub ident.fancy.sub
; with_name ident_fancy_subb ident.fancy.subb
; with_name ident_fancy_mulll ident.fancy.mulll
; with_name ident_fancy_mullh ident.fancy.mullh
; with_name ident_fancy_mulhl ident.fancy.mulhl
; with_name ident_fancy_mulhh ident.fancy.mulhh
; with_name ident_fancy_rshi ident.fancy.rshi
; with_name ident_fancy_selc ident.fancy.selc
; with_name ident_fancy_selm ident.fancy.selm
; with_name ident_fancy_sell ident.fancy.sell
; with_name ident_fancy_addm ident.fancy.addm
]%hlist).
Defined.
Definition scraped_data : ScrapedData.t.
exact ({| ScrapedData.base_type_list_named := base_type_list_named
; ScrapedData.all_ident_named_interped := all_ident_named_interped |}).
Defined.
Declare ML Module "coq-rewriter.rewriter_build".
Module Export Compilers.
Import IdentifiersBasicGenerate.Compilers.Basic.
Rewriter Emit Inductives From Scraped
{| ScrapedData.base_type_list_named := base_type_list_named ; ScrapedData.all_ident_named_interped := all_ident_named_interped |}
As base ident raw_ident pattern_ident.
Definition package : GoalType.package_with_args scraped_data var_like_idents base ident.
Proof.
Tactic.make_package.
Defined.
Module Export APINotations.
Import Ltac2.Ltac2.
Module Export Compilers.
Export Reify.Compilers.
Import IdentifiersBasicGenerate.Compilers.Basic.Tactic.
Definition exprInfo : Classes.ExprInfoT := Eval hnf in GoalType.exprInfo package.
Global Existing Instances
baseHasNat
baseHasNatCorrect
try_make_base_transport_cps_correct
buildEagerIdent
buildInterpEagerIdentCorrect
toRestrictedIdent
toFromRestrictedIdent
buildInterpIdentCorrect
invertIdent
buildInvertIdentCorrect
base_default
exprInfo
.
Ltac2 mk_reify_base_type () :=
let package := reify_package_of_package 'package in
reify_base_type_via_reify_package package.
Ltac2 mk_reify_type () :=
let package := reify_package_of_package 'package in
reify_type_via_reify_package package.
Ltac2 mk_reify_ident_opt () :=
let package := reify_package_of_package 'package in
reify_ident_via_reify_package_opt package.
Ltac2 reify_type (ty : constr) : constr := mk_reify_type () ty.
#[deprecated(since="8.15",note="Use Ltac2 instead.")]
Ltac reify_type term :=
let f := ltac2:(term
|- Control.refine (fun () => reify_type (Option.get (Ltac1.to_constr term)))) in
constr:(ltac:(f term)).
Module Export base.
Notation type := (@base.type base) (only parsing).
Notation base_interp := Compilers.base_interp (only parsing).
Notation interp := (base.interp Compilers.base_interp) (only parsing).
End base.
Ltac2 _Reify_rhs () : unit :=
let reify_base_type := mk_reify_base_type () in
let reify_ident_opt := mk_reify_ident_opt () in
expr._Reify_rhs 'base.type 'ident reify_base_type reify_ident_opt '@base.interp '@ident_interp ().
Ltac Reify_rhs _ :=
ltac2:(_Reify_rhs ()).
Module Import invert_expr.
End invert_expr.
End Compilers.
End APINotations.
Notation Expr := (@expr.Expr base.type ident).
Notation Interp := (@expr.Interp base.type ident base.interp (@ident_interp)).
Notation reify_type t := (ltac:(let rt := reify_type t in exact rt)) (only parsing).
Notation reify_type_of e := (reify_type ((fun t (_ : t) => t) _ e)) (only parsing).
Import Coq.Relations.Relation_Definitions.
Import Language.Wf.Compilers.
Fixpoint pointwise_equal {t} : relation (type.interp base.interp t)
:= match t with
| type.base t => Logic.eq
| type.arrow s d
=> fun (f g : type.interp base.interp s -> type.interp base.interp d)
=> forall x, pointwise_equal (f x) (g x)
end.
Definition is_reification_of' {t} (e : Expr t) (v : type.interp base.interp t) : Prop.
exact (pointwise_equal (Interp e) v /\ Wf e).
Defined.
Notation is_reification_of rop op
:= (match @is_reification_of' (reify_type_of op) rop op with
| T
=> ltac:(
let T := (eval cbv [pointwise_equal is_reification_of' T] in T) in
let T := (eval cbn [type.interp base.interp base.base_interp] in T) in
exact T)
end)
(only parsing).
Ltac cache_reify _ :=
split;
[ intros;
etransitivity;
[
| repeat match goal with |- _ = ?f' ?x => is_var x; apply (f_equal (fun f => f _)) end;
Reify_rhs ();
reflexivity ];
subst_evars;
reflexivity
| prove_Wf () ].
Import Coq.ZArith.ZArith.
Derive reified_id_gen
SuchThat (is_reification_of reified_id_gen (@id (list Z)))
As reified_id_gen_correct.
Proof.
Time cache_reify ().Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted) (truncated to 8.0KiB; full 28KiB file on GitHub Actions Artifacts under
|
|
Minimized File /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/src/PushButtonSynthesis/Primitives.v (from ci-fiat_crypto) (full log on GitHub Actions) We are collecting data on the user experience of the Coq Bug Minimizer. Partially Minimized Coq File (could not inline Rewriter.Util.plugins.RewriterBuildRegistry)(* -*- 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,unsupported-attributes" "-w" "-notation-overridden,-deprecated-hint-constr,-fragile-hint-constr,-native-compiler-disabled,-ambiguous-paths,-masking-absolute-name" "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" "-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/_build_ci/fiat_crypto/rupicola/bedrock2/deps/coqutil/src/coqutil" "coqutil" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/src/Rupicola" "Rupicola" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2" "bedrock2" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples" "bedrock2Examples" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/compiler/src/compiler" "compiler" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv" "riscv" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Bignums" "Bignums" "-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/Ltac2" "Ltac2" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Rewriter" "Rewriter" "-top" "Top.bug_01") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 1498 lines to 11 lines, then from 24 lines to 324 lines, then from 329 lines to 52 lines, then from 65 lines to 384 lines, then from 389 lines to 57 lines, then from 70 lines to 840 lines, then from 845 lines to 118 lines, then from 131 lines to 380 lines, then from 385 lines to 130 lines, then from 143 lines to 339 lines, then from 344 lines to 132 lines, then from 150 lines to 132 lines, then from 145 lines to 478 lines, then from 484 lines to 255 lines, then from 269 lines to 501 lines, then from 506 lines to 351 lines, then from 365 lines to 694 lines, then from 699 lines to 825 lines, then from 833 lines to 357 lines, then from 370 lines to 564 lines, then from 570 lines to 377 lines, then from 391 lines to 987 lines, then from 992 lines to 377 lines, then from 391 lines to 3948 lines, then from 3948 lines to 4401 lines, then from 4405 lines to 389 lines, then from 402 lines to 615 lines, then from 621 lines to 464 lines, then from 478 lines to 431 lines, then from 444 lines to 700 lines, then from 706 lines to 435 lines, then from 449 lines to 476 lines, then from 482 lines to 549 lines, then from 567 lines to 439 lines, then from 452 lines to 668 lines, then from 674 lines to 440 lines, then from 454 lines to 524 lines, then from 530 lines to 442 lines, then from 456 lines to 475 lines, then from 481 lines to 475 lines, then from 493 lines to 444 lines, then from 450 lines to 445 lines *)
(* coqc version 8.18+alpha compiled with OCaml 4.14.1
coqtop version runner-vxtc-u6t-project-6138686-concurrent-0:/builds/coq/coq/_build/default,(HEAD detached at d7ce6d9) (d7ce6d9deac92848bd8420d857a18a96a87da88b)
Modules that could not be inlined: Rewriter.Util.plugins.RewriterBuildRegistry
Expected coqc runtime on this file: 7.714 sec *)
Require Rewriter.Util.plugins.RewriterBuildRegistry.
Ltac subst_evars :=
repeat match goal with
| [ e := ?E |- _ ] => is_evar E; subst e
end.
Import Coq.Lists.List.
Import Coq.Classes.Morphisms.
#[export] Instance Proper_filter_eq {A} : Proper ((eq ==> eq) ==> eq ==> eq) (@filter A).
Admitted.
Reserved Infix "<<" (at level 30, no associativity).
Reserved Infix ">>" (at level 30, no associativity).
Reserved Infix "&'" (at level 50).
Import Coq.ZArith.BinInt.
Infix ">>" := Z.shiftr : Z_scope.
Infix "<<" := Z.shiftl : Z_scope.
Infix "&'" := Z.land : Z_scope.
Class Decidable (P : Prop) := dec : {P} + {~P}.
Arguments dec _%type_scope {_}.
Notation DecidableRel R := (forall x y, Decidable (R x y)).
Global Instance dec_eq_Z : DecidableRel (@eq Z) | 10.
Admitted.
Local Open Scope Z_scope.
Module Export Z.
Definition zselect (cond zero_case nonzero_case : Z) :=
if cond =? 0 then zero_case else nonzero_case.
Definition add_modulo x y modulus :=
if (modulus <=? x + y) then (x + y) - modulus else (x + y).
Definition lnot_modulo (v : Z) (modulus : Z) : Z.
Admitted.
Definition bneg (v : Z) : Z.
Admitted.
Definition cc_m s x := if dec (2 ^ (Z.log2 s) = s) then x >> (Z.log2 s - 1) else x / (s / 2).
Definition rshi s hi lo n :=
let k := Z.log2 s in
if dec (2 ^ k = s)
then ((lo + (hi << k)) >> n) &' (Z.ones k)
else ((lo + hi * s) >> n) mod s.
Definition truncating_shiftl bw x n := (x << n) mod (2^bw).
Definition add_with_carry (c : Z) (x y : Z) : Z.
Admitted.
Definition add_get_carry_full (bound : Z) (x y : Z) : Z * Z.
Admitted.
Definition add_with_get_carry_full (bound : Z) (c x y : Z) : Z * Z.
Admitted.
Definition sub_get_borrow_full (bound : Z) (x y : Z) : Z * Z.
Admitted.
Definition sub_with_get_borrow_full (bound : Z) (c x y : Z) : Z * Z.
Admitted.
Definition mul_split (s x y : Z) : Z * Z.
Admitted.
Definition mul_high (s x y : Z) : Z.
Admitted.
Definition ltz (x y : Z) : Z.
Admitted.
Definition combine_at_bitwidth (bitwidth lo hi : Z) : Z.
Admitted.
Definition value_barrier (x : Z) := x.
Fixpoint update_nth {T} n f (xs:list T) {struct n} :=
match n with
| O => match xs with
| nil => nil
| x'::xs' => f x'::xs'
end
| S n' => match xs with
| nil => nil
| x'::xs' => x'::update_nth n' f xs'
end
end.
Import Coq.Bool.Bool.
Notation reflect_rel P b := (forall x y, reflect (P x y) (b x y)).
Module Export Crypto_DOT_Util_DOT_ZRange_WRAPPED.
Module Export ZRange.
Declare Scope zrange_scope.
Record zrange := { lower : Z ; upper : Z }.
Bind Scope zrange_scope with zrange.
Scheme Minimality for zrange Sort Type.
Definition zrange_beq (x y : zrange) : bool.
Admitted.
Global Instance reflect_zrange_eq : reflect_rel (@eq zrange) zrange_beq | 10.
Admitted.
End ZRange.
End Crypto_DOT_Util_DOT_ZRange_WRAPPED.
Module Export ZRange.
Definition normalize (v : zrange) : zrange.
Admitted.
Definition opp (v : zrange) : zrange.
Admitted.
Notation "- x" := (opp x) : zrange_scope.
Export Rewriter.Language.Pre.
Module Export ident.
Section cast.
Definition is_more_pos_than_neg (r : zrange) (v : BinInt.Z) : bool.
Admitted.
Let cast_outside_of_range (r : zrange) (v : BinInt.Z) : BinInt.Z.
Admitted.
Definition cast (r : zrange) (x : BinInt.Z)
:= let r := ZRange.normalize r in
if (lower r <=? x) && (x <=? upper r)
then x
else if is_more_pos_than_neg r x
then cast_outside_of_range r x
else -cast_outside_of_range (-r) (-x).
Definition cast2 (r : zrange * zrange) (x : BinInt.Z * BinInt.Z)
:= (cast (Datatypes.fst r) (Datatypes.fst x),
cast (Datatypes.snd r) (Datatypes.snd x)).
End cast.
Section comment.
Definition comment {A} (x : A) := tt.
Definition comment_no_keep {A} (x : A) := tt.
End comment.
Module Export fancy.
Module Export with_wordmax.
Section with_wordmax.
Context (log2wordmax : BinInt.Z).
Definition add (imm : Z) : Z * Z -> Z * Z.
Admitted.
Definition addc (imm : Z) : Z * Z * Z -> Z * Z.
Admitted.
Definition sub (imm : Z) : Z * Z -> Z * Z.
Admitted.
Definition subb (imm : Z) : Z * Z * Z -> Z * Z.
Admitted.
Definition mulll : Z * Z -> Z.
Admitted.
Definition mullh : Z * Z -> Z.
Admitted.
Definition mulhl : Z * Z -> Z.
Admitted.
Definition mulhh : Z * Z -> Z.
Admitted.
Definition selm : Z * Z * Z -> Z.
Admitted.
Definition rshi (n : Z) : Z * Z -> Z.
Admitted.
End with_wordmax.
End with_wordmax.
Definition add : (Z * Z) * (Z * Z) -> Z * Z
:= Eval cbv [with_wordmax.add] in fun x => with_wordmax.add (fst (fst x)) (snd (fst x)) (snd x).
Definition addc : (Z * Z) * (Z * Z * Z) -> Z * Z
:= Eval cbv [with_wordmax.addc] in fun x => with_wordmax.addc (fst (fst x)) (snd (fst x)) (snd x).
Definition sub : (Z * Z) * (Z * Z) -> Z * Z
:= Eval cbv [with_wordmax.sub] in fun x => with_wordmax.sub (fst (fst x)) (snd (fst x)) (snd x).
Definition subb : (Z * Z) * (Z * Z * Z) -> Z * Z
:= Eval cbv [with_wordmax.subb] in fun x => with_wordmax.subb (fst (fst x)) (snd (fst x)) (snd x).
Definition mulll : Z * (Z * Z) -> Z
:= Eval cbv [with_wordmax.mulll] in fun x => with_wordmax.mulll (fst x) (snd x).
Definition mullh : Z * (Z * Z) -> Z
:= Eval cbv [with_wordmax.mullh] in fun x => with_wordmax.mullh (fst x) (snd x).
Definition mulhl : Z * (Z * Z) -> Z
:= Eval cbv [with_wordmax.mulhl] in fun x => with_wordmax.mulhl (fst x) (snd x).
Definition mulhh : Z * (Z * Z) -> Z
:= Eval cbv [with_wordmax.mulhh] in fun x => with_wordmax.mulhh (fst x) (snd x).
Definition selm : Z * (Z * Z * Z) -> Z
:= Eval cbv [with_wordmax.selm] in fun x => with_wordmax.selm (fst x) (snd x).
Definition rshi : (Z * Z) * (Z * Z) -> Z
:= Eval cbv [with_wordmax.rshi] in fun x => with_wordmax.rshi (fst (fst x)) (snd (fst x)) (snd x).
Definition selc : Z * Z * Z -> Z.
Admitted.
Definition sell : Z * Z * Z -> Z.
Admitted.
Definition addm : Z * Z * Z -> Z.
Admitted.
Notation prod_rect_nodep := Rewriter.Util.Prod.prod_rect_nodep (only parsing).
Notation nat_rect_arrow_nodep := Rewriter.Util.NatUtil.nat_rect_arrow_nodep (only parsing).
Notation list_rect_arrow_nodep := Rewriter.Util.ListUtil.list_rect_arrow_nodep (only parsing).
Notation bool_rect_nodep := Rewriter.Util.Bool.bool_rect_nodep (only parsing).
Module Export Thunked.
Notation bool_rect := Rewriter.Util.Bool.Thunked.bool_rect (only parsing).
Notation list_rect := Rewriter.Util.ListUtil.Thunked.list_rect (only parsing).
Notation list_case := Rewriter.Util.ListUtil.Thunked.list_case (only parsing).
Notation nat_rect := Rewriter.Util.NatUtil.Thunked.nat_rect (only parsing).
Notation option_rect := Rewriter.Util.Option.Thunked.option_rect (only parsing).
Definition var_like_idents : InductiveHList.hlist.
Admitted.
Definition base_type_list_named : InductiveHList.hlist.
exact ([with_name Z BinInt.Z
; with_name bool Datatypes.bool
; with_name nat Datatypes.nat
; with_name zrange ZRange.zrange
; with_name string String.string]%hlist).
Defined.
Definition all_ident_named_interped : InductiveHList.hlist.
exact ([with_name ident_Literal (@ident.literal)
; with_name ident_comment (@ident.comment)
; with_name ident_comment_no_keep (@ident.comment_no_keep)
; with_name ident_value_barrier (@Z.value_barrier)
; with_name ident_Nat_succ Nat.succ
; with_name ident_Nat_pred Nat.pred
; with_name ident_Nat_max Nat.max
; with_name ident_Nat_mul Nat.mul
; with_name ident_Nat_add Nat.add
; with_name ident_Nat_sub Nat.sub
; with_name ident_Nat_eqb Nat.eqb
; with_name ident_nil (@Datatypes.nil)
; with_name ident_cons (@Datatypes.cons)
; with_name ident_tt Datatypes.tt
; with_name ident_pair (@Datatypes.pair)
; with_name ident_fst (@Datatypes.fst)
; with_name ident_snd (@Datatypes.snd)
; with_name ident_prod_rect (@prod_rect_nodep)
; with_name ident_bool_rect (@Thunked.bool_rect)
; with_name ident_bool_rect_nodep (@bool_rect_nodep)
; with_name ident_nat_rect (@Thunked.nat_rect)
; with_name ident_eager_nat_rect (ident.eagerly (@Thunked.nat_rect))
; with_name ident_nat_rect_arrow (@nat_rect_arrow_nodep)
; with_name ident_eager_nat_rect_arrow (ident.eagerly (@nat_rect_arrow_nodep))
; with_name ident_list_rect (@Thunked.list_rect)
; with_name ident_eager_list_rect (ident.eagerly (@Thunked.list_rect))
; with_name ident_list_rect_arrow (@list_rect_arrow_nodep)
; with_name ident_eager_list_rect_arrow (ident.eagerly (@list_rect_arrow_nodep))
; with_name ident_list_case (@Thunked.list_case)
; with_name ident_List_length (@List.length)
; with_name ident_List_seq (@List.seq)
; with_name ident_List_firstn (@List.firstn)
; with_name ident_List_skipn (@List.skipn)
; with_name ident_List_repeat (@repeat)
; with_name ident_List_combine (@List.combine)
; with_name ident_List_map (@List.map)
; with_name ident_List_app (@List.app)
; with_name ident_List_rev (@List.rev)
; with_name ident_List_flat_map (@List.flat_map)
; with_name ident_List_partition (@List.partition)
; with_name ident_List_filter (@List.filter)
; with_name ident_List_fold_right (@List.fold_right)
; with_name ident_List_update_nth (@update_nth)
; with_name ident_List_nth_default (@nth_default)
; with_name ident_eager_List_nth_default (ident.eagerly (@nth_default))
; with_name ident_Z_add Z.add
; with_name ident_Z_mul Z.mul
; with_name ident_Z_pow Z.pow
; with_name ident_Z_sub Z.sub
; with_name ident_Z_opp Z.opp
; with_name ident_Z_div Z.div
; with_name ident_Z_modulo Z.modulo
; with_name ident_Z_eqb Z.eqb
; with_name ident_Z_leb Z.leb
; with_name ident_Z_ltb Z.ltb
; with_name ident_Z_geb Z.geb
; with_name ident_Z_gtb Z.gtb
; with_name ident_Z_log2 Z.log2
; with_name ident_Z_log2_up Z.log2_up
; with_name ident_Z_of_nat Z.of_nat
; with_name ident_Z_to_nat Z.to_nat
; with_name ident_Z_shiftr Z.shiftr
; with_name ident_Z_shiftl Z.shiftl
; with_name ident_Z_land Z.land
; with_name ident_Z_lor Z.lor
; with_name ident_Z_min Z.min
; with_name ident_Z_max Z.max
; with_name ident_Z_mul_split Z.mul_split
; with_name ident_Z_mul_high Z.mul_high
; with_name ident_Z_add_get_carry Z.add_get_carry_full
; with_name ident_Z_add_with_carry Z.add_with_carry
; with_name ident_Z_add_with_get_carry Z.add_with_get_carry_full
; with_name ident_Z_sub_get_borrow Z.sub_get_borrow_full
; with_name ident_Z_sub_with_get_borrow Z.sub_with_get_borrow_full
; with_name ident_Z_ltz Z.ltz
; with_name ident_Z_zselect Z.zselect
; with_name ident_Z_add_modulo Z.add_modulo
; with_name ident_Z_truncating_shiftl Z.truncating_shiftl
; with_name ident_Z_bneg Z.bneg
; with_name ident_Z_lnot_modulo Z.lnot_modulo
; with_name ident_Z_lxor Z.lxor
; with_name ident_Z_rshi Z.rshi
; with_name ident_Z_cc_m Z.cc_m
; with_name ident_Z_combine_at_bitwidth Z.combine_at_bitwidth
; with_name ident_Z_cast ident.cast
; with_name ident_Z_cast2 ident.cast2
; with_name ident_Some (@Datatypes.Some)
; with_name ident_None (@Datatypes.None)
; with_name ident_option_rect (@Thunked.option_rect)
; with_name ident_Build_zrange ZRange.Build_zrange
; with_name ident_zrange_rect (@ZRange.zrange_rect_nodep)
; with_name ident_fancy_add ident.fancy.add
; with_name ident_fancy_addc ident.fancy.addc
; with_name ident_fancy_sub ident.fancy.sub
; with_name ident_fancy_subb ident.fancy.subb
; with_name ident_fancy_mulll ident.fancy.mulll
; with_name ident_fancy_mullh ident.fancy.mullh
; with_name ident_fancy_mulhl ident.fancy.mulhl
; with_name ident_fancy_mulhh ident.fancy.mulhh
; with_name ident_fancy_rshi ident.fancy.rshi
; with_name ident_fancy_selc ident.fancy.selc
; with_name ident_fancy_selm ident.fancy.selm
; with_name ident_fancy_sell ident.fancy.sell
; with_name ident_fancy_addm ident.fancy.addm
]%hlist).
Defined.
Definition scraped_data : ScrapedData.t.
exact ({| ScrapedData.base_type_list_named := base_type_list_named
; ScrapedData.all_ident_named_interped := all_ident_named_interped |}).
Defined.
Declare ML Module "coq-rewriter.rewriter_build".
Module Export Compilers.
Import IdentifiersBasicGenerate.Compilers.Basic.
Rewriter Emit Inductives From Scraped
{| ScrapedData.base_type_list_named := base_type_list_named ; ScrapedData.all_ident_named_interped := all_ident_named_interped |}
As base ident raw_ident pattern_ident.
Definition package : GoalType.package_with_args scraped_data var_like_idents base ident.
Proof.
Tactic.make_package.
Defined.
Module Export APINotations.
Import Ltac2.Ltac2.
Module Export Compilers.
Export Reify.Compilers.
Import IdentifiersBasicGenerate.Compilers.Basic.Tactic.
Definition exprInfo : Classes.ExprInfoT := Eval hnf in GoalType.exprInfo package.
Global Existing Instances
baseHasNat
baseHasNatCorrect
try_make_base_transport_cps_correct
buildEagerIdent
buildInterpEagerIdentCorrect
toRestrictedIdent
toFromRestrictedIdent
buildInterpIdentCorrect
invertIdent
buildInvertIdentCorrect
base_default
exprInfo
.
Ltac2 mk_reify_base_type () :=
let package := reify_package_of_package 'package in
reify_base_type_via_reify_package package.
Ltac2 mk_reify_type () :=
let package := reify_package_of_package 'package in
reify_type_via_reify_package package.
Ltac2 mk_reify_ident_opt () :=
let package := reify_package_of_package 'package in
reify_ident_via_reify_package_opt package.
Ltac2 reify_type (ty : constr) : constr := mk_reify_type () ty.
#[deprecated(since="8.15",note="Use Ltac2 instead.")]
Ltac reify_type term :=
let f := ltac2:(term
|- Control.refine (fun () => reify_type (Option.get (Ltac1.to_constr term)))) in
constr:(ltac:(f term)).
Module Export base.
Notation type := (@base.type base) (only parsing).
Notation base_interp := Compilers.base_interp (only parsing).
Notation interp := (base.interp Compilers.base_interp) (only parsing).
End base.
Ltac2 _Reify_rhs () : unit :=
let reify_base_type := mk_reify_base_type () in
let reify_ident_opt := mk_reify_ident_opt () in
expr._Reify_rhs 'base.type 'ident reify_base_type reify_ident_opt '@base.interp '@ident_interp ().
Ltac Reify_rhs _ :=
ltac2:(_Reify_rhs ()).
Module Import invert_expr.
End invert_expr.
End Compilers.
End APINotations.
Notation Expr := (@expr.Expr base.type ident).
Notation Interp := (@expr.Interp base.type ident base.interp (@ident_interp)).
Notation reify_type t := (ltac:(let rt := reify_type t in exact rt)) (only parsing).
Notation reify_type_of e := (reify_type ((fun t (_ : t) => t) _ e)) (only parsing).
Import Coq.Relations.Relation_Definitions.
Import Language.Wf.Compilers.
Fixpoint pointwise_equal {t} : relation (type.interp base.interp t)
:= match t with
| type.base t => Logic.eq
| type.arrow s d
=> fun (f g : type.interp base.interp s -> type.interp base.interp d)
=> forall x, pointwise_equal (f x) (g x)
end.
Definition is_reification_of' {t} (e : Expr t) (v : type.interp base.interp t) : Prop.
exact (pointwise_equal (Interp e) v /\ Wf e).
Defined.
Notation is_reification_of rop op
:= (match @is_reification_of' (reify_type_of op) rop op with
| T
=> ltac:(
let T := (eval cbv [pointwise_equal is_reification_of' T] in T) in
let T := (eval cbn [type.interp base.interp base.base_interp] in T) in
exact T)
end)
(only parsing).
Ltac cache_reify _ :=
split;
[ intros;
etransitivity;
[
| repeat match goal with |- _ = ?f' ?x => is_var x; apply (f_equal (fun f => f _)) end;
Reify_rhs ();
reflexivity ];
subst_evars;
reflexivity
| prove_Wf () ].
Import Coq.ZArith.ZArith.
Derive reified_id_gen
SuchThat (is_reification_of reified_id_gen (@id (list Z)))
As reified_id_gen_correct.
Proof.
Time cache_reify ().Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted) (truncated to 8.0KiB; full 28KiB file on GitHub Actions Artifacts under
|
|
Further reduced I think it looks like Require Import Ltac2.Ltac2.
Goal tt = tt.
(* ' is open_constr *)
let x := '(eq_refl : tt = tt) in
abstract (Std.exact_no_check x).
Similarly Goal tt = tt.
let x := '(eq_refl : tt = tt) in
abstract (exact $x).produces anomaly evar not declared in this PR, and Require Import Ltac2.Ltac2.
Goal tt = tt.
let x := '_ in
let _ := '(eq_refl : $x = tt) in
abstract (exact $x).produces anomaly evar not declared in master. |
|
Ltac1 abstract runs Lines 318 to 333 in ba574c6 I guess we could have a notation It seems rewriter has only 1 use of abstract with non-closed tactic https://github.com/mit-plv/rewriter/blob/30653754f74caaa94e23d2e51ed9d839753f9d20/src/Rewriter/Language/Reify.v#L1034 If we consider that non-closed tactics in abstract are uncommon we could have cc @JasonGross |
SkySkimmer
force-pushed
the
open-constr-no-expand
branch
from
cecd173
to
ea7bb58
Compare
coqbot-app
bot
added
the
needs: full CI
|
What does "non-closed tactic" mean? Does this mean anything that references any Ltac2 variable? It seems unfriendly to not support this use case by default.
This seems okay to me if need be: AIUI, you only have to purge the bits of the environment that hold constr, and bool is fine to not purge. What happens to higher order tactics that are typed as, e.g., |
|
The tactic given to
It may be unfriendly but supporting it is broken.
It's hard to tell which bits that is though. And the only safe solution would be to purge everything we don't know about (by purge I mean remove from the environment btw). |
Why? Why is
I guess it's okay to say that any Ltac2 variable you want to reference must be mentioned to the left of |
The point of the |
I don't know. There may be perf consequences, or maybe it's just historical accident. |
I would guess historical accident, given that |
|
What's the design of |
|
It's relatively easy to make abstract support evars: modified vernac/declare.ml
@@ -1859,46 +1859,40 @@ let next = let n = ref 0 in fun () -> incr n; !n
let by tac = map_fold ~f:(Proof.solve (Goal_select.SelectNth 1) None tac)
-let build_constant_by_tactic ~name ?(opaque=Vernacexpr.Transparent) ~uctx ~sign ~poly (typ : EConstr.t) tac =
- let evd = Evd.from_ctx uctx in
+let build_constant_by_tactic ~name ?(opaque=Vernacexpr.Transparent) ~sigma ~sign ~poly (typ : EConstr.t) tac =
let typ_ = EConstr.Unsafe.to_constr typ in
let cinfo = [CInfo.make ~name ~typ:typ_ ()] in
let info = Info.make ~poly () in
let pinfo = Proof_info.make ~cinfo ~info () in
- let pf = start_proof_core ~name ~typ ~pinfo ~sign evd in
+ let pf = start_proof_core ~name ~typ ~pinfo ~sign sigma in
let pf, status = by tac pf in
let { entries; uctx } = close_proof ~opaque ~keep_body_ucst_separate:false pf in
+ let { Proof.sigma } = Proof.data pf.proof in
+ let sigma = Evd.set_universe_context sigma uctx in
match entries with
| [entry] ->
let entry = Internal.pmap_entry_body ~f:Future.force entry in
- entry, status, uctx
+ entry, status, sigma
| _ ->
CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term")
let build_by_tactic env ~uctx ~poly ~typ tac =
let name = Id.of_string ("temporary_proof"^string_of_int (next())) in
let sign = Environ.(val_of_named_context (named_context env)) in
- let ce, status, uctx = build_constant_by_tactic ~name ~uctx ~sign ~poly typ tac in
+ let sigma = Evd.from_ctx uctx in
+ let ce, status, sigma = build_constant_by_tactic ~name ~sigma ~sign ~poly typ tac in
+ let uctx = Evd.evar_universe_context sigma in
let cb, uctx = inline_private_constants ~uctx env ce in
cb, ce.proof_entry_type, ce.proof_entry_universes, status, uctx
let declare_abstract ~name ~poly ~kind ~sign ~secsign ~opaque ~solve_tac sigma concl =
- (* EJGA: flush_and_check_evars is only used in abstract, could we
- use a different API? *)
- let concl =
- try Evarutil.flush_and_check_evars sigma concl
- with Evarutil.Uninstantiated_evar _ ->
- CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials.")
- in
let sigma, concl =
(* FIXME: should be done only if the tactic succeeds *)
let sigma = Evd.minimize_universes sigma in
- sigma, Evarutil.nf_evars_universes sigma concl
+ sigma, Evarutil.nf_evar sigma concl
in
- let concl = EConstr.of_constr concl in
- let uctx = Evd.evar_universe_context sigma in
- let (const, safe, uctx) =
- try build_constant_by_tactic ~name ~opaque:Vernacexpr.Transparent ~poly ~uctx ~sign:secsign concl solve_tac
+ let (const, safe, sigma) =
+ try build_constant_by_tactic ~name ~opaque:Vernacexpr.Transparent ~poly ~sigma ~sign:secsign concl solve_tac
with Logic_monad.TacticFailure e as src ->
(* if the tactic [tac] fails, it reports a [TacticFailure e],
which is an error irrelevant to the proof system (in fact it
@@ -1907,7 +1901,6 @@ let declare_abstract ~name ~poly ~kind ~sign ~secsign ~opaque ~solve_tac sigma c
let (_, info) = Exninfo.capture src in
Exninfo.iraise (e, info)
in
- let sigma = Evd.set_universe_context sigma uctx in
let body, effs = const.proof_entry_body in
(* We drop the side-effects from the entry, they already exist in the ambient environment *)
let const = Internal.pmap_entry_body const ~f:(fun _ -> body, ()) in(although this patch causes it to warn that there are remaining goals (the surrounding proof) and error if a previous goal was admitted) The overall consequences are unclear. We could expose a primitive like Ltac2 abstract2 tac :=
let g := Control.goal() in
let c := constr:(ltac2:(tac) : $g) in
(* maybe a bit of Constr.Unsafe to remove the cast node? *)
let c := declare_private_constant true c in
exact_no_check cshould work |
SkySkimmer
added
the
request: full CI
SkySkimmer
force-pushed
the
open-constr-no-expand
branch
from
ea7bb58
to
03b92d9
Compare
coqbot-app
bot
removed
request: full CI
|
@coqbot bench |
|
🏁 Bench results: 🐢 Top 25 slow downs┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 54.3770 55.1980 0.8210 1.51% 609 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 64.6620 65.4120 0.7500 1.16% 361 coq-perennial/src/program_proof/buf/buf_proof.v.html │ │ 4.0530 4.7790 0.7260 17.91% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 112.6450 113.3470 0.7020 0.62% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 26.1180 26.7800 0.6620 2.53% 12 coq-fourcolor/theories/job554to562.v.html │ │ 8.3090 8.9580 0.6490 7.81% 1510 coq-perennial/src/program_proof/vrsm/configservice/config_proof.v.html │ │ 44.8660 45.5090 0.6430 1.43% 110 coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html │ │ 17.5410 18.1630 0.6220 3.55% 32 coq-performance-tests-lite/src/pattern.v.html │ │ 3.9410 4.5480 0.6070 15.40% 128 coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html │ │ 0.0040 0.4670 0.4630 11575.00% 753 coq-metacoq-pcuic/pcuic/theories/PCUICTyping.v.html │ │ 0.0030 0.4290 0.4260 14200.00% 1275 coq-metacoq-template/template-coq/theories/Typing.v.html │ │ 2.4360 2.8560 0.4200 17.24% 34 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 28.2930 28.7050 0.4120 1.46% 12 coq-fourcolor/theories/job499to502.v.html │ │ 113.0660 113.4720 0.4060 0.36% 968 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 29.6520 30.0470 0.3950 1.33% 12 coq-fourcolor/theories/job611to617.v.html │ │ 4.1880 4.5810 0.3930 9.38% 130 coq-category-theory/Functor/Strong/Product.v.html │ │ 160.0180 160.4090 0.3910 0.24% 233 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │ │ 0.0980 0.4710 0.3730 380.61% 1011 coq-perennial/src/program_proof/vrsm/storage/proof.v.html │ │ 24.9930 25.3580 0.3650 1.46% 12 coq-fourcolor/theories/job384to398.v.html │ │ 1.0210 1.3780 0.3570 34.97% 853 coq-stdlib/FSets/FMapAVL.v.html │ │ 0.2000 0.5490 0.3490 174.50% 1732 coq-perennial/src/program_proof/vrsm/apps/exactlyonce/proof.v.html │ │ 2.4790 2.8270 0.3480 14.04% 487 coq-stdlib/Numbers/HexadecimalFacts.v.html │ │ 4.4890 4.8140 0.3250 7.24% 102 coq-engine-bench-lite/coq/PerformanceDemos/rewrite_strat_repeated_app.v.html │ │ 54.6600 54.9820 0.3220 0.59% 609 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 2.8280 3.1480 0.3200 11.32% 475 coq-vst/veric/binop_lemmas3.v.html │ └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 19.2550 17.5520 -1.7030 -8.84% 376 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvMetric.v.html │ │ 23.7900 22.2060 -1.5840 -6.66% 660 coq-perennial/src/program_proof/vrsm/replica/roapply_proof.v.html │ │ 91.7580 91.0930 -0.6650 -0.72% 103 coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html │ │ 2.3810 1.7470 -0.6340 -26.63% 209 coq-stdlib/setoid_ring/Ncring_tac.v.html │ │ 127.6120 127.0230 -0.5890 -0.46% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 61.0310 60.4640 -0.5670 -0.93% 27 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html │ │ 7.8500 7.2890 -0.5610 -7.15% 288 coq-perennial/src/program_proof/vrsm/paxos/becomeleader_proof.v.html │ │ 32.7270 32.2150 -0.5120 -1.56% 12 coq-fourcolor/theories/job107to164.v.html │ │ 142.4220 141.9130 -0.5090 -0.36% 1190 coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html │ │ 113.9300 113.4430 -0.4870 -0.43% 48 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 27.4700 27.0050 -0.4650 -1.69% 823 coq-perennial/src/program_proof/aof/proof.v.html │ │ 16.8190 16.3850 -0.4340 -2.58% 483 coq-verdi-raft/raft-proofs/EndToEndLinearizability.v.html │ │ 24.1370 23.7190 -0.4180 -1.73% 1449 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Examples/KleisliEnriched.v.html │ │ 18.0330 17.6220 -0.4110 -2.28% 31 coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html │ │ 31.7300 31.3200 -0.4100 -1.29% 839 coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html │ │ 53.3350 52.9580 -0.3770 -0.71% 50 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 0.4710 0.0970 -0.3740 -79.41% 1699 coq-perennial/src/program_proof/vrsm/configservice/config_proof.v.html │ │ 0.6250 0.2550 -0.3700 -59.20% 1009 coq-perennial/src/program_proof/vrsm/storage/proof.v.html │ │ 22.8060 22.4400 -0.3660 -1.60% 233 coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html │ │ 21.2160 20.8500 -0.3660 -1.73% 12 coq-fourcolor/theories/job311to314.v.html │ │ 0.4930 0.1400 -0.3530 -71.60% 1734 coq-perennial/src/program_proof/vrsm/apps/exactlyonce/proof.v.html │ │ 0.9450 0.5950 -0.3500 -37.04% 170 coq-stdlib/Numbers/HexadecimalNat.v.html │ │ 30.4190 30.0920 -0.3270 -1.07% 12 coq-fourcolor/theories/job190to206.v.html │ │ 0.9190 0.5950 -0.3240 -35.26% 877 coq-metacoq-pcuic/pcuic/theories/PCUICTyping.v.html │ │ 20.8860 20.5840 -0.3020 -1.45% 12 coq-fourcolor/theories/job271to278.v.html │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
SkySkimmer
added
kind: performance
SkySkimmer
removed
the
needs: changelog entry
SkySkimmer
force-pushed
the
open-constr-no-expand
branch
from
03b92d9
to
2207de7
Compare
coqbot-app
bot
added
the
needs: full CI
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
This comment was marked as off-topic.
This comment was marked as off-topic.
ppedrot
approved these changes
Nov 8, 2023
|
@coqbot merge now |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Close? #13977
Unlike #17346 we still expand in
constr:(), hopefully we trigger less bugs this way.